From 0482fe48f2c8e1095305ba60ffb93cf1c0656201 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 6 Jul 2011 13:47:01 -0700 Subject: - implemented some sorts of symbolic evaluation of expressions - changed that the intermediate dafny files are written into separate files for different method analyses - added README and StartDafny-jen.bat --- Jennisys/Analyzer.fs | 33 ++++++--- Jennisys/AstUtils.fs | 130 ++++++++++++++++++++++++++++++++++-- Jennisys/CodeGen.fs | 12 ++-- Jennisys/README.txt | 5 ++ Jennisys/Resolver.fs | 7 ++ Jennisys/examples/List2.jen | 3 + Jennisys/examples/List3.jen | 3 + Jennisys/scripts/StartDafny-jen.bat | 3 + 8 files changed, 175 insertions(+), 21 deletions(-) create mode 100644 Jennisys/README.txt create mode 100644 Jennisys/scripts/StartDafny-jen.bat diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index 69b5bb69..244b50b4 100644 --- a/Jennisys/Analyzer.fs +++ b/Jennisys/Analyzer.fs @@ -104,7 +104,7 @@ let rec GetUnifications expr args (heap,env,ctx) = | _,_,true,Some(c1) -> Logger.DebugLine (" - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0)); Set.ofList [c1, e0] - | _ -> Logger.WarnLine (" - [WARN] couldn't unify anything from " + (PrintExpr 0 expr)); + | _ -> Logger.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); Set.empty else GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) @@ -113,7 +113,9 @@ let rec GetArgValueUnifications args env = match args with | Var(name,_) :: rest -> match Map.tryFind (VarConst(name)) env with - | Some(c) -> Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) + | Some(c) -> + Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); + Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) | None -> failwith ("couldn't find value for argument " + name) | [] -> Set.empty @@ -152,7 +154,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = // check if the assertion follows and if so update the env let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) Logger.Debug(" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") - let ok = CheckDafnyProgram code "unif" + let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) if ok then Logger.DebugLine " HOLDS" // change the value to expression @@ -161,9 +163,14 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = Logger.DebugLine " DOESN'T HOLDS" // don't change the value acc |> Map.add (o,f) l - else - // leave it as is - acc |> Map.add (o,f) l) restHeap + else + // see if it's a list, then try to match its elements + match value with + | SeqConst(clist) -> acc |> Map.add (o,f) l //TODO!! + | _ -> + // leave it as is + acc |> Map.add (o,f) l + ) restHeap (newHeap,env,ctx) | [] -> (heap,env,ctx) @@ -199,7 +206,7 @@ let AnalyzeConstructor prog comp m = let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral) Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m))) Logger.Info " - searching for a solution ..." - let models = RunDafnyProgram code dafnyScratchSuffix + let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) if models.Count = 0 then // no models means that the "assert false" was verified, which means that the spec is inconsistent Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!" @@ -213,15 +220,18 @@ let AnalyzeConstructor prog comp m = let heap,env,ctx = ReadFieldValuesFromModel model prog comp m |> GeneralizeSolution prog comp m if _opt_verifySolutions then - Logger.Info " - verifying synthesized solution ..." - if VerifySolution prog comp m (heap,env,ctx) then - Logger.InfoLine " OK" + Logger.InfoLine " - verifying synthesized solution ... " + let verified = VerifySolution prog comp m (heap,env,ctx) + Logger.Info " " + if verified then + Logger.InfoLine "~~~ VERIFIED ~~~" Some(heap,env,ctx) else - Logger.InfoLine " NOT VERIFIED" + Logger.InfoLine "!!! NOT VERIFIED !!!" Some(heap,env,ctx) else Some(heap,env,ctx) + // ============================================================================ /// Goes through a given list of methods of the given program and attempts to @@ -235,6 +245,7 @@ let rec AnalyzeMethods prog members = match m with | Method(_,_,_,_,true) -> let solOpt = AnalyzeConstructor prog comp m + Logger.InfoLine "" match solOpt with | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx) | None -> AnalyzeMethods prog rest diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs index f9f7c43f..442dfe57 100644 --- a/Jennisys/AstUtils.fs +++ b/Jennisys/AstUtils.fs @@ -27,15 +27,120 @@ let rec VisitExpr visitorFunc expr acc = exception EvalFailed -//TODO: stuff might be missing -let rec EvalToConst expr = +let rec EvalSym expr = match expr with | IntLiteral(n) -> IntConst(n) | IdLiteral(id) -> VarConst(id) | Dot(e, str) -> - match EvalToConst e with + match EvalSym e with | VarConst(lhsName) -> VarConst(lhsName + "." + str) - | _ -> raise EvalFailed + | _ -> ExprConst(expr) + | SeqLength(e) -> + match EvalSym e with + | SeqConst(clist) -> IntConst(List.length clist) + | _ -> ExprConst(expr) + | SequenceExpr(elist) -> + let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev |> Utils.ConvertToOptionList + SeqConst(clist) + | SelectExpr(lst, idx) -> + match EvalSym lst, EvalSym idx with + | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | _ -> ExprConst(expr) + | UpdateExpr(lst,idx,v) -> + match EvalSym lst, EvalSym idx, EvalSym v with + | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) + | _ -> ExprConst(expr) + | BinaryExpr(_,op,e1,e2) -> + match op with + | Exact "=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) + | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) + | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) + | _ -> ExprConst(expr) + | Exact "!=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) + | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) + | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) + | _ -> ExprConst(expr) + | Exact "<" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) + | _ -> ExprConst(expr) + | Exact "<=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) + | _ -> ExprConst(expr) + | Exact "in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(Set.contains (Some(c)) s) + | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains (Some(c)) s) + | _ -> ExprConst(expr) + | Exact "!in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(not (Set.contains (Some(c)) s)) + | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains (Some(c)) s)) + | _ -> ExprConst(expr) + | Exact "+" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) + | _ -> ExprConst(expr) + | Exact "*" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) + | _ -> ExprConst(expr) + | Exact "div" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) + | _ -> ExprConst(expr) + | Exact "mod" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + | UnaryExpr(op, e) -> + match op with + | Exact "!" _ -> + match EvalSym e with + | BoolConst(b) -> BoolConst(not b) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e with + | IntConst(n) -> IntConst(-n) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + +//TODO: stuff might be missing +let rec EvalToConst expr = + match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) -> raise EvalFailed //VarConst(id) + | Dot(e, str) -> raise EvalFailed | SeqLength(e) -> match EvalToConst e with | SeqConst(clist) -> IntConst(List.length clist) @@ -186,6 +291,13 @@ let FilterFieldMembers members = let FilterConstructorMembers members = members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None) +// ============================================================= +/// Out of all "members" returns only those that are +/// constructors and have at least one input parameter +// ============================================================= +let FilterConstructorMembersWithParams members = + members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) + // ========================================================== /// Out of all "members" returns only those that are "Method"s // ========================================================== @@ -229,6 +341,12 @@ let GetMethodName mthd = | Method(name,_,_,_,_) -> name | _ -> failwith ("not a method: " + mthd.ToString()) +// =========================================================== +/// Returns full name of a method (= . +// =========================================================== +let GetMethodFullName comp mthd = + (GetClassName comp) + "." + (GetMethodName mthd) + // ============================= /// Returns signature of a method // ============================= @@ -305,7 +423,7 @@ let rec Desugar expr = | SelectExpr(_) | SeqLength(_) -> expr | UpdateExpr(_) -> expr //TODO - | SequenceExpr(exs) -> expr //TODO: + | SequenceExpr(exs) -> expr //TODO | ForallExpr(v,e) -> ForallExpr(v, Desugar e) | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e) | BinaryExpr(p,op,e1,e2) -> @@ -313,7 +431,7 @@ let rec Desugar expr = try match op with | Exact "=" _ -> - match EvalToConst e1, EvalToConst e2 with + match EvalSym e1, EvalSym e2 with | VarConst(v), SeqConst(clist) | SeqConst(clist), VarConst(v) -> let rec __fff lst cnt = diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs index b7b5ff15..7e61ec7e 100644 --- a/Jennisys/CodeGen.fs +++ b/Jennisys/CodeGen.fs @@ -137,10 +137,14 @@ let GenConstructorCode mthd body = // NOTE: insert here coto to say which methods to analyze let GetMethodsToAnalyze prog = - let c = FindComponent prog "IntList" |> Utils.ExtractOption - let m = FindMethod c "Double" |> Utils.ExtractOption - [c, m] -// FilterMembers prog FilterConstructorMembers + (* exactly one *) +// let c = FindComponent prog "IntList" |> Utils.ExtractOption +// let m = FindMethod c "Sum" |> Utils.ExtractOption +// [c, m] + (* all *) + FilterMembers prog FilterConstructorMembers + (* only with parameters *) +// FilterMembers prog FilterConstructorMembersWithParams // solutions: (comp, constructor) |--> (heap, env, ctx) let PrintImplCode prog solutions methodsToPrintFunc = diff --git a/Jennisys/README.txt b/Jennisys/README.txt new file mode 100644 index 00000000..0e52dec9 --- /dev/null +++ b/Jennisys/README.txt @@ -0,0 +1,5 @@ +1. Installation instructions +---------------------------- + + - create c:\tmp folder + - copy the Jennisys\scripts\StartDafny-jen.bat script into c:\tmp diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs index ab7ffb8f..f1a1f67f 100644 --- a/Jennisys/Resolver.fs +++ b/Jennisys/Resolver.fs @@ -53,6 +53,12 @@ let rec EvalUnresolved expr (heap,env,ctx) = | ((_,_),x) :: [] -> x | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str + | SelectExpr(lst, idx) -> + let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) + let idxC = EvalUnresolved idx (heap,env,ctx) + match lstC, idxC with + | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | _ -> failwith "can't eval SelectExpr" | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! // | Star // | SelectExpr(_) @@ -63,6 +69,7 @@ let rec EvalUnresolved expr (heap,env,ctx) = // | UnaryExpr(_) // | BinaryExpr(_) +// TODO: can this be implemented on top of the existing AstUtils.EvalSym?? We must! let Eval expr (heap,env,ctx) = try let unresolvedConst = EvalUnresolved expr (heap,env,ctx) diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen index b7ceaec0..e99cf342 100644 --- a/Jennisys/examples/List2.jen +++ b/Jennisys/examples/List2.jen @@ -18,6 +18,9 @@ class IntList { constructor Double(p: int, q: int) ensures list = [p] + [q] + + constructor Sum(p: int, q: int) + ensures list = [p + q] } model IntList { diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen index f37a2631..6bb49eb8 100644 --- a/Jennisys/examples/List3.jen +++ b/Jennisys/examples/List3.jen @@ -18,6 +18,9 @@ class IntList { constructor Double(p: int, q: int) ensures list = [p] + [q] + + constructor Sum(p: int, q: int) + ensures list = [p + q] } model IntList { diff --git a/Jennisys/scripts/StartDafny-jen.bat b/Jennisys/scripts/StartDafny-jen.bat new file mode 100644 index 00000000..79d39a38 --- /dev/null +++ b/Jennisys/scripts/StartDafny-jen.bat @@ -0,0 +1,3 @@ +@echo off +"c:/boogie/Binaries/Dafny.exe" -nologo -compile:0 /print:xxx.bpl -timeLimit:60 %* > c:\tmp\jen-doo.out +exit 43 -- cgit v1.2.3