comparison src/especialize.sml @ 1077:a3273bee05a9

Initial generalization of Especialize, with security bug known
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Dec 2009 12:26:00 -0500
parents 066493f7f008
children b9321bcefb42
comparison
equal deleted inserted replaced
1076:dcf98ae3c48d 1077:a3273bee05a9
77 pof (pos + 1, ls') 77 pof (pos + 1, ls')
78 in 78 in
79 pof (0, ls) 79 pof (0, ls)
80 end 80 end
81 81
82 fun squish fvs = 82 fun squish (untouched, fvs) =
83 U.Exp.mapB {kind = fn _ => fn k => k, 83 U.Exp.mapB {kind = fn _ => fn k => k,
84 con = fn _ => fn c => c, 84 con = fn _ => fn c => c,
85 exp = fn bound => fn e => 85 exp = fn bound => fn e =>
86 case e of 86 case e of
87 ERel x => 87 ERel x =>
88 if x >= bound then 88 if x >= bound then
89 ERel (positionOf (x - bound, fvs) + bound) 89 ERel (positionOf (x - bound, fvs) + bound + untouched)
90 else 90 else
91 e 91 e
92 | _ => e, 92 | _ => e,
93 bind = fn (bound, b) => 93 bind = fn (bound, b) =>
94 case b of 94 case b of
163 | CFfi ("Basis", "sql_injectable_prim") => true 163 | CFfi ("Basis", "sql_injectable_prim") => true
164 | CFfi ("Basis", "sql_injectable") => true 164 | CFfi ("Basis", "sql_injectable") => true
165 | _ => false} 165 | _ => false}
166 val loc = ErrorMsg.dummySpan 166 val loc = ErrorMsg.dummySpan
167 167
168 fun findSplit (xs, typ, fxs, fvs) = 168 fun findSplit (xs, typ, fxs, fvs, ts) =
169 case (#1 typ, xs) of 169 case (#1 typ, xs) of
170 (TFun (dom, ran), e :: xs') => 170 (TFun (dom, ran), e :: xs') =>
171 if functionInside dom then 171 if functionInside dom then
172 findSplit (xs', 172 findSplit (xs',
173 ran, 173 ran,
174 e :: fxs, 174 (true, e) :: fxs,
175 IS.union (fvs, freeVars e)) 175 IS.union (fvs, freeVars e),
176 ts)
176 else 177 else
177 (rev fxs, xs, fvs) 178 findSplit (xs', ran, (false, e) :: fxs, fvs, dom :: ts)
178 | _ => (rev fxs, xs, fvs) 179 | _ => (List.revAppend (fxs, map (fn e => (false, e)) xs), fvs, rev ts)
179 180
180 val (fxs, xs, fvs) = findSplit (xs, typ, [], IS.empty) 181 val (xs, fvs, ts) = findSplit (xs, typ, [], IS.empty, [])
181 182 val fxs = List.mapPartial (fn (true, e) => SOME e | _ => NONE) xs
182 val fxs' = map (squish (IS.listItems fvs)) fxs 183 val untouched = length (List.filter (fn (false, _) => true | _ => false) xs)
183 184 val squish = squish (untouched, IS.listItems fvs)
184 fun firstRel () = 185 val fxs' = map squish fxs
185 case fxs' of
186 (ERel _, _) :: _ => true
187 | _ => false
188 in 186 in
189 (*Print.preface ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs');*) 187 (*Print.preface ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs');*)
190 if firstRel () 188 if List.all (fn (false, _) => true
191 orelse List.all (fn (ERel _, _) => true 189 | (true, (ERel _, _)) => true
192 | _ => false) fxs' then 190 | _ => false) xs then
193 (e, st) 191 (e, st)
194 else 192 else
195 case (KM.find (args, fxs'), SS.member (!mayNotSpec, name)) of 193 case (KM.find (args, fxs'), SS.member (!mayNotSpec, name)) of
196 (SOME f', _) => 194 (SOME f', _) =>
197 let 195 let
198 val e = (ENamed f', loc) 196 val e = (ENamed f', loc)
199 val e = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc)) 197 val e = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
200 e fvs 198 e fvs
201 val e = foldl (fn (arg, e) => (EApp (e, arg), loc)) 199 val e = foldl (fn ((false, arg), e) => (EApp (e, arg), loc)
200 | (_, e) => e)
202 e xs 201 e xs
203 in 202 in
204 (*Print.prefaces "Brand new (reuse)" 203 (*Print.prefaces "Brand new (reuse)"
205 [("e'", CorePrint.p_exp CoreEnv.empty e)];*) 204 [("e'", CorePrint.p_exp CoreEnv.empty e)];*)
206 (#1 e, st) 205 (#1 e, st)
218 217
219 (*val () = Print.prefaces ("Yes(" ^ name ^ ")") 218 (*val () = Print.prefaces ("Yes(" ^ name ^ ")")
220 [("fxs'", 219 [("fxs'",
221 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')]*) 220 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')]*)
222 221
223 fun subBody (body, typ, fxs') = 222 fun subBody (body, typ, xs) =
224 case (#1 body, #1 typ, fxs') of 223 case (#1 body, #1 typ, xs) of
225 (_, _, []) => SOME (body, typ) 224 (_, _, []) => SOME (body, typ)
226 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: fxs'') => 225 | (EAbs (_, _, _, body'), TFun (_, typ'), (b, x) :: xs) =>
227 let 226 let
228 val body'' = E.subExpInExp (0, x) body' 227 val body'' =
228 if b then
229 E.subExpInExp (0, squish x) body'
230 else
231 body'
229 in 232 in
230 subBody (body'', 233 subBody (body'',
231 typ', 234 typ',
232 fxs'') 235 xs)
233 end 236 end
234 | _ => NONE 237 | _ => NONE
235 in 238 in
236 case subBody (body, typ, fxs') of 239 case subBody (body, typ, xs) of
237 NONE => (e, st) 240 NONE => (e, st)
238 | SOME (body', typ') => 241 | SOME (body', typ') =>
239 let 242 let
240 val f' = #maxName st 243 val f' = #maxName st
241 val args = KM.insert (args, fxs', f') 244 val args = KM.insert (args, fxs', f')
255 ("f'", CorePrint.p_exp env (ENamed f', loc)), 258 ("f'", CorePrint.p_exp env (ENamed f', loc)),
256 ("xs", Print.p_list (CorePrint.p_exp env) xs), 259 ("xs", Print.p_list (CorePrint.p_exp env) xs),
257 ("fxs'", Print.p_list 260 ("fxs'", Print.p_list
258 (CorePrint.p_exp E.empty) fxs'), 261 (CorePrint.p_exp E.empty) fxs'),
259 ("e", CorePrint.p_exp env (e, loc))]*) 262 ("e", CorePrint.p_exp env (e, loc))]*)
263
264 val (body', typ') = foldr (fn (t, (body', typ')) =>
265 ((EAbs ("x", t, typ', body'), loc),
266 (TFun (t, typ'), loc)))
267 (body', typ') ts
268
260 val (body', typ') = IS.foldl (fn (n, (body', typ')) => 269 val (body', typ') = IS.foldl (fn (n, (body', typ')) =>
261 let 270 let
262 val (x, xt) = List.nth (env, n) 271 val (x, xt) = List.nth (env, n)
263 in 272 in
264 ((EAbs (x, xt, typ', body'), 273 ((EAbs (x, xt, typ', body'),
273 val () = mayNotSpec := mns 282 val () = mayNotSpec := mns
274 283
275 val e' = (ENamed f', loc) 284 val e' = (ENamed f', loc)
276 val e' = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc)) 285 val e' = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
277 e' fvs 286 e' fvs
278 val e' = foldl (fn (arg, e) => (EApp (e, arg), loc)) 287 val e' = foldl (fn ((false, arg), e) => (EApp (e, arg), loc)
288 | (_, e) => e)
279 e' xs 289 e' xs
280 (*val () = Print.prefaces "Brand new" 290 (*val () = Print.prefaces "Brand new"
281 [("e'", CorePrint.p_exp CoreEnv.empty e'), 291 [("e'", CorePrint.p_exp CoreEnv.empty e'),
282 ("e", CorePrint.p_exp CoreEnv.empty (e, loc)), 292 ("e", CorePrint.p_exp CoreEnv.empty (e, loc)),
283 ("body'", CorePrint.p_exp CoreEnv.empty body')]*) 293 ("body'", CorePrint.p_exp CoreEnv.empty body')]*)