Mercurial > urweb

comparison src/iflow.sml @ 1254:935a981f4380

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 May 2010 13:57:01 -0400
parents 9d65866ab9ab
children 3d06e0f7a6f3
comparison
equal deleted inserted replaced
1198:b52929351402 1254:935a981f4380
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 IS = IntBinarySet
33 structure IM = IntBinaryMap
34
35 structure SK = struct
36 type ord_key = string
37 val compare = String.compare
38 end
39
40 structure SS = BinarySetFn(SK)
41 structure SM = BinaryMapFn(SK)
42
43 val writers = ["htmlifyInt_w",
44 "htmlifyFloat_w",
45 "htmlifyString_w",
46 "htmlifyBool_w",
47 "htmlifyTime_w",
48 "attrifyInt_w",
49 "attrifyFloat_w",
50 "attrifyString_w",
51 "attrifyChar_w",
52 "urlifyInt_w",
53 "urlifyFloat_w",
54 "urlifyString_w",
55 "urlifyBool_w",
56 "set_cookie"]
57
58 val writers = SS.addList (SS.empty, writers)
59
60 type lvar = int
61
62 datatype func =
63 DtCon0 of string
64 | DtCon1 of string
65 | UnCon of string
66 | Other of string
67
68 datatype exp =
69 Const of Prim.t
70 | Var of int
71 | Lvar of lvar
72 | Func of func * exp list
73 | Recd of (string * exp) list
74 | Proj of exp * string
75
76 datatype reln =
77 Known
78 | Sql of string
79 | PCon0 of string
80 | PCon1 of string
81 | Eq
82 | Ne
83 | Lt
84 | Le
85 | Gt
86 | Ge
87
88 datatype prop =
89 True
90 | False
91 | Unknown
92 | And of prop * prop
93 | Or of prop * prop
94 | Reln of reln * exp list
95 | Cond of exp * prop
96
97 local
98 open Print
99 val string = PD.string
100 in
101
102 fun p_func f =
103 string (case f of
104 DtCon0 s => s
105 | DtCon1 s => s
106 | UnCon s => "un" ^ s
107 | Other s => s)
108
109 fun p_exp e =
110 case e of
111 Const p => Prim.p_t p
112 | Var n => string ("x" ^ Int.toString n)
113 | Lvar n => string ("X" ^ Int.toString n)
114 | Func (f, es) => box [p_func f,
115 string "(",
116 p_list p_exp es,
117 string ")"]
118 | Recd xes => box [string "{",
119 p_list (fn (x, e) => box [string x,
120 space,
121 string "=",
122 space,
123 p_exp e]) xes,
124 string "}"]
125 | Proj (e, x) => box [p_exp e,
126 string ("." ^ x)]
127
128 fun p_bop s es =
129 case es of
130 [e1, e2] => box [p_exp e1,
131 space,
132 string s,
133 space,
134 p_exp e2]
135 | _ => raise Fail "Iflow.p_bop"
136
137 fun p_reln r es =
138 case r of
139 Known =>
140 (case es of
141 [e] => box [string "known(",
142 p_exp e,
143 string ")"]
144 | _ => raise Fail "Iflow.p_reln: Known")
145 | Sql s => box [string (s ^ "("),
146 p_list p_exp es,
147 string ")"]
148 | PCon0 s => box [string (s ^ "("),
149 p_list p_exp es,
150 string ")"]
151 | PCon1 s => box [string (s ^ "("),
152 p_list p_exp es,
153 string ")"]
154 | Eq => p_bop "=" es
155 | Ne => p_bop "<>" es
156 | Lt => p_bop "<" es
157 | Le => p_bop "<=" es
158 | Gt => p_bop ">" es
159 | Ge => p_bop ">=" es
160
161 fun p_prop p =
162 case p of
163 True => string "True"
164 | False => string "False"
165 | Unknown => string "??"
166 | And (p1, p2) => box [string "(",
167 p_prop p1,
168 string ")",
169 space,
170 string "&&",
171 space,
172 string "(",
173 p_prop p2,
174 string ")"]
175 | Or (p1, p2) => box [string "(",
176 p_prop p1,
177 string ")",
178 space,
179 string "||",
180 space,
181 string "(",
182 p_prop p2,
183 string ")"]
184 | Reln (r, es) => p_reln r es
185 | Cond (e, p) => box [string "(",
186 p_exp e,
187 space,
188 string "==",
189 space,
190 p_prop p,
191 string ")"]
192
193 end
194
195 fun isKnown e =
196 case e of
197 Const _ => true
198 | Func (_, es) => List.all isKnown es
199 | Recd xes => List.all (isKnown o #2) xes
200 | Proj (e, _) => isKnown e
201 | _ => false
202
203 fun simplify unif =
204 let
205 fun simplify e =
206 case e of
207 Const _ => e
208 | Var _ => e
209 | Lvar n =>
210 (case IM.find (unif, n) of
211 NONE => e
212 | SOME e => simplify e)
213 | Func (f, es) => Func (f, map simplify es)
214 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
215 | Proj (e, s) => Proj (simplify e, s)
216 in
217 simplify
218 end
219
220 datatype atom =
221 AReln of reln * exp list
222 | ACond of exp * prop
223
224 fun p_atom a =
225 p_prop (case a of
226 AReln x => Reln x
227 | ACond x => Cond x)
228
229 val debug = ref false
230
231 (* Congruence closure *)
232 structure Cc :> sig
233 type database
234
235 exception Contradiction
236
237 val database : unit -> database
238 val clear : database -> unit
239
240 val assert : database * atom -> unit
241 val check : database * atom -> bool
242
243 val p_database : database Print.printer
244
245 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
246
247 val p_repOf : database -> exp Print.printer
248 end = struct
249
250 local
251 val count = ref 0
252 in
253 fun nodeId () =
254 let
255 val n = !count
256 in
257 count := n + 1;
258 n
259 end
260 end
261
262 exception Contradiction
263 exception Undetermined
264
265 structure CM = BinaryMapFn(struct
266 type ord_key = Prim.t
267 val compare = Prim.compare
268 end)
269
270 datatype node = Node of {Id : int,
271 Rep : node ref option ref,
272 Cons : node ref SM.map ref,
273 Variety : variety,
274 Known : bool ref,
275 Ge : Int64.int option ref}
276
277 and variety =
278 Dt0 of string
279 | Dt1 of string * node ref
280 | Prim of Prim.t
281 | Recrd of node ref SM.map ref * bool
282 | Nothing
283
284 type representative = node ref
285
286 type database = {Vars : representative IM.map ref,
287 Consts : representative CM.map ref,
288 Con0s : representative SM.map ref,
289 Records : (representative SM.map * representative) list ref,
290 Funcs : ((string * representative list) * representative) list ref}
291
292 fun database () = {Vars = ref IM.empty,
293 Consts = ref CM.empty,
294 Con0s = ref SM.empty,
295 Records = ref [],
296 Funcs = ref []}
297
298 fun clear (t : database) = (#Vars t := IM.empty;
299 #Consts t := CM.empty;
300 #Con0s t := SM.empty;
301 #Records t := [];
302 #Funcs t := [])
303
304 fun unNode n =
305 case !n of
306 Node r => r
307
308 open Print
309 val string = PD.string
310 val newline = PD.newline
311
312 fun p_rep n =
313 case !(#Rep (unNode n)) of
314 SOME n => p_rep n
315 | NONE =>
316 box [string (Int.toString (#Id (unNode n)) ^ ":"),
317 space,
318 case #Variety (unNode n) of
319 Nothing => string "?"
320 | Dt0 s => string ("Dt0(" ^ s ^ ")")
321 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
322 space,
323 p_rep n,
324 string ")"]
325 | Prim p => Prim.p_t p
326 | Recrd (ref m, b) => box [string "{",
327 p_list (fn (x, n) => box [string x,
328 space,
329 string "=",
330 space,
331 p_rep n]) (SM.listItemsi m),
332 string "}",
333 if b then
334 box [space,
335 string "(complete)"]
336 else
337 box []],
338 if !(#Known (unNode n)) then
339 string " (known)"
340 else
341 box [],
342 case !(#Ge (unNode n)) of
343 NONE => box []
344 | SOME n => string (" (>= " ^ Int64.toString n ^ ")")]
345
346 fun p_database (db : database) =
347 box [string "Vars:",
348 newline,
349 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
350 space,
351 string "=",
352 space,
353 p_rep n]) (IM.listItemsi (!(#Vars db)))]
354
355 fun repOf (n : representative) : representative =
356 case !(#Rep (unNode n)) of
357 NONE => n
358 | SOME r =>
359 let
360 val r = repOf r
361 in
362 #Rep (unNode n) := SOME r;
363 r
364 end
365
366 fun markKnown r =
367 let
368 val r = repOf r
369 in
370 (*Print.preface ("markKnown", p_rep r);*)
371 if !(#Known (unNode r)) then
372 ()(*TextIO.print "Already known\n"*)
373 else
374 (#Known (unNode r) := true;
375 SM.app markKnown (!(#Cons (unNode r)));
376 case #Variety (unNode r) of
377 Dt1 (_, r) => markKnown r
378 | Recrd (xes, _) => SM.app markKnown (!xes)
379 | _ => ())
380 end
381
382 fun representative (db : database, e) =
383 let
384 fun rep e =
385 case e of
386 Const p => (case CM.find (!(#Consts db), p) of
387 SOME r => repOf r
388 | NONE =>
389 let
390 val r = ref (Node {Id = nodeId (),
391 Rep = ref NONE,
392 Cons = ref SM.empty,
393 Variety = Prim p,
394 Known = ref true,
395 Ge = ref (case p of
396 Prim.Int n => SOME n
397 | _ => NONE)})
398 in
399 #Consts db := CM.insert (!(#Consts db), p, r);
400 r
401 end)
402 | Var n => (case IM.find (!(#Vars db), n) of
403 SOME r => repOf r
404 | NONE =>
405 let
406 val r = ref (Node {Id = nodeId (),
407 Rep = ref NONE,
408 Cons = ref SM.empty,
409 Variety = Nothing,
410 Known = ref false,
411 Ge = ref NONE})
412 in
413 #Vars db := IM.insert (!(#Vars db), n, r);
414 r
415 end)
416 | Lvar _ => raise Undetermined
417 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
418 SOME r => repOf r
419 | NONE =>
420 let
421 val r = ref (Node {Id = nodeId (),
422 Rep = ref NONE,
423 Cons = ref SM.empty,
424 Variety = Dt0 f,
425 Known = ref true,
426 Ge = ref NONE})
427 in
428 #Con0s db := SM.insert (!(#Con0s db), f, r);
429 r
430 end)
431 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
432 | Func (DtCon1 f, [e]) =>
433 let
434 val r = rep e
435 in
436 case SM.find (!(#Cons (unNode r)), f) of
437 SOME r => repOf r
438 | NONE =>
439 let
440 val r' = ref (Node {Id = nodeId (),
441 Rep = ref NONE,
442 Cons = ref SM.empty,
443 Variety = Dt1 (f, r),
444 Known = ref (!(#Known (unNode r))),
445 Ge = ref NONE})
446 in
447 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
448 r'
449 end
450 end
451 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
452 | Func (UnCon f, [e]) =>
453 let
454 val r = rep e
455 in
456 case #Variety (unNode r) of
457 Dt1 (f', n) => if f' = f then
458 repOf n
459 else
460 raise Contradiction
461 | Nothing =>
462 let
463 val cons = ref SM.empty
464 val r' = ref (Node {Id = nodeId (),
465 Rep = ref NONE,
466 Cons = cons,
467 Variety = Nothing,
468 Known = ref (!(#Known (unNode r))),
469 Ge = ref NONE})
470
471 val r'' = ref (Node {Id = nodeId (),
472 Rep = ref NONE,
473 Cons = #Cons (unNode r),
474 Variety = Dt1 (f, r'),
475 Known = #Known (unNode r),
476 Ge = ref NONE})
477 in
478 cons := SM.insert (!cons, f, r'');
479 #Rep (unNode r) := SOME r'';
480 r'
481 end
482 | _ => raise Contradiction
483 end
484 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
485 | Func (Other f, es) =>
486 let
487 val rs = map rep es
488 in
489 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
490 NONE =>
491 let
492 val r = ref (Node {Id = nodeId (),
493 Rep = ref NONE,
494 Cons = ref SM.empty,
495 Variety = Nothing,
496 Known = ref (f = "allow"),
497 Ge = ref NONE})
498 in
499 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
500 r
501 end
502 | SOME (_, r) => repOf r
503 end
504 | Recd xes =>
505 let
506 val xes = map (fn (x, e) => (x, rep e)) xes
507 val len = length xes
508 in
509 case List.find (fn (xes', _) =>
510 SM.numItems xes' = len
511 andalso List.all (fn (x, n) =>
512 case SM.find (xes', x) of
513 NONE => false
514 | SOME n' => n = repOf n') xes)
515 (!(#Records db)) of
516 SOME (_, r) => repOf r
517 | NONE =>
518 let
519 val xes = foldl SM.insert' SM.empty xes
520
521 val r' = ref (Node {Id = nodeId (),
522 Rep = ref NONE,
523 Cons = ref SM.empty,
524 Variety = Recrd (ref xes, true),
525 Known = ref false,
526 Ge = ref NONE})
527 in
528 #Records db := (xes, r') :: (!(#Records db));
529 r'
530 end
531 end
532 | Proj (e, f) =>
533 let
534 val r = rep e
535 in
536 case #Variety (unNode r) of
537 Recrd (xes, _) =>
538 (case SM.find (!xes, f) of
539 SOME r => repOf r
540 | NONE => let
541 val r = ref (Node {Id = nodeId (),
542 Rep = ref NONE,
543 Cons = ref SM.empty,
544 Variety = Nothing,
545 Known = ref (!(#Known (unNode r))),
546 Ge = ref NONE})
547 in
548 xes := SM.insert (!xes, f, r);
549 r
550 end)
551 | Nothing =>
552 let
553 val r' = ref (Node {Id = nodeId (),
554 Rep = ref NONE,
555 Cons = ref SM.empty,
556 Variety = Nothing,
557 Known = ref (!(#Known (unNode r))),
558 Ge = ref NONE})
559
560 val r'' = ref (Node {Id = nodeId (),
561 Rep = ref NONE,
562 Cons = #Cons (unNode r),
563 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
564 Known = #Known (unNode r),
565 Ge = ref NONE})
566 in
567 #Rep (unNode r) := SOME r'';
568 r'
569 end
570 | _ => raise Contradiction
571 end
572 in
573 rep e
574 end
575
576 fun p_repOf db e = p_rep (representative (db, e))
577
578 fun assert (db, a) =
579 let
580 fun markEq (r1, r2) =
581 let
582 val r1 = repOf r1
583 val r2 = repOf r2
584 in
585 if r1 = r2 then
586 ()
587 else case (#Variety (unNode r1), #Variety (unNode r2)) of
588 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
589 ()
590 else
591 raise Contradiction
592 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
593 ()
594 else
595 raise Contradiction
596 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
597 markEq (r1, r2)
598 else
599 raise Contradiction
600 | (Recrd (xes1, _), Recrd (xes2, _)) =>
601 let
602 fun unif (xes1, xes2) =
603 SM.appi (fn (x, r1) =>
604 case SM.find (!xes2, x) of
605 NONE => xes2 := SM.insert (!xes2, x, r1)
606 | SOME r2 => markEq (r1, r2)) (!xes1)
607 in
608 unif (xes1, xes2);
609 unif (xes2, xes1)
610 end
611 | (Nothing, _) => mergeNodes (r1, r2)
612 | (_, Nothing) => mergeNodes (r2, r1)
613 | _ => raise Contradiction
614 end
615
616 and mergeNodes (r1, r2) =
617 (#Rep (unNode r1) := SOME r2;
618 if !(#Known (unNode r1)) then
619 markKnown r2
620 else
621 ();
622 if !(#Known (unNode r2)) then
623 markKnown r1
624 else
625 ();
626 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
627
628 case !(#Ge (unNode r1)) of
629 NONE => ()
630 | SOME n1 =>
631 case !(#Ge (unNode r2)) of
632 NONE => #Ge (unNode r2) := SOME n1
633 | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));
634
635 compactFuncs ())
636
637 and compactFuncs () =
638 let
639 fun loop funcs =
640 case funcs of
641 [] => []
642 | (fr as ((f, rs), r)) :: rest =>
643 let
644 val rest = List.filter (fn ((f' : string, rs'), r') =>
645 if f' = f
646 andalso ListPair.allEq (fn (r1, r2) =>
647 repOf r1 = repOf r2)
648 (rs, rs') then
649 (markEq (r, r');
650 false)
651 else
652 true) rest
653 in
654 fr :: loop rest
655 end
656 in
657 #Funcs db := loop (!(#Funcs db))
658 end
659 in
660 case a of
661 ACond _ => ()
662 | AReln x =>
663 case x of
664 (Known, [e]) =>
665 ((*Print.prefaces "Before" [("e", p_exp e),
666 ("db", p_database db)];*)
667 markKnown (representative (db, e))(*;
668 Print.prefaces "After" [("e", p_exp e),
669 ("db", p_database db)]*))
670 | (PCon0 f, [e]) =>
671 let
672 val r = representative (db, e)
673 in
674 case #Variety (unNode r) of
675 Dt0 f' => if f = f' then
676 ()
677 else
678 raise Contradiction
679 | Nothing =>
680 (case SM.find (!(#Con0s db), f) of
681 SOME r' => markEq (r, r')
682 | NONE =>
683 let
684 val r' = ref (Node {Id = nodeId (),
685 Rep = ref NONE,
686 Cons = ref SM.empty,
687 Variety = Dt0 f,
688 Known = ref false,
689 Ge = ref NONE})
690 in
691 #Rep (unNode r) := SOME r';
692 #Con0s db := SM.insert (!(#Con0s db), f, r')
693 end)
694 | _ => raise Contradiction
695 end
696 | (PCon1 f, [e]) =>
697 let
698 val r = representative (db, e)
699 in
700 case #Variety (unNode r) of
701 Dt1 (f', e') => if f = f' then
702 ()
703 else
704 raise Contradiction
705 | Nothing =>
706 let
707 val cons = ref SM.empty
708
709 val r'' = ref (Node {Id = nodeId (),
710 Rep = ref NONE,
711 Cons = cons,
712 Variety = Nothing,
713 Known = ref (!(#Known (unNode r))),
714 Ge = ref NONE})
715
716 val r' = ref (Node {Id = nodeId (),
717 Rep = ref NONE,
718 Cons = ref SM.empty,
719 Variety = Dt1 (f, r''),
720 Known = #Known (unNode r),
721 Ge = ref NONE})
722 in
723 cons := SM.insert (!cons, f, r');
724 #Rep (unNode r) := SOME r'
725 end
726 | _ => raise Contradiction
727 end
728 | (Eq, [e1, e2]) =>
729 markEq (representative (db, e1), representative (db, e2))
730 | (Ge, [e1, e2]) =>
731 let
732 val r1 = representative (db, e1)
733 val r2 = representative (db, e2)
734 in
735 case !(#Ge (unNode (repOf r2))) of
736 NONE => ()
737 | SOME n2 =>
738 case !(#Ge (unNode (repOf r1))) of
739 NONE => #Ge (unNode (repOf r1)) := SOME n2
740 | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
741 end
742 | _ => ()
743 end handle Undetermined => ()
744
745 fun check (db, a) =
746 (case a of
747 ACond _ => false
748 | AReln x =>
749 case x of
750 (Known, [e]) =>
751 let
752 fun isKnown r =
753 let
754 val r = repOf r
755 in
756 !(#Known (unNode r))
757 orelse case #Variety (unNode r) of
758 Dt1 (_, r) => isKnown r
759 | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
760 | _ => false
761 end
762
763 val r = representative (db, e)
764 in
765 isKnown r
766 end
767 | (PCon0 f, [e]) =>
768 (case #Variety (unNode (representative (db, e))) of
769 Dt0 f' => f' = f
770 | _ => false)
771 | (PCon1 f, [e]) =>
772 (case #Variety (unNode (representative (db, e))) of
773 Dt1 (f', _) => f' = f
774 | _ => false)
775 | (Eq, [e1, e2]) =>
776 let
777 val r1 = representative (db, e1)
778 val r2 = representative (db, e2)
779 in
780 repOf r1 = repOf r2
781 end
782 | (Ge, [e1, e2]) =>
783 let
784 val r1 = representative (db, e1)
785 val r2 = representative (db, e2)
786 in
787 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
788 (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
789 | _ => false
790 end
791 | _ => false)
792 handle Undetermined => false
793
794 fun builtFrom (db, {Base = bs, Derived = d}) =
795 let
796 val bs = map (fn b => representative (db, b)) bs
797
798 fun loop d =
799 let
800 val d = repOf d
801 in
802 !(#Known (unNode d))
803 orelse List.exists (fn b => repOf b = d) bs
804 orelse (case #Variety (unNode d) of
805 Dt0 _ => true
806 | Dt1 (_, d) => loop d
807 | Prim _ => true
808 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
809 | Nothing => false)
810 orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs)
811 (SM.listItems (!(#Cons (unNode d))))
812 end
813
814 fun decomp e =
815 case e of
816 Func (Other _, es) => List.all decomp es
817 | _ => loop (representative (db, e))
818 in
819 decomp d
820 end handle Undetermined => false
821
822 end
823
824 val tabs = ref (SM.empty : (string list * string list list) SM.map)
825
826 fun patCon pc =
827 case pc of
828 PConVar n => "C" ^ Int.toString n
829 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
830
831 datatype chunk =
832 String of string
833 | Exp of Mono.exp
834
835 fun chunkify e =
836 case #1 e of
837 EPrim (Prim.String s) => [String s]
838 | EStrcat (e1, e2) =>
839 let
840 val chs1 = chunkify e1
841 val chs2 = chunkify e2
842 in
843 case chs2 of
844 String s2 :: chs2' =>
845 (case List.last chs1 of
846 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
847 | _ => chs1 @ chs2)
848 | _ => chs1 @ chs2
849 end
850 | _ => [Exp e]
851
852 type 'a parser = chunk list -> ('a * chunk list) option
853
854 fun always v chs = SOME (v, chs)
855
856 fun parse p s =
857 case p (chunkify s) of
858 SOME (v, []) => SOME v
859 | _ => NONE
860
861 fun const s chs =
862 case chs of
863 String s' :: chs => if String.isPrefix s s' then
864 SOME ((), if size s = size s' then
865 chs
866 else
867 String (String.extract (s', size s, NONE)) :: chs)
868 else
869 NONE
870 | _ => NONE
871
872 fun follow p1 p2 chs =
873 case p1 chs of
874 NONE => NONE
875 | SOME (v1, chs) =>
876 case p2 chs of
877 NONE => NONE
878 | SOME (v2, chs) => SOME ((v1, v2), chs)
879
880 fun wrap p f chs =
881 case p chs of
882 NONE => NONE
883 | SOME (v, chs) => SOME (f v, chs)
884
885 fun wrapP p f chs =
886 case p chs of
887 NONE => NONE
888 | SOME (v, chs) =>
889 case f v of
890 NONE => NONE
891 | SOME r => SOME (r, chs)
892
893 fun alt p1 p2 chs =
894 case p1 chs of
895 NONE => p2 chs
896 | v => v
897
898 fun altL ps =
899 case rev ps of
900 [] => (fn _ => NONE)
901 | p :: ps =>
902 foldl (fn (p1, p2) => alt p1 p2) p ps
903
904 fun opt p chs =
905 case p chs of
906 NONE => SOME (NONE, chs)
907 | SOME (v, chs) => SOME (SOME v, chs)
908
909 fun skip cp chs =
910 case chs of
911 String "" :: chs => skip cp chs
912 | String s :: chs' => if cp (String.sub (s, 0)) then
913 skip cp (String (String.extract (s, 1, NONE)) :: chs')
914 else
915 SOME ((), chs)
916 | _ => SOME ((), chs)
917
918 fun keep cp chs =
919 case chs of
920 String "" :: chs => keep cp chs
921 | String s :: chs' =>
922 let
923 val (befor, after) = Substring.splitl cp (Substring.full s)
924 in
925 if Substring.isEmpty befor then
926 NONE
927 else
928 SOME (Substring.string befor,
929 if Substring.isEmpty after then
930 chs'
931 else
932 String (Substring.string after) :: chs')
933 end
934 | _ => NONE
935
936 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
937 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
938
939 fun log name p chs =
940 (if !debug then
941 (print (name ^ ": ");
942 app (fn String s => print s
943 | _ => print "???") chs;
944 print "\n")
945 else
946 ();
947 p chs)
948
949 fun list p chs =
950 altL [wrap (follow p (follow (ws (const ",")) (list p)))
951 (fn (v, ((), ls)) => v :: ls),
952 wrap (ws p) (fn v => [v]),
953 always []] chs
954
955 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
956
957 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
958 SOME (String.extract (s, 2, NONE))
959 else
960 NONE)
961 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
962 SOME (str (Char.toUpper (String.sub (s, 3)))
963 ^ String.extract (s, 4, NONE))
964 else
965 NONE)
966
967 val field = wrap (follow t_ident
968 (follow (const ".")
969 uw_ident))
970 (fn (t, ((), f)) => (t, f))
971
972 datatype Rel =
973 Exps of exp * exp -> prop
974 | Props of prop * prop -> prop
975
976 datatype sqexp =
977 SqConst of Prim.t
978 | SqTrue
979 | SqFalse
980 | SqNot of sqexp
981 | Field of string * string
982 | Computed of string
983 | Binop of Rel * sqexp * sqexp
984 | SqKnown of sqexp
985 | Inj of Mono.exp
986 | SqFunc of string * sqexp
987 | Unmodeled
988 | Null
989
990 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
991
992 val sqbrel = altL [cmp "=" Eq,
993 cmp "<>" Ne,
994 cmp "<=" Le,
995 cmp "<" Lt,
996 cmp ">=" Ge,
997 cmp ">" Gt,
998 wrap (const "AND") (fn () => Props And),
999 wrap (const "OR") (fn () => Props Or)]
1000
1001 datatype ('a, 'b) sum = inl of 'a | inr of 'b
1002
1003 fun string chs =
1004 case chs of
1005 String s :: chs =>
1006 if size s >= 2 andalso String.sub (s, 0) = #"'" then
1007 let
1008 fun loop (cs, acc) =
1009 case cs of
1010 [] => NONE
1011 | c :: cs =>
1012 if c = #"'" then
1013 SOME (String.implode (rev acc), cs)
1014 else if c = #"\\" then
1015 case cs of
1016 c :: cs => loop (cs, c :: acc)
1017 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
1018 else
1019 loop (cs, c :: acc)
1020 in
1021 case loop (String.explode (String.extract (s, 1, NONE)), []) of
1022 NONE => NONE
1023 | SOME (s, []) => SOME (s, chs)
1024 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
1025 end
1026 else
1027 NONE
1028 | _ => NONE
1029
1030 val prim =
1031 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
1032 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
1033 (opt (const "::float8"))) #1,
1034 wrap (follow (wrapP (keep Char.isDigit)
1035 (Option.map Prim.Int o Int64.fromString))
1036 (opt (const "::int8"))) #1,
1037 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
1038 (Prim.String o #1 o #2)]
1039
1040 fun known' chs =
1041 case chs of
1042 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
1043 | _ => NONE
1044
1045 fun sqlify chs =
1046 case chs of
1047 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
1048 if String.isPrefix "sqlify" f then
1049 SOME (e, chs)
1050 else
1051 NONE
1052 | Exp (ECase (e, [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
1053 (EPrim (Prim.String "TRUE"), _)),
1054 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
1055 (EPrim (Prim.String "FALSE"), _))], _), _) :: chs =>
1056 SOME (e, chs)
1057
1058 | _ => NONE
1059
1060 fun constK s = wrap (const s) (fn () => s)
1061
1062 val funcName = altL [constK "COUNT",
1063 constK "MIN",
1064 constK "MAX",
1065 constK "SUM",
1066 constK "AVG"]
1067
1068 val unmodeled = altL [const "COUNT(*)",
1069 const "CURRENT_TIMESTAMP"]
1070
1071 fun sqexp chs =
1072 log "sqexp"
1073 (altL [wrap prim SqConst,
1074 wrap (const "TRUE") (fn () => SqTrue),
1075 wrap (const "FALSE") (fn () => SqFalse),
1076 wrap (const "NULL") (fn () => Null),
1077 wrap field Field,
1078 wrap uw_ident Computed,
1079 wrap known SqKnown,
1080 wrap func SqFunc,
1081 wrap unmodeled (fn () => Unmodeled),
1082 wrap sqlify Inj,
1083 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
1084 (follow (keep (fn ch => ch <> #")")) (const ")")))))
1085 (fn ((), (e, _)) => e),
1086 wrap (follow (const "(NOT ") (follow sqexp (const ")")))
1087 (fn ((), (e, _)) => SqNot e),
1088 wrap (follow (ws (const "("))
1089 (follow (wrap
1090 (follow sqexp
1091 (alt
1092 (wrap
1093 (follow (ws sqbrel)
1094 (ws sqexp))
1095 inl)
1096 (always (inr ()))))
1097 (fn (e1, sm) =>
1098 case sm of
1099 inl (bo, e2) => Binop (bo, e1, e2)
1100 | inr () => e1))
1101 (const ")")))
1102 (fn ((), (e, ())) => e)])
1103 chs
1104
1105 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
1106 (fn ((), ((), (e, ()))) => e) chs
1107
1108 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
1109 (fn (f, ((), (e, ()))) => (f, e)) chs
1110
1111 datatype sitem =
1112 SqField of string * string
1113 | SqExp of sqexp * string
1114
1115 val sitem = alt (wrap (follow sqexp (follow (const " AS ") uw_ident))
1116 (fn (e, ((), s)) => SqExp (e, s)))
1117 (wrap field SqField)
1118
1119 val select = log "select"
1120 (wrap (follow (const "SELECT ") (list sitem))
1121 (fn ((), ls) => ls))
1122
1123 val fitem = wrap (follow uw_ident
1124 (follow (const " AS ")
1125 t_ident))
1126 (fn (t, ((), f)) => (t, f))
1127
1128 val from = log "from"
1129 (wrap (follow (const "FROM ") (list fitem))
1130 (fn ((), ls) => ls))
1131
1132 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
1133 (fn ((), ls) => ls)
1134
1135 type query1 = {Select : sitem list,
1136 From : (string * string) list,
1137 Where : sqexp option}
1138
1139 val query1 = log "query1"
1140 (wrap (follow (follow select from) (opt wher))
1141 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
1142
1143 datatype query =
1144 Query1 of query1
1145 | Union of query * query
1146
1147 val orderby = log "orderby"
1148 (wrap (follow (ws (const "ORDER BY "))
1149 (follow (list sqexp)
1150 (opt (ws (const "DESC")))))
1151 ignore)
1152
1153 fun query chs = log "query"
1154 (wrap
1155 (follow
1156 (alt (wrap (follow (const "((")
1157 (follow query
1158 (follow (const ") UNION (")
1159 (follow query (const "))")))))
1160 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
1161 (wrap query1 Query1))
1162 (opt orderby))
1163 #1)
1164 chs
1165
1166 datatype dml =
1167 Insert of string * (string * sqexp) list
1168 | Delete of string * sqexp
1169 | Update of string * (string * sqexp) list * sqexp
1170
1171 val insert = log "insert"
1172 (wrapP (follow (const "INSERT INTO ")
1173 (follow uw_ident
1174 (follow (const " (")
1175 (follow (list uw_ident)
1176 (follow (const ") VALUES (")
1177 (follow (list sqexp)
1178 (const ")")))))))
1179 (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
1180 (SOME (tab, ListPair.zipEq (fs, es)))
1181 handle ListPair.UnequalLengths => NONE))
1182
1183 val delete = log "delete"
1184 (wrap (follow (const "DELETE FROM ")
1185 (follow uw_ident
1186 (follow (const " AS T_T WHERE ")
1187 sqexp)))
1188 (fn ((), (tab, ((), es))) => (tab, es)))
1189
1190 val setting = log "setting"
1191 (wrap (follow uw_ident (follow (const " = ") sqexp))
1192 (fn (f, ((), e)) => (f, e)))
1193
1194 val update = log "update"
1195 (wrap (follow (const "UPDATE ")
1196 (follow uw_ident
1197 (follow (const " AS T_T SET ")
1198 (follow (list setting)
1199 (follow (ws (const "WHERE "))
1200 sqexp)))))
1201 (fn ((), (tab, ((), (fs, ((), e))))) =>
1202 (tab, fs, e)))
1203
1204 val dml = log "dml"
1205 (altL [wrap insert Insert,
1206 wrap delete Delete,
1207 wrap update Update])
1208
1209 type check = exp * ErrorMsg.span
1210
1211 structure St :> sig
1212 val reset : unit -> unit
1213
1214 type stashed
1215 val stash : unit -> stashed
1216 val reinstate : stashed -> unit
1217
1218 type stashedPath
1219 val stashPath : unit -> stashedPath
1220 val reinstatePath : stashedPath -> unit
1221
1222 val nextVar : unit -> int
1223
1224 val assert : atom list -> unit
1225
1226 val addPath : check -> unit
1227
1228 val allowSend : atom list * exp list -> unit
1229 val send : check -> unit
1230
1231 val allowInsert : atom list -> unit
1232 val insert : ErrorMsg.span -> unit
1233
1234 val allowDelete : atom list -> unit
1235 val delete : ErrorMsg.span -> unit
1236
1237 val allowUpdate : atom list -> unit
1238 val update : ErrorMsg.span -> unit
1239
1240 val havocReln : reln -> unit
1241 val havocCookie : string -> unit
1242
1243 val check : atom -> bool
1244
1245 val debug : unit -> unit
1246 end = struct
1247
1248 val hnames = ref 1
1249
1250 type hyps = int * atom list * bool ref
1251
1252 val db = Cc.database ()
1253 val path = ref ([] : ((int * atom list) * check) option ref list)
1254 val hyps = ref (0, [] : atom list, ref false)
1255 val nvar = ref 0
1256
1257 fun setHyps (n', hs) =
1258 let
1259 val (n, _, _) = !hyps
1260 in
1261 if n' = n then
1262 ()
1263 else
1264 (hyps := (n', hs, ref false);
1265 Cc.clear db;
1266 app (fn a => Cc.assert (db, a)) hs)
1267 end
1268
1269 fun useKeys () =
1270 let
1271 val changed = ref false
1272
1273 fun findKeys (hyps, acc) =
1274 case hyps of
1275 [] => rev acc
1276 | (a as AReln (Sql tab, [r1])) :: hyps =>
1277 (case SM.find (!tabs, tab) of
1278 NONE => findKeys (hyps, a :: acc)
1279 | SOME (_, []) => findKeys (hyps, a :: acc)
1280 | SOME (_, ks) =>
1281 let
1282 fun finder (hyps, acc) =
1283 case hyps of
1284 [] => rev acc
1285 | (a as AReln (Sql tab', [r2])) :: hyps =>
1286 if tab' = tab andalso
1287 List.exists (List.all (fn f =>
1288 let
1289 val r =
1290 Cc.check (db,
1291 AReln (Eq, [Proj (r1, f),
1292 Proj (r2, f)]))
1293 in
1294 (*Print.prefaces "Fs"
1295 [("tab",
1296 Print.PD.string tab),
1297 ("r1",
1298 p_exp (Proj (r1, f))),
1299 ("r2",
1300 p_exp (Proj (r2, f))),
1301 ("r",
1302 Print.PD.string
1303 (Bool.toString r))];*)
1304 r
1305 end)) ks then
1306 (changed := true;
1307 Cc.assert (db, AReln (Eq, [r1, r2]));
1308 finder (hyps, acc))
1309 else
1310 finder (hyps, a :: acc)
1311 | a :: hyps => finder (hyps, a :: acc)
1312
1313 val hyps = finder (hyps, [])
1314 in
1315 findKeys (hyps, a :: acc)
1316 end)
1317 | a :: hyps => findKeys (hyps, a :: acc)
1318
1319 fun loop hs =
1320 let
1321 val hs = findKeys (hs, [])
1322 in
1323 if !changed then
1324 (changed := false;
1325 loop hs)
1326 else
1327 ()
1328 end
1329
1330 val (_, hs, _) = !hyps
1331 in
1332 (*print "useKeys\n";*)
1333 loop hs
1334 end
1335
1336 fun complete () =
1337 let
1338 val (_, _, bf) = !hyps
1339 in
1340 if !bf then
1341 ()
1342 else
1343 (bf := true;
1344 useKeys ())
1345 end
1346
1347 type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
1348 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
1349 fun reinstate (nv, p, h) =
1350 (nvar := nv;
1351 path := p;
1352 setHyps h)
1353
1354 type stashedPath = ((int * atom list) * check) option ref list
1355 fun stashPath () = !path
1356 fun reinstatePath p = path := p
1357
1358 fun nextVar () =
1359 let
1360 val n = !nvar
1361 in
1362 nvar := n + 1;
1363 n
1364 end
1365
1366 fun assert ats =
1367 let
1368 val n = !hnames
1369 val (_, hs, _) = !hyps
1370 in
1371 hnames := n + 1;
1372 hyps := (n, ats @ hs, ref false);
1373 app (fn a => Cc.assert (db, a)) ats
1374 end
1375
1376 fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
1377
1378 val sendable = ref ([] : (atom list * exp list) list)
1379
1380 fun checkGoals goals k =
1381 let
1382 fun checkGoals goals unifs =
1383 case goals of
1384 [] => k unifs
1385 | AReln (Sql tab, [Lvar lv]) :: goals =>
1386 let
1387 val saved = stash ()
1388 val (_, hyps, _) = !hyps
1389
1390 fun tryAll unifs hyps =
1391 case hyps of
1392 [] => false
1393 | AReln (Sql tab', [e]) :: hyps =>
1394 (tab' = tab andalso
1395 checkGoals goals (IM.insert (unifs, lv, e)))
1396 orelse tryAll unifs hyps
1397 | _ :: hyps => tryAll unifs hyps
1398 in
1399 tryAll unifs hyps
1400 end
1401 | (g as AReln (r, es)) :: goals =>
1402 (complete ();
1403 (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
1404 true
1405 else
1406 ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
1407 false))
1408 andalso checkGoals goals unifs)
1409 | ACond _ :: _ => false
1410 in
1411 checkGoals goals IM.empty
1412 end
1413
1414 fun buildable (e, loc) =
1415 let
1416 fun doPols pols acc =
1417 case pols of
1418 [] =>
1419 let
1420 val b = Cc.builtFrom (db, {Base = acc, Derived = e})
1421 in
1422 (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
1423 ("Derived", p_exp e),
1424 ("Hyps", Print.p_list p_atom (#2 (!hyps))),
1425 ("Good", Print.PD.string (Bool.toString b))];*)
1426 b
1427 end
1428 | (goals, es) :: pols =>
1429 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
1430 orelse doPols pols acc
1431 in
1432 if doPols (!sendable) [] then
1433 ()
1434 else
1435 let
1436 val (_, hs, _) = !hyps
1437 in
1438 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1439 Print.prefaces "Situation" [("User learns", p_exp e),
1440 ("Hypotheses", Print.p_list p_atom hs),
1441 ("E-graph", Cc.p_database db)]
1442 end
1443 end
1444
1445 fun checkPaths () =
1446 let
1447 val (n, hs, _) = !hyps
1448 val hs = (n, hs)
1449 in
1450 app (fn r =>
1451 case !r of
1452 NONE => ()
1453 | SOME (hs, e) =>
1454 (r := NONE;
1455 setHyps hs;
1456 buildable e)) (!path);
1457 setHyps hs
1458 end
1459
1460 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
1461 ("exps", Print.p_list p_exp (#2 v))];*)
1462 sendable := v :: !sendable)
1463
1464 fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
1465 complete ();
1466 checkPaths ();
1467 if isKnown e then
1468 ()
1469 else
1470 buildable (e, loc))
1471
1472 fun doable pols (loc : ErrorMsg.span) =
1473 let
1474 val pols = !pols
1475 in
1476 complete ();
1477 if List.exists (fn goals =>
1478 if checkGoals goals (fn _ => true) then
1479 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
1480 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
1481 true)
1482 else
1483 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
1484 ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
1485 false)) pols then
1486 ()
1487 else
1488 let
1489 val (_, hs, _) = !hyps
1490 in
1491 ErrorMsg.errorAt loc "The database update policy may be violated here.";
1492 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
1493 ("E-graph", Cc.p_database db)*)]
1494 end
1495 end
1496
1497 val insertable = ref ([] : atom list list)
1498 fun allowInsert v = insertable := v :: !insertable
1499 val insert = doable insertable
1500
1501 val updatable = ref ([] : atom list list)
1502 fun allowUpdate v = updatable := v :: !updatable
1503 val update = doable updatable
1504
1505 val deletable = ref ([] : atom list list)
1506 fun allowDelete v = deletable := v :: !deletable
1507 val delete = doable deletable
1508
1509 fun reset () = (Cc.clear db;
1510 path := [];
1511 hyps := (0, [], ref false);
1512 nvar := 0;
1513 sendable := [];
1514 insertable := [];
1515 updatable := [];
1516 deletable := [])
1517
1518 fun havocReln r =
1519 let
1520 val n = !hnames
1521 val (_, hs, _) = !hyps
1522 in
1523 hnames := n + 1;
1524 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
1525 end
1526
1527 fun havocCookie cname =
1528 let
1529 val cname = "cookie/" ^ cname
1530 val n = !hnames
1531 val (_, hs, _) = !hyps
1532 in
1533 hnames := n + 1;
1534 hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
1535 end
1536
1537 fun check a = Cc.check (db, a)
1538
1539 fun debug () =
1540 let
1541 val (_, hs, _) = !hyps
1542 in
1543 Print.preface ("Hyps", Print.p_list p_atom hs)
1544 end
1545
1546 end
1547
1548
1549 fun removeDups (ls : (string * string) list) =
1550 case ls of
1551 [] => []
1552 | x :: ls =>
1553 let
1554 val ls = removeDups ls
1555 in
1556 if List.exists (fn x' => x' = x) ls then
1557 ls
1558 else
1559 x :: ls
1560 end
1561
1562 fun deinj env e =
1563 case #1 e of
1564 ERel n => SOME (List.nth (env, n))
1565 | EField (e, f) =>
1566 (case deinj env e of
1567 NONE => NONE
1568 | SOME e => SOME (Proj (e, f)))
1569 | EApp ((EFfi mf, _), e) =>
1570 if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
1571 NONE
1572 else (case deinj env e of
1573 NONE => NONE
1574 | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
1575 | _ => NONE
1576
1577 fun expIn rv env rvOf =
1578 let
1579 fun expIn e =
1580 let
1581 fun default () = inl (rv ())
1582 in
1583 case e of
1584 SqConst p => inl (Const p)
1585 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
1586 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
1587 | Null => inl (Func (DtCon0 "None", []))
1588 | SqNot e =>
1589 inr (case expIn e of
1590 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
1591 | inr _ => Unknown)
1592 | Field (v, f) => inl (Proj (rvOf v, f))
1593 | Computed _ => default ()
1594 | Binop (bo, e1, e2) =>
1595 let
1596 val e1 = expIn e1
1597 val e2 = expIn e2
1598 in
1599 inr (case (bo, e1, e2) of
1600 (Exps f, inl e1, inl e2) => f (e1, e2)
1601 | (Props f, v1, v2) =>
1602 let
1603 fun pin v =
1604 case v of
1605 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1606 | inr p => p
1607 in
1608 f (pin v1, pin v2)
1609 end
1610 | _ => Unknown)
1611 end
1612 | SqKnown e =>
1613 (case expIn e of
1614 inl e => inr (Reln (Known, [e]))
1615 | _ => inr Unknown)
1616 | Inj e =>
1617 inl (case deinj env e of
1618 NONE => rv ()
1619 | SOME e => e)
1620 | SqFunc (f, e) =>
1621 (case expIn e of
1622 inl e => inl (Func (Other f, [e]))
1623 | _ => default ())
1624
1625 | Unmodeled => inl (Func (Other "allow", [rv ()]))
1626 end
1627 in
1628 expIn
1629 end
1630
1631 fun decomp {Save = save, Restore = restore, Add = add} =
1632 let
1633 fun go p k =
1634 case p of
1635 True => (k () handle Cc.Contradiction => ())
1636 | False => ()
1637 | Unknown => ()
1638 | And (p1, p2) => go p1 (fn () => go p2 k)
1639 | Or (p1, p2) =>
1640 let
1641 val saved = save ()
1642 in
1643 go p1 k;
1644 restore saved;
1645 go p2 k
1646 end
1647 | Reln x => (add (AReln x); k ())
1648 | Cond x => (add (ACond x); k ())
1649 in
1650 go
1651 end
1652
1653 datatype queryMode =
1654 SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
1655 | AllCols of exp -> unit
1656
1657 type 'a doQuery = {
1658 Env : exp list,
1659 NextVar : unit -> exp,
1660 Add : atom -> unit,
1661 Save : unit -> 'a,
1662 Restore : 'a -> unit,
1663 Cont : queryMode
1664 }
1665
1666 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
1667 let
1668 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
1669 in
1670 case parse query e of
1671 NONE => default ()
1672 | SOME q =>
1673 let
1674 fun doQuery q =
1675 case q of
1676 Query1 r =>
1677 let
1678 val new = ref NONE
1679 val old = ref NONE
1680
1681 val rvs = map (fn (tab, v) =>
1682 let
1683 val nv = #NextVar arg ()
1684 in
1685 case v of
1686 "New" => new := SOME (tab, nv)
1687 | "Old" => old := SOME (tab, nv)
1688 | _ => ();
1689 (v, nv)
1690 end) (#From r)
1691
1692 fun rvOf v =
1693 case List.find (fn (v', _) => v' = v) rvs of
1694 NONE => raise Fail "Iflow.queryProp: Bad table variable"
1695 | SOME (_, e) => e
1696
1697 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
1698
1699 val saved = #Save arg ()
1700 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1701
1702 fun usedFields e =
1703 case e of
1704 SqConst _ => []
1705 | SqTrue => []
1706 | SqFalse => []
1707 | Null => []
1708 | SqNot e => usedFields e
1709 | Field (v, f) => [(false, Proj (rvOf v, f))]
1710 | Computed _ => []
1711 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
1712 | SqKnown _ => []
1713 | Inj e =>
1714 (case deinj (#Env arg) e of
1715 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
1716 [])
1717 | SOME e => [(true, e)])
1718 | SqFunc (_, e) => usedFields e
1719 | Unmodeled => []
1720
1721 fun normal' () =
1722 case #Cont arg of
1723 SomeCol k =>
1724 let
1725 val sis = map (fn si =>
1726 case si of
1727 SqField (v, f) => Proj (rvOf v, f)
1728 | SqExp (e, f) =>
1729 case expIn e of
1730 inr _ => #NextVar arg ()
1731 | inl e => e) (#Select r)
1732 in
1733 k {New = !new, Old = !old, Outs = sis}
1734 end
1735 | AllCols k =>
1736 let
1737 val (ts, es) =
1738 foldl (fn (si, (ts, es)) =>
1739 case si of
1740 SqField (v, f) =>
1741 let
1742 val fs = getOpt (SM.find (ts, v), SM.empty)
1743 in
1744 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
1745 end
1746 | SqExp (e, f) =>
1747 let
1748 val e =
1749 case expIn e of
1750 inr _ => #NextVar arg ()
1751 | inl e => e
1752 in
1753 (ts, SM.insert (es, f, e))
1754 end)
1755 (SM.empty, SM.empty) (#Select r)
1756 in
1757 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
1758 (SM.listItemsi ts)
1759 @ SM.listItemsi es))
1760 end
1761
1762 fun doWhere final =
1763 (addFrom ();
1764 case #Where r of
1765 NONE => final ()
1766 | SOME e =>
1767 let
1768 val p = case expIn e of
1769 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1770 | inr p => p
1771
1772 val saved = #Save arg ()
1773 in
1774 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
1775 p (fn () => final () handle Cc.Contradiction => ());
1776 #Restore arg saved
1777 end)
1778 handle Cc.Contradiction => ()
1779
1780 fun normal () = doWhere normal'
1781 in
1782 (case #Select r of
1783 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1784 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1785 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1786 (case #Cont arg of
1787 SomeCol _ => ()
1788 | AllCols k =>
1789 let
1790 fun answer e = k (Recd [(f, e)])
1791
1792 val saved = #Save arg ()
1793 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
1794 handle Cc.Contradiction => ()
1795 in
1796 #Restore arg saved;
1797 (*print "True time!\n";*)
1798 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
1799 #Restore arg saved
1800 end)
1801 | _ => normal ())
1802 | _ => normal ())
1803 before #Restore arg saved
1804 end
1805 | Union (q1, q2) =>
1806 let
1807 val saved = #Save arg ()
1808 in
1809 doQuery q1;
1810 #Restore arg saved;
1811 doQuery q2;
1812 #Restore arg saved
1813 end
1814 in
1815 doQuery q
1816 end
1817 end
1818
1819 fun evalPat env e (pt, _) =
1820 case pt of
1821 PWild => env
1822 | PVar _ => e :: env
1823 | PPrim _ => env
1824 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
1825 | PCon (_, pc, SOME pt) =>
1826 let
1827 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
1828 in
1829 St.assert [AReln (PCon1 (patCon pc), [e])];
1830 env
1831 end
1832 | PRecord xpts =>
1833 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
1834 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
1835 | PSome (_, pt) =>
1836 let
1837 val env = evalPat env (Func (UnCon "Some", [e])) pt
1838 in
1839 St.assert [AReln (PCon1 "Some", [e])];
1840 env
1841 end
1842
1843 datatype arg_mode = Fixed | Decreasing | Arbitrary
1844 type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
1845 val rfuns = ref (IM.empty : rfun IM.map)
1846
1847 fun evalExp env (e as (_, loc)) k =
1848 let
1849 (*val () = St.debug ()*)
1850 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
1851
1852 fun default () = k (Var (St.nextVar ()))
1853
1854 fun doFfi (m, s, es) =
1855 if m = "Basis" andalso SS.member (writers, s) then
1856 let
1857 fun doArgs es =
1858 case es of
1859 [] =>
1860 (if s = "set_cookie" then
1861 case es of
1862 [_, cname, _, _, _] =>
1863 (case #1 cname of
1864 EPrim (Prim.String cname) =>
1865 St.havocCookie cname
1866 | _ => ())
1867 | _ => ()
1868 else
1869 ();
1870 k (Recd []))
1871 | e :: es =>
1872 evalExp env e (fn e => (St.send (e, loc); doArgs es))
1873 in
1874 doArgs es
1875 end
1876 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
1877 default ()
1878 else
1879 let
1880 fun doArgs (es, acc) =
1881 case es of
1882 [] => k (Func (Other (m ^ "." ^ s), rev acc))
1883 | e :: es =>
1884 evalExp env e (fn e => doArgs (es, e :: acc))
1885 in
1886 doArgs (es, [])
1887 end
1888 in
1889 case #1 e of
1890 EPrim p => k (Const p)
1891 | ERel n => k (List.nth (env, n))
1892 | ENamed _ => default ()
1893 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
1894 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
1895 | ENone _ => k (Func (DtCon0 "None", []))
1896 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
1897 | EFfi _ => default ()
1898
1899 | EFfiApp ("Basis", "rand", []) =>
1900 let
1901 val e = Var (St.nextVar ())
1902 in
1903 St.assert [AReln (Known, [e])];
1904 k e
1905 end
1906 | EFfiApp x => doFfi x
1907 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
1908
1909 | EApp (e1 as (EError _, _), _) => evalExp env e1 k
1910
1911 | EApp (e1, e2) =>
1912 let
1913 fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
1914 Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
1915 default ())
1916
1917 fun doArgs (e, args) =
1918 case #1 e of
1919 EApp (e1, e2) => doArgs (e1, e2 :: args)
1920 | ENamed n =>
1921 (case IM.find (!rfuns, n) of
1922 NONE => adefault ()
1923 | SOME rf =>
1924 if length (#args rf) <> length args then
1925 adefault ()
1926 else
1927 let
1928 val () = (SS.app (St.havocReln o Sql) (#tables rf);
1929 SS.app St.havocCookie (#cookies rf))
1930 val saved = St.stash ()
1931
1932 fun doArgs (args, modes, env') =
1933 case (args, modes) of
1934 ([], []) => (evalExp env' (#body rf) (fn _ => ());
1935 St.reinstate saved;
1936 default ())
1937
1938 | (arg :: args, mode :: modes) =>
1939 evalExp env arg (fn arg =>
1940 let
1941 val v = case mode of
1942 Arbitrary => Var (St.nextVar ())
1943 | Fixed => arg
1944 | Decreasing =>
1945 let
1946 val v = Var (St.nextVar ())
1947 in
1948 if St.check (AReln (Known, [arg])) then
1949 St.assert [(AReln (Known, [v]))]
1950 else
1951 ();
1952 v
1953 end
1954 in
1955 doArgs (args, modes, v :: env')
1956 end)
1957 | _ => raise Fail "Iflow.doArgs: Impossible"
1958 in
1959 doArgs (args, #args rf, [])
1960 end)
1961 | _ => adefault ()
1962 in
1963 doArgs (e, [])
1964 end
1965
1966 | EAbs _ => default ()
1967 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
1968 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
1969 | ERecord xets =>
1970 let
1971 fun doFields (xes, acc) =
1972 case xes of
1973 [] => k (Recd (rev acc))
1974 | (x, e, _) :: xes =>
1975 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
1976 in
1977 doFields (xets, [])
1978 end
1979 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
1980 | ECase (e, pes, {result = res, ...}) =>
1981 evalExp env e (fn e =>
1982 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
1983 | _ => false) pes then
1984 (St.send (e, loc);
1985 k (Recd []))
1986 else
1987 (St.addPath (e, loc);
1988 app (fn (p, pe) =>
1989 let
1990 val saved = St.stash ()
1991 in
1992 let
1993 val env = evalPat env e p
1994 in
1995 evalExp env pe k;
1996 St.reinstate saved
1997 end
1998 handle Cc.Contradiction => St.reinstate saved
1999 end) pes))
2000 | EStrcat (e1, e2) =>
2001 evalExp env e1 (fn e1 =>
2002 evalExp env e2 (fn e2 =>
2003 k (Func (Other "cat", [e1, e2]))))
2004 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
2005 | EReturnBlob {blob = b, mimeType = m, ...} =>
2006 evalExp env b (fn b =>
2007 (St.send (b, loc);
2008 evalExp env m
2009 (fn m => St.send (m, loc))))
2010 | ERedirect (e, _) =>
2011 evalExp env e (fn e => St.send (e, loc))
2012 | EWrite e =>
2013 evalExp env e (fn e => (St.send (e, loc);
2014 k (Recd [])))
2015 | ESeq (e1, e2) =>
2016 let
2017 val path = St.stashPath ()
2018 in
2019 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
2020 end
2021 | ELet (_, _, e1, e2) =>
2022 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
2023 | EClosure (n, es) =>
2024 let
2025 fun doArgs (es, acc) =
2026 case es of
2027 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
2028 | e :: es =>
2029 evalExp env e (fn e => doArgs (es, e :: acc))
2030 in
2031 doArgs (es, [])
2032 end
2033
2034 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
2035 evalExp env i (fn i =>
2036 let
2037 val r = Var (St.nextVar ())
2038 val acc = Var (St.nextVar ())
2039
2040 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
2041 exp = fn (e, st as (cs, ts)) =>
2042 case e of
2043 EDml e =>
2044 (case parse dml e of
2045 NONE => st
2046 | SOME c =>
2047 case c of
2048 Insert _ => st
2049 | Delete (tab, _) =>
2050 (cs, SS.add (ts, tab))
2051 | Update (tab, _, _) =>
2052 (cs, SS.add (ts, tab)))
2053 | EFfiApp ("Basis", "set_cookie",
2054 [_, (EPrim (Prim.String cname), _),
2055 _, _, _]) =>
2056 (SS.add (cs, cname), ts)
2057 | _ => st}
2058 (SS.empty, SS.empty) b
2059 in
2060 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
2061 (TRecord [], true, true) => ()
2062 | _ =>
2063 let
2064 val saved = St.stash ()
2065 in
2066 (k i)
2067 handle Cc.Contradiction => ();
2068 St.reinstate saved
2069 end;
2070
2071 SS.app (St.havocReln o Sql) ts;
2072 SS.app St.havocCookie cs;
2073
2074 doQuery {Env = env,
2075 NextVar = Var o St.nextVar,
2076 Add = fn a => St.assert [a],
2077 Save = St.stash,
2078 Restore = St.reinstate,
2079 Cont = AllCols (fn x =>
2080 (St.assert [AReln (Eq, [r, x])];
2081 evalExp (acc :: r :: env) b k))} q
2082 end)
2083 | EDml e =>
2084 (case parse dml e of
2085 NONE => (print ("Warning: Information flow checker can't parse DML command at "
2086 ^ ErrorMsg.spanToString loc ^ "\n");
2087 default ())
2088 | SOME d =>
2089 case d of
2090 Insert (tab, es) =>
2091 let
2092 val new = St.nextVar ()
2093
2094 val expIn = expIn (Var o St.nextVar) env
2095 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
2096
2097 val es = map (fn (x, e) =>
2098 case expIn e of
2099 inl e => (x, e)
2100 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
2101 es
2102
2103 val saved = St.stash ()
2104 in
2105 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
2106 St.insert loc;
2107 St.reinstate saved;
2108 St.assert [AReln (Sql tab, [Recd es])];
2109 k (Recd [])
2110 end
2111 | Delete (tab, e) =>
2112 let
2113 val old = St.nextVar ()
2114
2115 val expIn = expIn (Var o St.nextVar) env
2116 (fn "T" => Var old
2117 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
2118
2119 val p = case expIn e of
2120 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
2121 | inr p => p
2122
2123 val saved = St.stash ()
2124 in
2125 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
2126 AReln (Sql (tab), [Var old])];
2127 decomp {Save = St.stash,
2128 Restore = St.reinstate,
2129 Add = fn a => St.assert [a]} p
2130 (fn () => (St.delete loc;
2131 St.reinstate saved;
2132 St.havocReln (Sql tab);
2133 k (Recd []))
2134 handle Cc.Contradiction => ())
2135 end
2136 | Update (tab, fs, e) =>
2137 let
2138 val new = St.nextVar ()
2139 val old = St.nextVar ()
2140
2141 val expIn = expIn (Var o St.nextVar) env
2142 (fn "T" => Var old
2143 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
2144
2145 val fs = map
2146 (fn (x, e) =>
2147 (x, case expIn e of
2148 inl e => e
2149 | inr _ => raise Fail
2150 ("Iflow.evalExp: Selecting "
2151 ^ "boolean expression")))
2152 fs
2153
2154 val fs' = case SM.find (!tabs, tab) of
2155 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
2156 | SOME (fs', _) => fs'
2157
2158 val fs = foldl (fn (f, fs) =>
2159 if List.exists (fn (f', _) => f' = f) fs then
2160 fs
2161 else
2162 (f, Proj (Var old, f)) :: fs) fs fs'
2163
2164 val p = case expIn e of
2165 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
2166 | inr p => p
2167 val saved = St.stash ()
2168 in
2169 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
2170 AReln (Sql (tab ^ "$Old"), [Var old]),
2171 AReln (Sql tab, [Var old])];
2172 decomp {Save = St.stash,
2173 Restore = St.reinstate,
2174 Add = fn a => St.assert [a]} p
2175 (fn () => (St.update loc;
2176 St.reinstate saved;
2177 St.havocReln (Sql tab);
2178 k (Recd []))
2179 handle Cc.Contradiction => ())
2180 end)
2181
2182 | ENextval (EPrim (Prim.String seq), _) =>
2183 let
2184 val nv = St.nextVar ()
2185 in
2186 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
2187 k (Var nv)
2188 end
2189 | ENextval _ => default ()
2190 | ESetval _ => default ()
2191
2192 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
2193 let
2194 val e = Var (St.nextVar ())
2195 val e' = Func (Other ("cookie/" ^ cname), [])
2196 in
2197 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
2198 k e
2199 end
2200
2201 | EUnurlify _ => default ()
2202 | EJavaScript _ => default ()
2203 | ESignalReturn _ => default ()
2204 | ESignalBind _ => default ()
2205 | ESignalSource _ => default ()
2206 | EServerCall _ => default ()
2207 | ERecv _ => default ()
2208 | ESleep _ => default ()
2209 | ESpawn _ => default ()
2210 end
2211
2212 datatype var_source = Input of int | SubInput of int | Unknown
2213
2214 fun check file =
2215 let
2216 val () = (St.reset ();
2217 rfuns := IM.empty)
2218
2219 val file = MonoReduce.reduce file
2220 val file = MonoOpt.optimize file
2221 val file = Fuse.fuse file
2222 val file = MonoOpt.optimize file
2223 val file = MonoShake.shake file
2224 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
2225
2226 val exptd = foldl (fn ((d, _), exptd) =>
2227 case d of
2228 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
2229 | _ => exptd) IS.empty file
2230
2231 fun decl (d, loc) =
2232 case d of
2233 DTable (tab, fs, pk, _) =>
2234 let
2235 val ks =
2236 case #1 pk of
2237 EPrim (Prim.String s) =>
2238 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
2239 [] => []
2240 | pk => [pk])
2241 | _ => []
2242 in
2243 if size tab >= 3 then
2244 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
2245 (map #1 fs,
2246 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
2247 ^ String.extract (s, 4, NONE))) ks))
2248 else
2249 raise Fail "Table name does not begin with uw_"
2250 end
2251 | DVal (x, n, _, e, _) =>
2252 let
2253 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
2254
2255 val isExptd = IS.member (exptd, n)
2256
2257 val saved = St.stash ()
2258
2259 fun deAbs (e, env, ps) =
2260 case #1 e of
2261 EAbs (_, _, _, e) =>
2262 let
2263 val nv = Var (St.nextVar ())
2264 in
2265 deAbs (e, nv :: env,
2266 if isExptd then
2267 AReln (Known, [nv]) :: ps
2268 else
2269 ps)
2270 end
2271 | _ => (e, env, ps)
2272
2273 val (e, env, ps) = deAbs (e, [], [])
2274 in
2275 St.assert ps;
2276 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
2277 St.reinstate saved
2278 end
2279
2280 | DValRec [(x, n, _, e, _)] =>
2281 let
2282 val tables = ref SS.empty
2283 val cookies = ref SS.empty
2284
2285 fun deAbs (e, env, modes) =
2286 case #1 e of
2287 EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
2288 | _ => (e, env, rev modes)
2289
2290 val (e, env, modes) = deAbs (e, [], [])
2291
2292 fun doExp env (e as (_, loc)) =
2293 case #1 e of
2294 EPrim _ => e
2295 | ERel _ => e
2296 | ENamed _ => e
2297 | ECon (_, _, NONE) => e
2298 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
2299 | ENone _ => e
2300 | ESome (t, e) => (ESome (t, doExp env e), loc)
2301 | EFfi _ => e
2302 | EFfiApp (m, f, es) =>
2303 (case (m, f, es) of
2304 ("Basis", "set_cookie", [_, (EPrim (Prim.String cname), _), _, _, _]) =>
2305 cookies := SS.add (!cookies, cname)
2306 | _ => ();
2307 (EFfiApp (m, f, map (doExp env) es), loc))
2308
2309 | EApp (e1, e2) =>
2310 let
2311 fun default () = (EApp (doExp env e1, doExp env e2), loc)
2312
2313 fun explore (e, args) =
2314 case #1 e of
2315 EApp (e1, e2) => explore (e1, e2 :: args)
2316 | ENamed n' =>
2317 if n' = n then
2318 let
2319 fun doArgs (pos, args, modes) =
2320 case (args, modes) of
2321 ((e1, _) :: args, m1 :: modes) =>
2322 (case e1 of
2323 ERel n =>
2324 (case List.nth (env, n) of
2325 Input pos' =>
2326 if pos' = pos then
2327 ()
2328 else
2329 m1 := Arbitrary
2330 | SubInput pos' =>
2331 if pos' = pos then
2332 if !m1 = Arbitrary then
2333 ()
2334 else
2335 m1 := Decreasing
2336 else
2337 m1 := Arbitrary
2338 | Unknown => m1 := Arbitrary)
2339 | _ => m1 := Arbitrary;
2340 doArgs (pos + 1, args, modes))
2341 | (_ :: _, []) => ()
2342 | ([], ms) => app (fn m => m := Arbitrary) ms
2343 in
2344 doArgs (0, args, modes);
2345 (EFfi ("Basis", "?"), loc)
2346 end
2347 else
2348 default ()
2349 | _ => default ()
2350 in
2351 explore (e, [])
2352 end
2353 | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
2354 | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
2355 | EBinop (bo, e1, e2) => (EBinop (bo, doExp env e1, doExp env e2), loc)
2356 | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
2357 | EField (e1, f) => (EField (doExp env e1, f), loc)
2358 | ECase (e, pes, ts) =>
2359 let
2360 val source =
2361 case #1 e of
2362 ERel n =>
2363 (case List.nth (env, n) of
2364 Input n => SOME n
2365 | SubInput n => SOME n
2366 | Unknown => NONE)
2367 | _ => NONE
2368
2369 fun doV v =
2370 let
2371 fun doPat (p, env) =
2372 case #1 p of
2373 PWild => env
2374 | PVar _ => v :: env
2375 | PPrim _ => env
2376 | PCon (_, _, NONE) => env
2377 | PCon (_, _, SOME p) => doPat (p, env)
2378 | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
2379 | PNone _ => env
2380 | PSome (_, p) => doPat (p, env)
2381 in
2382 (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
2383 end
2384 in
2385 case source of
2386 NONE => doV Unknown
2387 | SOME inp => doV (SubInput inp)
2388 end
2389 | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
2390 | EError (e1, t) => (EError (doExp env e1, t), loc)
2391 | EReturnBlob {blob = b, mimeType = m, t} =>
2392 (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
2393 | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
2394 | EWrite e1 => (EWrite (doExp env e1), loc)
2395 | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
2396 | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
2397 | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
2398 | EQuery {exps, tables, state, query, body, initial} =>
2399 (EQuery {exps = exps, tables = tables, state = state,
2400 query = doExp env query,
2401 body = doExp (Unknown :: Unknown :: env) body,
2402 initial = doExp env initial}, loc)
2403 | EDml e1 =>
2404 (case parse dml e1 of
2405 NONE => ()
2406 | SOME c =>
2407 case c of
2408 Insert _ => ()
2409 | Delete (tab, _) =>
2410 tables := SS.add (!tables, tab)
2411 | Update (tab, _, _) =>
2412 tables := SS.add (!tables, tab);
2413 (EDml (doExp env e1), loc))
2414 | ENextval e1 => (ENextval (doExp env e1), loc)
2415 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
2416 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
2417 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
2418 | ESignalReturn _ => e
2419 | ESignalBind _ => e
2420 | ESignalSource _ => e
2421 | EServerCall _ => e
2422 | ERecv _ => e
2423 | ESleep _ => e
2424 | ESpawn _ => e
2425
2426 val e = doExp env e
2427 in
2428 rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
2429 args = map (fn r => !r) modes, body = e})
2430 end
2431
2432 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
2433
2434 | DPolicy pol =>
2435 let
2436 val rvN = ref 0
2437 fun rv () =
2438 let
2439 val n = !rvN
2440 in
2441 rvN := n + 1;
2442 Lvar n
2443 end
2444
2445 val atoms = ref ([] : atom list)
2446 fun doQ k = doQuery {Env = [],
2447 NextVar = rv,
2448 Add = fn a => atoms := a :: !atoms,
2449 Save = fn () => !atoms,
2450 Restore = fn ls => atoms := ls,
2451 Cont = SomeCol (fn r => k (rev (!atoms), r))}
2452
2453 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
2454 tab' <> tab
2455 orelse List.all (fn Lvar lv' => lv' <> lv
2456 | _ => false) nams
2457 | _ => true)
2458 in
2459 case pol of
2460 PolClient e =>
2461 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
2462 | PolInsert e =>
2463 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
2464 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
2465 | _ => raise Fail "Iflow: No New in mayInsert policy") e
2466 | PolDelete e =>
2467 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
2468 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
2469 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
2470 | PolUpdate e =>
2471 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
2472 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
2473 :: AReln (Sql (tab ^ "$New"), [new])
2474 :: untab (tab, [new, old]) ats)
2475 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
2476 | PolSequence e =>
2477 (case #1 e of
2478 EPrim (Prim.String seq) =>
2479 let
2480 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
2481 val outs = [Lvar 0]
2482 in
2483 St.allowSend ([p], outs)
2484 end
2485 | _ => ())
2486 end
2487
2488 | _ => ()
2489 in
2490 app decl file
2491 end
2492
2493 val check = fn file =>
2494 let
2495 val oldInline = Settings.getMonoInline ()
2496 in
2497 (Settings.setMonoInline (case Int.maxInt of
2498 NONE => 1000000
2499 | SOME n => n);
2500 check file;
2501 Settings.setMonoInline oldInline)
2502 handle ex => (Settings.setMonoInline oldInline;
2503 raise ex)
2504 end
2505
2506 end