From f2758f1e16e1a383ac6f49a0d68b7d6a50c368da Mon Sep 17 00:00:00 2001 From: Aleksandar Milicevic Date: Mon, 15 Aug 2011 18:46:08 -0700 Subject: Jennisys: - added concreteValues field to HeapInstance - brought back reading from Seq#Build when restoring Boogie models - changed the how the candidate conditions are inferred: now it only looks for unmodifiable concrete fields - method in parameter values are added to the list of potential candidate conditions --- Jennisys/Jennisys/Analyzer.fs | 114 +++++---- Jennisys/Jennisys/AstUtils.fs | 468 ++++++++++++++++++----------------- Jennisys/Jennisys/CodeGen.fs | 20 +- Jennisys/Jennisys/DafnyModelUtils.fs | 15 +- Jennisys/Jennisys/Jennisys.fsproj | 2 +- Jennisys/Jennisys/Logger.fs | 2 +- Jennisys/Jennisys/MethodUnifier.fs | 1 + Jennisys/Jennisys/Modularizer.fs | 6 +- Jennisys/Jennisys/Resolver.fs | 89 ++++++- Jennisys/Jennisys/examples/List.jen | 5 + Jennisys/Jennisys/tmp.out | 435 -------------------------------- 11 files changed, 403 insertions(+), 754 deletions(-) delete mode 100644 Jennisys/Jennisys/tmp.out diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index f439c8d0..512a6870 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -140,7 +140,7 @@ let GetHeapExpr prog mthd heapInst = objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc ) prepostExpr -let IsUnmodOnly (comp,meth) expr = +let IsUnmodConcrOnly (comp,meth) expr = let isConstr = IsConstructor meth let rec __IsUnmodOnly args expr = let __IsUnmodOnlyLst elist = @@ -151,11 +151,13 @@ let IsUnmodOnly (comp,meth) expr = | BoxLiteral(_) | Star | VarDeclExpr(_) - | ObjLiteral(_) -> true - | VarLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) - | IdLiteral("null") -> true - | IdLiteral(id) -> if isConstr then false else true //TODO: tempporary implementation - | Dot(e, fldName) -> if isConstr then false else __IsUnmodOnlyLst [e] + | ObjLiteral(_) -> true + | VarLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) + | IdLiteral("null") | IdLiteral("this") -> true + | IdLiteral(id) -> + let isAbstractFld = GetAbstractFields comp |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) + not (isConstr || isAbstractFld) + | Dot(e, fldName) -> if isConstr then false else __IsUnmodOnlyLst [e] // TODO: this is how it should really work // let lhsType = InferType prog e // let isMod = IsFieldModifiable lhsType fldName @@ -164,14 +166,14 @@ let IsUnmodOnly (comp,meth) expr = | AssumeExpr(e) | SeqLength(e) | LCIntervalExpr(e) - | UnaryExpr(_,e) -> __IsUnmodOnlyLst [e] + | UnaryExpr(_,e) -> __IsUnmodOnlyLst [e] | SelectExpr(e1, e2) - | BinaryExpr(_,_,e1,e2) -> __IsUnmodOnlyLst [e1; e2] + | BinaryExpr(_,_,e1,e2) -> __IsUnmodOnlyLst [e1; e2] | IteExpr(e3, e1, e2) - | UpdateExpr(e1, e2, e3) -> __IsUnmodOnlyLst [e1; e2; e3] - | SequenceExpr(exprs) | SetExpr(exprs) -> __IsUnmodOnlyLst exprs - | MethodCall(rcv,_,_,aparams) -> __IsUnmodOnlyLst (rcv :: aparams) - | ForallExpr(vars,e) -> __IsUnmodOnly (args @ vars) e + | UpdateExpr(e1, e2, e3) -> __IsUnmodOnlyLst [e1; e2; e3] + | SequenceExpr(exprs) | SetExpr(exprs) -> __IsUnmodOnlyLst exprs + | MethodCall(rcv,_,_,aparams) -> __IsUnmodOnlyLst (rcv :: aparams) + | ForallExpr(vars,e) -> __IsUnmodOnly (args @ vars) e (* --- function body starts here --- *) __IsUnmodOnly (GetMethodInArgs meth) expr @@ -196,7 +198,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr = else let builder = new CascadingBuilder<_>(unifsAcc) builder { - let! argsOnly = IsUnmodOnly (comp,meth) e |> Utils.BoolToOption + let! argsOnly = IsUnmodConcrOnly (comp,meth) e |> Utils.BoolToOption let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None return AddUnif indent e v unifsAcc } @@ -421,41 +423,59 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph = let methodArgs = GetMethodInArgs m let expr = GetHeapExpr prog m heapInst2 // now evaluate and see what's left - // printf "%s" (expr |> SplitIntoConjunts |> PrintSep newline (fun e -> PrintExpr 0 e)) - let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr - if newCond = TrueLiteral then - Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) - wrongSol - else - let candCond = - if newCond = FalseLiteral then - // it must be because there is some aliasing going on between method arguments, - // so we should try that as a candidate pre-condition - let tmp = DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2 - if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered") - tmp - else - newCond - Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 candCond)) - let _,_,m2 = AddPrecondition prog comp m candCond - let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph - Logger.Info (idt + " - verifying partial solution ... ") - let verified = - if Options.CONFIG.verifyPartialSolutions then - VerifySolution prog sol Options.CONFIG.genRepr - else - true - if verified then - if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" - let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with - | Some(sol2) -> sol2 - | None -> sol - let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond)) - let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph - MergeSolutions solThis solRest |> FixSolution comp m + //printfn "%s" (expr |> SplitIntoConjunts |> PrintSep (newline + newline) (fun e -> PrintExpr 0 e)) + + let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2) + let newConds = expr |> SplitIntoConjunts + |> List.fold (fun acc e -> + Logger.TraceLine (idt + ">>> " + (PrintExpr 0 e)) + let v = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) e + Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 v)) + if v = TrueLiteral then + acc + elif v = FalseLiteral && (not aliasingCond.IsValueCreated) then + let aliasingExpr = aliasingCond.Force() + if aliasingExpr = TrueLiteral then + failwith ("post-condition evaluated to false and no aliasing was discovered") + acc @ [aliasingExpr] + else + acc @ [v] + ) [] + |> List.filter (IsUnmodConcrOnly (comp,m)) + let newConds = + if newConds = [] && IsSolution1stLevelOnly heapInst2 then + heapInst2.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) [] else - Logger.InfoLine "NOT VERIFIED" - wrongSol + newConds + + // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr + match newConds with + | [] -> + Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) + wrongSol + | _ -> + //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO + let candCond = newConds |> List.fold BinaryAnd TrueLiteral + Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 candCond)) + let _,_,m2 = AddPrecondition prog comp m candCond + let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph + Logger.Info (idt + " - verifying partial solution ... ") + let verified = + if Options.CONFIG.verifyPartialSolutions then + VerifySolution prog sol Options.CONFIG.genRepr + else + true + if verified then + if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" + let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with + | Some(sol2) -> sol2 + | None -> sol + let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond)) + let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph + MergeSolutions solThis solRest |> FixSolution comp m + else + Logger.InfoLine "NOT VERIFIED" + wrongSol let GetMethodsToAnalyze prog = let mOpt = Options.CONFIG.methodToSynth; diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs index a866ad08..f5d90489 100644 --- a/Jennisys/Jennisys/AstUtils.fs +++ b/Jennisys/Jennisys/AstUtils.fs @@ -168,6 +168,7 @@ let UnaryNeg sub = let UnaryNot sub = match sub with | UnaryExpr("!", s) -> s + | BoolLiteral(b) -> BoolLiteral(not b) | _ -> UnaryExpr("!", sub) // ======================================================================= @@ -203,7 +204,7 @@ let BinaryOr (lhs: Expr) (rhs: Expr) = // =================================================================================== let BinaryImplies lhs rhs = match lhs, rhs with - | BoolLiteral(false), _ -> FalseLiteral + | BoolLiteral(false), _ -> TrueLiteral | BoolLiteral(true), _ -> rhs | _, BoolLiteral(true) -> lhs | _, BoolLiteral(false) -> UnaryNot(lhs) @@ -580,245 +581,243 @@ let __CheckEqual e1 e2 = | _ when e1 = e2 -> Some(true) | _ -> None -let rec __EvalSym resolverFunc ctx expr = - match expr with - | IntLiteral(_) -> expr - | BoolLiteral(_) -> expr - | BoxLiteral(_) -> expr - | ObjLiteral(_) -> expr - | Star -> expr //TODO: can we do better? - | VarDeclExpr(_) -> expr - | AssertExpr(e) -> AssertExpr(__EvalSym resolverFunc ctx e) - | AssumeExpr(e) -> AssumeExpr(__EvalSym resolverFunc ctx e) - | VarLiteral(id) -> - try - let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id) - e - with - | ex -> resolverFunc expr None - | IdLiteral(_) -> resolverFunc expr None - | Dot(e, str) -> - let discr = __EvalSym resolverFunc ctx e - resolverFunc discr (Some(str)) - | SeqLength(e) -> - let e' = __EvalSym resolverFunc ctx e - match e' with - | SequenceExpr(elist) -> IntLiteral(List.length elist) - | _ -> SeqLength(e') - | SequenceExpr(elist) -> - let elist' = elist |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev - SequenceExpr(elist') - | SetExpr(elist) -> - let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc ctx e) acc) Set.empty - SetExpr(Set.toList eset') - | MethodCall(rcv,cname, mname,aparams) -> - let rcv' = __EvalSym resolverFunc ctx rcv - let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev - MethodCall(rcv', cname, mname, aparams') - | LCIntervalExpr(_) -> expr - | SelectExpr(lst, idx) -> - let lst' = __EvalSym resolverFunc ctx lst - let idx' = __EvalSym resolverFunc ctx idx - match lst', idx' with - | SequenceExpr(elist), IntLiteral(n) -> elist.[n] - | SequenceExpr(elist), LCIntervalExpr(startIdx) -> - let startIdx' = __EvalSym resolverFunc ctx startIdx - match startIdx' with - | IntLiteral(startIdxInt) -> - let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l) - SequenceExpr(__Skip startIdxInt elist) - | _ -> SelectExpr(lst', idx') - | _ -> SelectExpr(lst', idx') - | UpdateExpr(lst,idx,v) -> - let lst', idx', v' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx, __EvalSym resolverFunc ctx v - match lst', idx', v' with - | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist) - | _ -> UpdateExpr(lst', idx', v') - | IteExpr(c, e1, e2) -> - let c' = __EvalSym resolverFunc ctx c - match c' with - | BoolLiteral(b) -> if b then __EvalSym resolverFunc ctx e1 else __EvalSym resolverFunc ctx e2 - | _ -> IteExpr(c', __EvalSym resolverFunc ctx e1, __EvalSym resolverFunc ctx e2) - | BinaryExpr(p,op,e1,e2) -> - let e1' = lazy (__EvalSym resolverFunc ctx e1) - let e2' = lazy (__EvalSym resolverFunc ctx e2) - let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force())) - match op with - | "=" -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - let eq = __CheckEqual e1'' e2'' - match eq with - | Some(b) -> BoolLiteral(b) - | None -> recomposed.Force() - | "!=" -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - let eq = __CheckEqual e1'' e2'' - match eq with - | Some(b) -> BoolLiteral(not b) - | None -> recomposed.Force() - | "<" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 < n2) - | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) - | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) - | _ -> recomposed.Force() - | "<=" -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - let eq = __CheckEqual e1'' e2'' - match eq with - | Some(true) -> TrueLiteral - | _ -> match e1'', e2'' with - | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2) - | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) - | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) - | _ -> recomposed.Force() - | ">" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2) - | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) - | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) - | _ -> recomposed.Force() - | ">=" -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - let eq = __CheckEqual e1'' e2'' - match eq with - | Some(true) -> TrueLiteral - | _ -> match e1'', e2'' with - | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2) - | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) - | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) - | _ -> recomposed.Force() - | ".." -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - match e1'', e2'' with - | IntLiteral(lo), IntLiteral(hi) -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n))) - | _ -> recomposed.Force(); - | "in" -> - match e1'.Force(), e2'.Force() with - | _, SetExpr(s) - | _, SequenceExpr(s) -> BoolLiteral(Utils.ListContains (e1'.Force()) s) - | _ -> recomposed.Force() - | "!in" -> - match e1'.Force(), e2'.Force() with - | _, SetExpr(s) - | _, SequenceExpr(s) -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s)) - | _ -> recomposed.Force() - | "+" -> - let e1'' = e1'.Force(); - let e2'' = e2'.Force(); - match e1'', e2'' with - | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2) - | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2) - | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList) - | SetExpr(s), _ -> SetExpr(Set.add e2'' (Set.ofList s) |> Set.toList) - | _, SetExpr(s) -> SetExpr(Set.add e1'' (Set.ofList s) |> Set.toList) - | _ -> recomposed.Force() - | "-" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2) - | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList) - | _ -> recomposed.Force() - | "*" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2) - | _ -> recomposed.Force() - | "div" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2) - | _ -> recomposed.Force() - | "mod" -> - match e1'.Force(), e2'.Force() with - | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2) - | _ -> recomposed.Force() - | "&&" -> - // shortcircuit - match e1'.Force() with - | BoolLiteral(false) -> BoolLiteral(false) - | _ -> - match e1'.Force(), e2'.Force() with - | BoolLiteral(false), _ -> BoolLiteral(false) - | _, BoolLiteral(false) -> BoolLiteral(false) - | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2) - | _ -> BinaryAnd (e1'.Force()) (e2'.Force()) - | "||" -> - // shortcircuit - match e1'.Force() with - | BoolLiteral(true) -> BoolLiteral(true) - | _ -> - match e1'.Force(), e2'.Force() with - | BoolLiteral(true), _ -> BoolLiteral(true) - | _, BoolLiteral(true) -> BoolLiteral(true) - | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2) - | _ -> BinaryOr (e1'.Force()) (e2'.Force()) - | "==>" -> - // shortcircuit - match e1'.Force() with - | BoolLiteral(false) -> BoolLiteral(true) - | _ -> - let e1'' = e1'.Force() - let e2'' = e2'.Force() - match e1'', e2'' with - | BoolLiteral(false), _ -> BoolLiteral(true) - | _, BoolLiteral(true) -> BoolLiteral(true) - | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2) - | _ -> BinaryImplies (e1'.Force()) (e2'.Force()) - | "<==>" -> - match e1'.Force(), e2'.Force() with - | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2) - | x, BoolLiteral(b) - | BoolLiteral(b), x -> if b then x else UnaryNot(x) - | _ -> recomposed.Force() - | _ -> recomposed.Force() - | UnaryExpr(op, e) -> - let e' = __EvalSym resolverFunc ctx e - let recomposed = UnaryExpr(op, e') - match op with - | "!" -> - match e' with - | BoolLiteral(b) -> BoolLiteral(not b) - | _ -> recomposed - | "-" -> - match e' with - | IntLiteral(n) -> IntLiteral(-n) - | _ -> recomposed - | _ -> recomposed - | ForallExpr(vars, e) -> - let rec __ExhaustVar v restV vDomain = - match vDomain with - | vv :: restD -> - let ctx' = (v,vv) :: ctx - let e' = __EvalSym resolverFunc ctx' (ForallExpr(restV, e)) - let erest = __ExhaustVar v restV restD - (* __EvalSym resolverFunc ctx' *) - BinaryAnd e' erest - | [] -> BoolLiteral(true) - let rec __TraverseVars vars = - match vars with - | v :: restV -> - try - let vDom = GetVarDomain resolverFunc ctx v e - __ExhaustVar v restV vDom - with - | ex -> ForallExpr([v], __TraverseVars restV) - | [] -> __EvalSym resolverFunc ctx e - (* --- function body starts here --- *) - __TraverseVars vars -and GetVarDomain resolverFunc ctx var expr = +let rec __EvalSym resolverFunc returnFunc ctx expr = + let expr' = + match expr with + | IntLiteral(_) -> expr + | BoolLiteral(_) -> expr + | BoxLiteral(_) -> expr + | ObjLiteral(_) -> expr + | Star -> expr //TODO: can we do better? + | VarDeclExpr(_) -> expr + | AssertExpr(e) -> AssertExpr(__EvalSym resolverFunc returnFunc ctx e) + | AssumeExpr(e) -> AssumeExpr(__EvalSym resolverFunc returnFunc ctx e) + | VarLiteral(id) -> + try + let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id) + e + with + | ex -> resolverFunc expr None + | IdLiteral(_) -> resolverFunc expr None + | Dot(e, str) -> + let discr = __EvalSym resolverFunc returnFunc ctx e + resolverFunc discr (Some(str)) + | SeqLength(e) -> + let e' = __EvalSym resolverFunc returnFunc ctx e + match e' with + | SequenceExpr(elist) -> IntLiteral(List.length elist) + | _ -> SeqLength(e') + | SequenceExpr(elist) -> + let elist' = elist |> List.fold (fun acc e -> (__EvalSym resolverFunc returnFunc ctx e) :: acc) [] |> List.rev + SequenceExpr(elist') + | SetExpr(elist) -> + let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc returnFunc ctx e) acc) Set.empty + SetExpr(Set.toList eset') + | MethodCall(rcv,cname, mname,aparams) -> + let rcv' = __EvalSym resolverFunc returnFunc ctx rcv + let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc returnFunc ctx e :: acc) [] |> List.rev + MethodCall(rcv', cname, mname, aparams') + | LCIntervalExpr(_) -> expr + | SelectExpr(lst, idx) -> + let lst' = __EvalSym resolverFunc returnFunc ctx lst + let idx' = __EvalSym resolverFunc returnFunc ctx idx + match lst', idx' with + | SequenceExpr(elist), IntLiteral(n) -> elist.[n] + | SequenceExpr(elist), LCIntervalExpr(startIdx) -> + let startIdx' = __EvalSym resolverFunc returnFunc ctx startIdx + match startIdx' with + | IntLiteral(startIdxInt) -> + let rec __Skip n l = if n = 0 then l else __Skip (n-1) (List.tail l) + SequenceExpr(__Skip startIdxInt elist) + | _ -> SelectExpr(lst', idx') + | _ -> SelectExpr(lst', idx') + | UpdateExpr(lst,idx,v) -> + let lst', idx', v' = __EvalSym resolverFunc returnFunc ctx lst, __EvalSym resolverFunc returnFunc ctx idx, __EvalSym resolverFunc returnFunc ctx v + match lst', idx', v' with + | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist) + | _ -> UpdateExpr(lst', idx', v') + | IteExpr(c, e1, e2) -> + let c' = __EvalSym resolverFunc returnFunc ctx c + match c' with + | BoolLiteral(b) -> if b then __EvalSym resolverFunc returnFunc ctx e1 else __EvalSym resolverFunc returnFunc ctx e2 + | _ -> IteExpr(c', __EvalSym resolverFunc returnFunc ctx e1, __EvalSym resolverFunc returnFunc ctx e2) + | BinaryExpr(p,op,e1,e2) -> + let e1' = lazy (__EvalSym resolverFunc returnFunc ctx e1) + let e2' = lazy (__EvalSym resolverFunc returnFunc ctx e2) + let recomposed = lazy (BinaryExpr(p, op, e1'.Force(), e2'.Force())) + match op with + | "=" -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + let eq = __CheckEqual e1'' e2'' + match eq with + | Some(b) -> BoolLiteral(b) + | None -> recomposed.Force() + | "!=" -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + let eq = __CheckEqual e1'' e2'' + match eq with + | Some(b) -> BoolLiteral(not b) + | None -> recomposed.Force() + | "<" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 < n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) + | _ -> recomposed.Force() + | "<=" -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + let eq = __CheckEqual e1'' e2'' + match eq with + | Some(true) -> TrueLiteral + | _ -> match e1'', e2'' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) + | _ -> recomposed.Force() + | ">" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) + | _ -> recomposed.Force() + | ">=" -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + let eq = __CheckEqual e1'' e2'' + match eq with + | Some(true) -> TrueLiteral + | _ -> match e1'', e2'' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) + | _ -> recomposed.Force() + | ".." -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + match e1'', e2'' with + | IntLiteral(lo), IntLiteral(hi) -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n))) + | _ -> recomposed.Force(); + | "in" -> + match e1'.Force(), e2'.Force() with + | _, SetExpr(s) + | _, SequenceExpr(s) -> BoolLiteral(Utils.ListContains (e1'.Force()) s) + | _ -> recomposed.Force() + | "!in" -> + match e1'.Force(), e2'.Force() with + | _, SetExpr(s) + | _, SequenceExpr(s) -> BoolLiteral(not (Utils.ListContains (e1'.Force()) s)) + | _ -> recomposed.Force() + | "+" -> + let e1'' = e1'.Force(); + let e2'' = e2'.Force(); + match e1'', e2'' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2) + | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | SetExpr(s), _ -> SetExpr(Set.add e2'' (Set.ofList s) |> Set.toList) + | _, SetExpr(s) -> SetExpr(Set.add e1'' (Set.ofList s) |> Set.toList) + | _ -> recomposed.Force() + | "-" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | _ -> recomposed.Force() + | "*" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2) + | _ -> recomposed.Force() + | "div" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2) + | _ -> recomposed.Force() + | "mod" -> + match e1'.Force(), e2'.Force() with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2) + | _ -> recomposed.Force() + | "&&" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(false) -> BoolLiteral(false) + | _ -> + match e1'.Force(), e2'.Force() with + | BoolLiteral(false), _ -> BoolLiteral(false) + | _, BoolLiteral(false) -> BoolLiteral(false) + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2) + | _ -> BinaryAnd (e1'.Force()) (e2'.Force()) + | "||" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(true) -> BoolLiteral(true) + | _ -> + match e1'.Force(), e2'.Force() with + | BoolLiteral(true), _ -> BoolLiteral(true) + | _, BoolLiteral(true) -> BoolLiteral(true) + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2) + | _ -> BinaryOr (e1'.Force()) (e2'.Force()) + | "==>" -> + // shortcircuit + match e1'.Force() with + | BoolLiteral(false) -> BoolLiteral(true) + | _ -> + let e1'' = e1'.Force() + let e2'' = e2'.Force() + BinaryImplies e1'' e2'' + | "<==>" -> + match e1'.Force(), e2'.Force() with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2) + | x, BoolLiteral(b) + | BoolLiteral(b), x -> if b then x else UnaryNot(x) + | _ -> recomposed.Force() + | _ -> recomposed.Force() + | UnaryExpr(op, e) -> + let e' = __EvalSym resolverFunc returnFunc ctx e + let recomposed = UnaryExpr(op, e') + match op with + | "!" -> + match e' with + | BoolLiteral(b) -> BoolLiteral(not b) + | _ -> recomposed + | "-" -> + match e' with + | IntLiteral(n) -> IntLiteral(-n) + | _ -> recomposed + | _ -> recomposed + | ForallExpr(vars, e) -> + let rec __ExhaustVar v restV vDomain = + match vDomain with + | vv :: restD -> + let ctx' = (v,vv) :: ctx + let e' = __EvalSym resolverFunc returnFunc ctx' (ForallExpr(restV, e)) + let erest = __ExhaustVar v restV restD + (* __EvalSym resolverFunc returnFunc ctx' *) + BinaryAnd e' erest + | [] -> BoolLiteral(true) + let rec __TraverseVars vars = + match vars with + | v :: restV -> + try + let vDom = GetVarDomain resolverFunc returnFunc ctx v e + __ExhaustVar v restV vDom + with + | ex -> ForallExpr([v], __TraverseVars restV) + | [] -> __EvalSym resolverFunc returnFunc ctx e + (* --- function body starts here --- *) + __TraverseVars vars + expr' |> returnFunc +and GetVarDomain resolverFunc returnFunc ctx var expr = match expr with | BinaryExpr(_, "==>", lhs, rhs) -> let conjs = SplitIntoConjunts lhs conjs |> List.fold (fun acc e -> match e with | BinaryExpr(_, "in", VarLiteral(vn), rhs) when GetVarName var = vn -> - match __EvalSym resolverFunc ctx rhs with + match __EvalSym resolverFunc returnFunc ctx rhs with | SetExpr(elist) | SequenceExpr(elist) -> elist |> List.append acc - | _ -> raise DomainNotInferred + | x -> raise DomainNotInferred | BinaryExpr(_, op, VarLiteral(vn),oth) | BinaryExpr(_, op, oth, VarLiteral(vn)) when GetVarName var = vn && Set.ofList ["<"; "<="; ">"; ">="] |> Set.contains op -> failwith "Not implemented yet" @@ -828,7 +827,10 @@ and GetVarDomain resolverFunc ctx var expr = raise DomainNotInferred let EvalSym resolverFunc expr = - __EvalSym resolverFunc [] expr + __EvalSym resolverFunc (fun e -> e) [] expr + +let EvalSymRet resolverFunc returnFunc expr = + __EvalSym resolverFunc returnFunc [] expr // ========================================================== /// Desugars a given expression so that all list constructors diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs index a6caaa6e..714c44f1 100644 --- a/Jennisys/Jennisys/CodeGen.fs +++ b/Jennisys/Jennisys/CodeGen.fs @@ -160,24 +160,8 @@ let PrintAllocNewObjects heapInst indent = let PrintVarAssignments heapInst indent = let idt = Indent indent - let fldAssgnsStr = heapInst.assignments |> PrintSep newline (fun asgn -> - let exprStr = - match asgn with - | FieldAssignment((o,f),e) -> - let fldName = GetVarName f - if fldName = "" then - PrintStmt (ExprStmt(e)) 0 false - else - PrintStmt (Assign(Dot(ObjLiteral(o.name), fldName), e)) 0 false - | ArbitraryStatement(stmt) -> - PrintStmt stmt 0 false - idt + exprStr) - let retValsAssgnsStr = heapInst.methodRetVals |> Map.toList - |> PrintSep newline (fun (retVarName, retVarVal) -> - let stmt = Assign(VarLiteral(retVarName), retVarVal) - let assgnStr = PrintStmt stmt 0 false - idt + assgnStr) - let str = [fldAssgnsStr; retValsAssgnsStr] |> List.filter (fun s -> not (s = "")) |> PrintSep newline (fun s -> s) + let stmts = ConvertToStatements heapInst + let str = stmts |> PrintSep (newline) (fun s -> idt + (PrintStmt s 0 false)) str + newline /// diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs index 65fd97d2..ffd30fc7 100644 --- a/Jennisys/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/Jennisys/DafnyModelUtils.fs @@ -213,19 +213,16 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = __ReadSeqIndex model rest (newEnv,newCtx) | _ -> (envMap,ctx) - //TODO: This has become obsolete now, as the Seq#Build function has a different meaning now. - // On the plus site, it might be that it is not necessary to read the model for this function anymore. // 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 lstElemVal = UnboxIfNeeded model ft.Args.[1] let dstLstLoc = GetLoc ft.Result - let oldLst = FindSeqInEnv envMap srcLstLoc - let idx = GetInt ft.Args.[1] - let lstElemVal = UnboxIfNeeded model ft.Args.[2] + let oldLst = FindSeqInEnv envMap srcLstLoc let dstLst = FindSeqInEnv envMap dstLstLoc - let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst + let newLst = oldLst @ [lstElemVal] let newCtx = UpdateContext dstLst newLst ctx let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) __ReadSeqBuild model rest (newEnv,newCtx) @@ -241,7 +238,7 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = let oldLst1 = FindSeqInEnv envMap srcLst1Loc let oldLst2 = FindSeqInEnv envMap srcLst2Loc let dstLst = FindSeqInEnv envMap dstLstLoc - let newLst = List.append oldLst1 oldLst2 + let newLst = oldLst1 @ oldLst2 let newCtx = UpdateContext dstLst newLst ctx let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst)) __ReadSeqAppend model rest (newEnv,newCtx) @@ -249,11 +246,11 @@ let ReadSeq (model: Microsoft.Boogie.Model) (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_bld = model.MkFunc("Seq#Build", 2) 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) + |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps) |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps) diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index a3c92ab7..beac24f8 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - examples/Set.jen /genMod /genRepr /method:Set.Double + examples/List.jen /genMod /genRepr /method:Node.Get C:\boogie\Jennisys\Jennisys\ diff --git a/Jennisys/Jennisys/Logger.fs b/Jennisys/Jennisys/Logger.fs index d9df47a7..dbf762cd 100644 --- a/Jennisys/Jennisys/Logger.fs +++ b/Jennisys/Jennisys/Logger.fs @@ -16,7 +16,7 @@ let _WARN = 40 let _ERROR = 20 let _NONE = 0 -let logLevel = _DEBUG +let logLevel = _ALL let Log level msg = if logLevel >= level then diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs index f12e8dd0..14d4f31f 100644 --- a/Jennisys/Jennisys/MethodUnifier.fs +++ b/Jennisys/Jennisys/MethodUnifier.fs @@ -209,6 +209,7 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph = let hInst = { objs = Utils.MapSingleton obj.name obj; modifiableObjs = modObjs; assignments = body; + concreteValues = body; methodArgs = Map.empty; methodRetVals = Map.empty; globals = Map.empty } diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs index b196d4cb..3215786d 100644 --- a/Jennisys/Jennisys/Modularizer.fs +++ b/Jennisys/Jennisys/Modularizer.fs @@ -39,12 +39,12 @@ let rec MakeModular indent prog comp meth cond hInst callGraph = | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc | _ -> acc - let __GetDirectChildren = - let thisRhsExprs = hInst.assignments |> List.choose (function FieldAssignment((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None) + let __GetDirectModifiableChildren = + let thisRhsExprs = hInst.assignments |> List.choose (function FieldAssignment((obj,_),e) when obj.name = "this" && Set.contains obj hInst.modifiableObjs -> Some(e) | _ -> None) thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty |> Set.toList - let directChildren = lazy (__GetDirectChildren) + let directChildren = lazy (__GetDirectModifiableChildren) let __IsAbstractField ty var = let builder = CascadingBuilder<_>(false) diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs index d38fbf7b..bb546834 100644 --- a/Jennisys/Jennisys/Resolver.fs +++ b/Jennisys/Jennisys/Resolver.fs @@ -22,7 +22,8 @@ type AssignmentType = type HeapInstance = { objs: Map; modifiableObjs: Set; - assignments: AssignmentType list + assignments: AssignmentType list; + concreteValues: AssignmentType list; methodArgs: Map; methodRetVals: Map; globals: Map; @@ -30,6 +31,20 @@ type HeapInstance = { let NoObj = { name = ""; objType = NamedType("", []) } +let ConvertToStatements heapInst = + let stmtLst1 = heapInst.assignments |> List.map (fun asgn -> + match asgn with + | FieldAssignment((o,f),e) -> + let fldName = GetVarName f + if fldName = "" then + ExprStmt(e) + else + Assign(Dot(ObjLiteral(o.name), fldName), e) + | ArbitraryStatement(stmt) -> stmt) + let stmtLst2 = heapInst.methodRetVals |> Map.toList + |> List.map (fun (retVarName, retVarVal) -> Assign(VarLiteral(retVarName), retVarVal)) + stmtLst1 @ stmtLst2 + // resolving values exception ConstResolveFailed of string @@ -95,7 +110,23 @@ let Resolve hModel cst = /// Evaluates a given expression with respect to a given heap instance // ================================================================== let Eval heapInst resolveExprFunc expr = - let rec __EvalResolver expr fldNameOpt = + let rec __EvalResolver useConcrete resolveExprFunc expr fldNameOpt = + let rec __FurtherResolve expr = + match expr with + | SetExpr(elist) -> SetExpr(elist |> List.map __FurtherResolve) + | SequenceExpr(elist) -> SequenceExpr(elist |> List.map __FurtherResolve) + | VarLiteral(_) -> + try + __EvalResolver useConcrete resolveExprFunc expr None + with + | _ -> expr + | IdLiteral(id) when not (id = "this" || id = "null") -> + try + __EvalResolver useConcrete resolveExprFunc expr None + with + | _ -> expr + | _ -> expr + if not (resolveExprFunc expr) then match fldNameOpt with | None -> expr @@ -117,19 +148,32 @@ let Eval heapInst resolveExprFunc expr = let globalVal = heapInst.globals |> Map.tryFind id match globalVal with | Some(e) -> e - | None -> __EvalResolver ThisLiteral (Some(id)) + | None -> __EvalResolver useConcrete resolveExprFunc ThisLiteral (Some(id)) | _ -> raise (EvalFailed(sprintf "I'm not supposed to resolve %O" expr)) | Some(fldName) -> match expr with | ObjLiteral(objName) -> - let h2 = heapInst.assignments |> List.filter (function FieldAssignment((o, Var(varName,_)), v) -> o.name = objName && varName = fldName | _ -> false) + let asgs = if useConcrete then heapInst.concreteValues else heapInst.assignments + let h2 = asgs |> List.filter (function FieldAssignment((o, Var(varName,_)), v) -> o.name = objName && varName = fldName | _ -> false) match h2 with - | FieldAssignment((_,_),x) :: [] -> x + | FieldAssignment((_,_),x) :: [] -> __FurtherResolve x | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName)) | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName)) // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model??? | _ -> Dot(expr, fldName) (* --- function body starts here --- *) - EvalSym __EvalResolver expr + //EvalSym (__EvalResolver resolveExprFunc) expr + EvalSymRet (__EvalResolver false resolveExprFunc) + (fun expr -> + // TODO: infer type of expr and then re-execute only if its type is Bool + let e1 = EvalSym (__EvalResolver true (fun _ -> true)) expr + match e1 with + | BoolLiteral(b) -> + if b then + expr + else + FalseLiteral + | _ -> expr + ) expr // ===================================================================== /// Takes an unresolved model of the heap (HeapModel), resolves all @@ -174,6 +218,7 @@ let ResolveModel hModel meth = { objs = objs; modifiableObjs = modObjs; assignments = hmap; + concreteValues = hmap; methodArgs = argmap; methodRetVals = retvals; globals = Map.empty } @@ -201,4 +246,34 @@ let rec GetCallGraph solutions graph = ) Set.empty let graph' = graph |> Map.add (comp,m) callees GetCallGraph rest graph' - | [] -> graph \ No newline at end of file + | [] -> graph + +////////////////////////////// + +let Is1stLevelExpr heapInst expr = + DescendExpr2 (fun expr acc -> + if not acc then + false + else + match expr with + | Dot(discr, fldName) -> + let obj = Eval heapInst (fun _ -> true) discr + match obj with + | ObjLiteral(id) -> not (id = "this") + | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral" + | _ -> true + ) expr true + +let IsSolution1stLevelOnly heapInst = + let rec __IsSol1stLevel stmts = + match stmts with + | stmt :: rest -> + match stmt with + | Assign(_, e) + | ExprStmt(e) -> + let ok = Is1stLevelExpr heapInst e + ok && __IsSol1stLevel rest + | Block(stmts) -> __IsSol1stLevel (stmts @ rest) + | [] -> true + (* --- function body starts here --- *) + __IsSol1stLevel (ConvertToStatements heapInst) \ No newline at end of file diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen index bb36c2bb..7fa04fc4 100644 --- a/Jennisys/Jennisys/examples/List.jen +++ b/Jennisys/Jennisys/examples/List.jen @@ -46,6 +46,11 @@ class Node[T] { requires num >= 0 ensures num >= |list| ==> ret = null ensures num < |list| ==> ret != null && ret.list = list[num..] + + method Get(idx: int) returns (ret: T) + requires idx >= 0 && idx < |list| + requires idx != 0 && next != null + ensures ret = list[idx] } model Node[T] { diff --git a/Jennisys/Jennisys/tmp.out b/Jennisys/Jennisys/tmp.out deleted file mode 100644 index 9a51a8c8..00000000 --- a/Jennisys/Jennisys/tmp.out +++ /dev/null @@ -1,435 +0,0 @@ -// Jennisys, Copyright (c) 2011, Microsoft. - [*] Analyzing constructor - ------------------------------------------ - constructor Set.Empty() - ensures elems = {}; - ------------------------------------------ - - searching for an instance ... OK - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - - [*] Analyzing constructor - ------------------------------------------ - constructor Set.Singleton(t: int) - ensures elems = {t}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification t <--> -463 - - adding unification {t} <--> {-463} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Init(x: int) - ensures elems = {x}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification x <--> -100 - - adding unification {x} <--> {-100} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - - [*] Analyzing constructor - ------------------------------------------ - constructor Set.Sum(p: int, q: int) - ensures elems = {p + q}; - ------------------------------------------ - - substitution method found: - constructor Set.Singleton(t: int) - ensures elems = {t}; - Unifications: - t -> p + q - - [*] Analyzing constructor - ------------------------------------------ - constructor Set.Double(p: int, q: int) - requires p != q; - ensures elems = {p q}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification q <--> -760 - - adding unification p <--> -463 - - adding unification p != q <--> true - - adding unification {p, q} <--> {-760, -463} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Double(p: int, q: int) - requires p != q; - ensures elems = {p q}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification q <--> 215 - - adding unification p <--> -249 - - adding unification p != q <--> true - - adding unification {p, q} <--> {-249, 215} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: q > p - - delegating to method calls ... - - verifying partial solution ... VERIFIED - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Double(p: int, q: int) - requires p != q; - requires !(q > p); - ensures elems = {p q}; - ------------------------------------------ - - substitution method found: - constructor SetNode.DoubleBase(x: int, y: int) - requires x > y; - ensures elems = {x y}; - Unifications: - y -> q - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.DoubleBase(x: int, y: int) - requires x > y; - ensures elems = {x y}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification y <--> 743 - - adding unification x <--> 744 - - adding unification x > y <--> true - - adding unification {x, y} <--> {743, 744} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - - - - - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> -224 - - adding unification y <--> -225 - - adding unification x <--> -452 - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification {x, y, z} <--> {-452, -225, -224} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: x < y && z > y - - delegating to method calls ... - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> z - - verifying partial solution ... VERIFIED - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> z - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - requires !(x < y && z > y); - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> -484 - - adding unification y <--> 123 - - adding unification x <--> 122 - - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification !(x < y && z > y) <--> true - - adding unification x < y && z > y <--> false - - adding unification x < y <--> true - - adding unification z > y <--> false - - adding unification {x, y, z} <--> {-484, 122, 123} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: z < x && y > x - - delegating to method calls ... - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> y - - verifying partial solution ... VERIFIED - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> y - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - requires !(x < y && z > y); - requires !(z < x && y > x); - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> -853 - - adding unification y <--> -852 - - adding unification x <--> -854 - - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true - - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification !(x < y && z > y) <--> true - - adding unification x < y && z > y <--> false - - adding unification x < y <--> true - - adding unification z > y <--> false - - adding unification !(z < x && y > x) <--> true - - adding unification z < x && y > x <--> false - - adding unification z < x <--> false - - adding unification y > x <--> true - - adding unification {x, y, z} <--> {-854, -853, -852} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: x < z && y > z - - delegating to method calls ... - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> y - - verifying partial solution ... VERIFIED - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> y - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - requires !(x < y && z > y); - requires !(z < x && y > x); - requires !(x < z && y > z); - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> -303 - - adding unification y <--> -155 - - adding unification x <--> -154 - - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true - - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true - - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification !(x < y && z > y) <--> true - - adding unification x < y && z > y <--> false - - adding unification x < y <--> false - - adding unification z > y <--> false - - adding unification !(z < x && y > x) <--> true - - adding unification z < x && y > x <--> false - - adding unification z < x <--> true - - adding unification y > x <--> false - - adding unification !(x < z && y > z) <--> true - - adding unification x < z && y > z <--> false - - adding unification x < z <--> false - - adding unification y > z <--> true - - adding unification {x, y, z} <--> {-303, -155, -154} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: z < y && x > y - - delegating to method calls ... - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> x - - verifying partial solution ... VERIFIED - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> x - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - requires !(x < y && z > y); - requires !(z < x && y > x); - requires !(x < z && y > z); - requires !(z < y && x > y); - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> -226 - - adding unification y <--> -227 - - adding unification x <--> -225 - - adding unification ((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y) <--> true - - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true - - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true - - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification !(x < y && z > y) <--> true - - adding unification x < y && z > y <--> false - - adding unification x < y <--> false - - adding unification z > y <--> true - - adding unification !(z < x && y > x) <--> true - - adding unification z < x && y > x <--> false - - adding unification z < x <--> true - - adding unification y > x <--> false - - adding unification !(x < z && y > z) <--> true - - adding unification x < z && y > z <--> false - - adding unification x < z <--> false - - adding unification y > z <--> false - - adding unification !(z < y && x > y) <--> true - - adding unification z < y && x > y <--> false - - adding unification z < y <--> false - - adding unification x > y <--> true - - adding unification {x, y, z} <--> {-227, -226, -225} - - delegating to method calls ... - - verifying synthesized solution ... - !!! NOT VERIFIED !!! - Strengthening the pre-condition - - candidate pre-condition: y < z && x > z - - delegating to method calls ... - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> x - - verifying partial solution ... VERIFIED - - substitution method found: - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - Unifications: - z -> x - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.Triple(x: int, y: int, z: int) - requires x != y; - requires y != z; - requires z != x; - requires !(x < y && z > y); - requires !(z < x && y > x); - requires !(x < z && y > z); - requires !(z < y && x > y); - requires !(y < z && x > z); - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> 123 - - adding unification y <--> -203 - - adding unification x <--> 122 - - adding unification (((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y)) && !(y < z && x > z) <--> true - - adding unification ((((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z)) && !(z < y && x > y) <--> true - - adding unification (((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x)) && !(x < z && y > z) <--> true - - adding unification ((x != y && (y != z && z != x)) && !(x < y && z > y)) && !(z < x && y > x) <--> true - - adding unification (x != y && (y != z && z != x)) && !(x < y && z > y) <--> true - - adding unification x != y && (y != z && z != x) <--> true - - adding unification x != y <--> true - - adding unification y != z && z != x <--> true - - adding unification y != z <--> true - - adding unification z != x <--> true - - adding unification !(x < y && z > y) <--> true - - adding unification x < y && z > y <--> false - - adding unification x < y <--> false - - adding unification z > y <--> true - - adding unification !(z < x && y > x) <--> true - - adding unification z < x && y > x <--> false - - adding unification z < x <--> false - - adding unification y > x <--> false - - adding unification !(x < z && y > z) <--> true - - adding unification x < z && y > z <--> false - - adding unification x < z <--> true - - adding unification y > z <--> false - - adding unification !(z < y && x > y) <--> true - - adding unification z < y && x > y <--> false - - adding unification z < y <--> false - - adding unification x > y <--> true - - adding unification !(y < z && x > z) <--> true - - adding unification y < z && x > z <--> false - - adding unification y < z <--> true - - adding unification x > z <--> false - - adding unification {x, y, z} <--> {-203, 122, 123} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - [*] Analyzing constructor - ------------------------------------------ - constructor SetNode.TripleBase(x: int, y: int, z: int) - requires x < y; - requires y < z; - ensures elems = {x y z}; - ------------------------------------------ - - searching for an instance ... OK - - adding unification z <--> 596 - - adding unification y <--> -384 - - adding unification x <--> -385 - - adding unification x < y && y < z <--> true - - adding unification x < y <--> true - - adding unification y < z <--> true - - adding unification {x, y, z} <--> {-385, -384, 596} - - delegating to method calls ... - - verifying synthesized solution ... - ~~~ VERIFIED ~~~ - - -Printing synthesized code -- cgit v1.2.3 From a1124a10dfb25608ea5a1dbb1a2f4102738c0342 Mon Sep 17 00:00:00 2001 From: Aleksandar Milicevic Date: Tue, 16 Aug 2011 18:17:37 -0700 Subject: Jennisys: - changed the way candidate conditions are discovered; now it simply uses all sub-expressions found in the spec that evaluate to TrueLiteral - changed the implementation so that when trying to infer a precondition, try out several different possibilities (and see which one works) - added some very basic (and incomplete) type inference - fixed a bug in the Modularizer (it didn't fix the solution after trying out the spec infered from the solution) - fixed a bug in DafnyModelUtils so that now when reading from the boogie model file it keeps getting information from Seq# functions until reaching a fixpoint (that's needed because the order or reads is important) --- Jennisys/Jennisys/Analyzer.fs | 327 ++++++++++++++++++++++------------- Jennisys/Jennisys/AstUtils.fs | 16 +- Jennisys/Jennisys/CodeGen.fs | 2 +- Jennisys/Jennisys/DafnyModelUtils.fs | 22 ++- Jennisys/Jennisys/Jennisys.fsproj | 2 +- Jennisys/Jennisys/Modularizer.fs | 2 +- Jennisys/Jennisys/Options.fs | 27 +-- Jennisys/Jennisys/Resolver.fs | 64 ++++--- Jennisys/Jennisys/TypeChecker.fs | 22 ++- Jennisys/Jennisys/Utils.fs | 13 ++ Jennisys/Jennisys/examples/List.jen | 3 +- 11 files changed, 324 insertions(+), 176 deletions(-) diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index 512a6870..7c8c472d 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -8,6 +8,7 @@ open MethodUnifier open Modularizer open PipelineUtils open Options +open TypeChecker open Resolver open PrintUtils open DafnyPrinter @@ -76,8 +77,9 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp = | [] -> "" // ========================================================================= -/// For a given constant "o" (which is an object, something like "gensym32"), -/// finds a path of field references from "this". +/// For a given constant "objRefName" (which is an object, something like +/// "gensym32"), finds a path of field references from "this" (e.g. something +/// like "this.next.next"). /// /// Implements a backtracking search over the heap entries to find that /// path. It starts from the given object, and follows the backpointers @@ -140,7 +142,7 @@ let GetHeapExpr prog mthd heapInst = objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc ) prepostExpr -let IsUnmodConcrOnly (comp,meth) expr = +let IsUnmodConcrOnly prog (comp,meth) expr = let isConstr = IsConstructor meth let rec __IsUnmodOnly args expr = let __IsUnmodOnlyLst elist = @@ -155,13 +157,14 @@ let IsUnmodConcrOnly (comp,meth) expr = | VarLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) | IdLiteral("null") | IdLiteral("this") -> true | IdLiteral(id) -> - let isAbstractFld = GetAbstractFields comp |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) - not (isConstr || isAbstractFld) - | Dot(e, fldName) -> if isConstr then false else __IsUnmodOnlyLst [e] - // TODO: this is how it should really work - // let lhsType = InferType prog e - // let isMod = IsFieldModifiable lhsType fldName - // (not isMod) && __IsUnmodOnlyLst [e] + not (isConstr || IsAbstractField comp id) + | Dot(e, fldName) -> //if isConstr then false else __IsUnmodOnlyLst [e] + if isConstr then + false + else + // assume it is unmodifiable, because it is a method, so just check if it's concrete + let lhsType = InferType prog comp e |> Utils.ExtractOptionMsg (sprintf "Inference failed for %s" (PrintExpr 0 e)) + IsConcreteField lhsType fldName | AssertExpr(e) | AssumeExpr(e) | SeqLength(e) @@ -187,7 +190,7 @@ let AddUnif indent e v unifMap = } //TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const" -let rec GetUnifications indent (comp,meth) heapInst unifs expr = +let rec GetUnifications prog indent (comp,meth) heapInst unifs expr = let idt = Indent indent // - first looks if the give expression talks only about method arguments (args) // - then it tries to evaluate it to a constant @@ -198,7 +201,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr = else let builder = new CascadingBuilder<_>(unifsAcc) builder { - let! argsOnly = IsUnmodConcrOnly (comp,meth) e |> Utils.BoolToOption + let! argsOnly = IsUnmodConcrOnly prog (comp,meth) e |> Utils.BoolToOption let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None return AddUnif indent e v unifsAcc } @@ -209,7 +212,7 @@ let rec GetUnifications indent (comp,meth) heapInst unifs expr = /// Returns a map (Expr |--> Const) containing unifications /// found for the given method and heap/env/ctx // ======================================================= -let GetUnificationsForMethod indent comp m heapInst = +let GetUnificationsForMethod indent prog comp m heapInst = let idt = Indent indent let rec GetArgValueUnifications args = match args with @@ -219,26 +222,34 @@ let GetUnificationsForMethod indent comp m heapInst = GetArgValueUnifications rest |> AddUnif indent (VarLiteral(name)) c | None -> failwith ("couldn't find value for argument " + name) | [] -> Map.empty - let rec GetFldValueUnifications fldNames unifs = - match fldNames with - | fldName :: rest -> - heapInst.assignments |> List.fold (fun acc asgn -> - match asgn with - | FieldAssignment((obj,Var(vname,_)), fldVal) when obj.name = "this" && vname = fldName -> - try - let c = Expr2Const fldVal - AddUnif indent (IdLiteral(fldName)) c acc - with - | _ -> acc - | _ -> acc - ) unifs - |> GetFldValueUnifications rest - | [] -> unifs + let rec GetFldValueUnifications unifs = + heapInst.assignments |> List.fold (fun acc asgn -> + match asgn with + | FieldAssignment((obj,Var(vname,_)), fldVal) -> + try + let comp = obj.objType |> FindComponentForType prog |> Utils.ExtractOption + if IsConcreteField comp vname then + let path = GetObjRefExpr obj.name heapInst |> Utils.ExtractOption + let c = Expr2Const fldVal + AddUnif indent (Dot(path, vname)) c acc + else + acc + with + | ex -> + Logger.WarnLine ("[WARN]: error during getting field value unifications: " + ex.Message) + acc + | _ -> acc + ) unifs + (* --- function body starts here --- *) let unifs = GetArgValueUnifications (GetMethodInArgs m) - let fldNames = if IsConstructor m then [] else GetConcreteFields comp |> List.map (function Var(name,_) -> name) - let unifs2 = GetFldValueUnifications fldNames unifs - GetUnifications indent (comp,m) heapInst unifs2 (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x)) + let unifs = + //TODO: it should really read the "modifies" clause and figure out modifiable fields from there + if not (IsConstructor m) then + GetFldValueUnifications unifs + else + unifs + GetUnifications prog indent (comp,m) heapInst unifs (GetMethodPrePost m |> fun x -> BinaryAnd (fst x) (snd x)) // ======================================================= /// Applies given unifications onto the given heap/env/ctx @@ -310,7 +321,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative = let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative let newHeap = heapInst.assignments|> List.fold (fun acc asgn -> match asgn with - | FieldAssignment((o,f),value) -> + | FieldAssignment((o,f),value) when heapInst.modifiableObjs |> Set.contains o -> let e2 = __Apply (o,f) c e value acc @ [FieldAssignment((o,f),e2)] | _ -> acc @ [asgn] @@ -343,25 +354,57 @@ let rec DiscoverAliasing exprList heapInst = BinaryAnd eqExpr (DiscoverAliasing rest heapInst) | [] -> TrueLiteral -// use the orginal method, not the one with an extra precondition -let FixSolution origComp origMeth sol = - sol |> Map.fold (fun acc (cc,mm) v -> - if CheckSameMethods (cc,mm) (origComp,origMeth) then - acc |> Map.add (origComp,origMeth) v - else - acc |> Map.add (cc,mm) v) Map.empty - // let DontResolveUnmodifiableStuff prog comp meth expr = let methodArgs = GetMethodInArgs meth let __IsMethodArg argName = methodArgs |> List.exists (fun (Var(vname,_)) -> vname = argName) - let isConstr = match meth with Method(_,_,_,_,b) -> b | _ -> false + let isConstr = IsConstructor meth match expr with | VarLiteral(id) when __IsMethodArg id -> false - | IdLiteral(id) when not (id = "this" || id = "null") -> isConstr - | Dot(lhs, fldName) -> isConstr + | IdLiteral(id) when id = "this" || id = "null" -> true + | IdLiteral(id) | Dot(_, id) -> + // this must be a field, so resolve it only if constructor + isConstr | _ -> true +/// Descends down a given expression and returns all sub-expressions that evaluate to TrueLiteral +let FindTrueClauses prog comp m heapInst expr = + let MyFun expr acc = + try + let exprEval = Eval heapInst (DontResolveUnmodifiableStuff prog comp m) expr + if exprEval = TrueLiteral then + acc + else + let exprAllResolved = Eval heapInst (fun _ -> true) expr + match exprAllResolved with + | BoolLiteral(true) -> acc @ [exprEval] + | _ -> acc + with + | _ -> acc + (* --- function body starts here --- *) + DescendExpr2 MyFun expr [] + +/// Returns a list of boolean expressions obtained by combining (in some way) +/// the two given list of conditions conditions +let GetAllPossibleConditions specConds argConds aliasingConds = + let __Conjoin lst = lst |> List.fold (fun acc e -> BinaryAnd acc e) TrueLiteral + let __Preproc lst = lst |> List.map SplitIntoConjunts |> List.concat |> Utils.ListDeduplicate + + // 0. aliasing conditions + // 1. conjunction of spec conditions + // 2. individual arg conditions + // 3. conjunction of arg conditions + // 4. individual spec conditions + let aliasing = aliasingConds |> __Preproc + let specIndi = specConds |> __Preproc + let specConj = [__Conjoin specIndi] + let argsIndi = argConds |> __Preproc + let argsConj = [__Conjoin argsIndi] + + let allConds = aliasing @ specConj @ argsIndi @ specIndi @ argsConj + allConds |> List.filter (fun e -> not (e = TrueLiteral)) + |> Utils.ListDeduplicate + // ============================================================================ /// Attempts to synthesize the initialization code for the given constructor "m" /// @@ -394,7 +437,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph = let model = models.[0] let hModel = ReadFieldValuesFromModel model prog comp m let heapInst = ResolveModel hModel m - let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList + let unifs = GetUnificationsForMethod indent prog comp m heapInst |> Map.toList let heapInst = ApplyUnifications indent prog comp m unifs heapInst true // split into method calls @@ -415,99 +458,137 @@ let rec AnalyzeConstructor indent prog comp m callGraph = else sol else - sol + sol and TryInferConditionals indent prog comp m unifs heapInst callGraph = + let rec __TryOutConditions candidateConditions = + let idt = Indent indent + match candidateConditions with + | [] -> + Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) + None + | candCond :: rest -> + Logger.InfoLine (sprintf "%s ________________________" idt) + Logger.InfoLine (sprintf "%s candidate pre-condition: %s" idt (PrintExpr 0 candCond)) + Logger.InfoLine (sprintf "%s ------------------------" idt) + let idt = idt + " " + let _,_,m2 = AddPrecondition prog comp m candCond + let sol = MakeModular (indent+2) prog comp m2 candCond heapInst callGraph + Logger.Info (idt + " - verifying partial solution ... ") + let verified = + if Options.CONFIG.verifyPartialSolutions then + VerifySolution prog sol Options.CONFIG.genRepr + else + true + if verified then + if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" + Some(candCond,m2,sol) + else + Logger.InfoLine "NOT VERIFIED" + __TryOutConditions rest + + (* --- function body starts here --- *) let idt = Indent indent let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst] let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false let methodArgs = GetMethodInArgs m - let expr = GetHeapExpr prog m heapInst2 - // now evaluate and see what's left - //printfn "%s" (expr |> SplitIntoConjunts |> PrintSep (newline + newline) (fun e -> PrintExpr 0 e)) - let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2) - let newConds = expr |> SplitIntoConjunts - |> List.fold (fun acc e -> - Logger.TraceLine (idt + ">>> " + (PrintExpr 0 e)) - let v = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) e - Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 v)) - if v = TrueLiteral then - acc - elif v = FalseLiteral && (not aliasingCond.IsValueCreated) then - let aliasingExpr = aliasingCond.Force() - if aliasingExpr = TrueLiteral then - failwith ("post-condition evaluated to false and no aliasing was discovered") - acc @ [aliasingExpr] - else - acc @ [v] - ) [] - |> List.filter (IsUnmodConcrOnly (comp,m)) - let newConds = - if newConds = [] && IsSolution1stLevelOnly heapInst2 then - heapInst2.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) [] - else - newConds - - // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr - match newConds with - | [] -> - Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) - wrongSol - | _ -> - //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO - let candCond = newConds |> List.fold BinaryAnd TrueLiteral - Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 candCond)) - let _,_,m2 = AddPrecondition prog comp m candCond - let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph - Logger.Info (idt + " - verifying partial solution ... ") - let verified = - if Options.CONFIG.verifyPartialSolutions then - VerifySolution prog sol Options.CONFIG.genRepr - else - true - if verified then - if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" + // find candidate conditions + let expr = GetHeapExpr prog m heapInst2 + let specConds = expr |> FindTrueClauses prog comp m heapInst2 + let specConds = specConds + |> List.filter (IsUnmodConcrOnly prog (comp,m)) + + let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2) + let argConds = heapInst2.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) [] + let allConds = GetAllPossibleConditions specConds argConds [aliasingCond.Force()] + + // --- trace + let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 e)) + allConds |> List.iter loggerFunc + // --- + + if IsSolution1stLevelOnly heapInst2 then + // try to find a non-recursive solution + match __TryOutConditions allConds with + | Some(candCond,m2,sol) -> let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with | Some(sol2) -> sol2 | None -> sol let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond)) let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph MergeSolutions solThis solRest |> FixSolution comp m - else - Logger.InfoLine "NOT VERIFIED" - wrongSol - -let GetMethodsToAnalyze prog = - let mOpt = Options.CONFIG.methodToSynth; - if mOpt = "*" then - (* all *) - FilterMembers prog FilterMethodMembers // FilterConstructorMembers - elif mOpt = "paramsOnly" then - (* only with parameters *) - FilterMembers prog FilterConstructorMembersWithParams + | None -> + Logger.InfoLine (idt + "!!! Giving up !!!") + wrongSol + + // let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr +// match newConds with +// | [] -> +// Logger.InfoLine (sprintf "%s - no more interesting pre-conditions" idt) +// wrongSol +// | _ -> +// //if not (rest = []) then Logger.WarnLine ("[WARN] NOT IMPLEMENTED YET: more than candidate condition ") //TODO +// let candCond = newConds |> List.fold BinaryAnd TrueLiteral //TODO: do some search or something +// Logger.InfoLine (sprintf "%s - candidate pre-condition: %s" idt (PrintExpr 0 candCond)) +// let _,_,m2 = AddPrecondition prog comp m candCond +// let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph +// Logger.Info (idt + " - verifying partial solution ... ") +// let verified = +// if Options.CONFIG.verifyPartialSolutions then +// VerifySolution prog sol Options.CONFIG.genRepr +// else +// true +// if verified then +// if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED" +// let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with +// | Some(sol2) -> sol2 +// | None -> sol +// let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond)) +// let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph +// MergeSolutions solThis solRest |> FixSolution comp m +// else +// Logger.InfoLine "NOT VERIFIED" +// wrongSol else - let allMethods,neg = - if mOpt.StartsWith("~") then - mOpt.Substring(1), true - else - mOpt, false - (* exact list *) - let methods = allMethods.Split([|','|]) - let lst = methods |> Array.fold (fun acc m -> - let idx = m.LastIndexOf(".") - if idx = -1 || idx = m.Length - 1 then - raise (InvalidCmdLineArg("Invalid method full name: " + m)) - let compName = m.Substring(0, idx) - let methName = m.Substring(idx + 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)) + // the solution is not immediate, so try to delegate to a method call, possibly to a recursive one + //TODO + Logger.InfoLine "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%" + wrongSol + +let GetMethodsToAnalyze prog = + let __ReadMethodsParam = + let mOpt = Options.CONFIG.methodToSynth; + if mOpt = "*" then + (* all *) + FilterMembers prog FilterMethodMembers else - lst - + let allMethods,neg = + if mOpt.StartsWith("~") then + mOpt.Substring(1), true + else + mOpt, false + (* exact list *) + let methods = allMethods.Split([|','|]) + let lst = methods |> Array.fold (fun acc m -> + let idx = m.LastIndexOf(".") + if idx = -1 || idx = m.Length - 1 then + raise (InvalidCmdLineArg("Invalid method full name: " + m)) + let compName = m.Substring(0, idx) + let methName = m.Substring(idx + 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 FilterMethodMembers |> List.filter (fun e -> not (Utils.ListContains e lst)) + else + lst + (* --- function body starts here --- *) + let meths = __ReadMethodsParam + if Options.CONFIG.constructorsOnly then + meths |> List.filter (fun (c,m) -> IsConstructor m) + else + meths // ============================================================================ /// Goes through a given list of methods of the given program and attempts to diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs index f5d90489..b4ed22e6 100644 --- a/Jennisys/Jennisys/AstUtils.fs +++ b/Jennisys/Jennisys/AstUtils.fs @@ -147,8 +147,11 @@ let rec DescendExpr2 visitorFunc expr acc = | SequenceExpr(exs) | SetExpr(exs) -> __Pipe exs -let PrintGenSym name = - sprintf "gensym%s" name +let PrintGenSym (name: string) = + if name.StartsWith("gensym") then + name + else + sprintf "gensym%s" name // ===================== /// Returns TRUE literal @@ -267,9 +270,10 @@ let rec Expr2Const e = match e with | IntLiteral(n) -> IntConst(n) | BoolLiteral(b) -> BoolConst(b) + | BoxLiteral(id) -> BoxConst(id) | ObjLiteral("this") -> ThisConst("this",None) | ObjLiteral("null") -> NullConst - | ObjLiteral(name) -> Unresolved(name) + | ObjLiteral(name) -> NewObj(name, None) | IdLiteral(id) -> Unresolved(id) | VarLiteral(id) -> VarConst(id) | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const) @@ -359,6 +363,9 @@ let rec GroupFieldsByType fields = let fldSet = Map.tryFind ty map |> Utils.ExtractOptionOr Set.empty map |> Map.add ty (fldSet |> Set.add (Var(name, ty))) | [] -> Map.empty + +let IsConcreteField comp fldName = GetConcreteFields comp |> List.exists (function Var(name,_) -> name = fldName) +let IsAbstractField comp fldName = GetAbstractFields comp |> List.exists (function Var(name,_) -> name = fldName) // ================================= /// Returns class name of a component @@ -476,6 +483,9 @@ let FindComponent (prog: Program) clsName = | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false) |> Utils.ListToOption +let FindComponentForType prog ty = + FindComponent prog (GetTypeShortName ty) + // =================================================== /// Finds a method of a component that has a given name // =================================================== diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs index 714c44f1..10398fa9 100644 --- a/Jennisys/Jennisys/CodeGen.fs +++ b/Jennisys/Jennisys/CodeGen.fs @@ -160,7 +160,7 @@ let PrintAllocNewObjects heapInst indent = let PrintVarAssignments heapInst indent = let idt = Indent indent - let stmts = ConvertToStatements heapInst + let stmts = ConvertToStatements heapInst true let str = stmts |> PrintSep (newline) (fun s -> idt + (PrintStmt s 0 false)) str + newline diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs index ffd30fc7..6a8cb727 100644 --- a/Jennisys/Jennisys/DafnyModelUtils.fs +++ b/Jennisys/Jennisys/DafnyModelUtils.fs @@ -244,14 +244,24 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) = __ReadSeqAppend model rest (newEnv,newCtx) | _ -> (envMap,ctx) + // keeps reading from Seq#Build and Seq#Append until fixpoint + let rec __ReadUntilFixpoint hmodel = + let f_seq_bld = model.MkFunc("Seq#Build", 2) + let f_seq_app = model.MkFunc("Seq#Append", 2) + let hmodel' = hmodel |> __ReadSeqBuild model (List.ofSeq f_seq_bld.Apps) + |> __ReadSeqAppend model (List.ofSeq f_seq_app.Apps) + if hmodel' = hmodel then + hmodel' + else + __ReadUntilFixpoint hmodel' + 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", 2) - 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) + let hmodel = (envMap,ctx) + let hmodel' = hmodel |> __ReadSeqLen model (List.ofSeq f_seq_len.Apps) + |> __ReadSeqIndex model (List.ofSeq f_seq_idx.Apps) + __ReadUntilFixpoint hmodel' + // ===================================================== diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index beac24f8..2613432c 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -23,7 +23,7 @@ 3 x86 bin\Debug\Language.XML - examples/List.jen /genMod /genRepr /method:Node.Get + examples/NumberMethods.jen /genMod /genRepr /method:NumberMethods.Min4 C:\boogie\Jennisys\Jennisys\ diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs index 3215786d..c6fcaaec 100644 --- a/Jennisys/Jennisys/Modularizer.fs +++ b/Jennisys/Jennisys/Modularizer.fs @@ -184,7 +184,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph = | Method (mname, msig, mpre, _, isConstr) -> Method(mname, msig, mpre, postSpec, isConstr) | _ -> failwithf "internal error: expected a Method but got %O" meth match TryFindExistingAndConvertToSolution indent comp meth' cond callGraph with - | Some(sol) -> sol + | Some(sol) -> sol |> FixSolution comp meth | None -> // if not found, try to split into parts let newMthdLst, newHeapInst = __GetModularBranch diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs index b61c16da..7aeb131a 100644 --- a/Jennisys/Jennisys/Options.fs +++ b/Jennisys/Jennisys/Options.fs @@ -9,18 +9,19 @@ module Options open Utils type Config = { - help: bool; - inputFilename: string; - methodToSynth: string; - inferConditionals: bool; - verifyPartialSolutions: bool; - verifySolutions: bool; - checkUnifications: bool; - genRepr: bool; - genMod: bool; - timeout: int; - numLoopUnrolls: int; - recursiveValid: bool; + help : bool; + inputFilename : string; + methodToSynth : string; + constructorsOnly : bool; + inferConditionals : bool; + verifyPartialSolutions : bool; + verifySolutions : bool; + checkUnifications : bool; + genRepr : bool; + genMod : bool; + timeout : int; + numLoopUnrolls : int; + recursiveValid : bool; } type CfgOption<'a> = { @@ -54,6 +55,7 @@ let CheckBool value optName = let cfgOptions = [ { optionName = "help"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with help = CheckBool v "help"}); descr = "description not available"; } { optionName = "method"; optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth = CheckNonEmpty v "method"}); descr = "description not available"; } + { optionName = "constrOnly"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly = CheckBool v "constrOnly"}); descr = "description not available"; } { optionName = "inferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = CheckBool v "inferConds"}); descr = "description not available"; } { optionName = "noInferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = not (CheckBool v "inferConds")}); descr = "description not available"; } { optionName = "verifyParSol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = CheckBool v "verifyParSol"}); descr = "description not available"; } @@ -98,6 +100,7 @@ let defaultConfig: Config = { inputFilename = ""; inferConditionals = true; methodToSynth = "*"; + constructorsOnly = false; verifyPartialSolutions = true; verifySolutions = true; checkUnifications = false; diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs index bb546834..711298f9 100644 --- a/Jennisys/Jennisys/Resolver.fs +++ b/Jennisys/Jennisys/Resolver.fs @@ -31,20 +31,29 @@ type HeapInstance = { let NoObj = { name = ""; objType = NamedType("", []) } -let ConvertToStatements heapInst = - let stmtLst1 = heapInst.assignments |> List.map (fun asgn -> - match asgn with - | FieldAssignment((o,f),e) -> - let fldName = GetVarName f - if fldName = "" then - ExprStmt(e) - else - Assign(Dot(ObjLiteral(o.name), fldName), e) - | ArbitraryStatement(stmt) -> stmt) +// use the orginal method, not the one with an extra precondition +let FixSolution origComp origMeth sol = + sol |> Map.fold (fun acc (cc,mm) v -> + if CheckSameMethods (cc,mm) (origComp,origMeth) then + acc |> Map.add (origComp,origMeth) v + else + acc |> Map.add (cc,mm) v) Map.empty + +let ConvertToStatements heapInst onModifiableObjsOnly = + let stmtLst1 = heapInst.assignments |> List.choose (fun asgn -> + match asgn with + | FieldAssignment((o,f),e) when (not onModifiableObjsOnly || Set.contains o heapInst.modifiableObjs) -> + let fldName = GetVarName f + if fldName = "" then + Some(ExprStmt(e)) + else + Some(Assign(Dot(ObjLiteral(o.name), fldName), e)) + | ArbitraryStatement(stmt) -> Some(stmt) + | _ -> None) let stmtLst2 = heapInst.methodRetVals |> Map.toList |> List.map (fun (retVarName, retVarVal) -> Assign(VarLiteral(retVarName), retVarVal)) stmtLst1 @ stmtLst2 - + // resolving values exception ConstResolveFailed of string @@ -73,11 +82,12 @@ let rec ResolveCont hModel failResolver cst = | Some(c) -> c | _ -> failResolver cst hModel | None -> - // finally, see if it's a method argument - let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList - match m with - | (vc,_) :: [] -> vc - | _ -> failResolver cst hModel + failResolver cst hModel +// // finally, see if it's an *input* (have no way of telling input from output params here) method argument +// let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList +// match m with +// | (vc,_) :: [] -> vc +// | _ -> failResolver cst hModel | SeqConst(cseq) -> let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) [] SeqConst(resolvedLst) @@ -127,10 +137,12 @@ let Eval heapInst resolveExprFunc expr = | _ -> expr | _ -> expr - if not (resolveExprFunc expr) then - match fldNameOpt with - | None -> expr - | Some(n) -> Dot(expr, n) + (* --- function body starts here --- *) + let ex = match fldNameOpt with + | None -> expr + | Some(n) -> Dot(expr, n) + if not (resolveExprFunc ex) then + ex else match fldNameOpt with | None -> @@ -142,7 +154,7 @@ let Eval heapInst resolveExprFunc expr = | Some(argValue) -> argValue |> Const2Expr | None -> match heapInst.methodRetVals |> Map.tryFind id with - | Some(e) -> e + | Some(e) -> e |> __FurtherResolve | None -> raise (EvalFailed("cannot find value for method parameter " + id)) | IdLiteral(id) -> let globalVal = heapInst.globals |> Map.tryFind id @@ -160,6 +172,7 @@ let Eval heapInst resolveExprFunc expr = | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName)) | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName)) // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model??? | _ -> Dot(expr, fldName) + (* --- function body starts here --- *) //EvalSym (__EvalResolver resolveExprFunc) expr EvalSymRet (__EvalResolver false resolveExprFunc) @@ -209,10 +222,11 @@ let ResolveModel hModel meth = let argmap, retvals = hModel.env |> Map.fold (fun (acc1,acc2) k v -> match k with | VarConst(name) -> + let resolvedValExpr = Resolve hModel v if outArgs |> List.exists (function Var(varName, _) -> varName = name) then - acc1, acc2 |> Map.add name (Resolve hModel v |> Const2Expr) + acc1, acc2 |> Map.add name (resolvedValExpr |> Const2Expr) else - acc1 |> Map.add name (Resolve hModel v), acc2 + acc1 |> Map.add name resolvedValExpr, acc2 | _ -> acc1, acc2 ) (Map.empty, Map.empty) { objs = objs; @@ -259,7 +273,7 @@ let Is1stLevelExpr heapInst expr = | Dot(discr, fldName) -> let obj = Eval heapInst (fun _ -> true) discr match obj with - | ObjLiteral(id) -> not (id = "this") + | ObjLiteral(id) -> id = "this" | _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral" | _ -> true ) expr true @@ -276,4 +290,4 @@ let IsSolution1stLevelOnly heapInst = | Block(stmts) -> __IsSol1stLevel (stmts @ rest) | [] -> true (* --- function body starts here --- *) - __IsSol1stLevel (ConvertToStatements heapInst) \ No newline at end of file + __IsSol1stLevel (ConvertToStatements heapInst true) \ No newline at end of file diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs index 8227b693..bc696f43 100644 --- a/Jennisys/Jennisys/TypeChecker.fs +++ b/Jennisys/Jennisys/TypeChecker.fs @@ -1,6 +1,7 @@ module TypeChecker open Ast +open AstUtils open Printer open System.Collections.Generic @@ -39,5 +40,22 @@ let TypeCheck prog = Some(Program(clist)) // TODO: implement this -let InferType prog expr = - NamedType("unknown", []) \ No newline at end of file +let rec InferType prog thisComp expr = + let __FindVar comp fldName = + let var = FindVar comp fldName |> Utils.ExtractOption + match var with + | Var(_, tyOpt) -> + let c = FindComponentForType prog (Utils.ExtractOption tyOpt) |> Utils.ExtractOption + Some(c) + try + match expr with + | ObjLiteral("this") -> Some(thisComp) + | ObjLiteral("null") -> None + | IdLiteral(id) -> __FindVar thisComp id + | Dot(discr, fldName) -> + match InferType prog thisComp discr with + | Some(comp) -> __FindVar comp fldName + | None -> None + | _ -> None + with + | ex -> None \ No newline at end of file diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs index 156d427c..5cd8af9d 100644 --- a/Jennisys/Jennisys/Utils.fs +++ b/Jennisys/Jennisys/Utils.fs @@ -74,6 +74,19 @@ let ListToOptionMsg lst errMsg = let ListToOption lst = ListToOptionMsg lst "given list contains more than one element" +let ListDeduplicate lst = + let rec __Dedup lst (visitedSet: System.Collections.Generic.HashSet<_>) acc = + match lst with + | fs :: rest -> + let newAcc = + if visitedSet.Add(fs) then + acc @ [fs] + else + acc + __Dedup rest visitedSet newAcc + | _ -> acc + __Dedup lst (new System.Collections.Generic.HashSet<_>()) [] + // ============================================================= /// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i]) // ============================================================= diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen index 7fa04fc4..e056bcfa 100644 --- a/Jennisys/Jennisys/examples/List.jen +++ b/Jennisys/Jennisys/examples/List.jen @@ -49,7 +49,6 @@ class Node[T] { method Get(idx: int) returns (ret: T) requires idx >= 0 && idx < |list| - requires idx != 0 && next != null ensures ret = list[idx] } @@ -61,6 +60,6 @@ model Node[T] { next invariant - next = null <==> list = [data] + next = null ==> list = [data] next != null ==> list = [data] + next.list } -- cgit v1.2.3 From 88aa33c40ee1cde79fc5b51ab2197da89eb1ddd7 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 17 Aug 2011 07:45:05 -0700 Subject: deleted lazyinlining option 2 and 3 fixed proc copy bounding --- Source/Core/CommandLineOptions.cs | 2 +- Source/Provers/SMTLib/Z3.cs | 5 - Source/Provers/Z3/Prover.cs | 6 -- Source/VCGeneration/VC.cs | 196 +++++++------------------------------- 4 files changed, 34 insertions(+), 175 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index c6b8e493..f0e325e8 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -353,7 +353,7 @@ namespace Microsoft.Boogie { public bool PrintInlined = false; public bool ExtractLoops = false; public int LazyInlining = 0; - public int ProcedureCopyBound = 1; + public int ProcedureCopyBound = 0; public int StratifiedInlining = 0; public int StratifiedInliningOption = 0; public bool UseUnsatCoreForInlining = false; diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index da9e8faa..9b90b12a 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -152,11 +152,6 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("TYPE_CHECK", "true"); options.AddWeakSmtOption("BV_REFLECT", "true"); - if (CommandLineOptions.Clo.LazyInlining == 2) { - options.AddWeakSmtOption("MACRO_EXPANSION", "true"); - options.AddWeakSmtOption("WARNING", "false"); - } - if (options.TimeLimit > 0) { options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString()); options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000); diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 640f98ae..8929e732 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -84,9 +84,6 @@ namespace Microsoft.Boogie.Z3 StringBuilder cmdLineArgsBldr = new StringBuilder(); AppendCmdLineOption(cmdLineArgsBldr, "si"); - if (CommandLineOptions.Clo.LazyInlining == 2) - AppendCmdLineOption(cmdLineArgsBldr, "nw"); - if (CommandLineOptions.Clo.z3AtFlag) AppendCmdLineOption(cmdLineArgsBldr, "@"); @@ -165,9 +162,6 @@ namespace Microsoft.Boogie.Z3 AddOption(result, "BV_REFLECT", "true"); } - if (CommandLineOptions.Clo.LazyInlining == 2) - AddOption(result, "MACRO_EXPANSION", "true"); - foreach (string opt in CommandLineOptions.Clo.Z3Options) { Contract.Assert(opt != null); int eq = opt.IndexOf("="); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 576ce080..51bdb033 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -27,7 +27,6 @@ namespace VC { [NotDelayed] public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile) : base(program) - // throws ProverException { Contract.Requires(program != null); this.appendLogFile = appendLogFile; @@ -36,10 +35,6 @@ namespace VC { if (CommandLineOptions.Clo.LazyInlining > 0) { this.GenerateVCsForLazyInlining(program); - if (CommandLineOptions.Clo.LazyInlining == 3) - { - CreateCopiesForLazyInlining(CommandLineOptions.Clo.ProcedureCopyBound, program); - } } } @@ -85,9 +80,9 @@ namespace VC { public Function function; public Variable controlFlowVariable; public List interfaceVars; + public List> interfaceVarCopies; public Expr assertExpr; public VCExpr vcexpr; - public VCExpr inside_vc; // (without the quantifiers) public List privateVars; public Dictionary incarnationOriginMap; public Hashtable /*Variable->Expr*/ exitIncarnationMap; @@ -163,6 +158,16 @@ namespace VC { Contract.Assert(returnVar != null); this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar); ctxt.DeclareFunction(this.function, ""); + + interfaceVarCopies = new List>(); + int temp = 0; + for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) { + interfaceVarCopies.Add(new List()); + foreach (Variable v in interfaceVars) { + interfaceVarCopies[i].Add( + new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type))); + } + } } } [ContractInvariantMethod] @@ -217,6 +222,25 @@ namespace VC { } Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs); proc.Ensures.Add(new Ensures(true, freePostExpr)); + + if (CommandLineOptions.Clo.ProcedureCopyBound > 0) { + Expr ret = new LiteralExpr(Token.NoToken, false); + for (int k = 0; k < CommandLineOptions.Clo.ProcedureCopyBound; k++) { + var iv = info.interfaceVarCopies[k]; + Contract.Assert(info.function.InParams.Length == iv.Count); + + Expr conj = new LiteralExpr(Token.NoToken, true); + for (int i = 0; i < iv.Count; i++) { + Expr eqExpr = new NAryExpr( + Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Eq), new ExprSeq(exprs[i], Expr.Ident(iv[i]))); + conj = + new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new ExprSeq(conj, eqExpr)); + } + ret = + new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Or), new ExprSeq(ret, conj)); + } + proc.Ensures.Add(new Ensures(true, ret)); + } } } @@ -226,145 +250,6 @@ namespace VC { } } - // proc name -> k -> interface variables - public static Dictionary>> interfaceVarCopies; - // proc name -> k -> VCExpr - Dictionary> procVcCopies; - - private void CreateCopiesForLazyInlining(int K, Program program) - { - interfaceVarCopies = new Dictionary>>(); - procVcCopies = new Dictionary>(); - - // Duplicate VCs of each procedure K times and remove quantifiers - Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); - foreach (LazyInliningInfo info in implName2LazyInliningInfo.Values) - { - Contract.Assert(info != null); - CreateCopyForLazyInlining(K, program, info, checker); - } - - // Change the procedure calls in each VC - // Push all to the theorem prover - var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies); - foreach (var kvp in procVcCopies) - { - for (int i = 0; i < kvp.Value.Count; i++) - { - kvp.Value[i] = bm.Mutate(kvp.Value[i], true); - checker.TheoremProver.PushVCExpression(kvp.Value[i]); - } - } - } - - public class BoundingVCMutator : MutatingVCExprVisitor - { - // proc name -> k -> interface variables - Dictionary>> interfaceVarCopies; - - public BoundingVCMutator(VCExpressionGenerator gen, Dictionary>> interfaceVarCopies) - : base(gen) - { - Contract.Requires(gen != null); - this.interfaceVarCopies = interfaceVarCopies; - } - - protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, - List/*!*/ newSubExprs, - // has any of the subexpressions changed? - bool changed, - bool arg) - { - //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); - Contract.Ensures(Contract.Result() != null); - - VCExpr node; - if (changed) - node = Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); - else - node = originalNode; - - var expr = node as VCExprNAry; - if (expr == null) return node; - var op = expr.Op as VCExprBoogieFunctionOp; - if (op == null) return node; - if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return node; - - // substitute - var K = interfaceVarCopies[op.Func.Name].Count; - - - VCExpr ret = VCExpressionGenerator.False; - for (int k = 0; k < K; k++) - { - var iv = interfaceVarCopies[op.Func.Name][k]; - Contract.Assert(op.Arity == iv.Count); - - VCExpr conj = VCExpressionGenerator.True; - for (int i = 0; i < iv.Count; i++) - { - var c = Gen.Eq(expr[i], iv[i]); - conj = Gen.And(conj, c); - } - ret = Gen.Or(conj, ret); - } - - return ret; - } - - } // end BoundingVCMutator - - private static int newVarCnt = 0; - - private void CreateCopyForLazyInlining(int K, Program program, LazyInliningInfo info, Checker checker) - { - var translator = checker.TheoremProver.Context.BoogieExprTranslator; - interfaceVarCopies.Add(info.impl.Name, new List>()); - procVcCopies.Add(info.impl.Name, new List()); - - for (int k = 0; k < K; k++) - { - var expr = info.inside_vc; - // Instantiate the "forall" variables - Dictionary substForallDict = new Dictionary(); - var ls = new List(); - for (int i = 0; i < info.interfaceVars.Count; i++) - { - var v = translator.LookupVariable(info.interfaceVars[i]); - string newName = v.Name + "_fa_" + k.ToString() + "_" + newVarCnt.ToString(); - newVarCnt++; - //checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); - var vp = checker.VCExprGen.Variable(newName, v.Type); - substForallDict.Add(v, vp); - ls.Add(vp); - } - interfaceVarCopies[info.impl.Name].Add(ls); - VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary()); - - SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen); - Contract.Assert(subst != null); - expr = subst.Mutate(expr, substForall); - - // Instantiate and declare the "exists" variables - Dictionary substExistsDict = new Dictionary(); - foreach (VCExprVar v in info.privateVars) - { - Contract.Assert(v != null); - string newName = v.Name + "_te_" + k.ToString() + "_" + newVarCnt.ToString(); - newVarCnt++; - checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); - substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type)); - } - VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary()); - - subst = new SubstitutingVCExprVisitor(checker.VCExprGen); - expr = subst.Mutate(expr, substExists); - - procVcCopies[info.impl.Name].Add(expr); - } - } - private void GenerateVCForLazyInlining(Program program, LazyInliningInfo info, Checker checker) { Contract.Requires(program != null); Contract.Requires(info != null); @@ -389,7 +274,7 @@ namespace VC { ResetPredecessors(impl.Blocks); VCExpr reachvcexpr = GenerateReachVC(impl, info, checker); vcexpr = gen.And(vcexpr, reachvcexpr); - + List privateVars = new List(); foreach (Variable v in impl.LocVars) { Contract.Assert(v != null); @@ -401,7 +286,6 @@ namespace VC { } info.privateVars = privateVars; - info.inside_vc = vcexpr; if (privateVars.Count > 0) { vcexpr = gen.Exists(new List(), privateVars, new List(), @@ -421,12 +305,7 @@ namespace VC { Function function = cce.NonNull(info.function); VCExpr expr = gen.Function(function, interfaceExprs); Contract.Assert(expr != null); - if (CommandLineOptions.Clo.LazyInlining == 1) { - vcexpr = gen.Implies(expr, vcexpr); - } else { - //Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2); - vcexpr = gen.Eq(expr, vcexpr); - } + vcexpr = gen.Implies(expr, vcexpr); List triggers = new List(); List exprs = new List(); @@ -442,10 +321,7 @@ namespace VC { new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr); info.vcexpr = vcexpr; - if (CommandLineOptions.Clo.LazyInlining != 3) - { - checker.TheoremProver.PushVCExpression(vcexpr); - } + checker.TheoremProver.PushVCExpression(vcexpr); } protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) { @@ -1662,12 +1538,6 @@ namespace VC { VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker); Contract.Assert(vc != null); - if (CommandLineOptions.Clo.LazyInlining == 3) - { - var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies); - vc = bm.Mutate(vc, true); - } - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) { reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program); } else { -- cgit v1.2.3 From fb23eb40279252804d9c5d9b642b8be137d1e1ef Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 17 Aug 2011 09:24:28 -0700 Subject: minor refactoring --- Source/VCGeneration/VC.cs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 51bdb033..79fdaaa2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -164,8 +164,9 @@ namespace VC { for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) { interfaceVarCopies.Add(new List()); foreach (Variable v in interfaceVars) { - interfaceVarCopies[i].Add( - new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type))); + Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type)); + interfaceVarCopies[i].Add(constant); + //program.TopLevelDeclarations.Add(constant); } } } -- cgit v1.2.3