diff options
| -rw-r--r-- | Jennisys/Jennisys/Analyzer.fs | 186 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Ast.fs | 25 | ||||
| -rw-r--r-- | Jennisys/Jennisys/AstUtils.fs | 223 | ||||
| -rw-r--r-- | Jennisys/Jennisys/CodeGen.fs | 9 | ||||
| -rw-r--r-- | Jennisys/Jennisys/DafnyModelUtils.fs | 21 | ||||
| -rw-r--r-- | Jennisys/Jennisys/EnvUtils.fs | 9 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Jennisys.fs | 2 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Jennisys.fsproj | 3 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Lexer.fsl | 2 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Logger.fs | 39 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Parser.fsy | 10 | ||||
| -rw-r--r-- | Jennisys/Jennisys/PipelineUtils.fs | 39 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Printer.fs | 38 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Resolver.fs | 71 | ||||
| -rw-r--r-- | Jennisys/Jennisys/TypeChecker.fs | 38 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Utils.fs | 51 | ||||
| -rw-r--r-- | Jennisys/Jennisys/examples/List2.jen | 11 | ||||
| -rw-r--r-- | Jennisys/Jennisys/examples/List3.jen | 7 |
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) } |