- implemented some sorts of symbolic evaluation of expressions

 - changed that the intermediate dafny files are written into separate
   files for different method analyses
 - added README and StartDafny-jen.bat

8 files changed, 175 insertions, 21 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 69b5bb69..244b50b4 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -104,7 +104,7 @@ let rec GetUnifications expr args (heap,env,ctx) =
         | _,_,true,Some(c1) -> 
                Logger.DebugLine ("      - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0));
                Set.ofList [c1, e0]
-        | _ -> Logger.WarnLine ("      - [WARN] couldn't unify anything from " + (PrintExpr 0 expr));
+        | _ -> Logger.TraceLine ("      - couldn't unify anything from " + (PrintExpr 0 expr));
                Set.empty
       else 
         GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx))
@@ -113,7 +113,9 @@ let rec GetArgValueUnifications args env =
   match args with
   | Var(name,_) :: rest -> 
       match Map.tryFind (VarConst(name)) env with
-      | Some(c) -> Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env)
+      | Some(c) ->
+          Logger.DebugLine ("      - adding unification " + (PrintConst c) + " <--> " + name);
+          Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env)
       | None -> failwith ("couldn't find value for argument " + name)
   | [] -> Set.empty
 
@@ -152,7 +154,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) =
                                               // check if the assertion follows and if so update the env
                                               let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)
                                               Logger.Debug("        - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")
-                                              let ok = CheckDafnyProgram code "unif"
+                                              let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))
                                               if ok then
                                                 Logger.DebugLine " HOLDS"
                                                 // change the value to expression
@@ -161,9 +163,14 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) =
                                                 Logger.DebugLine " DOESN'T HOLDS"
                                                 // don't change the value
                                                 acc |> Map.add (o,f) l
-                                            else
-                                              // leave it as is
-                                              acc |> Map.add (o,f) l) restHeap
+                                            else 
+                                              // see if it's a list, then try to match its elements
+                                              match value with
+                                              | SeqConst(clist) -> acc |> Map.add (o,f) l //TODO!!
+                                              | _ -> 
+                                                  // leave it as is
+                                                  acc |> Map.add (o,f) l
+                                         ) restHeap
       (newHeap,env,ctx)
   | [] -> (heap,env,ctx)
 
@@ -199,7 +206,7 @@ let AnalyzeConstructor prog comp m =
   let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral)
   Logger.InfoLine ("  [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m)))

   Logger.Info      "      - searching for a solution       ..."
-  let models = RunDafnyProgram code dafnyScratchSuffix   
+  let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  
   if models.Count = 0 then
     // no models means that the "assert false" was verified, which means that the spec is inconsistent
     Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!"
@@ -213,15 +220,18 @@ let AnalyzeConstructor prog comp m =
     let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
                        |> GeneralizeSolution prog comp m
     if _opt_verifySolutions then
-      Logger.Info "      - verifying synthesized solution ..."
-      if VerifySolution prog comp m (heap,env,ctx) then
-        Logger.InfoLine " OK"
+      Logger.InfoLine "      - verifying synthesized solution ... "
+      let verified = VerifySolution prog comp m (heap,env,ctx)
+      Logger.Info "      "      
+      if verified then
+        Logger.InfoLine "~~~ VERIFIED ~~~"
         Some(heap,env,ctx)
       else 
-        Logger.InfoLine " NOT VERIFIED"
+        Logger.InfoLine "!!! NOT VERIFIED !!!"
         Some(heap,env,ctx)
     else
       Some(heap,env,ctx)
+  
 
 // ============================================================================
 /// Goes through a given list of methods of the given program and attempts to 
@@ -235,6 +245,7 @@ let rec AnalyzeMethods prog members =
       match m with
       | Method(_,_,_,_,true) -> 
           let solOpt = AnalyzeConstructor prog comp m
+          Logger.InfoLine ""
           match solOpt with
           | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
           | None -> AnalyzeMethods prog rest
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index f9f7c43f..442dfe57 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -27,15 +27,120 @@ let rec VisitExpr visitorFunc expr acc =
 

 exception EvalFailed 

 

-//TODO: stuff might be missing

-let rec EvalToConst expr = 

+let rec EvalSym expr = 

   match expr with
   | IntLiteral(n) -> IntConst(n)
   | IdLiteral(id) -> VarConst(id)
   | Dot(e, str) -> 
-      match EvalToConst e with
+      match EvalSym e with
       | VarConst(lhsName) -> VarConst(lhsName + "." + str)
-      | _ -> raise EvalFailed
+      | _ -> ExprConst(expr)
+  | SeqLength(e) -> 
+      match EvalSym e with
+      | SeqConst(clist) -> IntConst(List.length clist)
+      | _ -> ExprConst(expr)
+  | SequenceExpr(elist) -> 
+      let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev |> Utils.ConvertToOptionList
+      SeqConst(clist)
+  | SelectExpr(lst, idx) ->
+      match EvalSym lst, EvalSym idx with
+      | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption
+      | _ -> ExprConst(expr)
+  | UpdateExpr(lst,idx,v) ->
+      match EvalSym lst, EvalSym idx, EvalSym v with
+      | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist)
+      | _ -> ExprConst(expr)
+  | BinaryExpr(_,op,e1,e2) ->
+      match op with
+      | Exact "=" _ ->
+          match EvalSym e1, EvalSym e2 with
+          | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)
+          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 = n2)
+          | VarConst(v1), VarConst(v2)   -> BoolConst(v1 = v2)
+          | _ -> ExprConst(expr)
+      | Exact "!=" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))
+          | IntConst(n1), IntConst(n2)   -> BoolConst(not (n1 = n2))
+          | VarConst(v1), VarConst(v2)   -> BoolConst(not (v1 = v2))
+          | _ -> ExprConst(expr)
+      | Exact "<" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 < n2)
+          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) < (Set.count s2))
+          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) < (List.length s2))
+          | _ -> ExprConst(expr)
+      | Exact "<=" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 <= n2)
+          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) <= (Set.count s2))
+          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) <= (List.length s2))
+          | _ -> ExprConst(expr)
+      | Exact ">" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 > n2)
+          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) > (Set.count s2))
+          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) > (List.length s2))
+          | _ -> ExprConst(expr)
+      | Exact ">=" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 >= n2)
+          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) >= (Set.count s2))
+          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) >= (List.length s2))
+          | _ -> ExprConst(expr)
+      | Exact "in" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | _ as c, SetConst(s)   -> BoolConst(Set.contains (Some(c)) s)
+          | _ as c, SeqConst(s)   -> BoolConst(Utils.ListContains (Some(c)) s)
+          | _ -> ExprConst(expr)
+      | Exact "!in" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | _ as c, SetConst(s)   -> BoolConst(not (Set.contains (Some(c)) s))
+          | _ as c, SeqConst(s)   -> BoolConst(not (Utils.ListContains (Some(c)) s))
+          | _ -> ExprConst(expr)
+      | Exact "+" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+          | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)
+          | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)
+          | _ -> ExprConst(expr)
+      | Exact "-" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)
+          | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)
+          | _ -> ExprConst(expr)
+      | Exact "*" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)
+          | _ -> ExprConst(expr)
+      | Exact "div" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)
+          | _ -> ExprConst(expr)
+      | Exact "mod" _ -> 
+          match EvalSym e1, EvalSym e2 with
+          | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)
+          | _ -> ExprConst(expr)
+      | _ -> ExprConst(expr)
+  | UnaryExpr(op, e) ->
+      match op with
+      | Exact "!" _ -> 
+          match EvalSym e with
+          | BoolConst(b) -> BoolConst(not b)
+          | _ -> ExprConst(expr)
+      | Exact "-" _ -> 
+          match EvalSym e with
+          | IntConst(n) -> IntConst(-n)
+          | _ -> ExprConst(expr)
+      | _ -> ExprConst(expr)
+  | _ -> ExprConst(expr)

+

+//TODO: stuff might be missing

+let rec EvalToConst expr = 

+  match expr with
+  | IntLiteral(n) -> IntConst(n)
+  | IdLiteral(id) -> raise EvalFailed //VarConst(id)
+  | Dot(e, str)   -> raise EvalFailed
   | SeqLength(e) -> 
       match EvalToConst e with
       | SeqConst(clist) -> IntConst(List.length clist)
@@ -186,6 +291,13 @@ let FilterFieldMembers members =
 let FilterConstructorMembers members = 
   members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)
 
+//  =============================================================
+/// Out of all "members" returns only those that are 
+/// constructors and have at least one input parameter
+//  =============================================================
+let FilterConstructorMembersWithParams members = 
+  members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None)
+
 //  ==========================================================
 /// Out of all "members" returns only those that are "Method"s
 //  ==========================================================
@@ -229,6 +341,12 @@ let GetMethodName mthd =
   | Method(name,_,_,_,_) -> name

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

 

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

+/// Returns full name of a method (= <class_name>.<method_name>

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

+let GetMethodFullName comp mthd = 

+  (GetClassName comp) + "." + (GetMethodName mthd)

+

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

 /// Returns signature of a method

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

@@ -305,7 +423,7 @@ let rec Desugar expr =
   | SelectExpr(_) 
   | SeqLength(_)           -> expr
   | UpdateExpr(_)          -> expr //TODO
-  | SequenceExpr(exs)      -> expr //TODO: 
+  | SequenceExpr(exs)      -> expr //TODO
   | ForallExpr(v,e)        -> ForallExpr(v, Desugar e)
   | UnaryExpr(op,e)        -> UnaryExpr(op, Desugar e)
   | BinaryExpr(p,op,e1,e2) -> 

@@ -313,7 +431,7 @@ let rec Desugar expr =
       try

         match op with

         | Exact "=" _ ->           

-            match EvalToConst e1, EvalToConst e2 with

+            match EvalSym e1, EvalSym e2 with

             | VarConst(v), SeqConst(clist)

             | SeqConst(clist), VarConst(v) -> 

                 let rec __fff lst cnt = 

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index b7b5ff15..7e61ec7e 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -137,10 +137,14 @@ let GenConstructorCode mthd body =
 
 // NOTE: insert here coto to say which methods to analyze
 let GetMethodsToAnalyze prog =
-  let c = FindComponent prog "IntList" |> Utils.ExtractOption
-  let m = FindMethod c "Double" |> Utils.ExtractOption
-  [c, m]
-//  FilterMembers prog FilterConstructorMembers
+  (* exactly one *)
+//  let c = FindComponent prog "IntList" |> Utils.ExtractOption
+//  let m = FindMethod c "Sum" |> Utils.ExtractOption
+//  [c, m]
+  (* all *)
+  FilterMembers prog FilterConstructorMembers 
+  (* only with parameters *)
+//  FilterMembers prog FilterConstructorMembersWithParams 
 
 // solutions: (comp, constructor) |--> (heap, env, ctx) 
 let PrintImplCode prog solutions methodsToPrintFunc =
diff --git a/Jennisys/README.txt b/Jennisys/README.txt
new file mode 100644
index 00000000..0e52dec9
--- /dev/null
+++ b/Jennisys/README.txt
@@ -0,0 +1,5 @@
+1. Installation instructions
+----------------------------
+
+  - create c:\tmp folder
+  - copy the Jennisys\scripts\StartDafny-jen.bat script into c:\tmp
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index ab7ffb8f..f1a1f67f 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -53,6 +53,12 @@ let rec EvalUnresolved expr (heap,env,ctx) =
       | ((_,_),x) :: [] -> x
       | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str
       | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str
+  | SelectExpr(lst, idx) ->
+      let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx)
+      let idxC = EvalUnresolved idx (heap,env,ctx)
+      match lstC, idxC with
+      | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption
+      | _ -> failwith "can't eval SelectExpr"
   | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this!
 //  | Star         
 //  | SelectExpr(_)   
@@ -63,6 +69,7 @@ let rec EvalUnresolved expr (heap,env,ctx) =
 //  | UnaryExpr(_)   
 //  | BinaryExpr(_)
 
+// TODO: can this be implemented on top of the existing AstUtils.EvalSym??  We must!
 let Eval expr (heap,env,ctx) = 

   try 

     let unresolvedConst = EvalUnresolved expr (heap,env,ctx)

diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index b7ceaec0..e99cf342 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -18,6 +18,9 @@ class IntList {
 
   constructor Double(p: int, q: int)
     ensures list = [p] + [q]
+
+  constructor Sum(p: int, q: int)
+    ensures list = [p + q]
 }
 
 model IntList {
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index f37a2631..6bb49eb8 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -18,6 +18,9 @@ class IntList {
 
   constructor Double(p: int, q: int)
     ensures list = [p] + [q]
+
+  constructor Sum(p: int, q: int)
+    ensures list = [p + q]
 }
 
 model IntList {
diff --git a/Jennisys/scripts/StartDafny-jen.bat b/Jennisys/scripts/StartDafny-jen.bat
new file mode 100644
index 00000000..79d39a38
--- /dev/null
+++ b/Jennisys/scripts/StartDafny-jen.bat
@@ -0,0 +1,3 @@
+@echo off

+"c:/boogie/Binaries/Dafny.exe" -nologo -compile:0 /print:xxx.bpl -timeLimit:60 %* > c:\tmp\jen-doo.out

+exit 43