Jennisys:

  - changed the way candidate conditions are discovered; now it simply uses
    all sub-expressions found in the spec that evaluate to TrueLiteral
  - changed the implementation so that when trying to infer a precondition,
    try out several different possibilities (and see which one works)
  - added some very basic (and incomplete) type inference
  - fixed a bug in the Modularizer (it didn't fix the solution after trying
    out the spec infered from the solution)
  - fixed a bug in DafnyModelUtils so that now when reading from the boogie
    model file it keeps getting information from Seq# functions until
    reaching a fixpoint (that's needed because the order or reads is important)

11 files changed, 324 insertions, 176 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 512a6870..7c8c472d 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -8,6 +8,7 @@ open MethodUnifier
 open Modularizer

 open PipelineUtils

 open Options

+open TypeChecker

 open Resolver

 open PrintUtils

 open DafnyPrinter

@@ -76,8 +77,9 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
   | [] -> ""     

 

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

-/// For a given constant "o" (which is an object, something like "gensym32"), 

-/// finds a path of field references from "this". 

+/// For a given constant "objRefName" (which is an object, something like 

+/// "gensym32"), finds a path of field references from "this" (e.g. something

+/// like "this.next.next"). 

 ///

 /// Implements a backtracking search over the heap entries to find that

 /// path.  It starts from the given object, and follows the backpointers

@@ -140,7 +142,7 @@ let GetHeapExpr prog mthd heapInst =
                           objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

                       ) prepostExpr

 

-let IsUnmodConcrOnly (comp,meth) expr = 

+let IsUnmodConcrOnly prog (comp,meth) expr = 

   let isConstr = IsConstructor meth

   let rec __IsUnmodOnly args expr = 

     let __IsUnmodOnlyLst elist = 

@@ -155,13 +157,14 @@ let IsUnmodConcrOnly (comp,meth) expr =
     | VarLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

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

     | IdLiteral(id)                         -> 

-        let isAbstractFld = GetAbstractFields comp |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

-        not (isConstr || isAbstractFld)

-    | Dot(e, fldName)                       -> if isConstr then false else __IsUnmodOnlyLst [e] 

-        // TODO: this is how it should really work

-        // let lhsType = InferType prog e

-        // let isMod = IsFieldModifiable lhsType fldName

-        // (not isMod) && __IsUnmodOnlyLst [e]

+        not (isConstr || IsAbstractField comp id)

+    | Dot(e, fldName)                       -> //if isConstr then false else __IsUnmodOnlyLst [e] 

+        if isConstr then

+          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))

+          IsConcreteField lhsType fldName          

     | AssertExpr(e)

     | AssumeExpr(e)

     | SeqLength(e)

@@ -187,7 +190,7 @@ let AddUnif indent e v unifMap =
   }

 

 //TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"

-let rec GetUnifications indent (comp,meth) heapInst unifs expr =

+let rec GetUnifications prog indent (comp,meth) heapInst unifs expr =

   let idt = Indent indent

   // - first looks if the give expression talks only about method arguments (args)

   // - then it tries to evaluate it to a constant

@@ -198,7 +201,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr =
     else      

       let builder = new CascadingBuilder<_>(unifsAcc)

       builder {

-        let! argsOnly = IsUnmodConcrOnly (comp,meth) e |> Utils.BoolToOption

+        let! argsOnly = IsUnmodConcrOnly prog (comp,meth) e |> Utils.BoolToOption

         let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None

         return AddUnif indent e v unifsAcc

       }

@@ -209,7 +212,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr =
 /// Returns a map (Expr |--> Const) containing unifications

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

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

-let GetUnificationsForMethod indent comp m heapInst =

+let GetUnificationsForMethod indent prog comp m heapInst =

   let idt = Indent indent

   let rec GetArgValueUnifications args = 

     match args with

@@ -219,26 +222,34 @@ let GetUnificationsForMethod indent comp m heapInst =
             GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c

         | None -> failwith ("couldn't find value for argument " + name)

     | [] -> Map.empty

-  let rec GetFldValueUnifications fldNames unifs = 

-    match fldNames with

-    | fldName :: rest -> 

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

-                                             match asgn with 

-                                             | FieldAssignment((obj,Var(vname,_)), fldVal) when obj.name = "this" && vname = fldName -> 

-                                                 try 

-                                                   let c = Expr2Const fldVal

-                                                   AddUnif indent (IdLiteral(fldName)) c acc

-                                                 with

-                                                 | _ -> acc

-                                             | _ -> acc

-                                          ) unifs

-                             |> GetFldValueUnifications rest 

-    | [] -> unifs

+  let rec GetFldValueUnifications unifs = 

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

+                                         match asgn with 

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

+                                             try 

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

+                                               if IsConcreteField comp vname then

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

+                                                 let c = Expr2Const fldVal

+                                                 AddUnif indent (Dot(path, vname)) c acc

+                                               else

+                                                 acc

+                                             with

+                                             | ex -> 

+                                                 Logger.WarnLine ("[WARN]: error during getting field value unifications: " + ex.Message)

+                                                 acc

+                                         | _ -> acc

+                                      ) unifs

+

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

   let unifs = GetArgValueUnifications (GetMethodInArgs m)

-  let fldNames = if IsConstructor m then [] else GetConcreteFields comp |> List.map (function Var(name,_) -> name)

-  let unifs2 = GetFldValueUnifications fldNames unifs

-  GetUnifications indent (comp,m) heapInst unifs2 (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x))

+  let unifs = 

+    //TODO: it should really read the "modifies" clause and figure out modifiable fields from there

+    if not (IsConstructor m) then 

+      GetFldValueUnifications unifs

+    else

+      unifs

+  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

@@ -310,7 +321,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
       let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative

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

                                                         match asgn with

-                                                        | FieldAssignment((o,f),value) ->

+                                                        | FieldAssignment((o,f),value) when heapInst.modifiableObjs |> Set.contains o ->

                                                             let e2 = __Apply (o,f) c e value

                                                             acc @ [FieldAssignment((o,f),e2)] 

                                                         | _ -> acc @ [asgn]

@@ -343,25 +354,57 @@ let rec DiscoverAliasing exprList heapInst =
       BinaryAnd eqExpr (DiscoverAliasing rest heapInst)

   | [] -> TrueLiteral

 

-// use the orginal method, not the one with an extra precondition

-let FixSolution origComp origMeth sol =

-  sol |> Map.fold (fun acc (cc,mm) v -> 

-                      if CheckSameMethods (cc,mm) (origComp,origMeth) then

-                        acc |> Map.add (origComp,origMeth) v

-                      else 

-                        acc |> Map.add (cc,mm) v) Map.empty

-

 //

 let DontResolveUnmodifiableStuff prog comp meth expr =

   let methodArgs = GetMethodInArgs meth

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

-  let isConstr = match meth with Method(_,_,_,_,b) -> b | _ -> false

+  let isConstr = IsConstructor meth

   match expr with

   | VarLiteral(id) when __IsMethodArg id -> false 

-  | IdLiteral(id) when not (id = "this" || id = "null") -> isConstr

-  | Dot(lhs, fldName) -> isConstr

+  | IdLiteral(id) when id = "this" || id = "null" -> true

+  | IdLiteral(id) | Dot(_, id) -> 

+      // this must be a field, so resolve it only if constructor

+      isConstr

   | _ -> true

 

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

+let FindTrueClauses prog comp m heapInst expr = 

+  let MyFun expr acc =

+    try 

+      let exprEval = Eval heapInst (DontResolveUnmodifiableStuff prog comp m) expr

+      if exprEval = TrueLiteral then

+        acc

+      else

+        let exprAllResolved = Eval heapInst (fun _ -> true) 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

+let GetAllPossibleConditions specConds argConds aliasingConds = 

+  let __Conjoin lst = lst |> List.fold (fun acc e -> BinaryAnd acc e) TrueLiteral

+  let __Preproc lst = lst |> List.map SplitIntoConjunts |> List.concat |> Utils.ListDeduplicate

+

+  // 0. aliasing conditions

+  // 1. conjunction of spec conditions

+  // 2. individual arg conditions

+  // 3. conjunction of arg conditions

+  // 4. individual spec conditions

+  let aliasing = aliasingConds |> __Preproc

+  let specIndi = specConds |> __Preproc

+  let specConj = [__Conjoin specIndi]

+  let argsIndi = argConds |> __Preproc

+  let argsConj = [__Conjoin argsIndi]

+  

+  let allConds = aliasing @ specConj @ argsIndi @ specIndi @ argsConj

+  allConds |> List.filter (fun e -> not (e = TrueLiteral)) 

+           |> Utils.ListDeduplicate

+

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

 /// Attempts to synthesize the initialization code for the given constructor "m"

 ///

@@ -394,7 +437,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
         let model = models.[0]

         let hModel = ReadFieldValuesFromModel model prog comp m

         let heapInst = ResolveModel hModel m

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

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

         let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

         // split into method calls

@@ -415,99 +458,137 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
             else

               sol      

         else

-          sol

+          sol             

 and TryInferConditionals indent prog comp m unifs heapInst callGraph = 

+  let rec __TryOutConditions candidateConditions =

+    let idt = Indent indent

+    match candidateConditions with 

+    | [] ->

+        Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+        None

+    | candCond :: rest ->

+        Logger.InfoLine (sprintf "%s    ________________________" idt)

+        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 sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph

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

+        let verified = 

+          if Options.CONFIG.verifyPartialSolutions then

+            VerifySolution prog sol Options.CONFIG.genRepr

+          else 

+            true

+        if verified then

+          if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+          Some(candCond,m2,sol)

+        else 

+          Logger.InfoLine "NOT VERIFIED"

+          __TryOutConditions rest

+

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

   let idt = Indent indent

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

   let methodArgs = GetMethodInArgs m

-  let expr = GetHeapExpr prog m heapInst2

-  // now evaluate and see what's left

-  //printfn "%s" (expr |> SplitIntoConjunts |> PrintSep (newline + newline) (fun e -> PrintExpr 0 e))

   

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

-  let newConds = expr |> SplitIntoConjunts 

-                      |> List.fold (fun acc e -> 

-                                      Logger.TraceLine (idt + ">>> " + (PrintExpr 0 e))

-                                      let v = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) e

-                                      Logger.TraceLine (sprintf "%s    --> %s" idt (PrintExpr 0 v))

-                                      if v = TrueLiteral then

-                                        acc

-                                      elif v = FalseLiteral && (not aliasingCond.IsValueCreated) then

-                                        let aliasingExpr = aliasingCond.Force()

-                                        if aliasingExpr = TrueLiteral then

-                                          failwith ("post-condition evaluated to false and no aliasing was discovered")

-                                        acc @ [aliasingExpr]

-                                      else

-                                        acc @ [v]

-                                   ) []

-                      |> List.filter (IsUnmodConcrOnly (comp,m))

-  let newConds = 

-    if newConds = [] && IsSolution1stLevelOnly heapInst2 then

-      heapInst2.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) []

-    else 

-      newConds                        

-  

-  // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

-  match newConds with 

-  | [] ->

-      Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

-      wrongSol

-  | _ ->

-      //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO

-      let candCond = newConds |> List.fold BinaryAnd TrueLiteral

-      Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

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

-      let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph

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

-      let verified = 

-        if Options.CONFIG.verifyPartialSolutions then

-          VerifySolution prog sol Options.CONFIG.genRepr

-        else 

-          true

-      if verified then

-        if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+  // find candidate conditions

+  let expr = GetHeapExpr prog m heapInst2

+  let specConds = expr |> FindTrueClauses prog comp m heapInst2

+  let specConds = specConds 

+                       |> List.filter (IsUnmodConcrOnly prog (comp,m))

+

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

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

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

+    

+  // --- trace

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

+  allConds |> List.iter loggerFunc

+  // ---

+                      

+  if IsSolution1stLevelOnly heapInst2 then

+    // try to find a non-recursive solution

+    match __TryOutConditions allConds with

+    | Some(candCond,m2,sol) ->

         let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

                       | Some(sol2) -> sol2

                       | None -> sol   

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

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

         MergeSolutions solThis solRest |> FixSolution comp m

-      else 

-        Logger.InfoLine "NOT VERIFIED"

-        wrongSol  

-      

-let GetMethodsToAnalyze prog =

-  let mOpt = Options.CONFIG.methodToSynth;

-  if mOpt = "*" then

-    (* all *)

-    FilterMembers prog FilterMethodMembers // FilterConstructorMembers

-  elif mOpt = "paramsOnly" then

-    (* only with parameters *)

-    FilterMembers prog FilterConstructorMembersWithParams 

+    | None -> 

+        Logger.InfoLine (idt + "!!! Giving up !!!")

+        wrongSol

+

+    // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

+//    match newConds with 

+//    | [] ->

+//        Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+//        wrongSol

+//    | _ ->

+//        //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO

+//        let candCond = newConds |> List.fold BinaryAnd TrueLiteral    //TODO: do some search or something

+//        Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

+//        let _,_,m2 = AddPrecondition prog comp m candCond

+//        let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph

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

+//        let verified = 

+//          if Options.CONFIG.verifyPartialSolutions then

+//            VerifySolution prog sol Options.CONFIG.genRepr

+//          else 

+//            true

+//        if verified then

+//          if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+//          let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

+//                        | Some(sol2) -> sol2

+//                        | None -> sol   

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

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

+//          MergeSolutions solThis solRest |> FixSolution comp m

+//        else 

+//          Logger.InfoLine "NOT VERIFIED"

+//          wrongSol  

   else

-    let allMethods,neg = 

-      if mOpt.StartsWith("~") then

-        mOpt.Substring(1), true

-      else

-        mOpt, false

-    (* exact list *)

-    let methods = allMethods.Split([|','|])

-    let lst = methods |> Array.fold (fun acc m -> 

-                                       let idx = m.LastIndexOf(".")

-                                       if idx = -1 || idx = m.Length - 1 then

-                                         raise (InvalidCmdLineArg("Invalid method full name: " + m))

-                                       let compName = m.Substring(0, idx)

-                                       let methName = m.Substring(idx + 1)

-                                       let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)

-                                       let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)

-                                       (c,mthd) :: acc

-                                    ) []

-    if neg then

-      FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst))

+    // the solution is not immediate, so try to delegate to a method call, possibly to a recursive one

+    //TODO

+    Logger.InfoLine "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"

+    wrongSol    

+

+let GetMethodsToAnalyze prog =

+  let __ReadMethodsParam = 

+    let mOpt = Options.CONFIG.methodToSynth;

+    if mOpt = "*" then

+      (* all *)

+      FilterMembers prog FilterMethodMembers

     else

-      lst

-  

+      let allMethods,neg = 

+        if mOpt.StartsWith("~") then

+          mOpt.Substring(1), true

+        else

+          mOpt, false

+      (* exact list *)

+      let methods = allMethods.Split([|','|])

+      let lst = methods |> Array.fold (fun acc m -> 

+                                         let idx = m.LastIndexOf(".")

+                                         if idx = -1 || idx = m.Length - 1 then

+                                           raise (InvalidCmdLineArg("Invalid method full name: " + m))

+                                         let compName = m.Substring(0, idx)

+                                         let methName = m.Substring(idx + 1)

+                                         let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)

+                                         let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)

+                                         (c,mthd) :: acc

+                                      ) []

+      if neg then

+        FilterMembers prog FilterMethodMembers |> List.filter (fun e -> not (Utils.ListContains e lst))

+      else

+        lst

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

+  let meths = __ReadMethodsParam

+  if Options.CONFIG.constructorsOnly then

+    meths |> List.filter (fun (c,m) -> IsConstructor m)

+  else 

+    meths

 

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

 /// Goes through a given list of methods of the given program and attempts to 

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index f5d90489..b4ed22e6 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -147,8 +147,11 @@ let rec DescendExpr2 visitorFunc expr acc =
   | SequenceExpr(exs)                

   | SetExpr(exs)                     -> __Pipe exs

 

-let PrintGenSym name =

-  sprintf "gensym%s" name

+let PrintGenSym (name: string) =

+  if name.StartsWith("gensym") then

+    name

+  else

+    sprintf "gensym%s" name

 

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

 /// Returns TRUE literal

@@ -267,9 +270,10 @@ let rec Expr2Const e =
   match e with

   | IntLiteral(n) -> IntConst(n)

   | BoolLiteral(b) -> BoolConst(b)

+  | BoxLiteral(id) -> BoxConst(id)

   | ObjLiteral("this") -> ThisConst("this",None)

   | ObjLiteral("null") -> NullConst

-  | ObjLiteral(name) -> Unresolved(name)

+  | ObjLiteral(name) -> NewObj(name, None)

   | IdLiteral(id) -> Unresolved(id)

   | VarLiteral(id) -> VarConst(id)

   | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)

@@ -359,6 +363,9 @@ let rec GroupFieldsByType fields =
       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

@@ -476,6 +483,9 @@ let FindComponent (prog: Program) clsName =
   | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)

                             |> Utils.ListToOption

 

+let FindComponentForType prog ty = 

+  FindComponent prog (GetTypeShortName ty)

+

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

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

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

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 714c44f1..10398fa9 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -160,7 +160,7 @@ let PrintAllocNewObjects heapInst indent =
 

 let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

-  let stmts = ConvertToStatements heapInst

+  let stmts = ConvertToStatements heapInst true

   let str = stmts |> PrintSep (newline) (fun s -> idt + (PrintStmt s 0 false))

   str + newline

 

diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index ffd30fc7..6a8cb727 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -244,14 +244,24 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
         __ReadSeqAppend model rest (newEnv,newCtx)

     | _ -> (envMap,ctx)  

 

+  // keeps reading from Seq#Build and Seq#Append until fixpoint

+  let rec __ReadUntilFixpoint hmodel = 

+    let f_seq_bld = model.MkFunc("Seq#Build", 2)

+    let f_seq_app = model.MkFunc("Seq#Append", 2)

+    let hmodel' = hmodel |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

+                       |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)               

+    if hmodel' = hmodel then

+      hmodel'

+    else

+      __ReadUntilFixpoint hmodel'

+

   let f_seq_len = model.MkFunc("Seq#Length", 1)

   let f_seq_idx = model.MkFunc("Seq#Index", 2)

-  let f_seq_bld = model.MkFunc("Seq#Build", 2)

-  let f_seq_app = model.MkFunc("Seq#Append", 2)

-  (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

-               |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

-               |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

-               |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)

+  let hmodel = (envMap,ctx)

+  let hmodel' = hmodel |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

+                       |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

+  __ReadUntilFixpoint hmodel'  

+  

 

 

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

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index beac24f8..2613432c 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

-    <StartArguments>examples/List.jen /genMod /genRepr /method:Node.Get</StartArguments>

+    <StartArguments>examples/NumberMethods.jen /genMod /genRepr /method:NumberMethods.Min4</StartArguments>

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

   </PropertyGroup>

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

diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs
index 3215786d..c6fcaaec 100644
--- a/Jennisys/Jennisys/Modularizer.fs
+++ b/Jennisys/Jennisys/Modularizer.fs
@@ -184,7 +184,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
                 | Method (mname, msig, mpre, _, isConstr) -> Method(mname, msig, mpre, postSpec, isConstr)

                 | _ -> failwithf "internal error: expected a Method but got %O" meth

     match TryFindExistingAndConvertToSolution indent comp meth' cond callGraph with

-    | Some(sol) -> sol

+    | Some(sol) -> sol |> FixSolution comp meth

     | None -> 

         // if not found, try to split into parts

         let newMthdLst, newHeapInst = __GetModularBranch

diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs
index b61c16da..7aeb131a 100644
--- a/Jennisys/Jennisys/Options.fs
+++ b/Jennisys/Jennisys/Options.fs
@@ -9,18 +9,19 @@ module Options
 open Utils

 

 type Config = {

-   help: bool;

-   inputFilename: string;

-   methodToSynth: string;

-   inferConditionals: bool;

-   verifyPartialSolutions: bool;

-   verifySolutions: bool;

-   checkUnifications: bool;

-   genRepr: bool;

-   genMod: bool;

-   timeout: int;

-   numLoopUnrolls: int;

-   recursiveValid: bool;

+   help                      : bool;

+   inputFilename             : string;

+   methodToSynth             : string;

+   constructorsOnly          : bool;

+   inferConditionals         : bool;

+   verifyPartialSolutions    : bool;

+   verifySolutions           : bool;

+   checkUnifications         : bool;

+   genRepr                   : bool;

+   genMod                    : bool;

+   timeout                   : int;

+   numLoopUnrolls            : int;

+   recursiveValid            : bool;

 }

 

 type CfgOption<'a> = {

@@ -54,6 +55,7 @@ let CheckBool value optName =
 let cfgOptions = [

   { optionName = "help";            optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with help                   =      CheckBool v "help"});           descr = "description not available"; }

   { optionName = "method";          optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth          = CheckNonEmpty v "method"});          descr = "description not available"; }

+  { optionName = "constrOnly";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly       =      CheckBool v "constrOnly"});     descr = "description not available"; }

   { optionName = "inferConds";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      =      CheckBool v "inferConds"});     descr = "description not available"; }

   { optionName = "noInferConds";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      = not (CheckBool v "inferConds")});    descr = "description not available"; }

   { optionName = "verifyParSol";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions =      CheckBool v "verifyParSol"});   descr = "description not available"; }

@@ -98,6 +100,7 @@ let defaultConfig: Config = {
   inputFilename     = "";

   inferConditionals = true;

   methodToSynth     = "*";

+  constructorsOnly  = false;

   verifyPartialSolutions = true;

   verifySolutions   = true;

   checkUnifications = false;

diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
index bb546834..711298f9 100644
--- a/Jennisys/Jennisys/Resolver.fs
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -31,20 +31,29 @@ type HeapInstance = {
 

 let NoObj = { name = ""; objType = NamedType("", []) }

 

-let ConvertToStatements heapInst = 

-  let stmtLst1 = heapInst.assignments |> List.map (fun asgn ->                                                        

-                                                     match asgn with

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

-                                                         let fldName = GetVarName f

-                                                         if fldName = "" then

-                                                           ExprStmt(e)

-                                                          else

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

-                                                      | ArbitraryStatement(stmt) -> stmt)

+// use the orginal method, not the one with an extra precondition

+let FixSolution origComp origMeth sol =

+  sol |> Map.fold (fun acc (cc,mm) v -> 

+                      if CheckSameMethods (cc,mm) (origComp,origMeth) then

+                        acc |> Map.add (origComp,origMeth) v

+                      else 

+                        acc |> Map.add (cc,mm) v) Map.empty

+

+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))

+                                                            else

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

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

+                                                        | _ -> None)

   let stmtLst2 = heapInst.methodRetVals |> Map.toList

                                         |> List.map (fun (retVarName, retVarVal) -> Assign(VarLiteral(retVarName), retVarVal))

   stmtLst1 @ stmtLst2

-

+                            

 // resolving values

 exception ConstResolveFailed of string

  

@@ -73,11 +82,12 @@ let rec ResolveCont hModel failResolver cst =
               | Some(c) -> c

               | _ -> failResolver cst hModel

           | None ->

-              // finally, see if it's a method argument

-              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList

-              match m with 

-              | (vc,_) :: [] -> vc

-              | _ -> failResolver cst hModel

+              failResolver cst hModel

+//              // finally, see if it's an *input* (have no way of telling input from output params here) method argument

+//              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList

+//              match m with 

+//              | (vc,_) :: [] -> vc

+//              | _ -> failResolver cst hModel

   | SeqConst(cseq) -> 

       let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) []

       SeqConst(resolvedLst)

@@ -127,10 +137,12 @@ let Eval heapInst resolveExprFunc expr =
           | _ -> expr

       | _ -> expr

 

-    if not (resolveExprFunc expr) then

-      match fldNameOpt with

-      | None -> expr

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

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

+    let ex = match fldNameOpt with

+             | None -> expr

+             | Some(n) -> Dot(expr, n)

+    if not (resolveExprFunc ex) then

+      ex

     else

       match fldNameOpt with

       | None -> 

@@ -142,7 +154,7 @@ let Eval heapInst resolveExprFunc expr =
               | Some(argValue) -> argValue |> Const2Expr

               | None -> 

                   match heapInst.methodRetVals |> Map.tryFind id with

-                  | Some(e) -> e

+                  | Some(e) -> e |> __FurtherResolve

                   | None -> raise (EvalFailed("cannot find value for method parameter " + id))              

           | IdLiteral(id) ->

               let globalVal = heapInst.globals |> Map.tryFind id

@@ -160,6 +172,7 @@ let Eval heapInst resolveExprFunc expr =
               | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName))

               | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???

           | _ -> Dot(expr, fldName)

+

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

   //EvalSym  (__EvalResolver resolveExprFunc) expr

   EvalSymRet  (__EvalResolver false resolveExprFunc)

@@ -209,10 +222,11 @@ let ResolveModel hModel meth =
   let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> 

                                                   match k with

                                                   | VarConst(name) -> 

+                                                      let resolvedValExpr = Resolve hModel v

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

-                                                        acc1, acc2 |> Map.add name (Resolve hModel v |> Const2Expr)

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

                                                       else

-                                                        acc1 |> Map.add name (Resolve hModel v), acc2

+                                                        acc1 |> Map.add name resolvedValExpr, acc2

                                                   | _ -> acc1, acc2

                                                ) (Map.empty, Map.empty)

   { objs           = objs;

@@ -259,7 +273,7 @@ let Is1stLevelExpr heapInst expr =
                     | Dot(discr, fldName) -> 

                         let obj = Eval heapInst (fun _ -> true) discr

                         match obj with 

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

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

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

                     | _ -> true                          

                ) expr true

@@ -276,4 +290,4 @@ let IsSolution1stLevelOnly heapInst =
         | Block(stmts) -> __IsSol1stLevel (stmts @ rest)

     | [] -> true

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

-  __IsSol1stLevel (ConvertToStatements heapInst)
\ No newline at end of file
+  __IsSol1stLevel (ConvertToStatements heapInst true)
\ No newline at end of file
diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs
index 8227b693..bc696f43 100644
--- a/Jennisys/Jennisys/TypeChecker.fs
+++ b/Jennisys/Jennisys/TypeChecker.fs
@@ -1,6 +1,7 @@
 module TypeChecker

 

 open Ast

+open AstUtils

 open Printer

 open System.Collections.Generic

 

@@ -39,5 +40,22 @@ let TypeCheck prog =
       Some(Program(clist))

 

 // TODO: implement this

-let InferType prog expr = 

-  NamedType("unknown", [])
\ No newline at end of file
+let rec InferType prog thisComp 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)

+  try 

+    match expr with

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

+    | ObjLiteral("null") -> None

+    | IdLiteral(id) -> __FindVar thisComp id

+    | Dot(discr, fldName) -> 

+        match InferType prog thisComp discr with

+        | Some(comp) -> __FindVar comp fldName

+        | None -> None

+    | _ -> None

+  with 

+  | ex -> None
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 156d427c..5cd8af9d 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -74,6 +74,19 @@ let ListToOptionMsg  lst errMsg =
 

 let ListToOption lst = ListToOptionMsg lst "given list contains more than one element"

 

+let ListDeduplicate lst = 

+  let rec __Dedup lst (visitedSet: System.Collections.Generic.HashSet<_>) acc = 

+    match lst with

+    | fs :: rest ->  

+        let newAcc = 

+          if visitedSet.Add(fs) then

+            acc @ [fs]

+          else

+            acc

+        __Dedup rest visitedSet newAcc

+    | _ -> acc

+  __Dedup lst (new System.Collections.Generic.HashSet<_>()) []

+        

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

 /// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])

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

diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index 7fa04fc4..e056bcfa 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -49,7 +49,6 @@ class Node[T] {
 
   method Get(idx: int) returns (ret: T)
     requires idx >= 0 && idx < |list|
-    requires idx != 0 && next != null
     ensures ret = list[idx]
 }
 
@@ -61,6 +60,6 @@ model Node[T] {
     next
 
   invariant
-    next = null <==> list = [data]
+    next = null ==> list = [data]
     next != null ==> list = [data] + next.list 
 }