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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
|
module MethodUnifier
open Ast
open AstUtils
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
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(name,_)) ->
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.NewSym
let v = Var(vname, None)
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), 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 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;
methodArgs = Map.empty;
methodRetVals = Map.empty;
globals = Map.empty }
Some(Map.empty |> Map.add (comp,m) [cond, hInst]
|> Map.add (comp,m') [])
| None -> None
|
