- implemented synthesis of some simple constructors with parameters

 - added some desugaring to help the verifier.  Expression like
     lst = [p] + [q r]
   are desugared into
     lst = [p] + [q r] && lst[0] = p && lst[1] = q && lst[2] = r

18 files changed, 655 insertions, 129 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 48adcca1..69b5bb69 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -7,7 +7,9 @@ open DafnyModelUtils
 open PipelineUtils
 open Options
 open Printer
+open Resolver
 open DafnyPrinter
+open Utils
 
 open Microsoft.Boogie
                     
@@ -35,7 +37,7 @@ let rec Substitute substMap = function
   | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
   | expr -> expr
 
-let GenMethodAnalysisCode comp methodName signature pre post =
+let GenMethodAnalysisCode comp methodName signature pre post assertion =
   "  method " + methodName + "()" + newline +
   "    modifies this;" + newline +
   "  {" + newline + 
@@ -52,71 +54,181 @@ let GenMethodAnalysisCode comp methodName signature pre post =
   (GetInvariantsAsList comp |> PrintSep newline (fun e -> "    assume " + (PrintExpr 0 e) + ";")) + newline +
   // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
   "    // assert false to search for a model satisfying the assumed constraints" + newline + 
-  "    assert false;" + newline + 
+  "    assert " + (PrintExpr 0 assertion) + ";" + newline + 
   "  }" + newline
              
-let MethodAnalysisPrinter onlyForThisCompMethod comp mthd = 
+let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd = 
   match onlyForThisCompMethod with
   | (c,m) when c = comp && m = mthd -> 
     match m with 
-    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post) + newline
+    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post assertion) + newline
     | _ -> ""
   | _ -> ""
 
+let rec IsArgsOnly args expr = 
+  match expr with
+  | IdLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)
+  | UnaryExpr(_,e) -> IsArgsOnly args e
+  | BinaryExpr(_,_,e1,e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
+  | Dot(e,_) -> IsArgsOnly args e
+  | SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)
+  | UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)
+  | SequenceExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true
+  | SeqLength(e) -> IsArgsOnly args e
+  | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e
+  | IntLiteral(_) -> true
+  | Star -> true
+
+let rec GetUnifications expr args (heap,env,ctx) = 
+  match expr with
+  | IntLiteral(_)
+  | IdLiteral(_)
+  | Star         
+  | Dot(_)
+  | SelectExpr(_)   // TODO: handle select expr
+  | UpdateExpr(_)   // TODO: handle update expr
+  | SequenceExpr(_) 
+  | SeqLength(_)    
+  | ForallExpr(_)   // TODO: handle forall expr
+  | UnaryExpr(_)   -> Set.empty
+  | BinaryExpr(strength,op,e0,e1) ->
+      if op = "=" then
+        let v0 = Eval e0 (heap,env,ctx)
+        let v1 = Eval e1 (heap,env,ctx)
+        let argsOnly0 = IsArgsOnly args e0
+        let argsOnly1 = IsArgsOnly args e1
+        match v0,argsOnly1,argsOnly0,v1 with
+        | Some(c0),true,_,_ -> 
+               Logger.DebugLine ("      - adding unification " + (PrintConst c0) + " <--> " + (PrintExpr 0 e1));
+               Set.ofList [c0, e1]
+        | _,_,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));
+               Set.empty
+      else 
+        GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx))
+
+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)
+      | None -> failwith ("couldn't find value for argument " + name)
+  | [] -> Set.empty
+
+let rec _GetObjRefExpr o (heap,env,ctx) visited = 
+  if Set.contains o visited then 
+    None
+  else 
+    let newVisited = Set.add o visited
+    let refName = PrintObjRefName o (env,ctx)
+    match refName with
+    | Exact "this" _ -> Some(IdLiteral(refName))
+    | _ -> 
+        let rec __fff lst = 
+          match lst with
+          | ((o,Var(fldName,_)),l) :: rest -> 
+              match _GetObjRefExpr o (heap,env,ctx) newVisited with
+              | Some(expr) -> Some(Dot(expr, fldName))
+              | None -> __fff rest
+          | [] -> None
+        let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList
+        __fff backPointers      
+
+let GetObjRefExpr o (heap,env,ctx) = 
+  _GetObjRefExpr o (heap,env,ctx) (Set.empty)
+
+let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = 
+  match unifs with
+  | (c,e) :: rest -> 
+      let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx)
+      let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->
+                                            let value = Resolve l (env,ctx)
+                                            if value = c then
+                                              let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx)))
+                                              let fldName = PrintVarName f                             
+                                              let assertionExpr = BinaryEq (Dot(objRefExpr, fldName)) e
+                                              // 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"
+                                              if ok then
+                                                Logger.DebugLine " HOLDS"
+                                                // change the value to expression
+                                                acc |> Map.add (o,f) (ExprConst(e))
+                                              else
+                                                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
+      (newHeap,env,ctx)
+  | [] -> (heap,env,ctx)
+
+let GeneralizeSolution prog comp mthd (heap,env,ctx) =
+  match mthd with
+  | Method(mName,Sig(ins, outs),pre,post,_) -> 
+      let args = List.concat [ins; outs]
+      match args with 
+      | [] -> (heap,env,ctx)
+      | _  -> 
+          let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx)
+                    |> Set.union (GetArgValueUnifications args env)
+          UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx)
+  | _ -> failwith ("not a method: " + mthd.ToString())
+
+//  ====================================================================================
 /// Returns whether the code synthesized for the given method can be verified with Dafny
-let VerifySolution (heap,env,ctx) prog comp mthd =
+//  ====================================================================================
+let VerifySolution prog comp mthd (heap,env,ctx) =
   // print the solution to file and try to verify it with Dafny
   let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx)
   let code = PrintImplCode prog solution (fun p -> [comp,mthd])
-  use file = System.IO.File.CreateText(dafnyVerifyFile)
-  file.AutoFlush <- true  
-  fprintfn file "%s" code
-  file.Close()
-  // run Dafny
-  RunDafny dafnyVerifyFile dafnyVerifyModelFile
-  // read models from the model file
-  use modelFile = System.IO.File.OpenText(dafnyVerifyModelFile)
-  let models = Microsoft.Boogie.Model.ParseModels modelFile
-  // if there are no models, verification was successful
-  models.Count = 0
-                           
+  CheckDafnyProgram code dafnyVerifySuffix
+   
+//  ============================================================================
+/// Attempts to synthesize the initialization code for the given constructor "m"

+///

+/// Returns a (heap,env,ctx) tuple
+//  ============================================================================                           
 let AnalyzeConstructor prog comp m =
   let methodName = GetMethodName m
   // generate Dafny code for analysis first
-  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
-  printfn "  [*] analyzing constructor %s" methodName 
-  printf  "       - searching for a solution       ..."
-  use file = System.IO.File.CreateText(dafnyScratchFile)
-  file.AutoFlush <- true
-  fprintf file "%s" code
-  file.Close()
-  // run Dafny
-  RunDafny dafnyScratchFile dafnyModelFile
-  // read models
-  use modelFile = System.IO.File.OpenText(dafnyModelFile)        
-  let models = Microsoft.Boogie.Model.ParseModels modelFile
+  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   
   if models.Count = 0 then
     // no models means that the "assert false" was verified, which means that the spec is inconsistent
-    printfn " !!! SPEC IS INCONSISTENT !!!"
+    Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!"
     None
   else 
     if models.Count > 1 then 
-      printfn " FAILED "
+      Logger.WarnLine " FAILED "
       failwith "internal error (more than one model for a single constructor analysis)"
-    printfn " OK "
+    Logger.InfoLine " OK "
     let model = models.[0]
     let heap,env,ctx = ReadFieldValuesFromModel model prog comp m
+                       |> GeneralizeSolution prog comp m
     if _opt_verifySolutions then
-      printf "       - verifying synthesized solution ..."
-      if VerifySolution (heap,env,ctx) prog comp m then
-        printfn " OK"
+      Logger.Info "      - verifying synthesized solution ..."
+      if VerifySolution prog comp m (heap,env,ctx) then
+        Logger.InfoLine " OK"
         Some(heap,env,ctx)
       else 
-        printfn " 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 
+/// synthesize code for each one of them.
+///
+/// Returns a map from (component * method) |--> (heap,env,ctx)
+// ============================================================================
 let rec AnalyzeMethods prog members = 
   match members with
   | (comp,m) :: rest -> 
@@ -133,7 +245,7 @@ let Analyze prog =
   let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
   use file = System.IO.File.CreateText(dafnySynthFile)
   file.AutoFlush <- true
-  printfn "Printing synthesized code"
+  Logger.InfoLine "Printing synthesized code"
   let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze
   fprintfn file "%s" synthCode
   ()
diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index 9e68ac56..bd66e688 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -16,21 +16,11 @@ type Type =
   | NamedType of string

   | InstantiatedType of string * Type (* type parameter *)

 

-type Const = 

-  | IntConst   of int

-  | BoolConst  of bool

-  | SetConst   of Set<Const option>

-  | SeqConst   of (Const option) list

-  | NullConst

-  | ThisConst  of (* loc id *) string * Type option

-  | NewObj     of (* loc id *) string * Type option

-  | Unresolved of (* loc id *) string 

-

 type VarDecl =

   | Var of string * Type option

 

 type Expr =

-  | IntLiteral of BigInteger

+  | IntLiteral of int

   | IdLiteral of string

   | Star

   | Dot of Expr * string

@@ -47,7 +37,7 @@ type Stmt =
   | Assign of Expr * Expr

 

 type Signature =

-  | Sig of VarDecl list * VarDecl list

+  | Sig of (* ins *) VarDecl list * (* outs *) VarDecl list

 

 type Member =

   | Field of VarDecl

@@ -68,3 +58,14 @@ type Component =
 type Program =

   | Program of Component list

 

+type Const = 

+  | IntConst   of int

+  | BoolConst  of bool

+  | SetConst   of Set<Const option>

+  | SeqConst   of (Const option) list

+  | NullConst

+  | ThisConst  of (* loc id *) string * Type option

+  | NewObj     of (* loc id *) string * Type option

+  | ExprConst  of Expr

+  | VarConst   of (* varName *) string

+  | Unresolved of (* loc id *) string 
\ No newline at end of file
diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 87903b5a..f9f7c43f 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -5,8 +5,114 @@
 module AstUtils

 

 open Ast

+open Utils

 

+// ------------------------------- Visitor Stuff -------------------------------------------

+

+let rec VisitExpr visitorFunc expr acc =

+  match expr with
+  | IntLiteral(_)
+  | IdLiteral(_)
+  | Star                   -> acc |> visitorFunc expr
+  | Dot(e, _)              -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+  | SelectExpr(e1, e2)     -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+  | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3
+  | SequenceExpr(exs)      -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)
+  | SeqLength(e)           -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+  | ForallExpr(_,e)        -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+  | UnaryExpr(_,e)         -> acc |> visitorFunc expr |> VisitExpr visitorFunc e
+  | BinaryExpr(_,_,e1,e2)  -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2

+

+// ------------------------------- End Visitor Stuff -------------------------------------------

+

+exception EvalFailed 

+

+//TODO: stuff might be missing

+let rec EvalToConst expr = 

+  match expr with
+  | IntLiteral(n) -> IntConst(n)
+  | IdLiteral(id) -> VarConst(id)
+  | Dot(e, str) -> 
+      match EvalToConst e with
+      | VarConst(lhsName) -> VarConst(lhsName + "." + str)
+      | _ -> raise EvalFailed
+  | SeqLength(e) -> 
+      match EvalToConst e with
+      | SeqConst(clist) -> IntConst(List.length clist)
+      | _ -> raise EvalFailed
+  | SequenceExpr(elist) -> 
+      let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev |> Utils.ConvertToOptionList
+      SeqConst(clist)
+  | SelectExpr(lst, idx) ->
+      match EvalToConst lst, EvalToConst idx with
+      | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption
+      | _ -> raise EvalFailed
+  | UpdateExpr(lst,idx,v) ->
+      match EvalToConst lst, EvalToConst idx, EvalToConst v with
+      | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist)
+      | _ -> raise EvalFailed
+  | BinaryExpr(_,op,e1,e2) ->
+      match op with
+      | Exact "=" _ ->
+          try 
+            BoolConst(EvalToBool(e1) = EvalToBool(e2))
+          with 
+          | EvalFailed -> BoolConst(EvalToInt(e1) = EvalToInt(e2))
+      | Exact "!=" _ -> 
+          try 
+            BoolConst(not(EvalToBool(e1) = EvalToBool(e2)))
+          with 
+          | EvalFailed -> BoolConst(not(EvalToInt e1 = EvalToInt e2))
+      | Exact "<" _ -> BoolConst(EvalToInt e1 < EvalToInt e2) //TODO sets, seqs
+      | Exact "<=" _ -> BoolConst(EvalToInt e1 <= EvalToInt e2) //TODO sets, seqs
+      | Exact ">" _ -> BoolConst(EvalToInt e1 > EvalToInt e2) //TODO sets, seqs
+      | Exact ">=" _ -> BoolConst(EvalToInt e1 >= EvalToInt e2) //TODO sets, seqs
+      | Exact "in" _ -> raise EvalFailed //TODO
+      | Exact "!in" _ -> raise EvalFailed //TODO
+      | Exact "+" _ -> 
+          match EvalToConst e1, EvalToConst 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)
+          | _ -> raise EvalFailed
+      | Exact "-" _ -> IntConst(EvalToInt e1 - EvalToInt e2)
+      | Exact "*" _ -> IntConst(EvalToInt e1 * EvalToInt e2)
+      | Exact "div" _ -> IntConst(EvalToInt e1 / EvalToInt e2)
+      | Exact "mod" _ -> IntConst(EvalToInt e1 % EvalToInt e2)
+      | _ -> raise EvalFailed 
+  | UnaryExpr(op, e) ->
+      match op with
+      | Exact "!" _ -> BoolConst(not (EvalToBool e))
+      | Exact "-" _ -> IntConst(-(EvalToInt e))
+      | _ -> raise EvalFailed  
+  | _ -> raise EvalFailed
+and EvalToBool e =
+  let c = EvalToConst e
+  match c with
+  | BoolConst(b) -> b
+  | _ -> raise EvalFailed
+and EvalToInt e = 
+  let c = EvalToConst e
+  match c with
+  | IntConst(n) -> n
+  | _ -> raise EvalFailed
+  
+let rec Const2Expr c =

+  match c with

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

+  | BoolConst(b) -> if b then IntLiteral(1) else IntLiteral(0) //?? BoolLiteral(b)

+  | SeqConst(clist) -> 

+      let expList = clist |> List.fold (fun acc c -> Const2Expr (Utils.ExtractOption c) :: acc) [] |> List.rev

+      SequenceExpr(expList)

+  | ThisConst(_) -> IdLiteral("this")

+  | VarConst(v) -> IdLiteral(v)

+  | NullConst -> IdLiteral("null")

+  | ExprConst(e) -> e

+  | _ -> failwith "not implemented or not supported"

+

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

 /// Returns a binary AND of the two given expressions with short-circuiting

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

 let BinaryAnd (lhs: Expr) (rhs: Expr) = 

     match lhs, rhs with

     | IdLiteral("true"), _  -> rhs

@@ -15,7 +121,9 @@ let BinaryAnd (lhs: Expr) (rhs: Expr) =
     | _, IdLiteral("false") -> IdLiteral("false")

     | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

 

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

 /// Returns a binary OR of the two given expressions with short-circuiting

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

 let BinaryOr (lhs: Expr) (rhs: Expr) = 

     match lhs, rhs with

     | IdLiteral("true"), _  -> IdLiteral("true")

@@ -24,43 +132,69 @@ let BinaryOr (lhs: Expr) (rhs: Expr) =
     | _, IdLiteral("false") -> lhs

     | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

 

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

 /// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)

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

 let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

 

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

 /// Returns a binary NEQ of the two given expressions

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

 let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)

 

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

+/// Returns a binary EQ of the two given expressions

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

+let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)

+

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

 /// Returns TRUE literal

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

 let TrueLiteral = IdLiteral("true")

+

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

 /// Returns FALSE literal

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

 let FalseLiteral = IdLiteral("false")

 

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

 /// Splits "expr" into a list of its conjuncts

+//  ==========================================
 let rec SplitIntoConjunts expr = 
   match expr with
   | IdLiteral("true") -> []
   | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1]
   | _ -> [expr]
 
+//  ======================================
 /// Applies "f" to each conjunct of "expr"
+//  ======================================
 let rec ForeachConjunct f expr =
   SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""

 

 // --- search functions ---

                      

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

 /// Out of all "members" returns only those that are "Field"s                                               

+//  =========================================================
 let FilterFieldMembers members =
   members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
 
+//  =============================================================
 /// Out of all "members" returns only those that are constructors
+//  =============================================================
 let FilterConstructorMembers members = 
   members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None)
 
+//  ==========================================================
 /// Out of all "members" returns only those that are "Method"s
+//  ==========================================================
 let FilterMethodMembers members = 
   members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None)
 
+//  =======================================================================
 /// Returns all members of the program "prog" that pass the filter "filter"
+//  =======================================================================
 let FilterMembers prog filter = 
   match prog with
   | Program(components) ->
@@ -69,7 +203,9 @@ let FilterMembers prog filter =
         | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            
         | _ -> acc) []

 

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

 /// Returns all fields of a component

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

 let GetAllFields comp = 

   match comp with
   | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->
@@ -77,19 +213,41 @@ let GetAllFields comp =
       List.concat [aVars ; cVars]

   | _ -> []

                     

-/// Returns the class name of a component                              

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

+/// Returns class name of a component

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

 let GetClassName comp =

   match comp with

   | Component(Class(name,_,_),_,_) -> name

   | _ -> failwith ("unrecognized component: " + comp.ToString())

 

-/// Returns the name of a method

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

+/// Returns name of a method

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

 let GetMethodName mthd = 

   match mthd with

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

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

 

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

+/// Returns signature of a method

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

+let GetMethodSig mthd = 

+  match mthd with

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

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

+

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

+/// Returns all arguments of a method (both input and output)

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

+let GetMethodArgs mthd = 

+  match mthd with

+  | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs]

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

+

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

 /// Returns all invariants of a component as a list of expressions

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

 let GetInvariantsAsList comp = 

   match comp with

   | Component(Class(_,_,members), Model(_,_,_,_,inv), _) -> 

@@ -97,28 +255,87 @@ let GetInvariantsAsList comp =
       List.append (SplitIntoConjunts inv) clsInvs

   | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())

 

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

 /// Returns all members of a component

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

 let GetMembers comp =

   match comp with

   | Component(Class(_,_,members),_,_) -> members

   | _ -> failwith ("unrecognized component: " + comp.ToString())

 

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

 /// Finds a component of a program that has a given name

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

 let FindComponent (prog: Program) clsName = 

   match prog with

   | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)

                             |> Utils.ListToOption

 

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

 /// Finds a method of a component that has a given name

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

 let FindMethod comp methodName =

+  let x = GetMembers comp

+  let y = x |> FilterMethodMembers

+  let z = y |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

   GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)

                                          |> Utils.ListToOption

 

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

 /// Finds a field of a class that has a given name

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

 let FindVar (prog: Program) clsName fldName =

   let copt = FindComponent prog clsName

   match copt with

   | Some(comp) -> 

       GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

                         |> Utils.ListToOption

-  | None -> None
\ No newline at end of file
+  | None -> None

+  

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

+/// Desugars a given expression so that all list constructors 

+/// are expanded into explicit assignments to indexed elements

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

+let rec Desugar expr = 

+  match expr with
+  | IntLiteral(_)          
+  | IdLiteral(_)           
+  | Star                   
+  | Dot(_)                 
+  | SelectExpr(_) 
+  | SeqLength(_)           -> expr
+  | UpdateExpr(_)          -> 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) -> 

+      let be = BinaryExpr(p, op, Desugar e1, Desugar e2)

+      try

+        match op with

+        | Exact "=" _ ->           

+            match EvalToConst e1, EvalToConst e2 with

+            | VarConst(v), SeqConst(clist)

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

+                let rec __fff lst cnt = 

+                  match lst with

+                  | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr (Utils.ExtractOption clist.[cnt])) :: __fff rest (cnt+1)

+                  | [] -> []

+                __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be

+            | SeqConst(cl1), SeqConst(cl2) -> 

+                let rec __fff lst1 lst2 cnt = 

+                  match lst1, lst2 with

+                  | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr (Utils.ExtractOption cl1.[cnt])) (Const2Expr (Utils.ExtractOption cl2.[cnt])) :: __fff rest1 rest2 (cnt+1)

+                  | [], [] -> []

+                  | _ -> failwith "Lists are of different sizes"

+                __fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be

+            | _ -> be

+        | _ -> be

+      with

+        | EvalFailed as ex -> (* printfn "%s" (ex.StackTrace.ToString());  *) be

+          

+

+let rec DesugarLst exprLst = 

+  match exprLst with

+  | expr :: rest -> Desugar expr :: DesugarLst rest

+  | [] -> []

+

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 408d77b0..b7b5ff15 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -4,6 +4,7 @@ open Ast
 open AstUtils

 open Utils
 open Printer   

+open Resolver

 open TypeChecker

 open DafnyPrinter

 

@@ -136,10 +137,10 @@ 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 "Singleton" |> Utils.ExtractOption
-//  [c, m]
-  FilterMembers prog FilterConstructorMembers
+  let c = FindComponent prog "IntList" |> Utils.ExtractOption
+  let m = FindMethod c "Double" |> Utils.ExtractOption
+  [c, m]
+//  FilterMembers prog FilterConstructorMembers
 
 // solutions: (comp, constructor) |--> (heap, env, ctx) 
 let PrintImplCode prog solutions methodsToPrintFunc =
diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs
index fca44270..6e78dc33 100644
--- a/Jennisys/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/Jennisys/DafnyModelUtils.fs
@@ -19,6 +19,9 @@ open Utils
 

 open Microsoft.Boogie

                 

+/// special object ref constant that will hold method argument values

+let argsObjRefConst = Unresolved("*0") 

+

 let GetElemFullName (elem: Model.Element) = 

   elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0)
              |> Seq.choose (fun ft -> Some(ft.Func.Name))
@@ -135,6 +138,21 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
                         | None -> acc
                       ) Map.empty

 

+let rec ReadArgValues (model: Microsoft.Boogie.Model) args = 

+  match args with 

+  | Var(name,_) as v :: rest -> 

+      let farg = model.Functions |> Seq.filter (fun f -> f.Arity = 0 && f.Name.StartsWith(name + "#")) |> Utils.SeqToOption

+      match farg with

+      | Some(func) -> 

+          let refObj = argsObjRefConst

+          let fldVar = v

+          assert (Seq.length func.Apps = 1)

+          let ft = Seq.head func.Apps

+          let fldVal = ConvertValue model (ft.Result)

+          ReadArgValues model rest |> Map.add (VarConst(name)) fldVal

+      | None -> failwith ("cannot find corresponding function for parameter " + name)

+  | [] -> Map.empty

+

 let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =

   match len_tuples with

   | ft :: rest -> 

@@ -227,5 +245,6 @@ let ReadEnv (model: Microsoft.Boogie.Model) =
 

 let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth =
   let heap = ReadHeap model prog
-  let env,ctx = ReadEnv model
+  let env0,ctx = ReadEnv model
+  let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth))
   heap,env,ctx
\ No newline at end of file
diff --git a/Jennisys/Jennisys/EnvUtils.fs b/Jennisys/Jennisys/EnvUtils.fs
new file mode 100644
index 00000000..0b840311
--- /dev/null
+++ b/Jennisys/Jennisys/EnvUtils.fs
@@ -0,0 +1,9 @@
+module EnvUtils

+

+open Ast

+

+let GetThisLoc env = 

+  Map.findKey (fun k v -> 

+                 match v with

+                 | ThisConst(_) -> true

+                 | _ -> false) env
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 28824237..0337c6a2 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -64,4 +64,4 @@ let args = Environment.GetCommandLineArgs()
 try 
   start 1 args false true null
 with 
-| e -> printfn "%s" e.StackTrace
\ No newline at end of file
+  | Failure(msg) as e -> printfn "WHYYYYYYYYYYYYYYY: %s" msg; printfn "%s" e.StackTrace
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 4341dfcf..39ed1aed 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -56,6 +56,7 @@
       <Link>Lexer.fs</Link>

     </Compile>

     <Compile Include="DafnyModelUtils.fs" />

+    <Compile Include="EnvUtils.fs" />

     <FsYacc Include="Parser.fsy">

       <OtherFlags>--module Parser</OtherFlags>

     </FsYacc>

@@ -63,8 +64,10 @@
       <OtherFlags>--unicode</OtherFlags>

     </FsLex>

     <Compile Include="Printer.fs" />

+    <Compile Include="Logger.fs" />

     <Compile Include="DafnyPrinter.fs" />

     <Compile Include="TypeChecker.fs" />

+    <Compile Include="Resolver.fs" />

     <Compile Include="CodeGen.fs" />

     <Compile Include="Analyzer.fs" />

     <Compile Include="Jennisys.fs" />

diff --git a/Jennisys/Jennisys/Lexer.fsl b/Jennisys/Jennisys/Lexer.fsl
index a0e62109..91c3239c 100644
--- a/Jennisys/Jennisys/Lexer.fsl
+++ b/Jennisys/Jennisys/Lexer.fsl
@@ -70,7 +70,7 @@ rule tokenize = parse
 | "::"     { COLONCOLON }

 | ","      { COMMA }

 // Numberic constants

-| digit+        { INTEGER (System.Numerics.BigInteger.Parse(lexeme lexbuf)) }

+| digit+        { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }

 // identifiers

 | idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }

 // EOF

diff --git a/Jennisys/Jennisys/Logger.fs b/Jennisys/Jennisys/Logger.fs
new file mode 100644
index 00000000..bb784ba2
--- /dev/null
+++ b/Jennisys/Jennisys/Logger.fs
@@ -0,0 +1,39 @@
+/// Simple logging facility

+///

+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)

+

+module Logger

+

+open Printer

+

+let _ALL = 100

+let _TRACE = 90

+let _DEBUG = 70

+let _INFO = 50

+let _WARN = 40

+let _ERROR = 20

+let _NONE = 0

+

+let logLevel = _ALL

+

+let Log level msg =

+  if logLevel >= level then

+    printf "%s" msg

+

+let LogLine level msg = 

+  Log level (msg + newline)

+

+let Trace msg = Log _TRACE msg

+let TraceLine msg = LogLine _TRACE msg

+

+let Debug msg = Log _DEBUG msg

+let DebugLine msg = LogLine _DEBUG msg

+

+let Info msg = Log _INFO msg

+let InfoLine msg = LogLine _INFO msg

+

+let Warn msg = Log _WARN msg

+let WarnLine msg = LogLine _WARN msg

+

+let Error msg = Log _ERROR msg

+let ErrorLine msg = LogLine _ERROR msg
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy
index 10aa7d1d..21e2c83e 100644
--- a/Jennisys/Jennisys/Parser.fsy
+++ b/Jennisys/Jennisys/Parser.fsy
@@ -6,7 +6,7 @@ open AstUtils
 let rec MyFold ee acc =

   match ee with

     | [] -> acc

-    | x::rest -> BinaryAnd x (MyFold rest acc)

+    | x::rest -> BinaryAnd (Desugar x) (MyFold rest acc)

 

 %}

 

@@ -16,7 +16,7 @@ let rec MyFold ee acc =
 // These are the terminal tokens of the grammar along with the types of

 // the data carried by each token:

 %token <string> ID

-%token <System.Numerics.BigInteger> INTEGER

+%token <int> INTEGER

 %token DOT

 %token NOT

 %token STAR DIV MOD

@@ -89,9 +89,9 @@ BlockStmt:
 

 Member:

     | VAR VarDecl                            { Field($2) }

-    | CONSTRUCTOR ID Signature Pre Post      { Method($2, $3, $4, $5, true) }

-    | METHOD ID Signature Pre Post           { Method($2, $3, $4, $5, false) }

-	  | INVARIANT ExprList                     { Invariant($2) }

+    | CONSTRUCTOR ID Signature Pre Post      { Method($2, $3, (Desugar $4), (Desugar $5), true) }

+    | METHOD ID Signature Pre Post           { Method($2, $3, (Desugar $4), (Desugar $5), false) }

+	  | INVARIANT ExprList                     { Invariant(DesugarLst $2) }

 

 FrameMembers:

     |                                        { [], [], IdLiteral("true") }

diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs
index c059e86b..686452b6 100644
--- a/Jennisys/Jennisys/PipelineUtils.fs
+++ b/Jennisys/Jennisys/PipelineUtils.fs
@@ -5,17 +5,19 @@
 

 module PipelineUtils

   
-let dafnyScratchFile = @"c:\tmp\jennisys-scratch.dfy"
-let dafnyVerifyFile = @"c:\tmp\jennisys-verify.dfy"
-let dafnyModelFile = @"c:\tmp\jennisys-scratch.bvd"
-let dafnyVerifyModelFile = @"c:\tmp\jennisys-verify.bvd"
-let dafnyOutFile = @"c:\tmp\jennisys-scratch.out"
+let dafnyScratchSuffix = "scratch"
+let dafnyVerifySuffix = "verify"
+let dafnyUnifSuffix = "unif"
 let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy"
 
 let CreateEmptyModelFile modelFile = 
   use mfile = System.IO.File.CreateText(modelFile)
   fprintf mfile ""
 
+//  =======================================================
+/// Runs Dafny on the given "inputFile" and prints 
+/// the resulting model to the given "modelFile"
+//  =======================================================
 let RunDafny inputFile modelFile =

   CreateEmptyModelFile modelFile

   async {

@@ -24,4 +26,29 @@ let RunDafny inputFile modelFile =
     proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile

     assert proc.Start()

     proc.WaitForExit() 

-  } |> Async.RunSynchronously     

+  } |> Async.RunSynchronously

+  

+//  =======================================================
+/// Runs Dafny on the given "dafnyCode" and returns models
+//  =======================================================
+let RunDafnyProgram dafnyProgram suffix =
+  let inFileName = @"c:\tmp\jennisys-" + suffix + ".dfy" 
+  let modelFileName = @"c:\tmp\jennisys-" + suffix + ".bvd" 
+  use file = System.IO.File.CreateText(inFileName)
+  file.AutoFlush <- true  
+  fprintfn file "%s" dafnyProgram
+  file.Close()
+  // run Dafny
+  RunDafny inFileName modelFileName
+  // read models from the model file
+  use modelFile = System.IO.File.OpenText(modelFileName)
+  Microsoft.Boogie.Model.ParseModels modelFile
+
+//  =======================================================
+/// Checks whether the given dafny program verifies
+//  =======================================================  
+let CheckDafnyProgram dafnyProgram suffix =
+  // TODO: also check whether Dafny produced any other errors (e.g. compilation errors, etc.)
+  let models = RunDafnyProgram dafnyProgram suffix
+  // if there are no models, verification was successful
+  models.Count = 0       

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 5410db31..eb70acbd 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -14,24 +14,6 @@ let rec PrintSep sep f list =
   | [a] -> f a
   | a :: more -> (f a) + sep + (PrintSep sep f more)
   
-let rec PrintConst cst = 
-  match cst with 
-  | IntConst(v)        -> sprintf "%d" v
-  | BoolConst(b)       -> sprintf "%b" b
-  | SetConst(cset)     -> cset.ToString() //TODO: this won't work
-  | SeqConst(cseq)     -> 
-      let seqCont = cseq |> List.fold (fun acc cOpt ->
-                                         let sep = if acc = "" then "" else ", "
-                                         match cOpt with 
-                                         | Some(c) -> acc + sep + (PrintConst c)
-                                         | None -> acc + sep + "null"
-                                      ) ""
-      sprintf "[%s]" seqCont
-  | NullConst          -> "null"
-  | ThisConst(_,_)     -> "this"
-  | NewObj(name,_)     -> PrintGenSym name
-  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
-
 let rec PrintType ty =
   match ty with
   | IntType                  -> "int"
@@ -132,3 +114,23 @@ let PrintDecl d =
 let Print prog =
   match prog with
   | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls
+
+let rec PrintConst cst = 
+  match cst with 
+  | IntConst(v)        -> sprintf "%d" v
+  | BoolConst(b)       -> sprintf "%b" b
+  | SetConst(cset)     -> cset.ToString() //TODO: this won't work
+  | SeqConst(cseq)     -> 
+      let seqCont = cseq |> List.fold (fun acc cOpt ->
+                                         let sep = if acc = "" then "" else ", "
+                                         match cOpt with 
+                                         | Some(c) -> acc + sep + (PrintConst c)
+                                         | None -> acc + sep + "null"
+                                      ) ""
+      sprintf "[%s]" seqCont
+  | NullConst          -> "null"
+  | ThisConst(_,_)     -> "this"
+  | NewObj(name,_)     -> PrintGenSym name
+  | ExprConst(e)       -> PrintExpr 0 e
+  | VarConst(name)     -> name
+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
new file mode 100644
index 00000000..ab7ffb8f
--- /dev/null
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -0,0 +1,71 @@
+module Resolver

+

+open Ast

+open Printer

+open EnvUtils

+

+// resolving values

+ 

+let rec Resolve cst (env,ctx) =

+  match cst with

+  | Unresolved(_) as u -> 

+      // see if it is in the env map first

+      let envVal = Map.tryFind cst env

+      match envVal with

+      | Some(c) -> Resolve c (env,ctx)

+      | None -> 

+          // not found in the env map --> check the equality sets

+          let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)

+                       |> Utils.SetToOption

+          match eq with 

+          | Some(eqSet) -> 

+              let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)

+                               |> Utils.SetToOption

+              match cOpt with 

+              | Some(c) -> c

+              | _ -> failwith ("failed to resolve " + cst.ToString())

+          | _ -> failwith ("failed to resolve " + cst.ToString())

+  | SeqConst(cseq) -> 

+      let resolvedLst = cseq |> List.rev |> List.fold (fun acc cOpt ->

+                                                         match cOpt with

+                                                         | Some(c) -> Some(Resolve c (env,ctx)) :: acc 

+                                                         | None -> cOpt :: acc

+                                                      ) []

+      SeqConst(resolvedLst)

+  | SetConst(cset) ->

+      let resolvedSet = cset |> Set.fold (fun acc cOpt ->

+                                            match cOpt with

+                                            | Some(c) -> acc |> Set.add (Some(Resolve c (env,ctx)))

+                                            | None -> acc |> Set.add(cOpt)

+                                          ) Set.empty

+      SetConst(resolvedSet)

+  | _ -> cst

+

+let rec EvalUnresolved expr (heap,env,ctx) = 

+  match expr with
+  | IntLiteral(n) -> IntConst(n)
+  | IdLiteral(id) when id = "this" -> GetThisLoc env
+  | IdLiteral(id) -> EvalUnresolved (Dot(IdLiteral("this"), id)) (heap,env,ctx)
+  | Dot(e, str) -> 
+      let discr = EvalUnresolved e (heap,env,ctx)
+      let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList
+      match h2 with
+      | ((_,_),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
+  | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this!
+//  | Star         
+//  | SelectExpr(_)   
+//  | UpdateExpr(_)   
+//  | SequenceExpr(_) 
+//  | SeqLength(_)    
+//  | ForallExpr(_)   
+//  | UnaryExpr(_)   
+//  | BinaryExpr(_)
+
+let Eval expr (heap,env,ctx) = 

+  try 

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

+    Some(Resolve unresolvedConst (env,ctx))

+  with

+    ex -> None
\ No newline at end of file
diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs
index a671a1ec..7414f253 100644
--- a/Jennisys/Jennisys/TypeChecker.fs
+++ b/Jennisys/Jennisys/TypeChecker.fs
@@ -1,6 +1,7 @@
 module TypeChecker

 

 open Ast

+open Printer

 open System.Collections.Generic

 

 let GetClass name decls =

@@ -36,40 +37,3 @@ let TypeCheck prog =
       let componentNames = decls |> List.choose (function Class(name,_,_) -> Some(name) | _ -> None)

       let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))

       Some(Program(clist))

-

-// resolving values

- 

-let rec Resolve cst (env,ctx) =

-  match cst with

-  | Unresolved(_) as u -> 

-      // see if it is in the env map first

-      let envVal = Map.tryFind cst env

-      match envVal with

-      | Some(c) -> Resolve c (env,ctx)

-      | None -> 

-          // not found in the env map --> check the equality sets

-          let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)

-                       |> Utils.SetToOption

-          match eq with 

-          | Some(eqSet) -> 

-              let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)

-                               |> Utils.SetToOption

-              match cOpt with 

-              | Some(c) -> c

-              | _ -> failwith ("failed to resolve " + cst.ToString())

-          | _ -> failwith ("failed to resolve " + cst.ToString())

-  | SeqConst(cseq) -> 

-      let resolvedLst = cseq |> List.rev |> List.fold (fun acc cOpt ->

-                                                         match cOpt with

-                                                         | Some(c) -> Some(Resolve c (env,ctx)) :: acc 

-                                                         | None -> cOpt :: acc

-                                                      ) []

-      SeqConst(resolvedLst)

-  | SetConst(cset) ->

-      let resolvedSet = cset |> Set.fold (fun acc cOpt ->

-                                            match cOpt with

-                                            | Some(c) -> acc |> Set.add (Some(Resolve c (env,ctx)))

-                                            | None -> acc |> Set.add(cOpt)

-                                          ) Set.empty

-      SetConst(resolvedSet)

-  | _ -> cst

diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs
index 2e9ca491..3cb8fee4 100644
--- a/Jennisys/Jennisys/Utils.fs
+++ b/Jennisys/Jennisys/Utils.fs
@@ -8,18 +8,29 @@ module Utils
 // ----------- collection util funcs ---------

 // -------------------------------------------

 

-/// requres: x = Some(a)

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

+/// requres: x = Some(a) or failswith msg

 /// ensures: ret = a

-let ExtractOption x = 

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

+let ExtractOptionMsg msg x = 

   match x with

   | Some(a) -> a

-  | None -> failwith "can't extract anything from a None"

+  | None -> failwith msg

 

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

+/// requres: x = Some(a)

+/// ensures: ret = a

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

+let ExtractOption x = 

+  ExtractOptionMsg "can't extract anything from a None" x

+

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

 /// requres: List.length lst <= 1

 /// ensures: if |lst| = 0 then

 ///            ret = None

 ///          else

 ///            ret = Some(lst[0])

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

 let ListToOption lst = 

   if List.length lst > 1 then

     failwith "given list contains more than one element"

@@ -28,11 +39,21 @@ let ListToOption lst =
   else

     Some(lst.[0])

 

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

+/// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])

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

+let rec ConvertToOptionList lst = 

+  match lst with

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

+  | [] -> []

+

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

 /// requres: Seq.length seq <= 1

 /// ensures: if |seq| = 0 then

 ///            ret = None

 ///          else

 ///            ret = Some(seq[0])

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

 let SeqToOption seq = 

   if Seq.length seq > 1 then

     failwith "given seq contains more than one element"

@@ -41,11 +62,13 @@ let SeqToOption seq =
   else

     Some(Seq.nth 0 seq)

 

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

 /// requires: Set.count set <= 1

 /// ensures: if |set| = 0 then

 ///            ret = None

 ///          else

 ///            ret = Some(set[0])

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

 let SetToOption set = 

   if Set.count set > 1 then

     failwith "give set contains more than one value"

@@ -54,8 +77,10 @@ let SetToOption set =
   else 

     Some(set |> Set.toList |> List.head)

 

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

 /// requires: n >= 0

 /// ensures:  |ret| = n && forall i :: 0 <= i < n ==> ret[i] = None

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

 let rec GenList n =

   if n < 0 then 

     failwith "n must be positive"

@@ -64,12 +89,16 @@ let rec GenList n =
   else

     None :: (GenList (n-1))

 

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

 /// ensures: ret = elem in lst

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

 let ListContains elem lst = 

   lst |> List.exists (fun e -> e = elem)

 

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

 /// ensures: |ret| = max(|lst| - cnt, 0)

 /// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]

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

 let rec ListSkip cnt lst = 

   if cnt = 0 then

     lst    

@@ -78,6 +107,7 @@ let rec ListSkip cnt lst =
     | fs :: rest -> ListSkip (cnt-1) rest

     | [] -> []

 

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

 /// ensures: forall i :: 0 <= i < max(|srcList|, |dstList|) ==> 

 ///            if i = idx then

 ///              ret[i] = v

@@ -85,6 +115,7 @@ let rec ListSkip cnt lst =
 ///              ret[i] = srcList[i]

 ///            else

 ///              ret[i] = dstList[i] 

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

 let rec ListBuild srcList idx v dstList =

   match srcList, dstList with

   | fs1 :: rest1, fs2 :: rest2 -> if idx = 0 then

@@ -97,11 +128,13 @@ let rec ListBuild srcList idx v dstList =
                                     fs2 :: ListBuild [] (idx-1) v rest2

   | _,            []           -> failwith "index out of range"

 

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

 /// ensures: forall i :: 0 <= i < |lst| ==>

 ///            if i = idx then

 ///              ret[i] = v

 ///            else

 ///              ret[i] = lst[i]

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

 let rec ListSet idx v lst =

   match lst with

   | fs :: rest -> if idx = 0 then 

@@ -110,6 +143,18 @@ let rec ListSet idx v lst =
                     fs :: ListSet (idx-1) v rest

   | [] -> failwith "index out of range"

 

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

+/// ensures: forall k,v :: 

+///            if k,v in map2 then

+//               k,v in ret

+///            elif k,v in map1 then

+///              k,v in ret

+///            else

+///              k,v !in ret

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

+let rec MapAddAll map1 map2 = 

+  map2 |> Map.fold (fun acc k v -> acc |> Map.add k v) map1

+                                                 

 // -------------------------------------------

 // ------ string active patterns -------------

 // -------------------------------------------

diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen
index 771fe680..b7ceaec0 100644
--- a/Jennisys/Jennisys/examples/List2.jen
+++ b/Jennisys/Jennisys/examples/List2.jen
@@ -8,7 +8,16 @@ class IntList {
     ensures list = [2]
 
   constructor OneTwo()
-    ensures list = [1] + [2]
+    ensures list = [1] + [2] 
+
+  constructor Singleton(p: int)
+    ensures list = [p]
+
+  constructor TwoConsecutive(p: int)
+    ensures list = [p] + [p+1]
+
+  constructor Double(p: int, q: int)
+    ensures list = [p] + [q]
 }
 
 model IntList {
diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen
index b668574b..f37a2631 100644
--- a/Jennisys/Jennisys/examples/List3.jen
+++ b/Jennisys/Jennisys/examples/List3.jen
@@ -45,6 +45,13 @@ class IntNode {
     ensures data = 1
     ensures |succ| = 1 && succ[0] != null && succ[0].data = 2
 
+  constructor Init(p: int)
+    ensures data = p
+
+  constructor InitInc(p: int)
+    ensures data = p + 1
+
+    
   invariant
     !(null in succ)
 }