- when analyzing a constructor, repeated "assume <inv>" statement explicitly

   since "assume Valid()" doesn't always work

 - added optional verification step after code has been synthesized

9 files changed, 93 insertions, 50 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index e3135cff..fab61ff4 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -5,6 +5,7 @@ open AstUtils
 open CodeGen
 open DafnyModelUtils
 open PipelineUtils
+open Options
 open Printer
 open DafnyPrinter
 
@@ -34,11 +35,10 @@ let rec Substitute substMap = function
   | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
   | expr -> expr
 
-let GenMethodAnalysisCode methodName signature pre post assumeInvInitially =
+let GenMethodAnalysisCode comp methodName signature pre post =
   "  method " + methodName + "()" + newline +
   "    modifies this;" + newline +
   "  {" + newline + 
-  (if assumeInvInitially then "    assume Valid();" else "") +
   // print signature as local variables
   (match signature with
     | Sig(ins,outs) ->
@@ -50,45 +50,81 @@ let GenMethodAnalysisCode methodName signature pre post assumeInvInitially =
   "    // assume invariant and postcondition" + newline + 
   "    assume Valid();" + newline +
   "    assume " + (PrintExpr 0 post) + ";" + newline +
+  // inline the user defined invariant because assuming Valid() doesn't always work
+  "    // assume user defined invariant again because assuming Valid() doesn't always work" +
+  (GetInvariantsAsList comp |> PrintSep newline (fun e -> "    assume " + (PrintExpr 0 e) + ";")) + newline +
   // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
   "    // assert false to search for a model satisfying the assumed constraints" + newline + 
   "    assert false;" + newline + 
-  "  }" + newline  
+  "  }" + newline
              
 let MethodAnalysisPrinter onlyForThisCompMethod comp mthd = 
   match onlyForThisCompMethod with
   | (c,m) when c = comp && m = mthd -> 
     match m with 
-    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
+    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post) + newline
     | _ -> ""
   | _ -> ""
+
+let VerifySolution (heap,env,ctx) prog comp mthd =
+  // print the solution to file and try to verify it with Dafny
+  let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)
+  let code = PrintImplCode prog solution (fun p -> [comp,mthd])
+  use file = System.IO.File.CreateText(dafnyVerifyFile)
+  file.AutoFlush <- true  
+  fprintfn file "%s" code
+  file.Close()
+  // run Dafny
+  RunDafny dafnyVerifyFile dafnyVerifyModelFile
+  // read models from the model file
+  use modelFile = System.IO.File.OpenText(dafnyVerifyModelFile)
+  let models = Microsoft.Boogie.Model.ParseModels modelFile
+  // if there are no models, verification was successful
+  models.Count = 0
                            
-let AnalyzeConstructor prog comp methodName signature pre post =
-  let m = Method(methodName, signature, pre, post, true)
+let AnalyzeConstructor prog comp m =
+  let methodName = GetMethodName m
+  // generate Dafny code for analysis first
+  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
+  printfn "  [*] analyzing constructor %s" methodName 
+  printf  "       - searching for a solution       ..."
   use file = System.IO.File.CreateText(dafnyScratchFile)
   file.AutoFlush <- true
-  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
-  printfn "analyzing constructor %s" methodName 
   fprintf file "%s" code
   file.Close()
+  // run Dafny
   RunDafny dafnyScratchFile dafnyModelFile
-  use modelFile = System.IO.File.OpenText(dafnyModelFile)
-        
+  // read models
+  use modelFile = System.IO.File.OpenText(dafnyModelFile)        
   let models = Microsoft.Boogie.Model.ParseModels modelFile
   if models.Count = 0 then
-    printfn "spec for method %s.%s is inconsistent (no valid solution exists)" (GetClassName comp) methodName
-    None //failwith "inconsistent spec"      // TODO: instead of failing, just continue
+    // no models means that the "assert false" was verified, which means that the spec is inconsistent
+    printfn " !!! SPEC IS INCONSISTENT !!!"
+    None
   else 
-    if models.Count > 1 then failwith "why did we get more than one model for a single constructor analysis???"
+    if models.Count > 1 then 
+      printfn " FAILED "
+      failwith "internal error (more than one model for a single constructor analysis)"
+    printfn " OK "
     let model = models.[0]
-    Some(ReadFieldValuesFromModel model prog comp m)
+    let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
+    if _opt_verifySolutions then
+      printf "       - verifying synthesized solution ..."
+      if VerifySolution (heap,env,ctx) prog comp m then
+        printfn " OK"
+        Some(heap,env,ctx)
+      else 
+        printfn " NOT VERIFIED"
+        Some(heap,env,ctx)
+    else
+      Some(heap,env,ctx)
 
 let rec AnalyzeMethods prog members = 
   match members with
   | (comp,m) :: rest -> 
       match m with
-      | Method(methodName,signature,pre,post,true) -> 
-          let solOpt = AnalyzeConstructor prog comp methodName signature pre post
+      | Method(_,_,_,_,true) -> 
+          let solOpt = AnalyzeConstructor prog comp m
           match solOpt with
           | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
           | None -> AnalyzeMethods prog rest
@@ -99,7 +135,8 @@ let Analyze prog =
   let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
   use file = System.IO.File.CreateText(dafnySynthFile)
   file.AutoFlush <- true
-  let synthCode = PrintImplCode prog solutions
+  printfn "Printing synthesized code"
+  let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze
   fprintfn file "%s" synthCode
   ()
 
diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index 45fd2aff..26d27fef 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -51,7 +51,7 @@ type Member =
 

 type TopLevelDecl =

   | Class of string * string list * Member list

-  | Model of string * string list * VarDecl list * Expr list * Expr

+  | Model of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr

   | Code of string * string list

 

 type SyntacticProgram =

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 23e802ab..47ee49b7 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -25,6 +25,15 @@ let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
 let TrueLiteral = IdLiteral("true")

 let FalseLiteral = IdLiteral("false")

 

+let rec SplitIntoConjunts expr = 
+  match expr with
+  | IdLiteral("true") -> []
+  | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
+  | _ -> [expr]
+
+let rec ForeachConjunct f expr =
+  SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""

+

 // --- search functions ---

                                                

 let FilterFieldMembers members =
@@ -44,13 +53,13 @@ let FilterMembers prog filter =
         | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            
         | _ -> acc) []

 

-let AllFields c = 

-  match c with
+let GetAllFields comp = 

+  match comp with
   | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
       let aVars = FilterFieldMembers members
       List.concat [aVars ; cVars]

   | _ -> []

-                

+                              

 let GetClassName comp =

   match comp with

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

@@ -61,6 +70,13 @@ let GetMethodName mthd =
   | Method(name,_,_,_,_) -> name

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

 

+let GetInvariantsAsList comp = 

+  match comp with

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

+      let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat

+      List.append (SplitIntoConjunts inv) clsInvs

+  | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())

+

 let GetMembers comp =

   match comp with

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

@@ -79,6 +95,6 @@ let FindVar (prog: Program) clsName fldName =
   let copt = FindComponent prog clsName

   match copt with

   | Some(comp) -> 

-      AllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

-                     |> Utils.ListToOption

+      GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

+                        |> Utils.ListToOption

   | None -> None
\ No newline at end of file
diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 6b08bf58..75422de7 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -35,10 +35,10 @@ let GetFieldsValidExprList clsName allFields prog : Expr list =
                                  GetFieldValidExpr name validFunName numUnrolls
                      )
 
-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 PrintValidFunctionCode comp prog : string = 
+  let clsName = GetClassName comp
+  let vars = GetAllFields comp
+  let allInvs = GetInvariantsAsList comp
   let fieldsValid = GetFieldsValidExprList clsName vars prog
   let idt = "    "
   let PrintInvs invs = 
@@ -68,7 +68,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
   match prog with
   | Program(components) -> components |> List.fold (fun acc comp -> 
       match comp with  
-      | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+      | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp ->
         let aVars = FilterFieldMembers members
         let allVars = List.concat [aVars ; cVars];
         let compMethods = FilterConstructorMembers members
@@ -79,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 name members inv allVars prog)) + newline +
+        (sprintf "%s" (PrintValidFunctionCode comp 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
@@ -119,7 +119,6 @@ let PrintHeapCreationCode (heap,env,ctx) indent =
   (PrintVarAssignments (heap,env,ctx) indent)
 
 let GenConstructorCode mthd body =
-  printfn "Printing code for method %s." (GetMethodName mthd)
   let validExpr = IdLiteral("Valid()");
   match mthd with
   | Method(methodName, sign, pre, post, _) -> 
@@ -143,8 +142,8 @@ let GetMethodsToAnalyze prog =
   FilterMembers prog FilterConstructorMembers
 
 // solutions: (comp, constructor) |--> (heap, env, ctx) 
-let PrintImplCode prog solutions =
-  let methods = GetMethodsToAnalyze prog
+let PrintImplCode prog solutions methodsToPrintFunc =
+  let methods = methodsToPrintFunc prog
   PrintDafnyCodeSkeleton prog (fun comp mthd ->
                                  if Utils.ListContains (comp,mthd) methods  then
                                    let mthdBody = match Map.tryFind (comp,mthd) solutions with
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 9d776796..4341dfcf 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -42,6 +42,7 @@
     <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>

   </PropertyGroup>

   <ItemGroup>

+    <Compile Include="Options.fs" />

     <Compile Include="Utils.fs" />

     <Compile Include="PipelineUtils.fs" />

     <Compile Include="Ast.fs" />

diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs
index 2363995d..35507d1e 100644
--- a/Jennisys/Jennisys/PipelineUtils.fs
+++ b/Jennisys/Jennisys/PipelineUtils.fs
@@ -1,7 +1,9 @@
 module PipelineUtils

   
 let dafnyScratchFile = @"c:\tmp\jennisys-scratch.dfy"
-let dafnyModelFile = @"c:\tmp\jennisys-scratch.model"
+let dafnyVerifyFile = @"c:\tmp\jennisys-verify.dfy"
+let dafnyModelFile = @"c:\tmp\jennisys-scratch.bvd"
+let dafnyVerifyModelFile = @"c:\tmp\jennisys-verify.bvd"
 let dafnyOutFile = @"c:\tmp\jennisys-scratch.out"
 let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy"
 
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 97b537db..5410db31 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -1,6 +1,7 @@
 module Printer
 
 open Ast
+open AstUtils
 
 let newline = System.Environment.NewLine // "\r\n"
 
@@ -79,15 +80,6 @@ let PrintSig signature =
         else ""
       sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
 
-let rec SplitIntoConjunts expr = 
-  match expr with
-  | IdLiteral("true") -> []
-  | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
-  | _ -> [expr]
-
-let rec ForeachConjunct f expr =
-  SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""
-
 let rec Indent i =
   if i = 0 then "" else " " + (Indent (i-1))
 
diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen
index 5c95e20f..771fe680 100644
--- a/Jennisys/Jennisys/examples/List2.jen
+++ b/Jennisys/Jennisys/examples/List2.jen
@@ -8,9 +8,7 @@ class IntList {
     ensures list = [2]
 
   constructor OneTwo()
-    ensures |list| = 2
-    ensures list[0] = 1
-    ensures list[1] = 2
+    ensures list = [1] + [2]
 }
 
 model IntList {
diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen
index 1b6cef80..13ed2878 100644
--- a/Jennisys/Jennisys/examples/List3.jen
+++ b/Jennisys/Jennisys/examples/List3.jen
@@ -8,9 +8,7 @@ class IntList {
     ensures list = [2]
 
   constructor OneTwo()
-    ensures |list| = 2
-    ensures list[0] = 1
-    ensures list[1] = 2
+    ensures list = [1] + [2] 
 }
 
 model IntList {
@@ -23,7 +21,7 @@ model IntList {
     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)))
+                      (forall i:int :: (0 <= i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data)))
 }
 
 class IntNode {
@@ -36,7 +34,7 @@ class IntNode {
 
   constructor OneTwo()
     ensures data = 1
-    ensures |succ| = 1 && succ[0] != null && succ[0].data = 1
+    ensures |succ| = 1 && succ[0] != null && succ[0].data = 2
 
   invariant
     !(null in succ)