From 87e454054629237ce9b2dcf2a31de059bbda1749 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 6 Jul 2011 19:56:38 -0700 Subject: - fixed some bugs with applying unification over list elements - fixed the List.jen example (generic list) - changed SeqConst and SetConst to contain a list/set of "Const" and not "Const option" like before --- Jennisys/Analyzer.fs | 56 +++-- Jennisys/Ast.fs | 9 +- Jennisys/AstUtils.fs | 501 +++++++++++++++++++++++--------------------- Jennisys/CodeGen.fs | 272 ++++++++++++------------ Jennisys/DafnyModelUtils.fs | 87 ++++---- Jennisys/DafnyPrinter.fs | 12 +- Jennisys/Jennisys.fs | 10 +- Jennisys/Jennisys.fsproj | 12 +- Jennisys/Parser.fsy | 12 +- Jennisys/PipelineUtils.fs | 75 +++---- Jennisys/Printer.fs | 19 +- Jennisys/Resolver.fs | 33 +-- Jennisys/TypeChecker.fs | 32 +-- Jennisys/Utils.fs | 26 ++- Jennisys/examples/List.jen | 6 + Jennisys/examples/List3.jen | 2 +- 16 files changed, 619 insertions(+), 545 deletions(-) (limited to 'Jennisys') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 244b50b4..24b8cbc7 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -37,7 +37,12 @@ let rec Substitute substMap = function | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) | expr -> expr -let GenMethodAnalysisCode comp methodName signature pre post assertion = +let GenMethodAnalysisCode comp m assertion = + let methodName = GetMethodName m + let signature = GetMethodSig m + let ppre,ppost = GetMethodPrePost m + let pre = Desugar ppre + let post = Desugar ppost " method " + methodName + "()" + newline + " modifies this;" + newline + " {" + newline + @@ -61,7 +66,7 @@ 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 assertion) + newline + | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp m assertion) + newline | _ -> "" | _ -> "" @@ -142,20 +147,23 @@ let GetObjRefExpr o (heap,env,ctx) = _GetObjRefExpr o (heap,env,ctx) (Set.empty) let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = + let __CheckUnif o f e idx = + 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 lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) + let assertionExpr = BinaryEq lhs 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) + " ... ") + CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) + 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) + let value = TryResolve 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_" + (GetMethodFullName comp mthd)) - if ok then + if __CheckUnif o f e -1 then Logger.DebugLine " HOLDS" // change the value to expression acc |> Map.add (o,f) (ExprConst(e)) @@ -164,11 +172,24 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = // don't change the value acc |> Map.add (o,f) l else - // see if it's a list, then try to match its elements + // see if it's a list, then try to match its elements, otherwise leave it as is match value with - | SeqConst(clist) -> acc |> Map.add (o,f) l //TODO!! + | SeqConst(clist) -> + let rec __UnifyOverLst lst cnt = + match lst with + | lstElem :: rest when lstElem = c -> + if __CheckUnif o f e cnt then + Logger.DebugLine " HOLDS" + ExprConst(e) :: __UnifyOverLst rest (cnt+1) + else + Logger.DebugLine " DOESN'T HOLDS" + lstElem :: __UnifyOverLst rest (cnt+1) + | lstElem :: rest -> + lstElem :: __UnifyOverLst rest (cnt+1) + | [] -> [] + let newLstConst = __UnifyOverLst clist 0 + acc |> Map.add (o,f) (SeqConst(newLstConst)) | _ -> - // leave it as is acc |> Map.add (o,f) l ) restHeap (newHeap,env,ctx) @@ -181,7 +202,7 @@ let GeneralizeSolution prog comp mthd (heap,env,ctx) = match args with | [] -> (heap,env,ctx) | _ -> - let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx) + let unifs = GetUnifications (BinaryAnd pre post |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv |> Set.union (GetArgValueUnifications args env) UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx) | _ -> failwith ("not a method: " + mthd.ToString()) @@ -252,9 +273,10 @@ let rec AnalyzeMethods prog members = | _ -> AnalyzeMethods prog rest | [] -> Map.empty -let Analyze prog = +let Analyze prog filename = let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) - use file = System.IO.File.CreateText(dafnySynthFile) + let progName = System.IO.Path.GetFileNameWithoutExtension(filename) + use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName)) file.AutoFlush <- true Logger.InfoLine "Printing synthesized code" let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index bd66e688..5c42dbec 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -13,8 +13,8 @@ type Type = | BoolType | SetType of Type (* type parameter *) | SeqType of Type (* type parameter *) - | NamedType of string - | InstantiatedType of string * Type (* type parameter *) + | NamedType of string * string list (* type parameters *) + | InstantiatedType of string * Type list (* type parameters *) type VarDecl = | Var of string * Type option @@ -61,9 +61,10 @@ type Program = type Const = | IntConst of int | BoolConst of bool - | SetConst of Set - | SeqConst of (Const option) list + | SetConst of Set + | SeqConst of Const list | NullConst + | NoneConst | ThisConst of (* loc id *) string * Type option | NewObj of (* loc id *) string * Type option | ExprConst of Expr diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 442dfe57..af80fb65 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -10,17 +10,17 @@ 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 + 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 ------------------------------------------- @@ -28,186 +28,186 @@ let rec VisitExpr visitorFunc expr acc = exception EvalFailed let rec EvalSym expr = - match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> VarConst(id) - | Dot(e, str) -> - match EvalSym e with - | VarConst(lhsName) -> VarConst(lhsName + "." + str) - | _ -> ExprConst(expr) - | SeqLength(e) -> - match EvalSym e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> ExprConst(expr) - | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev |> Utils.ConvertToOptionList - SeqConst(clist) - | SelectExpr(lst, idx) -> - match EvalSym lst, EvalSym idx with - | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption - | _ -> ExprConst(expr) - | UpdateExpr(lst,idx,v) -> - match EvalSym lst, EvalSym idx, EvalSym v with - | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) - | _ -> ExprConst(expr) - | BinaryExpr(_,op,e1,e2) -> - match op with - | Exact "=" _ -> - match EvalSym e1, EvalSym e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) - | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) - | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) - | _ -> ExprConst(expr) - | Exact "!=" _ -> - match EvalSym e1, EvalSym e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) - | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) - | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) - | _ -> ExprConst(expr) - | Exact "<" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) - | _ -> ExprConst(expr) - | Exact "<=" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) - | _ -> ExprConst(expr) - | Exact ">" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) - | _ -> ExprConst(expr) - | Exact ">=" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) - | _ -> ExprConst(expr) - | Exact "in" _ -> - match EvalSym e1, EvalSym e2 with - | _ as c, SetConst(s) -> BoolConst(Set.contains (Some(c)) s) - | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains (Some(c)) s) - | _ -> ExprConst(expr) - | Exact "!in" _ -> - match EvalSym e1, EvalSym e2 with - | _ as c, SetConst(s) -> BoolConst(not (Set.contains (Some(c)) s)) - | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains (Some(c)) s)) - | _ -> ExprConst(expr) - | Exact "+" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) - | _ -> ExprConst(expr) - | Exact "-" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) - | _ -> ExprConst(expr) - | Exact "*" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) - | _ -> ExprConst(expr) - | Exact "div" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) - | _ -> ExprConst(expr) - | Exact "mod" _ -> - match EvalSym e1, EvalSym e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) - | UnaryExpr(op, e) -> - match op with - | Exact "!" _ -> - match EvalSym e with - | BoolConst(b) -> BoolConst(not b) - | _ -> ExprConst(expr) - | Exact "-" _ -> - match EvalSym e with - | IntConst(n) -> IntConst(-n) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) + match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) -> VarConst(id) + | Dot(e, str) -> + match EvalSym e with + | VarConst(lhsName) -> VarConst(lhsName + "." + str) + | _ -> ExprConst(expr) + | SeqLength(e) -> + match EvalSym e with + | SeqConst(clist) -> IntConst(List.length clist) + | _ -> ExprConst(expr) + | SequenceExpr(elist) -> + let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev + SeqConst(clist) + | SelectExpr(lst, idx) -> + match EvalSym lst, EvalSym idx with + | SeqConst(clist), IntConst(n) -> clist.[n] + | _ -> ExprConst(expr) + | UpdateExpr(lst,idx,v) -> + match EvalSym lst, EvalSym idx, EvalSym v with + | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist) + | _ -> ExprConst(expr) + | BinaryExpr(_,op,e1,e2) -> + match op with + | Exact "=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) + | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) + | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) + | _ -> ExprConst(expr) + | Exact "!=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) + | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) + | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) + | _ -> ExprConst(expr) + | Exact "<" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) + | _ -> ExprConst(expr) + | Exact "<=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) + | _ -> ExprConst(expr) + | Exact "in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(Set.contains c s) + | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s) + | _ -> ExprConst(expr) + | Exact "!in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s)) + | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s)) + | _ -> ExprConst(expr) + | Exact "+" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) + | _ -> ExprConst(expr) + | Exact "*" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) + | _ -> ExprConst(expr) + | Exact "div" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) + | _ -> ExprConst(expr) + | Exact "mod" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + | UnaryExpr(op, e) -> + match op with + | Exact "!" _ -> + match EvalSym e with + | BoolConst(b) -> BoolConst(not b) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e with + | IntConst(n) -> IntConst(-n) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) | _ -> ExprConst(expr) //TODO: stuff might be missing let rec EvalToConst expr = - match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> raise EvalFailed //VarConst(id) - | Dot(e, str) -> raise EvalFailed - | SeqLength(e) -> - match EvalToConst e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> 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 - + match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) -> raise EvalFailed //VarConst(id) + | Dot(e, str) -> raise EvalFailed + | SeqLength(e) -> + match EvalToConst e with + | SeqConst(clist) -> IntConst(List.length clist) + | _ -> raise EvalFailed + | SequenceExpr(elist) -> + let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev + SeqConst(clist) + | SelectExpr(lst, idx) -> + match EvalToConst lst, EvalToConst idx with + | SeqConst(clist), IntConst(n) -> clist.[n] + | _ -> raise EvalFailed + | UpdateExpr(lst,idx,v) -> + match EvalToConst lst, EvalToConst idx, EvalToConst v with + | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n 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 + let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev SequenceExpr(expList) | ThisConst(_) -> IdLiteral("this") | VarConst(v) -> IdLiteral(v) @@ -264,64 +264,64 @@ 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 = +// ========================================== +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 -/// constructors and have at least one input parameter -// ============================================================= -let FilterConstructorMembersWithParams members = - members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) - -// ========================================================== -/// Out of all "members" returns only those that are "Method"s -// ========================================================== -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) -> - components |> List.fold (fun acc comp -> - match comp with - | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))] +// ========================================================= +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 +/// constructors and have at least one input parameter +// ============================================================= +let FilterConstructorMembersWithParams members = + members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) + +// ========================================================== +/// Out of all "members" returns only those that are "Method"s +// ========================================================== +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) -> + components |> List.fold (fun acc comp -> + match comp with + | 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,_,_), _) -> - let aVars = FilterFieldMembers members + match comp with + | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) -> + let aVars = FilterFieldMembers members List.concat [aVars ; cVars] | _ -> [] @@ -333,6 +333,11 @@ let GetClassName comp = | Component(Class(name,_,_),_,_) -> name | _ -> failwith ("unrecognized component: " + comp.ToString()) +let GetClassType comp = + match comp with + | Component(Class(name,typeParams,_),_,_) -> NamedType(name, typeParams) + | _ -> failwith ("unrecognized component: " + comp.ToString()) + // ======================== /// Returns name of a method // ======================== @@ -355,6 +360,11 @@ let GetMethodSig mthd = | Method(_,sgn,_,_,_) -> sgn | _ -> failwith ("not a method: " + mthd.ToString()) +let GetMethodPrePost mthd = + match mthd with + | Method(_,_,pre,post,_) -> pre,post + | _ -> failwith ("not a method: " + mthd.ToString()) + // ========================================================= /// Returns all arguments of a method (both input and output) // ========================================================= @@ -363,6 +373,15 @@ let GetMethodArgs mthd = | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs] | _ -> failwith ("not a method: " + mthd.ToString()) +let rec GetTypeShortName ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | SetType(_) -> "set" + | SeqType(_) -> "seq" + | NamedType(n,_) -> n + | InstantiatedType(n,_) -> n + // ============================================================== /// Returns all invariants of a component as a list of expressions // ============================================================== @@ -415,17 +434,17 @@ let FindVar (prog: Program) clsName fldName = /// 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) + 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 @@ -436,13 +455,13 @@ let rec Desugar expr = | 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) + | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr 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) + | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr cl1.[cnt]) (Const2Expr 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 diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index 7e61ec7e..3c97b94f 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -2,7 +2,7 @@ open Ast open AstUtils -open Utils +open Utils open Printer open Resolver open TypeChecker @@ -18,143 +18,143 @@ let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr (BinaryAnd (Dot(fldExpr, validFunName)) (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1))) -let GetFieldValidExpr fldName validFunName numUnrolls : Expr = - GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls - //BinaryImplies (BinaryNeq (IdLiteral(fldName)) (IdLiteral("null"))) (Dot(IdLiteral(fldName), validFunName)) - -let GetFieldsForValidExpr allFields prog : VarDecl list = - allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true - | _ -> false) - -let GetFieldsValidExprList clsName allFields prog : Expr list = - let fields = GetFieldsForValidExpr allFields prog - fields |> List.map (function Var(name, t) -> - let validFunName, numUnrolls = - match t with - | Some(ty) when clsName = (PrintType ty) -> "Valid_self()", numLoopUnrolls - | _ -> "Valid()", 1 - GetFieldValidExpr name validFunName numUnrolls - ) - -let PrintValidFunctionCode comp prog : string = - let clsName = GetClassName comp - let vars = GetAllFields comp - let allInvs = GetInvariantsAsList comp - let fieldsValid = GetFieldsValidExprList clsName vars prog - let idt = " " - let PrintInvs invs = - invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) [] - |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e)) - |> fun s -> if s = "" then (idt + "true") else s - // TODO: don't hardcode decr vars!!! -// let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then -// ["list"] -// else -// [] -// (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) + - " function Valid_self(): bool" + newline + - " reads *;" + newline + - " {" + newline + - (PrintInvs allInvs) + newline + - " }" + newline + - newline + - " function Valid(): bool" + newline + - " reads *;" + newline + - " {" + newline + - " this.Valid_self() &&" + newline + - (PrintInvs fieldsValid) + newline + +let GetFieldValidExpr fldName validFunName numUnrolls : Expr = + GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls + +let GetFieldsForValidExpr allFields prog : VarDecl list = + allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true + | _ -> false) + +let GetFieldsValidExprList clsName allFields prog : Expr list = + let fields = GetFieldsForValidExpr allFields prog + fields |> List.map (function Var(name, t) -> + let validFunName, numUnrolls = + match t with + | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", numLoopUnrolls + | _ -> "Valid()", 1 + GetFieldValidExpr name validFunName numUnrolls + ) + +let PrintValidFunctionCode comp prog : string = + let idt = " " + let __PrintInvs invs = + invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) [] + |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e)) + |> fun s -> if s = "" then (idt + "true") else s + let clsName = GetClassName comp + let vars = GetAllFields comp + let allInvs = GetInvariantsAsList comp |> DesugarLst + let fieldsValid = GetFieldsValidExprList clsName vars prog + + // TODO: don't hardcode decr vars!!! +// let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then +// ["list"] +// else +// [] +// (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) + + " function Valid_self(): bool" + newline + + " reads *;" + newline + + " {" + newline + + (__PrintInvs allInvs) + newline + + " }" + newline + + newline + + " function Valid(): bool" + newline + + " reads *;" + newline + + " {" + newline + + " this.Valid_self() &&" + newline + + (__PrintInvs fieldsValid) + newline + " }" + newline -let PrintDafnyCodeSkeleton prog methodPrinterFunc: string = - match prog with - | Program(components) -> components |> List.fold (fun acc comp -> - match comp with - | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp -> - let aVars = FilterFieldMembers members - let allVars = List.concat [aVars ; cVars]; - let compMethods = FilterConstructorMembers members - // Now print it as a Dafny program - acc + - (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline + - // the fields: original abstract fields plus concrete fields - (sprintf "%s" (PrintFields aVars 2 true)) + newline + - (sprintf "%s" (PrintFields cVars 2 false)) + newline + - // generate the Valid function - (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline + - // call the method printer function on all methods of this component - (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") + - // the end of the class - "}" + newline + newline +let PrintDafnyCodeSkeleton prog methodPrinterFunc: string = + match prog with + | Program(components) -> components |> List.fold (fun acc comp -> + match comp with + | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp -> + let aVars = FilterFieldMembers members + let allVars = List.concat [aVars ; cVars]; + let compMethods = FilterConstructorMembers members + // Now print it as a Dafny program + acc + + (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline + + // the fields: original abstract fields plus concrete fields + (sprintf "%s" (PrintFields aVars 2 true)) + newline + + (sprintf "%s" (PrintFields cVars 2 false)) + newline + + // generate the Valid function + (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline + + // call the method printer function on all methods of this component + (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") + + // the end of the class + "}" + newline + newline | _ -> assert false; "") "" -let PrintAllocNewObjects (heap,env,ctx) indent = - let idt = Indent indent - env |> Map.fold (fun acc l v -> - match v with - | NewObj(_,_) -> acc |> Set.add v - | _ -> acc - ) Set.empty - |> Set.fold (fun acc newObjConst -> - match newObjConst with - | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline) - | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString()) - ) "" - -let PrintObjRefName o (env,ctx) = - match Resolve o (env,ctx) with - | ThisConst(_,_) -> "this"; - | NewObj(name, _) -> PrintGenSym name - | _ -> failwith ("unresolved object ref: " + o.ToString()) - -let PrintVarAssignments (heap,env,ctx) indent = - let idt = Indent indent - heap |> Map.fold (fun acc (o,f) l -> - let objRef = PrintObjRefName o (env,ctx) - let fldName = PrintVarName f - let value = Resolve l (env,ctx) |> PrintConst - acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline - ) "" - -let PrintHeapCreationCode (heap,env,ctx) indent = - (PrintAllocNewObjects (heap,env,ctx) indent) + - (PrintVarAssignments (heap,env,ctx) indent) - -let GenConstructorCode mthd body = - let validExpr = IdLiteral("Valid()"); - match mthd with - | Method(methodName, sign, pre, post, _) -> - let preExpr = BinaryAnd validExpr pre - let postExpr = BinaryAnd validExpr post - let PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";") - " method " + methodName + (PrintSig sign) + newline + - " modifies this;" + newline + - (PrintPrePost " requires " preExpr) + newline + - (PrintPrePost " ensures " postExpr) + newline + - " {" + newline + - body + - " }" + newline - | _ -> "" - -// NOTE: insert here coto to say which methods to analyze -let GetMethodsToAnalyze prog = - (* exactly one *) -// let c = FindComponent prog "IntList" |> Utils.ExtractOption -// let m = FindMethod c "Sum" |> Utils.ExtractOption -// [c, m] - (* all *) - FilterMembers prog FilterConstructorMembers - (* only with parameters *) -// FilterMembers prog FilterConstructorMembersWithParams - -// solutions: (comp, constructor) |--> (heap, env, ctx) -let PrintImplCode prog solutions methodsToPrintFunc = - let methods = methodsToPrintFunc prog - PrintDafnyCodeSkeleton prog (fun comp mthd -> - if Utils.ListContains (comp,mthd) methods then - let mthdBody = match Map.tryFind (comp,mthd) solutions with - | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4 - | _ -> " //unable to synthesize" + newline - (GenConstructorCode mthd mthdBody) + newline - else - "" +let PrintAllocNewObjects (heap,env,ctx) indent = + let idt = Indent indent + env |> Map.fold (fun acc l v -> + match v with + | NewObj(_,_) -> acc |> Set.add v + | _ -> acc + ) Set.empty + |> Set.fold (fun acc newObjConst -> + match newObjConst with + | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline) + | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString()) + ) "" + +let PrintObjRefName o (env,ctx) = + match Resolve o (env,ctx) with + | ThisConst(_,_) -> "this"; + | NewObj(name, _) -> PrintGenSym name + | _ -> failwith ("unresolved object ref: " + o.ToString()) + +let PrintVarAssignments (heap,env,ctx) indent = + let idt = Indent indent + heap |> Map.fold (fun acc (o,f) l -> + let objRef = PrintObjRefName o (env,ctx) + let fldName = PrintVarName f + let value = Resolve l (env,ctx) |> PrintConst + acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline + ) "" + +let PrintHeapCreationCode (heap,env,ctx) indent = + (PrintAllocNewObjects (heap,env,ctx) indent) + + (PrintVarAssignments (heap,env,ctx) indent) + +let GenConstructorCode mthd body = + let validExpr = IdLiteral("Valid()"); + match mthd with + | Method(methodName, sign, pre, post, _) -> + let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";") + let preExpr = pre + let postExpr = BinaryAnd validExpr post + " method " + methodName + (PrintSig sign) + newline + + " modifies this;" + newline + + (__PrintPrePost " requires " preExpr) + newline + + (__PrintPrePost " ensures " postExpr) + newline + + " {" + newline + + body + + " }" + newline + | _ -> "" + +// NOTE: insert here coto to say which methods to analyze +let GetMethodsToAnalyze prog = + (* exactly one *) +// let c = FindComponent prog "List" |> Utils.ExtractOption +// let m = FindMethod c "Double" |> Utils.ExtractOption +// [c, m] + (* all *) + FilterMembers prog FilterConstructorMembers + (* only with parameters *) +// FilterMembers prog FilterConstructorMembersWithParams + +// solutions: (comp, constructor) |--> (heap, env, ctx) +let PrintImplCode prog solutions methodsToPrintFunc = + let methods = methodsToPrintFunc prog + PrintDafnyCodeSkeleton prog (fun comp mthd -> + if Utils.ListContains (comp,mthd) methods then + let mthdBody = match Map.tryFind (comp,mthd) solutions with + | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4 + | _ -> " //unable to synthesize" + newline + (GenConstructorCode mthd mthdBody) + newline + else + "" ) \ No newline at end of file diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index 6e78dc33..597ac7c9 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -23,16 +23,16 @@ open Microsoft.Boogie 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)) + elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0) + |> Seq.choose (fun ft -> Some(ft.Func.Name)) |> Utils.SeqToOption let GetElemName (elem: Model.Element) = - let fullNameOpt = GetElemFullName elem - match fullNameOpt with - | Some(fullName) -> - let dotIdx = fullName.LastIndexOf(".") - let fldName = fullName.Substring(dotIdx + 1) + let fullNameOpt = GetElemFullName elem + match fullNameOpt with + | Some(fullName) -> + let dotIdx = fullName.LastIndexOf(".") + let fldName = fullName.Substring(dotIdx + 1) let clsName = if dotIdx = -1 then "" else fullName.Substring(0, dotIdx) Some(clsName, fldName) | None -> None @@ -60,12 +60,15 @@ let GetBool (elem: Model.Element) = | :? Model.Boolean as bval -> bval.Value | _ -> failwith ("not a bool element: " + elem.ToString()) -let GetType (e: Model.Element) = +let GetType (e: Model.Element) prog = let fNameOpt = GetElemFullName e match fNameOpt with | Some(fname) -> match fname with | Exact "intType" _ -> Some(IntType) - | Prefix "class." clsName -> Some(NamedType(clsName)) + | Prefix "class." clsName -> + match FindComponent prog clsName with + | Some(comp) -> Some(GetClassType comp) + | None -> None | _ -> None | None -> None @@ -100,8 +103,8 @@ let rec UpdateContext lst1 lst2 ctx = match lst1, lst2 with | fs1 :: rest1, fs2 :: rest2 -> match fs1, fs2 with - | Some(c1), Some(c2) -> UpdateContext rest1 rest2 (AddConstr c1 c2 ctx) - | _ -> UpdateContext rest1 rest2 ctx + | NoneConst,_ | _,NoneConst -> UpdateContext rest1 rest2 ctx + | _ -> UpdateContext rest1 rest2 (AddConstr fs1 fs2 ctx) | [], [] -> ctx | _ -> failwith "lists are not of the same length" @@ -115,27 +118,27 @@ let UnboxIfNeeded (model: Microsoft.Boogie.Model) (e: Model.Element) = | None -> GetLoc e let ReadHeap (model: Microsoft.Boogie.Model) prog = - let f_heap_select = model.MkFunc("[3]", 3) - let values = f_heap_select.Apps - values |> Seq.fold (fun acc ft -> - assert (ft.Args.Length = 3) - let ref = ft.Args.[1] - let fld = ft.Args.[2] - assert (Seq.length fld.Names = 1) - let fldFullName = (Seq.nth 0 fld.Names).Func.Name - let dotIdx = fldFullName.LastIndexOf(".") - let fldName = fldFullName.Substring(dotIdx + 1) - let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx) - let refVal = ft.Result - let refObj = Unresolved(GetRefName ref) - let fldVarOpt = FindVar prog clsName fldName - match fldVarOpt with - | Some(fldVar) -> - let fldType = match fldVar with - | Var(_,t) -> t - let fldVal = ConvertValue model refVal - acc |> Map.add (refObj, fldVar) fldVal - | None -> acc + let f_heap_select = model.MkFunc("[3]", 3) + let values = f_heap_select.Apps + values |> Seq.fold (fun acc ft -> + assert (ft.Args.Length = 3) + let ref = ft.Args.[1] + let fld = ft.Args.[2] + assert (Seq.length fld.Names = 1) + let fldFullName = (Seq.nth 0 fld.Names).Func.Name + let dotIdx = fldFullName.LastIndexOf(".") + let fldName = fldFullName.Substring(dotIdx + 1) + let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx) + let refVal = ft.Result + let refObj = Unresolved(GetRefName ref) + let fldVarOpt = FindVar prog clsName fldName + match fldVarOpt with + | Some(fldVar) -> + let fldType = match fldVar with + | Var(_,t) -> t + let fldVal = ConvertValue model refVal + acc |> Map.add (refObj, fldVar) fldVal + | None -> acc ) Map.empty let rec ReadArgValues (model: Microsoft.Boogie.Model) args = @@ -157,7 +160,7 @@ let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple match len_tuples with | ft :: rest -> let len = GetInt ft.Result - let emptyList = Utils.GenList len + let emptyList = Utils.GenList len NoneConst let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList)) ReadSeqLen model rest (newMap,ctx) | _ -> (envMap,ctx) @@ -169,7 +172,7 @@ let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTupl let oldLst = GetSeqFromEnv envMap srcLstKey let idx = GetInt ft.Args.[1] let lstElem = UnboxIfNeeded model ft.Result - let newLst = Utils.ListSet idx (Some(lstElem)) oldLst + let newLst = Utils.ListSet idx lstElem oldLst let newCtx = UpdateContext oldLst newLst ctx let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst)) ReadSeqIndex model rest (newEnv,newCtx) @@ -184,7 +187,7 @@ let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTupl let idx = GetInt ft.Args.[1] let lstElemVal = UnboxIfNeeded model ft.Args.[2] let dstLst = GetSeqFromEnv envMap dstLstLoc - let newLst = Utils.ListBuild oldLst idx (Some(lstElemVal)) dstLst + let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst let newCtx = UpdateContext dstLst newLst ctx let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) ReadSeqBuild model rest (newEnv,newCtx) @@ -226,14 +229,14 @@ let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = let newEnv = envMap |> Map.add (GetLoc e) NullConst (newEnv,ctx) -let ReadEnv (model: Microsoft.Boogie.Model) = - let f_dtype = model.MkFunc("dtype", 1) +let ReadEnv (model: Microsoft.Boogie.Model) prog = + let f_dtype = model.MkFunc("dtype", 1) let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0])) let envMap = f_dtype.Apps |> Seq.fold (fun acc ft -> let locName = GetRefName ft.Args.[0] let elemName = GetElemFullName ft.Args.[0] let loc = Unresolved(locName) - let locType = GetType ft.Result + let locType = GetType ft.Result prog let value = match elemName with | Some(n) when n.StartsWith("this") -> ThisConst(locName.Replace("*", ""), locType) | _ -> NewObj(locName.Replace("*", ""), locType) @@ -243,8 +246,8 @@ let ReadEnv (model: Microsoft.Boogie.Model) = |> ReadSeq model |> ReadSet model -let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth = - let heap = ReadHeap model prog - let env0,ctx = ReadEnv model - let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth)) +let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth = + let heap = ReadHeap model prog + let env0,ctx = ReadEnv model prog + let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth)) heap,env,ctx \ No newline at end of file diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index 87937850..fb9f3bf7 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -5,12 +5,12 @@ open Printer let rec PrintType ty = match ty with - | IntType -> "int" - | BoolType -> "bool" - | NamedType(id) -> id - | SeqType(t) -> sprintf "seq<%s>" (PrintType t) - | SetType(t) -> sprintf "set<%s>" (PrintType t) - | InstantiatedType(id,arg) -> sprintf "%s<%s>" id (PrintType arg) + | IntType -> "int" + | BoolType -> "bool" + | SeqType(t) -> sprintf "seq<%s>" (PrintType t) + | SetType(t) -> sprintf "set<%s>" (PrintType t) + | NamedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args) + | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args) let rec PrintExpr ctx expr = match expr with diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs index 0337c6a2..32827f39 100644 --- a/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys.fs @@ -38,18 +38,20 @@ let readAndProcess tracing analyzing (filename: string) = | Some(prog) -> if analyzing then // output a Dafny program with the constraints to be solved - Analyze prog + Analyze prog filename else () // that's it if tracing then printfn "----------" else () with - | ex -> - let pos = lexbuf.EndPos - printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + | ex -> + let pos = lexbuf.EndPos + printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + printfn "%s" (ex.StackTrace.ToString()) with | ex -> printfn "Unhandled Exception: %s" ex.Message + printfn "%s" (ex.StackTrace.ToString()) let rec start n (args: string []) tracing analyzing filename = if n < args.Length then diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 39ed1aed..bbb15dc4 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - C:\boogie\Jennisys\Jennisys\examples\List3.jen + C:\boogie\Jennisys\Jennisys\examples\List.jen pdbonly @@ -83,17 +83,21 @@ - - ModelViewer - {a678c6eb-b329-46a9-bbfc-7585f01acd7c} + + Model + {acef88d5-dadd-46da-bae1-2144d63f4c83} True + + check the equality sets let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet) @@ -23,24 +24,24 @@ let rec Resolve cst (env,ctx) = |> Utils.SetToOption match cOpt with | Some(c) -> c - | _ -> failwith ("failed to resolve " + cst.ToString()) - | _ -> failwith ("failed to resolve " + cst.ToString()) + | _ -> failResolver cst (env,ctx) + | _ -> failResolver cst (env,ctx) | 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 - ) [] + let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont c (env,ctx) failResolver :: 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 + let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont c (env,ctx) failResolver)) Set.empty SetConst(resolvedSet) | _ -> cst +let TryResolve cst (env,ctx) = + ResolveCont cst (env,ctx) (fun c (e,x) -> c) + +let Resolve cst (env,ctx) = + ResolveCont cst (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) + + + let rec EvalUnresolved expr (heap,env,ctx) = match expr with | IntLiteral(n) -> IntConst(n) @@ -57,7 +58,7 @@ let rec EvalUnresolved expr (heap,env,ctx) = let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) let idxC = EvalUnresolved idx (heap,env,ctx) match lstC, idxC with - | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | SeqConst(clist), IntConst(n) -> clist.[n] | _ -> failwith "can't eval SelectExpr" | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! // | Star @@ -73,6 +74,6 @@ let rec EvalUnresolved expr (heap,env,ctx) = let Eval expr (heap,env,ctx) = try let unresolvedConst = EvalUnresolved expr (heap,env,ctx) - Some(Resolve unresolvedConst (env,ctx)) + Some(TryResolve unresolvedConst (env,ctx)) with ex -> None \ No newline at end of file diff --git a/Jennisys/TypeChecker.fs b/Jennisys/TypeChecker.fs index 7414f253..377082d9 100644 --- a/Jennisys/TypeChecker.fs +++ b/Jennisys/TypeChecker.fs @@ -6,34 +6,34 @@ open System.Collections.Generic let GetClass name decls = match decls |> List.tryFind (function Class(n,_,_) when n = name -> true | _ -> false) with - | Some(cl) -> cl - | None -> Class(name,[],[]) + | Some(cl) -> cl + | None -> Class(name,[],[]) let GetModel name decls = match decls |> List.tryFind (function Model(n,_,_,_,_) when n = name -> true | _ -> false) with - | Some(m) -> m - | None -> Model(name,[],[],[],IdLiteral("true")) + | Some(m) -> m + | None -> Model(name,[],[],[],IdLiteral("true")) let GetCode name decls = match decls |> List.tryFind (function Code(n,_) when n = name -> true | _ -> false) with - | Some(c) -> c - | None -> Code(name,[]) + | Some(c) -> c + | None -> Code(name,[]) let IsUserType prog tpo = match tpo with - | Some(tp) -> - let tpname = match tp with - | NamedType(tname) -> tname - | InstantiatedType(tname, _) -> tname - | _ -> "" - match prog with - | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true - | _ -> false) |> List.isEmpty |> not - | None -> false + | Some(tp) -> + let tpname = match tp with + | NamedType(tname,_) -> tname + | InstantiatedType(tname, _) -> tname + | _ -> "" + match prog with + | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true + | _ -> false) |> List.isEmpty |> not + | None -> false let TypeCheck prog = match prog with - | SProgram(decls) -> + | SProgram(decls) -> 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)) diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index 3cb8fee4..6540173c 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -77,17 +77,17 @@ 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 = +/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = e +// ============================================================ +let rec GenList n e = if n < 0 then failwith "n must be positive" if n = 0 then [] else - None :: (GenList (n-1)) + e :: (GenList (n-1) e) // ========================== /// ensures: ret = elem in lst @@ -171,3 +171,19 @@ let (|Exact|_|) (p:string) (s:string) = else None +// ------------------------------------------- +// ----------------- random ------------------ +// ------------------------------------------- + +let IfDo1 cond func1 a = + if cond then + func1 a + else + a + +let IfDo2 cond func2 (a1,a2) = + if cond then + func2 a1 a2 + else + a1,a2 + diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen index 184f4947..e7f42ddc 100644 --- a/Jennisys/examples/List.jen +++ b/Jennisys/examples/List.jen @@ -6,6 +6,9 @@ class List[T] { constructor Singleton(t: T) ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] } model List[T] { @@ -27,6 +30,9 @@ class Node[T] { constructor Init(t: T) ensures list = [t] + + constructor Double(p: T, q: T) + ensures list = [p q] } model Node[T] { diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen index 6bb49eb8..acb10ad5 100644 --- a/Jennisys/examples/List3.jen +++ b/Jennisys/examples/List3.jen @@ -33,7 +33,7 @@ model IntList { root = null ==> |list| = 0 root != null ==> (|list| = |root.succ| + 1 && list[0] = root.data && - (forall i:int :: (0 <= i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data))) + (forall i:int :: (0 < i && i <= |root.succ|) ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data))) } class IntNode { -- cgit v1.2.3 From dbb1fbe420eddf778da724c5eec6549ce068c28d Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 8 Jul 2011 16:46:05 -0700 Subject: - removed VarConst from Const - generalized the AstUtils.EvalSym functions and made the Resolver.Eval function re-use it. --- Jennisys/Analyzer.fs | 628 ++++++++++++++++++++++---------------------- Jennisys/Ast.fs | 10 +- Jennisys/AstUtils.fs | 197 +++++--------- Jennisys/CodeGen.fs | 8 +- Jennisys/DafnyModelUtils.fs | 157 ++++++----- Jennisys/DafnyPrinter.fs | 3 +- Jennisys/Jennisys.fsproj | 2 +- Jennisys/Options.fs | 6 +- Jennisys/PipelineUtils.fs | 8 +- Jennisys/Printer.fs | 4 +- Jennisys/Resolver.fs | 96 +++---- Jennisys/Utils.fs | 45 ++-- 12 files changed, 578 insertions(+), 586 deletions(-) (limited to 'Jennisys') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 24b8cbc7..8737ad86 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -1,317 +1,319 @@ -module Analyzer - -open Ast -open AstUtils -open CodeGen -open DafnyModelUtils -open PipelineUtils -open Options -open Printer -open Resolver -open DafnyPrinter -open Utils - -open Microsoft.Boogie - -let VarsAreDifferent aa bb = - printf "false" - List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb - -let Rename suffix vars = - vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp)) - -let ReplaceName substMap nm = - match Map.tryFind nm substMap with - | Some(Var(name, tp)) -> name - | None -> nm - -let rec Substitute substMap = function - | IdLiteral(s) -> IdLiteral(ReplaceName substMap s) - | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f) - | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e) - | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1) - | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1) - | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2) - | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee) - | SeqLength(e) -> SeqLength(Substitute substMap e) - | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) - | expr -> expr - -let GenMethodAnalysisCode comp m assertion = - let methodName = GetMethodName m - let signature = GetMethodSig m - let ppre,ppost = GetMethodPrePost m - let pre = Desugar ppre - let post = Desugar ppost - " method " + methodName + "()" + newline + - " modifies this;" + newline + - " {" + newline + - // print signature as local variables - (match signature with - | Sig(ins,outs) -> - List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") + - " // assume precondition" + newline + - " assume " + (PrintExpr 0 pre) + ";" + newline + - " // assume invariant and postcondition" + newline + - " assume Valid();" + newline + - " assume " + (PrintExpr 0 post) + ";" + newline + - " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + - (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 " + (PrintExpr 0 assertion) + ";" + newline + - " }" + newline - -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 m 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.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); - Set.empty - else - GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) - -let rec GetArgValueUnifications args env = - match args with - | Var(name,_) :: rest -> - match Map.tryFind (VarConst(name)) env with - | Some(c) -> - Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); - Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) - | None -> failwith ("couldn't find value for argument " + name) - | [] -> Set.empty - -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) = - let __CheckUnif o f e idx = - 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 lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) - let assertionExpr = BinaryEq lhs 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) + " ... ") - CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) - - 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 = TryResolve l (env,ctx) - if value = c then - if __CheckUnif o f e -1 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 - // see if it's a list, then try to match its elements, otherwise leave it as is - match value with - | SeqConst(clist) -> - let rec __UnifyOverLst lst cnt = - match lst with - | lstElem :: rest when lstElem = c -> - if __CheckUnif o f e cnt then - Logger.DebugLine " HOLDS" - ExprConst(e) :: __UnifyOverLst rest (cnt+1) - else - Logger.DebugLine " DOESN'T HOLDS" - lstElem :: __UnifyOverLst rest (cnt+1) - | lstElem :: rest -> - lstElem :: __UnifyOverLst rest (cnt+1) - | [] -> [] - let newLstConst = __UnifyOverLst clist 0 - acc |> Map.add (o,f) (SeqConst(newLstConst)) - | _ -> - 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 |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv - |> 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 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]) - CheckDafnyProgram code dafnyVerifySuffix - -// ============================================================================ +module Analyzer + +open Ast +open AstUtils +open CodeGen +open DafnyModelUtils +open PipelineUtils +open Options +open Printer +open Resolver +open DafnyPrinter +open Utils + +open Microsoft.Boogie + +let VarsAreDifferent aa bb = + printf "false" + List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb + +let Rename suffix vars = + vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp)) + +let ReplaceName substMap nm = + match Map.tryFind nm substMap with + | Some(Var(name, tp)) -> name + | None -> nm + +let rec Substitute substMap = function + | IdLiteral(s) -> IdLiteral(ReplaceName substMap s) + | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f) + | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e) + | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1) + | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1) + | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2) + | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee) + | SeqLength(e) -> SeqLength(Substitute substMap e) + | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e) + | expr -> expr + +let GenMethodAnalysisCode comp m assertion = + let methodName = GetMethodName m + let signature = GetMethodSig m + let ppre,ppost = GetMethodPrePost m + let pre = Desugar ppre + let post = Desugar ppost + " method " + methodName + "()" + newline + + " modifies this;" + newline + + " {" + newline + + // print signature as local variables + (match signature with + | Sig(ins,outs) -> + List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") + + " // assume precondition" + newline + + " assume " + (PrintExpr 0 pre) + ";" + newline + + " // assume invariant and postcondition" + newline + + " assume Valid();" + newline + + " assume " + (PrintExpr 0 post) + ";" + newline + + " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + + (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 " + (PrintExpr 0 assertion) + ";" + newline + + " }" + newline + +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 m assertion) + newline + | _ -> "" + | _ -> "" + +let rec IsArgsOnly args expr = + match expr with + | IntLiteral(_) -> true + | BoolLiteral(_) -> true + | 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 + | Star -> true + +let rec GetUnifications expr args (heap,env,ctx) = + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | 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 (heap,env,ctx) e0 + let v1 = Eval (heap,env,ctx) e1 + 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.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); + Set.empty + else + GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) + +let rec GetArgValueUnifications args env = + match args with + | Var(name,_) :: rest -> + match Map.tryFind (Unresolved(name)) env with + | Some(c) -> + Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); + Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) + | None -> failwith ("couldn't find value for argument " + name) + | [] -> Set.empty + +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) = + let __CheckUnif o f e idx = + 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 lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) + let assertionExpr = BinaryEq lhs 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) + " ... ") + CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) + + 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 = TryResolve (env,ctx) l + if value = c then + if __CheckUnif o f e -1 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 + // see if it's a list, then try to match its elements, otherwise leave it as is + match value with + | SeqConst(clist) -> + let rec __UnifyOverLst lst cnt = + match lst with + | lstElem :: rest when lstElem = c -> + if __CheckUnif o f e cnt then + Logger.DebugLine " HOLDS" + ExprConst(e) :: __UnifyOverLst rest (cnt+1) + else + Logger.DebugLine " DOESN'T HOLDS" + lstElem :: __UnifyOverLst rest (cnt+1) + | lstElem :: rest -> + lstElem :: __UnifyOverLst rest (cnt+1) + | [] -> [] + let newLstConst = __UnifyOverLst clist 0 + acc |> Map.add (o,f) (SeqConst(newLstConst)) + | _ -> + 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 |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv + |> 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 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]) + 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) FalseLiteral) +/// 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) FalseLiteral) Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m))) - Logger.Info " - searching for a solution ..." - let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) - if models.Count = 0 then - // no models means that the "assert false" was verified, which means that the spec is inconsistent - Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!" - None - else - if models.Count > 1 then - Logger.WarnLine " FAILED " - failwith "internal error (more than one model for a single constructor analysis)" - Logger.InfoLine " OK " - let model = models.[0] - let heap,env,ctx = ReadFieldValuesFromModel model prog comp m - |> GeneralizeSolution prog comp m - if _opt_verifySolutions then - Logger.InfoLine " - verifying synthesized solution ... " - let verified = VerifySolution prog comp m (heap,env,ctx) - Logger.Info " " - if verified then - Logger.InfoLine "~~~ VERIFIED ~~~" - Some(heap,env,ctx) - else - Logger.InfoLine "!!! NOT VERIFIED !!!" - 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 -> - match m with - | Method(_,_,_,_,true) -> - let solOpt = AnalyzeConstructor prog comp m - Logger.InfoLine "" - match solOpt with - | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx) - | None -> AnalyzeMethods prog rest - | _ -> AnalyzeMethods prog rest - | [] -> Map.empty - -let Analyze prog filename = - let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) - let progName = System.IO.Path.GetFileNameWithoutExtension(filename) - use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName)) - file.AutoFlush <- true - Logger.InfoLine "Printing synthesized code" - let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze - fprintfn file "%s" synthCode - () - -//let AnalyzeComponent_rustan c = -// match c with -// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) -> -// let aVars = Fields members -// let aVars0 = Rename "0" aVars -// let aVars1 = Rename "1" aVars -// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars] -// let inv0 = Substitute (Map.ofList aVars0) inv -// let inv1 = Substitute (Map.ofList aVars1) inv -// // Now print it as a Dafny program -// printf "class %s" name -// match typeParams with -// | [] -> () -// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) -// printfn " {" -// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields -// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp)) -// // the method -// printfn " method %s_checkInjective() {" name -// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";" -// printfn " assume %s;" (PrintExpr 0 inv0) -// printfn " assume %s;" (PrintExpr 0 inv1) -// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"} -// printfn " }" -// // generate code -// members |> List.iter (function -// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false) -// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true) -// | _ -> ()) -// // the end of the class -// printfn "}" + Logger.Info " - searching for a solution ..." + let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) + if models.Count = 0 then + // no models means that the "assert false" was verified, which means that the spec is inconsistent + Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!" + None + else + if models.Count > 1 then + Logger.WarnLine " FAILED " + failwith "internal error (more than one model for a single constructor analysis)" + Logger.InfoLine " OK " + let model = models.[0] + let heap,env,ctx = ReadFieldValuesFromModel model prog comp m + |> GeneralizeSolution prog comp m + if _opt_verifySolutions then + Logger.InfoLine " - verifying synthesized solution ... " + let verified = VerifySolution prog comp m (heap,env,ctx) + Logger.Info " " + if verified then + Logger.InfoLine "~~~ VERIFIED ~~~" + Some(heap,env,ctx) + else + Logger.InfoLine "!!! NOT VERIFIED !!!" + 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 -> + match m with + | Method(_,_,_,_,true) -> + let solOpt = AnalyzeConstructor prog comp m + Logger.InfoLine "" + match solOpt with + | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx) + | None -> AnalyzeMethods prog rest + | _ -> AnalyzeMethods prog rest + | [] -> Map.empty + +let Analyze prog filename = + let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) + let progName = System.IO.Path.GetFileNameWithoutExtension(filename) + use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName)) + file.AutoFlush <- true + Logger.InfoLine "Printing synthesized code" + let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze + fprintfn file "%s" synthCode + () + +//let AnalyzeComponent_rustan c = +// match c with +// | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) -> +// let aVars = Fields members +// let aVars0 = Rename "0" aVars +// let aVars1 = Rename "1" aVars +// let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars] +// let inv0 = Substitute (Map.ofList aVars0) inv +// let inv1 = Substitute (Map.ofList aVars1) inv +// // Now print it as a Dafny program +// printf "class %s" name +// match typeParams with +// | [] -> () +// | _ -> printf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) +// printfn " {" +// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields +// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp)) +// // the method +// printfn " method %s_checkInjective() {" name +// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";" +// printfn " assume %s;" (PrintExpr 0 inv0) +// printfn " assume %s;" (PrintExpr 0 inv1) +// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"} +// printfn " }" +// // generate code +// members |> List.iter (function +// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false) +// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true) +// | _ -> ()) +// // the end of the class +// printfn "}" // | _ -> assert false // unexpected case \ No newline at end of file diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 5c42dbec..167a5eef 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -1,7 +1,9 @@ -/// The AST of a Jennisy program +// #################################################################### +/// The AST of a Jennisy program /// -/// author: Rustan Leino (leino@microsoft.com) -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Rustan Leino (leino@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### namespace Ast @@ -21,6 +23,7 @@ type VarDecl = type Expr = | IntLiteral of int + | BoolLiteral of bool | IdLiteral of string | Star | Dot of Expr * string @@ -68,5 +71,4 @@ type Const = | 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/AstUtils.fs b/Jennisys/AstUtils.fs index af80fb65..26544f65 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -1,6 +1,8 @@ -/// Utility functions for manipulating AST elements +// #################################################################### +/// Utility functions for manipulating AST elements /// -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### module AstUtils @@ -12,6 +14,7 @@ open Utils let rec VisitExpr visitorFunc expr acc = match expr with | IntLiteral(_) + | BoolLiteral(_) | IdLiteral(_) | Star -> acc |> visitorFunc expr | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e @@ -27,190 +30,124 @@ let rec VisitExpr visitorFunc expr acc = exception EvalFailed -let rec EvalSym expr = +let DefaultResolver e = ExprConst(e) + +let rec EvalSym resolverFunc expr = match expr with | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> VarConst(id) - | Dot(e, str) -> - match EvalSym e with - | VarConst(lhsName) -> VarConst(lhsName + "." + str) - | _ -> ExprConst(expr) + | IdLiteral(_) | Dot(_) -> resolverFunc expr | SeqLength(e) -> - match EvalSym e with + match EvalSym resolverFunc e with | SeqConst(clist) -> IntConst(List.length clist) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev + let clist = elist |> List.fold (fun acc e -> EvalSym resolverFunc e :: acc) [] |> List.rev SeqConst(clist) | SelectExpr(lst, idx) -> - match EvalSym lst, EvalSym idx with + match EvalSym resolverFunc lst, EvalSym resolverFunc idx with | SeqConst(clist), IntConst(n) -> clist.[n] - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | UpdateExpr(lst,idx,v) -> - match EvalSym lst, EvalSym idx, EvalSym v with + match EvalSym resolverFunc lst, EvalSym resolverFunc idx, EvalSym resolverFunc v with | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | BinaryExpr(_,op,e1,e2) -> match op with | Exact "=" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) - | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) - | _ -> ExprConst(expr) + | ExprConst(e1), ExprConst(e2) -> BoolConst(e1 = e2) + | _ -> resolverFunc expr | Exact "!=" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) - | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) - | _ -> ExprConst(expr) + | ExprConst(e1), ExprConst(e2) -> BoolConst(not (e1 = e2)) + | _ -> resolverFunc expr | Exact "<" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "<=" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact ">" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact ">=" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "in" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | _ as c, SetConst(s) -> BoolConst(Set.contains c s) | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "!in" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s)) | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s)) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "+" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "-" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "*" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "div" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "mod" _ -> - match EvalSym e1, EvalSym e2 with + match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr + | _ -> resolverFunc expr | UnaryExpr(op, e) -> match op with | Exact "!" _ -> - match EvalSym e with + match EvalSym resolverFunc e with | BoolConst(b) -> BoolConst(not b) - | _ -> ExprConst(expr) + | _ -> resolverFunc expr | Exact "-" _ -> - match EvalSym e with + match EvalSym resolverFunc e with | IntConst(n) -> IntConst(-n) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) - | _ -> ExprConst(expr) - -//TODO: stuff might be missing -let rec EvalToConst expr = - match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(id) -> raise EvalFailed //VarConst(id) - | Dot(e, str) -> raise EvalFailed - | SeqLength(e) -> - match EvalToConst e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> raise EvalFailed - | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev - SeqConst(clist) - | SelectExpr(lst, idx) -> - match EvalToConst lst, EvalToConst idx with - | SeqConst(clist), IntConst(n) -> clist.[n] - | _ -> raise EvalFailed - | UpdateExpr(lst,idx,v) -> - match EvalToConst lst, EvalToConst idx, EvalToConst v with - | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n 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 - + | _ -> resolverFunc expr + | _ -> resolverFunc expr + | _ -> resolverFunc expr + +// ======================================= +/// Converts a given constant to expression +// ======================================= let rec Const2Expr c = match c with | IntConst(n) -> IntLiteral(n) - | BoolConst(b) -> if b then IntLiteral(1) else IntLiteral(0) //?? BoolLiteral(b) + | BoolConst(b) -> BoolLiteral(b) | SeqConst(clist) -> let expList = clist |> List.fold (fun acc c -> Const2Expr c :: acc) [] |> List.rev SequenceExpr(expList) | ThisConst(_) -> IdLiteral("this") - | VarConst(v) -> IdLiteral(v) + | Unresolved(name) -> IdLiteral(name) | NullConst -> IdLiteral("null") | ExprConst(e) -> e | _ -> failwith "not implemented or not supported" @@ -436,6 +373,7 @@ let FindVar (prog: Program) clsName fldName = let rec Desugar expr = match expr with | IntLiteral(_) + | BoolLiteral(_) | IdLiteral(_) | Star | Dot(_) @@ -450,14 +388,7 @@ let rec Desugar expr = try match op with | Exact "=" _ -> - match EvalSym e1, EvalSym 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 clist.[cnt]) :: __fff rest (cnt+1) - | [] -> [] - __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be + match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with | SeqConst(cl1), SeqConst(cl2) -> let rec __fff lst1 lst2 cnt = match lst1, lst2 with @@ -465,11 +396,17 @@ let rec Desugar expr = | [], [] -> [] | _ -> failwith "Lists are of different sizes" __fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be + | c, SeqConst(clist) + | SeqConst(clist), c -> + let rec __fff lst cnt = + match lst with + | fs :: rest -> BinaryEq (SelectExpr(Const2Expr c, IntLiteral(cnt))) (Const2Expr clist.[cnt]) :: __fff rest (cnt+1) + | [] -> [] + __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be | _ -> be | _ -> be with - | EvalFailed as ex -> (* printfn "%s" (ex.StackTrace.ToString()); *) be - + | EvalFailed as ex -> (* printfn "%O" (ex.StackTrace); *) be let rec DesugarLst exprLst = match exprLst with diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index 3c97b94f..80b180be 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -101,7 +101,7 @@ let PrintAllocNewObjects (heap,env,ctx) indent = ) "" let PrintObjRefName o (env,ctx) = - match Resolve o (env,ctx) with + match Resolve (env,ctx) o with | ThisConst(_,_) -> "this"; | NewObj(name, _) -> PrintGenSym name | _ -> failwith ("unresolved object ref: " + o.ToString()) @@ -111,7 +111,7 @@ let PrintVarAssignments (heap,env,ctx) indent = heap |> Map.fold (fun acc (o,f) l -> let objRef = PrintObjRefName o (env,ctx) let fldName = PrintVarName f - let value = Resolve l (env,ctx) |> PrintConst + let value = Resolve (env,ctx) l |> PrintConst acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline ) "" @@ -138,8 +138,8 @@ let GenConstructorCode mthd body = // NOTE: insert here coto to say which methods to analyze let GetMethodsToAnalyze prog = (* exactly one *) -// let c = FindComponent prog "List" |> Utils.ExtractOption -// let m = FindMethod c "Double" |> Utils.ExtractOption +// let c = FindComponent prog "IntList" |> Utils.ExtractOption +// let m = FindMethod c "Singleton" |> Utils.ExtractOption // [c, m] (* all *) FilterMembers prog FilterConstructorMembers diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index 597ac7c9..b862ffe3 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -1,4 +1,10 @@ -module DafnyModelUtils +// ######################################################################### +/// Utilities for reading/building models from Boogie Visual Debugger files +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// ######################################################################### + +module DafnyModelUtils (* The heap maps objects and fields to locations. @@ -18,10 +24,7 @@ open AstUtils 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)) @@ -141,87 +144,109 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog = | None -> acc ) Map.empty +// ==================================================================== +/// Reads values that were assigned to given arguments. Those values +/// can be in functions with the same name as the argument name appended +/// with an "#" and some number after it. +// ==================================================================== 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 + ReadArgValues model rest |> Map.add (Unresolved(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 -> - let len = GetInt ft.Result - let emptyList = Utils.GenList len NoneConst - let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList)) - ReadSeqLen model rest (newMap,ctx) - | _ -> (envMap,ctx) - -let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) = - match idx_tuples with - | ft :: rest -> - let srcLstKey = GetLoc ft.Args.[0] - let oldLst = GetSeqFromEnv envMap srcLstKey - let idx = GetInt ft.Args.[1] - let lstElem = UnboxIfNeeded model ft.Result - let newLst = Utils.ListSet idx lstElem oldLst - let newCtx = UpdateContext oldLst newLst ctx - let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst)) - ReadSeqIndex model rest (newEnv,newCtx) - | _ -> (envMap,ctx) - -let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) = - match bld_tuples with - | ft :: rest -> - let srcLstLoc = GetLoc ft.Args.[0] - let dstLstLoc = GetLoc ft.Result - let oldLst = GetSeqFromEnv envMap srcLstLoc - let idx = GetInt ft.Args.[1] - let lstElemVal = UnboxIfNeeded model ft.Args.[2] - let dstLst = GetSeqFromEnv envMap dstLstLoc - let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst - let newCtx = UpdateContext dstLst newLst ctx - let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) - ReadSeqBuild model rest (newEnv,newCtx) - | _ -> (envMap,ctx) - -let rec ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) = - match app_tuples with - | ft :: rest -> - let srcLst1Loc = GetLoc ft.Args.[0] - let srcLst2Loc = GetLoc ft.Args.[1] - let dstLstLoc = GetLoc ft.Result - let oldLst1 = GetSeqFromEnv envMap srcLst1Loc - let oldLst2 = GetSeqFromEnv envMap srcLst2Loc - let dstLst = GetSeqFromEnv envMap dstLstLoc - let newLst = List.append oldLst1 oldLst2 - let newCtx = UpdateContext dstLst newLst ctx - let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) - ReadSeqAppend model rest (newEnv,newCtx) - | _ -> (envMap,ctx) - +// ============================================================== +/// Reads stuff about sequences from a given model and ads it to +/// the given "envMap" map and a "ctx" set. The relevant stuff is +/// fetched from the following functions: +/// Seq#Length, Seq#Index, Seq#Build, Seq#Append +// ============================================================== let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = + // reads stuff from Seq#Length + let rec __ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) = + match len_tuples with + | ft :: rest -> + let len = GetInt ft.Result + let emptyList = Utils.GenList len NoneConst + let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList)) + __ReadSeqLen model rest (newMap,ctx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Index + let rec __ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) = + match idx_tuples with + | ft :: rest -> + let srcLstKey = GetLoc ft.Args.[0] + let oldLst = GetSeqFromEnv envMap srcLstKey + let idx = GetInt ft.Args.[1] + let lstElem = UnboxIfNeeded model ft.Result + let newLst = Utils.ListSet idx lstElem oldLst + let newCtx = UpdateContext oldLst newLst ctx + let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst)) + __ReadSeqIndex model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Build + let rec __ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) = + match bld_tuples with + | ft :: rest -> + let srcLstLoc = GetLoc ft.Args.[0] + let dstLstLoc = GetLoc ft.Result + let oldLst = GetSeqFromEnv envMap srcLstLoc + let idx = GetInt ft.Args.[1] + let lstElemVal = UnboxIfNeeded model ft.Args.[2] + let dstLst = GetSeqFromEnv envMap dstLstLoc + let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst + let newCtx = UpdateContext dstLst newLst ctx + let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) + __ReadSeqBuild model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + + // reads stuff from Seq#Append + let rec __ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) = + match app_tuples with + | ft :: rest -> + let srcLst1Loc = GetLoc ft.Args.[0] + let srcLst2Loc = GetLoc ft.Args.[1] + let dstLstLoc = GetLoc ft.Result + let oldLst1 = GetSeqFromEnv envMap srcLst1Loc + let oldLst2 = GetSeqFromEnv envMap srcLst2Loc + let dstLst = GetSeqFromEnv envMap dstLstLoc + let newLst = List.append oldLst1 oldLst2 + let newCtx = UpdateContext dstLst newLst ctx + let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) + __ReadSeqAppend model rest (newEnv,newCtx) + | _ -> (envMap,ctx) + let f_seq_len = model.MkFunc("Seq#Length", 1) let f_seq_idx = model.MkFunc("Seq#Index", 2) let f_seq_bld = model.MkFunc("Seq#Build", 4) let f_seq_app = model.MkFunc("Seq#Append", 2) - (envMap,ctx) |> ReadSeqLen model (List.ofSeq f_seq_len.Apps) - |> ReadSeqIndex model (List.ofSeq f_seq_idx.Apps) - |> ReadSeqBuild model (List.ofSeq f_seq_bld.Apps) - |> ReadSeqAppend model (List.ofSeq f_seq_app.Apps) + (envMap,ctx) |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps) + |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps) + |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps) + |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps) +// ===================================================== +/// Reads stuff about sets from a given model and adds it +/// to the given "envMap" map and "ctx" set. (TODO) +// ===================================================== let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = (envMap,ctx) +// ====================================================== +/// Reads staff about the null constant from a given model +/// and adds it to the given "envMap" map and "ctx" set. +// ====================================================== let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = let f_null = model.MkFunc("null", 0) assert (f_null.AppCount = 1) @@ -229,6 +254,12 @@ let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) = let newEnv = envMap |> Map.add (GetLoc e) NullConst (newEnv,ctx) +// ============================================================================================ +/// Reads the evinronment map and the context set. +/// +/// It starts by reading the model for the "dtype" function to discover all objects on the heap, +/// and then proceeds by reading stuff about the null constant, about sequences, and about sets. +// ============================================================================================ let ReadEnv (model: Microsoft.Boogie.Model) prog = let f_dtype = model.MkFunc("dtype", 1) let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0])) diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index fb9f3bf7..bf63f453 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -14,7 +14,8 @@ let rec PrintType ty = let rec PrintExpr ctx expr = match expr with - | IntLiteral(n) -> sprintf "%O" n + | IntLiteral(n) -> sprintf "%d" n + | BoolLiteral(b) -> sprintf "%b" b | IdLiteral(id) -> id | Star -> assert false; "" // I hope this won't happen | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index bbb15dc4..7f0e7ff0 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - C:\boogie\Jennisys\Jennisys\examples\List.jen + C:\boogie\Jennisys\Jennisys\examples\List2.jen pdbonly diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 34a0422b..d98607b2 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -1,6 +1,8 @@ -/// This module is intended to store and handle configuration options +// #################################################################### +/// This module is intended to store and handle configuration options /// -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### module Options diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs index c17ebfa7..d24391f1 100644 --- a/Jennisys/PipelineUtils.fs +++ b/Jennisys/PipelineUtils.fs @@ -1,7 +1,9 @@ -/// Utility functions for executing shell commands and -/// running Dafny in particular +// #################################################################### +/// Utility functions for executing shell commands and +/// running Dafny in particular /// -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### module PipelineUtils diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index e4f6e0a0..f2cbf30f 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -34,7 +34,8 @@ let PrintVarName vd = let rec PrintExpr ctx expr = match expr with - | IntLiteral(n) -> sprintf "%O" n + | IntLiteral(n) -> sprintf "%d" n + | BoolLiteral(b) -> sprintf "%b" b | IdLiteral(id) -> id | Star -> "*" | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id @@ -131,5 +132,4 @@ let rec PrintConst cst = | 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/Resolver.fs b/Jennisys/Resolver.fs index c6bb1991..2ac6b96a 100644 --- a/Jennisys/Resolver.fs +++ b/Jennisys/Resolver.fs @@ -1,19 +1,33 @@ -module Resolver +// #################################################################### +/// Utilities for resolving the "Unresolved" constants with respect to +/// a given context (heap/env/ctx) +/// +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### + +module Resolver open Ast +open AstUtils open Printer open EnvUtils // resolving values exception ConstResolveFailed of string -let rec ResolveCont cst (env,ctx) failResolver = +// ================================================================ +/// Resolves a given Const (cst) with respect to a given env/ctx. +/// +/// If unable to resolve, it just delegates the task to the +/// failResolver function +// ================================================================ +let rec ResolveCont (env,ctx) failResolver cst = 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) -> ResolveCont c (env,ctx) failResolver + | Some(c) -> ResolveCont (env,ctx) failResolver c | None -> // not found in the env map --> check the equality sets let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet) @@ -27,53 +41,47 @@ let rec ResolveCont cst (env,ctx) failResolver = | _ -> failResolver cst (env,ctx) | _ -> failResolver cst (env,ctx) | SeqConst(cseq) -> - let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont c (env,ctx) failResolver :: acc) [] + let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont (env,ctx) failResolver c :: acc) [] SeqConst(resolvedLst) | SetConst(cset) -> - let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont c (env,ctx) failResolver)) Set.empty + let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont (env,ctx) failResolver c)) Set.empty SetConst(resolvedSet) | _ -> cst -let TryResolve cst (env,ctx) = - ResolveCont cst (env,ctx) (fun c (e,x) -> c) - -let Resolve cst (env,ctx) = - ResolveCont cst (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) - - +// ===================================================================== +/// Tries to resolve a given Const (cst) with respect to a given env/ctx. +/// +/// If unable to resolve, just returns the original Unresolved const. +// ===================================================================== +let TryResolve (env,ctx) cst = + ResolveCont (env,ctx) (fun c (e,x) -> c) 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 - | SelectExpr(lst, idx) -> - let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) - let idxC = EvalUnresolved idx (heap,env,ctx) - match lstC, idxC with - | SeqConst(clist), IntConst(n) -> clist.[n] - | _ -> failwith "can't eval SelectExpr" - | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! -// | Star -// | SelectExpr(_) -// | UpdateExpr(_) -// | SequenceExpr(_) -// | SeqLength(_) -// | ForallExpr(_) -// | UnaryExpr(_) -// | BinaryExpr(_) - -// TODO: can this be implemented on top of the existing AstUtils.EvalSym?? We must! -let Eval expr (heap,env,ctx) = +// ============================================================== +/// Resolves a given Const (cst) with respect to a given env/ctx. +/// +/// If unable to resolve, raises a ConstResolveFailed exception +// ============================================================== +let Resolve (env,ctx) cst = + ResolveCont (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst + +// ================================================================= +/// Evaluates a given expression with respect to a given heap/env/ctx +// ================================================================= +let Eval (heap,env,ctx) expr = + let rec __EvalResolver expr = + match expr with + | IdLiteral(id) when id = "this" -> GetThisLoc env + | IdLiteral(id) -> __EvalResolver (Dot(IdLiteral("this"), id)) + | Dot(e, str) -> + let discr = __EvalResolver e + 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" try - let unresolvedConst = EvalUnresolved expr (heap,env,ctx) - Some(TryResolve unresolvedConst (env,ctx)) + let unresolvedConst = EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx)) expr + Some(TryResolve (env,ctx) unresolvedConst) with ex -> None \ No newline at end of file diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index 6540173c..7c55e1e8 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -1,6 +1,8 @@ -/// Various utility functions +// #################################################################### +/// Various utility functions /// -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// #################################################################### module Utils @@ -24,21 +26,23 @@ let ExtractOptionMsg msg x = let ExtractOption x = ExtractOptionMsg "can't extract anything from a None" x -// ============================= -/// requres: List.length lst <= 1 +// ========================================================== +/// requres: List.length lst <= 1, otherwise fails with errMsg /// ensures: if |lst| = 0 then /// ret = None /// else /// ret = Some(lst[0]) -// ============================= -let ListToOption lst = +// ========================================================== +let ListToOptionMsg lst errMsg = if List.length lst > 1 then - failwith "given list contains more than one element" + failwith errMsg if List.isEmpty lst then None else Some(lst.[0]) +let ListToOption lst = ListToOptionMsg lst "given list contains more than one element" + // ============================================================= /// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i]) // ============================================================= @@ -47,36 +51,40 @@ let rec ConvertToOptionList lst = | fs :: rest -> Some(fs) :: ConvertToOptionList rest | [] -> [] -// ============================= -/// requres: Seq.length seq <= 1 +// ========================================================= +/// requres: Seq.length seq <= 1, otherwise fails with errMsg /// ensures: if |seq| = 0 then /// ret = None /// else /// ret = Some(seq[0]) -// ============================= -let SeqToOption seq = +// ========================================================= +let SeqToOptionMsg seq errMsg = if Seq.length seq > 1 then - failwith "given seq contains more than one element" + failwith errMsg if Seq.isEmpty seq then None else Some(Seq.nth 0 seq) -// ============================= -/// requires: Set.count set <= 1 +let SeqToOption seq = SeqToOptionMsg seq "given seq contains more than one element" + +// ========================================================= +/// requires: Set.count set <= 1, otherwise fails with errMsg /// ensures: if |set| = 0 then /// ret = None /// else /// ret = Some(set[0]) -// ============================= -let SetToOption set = +// ========================================================= +let SetToOptionMsg set errMsg = if Set.count set > 1 then - failwith "give set contains more than one value" + failwith errMsg if (Set.isEmpty set) then None else Some(set |> Set.toList |> List.head) +let SetToOption set = SetToOptionMsg set "give set contains more than one value" + // ============================================================ /// requires: n >= 0 /// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = e @@ -185,5 +193,4 @@ let IfDo2 cond func2 (a1,a2) = if cond then func2 a1 a2 else - a1,a2 - + a1,a2 \ No newline at end of file -- cgit v1.2.3 From 776eb757b0e4b7b98ea9c7ca9bcee002eaf6bee2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 13:52:58 -0700 Subject: - added Set.jen example - fixed implementation for sets - generalized unification rules - added command line options - removed the "Exact" active pattern for strings (the same thing is already supported by F#) - added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST --- Jennisys/Analyzer.fs | 156 ++++++++++++++++++++++++++++---------------- Jennisys/Ast.fs | 2 + Jennisys/AstUtils.fs | 77 ++++++++++++---------- Jennisys/CodeGen.fs | 25 ++++--- Jennisys/DafnyModelUtils.fs | 118 ++++++++++++++++++++++++++++++--- Jennisys/DafnyPrinter.fs | 2 + Jennisys/Jennisys.fs | 74 ++++++++------------- Jennisys/Jennisys.fsproj | 6 +- Jennisys/Lexer.fsl | 1 + Jennisys/Logger.fs | 6 +- Jennisys/Options.fs | 61 ++++++++++++++++- Jennisys/Parser.fsy | 10 ++- Jennisys/Printer.fs | 6 +- Jennisys/Resolver.fs | 5 +- Jennisys/Utils.fs | 47 ++++++++++--- Jennisys/examples/Set.jen | 53 +++++++++++++++ 16 files changed, 470 insertions(+), 179 deletions(-) create mode 100644 Jennisys/examples/Set.jen (limited to 'Jennisys') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 8737ad86..7b6527f9 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -72,49 +72,87 @@ let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd = let rec IsArgsOnly args expr = match expr with - | IntLiteral(_) -> true - | BoolLiteral(_) -> true - | 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 - | Star -> true + | IntLiteral(_) -> true + | BoolLiteral(_) -> true + | Star -> true + | 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) + | IteExpr(c,e1,e2) -> (IsArgsOnly args c) && (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) | SetExpr(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 -let rec GetUnifications expr args (heap,env,ctx) = - match expr with - | IntLiteral(_) - | BoolLiteral(_) - | 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 (heap,env,ctx) e0 - let v1 = Eval (heap,env,ctx) e1 - 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.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); - Set.empty - else - GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) +let GetUnifications expr args (heap,env,ctx) = + // - first looks if the give expression talks only about method arguments (args) + // - then checks if it doesn't already exist in the unification map + // - then it tries to evaluate it to a constant + // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map + let __AddUnif e unifMap = + let builder = new CascadingBuilder<_>(unifMap) + builder { + let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption + let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption + let! v = Eval (heap,env,ctx) e + Logger.DebugLine (" - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v)); + return Map.add e v unifMap + } + // just recurses on all expressions + let rec __GetUnifications expr args unifs = + let unifs = __AddUnif expr unifs + match expr with + | IntLiteral(_) + | BoolLiteral(_) + | IdLiteral(_) + | Star -> unifs + | Dot(e, _) + | SeqLength(e) + | ForallExpr(_,e) + | UnaryExpr(_,e) -> unifs |> __GetUnifications e args + | SelectExpr(e1, e2) + | BinaryExpr(_,_,e1,e2) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args + | IteExpr(e1,e2,e3) + | UpdateExpr(e1, e2, e3) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args |> __GetUnifications e3 args + | SetExpr(elst) + | SequenceExpr(elst) -> elst |> List.fold (fun acc e -> acc |> __GetUnifications e args) unifs + + __GetUnifications expr args Map.empty + +//let rec GetUnifications expr args (heap,env,ctx) = +// match expr with +// | IntLiteral(_) +// | BoolLiteral(_) +// | IdLiteral(_) +// | Star +// | Dot(_) +// | SelectExpr(_) // TODO: handle select expr +// | UpdateExpr(_) // TODO: handle update expr +// | SequenceExpr(_) +// | SeqLength(_) +// | SetExpr(_) +// | ForallExpr(_) // TODO: handle forall expr +// | UnaryExpr(_) -> Map.empty +// | IteExpr(c,e0,e1) -> (GetUnifications e0 args (heap,env,ctx)) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx)) +// | BinaryExpr(strength,op,e0,e1) -> +// if op = "=" then +// let v0 = Eval (heap,env,ctx) e0 +// let v1 = Eval (heap,env,ctx) e1 +// 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)); +// Map.ofList [e1, c0] +// | _,_,true,Some(c1) -> +// Logger.DebugLine (" - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0)); +// Map.ofList [e0, c1] +// | _ -> Logger.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); +// Map.empty +// else +// GetUnifications e0 args (heap,env,ctx) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx)) let rec GetArgValueUnifications args env = match args with @@ -122,9 +160,9 @@ let rec GetArgValueUnifications args env = match Map.tryFind (Unresolved(name)) env with | Some(c) -> Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); - Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) + Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env) | None -> failwith ("couldn't find value for argument " + name) - | [] -> Set.empty + | [] -> Map.empty let rec _GetObjRefExpr o (heap,env,ctx) visited = if Set.contains o visited then @@ -133,7 +171,7 @@ let rec _GetObjRefExpr o (heap,env,ctx) visited = let newVisited = Set.add o visited let refName = PrintObjRefName o (env,ctx) match refName with - | Exact "this" _ -> Some(IdLiteral(refName)) + | "this" -> Some(IdLiteral(refName)) | _ -> let rec __fff lst = match lst with @@ -152,15 +190,18 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = let __CheckUnif o f e idx = 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 lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx))) - let assertionExpr = BinaryEq lhs e + let lhs = Dot(objRefExpr, fldName) + let assertionExpr = match f with + | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e + | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs + | _ -> BinaryEq lhs 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) + " ... ") CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) match unifs with - | (c,e) :: rest -> + | (e,c) :: 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 = TryResolve (env,ctx) l @@ -174,10 +215,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = // don't change the value acc |> Map.add (o,f) l else - // see if it's a list, then try to match its elements, otherwise leave it as is - match value with - | SeqConst(clist) -> - let rec __UnifyOverLst lst cnt = + let rec __UnifyOverLst lst cnt = match lst with | lstElem :: rest when lstElem = c -> if __CheckUnif o f e cnt then @@ -189,8 +227,14 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = | lstElem :: rest -> lstElem :: __UnifyOverLst rest (cnt+1) | [] -> [] + // see if it's a list, then try to match its elements, otherwise leave it as is + match value with + | SeqConst(clist) -> let newLstConst = __UnifyOverLst clist 0 acc |> Map.add (o,f) (SeqConst(newLstConst)) + | SetConst(cset) -> + let newLstConst = __UnifyOverLst (Set.toList cset) 0 + acc |> Map.add (o,f) (SetConst(newLstConst |> Set.ofList)) | _ -> acc |> Map.add (o,f) l ) restHeap @@ -204,9 +248,9 @@ let GeneralizeSolution prog comp mthd (heap,env,ctx) = match args with | [] -> (heap,env,ctx) | _ -> - let unifs = GetUnifications (BinaryAnd pre post |> Desugar) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv - |> Set.union (GetArgValueUnifications args env) - UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx) + let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv + |> Utils.MapAddAll (GetArgValueUnifications args env) + UpdateHeapEnv prog comp mthd (Map.toList unifs) (heap,env,ctx) | _ -> failwith ("not a method: " + mthd.ToString()) // ==================================================================================== @@ -242,7 +286,7 @@ let AnalyzeConstructor prog comp m = let model = models.[0] let heap,env,ctx = ReadFieldValuesFromModel model prog comp m |> GeneralizeSolution prog comp m - if _opt_verifySolutions then + if Options.CONFIG.verifySolutions then Logger.InfoLine " - verifying synthesized solution ... " let verified = VerifySolution prog comp m (heap,env,ctx) Logger.Info " " diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 167a5eef..86f6861f 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -29,10 +29,12 @@ type Expr = | Dot of Expr * string | UnaryExpr of string * Expr | BinaryExpr of int * string * Expr * Expr + | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr | SelectExpr of Expr * Expr | UpdateExpr of Expr * Expr * Expr | SequenceExpr of Expr list | SeqLength of Expr + | SetExpr of Expr list | ForallExpr of VarDecl list * Expr type Stmt = diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 26544f65..32d58ec7 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -16,15 +16,16 @@ let rec VisitExpr visitorFunc expr acc = | IntLiteral(_) | BoolLiteral(_) | 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 + | 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) | SetExpr(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 + | IteExpr(c,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc c |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 // ------------------------------- End Visitor Stuff ------------------------------------------- @@ -53,83 +54,83 @@ let rec EvalSym resolverFunc expr = | _ -> resolverFunc expr | BinaryExpr(_,op,e1,e2) -> match op with - | Exact "=" _ -> + | "=" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) | ExprConst(e1), ExprConst(e2) -> BoolConst(e1 = e2) | _ -> resolverFunc expr - | Exact "!=" _ -> + | "!=" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) | ExprConst(e1), ExprConst(e2) -> BoolConst(not (e1 = e2)) | _ -> resolverFunc expr - | Exact "<" _ -> + | "<" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) | _ -> resolverFunc expr - | Exact "<=" _ -> + | "<=" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) | _ -> resolverFunc expr - | Exact ">" _ -> + | ">" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) | _ -> resolverFunc expr - | Exact ">=" _ -> + | ">=" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) | _ -> resolverFunc expr - | Exact "in" _ -> + | "in" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | _ as c, SetConst(s) -> BoolConst(Set.contains c s) | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s) | _ -> resolverFunc expr - | Exact "!in" _ -> + | "!in" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s)) | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s)) | _ -> resolverFunc expr - | Exact "+" _ -> + | "+" -> match EvalSym resolverFunc e1, EvalSym resolverFunc 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) - | _ -> resolverFunc expr - | Exact "-" _ -> + | q,w -> resolverFunc expr + | "-" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) | _ -> resolverFunc expr - | Exact "*" _ -> + | "*" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) | _ -> resolverFunc expr - | Exact "div" _ -> + | "div" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) | _ -> resolverFunc expr - | Exact "mod" _ -> + | "mod" -> match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) | _ -> resolverFunc expr | _ -> resolverFunc expr | UnaryExpr(op, e) -> match op with - | Exact "!" _ -> + | "!" -> match EvalSym resolverFunc e with | BoolConst(b) -> BoolConst(not b) | _ -> resolverFunc expr - | Exact "-" _ -> + | "-" -> match EvalSym resolverFunc e with | IntConst(n) -> IntConst(-n) | _ -> resolverFunc expr @@ -179,16 +180,18 @@ let BinaryOr (lhs: Expr) (rhs: Expr) = // =================================================================================== let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs) -// ================================================= -/// Returns a binary NEQ of the two given expressions -// ================================================= +// ======================================================= +/// Constructors for binary EQ/NEQ of 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) +// ======================================================= +/// Constructors for binary IN/!IN of two given expressions +// ======================================================= +let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs) +let BinaryNotIn lhs rhs = BinaryExpr(40, "!in", lhs, rhs) + // ===================== /// Returns TRUE literal // ===================== @@ -378,16 +381,18 @@ let rec Desugar expr = | Star | Dot(_) | SelectExpr(_) - | SeqLength(_) -> expr - | UpdateExpr(_) -> expr //TODO - | SequenceExpr(exs) -> expr //TODO + | SeqLength(_) + | UpdateExpr(_) + | SetExpr(_) + | SequenceExpr(_) -> expr | ForallExpr(v,e) -> ForallExpr(v, Desugar e) | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e) + | IteExpr(c,e1,e2) -> IteExpr(c, Desugar e1, Desugar e2) | BinaryExpr(p,op,e1,e2) -> let be = BinaryExpr(p, op, Desugar e1, Desugar e2) try match op with - | Exact "=" _ -> + | "=" -> match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with | SeqConst(cl1), SeqConst(cl2) -> let rec __fff lst1 lst2 cnt = diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index 80b180be..f59215ed 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -111,7 +111,7 @@ let PrintVarAssignments (heap,env,ctx) indent = heap |> Map.fold (fun acc (o,f) l -> let objRef = PrintObjRefName o (env,ctx) let fldName = PrintVarName f - let value = Resolve (env,ctx) l |> PrintConst + let value = TryResolve (env,ctx) l |> PrintConst acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline ) "" @@ -137,14 +137,21 @@ let GenConstructorCode mthd body = // NOTE: insert here coto to say which methods to analyze let GetMethodsToAnalyze prog = - (* exactly one *) -// let c = FindComponent prog "IntList" |> Utils.ExtractOption -// let m = FindMethod c "Singleton" |> Utils.ExtractOption -// [c, m] - (* all *) - FilterMembers prog FilterConstructorMembers - (* only with parameters *) -// FilterMembers prog FilterConstructorMembersWithParams + let m = Options.CONFIG.methodToSynth; + if m = "*" then + (* all *) + FilterMembers prog FilterConstructorMembers + elif m = "paramsOnly" then + (* only with parameters *) + FilterMembers prog FilterConstructorMembersWithParams + else + (* exactly one *) + let compName = m.Substring(0, m.LastIndexOf(".")) + let methName = m.Substring(m.LastIndexOf(".") + 1) + let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) + let m = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) + [c, m] + // solutions: (comp, constructor) |--> (heap, env, ctx) let PrintImplCode prog solutions methodsToPrintFunc = diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index b862ffe3..4cc517f2 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -67,7 +67,7 @@ let GetType (e: Model.Element) prog = let fNameOpt = GetElemFullName e match fNameOpt with | Some(fname) -> match fname with - | Exact "intType" _ -> Some(IntType) + | "intType" -> Some(IntType) | Prefix "class." clsName -> match FindComponent prog clsName with | Some(comp) -> Some(GetClassType comp) @@ -78,10 +78,16 @@ let GetType (e: Model.Element) prog = let GetLoc (e: Model.Element) = Unresolved(GetRefName e) -let GetSeqFromEnv env key = +let FindSeqInEnv env key = match Map.find key env with | SeqConst(lst) -> lst | _ as x-> failwith ("not a SeqConst but: " + x.ToString()) + +let TryFindSetInEnv env key = + match Map.tryFind key env with + | Some(SetConst(s)) -> Some(s) + | Some(x) -> failwith ("not a SetConst but: " + x.ToString()) + | None -> None let AddConstr c1 c2 ctx = if c1 = c2 then @@ -185,7 +191,7 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = match idx_tuples with | ft :: rest -> let srcLstKey = GetLoc ft.Args.[0] - let oldLst = GetSeqFromEnv envMap srcLstKey + let oldLst = FindSeqInEnv envMap srcLstKey let idx = GetInt ft.Args.[1] let lstElem = UnboxIfNeeded model ft.Result let newLst = Utils.ListSet idx lstElem oldLst @@ -200,10 +206,10 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = | ft :: rest -> let srcLstLoc = GetLoc ft.Args.[0] let dstLstLoc = GetLoc ft.Result - let oldLst = GetSeqFromEnv envMap srcLstLoc + let oldLst = FindSeqInEnv envMap srcLstLoc let idx = GetInt ft.Args.[1] let lstElemVal = UnboxIfNeeded model ft.Args.[2] - let dstLst = GetSeqFromEnv envMap dstLstLoc + let dstLst = FindSeqInEnv envMap dstLstLoc let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst let newCtx = UpdateContext dstLst newLst ctx let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) @@ -217,9 +223,9 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = let srcLst1Loc = GetLoc ft.Args.[0] let srcLst2Loc = GetLoc ft.Args.[1] let dstLstLoc = GetLoc ft.Result - let oldLst1 = GetSeqFromEnv envMap srcLst1Loc - let oldLst2 = GetSeqFromEnv envMap srcLst2Loc - let dstLst = GetSeqFromEnv envMap dstLstLoc + let oldLst1 = FindSeqInEnv envMap srcLst1Loc + let oldLst2 = FindSeqInEnv envMap srcLst2Loc + let dstLst = FindSeqInEnv envMap dstLstLoc let newLst = List.append oldLst1 oldLst2 let newCtx = UpdateContext dstLst newLst ctx let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) @@ -238,10 +244,102 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = // ===================================================== /// Reads stuff about sets from a given model and adds it -/// to the given "envMap" map and "ctx" set. (TODO) +/// to the given "envMap" map and "ctx" set. // ===================================================== let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = - (envMap,ctx) + // reads stuff from Set#Empty + let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) = + match empty_tuples with + | ft :: rest -> + let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty)) + __ReadSetEmpty rest (newMap,ctx) + | [] -> (envMap,ctx) + + // reads stuff from [2] + let __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = + match set_tuples with + | ft :: rest when GetBool ft.Result -> + let srcSetKey = GetLoc ft.Args.[0] + let srcSet = match TryFindSetInEnv env srcSetKey with + | Some(s) -> s + | None -> Set.empty + let elem = UnboxIfNeeded model ft.Args.[1] + let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) + (newEnv,ctx) + | _ -> (env,ctx) + + let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps) + let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps) + (envMap,ctx) |> __ReadSetEmpty t_set_empty + |> __ReadSetMembership t_set + +(* More complicated way which now doesn't seem to be necessary *) +//let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = +// // reads stuff from Set#Empty +// let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) = +// match empty_tuples with +// | ft :: rest -> +// let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty)) +// __ReadSetEmpty rest (newMap,ctx) +// | [] -> (envMap,ctx) +// +// // reads stuff from Set#UnionOne and Set#Union +// let rec __ReadSetUnions (envMap,ctx) = +// // this one goes through a given list of "UnionOne" tuples, updates +// // the env for those set that it was able to resolve, and returns a +// // list of tuples for which it wasn't able to resolve sets +// let rec ___RSU1 (tuples: Model.FuncTuple list) env unprocessed = +// match tuples with +// | ft :: rest -> +// let srcSetKey = GetLoc ft.Args.[0] +// match TryFindSetInEnv env srcSetKey with +// | Some(oldSet) -> +// let elem = UnboxIfNeeded model ft.Args.[1] +// let newSet = Set.add elem oldSet +// // update contex? +// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet)) +// ___RSU1 rest newEnv unprocessed +// | None -> ___RSU1 rest env (ft :: unprocessed) +// | [] -> (env,unprocessed) +// // this one goes through a given list of "Union" tuples, updates +// // the env for those set that it was able to resolve, and returns a +// // list of tuples for which it wasn't able to resolve sets +// let rec ___RSU (tuples: Model.FuncTuple list) env unprocessed = +// match tuples with +// | ft :: rest -> +// let set1Key = GetLoc ft.Args.[0] +// let set2Key = GetLoc ft.Args.[1] +// match TryFindSetInEnv env set1Key, TryFindSetInEnv env set2Key with +// | Some(oldSet1), Some(oldSet2) -> +// let newSet = Set.union oldSet1 oldSet2 +// // update contex? +// let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet)) +// ___RSU rest newEnv unprocessed +// | _ -> ___RSU rest env (ft :: unprocessed) +// | [] -> (env,unprocessed) +// // this one keeps looping as loong as the list of unprocessed tuples +// // is decreasing, it ends when if falls down to 0, or fails if +// // the list stops decreasing +// let rec ___RSU_until_fixpoint u1tuples utuples env = +// let newEnv1,unprocessed1 = ___RSU1 u1tuples env [] +// let newEnv2,unprocessed2 = ___RSU utuples newEnv1 [] +// let oldLen = (List.length u1tuples) + (List.length utuples) +// let totalUnprocLen = (List.length unprocessed1) + (List.length unprocessed2) +// if totalUnprocLen = 0 then +// newEnv2 +// elif totalUnprocLen < oldLen then +// ___RSU_until_fixpoint unprocessed1 unprocessed2 newEnv2 +// else +// failwith "cannot resolve all sets in Set#UnionOne/Set#Union" +// // finally, just invoke the fixpoint function for UnionOne and Union tuples +// let t_union_one = Seq.toList (model.MkFunc("Set#UnionOne", 2).Apps) +// let t_union = Seq.toList (model.MkFunc("Set#Union", 2).Apps) +// let newEnv = ___RSU_until_fixpoint t_union_one t_union envMap +// (newEnv,ctx) +// +// let f_set_empty = model.MkFunc("Set#Empty", 1) +// (envMap,ctx) |> __ReadSetEmpty (List.ofSeq f_set_empty.Apps) +// |> __ReadSetUnions // ====================================================== /// Reads staff about the null constant from a given model diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs index bf63f453..9ef9e74a 100644 --- a/Jennisys/DafnyPrinter.fs +++ b/Jennisys/DafnyPrinter.fs @@ -31,10 +31,12 @@ let rec PrintExpr ctx expr = let openParen = if needParens then "(" else "" let closeParen = if needParens then ")" else "" sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | IteExpr(c,e1,e2) -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2) | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0)) | ForallExpr(vv,e) -> let needParens = true let openParen = if needParens then "(" else "" diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs index 32827f39..ca1ab1ad 100644 --- a/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys.fs @@ -10,60 +10,42 @@ open Microsoft.FSharp.Text.Lexing open Ast open Lexer +open Options open Parser open Printer open TypeChecker open Analyzer -let readAndProcess tracing analyzing (filename: string) = +let readAndProcess (filename: string) = + try + printfn "// Jennisys, Copyright (c) 2011, Microsoft." + // lex + let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader + let lexbuf = LexBuffer.FromTextReader(f) + lexbuf.EndPos <- { pos_bol = 0; + pos_fname=if filename = null then "stdin" else filename; + pos_cnum=0; + pos_lnum=1 } try - printfn "// Jennisys, Copyright (c) 2011, Microsoft." - // lex - let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader - let lexbuf = LexBuffer.FromTextReader(f) - lexbuf.EndPos <- { pos_bol = 0; - pos_fname=if filename = null then "stdin" else filename; - pos_cnum=0; - pos_lnum=1 } - try - // parse - let sprog = Parser.start Lexer.tokenize lexbuf - // print the given Jennisys program - if tracing then - printfn "---------- Given Jennisys program ----------" - printfn "%s" (Print sprog) - else () - match TypeCheck sprog with - | None -> () // errors have already been reported - | Some(prog) -> - if analyzing then - // output a Dafny program with the constraints to be solved - Analyze prog filename - else () - // that's it - if tracing then printfn "----------" else () - with - | ex -> - let pos = lexbuf.EndPos - printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message - printfn "%s" (ex.StackTrace.ToString()) - + // parse + let sprog = Parser.start Lexer.tokenize lexbuf + match TypeCheck sprog with + | None -> () // errors have already been reported + | Some(prog) -> + Analyze prog filename with - | ex -> + | ex -> + let pos = lexbuf.EndPos + printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + printfn "%s" (ex.StackTrace.ToString()) + with + | ex -> printfn "Unhandled Exception: %s" ex.Message printfn "%s" (ex.StackTrace.ToString()) -let rec start n (args: string []) tracing analyzing filename = - if n < args.Length then - let arg = args.[n] - if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else () - let filename = if arg.StartsWith "/" then filename else arg - start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename - else - readAndProcess tracing analyzing filename - -let args = Environment.GetCommandLineArgs() try - start 1 args false true null -with - | Failure(msg) as e -> printfn "WHYYYYYYYYYYYYYYY: %s" msg; printfn "%s" e.StackTrace \ No newline at end of file + let args = Environment.GetCommandLineArgs() + ParseCmdLineArgs (List.ofArray args) + readAndProcess CONFIG.inputFilename +with + | InvalidCmdLineOption(msg) as ex -> printfn "%s" msg; printfn "%s" ex.StackTrace \ No newline at end of file diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 7f0e7ff0..1c87ba4d 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - C:\boogie\Jennisys\Jennisys\examples\List2.jen + C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.sum pdbonly @@ -42,8 +42,8 @@ $(IntermediateOutputPath) - + @@ -64,8 +64,8 @@ --unicode - + diff --git a/Jennisys/Lexer.fsl b/Jennisys/Lexer.fsl index 91c3239c..9eaf7421 100644 --- a/Jennisys/Lexer.fsl +++ b/Jennisys/Lexer.fsl @@ -69,6 +69,7 @@ rule tokenize = parse | ":" { COLON } | "::" { COLONCOLON } | "," { COMMA } +| "?" { QMARK } // Numberic constants | digit+ { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) } // identifiers diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs index bb784ba2..2801354d 100644 --- a/Jennisys/Logger.fs +++ b/Jennisys/Logger.fs @@ -1,6 +1,8 @@ -/// Simple logging facility +// ####################################################### +/// Simple logging facility /// -/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +/// author: Aleksandar Milicevic (t-alekm@microsoft.com) +// ####################################################### module Logger diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index d98607b2..355ada6e 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -6,5 +6,62 @@ module Options -/// attempt to verify synthesized code -let _opt_verifySolutions = true \ No newline at end of file +open Utils + +type Config = { + inputFilename: string; + methodToSynth: string; + verifySolutions: bool; +} + +let defaultConfig: Config = { + inputFilename = ""; + methodToSynth = "*"; + verifySolutions = true; +} + +let mutable CONFIG = defaultConfig + +exception InvalidCmdLineArg of string +exception InvalidCmdLineOption of string + +let ParseCmdLineArgs args = + let __StripSwitches str = + match str with + | Prefix "--" x + | Prefix "-" x + | Prefix "/" x -> x + | _ -> str + + let __Split (str: string) = + let stripped = __StripSwitches str + if stripped = str then + ("",str) + else + let splits = stripped.Split([| ':' |]) + if splits.Length > 2 then raise (InvalidCmdLineOption("more than 2 colons in " + str)) + if splits.Length = 2 then + let opt = splits.[0] + let value = splits.[1] + (opt,value) + else + let x = __StripSwitches splits.[0] + (x, "") + + let rec __Parse args cfg = + match args with + | fs :: rest -> + let opt,value = __Split fs + match opt with + | "method" -> + if value = "" then raise (InvalidCmdLineArg("Must provide method name")) + __Parse rest { cfg with methodToSynth = value } + | "verifySol" -> + __Parse rest { cfg with verifySolutions = true } + | "" -> + __Parse rest { cfg with inputFilename = value } + | _ -> + raise (InvalidCmdLineOption("Unknown option: " + opt)) + | [] -> cfg + CONFIG <- __Parse args defaultConfig + diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy index 5053bd18..395ee223 100644 --- a/Jennisys/Parser.fsy +++ b/Jennisys/Parser.fsy @@ -26,7 +26,7 @@ let rec MyFold ee acc = %token IMPLIES %token IFF %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR -%token GETS COLON COLONCOLON COMMA +%token GETS COLON COLONCOLON COMMA QMARK %token CLASS MODEL CODE %token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL %token INTTYPE BOOLTYPE SEQTYPE SETTYPE @@ -134,9 +134,12 @@ Expr10: | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) } Expr20: - | Expr30 { $1 } - | Expr30 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) } + | Expr25 { $1 } + | Expr25 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) } +Expr25: + | Expr30 { $1 } + | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) } Expr30: | Expr40 { $1 } | Expr40 AND Expr30and { BinaryAnd $1 $3 } @@ -183,6 +186,7 @@ Expr100: | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) } | LPAREN Expr RPAREN { $2 } | LBRACKET ExprList RBRACKET { SequenceExpr($2) } + | LCURLY ExprList RCURLY { SetExpr($2) } | VERTBAR Expr VERTBAR { SeqLength($2) } | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, $4) } diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index f2cbf30f..53bf6b6d 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -45,10 +45,12 @@ let rec PrintExpr ctx expr = let openParen = if needParens then "(" else "" let closeParen = if needParens then ")" else "" sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | IteExpr(c,e1,e2) -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2) | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) - | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) + | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0)) | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | SetExpr(ee) -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0)) | ForallExpr(vv,e) -> let needParens = ctx <> 0 let openParen = if needParens then "(" else "" @@ -120,7 +122,7 @@ 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 + | SetConst(cset) -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset)) | SeqConst(cseq) -> let seqCont = cseq |> List.fold (fun acc c -> let sep = if acc = "" then "" else ", " diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs index 2ac6b96a..59c6904d 100644 --- a/Jennisys/Resolver.fs +++ b/Jennisys/Resolver.fs @@ -71,7 +71,10 @@ let Eval (heap,env,ctx) expr = let rec __EvalResolver expr = match expr with | IdLiteral(id) when id = "this" -> GetThisLoc env - | IdLiteral(id) -> __EvalResolver (Dot(IdLiteral("this"), id)) + | IdLiteral(id) -> + match TryResolve (env,ctx) (Unresolved(id)) with + | Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id)) + | _ as c -> c | Dot(e, str) -> let discr = __EvalResolver e let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index 7c55e1e8..b7db5706 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -10,6 +10,28 @@ module Utils // ----------- collection util funcs --------- // ------------------------------------------- +// ===================================== +/// ensures: ret = b ? Some(b) : None +// ===================================== +let BoolToOption b = + if b then + Some(b) + else + None + +// ===================================== +/// ensures: ret = (opt == Some(_)) +// ===================================== +let IsSomeOption opt = + match opt with + | Some(_) -> true + | None -> false + +// ===================================== +/// ensures: ret = (opt == None) +// ===================================== +let IsNoneOption opt = IsSomeOption opt |> not + // ===================================== /// requres: x = Some(a) or failswith msg /// ensures: ret = a @@ -172,15 +194,9 @@ let (|Prefix|_|) (p:string) (s:string) = Some(s.Substring(p.Length)) else None - -let (|Exact|_|) (p:string) (s:string) = - if s = p then - Some(s) - else - None - + // ------------------------------------------- -// ----------------- random ------------------ +// --------------- workflow ------------------ // ------------------------------------------- let IfDo1 cond func1 a = @@ -193,4 +209,17 @@ let IfDo2 cond func2 (a1,a2) = if cond then func2 a1 a2 else - a1,a2 \ No newline at end of file + a1,a2 + +type CascadingBuilder<'a>(failVal: 'a) = + member this.Bind(v, f) = + match v with + | Some(x) -> f x + | None -> failVal + member this.Return(v) = v + +// ------------------------------------------- +// --------------- random -------------------- +// ------------------------------------------- + +let Iden x = x \ No newline at end of file diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen new file mode 100644 index 00000000..5626babb --- /dev/null +++ b/Jennisys/examples/Set.jen @@ -0,0 +1,53 @@ +class Set { + var elems: set[int] + + constructor Empty() + ensures elems = {} + + constructor Singleton(t: int) + ensures elems = {t} + + constructor Sum(p: int, q: int) + ensures elems = {p + q} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model Set { + var root: SetNode + + frame + root * root.elems[*] + + invariant + root = null ==> elems = {} + root != null ==> elems = root.elems +} + +class SetNode { + var elems: set[int] + + constructor Init(t: int) + ensures elems = {t} + + constructor Double(p: int, q: int) + requires p != q + ensures elems = {p q} +} + +model SetNode { + var data: int + var left: SetNode + var right: SetNode + + frame + data * left * right + + invariant + left = null && right = null ==> elems = {data} + elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) + left != null ==> forall e :: e in left.elems ==> e < data + right != null ==> forall e :: e in right.elems ==> e > data +} -- cgit v1.2.3 From d9a484aaaee37d4192b6abe67328f9cc875e9294 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 17:03:18 -0700 Subject: - fixed a bug in DafnyModelUtils.fs (reading set values from models) - changed Dafny so that it returns an exit code - changed CheckDafnyProgram so that it checks Dafny exit code as well --- DafnyDriver/DafnyDriver.cs | 22 +++++++++++++++++----- Jennisys/CodeGen.fs | 37 ++++++++++++++++++++++++++----------- Jennisys/DafnyModelUtils.fs | 23 +++++++++++++---------- Jennisys/Jennisys.fsproj | 2 +- Jennisys/PipelineUtils.fs | 6 ++++-- Jennisys/examples/Set.jen | 1 - 6 files changed, 61 insertions(+), 30 deletions(-) (limited to 'Jennisys') diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 73f7fc71..afd36aa8 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -34,23 +34,27 @@ namespace Microsoft.Boogie // ------------------------------------------------------------------------ // Main - public static void Main (string[] args) + public static int Main (string[] args) {Contract.Requires(cce.NonNullElements(args)); //assert forall{int i in (0:args.Length); args[i] != null}; + ExitValue exitValue = ExitValue.VERIFIED; CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; if (CommandLineOptions.Clo.Parse(args) != 1) { + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } if (CommandLineOptions.Clo.Files.Count == 0) { ErrorWriteLine("*** Error: No input files were specified."); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } if (CommandLineOptions.Clo.XmlSink != null) { string errMsg = CommandLineOptions.Clo.XmlSink.Open(); if (errMsg != null) { ErrorWriteLine("*** Error: " + errMsg); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } } @@ -76,11 +80,12 @@ namespace Microsoft.Boogie { ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy).", file, extension == null ? "" : extension); + exitValue = ExitValue.PREPROCESSING_ERROR; goto END; } } CommandLineOptions.Clo.RunningBoogieOnSsc = false; - ProcessFiles(CommandLineOptions.Clo.Files); + exitValue = ProcessFiles(CommandLineOptions.Clo.Files); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -91,6 +96,7 @@ namespace Microsoft.Boogie Console.WriteLine("Press Enter to exit."); Console.ReadLine(); } + return (int)exitValue; } public static void ErrorWriteLine(string s) {Contract.Requires(s != null); @@ -136,14 +142,16 @@ namespace Microsoft.Boogie enum FileType { Unknown, Cil, Bpl, Dafny }; - static void ProcessFiles (List/*!*/ fileNames) + static ExitValue ProcessFiles (List/*!*/ fileNames) { Contract.Requires(cce.NonNullElements(fileNames)); + ExitValue exitValue = ExitValue.VERIFIED; using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram); if (err != null) { + exitValue = ExitValue.DAFNY_ERROR; ErrorWriteLine(err); } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) { Dafny.Translator translator = new Dafny.Translator(); @@ -164,10 +172,11 @@ namespace Microsoft.Boogie int errorCount, verified, inconclusives, timeOuts, outOfMemories; PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); + bool allOk = errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0; switch (oc) { case PipelineOutcome.VerificationCompleted: WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories); - if ((CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) || CommandLineOptions.Clo.ForceCompile) + if ((CommandLineOptions.Clo.Compile && allOk) || CommandLineOptions.Clo.ForceCompile) CompileDafnyProgram(dafnyProgram); break; case PipelineOutcome.Done: @@ -179,8 +188,10 @@ namespace Microsoft.Boogie // error has already been reported to user break; } + exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED; } } + return exitValue; } private static void CompileDafnyProgram(Dafny.Program dafnyProgram) @@ -373,7 +384,8 @@ namespace Microsoft.Boogie enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted } - + enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED } + /// /// Resolves and type checks the given Boogie program. Any errors are reported to the /// console. Returns: diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index f59215ed..1a2d207a 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -106,12 +106,17 @@ let PrintObjRefName o (env,ctx) = | NewObj(name, _) -> PrintGenSym name | _ -> failwith ("unresolved object ref: " + o.ToString()) +let CheckUnresolved c = + match c with + | Unresolved(_) -> Logger.WarnLine "!!! There are some unresolved constants in the output file !!!"; c + | _ -> c + let PrintVarAssignments (heap,env,ctx) indent = let idt = Indent indent heap |> Map.fold (fun acc (o,f) l -> let objRef = PrintObjRefName o (env,ctx) let fldName = PrintVarName f - let value = TryResolve (env,ctx) l |> PrintConst + let value = TryResolve (env,ctx) l |> CheckUnresolved |> PrintConst acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline ) "" @@ -135,23 +140,33 @@ let GenConstructorCode mthd body = " }" + newline | _ -> "" -// NOTE: insert here coto to say which methods to analyze let GetMethodsToAnalyze prog = - let m = Options.CONFIG.methodToSynth; - if m = "*" then + let mOpt = Options.CONFIG.methodToSynth; + if mOpt = "*" then (* all *) FilterMembers prog FilterConstructorMembers - elif m = "paramsOnly" then + elif mOpt = "paramsOnly" then (* only with parameters *) FilterMembers prog FilterConstructorMembersWithParams else + let allMethods,neg = + if mOpt.StartsWith("~") then + mOpt.Substring(1), true + else + mOpt, false (* exactly one *) - let compName = m.Substring(0, m.LastIndexOf(".")) - let methName = m.Substring(m.LastIndexOf(".") + 1) - let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) - let m = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) - [c, m] - + let methods = allMethods.Split([|','|]) + let lst = methods |> Array.fold (fun acc m -> + let compName = m.Substring(0, m.LastIndexOf(".")) + let methName = m.Substring(m.LastIndexOf(".") + 1) + let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName) + let mthd = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName) + (c,mthd) :: acc + ) [] + if neg then + FilterMembers prog FilterConstructorMembers |> List.filter (fun e -> not (Utils.ListContains e lst)) + else + lst // solutions: (comp, constructor) |--> (heap, env, ctx) let PrintImplCode prog solutions methodsToPrintFunc = diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs index 4cc517f2..4b9b0c60 100644 --- a/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/DafnyModelUtils.fs @@ -256,17 +256,20 @@ let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) = | [] -> (envMap,ctx) // reads stuff from [2] - let __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = + let rec __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = match set_tuples with - | ft :: rest when GetBool ft.Result -> - let srcSetKey = GetLoc ft.Args.[0] - let srcSet = match TryFindSetInEnv env srcSetKey with - | Some(s) -> s - | None -> Set.empty - let elem = UnboxIfNeeded model ft.Args.[1] - let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) - (newEnv,ctx) - | _ -> (env,ctx) + | ft :: rest -> + if GetBool ft.Result then + let srcSetKey = GetLoc ft.Args.[0] + let srcSet = match TryFindSetInEnv env srcSetKey with + | Some(s) -> s + | None -> Set.empty + let elem = UnboxIfNeeded model ft.Args.[1] + let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet)) + __ReadSetMembership rest (newEnv,ctx) + else + __ReadSetMembership rest (env,ctx) + | [] -> (env,ctx) let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps) let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps) diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 1c87ba4d..17c74563 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.sum + C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double pdbonly diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs index d24391f1..f4c0177c 100644 --- a/Jennisys/PipelineUtils.fs +++ b/Jennisys/PipelineUtils.fs @@ -12,6 +12,8 @@ let dafnyVerifySuffix = "verify" let dafnyUnifSuffix = "unif" let dafnySynthFileNameTemplate = @"c:\tmp\jennisys-synth_###.dfy" +let mutable lastDafnyExitCode = 0 //TODO: how to avoid this muttable state? + let CreateEmptyModelFile modelFile = use mfile = System.IO.File.CreateText(modelFile) fprintf mfile "" @@ -29,6 +31,7 @@ let RunDafny inputFile modelFile = proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden assert proc.Start() proc.WaitForExit() + lastDafnyExitCode <- proc.ExitCode } |> Async.RunSynchronously // ======================================================= @@ -51,7 +54,6 @@ let RunDafnyProgram dafnyProgram suffix = /// 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 + lastDafnyExitCode = 0 && models.Count = 0 diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen index 5626babb..6404bfd6 100644 --- a/Jennisys/examples/Set.jen +++ b/Jennisys/examples/Set.jen @@ -46,7 +46,6 @@ model SetNode { data * left * right invariant - left = null && right = null ==> elems = {data} elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {}) left != null ==> forall e :: e in left.elems ==> e < data right != null ==> forall e :: e in right.elems ==> e > data -- cgit v1.2.3 From 0392bb7f399fd0dc55159bc6caf6c249372d480d Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 17:27:13 -0700 Subject: - typos --- Jennisys/Analyzer.fs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Jennisys') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 7b6527f9..7f4b326f 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -188,7 +188,7 @@ let GetObjRefExpr o (heap,env,ctx) = let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = let __CheckUnif o f e idx = - let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx))) + 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 lhs = Dot(objRefExpr, fldName) let assertionExpr = match f with @@ -211,7 +211,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = // change the value to expression acc |> Map.add (o,f) (ExprConst(e)) else - Logger.DebugLine " DOESN'T HOLDS" + Logger.DebugLine " DOESN'T HOLD" // don't change the value acc |> Map.add (o,f) l else @@ -222,7 +222,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = Logger.DebugLine " HOLDS" ExprConst(e) :: __UnifyOverLst rest (cnt+1) else - Logger.DebugLine " DOESN'T HOLDS" + Logger.DebugLine " DOESN'T HOLD" lstElem :: __UnifyOverLst rest (cnt+1) | lstElem :: rest -> lstElem :: __UnifyOverLst rest (cnt+1) -- cgit v1.2.3 From 61acaf623c5acf36b57d958e788f10f3c23bd309 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 19:04:00 -0700 Subject: - added the "timeout" option - started to work on infering branches --- Jennisys/Analyzer.fs | 192 ++++++++++++++++++++++------------------------ Jennisys/AstUtils.fs | 7 ++ Jennisys/Options.fs | 41 +++++++++- Jennisys/PipelineUtils.fs | 2 +- 4 files changed, 139 insertions(+), 103 deletions(-) (limited to 'Jennisys') diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 7f4b326f..7bee9194 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -118,111 +118,112 @@ let GetUnifications expr args (heap,env,ctx) = | UpdateExpr(e1, e2, e3) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args |> __GetUnifications e3 args | SetExpr(elst) | SequenceExpr(elst) -> elst |> List.fold (fun acc e -> acc |> __GetUnifications e args) unifs - + (* --- function body starts here --- *) __GetUnifications expr args Map.empty -//let rec GetUnifications expr args (heap,env,ctx) = -// match expr with -// | IntLiteral(_) -// | BoolLiteral(_) -// | IdLiteral(_) -// | Star -// | Dot(_) -// | SelectExpr(_) // TODO: handle select expr -// | UpdateExpr(_) // TODO: handle update expr -// | SequenceExpr(_) -// | SeqLength(_) -// | SetExpr(_) -// | ForallExpr(_) // TODO: handle forall expr -// | UnaryExpr(_) -> Map.empty -// | IteExpr(c,e0,e1) -> (GetUnifications e0 args (heap,env,ctx)) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx)) -// | BinaryExpr(strength,op,e0,e1) -> -// if op = "=" then -// let v0 = Eval (heap,env,ctx) e0 -// let v1 = Eval (heap,env,ctx) e1 -// 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)); -// Map.ofList [e1, c0] -// | _,_,true,Some(c1) -> -// Logger.DebugLine (" - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0)); -// Map.ofList [e0, c1] -// | _ -> Logger.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); -// Map.empty -// else -// GetUnifications e0 args (heap,env,ctx) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx)) - -let rec GetArgValueUnifications args env = - match args with - | Var(name,_) :: rest -> - match Map.tryFind (Unresolved(name)) env with - | Some(c) -> - Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); - Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env) - | None -> failwith ("couldn't find value for argument " + name) - | [] -> Map.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 - | "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 +// ======================================================= +/// Returns a map (Expr |--> Const) containing unifications +/// found for the given method and heap/env/ctx +// ======================================================= +let GetUnificationsForMethod comp m (heap,env,ctx) = + let rec GetArgValueUnifications args env = + match args with + | Var(name,_) :: rest -> + match Map.tryFind (Unresolved(name)) env with + | Some(c) -> + Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); + Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env) + | None -> failwith ("couldn't find value for argument " + name) + | [] -> Map.empty + (* --- function body starts here --- *) + match m with + | Method(mName,Sig(ins, outs),pre,post,_) -> + let args = List.concat [ins; outs] + match args with + | [] -> Map.empty + | _ -> GetUnifications (BinaryAnd pre post) args (heap,env,ctx) + |> Utils.MapAddAll (GetArgValueUnifications args env) + | _ -> failwith ("not a method: " + m.ToString()) +// ========================================================================= +/// For a given constant "o" (which is an object, something like "gensym32"), +/// finds a path of field references from "this". +/// +/// Implements a backtracking search over the heap entries to find that +/// path. It starts from the given object, and follows the backpointers +/// until it reaches the root ("this") +// ========================================================================= let GetObjRefExpr o (heap,env,ctx) = - _GetObjRefExpr o (heap,env,ctx) (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 + | "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 + (* --- function body starts here --- *) + __GetObjRefExpr o (heap,env,ctx) (Set.empty) -let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = +// ======================================================= +/// Applies given unifications onto the given heap/env/ctx +/// +/// If "conservative" is true, applies only those that +/// can be verified to hold, otherwise applies all of them +// ======================================================= +let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = let __CheckUnif o f e idx = - 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 lhs = Dot(objRefExpr, fldName) - let assertionExpr = match f with - | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e - | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs - | _ -> BinaryEq lhs 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) + " ... ") - CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) - + if not conservative then + true + else + 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 lhs = Dot(objRefExpr, fldName) + let assertionExpr = match f with + | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e + | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs + | _ -> BinaryEq lhs 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_" + (GetMethodFullName comp mthd)) + if ok then + Logger.DebugLine " HOLDS" + else + Logger.DebugLine " DOESN'T HOLD" + ok + (* --- function body starts here --- *) match unifs with | (e,c) :: rest -> - let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx) + let restHeap,env,ctx = ApplyUnifications prog comp mthd rest (heap,env,ctx) conservative let newHeap = restHeap |> Map.fold (fun acc (o,f) l -> let value = TryResolve (env,ctx) l if value = c then - if __CheckUnif o f e -1 then - Logger.DebugLine " HOLDS" + if __CheckUnif o f e -1 then // change the value to expression + Logger.TraceLine (sprintf " - applied: %s.%s --> %s" (PrintConst o) (GetVarName f) (PrintExpr 0 e) ) acc |> Map.add (o,f) (ExprConst(e)) else - Logger.DebugLine " DOESN'T HOLD" - // don't change the value + // don't change the value unless "conservative = false" acc |> Map.add (o,f) l else let rec __UnifyOverLst lst cnt = match lst with | lstElem :: rest when lstElem = c -> if __CheckUnif o f e cnt then - Logger.DebugLine " HOLDS" + Logger.TraceLine (sprintf " - applied: %s.%s[%d] --> %s" (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) ) ExprConst(e) :: __UnifyOverLst rest (cnt+1) - else - Logger.DebugLine " DOESN'T HOLD" + else lstElem :: __UnifyOverLst rest (cnt+1) | lstElem :: rest -> lstElem :: __UnifyOverLst rest (cnt+1) @@ -241,18 +242,6 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = (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) //TODO: we shouldn't use desugar here, but in UpdateHeapEnv - |> Utils.MapAddAll (GetArgValueUnifications args env) - UpdateHeapEnv prog comp mthd (Map.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 // ==================================================================================== @@ -261,6 +250,10 @@ let VerifySolution prog comp mthd (heap,env,ctx) = let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx) let code = PrintImplCode prog solution (fun p -> [comp,mthd]) CheckDafnyProgram code dafnyVerifySuffix + +let TryInferConditionals prog comp m unifs (heap,env,ctx) = + let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false + Some(heap2,env2,ctx2) // ============================================================================ /// Attempts to synthesize the initialization code for the given constructor "m" @@ -272,7 +265,7 @@ let AnalyzeConstructor prog comp m = // generate Dafny code for analysis first let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral) Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m))) - Logger.Info " - searching for a solution ..." + Logger.Info " - searching for an instance ..." let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) if models.Count = 0 then // no models means that the "assert false" was verified, which means that the spec is inconsistent @@ -285,7 +278,8 @@ let AnalyzeConstructor prog comp m = Logger.InfoLine " OK " let model = models.[0] let heap,env,ctx = ReadFieldValuesFromModel model prog comp m - |> GeneralizeSolution prog comp m + let unifs = GetUnificationsForMethod comp m (heap,env,ctx) |> Map.toList + let heap,env,ctx = ApplyUnifications prog comp m unifs (heap,env,ctx) true if Options.CONFIG.verifySolutions then Logger.InfoLine " - verifying synthesized solution ... " let verified = VerifySolution prog comp m (heap,env,ctx) @@ -295,7 +289,7 @@ let AnalyzeConstructor prog comp m = Some(heap,env,ctx) else Logger.InfoLine "!!! NOT VERIFIED !!!" - Some(heap,env,ctx) + TryInferConditionals prog comp m unifs (heap,env,ctx) else Some(heap,env,ctx) diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index 32d58ec7..a0d53d0c 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -332,6 +332,13 @@ let GetInvariantsAsList comp = List.append (SplitIntoConjunts inv) clsInvs | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString()) +// ================================== +/// Returns variable name +// ================================== +let GetVarName var = + match var with + | Var(name,_) -> name + // ================================== /// Returns all members of a component // ================================== diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 355ada6e..291bd678 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -12,12 +12,14 @@ type Config = { inputFilename: string; methodToSynth: string; verifySolutions: bool; + timeout: int; } let defaultConfig: Config = { inputFilename = ""; methodToSynth = "*"; verifySolutions = true; + timeout = 0; } let mutable CONFIG = defaultConfig @@ -47,6 +49,24 @@ let ParseCmdLineArgs args = else let x = __StripSwitches splits.[0] (x, "") + + let __CheckNonEmpty value optName = + if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty")) + + let __CheckInt value optName = + try + System.Int32.Parse value + with + | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean")) + + let __CheckBool value optName = + if value = "" then + true + else + try + System.Boolean.Parse value + with + | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer")) let rec __Parse args cfg = match args with @@ -54,14 +74,29 @@ let ParseCmdLineArgs args = let opt,value = __Split fs match opt with | "method" -> - if value = "" then raise (InvalidCmdLineArg("Must provide method name")) + __CheckNonEmpty value opt __Parse rest { cfg with methodToSynth = value } | "verifySol" -> - __Parse rest { cfg with verifySolutions = true } + let b = __CheckBool value opt + __Parse rest { cfg with verifySolutions = b } + | "timeout" -> + let t = __CheckInt value opt + __Parse rest { cfg with timeout = t } | "" -> __Parse rest { cfg with inputFilename = value } | _ -> raise (InvalidCmdLineOption("Unknown option: " + opt)) - | [] -> cfg + | [] -> cfg + + let __CheckBool value optName = + if value = "" then + true + else + try + System.Boolean.Parse value + with + | ex -> raise (InvalidCmdLineArg("Option " + optName " must be boolean")) + + (* --- function body starts here --- *) CONFIG <- __Parse args defaultConfig diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs index f4c0177c..1439018a 100644 --- a/Jennisys/PipelineUtils.fs +++ b/Jennisys/PipelineUtils.fs @@ -27,7 +27,7 @@ let RunDafny inputFile modelFile = async { use proc = new System.Diagnostics.Process() proc.StartInfo.FileName <- @"c:\tmp\StartDafny-jen.bat" - proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile + proc.StartInfo.Arguments <- (sprintf "/mv:%s /timeLimit:%d %s" modelFile Options.CONFIG.timeout inputFile) proc.StartInfo.WindowStyle <- System.Diagnostics.ProcessWindowStyle.Hidden assert proc.Start() proc.WaitForExit() -- cgit v1.2.3