Expand Laurel implementation, so that tests T2 (impure expressions) and T3 (dag control flow) pass as well

Strata/DDM/Elab.lean

@@ -390,22 +390,17 @@ def elabDialect
   | .dialect loc dialect =>
     elabDialectRest fm dialects #[] inputContext loc dialect startPos stopPos
 
-def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (filePath : String) : IO (InputContext × Strata.Program) := do
-  let bytes ← Strata.Util.readBinInputSource filePath
-  let fileContent ← match String.fromUTF8? bytes with
-    | some s => pure s
-    | none => throw (IO.userError s!"File {filePath} contains non UTF-8 data")
+def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (input : InputContext) : IO Strata.Program := do
 
   let leanEnv ← Lean.mkEmptyEnvironment 0
-  let inputContext := Strata.Parser.stringInputContext filePath fileContent
 
   let isTrue mem := inferInstanceAs (Decidable (dialect ∈ dialects.dialects))
     | throw <| IO.userError "Internal {dialect} missing from loaded dialects."
 
   let strataProgram ←
-    match elabProgramRest dialects leanEnv inputContext dialect mem 0 with
+    match elabProgramRest dialects leanEnv input dialect mem 0 with
     | .ok program =>
-      pure (inputContext, program)
+      pure program
     | .error errors =>
       let errMsg ← errors.foldlM (init := "Parse errors:\n") fun msg e =>
         return s!"{msg}  {e.pos.line}:{e.pos.column}: {← e.data.toString}\n"

Strata/DL/Imperative/MetaData.lean

@@ -67,7 +67,7 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
 
 inductive Uri where
   | file (path: String)
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : ToFormat Uri where
  format fr := match fr with | .file path => path
@@ -76,7 +76,7 @@ structure FileRange where
   file: Uri
   start: Lean.Position
   ending: Lean.Position
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : ToFormat FileRange where
  format fr := f!"{fr.file}:{fr.start}-{fr.ending}"
@@ -100,7 +100,7 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       match v with
       | .expr e => f!"MetaDataElem.Value.expr {reprPrec e prec}"
       | .msg s => f!"MetaDataElem.Value.msg {s}"
-      | .fileRange fr => f!"MetaDataElem.Value.fileRange {fr}"
+      | .fileRange fr => f!"MetaDataElem.Value.fileRange {repr fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=

Strata/Languages/Boogie/Verifier.lean

@@ -113,22 +113,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,7 +142,7 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error ans
+  | _     =>  .error (stdout ++ output.stderr)
 
 open Imperative
 
@@ -220,8 +221,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)
 
@@ -382,7 +383,7 @@ def toDiagnostic (vcr : Boogie.VCResult) : Option Diagnostic := do
     | .fileRange range =>
       let message := match result with
         | .sat _ => "assertion does not hold"
-        | .unknown => "assertion verification result is unknown"
+        | .unknown => "assertion could not be proved"
         | .err msg => s!"verification error: {msg}"
         | _ => "verification failed"
       some {

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -12,25 +12,23 @@ import Strata.Languages.Boogie.Expressions
 
 namespace Laurel
 
-open Laurel
 open Std (ToFormat Format format)
 open Strata (QualifiedIdent Arg SourceRange)
 open Lean.Parser (InputContext)
 open Imperative (MetaData Uri FileRange)
 
 structure TransState where
   inputCtx : InputContext
-  errors : Array String
 
-abbrev TransM := StateM TransState
+abbrev TransM := StateT TransState (Except String)
 
-def TransM.run (ictx : InputContext) (m : TransM α) : (α × Array String) :=
-  let (v, s) := StateT.run m { inputCtx := ictx, errors := #[] }
-  (v, s.errors)
+def TransM.run (ictx : InputContext) (m : TransM α) : Except String α :=
+  match StateT.run m { inputCtx := ictx } with
+  | .ok (v, _) => .ok v
+  | .error e => .error e
 
-def TransM.error [Inhabited α] (msg : String) : TransM α := do
-  modify fun s => { s with errors := s.errors.push msg }
-  return panic msg
+def TransM.error (msg : String) : TransM α :=
+  throw msg
 
 def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.Expression :=
   let file := ictx.fileName
@@ -64,58 +62,150 @@ def translateIdent (arg : Arg) : TransM Identifier := do
 def translateBool (arg : Arg) : TransM Bool := do
   match arg with
   | .expr (.fn _ name) =>
-    if name == q`Laurel.boolTrue then
-      return true
-    else if name == q`Laurel.boolFalse then
-      return false
-    else
-      TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
+    match name with
+    | q`Laurel.boolTrue => return true
+    | q`Laurel.boolFalse => return false
+    | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
   | .op op =>
-    if op.name == q`Laurel.boolTrue then
-      return true
-    else if op.name == q`Laurel.boolFalse then
-      return false
-    else
-      TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
+    match op.name with
+    | q`Laurel.boolTrue => return true
+    | q`Laurel.boolFalse => return false
+    | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
+instance : Inhabited HighType where
+  default := .TVoid
+
+instance : Inhabited Parameter where
+  default := { name := "", type := .TVoid }
+
+def translateHighType (arg : Arg) : TransM HighType := do
+  match arg with
+  | .op op =>
+    match op.name with
+    | q`Laurel.intType => return .TInt
+    | q`Laurel.boolType => return .TBool
+    | _ => TransM.error s!"translateHighType expects intType or boolType, got {repr op.name}"
+  | _ => TransM.error s!"translateHighType expects operation"
+
+def translateNat (arg : Arg) : TransM Nat := do
+  let .num _ n := arg
+    | TransM.error s!"translateNat expects num literal"
+  return n
+
+def translateParameter (arg : Arg) : TransM Parameter := do
+  let .op op := arg
+    | TransM.error s!"translateParameter expects operation"
+  match op.name, op.args with
+  | q`Laurel.parameter, #[arg0, arg1] =>
+    let name ← translateIdent arg0
+    let paramType ← translateHighType arg1
+    return { name := name, type := paramType }
+  | q`Laurel.parameter, args =>
+    TransM.error s!"parameter needs two arguments, not {args.size}"
+  | _, _ =>
+    TransM.error s!"translateParameter expects parameter operation, got {repr op.name}"
+
+def translateParameters (arg : Arg) : TransM (List Parameter) := do
+  match arg with
+  | .commaSepList _ args =>
+    args.toList.mapM translateParameter
+  | _ => pure []
+
 instance : Inhabited Procedure where
   default := {
     name := ""
     inputs := []
-    output := .TVoid
+    outputs := []
     precondition := .LiteralBool true
     decreases := none
     determinism := Determinism.deterministic none
     modifies := none
     body := .Transparent (.LiteralBool true)
   }
 
+def getBinaryOp? (name : QualifiedIdent) : Option Operation :=
+  match name with
+  | q`Laurel.add => some Operation.Add
+  | q`Laurel.eq => some Operation.Eq
+  | q`Laurel.neq => some Operation.Neq
+  | q`Laurel.gt => some Operation.Gt
+  | q`Laurel.lt => some Operation.Lt
+  | q`Laurel.le => some Operation.Leq
+  | q`Laurel.ge => some Operation.Geq
+  | _ => none
+
 mutual
 
 partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
   match arg with
-  | .op op =>
-    if op.name == q`Laurel.assert then
-      let cond ← translateStmtExpr op.args[0]!
+  | .op op => match op.name, op.args with
+    | q`Laurel.assert, #[arg0] =>
+      let cond ← translateStmtExpr arg0
       let md ← getArgMetaData (.op op)
       return .Assert cond md
-    else if op.name == q`Laurel.assume then
-      let cond ← translateStmtExpr op.args[0]!
+    | q`Laurel.assume, #[arg0] =>
+      let cond ← translateStmtExpr arg0
       let md ← getArgMetaData (.op op)
       return .Assume cond md
-    else if op.name == q`Laurel.block then
-      let stmts ← translateSeqCommand op.args[0]!
+    | q`Laurel.block, #[arg0] =>
+      let stmts ← translateSeqCommand arg0
       return .Block stmts none
-    else if op.name == q`Laurel.literalBool then
-      let boolVal ← translateBool op.args[0]!
-      return .LiteralBool boolVal
-    else if op.name == q`Laurel.boolTrue then
-      return .LiteralBool true
-    else if op.name == q`Laurel.boolFalse then
-      return .LiteralBool false
-    else
-      TransM.error s!"Unknown operation: {op.name}"
+    | q`Laurel.boolTrue, _ => return .LiteralBool true
+    | q`Laurel.boolFalse, _ => return .LiteralBool false
+    | q`Laurel.int, #[arg0] =>
+      let n ← translateNat arg0
+      return .LiteralInt n
+    | q`Laurel.varDecl, #[arg0, typeArg, assignArg] =>
+      let name ← translateIdent arg0
+      let varType ← match typeArg with
+        | .option _ (some (.op typeOp)) => match typeOp.name, typeOp.args with
+          | q`Laurel.optionalType, #[typeArg0] => translateHighType typeArg0
+          | _, _ => pure .TInt
+        | _ => pure .TInt
+      let value ← match assignArg with
+        | .option _ (some (.op assignOp)) => match assignOp.args with
+          | #[assignArg0] => translateStmtExpr assignArg0 >>= (pure ∘ some)
+          | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
+        | .option _ none => pure none
+        | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
+      return .LocalVariable name varType value
+    | q`Laurel.identifier, #[arg0] =>
+      let name ← translateIdent arg0
+      return .Identifier name
+    | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0
+    | q`Laurel.assign, #[arg0, arg1] =>
+      let target ← translateStmtExpr arg0
+      let value ← translateStmtExpr arg1
+      return .Assign target value
+    | q`Laurel.call, #[arg0, argsSeq] =>
+      let callee ← translateStmtExpr arg0
+      let calleeName := match callee with
+        | .Identifier name => name
+        | _ => ""
+      let argsList ← match argsSeq with
+        | .commaSepList _ args => args.toList.mapM translateStmtExpr
+        | _ => pure []
+      return .StaticCall calleeName argsList
+    | q`Laurel.return, #[arg0] =>
+      let value ← translateStmtExpr arg0
+      return .Return (some value)
+    | q`Laurel.ifThenElse, #[arg0, arg1, elseArg] =>
+      let cond ← translateStmtExpr arg0
+      let thenBranch ← translateStmtExpr arg1
+      let elseBranch ← match elseArg with
+        | .option _ (some (.op elseOp)) => match elseOp.name, elseOp.args with
+          | q`Laurel.optionalElse, #[elseArg0] => translateStmtExpr elseArg0 >>= (pure ∘ some)
+          | _, _ => pure none
+        | _ => pure none
+      return .IfThenElse cond thenBranch elseBranch
+    | _, #[arg0, arg1] => match getBinaryOp? op.name with
+      | some primOp =>
+        let lhs ← translateStmtExpr arg0
+        let rhs ← translateStmtExpr arg1
+        return .PrimitiveOp primOp [lhs, rhs]
+      | none => TransM.error s!"Unknown operation: {op.name}"
+    | _, _ => TransM.error s!"Unknown operation: {op.name}"
   | _ => TransM.error s!"translateStmtExpr expects operation"
 
 partial def translateSeqCommand (arg : Arg) : TransM (List StmtExpr) := do
@@ -135,20 +225,37 @@ end
 def parseProcedure (arg : Arg) : TransM Procedure := do
   let .op op := arg
     | TransM.error s!"parseProcedure expects operation"
-  let name ← translateIdent op.args[0]!
-  let body ← translateCommand op.args[1]!
-  return {
-    name := name
-    inputs := []
-    output := .TVoid
-    precondition := .LiteralBool true
-    decreases := none
-    determinism := Determinism.deterministic none
-    modifies := none
-    body := .Transparent body
-  }
 
-/- Translate concrete Laurel syntax into abstract Laurel syntax -/
+  match op.name, op.args with
+  | q`Laurel.procedure, #[arg0, arg1, returnParamsArg, arg3] =>
+    let name ← translateIdent arg0
+    let parameters ← translateParameters arg1
+    -- returnParamsArg is ReturnParameters category, need to unwrap returnParameters operation
+    let returnParameters ← match returnParamsArg with
+      | .option _ (some (.op returnOp)) => match returnOp.name, returnOp.args with
+        | q`Laurel.returnParameters, #[returnArg0] => translateParameters returnArg0
+        | _, _ => TransM.error s!"Expected returnParameters operation, got {repr returnOp.name}"
+      | .option _ none => pure []
+      | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
+    let body ← translateCommand arg3
+    return {
+      name := name
+      inputs := parameters
+      outputs := returnParameters
+      precondition := .LiteralBool true
+      decreases := none
+      determinism := Determinism.deterministic none
+      modifies := none
+      body := .Transparent body
+    }
+  | q`Laurel.procedure, args =>
+    TransM.error s!"parseProcedure expects 4 arguments, got {args.size}"
+  | _, _ =>
+    TransM.error s!"parseProcedure expects procedure, got {repr op.name}"
+
+/--
+Translate concrete Laurel syntax into abstract Laurel syntax
+-/
 def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
   -- Unwrap the program operation if present
   -- The parsed program may have a single `program` operation wrapping the procedures