Changes to enable communication with JVerify

Strata/DDM/AST.lean

@@ -16,6 +16,7 @@ set_option autoImplicit false
 
 public section
 namespace Strata
+open Std (ToFormat Format format)
 
 abbrev DialectName := String
 
@@ -233,7 +234,25 @@ structure SourceRange where
   start : String.Pos.Raw
   /-- One past the end of the range. -/
   stop : String.Pos.Raw
-deriving BEq, Inhabited, Repr
+deriving DecidableEq, Inhabited, Repr
+
+instance : ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
+inductive Uri where
+  | file (path: String)
+  deriving DecidableEq, Repr
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
 
 namespace SourceRange
 

Strata/DDM/Ion.lean

@@ -183,7 +183,7 @@ private protected def asList (v : Ion SymbolId) : FromIonM { a : Array (Ion Symb
   match v with
   | .mk (.list args) =>
     return .mk args (by simp; omega)
-  | _ => throw s!"Expected list"
+  | x => throw s!"Expected list but got {repr x}"
 
 private protected def asSexp (name : String) (v : Ion SymbolId) : FromIonM ({ a : Array (Ion SymbolId) // a.size > 0 ∧ sizeOf a < sizeOf v}) :=
   match v with
@@ -284,7 +284,7 @@ private def deserializeValue {α} (bs : ByteArray) (act : Ion SymbolId → FromI
       throw s!"Error reading Ion: {msg} (offset = {off})"
     | .ok a => pure a
   let .isTrue p := inferInstanceAs (Decidable (a.size = 1))
-    | throw s!"Expected single Ion value."
+    | throw s!"Expected single Ion value, but got {repr a}."
   let entries := a[0]
   let .isTrue p := inferInstanceAs (Decidable (entries.size = 2))
     | throw s!"Expected symbol table and value in dialect."
@@ -1294,6 +1294,11 @@ private instance : FromIon Dialect where
 
 end Dialect
 
+structure StrataFile where
+  filePath : String
+  program : Program
+  deriving Inhabited
+
 namespace Program
 
 private instance : CachedToIon Program where
@@ -1319,7 +1324,7 @@ def fromIonFragment (f : Ion.Fragment)
     commands := ← fromIonFragmentCommands f
   }
 
-def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
+def fileFromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
   let (hdr, frag) ←
     match Strata.Ion.Header.parse bytes with
     | .error msg =>
@@ -1334,5 +1339,60 @@ def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray)
       throw s!"{name} program found when {dialect} expected."
     fromIonFragment frag dialects dialect
 
+def filesFromIon (dialects : DialectMap) (bytes : ByteArray) : Except String (List StrataFile) := do
+  let ctx ←
+    match Ion.deserialize bytes with
+    | .error (off, msg) => throw s!"Error reading Ion: {msg} (offset = {off})"
+    | .ok a =>
+      if p : a.size = 1 then
+        pure a[0]
+      else
+        throw s!"Expected single Ion value"
+
+  let .isTrue p := inferInstanceAs (Decidable (ctx.size = 2))
+    | throw "Expected symbol table and value"
+
+  let symbols ←
+    match SymbolTable.ofLocalSymbolTable ctx[0] with
+    | .error (p, msg) => throw s!"Error at {p}: {msg}"
+    | .ok symbols => pure symbols
+
+  let ionCtx : FromIonContext := ⟨symbols⟩
+
+  let ⟨filesList, _⟩ ← FromIonM.asList ctx[1]! ionCtx
+
+  let tbl := symbols
+  let filePathId := tbl.symbolId! "filePath"
+  let programId := tbl.symbolId! "program"
+
+  filesList.toList.mapM fun fileEntry => do
+    let fields ← FromIonM.asStruct0 fileEntry ionCtx
+
+    let some (_, filePathData) := fields.find? (·.fst == filePathId)
+      | throw "Could not find 'filePath' field"
+
+    let some (_, programData) := fields.find? (·.fst == programId)
+      | throw "Could not find 'program' field"
+
+    let filePath ← FromIonM.asString "filePath" filePathData ionCtx
+
+    let ⟨programValues, _⟩ ← FromIonM.asList programData ionCtx
+    let .isTrue ne := inferInstanceAs (Decidable (programValues.size ≥ 1))
+      | throw "Expected program header"
+
+    let hdr ← Ion.Header.fromIon programValues[0] ionCtx
+    let dialect ← match hdr with
+      | .program name => pure name
+      | .dialect _ => throw "Expected program, not dialect"
+
+    let frag : Ion.Fragment := {
+      symbols := symbols,
+      values := programValues,
+      offset := 1
+    }
+
+    let program ← fromIonFragment frag dialects dialect
+
+    pure { filePath := filePath, program := program }
+
 end Strata.Program
-end

Strata/DL/Imperative/MetaData.lean

@@ -6,6 +6,7 @@
 
 import Strata.DL.Imperative.PureExpr
 import Strata.DL.Util.DecidableEq
+import Strata.DDM.AST
 import Lean.Data.Position
 
 namespace Imperative
@@ -65,31 +66,14 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
       | .label s => f!"MetaDataElem.Field.label {s}"
     Repr.addAppParen res prec
 
-inductive Uri where
-  | file (path: String)
-  deriving DecidableEq
-
-instance : ToFormat Uri where
- format fr := match fr with | .file path => path
-
-structure FileRange where
-  file: Uri
-  start: Lean.Position
-  ending: Lean.Position
-  deriving DecidableEq
-
-instance : ToFormat FileRange where
- format fr := f!"{fr.file}:{fr.start}-{fr.ending}"
-
 /-- A metadata value, which can be either an expression, a message, or a fileRange -/
 inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of a structured expression. -/
   | expr (e : P.Expr)
   /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
-  | fileRange (r: FileRange)
-
+  | fileRange (r: Strata.FileRange)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
   format f := match f with | .expr e => f!"{e}" | .msg s => f!"{s}" | .fileRange r => f!"{r}"

Strata/DL/Imperative/SMTUtils.lean

@@ -115,31 +115,32 @@ def processModel {P : PureExpr} [ToFormat P.Ident]
     | none => .error f!"Cannot find model for id: {id}"
     | some p => .ok p.value
 
-def runSolver (solver : String) (args : Array String) : IO String := do
+def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {
     cmd := solver
     args := args
   }
   -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
   --                         stderr: {repr output.stderr}\n\
   --                         stdout: {repr output.stdout}"
-  return output.stdout
+  return output
 
 def solverResult {P : PureExpr} [ToFormat P.Ident]
     (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
-    (vars : List P.TypedIdent) (ans : String)
+    (vars : List P.TypedIdent) (output : IO.Process.Output)
     (E : Strata.SMT.EncoderState) : Except Format (Result P.TypedIdent) := do
-  let pos := (ans.find (fun c => c == '\n' || c == '\r')).byteIdx
-  let verdict := ans.take pos
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n' || c == '\r')).byteIdx
+  let verdict := stdout.take pos
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
     let model ← processModel typedVarToSMTFn vars rawModel E
     .ok (.sat model)
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | other     =>  .error other
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 def VC_folder_name: String := "vcs"
 
@@ -169,8 +170,8 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
       .ok "--produce-models"
     else
       return .error f!"Unsupported SMT solver: {smtsolver}"
-  let solver_out ← runSolver smtsolver #[filename, produce_models]
-  match solverResult typedVarToSMTFn vars solver_out estate with
+  let solver_output ← runSolver smtsolver #[filename, produce_models]
+  match solverResult typedVarToSMTFn vars solver_output estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 

Strata/Languages/Boogie/DDMTransform/Translate.lean

@@ -47,10 +47,8 @@ def TransM.error [Inhabited α] (msg : String) : TransM α := do
 
 def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.Expression :=
   let file := ictx.fileName
-  let startPos := ictx.fileMap.toPosition sr.start
-  let endPos := ictx.fileMap.toPosition sr.stop
   let uri: Uri := .file file
-  let fileRangeElt := ⟨ MetaData.fileRange, .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+  let fileRangeElt := ⟨ MetaData.fileRange, .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
 def getOpMetaData (op : Operation) : TransM (Imperative.MetaData Boogie.Expression) :=

Strata/Languages/Boogie/Verifier.lean

@@ -11,12 +11,14 @@ import Strata.Languages.Boogie.SMTEncoder
 import Strata.DL.Imperative.MetaData
 import Strata.DL.Imperative.SMTUtils
 import Strata.DL.SMT.CexParser
+import Strata.DDM.AST
 
 ---------------------------------------------------------------------
 
 namespace Strata.SMT.Encoder
 
 open Strata.SMT.Encoder
+open Strata
 
 -- Derived from Strata.SMT.Encoder.encode.
 def encodeBoogie (ctx : Boogie.SMT.Context) (prelude : SolverM Unit) (ts : List Term) :
@@ -113,22 +115,23 @@ instance : ToFormat Result where
 
 def VC_folder_name: String := "vcs"
 
-def runSolver (solver : String) (args : Array String) : IO String := do
+def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {
     cmd := solver
     args := args
   }
   -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
   --                         stderr: {repr output.stderr}\n\
   --                         stdout: {repr output.stdout}"
-  return output.stdout
+  return output
 
-def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
+def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.Output)
     (ctx : SMT.Context) (E : EncoderState) :
   Except Format Result := do
-  let pos := (ans.find (fun c => c == '\n')).byteIdx
-  let verdict := (ans.take pos).trim
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n')).byteIdx
+  let verdict := (stdout.take pos).trim
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
@@ -141,17 +144,21 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error ans
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 open Imperative
 
-def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr] (md : MetaData P): Option Format := do
+def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr]
+  (files: Map Strata.Uri Lean.FileMap)
+  (md : MetaData P): Option Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
-    let baseName := match m.file with
+  | .fileRange fileRange =>
+    let fileMap := (files.find? fileRange.file).get!
+    let startPos := fileMap.toPosition fileRange.range.start
+    let baseName := match fileRange.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
-    return f!"{baseName}({m.start.line}, {m.start.column})"
+    return f!"{baseName}({startPos.line}, {startPos.column})"
   | _ => none
 
 structure VCResult where
@@ -220,8 +227,8 @@ def dischargeObligation
   let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
   if options.verbose then IO.println s!"Wrote problem to {filename}."
   let flags := getSolverFlags options smtsolver
-  let solver_out ← runSolver smtsolver (#[filename] ++ flags)
-  match solverResult vars solver_out ctx estate with
+  let output ← runSolver smtsolver (#[filename] ++ flags)
+  match solverResult vars output ctx estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
@@ -290,7 +297,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
         -- let rand_suffix ← IO.rand 0 0xFFFFFFFF
         let ans ←
             IO.toEIO
-              (fun e => f!"{e}")
+              (fun e => f!"IO error: {e}")
               (dischargeObligation options
                 (ProofObligation.getVars obligation) smtsolver
                   (Imperative.smt2_filename obligation.label)
@@ -364,35 +371,50 @@ def verify
   else
     panic! s!"DDM Transform Error: {repr errors}"
 
-/-- A diagnostic produced by analyzing a file -/
-structure Diagnostic where
-  start : Lean.Position
-  ending : Lean.Position
+structure DiagnosticModel where
+  fileRange : Strata.FileRange
   message : String
   deriving Repr, BEq
 
-def toDiagnostic (vcr : Boogie.VCResult) : Option Diagnostic := do
-  -- Only create a diagnostic if the result is not .unsat (i.e., verification failed)
+def toDiagnosticModel (vcr : Boogie.VCResult) : Option DiagnosticModel := do
   match vcr.result with
   | .unsat => none  -- Verification succeeded, no diagnostic
   | result =>
-    -- Extract file range from metadata
     let fileRangeElem ← vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
     match fileRangeElem.value with
-    | .fileRange range =>
+    | .fileRange fileRange =>
       let message := match result with
         | .sat _ => "assertion does not hold"
         | .unknown => "assertion verification result is unknown"
         | .err msg => s!"verification error: {msg}"
         | _ => "verification failed"
+
       some {
         -- Subtract headerOffset to account for program header we added
-        start := { line := range.start.line, column := range.start.column }
-        ending := { line := range.ending.line, column := range.ending.column }
+        fileRange := fileRange
         message := message
       }
     | _ => none
 
+structure Diagnostic where
+  start : Lean.Position
+  ending : Lean.Position
+  message : String
+  deriving Repr, BEq
+
+def toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
+  let modelOption := toDiagnosticModel vcr
+  modelOption.map (fun dm =>
+      let fileMap := (files.find? dm.fileRange.file).get!
+      let startPos := fileMap.toPosition dm.fileRange.range.start
+      let endPos := fileMap.toPosition dm.fileRange.range.stop
+      {
+        start := { line := startPos.line, column := startPos.column }
+        ending := { line := endPos.line, column := endPos.column }
+        message := dm.message
+      }
+    )
+
 end Strata
 
 ---------------------------------------------------------------------