Mercurial > urweb

comparison src/iflow.sml @ 1200:5eac14322548

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generated basic dummy Iflow conditions
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Apr 2010 14:37:19 -0400
parents
children 8793fd48968c
comparison
equal deleted inserted replaced
1199:c316ca3c9ec6 1200:5eac14322548
1 (* Copyright (c) 2010, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure Iflow :> IFLOW = struct
29
30 open Mono
31
32 structure SS = BinarySetFn(struct
33 type ord_key = string
34 val compare = String.compare
35 end)
36
37 val writers = ["htmlifyInt_w",
38 "htmlifyFloat_w",
39 "htmlifyString_w",
40 "htmlifyBool_w",
41 "htmlifyTime_w",
42 "attrifyInt_w",
43 "attrifyFloat_w",
44 "attrifyString_w",
45 "attrifyChar_w",
46 "urlifyInt_w",
47 "urlifyFloat_w",
48 "urlifyString_w",
49 "urlifyBool_w"]
50
51 val writers = SS.addList (SS.empty, writers)
52
53 type lvar = int
54
55 datatype exp =
56 Const of Prim.t
57 | Var of int
58 | Lvar of lvar
59 | Func of string * exp list
60 | Recd of (string * exp) list
61 | Proj of exp * string
62 | Finish
63
64 datatype reln =
65 Sql of string
66 | Eq
67
68 datatype prop =
69 True
70 | False
71 | Unknown
72 | And of prop * prop
73 | Or of prop * prop
74 | Reln of reln * exp list
75 | Select of int * lvar * lvar * prop * exp
76
77 local
78 val count = ref 0
79 in
80 fun newLvar () =
81 let
82 val n = !count
83 in
84 count := n + 1;
85 n
86 end
87 end
88
89 fun subExp (v, lv) =
90 let
91 fun sub e =
92 case e of
93 Const _ => e
94 | Var v' => if v' = v then Lvar lv else e
95 | Lvar _ => e
96 | Func (f, es) => Func (f, map sub es)
97 | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
98 | Proj (e, s) => Proj (sub e, s)
99 | Finish => Finish
100 in
101 sub
102 end
103
104 fun subProp (v, lv) =
105 let
106 fun sub p =
107 case p of
108 True => p
109 | False => p
110 | Unknown => p
111 | And (p1, p2) => And (sub p1, sub p2)
112 | Or (p1, p2) => Or (sub p1, sub p2)
113 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
114 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
115 in
116 sub
117 end
118
119 fun eq' (e1, e2) =
120 case (e1, e2) of
121 (Const p1, Const p2) => Prim.equal (p1, p2)
122 | (Var n1, Var n2) => n1 = n2
123 | (Lvar n1, Lvar n2) => n1 = n2
124 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
125 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
126 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
127 | (Finish, Finish) => true
128 | _ => false
129
130 fun isKnown e =
131 case e of
132 Const _ => true
133 | Func (_, es) => List.all isKnown es
134 | Recd xes => List.all (isKnown o #2) xes
135 | Proj (e, _) => isKnown e
136 | _ => false
137
138 fun isFinish e =
139 case e of
140 Finish => true
141 | _ => false
142
143 fun simplify e =
144 case e of
145 Const _ => e
146 | Var _ => e
147 | Lvar _ => e
148 | Func (f, es) =>
149 let
150 val es = map simplify es
151 in
152 if List.exists isFinish es then
153 Finish
154 else
155 Func (f, es)
156 end
157 | Recd xes =>
158 let
159 val xes = map (fn (x, e) => (x, simplify e)) xes
160 in
161 if List.exists (isFinish o #2) xes then
162 Finish
163 else
164 Recd xes
165 end
166 | Proj (e, s) =>
167 (case simplify e of
168 Recd xes =>
169 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
170 | e' =>
171 if isFinish e' then
172 Finish
173 else
174 Proj (e', s))
175 | Finish => Finish
176
177 fun eq (e1, e2) = eq' (simplify e1, simplify e2)
178
179 fun decomp or =
180 let
181 fun decomp p k =
182 case p of
183 True => k []
184 | False => true
185 | Unknown => k []
186 | And (p1, p2) =>
187 decomp p1 (fn ps1 =>
188 decomp p2 (fn ps2 =>
189 k (ps1 @ ps2)))
190 | Or (p1, p2) =>
191 or (decomp p1 k, fn () => decomp p2 k)
192 | Reln x => k [x]
193 | Select _ => k []
194 in
195 decomp
196 end
197
198 fun rimp ((r1 : reln, es1), (r2, es2)) =
199 r1 = r2 andalso ListPair.allEq eq (es1, es2)
200
201 fun imp (p1, p2) =
202 decomp (fn (e1, e2) => e1 andalso e2 ()) p1
203 (fn hyps =>
204 decomp (fn (e1, e2) => e1 orelse e2 ()) p2
205 (fn goals =>
206 List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals))
207
208 fun patCon pc =
209 case pc of
210 PConVar n => "C" ^ Int.toString n
211 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
212
213 exception Summaries of (string * exp * prop * (exp * prop) list) list
214
215 datatype chunk =
216 String of string
217 | Exp of Mono.exp
218
219 fun chunkify e =
220 case #1 e of
221 EPrim (Prim.String s) => [String s]
222 | EStrcat (e1, e2) => chunkify e1 @ chunkify e2
223 | _ => [Exp e]
224
225 fun queryProp rv e =
226 let
227 fun query chs =
228 case chs of
229 [] => raise Fail "Iflow: Empty query"
230 | Exp _ :: _ => Unknown
231 | String "" :: chs => query chs
232 | String s :: chs => True
233 in
234 query (chunkify e)
235 end
236
237 fun evalExp env (e : Mono.exp, st as (nv, p, sent)) =
238 let
239 fun default () =
240 (Var nv, (nv+1, p, sent))
241
242 fun addSent (p, e, sent) =
243 if isKnown e then
244 sent
245 else
246 (e, p) :: sent
247 in
248 case #1 e of
249 EPrim p => (Const p, st)
250 | ERel n => (List.nth (env, n), st)
251 | ENamed _ => default ()
252 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
253 | ECon (_, pc, SOME e) =>
254 let
255 val (e, st) = evalExp env (e, st)
256 in
257 (Func (patCon pc, [e]), st)
258 end
259 | ENone _ => (Func ("None", []), st)
260 | ESome (_, e) =>
261 let
262 val (e, st) = evalExp env (e, st)
263 in
264 (Func ("Some", [e]), st)
265 end
266 | EFfi _ => default ()
267 | EFfiApp (m, s, es) =>
268 if m = "Basis" andalso SS.member (writers, s) then
269 let
270 val (es, st) = ListUtil.foldlMap (evalExp env) st es
271 in
272 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
273 end
274 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
275 default ()
276 else
277 let
278 val (es, st) = ListUtil.foldlMap (evalExp env) st es
279 in
280 (Func (m ^ "." ^ s, es), st)
281 end
282 | EApp _ => default ()
283 | EAbs _ => default ()
284 | EUnop (s, e1) =>
285 let
286 val (e1, st) = evalExp env (e1, st)
287 in
288 (Func (s, [e1]), st)
289 end
290 | EBinop (s, e1, e2) =>
291 let
292 val (e1, st) = evalExp env (e1, st)
293 val (e2, st) = evalExp env (e2, st)
294 in
295 (Func (s, [e1, e2]), st)
296 end
297 | ERecord xets =>
298 let
299 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
300 let
301 val (e, st) = evalExp env (e, st)
302 in
303 ((x, e), st)
304 end) st xets
305 in
306 (Recd xes, st)
307 end
308 | EField (e, s) =>
309 let
310 val (e, st) = evalExp env (e, st)
311 in
312 (Proj (e, s), st)
313 end
314 | ECase _ => default ()
315 | EStrcat (e1, e2) =>
316 let
317 val (e1, st) = evalExp env (e1, st)
318 val (e2, st) = evalExp env (e2, st)
319 in
320 (Func ("cat", [e1, e2]), st)
321 end
322 | EError _ => (Finish, st)
323 | EReturnBlob {blob = b, mimeType = m, ...} =>
324 let
325 val (b, st) = evalExp env (b, st)
326 val (m, st) = evalExp env (m, st)
327 in
328 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
329 end
330 | ERedirect (e, _) =>
331 let
332 val (e, st) = evalExp env (e, st)
333 in
334 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
335 end
336 | EWrite e =>
337 let
338 val (e, st) = evalExp env (e, st)
339 in
340 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
341 end
342 | ESeq (e1, e2) =>
343 let
344 val (_, st) = evalExp env (e1, st)
345 in
346 evalExp env (e2, st)
347 end
348 | ELet (_, _, e1, e2) =>
349 let
350 val (e1, st) = evalExp env (e1, st)
351 in
352 evalExp (e1 :: env) (e2, st)
353 end
354 | EClosure (n, es) =>
355 let
356 val (es, st) = ListUtil.foldlMap (evalExp env) st es
357 in
358 (Func ("Cl" ^ Int.toString n, es), st)
359 end
360
361 | EQuery {query = q, body = b, initial = i, ...} =>
362 let
363 val (_, st) = evalExp env (q, st)
364 val (i, st) = evalExp env (i, st)
365
366 val r = #1 st
367 val acc = #1 st + 1
368 val st' = (#1 st + 2, #2 st, #3 st)
369
370 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
371
372 val r' = newLvar ()
373 val acc' = newLvar ()
374 val qp = queryProp r' q
375
376 val doSubExp = subExp (r, r') o subExp (acc, acc')
377 val doSubProp = subProp (r, r') o subProp (acc, acc')
378
379 val p = doSubProp (#2 st')
380 val p = And (p, qp)
381 val p = Select (r, r', acc', p, doSubExp b)
382 in
383 (Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st')))
384 end
385 | EDml _ => default ()
386 | ENextval _ => default ()
387 | ESetval _ => default ()
388
389 | EUnurlify _ => default ()
390 | EJavaScript _ => default ()
391 | ESignalReturn _ => default ()
392 | ESignalBind _ => default ()
393 | ESignalSource _ => default ()
394 | EServerCall _ => default ()
395 | ERecv _ => default ()
396 | ESleep _ => default ()
397 | ESpawn _ => default ()
398 end
399
400 fun check file =
401 let
402 fun decl ((d, _), summaries) =
403 case d of
404 DVal (x, _, _, e, _) =>
405 let
406 fun deAbs (e, env, nv) =
407 case #1 e of
408 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
409 | _ => (e, env, nv)
410
411 val (e, env, nv) = deAbs (e, [], 0)
412
413 val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
414 in
415 (x, e, p, sent) :: summaries
416 end
417 | _ => summaries
418 in
419 raise Summaries (foldl decl [] file)
420 end
421
422 end