diff options
| -rw-r--r-- | Jennisys/Analyzer.fs | 43 | ||||
| -rw-r--r-- | Jennisys/AstUtils.fs | 2 | ||||
| -rw-r--r-- | Jennisys/CodeGen.fs | 30 | ||||
| -rw-r--r-- | Jennisys/scripts/StartDafny-jen.bat | 1 |
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
|