Jennisys: added some more simple methods in Simple.jen, implemented a couple of

optimiations/exensions

7 files changed, 105 insertions, 49 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index a17a7bfd..7b60104a 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -108,10 +108,10 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
                 | Some(expr) -> Some(Dot(expr, GetExtVarName var))

                 | None -> __fff rest

             | [] -> None

-          let backPointers = heapInst.assignments |> List.choose (function 

-                                                                    FieldAssignment (x,l) -> 

-                                                                      if l = ObjLiteral(objRefName) then Some(x,l) else None

-                                                                    |_ -> None)

+          let backPointers = heapInst.concreteValues |> List.choose (function 

+                                                                        FieldAssignment (x,l) -> 

+                                                                          if l = ObjLiteral(objRefName) then Some(x,l) else None

+                                                                        |_ -> None)

           __fff backPointers 

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

   __GetObjRefExpr objRefName (Set.empty)

@@ -156,7 +156,7 @@ let GetHeapExpr prog mthd heapInst includePreState =
                       ) prepostExpr

 

 let IsUnmodConcrOnly prog (comp,meth) expr = 

-  let isConstr = IsConstructor meth

+  let isConstr = IsModifiableObj (ThisObj comp) (comp,meth)

   let rec __IsUnmodOnly args expr = 

     let __IsUnmodOnlyLst elist = 

       elist |> List.fold (fun acc e -> acc && (__IsUnmodOnly args e)) true

@@ -382,13 +382,13 @@ let rec DiscoverAliasing exprList heapInst =
 let DontResolveUnmodifiableStuff prog comp meth expr =

   let methodArgs = GetMethodInArgs meth

   let __IsMethodArg argName = methodArgs |> List.exists (fun var -> GetExtVarName var = argName)

-  let isConstr = IsConstructor meth

+  let isMod = IsModifiableObj (ThisObj comp) (comp,meth)

   match expr with

   | VarLiteral(id) when __IsMethodArg id -> false 

   | IdLiteral(id) when id = "this" || id = "null" -> true

   | IdLiteral(id) | Dot(_, id) -> 

-      // this must be a field, so resolve it only if constructor

-      isConstr

+      // this must be a field, so resolve it only if modifiable

+      isMod

   | _ -> true

 

 /// Descends down a given expression and returns bunch of sub-expressions that all evaluate to true

@@ -405,8 +405,8 @@ let FindClauses trueOnly resolverFunc heapInst expr =
           | _ ->

               let exprAllResolved = EvalFull heapInst expr

               match exprAllResolved with

-              | BoolLiteral(true) -> acc @ [exprEval]

-              | BoolLiteral(false) -> if trueOnly then acc else acc @ [UnaryNot exprEval]

+              | BoolLiteral(true) -> acc @ (exprEval |> SplitIntoConjunts)

+              | BoolLiteral(false) -> if trueOnly then acc else acc @ (UnaryNot exprEval |> SplitIntoConjunts)

               | _ -> acc

     with

     | _ -> acc

@@ -528,36 +528,30 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
   /// checks whether an expression is ok, meaning 

   ///   - only immediate concrete fields of the "this" object are used,

   ///   - no recursion on the same object with the same parameters

-  ///   - not a constant

   let __IsOk hInst expr = 

     let compName = GetComponentName comp

     let methName = GetMethodName m

-    try

-      expr |> EvalNone hInst |> Expr2Const |> ignore

-      false

-    with

-    | _ -> 

-        let myVisitor = 

-          fun expr acc ->

-            if not acc then

-              false

-            else

-              match expr with

-              | Dot(discr, fldName) -> 

-                  let obj = EvalFull heapInst discr

-                  match obj with 

-                  | ObjLiteral(id) when id = "this" -> 

-                      try 

-                        let fname = RenameFromOld fldName

-                        IsConcreteField (InferType prog comp (MethodArgChecker prog m) discr |> Utils.ExtractOption) fname

-                      with

-                        | _ -> false

-                  | ObjLiteral(id) -> false

-                  | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"

-              | MethodCall(receiver, cn, mn, elst) when receiver = ThisLiteral && cn = compName && mn = methName -> 

-                  elst |> List.exists (function VarLiteral(_) -> false | _ -> true)

-              | _ -> true                          

-        DescendExpr2 myVisitor expr true

+    let myVisitor = 

+        fun expr acc ->

+        if not acc then

+            false

+        else

+            match expr with

+            | Dot(discr, fldName) -> 

+                let obj = EvalFull heapInst discr

+                match obj with 

+                | ObjLiteral(id) when id = "this" -> 

+                    try 

+                    let fname = RenameFromOld fldName

+                    IsConcreteField (InferType prog comp (MethodArgChecker prog m) discr |> Utils.ExtractOption) fname

+                    with

+                    | _ -> false

+                | ObjLiteral(id) -> false

+                | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"

+            | MethodCall(receiver, cn, mn, elst) when receiver = ThisLiteral && cn = compName && mn = methName -> 

+                elst |> List.exists (function VarLiteral(_) -> false | _ -> true)

+            | _ -> true                          

+    DescendExpr2 myVisitor expr true

 

   /// Finds all modifiable fields in a given hInst, and checks if an "ok" 

   /// expression exists for each one of them.

@@ -697,13 +691,12 @@ and TryRecursion indent prog comp m unifs heapInst callGraph =
       | IdLiteral(_) -> true

       | Dot(_,_) -> true

       | _ -> false     

-//      let str = PrintExpr 0 l

-//      str.Contains("ret")

-

     match e with

     | BinaryExpr(_,"=",l,_) -> 

         //TODO: it should really check both lhs and rhs

         __CheckExpr l

+    | BinaryExpr(_,op,l,_) when IsRelationalOp op ->

+        __CheckExpr l

     | _ -> __CheckExpr e

 

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index a3e1e807..4b5ad7bd 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -447,6 +447,18 @@ let rec Expr2Const e =
   | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList)

   | _ -> failwithf "Not a constant: %O" e

 

+let rec Expr2ConstStrict e =

+  match e with

+  | IntLiteral(n) -> IntConst(n)

+  | BoolLiteral(b) -> BoolConst(b)

+  | BoxLiteral(id) -> BoxConst(id)

+  | ObjLiteral("this") -> ThisConst("this",None)

+  | ObjLiteral("null") -> NullConst

+  | ObjLiteral(name) -> NewObj(name, None)

+  | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2ConstStrict)

+  | SetExpr(elist) -> SetConst(elist |> List.map Expr2ConstStrict |> Set.ofList)

+  | _ -> failwithf "Not a constant: %O" e

+

 let TryExpr2Const e =

   try 

     Some(Expr2Const e)

@@ -688,12 +700,28 @@ let EvalSym2 fullResolverFunc otherResolverFunc returnFunc ctx expr =
           | "in" -> 

               match e1'.Force(), e2'.Force() with

               | _, SetExpr(s)       

-              | _, SequenceExpr(s)  -> BoolLiteral(Utils.ListContains (e1'.Force()) s)

+              | _, SequenceExpr(s)  -> //BoolLiteral(Utils.ListContains (e1'.Force()) s)

+                  if Utils.ListContains (e1'.Force()) s then

+                    TrueLiteral

+                  else

+                    try 

+                      let contains = s |> List.map Expr2ConstStrict |> Utils.ListContains (e1'.Force() |> Expr2ConstStrict)

+                      BoolLiteral(contains)

+                    with

+                    | _ -> recomposed.Force()

               | _ -> recomposed.Force()

           | "!in" -> 

               match e1'.Force(), e2'.Force() with

               | _, SetExpr(s)       

-              | _, SequenceExpr(s)  -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s))

+              | _, SequenceExpr(s)  -> //BoolLiteral(not (Utils.ListContains (e1'.Force()) s))

+                  if Utils.ListContains (e1'.Force()) s then

+                    FalseLiteral

+                  else

+                    try 

+                      let contains = s |> List.map Expr2ConstStrict |> Utils.ListContains (e1'.Force() |> Expr2ConstStrict)

+                      BoolLiteral(not contains)

+                    with

+                    | _ -> recomposed.Force()

               | _ -> recomposed.Force()

           | "+" -> 

               let e1'' = e1'.Force();

@@ -987,6 +1015,7 @@ let rec PullUpMethodCalls stmt =
 let IsModifiableObj obj (c,m) = 

   let __IsFld name = FindVar c name |> Utils.OptionToBool

   match m with

+  | Method(name,_,_,_,_) when name.EndsWith("__mod__") -> true

   | Method(_,_,_,_,true) -> true

   | Method(_,_,_,post,false) -> 

       DescendExpr2 (fun e acc -> 

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index d81fca75..79b78173 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -360,7 +360,7 @@ let GenConstructorCode prog comp mthd decreasesClause body genRepr =
   | Method(methodName,sign,_,_,isConstr) -> 

       let preExpr = GetPreconditionForMethod prog mthd |> Desugar

       let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar

-      let thisObj = {name = "this"; objType = GetComponentType comp}

+      let thisObj = ThisObj comp

       "  method " + methodName + (PrintSig sign) + 

       (if IsModifiableObj thisObj (comp,mthd) then newline + "    modifies this;" else "") +

       (PrintPrePost (newline + "    requires ") preExpr) + 

diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs
index 4cbff30b..df2d044f 100644
--- a/Jennisys/FixpointSolver.fs
+++ b/Jennisys/FixpointSolver.fs
@@ -158,12 +158,15 @@ let rec ComputeClosure heapInst expandExprFunc premises =
                                           elif rhs = expr && not (lhs = except) then

                                             Some(lhs)

                                           else 

-                                            match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with

-                                            | Some(unifs) -> Some(ApplyUnifs unifs rhs)

-                                            | None -> 

-                                                match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with

-                                                | Some(unifs) -> Some(ApplyUnifs unifs lhs)

-                                                | None -> None

+                                            if expr = TrueLiteral then 

+                                              None

+                                            else

+                                               match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with

+                                               | Some(unifs) -> Some(ApplyUnifs unifs rhs)

+                                               | None -> 

+                                                   match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with

+                                                   | Some(unifs) -> Some(ApplyUnifs unifs lhs)

+                                                   | None -> None

                                         | _ -> None)

     //Logger.TraceLine (sprintf "Number of matches for %s: %i" (PrintExpr 0 expr) (List.length matches))

     matches

@@ -247,6 +250,14 @@ let rec ComputeClosure heapInst expandExprFunc premises =
               [BinaryEq lhs elist.[0]]

             else 

               [BinaryIn lhs (SequenceExpr(elist |> List.tail))]

+      | SetExpr(elist) -> 

+          let evalElist = elist |> List.map (EvalFull heapInst)

+          let evalLhs = EvalFull heapInst lhs

+          try 

+            let idx = evalElist |> List.findIndex (fun e -> e = evalLhs)

+            [BinaryEq lhs elist.[idx]]

+          with

+          | _ -> [binInExpr]

       | _ -> [binInExpr] 

     __fff lhs rhs

 

diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index dd5da320..bc330520 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -32,6 +32,7 @@ type HeapInstance = {
 }

 

 let NoObj = { name = ""; objType = NamedType("", []) }

+let ThisObj comp = {name = "this"; objType = GetComponentType comp}

 

 let ExtractAllExpressions asg = 

   match asg with

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index 9d29aeee..cba09f46 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -59,6 +59,12 @@ interface Node[T] {
 
   method Find(n: T) returns (ret: bool)
     ensures ret = (n in list)
+
+  method SetZ(n: T) 
+    ensures list = old(list[0 := n])
+	
+  method Insert(n: T) 
+    ensures list = old(list) + [n]  
 }
 
 datamodel Node[T] {
diff --git a/Jennisys/examples/Simple.jen b/Jennisys/examples/Simple.jen
index bd2e2993..12b2cdf0 100644
--- a/Jennisys/examples/Simple.jen
+++ b/Jennisys/examples/Simple.jen
@@ -3,6 +3,22 @@ interface Simple {
  

  method Inc()

    a := old(a) + 1

+   

+ method Init(n: int)

+   a := n

+   

+ method Max(x: int, y: int)

+   ensures x < y ==> a = y

+   ensures x >= y ==> a = x

+   

+ 

+ method Max2(x: int, y: int)

+   ensures a = x || a = y

+   ensures forall t :: t in {x y} ==> a >= t

+   

+ method Max3__mod__(x: int, y: int)

+   ensures a in {x y}

+   ensures forall t :: t in {x y} ==> a >= t   

 }

 

 datamodel Simple {