summaryrefslogtreecommitdiff
path: root/Jennisys
diff options
context:
space:
mode:
authorGravatar Aleksandar Milicevic <unknown>2011-08-15 18:46:08 -0700
committerGravatar Aleksandar Milicevic <unknown>2011-08-15 18:46:08 -0700
commite68494fba6e0b6f419bbfa109f877e794928c832 (patch)
treebc9ed0f9118e2573eaf093d07b36851017fdcb7a /Jennisys
parent5ff5c7243d5a710e29ed7c6e639070b93ff41e89 (diff)
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
Diffstat (limited to 'Jennisys')
-rw-r--r--Jennisys/Analyzer.fs114
-rw-r--r--Jennisys/AstUtils.fs468
-rw-r--r--Jennisys/CodeGen.fs20
-rw-r--r--Jennisys/DafnyModelUtils.fs15
-rw-r--r--Jennisys/Jennisys.fsproj2
-rw-r--r--Jennisys/Logger.fs2
-rw-r--r--Jennisys/MethodUnifier.fs1
-rw-r--r--Jennisys/Modularizer.fs6
-rw-r--r--Jennisys/Resolver.fs89
-rw-r--r--Jennisys/examples/List.jen5
-rw-r--r--Jennisys/tmp.out435
11 files changed, 403 insertions, 754 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index f439c8d0..512a6870 100644
--- a/Jennisys/Analyzer.fs
+++ b/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/AstUtils.fs b/Jennisys/AstUtils.fs
index a866ad08..f5d90489 100644
--- a/Jennisys/AstUtils.fs
+++ b/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/CodeGen.fs b/Jennisys/CodeGen.fs
index a6caaa6e..714c44f1 100644
--- a/Jennisys/CodeGen.fs
+++ b/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/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index 65fd97d2..ffd30fc7 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/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.fsproj b/Jennisys/Jennisys.fsproj
index a3c92ab7..beac24f8 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
<WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
- <StartArguments>examples/Set.jen /genMod /genRepr /method:Set.Double</StartArguments>
+ <StartArguments>examples/List.jen /genMod /genRepr /method:Node.Get</StartArguments>
<StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs
index d9df47a7..dbf762cd 100644
--- a/Jennisys/Logger.fs
+++ b/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/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index f12e8dd0..14d4f31f 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/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/Modularizer.fs b/Jennisys/Modularizer.fs
index b196d4cb..3215786d 100644
--- a/Jennisys/Modularizer.fs
+++ b/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/Resolver.fs b/Jennisys/Resolver.fs
index d38fbf7b..bb546834 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -22,7 +22,8 @@ type AssignmentType =
type HeapInstance = {
objs: Map<string, Obj>;
modifiableObjs: Set<Obj>;
- assignments: AssignmentType list
+ assignments: AssignmentType list;
+ concreteValues: AssignmentType list;
methodArgs: Map<string, Const>;
methodRetVals: Map<string, Expr>;
globals: Map<string, Expr>;
@@ -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/examples/List.jen b/Jennisys/examples/List.jen
index bb36c2bb..7fa04fc4 100644
--- a/Jennisys/examples/List.jen
+++ b/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/tmp.out b/Jennisys/tmp.out
deleted file mode 100644
index 9a51a8c8..00000000
--- a/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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 01:25:08 +0000