Merge

8 files changed, 333 insertions, 51 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index b8416c93..0970a193 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -85,44 +85,31 @@ let rec IsArgsOnly args expr =
   | SeqLength(e)                         -> IsArgsOnly args e

   | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

 

+let AddUnif indent e v unifMap =

+  let idt = Indent indent

+  let builder = new CascadingBuilder<_>(unifMap)

+  builder {

+    let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption

+    Logger.DebugLine (idt + "    - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v))

+    return Map.add e v unifMap

+  }

+

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

-let GetUnifications indent expr args heapInst =

+let rec GetUnifications indent args heapInst unifs expr =

   let idt = Indent indent

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

   // - then checks if it doesn't already exist in the unification map

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

   // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map

-  let __AddUnif e unifMap =

-    let builder = new CascadingBuilder<_>(unifMap)

+  let __AddUnif e unifsAcc =

+    let builder = new CascadingBuilder<_>(unifsAcc)

     builder {

       let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption

-      let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption

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

-      Logger.DebugLine (idt + "    - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v))

-      return Map.add e v unifMap

+      return AddUnif indent e v unifsAcc

     }

-  // just recurses on all expressions

-  let rec __GetUnifications expr args unifs = 

-    let unifs = __AddUnif expr unifs

-    match expr with

-    | IntLiteral(_)

-    | BoolLiteral(_)

-    | VarLiteral(_)

-    | ObjLiteral(_)

-    | IdLiteral(_)

-    | Star                   -> unifs

-    | Dot(e, _)

-    | SeqLength(e)

-    | ForallExpr(_,e)  

-    | UnaryExpr(_,e)         -> unifs |> __GetUnifications e args

-    | SelectExpr(e1, e2)      

-    | BinaryExpr(_,_,e1,e2)  -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args

-    | IteExpr(e1,e2,e3)

-    | UpdateExpr(e1, e2, e3) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args |> __GetUnifications e3 args

-    | SetExpr(elst)

-    | SequenceExpr(elst)     -> elst |> List.fold (fun acc e -> acc |> __GetUnifications e args) unifs 

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

-  __GetUnifications expr args Map.empty

+  AstUtils.DescendExpr2 __AddUnif expr unifs

 

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

 /// Returns a map (Expr |--> Const) containing unifications

@@ -135,8 +122,7 @@ let GetUnificationsForMethod indent comp m heapInst =
     | Var(name,_) :: rest -> 

         match Map.tryFind name heapInst.methodArgs with

         | Some(c) ->

-            Logger.DebugLine (idt + "    - adding unification " + name + " <--> " + (PrintConst c));

-            Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest)

+            GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c

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

     | [] -> Map.empty

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

@@ -145,8 +131,9 @@ let GetUnificationsForMethod indent comp m heapInst =
       let args = List.concat [ins; outs]

       match args with 

       | [] -> Map.empty

-      | _  -> GetUnifications indent (BinaryAnd pre post) args heapInst

-              |> Utils.MapAddAll (GetArgValueUnifications args)

+      | _  -> let unifs = GetArgValueUnifications args

+              GetUnifications indent args heapInst unifs (BinaryAnd pre post)

+              

   | _ -> failwith ("not a method: " + m.ToString())

 

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

@@ -250,7 +237,6 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
                                                          | _ -> 

                                                              Utils.ListMapAdd (o,f) value acc

                                                      ) heapInst.assignments

-                                        |> List.rev

       {heapInst with assignments = newHeap }

   | [] -> heapInst

 

@@ -263,6 +249,18 @@ let VerifySolution prog comp mthd sol genRepr =
   let code = PrintImplCode prog solutions (fun p -> [comp,mthd]) genRepr

   CheckDafnyProgram code dafnyVerifySuffix

 

+let rec DiscoverAliasing exprList heapInst = 

+  match exprList with

+  | e1 :: rest -> 

+      let eqExpr = rest |> List.fold (fun acc e -> 

+                                        if Eval heapInst true (BinaryEq e1 e) = TrueLiteral then

+                                          BinaryAnd acc (BinaryEq e1 e)

+                                        else

+                                          acc

+                                     ) TrueLiteral

+      BinaryAnd eqExpr (DiscoverAliasing rest heapInst)

+  | [] -> TrueLiteral

+

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

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

 ///

@@ -294,9 +292,9 @@ let rec AnalyzeConstructor indent prog comp m =
     let heapInst = ResolveModel hModel

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

     let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

+    let sol = [TrueLiteral, heapInst]

     if Options.CONFIG.verifySolutions then

       Logger.InfoLine (idt + "    - verifying synthesized solution ... ")

-      let sol = [TrueLiteral, heapInst]

       let verified = VerifySolution prog comp m sol Options.CONFIG.genRepr

       Logger.Info (idt + "    ")

       if verified then

@@ -304,8 +302,11 @@ let rec AnalyzeConstructor indent prog comp m =
         sol

       else 

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

-        Logger.InfoLine (idt + "    Strengthening the pre-condition")

-        TryInferConditionals (indent + 4) prog comp m unifs heapInst

+        if Options.CONFIG.inferConditionals then

+          Logger.InfoLine (idt + "    Strengthening the pre-condition")

+          TryInferConditionals (indent + 4) prog comp m unifs heapInst

+        else

+          sol      

     else

       [TrueLiteral, heapInst]

 and TryInferConditionals indent prog comp m unifs heapInst = 

@@ -333,10 +334,19 @@ and TryInferConditionals indent prog comp m unifs heapInst =
       Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

       wrongSol

     else

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

-      let p2,c2,m2 = AddPrecondition prog comp m newCond

+      let candCond = 

+        if newCond = FalseLiteral then

+          // it must be because there is some aliasing going on between method arguments, 

+          // so we should try that as a candidate pre-condition

+          let tmp = DiscoverAliasing (GetMethodArgs m |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2

+          if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered")

+          tmp

+        else 

+          newCond

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

+      let p2,c2,m2 = AddPrecondition prog comp m candCond

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

-      let sol = [newCond, heapInst2]

+      let sol = [candCond, heapInst2]

       let verified = 

         if Options.CONFIG.verifyPartialSolutions then

           VerifySolution p2 c2 m2 sol Options.CONFIG.genRepr

@@ -347,7 +357,7 @@ and TryInferConditionals indent prog comp m unifs heapInst =
           Logger.InfoLine "VERIFIED"

         else 

           Logger.InfoLine "SKIPPED"

-        let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(newCond))

+        let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

         sol.[0] :: AnalyzeConstructor (indent + 2) p3 c3 m3

       else 

         Logger.InfoLine "NOT VERIFIED"

@@ -401,19 +411,23 @@ let rec AnalyzeMethods prog members =
       | _ -> AnalyzeMethods prog rest

   | [] -> Map.empty

 

+let GetModularSol prog sol = 

+  

+  sol

+

 let Modularize prog solutions = 

-  let rec __Modularize acc sols = 

+  let rec __Modularize sols acc = 

     match sols with

     | sol :: rest -> 

-        let newSol = sol

+        let newSol = GetModularSol prog sol

         let newAcc = acc |> Map.add (fst newSol) (snd newSol)

-        __Modularize newAcc rest

+        __Modularize rest newAcc 

     | [] -> acc

-  (* --- --- *) 

-  __Modularize Map.empty (Map.toList solutions)

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

+  __Modularize (Map.toList solutions) Map.empty 

 

 let Analyze prog filename =

-  /// Prints a given (flat) solution to a designated file on the disk

+  /// Prints given solutions to a file

   let __PrintSolution outFileName solutions = 

     use file = System.IO.File.CreateText(outFileName)

     file.AutoFlush <- true  

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index cf008458..2c8c4440 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -78,7 +78,25 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
                                         | [] -> leafVal

                                         | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)

               

-

+let rec DescendExpr2 visitorFunc expr acc = 

+  let newAcc = acc |> visitorFunc expr

+  match expr with

+  | IntLiteral(_)

+  | BoolLiteral(_)                   

+  | Star      

+  | VarLiteral(_) 

+  | ObjLiteral(_)                      

+  | IdLiteral(_)                     -> newAcc

+  | Dot(e, _)

+  | ForallExpr(_,e)

+  | UnaryExpr(_,e)           

+  | SeqLength(e)                     -> newAcc |> DescendExpr2 visitorFunc e

+  | SelectExpr(e1, e2)

+  | BinaryExpr(_,_,e1,e2)            -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2

+  | IteExpr(e1,e2,e3)

+  | UpdateExpr(e1,e2,e3)             -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2 |> DescendExpr2 visitorFunc e3

+  | SequenceExpr(exs)                

+  | SetExpr(exs)                     -> exs |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc              

 

 let PrintGenSym name =

   sprintf "gensym%s" name

@@ -686,7 +704,8 @@ let rec Desugar expr =
   | UpdateExpr(_)     

   | SetExpr(_)     

   | SequenceExpr(_)        -> expr 

-  // forall v :: v in {a1, a2, ..., an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

+  // forall v :: v in {a1 a2 ... an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

+  // forall v :: v in [a1 a2 ... an] ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

   | ForallExpr([Var(vn1,ty1)] as v, (BinaryExpr(_, "==>", BinaryExpr(_, "in", VarLiteral(vn2), rhsCol), sub) as ee)) when vn1 = vn2 ->

       match rhsCol with 

       | SetExpr(elist)

diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 082a54e1..69ab0ff2 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

-    <StartArguments>examples/Set.jen /method:SetNode.Double /genRepr</StartArguments>

+    <StartArguments>examples/Set.jen /method:Set.Double /genRepr /noVerifyParSol</StartArguments>

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

   </PropertyGroup>

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

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index 567967ae..e1fc9e91 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -12,6 +12,7 @@ type Config = {
    help: bool;

    inputFilename: string;

    methodToSynth: string;

+   inferConditionals: bool;

    verifyPartialSolutions: bool;

    verifySolutions: bool;

    checkUnifications: bool;

@@ -51,6 +52,8 @@ 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 = "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"; }

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

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

@@ -87,6 +90,7 @@ let PrintHelpMsg =
 let defaultConfig: Config = {

   help              = false;

   inputFilename     = "";

+  inferConditionals = true;

   methodToSynth     = "*";

   verifyPartialSolutions = true;

   verifySolutions   = true;

diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index 61fad148..116804fa 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -8,7 +8,7 @@ class IntList {
     ensures list = [2]
 
   constructor OneTwo()
-    ensures list = [1] + [2] 
+    ensures list = [1 2]
 
   constructor Singleton(p: int)
     ensures list = [p]
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index 776bd43d..d01300bb 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -8,7 +8,7 @@ class IntList {
     ensures list = [2]
 
   constructor OneTwo()
-    ensures list = [1] + [2] 
+    ensures list = [1 2]
 
   constructor Singleton(p: int)
     ensures list = [p]
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index 6006268e..3bee04e8 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -11,7 +11,6 @@ class Set {
     ensures elems = {p + q}
 
   constructor Double(p: int, q: int)
-    requires p != q
     ensures elems = {p q}
 
   constructor Triple(p: int, q: int, r: int)
diff --git a/Jennisys/examples/set.dfy b/Jennisys/examples/set.dfy
new file mode 100644
index 00000000..627f1ecb
--- /dev/null
+++ b/Jennisys/examples/set.dfy
@@ -0,0 +1,246 @@
+class Set {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var root: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (root == null ==> elems == {}) &&

+    (root != null ==> elems == root.elems)

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (root != null ==> root.Valid())

+  }

+

+  method Empty()

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {};

+  {

+    this.elems := {};

+    this.root := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Singleton(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    var gensym66 := new SetNode;

+    gensym66.Init(t);

+    this.elems := {t};

+    this.root := gensym66;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Sum(p: int, q: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p + q};

+  {

+    var gensym68 := new SetNode;

+    gensym68.Init(p+q);

+    this.elems := {p + q};

+    this.root := gensym68;

+    this.Repr := {this} + this.root.Repr;

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    var gensym71 := new SetNode; 

+    gensym71.Double(p, q);

+    this.elems := {p, q}; 

+    this.root := gensym71; 

+    this.Repr := {this} + this.root.Repr; 

+  }

+

+}

+

+class SetNode {

+  ghost var Repr: set<object>;

+  ghost var elems: set<int>;

+

+  var data: int;

+  var left: SetNode;

+  var right: SetNode;

+

+  function Valid_repr(): bool

+    reads *;

+  {

+    this in Repr &&

+    null !in Repr &&

+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&

+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)

+  }

+

+  function Valid_self(): bool

+    reads *;

+  {

+    Valid_repr() &&

+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&

+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&

+    (right != null ==> (forall e :: e in right.elems ==> e > data))

+  }

+

+  function Valid(): bool

+    reads *;

+  {

+    this.Valid_self() &&

+    (left != null ==> left.Valid_self() && (left.left != null ==> left.left.Valid_self())) &&

+    (right != null ==> right.Valid_self() && (right.right != null ==> right.right.Valid_self()))

+  }

+

+  method Init(t: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {t};

+  {

+    this.data := t;

+    this.elems := {t};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+  method Double(p: int, q: int)

+    modifies this;

+//    requires p != q;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q};

+  {

+    if (q > p) {

+      var gensym79 := new SetNode;

+      gensym79.Init(q);

+      this.data := p;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      this.Repr := {this} + this.right.Repr;

+    } else if (q < p) {

+      var gensym79 := new SetNode;

+      gensym79.Init(p);

+      this.data := q;

+      this.elems := {p, q};

+      this.left := null;

+      this.right := gensym79;

+      this.Repr := {this} + this.right.Repr;

+    } else {

+      this.data := p; 

+      this.elems := {p};

+      this.left := null;

+      this.right := null;

+      this.Repr := {this};

+    } 

+  }

+

+  method Triple(p: int, q: int, r: int)

+    modifies this;

+    requires p != q;

+    requires q != r;

+    requires r != p;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {p, q, r};

+  {

+    if (p < q && r > q) {

+      var gensym83 := new SetNode;

+      var gensym84 := new SetNode;

+      gensym83.Init(r);

+      gensym84.Init(p);

+      this.data := q;

+      this.elems := {p, q, r};

+      this.left := gensym84;

+      this.right := gensym83;

+      this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+    } else {

+      if (p < r && q > r) {

+        var gensym85 := new SetNode;

+        var gensym86 := new SetNode;

+        gensym85.Init(q);

+        gensym86.Init(p);

+        this.data := r;

+        this.elems := {p, q, r};

+        this.left := gensym86;

+        this.right := gensym85;

+        this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+      } else {

+        if (r < p && q > p) {

+          var gensym84 := new SetNode;

+          var gensym85 := new SetNode;

+          gensym84.Init(q);

+          gensym85.Init(r);

+          this.data := p;

+          this.elems := {p, q, r};

+          this.left := gensym85;

+          this.right := gensym84;

+          this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+        } else {

+          if (q < p && r > p) {

+            var gensym82 := new SetNode;

+            var gensym83 := new SetNode;

+            gensym82.Init(r);

+            gensym83.Init(q);

+            this.data := p;

+            this.elems := {p, q, r};

+            this.left := gensym83;

+            this.right := gensym82;

+            this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+          } else {

+            if (q < r && p > r) {

+              var gensym85 := new SetNode;

+              var gensym86 := new SetNode;

+              gensym85.Init(p);

+              gensym86.Init(q);

+              this.data := r;

+              this.elems := {p, q, r};

+              this.left := gensym86;

+              this.right := gensym85;

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            } else {

+              var gensym82 := new SetNode;

+              var gensym83 := new SetNode;

+              gensym82.Init(p);

+              gensym83.Init(r);

+              this.data := q;

+              this.elems := {p, q, r};

+              this.left := gensym83;

+              this.right := gensym82;

+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            }

+          }

+        }

+      }

+    }

+  }

+

+}

+

+