Add provenance info to generated SMT files

Examples/run_examples.sh

@@ -8,14 +8,21 @@ for test_file in *.st; do
         expected_file="expected/${base_name}.expected"
         if [ -f "$expected_file" ]; then
 
-            output=$(cd .. && lake exe StrataVerify "Examples/${test_file}")
+            output=$(cd .. && lake exe StrataVerify --vc-directory vcs "Examples/${test_file}")
 
             if ! echo "$output" | diff -q "$expected_file" - > /dev/null; then
                 echo "ERROR: Analysis output for $base_name does not match expected result"
                 echo "$output" | diff "$expected_file" -
                 failed=1
             fi
-        fi	
+            if ls ../vcs/*.smt2 2> /dev/null > /dev/null ; then
+                if ! grep -q "set-info" ../vcs/*.smt2 ; then
+                  echo "ERROR: No provenance information in VCs"
+                  failed=1
+                fi
+            fi
+            rm -rf ../vcs
+        fi
     fi
 done
 

Strata/DL/SMT/Solver.lean

@@ -102,6 +102,9 @@ def setLogic (logic : String) : SolverM Unit :=
 def setOption (name value : String) : SolverM Unit :=
   emitln s!"(set-option :{name} {value})"
 
+def setInfo (name value : String) : SolverM Unit :=
+  emitln s!"(set-info :{name} {value})"
+
 def comment (comment : String) : SolverM Unit :=
   let inline := comment.replace "\n" " "
   emitln s!"; {inline}"

Strata/Languages/C_Simp/Verify.lean

@@ -132,13 +132,13 @@ def C_Simp.typeCheck (p : Strata.Program) (options : Options := Options.default)
   let program := C_Simp.get_program p
   Core.typeCheck options (to_core program)
 
-def C_Simp.verify (smtsolver : String) (p : Strata.Program)
+def C_Simp.verify (p : Strata.Program)
     (options : Options := Options.default)
     (tempDir : Option String := .none):
   IO Core.VCResults := do
   let program := C_Simp.get_program p
   let runner tempDir := EIO.toIO (fun f => IO.Error.userError (toString f))
-    (Core.verify smtsolver (to_core program) tempDir .none options)
+    (Core.verify (to_core program) tempDir .none options)
   match tempDir with
   | .none =>
     IO.FS.withTempDir runner

Strata/Languages/Core/Options.lean

@@ -54,6 +54,8 @@ structure Options where
   outputSarif : Bool
   /-- SMT solver executable to use -/
   solver : String
+  /-- Directory to store VCs -/
+  vcDirectory : Option System.FilePath
 
 def Options.default : Options := {
   verbose := .normal,
@@ -65,6 +67,7 @@ def Options.default : Options := {
   solverTimeout := 10,
   outputSarif := false,
   solver := defaultSolver
+  vcDirectory := .none
 }
 
 instance : Inhabited Options where

Strata/Languages/Core/Verifier.lean

@@ -175,34 +175,52 @@ def getSolverPrelude : String → SolverM Unit
 | "cvc5" => return ()
 | _ => return ()
 
-def getSolverFlags (options : Options) (solver : String) : Array String :=
+def getSolverFlags (options : Options) : Array String :=
   let produceModels :=
-    match solver with
+    match options.solver with
     | "cvc5" => #["--produce-models"]
     -- No need to specify -model for Z3 because we already have `get-value`
     -- in the generated SMT file.
     | _ => #[]
   let setTimeout :=
-    match solver with
+    match options.solver with
     | "cvc5" => #[s!"--tlimit={options.solverTimeout*1000}"]
     | "z3" => #[s!"-T:{options.solverTimeout}"]
     | _ => #[]
   produceModels ++ setTimeout
 
+def addLocationInfo
+  (solver : Solver)
+  (md : Imperative.MetaData Expression)
+  : IO Unit := do
+  match Imperative.getFileRange md with
+    | .some fileRange => do
+      solver.setInfo "file" s!"\"{format fileRange.file}\""
+      solver.setInfo "start" s!"{fileRange.range.start}"
+      solver.setInfo "stop" s!"{fileRange.range.stop}"
+      -- TODO: the following should probably be stored in metadata so it
+      -- can be set in an application-specific way.
+      solver.setInfo "unsat-message" s!"\"Assertion cannot be proven\""
+    | .none => pure ()
+
 def dischargeObligation
   (options : Options)
-  (vars : List (IdentT LMonoTy Visibility)) (smtsolver filename : String)
-  (terms : List Term) (ctx : SMT.Context)
+  (vars : List (IdentT LMonoTy Visibility))
+  (md : Imperative.MetaData Expression)
+  (filename : String)
+  (terms : List Term)
+  (ctx : SMT.Context)
   : IO (Except Format (SMT.Result × EncoderState)) := do
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Solver.fileWriter handle
-  let prelude := getSolverPrelude smtsolver
+  let prelude := getSolverPrelude options.solver
   let (ids, estate) ← Strata.SMT.Encoder.encodeCore ctx prelude terms solver
+  addLocationInfo solver md
   let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
   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 smtsolver with
+  let flags := getSolverFlags options
+  let output ← runSolver options.solver (#[filename] ++ flags)
+  match SMT.solverResult vars output ctx estate options.solver with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
@@ -338,7 +356,7 @@ given proof obligation.
 -/
 def getObligationResult (terms : List Term) (ctx : SMT.Context)
     (obligation : ProofObligation Expression) (p : Program)
-    (smtsolver : String) (options : Options) (counter : IO.Ref Nat)
+    (options : Options) (counter : IO.Ref Nat)
     (tempDir : System.FilePath) : EIO DiagnosticModel VCResult := do
   let prog := f!"\n\nEvaluated program:\n{p}"
   let counterVal ← counter.get
@@ -348,8 +366,9 @@ def getObligationResult (terms : List Term) (ctx : SMT.Context)
       IO.toEIO
         (fun e => DiagnosticModel.fromFormat f!"{e}")
         (SMT.dischargeObligation options
-          (ProofObligation.getVars obligation) smtsolver
-            filename.toString
+          (ProofObligation.getVars obligation)
+          obligation.metadata
+          filename.toString
           terms ctx)
   match ans with
   | .error e =>
@@ -365,7 +384,7 @@ def getObligationResult (terms : List Term) (ctx : SMT.Context)
                      verbose := options.verbose }
     return result
 
-def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options)
+def verifySingleEnv (pE : Program × Env) (options : Options)
     (counter : IO.Ref Nat) (tempDir : System.FilePath) :
     EIO DiagnosticModel VCResults := do
   let (p, E) := pE
@@ -403,7 +422,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
         results := results.push result
         if options.stopOnFirstError then break
       | .ok (terms, ctx) =>
-        let result ← getObligationResult terms ctx obligation p smtsolver options
+        let result ← getObligationResult terms ctx obligation p options
                       counter tempDir
         results := results.push result
         if result.isNotSuccess then
@@ -413,7 +432,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
           if options.stopOnFirstError then break
     return results
 
-def verify (smtsolver : String) (program : Program)
+def verify (program : Program)
     (tempDir : System.FilePath)
     (proceduresToVerify : Option (List String) := none)
     (options : Options := Options.default)
@@ -443,7 +462,7 @@ def verify (smtsolver : String) (program : Program)
     let VCss ← if options.checkOnly then
                  pure []
                else
-                 (List.mapM (fun pE => verifySingleEnv smtsolver pE options counter tempDir) pEs)
+                 (List.mapM (fun pE => verifySingleEnv pE options counter tempDir) pEs)
     .ok VCss.toArray.flatten
 
 end Core
@@ -470,24 +489,23 @@ def Core.getProgram
   TransM.run ictx (translateProgram p)
 
 def verify
-    (smtsolver : String) (env : Program)
+    (env : Program)
     (ictx : InputContext := Inhabited.default)
     (proceduresToVerify : Option (List String) := none)
     (options : Options := Options.default)
     (moreFns : @Lambda.Factory Core.CoreLParams := Lambda.Factory.default)
-    (tempDir : Option String := .none)
     : IO Core.VCResults := do
   let (program, errors) := Core.getProgram env ictx
   if errors.isEmpty then
     let runner tempDir :=
       EIO.toIO (fun dm => IO.Error.userError (toString (dm.format (some ictx.fileMap))))
-                  (Core.verify smtsolver program tempDir proceduresToVerify options moreFns)
-    match tempDir with
+                  (Core.verify program tempDir proceduresToVerify options moreFns)
+    match options.vcDirectory with
     | .none =>
       IO.FS.withTempDir runner
     | .some p =>
-      IO.FS.createDirAll ⟨p⟩
-      runner ⟨p⟩
+      IO.FS.createDirAll ⟨p.toString⟩
+      runner ⟨p.toString⟩
   else
     panic! s!"DDM Transform Error: {repr errors}"
 

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -435,9 +435,8 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program
 /--
 Verify a Laurel program using an SMT solver
 -/
-def verifyToVcResults (smtsolver : String) (program : Program)
+def verifyToVcResults (program : Program)
     (options : Options := Options.default)
-    (tempDir : Option String := .none)
     : IO (Except (Array DiagnosticModel) VCResults) := do
   let (strataCoreProgram, translateDiags) ← match translate program with
     | .error translateErrorDiags => return .error translateErrorDiags
@@ -451,25 +450,25 @@ def verifyToVcResults (smtsolver : String) (program : Program)
   dbg_trace "================================="
   let runner tempDir :=
     EIO.toIO (fun f => IO.Error.userError (toString f))
-        (Core.verify smtsolver strataCoreProgram tempDir .none options)
-  let ioResult ← match tempDir with
+        (Core.verify strataCoreProgram tempDir .none options)
+  let ioResult ← match options.vcDirectory with
     | .none => IO.FS.withTempDir runner
-    | .some p => IO.FS.createDirAll ⟨p⟩; runner ⟨p⟩
+    | .some p => IO.FS.createDirAll ⟨p.toString⟩; runner ⟨p.toString⟩
   if translateDiags.isEmpty then
     return .ok ioResult
   else
     return .error (translateDiags ++ ioResult.filterMap toDiagnosticModel)
 
 
-def verifyToDiagnostics (smtsolver : String) (files: Map Strata.Uri Lean.FileMap) (program : Program): IO (Array Diagnostic) := do
-  let results <- verifyToVcResults smtsolver program
+def verifyToDiagnostics (files: Map Strata.Uri Lean.FileMap) (program : Program) (options : Options := Options.default): IO (Array Diagnostic) := do
+  let results <- verifyToVcResults program options
   match results with
   | .error errors => return errors.map (fun dm => dm.toDiagnostic files)
   | .ok results => return results.filterMap (fun dm => dm.toDiagnostic files)
 
 
-def verifyToDiagnosticModels (smtsolver : String) (program : Program): IO (Array DiagnosticModel) := do
-  let results <- verifyToVcResults smtsolver program
+def verifyToDiagnosticModels (program : Program) (options : Options := Options.default) : IO (Array DiagnosticModel) := do
+  let results <- verifyToVcResults program options
   match results with
   | .error errors => return errors
   | .ok results => return results.filterMap toDiagnosticModel

StrataMain.lean

@@ -273,12 +273,20 @@ def pyAnalyzeCommand : Command where
         IO.print newPgm
       let solverName : String := "Strata/Languages/Python/z3_parallel.py"
       let verboseMode := VerboseMode.ofBool verbose
-      let vcResults ← IO.FS.withTempDir (fun tempDir =>
+      let options :=
+              { Options.default with
+                stopOnFirstError := false,
+                verbose := verboseMode,
+                removeIrrelevantAxioms := true,
+                solver := solverName }
+      let runVerification tempDir :=
           EIO.toIO
             (fun f => IO.Error.userError (toString f))
-            (Core.verify solverName newPgm tempDir .none
-              { Options.default with stopOnFirstError := false, verbose := verboseMode, removeIrrelevantAxioms := true }
-                                      (moreFns := Strata.Python.ReFactory)))
+            (Core.verify newPgm tempDir .none options
+                                      (moreFns := Strata.Python.ReFactory))
+      let vcResults ← match options.vcDirectory with
+                      | .none => IO.FS.withTempDir runVerification
+                      | .some tempDir => runVerification tempDir
       let mut s := ""
       for vcResult in vcResults do
         -- Build location string based on available metadata
@@ -362,7 +370,7 @@ def laurelAnalyzeCommand : Command where
           types := combinedProgram.types ++ laurelProgram.types
         }
 
-    let diagnostics ← Strata.Laurel.verifyToDiagnosticModels "cvc5" combinedProgram
+    let diagnostics ← Strata.Laurel.verifyToDiagnosticModels combinedProgram
 
     IO.println s!"==== DIAGNOSTICS ===="
     for diag in diagnostics do

StrataTest/DL/Imperative/Examples.lean

@@ -39,7 +39,7 @@ Result: failed
 Counterexample: (($__x0, Num), 0)
 -/
 #guard_msgs in
-#eval Strata.ArithPrograms.verify "cvc5" testProgram1
+#eval Strata.ArithPrograms.verify testProgram1
 
 ---------------------------------------------------------------------
 
@@ -65,7 +65,7 @@ Obligation: x_eq_y
 Result: verified
 -/
 #guard_msgs in
-#eval Strata.ArithPrograms.verify "cvc5" testProgram2
+#eval Strata.ArithPrograms.verify testProgram2
 
 ---------------------------------------------------------------------
 
@@ -91,6 +91,6 @@ Obligation: double_x_lemma
 Result: verified
 -/
 #guard_msgs in
-#eval Strata.ArithPrograms.verify "cvc5" testProgram3
+#eval Strata.ArithPrograms.verify testProgram3
 
 ---------------------------------------------------------------------

StrataTest/DL/Imperative/Verify.lean

@@ -25,7 +25,7 @@ def typedVarToSMT (v : String) (ty : Ty) : Except Format (String × Strata.SMT.T
   let ty' ← toSMTType ty
   return (v, ty')
 
-def verify (smtsolver : String) (cmds : Commands) (verbose : Bool) :
+def verify (cmds : Commands) (verbose : Bool) :
   EIO Format (Imperative.VCResults Arith.PureExpr) := do
   match typeCheckAndPartialEval cmds with
   | .error err =>
@@ -55,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 filename.toString
+                "cvc5" filename.toString
                 terms)
         match ans with
         | .ok (result, estate) =>
@@ -82,12 +82,12 @@ end Arith
 namespace Strata
 namespace ArithPrograms
 
-def verify (smtsolver : String) (pgm : Program)
+def verify (pgm : Program)
     (verbose : Bool := false) : IO (Imperative.VCResults Arith.PureExpr) := do
   let (program, errors) := ArithPrograms.TransM.run (ArithPrograms.translateProgram pgm.commands)
   if errors.isEmpty then
     EIO.toIO (fun f => IO.Error.userError (toString f))
-                (Arith.verify smtsolver program verbose)
+                (Arith.verify program verbose)
   else
     let errors := Std.Format.joinSep errors.toList "{Format.line}"
     panic! s!"DDM Transform Error: {errors}"

StrataTest/Languages/C_Simp/Examples/LoopSimple.lean

@@ -321,4 +321,4 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval Strata.C_Simp.verify "cvc5" LoopSimplePgm
+#eval Strata.C_Simp.verify LoopSimplePgm

StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean

@@ -287,4 +287,4 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval Strata.C_Simp.verify "cvc5" LoopTrivialPgm
+#eval Strata.C_Simp.verify LoopTrivialPgm

StrataTest/Languages/C_Simp/Examples/Min.lean

@@ -84,4 +84,4 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval Strata.C_Simp.verify "cvc5" MinPgm
+#eval Strata.C_Simp.verify MinPgm

StrataTest/Languages/C_Simp/Examples/SimpleTest.lean

@@ -122,4 +122,4 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval Strata.C_Simp.verify "cvc5" SimpleTestEnv
+#eval Strata.C_Simp.verify SimpleTestEnv

StrataTest/Languages/C_Simp/Examples/Trivial.lean

@@ -66,4 +66,4 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval Strata.C_Simp.verify "cvc5" TrivialPgm
+#eval Strata.C_Simp.verify TrivialPgm

StrataTest/Languages/Core/DatatypeVerificationTests.lean

@@ -109,7 +109,7 @@ Run verification and return a summary string.
 def runVerificationTest (testName : String) (program : Program) : IO String := do
   try
     match ← (IO.FS.withTempDir (fun tempDir =>
-      EIO.toIO' (Core.verify "cvc5" program tempDir .none Options.quiet))) with
+      EIO.toIO' (Core.verify program tempDir .none Options.quiet))) with
     | .error err =>
       return s!"{testName}: FAILED\n  Error: {err}"
     | .ok results =>

StrataTest/Languages/Core/Examples/AdvancedMaps.lean

@@ -212,6 +212,6 @@ Property: assert
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval verify "cvc5" mapPgm
+#eval verify mapPgm
 
 ---------------------------------------------------------------------