Jennisys: implemented minimization of inferred guards

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 {