Mercurial > urweb
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')]*) |