- removed the "Constructor" discriminator from type Member, and added a

   boolean flag to the "Method" discriminator instead

 - added a new example called "List3.jen".  The difference between List2 is
   that the IntNode class has a "succ" field that returns a list of all
   successor nodes, instead of list of integers as in List2.  In this example,
   the invariant is very verbose because of the lack of better syntax, so
   maybe we can add some syntactic sugar to Jennisys (e.g. for transitive
   closure, comprehensions, etc.) and synthesize Dafny code from that.

 - reading from BVD models now also reads Seq#Append, because some lists are
   created only that way

10 files changed, 168 insertions, 49 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 30d4b85a..e3135cff 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -59,12 +59,12 @@ let MethodAnalysisPrinter onlyForThisCompMethod comp mthd =
   match onlyForThisCompMethod with
   | (c,m) when c = comp && m = mthd -> 
     match m with 
-    | Constructor(methodName, sign, pre, post) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
+    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
     | _ -> ""
   | _ -> ""
                            
 let AnalyzeConstructor prog comp methodName signature pre post =
-  let m = Constructor(methodName, signature, pre, post)
+  let m = Method(methodName, signature, pre, post, true)
   use file = System.IO.File.CreateText(dafnyScratchFile)
   file.AutoFlush <- true
   let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
@@ -83,11 +83,11 @@ let AnalyzeConstructor prog comp methodName signature pre post =
     let model = models.[0]
     Some(ReadFieldValuesFromModel model prog comp m)
 
-let rec AnalyzeMethods prog methods = 
-  match methods with
+let rec AnalyzeMethods prog members = 
+  match members with
   | (comp,m) :: rest -> 
       match m with
-      | Constructor(methodName,signature,pre,post) -> 
+      | Method(methodName,signature,pre,post,true) -> 
           let solOpt = AnalyzeConstructor prog comp methodName signature pre post
           match solOpt with
           | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
@@ -96,7 +96,7 @@ let rec AnalyzeMethods prog methods =
   | [] -> Map.empty
 
 let Analyze prog =
-  let solutions = AnalyzeMethods prog (Methods prog)
+  let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
   use file = System.IO.File.CreateText(dafnySynthFile)
   file.AutoFlush <- true
   let synthCode = PrintImplCode prog solutions
diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index b2bd27c0..45fd2aff 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -46,8 +46,7 @@ type Signature =
 

 type Member =

   | Field of VarDecl

-  | Constructor of string * Signature * Expr * Expr

-  | Method of string * Signature * Expr * Expr

+  | Method of (* name *) string * Signature * (* pre *) Expr * (* post *) Expr * (* isConstructor *) bool

   | Invariant of Expr list

 

 type TopLevelDecl =

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 3e32fd5c..23e802ab 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -31,17 +31,17 @@ let FilterFieldMembers members =
   members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
 
 let FilterConstructorMembers members = 
-  members |> List.choose (function Constructor(_,_,_,_) as m -> Some(m) | _ -> None)
+  members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)
 
 let FilterMethodMembers members = 
-  members |> List.choose (function Method(_,_,_,_) as m -> Some(m) | _ -> None)
+  members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None)
 
-let Methods prog = 
+let FilterMembers prog filter = 
   match prog with
   | Program(components) ->
       components |> List.fold (fun acc comp -> 
         match comp with
-        | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> List.choose (fun m -> Some(comp, m))]            
+        | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            
         | _ -> acc) []

 

 let AllFields c = 

@@ -50,17 +50,31 @@ let AllFields c =
       let aVars = FilterFieldMembers members
       List.concat [aVars ; cVars]

   | _ -> []

-

+                

 let GetClassName comp =

   match comp with

   | Component(Class(name,_,_),_,_) -> name

   | _ -> failwith ("unrecognized component: " + comp.ToString())

 

+let GetMethodName mthd = 

+  match mthd with

+  | Method(name,_,_,_,_) -> name

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

+

+let GetMembers comp =

+  match comp with

+  | Component(Class(_,_,members),_,_) -> members

+  | _ -> failwith ("unrecognized component: " + comp.ToString())

+

 let FindComponent (prog: Program) clsName = 

   match prog with

   | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)

                             |> Utils.ListToOption

 

+let FindMethod comp methodName =

+  GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

+                                         |> Utils.ListToOption

+

 let FindVar (prog: Program) clsName fldName =

   let copt = FindComponent prog clsName

   match copt with

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index a1d89812..f7b953f7 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -7,39 +7,61 @@ open Printer
 open TypeChecker

 open DafnyPrinter

 

-let GetFieldValidExpr (name: string) : Expr = 
-  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))
+let numLoopUnrolls = 2

+

+let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr = 

+  if numUnrolls = 0 then

+    TrueLiteral

+  else

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

+                  (BinaryAnd (Dot(fldExpr, validFunName))

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

+

+let GetFieldValidExpr fldName validFunName numUnrolls : Expr = 
+  GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls
+  //BinaryImplies (BinaryNeq (IdLiteral(fldName)) (IdLiteral("null"))) (Dot(IdLiteral(fldName), validFunName))
 
-let GetFieldsForValidExpr (allFields: VarDecl list) prog : VarDecl list =
+let GetFieldsForValidExpr allFields prog : VarDecl list =
   allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
                                      | _                                   -> false)
 
-let GetFieldsValidExprList (allFields: VarDecl list) prog : Expr list =
+let GetFieldsValidExprList clsName allFields prog : Expr list =
   let fields = GetFieldsForValidExpr allFields prog
-  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)
+  fields |> List.map (function Var(name, t) -> 
+                                 let validFunName, numUnrolls = 
+                                   match t with
+                                   | Some(ty) when clsName = (PrintType ty) -> "Valid_self()", numLoopUnrolls
+                                   | _ -> "Valid()", 1
+                                 GetFieldValidExpr name validFunName numUnrolls
+                     )
 
-let PrintValidFunctionCode clsMembers modelInv vars prog : string = 
+let PrintValidFunctionCode clsName clsMembers modelInv vars prog : string = 
   let invMembers = clsMembers |> List.filter (function Invariant(_) -> true | _ -> false)
   let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
   let allInvs = modelInv :: clsInvs
-  let fieldsValid = GetFieldsValidExprList vars prog
+  let fieldsValid = GetFieldsValidExprList clsName vars prog
   let idt = "    "
-  let invsStr = List.concat [allInvs ; fieldsValid] |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
-                                                    |> List.fold (fun acc (e: Expr) -> 
-                                                                    if acc = "" then
-                                                                      sprintf "%s(%s)" idt (PrintExpr 0 e)
-                                                                    else
-                                                                      acc + " &&" + newline + sprintf "%s(%s)" idt (PrintExpr 0 e)) ""
+  let PrintInvs invs = 
+    invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []
+         |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e))
+         |> fun s -> if s = "" then (idt + "true") else s
   // TODO: don't hardcode decr vars!!!
-  let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then
-                   ["list"]
-                 else
-                   []
+//  let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then
+//                   ["list"]
+//                 else
+//                   []
+//  (if List.isEmpty decrVars then "" else sprintf "    decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
+  "  function Valid_self(): bool" + newline +
+  "    reads *;" + newline +
+  "  {" + newline + 
+  (PrintInvs allInvs) + newline +
+  "  }" + newline +
+  newline +
   "  function Valid(): bool" + newline +
   "    reads *;" + newline +
-  (if List.isEmpty decrVars then "" else sprintf "    decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +
   "  {" + newline + 
-  invsStr + newline +
+  "    this.Valid_self() &&" + newline +
+  (PrintInvs fieldsValid) + newline +
   "  }" + newline

 

 let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
@@ -57,7 +79,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
         (sprintf "%s" (PrintFields aVars 2 true)) + newline +     
         (sprintf "%s" (PrintFields cVars 2 false)) + newline +                           
         // generate the Valid function
-        (sprintf "%s" (PrintValidFunctionCode members inv allVars prog)) + newline +
+        (sprintf "%s" (PrintValidFunctionCode name members inv allVars prog)) + newline +
         // call the method printer function on all methods of this component
         (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") +
         // the end of the class
@@ -97,8 +119,9 @@ let PrintHeapCreationCode (heap,env,ctx) indent =
   (PrintVarAssignments (heap,env,ctx) indent)
 
 let GenConstructorCode mthd body =
+  printfn "Printing code for method %s." (GetMethodName mthd)
   match mthd with
-  | Constructor(methodName, sign, pre, post) -> 
+  | Method(methodName, sign, pre, post, _) -> 
       "  method " + methodName + (PrintSig sign) + newline +
       "    modifies this;" + newline +
       "    requires " + (PrintExpr 0 pre) + ";" + newline +
@@ -109,11 +132,22 @@ let GenConstructorCode mthd body =
       "  }" + newline
   | _ -> ""
 
+// NOTE: insert here coto to say which methods to analyze
+let GetMethodsToAnalyze prog =
+  let c = FindComponent prog "IntList" |> Utils.ExtractOption
+  let m = FindMethod c "OneTwo" |> Utils.ExtractOption
+  [c, m]
+  //FilterMembers prog FilterConstructorMembers
+
 // solutions: (comp, constructor) |--> (heap, env, ctx) 
 let PrintImplCode prog solutions =
+  let methods = GetMethodsToAnalyze prog
   PrintDafnyCodeSkeleton prog (fun comp mthd ->
-                                 let mthdBody = match Map.tryFind (comp,mthd) solutions with
-                                                | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4
-                                                | _ -> "    //unable to synthesize" + newline
-                                 (GenConstructorCode mthd mthdBody) + newline
+                                 if Utils.ListContains (comp,mthd) methods  then
+                                   let mthdBody = match Map.tryFind (comp,mthd) solutions with
+                                                  | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4
+                                                  | _ -> "    //unable to synthesize" + newline
+                                   (GenConstructorCode mthd mthdBody) + newline
+                                 else
+                                   ""
                               )
\ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index 800a65d5..fca44270 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -160,25 +160,42 @@ let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTupl
 let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) = 

   match bld_tuples with

   | ft :: rest -> 

-      let srcLstKey = GetLoc ft.Args.[0]

-      let dstLstKey = GetLoc ft.Result

-      let oldLst = GetSeqFromEnv envMap srcLstKey

+      let srcLstLoc = GetLoc ft.Args.[0]

+      let dstLstLoc = GetLoc ft.Result

+      let oldLst = GetSeqFromEnv envMap srcLstLoc

       let idx = GetInt ft.Args.[1]

       let lstElemVal = UnboxIfNeeded model ft.Args.[2]

-      let dstLst = GetSeqFromEnv envMap dstLstKey

+      let dstLst = GetSeqFromEnv envMap dstLstLoc

       let newLst = Utils.ListBuild oldLst idx (Some(lstElemVal)) dstLst

       let newCtx = UpdateContext dstLst newLst ctx

-      let newEnv = envMap |> Map.add dstLstKey (SeqConst(newLst))

+      let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

       ReadSeqBuild model rest (newEnv,newCtx)

   | _ -> (envMap,ctx)

 

+let rec ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) = 

+  match app_tuples with

+  | ft :: rest -> 

+      let srcLst1Loc = GetLoc ft.Args.[0]

+      let srcLst2Loc = GetLoc ft.Args.[1]

+      let dstLstLoc = GetLoc ft.Result

+      let oldLst1 = GetSeqFromEnv envMap srcLst1Loc

+      let oldLst2 = GetSeqFromEnv envMap srcLst2Loc

+      let dstLst = GetSeqFromEnv envMap dstLstLoc

+      let newLst = List.append oldLst1 oldLst2

+      let newCtx = UpdateContext dstLst newLst ctx

+      let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

+      ReadSeqAppend model rest (newEnv,newCtx)

+  | _ -> (envMap,ctx)

+

 let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =

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

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

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

+  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)

+               |> ReadSeqAppend model (List.ofSeq f_seq_app.Apps)

 

 

 let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index fb1008d0..9d776796 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

-    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List2.jen</StartArguments>

+    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List3.jen</StartArguments>

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy
index 71ca4de0..10aa7d1d 100644
--- a/Jennisys/Jennisys/Parser.fsy
+++ b/Jennisys/Jennisys/Parser.fsy
@@ -89,8 +89,8 @@ BlockStmt:
 

 Member:

     | VAR VarDecl                            { Field($2) }

-    | CONSTRUCTOR ID Signature Pre Post      { Constructor($2, $3, $4, $5) }

-    | METHOD ID Signature Pre Post           { Method($2, $3, $4, $5) }

+    | CONSTRUCTOR ID Signature Pre Post      { Method($2, $3, $4, $5, true) }

+    | METHOD ID Signature Pre Post           { Method($2, $3, $4, $5, false) }

 	  | INVARIANT ExprList                     { Invariant($2) }

 

 FrameMembers:

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index b0d4746c..97b537db 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -109,8 +109,8 @@ let PrintRoutine signature pre body =
 let PrintMember m =
   match m with
   | Field(vd) -> sprintf "  var %s%s" (PrintVarDecl vd) newline 
-  | Constructor(id,signature,pre,body) -> sprintf "  constructor %s%s" id (PrintRoutine signature pre body)
-  | Method(id,signature,pre,body) -> sprintf "  method %s%s" id (PrintRoutine signature pre body)
+  | Method(id,signature,pre,body,true) -> sprintf "  constructor %s%s" id (PrintRoutine signature pre body)
+  | Method(id,signature,pre,body,false) -> sprintf "  method %s%s" id (PrintRoutine signature pre body)
   | Invariant(_) -> ""  // invariants are handled separately
       
 let PrintTopLevelDeclHeader kind id typeParams =
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 9a743fe0..5f991049 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -4,6 +4,11 @@
 // ----------- collection util funcs ---------

 // -------------------------------------------

 

+let ExtractOption x = 

+  match x with

+  | Some(a) -> a

+  | None -> failwith "can't extract anything from a None"

+

 let ListToOption lst = 

   assert (List.length lst <= 1)

   if List.isEmpty lst then

@@ -31,6 +36,9 @@ let rec GenList n =
   else

     None :: (GenList (n-1))

 

+let ListContains elem lst = 

+  lst |> List.exists (fun e -> e = elem)

+

 let rec ListSkip cnt lst = 

   if cnt = 0 then

     lst

diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen
new file mode 100644
index 00000000..ef675873
--- /dev/null
+++ b/Jennisys/Jennisys/examples/List3.jen
@@ -0,0 +1,47 @@
+class IntList {
+  var list: seq[int]
+
+  constructor Empty()
+    ensures list = []
+
+  constructor SingletonTwo()
+    ensures list = [2]
+
+  constructor OneTwo()
+    ensures |list| = 2
+    ensures list[0] = 1
+    ensures list[1] = 2
+}
+
+model IntList {
+  var root: IntNode
+
+  frame
+    root * root.list[*]
+
+  invariant
+    root = null  ==> |list| = 0
+    root != null ==> (|list| = |root.succ| + 1 && 
+                      list[0] = root.data && 
+                      (forall i :: (0 < i && i < |root.succ| && root.succ[i] != null) ==> list[i+1] = root.succ[i].data))
+}
+
+class IntNode {
+  var succ: seq[IntNode]
+  var data: int
+
+  constructor Zero()
+    ensures data = 0
+    ensures succ = []
+}
+
+model IntNode {
+  var next: IntNode
+
+  frame 
+    data * next
+
+  invariant
+    next = null  ==> |succ| = 0
+    next != null ==> (succ = [next] + next.succ)
+}