[Strata] Better isolation of non-determinism in Core

Examples/NondetCond.core.st

@@ -0,0 +1,14 @@
+// Test non-deterministic conditions in if and while statements
+procedure nondet_if()
+  modifies x;
+  ensures x >= 0;
+{
+  var x : int;
+  x := 0;
+  if (*) {
+    x := 1;
+  } else {
+    x := 2;
+  }
+  assert x >= 0;
+}

Strata/Backends/CBMC/CollectSymbols.lean

@@ -125,11 +125,11 @@ private def collectGlobalSymbols (pgm : Core.Program) :
       let gty ← Lambda.LMonoTy.toGotoType ty.toMonoTypeUnsafe
       let tyJson := CProverGOTO.tyToJson gty
       let valueJson ← match e with
-        | some expr =>
+        | .det expr =>
           let gotoExpr ← Lambda.LExpr.toGotoExprCtx
             (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] expr
           (CProverGOTO.exprToJson gotoExpr).mapError (fun e => f!"{e}")
-        | none => pure (Lean.Json.mkObj [("id", "nil")])
+        | .nondet => pure (Lean.Json.mkObj [("id", "nil")])
       syms := syms ++ [(gname, {
         baseName := gname
         isLvalue := true

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -99,7 +99,7 @@ def cmdToJson (e : Core.Command) (loc: SourceLoc) : Except String Json :=
       ])
     | .set ("ret") _ _ =>
       returnStmt loc.functionName
-    | .set name expr _ => do
+    | .set name (.det expr) _ => do
       let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" }
       return (mkCodeBlock "expression" "6" loc.functionName #[
         mkSideEffect "assign" "6" loc.functionName mkIntType #[
@@ -165,7 +165,7 @@ def cmdToJson (e : Core.Command) (loc: SourceLoc) : Except String Json :=
     | .cover _ _ md =>
        throw s!"{Imperative.MetaData.formatFileRangeD md}\
                   cover unimplemented"
-    | .havoc _ md =>
+    | .set _ .nondet md =>
        throw s!"{Imperative.MetaData.formatFileRangeD md}\
                   havoc unimplemented"
 
@@ -188,7 +188,7 @@ def stmtToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (L
   (e : Imperative.Stmt P Command) (loc: SourceLoc) : Except String Json :=
   match e with
   | .cmd cmd => cmdToJson cmd loc
-  | .ite cond thenb elseb _ => do
+  | .ite (.det cond) thenb elseb _ => do
     let converted_cond : Lambda.LExpr I.mono := @HasLExpr.expr_eq P (I:=I) _ ▸ cond
     return Json.mkObj [
       ("id", "code"),

Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean

@@ -117,14 +117,10 @@ def Core.Cmd.renameVars (frto : Map String String) (c : Imperative.Cmd Core.Expr
     let new := name_alt.getD (Core.CoreIdent.toPretty name)
     .init new ty e' (convertMetaData md)
   | .set name e md =>
-    let e' := substVarNames e frto
+    let e' := e.map (substVarNames · frto)
     let name_alt := frto.find? (Core.CoreIdent.toPretty name)
     let new := name_alt.getD (Core.CoreIdent.toPretty name)
     .set new e' (convertMetaData md)
-  | .havoc name md =>
-    let name_alt := frto.find? (Core.CoreIdent.toPretty name)
-    let new := name_alt.getD (Core.CoreIdent.toPretty name)
-    .havoc new (convertMetaData md)
   | .assume label e md =>
     let e' := substVarNames e frto
     .assume label e' (convertMetaData md)

Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean

@@ -61,8 +61,7 @@ private def renameCmd
     (rn : Std.HashMap String String)
     : Imperative.Cmd Core.Expression → Imperative.Cmd Core.Expression
   | .init name ty e md => .init (renameIdent rn name) ty (e.map (renameExpr rn)) md
-  | .set name e md => .set (renameIdent rn name) (renameExpr rn e) md
-  | .havoc name md => .havoc (renameIdent rn name) md
+  | .set name e md => .set (renameIdent rn name) (e.map (renameExpr rn)) md
   | .assert l e md => .assert l (renameExpr rn e) md
   | .assume l e md => .assume l (renameExpr rn e) md
   | .cover l e md => .cover l (renameExpr rn e) md
@@ -79,10 +78,16 @@ private partial def unwrapCmdExt
   | .ite c t e md => do
     let t' ← t.mapM (unwrapCmdExt rn)
     let e' ← e.mapM (unwrapCmdExt rn)
-    .ok (.ite (renameExpr rn c) t' e' md)
+    let c' := match c with
+      | .det expr => Imperative.ExprOrNondet.det (renameExpr rn expr)
+      | .nondet => .nondet
+    .ok (.ite c' t' e' md)
   | .loop g m i body md => do
     let body' ← body.mapM (unwrapCmdExt rn)
-    .ok (.loop (renameExpr rn g) (m.map (renameExpr rn)) (i.map (renameExpr rn)) body' md)
+    let g' := match g with
+      | .det expr => Imperative.ExprOrNondet.det (renameExpr rn expr)
+      | .nondet => .nondet
+    .ok (.loop g' (m.map (renameExpr rn)) (i.map (renameExpr rn)) body' md)
   | .exit l md => .ok (.exit l md)
   | .funcDecl _d _md =>
     .error f!"[unwrapCmdExt] Unexpected funcDecl; should have been lifted by collectFuncDecls."
@@ -186,7 +191,9 @@ private partial def coreStmtsToGoto
       | .ite cond thenb elseb md =>
         if hasCallStmt thenb || hasCallStmt elseb then
           let srcLoc := Imperative.metadataToSourceLoc md pname trans.sourceText
-          let cond_expr ← toExpr (renameExpr rn cond)
+          let cond_expr ← match cond with
+            | .det e => toExpr (renameExpr rn e)
+            | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : CProverGOTO.Expr }
           let (trans, goto_else_idx) :=
             Imperative.emitCondGoto (CProverGOTO.Expr.not cond_expr) srcLoc trans
           let trans ← coreStmtsToGoto Env pname rn thenb trans
@@ -206,7 +213,9 @@ private partial def coreStmtsToGoto
           let srcLoc := Imperative.metadataToSourceLoc md pname trans.sourceText
           let loop_head := trans.nextLoc
           let trans := Imperative.emitLabel s!"loop_{loop_head}" srcLoc trans
-          let guard_expr ← toExpr (renameExpr rn guard)
+          let guard_expr ← match guard with
+            | .det e => toExpr (renameExpr rn e)
+            | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : CProverGOTO.Expr }
           let (trans, goto_end_idx) :=
             Imperative.emitCondGoto (CProverGOTO.Expr.not guard_expr) srcLoc trans
           let trans ← coreStmtsToGoto Env pname rn body trans

Strata/Backends/CBMC/StrataToCBMC.lean

@@ -224,7 +224,7 @@ def cmdToJson (e : Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json
       ]
     ])
   | .set ("return") _ _ => returnStmt loc.functionName
-  | .set name expr _ =>
+  | .set name (.det expr) _ =>
     let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" }
     return (mkCodeBlock "expression" "6" loc.functionName (config := cfg) #[
       mkSideEffect "assign" "6" loc.functionName (mkIntType cfg) (config := cfg) #[
@@ -287,7 +287,7 @@ def cmdToJson (e : Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json
         ]
       ]
     ])
-  | .havoc _ _ | .cover _ _ _ => throw "cmdToJson: Unimplemented"
+  | .set _ .nondet _ | .cover _ _ _ => throw "cmdToJson: Unimplemented"
 
 mutual
 def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json := do
@@ -307,7 +307,7 @@ def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Comm
  def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Except String Json :=
   match e with
   | .cmd cmd => cmdToJson cmd loc
-  | .ite cond thenb elseb _ => do
+  | .ite (.det cond) thenb elseb _ => do
     return Json.mkObj [
       ("id", "code"),
       ("namedSub", Json.mkObj [

Strata/DL/Imperative/Cmd.lean

@@ -24,6 +24,21 @@ programs. These constructs are parameterized by `PureExpr`, which can be
 instantiated with any language construct that does not have side-effects.
 -/
 
+/-! ## Deterministic or Non-deterministic Expressions
+
+`ExprOrNondet` represents a value that is either a deterministic expression or
+a non-deterministic (arbitrary) choice. This is used in commands where the
+right-hand side can be either a concrete expression or a havoc.
+-/
+
+/-- A value that is either a deterministic expression or a non-deterministic choice. -/
+inductive ExprOrNondet (P : PureExpr) where
+  /-- A deterministic expression. -/
+  | det (e : P.Expr)
+  /-- A non-deterministic (arbitrary) value. -/
+  | nondet
+  deriving Inhabited
+
 /-! ## Commands
 
 Commands form the core of the Imperative dialect. They include constructs for
@@ -37,13 +52,12 @@ Commands don't create local control flow, and are typically used as a parameter
 to `Imperative.Stmt` or other similar types.
 -/
 inductive Cmd (P : PureExpr) : Type where
-  /-- Define a variable called `name` with type `ty` and optional initial value `e`.
-      When `e` is `none`, the variable is initialized with an arbitrary value. -/
-  | init     (name : P.Ident) (ty : P.Ty) (e : Option P.Expr) (md : (MetaData P))
-  /-- Assign `e` to a pre-existing variable `name`. -/
-  | set      (name : P.Ident) (e : P.Expr) (md : (MetaData P))
-  /-- Assigns an arbitrary value to an existing variable `name`. -/
-  | havoc    (name : P.Ident) (md : (MetaData P))
+  /-- Define a variable called `name` with type `ty` and value `e`.
+      When `e` is `.nondet`, the variable is initialized with an arbitrary value. -/
+  | init     (name : P.Ident) (ty : P.Ty) (e : ExprOrNondet P) (md : (MetaData P))
+  /-- Assign `e` to a pre-existing variable `name`.
+      When `e` is `.nondet`, assigns an arbitrary value (havoc semantics). -/
+  | set      (name : P.Ident) (e : ExprOrNondet P) (md : (MetaData P))
   /-- Checks if condition `b` is true on _all_ paths on which this command is
     encountered. Reports an error if `b` does not hold on _any_ of these paths.
   -/
@@ -60,13 +74,13 @@ inductive Cmd (P : PureExpr) : Type where
 @[expose] abbrev Cmds (P : PureExpr) := List (Cmd P)
 
 instance [Inhabited P.Ident]: Inhabited (Cmd P) where
-  default := .havoc default default
+  default := .set default .nondet default
 
 ---------------------------------------------------------------------
 
 def Cmd.getMetaData (c : Cmd P) : MetaData P :=
   match c with
-  | .init _ _ _ md | .set _ _ md | .havoc _ md
+  | .init _ _ _ md | .set _ _ md
   | .assert _ _ md | .assume _ _ md | .cover _ _ md =>
    md
 
@@ -84,26 +98,34 @@ class HasHavoc (P : PureExpr) (CmdT : Type) where
   havoc : P.Ident → MetaData P → CmdT
 
 instance : HasHavoc P (Cmd P) where
-  havoc x md := .havoc x md
+  havoc x md := .set x .nondet md
 
-/-- Declare a variable with a given type and optional initial value. -/
+/-- Declare a variable with a given type and value (deterministic or non-deterministic). -/
 class HasInit (P : PureExpr) (CmdT : Type) where
-  init : P.Ident → P.Ty → Option P.Expr → MetaData P → CmdT
+  init : P.Ident → P.Ty → ExprOrNondet P → MetaData P → CmdT
 
 instance : HasInit P (Cmd P) where
   init x ty e md := .init x ty e md
 
 ---------------------------------------------------------------------
 
+/-- Get all variables accessed by an `ExprOrNondet`. -/
+def ExprOrNondet.getVars [HasVarsPure P P.Expr] (e : ExprOrNondet P) : List P.Ident :=
+  match e with
+  | .det e => HasVarsPure.getVars e
+  | .nondet => []
+
+/-- Map a function over the expression in an `ExprOrNondet`. -/
+def ExprOrNondet.map {P Q : PureExpr} (f : P.Expr → Q.Expr) : ExprOrNondet P → ExprOrNondet Q
+  | .det e => .det (f e)
+  | .nondet => .nondet
+
 mutual
 /-- Get all variables accessed by `c`. -/
 def Cmd.getVars [HasVarsPure P P.Expr] (c : Cmd P) : List P.Ident :=
   match c with
-  | .init _ _ eOpt _ => match eOpt with
-    | some e => HasVarsPure.getVars e
-    | none => []
-  | .set _ e _ => HasVarsPure.getVars e
-  | .havoc _ _ => []
+  | .init _ _ e _ => e.getVars
+  | .set _ e _ => e.getVars
   | .assert _ e _ => HasVarsPure.getVars e
   | .assume _ e _ => HasVarsPure.getVars e
   | .cover _ e _ => HasVarsPure.getVars e
@@ -142,7 +164,6 @@ def Cmd.modifiedVars (c : Cmd P) : List P.Ident :=
   match c with
   | .init _ _ _ _ => []
   | .set name _ _ => [name]
-  | .havoc name _ => [name]
   | .assert _ _ _ => []
   | .assume _ _ _ => []
   | .cover _ _ _ => []
@@ -168,13 +189,22 @@ instance (P : PureExpr) : HasVarsImp P (Cmds P) where
 
 open Std (ToFormat Format format)
 
+def formatExprOrNondet (P : PureExpr) (e : ExprOrNondet P)
+    [ToFormat P.Expr] : Format :=
+  match e with
+  | .det e => format e
+  | .nondet => f!"*"
+
+instance [ToFormat P.Expr] : ToFormat (ExprOrNondet P) where
+  format e := formatExprOrNondet P e
+
 def formatCmd (P : PureExpr) (c : Cmd P)
     [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=
   match c with
-  | .init name ty (some e) _md => f!"init ({name} : {ty}) := {e}"
-  | .init name ty none _md => f!"init ({name} : {ty})"
-  | .set name e _md => f!"{name} := {e}"
-  | .havoc name _md => f!"havoc {name}"
+  | .init name ty (.det e) _md => f!"init ({name} : {ty}) := {e}"
+  | .init name ty .nondet _md => f!"init ({name} : {ty})"
+  | .set name (.det e) _md => f!"{name} := {e}"
+  | .set name .nondet _md => f!"havoc {name}"
   | .assert label b _md => f!"assert [{label}] {b}"
   | .assume label b _md => f!"assume [{label}] {b}"
   | .cover label b _md => f!"cover [{label}] {b}"

Strata/DL/Imperative/CmdEval.lean

@@ -23,42 +23,43 @@ def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P 
   | some _ => (c, σ)
   | none =>
     match c with
-    | .init x ty eOpt md =>
+    | .init x ty e md =>
       match EC.lookup σ x with
       | none =>
-        match eOpt with
-        | some e =>
-          let (e, σ) := EC.preprocess σ c e
-          let e := EC.eval σ e
-          let σ := EC.update σ x ty e
-          let c' := .init x ty (some e) md
+        match e with
+        | .det expr =>
+          let (expr, σ) := EC.preprocess σ c expr
+          let expr := EC.eval σ expr
+          let σ := EC.update σ x ty expr
+          let c' := .init x ty (.det expr) md
           (c', σ)
-        | none =>
+        | .nondet =>
           -- Unconstrained initialization - generate a fresh value
-          let (e, σ) := EC.genFreeVar σ x ty
-          let σ := EC.update σ x ty e
-          let c' := .init x ty none md
+          let (expr, σ) := EC.genFreeVar σ x ty
+          let σ := EC.update σ x ty expr
+          let c' := .init x ty .nondet md
           (c', σ)
       | some (xv, xty) => (c, EC.updateError σ (.InitVarExists (x, xty) xv))
 
     | .set x e md =>
       match EC.lookup σ x with
-      | none => (c, EC.updateError σ (.AssignVarNotExists x e))
+      | none =>
+        match e with
+        | .det expr => (c, EC.updateError σ (.AssignVarNotExists x expr))
+        | .nondet => (c, EC.updateError σ (.HavocVarNotExists x))
       | some (_xv, xty) =>
-        let (e, σ) := EC.preprocess σ c e
-        let e := EC.eval σ e
-        let σ := EC.update σ x xty e
-        let c' := .set x e md
-        (c', σ)
-
-    | .havoc x md =>
-      match EC.lookup σ x with
-      | none => (c, EC.updateError σ (.HavocVarNotExists x))
-      | some (_, xty) =>
-        let (e, σ) := EC.genFreeVar σ x xty
-        let σ := EC.update σ x xty e
-        let c' := .havoc x (md.pushElem (.var x) (.expr e))
-        (c', σ)
+        match e with
+        | .det expr =>
+          let (expr, σ) := EC.preprocess σ c expr
+          let expr := EC.eval σ expr
+          let σ := EC.update σ x xty expr
+          let c' := .set x (.det expr) md
+          (c', σ)
+        | .nondet =>
+          let (expr, σ) := EC.genFreeVar σ x xty
+          let σ := EC.update σ x xty expr
+          let c' := .set x .nondet (md.pushElem (.var x) (.expr expr))
+          (c', σ)
 
     | .assert label e md =>
       let (e, σ) := EC.preprocess σ c e

Strata/DL/Imperative/CmdSemantics.lean

@@ -282,29 +282,29 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     InitState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ---
-    EvalCmd δ σ (.init x _ (some e) _) σ'
+    EvalCmd δ σ (.init x _ (.det e) _) σ'
 
   /-- Initialize `x` with an unconstrained value (havoc semantics). -/
   | eval_init_unconstrained :
     InitState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ---
-    EvalCmd δ σ (.init x _ none _) σ'
+    EvalCmd δ σ (.init x _ .nondet _) σ'
 
   /-- If `e` evaluates to a value `v`, assign `x` according to `UpdateState`. -/
   | eval_set :
     δ σ e = .some v →
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
-    EvalCmd δ σ (.set x e _) σ'
+    EvalCmd δ σ (.set x (.det e) _) σ'
 
   /-- Assign `x` an arbitrary value `v` according to `UpdateState`. -/
-  | eval_havoc :
+  | eval_set_nondet :
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
-    EvalCmd δ σ (.havoc x _) σ'
+    EvalCmd δ σ (.set x .nondet _) σ'
 
   /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. This semantics
   does not have a concept of an erroneous execution. -/