- removed "exit 43" from StartDafny-jen.bat

 - some very small changes

4 files changed, 44 insertions, 32 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 7bee9194..c02e290e 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -153,6 +153,7 @@ let GetUnificationsForMethod comp m (heap,env,ctx) =
 /// path.  It starts from the given object, and follows the backpointers

 /// until it reaches the root ("this")

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

+let objRef2ExprCache = new System.Collections.Generic.Dictionary<Const, Expr>()

 let GetObjRefExpr o (heap,env,ctx) = 

   let rec __GetObjRefExpr o (heap,env,ctx) visited = 

     if Set.contains o visited then 

@@ -173,7 +174,14 @@ let GetObjRefExpr o (heap,env,ctx) =
           let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList

           __fff backPointers 

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

-  __GetObjRefExpr o (heap,env,ctx) (Set.empty)

+  if objRef2ExprCache.ContainsKey(o) then

+    Some(objRef2ExprCache.[o])

+  else

+      let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)

+      match res with 

+      | Some(e) -> objRef2ExprCache.Add(o, e)

+      | None -> ()

+      res

 

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

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

@@ -253,6 +261,10 @@ let VerifySolution prog comp mthd (heap,env,ctx) =
 

 let TryInferConditionals prog comp m unifs (heap,env,ctx) = 

   let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false

+  // get expressions to evaluate:

+  //   - go through all objects on the heap and assert its invariant

+  //   - add pre and post conditions

+

   Some(heap2,env2,ctx2)

    

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

@@ -289,9 +301,38 @@ let AnalyzeConstructor prog comp m =
         Some(heap,env,ctx)

       else 

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

+        Logger.InfoLine "Trying to infer conditionals"

         TryInferConditionals prog comp m unifs (heap,env,ctx)

     else

       Some(heap,env,ctx)

+

+let GetMethodsToAnalyze prog =

+  let mOpt = Options.CONFIG.methodToSynth;

+  if mOpt = "*" then

+    (* all *)

+    FilterMembers prog FilterConstructorMembers   

+  elif mOpt = "paramsOnly" then

+    (* only with parameters *)

+    FilterMembers prog FilterConstructorMembersWithParams 

+  else

+    let allMethods,neg = 

+      if mOpt.StartsWith("~") then

+        mOpt.Substring(1), true

+      else

+        mOpt, false

+    (* exactly one *)

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

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

+                                       let compName = m.Substring(0, m.LastIndexOf("."))

+                                       let methName = m.Substring(m.LastIndexOf(".") + 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))

+    else

+      lst

   

 

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

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index a0d53d0c..4f8b4099 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -330,7 +330,7 @@ let GetInvariantsAsList comp =
   | Component(Class(_,_,members), Model(_,_,_,_,inv), _) -> 

       let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat

       List.append (SplitIntoConjunts inv) clsInvs

-  | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())

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

 

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

 /// Returns variable name

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 1a2d207a..c13b94d2 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -97,7 +97,7 @@ let PrintAllocNewObjects (heap,env,ctx) indent =
       |> Set.fold (fun acc newObjConst ->

                     match newObjConst with

                     | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline)

-                    | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString())

+                    | _ -> failwithf "NewObj doesn't have a type: %O" newObjConst

                   ) ""

 

 let PrintObjRefName o (env,ctx) = 

@@ -140,34 +140,6 @@ let GenConstructorCode mthd body =
       "  }" + newline

   | _ -> ""

 

-let GetMethodsToAnalyze prog =

-  let mOpt = Options.CONFIG.methodToSynth;

-  if mOpt = "*" then

-    (* all *)

-    FilterMembers prog FilterConstructorMembers   

-  elif mOpt = "paramsOnly" then

-    (* only with parameters *)

-    FilterMembers prog FilterConstructorMembersWithParams 

-  else

-    let allMethods,neg = 

-      if mOpt.StartsWith("~") then

-        mOpt.Substring(1), true

-      else

-        mOpt, false

-    (* exactly one *)

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

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

-                                       let compName = m.Substring(0, m.LastIndexOf("."))

-                                       let methName = m.Substring(m.LastIndexOf(".") + 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))

-    else

-      lst

-

 // solutions: (comp, constructor) |--> (heap, env, ctx) 

 let PrintImplCode prog solutions methodsToPrintFunc =

   let methods = methodsToPrintFunc prog

diff --git a/Jennisys/scripts/StartDafny-jen.bat b/Jennisys/scripts/StartDafny-jen.bat
index 79d39a38..6f44ec4c 100644
--- a/Jennisys/scripts/StartDafny-jen.bat
+++ b/Jennisys/scripts/StartDafny-jen.bat
@@ -1,3 +1,2 @@
 @echo off

 "c:/boogie/Binaries/Dafny.exe" -nologo -compile:0 /print:xxx.bpl -timeLimit:60 %* > c:\tmp\jen-doo.out

-exit 43