- changed heapInst.assignments' type from Map to List (because assignment order can matter)

 - fixed a bug in the piece of code for desugaring quantifiers

8 files changed, 78 insertions, 27 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 2bbd43cf..b8416c93 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -174,7 +174,7 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
                 | Some(expr) -> Some(Dot(expr, fldName))

                 | None -> __fff rest

             | [] -> None

-          let backPointers = heapInst.assignments |> Map.filter (fun (_,_) l -> l = ObjLiteral(objRefName)) |> Map.toList

+          let backPointers = heapInst.assignments |> List.filter (fun ((_,_),l) -> l = ObjLiteral(objRefName))

           __fff backPointers 

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

   if objRef2ExprCache.ContainsKey(objRefName) then

@@ -218,15 +218,15 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
   match unifs with

   | (e,c) :: rest -> 

       let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative

-      let newHeap = heapInst.assignments|> Map.fold (fun acc (o,f) value ->

+      let newHeap = heapInst.assignments|> List.fold (fun acc ((o,f),value) ->

                                                        if value = Const2Expr c then

                                                          if __CheckUnif o.name f e -1 then                                                

                                                            // change the value to expression

                                                            //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

-                                                           acc |> Map.add (o,f) e

+                                                           Utils.ListMapAdd (o,f) e acc 

                                                          else

                                                            // don't change the value unless "conservative = false"

-                                                           acc |> Map.add (o,f) value

+                                                           Utils.ListMapAdd (o,f) value acc

                                                        else 

                                                          let rec __UnifyOverLst lst cnt =

                                                                match lst with

@@ -243,13 +243,14 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
                                                          match value with

                                                          | SequenceExpr(elist) -> 

                                                              let newExprList = __UnifyOverLst elist 0

-                                                             acc |> Map.add (o,f) (SequenceExpr(newExprList))

+                                                             Utils.ListMapAdd (o,f) (SequenceExpr(newExprList)) acc

                                                          | SetExpr(elist) ->

                                                              let newExprList = __UnifyOverLst elist 0

-                                                             acc |> Map.add (o,f) (SetExpr(newExprList))

+                                                             Utils.ListMapAdd (o,f) (SetExpr(newExprList)) acc

                                                          | _ -> 

-                                                             acc |> Map.add (o,f) value

+                                                             Utils.ListMapAdd (o,f) value acc

                                                      ) heapInst.assignments

+                                        |> List.rev

       {heapInst with assignments = newHeap }

   | [] -> heapInst

 

@@ -316,7 +317,7 @@ and TryInferConditionals indent prog comp m unifs heapInst =
   //   - go through all objects on the heap and assert their invariants  

   let pre,post = GetMethodPrePost m

   let prepostExpr = post //TODO: do we need the "pre" here as well?

-  let heapObjs = heapInst2.assignments |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

+  let heapObjs = heapInst2.assignments |> List.fold (fun acc ((o,_),_) -> acc |> Set.add o) Set.empty

   let expr = heapObjs |> Set.fold (fun acc o -> 

                                      let receiverOpt = GetObjRefExpr o.name heapInst2

                                      let receiver = Utils.ExtractOption receiverOpt

@@ -387,7 +388,7 @@ let GetMethodsToAnalyze prog =
 /// Goes through a given list of methods of the given program and attempts to 

 /// synthesize code for each one of them.

 ///

-/// Returns a map from (component * method) |--> (heap,env,ctx)

+/// Returns a map from (component * method) |--> Expr * HeapInstance

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

 let rec AnalyzeMethods prog members = 

   match members with

@@ -400,14 +401,35 @@ let rec AnalyzeMethods prog members =
       | _ -> AnalyzeMethods prog rest

   | [] -> Map.empty

 

+let Modularize prog solutions = 

+  let rec __Modularize acc sols = 

+    match sols with

+    | sol :: rest -> 

+        let newSol = sol

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

+        __Modularize newAcc rest

+    | [] -> acc

+  (* --- --- *) 

+  __Modularize Map.empty (Map.toList solutions)

+

 let Analyze prog filename =

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

+  let __PrintSolution outFileName solutions = 

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

+    file.AutoFlush <- true  

+    let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr

+    fprintfn file "%s" synthCode

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

   let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)

   let progName = System.IO.Path.GetFileNameWithoutExtension(filename)

-  use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName))

-  file.AutoFlush <- true

+  let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName)

   Logger.InfoLine "Printing synthesized code"

-  let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr

-  fprintfn file "%s" synthCode

+  __PrintSolution outFlatSolFileName solutions

+  // try to modularize

+  let modularSolutions = Modularize prog solutions

+  let outModSolFileName = dafnyModularSynthFileNameTemplate.Replace("###", progName)

+  Logger.InfoLine "Printing modularized code"

+  __PrintSolution outModSolFileName modularSolutions

   ()

 

 //let AnalyzeComponent_rustan c =

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 8322d1a7..cf008458 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -687,11 +687,11 @@ let rec Desugar expr =
   | SetExpr(_)     

   | SequenceExpr(_)        -> expr 

   // 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)) when vn1 = vn2 ->

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

       match rhsCol with 

       | SetExpr(elist)

       | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral

-      | _ -> ForallExpr(v, Desugar sub)

+      | _ -> ForallExpr(v, Desugar ee)

   | ForallExpr(v,e)        -> ForallExpr(v, Desugar e)

   | UnaryExpr(op,e)        -> UnaryExpr(op, Desugar e)

   | IteExpr(c,e1,e2)       -> IteExpr(c, Desugar e1, Desugar e2)

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 6b53112e..54c22053 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -147,7 +147,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =
 

 let PrintAllocNewObjects heapInst indent = 

   let idt = Indent indent

-  heapInst.assignments |> Map.fold (fun acc (obj,fld) _ ->

+  heapInst.assignments |> List.fold (fun acc ((obj,fld),_) ->

                                       if not (obj.name = "this") then

                                         acc |> Set.add obj

                                       else 

@@ -157,7 +157,7 @@ let PrintAllocNewObjects heapInst indent =
 

 let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

-  heapInst.assignments |> Map.fold (fun acc (o,f) e ->

+  heapInst.assignments |> List.fold (fun acc ((o,f),e) ->

                                       let fldName = PrintVarName f

                                       let value = PrintExpr 0 e

                                       acc + (sprintf "%s%s.%s := %s;" idt o.name fldName value) + newline

@@ -165,11 +165,11 @@ let PrintVarAssignments heapInst indent =
 

 let PrintReprAssignments prog heapInst indent = 

   let __FollowsFunc o1 o2 = 

-    heapInst.assignments |> Map.fold (fun acc (srcObj,fld) value -> 

+    heapInst.assignments |> List.fold (fun acc ((srcObj,fld),value) -> 

                                         acc || (srcObj = o1 && value = ObjLiteral(o2.name))

                                      ) false

   let idt = Indent indent

-  let objs = heapInst.assignments |> Map.fold (fun acc (obj,fld) _ -> acc |> Set.add obj) Set.empty

+  let objs = heapInst.assignments |> List.fold (fun acc ((obj,fld),_) -> acc |> Set.add obj) Set.empty

                                   |> Set.toList

                                   |> Utils.TopSort __FollowsFunc

                                   |> List.rev

@@ -181,7 +181,7 @@ let PrintReprAssignments prog heapInst indent =
                                             let! comp = FindComponent prog typeName

                                             let vars = GetFrameFields comp

                                             let nonNullVars = vars |> List.filter (fun v -> 

-                                                                                      match Map.tryFind (obj,v) heapInst.assignments with

+                                                                                      match Utils.ListMapTryFind (obj,v) heapInst.assignments with

                                                                                       | Some(ObjLiteral(n)) when not (n = "null") -> true

                                                                                       | _ -> false)

                                             return nonNullVars |> List.fold (fun a v -> 

diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 604f02f8..72c50b44 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -9,6 +9,7 @@ open System.IO
 open Microsoft.FSharp.Text.Lexing
 
 open Ast
+open AstUtils
 open Lexer
 open Options
 open Parser
@@ -52,4 +53,7 @@ with
   | InvalidCmdLineOption(msg) 
   | InvalidCmdLineArg(msg) as ex -> 
       printfn "  [ERROR] %s" msg; 
-      printfn "%s" PrintHelpMsg
\ No newline at end of file
+      printfn "%s" PrintHelpMsg
+  | EvalFailed(msg) as ex -> 
+      printfn "  [EVALUATION ERROR]  %s" msg
+      printfn "%O" ex.StackTrace 
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index b88b6330..082a54e1 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,8 +23,8 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

-    <StartArguments>

-    </StartArguments>

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

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

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs
index 1439018a..7d0b3e55 100644
--- a/Jennisys/Jennisys/PipelineUtils.fs
+++ b/Jennisys/Jennisys/PipelineUtils.fs
@@ -11,6 +11,7 @@ let dafnyScratchSuffix = "scratch"
 let dafnyVerifySuffix = "verify"

 let dafnyUnifSuffix = "unif"

 let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy"

+let dafnyModularSynthFileNameTemplate = @"c:\tmp\jennisys-synth_###_mod.dfy"

 

 let mutable lastDafnyExitCode = 0 //TODO: how to avoid this muttable state?

 

diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
index 64f80584..c4bd99a2 100644
--- a/Jennisys/Jennisys/Resolver.fs
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -16,7 +16,7 @@ open DafnyModelUtils
 type Obj = { name: string; objType: Type }

 

 type HeapInstance = {

-   assignments: Map<Obj * VarDecl, Expr>; // the first string is the symbolic name of an object literal

+   assignments: ((Obj * VarDecl) * Expr) list; // the first string is the symbolic name of an object literal

    methodArgs: Map<string, Const>;

    globals: Map<string, Expr>;

 }

@@ -99,7 +99,7 @@ let Eval heapInst resolveVars expr =
         let discr = __EvalResolver e

         match discr with

         | ObjLiteral(objName) -> 

-            let h2 = heapInst.assignments |> Map.filter (fun (o,Var(fldName,_)) v -> o.name = objName && fldName = str) |> Map.toList

+            let h2 = heapInst.assignments |> List.filter (fun ((o, Var(fldName,_)), v) -> o.name = objName && fldName = str)

             match h2 with

             | ((_,_),x) :: [] -> x

             | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName str))

@@ -123,8 +123,9 @@ let ResolveModel hModel =
                                                                | _ -> failwith ("unresolved object ref: " + o.ToString())

                                         let objType = objType |> Utils.ExtractOptionMsg "unknown object type"

                                         let value = TryResolve hModel l |> Const2Expr

-                                        acc |> Map.add ({name = objName; objType = objType}, f) value 

-                                     ) Map.empty

+                                        Utils.ListMapAdd ({name = objName; objType = objType}, f) value acc 

+                                     ) []

+                         |> List.rev

   let argmap = hModel.env |> Map.fold (fun acc k v -> 

                                          match k with

                                          | VarConst(name) -> acc |> Map.add name (Resolve hModel v)

diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index c9f18e23..6a6213fd 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -138,6 +138,29 @@ let rec GenList n e =
 let ListReplace oldElem newElem lst = 

   lst |> List.choose (fun e -> if e = oldElem then Some(newElem) else Some(e))

 

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

+/// if (exists (k,v) :: (k,v) in lst && k = key) then

+///   ret = Some(v)

+/// else

+///   ret = None

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

+let ListMapTryFind key lst = 

+  let filtered = lst |> List.filter (fun (k,v) -> k = key)

+  match filtered with

+  | fs :: rest -> Some(snd fs)

+  | [] -> None

+

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

+/// Replaces the first occurence of the given key in 

+/// the given list with the given value, or appends 

+/// (key,value) if key does not exist in the list

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

+let rec ListMapAdd key value lst = 

+  match lst with

+  | (k,v) :: rest -> if k = key then (k, value) :: rest else (k,v) :: (ListMapAdd key value rest)

+  | [] -> [(key,value)]

+  

+

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

 /// ensures: ret = elem in lst

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