jennisys: got the List.Get example to work. List.Tail also works. Others should follow soon

10 files changed, 353 insertions, 239 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index f31c41ec..6f8c5d87 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -43,6 +43,7 @@ let GenMethodAnalysisCode comp m assertion =
   let ppre,ppost = GetMethodPrePost m 

   let pre = Desugar ppre

   let post = Desugar ppost

+  let ghostPre = GetMethodGhostPrecondition m |> Desugar 

   //let sigStr = PrintSig signature

   let sigVars = 

     match signature with

@@ -54,7 +55,9 @@ let GenMethodAnalysisCode comp m assertion =
   // print signature as local variables

   sigVars +

   "    // assume precondition" + newline +

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

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

+  "    // assume ghost precondition" + newline +

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

   "    // assume invariant and postcondition" + newline + 

   "    assume Valid();" + newline +

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

@@ -70,7 +73,7 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
   match onlyForThese with

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

     match m with 

-    | Method(methodName, sign, pre, post, _) -> 

+    | Method(_) -> 

         (GenMethodAnalysisCode c m assertion) + newline +

         (MethodAnalysisPrinter rest assertion comp)

     | _ -> ""

@@ -164,12 +167,13 @@ let IsUnmodConcrOnly prog (comp,meth) expr =
           false

         else

           // assume it is unmodifiable, because it is a method, so just check if it's concrete

-          let lhsType = InferType prog comp e |> Utils.ExtractOptionMsg (sprintf "Inference failed for %s" (PrintExpr 0 e))

+          let lhsType = InferType prog comp (MethodArgChecker prog meth) e |> Utils.ExtractOptionMsg (sprintf "Inference failed for %s" (PrintExpr 0 e))

           IsConcreteField lhsType fldName          

     | AssertExpr(e)

     | AssumeExpr(e)

     | SeqLength(e)

     | LCIntervalExpr(e)

+    | MethodOutSelect(e,_)   

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

     | SelectExpr(e1, e2)

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

@@ -487,7 +491,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
         Logger.InfoLine (sprintf "%s    candidate pre-condition: %s" idt (PrintExpr 0 candCond))

         Logger.InfoLine (sprintf "%s    ------------------------" idt)

         let idt = idt + "  "

-        let _,_,m2 = AddPrecondition prog comp m candCond

+        let m2 = AddPrecondition prog comp m candCond

         let sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph

         Logger.Info (idt + "    - verifying partial solution ... ")

         let verified = 

@@ -530,7 +534,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
         let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

                       | Some(sol2) -> sol2

                       | None -> sol   

-        let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

+        let m3 = AddPrecondition prog comp m (UnaryNot(candCond))

         let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph

         MergeSolutions solThis solRest |> FixSolution comp m

     | None -> 

@@ -543,7 +547,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
     expr |> SplitIntoConjunts |> List.iter loggerFunc

 

     let premises = expr |> FindTrueClauses (fun e -> false) heapInst2

-    let closedPremise = ComputeClosure (premises |> Set.ofList) heapInst2

+    let closedPremise = ComputeClosure heapInst2 (premises |> Set.ofList) 

 

     // --- trace

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

@@ -552,6 +556,30 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
     closedPremise |> Set.iter loggerFunc

 

     //------------------

+    let compName = GetComponentName comp

+    let methName = GetMethodName m

+

+    let __IsOk expr = 

+      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 __CheckSol hInst premises = 

       let rec __CheckVars vars = 

         match vars with

@@ -560,6 +588,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
                                       |> List.choose (function

                                                         | BinaryExpr(_,"=",l,r) -> if l = lhs then Some(r) elif r = lhs then Some(l) else None

                                                         | _ -> None)

+                                      |> List.filter __IsOk

                                       |> List.map (fun e -> [lhs,e])

             lhsOptions

         | lhs :: rest -> 

@@ -576,65 +605,102 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
                                             | Assign(lhs,_) -> Some(lhs)

                                             | _ -> None)

       __CheckVars modVars

+

+    let rec __ConvToAssignments s = 

+      match s with 

+      | (l,r) :: rest ->

+          ArbitraryStatement(Assign(l,r)) :: __ConvToAssignments rest

+      | [] -> []

+

+    let rec __IterSolutions hInst sList = 

+      match sList with

+      | s :: rest -> 

+          let asgs = __ConvToAssignments s

+          let hInst' = { hInst with assignments = asgs; methodRetVals = Map.empty}

+          let sol = Utils.MapSingleton (comp,m) [TrueLiteral, hInst']

+          Logger.Info (idt + "    ")

+          if VerifySolution prog sol Options.CONFIG.genRepr then

+            Logger.InfoLine "~~~ VERIFIED ~~~"

+            Some(sol)

+          else 

+            Logger.InfoLine "!!! NOT VERIFIED !!!"

+            __IterSolutions hInst rest    

+      | [] -> None

     //-------------------

 

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

-    let compName = GetComponentName comp

-    let methName = GetMethodName m

     let invocationArgs = GetMethodInArgs m |> List.map (function Var(name,_) -> VarLiteral("$" + name))

-      

-    let s = __CheckSol heapInst2 closedPremise

-     

-    // add only recursive calls to immediate children

+                                                     

+    // add only recursive call for now

+    let ins = GetMethodInArgs m

+    let outs = GetMethodOutArgs m

     let post = GetMethodPrePost m |> snd 

                                   |> RewriteWithCtx (fun ctx e -> 

                                                         match e with 

-                                                        | VarLiteral(id) when not (IsInVarList ctx id) -> Some(VarLiteral("$" + id)) 

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

+                                                            if IsInVarList outs id then

+                                                              //Some(VarLiteral((GetMethodFullName comp m) + "_" + id))

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

+                                                              let outSel = MethodOutSelect(mcall, id)

+                                                              Some(outSel)

+                                                            else

+                                                              Some(VarLiteral("$" + id)) 

                                                         | _ -> None) []

-    

-    let rec Try spec s = 

-      match s with

-      | fs :: rest -> 

-          let goal = fs |> List.fold (fun acc (e1,e2) -> BinaryAnd acc (BinaryEq e1 e2)) TrueLiteral

-          match UnifyImplies spec goal LTR Map.empty with

-          | Some(x) -> Some(x)

-          | None -> Try spec rest

-      | [] -> None

+                                  |> ChangeThisReceiver (VarLiteral("$this"))

+    let closedPremises' = closedPremise |> Set.add post |> ComputeClosure heapInst2

+    Logger.TraceLine "Closed premises with methods"

+    closedPremises' |> Set.iter loggerFunc

 

-    let rec __IterAsgs asgs = 

-      match asgs with

-      | FieldAssignment((obj,Var(fldName,Some(fldType))),fldVal) :: rest

-            when obj.name = "this" && not (fldVal = NullLiteral) && IsConcreteField comp fldName && CheckSameCompType comp fldType ->

-          let receiver = Dot(ThisLiteral, fldName)

-          let changedThis = ChangeThisReceiver receiver post

-          let mcall = MethodCall(receiver, compName, methName, invocationArgs)

-

-          match Try changedThis s with

-          | Some(unifs) -> 

-              let unifs = unifs |> Map.fold (fun acc (k: string) v -> acc |> Map.add (k.Replace("$", "")) v) Map.empty

-              //s |> Map.iter (fun k v -> Logger.TraceLine (sprintf "%s --> %s" k (PrintExpr 0 v)))

-              let asgs = ApplyMethodUnifs receiver (comp,m) unifs

-              let restRes = __IterAsgs rest              

-              (fst restRes, asgs @ (snd restRes))

-          | None -> (false, [])

-      | _ :: rest -> 

-          __IterAsgs rest

-      | [] -> (true, [])

-   

-    match __IterAsgs heapInst2.assignments with

-    | (true, asgs) -> 

-        Logger.InfoLine "AAAAAAAAAAAAAAAAA"

-        let heapInst3 = {heapInst2 with assignments = asgs}

-        let sol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst3]

-        Logger.Info (idt + "    ")

-        if VerifySolution prog sol Options.CONFIG.genRepr then

-          Logger.InfoLine "~~~ VERIFIED ~~~"

-          sol

-        else 

-          Logger.InfoLine "!!! NOT VERIFIED !!!"

-          sol

+    let s = __CheckSol heapInst2 closedPremises'

+    match __IterSolutions heapInst2 s with

+    | Some(x) -> x 

+    | None -> wrongSol

 

-    | (false, _) -> wrongSol

+    //s |> List.iter (fun lst -> lst |> List.iter (fun (l,r) -> Logger.TraceLine (sprintf "%s = %s" (PrintExpr 0 l) (PrintExpr 0 r))))

+    

+//    let rec Try spec s = 

+//      match s with

+//      | fs :: rest -> 

+//          let goal = fs |> List.fold (fun acc (e1,e2) -> BinaryAnd acc (BinaryEq e1 e2)) TrueLiteral

+//          match UnifyImplies spec goal LTR Map.empty with

+//          | Some(x) -> Some(x)

+//          | None -> Try spec rest

+//      | [] -> None

+//

+//    let rec __IterAsgs asgs = 

+//      match asgs with

+//      | FieldAssignment((obj,Var(fldName,Some(fldType))),fldVal) :: rest

+//            when obj.name = "this" && not (fldVal = NullLiteral) && IsConcreteField comp fldName && CheckSameCompType comp fldType ->

+//          let receiver = Dot(ThisLiteral, fldName)

+//          let changedThis = ChangeThisReceiver receiver post

+//          let mcall = MethodCall(receiver, compName, methName, invocationArgs)

+//

+//          match Try changedThis s with

+//          | Some(unifs) -> 

+//              let unifs = unifs |> Map.fold (fun acc (k: string) v -> acc |> Map.add (k.Replace("$", "")) v) Map.empty

+//              //s |> Map.iter (fun k v -> Logger.TraceLine (sprintf "%s --> %s" k (PrintExpr 0 v)))

+//              let asgs = ApplyMethodUnifs receiver (comp,m) unifs

+//              let restRes = __IterAsgs rest              

+//              (fst restRes, asgs @ (snd restRes))

+//          | None -> (false, [])

+//      | _ :: rest -> 

+//          __IterAsgs rest

+//      | [] -> (true, [])

+//   

+//    match __IterAsgs heapInst2.assignments with

+//    | (true, asgs) -> 

+//        Logger.InfoLine "AAAAAAAAAAAAAAAAA"

+//        let heapInst3 = {heapInst2 with assignments = asgs}

+//        let sol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst3]

+//        Logger.Info (idt + "    ")

+//        if VerifySolution prog sol Options.CONFIG.genRepr then

+//          Logger.InfoLine "~~~ VERIFIED ~~~"

+//          sol

+//        else 

+//          Logger.InfoLine "!!! NOT VERIFIED !!!"

+//          sol

+//

+//    | (false, _) -> wrongSol

                                           

 //    if List.isEmpty s then

 //

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index beb4ba2e..bc66e761 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -48,6 +48,7 @@ type Expr =
   | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list

   | ForallExpr of VarDecl list * Expr

   | MethodCall of (* receiver *) Expr * (* component name *) string * (* method name *) string * (* actual parameters *) Expr list

+  | MethodOutSelect of (* method *) Expr * (* out param name *) string

   | VarDeclExpr of (* var list *) VarDecl list * (* declareAlso *) bool

   | AssertExpr of Expr

   | AssumeExpr of Expr

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index b56ddb57..dba80e88 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -64,6 +64,7 @@ let rec Rewrite rewriterFunc expr =
   | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map __RewriteOrRecurse)

   | SetExpr(exs)                     -> SetExpr(exs |> List.map __RewriteOrRecurse)

   | MethodCall(rcv,cname,mname,ins)  -> MethodCall(__RewriteOrRecurse rcv, cname, mname, ins |> List.map __RewriteOrRecurse)

+  | MethodOutSelect(mth,name)        -> MethodOutSelect(__RewriteOrRecurse mth, name)

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

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

 

@@ -95,6 +96,7 @@ let rec RewriteWithCtx rewriterFunc ctx expr =
   | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map (__RewriteOrRecurse ctx))

   | SetExpr(exs)                     -> SetExpr(exs |> List.map (__RewriteOrRecurse ctx))

   | MethodCall(rcv,cname,mname,ins)  -> MethodCall(__RewriteOrRecurse ctx rcv, cname, mname, ins |> List.map (__RewriteOrRecurse ctx))

+  | MethodOutSelect(mth,name)        -> MethodOutSelect(__RewriteOrRecurse ctx mth, name)

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

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

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

@@ -163,7 +165,8 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

-  | UnaryExpr(_,e)           

+  | UnaryExpr(_,e) 

+  | MethodOutSelect(e,_)          

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

   | SelectExpr(e1, e2)

   | BinaryExpr(_,_,e1,e2)            -> __Compose (e1 :: e2 :: [])

@@ -190,7 +193,8 @@ let rec DescendExpr2 visitorFunc expr acc =
   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

-  | UnaryExpr(_,e)           

+  | UnaryExpr(_,e)  

+  | MethodOutSelect(e,_)         

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

   | SelectExpr(e1, e2)

   | BinaryExpr(_,_,e1,e2)            -> __Pipe (e1 :: e2 :: [])

@@ -453,8 +457,15 @@ let GetMethodSig mthd =
   | _ -> failwith ("not a method: " + mthd.ToString())

 

 let GetMethodPrePost mthd = 

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

   match mthd with

-  | Method(_,_,pre,post,_) -> pre,post

+  | Method(_,_,pre,post,_) -> __FilterOutAssumes pre,post

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

+

+let GetMethodGhostPrecondition mthd = 

+  match mthd with 

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

+      pre |> SplitIntoConjunts |> List.choose (function AssumeExpr(e) -> Some(e) | _ -> None) |> List.fold BinaryAnd TrueLiteral

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

 

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

@@ -543,6 +554,11 @@ let FindComponent (prog: Program) clsName =
 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

 

@@ -615,9 +631,8 @@ let AddReplaceMethod prog comp newMthd oldMethod =
 let AddPrecondition prog comp m e =

   match m with

   | Method(mn, sgn, pre, post, cstr) ->

-      let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)

-      let newProg, newComp = AddReplaceMethod prog comp newMthd (Some(m))

-      newProg, newComp, newMthd

+      let newMthd = Method(mn, sgn, BinaryAnd pre (AssumeExpr(e)), post, cstr)

+      newMthd

   | _ -> failwithf "Not a method: %O" m

 

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

@@ -683,6 +698,8 @@ let rec __EvalSym resolverFunc returnFunc ctx expr =
     | SetExpr(elist) -> 

         let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc returnFunc ctx e) acc) Set.empty

         SetExpr(Set.toList eset') 

+    | MethodOutSelect(e,name) -> 

+        MethodOutSelect(__EvalSym resolverFunc returnFunc ctx e, name)

     | MethodCall(rcv,cname, mname,aparams) ->

         let rcv' = __EvalSym resolverFunc returnFunc ctx rcv

         let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc returnFunc ctx e :: acc) [] |> List.rev

@@ -922,7 +939,8 @@ let MyDesugar expr removeOriginal =
     | SeqLength(_)           

     | UpdateExpr(_)     

     | SetExpr(_)

-    | MethodCall(_)     

+    | MethodCall(_)  

+    | MethodOutSelect(_)   

     | 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] 

@@ -1001,6 +1019,7 @@ let ChangeThisReceiver receiver expr =
     | UpdateExpr(e1,e2,e3)                 -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

     | SequenceExpr(exs)                    -> SequenceExpr(exs |> List.map (__ChangeThis locals))

     | SetExpr(exs)                         -> SetExpr(exs |> List.map (__ChangeThis locals))

+    | MethodOutSelect(e, name)             -> MethodOutSelect(__ChangeThis locals e, name)

     | MethodCall(rcv,cname, mname,aparams) -> MethodCall(__ChangeThis locals rcv, cname, mname, aparams |> List.map (__ChangeThis locals))

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

   __ChangeThis Set.empty expr

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 2892a07b..2f50a360 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -144,6 +144,42 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =
         "}" + newline + newline

       | _ -> assert false; "") ""

 

+let PrintPrePost pfix expr = 

+  SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

+

+let GetPreconditionForMethod prog m = 

+  let validExpr = IdLiteral(validFuncName);

+  if IsConstructor m then

+    GetMethodPrePost m |> fst

+  else 

+    BinaryAnd validExpr (GetMethodPrePost m |> fst)

+  

+let GetPostconditionForMethod prog m genRepr = 

+  let validExpr = IdLiteral(validFuncName);

+  match m with

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

+      // 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 argValidExpr = BinaryImplies (BinaryNeq varExpr NullLiteral) (Dot(varExpr, validFuncName))

+                                                            BinaryAnd acc argValidExpr

+                                                          else 

+                                                            acc

+                                                       ) postExpr

+      // fresh Repr

+      if genRepr then

+        let freshExpr = if isConstr then "fresh(Repr - {this})" else "fresh(Repr - old(Repr))";

+        BinaryAnd (IdLiteral(freshExpr)) postExpr

+      else

+        postExpr

+  | _ -> failwithf "expected a method, got %O" m 

+

+let PrintAssumePostcondition prog m genRepr prefix = 

+  PrintPrePost prefix (GetPostconditionForMethod prog m genRepr |> Desugar) + newline

+

 let GetAllocObjects heapInst = 

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

                                        match a with

@@ -219,7 +255,7 @@ let PrintReprAssignments prog heapInst indent =
   else 

     newline + outStr   

                                                           

-let rec PrintHeapCreationCode prog sol indent genRepr =

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

   /// just removes all FieldAssignments to unmodifiable objects    

   let __RemoveUnmodifiableStuff heapInst = 

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

@@ -229,7 +265,7 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
                                                        | _ -> acc @ [a]

                                                     ) []

     { heapInst with assignments = newAsgs }

-

+  

   let idt = Indent indent

   match sol with

   | (c, hi) :: rest ->

@@ -243,7 +279,7 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
         (PrintAllocNewObjects heapInstMod indent) +

         (PrintVarAssignments heapInstMod indent) +

         (__ReprAssignments indent) +

-        (PrintHeapCreationCode prog rest indent genRepr) 

+        (PrintHeapCreationCodeOld prog (comp,meth) rest indent genRepr) 

       else

         if List.length rest > 0 then

           idt + "if (" + (PrintExpr 0 c) + ") {" + newline +

@@ -251,7 +287,7 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
           (PrintVarAssignments heapInstMod (indent+2)) +

           (__ReprAssignments (indent+2)) +

           idt + "} else {" + newline + 

-          (PrintHeapCreationCode prog rest (indent+2) genRepr) +

+          (PrintHeapCreationCodeOld prog (comp,meth) rest (indent+2) genRepr) +

           idt + "}" + newline

         else 

           (PrintAllocNewObjects heapInstMod indent) +

@@ -259,46 +295,19 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
           (__ReprAssignments indent)

   | [] -> ""

 

-let PrintPrePost pfix expr = 

-  SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

-

-let GetPreconditionForMethod prog m = 

-  let validExpr = IdLiteral(validFuncName);

-  match m with

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

-      if isConstr then

-        pre

-      else

-        BinaryAnd validExpr pre

-  | _ -> failwithf "expected a method, got %O" m     

-

-let GetPostconditionForMethod prog m genRepr = 

-  let validExpr = IdLiteral(validFuncName);

-  match m with

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

-      // 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 argValidExpr = BinaryImplies (BinaryNeq varExpr NullLiteral) (Dot(varExpr, validFuncName))

-                                                            BinaryAnd acc argValidExpr

-                                                          else 

-                                                            acc

-                                                       ) postExpr

-      // fresh Repr

-      if genRepr then

-        let freshExpr = if isConstr then "fresh(Repr - {this})" else "fresh(Repr - old(Repr))";

-        BinaryAnd (IdLiteral(freshExpr)) postExpr

-      else

-        postExpr

-  | _ -> failwithf "expected a method, got %O" m     

+let PrintHeapCreationCode prog (comp,meth) sol indent genRepr =

+  let idt = Indent indent

+  let ghostPre = GetMethodGhostPrecondition meth

+  if ghostPre = TrueLiteral then

+    PrintHeapCreationCodeOld prog (comp,meth) sol indent genRepr

+  else 

+    (ghostPre |> SplitIntoConjunts |> PrintSep newline (fun e -> idt + "assume " + (PrintExpr 0 e) + ";")) + newline + 

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

       

 let GenConstructorCode prog mthd body genRepr =

   let validExpr = IdLiteral(validFuncName);

   match mthd with

-  | Method(methodName, sign, pre, post, isConstr) -> 

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

       let preExpr = GetPreconditionForMethod prog mthd |> Desugar

       let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar

       "  method " + methodName + (PrintSig sign) + 

@@ -321,9 +330,10 @@ let PrintImplCode prog solutions genRepr =
                                                               match sol with

                                                               | [] -> 

                                                                   "    //unable to synthesize" +

-                                                                  PrintPrePost (newline + "    assume ") (GetPostconditionForMethod prog m genRepr |> Desugar) + newline

+                                                                  PrintAssumePostcondition prog m genRepr (newline + "    assume ")

+                                                                  //PrintPrePost (newline + "    assume ") (GetPostconditionForMethod prog m genRepr |> Desugar) + newline

                                                               | _ -> 

-                                                                  PrintHeapCreationCode prog sol 4 genRepr

+                                                                  PrintHeapCreationCode prog (c,m) sol 4 genRepr

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

                                   

                                                           else

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 947a72f2..44fd1d50 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -69,6 +69,9 @@ let rec PrintExpr ctx expr =
       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

   | MethodCall(rcv,_,name,aparams) ->

       sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

+  | MethodOutSelect(mth,name)      ->      

+      // TODO: this can only work if there is only 1 out parameter

+      sprintf "%s" (PrintExpr 0 mth) 

 

 let rec PrintConst cst = 

   match cst with 

diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs
index 097e72c9..5fff60c6 100644
--- a/Jennisys/FixpointSolver.fs
+++ b/Jennisys/FixpointSolver.fs
@@ -5,145 +5,25 @@ open AstUtils
 open Resolver

 open Utils

 

-let rec ComputeClosure premises heapInst = 

-  let bogusExpr = VarLiteral("!@#$%^&*()")

-

-  let FindMatches expr except premises = 

-    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 None

-                                      | _ -> None)

-  

-  let MySetAdd expr set =

-    match expr with

-    | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && Set.contains (BinaryExpr(p,op,rhs,lhs)) set -> set

-    | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && rhs = lhs -> set

-    | _ -> Set.add expr set

-

-//  let rec __ExpandPremise expr premises = 

-//    let bogusExpr = VarLiteral("!@#$%^&*()")

-//    match expr with

-//    | BinaryExpr(p,op,lhs,rhs) ->

-//        let __AddLhsToPremisses expr exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryExpr(p,op,expr,e)) acc) premises

-//        let __AddRhsToPremisses exprLst expr premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryExpr(p,op,e,expr)) acc) premises

-//        let premises' = __ExpandPremise lhs premises |> __ExpandPremise rhs

-//        let lhsMatches = __FindMatches lhs rhs premises'

-//        let rhsMatches = __FindMatches rhs lhs premises'

-//        premises' |> __AddLhsToPremisses lhs rhsMatches 

-//                  |> __AddRhsToPremisses lhsMatches rhs

-//    | UnaryExpr(op, sub) ->

-//        let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryEq expr (UnaryExpr(op,e))) acc) premises

-//        let premises' = __ExpandPremise sub premises

-//        let subMatches = __FindMatches sub bogusExpr premises'

-//        premises' |> __AddToPremisses subMatches 

-//    | SelectExpr(lst, idx) ->

-//        let __EvalLst lst idx = BinaryEq expr (SelectExpr(lst,idx))

-//

-//

-//        let __AddLstToPremisses lstMatches idx premises = lstMatches |> List.fold (fun acc lst -> MySetAdd (__EvalLst lst idx) acc) premises

-//        let __AddIdxToPremisses lst idxMatches premises = idxMatches |> List.fold (fun acc idx -> MySetAdd (__EvalLst lst idx) acc) premises

-//        let premises' = __ExpandPremise lst premises |> __ExpandPremise idx

-//        let lstMatches = __FindMatches lst bogusExpr premises'

-//        let idxMatches = __FindMatches idx bogusExpr premises'

-//        premises' |> __AddLstToPremisses lstMatches idx

-//                  |> __AddIdxToPremisses lst idxMatches

-//

-//    | _ -> premises

-

-  let SelectExprCombinerFunc lst idx = 

-    // distribute the indexing operation if possible

-    let rec __fff lst idx = 

-      let selExpr = SelectExpr(lst, idx)

-      match lst with

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

-          let idxVal = EvalFull heapInst idx |> Expr2Int

-          let lhsVal = EvalFull heapInst lhs |> Expr2List

-          let rhsVal = EvalFull heapInst rhs |> Expr2List

-          if idxVal < List.length lhsVal then

-            __fff lhs idx

-          else 

-            __fff rhs (BinarySub idx (IntLiteral(List.length lhsVal)))

-      | SequenceExpr(elist) -> 

-          let idxVal = EvalFull heapInst idx |> Expr2Int

-          [elist.[idxVal]]

-      | _ -> [selExpr] 

-    __fff lst idx   

-

-  let SeqLenCombinerFunc lst =

-    // distribute the SeqLength operation if possible 

-    let rec __fff lst = 

-      let lenExpr = SeqLength(lst)

-      match lst with

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

-          BinaryAdd (__fff lhs) (__fff rhs)          

-      | SequenceExpr(elist) -> 

-          IntLiteral(List.length elist)

-      | _ -> lenExpr

-    [__fff lst]

-

-  let rec __CombineAllMatches expr premises =

-    match expr with

-    | BinaryExpr(p,op,lhs,rhs) -> 

-        let lhsMatches = __CombineAllMatches lhs premises

-        let rhsMatches = __CombineAllMatches rhs premises

-        Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches

-    | UnaryExpr(op,sub) -> 

-        __CombineAllMatches sub premises |> List.map (fun e -> UnaryExpr(op,e))

-    | SelectExpr(lst,idx) -> 

-        let lstMatches = __CombineAllMatches lst premises

-        let idxMatches = __CombineAllMatches idx premises

-        Utils.ListCombineMult SelectExprCombinerFunc lstMatches idxMatches

-    | SeqLength(lst) -> 

-        __CombineAllMatches lst premises |> List.map SeqLenCombinerFunc |> List.concat

-    // TODO: other cases

-    | _ -> expr :: (FindMatches expr bogusExpr premises)

-

-  let rec __ExpandPremise expr premises = 

-    let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd e acc) premises

-    let allMatches = lazy(__CombineAllMatches expr premises)

-    match expr with

-    | BinaryExpr(p,op,lhs,rhs) when IsRelationalOp op ->

-        let x = allMatches.Force()

-        __AddToPremisses x premises

-    | SelectExpr(lst, idx) ->

-        let x = allMatches.Force()

-        __AddToPremisses x premises

-    | _ -> premises  

-

-  let rec __Iter exprLst premises = 

-    match exprLst with

-    | expr :: rest ->  

-        let newPremises = __ExpandPremise expr premises

-        __Iter rest newPremises

-    | [] -> premises

-

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

-  let premises' = __Iter (premises |> Set.toList) premises

-  if premises' = premises then

-    premises'

-  else 

-    ComputeClosure premises' heapInst

-

-

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

 

 type UnifDirection = LTR | RTL

 

 exception CannotUnify

 

-let rec UnifyImplies lhs rhs dir unifs = 

+let rec SelectiveUnifyImplies okToUnifyFunc lhs rhs dir unifs = 

   ///

-  let __AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)

+  let __AddOrNone unifs name e = 

+    if okToUnifyFunc name then

+      Some(unifs |> Utils.MapAddNew name e)

+    else

+      None

   

   ///

   let __UnifLists lstL lstR = 

     if List.length lstL = List.length lstR then

       try 

-        let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with

+        let unifs2 = List.fold2 (fun acc elL elR -> match SelectiveUnifyImplies okToUnifyFunc elL elR dir acc with

                                                     | Some(u) -> u

                                                     | None -> raise CannotUnify) unifs lstL lstR

         Some(unifs2)

@@ -190,8 +70,8 @@ let rec UnifyImplies lhs rhs dir unifs =
           let __TryUnifyPair x1 a1 x2 a2 unifs = 

             let builder = new Utils.CascadingBuilder<_>(None)

             builder {

-              let! unifsLhs = UnifyImplies x1 a1 dir unifs

-              let! unifsRhs = UnifyImplies x2 a2 dir unifsLhs

+              let! unifsLhs = SelectiveUnifyImplies okToUnifyFunc x1 a1 dir unifs

+              let! unifsRhs = SelectiveUnifyImplies okToUnifyFunc x2 a2 dir unifsLhs

               return Some(unifsRhs)

             }

 

@@ -213,9 +93,11 @@ let rec UnifyImplies lhs rhs dir unifs =
             | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when DoesImplyOp opC opT ->

                 __TryUnifyPair lhsC lhsT rhsC rhsT unifs

             | UnaryExpr(opC, subC), UnaryExpr(opP, subP) when opC = opP ->

-                UnifyImplies subP subC dir unifs 

+                SelectiveUnifyImplies okToUnifyFunc subP subC dir unifs 

             | SelectExpr(lstC, idxC), SelectExpr(lstP, idxP) ->

                 __TryUnifyPair lstP lstC idxP idxC unifs

+            | Dot(exprC, fldNameC), Dot(exprP, fldNameP) when fldNameC = fldNameP ->

+                SelectiveUnifyImplies okToUnifyFunc exprP exprC dir unifs

             | _ -> None                     

 

           let rec ___f1 targetLst candidateLst unifs = 

@@ -246,4 +128,125 @@ let rec UnifyImplies lhs rhs dir unifs =
           ___f1 rhsConjs lhsConjs unifs

     with

     | CannotUnify

-    | KeyAlreadyExists -> None
\ No newline at end of file
+    | KeyAlreadyExists -> None

+

+let UnifyImplies lhs rhs dir unifs = SelectiveUnifyImplies (fun e -> true) lhs rhs dir unifs

+

+////////////////////////////////////////////

+

+let rec ComputeClosure heapInst premises = 

+  let bogusExpr = VarLiteral("!@#$%^&*()")

+

+  let ApplyUnifs unifs expr =

+    Rewrite (function 

+               | VarLiteral(id) when unifs |> Map.containsKey id -> 

+                   Some(unifs |> Map.find id)

+               | _ -> None                 

+            ) expr    

+

+  let FindMatches expr except premises = 

+    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 MySetAdd expr set =

+    let x = Printer.PrintExpr 0 expr

+    if x.Contains("$") then

+      set

+    else 

+      match expr with

+      | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && Set.contains (BinaryExpr(p,op,rhs,lhs)) set -> set

+      | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && rhs = lhs -> set

+      | _ -> Set.add expr set

+

+  let SelectExprCombinerFunc lst idx = 

+    // distribute the indexing operation if possible

+    let rec __fff lst idx = 

+      let selExpr = SelectExpr(lst, idx)

+      match lst with

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

+          let idxVal = EvalFull heapInst idx |> Expr2Int

+          let lhsVal = EvalFull heapInst lhs |> Expr2List

+          let rhsVal = EvalFull heapInst rhs |> Expr2List

+          if idxVal < List.length lhsVal then

+            __fff lhs idx

+          else 

+            __fff rhs (BinarySub idx (IntLiteral(List.length lhsVal)))

+      | SequenceExpr(elist) -> 

+          let idxVal = EvalFull heapInst idx |> Expr2Int

+          [elist.[idxVal]]

+      | _ -> [selExpr] 

+    __fff lst idx   

+

+  let SeqLenCombinerFunc lst =

+    // distribute the SeqLength operation if possible 

+    let rec __fff lst = 

+      let lenExpr = SeqLength(lst)

+      match lst with

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

+          BinaryAdd (__fff lhs) (__fff rhs)          

+      | SequenceExpr(elist) -> 

+          IntLiteral(List.length elist)

+      | _ -> lenExpr

+    [__fff lst]

+

+  let rec __CombineAllMatches expr premises =

+    match expr with

+    | BinaryExpr(p,op,lhs,rhs) -> 

+        let lhsMatches = __CombineAllMatches lhs premises

+        let rhsMatches = __CombineAllMatches rhs premises

+        Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches

+    | UnaryExpr(op,sub) -> 

+        __CombineAllMatches sub premises |> List.map (fun e -> UnaryExpr(op,e))

+    | SelectExpr(lst,idx) ->

+        let lst1 = FindMatches expr bogusExpr premises 

+        let lstMatches = __CombineAllMatches lst premises

+        let idxMatches = __CombineAllMatches idx premises

+        let lst2 = Utils.ListCombineMult SelectExprCombinerFunc lstMatches idxMatches

+        lst1 @ lst2

+    | SeqLength(lst) -> 

+        let lst1 = FindMatches expr bogusExpr premises 

+        let lst2 = __CombineAllMatches lst premises |> List.map SeqLenCombinerFunc |> List.concat

+        lst1 @ lst2

+    // TODO: other cases

+    | _ -> expr :: (FindMatches expr bogusExpr premises)

+

+  let rec __ExpandPremise expr premises = 

+    let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd e acc) premises

+    let allMatches = lazy(__CombineAllMatches expr premises)

+    match expr with

+    | BinaryExpr(p,op,lhs,rhs) when IsRelationalOp op ->

+        let x = allMatches.Force()

+        __AddToPremisses x premises

+    | SelectExpr(lst, idx) ->

+        let x = allMatches.Force()

+        __AddToPremisses x premises

+    | _ -> premises  

+

+  let rec __Iter exprLst premises = 

+    match exprLst with

+    | expr :: rest ->  

+        let newPremises = __ExpandPremise expr premises

+        __Iter rest newPremises

+    | [] -> premises

+

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

+  let premises' = __Iter (premises |> Set.toList) premises

+  if premises' = premises then

+    premises'

+  else 

+    ComputeClosure heapInst premises' 

+

+

diff --git a/Jennisys/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index 0ac1ecf6..62800dcd 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/Jennisys/MethodUnifier.fs
@@ -9,7 +9,9 @@ open Utils
 

 let TryUnify targetMthd candMethod = 

   let targetPre,targetPost = GetMethodPrePost targetMthd

+  let targetPre = BinaryAnd targetPre (GetMethodGhostPrecondition targetMthd)

   let candPre,candPost = GetMethodPrePost candMethod

+  let candPre = BinaryAnd candPre (GetMethodGhostPrecondition candMethod)

   let builder = new CascadingBuilder<_>(None)

   builder {

     let! unifs1 = UnifyImplies targetPre candPre RTL Map.empty

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index 7de4c27d..a3c9d10d 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -55,6 +55,8 @@ let rec PrintExpr ctx expr =
       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

   | MethodCall(rcv,_,name,aparams) ->

       sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

+  | MethodOutSelect(mth,name)      ->

+      sprintf "%s[\"%s\"]" (PrintExpr 0 mth) name

 

 let rec PrintConst cst = 

   match cst with 

diff --git a/Jennisys/TypeChecker.fs b/Jennisys/TypeChecker.fs
index bc696f43..cb89183f 100644
--- a/Jennisys/TypeChecker.fs
+++ b/Jennisys/TypeChecker.fs
@@ -39,8 +39,13 @@ let TypeCheck prog =
       let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))

       Some(Program(clist))

 

+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

+

 // TODO: implement this

-let rec InferType prog thisComp expr = 

+let rec InferType prog thisComp checkLocalFunc expr = 

   let __FindVar comp fldName = 

     let var = FindVar comp fldName |> Utils.ExtractOption

     match var with

@@ -52,10 +57,11 @@ let rec InferType prog thisComp expr =
     | ObjLiteral("this") -> Some(thisComp)

     | ObjLiteral("null") -> None

     | IdLiteral(id) -> __FindVar thisComp id

+    | VarLiteral(id) -> checkLocalFunc id

     | Dot(discr, fldName) -> 

-        match InferType prog thisComp discr with

+        match InferType prog thisComp checkLocalFunc discr with

         | Some(comp) -> __FindVar comp fldName

-        | None -> None

+        | None -> None                        

     | _ -> None

   with 

   | ex -> None
\ No newline at end of file
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index fe79c671..8e3096d9 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -42,6 +42,9 @@ class Node[T] {
     ensures |list| = 1 ==> tail = null
     ensures |list| > 1 ==> tail != null && tail.list = list[1..]
 
+  method Size() returns (size: int)
+    ensures size = |list|
+
   method SkipFew(num: int) returns (ret: Node[T])
     requires num >= 0
     ensures num >= |list| ==> ret = null
@@ -49,7 +52,6 @@ class Node[T] {
 
   method Get(idx: int) returns (ret: T)
     requires idx >= 0 && idx < |list|
-    requires idx >= 1 && next != null
     ensures ret = list[idx]
 }