1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
module MethodUnifier
open Ast
open Getters
open AstUtils
open FixpointSolver
open PrintUtils
open Resolver
open Utils
let TryUnify targetMthd candMethod =
let targetPre,targetPost = GetMethodPrePost targetMthd
let targetPre = BinaryAnd targetPre (GetMethodGhostPrecondition targetMthd)
let candPre,candPost = GetMethodPrePost candMethod
let candPre = BinaryAnd candPre (GetMethodGhostPrecondition candMethod)
let builder = new CascadingBuilder<_>(None)
builder {
let! unifs1 = UnifyImplies targetPre candPre RTL Map.empty
let! unifs2 = UnifyImplies candPost targetPost LTR unifs1
return Some(unifs2)
}
let rec TryFindAMatch targetMthd candidateMethods =
let targetMthdName = GetMethodName targetMthd
match candidateMethods with
| candMthd :: rest ->
if GetMethodName candMthd = targetMthdName then
// skip if it is the same method
TryFindAMatch targetMthd rest
else
match TryUnify targetMthd candMthd with
| Some(unifs) -> Some(candMthd,unifs)
| None -> TryFindAMatch targetMthd rest
| [] -> None
let TryFindExistingOpt comp targetMthd =
TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers)
let TryFindExisting comp targetMthd =
match TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with
| Some(m,unifs) -> m,unifs
| None -> targetMthd, Map.empty
let ApplyMethodUnifs receiver (c,m) unifs =
let __Apply args = args |> List.map (fun var ->
let name = GetExtVarName var
match Map.tryFind name unifs with
| Some(e) -> e
| None -> VarLiteral(name))
let ins = GetMethodInArgs m |> __Apply
let outs = GetMethodOutArgs m |> __Apply
let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e ->
let vname = SymGen.NewSymFake e
let v = Var(vname, None, false)
let acc1' = acc1 @ [v]
let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))]
acc1', acc2'
) ([],[])
let mcallExpr = MethodCall(receiver, GetComponentName c, GetMethodName m, ins)
match retVars, outs with
| [], [] -> [ArbitraryStatement(ExprStmt(mcallExpr))]
| [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None, false)], false), mcallExpr))]
| _ ->
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))
match keyOpt with
| Some(k) -> callGraph |> Map.find k |> Set.contains ((GetComponentName comp),(GetMethodName callee))
| None -> false
(* --- function body starts here --- *)
if not Options.CONFIG.genMod then
None
else
let idt = Indent indent
let candidateMethods = GetMembers comp |> List.filter (fun cm ->
match cm with
| Method(mname,_,_,_,_) when not (__Calls cm m) -> true
| _ -> false)
match TryFindAMatch m candidateMethods with
| Some(m',unifs) ->
Logger.InfoLine (idt + " - substitution method found:")
Logger.InfoLine (Printer.PrintMethodSignFull (indent+6) comp m')
Logger.DebugLine (idt + " Unifications: ")
let idtt = idt + " "
unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug
let obj = { name = "this"; objType = GetClassType comp }
let modObjs = if IsModifiableObj obj (comp,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;
concreteMethodRetVals = Map.empty;
globals = Map.empty }
Some(Map.empty |> Map.add (comp,m) [cond, hInst]
|> Map.add (comp,m') [])
| None -> None
|
