18 files changed, 660 insertions, 419 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 879163db..a17a7bfd 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -1,6 +1,7 @@
 module Analyzer

 

 open Ast

+open Getters

 open AstUtils

 open CodeGen

 open DafnyModelUtils

@@ -18,11 +19,11 @@ open Utils
 open Microsoft.Boogie

 

 let Rename suffix vars =

-  vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))

+  vars |> List.map (function Var(nm,tp,old) -> nm, Var(nm + suffix, tp, old))

 

 let ReplaceName substMap nm =

   match Map.tryFind nm substMap with

-    | Some(Var(name, tp)) -> name

+    | Some(Var(name,_,_)) -> name

     | None -> nm

 

 let rec Substitute substMap = function

@@ -37,29 +38,30 @@ let rec Substitute substMap = function
   | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)

   | expr -> expr

 

-let GenMethodAnalysisCode comp m assertion =

+let GenMethodAnalysisCode comp m assertion genOld =

   let methodName = GetMethodName m

   let signature = GetMethodSig m 

   let ppre,ppost = GetMethodPrePost m 

   let pre = Desugar ppre

-  let post = Desugar ppost

+  let post = Desugar ppost |> RewriteOldExpr  

   let ghostPre = GetMethodGhostPrecondition m |> Desugar 

   //let sigStr = PrintSig signature

-  let sigVars = 

+  let sigVarsDecl = 

     match signature with

-    | Sig(ins,outs) ->

-        List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf "    var %s;" (PrintVarDecl vd)) + newline) ""

+    | Sig(ins,outs) -> ins @ outs |> List.fold (fun acc vd -> acc + (sprintf "    var %s;" (PrintVarDecl vd)) + newline) ""

+

   "  method " + methodName + "()" + newline +

   "    modifies this;" + newline +

   "  {" + newline + 

   // print signature as local variables

-  sigVars +

+  sigVarsDecl +

   "    // assume precondition" + newline +

   "    assume " + (PrintExpr 0 pre) + ";" + newline +

   "    // assume ghost precondition" + newline +

   "    assume " + (PrintExpr 0 ghostPre) + ";" + newline +

   "    // assume invariant and postcondition" + newline + 

   "    assume Valid();" + newline +

+  (if genOld then "    assume Valid_old();" + newline else "") + 

   "    assume " + (PrintExpr 0 post) + ";" + newline +

   "    // assume user defined invariant again because assuming Valid() doesn't always work" + newline +

   (GetInvariantsAsList comp |> PrintSep newline (fun e -> "    assume " + (PrintExpr 0 e) + ";")) + newline +

@@ -68,16 +70,16 @@ let GenMethodAnalysisCode comp m assertion =
   "    assert " + (PrintExpr 0 assertion) + ";" + newline + 

   "  }" + newline

              

-let rec MethodAnalysisPrinter onlyForThese assertion comp = 

+let rec MethodAnalysisPrinter onlyForThese assertion genOld comp = 

   let cname = GetComponentName comp

   match onlyForThese with

   | (c,m) :: rest when GetComponentName c = cname -> 

     match m with 

     | Method(_) -> 

-        (GenMethodAnalysisCode c m assertion) + newline +

-        (MethodAnalysisPrinter rest assertion comp)

+        (GenMethodAnalysisCode c m assertion genOld) + newline +

+        (MethodAnalysisPrinter rest assertion genOld comp)

     | _ -> ""

-  | _ :: rest -> MethodAnalysisPrinter rest assertion comp

+  | _ :: rest -> MethodAnalysisPrinter rest assertion genOld comp 

   | [] -> ""     

 

 //  =========================================================================

@@ -101,9 +103,9 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
       | _ -> 

           let rec __fff lst = 

             match lst with

-            | ((o,Var(fldName,_)),_) :: rest -> 

+            | ((o,var),_) :: rest -> 

                 match __GetObjRefExpr o.name newVisited with

-                | Some(expr) -> Some(Dot(expr, fldName))

+                | Some(expr) -> Some(Dot(expr, GetExtVarName var))

                 | None -> __fff rest

             | [] -> None

           let backPointers = heapInst.assignments |> List.choose (function 

@@ -127,7 +129,7 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
 /// Returns an expression that combines the post-condition of a given method with

 /// invariants for all objects present on the heap

 //  =============================================================================

-let GetHeapExpr prog mthd heapInst = 

+let GetHeapExpr prog mthd heapInst includePreState = 

   // get expressions to evaluate:

   //   - add post (and pre?) conditions                                     

   //   - go through all objects on the heap and assert their invariants  

@@ -143,7 +145,14 @@ let GetHeapExpr prog mthd heapInst =
                           let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption

                           let objInvs = GetInvariantsAsList objComp

                           let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

-                          objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

+                          let objInvFinal = objInvsUpdated |> List.fold BinaryAnd TrueLiteral

+                          let objAllInvs = 

+                            if includePreState then

+                              let objInvPre = MakeOld objInvFinal

+                              BinaryAnd objInvFinal objInvPre

+                            else  

+                              objInvFinal

+                          BinaryAnd prepostExpr objAllInvs

                       ) prepostExpr

 

 let IsUnmodConcrOnly prog (comp,meth) expr = 

@@ -158,7 +167,7 @@ let IsUnmodConcrOnly prog (comp,meth) expr =
     | Star        

     | VarDeclExpr(_)

     | ObjLiteral(_)                         -> true

-    | VarLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

+    | VarLiteral(id)                        -> args |> List.exists (fun var -> GetExtVarName var = id)

     | IdLiteral("null") | IdLiteral("this") -> true

     | IdLiteral(id)                         -> 

         not (isConstr || IsAbstractField comp id)

@@ -174,6 +183,7 @@ let IsUnmodConcrOnly prog (comp,meth) expr =
     | SeqLength(e)

     | LCIntervalExpr(e)

     | MethodOutSelect(e,_)   

+    | OldExpr(e)

     | UnaryExpr(_,e)                        -> __IsUnmodOnlyLst [e]

     | SelectExpr(e1, e2)

     | BinaryExpr(_,_,e1,e2)                 -> __IsUnmodOnlyLst [e1; e2]

@@ -215,13 +225,20 @@ let rec GetUnifications prog indent (comp,meth) heapInst unifs expr =
 

 //  =======================================================

 /// Returns a map (Expr |--> Const) containing unifications

-/// found for the given method and heap/env/ctx

+/// found for the given method wrt to heapInst.

+/// 

+/// The list of potential unifications include: 

+///   (1) arg-value pairs for all method arguments,

+///   (2) field-value pairs for all unmodifiable fields,

+///   (3) expr-value pairs where expr are unmodifiable 

+///       expressions found in the spec.

 //  =======================================================

 let GetUnificationsForMethod indent prog comp m heapInst =

   let idt = Indent indent

   let rec GetArgValueUnifications args = 

     match args with

-    | Var(name,_) :: rest -> 

+    | var :: rest -> 

+        let name = GetExtVarName var

         match Map.tryFind name heapInst.methodArgs with

         | Some(c) ->

             GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c

@@ -230,8 +247,9 @@ let GetUnificationsForMethod indent prog comp m heapInst =
   let rec GetFldValueUnifications unifs = 

     heapInst.assignments |> List.fold (fun acc asgn ->  

                                          match asgn with 

-                                         | FieldAssignment((obj,Var(vname,_)), fldVal) -> 

+                                         | FieldAssignment((obj,var), fldVal) -> 

                                              try 

+                                               let vname = GetExtVarName var

                                                let comp = obj.objType |> FindComponentForType prog |> Utils.ExtractOption

                                                if IsConcreteField comp vname then

                                                  let path = GetObjRefExpr obj.name heapInst |> Utils.ExtractOption

@@ -257,7 +275,7 @@ let GetUnificationsForMethod indent prog comp m heapInst =
   GetUnifications prog indent (comp,m) heapInst unifs (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x))

 

 //  =======================================================

-/// Applies given unifications onto the given heap/env/ctx

+/// Applies given unifications onto a given heapInstance

 /// 

 /// If "conservative" is true, applies only those that 

 /// can be verified to hold, otherwise applies all of them

@@ -275,12 +293,13 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
                   let objRefExpr = GetObjRefExpr o.name heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o.name)

                   let fldName = GetVarName f                             

                   Dot(objRefExpr, fldName)

-      let assertionExpr = match f with

-                          | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e

-                          | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs

-                          | _                                            -> BinaryEq lhs e 

+      let assertionExpr = match GetVarType f with

+                          | Some(SeqType(_)) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e

+                          | Some(SetType(_)) when not (idx = -1) -> BinaryIn e lhs

+                          | _                                    -> BinaryEq lhs e 

       // check if the assertion follows and if so update the env

-      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,mthd] assertionExpr) true

+      let genOld = false

+      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,mthd] assertionExpr genOld) true genOld

       Logger.Debug (idt + "    - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")

       let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))

       if ok then

@@ -332,7 +351,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
                                                         | _ -> acc @ [asgn]

                                                      ) [] 

       let newRetVals = heapInst.methodRetVals |> Map.fold (fun acc key value ->

-                                                             let e2 = __Apply (NoObj,Var(key, None)) c e value

+                                                             let e2 = __Apply (NoObj,Var(key, None, false)) c e value

                                                              acc |> Map.add key e2

                                                           ) Map.empty

       {heapInst with assignments = newHeap; methodRetVals = newRetVals}

@@ -344,7 +363,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
 let VerifySolution prog solutions genRepr =

   // print the solution to file and try to verify it with Dafny

   //let prog = Program(solutions |> Utils.MapKeys |> Map.ofList |> Utils.MapKeys)

-  let code = PrintImplCode prog solutions genRepr

+  let code = PrintImplCode prog solutions genRepr false

   CheckDafnyProgram code dafnyVerifySuffix

 

 let rec DiscoverAliasing exprList heapInst = 

@@ -362,7 +381,7 @@ let rec DiscoverAliasing exprList heapInst =
 //

 let DontResolveUnmodifiableStuff prog comp meth expr =

   let methodArgs = GetMethodInArgs meth

-  let __IsMethodArg argName = methodArgs |> List.exists (fun (Var(vname,_)) -> vname = argName)

+  let __IsMethodArg argName = methodArgs |> List.exists (fun var -> GetExtVarName var = argName)

   let isConstr = IsConstructor meth

   match expr with

   | VarLiteral(id) when __IsMethodArg id -> false 

@@ -373,7 +392,7 @@ let DontResolveUnmodifiableStuff prog comp meth expr =
   | _ -> true

 

 /// Descends down a given expression and returns bunch of sub-expressions that all evaluate to true

-let FindClauses resolverFunc heapInst expr = 

+let FindClauses trueOnly resolverFunc heapInst expr = 

   let MyFun expr acc =

     try

       match expr with

@@ -387,7 +406,7 @@ let FindClauses resolverFunc heapInst expr =
               let exprAllResolved = EvalFull heapInst expr

               match exprAllResolved with

               | BoolLiteral(true) -> acc @ [exprEval]

-              | BoolLiteral(false) -> acc @ [UnaryNot exprEval]

+              | BoolLiteral(false) -> if trueOnly then acc else acc @ [UnaryNot exprEval]

               | _ -> acc

     with

     | _ -> acc

@@ -396,24 +415,25 @@ let FindClauses resolverFunc heapInst expr =
 

 /// Descends down a given expression and returns all sub-expressions that evaluate to TrueLiteral

 let FindTrueClauses resolverFunc heapInst expr = 

-  let MyFun expr acc =

-    try

-      match expr with

-      // skip binary logical operators because we want to find smallest sub-expressions

-      | BinaryExpr(_,op,_,_) when IsLogicalOp op -> acc 

-      | _ ->

-          let exprEval = EvalAndCheckTrue heapInst resolverFunc expr

-          match exprEval with

-          | _ when exprEval = TrueLiteral -> acc

-          | _ ->

-              let exprAllResolved = EvalFull heapInst expr

-              match exprAllResolved with

-              | BoolLiteral(true) -> acc @ [exprEval]

-              | _ -> acc

-    with

-    | _ -> acc

-  (* --- function body starts here --- *)

-  DescendExpr2 MyFun expr []

+  FindClauses true resolverFunc heapInst expr

+//  let MyFun expr acc =

+//    try

+//      match expr with

+//      // skip binary logical operators because we want to find smallest sub-expressions

+//      | BinaryExpr(_,op,_,_) when IsLogicalOp op -> acc 

+//      | _ ->

+//          let exprEval = EvalAndCheckTrue heapInst resolverFunc expr

+//          match exprEval with

+//          | _ when exprEval = TrueLiteral -> acc

+//          | _ ->

+//              let exprAllResolved = EvalFull heapInst expr

+//              match exprAllResolved with

+//              | BoolLiteral(true) -> acc @ [exprEval]

+//              | _ -> acc

+//    with

+//    | _ -> acc

+//  (* --- function body starts here --- *)

+//  DescendExpr2 MyFun expr []

 

 /// Returns a list of boolean expressions obtained by combining (in some way) 

 /// the two given list of conditions conditions

@@ -454,6 +474,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
           None

     | None -> None

 

+  (* --- function body starts here --- *)

   Logger.InfoLine (idt + "[*] Analyzing constructor")

   Logger.InfoLine (idt + "------------------------------------------")

   Logger.InfoLine (Printer.PrintMethodSignFull (indent + 4) comp m)

@@ -464,7 +485,8 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
       let methodName = GetMethodName m

       let pre,post = GetMethodPrePost m

       // generate Dafny code for analysis first

-      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) true

+      let genOld = true

+      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral genOld) true genOld

       Logger.Info     (idt + "    - searching for an instance      ...")

       let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  

       if models.Count = 0 then

@@ -478,7 +500,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
         Logger.InfoLine " OK "

         let model = models.[0]

         let hModel = ReadFieldValuesFromModel model prog comp m

-        let heapInst = ResolveModel hModel m

+        let heapInst = ResolveModel hModel (comp,m)

         let unifs = GetUnificationsForMethod indent prog comp m heapInst |> Map.toList

         let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

@@ -515,25 +537,27 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
       false

     with

     | _ -> 

-        DescendExpr2 (fun expr acc ->

-                        if not acc then

-                          false

-                        else

-                          match expr with

-                          | Dot(discr, fldName) -> 

-                              let obj = EvalFull heapInst discr

-                              match obj with 

-                              | ObjLiteral(id) when id = "this" -> 

-                                  try 

-                                    IsConcreteField (InferType prog comp (MethodArgChecker prog m) discr |> Utils.ExtractOption) fldName

-                                  with

-                                    | _ -> false

-                              | ObjLiteral(id) -> false

-                              | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"

-                          | MethodCall(receiver, cn, mn, elst) when receiver = ThisLiteral && cn = compName && mn = methName -> 

-                              elst |> List.exists (function VarLiteral(_) -> false | _ -> true)

-                          | _ -> true                          

-                      ) expr true

+        let myVisitor = 

+          fun expr acc ->

+            if not acc then

+              false

+            else

+              match expr with

+              | Dot(discr, fldName) -> 

+                  let obj = EvalFull heapInst discr

+                  match obj with 

+                  | ObjLiteral(id) when id = "this" -> 

+                      try 

+                        let fname = RenameFromOld fldName

+                        IsConcreteField (InferType prog comp (MethodArgChecker prog m) discr |> Utils.ExtractOption) fname

+                      with

+                        | _ -> false

+                  | ObjLiteral(id) -> false

+                  | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"

+              | MethodCall(receiver, cn, mn, elst) when receiver = ThisLiteral && cn = compName && mn = methName -> 

+                  elst |> List.exists (function VarLiteral(_) -> false | _ -> true)

+              | _ -> true                          

+        DescendExpr2 myVisitor expr true

 

   /// Finds all modifiable fields in a given hInst, and checks if an "ok" 

   /// expression exists for each one of them.

@@ -591,7 +615,7 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
                               match e with 

                               | VarLiteral(id) when not (IsInVarList ctx id) -> 

                                   if IsInVarList outs id then

-                                    let mcall = MethodCall(ThisLiteral, compName, methName, ins |> List.map (function Var(name,_) -> VarLiteral("$" + name)))

+                                    let mcall = MethodCall(ThisLiteral, compName, methName, ins |> List.map (function var -> VarLiteral("$" + (GetExtVarName var))))

                                     let outSel = MethodOutSelect(mcall, id)

                                     Some(outSel)

                                   else

@@ -607,9 +631,9 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
       | asg :: rest -> 

           let newAsg = 

             match asg with

-            | FieldAssignment((obj,Var(fldName,_)) as discr,valExpr) -> 

+            | FieldAssignment((obj,var) as discr,valExpr) -> 

                 let objPath = GetObjRefExpr obj.name hInst |> Utils.ExtractOption

-                let lhs = Dot(objPath, fldName)

+                let lhs = Dot(objPath, GetExtVarName var)

                 match __FindRhs lhs with

                 | Some(rhs) -> FieldAssignment(discr,rhs)

                 | None -> asg

@@ -662,11 +686,20 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
 

   (* --- function body starts here --- *) 

   let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s    --> %s" idt (PrintExpr 0 e))

+

+  //TODO

   let expandOnlyModVarsFunc = fun e ->

+//    true

     let __CheckExpr l = 

       //TODO: FIX THIS!!!!!

-      let str = PrintExpr 0 l

-      str.Contains("ret")

+      match l with 

+      | VarLiteral(vname) -> GetMethodOutArgs m |> List.exists (fun var -> GetVarName var = vname)

+      | IdLiteral(_) -> true

+      | Dot(_,_) -> true

+      | _ -> false     

+//      let str = PrintExpr 0 l

+//      str.Contains("ret")

+

     match e with

     | BinaryExpr(_,"=",l,_) -> 

         //TODO: it should really check both lhs and rhs

@@ -676,10 +709,12 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst = ApplyUnifications indent prog comp m unifs heapInst false

   let methodArgs = GetMethodInArgs m

-  let heapExpr = GetHeapExpr prog m heapInst

+  let heapExpr = GetHeapExpr prog m heapInst true

+

+  //Logger.TraceLine (PrintExpr 0 heapExpr)

 

   // find set of premises (don't resolve anything)

-  let premises = heapExpr |> FindClauses (fun e -> false) heapInst 

+  let premises = heapExpr |> FindClauses false (fun e -> false) heapInst 

 

   Logger.TraceLine (sprintf "%s Premises:" idt)

   premises |> List.iter loggerFunc  

@@ -741,7 +776,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises =
   if IsSolution1stLevelOnly heapInst then

     // try to find a non-recursive solution

     Logger.InfoLine (idt + "Strengthening the pre-condition")

-    let expr = GetHeapExpr prog m heapInst

+    let expr = GetHeapExpr prog m heapInst false

     let specConds1 = expr |> FindTrueClauses (DontResolveUnmodifiableStuff prog comp m) heapInst

     let specConds2 = premises |> Set.toList

     

@@ -757,7 +792,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises =
                        |> List.map SimplifyExpr 

                        |> List.filter (fun e -> is1stLevelFunc e && unmodConcrFunc e && not (isConstFunc e))

     

-    let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst) 

+    let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function var -> VarLiteral(GetExtVarName var))) heapInst) 

     let argConds = heapInst.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) []

     let allConds = GetAllPossibleConditions specConds argConds [aliasingCond.Force()]

     allConds |> List.iter loggerFunc

@@ -872,7 +907,7 @@ let Analyze prog filename =
     // add all other methods (those for which we don't have synthesized solution) as well

     let allMethods = FilterMembers prog FilterConstructorMembers

     let extSolutions = solutions //__AddMethodsFromProg allMethods solutions

-    let synthCode = PrintImplCode prog extSolutions Options.CONFIG.genRepr

+    let synthCode = PrintImplCode prog extSolutions Options.CONFIG.genRepr false

     fprintfn file "%s" synthCode

 

   (* --- function body starts here --- *)

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index fa18b107..d355023a 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -19,7 +19,7 @@ type Type =
   | InstantiatedType of string * Type list (* type parameters *)

 

 type VarDecl =

-  | Var of string * Type option

+  | Var of string * Type option * (* isOld *) bool 

 

 (* 

    the difference between IdLiteral and VarLiteral is that the VarLiteral is more specific, 

@@ -38,6 +38,7 @@ type Expr =
   | Star

   | Dot of Expr * string

   | UnaryExpr of string * Expr

+  | OldExpr of Expr

   | LCIntervalExpr of Expr

   | BinaryExpr of int * string * Expr * Expr

   | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 03fa1899..a3e1e807 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -7,6 +7,7 @@
 module AstUtils

 

 open Ast

+open Getters

 open Logger

 open Utils

 

@@ -58,6 +59,7 @@ let rec MyRewrite rewriterFunc rewriteRecurseFunc expr =
   | Dot(e, id)                       -> Dot(rewriteRecurseFunc e, id)

   | ForallExpr(vars,e)               -> ForallExpr(vars, rewriteRecurseFunc e)   

   | UnaryExpr(op,e)                  -> UnaryExpr(op, rewriteRecurseFunc e)

+  | OldExpr(e)                       -> OldExpr(rewriteRecurseFunc e)

   | LCIntervalExpr(e)                -> LCIntervalExpr(rewriteRecurseFunc e)

   | SeqLength(e)                     -> SeqLength(rewriteRecurseFunc e)

   | SelectExpr(e1, e2)               -> SelectExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2)

@@ -78,12 +80,14 @@ let rec Rewrite rewriterFunc expr =
     | None -> Rewrite rewriterFunc e 

   MyRewrite rewriterFunc __RewriteOrRecurse expr

 

+// TODO: double check this!

 let rec RewriteBU rewriterFunc expr = 

   let rewriteRecurseFunc e =

-    let e' = Rewrite rewriterFunc e

-    match rewriterFunc e' with

-    | Some(ee) -> ee

-    | None -> e'

+    RewriteBU rewriterFunc e

+//    let e' = Rewrite rewriterFunc e

+//    match rewriterFunc e' with

+//    | Some(ee) -> ee

+//    | None -> e'

   let rewriteFunc e = 

     match rewriterFunc e with

     | Some(ee) -> ee

@@ -101,6 +105,7 @@ let rec RewriteBU rewriterFunc expr =
     | Dot(e, id)                       -> Dot(rewriteRecurseFunc e, id) 

     | ForallExpr(vars,e)               -> ForallExpr(vars, rewriteRecurseFunc e)   

     | UnaryExpr(op,e)                  -> UnaryExpr(op, rewriteRecurseFunc e)

+    | OldExpr(e)                       -> OldExpr(rewriteRecurseFunc e)

     | LCIntervalExpr(e)                -> LCIntervalExpr(rewriteRecurseFunc e)

     | SeqLength(e)                     -> SeqLength(rewriteRecurseFunc e)

     | SelectExpr(e1, e2)               -> SelectExpr(rewriteRecurseFunc e1, rewriteRecurseFunc e2)

@@ -134,6 +139,7 @@ let rec RewriteWithCtx rewriterFunc ctx expr =
   | Dot(e, id)                       -> Dot(__RewriteOrRecurse ctx e, id)

   | ForallExpr(vars,e)               -> ForallExpr(vars, __RewriteOrRecurse (ctx @ vars) e)   

   | UnaryExpr(op,e)                  -> UnaryExpr(op, __RewriteOrRecurse ctx e)

+  | OldExpr(e)                       -> OldExpr(__RewriteOrRecurse ctx e)

   | LCIntervalExpr(e)                -> LCIntervalExpr(__RewriteOrRecurse ctx e)

   | SeqLength(e)                     -> SeqLength(__RewriteOrRecurse ctx e)

   | SelectExpr(e1, e2)               -> SelectExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2)

@@ -146,13 +152,14 @@ let rec RewriteWithCtx rewriterFunc ctx expr =
   | MethodOutSelect(mth,name)        -> MethodOutSelect(__RewriteOrRecurse ctx mth, name)

   | AssertExpr(e)                    -> AssertExpr(__RewriteOrRecurse ctx e)

   | AssumeExpr(e)                    -> AssumeExpr(__RewriteOrRecurse ctx e)

+

 //  ====================================================

 /// Substitutes all occurences of all IdLiterals having 

 /// the same name as one of the variables in "vars" with

 /// VarLiterals, in "expr".

 //  ====================================================

 let RewriteVars vars expr = 

-  let __IdIsArg id = vars |> List.exists (function Var(name,_) -> name = id)

+  let __IdIsArg id = vars |> List.exists (fun var -> GetVarName var = id)

   Rewrite (fun e ->

              match e with 

              | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id))

@@ -212,6 +219,7 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

+  | OldExpr(e)

   | UnaryExpr(_,e) 

   | MethodOutSelect(e,_)          

   | SeqLength(e)                     -> __Compose (e :: [])

@@ -240,6 +248,7 @@ let rec DescendExpr2 visitorFunc expr acc =
   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

+  | OldExpr(e)

   | UnaryExpr(_,e)  

   | MethodOutSelect(e,_)         

   | SeqLength(e)                     -> __Pipe (e :: [])

@@ -269,6 +278,7 @@ let rec DescendExpr2BU visitorFunc expr acc =
   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

+  | OldExpr(e)

   | UnaryExpr(_,e)  

   | MethodOutSelect(e,_)         

   | SeqLength(e)                     -> __Pipe (e :: [])

@@ -450,114 +460,7 @@ let IsConstExpr e =
   with

     | _ -> false

 

-// --- search functions ---

-                     

-//  =========================================================

-/// Out of all "members" returns only those that are "Field"s                                               

-//  =========================================================

-let FilterFieldMembers members =

-  members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)

-

-//  =============================================================

-/// Out of all "members" returns only those that are constructors

-//  =============================================================

-let FilterConstructorMembers members = 

-  members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)

-

-//  =============================================================

-/// Out of all "members" returns only those that are 

-/// constructors and have at least one input parameter

-//  =============================================================

-let FilterConstructorMembersWithParams members = 

-  members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None)

-

-//  ==========================================================

-/// Out of all "members" returns only those that are "Method"s

-//  ==========================================================

-let FilterMethodMembers members = 

-  members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None)

-

-//  =======================================================================

-/// Returns all members of the program "prog" that pass the filter "filter"

-//  =======================================================================

-let FilterMembers prog filter = 

-  match prog with

-  | Program(components) ->

-      components |> List.fold (fun acc comp -> 

-        match comp with

-        | Component(Interface(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            

-        | _ -> acc) []

-

-let GetAbstractFields comp = 

-  match comp with 

-  | Component(Interface(_,_,members), _, _) -> FilterFieldMembers members

-  | _ -> failwithf "internal error: invalid component: %O" comp

-    

-let GetConcreteFields comp = 

-  match comp with 

-  | Component(_, DataModel(_,_,cVars,_,_), _) -> cVars

-  | _ -> failwithf "internal error: invalid component: %O" comp

-     

-//  =================================

-/// Returns all fields of a component

-//  =================================

-let GetAllFields comp = 

-  List.concat [GetAbstractFields comp; GetConcreteFields comp]

-    

-//  ===========================================================

-/// Returns a map (Type |--> Set<Var>) where all 

-/// the given fields are grouped by their type

-///

-/// ensures: forall v :: v in ret.values.elems ==> v in fields

-/// ensures: forall k :: k in ret.keys ==> 

-///            forall v1, v2 :: v1, v2 in ret[k].elems ==> 

-///              v1.type = v2.type

-//  ===========================================================

-let rec GroupFieldsByType fields = 

-  match fields with

-  | Var(name, ty) :: rest -> 

-      let map = GroupFieldsByType rest

-      let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty

-      map |> Map.add ty (fldSet |> Set.add (Var(name, ty)))

-  | [] -> Map.empty

- 

-let IsConcreteField comp fldName = GetConcreteFields comp |> List.exists (function Var(name,_) -> name = fldName)

-let IsAbstractField comp fldName = GetAbstractFields comp |> List.exists (function Var(name,_) -> name = fldName)

-                    

-//  =================================

-/// Returns class name of a component

-//  =================================

-let GetClassName comp =

-  match comp with

-  | Component(Interface(name,_,_),_,_) -> name

-  | _ -> failwith ("unrecognized component: " + comp.ToString())

-

-let GetClassType comp = 

-  match comp with

-  | Component(Interface(name,typeParams,_),_,_) -> NamedType(name, typeParams)

-  | _ -> failwith ("unrecognized component: " + comp.ToString())

-

-//  ========================

-/// Returns name of a method

-//  ========================

-let GetMethodName mthd = 

-  match mthd with

-  | Method(name,_,_,_,_) -> name

-  | _ -> failwith ("not a method: " + mthd.ToString())

-

-//  ===========================================================

-/// Returns full name of a method (= <class_name>.<method_name>

-//  ===========================================================

-let GetMethodFullName comp mthd = 

-  (GetClassName comp) + "." + (GetMethodName mthd)

-

-//  =============================

-/// Returns signature of a method

-//  =============================

-let GetMethodSig mthd = 

-  match mthd with

-  | Method(_,sgn,_,_,_) -> sgn

-  | _ -> failwith ("not a method: " + mthd.ToString())

+///////

 

 let GetMethodPrePost mthd = 

   let __FilterOutAssumes e = e |> SplitIntoConjunts |> List.filter (function AssumeExpr(_) -> false | _ -> true) |> List.fold BinaryAnd TrueLiteral

@@ -571,41 +474,6 @@ let GetMethodGhostPrecondition mthd =
       pre |> SplitIntoConjunts |> List.choose (function AssumeExpr(e) -> Some(e) | _ -> None) |> List.fold BinaryAnd TrueLiteral

   | _ -> failwith ("not a method: " + mthd.ToString())

 

-//  =========================================================

-/// Returns all arguments of a method (both input and output)

-//  =========================================================

-let GetSigVars sign = 

-  match sign with

-  | Sig(ins, outs) -> List.concat [ins; outs]

-

-let GetMethodInArgs mthd = 

-  match mthd with

-  | Method(_,Sig(ins, _),_,_,_) -> ins

-  | _ -> failwith ("not a method: " + mthd.ToString())

-

-let GetMethodOutArgs mthd = 

-  match mthd with

-  | Method(_,Sig(_, outs),_,_,_) -> outs

-  | _ -> failwith ("not a method: " + mthd.ToString())

-

-let GetMethodArgs mthd = 

-  let ins = GetMethodInArgs mthd

-  let outs = GetMethodOutArgs mthd

-  List.concat [ins; outs]

-

-let IsConstructor mthd = 

-  match mthd with

-  | Method(_,_,_,_,isConstr) -> isConstr

-  | _ -> failwithf "expected a method but got %O" mthd

-

-let rec GetTypeShortName ty =

-  match ty with

-  | IntType -> "int"

-  | BoolType -> "bool"

-  | SetType(_) -> "set"

-  | SeqType(_) -> "seq"

-  | NamedType(n,_) | InstantiatedType(n,_) -> n

-

 //  ==============================================================

 /// Returns all invariants of a component as a list of expressions

 //  ==============================================================

@@ -616,105 +484,31 @@ let GetInvariantsAsList comp =
       List.append (SplitIntoConjunts inv) clsInvs

   | _ -> failwithf "unexpected kind of component: %O" comp

 

-//  ==================================

-/// Returns variable name

-//  ==================================

-let GetVarName var =

+/// Replaces all Old nodes with IdLiteral with name = "old_" + <name>

+let RewriteOldExpr expr = 

+  expr |> RewriteBU (fun e -> match e with

+                              | OldExpr(IdLiteral(name)) -> Some(IdLiteral(RenameToOld name))

+                              | _ -> None)

+

+let MakeOldVar var = 

   match var with

-  | Var(name,_) -> name

-

-//  ===============================================

-/// Returns whether there exists a variable 

-/// in a given VarDecl list with a given name (id)

-//  ===============================================

-let IsInVarList varLst id = 

-  varLst |> List.exists (function Var(name,_) -> name = id)

-

-//  ==================================

-/// Returns component name

-//  ==================================

-let GetComponentName comp = 

-  match comp with

-  | Component(Interface(name,_,_),_,_) -> name

-  | _ -> failwithf "invalid component %O" comp

+  | Var(name, ty, _) -> Var(name, ty, true)

 

-//  ==================================

-/// Returns all members of a component

-//  ==================================

-let GetMembers comp =

-  match comp with

-  | Component(Interface(_,_,members),_,_) -> members

-  | _ -> failwith ("unrecognized component: " + comp.ToString())

+let MakeOldVars varLst =

+  varLst |> List.map MakeOldVar

 

-//  ====================================================

-/// Finds a component of a program that has a given name

-//  ====================================================

-let FindComponent (prog: Program) clsName = 

-  match prog with

-  | Program(comps) -> comps |> List.filter (function Component(Interface(name,_,_),_,_) when name = clsName -> true | _ -> false)

-                            |> Utils.ListToOption

-

-let FindComponentForType prog ty = 

-  FindComponent prog (GetTypeShortName ty)

-

-let FindComponentForTypeOpt prog tyOpt = 

-  match tyOpt with

-  | Some(ty) -> FindComponentForType prog ty

-  | None -> None

-

-let CheckSameCompType comp ty = 

-  GetComponentName comp = GetTypeShortName ty

-

-//  ===================================================

-/// Finds a method of a component that has a given name

-//  ===================================================

-let FindMethod comp methodName =

-  let x = GetMembers comp

-  let y = x |> FilterMethodMembers

-  let z = y |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

-  GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

-                                         |> Utils.ListToOption

-

-//  ==============================================

-/// Finds a field of a class that has a given name

-//  ==============================================

-//let FindCompVar prog clsName fldName =

-//  let copt = FindComponent prog clsName

-//  match copt with

-//  | Some(comp) -> 

-//      GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

-//                        |> Utils.ListToOption

-//  | None -> None

-

-let FindVar comp fldName =

-  GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

-                    |> Utils.ListToOption

+/// renames ALL variables to "old_"+<varname>

+let MakeOld expr = 

+  expr |> RewriteBU (fun e -> match e with 

+                              | IdLiteral(name) when not (name="this") -> Some(IdLiteral(RenameToOld name)) 

+                              | Dot(e, name) -> Some(Dot(e, RenameToOld name))

+                              | _ -> None)

 

-//  ======================================

-/// Returns the frame of a given component

-//  ======================================

-let GetFrame comp = 

-  match comp with 

-  | Component(_, DataModel(_,_,_,frame,_), _) -> frame

-  | _ -> failwithf "not a valid component %O" comp

-

-let GetFrameFields comp =

-  let frame = GetFrame comp

-  frame |> List.choose (function IdLiteral(name) -> Some(name) | _ -> None) // TODO: is it really enough to handle only IdLiteral's

-        |> List.choose (fun varName -> 

-                          let v = FindVar comp varName

-                          Utils.ExtractOptionMsg ("field not found: " + varName) v |> ignore

-                          v

-                       )

-

-//  ==============================================

-/// Checks whether two given methods are the same.

-///

-/// Methods are the same if their names are the 

-/// same and their components have the same name.

-//  ==============================================

-let CheckSameMethods (c1,m1) (c2,m2) = 

-  GetComponentName c1 = GetComponentName c2 && GetMethodName m1 = GetMethodName m2

+let BringToPost expr =

+  expr |> RewriteBU (fun e -> match e with 

+                              | IdLiteral(name) -> Some(IdLiteral(RenameFromOld name))

+                              | Dot(e, name) -> Some(Dot(e, RenameFromOld name))

+                              | _ -> None)

 

 ////////////////////////

 

@@ -961,6 +755,12 @@ let EvalSym2 fullResolverFunc otherResolverFunc returnFunc ctx expr =
               | BoolLiteral(b), x -> if b then x else UnaryNot(x)

               | _ -> recomposed.Force()

           | _ -> recomposed.Force()

+      | OldExpr(e) ->  

+          let e' = __EvalSym resolverFunc returnFunc ctx e

+          let recomposed = OldExpr(e')

+          match e with

+          | IdLiteral(name) -> resolverFunc (IdLiteral(RenameToOld name)) None

+          | _ -> recomposed

       | UnaryExpr(op, e) ->

           let e' = __EvalSym resolverFunc returnFunc ctx e

           let recomposed = UnaryExpr(op, e')

@@ -1049,13 +849,14 @@ let MyDesugar expr removeOriginal =
     | SequenceExpr(_)        -> expr 

     // forall v :: v in {a1 a2 ... an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

     // forall v :: v in [a1 a2 ... an] ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

-    | ForallExpr([Var(vn1,ty1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 ->

+    | ForallExpr([Var(vn1,ty1,old1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 ->

         match rhsCol with 

         | SetExpr(elist)

         | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (__Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral

         | _ -> ForallExpr(v, __Desugar ee)

     | ForallExpr(v,e)        -> ForallExpr(v, __Desugar e)

     | LCIntervalExpr(e)      -> LCIntervalExpr(__Desugar e)

+    | OldExpr(e)             -> OldExpr(__Desugar e)

     | UnaryExpr(op,e)        -> UnaryExpr(op, __Desugar e)

     | AssertExpr(e)          -> AssertExpr(__Desugar e)

     | AssumeExpr(e)          -> AssumeExpr(__Desugar e)

@@ -1113,9 +914,10 @@ let ChangeThisReceiver receiver expr =
     | Dot(e, id)                           -> Dot(__ChangeThis locals e, id)

     | AssertExpr(e)                        -> AssertExpr(__ChangeThis locals e)

     | AssumeExpr(e)                        -> AssumeExpr(__ChangeThis locals e)

-    | ForallExpr(vars,e)                   -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

+    | ForallExpr(vars,e)                   -> let newLocals = vars |> List.map GetVarName |> Set.ofList |> Set.union locals

                                               ForallExpr(vars, __ChangeThis newLocals e)   

     | LCIntervalExpr(e)                    -> LCIntervalExpr(__ChangeThis locals e)

+    | OldExpr(e)                           -> OldExpr(__ChangeThis locals e)

     | UnaryExpr(op,e)                      -> UnaryExpr(op, __ChangeThis locals e)

     | SeqLength(e)                         -> SeqLength(__ChangeThis locals e)

     | SelectExpr(e1, e2)                   -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)

@@ -1157,7 +959,7 @@ let rec PullUpMethodCalls stmt =
                                | MethodOutSelect(_) ->

                                    let vname = SymGen.NewSymFake expr

                                    let e' = VarLiteral(vname)

-                                   let var = VarDeclExpr([Var(vname,None)], true)

+                                   let var = VarDeclExpr([Var(vname,None,false)], true)

                                    let asgn = BinaryGets var expr

                                    stmtList.AddLast asgn |> ignore

                                    Some(e')

@@ -1177,9 +979,20 @@ let rec PullUpMethodCalls stmt =
 //  ==========================================================

 /// Very simple for now: 

 ///   - if "m" is a constructor, everything is modifiable

-///   - otherwise, all objects are immutable (TODO: instead it should read the "modifies" clause of a method and figure out what's modifiable from there)

+///   - if the method's post condition contains assignments to fields, everything is modifiable

+///   - otherwise, all objects are immutable 

+///

+/// (TODO: instead it should read the "modifies" clause of a method and figure out what's modifiable from there)

 //  ==========================================================

-let IsModifiableObj obj m = 

+let IsModifiableObj obj (c,m) = 

+  let __IsFld name = FindVar c name |> Utils.OptionToBool

   match m with

-  | Method(_,_,_,_,isConstr) -> isConstr

+  | Method(_,_,_,_,true) -> true

+  | Method(_,_,_,post,false) -> 

+      DescendExpr2 (fun e acc -> 

+                      match e with 

+                      | BinaryExpr(_,"=",IdLiteral(name),r) when __IsFld name -> true

+                      | Dot(_,name) when __IsFld name -> true

+                      | _ -> acc

+                   ) post false

   | _ -> failwithf "expected a Method but got %O" m
\ No newline at end of file
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 229f19bb..d81fca75 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -1,6 +1,7 @@
 module CodeGen

 

 open Ast

+open Getters

 open AstUtils

 open Utils

 open Resolver

@@ -41,20 +42,21 @@ let rec GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse numUnrolls =
       List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse (numUnrolls - 1))

                                   

 let GetFieldValidExpr flds validFunName numUnrolls = 

-  let fldExprs = flds |> List.map (function Var(name, _) -> IdLiteral(name))

-  let fldNames = flds |> List.map (function Var(name, _) -> name)

+  let fldExprs = flds |> List.map (fun var -> IdLiteral(GetExtVarName var))

+  let fldNames = flds |> List.map GetExtVarName

   let unrolledExprs = GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls

   // add the recursive definition as well

   let recExprs = 

     if not (validFunName = validFuncName) && Options.CONFIG.recursiveValid then

-      flds |> List.map (function Var(name,_) -> BinaryImplies (BinaryNeq (IdLiteral(name)) NullLiteral) (Dot(IdLiteral(name), validFuncName)))

+      flds |> List.map (fun var -> 

+                          let name = GetExtVarName var

+                          BinaryImplies (BinaryNeq (IdLiteral(name)) NullLiteral) (Dot(IdLiteral(name), validFuncName)))

     else

       []

   recExprs @ unrolledExprs

 

 let GetFieldsForValidExpr allFields prog : VarDecl list =

-  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true

-                                     | _                                   -> false)

+  allFields |> List.filter (fun var -> IsUserType prog (GetVarType var))

 

 let GetFieldsValidExprList clsName allFields prog : Expr list =

   let fields = GetFieldsForValidExpr allFields prog

@@ -67,20 +69,21 @@ let GetFieldsValidExprList clsName allFields prog : Expr list =
                               acc |> List.append (GetFieldValidExpr (Set.toList varSet) validFunName numUnrolls)

                            ) []

 

-let PrintValidFunctionCode comp prog genRepr: string = 

+let PrintValidFunctionCode comp prog vars allInvs genRepr nameSuffix: string = 

+  let validFuncName = "Valid" + nameSuffix + "()"

+  let validReprFuncName = "Valid_repr" + nameSuffix + "()"

+  let validSelfFuncName = "Valid_self" + nameSuffix + "()"

   let idt = "    "

   let __PrintInvs invs = 

     invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []

          |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e))

          |> fun s -> if s = "" then (idt + "true") else s

   let clsName = GetClassName comp

-  let vars = GetAllFields comp

   let compTypeName = GetClassType comp |> PrintType

-  let hasLoop = vars |> List.exists (function Var(_,tyOpt) -> match tyOpt with Some(ty) when compTypeName = PrintType ty -> true | _ -> false)

-  let allInvs = GetInvariantsAsList comp |> DesugarLst

+  let hasLoop = vars |> List.exists (fun var -> match GetVarType var with Some(ty) when compTypeName = PrintType ty -> true | _ -> false)

   let fieldsValid = GetFieldsValidExprList clsName vars prog

   

-  let frameFldNames = GetFrameFields comp |> List.choose (function Var(name,_) -> Some(name))

+  let frameFldNames = GetFrameFields comp |> List.map GetExtVarName

   let validReprBody = 

     "    this in Repr &&" + newline +

     "    null !in Repr" + 

@@ -115,7 +118,7 @@ let PrintValidFunctionCode comp prog genRepr: string =
   (__PrintInvs allInvs) + newline +

   "  }" + newline +

   newline +

-  "  function Valid(): bool" + newline +

+  "  function " + validFuncName + ": bool" + newline +

   "    reads *;" + newline +

   decreasesStr + 

   "  {" + newline + 

@@ -123,21 +126,35 @@ let PrintValidFunctionCode comp prog genRepr: string =
   (__PrintInvs fieldsValid) + newline +

   "  }" + newline

 

-let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =

+let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr genOld =

   match prog with

   | Program(components) -> components |> List.fold (fun acc comp -> 

       match comp with  

       | Component(Interface(name,typeParams,members), DataModel(_,_,cVars,frame,inv), code) as comp ->

-        let aVars = FilterFieldMembers members |> List.append (Utils.Ite genRepr [Var("Repr", Some(SetType(NamedType("object", []))))] [])

+        let aVars = FilterFieldMembers members

+        let aOldVars = MakeOldVars aVars

+        let cOldVars = MakeOldVars cVars

+        let allInvs = GetInvariantsAsList comp |> DesugarLst

+        let allOldInvs = MakeOld (allInvs |> List.fold BinaryAnd TrueLiteral) |> SplitIntoConjunts

+        let aVarsAndRepr = aVars |> List.append (Utils.Ite genRepr [Var("Repr", Some(SetType(NamedType("object", []))), false)] [])

         let compMethods = FilterConstructorMembers members

         // Now print it as a Dafny program

         acc + 

         (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +       

         // the fields: original abstract fields plus concrete fields

-        (sprintf "%s" (PrintFields aVars 2 true)) + newline +     

-        (sprintf "%s" (PrintFields cVars 2 false)) + newline +                           

+        (sprintf "%s" (PrintFields aVarsAndRepr 2 true)) + newline +     

+        (sprintf "%s" (PrintFields cVars 2 false)) + newline +  

+        (if genOld then

+           (sprintf "%s" (PrintFields aOldVars 2 true)) + newline +     

+           (sprintf "%s" (PrintFields cOldVars 2 false)) + newline

+         else

+           "") +                                  

         // generate the Valid function

-        (sprintf "%s" (PrintValidFunctionCode comp prog genRepr)) + newline +

+        (sprintf "%s" (PrintValidFunctionCode comp prog (aVars @ cVars) allInvs genRepr "")) + newline +

+        (if genOld then

+           (sprintf "%s" (PrintValidFunctionCode comp prog (aOldVars @ cOldVars) allOldInvs genRepr "_old")) + newline

+         else

+           "") +

         // call the method printer function on all methods of this component

         (methodPrinterFunc comp) +

         // the end of the class

@@ -161,9 +178,9 @@ let GetPostconditionForMethod prog m genRepr =
       // this.Valid() and user-defined post-condition

       let postExpr = BinaryAnd validExpr post

       // method out args are valid

-      let postExpr = (GetMethodOutArgs m) |> List.fold (fun acc (Var(name,tyOpt)) ->

-                                                          if IsUserType prog tyOpt then

-                                                            let varExpr = VarLiteral(name)

+      let postExpr = (GetMethodOutArgs m) |> List.fold (fun acc var ->

+                                                          if IsUserType prog (GetVarType var) then

+                                                            let varExpr = VarLiteral(GetExtVarName var)

                                                             let argValidExpr = BinaryImplies (BinaryNeq varExpr NullLiteral) (Dot(varExpr, validFuncName))

                                                             BinaryAnd acc argValidExpr

                                                           else 

@@ -211,7 +228,7 @@ let PrintReprAssignments prog heapInst indent =
   let idt = Indent indent

   let objs = heapInst.assignments |> List.fold (fun acc assgn -> 

                                                   match assgn with

-                                                  | FieldAssignment((obj,(Var(fldName,_))),_) -> if fldName = "" then acc else acc |> Set.add obj

+                                                  | FieldAssignment((obj,var),_) -> if GetVarName var = "" then acc else acc |> Set.add obj

                                                   | _ -> acc

                                                ) Set.empty

                                   |> Set.toList

@@ -256,13 +273,46 @@ let PrintReprAssignments prog heapInst indent =
     newline + outStr   

                                                           

 let rec PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr =

-  /// just removes all FieldAssignments to unmodifiable objects    

+  let rec __RewriteOldStmt stmt = 

+    match stmt with

+    | Assign(l, r) -> Assign(l, BringToPost r)

+    | ExprStmt(e) -> ExprStmt(BringToPost e)

+    | Block(slist) -> Block(slist |> List.map __RewriteOldStmt)

+

+  let __RewriteOldAsgn a =

+    match a with

+    | FieldAssignment((o,f),e) -> FieldAssignment((o,f), BringToPost e)

+    | ArbitraryStatement(stmt) -> ArbitraryStatement(__RewriteOldStmt stmt)

+

+  /// inserts an assignments into a list of assignments such that the list remains

+  /// topologically sorted wrt field dependencies between different assignments

+  let rec __InsertSorted asgsLst asg = 

+    let ___DependsOn dependentAsg asg = 

+      match asg, dependentAsg with

+      | FieldAssignment((o,f),_), FieldAssignment(_,e) ->

+          let mf = fun e acc -> 

+                          match e with 

+                          | IdLiteral(name) when name = GetVarName f && o.name = "this" -> true

+                          | Dot(discr, name) -> 

+                              let t1 = InferType prog comp (fun s -> None) discr

+                              let t2 = FindComponentForType prog o.objType

+                              acc || (name = GetVarName f && t1 = t2)

+                          | _ -> acc

+          DescendExpr2 (mf    

+                       ) e false

+      | _ -> false

+    match asgsLst with

+    | [] -> [asg]

+    | a :: rest -> if ___DependsOn a asg then asg :: a :: rest else a :: __InsertSorted rest asg                    

+

+  /// - removes all FieldAssignments to unmodifiable objects and old variables

+  /// - rewrites expressions not to use old fields    

   let __RemoveUnmodifiableStuff heapInst = 

     let newAsgs = heapInst.assignments |> List.fold (fun acc a ->

                                                        match a with

-                                                       | FieldAssignment((obj,_),_) when not (Set.contains obj heapInst.modifiableObjs) ->

-                                                           acc

-                                                       | _ -> acc @ [a]

+                                                       | FieldAssignment((obj,_),_) when not (Set.contains obj heapInst.modifiableObjs) -> acc

+                                                       | FieldAssignment((_,var),_) when IsOldVar var -> acc

+                                                       | _ -> __InsertSorted acc (__RewriteOldAsgn a)

                                                     ) []

     { heapInst with assignments = newAsgs }

   

@@ -304,14 +354,15 @@ let PrintHeapCreationCode prog (comp,meth) sol indent genRepr =
     (ghostPre |> SplitIntoConjunts |> PrintSep newline (fun e -> idt + "assume " + (PrintExpr 0 e) + ";")) + newline + 

     (PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr)

       

-let GenConstructorCode prog mthd decreasesClause body genRepr =

+let GenConstructorCode prog comp mthd decreasesClause body genRepr =

   let validExpr = IdLiteral(validFuncName);

   match mthd with

   | Method(methodName,sign,_,_,isConstr) -> 

       let preExpr = GetPreconditionForMethod prog mthd |> Desugar

       let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar

+      let thisObj = {name = "this"; objType = GetComponentType comp}

       "  method " + methodName + (PrintSig sign) + 

-      (if isConstr then newline + "    modifies this;" else "") +

+      (if IsModifiableObj thisObj (comp,mthd) then newline + "    modifies this;" else "") +

       (PrintPrePost (newline + "    requires ") preExpr) + 

       (PrintPrePost (newline + "    ensures ") postExpr) + 

       newline +

@@ -344,7 +395,7 @@ let PrintImplCode prog solutions genRepr =
                                                                   let body = PrintHeapCreationCode prog (c,m) sol 4 genRepr

                                                                   let decr = GetDecreasesClause (c,m) sol

                                                                   body,decr

-                                                            acc + newline + (GenConstructorCode prog m decr mthdBody genRepr) + newline

+                                                            acc + newline + (GenConstructorCode prog comp m decr mthdBody genRepr) + newline

                                   

                                                           else

                                                             acc) "") genRepr
\ No newline at end of file
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index afab212c..1588da57 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -20,6 +20,7 @@ module DafnyModelUtils
 *)

 

 open Ast

+open Getters

 open AstUtils

 open Utils

 

@@ -162,12 +163,16 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
                         let nonebuilder = CascadingBuilder<_>(None)

                         let fldVarOpt = nonebuilder {

                           let! comp = FindComponent prog clsName

-                          return FindVar comp fldName

+                          if fldName.StartsWith("old_") then

+                            let fn = RenameFromOld fldName 

+                            let! var = FindVar comp fn

+                            return Some(MakeOldVar var)

+                          else

+                            return FindVar comp fldName

                         }

                         match fldVarOpt with

                         | Some(fldVar) ->

-                            let fldType = match fldVar with 

-                                          | Var(_,t) -> t

+                            let fldType = GetVarType fldVar 

                             let fldVal = ConvertValue model refVal

                             acc |> Map.add (refObj, fldVar) fldVal

                         | None -> acc

@@ -180,7 +185,8 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
 //  ====================================================================

 let rec ReadArgValues (model: Microsoft.Boogie.Model) args = 

   match args with 

-  | Var(name,_) as v :: rest -> 

+  | v :: rest ->

+      let name = GetVarName v 

       let farg = model.Functions |> Seq.filter (fun f -> f.Arity = 0 && f.Name.StartsWith(name + "#")) |> Utils.SeqToOption

       match farg with

       | Some(func) -> 

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 6c84c482..f2e71e8b 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -1,6 +1,7 @@
 module DafnyPrinter

 

 open Ast

+open Getters

 open AstUtils

 open PrintUtils

 

@@ -14,9 +15,10 @@ let rec PrintType ty =
   | InstantiatedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)

 

 let PrintVarDecl vd =

-  match vd with

-  | Var(id,None) -> id

-  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

+  let name = GetExtVarName vd

+  match GetVarType vd with

+  | None     -> name

+  | Some(ty) -> sprintf "%s: %s" name (PrintType ty)

 

 let rec PrintExpr ctx expr =

   match expr with

@@ -33,6 +35,7 @@ let rec PrintExpr ctx expr =
   | Star -> "*"

   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id

   | LCIntervalExpr(e) -> sprintf "%s.." (PrintExpr 90 e)

+  | OldExpr(e) -> sprintf "old(%s)" (PrintExpr 90 e)

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)

   | BinaryExpr(strength,"in",lhs,BinaryExpr(_,"...",lo,hi)) ->

@@ -102,9 +105,9 @@ let PrintTypeParams typeParams =
 

 let PrintFields vars indent ghost = 

   let ghostStr = if ghost then "ghost " else ""

-  vars |> List.fold (fun acc v -> match v with 

-                                  | Var(nm,None)     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)

-                                  | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""

+  vars |> List.fold (fun acc v -> match GetVarType v with 

+                                  | None     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr (GetExtVarName v) newline)

+                                  | Some(tp) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr (GetExtVarName v) (PrintType tp) newline)) ""

 

 let rec _PrintStmt stmt indent printNewline =

   let idt = Indent indent

diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs
index ef6e8e43..4cbff30b 100644
--- a/Jennisys/FixpointSolver.fs
+++ b/Jennisys/FixpointSolver.fs
@@ -2,6 +2,7 @@
 

 open Ast

 open AstUtils

+open Printer

 open Resolver

 open Utils

 

@@ -146,22 +147,26 @@ let rec ComputeClosure heapInst expandExprFunc premises =
                | _ -> None                 

             ) expr    

 

-  let FindMatches expr except premises = 

+  let FindMatches expr except premises =

+    //Logger.TraceLine ("finding matches for: " + (PrintExpr 0 expr) + "; #premises = " + (Set.count premises |> sprintf "%i"))

     let okToUnifyFunc = fun (varName: string) -> varName.StartsWith("$")

-    premises |> Set.toList

-             |> List.choose (function BinaryExpr(_,"=",lhs,rhs) -> 

-                                        if lhs = expr && not (rhs = except) then 

-                                          Some(rhs)

-                                        elif rhs = expr && not (lhs = except) then

-                                          Some(lhs)

-                                        else 

-                                          match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with

-                                          | Some(unifs) -> Some(ApplyUnifs unifs rhs)

-                                          | None -> 

-                                              match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with

-                                              | Some(unifs) -> Some(ApplyUnifs unifs lhs)

-                                              | None -> None

-                                      | _ -> None)

+    let matches = 

+      premises |> Set.toList

+               |> List.choose (function BinaryExpr(_,"=",lhs,rhs) -> 

+                                          if lhs = expr && not (rhs = except) then 

+                                            Some(rhs)

+                                          elif rhs = expr && not (lhs = except) then

+                                            Some(lhs)

+                                          else 

+                                            match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with

+                                            | Some(unifs) -> Some(ApplyUnifs unifs rhs)

+                                            | None -> 

+                                                match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with

+                                                | Some(unifs) -> Some(ApplyUnifs unifs lhs)

+                                                | None -> None

+                                        | _ -> None)

+    //Logger.TraceLine (sprintf "Number of matches for %s: %i" (PrintExpr 0 expr) (List.length matches))

+    matches

   

   let MySetAdd expr set =

     let x = Printer.PrintExpr 0 expr

@@ -176,6 +181,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   let SelectExprCombinerFunc lst idx = 

     // distribute the indexing operation if possible

     let rec __fff lst idx = 

+      //Logger.TraceLine ("SelectExpr fff for " + (PrintExpr 0 lst))

       let selExpr = SelectExpr(lst, idx)

       match lst with

       | BinaryExpr(_,"+",lhs,rhs) -> 

@@ -195,6 +201,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   let SeqLenCombinerFunc lst =

     // distribute the SeqLength operation if possible 

     let rec __fff lst = 

+      //Logger.TraceLine ("SeqLen fff for " + (PrintExpr 0 lst))

       let lenExpr = SeqLength(lst)

       match lst with

       | BinaryExpr(_,"+",lhs,rhs) -> 

@@ -207,10 +214,11 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   let BinaryInCombiner lhs rhs =

     // distribute the "in" operation if possible

     let rec __fff lhs rhs = 

+      //Logger.TraceLine ("In fff for " + (PrintExpr 0 lhs) + " and " + (PrintExpr 0 rhs))

       let binInExpr = BinaryIn lhs rhs

-      match rhs with

-      | BinaryExpr(_,"+",BinaryExpr(_,"+",SetExpr(_), Dot(_)), Dot(_)) -> Logger.Trace ""

-      | _ -> ()//TODO: remove

+//      match rhs with

+//      | BinaryExpr(_,"+",BinaryExpr(_,"+",SetExpr(_), Dot(_)), Dot(_)) -> Logger.Trace ""

+//      | _ -> ()//TODO: remove

 

       match rhs with

       | BinaryExpr(_,"+",l,r) -> 

@@ -245,6 +253,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   let BinaryNotInCombiner lhs rhs =

     // distribute the "!in" operation if possible

     let rec __fff lhs rhs = 

+      //Logger.TraceLine ("NotIn fff for " + (PrintExpr 0 lhs) + " and " + (PrintExpr 0 rhs))

       let binNotInExpr = BinaryNotIn lhs rhs

       match rhs with

       | BinaryExpr(_,"+",l,r) -> 

@@ -273,6 +282,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
     __fff lhs rhs

 

   let rec __CombineAllMatches expr premises =

+    //Logger.TraceLine ("Combining all matches for: " + (PrintExpr 0 expr))

     let lst0 = FindMatches expr bogusExpr premises 

     let lstCombined = 

       match expr with

@@ -317,6 +327,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
     | expr :: rest ->  

         let newPremises = 

           if expandExprFunc expr then

+            //Logger.TraceLine ("expanding " + (PrintExpr 0 expr))

             __ExpandPremise expr premises

           else 

             premises

@@ -326,7 +337,10 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   (* --- function body starts here --- *)

   let iterOnceFunc p = __Iter (p |> Set.toList) p

   // TODO: iterate only 3 times, instead of to full closure

-  iterOnceFunc premises |> iterOnceFunc |> iterOnceFunc

+  let p1 = iterOnceFunc premises 

+  let p2 = p1 |> iterOnceFunc 

+  let p3 = p2 |> iterOnceFunc

+  p3

 //  let premises' = iterOnceFunc premises 

 //  if premises' = premises then

 //    premises'

diff --git a/Jennisys/Getters.fs b/Jennisys/Getters.fs
new file mode 100644
index 00000000..2e2732af
--- /dev/null
+++ b/Jennisys/Getters.fs
@@ -0,0 +1,284 @@
+module Getters

+

+open Ast

+

+let RenameToOld name = 

+  "old_" + name

+

+let RenameFromOld (name: string) = 

+  if name.StartsWith("old_") then

+    name.Substring(4)

+  else

+    name

+

+// --- search functions ---

+

+//  ==================================

+/// Returns variable name

+//  ==================================

+let GetVarName var =

+  match var with

+  | Var(name,_,_) -> name

+

+let GetExtVarName var = 

+  match var with

+  | Var(id, _, false) -> id

+  | Var(id, _, true) -> RenameToOld id

+

+let IsOldVar var =

+  match var with

+  | Var(_,_,isOld) -> isOld

+

+//  ==================================

+/// Returns variable type

+//  ==================================

+let GetVarType var = 

+  match var with

+  | Var(_,t,_) -> t

+

+//  ===============================================

+/// Returns whether there exists a variable 

+/// in a given VarDecl list with a given name (id)

+//  ===============================================

+let IsInVarList varLst id = 

+  varLst |> List.exists (fun var -> GetVarName var = id)

+

+                     

+//  =========================================================

+/// Out of all "members" returns only those that are "Field"s                                               

+//  =========================================================

+let FilterFieldMembers members =

+  members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)

+

+//  =============================================================

+/// Out of all "members" returns only those that are constructors

+//  =============================================================

+let FilterConstructorMembers members = 

+  members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)

+

+//  =============================================================

+/// Out of all "members" returns only those that are 

+/// constructors and have at least one input parameter

+//  =============================================================

+let FilterConstructorMembersWithParams members = 

+  members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None)

+

+//  ==========================================================

+/// Out of all "members" returns only those that are "Method"s

+//  ==========================================================

+let FilterMethodMembers members = 

+  members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None)

+

+//  =======================================================================

+/// Returns all members of the program "prog" that pass the filter "filter"

+//  =======================================================================

+let FilterMembers prog filter = 

+  match prog with

+  | Program(components) ->

+      components |> List.fold (fun acc comp -> 

+        match comp with

+        | Component(Interface(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            

+        | _ -> acc) []

+

+let GetAbstractFields comp = 

+  match comp with 

+  | Component(Interface(_,_,members), _, _) -> FilterFieldMembers members

+  | _ -> failwithf "internal error: invalid component: %O" comp

+    

+let GetConcreteFields comp = 

+  match comp with 

+  | Component(_, DataModel(_,_,cVars,_,_), _) -> cVars

+  | _ -> failwithf "internal error: invalid component: %O" comp

+     

+//  =================================

+/// Returns all fields of a component

+//  =================================

+let GetAllFields comp = 

+  List.concat [GetAbstractFields comp; GetConcreteFields comp]

+    

+//  ===========================================================

+/// Returns a map (Type |--> Set<Var>) where all 

+/// the given fields are grouped by their type

+///

+/// ensures: forall v :: v in ret.values.elems ==> v in fields

+/// ensures: forall k :: k in ret.keys ==> 

+///            forall v1, v2 :: v1, v2 in ret[k].elems ==> 

+///              v1.type = v2.type

+//  ===========================================================

+let rec GroupFieldsByType fields = 

+  match fields with

+  | Var(name, ty, old) :: rest -> 

+      let map = GroupFieldsByType rest

+      let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty

+      map |> Map.add ty (fldSet |> Set.add (Var(name, ty, old)))

+  | [] -> Map.empty

+ 

+let IsConcreteField comp fldName = GetConcreteFields comp |> List.exists (fun var -> GetVarName var = fldName)

+let IsAbstractField comp fldName = GetAbstractFields comp |> List.exists (fun var -> GetVarName var = fldName)

+                    

+//  =================================

+/// Returns class name of a component

+//  =================================

+let GetClassName comp =

+  match comp with

+  | Component(Interface(name,_,_),_,_) -> name

+  | _ -> failwith ("unrecognized component: " + comp.ToString())

+

+let GetClassType comp = 

+  match comp with

+  | Component(Interface(name,typeParams,_),_,_) -> NamedType(name, typeParams)

+  | _ -> failwith ("unrecognized component: " + comp.ToString())

+

+//  ========================

+/// Returns name of a method

+//  ========================

+let GetMethodName mthd = 

+  match mthd with

+  | Method(name,_,_,_,_) -> name

+  | _ -> failwith ("not a method: " + mthd.ToString())

+

+//  ===========================================================

+/// Returns full name of a method (= <class_name>.<method_name>

+//  ===========================================================

+let GetMethodFullName comp mthd = 

+  (GetClassName comp) + "." + (GetMethodName mthd)

+

+//  =============================

+/// Returns signature of a method

+//  =============================

+let GetMethodSig mthd = 

+  match mthd with

+  | Method(_,sgn,_,_,_) -> sgn

+  | _ -> failwith ("not a method: " + mthd.ToString())

+

+//  =========================================================

+/// Returns all arguments of a method (both input and output)

+//  =========================================================

+let GetSigVars sign = 

+  match sign with

+  | Sig(ins, outs) -> List.concat [ins; outs]

+

+let GetMethodInArgs mthd = 

+  match mthd with

+  | Method(_,Sig(ins, _),_,_,_) -> ins

+  | _ -> failwith ("not a method: " + mthd.ToString())

+

+let GetMethodOutArgs mthd = 

+  match mthd with

+  | Method(_,Sig(_, outs),_,_,_) -> outs

+  | _ -> failwith ("not a method: " + mthd.ToString())

+

+let GetMethodArgs mthd = 

+  let ins = GetMethodInArgs mthd

+  let outs = GetMethodOutArgs mthd

+  List.concat [ins; outs]

+

+let IsConstructor mthd = 

+  match mthd with

+  | Method(_,_,_,_,isConstr) -> isConstr

+  | _ -> failwithf "expected a method but got %O" mthd

+

+let rec GetTypeShortName ty =

+  match ty with

+  | IntType -> "int"

+  | BoolType -> "bool"

+  | SetType(_) -> "set"

+  | SeqType(_) -> "seq"

+  | NamedType(n,_) | InstantiatedType(n,_) -> n

+

+//  ==================================

+/// Returns component name

+//  ==================================

+let GetComponentName comp = 

+  match comp with

+  | Component(Interface(name,_,_),_,_) -> name

+  | _ -> failwithf "invalid component %O" comp

+

+let GetComponentTypeParameters comp = 

+  match comp with

+  | Component(Interface(_,tp,_),_,_) -> tp

+  | _ -> failwithf "invalid component %O" comp

+

+

+//  ==================================

+/// Returns all members of a component

+//  ==================================

+let GetMembers comp =

+  match comp with

+  | Component(Interface(_,_,members),_,_) -> members

+  | _ -> failwith ("unrecognized component: " + comp.ToString())

+

+//  ====================================================

+/// Finds a component of a program that has a given name

+//  ====================================================

+let FindComponent (prog: Program) clsName = 

+  match prog with

+  | Program(comps) -> comps |> List.filter (function Component(Interface(name,_,_),_,_) when name = clsName -> true | _ -> false)

+                            |> Utils.ListToOption

+

+let FindComponentForType prog ty = 

+  FindComponent prog (GetTypeShortName ty)

+

+let FindComponentForTypeOpt prog tyOpt = 

+  match tyOpt with

+  | Some(ty) -> FindComponentForType prog ty

+  | None -> None

+

+let CheckSameCompType comp ty = 

+  GetComponentName comp = GetTypeShortName ty

+

+let GetComponentType comp = 

+  NamedType(GetComponentName comp, GetComponentTypeParameters comp)

+

+//  ===================================================

+/// Finds a method of a component that has a given name

+//  ===================================================

+let FindMethod comp methodName =

+  let x = GetMembers comp

+  let y = x |> FilterMethodMembers

+  let z = y |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

+  GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

+                                         |> Utils.ListToOption

+

+//  ==============================================

+/// Finds a field of a class that has a given name

+//  ==============================================

+//let FindCompVar prog clsName fldName =

+//  let copt = FindComponent prog clsName

+//  match copt with

+//  | Some(comp) -> 

+//      GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

+//                        |> Utils.ListToOption

+//  | None -> None

+

+let FindVar comp fldName =

+  GetAllFields comp |> List.filter (fun var -> GetVarName var = fldName)

+                    |> Utils.ListToOption

+

+//  ======================================

+/// Returns the frame of a given component

+//  ======================================

+let GetFrame comp = 

+  match comp with 

+  | Component(_, DataModel(_,_,_,frame,_), _) -> frame

+  | _ -> failwithf "not a valid component %O" comp

+

+let GetFrameFields comp =

+  let frame = GetFrame comp

+  frame |> List.choose (function IdLiteral(name) -> Some(name) | _ -> None) // TODO: is it really enough to handle only IdLiteral's

+        |> List.choose (fun varName -> 

+                          let v = FindVar comp varName

+                          Utils.ExtractOptionMsg ("field not found: " + varName) v |> ignore

+                          v

+                       )

+

+//  ==============================================

+/// Checks whether two given methods are the same.

+///

+/// Methods are the same if their names are the 

+/// same and their components have the same name.

+//  ==============================================

+let CheckSameMethods (c1,m1) (c2,m2) = 

+  GetComponentName c1 = GetComponentName c2 && GetMethodName m1 = GetMethodName m2

+

+////////////////////////
\ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index e7e129f8..38c444f9 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>examples/Set.jen /genMod /genRepr /method:SetNode.Double</StartArguments>

+    <StartArguments>examples/List.jen /method:Node.Find</StartArguments>

     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

@@ -49,6 +49,7 @@
     <Compile Include="Options.fs" />

     <Compile Include="PipelineUtils.fs" />

     <Compile Include="Ast.fs" />

+    <Compile Include="Getters.fs" />

     <Compile Include="AstUtils.fs" />

     <Compile Include="$(IntermediateOutputPath)\Parser.fs">

       <Visible>false</Visible>

diff --git a/Jennisys/Lexer.fsl b/Jennisys/Lexer.fsl
index 006f1853..e1d4795b 100644
--- a/Jennisys/Lexer.fsl
+++ b/Jennisys/Lexer.fsl
@@ -41,6 +41,7 @@ rule tokenize = parse
 | "..."    { DOTDOTDOT }

 | ".."     { DOTDOT }

 | "."      { DOT }

+| "old"    { OLD }

 | "+"      { PLUS }

 | "-"      { MINUS }

 | "*"      { STAR }

diff --git a/Jennisys/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index 0a6ec6a6..d2b1db68 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/Jennisys/MethodUnifier.fs
@@ -1,6 +1,7 @@
 module MethodUnifier

 

 open Ast

+open Getters

 open AstUtils

 open FixpointSolver

 open PrintUtils

@@ -41,16 +42,17 @@ let TryFindExisting comp targetMthd =
   | None -> targetMthd, Map.empty

 

 let ApplyMethodUnifs receiver (c,m) unifs =

-  let __Apply args = args |> List.map (fun (Var(name,_)) -> 

-                                             match Map.tryFind name unifs with

-                                             | Some(e) -> e

-                                             | None -> VarLiteral(name))

+  let __Apply args = args |> List.map (fun var -> 

+                                         let name = GetExtVarName var

+                                         match Map.tryFind name unifs with

+                                         | Some(e) -> e

+                                         | None -> VarLiteral(name))

   let ins = GetMethodInArgs m |> __Apply

   let outs = GetMethodOutArgs m |> __Apply

   

   let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e -> 

                                           let vname = SymGen.NewSymFake e

-                                          let v = Var(vname, None)

+                                          let v = Var(vname, None, false)

                                           let acc1' = acc1 @ [v]

                                           let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))]

                                           acc1', acc2'

@@ -58,7 +60,7 @@ let ApplyMethodUnifs receiver (c,m) unifs =
   let mcallExpr = MethodCall(receiver, GetComponentName c, GetMethodName m, ins)

   match retVars, outs with

   | [], [] -> [ArbitraryStatement(ExprStmt(mcallExpr))]

-  | [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None)], false), mcallExpr))]

+  | [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None, false)], false), mcallExpr))]

   | _ ->

       let mcall = ArbitraryStatement(Assign(VarDeclExpr(retVars, true), mcallExpr))

       mcall :: asgs

@@ -89,7 +91,7 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
         let idtt = idt + "        "

         unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug 

         let obj = { name = "this"; objType = GetClassType comp }

-        let modObjs = if IsModifiableObj obj m then Set.singleton obj else Set.empty

+        let modObjs = if IsModifiableObj obj (comp,m) then Set.singleton obj else Set.empty

         let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs

         let hInst = { objs           = Utils.MapSingleton obj.name obj;

                       modifiableObjs         = modObjs;

diff --git a/Jennisys/Modularizer.fs b/Jennisys/Modularizer.fs
index 44ac7b80..f5d7e7b7 100644
--- a/Jennisys/Modularizer.fs
+++ b/Jennisys/Modularizer.fs
@@ -1,6 +1,7 @@
 module Modularizer

 

 open Ast

+open Getters

 open AstUtils

 open MethodUnifier

 open PrintUtils

@@ -86,7 +87,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
     match e with

     | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> //TODO: is it really only non-direct children?

         let absFlds = __GetAbsFldAssignments id

-        absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral

+        absFlds |> List.fold (fun acc (var,vval) -> BinaryAnd acc (BinaryEq (Dot(x, GetVarName var)) vval)) TrueLiteral

     | SequenceExpr(elist) ->

         let rec __fff lst acc cnt = 

           match lst with

@@ -107,7 +108,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
   //  ================================================================================

   let __GetSpecFor objLitName =

     let absFieldAssignments = __GetAbsFldAssignments objLitName

-    let absFldAssgnExpr = absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

+    let absFldAssgnExpr = absFieldAssignments |> List.fold (fun acc (var,e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(GetVarName var)) e)) TrueLiteral

     let retValExpr = hInst.methodRetVals |> Map.fold (fun acc varName varValueExpr -> BinaryAnd acc (BinaryEq (VarLiteral(varName)) varValueExpr)) TrueLiteral

     BinaryAnd absFldAssgnExpr retValExpr

   

@@ -119,7 +120,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
     let argSet = DescendExpr2 (fun e acc ->

                                  match e with

                                  | VarLiteral(vname) ->

-                                     match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with

+                                     match args |> List.tryFind (fun var -> GetVarName var = vname) with

                                      | Some(var) -> acc |> Set.add var

                                      | None -> acc

                                  | _ -> acc

diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 5072cc0f..de8e1fb8 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -1,6 +1,7 @@
 %{

 

 open Ast

+open Getters

 open AstUtils

 

 let rec MyFold ee acc =

@@ -21,6 +22,7 @@ let rec MyFold ee acc =
 %token NOT

 %token STAR DIV MOD

 %token PLUS MINUS

+%token OLD

 %token DOTDOT DOTDOTDOT

 %token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN

 %token AND OR

@@ -75,7 +77,7 @@ Pre:
 

 Post: 

   |                           { TrueLiteral }

-	| ENSURES Expr Post         { BinaryAnd $2 $3 }

+  | ENSURES Expr Post         { BinaryAnd $2 $3 }

   | ID GETS Expr Post         { BinaryAnd (BinaryExpr(40,"=",IdLiteral($1),$3)) $4 }

 

 StmtList:

@@ -112,8 +114,8 @@ VarDeclList:
     | VarDecl COMMA VarDeclList { $1 :: $3 }

 

 VarDecl:

-    | ID               { Var($1,None) }

-    | ID COLON Type    { Var($1,Some($3)) }

+    | ID               { Var($1,None, false) }

+    | ID COLON Type    { Var($1,Some($3), false) }

 

 Type:

     | INTTYPE                        { IntType }

@@ -180,10 +182,11 @@ Expr60:
     | Expr60 MOD Expr90   { BinaryExpr(60,"mod",$1,$3) }

 

 Expr90:

-  | Expr100           { $1 }

-  | NOT Expr90        { UnaryExpr("!", $2) }

-  | MINUS Expr90      { UnaryExpr("-", $2) }

-  | Expr90 DOTDOT     { LCIntervalExpr($1) }

+  | Expr100                  { $1 }

+  | OLD LPAREN Expr90 RPAREN { OldExpr($3) }

+  | NOT Expr90               { UnaryExpr("!", $2) }

+  | MINUS Expr90             { UnaryExpr("-", $2) }

+  | Expr90 DOTDOT            { LCIntervalExpr($1) }

 

 Expr100:

   | INTEGER                                  { IntLiteral($1) }

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index af57202f..32ae21ac 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -1,6 +1,7 @@
 module Printer

 

 open Ast

+open Getters

 open AstUtils

 open PrintUtils     

   

@@ -14,9 +15,10 @@ let rec PrintType ty =
   | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)

 

 let PrintVarDecl vd =

-  match vd with

-  | Var(id,None) -> id

-  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

+  let name = GetExtVarName vd

+  match GetVarType vd with

+  | None     -> name

+  | Some(ty) -> sprintf "%s: %s" name (PrintType ty)

 

 let rec PrintExpr ctx expr =

   match expr with

@@ -33,6 +35,7 @@ let rec PrintExpr ctx expr =
   | Star              -> "*"

   | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id

   | LCIntervalExpr(e) -> sprintf "%s.." (PrintExpr 90 e)

+  | OldExpr(e)        -> sprintf "old(%s)" (PrintExpr 90 e)

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)

   | BinaryExpr(strength,op,e0,e1) ->

diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index 82ad98b6..dd5da320 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -8,6 +8,7 @@
 module Resolver

 

 open Ast

+open Getters

 open AstUtils 

 open Printer

 open EnvUtils

@@ -49,10 +50,13 @@ let ConvertToStatements heapInst onModifiableObjsOnly =
   let stmtLst1 = heapInst.assignments |> List.choose (fun asgn ->                                                        

                                                         match asgn with

                                                         | FieldAssignment((o,f),e) when (not onModifiableObjsOnly || Set.contains o heapInst.modifiableObjs) ->

-                                                            let fldName = GetVarName f

-                                                            if fldName = "" then

-                                                              Some(ExprStmt(e))

+                                                            if IsOldVar f then

+                                                              None

                                                             else

+                                                              let fldName = GetVarName f

+                                                              if fldName = "" then

+                                                                Some(ExprStmt(e))

+                                                              else

                                                               Some(Assign(Dot(ObjLiteral(o.name), fldName), e))

                                                         | ArbitraryStatement(stmt) -> Some(stmt)

                                                         | _ -> None)

@@ -173,7 +177,7 @@ let rec _EvalResolver heapInst useConcrete resolveExprFunc expr fldNameOpt =
         match expr with

         | ObjLiteral(objName) -> 

             let asgs = if useConcrete then heapInst.concreteValues else heapInst.assignments

-            let h2 = asgs |> List.filter (function FieldAssignment((o, Var(varName,_)), v) -> o.name = objName && varName = fldName | _ -> false)

+            let h2 = asgs |> List.filter (function FieldAssignment((o, var), v) -> o.name = objName && GetExtVarName var = fldName | _ -> false)

             match h2 with

             | FieldAssignment((_,_),x) :: [] -> __FurtherResolve x

             | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName))

@@ -232,7 +236,7 @@ let EvalAndCheckTrue heapInst resolveExprFunc expr =
 /// (HeapInstance), where all fields for all objects have explicit 

 /// assignments.

 //  =====================================================================

-let ResolveModel hModel meth = 

+let ResolveModel hModel (comp,meth) = 

   let outArgs = GetMethodOutArgs meth

   let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->

                                         let objName, objTypeOpt = match Resolve hModel o with

@@ -250,7 +254,7 @@ let ResolveModel hModel meth =
                                            | FieldAssignment((obj,_),_) -> 

                                                let acc1' = acc1 |> Map.add obj.name obj

                                                let acc2' = 

-                                                 if IsModifiableObj obj meth then

+                                                 if IsModifiableObj obj (comp,meth) then

                                                    acc2 |> Set.add obj

                                                  else

                                                    acc2

@@ -261,7 +265,7 @@ let ResolveModel hModel meth =
                                                   match k with

                                                   | VarConst(name) -> 

                                                       let resolvedValExpr = Resolve hModel v

-                                                      if outArgs |> List.exists (function Var(varName, _) -> varName = name) then

+                                                      if outArgs |> List.exists (fun var -> GetVarName var = name) then

                                                         acc1, acc2 |> Map.add name (resolvedValExpr |> Const2Expr)

                                                       else

                                                         acc1 |> Map.add name resolvedValExpr, acc2

diff --git a/Jennisys/TypeChecker.fs b/Jennisys/TypeChecker.fs
index 6556e639..cef88072 100644
--- a/Jennisys/TypeChecker.fs
+++ b/Jennisys/TypeChecker.fs
@@ -1,6 +1,7 @@
 module TypeChecker

 

 open Ast

+open Getters

 open AstUtils

 open Printer

 open System.Collections.Generic

@@ -42,16 +43,15 @@ let TypeCheck prog =
 let MethodArgChecker prog meth varName = 

   let ins = GetMethodInArgs meth

   let outs = GetMethodOutArgs meth

-  ins @ outs |> List.choose (function Var(vname,ty) when vname = varName -> ty |> FindComponentForTypeOpt prog | _ -> None) |> Utils.ListToOption

+  ins @ outs |> List.choose (fun var -> if GetVarName var = varName then GetVarType var |> FindComponentForTypeOpt prog else None) |> Utils.ListToOption

 

 // TODO: implement this

 let rec InferType prog thisComp checkLocalFunc expr = 

   let __FindVar comp fldName = 

     let var = FindVar comp fldName |> Utils.ExtractOption

-    match var with

-    | Var(_, tyOpt) -> 

-        let c = FindComponentForType prog (Utils.ExtractOption tyOpt) |> Utils.ExtractOption

-        Some(c)

+    let c = FindComponentForType prog (Utils.ExtractOption (GetVarType var)) |> Utils.ExtractOption

+    Some(c)

+    

   try 

     match expr with

     | ObjLiteral("this") -> Some(thisComp)

diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index dcb13f08..e39464f1 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -22,6 +22,14 @@ let BoolToOption b =
 //  =====================================

 /// ensures: ret = (opt == Some(_))

 //  =====================================

+let OptionToBool opt = 

+  match opt with

+  | Some(_) -> true

+  | None -> false

+

+//  =====================================

+/// ensures: ret = (opt == Some(_))

+//  =====================================

 let IsSomeOption opt = 

   match opt with

   | Some(_) -> true

diff --git a/Jennisys/examples/Simple.jen b/Jennisys/examples/Simple.jen
new file mode 100644
index 00000000..bd2e2993
--- /dev/null
+++ b/Jennisys/examples/Simple.jen
@@ -0,0 +1,11 @@
+interface Simple {

+ var a: int

+ 

+ method Inc()

+   a := old(a) + 1

+}

+

+datamodel Simple {

+ var c: int

+ invariant a = c

+}
\ No newline at end of file