diff options
author | 2011-10-10 18:27:07 -0400 | |
---|---|---|
committer | 2011-10-10 18:27:07 -0400 | |
commit | 34524d3a409b64ae93d2d5672bb29e2de9988f1d (patch) | |
tree | 0a3300fbbdb14c0e2dc8e4d6b88ea1cb7b44aa82 /Jennisys | |
parent | 8e04cd792ec754798974e112dedfc7131f3aedb3 (diff) |
Jennisys: implemented minimization of inferred guards
Diffstat (limited to 'Jennisys')
-rw-r--r-- | Jennisys/Analyzer.fs | 74 | ||||
-rw-r--r-- | Jennisys/AstUtils.fs | 18 | ||||
-rw-r--r-- | Jennisys/CodeGen.fs | 4 | ||||
-rw-r--r-- | Jennisys/FixpointSolver.fs | 6 | ||||
-rw-r--r-- | Jennisys/Options.fs | 3 | ||||
-rw-r--r-- | Jennisys/Utils.fs | 11 | ||||
-rw-r--r-- | Jennisys/examples/List.jen | 3 | ||||
-rw-r--r-- | Jennisys/examples/List2.jen | 5 | ||||
-rw-r--r-- | Jennisys/examples/Set.jen | 1 | ||||
-rw-r--r-- | Jennisys/examples/Simple.jen | 8 |
10 files changed, 102 insertions, 31 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 7b60104a..eb29e4d1 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -671,7 +671,7 @@ and TryRecursion indent prog comp m unifs heapInst callGraph = Logger.InfoLine (idt + " !!! NOT VERIFIED !!!")
match TryInferConditionals indent prog comp m unifs hInst' callGraph premises with
| Some(candCond,solThis) ->
- let m' = AddPrecondition prog comp m (UnaryNot(candCond))
+ let m' = AddPrecondition m (UnaryNot(candCond))
let solRest = AnalyzeConstructor (indent + 2) prog comp m' callGraph
MergeSolutions solThis solRest |> FixSolution comp m
| None ->
@@ -683,21 +683,21 @@ and TryRecursion indent prog comp m unifs heapInst callGraph = //TODO
let expandOnlyModVarsFunc = fun e ->
-// true
- let __CheckExpr l =
- //TODO: FIX THIS!!!!!
- match l with
- | VarLiteral(vname) -> GetMethodOutArgs m |> List.exists (fun var -> GetVarName var = vname)
- | IdLiteral(_) -> true
- | Dot(_,_) -> true
- | _ -> false
- match e with
- | BinaryExpr(_,"=",l,_) ->
- //TODO: it should really check both lhs and rhs
- __CheckExpr l
- | BinaryExpr(_,op,l,_) when IsRelationalOp op ->
- __CheckExpr l
- | _ -> __CheckExpr e
+ true
+// let __CheckExpr l =
+// //TODO: FIX THIS!!!!!
+// match l with
+// | VarLiteral(vname) -> GetMethodOutArgs m |> List.exists (fun var -> GetVarName var = vname)
+// | IdLiteral(_) -> true
+// | Dot(_,_) -> true
+// | _ -> false
+// match e with
+// | BinaryExpr(_,"=",l,_) ->
+// //TODO: it should really check both lhs and rhs
+// __CheckExpr l
+// | BinaryExpr(_,op,l,_) when IsRelationalOp op ->
+// __CheckExpr l
+// | _ -> __CheckExpr e
let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]
let heapInst = ApplyUnifications indent prog comp m unifs heapInst false
@@ -733,6 +733,32 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 e))
let methodArgs = GetMethodInArgs m
+ /// Tries to minimize the guard for a given (already verified) solution
+ let rec __MinimizeGuard oldGuard guard c m sol i =
+ let guardList = SplitIntoConjunts guard
+ Logger.TraceLine (sprintf "Minimizing guard: %s [%i]" (PrintExpr 0 guard) i)
+ let ___ReplaceGuard newGuard sol =
+ let lst = sol |> Map.find (c,m)
+ let newLst = lst |> List.map (fun (g,hInst) -> if g = guard then (newGuard,hInst) else (g,hInst))
+ if newLst = lst then
+ Logger.TraceLine "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa lst aaaaaaaaaaaaaaaaaaaaaaa" else ()
+ let newMeth = SetPrecondition m (BinaryAnd oldGuard newGuard)
+ let newSol = sol |> Utils.MapReplaceKey (c,m) (c,newMeth) newLst
+ if newSol = sol then Logger.TraceLine "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa sol aaaaaaaaaaaaaaaaaaaaaaaaaa" else ()
+ newMeth,newSol
+ if i >= List.length guardList then
+ guard,m,sol
+ else
+ let newGuardList = Utils.ListRemoveNth i guardList
+ let newGuard = newGuardList |> List.fold BinaryAnd TrueLiteral
+ let m',sol' = ___ReplaceGuard newGuard sol
+ let verified = VerifySolution prog sol' Options.CONFIG.genRepr
+ if verified then
+ Logger.TraceLine (sprintf "clause %s successfully removed" (PrintExpr 0 (List.nth guardList i)))
+ __MinimizeGuard oldGuard newGuard c m' sol' 0
+ else
+ __MinimizeGuard oldGuard guard c m sol (i+1)
+
/// Iterates through a given list of boolean conditions and checks
/// which one suffices. If it finds such a condition, it returns
/// the following three things:
@@ -751,7 +777,8 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = 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 oldPrecondition = GetMethodPre m
+ let m2 = AddPrecondition m candCond
let sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph
Logger.Info (idt + " - verifying partial solution ... ")
let verified =
@@ -760,8 +787,17 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = else
true
if verified then
- if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"
- Some(candCond,m2,sol)
+ if Options.CONFIG.verifyPartialSolutions then
+ Logger.InfoLine "VERIFIED"
+ let g',m',sol' =
+ if Options.CONFIG.minimizeGuards then
+ __MinimizeGuard oldPrecondition candCond comp m2 sol 0
+ else
+ candCond,m2,sol
+ Some(g',m',sol')
+ else
+ Logger.InfoLine "SKIPPED"
+ Some(candCond,m2,sol)
else
Logger.InfoLine "NOT VERIFIED"
__TryOutConditions heapInst rest
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 4b5ad7bd..28b84ab9 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -474,6 +474,11 @@ let IsConstExpr e = ///////
+let GetMethodPre mthd =
+ match mthd with
+ | Method(_,_,pre,_,_) -> pre
+ | _ -> 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
@@ -537,11 +542,16 @@ let AddReplaceMethod prog comp newMthd oldMethod = newProg, newComp
| _ -> failwithf "Invalid component: %O" comp
-let AddPrecondition prog comp m e =
+let UnwrapAssumes e = e |> SplitIntoConjunts |> List.map (function AssumeExpr(e) -> e | x -> x) |> List.fold BinaryAnd TrueLiteral
+
+let AddPrecondition m e =
+ match m with
+ | Method(mn, sgn, pre, post, cstr) -> Method(mn, sgn, BinaryAnd pre (AssumeExpr(e |> UnwrapAssumes)), post, cstr)
+ | _ -> failwithf "Not a method: %O" m
+
+let SetPrecondition m e =
match m with
- | Method(mn, sgn, pre, post, cstr) ->
- let newMthd = Method(mn, sgn, BinaryAnd pre (AssumeExpr(e)), post, cstr)
- newMthd
+ | Method(mn, sgn, pre, post, cstr) -> Method(mn, sgn, AssumeExpr(e |> UnwrapAssumes), post, cstr)
| _ -> failwithf "Not a method: %O" m
////////////////////
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index 79b78173..7ec8d33e 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -164,7 +164,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr genOld = let PrintPrePost pfix expr =
SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")
-let GetPreconditionForMethod prog m =
+let GetPreconditionForMethod m =
let validExpr = IdLiteral(validFuncName);
if IsConstructor m then
GetMethodPrePost m |> fst
@@ -358,7 +358,7 @@ let GenConstructorCode prog comp mthd decreasesClause body genRepr = let validExpr = IdLiteral(validFuncName);
match mthd with
| Method(methodName,sign,_,_,isConstr) ->
- let preExpr = GetPreconditionForMethod prog mthd |> Desugar
+ let preExpr = GetPreconditionForMethod mthd |> Desugar
let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar
let thisObj = ThisObj comp
" method " + methodName + (PrintSig sign) +
diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs index df2d044f..34a9b070 100644 --- a/Jennisys/FixpointSolver.fs +++ b/Jennisys/FixpointSolver.fs @@ -236,7 +236,13 @@ let rec ComputeClosure heapInst expandExprFunc premises = // else
// __fff lhs r
// | _ -> [binInExpr]
+///////////////////////////////
[BinaryOr (BinaryIn lhs l) (BinaryIn lhs r)]
+// let opt1 = BinaryIn lhs l
+// let opt2 = BinaryIn lhs r
+// match EvalFull heapInst opt1 with
+// | BoolLiteral(true) -> [opt1]
+// | _ -> [opt2]
| SequenceExpr(elist) ->
let len = elist |> List.length
if len = 0 then
diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 2be3a550..66aa5b85 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -23,6 +23,7 @@ type Config = { numLoopUnrolls : int;
recursiveValid : bool;
breakIntoDebugger : bool;
+ minimizeGuards : bool;
}
type CfgOption<'a> = {
@@ -74,6 +75,7 @@ let cfgOptions = [ { optionName = "recValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = CheckBool v "recValid"}); descr = "generate recursive Valid() function"; }
{ optionName = "noRecValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = not (CheckBool v "noRecValid")}); descr = "unroll Valid() function"; }
{ optionName = "break"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with breakIntoDebugger = CheckBool v "break"}); descr = "launches debugger upon start-up"; }
+ { optionName = "minGuards"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with minimizeGuards = CheckBool v "minGuards"}); descr = "tries to remove unnecessary clauses from the inferred guards"; }
]
let cfgOptMap = cfgOptions |> List.fold (fun acc o -> acc |> Map.add o.optionName o) Map.empty
@@ -112,6 +114,7 @@ let defaultConfig: Config = { numLoopUnrolls = 2;
recursiveValid = true;
breakIntoDebugger = false;
+ minimizeGuards = true;
}
/// Should not be mutated outside the ParseCmdLineArgs method, which is
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index e39464f1..469e5e5a 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -171,7 +171,7 @@ let rec GenList n e = /// ret[i] = lst[i]
// =======================================
let ListReplace oldElem newElem lst =
- lst |> List.choose (fun e -> if e = oldElem then Some(newElem) else Some(e))
+ lst |> List.map (fun e -> if e = oldElem then newElem else e)
// =================================================
/// if (exists (k,v) :: (k,v) in lst && k = key) then
@@ -207,6 +207,12 @@ let ListContains elem lst = let ListRemove elem lst =
lst |> List.choose (fun e -> if e = elem then None else Some(e))
+let rec ListRemoveNth n lst =
+ if n = 0 then
+ List.tail lst
+ else
+ List.head lst :: ListRemoveNth (n-1) (List.tail lst)
+
// ===============================================================
/// ensures: |ret| = max(|lst| - cnt, 0)
/// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]
@@ -294,6 +300,9 @@ let MapSingleton key value = let MapKeys map =
map |> Map.toList |> List.map (fun (k,v) -> k)
+let MapReplaceKey oldKey newKey newVal map =
+ map |> Map.toList |> List.fold (fun acc (k,v) -> if k = oldKey then acc |> Map.add newKey newVal else acc |> Map.add k v) Map.empty
+
// -------------------------------------------
// ------------ algorithms -------------------
// -------------------------------------------
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index cba09f46..85a3b692 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -59,9 +59,6 @@ interface Node[T] { method Find(n: T) returns (ret: bool) ensures ret = (n in list) - - method SetZ(n: T) - ensures list = old(list[0 := n]) method Insert(n: T) ensures list = old(list) + [n] diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen index ae8a2845..3bd527fb 100644 --- a/Jennisys/examples/List2.jen +++ b/Jennisys/examples/List2.jen @@ -48,6 +48,11 @@ interface IntNode { constructor Double(x: int, y: int) ensures list = [x y] + + method Max() returns (ret: int) + ensures ret in list + ensures forall t :: t in list ==> ret >= t + } datamodel IntNode { diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen index a04ee481..01532f96 100644 --- a/Jennisys/examples/Set.jen +++ b/Jennisys/examples/Set.jen @@ -54,6 +54,7 @@ interface SetNode { method Find(n: int) returns (ret: bool) ensures ret = (n in elems) + } datamodel SetNode { diff --git a/Jennisys/examples/Simple.jen b/Jennisys/examples/Simple.jen index 12b2cdf0..2f5e7feb 100644 --- a/Jennisys/examples/Simple.jen +++ b/Jennisys/examples/Simple.jen @@ -1,8 +1,8 @@ interface Simple {
var a: int
- method Inc()
- a := old(a) + 1
+ method Inc(p: int)
+ a := old(a) + p
method Init(n: int)
a := n
@@ -19,6 +19,10 @@ interface Simple { method Max3__mod__(x: int, y: int)
ensures a in {x y}
ensures forall t :: t in {x y} ==> a >= t
+
+ method MaxAll__mod__(x: seq[int])
+ ensures a in x
+ ensures forall t :: t in x ==> a >= t
}
datamodel Simple {
|