Create variables for old expressions in Boogie

Strata/DL/Lambda/Identifiers.lean

@@ -22,7 +22,7 @@ Identifiers with a name and additional metadata
 structure Identifier (IDMeta : Type) : Type where
   name : String
   metadata : IDMeta
-deriving Repr, DecidableEq, Inhabited
+deriving Repr, DecidableEq, Inhabited, Hashable, Ord
 
 instance : ToFormat (Identifier IDMeta) where
   format i := i.name

Strata/Languages/Boogie/DDMTransform/Translate.lean

@@ -5,8 +5,10 @@
 -/
 
 import Strata.DDM.AST
+import Strata.DL.Lambda.Identifiers
 import Strata.Languages.Boogie.DDMTransform.Parse
 import Strata.Languages.Boogie.BoogieGen
+import Strata.Languages.Boogie.OldExpressions
 import Strata.DDM.Util.DecimalRat
 
 
@@ -22,24 +24,39 @@ open Std (ToFormat Format format)
 
 /- Translation Monad -/
 
+abbrev OldVarSubst := BoogieIdent × LMonoTy × BoogieIdent
+
 structure TransState where
+  globalTypes : Std.TreeMap BoogieIdent LTy
+  oldVarSubsts : List OldVarSubst
   errors : Array String
 
 def TransM := StateM TransState
   deriving Monad
 
 def TransM.run (m : TransM α) : (α × Array String) :=
-  let (v, s) := StateT.run m { errors := #[] }
+  let (v, s) := StateT.run m { errors := #[], globalTypes := .empty, oldVarSubsts := [] }
   (v, s.errors)
 
 instance : ToString (Boogie.Program × Array String) where
   toString p := toString (Std.format p.fst) ++ "\n" ++
                 "Errors: " ++ (toString p.snd)
 
 def TransM.error [Inhabited α] (msg : String) : TransM α := do
-  fun s => ((), { errors := s.errors.push msg })
+  fun s => ((), { s with errors := s.errors.push msg })
   return panic msg
 
+def TransM.addGlobal (id : BoogieIdent) (ty : LTy) : TransM Unit :=
+  fun s => ((), { s with globalTypes := s.globalTypes.insert id ty })
+
+def TransM.lookupGlobal (id : BoogieIdent) : TransM (Option LTy) :=
+  fun s => (s.globalTypes.get? id, s)
+
+def TransM.setOldVarSubst (ss: List OldVarSubst) : TransM Unit :=
+  fun s => ((), { s with oldVarSubsts := ss })
+
+def TransM.get : TransM TransState := fun s => (s, s)
+
 ---------------------------------------------------------------------
 
 def checkOp (op : Operation) (name : QualifiedIdent) (argc : Nat) :
@@ -568,7 +585,6 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Boogie.Expr
   | _, q`Boogie.bvextract_15_0_64 => return bv64Extract_15_0_Op
   | _, q`Boogie.bvextract_31_0_64 => return bv64Extract_31_0_Op
 
-  | _, q`Boogie.old          => return polyOldOp
   | _, q`Boogie.str_len      => return strLengthOp
   | _, q`Boogie.str_concat   => return strConcatOp
   | _, q`Boogie.str_toregex  => return strToRegexOp
@@ -742,8 +758,14 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
      let y ← translateExpr p bindings ya
      return .mkApp Boogie.strConcatOp [x, y]
   | .fn _ q`Boogie.old, [_tp, xa] =>
+     let s ← TransM.get
      let x ← translateExpr p bindings xa
-     return .mkApp Boogie.polyOldOp [x]
+     let x' := OldExpressions.normalizeOldExpr x true
+     match s.oldVarSubsts with
+     | [] => return x'
+     | _ => do
+       let subst := Map.ofList (s.oldVarSubsts.map (λ (x, ty, x') => (x, .fvar x' ty)))
+       return OldExpressions.substsOldExpr subst x'
   | .fn _ q`Boogie.map_get, [_ktp, _vtp, ma, ia] =>
      let kty ← translateLMonoTy bindings _ktp
      let vty ← translateLMonoTy bindings _vtp
@@ -908,6 +930,24 @@ def translateInitStatement (p : Program) (bindings : TransBindings) (args : Arra
     let bbindings := bindings.boundVars ++ [newBinding]
     return ([.init lhs ty val], { bindings with boundVars := bbindings })
 
+def oldPrefix : String := "old$"
+
+def addOldPrefix (i : BoogieIdent) : BoogieIdent :=
+  { i with name := oldPrefix ++ i.name }
+
+def mkOldVarSubsts (modifies : List BoogieIdent) : TransM (List OldVarSubst) :=
+  modifies.mapM $ λ x => do
+    let ty? ← TransM.lookupGlobal x
+    match ty? with
+    | .some (.forAll [] ty) => return (x, ty, addOldPrefix x)
+    | .some (.forAll _ _) =>
+      TransM.error s!"Polymorphic type found for modified variable {x}"
+    | .none =>
+      TransM.error s!"No type found for modified variable {x}"
+
+def mkOldVarInitStmts (subst : List OldVarSubst) : List Statement :=
+  subst.map (λ (x, ty, x') => .cmd (.cmd (.init x' (.forAll [] ty) (.fvar x ty))))
+
 mutual
 partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
   TransM (List Boogie.Statement × TransBindings) := do
@@ -1096,7 +1136,12 @@ def translateProcedure (p : Program) (bindings : TransBindings) (op : Operation)
     if speca.isSome then translateSpec p pname bindings speca.get! else pure ([], [], [])
   let .option _ bodya := op.args[5]!
     | TransM.error s!"translateProcedure body expected here: {repr op.args[4]!}"
-  let (body, bindings) ← if bodya.isSome then translateBlock p bindings bodya.get! else pure ([], bindings)
+  let oldSubsts ← mkOldVarSubsts modifies
+  TransM.setOldVarSubst oldSubsts
+  let (body, bindings) ← match bodya with
+    | .some b => translateBlock p bindings b
+    | .none => pure ([], bindings)
+  TransM.setOldVarSubst []
   let origBindings := { origBindings with gen := bindings.gen }
   return (.proc { header := { name := pname,
                               typeArgs := typeArgs.toList,
@@ -1105,7 +1150,7 @@ def translateProcedure (p : Program) (bindings : TransBindings) (op : Operation)
                   spec := { modifies := modifies,
                             preconditions := requires,
                             postconditions := ensures },
-                  body := body
+                  body := mkOldVarInitStmts oldSubsts ++ body
                 },
           origBindings)
 
@@ -1208,6 +1253,7 @@ def translateGlobalVar (bindings : TransBindings) (op : Operation) :
   let (id, targs, mty) ← translateBindMk bindings op.args[0]!
   let ty := LTy.forAll targs mty
   let decl := (.var id ty (Names.initVarValue (id.name ++ "_" ++ (toString bindings.gen.var_def))))
+  TransM.addGlobal id ty
   let bindings := incrNum .var_def bindings
   return (decl, { bindings with freeVars := bindings.freeVars.push decl})
 

Strata/Languages/Boogie/Examples/AdvancedMaps.lean

@@ -63,7 +63,10 @@ var (c : (Map int MapII)) := init_c_2
 modifies: [a, b, c]
 preconditions: (P_requires_3, ((((~select : (arrow (Map int int) (arrow int int))) (a : MapII)) #0) == #0)) (P_requires_4, ((((~select : (arrow (Map int MapII) (arrow int MapII))) (c : (Map int MapII))) #0) == (a : MapII)))
 postconditions: ⏎
-body: assert [c_0_eq_a] ((((~select : (arrow (Map int MapII) (arrow int MapII))) (c : (Map int MapII))) #0) == (a : MapII))
+body: init (old$a : MapII) := (a : MapII)
+init (old$b : (Map bool int)) := (b : (Map bool int))
+init (old$c : (Map int MapII)) := (c : (Map int MapII))
+assert [c_0_eq_a] ((((~select : (arrow (Map int MapII) (arrow int MapII))) (c : (Map int MapII))) #0) == (a : MapII))
 c := ((((~update : (arrow (Map int MapII) (arrow int (arrow MapII (Map int MapII))))) (c : (Map int MapII))) #1) (a : MapII))
 assert [c_1_eq_a] ((((~select : (arrow (Map int MapII) (arrow int MapII))) (c : (Map int MapII))) #1) == (a : MapII))
 assert [a0eq0] ((((~select : (arrow (Map int int) (arrow int int))) (a : MapII)) #0) == #0)

Strata/Languages/Boogie/Examples/FreeRequireEnsure.lean

@@ -77,6 +77,7 @@ modifies: [g]
 preconditions: (g_eq_15, ((g : int) == #15) (Attribute: Boogie.Procedure.CheckAttr.Free))
 postconditions: (g_lt_10, (((~Int.Lt : (arrow int (arrow int bool))) (g : int)) #10) (Attribute: Boogie.Procedure.CheckAttr.Free))
 body: assume [g_eq_15] ($__g0 == #15)
+init (old$g : int) := $__g0
 assert [g_gt_10_internal] ((~Int.Gt $__g0) #10)
 g := ((~Int.Add $__g0) #1)
 #[<[g_lt_10]: (((~Int.Lt : (arrow int (arrow int bool))) (g : int)) #10)>,

Strata/Languages/Boogie/Examples/SimpleProc.lean

@@ -15,12 +15,15 @@ program Boogie;
 var g : bool;
 procedure Test(x : bool) returns (y : bool)
 spec {
+  modifies g;
   ensures (y == x);
   ensures (x == y);
   ensures (g == old(g));
 }
 {
+  g := g && true;
   y := x || x;
+  assert g == old(g);
 };
 #end
 
@@ -34,10 +37,13 @@ spec {
 /--
 info: var (g : bool) := init_g_0
 (procedure Test :  ((x : bool)) → ((y : bool)))
-modifies: []
+modifies: [g]
 preconditions: ⏎
-postconditions: (Test_ensures_0, ((y : bool) == (x : bool))) (Test_ensures_1, ((x : bool) == (y : bool))) (Test_ensures_2, ((g : bool) == ((~old : (arrow a a)) (g : bool))))
-body: y := (((~Bool.Or : (arrow bool (arrow bool bool))) (x : bool)) (x : bool))
+postconditions: (Test_ensures_1, ((y : bool) == (x : bool))) (Test_ensures_2, ((x : bool) == (y : bool))) (Test_ensures_3, ((g : bool) == (~old (g : bool))))
+body: init (old$g : bool) := (g : bool)
+g := (((~Bool.And : (arrow bool (arrow bool bool))) (g : bool)) #true)
+y := (((~Bool.Or : (arrow bool (arrow bool bool))) (x : bool)) (x : bool))
+assert [assert_0] ((g : bool) == (old$g : bool))
 
 Errors: #[]
 -/
@@ -49,39 +55,51 @@ info: [Strata.Boogie] Type checking succeeded.
 
 
 VCs:
-Label: Test_ensures_0
+Label: assert_0
 Assumptions:
 
 
 Proof Obligation:
-(((~Bool.Or $__x0) $__x0) == $__x0)
+(((~Bool.And $__g0) #true) == $__g0)
 
 Label: Test_ensures_1
 Assumptions:
 
 
 Proof Obligation:
-($__x0 == ((~Bool.Or $__x0) $__x0))
+(((~Bool.Or $__x1) $__x1) == $__x1)
 
 Label: Test_ensures_2
 Assumptions:
 
 
 Proof Obligation:
-#true
+($__x1 == ((~Bool.Or $__x1) $__x1))
 
-Wrote problem to vcs/Test_ensures_0.smt2.
+Label: Test_ensures_3
+Assumptions:
+
+
+Proof Obligation:
+(((~Bool.And $__g0) #true) == $__g0)
+
+Wrote problem to vcs/assert_0.smt2.
 Wrote problem to vcs/Test_ensures_1.smt2.
+Wrote problem to vcs/Test_ensures_2.smt2.
+Wrote problem to vcs/Test_ensures_3.smt2.
 ---
 info:
-Obligation: Test_ensures_0
+Obligation: assert_0
 Result: verified
 
 Obligation: Test_ensures_1
 Result: verified
 
 Obligation: Test_ensures_2
 Result: verified
+
+Obligation: Test_ensures_3
+Result: verified
 -/
 #guard_msgs in
 #eval verify "cvc5" simpleProcPgm

Strata/Languages/Boogie/Identifiers.lean

@@ -40,7 +40,7 @@ inductive Visibility where
   | glob
   | locl
   | temp
-deriving DecidableEq, Repr
+deriving DecidableEq, Repr, Ord, Hashable
 
 instance : ToFormat Visibility where
   format