- changed the way Valid() is unrolled

 - removed reading from Seq#Build because it doesn't seem to be needed anymore

5 files changed, 88 insertions, 17 deletions

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index ab86324b..fa5a0a77 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -189,6 +189,23 @@ let GetAllFields comp =
       let aVars = FilterFieldMembers members

       List.concat [aVars ; cVars]

   | _ -> []

+

+//  ===========================================================

+/// Returns a map (Type |--> Set<Var>) where all 

+/// the given fields are grouped by their type

+///

+/// ensures: forall v :: v in ret.values.elems ==> v in fields

+/// ensures: forall k :: k in ret.keys ==> 

+///            forall v1, v2 :: v1, v2 in ret[k].elems ==> 

+///              v1.type = v2.type

+//  ===========================================================

+let rec GroupFieldsByType fields = 

+  match fields with

+  | Var(name, ty) :: rest -> 

+      let map = GroupFieldsByType rest

+      let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty

+      map |> Map.add ty (fldSet |> Set.add (Var(name, ty)))

+  | [] -> Map.empty

                     

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

 /// Returns class name of a component

@@ -642,7 +659,7 @@ let ChangeThisReceiver receiver expr =
     | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

     | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map (__ChangeThis locals))

     | SetExpr(exs)                     -> SetExpr(exs |> List.map (__ChangeThis locals))

-  (* function body starts here *)

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

   __ChangeThis Set.empty expr

 

 let rec Rewrite rewriterFunc expr =

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index f2d5766c..6b53112e 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -10,16 +10,49 @@ open DafnyPrinter
 open DafnyModelUtils

 

 // TODO: this should take a list of fields and unroll all possibilities (instead of unrolling on branch only, following exactly one field)

-let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr = 

+//let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr = 

+//  if numUnrolls = 0 then

+//    TrueLiteral

+//  else

+//    BinaryImplies (BinaryNeq fldExpr (ObjLiteral("null")))

+//                  (BinaryAnd (Dot(fldExpr, validFunName))

+//                             (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))

+

+/// requires: numUnrols >= 0

+/// requires: |fldExprs| = |fldNames|

+let rec GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls = 

+  let rec __Combine exprLst strLst = 

+    match exprLst with

+    | e :: rest ->

+        let resLst1 = strLst |> List.map (fun s -> Dot(e, s))

+        List.concat [resLst1; __Combine rest strLst]

+    | [] -> []

+  let rec __NotNull e = 

+    match e with

+    | IdLiteral(_)

+    | ObjLiteral(_) -> BinaryNeq e (ObjLiteral("null"))

+    | Dot(sub, str) -> BinaryAnd (__NotNull sub) (BinaryNeq e (ObjLiteral("null")))

+    | _ -> failwith "not supposed to happen"

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

+  assert (numUnrolls >= 0)

   if numUnrolls = 0 then

-    TrueLiteral

+    [TrueLiteral]

   else

-    BinaryImplies (BinaryNeq fldExpr (IdLiteral("null")))

-                  (BinaryAnd (Dot(fldExpr, validFunName))

-                             (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))

+    let exprList = fldExprs |> List.map (fun e -> BinaryImplies (__NotNull e) (Dot(e, validFunName)))

+    if numUnrolls = 1 then 

+      exprList

+    else 

+      let fldExprs = __Combine fldExprs fldNames

+      List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFunName (numUnrolls - 1))

+                                                                    

+

+//let GetFieldValidExpr fldName validFunName numUnrolls : Expr = 

+//  GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls

 

-let GetFieldValidExpr fldName validFunName numUnrolls : Expr = 

-  GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls

+let GetFieldValidExpr flds validFunName numUnrolls = 

+  let fldExprs = flds |> List.map (function Var(name, _) -> IdLiteral(name))

+  let fldNames = flds |> List.map (function Var(name, _) -> name)

+  GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls

 

 let GetFieldsForValidExpr allFields prog : VarDecl list =

   allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true

@@ -27,13 +60,22 @@ let GetFieldsForValidExpr allFields prog : VarDecl list =
 

 let GetFieldsValidExprList clsName allFields prog : Expr list =

   let fields = GetFieldsForValidExpr allFields prog

-  fields |> List.map (function Var(name, t) -> 

-                                 let validFunName, numUnrolls = 

-                                   match t with

-                                   | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls

-                                   | _ -> "Valid()", 1

-                                 GetFieldValidExpr name validFunName numUnrolls

-                     )

+  let fieldsByType = GroupFieldsByType fields

+  fieldsByType |> Map.fold (fun acc t varSet ->

+                              let validFunName, numUnrolls = 

+                                match t with

+                                | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls

+                                | _ -> "Valid()", 1 

+                              acc |> List.append (GetFieldValidExpr (Set.toList varSet) validFunName numUnrolls)

+                           ) []

+

+//  fields |> List.map (function Var(name, t) -> 

+//                                 let validFunName, numUnrolls = 

+//                                   match t with

+//                                   | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls

+//                                   | _ -> "Valid()", 1

+//                                 GetFieldValidExpr name validFunName numUnrolls

+//                     )

 

 let PrintValidFunctionCode comp prog genRepr: string = 

   let idt = "    "

diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index f04a0ca5..83de2292 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -247,11 +247,11 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
 

   let f_seq_len = model.MkFunc("Seq#Length", 1)

   let f_seq_idx = model.MkFunc("Seq#Index", 2)

-  let f_seq_bld = model.MkFunc("Seq#Build", 4)

+  //let f_seq_bld = model.MkFunc("Seq#Build", 4)

   let f_seq_app = model.MkFunc("Seq#Append", 2)

   (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps)

                |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)

-               |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

+         //      |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)

                |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps)

 

 

diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 8c25726a..c9f18e23 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -48,6 +48,15 @@ let ExtractOptionMsg msg x =
 let ExtractOption x = 

   ExtractOptionMsg "can't extract anything from a None" x

 

+//  ====================================

+/// ensures: res = Some(a) ==> ret = a

+/// ensures: res = None ==> ret = defVal

+//  ====================================

+let ExtractOptionOr defVal opt = 

+  match opt with 

+  | Some(a) -> a

+  | None -> defVal

+

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

 /// requres: List.length lst <= 1, otherwise fails with errMsg

 /// ensures: if |lst| = 0 then

diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
index 2142738e..6006268e 100644
--- a/Jennisys/Jennisys/examples/Set.jen
+++ b/Jennisys/Jennisys/examples/Set.jen
@@ -14,6 +14,9 @@ class Set {
     requires p != q
     ensures elems = {p q}
 
+  constructor Triple(p: int, q: int, r: int)
+    requires p != q && q != r && r != p
+    ensures elems = {p q r}
 }
 
 model Set {