(Fixes #75) Create temporary directory for dumping SMT files

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

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
 

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 }

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,33 +387,36 @@ 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
     return results
 
 def verify (smtsolver : String) (program : Program)
+    (tempDir : System.FilePath)
     (options : Options := Options.default)
-    (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default) :
-    EIO Format VCResults := do
+    (moreFns : @Lambda.Factory BoogieLParams := Lambda.Factory.default)
+    : EIO Format VCResults := do
   match Boogie.typeCheckAndPartialEval options program moreFns with
   | .error err =>
     .error f!"❌ Type checking error.\n{format err}"
   | .ok pEs =>
+    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
@@ -443,12 +446,20 @@ 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)
+    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}"
 

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

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

StrataMain.lean

@@ -213,9 +213,13 @@ def pyAnalyzeCommand : Command where
         IO.println "Inlined: "
         IO.print newPgm
       let solverName : String := "Strata/Languages/Python/z3_parallel.py"
-      let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
-                          (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true }
-                                                    (moreFns := Strata.Python.ReFactory))
+      let verboseMode := VerboseMode.ofBool verbose
+      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"

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

StrataTest/DL/Imperative/Verify.lean

@@ -46,14 +46,16 @@ 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}")
               (@Imperative.dischargeObligation Arith.PureExpr _
                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) =>

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 =>

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

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