diff --git a/include/Verification/Utils.h b/include/Verification/Utils.h index b4a0254..96488a0 100644 --- a/include/Verification/Utils.h +++ b/include/Verification/Utils.h @@ -7,8 +7,20 @@ #include #include +#include +#include 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, diff --git a/include/Verification/WeakestPrecondition.h b/include/Verification/WeakestPrecondition.h index 79e956c..63c6c96 100644 --- a/include/Verification/WeakestPrecondition.h +++ b/include/Verification/WeakestPrecondition.h @@ -8,6 +8,7 @@ #include "Verification/TermUtils.h" #include +#include #include #include #include @@ -58,8 +59,8 @@ class WeakestPreconditionAnalysis { }); } - llvm::FailureOr - 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); diff --git a/lib/Verification/TermUtils.cpp b/lib/Verification/TermUtils.cpp index 5f9cddf..1f77d5c 100644 --- a/lib/Verification/TermUtils.cpp +++ b/lib/Verification/TermUtils.cpp @@ -406,15 +406,20 @@ cvc5::Term TermBuilder::getExpression(mlir::Value value) { return mgr.mkTerm(cvc5::Kind::ITE, {condition, trueValue, falseValue}); }) - .Case([this](auto) -> cvc5::Term { - llvm::report_fatal_error("loop-yielded values not yet supported"); + .Case([this](auto op) -> cvc5::Term { + throw util::UnsupportedConstruct(op->getLoc(), + "loop-yielded values"); }) .Case([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 args = call.getArgOperands(); @@ -422,8 +427,8 @@ cvc5::Term TermBuilder::getExpression(mlir::Value value) { target->get()->getParentOfType(), 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}); diff --git a/lib/Verification/WeakestPrecondition.cpp b/lib/Verification/WeakestPrecondition.cpp index 5c056c7..3f426f4 100644 --- a/lib/Verification/WeakestPrecondition.cpp +++ b/lib/Verification/WeakestPrecondition.cpp @@ -16,6 +16,7 @@ #include #include #include +#include #include #include @@ -225,7 +226,7 @@ FailingCore getFailingCore(cvc5::Term invariant, } // namespace -FailureOr WeakestPreconditionAnalysis::computeInvariant( +cvc5::Term WeakestPreconditionAnalysis::computeInvariant( scf::ForOp loop, const ConjunctionTerm &postcondition) { SmallVector loopInfo; auto *body = nestedLoopBody(loop, loopInfo, builder); @@ -464,12 +465,13 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op, ConjunctionTerm &postcondition) { llvm::TypeSwitch(op) .Case( - [&postcondition](auto) { return postcondition; }) + [](auto) { return llvm::Error::success(); }) .Case([this, &postcondition](MemberWriteOp writeOp) { postcondition.addAntecedent(builder.assertEqual( builder.getConstant(writeOp.getMemberDefOp(tables)->get(), /*isWitness=*/true), writeOp.getVal())); + return llvm::Error::success(); }) .Case([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([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([this, &postcondition](EmitEqualityOp eqOp) { @@ -500,21 +518,22 @@ void WeakestPreconditionAnalysis::calculateWP(Operation *op, } }) .Case([this, &postcondition](scf::IfOp op) { - calculateWP(op, postcondition); + return calculateWP(op, postcondition); }) - .Case([this](auto) { return; }) + .Case( + [this](auto) { return llvm::Error::success(); }) .Case([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([this, &postcondition](boolean::AssertOp op) { postcondition.addAntecedent(builder.getExpression(op.getCondition())); + return llvm::Error::success(); }) .Case([this, &postcondition](smt::AssertOp op) { postcondition.addAntecedent(builder.getExpression(op.getInput())); + return llvm::Error::success(); }) .Case([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 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 memberEquivs; SmallVector> annotations; @@ -620,21 +639,13 @@ ImplicationTerm WeakestPreconditionAnalysis::getPostcondition() { return ImplicationTerm{{}, memberEquivs, annotations}; } -void WeakestPreconditionAnalysis::populateVerificationConditions() { - util::ensureProductFunc(structDef->getParentOfType(), 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(), 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 diff --git a/scripts/collect_circom_demo_results.py b/scripts/collect_circom_demo_results.py index b1e9abc..cae0443 100644 --- a/scripts/collect_circom_demo_results.py +++ b/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 ) ) diff --git a/scripts/lleq_eval.py b/scripts/lleq_eval.py index 548653d..0cee1b7 100644 --- a/scripts/lleq_eval.py +++ b/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}") - -