From 06219bf1e337856e8cf8824ada213e0130ce1da2 Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Thu, 15 Jan 2026 20:28:24 -0600 Subject: [PATCH 1/4] Create temp directory for dumping SMT file names; add a new debug verbose option --- Strata/DL/Imperative/SMTUtils.lean | 9 ---- Strata/Languages/Boogie/Boogie.lean | 5 +-- Strata/Languages/Boogie/Options.lean | 41 +++++++++++++++++-- Strata/Languages/Boogie/Verifier.lean | 37 +++++++++-------- StrataMain.lean | 3 +- StrataTest/DL/Imperative/Examples.lean | 3 -- StrataTest/DL/Imperative/Verify.lean | 4 +- .../Boogie/Examples/AdvancedMaps.lean | 8 ---- .../Boogie/Examples/AdvancedQuantifiers.lean | 2 - .../Examples/AssertionDefaultNames.lean | 1 - .../Languages/Boogie/Examples/Axioms.lean | 5 --- .../Boogie/Examples/BitVecParse.lean | 1 - .../Boogie/Examples/FailingAssertion.lean | 1 - .../Boogie/Examples/FreeRequireEnsure.lean | 2 - .../Languages/Boogie/Examples/Functions.lean | 1 - .../Boogie/Examples/GeneratedLabels.lean | 1 - .../Languages/Boogie/Examples/Goto.lean | 2 - .../Languages/Boogie/Examples/Havoc.lean | 1 - .../Languages/Boogie/Examples/Loops.lean | 3 -- StrataTest/Languages/Boogie/Examples/Map.lean | 2 - StrataTest/Languages/Boogie/Examples/Min.lean | 1 - .../Boogie/Examples/OldExpressions.lean | 3 -- .../Boogie/Examples/PrecedenceCheck.lean | 5 --- .../Boogie/Examples/ProcedureCall.lean | 2 - .../Boogie/Examples/Quantifiers.lean | 6 --- .../Examples/QuantifiersWithTypeAliases.lean | 1 - .../Boogie/Examples/RealBitVector.lean | 4 -- .../Boogie/Examples/RecursiveProcIte.lean | 2 - .../Languages/Boogie/Examples/Regex.lean | 10 ----- .../Languages/Boogie/Examples/SimpleProc.lean | 2 - .../Languages/Boogie/Examples/String.lean | 3 -- .../Languages/Boogie/Examples/TypeAlias.lean | 2 - .../Languages/Boogie/Examples/TypeDecl.lean | 1 - .../Boogie/Examples/UnreachableAssert.lean | 2 - StrataTest/Languages/Boogie/ExprEvalTest.lean | 6 ++- .../Languages/C_Simp/Examples/LoopSimple.lean | 6 --- .../C_Simp/Examples/LoopTrivial.lean | 6 --- .../Languages/C_Simp/Examples/SimpleTest.lean | 1 - StrataVerify.lean | 2 +- docs/GettingStarted.md | 2 - 40 files changed, 70 insertions(+), 129 deletions(-) diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean index 832238382..81c72f988 100644 --- a/Strata/DL/Imperative/SMTUtils.lean +++ b/Strata/DL/Imperative/SMTUtils.lean @@ -141,25 +141,16 @@ def solverResult {P : PureExpr} [ToFormat P.Ident] | "unknown" => .ok .unknown | other => .error other -def VC_folder_name: String := "vcs" - -def smt2_filename (name: String) (suffix : String := "") : String := - name ++ suffix ++ ".smt2" - def dischargeObligation {P : PureExpr} [ToFormat P.Ident] (encodeTerms : List Strata.SMT.Term → Strata.SMT.SolverM (List String × Strata.SMT.EncoderState)) (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType)) (vars : List P.TypedIdent) (smtsolver filename : String) (terms : List Strata.SMT.Term) : IO (Except Format (Result P.TypedIdent × Strata.SMT.EncoderState)) := do - if !(← System.FilePath.isDir VC_folder_name) then - let _ ← IO.FS.createDir VC_folder_name - let filename := s!"{VC_folder_name}/{filename}" let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write let solver ← Strata.SMT.Solver.fileWriter handle let (ids, estate) ← encodeTerms terms solver let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter - IO.println s!"Wrote problem to {filename}." let produce_models ← if smtsolver.endsWith "z3" then -- No need to specify -model because we already have `get-value` in the diff --git a/Strata/Languages/Boogie/Boogie.lean b/Strata/Languages/Boogie/Boogie.lean index b8f609e59..75ad4b490 100644 --- a/Strata/Languages/Boogie/Boogie.lean +++ b/Strata/Languages/Boogie/Boogie.lean @@ -45,7 +45,7 @@ def typeCheck (options : Options) (program : Program) let (program, _T) ← Program.typeCheck C T program -- dbg_trace f!"[Strata.Boogie] Type variables:\n{T.state.substInfo.subst.length}" -- dbg_trace f!"[Strata.Boogie] Annotated program:\n{program}" - if options.verbose then dbg_trace f!"[Strata.Boogie] Type checking succeeded.\n" + if options.verbose >= .normal then dbg_trace f!"[Strata.Boogie] Type checking succeeded.\n" return program def typeCheckAndPartialEval (options : Options) (program : Program) @@ -63,10 +63,9 @@ def typeCheckAndPartialEval (options : Options) (program : Program) program := program } let E ← E.addDatatypes datatypes let pEs := Program.eval E - if options.verbose then do + if options.verbose >= .normal then do dbg_trace f!"{Std.Format.line}VCs:" for (_p, E) in pEs do - -- dbg_trace f!"Program: {p}" dbg_trace f!"{ProofObligations.eraseTypes E.deferred}" return pEs diff --git a/Strata/Languages/Boogie/Options.lean b/Strata/Languages/Boogie/Options.lean index 042feea1d..c85c0028a 100644 --- a/Strata/Languages/Boogie/Options.lean +++ b/Strata/Languages/Boogie/Options.lean @@ -4,8 +4,40 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +inductive VerboseMode where + | quiet + | normal + | debug + deriving Inhabited, Repr, DecidableEq + +def VerboseMode.toNat (v : VerboseMode) : Nat := + match v with + | .quiet => 0 + | .normal => 1 + | .debug => 2 + +def VerboseMode.ofBool (b : Bool) : VerboseMode := + match b with + | false => .quiet + | true => .normal + +instance : Coe VerboseMode Nat where + coe := VerboseMode.toNat + +instance : LT VerboseMode where + lt a b := a.toNat < b.toNat + +instance : DecidableRel (fun a b : VerboseMode => a < b) := + fun a b => decidable_of_iff (a.toNat < b.toNat) Iff.rfl + +instance : LE VerboseMode where + le a b := a.toNat ≤ b.toNat + +instance : DecidableRel (fun a b : VerboseMode => a ≤ b) := + fun a b => decidable_of_iff (a.toNat ≤ b.toNat) Iff.rfl + structure Options where - verbose : Bool + verbose : VerboseMode parseOnly : Bool typeCheckOnly : Bool checkOnly : Bool @@ -15,7 +47,7 @@ structure Options where solverTimeout : Nat def Options.default : Options := { - verbose := true, + verbose := .normal, parseOnly := false, typeCheckOnly := false, checkOnly := false, @@ -28,4 +60,7 @@ instance : Inhabited Options where default := .default def Options.quiet : Options := - { Options.default with verbose := false } + { Options.default with verbose := .quiet } + +def Options.debug : Options := + { Options.default with verbose := .debug } diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean index fce61d485..746637097 100644 --- a/Strata/Languages/Boogie/Verifier.lean +++ b/Strata/Languages/Boogie/Verifier.lean @@ -125,8 +125,6 @@ def Result.formatModelIfSat (r : Result) (verbose : Bool) : Format := f!"\nModel:\n{m}" | _ => f!"" -def VC_folder_name: String := "vcs" - def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do let output ← IO.Process.output { cmd := solver @@ -187,15 +185,12 @@ def dischargeObligation (vars : List (IdentT LMonoTy Visibility)) (smtsolver filename : String) (terms : List Term) (ctx : SMT.Context) : IO (Except Format (SMT.Result × EncoderState)) := do - if !(← System.FilePath.isDir VC_folder_name) then - let _ ← IO.FS.createDir VC_folder_name - let filename := s!"{VC_folder_name}/{filename}" let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write let solver ← Solver.fileWriter handle let prelude := getSolverPrelude smtsolver let (ids, estate) ← Strata.SMT.Encoder.encodeBoogie ctx prelude terms solver let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter - if options.verbose then IO.println s!"Wrote problem to {filename}." + if options.verbose > .normal then IO.println s!"Wrote problem to {filename}." let flags := getSolverFlags options smtsolver let output ← runSolver smtsolver (#[filename] ++ flags) match SMT.solverResult vars output ctx estate with @@ -235,7 +230,7 @@ structure VCResult where smtResult : SMT.Result := .unknown result : Outcome := .unknown estate : EncoderState := EncoderState.init - verbose : Bool := true + verbose : VerboseMode := .normal /-- Map the result from an SMT backend engine to an `Outcome`. @@ -292,7 +287,7 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program) if obligation.obligation.isFalse then -- If PE determines that the consequent is false, then we can immediately -- report a failure. - let result := { obligation, result := .fail, verbose := options.verbose } + let result := { obligation, result := .fail, verbose := options.verbose } return (obligation, some result) else return (obligation, none) @@ -311,7 +306,7 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program) let prog := f!"\n\nEvaluated program:\n{p}" dbg_trace f!"\n\nObligation {obligation.label}: failed!\ \n\nResult obtained during partial evaluation.\ - {if options.verbose then prog else ""}" + {if options.verbose >= .normal then prog else ""}" let result := { obligation, result := .fail, verbose := options.verbose } return (obligation, some result) else if options.removeIrrelevantAxioms then @@ -333,20 +328,24 @@ given proof obligation. -/ def getObligationResult (terms : List Term) (ctx : SMT.Context) (obligation : ProofObligation Expression) (p : Program) - (smtsolver : String) (options : Options) : EIO Format VCResult := do + (smtsolver : String) (options : Options) (counter : IO.Ref Nat) + (tempDir : System.FilePath) : EIO Format VCResult := do let prog := f!"\n\nEvaluated program:\n{p}" + let counterVal ← counter.get + counter.set (counterVal + 1) + let filename := tempDir / s!"{obligation.label}_{counterVal}.smt2" let ans ← IO.toEIO (fun e => f!"{e}") (SMT.dischargeObligation options (ProofObligation.getVars obligation) smtsolver - (Imperative.smt2_filename obligation.label) + filename.toString terms ctx) match ans with | .error e => dbg_trace f!"\n\nObligation {obligation.label}: SMT Solver Invocation Error!\ \n\nError: {e}\ - {if options.verbose then prog else ""}" + {if options.verbose >= .normal then prog else ""}" .error e | .ok (smt_result, estate) => let result := { obligation, @@ -356,7 +355,8 @@ def getObligationResult (terms : List Term) (ctx : SMT.Context) verbose := options.verbose } return result -def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options) : +def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options) + (counter : IO.Ref Nat) (tempDir : System.FilePath) : EIO Format VCResults := do let (p, E) := pE match E.error with @@ -375,7 +375,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option -- No need to use the SMT solver. continue if (result.isFailure || result.isImplementationError) then - if options.verbose then + if options.verbose >= .normal then let prog := f!"\n\nEvaluated program:\n{p}" dbg_trace f!"\n\nResult: {result}\n{prog}" if options.stopOnFirstError then break else continue @@ -387,16 +387,17 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option let result := { obligation, result := .implementationError (toString err), verbose := options.verbose } - if options.verbose then + if options.verbose >= .normal then let prog := f!"\n\nEvaluated program:\n{p}" dbg_trace f!"\n\nResult: {result}\n{prog}" results := results.push result if options.stopOnFirstError then break | .ok (terms, ctx) => let result ← getObligationResult terms ctx obligation p smtsolver options + counter tempDir results := results.push result if result.isNotSuccess then - if options.verbose then + if options.verbose >= .normal then let prog := f!"\n\nEvaluated program:\n{p}" dbg_trace f!"\n\nResult: {result}\n{prog}" if options.stopOnFirstError then break @@ -410,10 +411,12 @@ def verify (smtsolver : String) (program : Program) | .error err => .error f!"❌ Type checking error.\n{format err}" | .ok pEs => + let tempDir ← IO.toEIO (fun e => f!"{e}") IO.FS.createTempDir + let counter ← IO.toEIO (fun e => f!"{e}") (IO.mkRef 0) let VCss ← if options.checkOnly then pure [] else - (List.mapM (fun pE => verifySingleEnv smtsolver pE options) pEs) + (List.mapM (fun pE => verifySingleEnv smtsolver pE options counter tempDir) pEs) .ok VCss.toArray.flatten end Boogie diff --git a/StrataMain.lean b/StrataMain.lean index 4d74c8c1c..a831d7dbf 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -213,8 +213,9 @@ def pyAnalyzeCommand : Command where IO.println "Inlined: " IO.print newPgm let solverName : String := "Strata/Languages/Python/z3_parallel.py" + let verboseMode := VerboseMode.ofBool verbose let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true } + (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose := verboseMode, removeIrrelevantAxioms := true } (moreFns := Strata.Python.ReFactory)) let mut s := "" for vcResult in vcResults do diff --git a/StrataTest/DL/Imperative/Examples.lean b/StrataTest/DL/Imperative/Examples.lean index 6196043df..1f100b25a 100644 --- a/StrataTest/DL/Imperative/Examples.lean +++ b/StrataTest/DL/Imperative/Examples.lean @@ -26,7 +26,6 @@ Assumptions: ⏎ Obligation: ($__x0 : Num) = 1 Metadata: ⏎ -Wrote problem to vcs/x_eq_1.smt2. Obligation x_eq_1: could not be proved! @@ -60,7 +59,6 @@ Assumptions: ⏎ Obligation: true Metadata: ⏎ -Wrote problem to vcs/x_eq_y.smt2. --- info: Obligation: x_eq_y @@ -87,7 +85,6 @@ Assumptions: ⏎ Obligation: 2 × (init_x_0 : Num) = (init_x_0 : Num) + (init_x_0 : Num) Metadata: ⏎ -Wrote problem to vcs/double_x_lemma.smt2. --- info: Obligation: double_x_lemma diff --git a/StrataTest/DL/Imperative/Verify.lean b/StrataTest/DL/Imperative/Verify.lean index c5cf224b9..d851676fa 100644 --- a/StrataTest/DL/Imperative/Verify.lean +++ b/StrataTest/DL/Imperative/Verify.lean @@ -46,6 +46,8 @@ def verify (smtsolver : String) (cmds : Commands) (verbose : Bool) : results := results.push { obligation, result := .err msg } break | .ok terms => + let tempDir ← IO.toEIO (fun e => f!"{e}") IO.FS.createTempDir + let filename := tempDir / s!"{obligation.label}.smt2" let ans ← IO.toEIO (fun e => f!"{e}") @@ -53,7 +55,7 @@ def verify (smtsolver : String) (cmds : Commands) (verbose : Bool) : encodeArithToSMTTerms typedVarToSMT -- (FIXME) ((Arith.Eval.ProofObligation.freeVars obligation).map (fun v => (v, Arith.Ty.Num))) - smtsolver (Imperative.smt2_filename obligation.label) + smtsolver filename.toString terms) match ans with | .ok (result, estate) => diff --git a/StrataTest/Languages/Boogie/Examples/AdvancedMaps.lean b/StrataTest/Languages/Boogie/Examples/AdvancedMaps.lean index 09773e6ed..295201201 100644 --- a/StrataTest/Languages/Boogie/Examples/AdvancedMaps.lean +++ b/StrataTest/Languages/Boogie/Examples/AdvancedMaps.lean @@ -158,14 +158,6 @@ Assumptions: Proof Obligation: (((~select (((~update (((~update $__a0) #1) #1)) #0) #1)) #1) == (~Int.Neg ((~select (((~update $__b1) #true) #-1)) #true))) -Wrote problem to vcs/c_0_eq_a.smt2. -Wrote problem to vcs/c_1_eq_a.smt2. -Wrote problem to vcs/a0eq0.smt2. -Wrote problem to vcs/a1eq1.smt2. -Wrote problem to vcs/a0eq1.smt2. -Wrote problem to vcs/a0neq2.smt2. -Wrote problem to vcs/bTrueEqTrue.smt2. -Wrote problem to vcs/mix.smt2. --- info: Obligation: c_0_eq_a diff --git a/StrataTest/Languages/Boogie/Examples/AdvancedQuantifiers.lean b/StrataTest/Languages/Boogie/Examples/AdvancedQuantifiers.lean index 0ade81810..5b448305d 100644 --- a/StrataTest/Languages/Boogie/Examples/AdvancedQuantifiers.lean +++ b/StrataTest/Languages/Boogie/Examples/AdvancedQuantifiers.lean @@ -45,8 +45,6 @@ Assumptions: Proof Obligation: (((~select $__mArg0) $__kArg1) == #0) -Wrote problem to vcs/a.smt2. -Wrote problem to vcs/Update_ensures_0.smt2. --- info: Obligation: a diff --git a/StrataTest/Languages/Boogie/Examples/AssertionDefaultNames.lean b/StrataTest/Languages/Boogie/Examples/AssertionDefaultNames.lean index 6f2601738..38dd61f2e 100644 --- a/StrataTest/Languages/Boogie/Examples/AssertionDefaultNames.lean +++ b/StrataTest/Languages/Boogie/Examples/AssertionDefaultNames.lean @@ -53,7 +53,6 @@ Assumptions: Proof Obligation: ($__x0 == #1) -Wrote problem to vcs/assert_0.smt2. --- info: Obligation: assert_0 diff --git a/StrataTest/Languages/Boogie/Examples/Axioms.lean b/StrataTest/Languages/Boogie/Examples/Axioms.lean index 165d8fcb2..205ff4cd1 100644 --- a/StrataTest/Languages/Boogie/Examples/Axioms.lean +++ b/StrataTest/Languages/Boogie/Examples/Axioms.lean @@ -82,10 +82,6 @@ Assumptions: Proof Obligation: ((~Int.Gt (~f ~y)) ~y) -Wrote problem to vcs/use_a1_a2.smt2. -Wrote problem to vcs/use_f1.smt2. -Wrote problem to vcs/use_a1_again.smt2. -Wrote problem to vcs/use_a2_again.smt2. --- info: Obligation: use_a1_a2 @@ -146,7 +142,6 @@ Assumptions: Proof Obligation: ((~Bool.Implies ((~Int.Ge $__x0) #0)) ((~Int.Gt (~f $__x0)) $__x0)) -Wrote problem to vcs/axiomPgm2_main_assert.smt2. --- info: Obligation: axiomPgm2_main_assert diff --git a/StrataTest/Languages/Boogie/Examples/BitVecParse.lean b/StrataTest/Languages/Boogie/Examples/BitVecParse.lean index b3184492b..f8eb356ea 100644 --- a/StrataTest/Languages/Boogie/Examples/BitVecParse.lean +++ b/StrataTest/Languages/Boogie/Examples/BitVecParse.lean @@ -43,7 +43,6 @@ Assumptions: Proof Obligation: #false -Wrote problem to vcs/bitvec64_test.smt2. Result: Obligation: bitvec64_test diff --git a/StrataTest/Languages/Boogie/Examples/FailingAssertion.lean b/StrataTest/Languages/Boogie/Examples/FailingAssertion.lean index 163e7815f..0765a5801 100644 --- a/StrataTest/Languages/Boogie/Examples/FailingAssertion.lean +++ b/StrataTest/Languages/Boogie/Examples/FailingAssertion.lean @@ -61,7 +61,6 @@ Assumptions: Proof Obligation: (((~select $__a0) #0) == #1) -Wrote problem to vcs/assert_0.smt2. Result: Obligation: assert_0 diff --git a/StrataTest/Languages/Boogie/Examples/FreeRequireEnsure.lean b/StrataTest/Languages/Boogie/Examples/FreeRequireEnsure.lean index 4fdab9aed..e4b0c22d2 100644 --- a/StrataTest/Languages/Boogie/Examples/FreeRequireEnsure.lean +++ b/StrataTest/Languages/Boogie/Examples/FreeRequireEnsure.lean @@ -64,8 +64,6 @@ Assumptions: Proof Obligation: ($__g2 == #15) -Wrote problem to vcs/g_gt_10_internal.smt2. -Wrote problem to vcs/g_eq_15_internal.smt2. Result: Obligation: g_eq_15_internal diff --git a/StrataTest/Languages/Boogie/Examples/Functions.lean b/StrataTest/Languages/Boogie/Examples/Functions.lean index ef156b190..582e6c436 100644 --- a/StrataTest/Languages/Boogie/Examples/Functions.lean +++ b/StrataTest/Languages/Boogie/Examples/Functions.lean @@ -65,7 +65,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/barEq.smt2. --- info: Obligation: barEq diff --git a/StrataTest/Languages/Boogie/Examples/GeneratedLabels.lean b/StrataTest/Languages/Boogie/Examples/GeneratedLabels.lean index 3e3fffb1f..1c04f149c 100644 --- a/StrataTest/Languages/Boogie/Examples/GeneratedLabels.lean +++ b/StrataTest/Languages/Boogie/Examples/GeneratedLabels.lean @@ -66,7 +66,6 @@ Assumptions: Proof Obligation: (((~select ((~select (((~update $__h0) $__ref1) (((~update ((~select $__h0) $__ref1)) $__field2) ((~Int.Add ((~select ((~select $__h0) $__ref1)) $__field2)) #1)))) $__ref1)) $__field2) == ((~Int.Add ((~select ((~select $__h0) $__ref1)) $__field2)) #1)) -Wrote problem to vcs/assert_0.smt2. --- info: Obligation: assert_0 diff --git a/StrataTest/Languages/Boogie/Examples/Goto.lean b/StrataTest/Languages/Boogie/Examples/Goto.lean index 0f146227a..f5b06728b 100644 --- a/StrataTest/Languages/Boogie/Examples/Goto.lean +++ b/StrataTest/Languages/Boogie/Examples/Goto.lean @@ -103,8 +103,6 @@ Assumptions: Proof Obligation: ((~Int.Le $__x2) #0) -Wrote problem to vcs/a6.smt2. -Wrote problem to vcs/a7.smt2. --- info: Obligation: a1 diff --git a/StrataTest/Languages/Boogie/Examples/Havoc.lean b/StrataTest/Languages/Boogie/Examples/Havoc.lean index 12d693e92..6c9263fc5 100644 --- a/StrataTest/Languages/Boogie/Examples/Havoc.lean +++ b/StrataTest/Languages/Boogie/Examples/Havoc.lean @@ -54,7 +54,6 @@ Assumptions: Proof Obligation: ($__x0 == #1) -Wrote problem to vcs/x_eq_1.smt2. Result: Obligation: x_eq_1 diff --git a/StrataTest/Languages/Boogie/Examples/Loops.lean b/StrataTest/Languages/Boogie/Examples/Loops.lean index ac40121c6..21cbc94ce 100644 --- a/StrataTest/Languages/Boogie/Examples/Loops.lean +++ b/StrataTest/Languages/Boogie/Examples/Loops.lean @@ -66,9 +66,6 @@ Assumptions: Proof Obligation: ((if ((~Int.Lt #0) $__n0) then $__s5 else #0) == ((~Int.Div ((~Int.Mul $__n0) ((~Int.Add $__n0) #1))) #2)) -Wrote problem to vcs/entry_invariant_0.smt2. -Wrote problem to vcs/arbitrary_iter_maintain_invariant_0.smt2. -Wrote problem to vcs/sum_ensures_1.smt2. --- info: Obligation: entry_invariant_0 diff --git a/StrataTest/Languages/Boogie/Examples/Map.lean b/StrataTest/Languages/Boogie/Examples/Map.lean index 85f252845..b6409d133 100644 --- a/StrataTest/Languages/Boogie/Examples/Map.lean +++ b/StrataTest/Languages/Boogie/Examples/Map.lean @@ -64,8 +64,6 @@ Assumptions: Proof Obligation: ((~select ~a) #1) -Wrote problem to vcs/a_zero_true.smt2. -Wrote problem to vcs/a_one_true.smt2. Result: Obligation: a_one_true diff --git a/StrataTest/Languages/Boogie/Examples/Min.lean b/StrataTest/Languages/Boogie/Examples/Min.lean index 0404de5fd..166c8f350 100644 --- a/StrataTest/Languages/Boogie/Examples/Min.lean +++ b/StrataTest/Languages/Boogie/Examples/Min.lean @@ -37,7 +37,6 @@ Assumptions: Proof Obligation: ((~Bool.And ((~Int.Le (if ((~Int.Lt $__n0) $__m1) then $__n0 else $__m1)) $__n0)) ((~Int.Le (if ((~Int.Lt $__n0) $__m1) then $__n0 else $__m1)) $__m1)) -Wrote problem to vcs/min_ensures_0.smt2. --- info: Obligation: min_ensures_0 diff --git a/StrataTest/Languages/Boogie/Examples/OldExpressions.lean b/StrataTest/Languages/Boogie/Examples/OldExpressions.lean index 9a5e65ff3..27f6ea8de 100644 --- a/StrataTest/Languages/Boogie/Examples/OldExpressions.lean +++ b/StrataTest/Languages/Boogie/Examples/OldExpressions.lean @@ -138,9 +138,6 @@ Assumptions: Proof Obligation: ($__b6 == #false) -Wrote problem to vcs/T2_g2_eq_g.smt2. -Wrote problem to vcs/T2_a_eq_false.smt2. -Wrote problem to vcs/T2_b_eq_false.smt2. --- info: Obligation: T1_z_eq_g diff --git a/StrataTest/Languages/Boogie/Examples/PrecedenceCheck.lean b/StrataTest/Languages/Boogie/Examples/PrecedenceCheck.lean index df028bbd0..b9cc7fb9c 100644 --- a/StrataTest/Languages/Boogie/Examples/PrecedenceCheck.lean +++ b/StrataTest/Languages/Boogie/Examples/PrecedenceCheck.lean @@ -78,11 +78,6 @@ Assumptions: Proof Obligation: ((~Bool.Equiv ((~Bool.Implies init_a_0) init_b_1)) ((~Bool.Or (~Bool.Not init_a_0)) init_b_1)) -Wrote problem to vcs/implies_and_eq_not_or_1.smt2. -Wrote problem to vcs/implies_and_eq_not_or_2.smt2. -Wrote problem to vcs/implies_and_eq_not_or_3.smt2. -Wrote problem to vcs/implies_and_eq_not_or_4.smt2. -Wrote problem to vcs/implies_equiv.smt2. --- info: Obligation: implies_and_eq_not_or_1 diff --git a/StrataTest/Languages/Boogie/Examples/ProcedureCall.lean b/StrataTest/Languages/Boogie/Examples/ProcedureCall.lean index e3fff34a0..bd2e7b70f 100644 --- a/StrataTest/Languages/Boogie/Examples/ProcedureCall.lean +++ b/StrataTest/Languages/Boogie/Examples/ProcedureCall.lean @@ -112,8 +112,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/old_g_property.smt2. -Wrote problem to vcs/return_value_lemma.smt2. --- info: Obligation: new_g_value diff --git a/StrataTest/Languages/Boogie/Examples/Quantifiers.lean b/StrataTest/Languages/Boogie/Examples/Quantifiers.lean index 45e796f9d..ce0eb42a0 100644 --- a/StrataTest/Languages/Boogie/Examples/Quantifiers.lean +++ b/StrataTest/Languages/Boogie/Examples/Quantifiers.lean @@ -75,9 +75,6 @@ Assumptions: Proof Obligation: (∀ ((~Int.Lt %0) $__x0)) -Wrote problem to vcs/good_assert.smt2. -Wrote problem to vcs/good.smt2. -Wrote problem to vcs/bad.smt2. Result: Obligation: bad @@ -148,9 +145,6 @@ Assumptions: Proof Obligation: ((~Int.Lt ((~g (~f $__x0)) $__x0)) #0) -Wrote problem to vcs/trigger_assert.smt2. -Wrote problem to vcs/multi_trigger_assert.smt2. -Wrote problem to vcs/f_and_g.smt2. --- info: Obligation: trigger_assert diff --git a/StrataTest/Languages/Boogie/Examples/QuantifiersWithTypeAliases.lean b/StrataTest/Languages/Boogie/Examples/QuantifiersWithTypeAliases.lean index 6aac47fbb..101f2097c 100644 --- a/StrataTest/Languages/Boogie/Examples/QuantifiersWithTypeAliases.lean +++ b/StrataTest/Languages/Boogie/Examples/QuantifiersWithTypeAliases.lean @@ -71,7 +71,6 @@ Assumptions: Proof Obligation: (((~select ((~select (((~update $__h0) $__ref1) (((~update ((~select $__h0) $__ref1)) $__field2) ((~Int.Add ((~select ((~select $__h0) $__ref1)) $__field2)) #1)))) $__ref1)) $__field2) == ((~Int.Add ((~select ((~select $__h0) $__ref1)) $__field2)) #1)) -Wrote problem to vcs/assert0.smt2. --- info: Obligation: assert0 diff --git a/StrataTest/Languages/Boogie/Examples/RealBitVector.lean b/StrataTest/Languages/Boogie/Examples/RealBitVector.lean index 9187e138e..f0e37d546 100644 --- a/StrataTest/Languages/Boogie/Examples/RealBitVector.lean +++ b/StrataTest/Languages/Boogie/Examples/RealBitVector.lean @@ -71,8 +71,6 @@ Assumptions: Proof Obligation: ((~Real.Ge ((~Real.Add ~x) ~y)) #4) -Wrote problem to vcs/real_add_ge_good.smt2. -Wrote problem to vcs/real_add_ge_bad.smt2. Result: Obligation: real_add_ge_bad @@ -180,8 +178,6 @@ Assumptions: Proof Obligation: (((~Bv1.Add $__x0) $__x0) == ((~Bv1.Sub $__x0) $__x0)) -Wrote problem to vcs/bv_add_ge.smt2. -Wrote problem to vcs/Q_ensures_0.smt2. --- info: Obligation: bv_add_ge diff --git a/StrataTest/Languages/Boogie/Examples/RecursiveProcIte.lean b/StrataTest/Languages/Boogie/Examples/RecursiveProcIte.lean index 929792425..1a6d71c05 100644 --- a/StrataTest/Languages/Boogie/Examples/RecursiveProcIte.lean +++ b/StrataTest/Languages/Boogie/Examples/RecursiveProcIte.lean @@ -54,8 +54,6 @@ Assumptions: Proof Obligation: ((~Bool.Implies ((~Int.Le $__n0) #100)) ((if ((~Int.Lt #100) $__n0) then ((~Int.Sub $__n0) #10) else $__r3) == #91)) -Wrote problem to vcs/n_gt_100_postcond.smt2. -Wrote problem to vcs/n_le_100_postcond.smt2. --- info: Obligation: n_gt_100_postcond diff --git a/StrataTest/Languages/Boogie/Examples/Regex.lean b/StrataTest/Languages/Boogie/Examples/Regex.lean index 5f0a38391..91e9473a4 100644 --- a/StrataTest/Languages/Boogie/Examples/Regex.lean +++ b/StrataTest/Languages/Boogie/Examples/Regex.lean @@ -124,15 +124,6 @@ Assumptions: Proof Obligation: (~Bool.Not ((~Str.InRegEx #b) ~optionally_a)) -Wrote problem to vcs/hello_dot_ends_with_period.smt2. -Wrote problem to vcs/dot_ends_with_period.smt2. -Wrote problem to vcs/bye_exclaim_no_end_with_period.smt2. -Wrote problem to vcs/ok_chars_str.smt2. -Wrote problem to vcs/cannot_contain_exclaim.smt2. -Wrote problem to vcs/has_to_be_at_least_1_char.smt2. -Wrote problem to vcs/cannot_exceed_10_chars.smt2. -Wrote problem to vcs/optionally_a_check1.smt2. -Wrote problem to vcs/optionally_a_check2.smt2. --- info: Obligation: hello_dot_ends_with_period @@ -302,7 +293,6 @@ Assumptions: Proof Obligation: (~Bool.Not ((~Str.InRegEx init_s_0) ~Re.None)) -Wrote problem to vcs/assert_0.smt2. --- info: Obligation: assert_0 diff --git a/StrataTest/Languages/Boogie/Examples/SimpleProc.lean b/StrataTest/Languages/Boogie/Examples/SimpleProc.lean index 347d9b91c..afaad96cd 100644 --- a/StrataTest/Languages/Boogie/Examples/SimpleProc.lean +++ b/StrataTest/Languages/Boogie/Examples/SimpleProc.lean @@ -73,8 +73,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/Test_ensures_0.smt2. -Wrote problem to vcs/Test_ensures_1.smt2. --- info: Obligation: Test_ensures_0 diff --git a/StrataTest/Languages/Boogie/Examples/String.lean b/StrataTest/Languages/Boogie/Examples/String.lean index fd32b7194..9085ad8d2 100644 --- a/StrataTest/Languages/Boogie/Examples/String.lean +++ b/StrataTest/Languages/Boogie/Examples/String.lean @@ -76,9 +76,6 @@ Assumptions: Proof Obligation: ((((~Str.Substr #testing123) #2) #0) == #) -Wrote problem to vcs/s1_s2_len_sum_eq_s3_len.smt2. -Wrote problem to vcs/substr_of_concat.smt2. -Wrote problem to vcs/substr_of_concat_concrete_test.smt2. --- info: Obligation: concrete_string_test diff --git a/StrataTest/Languages/Boogie/Examples/TypeAlias.lean b/StrataTest/Languages/Boogie/Examples/TypeAlias.lean index 6068a759f..1ce1a0e16 100644 --- a/StrataTest/Languages/Boogie/Examples/TypeAlias.lean +++ b/StrataTest/Languages/Boogie/Examples/TypeAlias.lean @@ -88,7 +88,6 @@ Assumptions: Proof Obligation: (~fooConst1 == ~fooConst2) -Wrote problem to vcs/fooAssertion.smt2. --- info: Obligation: fooAssertion @@ -132,7 +131,6 @@ Assumptions: Proof Obligation: ((((~MapGetEq init_d_0) init_k_1) init_v_2) == (((~MapGetEq init_d_0) init_k_1) #0)) -Wrote problem to vcs/assert_0.smt2. --- info: Obligation: assert_0 diff --git a/StrataTest/Languages/Boogie/Examples/TypeDecl.lean b/StrataTest/Languages/Boogie/Examples/TypeDecl.lean index 24151e259..40c159470 100644 --- a/StrataTest/Languages/Boogie/Examples/TypeDecl.lean +++ b/StrataTest/Languages/Boogie/Examples/TypeDecl.lean @@ -104,7 +104,6 @@ Assumptions: Proof Obligation: (~fooConst1 == ~fooConst2) -Wrote problem to vcs/fooAssertion.smt2. --- info: Obligation: fooAssertion diff --git a/StrataTest/Languages/Boogie/Examples/UnreachableAssert.lean b/StrataTest/Languages/Boogie/Examples/UnreachableAssert.lean index fd9b9bd08..5e67c4831 100644 --- a/StrataTest/Languages/Boogie/Examples/UnreachableAssert.lean +++ b/StrataTest/Languages/Boogie/Examples/UnreachableAssert.lean @@ -59,8 +59,6 @@ Assumptions: Proof Obligation: (init_x_0 == (if (init_z_2 == #false) then init_x_0 else init_y_1)) -Wrote problem to vcs/unreachable.smt2. -Wrote problem to vcs/x_eq_y.smt2. --- info: Obligation: x_eq_y_internal diff --git a/StrataTest/Languages/Boogie/ExprEvalTest.lean b/StrataTest/Languages/Boogie/ExprEvalTest.lean index 477df201d..e3ab73430 100644 --- a/StrataTest/Languages/Boogie/ExprEvalTest.lean +++ b/StrataTest/Languages/Boogie/ExprEvalTest.lean @@ -65,9 +65,11 @@ def checkValid (e:LExpr BoogieLParams.mono): IO Bool := do | .error msg => throw (IO.userError s!"error: {msg}") | .ok (.none) => return false | .ok (.some (smt_term, ctx)) => + let tempDir ← IO.FS.createTempDir + let filename := tempDir / s!"exprEvalTest.smt2" let ans ← Boogie.SMT.dischargeObligation - { Options.default with verbose := false } - (LExpr.freeVars e) "z3" s!"exprEvalTest.smt2" + { Options.default with verbose := .quiet } + (LExpr.freeVars e) "z3" filename.toString [smt_term] ctx match ans with | .ok (.sat _,_) => return true diff --git a/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean b/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean index e39921935..4aa5702a7 100644 --- a/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean +++ b/StrataTest/Languages/C_Simp/Examples/LoopSimple.lean @@ -177,12 +177,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/entry_invariant.smt2. -Wrote problem to vcs/assert_measure_pos.smt2. -Wrote problem to vcs/measure_decreases.smt2. -Wrote problem to vcs/measure_imp_not_guard.smt2. -Wrote problem to vcs/arbitrary_iter_maintain_invariant.smt2. -Wrote problem to vcs/sum_assert.smt2. --- info: Obligation: entry_invariant diff --git a/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean b/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean index 0cb4cbeb5..98488be05 100644 --- a/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean +++ b/StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean @@ -167,12 +167,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/entry_invariant.smt2. -Wrote problem to vcs/assert_measure_pos.smt2. -Wrote problem to vcs/measure_decreases.smt2. -Wrote problem to vcs/measure_imp_not_guard.smt2. -Wrote problem to vcs/arbitrary_iter_maintain_invariant.smt2. -Wrote problem to vcs/i_eq_n.smt2. --- info: Obligation: entry_invariant diff --git a/StrataTest/Languages/C_Simp/Examples/SimpleTest.lean b/StrataTest/Languages/C_Simp/Examples/SimpleTest.lean index 6755f7ebd..9a9255c16 100644 --- a/StrataTest/Languages/C_Simp/Examples/SimpleTest.lean +++ b/StrataTest/Languages/C_Simp/Examples/SimpleTest.lean @@ -93,7 +93,6 @@ Assumptions: Proof Obligation: #true -Wrote problem to vcs/test_assert.smt2. --- info: Obligation: test_assert diff --git a/StrataVerify.lean b/StrataVerify.lean index ff7aef041..eec37005e 100644 --- a/StrataVerify.lean +++ b/StrataVerify.lean @@ -16,7 +16,7 @@ def parseOptions (args : List String) : Except Std.Format (Options × String) := go Options.quiet args where go : Options → List String → Except Std.Format (Options × String) - | opts, "--verbose" :: rest => go {opts with verbose := true} rest + | opts, "--verbose" :: rest => go {opts with verbose := .normal} rest | opts, "--check" :: rest => go {opts with checkOnly := true} rest | opts, "--type-check" :: rest => go {opts with typeCheckOnly := true} rest | opts, "--parse-only" :: rest => go {opts with parseOnly := true} rest diff --git a/docs/GettingStarted.md b/docs/GettingStarted.md index e4e5649d8..89e1aee34 100644 --- a/docs/GettingStarted.md +++ b/docs/GettingStarted.md @@ -272,8 +272,6 @@ assert [double_x_lemma]: (2 * x == x + x); #end /-- -info: Wrote problem to vcs/double_x_lemma.smt2. ---- info: Obligation: double_x_lemma Result: verified From 2884cdd1c99b761bae26b93b995a439b25fe336b Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Fri, 16 Jan 2026 14:22:54 -0600 Subject: [PATCH 2/4] Add tempDir --- Strata/Languages/Boogie/Verifier.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean index 746637097..f6a5f3656 100644 --- a/Strata/Languages/Boogie/Verifier.lean +++ b/Strata/Languages/Boogie/Verifier.lean @@ -405,13 +405,17 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option def verify (smtsolver : String) (program : Program) (options : Options := Options.default) - (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) : + (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) + (tempDir : Option String := .none) : EIO Format VCResults := do match Boogie.typeCheckAndPartialEval options program moreFns with | .error err => .error f!"❌ Type checking error.\n{format err}" | .ok pEs => - let tempDir ← IO.toEIO (fun e => f!"{e}") IO.FS.createTempDir + let tempDir ← IO.toEIO (fun e => f!"{e}") + (match tempDir with + | .none => IO.FS.createTempDir + | .some p => do IO.FS.createDirAll ⟨p⟩; return ⟨p⟩) let counter ← IO.toEIO (fun e => f!"{e}") (IO.mkRef 0) let VCss ← if options.checkOnly then pure [] @@ -446,12 +450,13 @@ def verify (ictx : InputContext := Inhabited.default) (options : Options := Options.default) (moreFns : @Lambda.Factory Boogie.BoogieLParams := Lambda.Factory.default) + (tempDir : Option String := .none) : IO Boogie.VCResults := do let (program, errors) := Boogie.getProgram env ictx if errors.isEmpty then -- dbg_trace f!"AST: {program}" EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify smtsolver program options moreFns) + (Boogie.verify smtsolver program options moreFns tempDir) else panic! s!"DDM Transform Error: {repr errors}" From 6a9dc4be3bf0391b3dbc3bf0e65659cd16ae825b Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Fri, 16 Jan 2026 14:55:09 -0600 Subject: [PATCH 3/4] Use IO.FS.withTempDir and hoist out its usage to Strata.verify and the unit tests --- Strata/Languages/Boogie/Verifier.lean | 19 +++++++++++-------- Strata/Languages/C_Simp/Verify.lean | 14 +++++++++++--- .../Laurel/LaurelToBoogieTranslator.lean | 5 +++-- StrataMain.lean | 9 ++++++--- .../Boogie/DatatypeVerificationTests.lean | 3 ++- 5 files changed, 33 insertions(+), 17 deletions(-) diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean index f6a5f3656..cc34f384e 100644 --- a/Strata/Languages/Boogie/Verifier.lean +++ b/Strata/Languages/Boogie/Verifier.lean @@ -404,18 +404,14 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option return results def verify (smtsolver : String) (program : Program) + (tempDir : System.FilePath) (options : Options := Options.default) (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) - (tempDir : Option String := .none) : - EIO Format VCResults := do + : EIO Format VCResults := do match Boogie.typeCheckAndPartialEval options program moreFns with | .error err => .error f!"❌ Type checking error.\n{format err}" | .ok pEs => - let tempDir ← IO.toEIO (fun e => f!"{e}") - (match tempDir with - | .none => IO.FS.createTempDir - | .some p => do IO.FS.createDirAll ⟨p⟩; return ⟨p⟩) let counter ← IO.toEIO (fun e => f!"{e}") (IO.mkRef 0) let VCss ← if options.checkOnly then pure [] @@ -455,8 +451,15 @@ def verify let (program, errors) := Boogie.getProgram env ictx if errors.isEmpty then -- dbg_trace f!"AST: {program}" - EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify smtsolver program options moreFns tempDir) + let runner tempDir := + EIO.toIO (fun f => IO.Error.userError (toString f)) + (Boogie.verify smtsolver program tempDir options moreFns) + match tempDir with + | .none => + IO.FS.withTempDir runner + | .some p => + IO.FS.createDirAll ⟨p⟩ + runner ⟨p⟩ else panic! s!"DDM Transform Error: {repr errors}" diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean index 309943be9..e9798b9e2 100644 --- a/Strata/Languages/C_Simp/Verify.lean +++ b/Strata/Languages/C_Simp/Verify.lean @@ -131,10 +131,18 @@ def C_Simp.typeCheck (p : Strata.Program) (options : Options := Options.default) let program := C_Simp.get_program p Boogie.typeCheck options (to_boogie program) -def C_Simp.verify (smtsolver : String) (p : Strata.Program) (options : Options := Options.default): +def C_Simp.verify (smtsolver : String) (p : Strata.Program) + (options : Options := Options.default) + (tempDir : Option String := .none): IO Boogie.VCResults := do let program := C_Simp.get_program p - EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify smtsolver (to_boogie program) options) + let runner tempDir := EIO.toIO (fun f => IO.Error.userError (toString f)) + (Boogie.verify smtsolver (to_boogie program) tempDir options) + match tempDir with + | .none => + IO.FS.withTempDir runner + | .some p => + IO.FS.createDirAll ⟨p⟩ + runner ⟨p⟩ end Strata diff --git a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean index 2063f4a39..c8be1d9ef 100644 --- a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean @@ -218,8 +218,9 @@ def verifyToVcResults (smtsolver : String) (program : Program) dbg_trace "=== Generated Boogie Program ===" dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format boogieProgram))) dbg_trace "=================================" - EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify smtsolver boogieProgram options) + IO.FS.withTempDir (fun tempDir => + EIO.toIO (fun f => IO.Error.userError (toString f)) + (Boogie.verify smtsolver boogieProgram tempDir options)) def verifyToDiagnostics (smtsolver : String) (program : Program): IO (Array Diagnostic) := do let results <- verifyToVcResults smtsolver program diff --git a/StrataMain.lean b/StrataMain.lean index a831d7dbf..5556a1c8c 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -214,9 +214,12 @@ def pyAnalyzeCommand : Command where IO.print newPgm let solverName : String := "Strata/Languages/Python/z3_parallel.py" let verboseMode := VerboseMode.ofBool verbose - let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f)) - (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose := verboseMode, removeIrrelevantAxioms := true } - (moreFns := Strata.Python.ReFactory)) + let vcResults ← IO.FS.withTempDir (fun tempDir => + EIO.toIO + (fun f => IO.Error.userError (toString f)) + (Boogie.verify solverName newPgm tempDir + { Options.default with stopOnFirstError := false, verbose := verboseMode, removeIrrelevantAxioms := true } + (moreFns := Strata.Python.ReFactory))) let mut s := "" for vcResult in vcResults do s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n" diff --git a/StrataTest/Languages/Boogie/DatatypeVerificationTests.lean b/StrataTest/Languages/Boogie/DatatypeVerificationTests.lean index 6eaa6f5f9..5a66914b1 100644 --- a/StrataTest/Languages/Boogie/DatatypeVerificationTests.lean +++ b/StrataTest/Languages/Boogie/DatatypeVerificationTests.lean @@ -108,7 +108,8 @@ Run verification and return a summary string. -/ def runVerificationTest (testName : String) (program : Program) : IO String := do try - match ← EIO.toIO' (Boogie.verify "cvc5" program Options.quiet) with + match ← (IO.FS.withTempDir (fun tempDir => + EIO.toIO' (Boogie.verify "cvc5" program tempDir Options.quiet))) with | .error err => return s!"{testName}: FAILED\n Error: {err}" | .ok results => From 0f48d693f1a16b81d0c57b0698c58ef16aaf5afb Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Fri, 16 Jan 2026 15:16:34 -0600 Subject: [PATCH 4/4] missing IO.FS.withTempDir --- StrataTest/Languages/Boogie/ExprEvalTest.lean | 25 +++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/StrataTest/Languages/Boogie/ExprEvalTest.lean b/StrataTest/Languages/Boogie/ExprEvalTest.lean index e3ab73430..7dc5956ad 100644 --- a/StrataTest/Languages/Boogie/ExprEvalTest.lean +++ b/StrataTest/Languages/Boogie/ExprEvalTest.lean @@ -65,18 +65,18 @@ def checkValid (e:LExpr BoogieLParams.mono): IO Bool := do | .error msg => throw (IO.userError s!"error: {msg}") | .ok (.none) => return false | .ok (.some (smt_term, ctx)) => - let tempDir ← IO.FS.createTempDir - let filename := tempDir / s!"exprEvalTest.smt2" - let ans ← Boogie.SMT.dischargeObligation - { Options.default with verbose := .quiet } - (LExpr.freeVars e) "z3" filename.toString - [smt_term] ctx - match ans with - | .ok (.sat _,_) => return true - | _ => - IO.println s!"Test failed on {e}" - IO.println s!"The query: {repr smt_term}" - throw (IO.userError "- failed") + IO.FS.withTempDir (fun tempDir => do + let filename := tempDir / s!"exprEvalTest.smt2" + let ans ← Boogie.SMT.dischargeObligation + { Options.default with verbose := .quiet } + (LExpr.freeVars e) "z3" filename.toString + [smt_term] ctx + match ans with + | .ok (.sat _,_) => return true + | _ => + IO.println s!"Test failed on {e}" + IO.println s!"The query: {repr smt_term}" + throw (IO.userError "- failed")) /-- If a randomly chosen value is <= odd / 10, pick from interesting vals, @@ -205,7 +205,6 @@ def test_lctx : LContext BoogieLParams := def test_ctx : TContext Visibility := ⟨[[]], []⟩ abbrev test_ty : LTy := .forAll [] <| .tcons "bool" [] - #guard_msgs(drop all) in #eval do let P : LExpr BoogieLParams.mono → Prop := fun t => HasType test_lctx test_ctx t test_ty