summaryrefslogtreecommitdiff
path: root/Jennisys
diff options
context:
space:
mode:
authorGravatar Aleksandar Milicevic <unknown>2011-08-20 14:51:32 -0700
committerGravatar Aleksandar Milicevic <unknown>2011-08-20 14:51:32 -0700
commit21c0769882e3969e51b2085fcbe5ac419bdac2c3 (patch)
treea0605ad3250db7b15148ae7f19a3c7d22b5b9ee2 /Jennisys
parentf0989291edf82f7548d6146632269473c32b9286 (diff)
Jennisys: added some more infrastructure for synthesizing read only methods
Diffstat (limited to 'Jennisys')
-rw-r--r--Jennisys/Analyzer.fs214
-rw-r--r--Jennisys/AstUtils.fs72
-rw-r--r--Jennisys/CodeGen.fs2
-rw-r--r--Jennisys/DafnyModelUtils.fs12
-rw-r--r--Jennisys/FixpointSolver.fs249
-rw-r--r--Jennisys/Jennisys.fsproj3
-rw-r--r--Jennisys/MethodUnifier.fs141
-rw-r--r--Jennisys/Modularizer.fs20
-rw-r--r--Jennisys/Resolver.fs195
-rw-r--r--Jennisys/Utils.fs14
-rw-r--r--Jennisys/examples/List.jen1
-rw-r--r--Jennisys/examples/Set.jen3
-rw-r--r--Jennisys/examples/Set2.jen60
13 files changed, 699 insertions, 287 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 7c8c472d..f31c41ec 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -4,14 +4,15 @@ open Ast
open AstUtils
open CodeGen
open DafnyModelUtils
+open DafnyPrinter
+open FixpointSolver
open MethodUnifier
open Modularizer
-open PipelineUtils
open Options
-open TypeChecker
-open Resolver
+open PipelineUtils
open PrintUtils
-open DafnyPrinter
+open Resolver
+open TypeChecker
open Utils
open Microsoft.Boogie
@@ -202,7 +203,7 @@ let rec GetUnifications prog indent (comp,meth) heapInst unifs expr =
let builder = new CascadingBuilder<_>(unifsAcc)
builder {
let! argsOnly = IsUnmodConcrOnly prog (comp,meth) e |> Utils.BoolToOption
- let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None
+ let! v = try Some(EvalFull heapInst e |> Expr2Const) with ex -> None
return AddUnif indent e v unifsAcc
}
(* --- function body starts here --- *)
@@ -346,7 +347,7 @@ let rec DiscoverAliasing exprList heapInst =
match exprList with
| e1 :: rest ->
let eqExpr = rest |> List.fold (fun acc e ->
- if Eval heapInst (fun _ -> true) (BinaryEq e1 e) = TrueLiteral then
+ if EvalFull heapInst (BinaryEq e1 e) = TrueLiteral then
BinaryAnd acc (BinaryEq e1 e)
else
acc
@@ -368,17 +369,21 @@ let DontResolveUnmodifiableStuff prog comp meth expr =
| _ -> true
/// Descends down a given expression and returns all sub-expressions that evaluate to TrueLiteral
-let FindTrueClauses prog comp m heapInst expr =
+let FindTrueClauses resolverFunc 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
+ try
+ match expr with
+ // skip binary logical operators because we want to find smallest sub-expressions
+ | BinaryExpr(_,op,_,_) when IsLogicalOp op -> acc
+ | _ ->
+ let exprEval = EvalAndCheckTrue heapInst resolverFunc expr
+ match exprEval with
+ | _ when exprEval = TrueLiteral -> acc
+ | _ ->
+ let exprAllResolved = EvalFull heapInst expr
+ match exprAllResolved with
+ | BoolLiteral(true) -> acc @ [exprEval]
+ | _ -> acc
with
| _ -> acc
(* --- function body starts here --- *)
@@ -412,11 +417,22 @@ let GetAllPossibleConditions specConds argConds aliasingConds =
// ============================================================================
let rec AnalyzeConstructor indent prog comp m callGraph =
let idt = Indent indent
+ let TryFindAndVerify =
+ match TryFindExistingAndConvertToSolution indent comp m TrueLiteral callGraph with
+ | Some(sol) ->
+ if VerifySolution prog sol Options.CONFIG.genRepr then
+ Logger.InfoLine (idt + " ~~~ VERIFIED ~~~")
+ Some(sol)
+ else
+ Logger.InfoLine (idt + " !!! NOT VERIFIED !!!")
+ None
+ | None -> None
+
Logger.InfoLine (idt + "[*] Analyzing constructor")
Logger.InfoLine (idt + "------------------------------------------")
Logger.InfoLine (Printer.PrintMethodSignFull (indent + 4) comp m)
Logger.InfoLine (idt + "------------------------------------------")
- match TryFindExistingAndConvertToSolution indent comp m TrueLiteral callGraph with
+ match TryFindAndVerify with
| Some(sol) -> sol
| None ->
let methodName = GetMethodName m
@@ -488,14 +504,15 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
(* --- function body starts here --- *)
let idt = Indent indent
+ let loggerFunc = fun e -> Logger.TraceLine (sprintf "%s --> %s" idt (PrintExpr 0 e))
+
let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]
let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false
let methodArgs = GetMethodInArgs m
// find candidate conditions
let expr = GetHeapExpr prog m heapInst2
- let specConds = expr |> FindTrueClauses prog comp m heapInst2
- let specConds = specConds
+ let specConds = expr |> FindTrueClauses (DontResolveUnmodifiableStuff prog comp m) heapInst2
|> List.filter (IsUnmodConcrOnly prog (comp,m))
let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2)
@@ -503,7 +520,6 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
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
// ---
@@ -520,40 +536,134 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
| 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
// the solution is not immediate, so try to delegate to a method call, possibly to a recursive one
- //TODO
- Logger.InfoLine "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"
- wrongSol
+
+ // find set of premises (don't resolve anything)
+ expr |> SplitIntoConjunts |> List.iter loggerFunc
+
+ let premises = expr |> FindTrueClauses (fun e -> false) heapInst2
+ let closedPremise = ComputeClosure (premises |> Set.ofList) heapInst2
+
+ // --- trace
+ Logger.TraceLine (sprintf "%s Premises:" idt)
+ premises |> List.iter loggerFunc //
+ Logger.TraceLine (sprintf "%s Closed premises:" idt)
+ closedPremise |> Set.iter loggerFunc
+
+ //------------------
+ let __CheckSol hInst premises =
+ let rec __CheckVars vars =
+ match vars with
+ | lhs :: [] ->
+ let lhsOptions = premises |> Set.toList
+ |> List.choose (function
+ | BinaryExpr(_,"=",l,r) -> if l = lhs then Some(r) elif r = lhs then Some(l) else None
+ | _ -> None)
+ |> List.map (fun e -> [lhs,e])
+ lhsOptions
+ | lhs :: rest ->
+ let lhsOptions = __CheckVars [lhs]
+ if List.isEmpty lhsOptions then
+ List.empty
+ else
+ let restOptions = __CheckVars rest
+ Utils.ListCombine (fun t1 t2 -> t1 @ t2) lhsOptions restOptions
+ | [] -> List.empty
+
+ let stmts = ConvertToStatements hInst true
+ let modVars = stmts |> List.choose (function
+ | Assign(lhs,_) -> Some(lhs)
+ | _ -> None)
+ __CheckVars modVars
+ //-------------------
+
+ let __InCtx ctx id = ctx |> List.exists (function Var(name,_) -> name = id)
+ let compName = GetComponentName comp
+ let methName = GetMethodName m
+ let invocationArgs = GetMethodInArgs m |> List.map (function Var(name,_) -> VarLiteral("$" + name))
+
+ let s = __CheckSol heapInst2 closedPremise
+
+ // add only recursive calls to immediate children
+ let post = GetMethodPrePost m |> snd
+ |> RewriteWithCtx (fun ctx e ->
+ match e with
+ | VarLiteral(id) when not (IsInVarList ctx id) -> Some(VarLiteral("$" + id))
+ | _ -> None) []
+
+ let rec Try spec s =
+ match s with
+ | fs :: rest ->
+ let goal = fs |> List.fold (fun acc (e1,e2) -> BinaryAnd acc (BinaryEq e1 e2)) TrueLiteral
+ match UnifyImplies spec goal LTR Map.empty with
+ | Some(x) -> Some(x)
+ | None -> Try spec rest
+ | [] -> None
+
+ let rec __IterAsgs asgs =
+ match asgs with
+ | FieldAssignment((obj,Var(fldName,Some(fldType))),fldVal) :: rest
+ when obj.name = "this" && not (fldVal = NullLiteral) && IsConcreteField comp fldName && CheckSameCompType comp fldType ->
+ let receiver = Dot(ThisLiteral, fldName)
+ let changedThis = ChangeThisReceiver receiver post
+ let mcall = MethodCall(receiver, compName, methName, invocationArgs)
+
+ match Try changedThis s with
+ | Some(unifs) ->
+ let unifs = unifs |> Map.fold (fun acc (k: string) v -> acc |> Map.add (k.Replace("$", "")) v) Map.empty
+ //s |> Map.iter (fun k v -> Logger.TraceLine (sprintf "%s --> %s" k (PrintExpr 0 v)))
+ let asgs = ApplyMethodUnifs receiver (comp,m) unifs
+ let restRes = __IterAsgs rest
+ (fst restRes, asgs @ (snd restRes))
+ | None -> (false, [])
+ | _ :: rest ->
+ __IterAsgs rest
+ | [] -> (true, [])
+
+ match __IterAsgs heapInst2.assignments with
+ | (true, asgs) ->
+ Logger.InfoLine "AAAAAAAAAAAAAAAAA"
+ let heapInst3 = {heapInst2 with assignments = asgs}
+ let sol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst3]
+ Logger.Info (idt + " ")
+ if VerifySolution prog sol Options.CONFIG.genRepr then
+ Logger.InfoLine "~~~ VERIFIED ~~~"
+ sol
+ else
+ Logger.InfoLine "!!! NOT VERIFIED !!!"
+ sol
+
+ | (false, _) -> wrongSol
+
+// if List.isEmpty s then
+//
+//
+// // add only recursive calls to immediate children
+// let post = GetMethodPrePost m |> snd
+// |> RewriteWithCtx (fun ctx e ->
+// match e with
+// | VarLiteral(id) when not (IsInVarList ctx id) -> Some(VarLiteral("$" + id))
+// | _ -> None) []
+// let extraExprs = heapInst2.assignments |> List.fold (fun acc asgn ->
+// match asgn with
+// | FieldAssignment((obj,Var(fldName,Some(fldType))),fldVal)
+// when obj.name = "this" && not (fldVal = NullLiteral) && IsConcreteField comp fldName && CheckSameCompType comp fldType ->
+// let receiver = Dot(ThisLiteral, fldName)
+// let changedThis = ChangeThisReceiver receiver post
+// let mcall = MethodCall(receiver, compName, methName, invocationArgs)
+// acc @ [BinaryEq mcall changedThis]
+// | _ -> acc
+// ) []
+// let newPremises = closedPremise |> Set.union (extraExprs |> Set.ofList)
+// Logger.TraceLine (sprintf "%s With extra premises:" idt)
+// //newPremises |> Set.iter loggerFunc
+// extraExprs |> List.iter loggerFunc
+// wrongSol
+// else
+// s |> List.iter (fun lst -> lst |> List.iter (fun (l,r) -> Logger.TraceLine (sprintf "%s --> %s" (PrintExpr 0 l) (PrintExpr 0 r))))
+// wrongSol
+
let GetMethodsToAnalyze prog =
let __ReadMethodsParam =
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index b4ed22e6..b56ddb57 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -13,6 +13,29 @@ open Utils
let ThisLiteral = ObjLiteral("this")
let NullLiteral = ObjLiteral("null")
+let IsLogicalOp op = [ "&&"; "||"; "==>"; "<==>" ] |> Utils.ListContains op
+let IsRelationalOp op = [ "="; "!="; "<"; "<="; ">"; ">=" ] |> Utils.ListContains op
+
+let AreInverseOps op1 op2 = match op1, op2 with "<" , ">" | ">" , "<" | "<=", ">=" | ">=", "<=" -> true | _ -> false
+let DoesImplyOp op1 op2 =
+ match op1, op2 with
+ | "<" , "!=" | ">" , "!=" -> true
+ | "=" , ">=" | "=" , "<=" -> true
+ | _ -> false
+let IsCommutativeOp op = match op with "=" | "!=" -> true | _ -> false
+
+exception ExprConvFailed of string
+
+let Expr2Int e =
+ match e with
+ | IntLiteral(n) -> n
+ | _ -> raise (ExprConvFailed(sprintf "not an int but: %O" e))
+
+let Expr2List e =
+ match e with
+ | SequenceExpr(elist) -> elist
+ | _ -> raise (ExprConvFailed(sprintf "not a Seq but: %O" e))
+
let rec Rewrite rewriterFunc expr =
let __RewriteOrRecurse e =
match rewriterFunc e with
@@ -44,6 +67,36 @@ let rec Rewrite rewriterFunc expr =
| AssertExpr(e) -> AssertExpr(__RewriteOrRecurse e)
| AssumeExpr(e) -> AssumeExpr(__RewriteOrRecurse e)
+let rec RewriteWithCtx rewriterFunc ctx expr =
+ let __RewriteOrRecurse ctx e =
+ match rewriterFunc ctx e with
+ | Some(ee) -> ee
+ | None -> RewriteWithCtx rewriterFunc ctx e
+ match expr with
+ | IntLiteral(_)
+ | BoolLiteral(_)
+ | BoxLiteral(_)
+ | Star
+ | VarLiteral(_)
+ | ObjLiteral(_)
+ | VarDeclExpr(_)
+ | IdLiteral(_) -> match rewriterFunc ctx expr with
+ | Some(e) -> e
+ | None -> expr
+ | Dot(e, id) -> Dot(__RewriteOrRecurse ctx e, id)
+ | ForallExpr(vars,e) -> ForallExpr(vars, __RewriteOrRecurse (ctx @ vars) e)
+ | UnaryExpr(op,e) -> UnaryExpr(op, __RewriteOrRecurse ctx e)
+ | LCIntervalExpr(e) -> LCIntervalExpr(__RewriteOrRecurse ctx e)
+ | SeqLength(e) -> SeqLength(__RewriteOrRecurse ctx e)
+ | SelectExpr(e1, e2) -> SelectExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2)
+ | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2)
+ | IteExpr(e1,e2,e3) -> IteExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2, __RewriteOrRecurse ctx e3)
+ | UpdateExpr(e1,e2,e3) -> UpdateExpr(__RewriteOrRecurse ctx e1, __RewriteOrRecurse ctx e2, __RewriteOrRecurse ctx e3)
+ | SequenceExpr(exs) -> SequenceExpr(exs |> List.map (__RewriteOrRecurse ctx))
+ | SetExpr(exs) -> SetExpr(exs |> List.map (__RewriteOrRecurse ctx))
+ | MethodCall(rcv,cname,mname,ins) -> MethodCall(__RewriteOrRecurse ctx rcv, cname, mname, ins |> List.map (__RewriteOrRecurse ctx))
+ | AssertExpr(e) -> AssertExpr(__RewriteOrRecurse ctx e)
+ | AssumeExpr(e) -> AssumeExpr(__RewriteOrRecurse ctx e)
// ====================================================
/// Substitutes all occurences of all IdLiterals having
/// the same name as one of the variables in "vars" with
@@ -175,12 +228,6 @@ let UnaryNot sub =
| _ -> UnaryExpr("!", sub)
// =======================================================================
-/// Returns a binary PLUS of the two given expressions
-// =======================================================================
-let BinaryPlus (lhs: Expr) (rhs: Expr) =
- BinaryExpr(50, "+", lhs, rhs)
-
-// =======================================================================
/// Returns a binary AND of the two given expressions with short-circuiting
// =======================================================================
let BinaryAnd (lhs: Expr) (rhs: Expr) =
@@ -224,6 +271,9 @@ let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)
// =======================================================
let BinaryGets lhs rhs = Assign(lhs, rhs)
+let BinaryAdd lhs rhs = BinaryExpr(55, "+", lhs, rhs)
+let BinarySub lhs rhs = BinaryExpr(55, "-", lhs, rhs)
+
// =======================================================
/// Constructors for binary IN/!IN of two given expressions
// =======================================================
@@ -459,6 +509,13 @@ let GetVarName var =
match var with
| Var(name,_) -> name
+// ===============================================
+/// Returns whether there exists a variable
+/// in a given VarDecl list with a given name (id)
+// ===============================================
+let IsInVarList varLst id =
+ varLst |> List.exists (function Var(name,_) -> name = id)
+
// ==================================
/// Returns component name
// ==================================
@@ -486,6 +543,9 @@ let FindComponent (prog: Program) clsName =
let FindComponentForType prog ty =
FindComponent prog (GetTypeShortName ty)
+let CheckSameCompType comp ty =
+ GetComponentName comp = GetTypeShortName ty
+
// ===================================================
/// Finds a method of a component that has a given name
// ===================================================
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 10398fa9..2892a07b 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -194,7 +194,7 @@ let PrintReprAssignments prog heapInst indent =
| Some(ObjLiteral(n)) when not (n = "null") -> true
| _ -> false)
return nonNullVars |> List.fold (fun a v ->
- BinaryPlus a (Dot(Dot(ObjLiteral(obj.name), (GetVarName v)), "Repr"))
+ BinaryAdd a (Dot(Dot(ObjLiteral(obj.name), (GetVarName v)), "Repr"))
) expr
}
let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index 6a8cb727..afab212c 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -87,6 +87,16 @@ let GetType (e: Model.Element) prog =
let GetLoc (e: Model.Element) =
Unresolved(GetRefName e)
+let FindOrCreateSeq env key len =
+ match Map.tryFind key env with
+ | Some(SeqConst(lst)) -> lst,env
+ | None ->
+ let emptyList = Utils.GenList len NoneConst
+ let newSeq = SeqConst(emptyList)
+ let newMap = env |> Map.add key newSeq
+ emptyList,newMap
+ | Some(_) as x-> failwith ("not a SeqConst but: " + x.ToString())
+
let FindSeqInEnv env key =
match Map.find key env with
| SeqConst(lst) -> lst
@@ -204,8 +214,8 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
match idx_tuples with
| ft :: rest ->
let srcLstKey = GetLoc ft.Args.[0]
- let oldLst = FindSeqInEnv envMap srcLstKey
let idx = GetInt ft.Args.[1]
+ let oldLst,envMap = FindOrCreateSeq envMap srcLstKey (idx+1)
let lstElem = UnboxIfNeeded model ft.Result
let newLst = Utils.ListSet idx lstElem oldLst
let newCtx = UpdateContext oldLst newLst ctx
diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs
new file mode 100644
index 00000000..097e72c9
--- /dev/null
+++ b/Jennisys/FixpointSolver.fs
@@ -0,0 +1,249 @@
+module FixpointSolver
+
+open Ast
+open AstUtils
+open Resolver
+open Utils
+
+let rec ComputeClosure premises heapInst =
+ let bogusExpr = VarLiteral("!@#$%^&*()")
+
+ let FindMatches expr except premises =
+ premises |> Set.toList
+ |> List.choose (function BinaryExpr(_,"=",lhs,rhs) ->
+ if lhs = expr && not (rhs = except) then
+ Some(rhs)
+ elif rhs = expr && not (lhs = except) then
+ Some(lhs)
+ else None
+ | _ -> None)
+
+ let MySetAdd expr set =
+ match expr with
+ | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && Set.contains (BinaryExpr(p,op,rhs,lhs)) set -> set
+ | BinaryExpr(p,op,lhs,rhs) when IsCommutativeOp op && rhs = lhs -> set
+ | _ -> Set.add expr set
+
+// let rec __ExpandPremise expr premises =
+// let bogusExpr = VarLiteral("!@#$%^&*()")
+// match expr with
+// | BinaryExpr(p,op,lhs,rhs) ->
+// let __AddLhsToPremisses expr exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryExpr(p,op,expr,e)) acc) premises
+// let __AddRhsToPremisses exprLst expr premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryExpr(p,op,e,expr)) acc) premises
+// let premises' = __ExpandPremise lhs premises |> __ExpandPremise rhs
+// let lhsMatches = __FindMatches lhs rhs premises'
+// let rhsMatches = __FindMatches rhs lhs premises'
+// premises' |> __AddLhsToPremisses lhs rhsMatches
+// |> __AddRhsToPremisses lhsMatches rhs
+// | UnaryExpr(op, sub) ->
+// let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd (BinaryEq expr (UnaryExpr(op,e))) acc) premises
+// let premises' = __ExpandPremise sub premises
+// let subMatches = __FindMatches sub bogusExpr premises'
+// premises' |> __AddToPremisses subMatches
+// | SelectExpr(lst, idx) ->
+// let __EvalLst lst idx = BinaryEq expr (SelectExpr(lst,idx))
+//
+//
+// let __AddLstToPremisses lstMatches idx premises = lstMatches |> List.fold (fun acc lst -> MySetAdd (__EvalLst lst idx) acc) premises
+// let __AddIdxToPremisses lst idxMatches premises = idxMatches |> List.fold (fun acc idx -> MySetAdd (__EvalLst lst idx) acc) premises
+// let premises' = __ExpandPremise lst premises |> __ExpandPremise idx
+// let lstMatches = __FindMatches lst bogusExpr premises'
+// let idxMatches = __FindMatches idx bogusExpr premises'
+// premises' |> __AddLstToPremisses lstMatches idx
+// |> __AddIdxToPremisses lst idxMatches
+//
+// | _ -> premises
+
+ let SelectExprCombinerFunc lst idx =
+ // distribute the indexing operation if possible
+ let rec __fff lst idx =
+ let selExpr = SelectExpr(lst, idx)
+ match lst with
+ | BinaryExpr(_,"+",lhs,rhs) ->
+ let idxVal = EvalFull heapInst idx |> Expr2Int
+ let lhsVal = EvalFull heapInst lhs |> Expr2List
+ let rhsVal = EvalFull heapInst rhs |> Expr2List
+ if idxVal < List.length lhsVal then
+ __fff lhs idx
+ else
+ __fff rhs (BinarySub idx (IntLiteral(List.length lhsVal)))
+ | SequenceExpr(elist) ->
+ let idxVal = EvalFull heapInst idx |> Expr2Int
+ [elist.[idxVal]]
+ | _ -> [selExpr]
+ __fff lst idx
+
+ let SeqLenCombinerFunc lst =
+ // distribute the SeqLength operation if possible
+ let rec __fff lst =
+ let lenExpr = SeqLength(lst)
+ match lst with
+ | BinaryExpr(_,"+",lhs,rhs) ->
+ BinaryAdd (__fff lhs) (__fff rhs)
+ | SequenceExpr(elist) ->
+ IntLiteral(List.length elist)
+ | _ -> lenExpr
+ [__fff lst]
+
+ let rec __CombineAllMatches expr premises =
+ match expr with
+ | BinaryExpr(p,op,lhs,rhs) ->
+ let lhsMatches = __CombineAllMatches lhs premises
+ let rhsMatches = __CombineAllMatches rhs premises
+ Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches
+ | UnaryExpr(op,sub) ->
+ __CombineAllMatches sub premises |> List.map (fun e -> UnaryExpr(op,e))
+ | SelectExpr(lst,idx) ->
+ let lstMatches = __CombineAllMatches lst premises
+ let idxMatches = __CombineAllMatches idx premises
+ Utils.ListCombineMult SelectExprCombinerFunc lstMatches idxMatches
+ | SeqLength(lst) ->
+ __CombineAllMatches lst premises |> List.map SeqLenCombinerFunc |> List.concat
+ // TODO: other cases
+ | _ -> expr :: (FindMatches expr bogusExpr premises)
+
+ let rec __ExpandPremise expr premises =
+ let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd e acc) premises
+ let allMatches = lazy(__CombineAllMatches expr premises)
+ match expr with
+ | BinaryExpr(p,op,lhs,rhs) when IsRelationalOp op ->
+ let x = allMatches.Force()
+ __AddToPremisses x premises
+ | SelectExpr(lst, idx) ->
+ let x = allMatches.Force()
+ __AddToPremisses x premises
+ | _ -> premises
+
+ let rec __Iter exprLst premises =
+ match exprLst with
+ | expr :: rest ->
+ let newPremises = __ExpandPremise expr premises
+ __Iter rest newPremises
+ | [] -> premises
+
+ (* --- function body starts here --- *)
+ let premises' = __Iter (premises |> Set.toList) premises
+ if premises' = premises then
+ premises'
+ else
+ ComputeClosure premises' heapInst
+
+
+/////////////
+
+type UnifDirection = LTR | RTL
+
+exception CannotUnify
+
+let rec UnifyImplies lhs rhs dir unifs =
+ ///
+ let __AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)
+
+ ///
+ let __UnifLists lstL lstR =
+ if List.length lstL = List.length lstR then
+ try
+ let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with
+ | Some(u) -> u
+ | None -> raise CannotUnify) unifs lstL lstR
+ Some(unifs2)
+ with
+ | CannotUnify -> None
+ else
+ None
+
+ ///
+ let __ApplyUnifs unifs exprList =
+ exprList |> List.fold (fun acc e ->
+ let e' = e |> Rewrite (fun e ->
+ match e with
+ | VarLiteral(id) when Map.containsKey id unifs -> Some(unifs |> Map.find id)
+ | _ -> None)
+ acc |> Set.add e'
+ ) Set.empty
+
+ if lhs = FalseLiteral || rhs = TrueLiteral then
+ Some(unifs)
+ else
+ try
+ let l,r = match dir with
+ | LTR -> lhs,rhs
+ | RTL -> rhs,lhs
+ match l, r with
+ | VarLiteral(vname), rhs -> __AddOrNone unifs vname rhs
+ | IntLiteral(nL), IntLiteral(nR) when nL = nR ->
+ Some(unifs)
+ | BoolLiteral(bL), BoolLiteral(bR) when bL = bR ->
+ Some(unifs)
+ | SetExpr(elistL), SetExpr(elistR) ->
+ let s1 = elistL |> __ApplyUnifs unifs
+ let s2 = elistR |> Set.ofList
+ if (s1 = s2) then
+ Some(unifs)
+ else
+ __UnifLists elistL elistR
+ | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->
+ __UnifLists elistL elistR
+ | _ when l = r ->
+ Some(unifs)
+ | _ ->
+ let __TryUnifyPair x1 a1 x2 a2 unifs =
+ let builder = new Utils.CascadingBuilder<_>(None)
+ builder {
+ let! unifsLhs = UnifyImplies x1 a1 dir unifs
+ let! unifsRhs = UnifyImplies x2 a2 dir unifsLhs
+ return Some(unifsRhs)
+ }
+
+ // target implies candidate!
+ let rec ___f2 consequence premise unifs =
+ match consequence, premise with
+ // same operators + commutative -> try both
+ | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC && IsCommutativeOp opT ->
+ match __TryUnifyPair lhsC lhsT rhsC rhsT unifs with
+ | Some(x) -> Some(x)
+ | None -> __TryUnifyPair lhsC rhsT rhsC lhsT unifs
+ // operators are the same
+ | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opC = opT ->
+ __TryUnifyPair lhsC lhsT rhsC rhsT unifs
+ // operators are exactly the invers of one another
+ | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when AreInverseOps opC opT ->
+ __TryUnifyPair lhsC rhsT rhsC lhsT unifs
+ //
+ | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when DoesImplyOp opC opT ->
+ __TryUnifyPair lhsC lhsT rhsC rhsT unifs
+ | UnaryExpr(opC, subC), UnaryExpr(opP, subP) when opC = opP ->
+ UnifyImplies subP subC dir unifs
+ | SelectExpr(lstC, idxC), SelectExpr(lstP, idxP) ->
+ __TryUnifyPair lstP lstC idxP idxC unifs
+ | _ -> None
+
+ let rec ___f1 targetLst candidateLst unifs =
+ match targetLst, candidateLst with
+ | targetExpr :: targetRest, candExpr :: candRest ->
+ // trying to find a unification for "targetExpr"
+ let uOpt = match ___f2 targetExpr candExpr unifs with
+ // found -> just return
+ | Some(unifs2) -> Some(unifs2)
+ // not found -> keep looking in the rest of the candidate expressions
+ | None -> ___f1 [targetExpr] candRest unifs
+ match uOpt with
+ // found -> try find for the rest of the target expressions
+ | Some(unifs2) -> ___f1 targetRest candidateLst unifs2
+ // not found -> fail
+ | None -> None
+ | targetExpr :: _, [] ->
+ // no more candidates for unification for this targetExpr -> fail
+ None
+ | [], _ ->
+ // we've found unifications for all target expressions -> return the current unifications map
+ Some(unifs)
+
+ let __HasSetExpr e = DescendExpr2 (fun ex acc -> if acc then true else match ex with SetExpr(_) -> true | _ -> false) e false
+ let __PreprocSplitSort e = e |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts |> List.sortBy (fun e -> if __HasSetExpr e then 1 else 0)
+ let lhsConjs = lhs |> __PreprocSplitSort
+ let rhsConjs = rhs |> __PreprocSplitSort
+ ___f1 rhsConjs lhsConjs unifs
+ with
+ | CannotUnify
+ | KeyAlreadyExists -> None \ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 2613432c..e4b1493c 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/NumberMethods.jen /genMod /genRepr /method:NumberMethods.Min4</StartArguments>
+ <StartArguments>examples/List.jen /genMod /genRepr /method:Node.Get</StartArguments>
<StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
@@ -71,6 +71,7 @@
<Compile Include="DafnyPrinter.fs" />
<Compile Include="TypeChecker.fs" />
<Compile Include="Resolver.fs" />
+ <Compile Include="FixpointSolver.fs" />
<Compile Include="MethodUnifier.fs" />
<Compile Include="Modularizer.fs" />
<Compile Include="CodeGen.fs" />
diff --git a/Jennisys/MethodUnifier.fs b/Jennisys/MethodUnifier.fs
index 14d4f31f..0ac1ecf6 100644
--- a/Jennisys/MethodUnifier.fs
+++ b/Jennisys/MethodUnifier.fs
@@ -2,131 +2,11 @@
open Ast
open AstUtils
+open FixpointSolver
open PrintUtils
open Resolver
open Utils
-exception CannotUnify
-
-type UnifDirection = LTR | RTL
-
-let rec UnifyImplies lhs rhs dir unifs =
- ///
- let __AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)
- ///
- let __UnifLists lstL lstR =
- if List.length lstL = List.length lstR then
- try
- let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with
- | Some(u) -> u
- | None -> raise CannotUnify) unifs lstL lstR
- Some(unifs2)
- with
- | CannotUnify -> None
- else
- None
- ///
- let __ApplyUnifs unifs exprList =
- exprList |> List.fold (fun acc e ->
- let e' = e |> Rewrite (fun e ->
- match e with
- | VarLiteral(id) when Map.containsKey id unifs -> Some(unifs |> Map.find id)
- | _ -> None)
- acc |> Set.add e'
- ) Set.empty
-
- if lhs = FalseLiteral || rhs = TrueLiteral then
- Some(unifs)
- else
- try
- let l,r = match dir with
- | LTR -> lhs,rhs
- | RTL -> rhs,lhs
- match l, r with
- | VarLiteral(vname), rhs -> __AddOrNone unifs vname rhs
- | IntLiteral(nL), IntLiteral(nR) when nL = nR ->
- Some(unifs)
- | BoolLiteral(bL), BoolLiteral(bR) when bL = bR ->
- Some(unifs)
- | SetExpr(elistL), SetExpr(elistR) ->
- let s1 = elistL |> __ApplyUnifs unifs
- let s2 = elistR |> Set.ofList
- if (s1 = s2) then
- Some(unifs)
- else
- __UnifLists elistL elistR
- | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->
- __UnifLists elistL elistR
- | _ when l = r ->
- Some(unifs)
- | _ ->
- let __InvOps op1 op2 = match op1, op2 with "<" , ">" | ">" , "<" | "<=", ">=" | ">=", "<=" -> true | _ -> false
- let __ImpliesOp op1 op2 =
- match op1, op2 with
- | "<" , "!=" | ">" , "!=" -> true
- | "=" , ">=" | "=" , "<=" -> true
- | _ -> false
- let __CommOp op = match op with "=" | "!=" -> true | _ -> false
-
- let __TryUnifyPair x1 a1 x2 a2 unifs =
- let builder = new CascadingBuilder<_>(None)
- builder {
- let! unifsLhs = UnifyImplies x1 a1 dir unifs
- let! unifsRhs = UnifyImplies x2 a2 dir unifsLhs
- return Some(unifsRhs)
- }
-
- // target implies candidate!
- let rec ___f2 consequence premise unifs =
- match consequence, premise with
- // same operators + commutative -> try both
- | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC && __CommOp opT ->
- match __TryUnifyPair lhsC lhsT rhsC rhsT unifs with
- | Some(x) -> Some(x)
- | None -> __TryUnifyPair lhsC rhsT rhsC lhsT unifs
- // operators are the same
- | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opC = opT ->
- __TryUnifyPair lhsC lhsT rhsC rhsT unifs
- // operators are exactly the invers of one another
- | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when __InvOps opC opT ->
- __TryUnifyPair lhsC rhsT rhsC lhsT unifs
- //
- | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when __ImpliesOp opC opT ->
- __TryUnifyPair lhsC lhsT rhsC rhsT unifs
- | UnaryExpr(opC, subC), UnaryExpr(opP, subP) when opC = opP ->
- UnifyImplies subP subC dir unifs
- | _ -> None
-
- let rec ___f1 targetLst candidateLst unifs =
- match targetLst, candidateLst with
- | targetExpr :: targetRest, candExpr :: candRest ->
- // trying to find a unification for "targetExpr"
- let uOpt = match ___f2 targetExpr candExpr unifs with
- // found -> just return
- | Some(unifs2) -> Some(unifs2)
- // not found -> keep looking in the rest of the candidate expressions
- | None -> ___f1 [targetExpr] candRest unifs
- match uOpt with
- // found -> try find for the rest of the target expressions
- | Some(unifs2) -> ___f1 targetRest candidateLst unifs2
- // not found -> fail
- | None -> None
- | targetExpr :: _, [] ->
- // no more candidates for unification for this targetExpr -> fail
- None
- | [], _ ->
- // we've found unifications for all target expressions -> return the current unifications map
- Some(unifs)
-
- let __HasSetExpr e = DescendExpr2 (fun ex acc -> if acc then true else match ex with SetExpr(_) -> true | _ -> false) e false
- let __PreprocSplitSort e = e |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts |> List.sortBy (fun e -> if __HasSetExpr e then 1 else 0)
- let lhsConjs = lhs |> __PreprocSplitSort
- let rhsConjs = rhs |> __PreprocSplitSort
- ___f1 rhsConjs lhsConjs unifs
- with
- | KeyAlreadyExists
- | CannotUnify -> None
-
let TryUnify targetMthd candMethod =
let targetPre,targetPost = GetMethodPrePost targetMthd
let candPre,candPost = GetMethodPrePost candMethod
@@ -181,6 +61,9 @@ let ApplyMethodUnifs receiver (c,m) unifs =
let mcall = ArbitraryStatement(Assign(VarDeclExpr(retVars, true), mcallExpr))
mcall :: asgs
+// ====================================================
+///
+// ====================================================
let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
let __Calls caller callee =
let keyOpt = callGraph |> Map.tryFindKey (fun (cc,mm) mset -> CheckSameMethods (comp,caller) (cc,mm))
@@ -207,12 +90,14 @@ let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
let modObjs = if IsModifiableObj obj m then Set.singleton obj else Set.empty
let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs
let hInst = { objs = Utils.MapSingleton obj.name obj;
- modifiableObjs = modObjs;
- assignments = body;
- concreteValues = body;
- methodArgs = Map.empty;
- methodRetVals = Map.empty;
- globals = Map.empty }
+ modifiableObjs = modObjs;
+ assignments = body;
+ concreteValues = body;
+ methodArgs = Map.empty;
+ methodRetVals = Map.empty;
+ concreteMethodRetVals = Map.empty;
+ globals = Map.empty }
Some(Map.empty |> Map.add (comp,m) [cond, hInst]
|> Map.add (comp,m') [])
- | None -> None \ No newline at end of file
+ | None -> None
+
diff --git a/Jennisys/Modularizer.fs b/Jennisys/Modularizer.fs
index c6fcaaec..44ac7b80 100644
--- a/Jennisys/Modularizer.fs
+++ b/Jennisys/Modularizer.fs
@@ -32,19 +32,7 @@ let MergeSolutions sol1 sol2 =
///
// ===========================================
let rec MakeModular indent prog comp meth cond hInst callGraph =
- let rec __AddDirectChildren e acc =
- match e with
- | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e
- | SequenceExpr(elist)
- | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc
- | _ -> acc
-
- 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 (__GetDirectModifiableChildren)
+ let directChildren = lazy (GetDirectModifiableChildren hInst)
let __IsAbstractField ty var =
let builder = CascadingBuilder<_>(false)
@@ -164,10 +152,6 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
let initChildrenExprList = delegateMethods |> Map.toList
|> List.map (fun (_, (_,_,asgs)) -> asgs)
|> List.concat
-//TODO(remove)
-// let key = __FindObj (Printer.PrintExpr 0 receiver), Var("", None)
-// let e = MethodCall(receiver, GetMethodName mthd, fst args)
-// FieldAssignment(key, e))
let newAssgns = hInst.assignments |> List.filter (function FieldAssignment((obj,_),_) -> obj.name = "this" | _ -> false)
let newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->
(c,newMthd) :: acc
@@ -177,7 +161,7 @@ let rec MakeModular indent prog comp meth cond hInst callGraph =
(* --- function body starts here --- *)
let idt = Indent indent
if Options.CONFIG.genMod then
- Logger.InfoLine (idt + " - delegating to method calls ...")
+ Logger.InfoLine (idt + " - delegating to method calls ...")
// first try to find a match for the entire method (based on the given solution)
let postSpec = __GetSpecFor "this"
let meth' = match meth with
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index 711298f9..34920bff 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -20,13 +20,14 @@ type AssignmentType =
| ArbitraryStatement of Stmt
type HeapInstance = {
- objs: Map<string, Obj>;
- modifiableObjs: Set<Obj>;
- assignments: AssignmentType list;
- concreteValues: AssignmentType list;
- methodArgs: Map<string, Const>;
- methodRetVals: Map<string, Expr>;
- globals: Map<string, Expr>;
+ objs : Map<string, Obj>;
+ modifiableObjs : Set<Obj>;
+ assignments : AssignmentType list;
+ concreteValues : AssignmentType list;
+ methodArgs : Map<string, Const>;
+ methodRetVals : Map<string, Expr>;
+ concreteMethodRetVals : Map<string, Expr>;
+ globals : Map<string, Expr>;
}
let NoObj = { name = ""; objType = NamedType("", []) }
@@ -119,74 +120,87 @@ let Resolve hModel cst =
// ==================================================================
/// Evaluates a given expression with respect to a given heap instance
// ==================================================================
-let Eval heapInst resolveExprFunc expr =
- 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
- (* --- 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 ->
- match expr with
- | ObjLiteral("this") | ObjLiteral("null") -> expr
- | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO
- | VarLiteral(id) ->
- match heapInst.methodArgs |> Map.tryFind id with
- | Some(argValue) -> argValue |> Const2Expr
- | None ->
- match heapInst.methodRetVals |> Map.tryFind id with
- | Some(e) -> e |> __FurtherResolve
- | None -> raise (EvalFailed("cannot find value for method parameter " + id))
- | IdLiteral(id) ->
- let globalVal = heapInst.globals |> Map.tryFind id
- match globalVal with
- | Some(e) -> e
- | 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 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) :: [] -> __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)
+let rec _EvalResolver heapInst 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 heapInst useConcrete resolveExprFunc expr None
+ with
+ | _ -> expr
+ | IdLiteral(id) when not (id = "this" || id = "null") ->
+ try
+ _EvalResolver heapInst useConcrete resolveExprFunc expr None
+ with
+ | _ -> expr
+ | _ -> expr
+
+ (* --- 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 ->
+ match expr with
+ | ObjLiteral("this") | ObjLiteral("null") -> expr
+ | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO
+ | VarLiteral(id) ->
+ match heapInst.methodArgs |> Map.tryFind id with
+ | Some(argValue) -> argValue |> Const2Expr
+ | None ->
+ let retVals = if useConcrete then heapInst.concreteMethodRetVals else heapInst.methodRetVals
+ match retVals |> Map.tryFind id with
+ | Some(e) -> e |> __FurtherResolve
+ | None -> raise (EvalFailed("cannot find value for method parameter " + id))
+ | IdLiteral(id) ->
+ let globalVal = heapInst.globals |> Map.tryFind id
+ match globalVal with
+ | Some(e) -> e
+ | None -> _EvalResolver heapInst useConcrete resolveExprFunc ThisLiteral (Some(id))
+ | _ -> raise (EvalFailed(sprintf "I'm not supposed to resolve %O" expr))
+ | Some(fldName) ->
+ match expr with
+ | ObjLiteral(objName) ->
+ 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) :: [] -> __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)
+let _Eval heapInst resolveExprFunc returnFunc expr =
(* --- function body starts here --- *)
//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
+ EvalSymRet (_EvalResolver heapInst false resolveExprFunc) returnFunc expr
+
+/// Resolves everything
+let EvalFull heapInst expr =
+ EvalSym (_EvalResolver heapInst true (fun e -> true)) expr
+ //_Eval heapInst (fun _ -> true) (fun e -> e) expr
+
+let EvalAndCheckTrue heapInst resolveExprFunc expr =
+ let returnFunc = fun expr ->
+ // TODO: this is just to ensure that all field accesses to this object are prefixed with "this."
+ // this is not the best place to do it, though
+ let expr = match expr with IdLiteral(id) -> Dot(ThisLiteral, id) | _ -> expr
+ // TODO: infer type of expr and then re-execute only if its type is Bool
+ let e1 = EvalFull heapInst expr //EvalSym (_EvalResolver heapInst true (fun _ -> true)) expr
+ match e1 with
+ | BoolLiteral(b) ->
+ if b then
+ expr
+ else
+ FalseLiteral
+ | _ -> expr
+ EvalSymRet (_EvalResolver heapInst false resolveExprFunc) returnFunc expr
+ //_Eval heapInst resolveExprFunc returnFunc expr
// =====================================================================
/// Takes an unresolved model of the heap (HeapModel), resolves all
@@ -229,13 +243,14 @@ let ResolveModel hModel meth =
acc1 |> Map.add name resolvedValExpr, acc2
| _ -> acc1, acc2
) (Map.empty, Map.empty)
- { objs = objs;
- modifiableObjs = modObjs;
- assignments = hmap;
- concreteValues = hmap;
- methodArgs = argmap;
- methodRetVals = retvals;
- globals = Map.empty }
+ { objs = objs;
+ modifiableObjs = modObjs;
+ assignments = hmap;
+ concreteValues = hmap;
+ methodArgs = argmap;
+ methodRetVals = retvals;
+ concreteMethodRetVals = retvals;
+ globals = Map.empty }
let rec GetCallGraph solutions graph =
let rec __SearchExprsForMethodCalls elist acc =
@@ -264,6 +279,8 @@ let rec GetCallGraph solutions graph =
//////////////////////////////
+//TODO: below here should really go to a different module
+
let Is1stLevelExpr heapInst expr =
DescendExpr2 (fun expr acc ->
if not acc then
@@ -271,7 +288,7 @@ let Is1stLevelExpr heapInst expr =
else
match expr with
| Dot(discr, fldName) ->
- let obj = Eval heapInst (fun _ -> true) discr
+ let obj = EvalFull heapInst discr
match obj with
| ObjLiteral(id) -> id = "this"
| _ -> failwithf "Didn't expect the discriminator of a Dot to not be ObjLiteral"
@@ -290,4 +307,22 @@ let IsSolution1stLevelOnly heapInst =
| Block(stmts) -> __IsSol1stLevel (stmts @ rest)
| [] -> true
(* --- function body starts here --- *)
- __IsSol1stLevel (ConvertToStatements heapInst true) \ No newline at end of file
+ __IsSol1stLevel (ConvertToStatements heapInst true)
+
+/// Returns a list of direct modifiable children objects with respect to "this" object
+///
+/// All returned expressions are of type ObjLiteral
+///
+/// ensures: forall e :: e in ret ==> e is ObjInstance
+let GetDirectModifiableChildren hInst =
+ let rec __AddDirectChildren e acc =
+ match e with
+ | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e
+ | SequenceExpr(elist)
+ | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc
+ | _ -> acc
+
+ (* --- function body starts here --- *)
+ 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
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index 5cd8af9d..dcb13f08 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -86,6 +86,20 @@ let ListDeduplicate lst =
__Dedup rest visitedSet newAcc
| _ -> acc
__Dedup lst (new System.Collections.Generic.HashSet<_>()) []
+
+let rec ListCombine combinerFunc lst1 lst2 =
+ match lst1 with
+ | e1 :: rest ->
+ let resLst1 = lst2 |> List.fold (fun acc e2 -> acc @ [combinerFunc e1 e2]) []
+ List.concat [resLst1; ListCombine combinerFunc rest lst2]
+ | [] -> []
+
+let rec ListCombineMult combinerFunc lst1 lst2 =
+ match lst1 with
+ | e1 :: rest ->
+ let resLst1 = lst2 |> List.fold (fun acc e2 -> acc @ combinerFunc e1 e2) []
+ List.concat [resLst1; ListCombineMult combinerFunc rest lst2]
+ | [] -> []
// =============================================================
/// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])
diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index e056bcfa..fe79c671 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -49,6 +49,7 @@ class Node[T] {
method Get(idx: int) returns (ret: T)
requires idx >= 0 && idx < |list|
+ requires idx >= 1 && next != null
ensures ret = list[idx]
}
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index 0bd42701..6a447331 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -4,6 +4,9 @@ class Set {
constructor Empty()
ensures elems = {}
+ constructor SingletonZero()
+ ensures elems = {0}
+
constructor Singleton(t: int)
ensures elems = {t}
diff --git a/Jennisys/examples/Set2.jen b/Jennisys/examples/Set2.jen
new file mode 100644
index 00000000..cfbcbce7
--- /dev/null
+++ b/Jennisys/examples/Set2.jen
@@ -0,0 +1,60 @@
+class Set { var elems: seq[int]
+
+ constructor Empty()
+ ensures elems = []
+
+ constructor Singleton(t: int)
+ ensures elems = [t]
+
+ constructor Sum(p: int, q: int)
+ ensures elems = [p + q]
+
+}
+
+model Set {
+ var root: SetNode
+
+ frame
+ root
+
+ invariant
+ root = null ==> elems = []
+ root != null ==> elems = root.elems
+}
+
+class SetNode {
+ var elems: seq[int]
+
+ constructor Init(x: int)
+ ensures elems = [x]
+
+ constructor Double(a: int, b: int)
+ requires a != b
+ ensures |elems| = 2 && a in elems && b in elems
+
+ constructor DoubleBase(x: int, y: int)
+ requires x < y
+ ensures elems = [x y]
+
+ constructor Triple(x: int, y: int, z: int)
+ requires x != y && y != z && z != x
+ ensures |elems| = 3 && x in elems && y in elems && z in elems
+
+ constructor TripleBase(x: int, y: int, z: int)
+ requires x < y && y < z
+ ensures elems = [x y z]
+}
+
+model SetNode {
+ var data: int
+ var left: SetNode
+ var right: SetNode
+
+ frame
+ left * right
+
+ invariant
+ elems = (left != null ? left.elems : []) + [data] + (right != null ? right.elems : [])
+ left != null ==> forall e :: e in left.elems ==> e < data
+ right != null ==> forall e :: e in right.elems ==> e > data
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:01:10 +0000