Raghav/unsupported warn

include/Verification/Utils.h

@@ -7,8 +7,20 @@
 
 #include <llvm/Support/LogicalResult.h>
 #include <llzk/Dialect/Struct/IR/Ops.h>
+#include <mlir/Transforms/LocationSnapshot.h>
+#include <stdexcept>
 
 namespace lleq::util {
+
+class UnsupportedConstruct : public std::runtime_error {
+  mlir::Location loc;
+
+public:
+  UnsupportedConstruct(mlir::Location errorLoc, const std::string &message)
+      : std::runtime_error{message}, loc{errorLoc} {}
+  mlir::Location getLoc() const { return loc; }
+};
+
 /// Run product alignment on the module if no @product function is found; errors
 /// if product alignment failed
 void ensureProductFunc(mlir::ModuleOp module,

include/Verification/WeakestPrecondition.h

@@ -8,6 +8,7 @@
 #include "Verification/TermUtils.h"
 #include <cvc5/cvc5.h>
 
+#include <llvm/Support/Error.h>
 #include <llvm/Support/LogicalResult.h>
 #include <llvm/Support/raw_ostream.h>
 #include <llzk/Dialect/Array/IR/Ops.h>
@@ -58,8 +59,8 @@ class WeakestPreconditionAnalysis {
     });
   }
 
-  llvm::FailureOr<cvc5::Term>
-  computeInvariant(mlir::scf::ForOp loop, const ConjunctionTerm &postcondition);
+  cvc5::Term computeInvariant(mlir::scf::ForOp loop,
+                              const ConjunctionTerm &postcondition);
 
 public:
   WeakestPreconditionAnalysis(llzk::component::StructDefOp structDef,
@@ -69,7 +70,6 @@ class WeakestPreconditionAnalysis {
   }
 
   ImplicationTerm getPostcondition();
-  void populateVerificationConditions();
   cvc5::Term generateVerificationConditions();
 
   void applyStructContract(llzk::verif::ContractOp contract);

lib/Verification/TermUtils.cpp

@@ -406,24 +406,29 @@ cvc5::Term TermBuilder::getExpression(mlir::Value value) {
             return mgr.mkTerm(cvc5::Kind::ITE,
                               {condition, trueValue, falseValue});
           })
-          .Case<scf::ForOp>([this](auto) -> cvc5::Term {
-            llvm::report_fatal_error("loop-yielded values not yet supported");
+          .Case<scf::ForOp>([this](auto op) -> cvc5::Term {
+            throw util::UnsupportedConstruct(op->getLoc(),
+                                             "loop-yielded values");
           })
           .Case<function::CallOp>([this](function::CallOp call) {
             // For now just deal with calls to @compute and error out on other
             // function calls
             SymbolTableCollection tables;
-            ensure(call.calleeIsStructCompute() || call.calleeIsStructProduct(),
-                   "arbitrary function calls not supported yet");
+            if (!call.calleeIsStructCompute() &&
+                !call.calleeIsStructProduct()) {
+              throw util::UnsupportedConstruct(call->getLoc(),
+                                               "arbitrary function calls");
+            }
+
             auto target = call.getCalleeTarget(tables);
             ensure(succeeded(target), "failed to resolve callee target");
             SmallVector<Value> args = call.getArgOperands();
             return initSubcmp(
                 target->get()->getParentOfType<component::StructDefOp>(), args);
           })
           .Default([op](auto) -> cvc5::Term {
-            llvm::report_fatal_error("unknown op: " +
-                                     op->getName().getStringRef());
+            throw util::UnsupportedConstruct(
+                op->getLoc(), ("op: " + op->getName().getStringRef()).str());
           });
 
   expressions.insert({value, expression});

lib/Verification/WeakestPrecondition.cpp

@@ -16,6 +16,7 @@
 #include <llvm/ADT/SmallVectorExtras.h>
 #include <llvm/ADT/StringMap.h>
 #include <llvm/ADT/TypeSwitch.h>
+#include <llvm/Support/Error.h>
 
 #include <llvm/Support/Casting.h>
 #include <llvm/Support/Debug.h>
@@ -225,7 +226,7 @@ FailingCore getFailingCore(cvc5::Term invariant,
 
 } // namespace
 
-FailureOr<cvc5::Term> WeakestPreconditionAnalysis::computeInvariant(
+cvc5::Term WeakestPreconditionAnalysis::computeInvariant(
     scf::ForOp loop, const ConjunctionTerm &postcondition) {
   SmallVector<LoopCounterInfo> loopInfo;
   auto *body = nestedLoopBody(loop, loopInfo, builder);
@@ -464,12 +465,13 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
                                               ConjunctionTerm &postcondition) {
   llvm::TypeSwitch<mlir::Operation *, void>(op)
       .Case<component::CreateStructOp>(
-          [&postcondition](auto) { return postcondition; })
+          [](auto) { return llvm::Error::success(); })
       .Case<MemberWriteOp>([this, &postcondition](MemberWriteOp writeOp) {
         postcondition.addAntecedent(builder.assertEqual(
             builder.getConstant(writeOp.getMemberDefOp(tables)->get(),
                                 /*isWitness=*/true),
             writeOp.getVal()));
+        return llvm::Error::success();
       })
       .Case<WriteArrayOp>([this, &postcondition](WriteArrayOp writeOp) {
         auto arr = writeOp.getArrRef();
@@ -480,10 +482,26 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
         if (valueIsMemberRead(arr, tables) || valueIsMemberWrite(arr, tables)) {
           postcondition.addAntecedent(
               builder.assertEqual(builder.arrayRead(arr, indices), value));
-          return;
+          return llvm::Error::success();
         }
         postcondition.substitute(builder.getConstant(arr),
                                  builder.arrayWrite(arr, indices, value));
+        return llvm::Error::success();
+      })
+      .Case<constrain::EmitEqualityOp>([this,
+                                        &postcondition](EmitEqualityOp eqOp) {
+        // XXX: If one side of the equality is a Bool
+        // and the other side is a constant `1`, then instead of asserting
+        // equality just directly assert the Bool. This is a hack until the
+        // SMT encoding can deal with this correctly.
+        if (auto assertedBool = getAssertedBool(eqOp.getLhs(), eqOp.getRhs());
+            succeeded(assertedBool)) {
+          postcondition.addAntecedent(builder.getExpression(*assertedBool));
+        } else {
+          postcondition.addAntecedent(
+              builder.assertEqual(eqOp.getLhs(), eqOp.getRhs()));
+        }
+        return llvm::Error::success();
       })
       .Case<constrain::EmitEqualityOp>([this,
                                         &postcondition](EmitEqualityOp eqOp) {
@@ -500,21 +518,22 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
         }
       })
       .Case<scf::IfOp>([this, &postcondition](scf::IfOp op) {
-        calculateWP(op, postcondition);
+        return calculateWP(op, postcondition);
       })
-      .Case<UnrealizedConversionCastOp>([this](auto) { return; })
+      .Case<UnrealizedConversionCastOp>(
+          [this](auto) { return llvm::Error::success(); })
       .Case<scf::ForOp>([this, &postcondition](scf::ForOp op) {
         auto invariant = computeInvariant(op, postcondition);
-        llzk::ensure(succeeded(invariant),
-                     "failed to infer invariant for loop");
         // It should already be the case that invariant => postcondition
-        postcondition = ConjunctionTerm::of(*invariant);
+        postcondition = ConjunctionTerm::of(invariant);
       })
       .Case<boolean::AssertOp>([this, &postcondition](boolean::AssertOp op) {
         postcondition.addAntecedent(builder.getExpression(op.getCondition()));
+        return llvm::Error::success();
       })
       .Case<smt::AssertOp>([this, &postcondition](smt::AssertOp op) {
         postcondition.addAntecedent(builder.getExpression(op.getInput()));
+        return llvm::Error::success();
       })
       .Case<llzk::function::CallOp>([this, &postcondition](
                                         llzk::function::CallOp call) {
@@ -533,12 +552,13 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op,
           auto expression = builder.getExpression(call.getResult(0));
           postcondition.substitute(builder.getConstant(call->getResult(0)),
                                    expression);
-        } else {
-          // Technically a call to @product has already aligned the subcomponent
-          // values so there's nothing to prove
-          llzk::ensure(call.calleeIsStructProduct(),
-                       "arbitrary function calls not supported");
+        } else if (!call.calleeIsStructProduct()) {
+          // Technically a call to @product has already aligned the
+          // subcomponent values so there's nothing to prove
+          throw util::UnsupportedConstruct(call->getLoc(),
+                                           "arbitrary function calls");
         }
+        return llvm::Error::success();
       })
       .Default([this, &postcondition](auto op) {
         // The default case is just an expression op, but we shouldn't have to
@@ -594,9 +614,8 @@ SmallVector<cvc5::Term> getArrayExtents(array::ArrayType type,
 
 ImplicationTerm WeakestPreconditionAnalysis::getPostcondition() {
 
+  // The caller already checks for zero members, so no need to do it again
   auto members = structDef.getMemberDefs();
-  llzk::ensure(!members.empty(),
-               "cannot build postcondition for struct with empty members");
 
   SmallVector<cvc5::Term> memberEquivs;
   SmallVector<std::optional<Annotation>> annotations;
@@ -620,21 +639,13 @@ ImplicationTerm WeakestPreconditionAnalysis::getPostcondition() {
   return ImplicationTerm{{}, memberEquivs, annotations};
 }
 
-void WeakestPreconditionAnalysis::populateVerificationConditions() {
-  util::ensureProductFunc(structDef->getParentOfType<ModuleOp>(), structDef);
-
-  auto postcondition = ConjunctionTerm::of(getPostcondition());
-  calculateWP(&structDef.getProductFuncOp().getFunctionBody().front(),
-              postcondition);
-
-  verificationConditions = postcondition.buildTerm(mgr);
-  extraDecls = builder.getExtraDecls(verificationConditions);
-  declBounds = builder.getDeclBounds(extraDecls, field.prime());
-}
-
 cvc5::Term WeakestPreconditionAnalysis::generateVerificationConditions() {
   util::ensureProductFunc(structDef->getParentOfType<ModuleOp>(), structDef);
 
+  if (structDef.getMemberDefs().empty()) {
+    throw util::UnsupportedConstruct(structDef->getLoc(),
+                                     "struct without members");
+  }
   auto postcondition = ConjunctionTerm::of(getPostcondition());
   calculateWP(&structDef.getProductFuncOp().getFunctionBody().front(),
               postcondition);
@@ -643,28 +654,33 @@ cvc5::Term WeakestPreconditionAnalysis::generateVerificationConditions() {
 }
 
 void WeakestPreconditionAnalysis::emit(llvm::raw_ostream &os) {
-  auto verificationConditions = generateVerificationConditions();
-  auto extraDecls = builder.getExtraDecls(verificationConditions);
-  auto bounds = builder.getDeclBounds(extraDecls, field.prime());
-
-  os << "(set-logic ALL)\n";
-  builder.emitSubcmpDeclarations(os);
+  try {
+    cvc5::Term verificationConditions = generateVerificationConditions();
+    auto extraDecls = builder.getExtraDecls(verificationConditions);
+    auto bounds = builder.getDeclBounds(extraDecls, field.prime());
+
+    os << "(set-logic ALL)\n";
+    builder.emitSubcmpDeclarations(os);
+
+    os << "; Extra declarations\n";
+    for (auto decl : extraDecls) {
+      os << "(declare-const " << decl.toString() << " "
+         << decl.getSort().toString() << ")\n";
+    }
 
-  os << "; Extra declarations\n";
-  for (auto decl : extraDecls) {
-    os << "(declare-const " << decl.toString() << " "
-       << decl.getSort().toString() << ")\n";
-  }
+    os << "; Extra bounds\n";
+    for (auto bound : bounds) {
+      os << "(assert " << bound.toString() << ")\n";
+    }
 
-  os << "; Extra bounds\n";
-  for (auto bound : bounds) {
-    os << "(assert " << bound.toString() << ")\n";
+    os << "; Verification condition\n";
+    os << "(assert " << verificationConditions.notTerm().toString() << ")\n";
+    os << "(check-sat)\n";
+    os << "(get-model)\n";
+  } catch (const util::UnsupportedConstruct &exception) {
+    mlir::emitError(exception.getLoc()) << "Unsupported: " << exception.what();
+    return;
   }
-
-  os << "; Verification condition\n";
-  os << "(assert " << verificationConditions.notTerm().toString() << ")\n";
-  os << "(check-sat)\n";
-  os << "(get-model)\n";
 }
 
 } // namespace lleq

scripts/collect_circom_demo_results.py

@@ -22,6 +22,15 @@
 SAT_RE = re.compile(r"^\s*sat\s*$", re.MULTILINE)
 UNSAT_RE = re.compile(r"^\s*unsat\s*$", re.MULTILINE)
 UNKNOWN_RE = re.compile(r"^\s*unknown\s*$", re.MULTILINE)
+UNSUPPORTED_ERROR_RE = re.compile(
+    r"^error: .*?:Unsupported:",
+    re.MULTILINE,
+)
+
+
+def has_unsupported_error(stderr: str) -> bool:
+    """Return whether LLEQ reported an unsupported construct diagnostic."""
+    return UNSUPPORTED_ERROR_RE.search(stderr) is not None
 
 
 def get_benchmarks(benchmark_dir: pathlib.Path) -> list[tuple[str, pathlib.Path, str]]:
@@ -73,6 +82,9 @@ def run_verify(
         )
 
     elapsed = time.perf_counter() - start
+    if has_unsupported_error(proc.stderr):
+        message = proc.stderr.strip()[:500]
+        return (benchmark, root_struct, "verify", "unsupported", f"{elapsed:.6f}", message)
     if proc.returncode != 0:
         message = (proc.stderr or proc.stdout).strip()[:500]
         return (benchmark, root_struct, "verify", "error", f"{elapsed:.6f}", message)
@@ -150,6 +162,16 @@ def run_wp(
         return (benchmark, root_struct, "wp", "timeout", f"{elapsed:.6f}", "timeout")
 
     elapsed = time.perf_counter() - start
+    if has_unsupported_error(lleq_stderr):
+        message = lleq_stderr.strip()[:500]
+        return (
+            benchmark,
+            root_struct,
+            "wp",
+            "unsupported",
+            f"{elapsed:.6f}",
+            message,
+        )
     if lleq_proc.returncode != 0:
         message = (lleq_stderr or lleq_stdout).strip()[:500]
         return (benchmark, root_struct, "wp", "error", f"{elapsed:.6f}", message)
@@ -291,13 +313,14 @@ def main() -> None:
         "counterexample": 0,
         "partial": 0,
         "timeout": 0,
+        "unsupported": 0,
         "error": 0,
     }
     for _, _, _, result, _, _ in results:
         counts[result] += 1
 
     print(
-        "verified: {verified}, counterexample: {counterexample}, partial: {partial}, timeout: {timeout}, error: {error}".format(
+        "verified: {verified}, counterexample: {counterexample}, partial: {partial}, timeout: {timeout}, unsupported: {unsupported}, error: {error}".format(
             **counts
         )
     )

scripts/lleq_eval.py

@@ -8,6 +8,14 @@
 import time
 
 ENTRYPOINT_RE = re.compile(r'module attributes {.*llzk\.main\s+=\s+\!struct.type<@([A-Za-z0-9_]+).*>}', re.ASCII)
+UNSUPPORTED_ERROR_RE = re.compile(r"^error: .*?:Unsupported:", re.MULTILINE)
+
+
+def has_unsupported_error(stderr: str) -> bool:
+    """Return whether a tool reported an unsupported construct diagnostic."""
+    return UNSUPPORTED_ERROR_RE.search(stderr) is not None
+
+
 def get_llzk_files(benchmark_dir: str) -> list[tuple[str, str, str]]:
     root = pathlib.Path(benchmark_dir)
 
@@ -32,7 +40,7 @@ def run_task(benchmark_name: str, args: list[str], timeout: int) -> tuple[str, s
     try:
         proc = subprocess.run(args, capture_output=True, text=True, timeout=timeout)
         elapsed = time.perf_counter() - start
-        if proc.returncode == 0:
+        if proc.returncode == 0 and not has_unsupported_error(proc.stderr):
             return (benchmark_name, 'success', f'{elapsed:.6f}', '')
         error_msg = proc.stderr.strip()[:500]
         return (benchmark_name, 'error', f'{elapsed:.6f}', error_msg)
@@ -87,5 +95,3 @@ def build_tasks(benchmarks: list[tuple[str, str, str]], llzk_bin: str, lleq_bin:
         writer.writerow(["Benchmark", "Result", "Time Seconds", "Error Message"])
         writer.writerows(results)
     print(f"success: {success_cnt}, errored: {error_cnt}, timeout: {timeout_cnt}")
-
-