diff options
| author |  Aleksandar Milicevic <unknown> | 2011-08-22 23:05:37 -0700 |
|---|---|---|
| committer | Aleksandar Milicevic <unknown> | 2011-08-22 23:05:37 -0700 |
| commit | 966cf286c467d57402cb580b788a079b9c0d54b2 (patch) | |
| tree | 6e848ffd57840638f8aa67236e4fae3233491dc3 /Jennisys/Jennisys | |
| parent | 0336c0b486aaf61b1ecb7ba43c15b8e133b83844 (diff) | |
Jennisys: changed the Combiner method to produce more
combinations, so now List.Find works
Diffstat (limited to 'Jennisys/Jennisys')
| -rw-r--r-- | Jennisys/Jennisys/Analyzer.fs | 6 | ||||
| -rw-r--r-- | Jennisys/Jennisys/FixpointSolver.fs | 53 |
2 files changed, 27 insertions, 32 deletions
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index 70b36fb8..ec8a57c6 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -742,11 +742,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = false
with
| _ -> true)
- let specConds = (specConds1 @ specConds2) |> List.map (fun e ->
- PrintExpr 0 e |> Logger.TraceLine
- let e' = SimplifyExpr e
- PrintExpr 0 e' |> Logger.TraceLine
- e')
+ let specConds = (specConds1 @ specConds2) |> List.map SimplifyExpr
let aliasingCond = lazy(DiscoverAliasing (methodArgs |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst)
let argConds = heapInst.methodArgs |> Map.fold (fun acc name value -> acc @ [BinaryEq (VarLiteral(name)) (Const2Expr value)]) []
let allConds = GetAllPossibleConditions specConds argConds [aliasingCond.Force()]
diff --git a/Jennisys/Jennisys/FixpointSolver.fs b/Jennisys/Jennisys/FixpointSolver.fs index 60b01192..c1cb1ba4 100644 --- a/Jennisys/Jennisys/FixpointSolver.fs +++ b/Jennisys/Jennisys/FixpointSolver.fs @@ -267,33 +267,32 @@ let rec ComputeClosure heapInst premises = __fff lhs rhs
let rec __CombineAllMatches expr premises =
- match expr with
- | BinaryExpr(p,op,lhs,rhs) ->
- let lhsMatches = __CombineAllMatches lhs premises
- let rhsMatches = __CombineAllMatches rhs premises
- let lst1 = Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches
- let lst2 =
- if op = "in" then
- Utils.ListCombineMult BinaryInCombiner lhsMatches rhsMatches
- elif op = "!in" then
- Utils.ListCombineMult BinaryNotInCombiner lhsMatches rhsMatches
- else
- []
- lst1 @ lst2
- | UnaryExpr(op,sub) ->
- __CombineAllMatches sub premises |> List.map (fun e -> UnaryExpr(op,e))
- | SelectExpr(lst,idx) ->
- let lst1 = FindMatches expr bogusExpr premises
- let lstMatches = __CombineAllMatches lst premises
- let idxMatches = __CombineAllMatches idx premises
- let lst2 = Utils.ListCombineMult SelectExprCombinerFunc lstMatches idxMatches
- lst1 @ lst2
- | SeqLength(lst) ->
- let lst1 = FindMatches expr bogusExpr premises
- let lst2 = __CombineAllMatches lst premises |> List.map SeqLenCombinerFunc |> List.concat
- lst1 @ lst2
- // TODO: other cases
- | _ -> expr :: (FindMatches expr bogusExpr premises)
+ let lst0 = FindMatches expr bogusExpr premises
+ let lstCombined =
+ match expr with
+ | BinaryExpr(p,op,lhs,rhs) ->
+ let lhsMatches = __CombineAllMatches lhs premises
+ let rhsMatches = __CombineAllMatches rhs premises
+ let lst1 = Utils.ListCombine (fun e1 e2 -> BinaryExpr(p,op,e1,e2)) lhsMatches rhsMatches
+ let lst2 =
+ if op = "in" then
+ Utils.ListCombineMult BinaryInCombiner lhsMatches rhsMatches
+ elif op = "!in" then
+ Utils.ListCombineMult BinaryNotInCombiner lhsMatches rhsMatches
+ else
+ []
+ lst1 @ lst2
+ | 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 :: (lst0 @ lstCombined)
let rec __ExpandPremise expr premises =
let __AddToPremisses exprLst premises = exprLst |> List.fold (fun acc e -> MySetAdd e acc) premises
|