Jennisys:

  - added "modifiable objects" to heap instance
  - when verifying synthesized program, only fields of the modifiable
    objects are considered

13 files changed, 101 insertions, 41 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index a98fa057..cea90d0e 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -89,6 +89,7 @@ let rec IsArgsOnly args expr =
   | IdLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

   | Dot(e,_)

   | SeqLength(e)

+  | LCIntervalExpr(e)

   | UnaryExpr(_,e)                       -> __IsArgsOnlyLst [e]

   | SelectExpr(e1, e2)

   | BinaryExpr(_,_,e1,e2)                -> __IsArgsOnlyLst [e1; e2]

@@ -111,7 +112,6 @@ let AddUnif indent e v unifMap =
 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

   // - then it tries to evaluate it to a constant

   // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map

   let __AddUnif e unifsAcc =

@@ -320,6 +320,17 @@ let FixSolution origComp origMeth sol =
                       else 

                         acc |> Map.add (cc,mm) v) Map.empty

 

+//

+let DontResolveUnmodifiableStuff prog comp meth expr =

+  let methodArgs = GetMethodInArgs meth

+  let __IsMethodArg argName = methodArgs |> List.exists (fun (Var(vname,_)) -> vname = argName)

+  let isConstr = match meth with Method(_,_,_,_,b) -> b | _ -> false

+  match expr with

+  | VarLiteral(id) when __IsMethodArg id -> false 

+  | IdLiteral(id) when not (id = "this" || id = "null") -> isConstr

+  | Dot(lhs, fldName) -> isConstr

+  | _ -> true

+

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

 /// Attempts to synthesize the initialization code for the given constructor "m"

 ///

@@ -351,7 +362,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
         Logger.InfoLine " OK "

         let model = models.[0]

         let hModel = ReadFieldValuesFromModel model prog comp m

-        let heapInst = ResolveModel hModel (GetMethodOutArgs m)

+        let heapInst = ResolveModel hModel m

         let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList

         let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

@@ -379,10 +390,9 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

   let methodArgs = GetMethodInArgs m

-  let __IsMethodArg argName = methodArgs |> List.exists (fun (Var(vname,_)) -> vname = argName)

   let expr = GetHeapExpr prog m heapInst2

   // now evaluate and see what's left

-  let newCond = Eval heapInst2 (function VarLiteral(id) when __IsMethodArg id -> false | _ -> true) expr

+  let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

   if newCond = TrueLiteral then

     Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

     wrongSol

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index d0ad5310..cad5352c 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -38,6 +38,7 @@ type Expr =
   | Star

   | Dot of Expr * string

   | UnaryExpr of string * Expr

+  | LCIntervalExpr of Expr

   | BinaryExpr of int * string * Expr * Expr

   | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr

   | SelectExpr of Expr * Expr

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 8ac62606..e37f461a 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -32,6 +32,7 @@ let rec Rewrite rewriterFunc expr =
   | Dot(e, id)                       -> Dot(__RewriteOrRecurse e, id)

   | ForallExpr(vars,e)               -> ForallExpr(vars, __RewriteOrRecurse e)   

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

+  | LCIntervalExpr(e)                -> LCIntervalExpr(__RewriteOrRecurse e)

   | SeqLength(e)                     -> SeqLength(__RewriteOrRecurse e)

   | SelectExpr(e1, e2)               -> SelectExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2)

   | BinaryExpr(p,op,e1,e2)           -> BinaryExpr(p, op, __RewriteOrRecurse e1, __RewriteOrRecurse e2)

@@ -104,6 +105,7 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | IdLiteral(_)                     -> leafVal

   | Dot(e, _)

   | ForallExpr(_,e)

+  | LCIntervalExpr(e)

   | UnaryExpr(_,e)           

   | SeqLength(e)                     -> __Compose (e :: [])

   | SelectExpr(e1, e2)

@@ -128,6 +130,7 @@ let rec DescendExpr2 visitorFunc expr acc =
   | IdLiteral(_)                     -> newAcc

   | Dot(e, _)

   | ForallExpr(_,e)

+  | LCIntervalExpr(e)

   | UnaryExpr(_,e)           

   | SeqLength(e)                     -> __Pipe (e :: [])

   | SelectExpr(e1, e2)

@@ -592,11 +595,19 @@ let rec __EvalSym resolverFunc ctx expr =
       let rcv' = __EvalSym resolverFunc ctx rcv

       let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev

       MethodCall(rcv', cname, mname, aparams')

+  | LCIntervalExpr(_) -> expr

   | SelectExpr(lst, idx) ->

       let lst' = __EvalSym resolverFunc ctx lst

       let idx' = __EvalSym resolverFunc ctx idx 

       match lst', idx' with

       | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

+      | SequenceExpr(elist), LCIntervalExpr(startIdx) ->

+          let startIdx' = __EvalSym resolverFunc ctx startIdx

+          match startIdx' with

+          | IntLiteral(startIdxInt) -> 

+              let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l)

+              SequenceExpr(__Skip startIdxInt elist)

+          | _ -> SelectExpr(lst', idx')

       | _ -> SelectExpr(lst', idx')

   | UpdateExpr(lst,idx,v) ->

       let lst', idx', v' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx, __EvalSym resolverFunc ctx v

@@ -829,6 +840,7 @@ let MyDesugar expr removeOriginal =
         | SequenceExpr(elist) -> elist |> List.fold (fun acc e -> BinaryAnd acc (__Desugar (Substitute (VarLiteral(vn2)) e sub))) TrueLiteral

         | _ -> ForallExpr(v, __Desugar ee)

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

+    | LCIntervalExpr(e)      -> LCIntervalExpr(__Desugar e)

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

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

     // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an && |lst| = n

@@ -884,6 +896,7 @@ let ChangeThisReceiver receiver expr =
     | Dot(e, id)                           -> Dot(__ChangeThis locals e, id)

     | ForallExpr(vars,e)                   -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

                                               ForallExpr(vars, __ChangeThis newLocals e)   

+    | LCIntervalExpr(e)                    -> LCIntervalExpr(__ChangeThis locals e)

     | UnaryExpr(op,e)                      -> UnaryExpr(op, __ChangeThis locals e)

     | SeqLength(e)                         -> SeqLength(__ChangeThis locals e)

     | SelectExpr(e1, e2)                   -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)

@@ -902,3 +915,12 @@ let rec ExtractTopLevelExpressions stmt =
   | Assign(e1, e2) -> [e1; e2]

   | Block(slist)   -> slist |> List.fold (fun acc s -> acc @ ExtractTopLevelExpressions s) [] 

 

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

+/// Very simple for now: 

+///   - if "m" is a constructor, everything is modifiable

+///   - otherwise, all objects are immutable (TODO: instead it should read the "modifies" clause of a method and figure out what's modifiable from there)

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

+let IsModifiableObj obj m = 

+  match m with

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

+  | _ -> failwithf "expected a Method but got %O" m
\ No newline at end of file
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 9c2dca77..8414c8ce 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -222,32 +222,43 @@ let PrintReprAssignments prog heapInst indent =
   else

     ""

                                                           

-let rec PrintHeapCreationCode prog sol indent genRepr =    

+let rec PrintHeapCreationCode prog sol indent genRepr =

+  /// just removes all FieldAssignments to unmodifiable objects    

+  let __RemoveUnmodifiableStuff heapInst = 

+    let newAsgs = heapInst.assignments |> List.fold (fun acc a ->

+                                                       match a with

+                                                       | FieldAssignment((obj,_),_) when not (Set.contains obj heapInst.modifiableObjs) ->

+                                                           acc

+                                                       | _ -> acc @ [a]

+                                                    ) []

+    { heapInst with assignments = newAsgs }

+

   let idt = Indent indent

   match sol with

-  | (c, heapInst) :: rest ->

+  | (c, hi) :: rest ->

+      let heapInstMod = __RemoveUnmodifiableStuff hi

       let __ReprAssignments ind = 

         if genRepr then

-          (PrintReprAssignments prog heapInst ind)

+          (PrintReprAssignments prog heapInstMod ind)

         else 

           ""

       if c = TrueLiteral then

-        (PrintAllocNewObjects heapInst indent) +

-        (PrintVarAssignments heapInst indent) +

+        (PrintAllocNewObjects heapInstMod indent) +

+        (PrintVarAssignments heapInstMod indent) +

         (__ReprAssignments indent) +

         (PrintHeapCreationCode prog rest indent genRepr) 

       else

         if List.length rest > 0 then

           idt + "if (" + (PrintExpr 0 c) + ") {" + newline +

-          (PrintAllocNewObjects heapInst (indent+2)) +

-          (PrintVarAssignments heapInst (indent+2)) +

+          (PrintAllocNewObjects heapInstMod (indent+2)) +

+          (PrintVarAssignments heapInstMod (indent+2)) +

           (__ReprAssignments (indent+2)) +

           idt + "} else {" + newline + 

           (PrintHeapCreationCode prog rest (indent+2) genRepr) +

           idt + "}" + newline

         else 

-          (PrintAllocNewObjects heapInst indent) +

-          (PrintVarAssignments heapInst indent) +

+          (PrintAllocNewObjects heapInstMod indent) +

+          (PrintVarAssignments heapInstMod indent) +

           (__ReprAssignments indent)

   | [] -> ""

 

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 73b9415a..df20fc4b 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -32,9 +32,10 @@ let rec PrintExpr ctx expr =
       sprintf "%s%s" decl vars

   | Star -> "*"

   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id

+  | LCIntervalExpr(e) -> sprintf "%s.." (PrintExpr 90 e)

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)

-  | BinaryExpr(strength,"in",lhs,BinaryExpr(_,"..",lo,hi)) ->

+  | BinaryExpr(strength,"in",lhs,BinaryExpr(_,"...",lo,hi)) ->

       let needParens = strength <= ctx

       let openParen = if needParens then "(" else ""

       let closeParen = if needParens then ")" else ""

diff --git a/Jennisys/Lexer.fsl b/Jennisys/Lexer.fsl
index d1b8ad91..9186e957 100644
--- a/Jennisys/Lexer.fsl
+++ b/Jennisys/Lexer.fsl
@@ -38,8 +38,9 @@ rule tokenize = parse
 | "seq"          { SEQTYPE }

 | "set"          { SETTYPE }

 // Operators

-| "."      { DOT }

+| "..."    { DOTDOTDOT }

 | ".."     { DOTDOT }

+| "."      { DOT }

 | "+"      { PLUS }

 | "-"      { MINUS }

 | "*"      { STAR }

diff --git a/Jennisys/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index af59799e..f12e8dd0 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/Jennisys/MethodUnifier.fs
@@ -203,18 +203,15 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
         Logger.DebugLine (idt + "      Unifications: ")

         let idtt = idt + "        "

         unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug 

-//        let ins,outs = ApplyMethodUnifs m' unifs

-//        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', ins)

-//        let obj = { name = "this"; objType = GetClassType comp }

-//        let var = Var("", None)

-//        let body = [FieldAssignment((obj,var), delegateCall)]

         let obj = { name = "this"; objType = GetClassType comp }

+        let modObjs = if IsModifiableObj obj m then Set.singleton obj else Set.empty

         let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs

-        let hInst = { objs        = Utils.MapSingleton obj.name obj;

-                      assignments = body; 

-                      methodArgs  = Map.empty; 

-                      methodRetVals = Map.empty;

-                      globals     = Map.empty }

+        let hInst = { objs           = Utils.MapSingleton obj.name obj;

+                      modifiableObjs = modObjs;

+                      assignments    = body; 

+                      methodArgs     = Map.empty; 

+                      methodRetVals  = Map.empty;

+                      globals        = Map.empty }

         Some(Map.empty |> Map.add (comp,m) [cond, hInst]

                        |> Map.add (comp,m') [])

     | None -> None
\ No newline at end of file
diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 2dd1eb35..0cf9dba9 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -21,7 +21,7 @@ let rec MyFold ee acc =
 %token NOT

 %token STAR DIV MOD

 %token PLUS MINUS

-%token DOTDOT

+%token DOTDOT DOTDOTDOT

 %token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN

 %token AND OR

 %token IMPLIES

@@ -164,8 +164,8 @@ Expr40:
     | Expr50 NOTIN Expr50   { BinaryExpr(40,"!in",$1,$3) }

     

 Expr50:

-    | Expr55                { $1 }

-    | Expr55 DOTDOT Expr55  { BinaryExpr(50,"..",$1,$3) }

+    | Expr55                   { $1 }

+    | Expr55 DOTDOTDOT Expr55  { BinaryExpr(50,"...",$1,$3) }        

 

 Expr55:

     | Expr60               { $1 }

@@ -182,6 +182,7 @@ Expr90:
   | Expr100           { $1 }

   | NOT Expr90        { UnaryExpr("!", $2) }

   | MINUS Expr90      { UnaryExpr("-", $2) }

+  | Expr90 DOTDOT     { LCIntervalExpr($1) }

 

 Expr100:

   | INTEGER                                  { IntLiteral($1) }

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index cb9fb06e..95638ea5 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -32,6 +32,7 @@ let rec PrintExpr ctx expr =
       sprintf "%s%s" decl vars

   | Star              -> "*"

   | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id

+  | LCIntervalExpr(e) -> sprintf "%s.." (PrintExpr 90 e)

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)

   | BinaryExpr(strength,op,e0,e1) ->

diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index b86b782f..d38fbf7b 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -21,6 +21,7 @@ type AssignmentType =
 

 type HeapInstance = {

    objs: Map<string, Obj>;

+   modifiableObjs: Set<Obj>;

    assignments: AssignmentType list

    methodArgs: Map<string, Const>;

    methodRetVals: Map<string, Expr>;

@@ -136,7 +137,8 @@ let Eval heapInst resolveExprFunc expr =
 /// (HeapInstance), where all fields for all objects have explicit 

 /// assignments.

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

-let ResolveModel hModel outArgs = 

+let ResolveModel hModel meth = 

+  let outArgs = GetMethodOutArgs meth

   let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->

                                         let objName, objTypeOpt = match Resolve hModel o with

                                                                   | ThisConst(_,t) -> "this", t;

@@ -148,10 +150,18 @@ let ResolveModel hModel outArgs =
                                         Utils.ListMapAdd (obj, f) value acc 

                                      ) []

                          |> List.map (fun el -> FieldAssignment(el))

-  let objs = hmap |> List.fold (fun acc asgn -> 

-                                  match asgn with

-                                  | FieldAssignment((obj,_),_) -> acc |> Map.add obj.name obj

-                                  | _ -> acc) Map.empty

+  let objs, modObjs = hmap |> List.fold (fun (acc1,acc2) asgn -> 

+                                           match asgn with

+                                           | FieldAssignment((obj,_),_) -> 

+                                               let acc1' = acc1 |> Map.add obj.name obj

+                                               let acc2' = 

+                                                 if IsModifiableObj obj meth then

+                                                   acc2 |> Set.add obj

+                                                 else

+                                                   acc2

+                                               acc1',acc2'

+                                           | _ -> acc1,acc2

+                                        ) (Map.empty, Set.empty)

   let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> 

                                                   match k with

                                                   | VarConst(name) -> 

@@ -161,11 +171,12 @@ let ResolveModel hModel outArgs =
                                                         acc1 |> Map.add name (Resolve hModel v), acc2

                                                   | _ -> acc1, acc2

                                                ) (Map.empty, Map.empty)

-  { objs          = objs;

-    assignments   = hmap; 

-    methodArgs    = argmap; 

-    methodRetVals = retvals;

-    globals       = Map.empty }

+  { objs           = objs;

+    modifiableObjs = modObjs;

+    assignments    = hmap; 

+    methodArgs     = argmap; 

+    methodRetVals  = retvals;

+    globals        = Map.empty }

 

 let rec GetCallGraph solutions graph = 

   let rec __SearchExprsForMethodCalls elist acc = 

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index a7ba26ed..ca21b65b 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -37,6 +37,10 @@ class Node[T] {
   method List() returns (lst: seq[T])
     requires |list| = 1
     ensures lst = list
+
+  method Tail() returns (tail: Node[T])
+    ensures |list| = 1 ==> tail = null
+    ensures |list| > 1 ==> tail != null && tail.list = list[1..]
 }
 
 model Node[T] {
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index f9828741..3900b1d1 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -33,7 +33,7 @@ model IntList {
     root = null  ==> |list| = 0
     root != null ==> (|list| = |root.succ| + 1 && 
                       list[0] = root.data && 
-                      (forall i :: i in 1 .. |root.succ| ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
+                      (forall i :: i in 1 ... |root.succ| ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
 }
 
 class IntNode {
diff --git a/Jennisys/examples/Number.jen b/Jennisys/examples/Number.jen
index be33a00e..ce76c09c 100644
--- a/Jennisys/examples/Number.jen
+++ b/Jennisys/examples/Number.jen
@@ -26,11 +26,11 @@ class Number {
     ensures num in {a b c}
     ensures forall x :: x in {a b c} ==> num <= x
 
- constructor MinSum(a: int, b: int, c: int)
+  constructor MinSum(a: int, b: int, c: int)
     ensures num in {a+b a+c b+c}
     ensures num <= a+b && num <= b+c && num <= a+c
 
- constructor Min4(a: int, b: int, c: int, d: int)
+  constructor Min4(a: int, b: int, c: int, d: int)
     ensures num in {a b c d}
     ensures forall x :: x in {a b c d} ==> num <= x