Changes to enable communication with JVerify

Strata/DDM/AST.lean

@@ -8,6 +8,7 @@ module
 public import Std.Data.HashMap.Basic
 public import Strata.DDM.Util.ByteArray
 public import Strata.DDM.Util.Decimal
+public import Lean.Data.Position
 public import Strata.DDM.AST.Datatype
 
 import Std.Data.HashMap
@@ -18,6 +19,7 @@ set_option autoImplicit false
 
 public section
 namespace Strata
+open Std (ToFormat Format format)
 
 abbrev DialectName := String
 
@@ -271,16 +273,46 @@ 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
 
 namespace SourceRange
 
 def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
 
+instance : ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
 end SourceRange
 
+inductive Uri where
+  | file (path: String)
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
+
+structure File2dRange where
+  file: Uri
+  start: Lean.Position
+  ending: Lean.Position
+  deriving DecidableEq, Repr
+
+instance : ToFormat File2dRange where
+ format fr :=
+    let baseName := match fr.file with
+                    | .file path => (path.splitToList (· == '/')).getLast!
+    f!"{baseName}({fr.start.line}, {fr.start.column})-({fr.ending.line}, {fr.ending.column})"
+
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange
 abbrev Operation := OperationF SourceRange

Strata/DDM/Ion.lean

@@ -294,7 +294,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 {a.size} values."
   let entries := a[0]
   let .isTrue p := inferInstanceAs (Decidable (entries.size = 2))
     | throw s!"Expected symbol table and value in dialect."
@@ -1411,6 +1411,11 @@ private instance : FromIon Dialect where
 
 end Dialect
 
+structure StrataFile where
+  filePath : String
+  program : Program
+  deriving Inhabited
+
 namespace Program
 
 private instance : CachedToIon Program where
@@ -1436,7 +1441,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 =>
@@ -1451,5 +1456,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 h : 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,36 +66,23 @@ 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, Repr, Inhabited
-
-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, Repr, Inhabited
-
-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)
+  /-- Metadata value in the form of a fileRange. -/
+  | file2dRange (r: Strata.File2dRange)
 
 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}"
+              | .file2dRange r => f!"{r}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -103,13 +91,15 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       | .expr e => f!".expr {reprPrec e prec}"
       | .msg s => f!".msg {s}"
       | .fileRange fr => f!".fileRange {fr}"
+      | .file2dRange fr => f!".file2dRange {fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   match v1, v2 with
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
+  | .file2dRange r1, .file2dRange r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -185,7 +175,7 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
-def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Imperative.FileRange := do
+def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Strata.FileRange := do
   let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with
     | .fileRange fileRange =>
@@ -196,7 +186,7 @@ def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? :
     Option Std.Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
+  | .file2dRange m =>
     let baseName := match m.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
     if includeEnd? then

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

@@ -50,7 +50,7 @@ def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative
   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, .file2dRange ⟨ uri, startPos, endPos ⟩ ⟩
   #[fileRangeElt]
 
 def getOpMetaData (op : Operation) : TransM (Imperative.MetaData Boogie.Expression) :=