Jennisys:

   - added "inferConds" cmd line option
   - refactored out some pieces of code into their own functions

6 files changed, 52 insertions, 40 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index b8416c93..3577379e 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -85,8 +85,17 @@ 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

@@ -96,33 +105,11 @@ let GetUnifications indent expr args heapInst =
     let builder = new CascadingBuilder<_>(unifMap)

     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 unifMap

     }

-  // 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

 

@@ -294,9 +280,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 +290,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 = 

@@ -409,11 +398,11 @@ let Modularize prog solutions =
         let newAcc = acc |> Map.add (fst newSol) (snd newSol)

         __Modularize newAcc rest

     | [] -> acc

-  (* --- --- *) 

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

   __Modularize Map.empty (Map.toList solutions)

 

 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..49696e58 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/List.jen /method:List.Double /genRepr</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]