Mercurial > urweb

comparison src/iflow.sml @ 1211:1d4d65245dd3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
About to try removing Select predicate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 13:59:16 -0400
parents c5bd970e77a5
children fc33072c4d33
comparison
equal deleted inserted replaced
1210:c5bd970e77a5 1211:1d4d65245dd3
65 | Finish 65 | Finish
66 66
67 datatype reln = 67 datatype reln =
68 Known 68 Known
69 | Sql of string 69 | Sql of string
70 | DtCon of string
70 | Eq 71 | Eq
71 | Ne 72 | Ne
72 | Lt 73 | Lt
73 | Le 74 | Le
74 | Gt 75 | Gt
125 string ")"] 126 string ")"]
126 | _ => raise Fail "Iflow.p_reln: Known") 127 | _ => raise Fail "Iflow.p_reln: Known")
127 | Sql s => box [string (s ^ "("), 128 | Sql s => box [string (s ^ "("),
128 p_list p_exp es, 129 p_list p_exp es,
129 string ")"] 130 string ")"]
131 | DtCon s => box [string (s ^ "("),
132 p_list p_exp es,
133 string ")"]
130 | Eq => p_bop "=" es 134 | Eq => p_bop "=" es
131 | Ne => p_bop "<>" es 135 | Ne => p_bop "<>" es
132 | Lt => p_bop "<" es 136 | Lt => p_bop "<" es
133 | Le => p_bop "<=" es 137 | Le => p_bop "<=" es
134 | Gt => p_bop ">" es 138 | Gt => p_bop ">" es
239 NONE => e 243 NONE => e
240 | SOME e => simplify e) 244 | SOME e => simplify e)
241 | Func (f, es) => 245 | Func (f, es) =>
242 let 246 let
243 val es = map simplify es 247 val es = map simplify es
248
249 fun default () = Func (f, es)
244 in 250 in
245 if List.exists isFinish es then 251 if List.exists isFinish es then
246 Finish 252 Finish
253 else if String.isPrefix "un" f then
254 case es of
255 [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then
256 e
257 else
258 default ()
259 | _ => default ()
247 else 260 else
248 Func (f, es) 261 default ()
249 end 262 end
250 | Recd xes => 263 | Recd xes =>
251 let 264 let
252 val xes = map (fn (x, e) => (x, simplify e)) xes 265 val xes = map (fn (x, e) => (x, simplify e)) xes
253 in 266 in
349 else 362 else
350 (restore saved; 363 (restore saved;
351 false) 364 false)
352 end 365 end
353 366
354 exception Imply of prop * prop
355
356 val debug = ref false 367 val debug = ref false
357 368
369 fun eeq (e1, e2) =
370 case (e1, e2) of
371 (Const p1, Const p2) => Prim.equal (p1, p2)
372 | (Var n1, Var n2) => n1 = n2
373 | (Lvar n1, Lvar n2) => n1 = n2
374 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
375 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
376 List.all (fn (x2, e2) =>
377 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
378 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
379 | (Finish, Finish) => true
380 | _ => false
381
358 (* Congruence closure *) 382 (* Congruence closure *)
359 structure Cc :> sig 383 structure Cc :> sig
360 type t 384 type t
361 val empty : t 385 val empty : t
362 val assert : t * exp * exp -> t 386 val assert : t * exp * exp -> t
363 val query : t * exp * exp -> bool 387 val query : t * exp * exp -> bool
364 val allPeers : t * exp -> exp list 388 val allPeers : t * exp -> exp list
365 end = struct 389 end = struct
366 390
367 fun eq' (e1, e2) = 391 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
368 case (e1, e2) of
369 (Const p1, Const p2) => Prim.equal (p1, p2)
370 | (Var n1, Var n2) => n1 = n2
371 | (Lvar n1, Lvar n2) => n1 = n2
372 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
373 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
374 List.all (fn (x2, e2) =>
375 List.exists (fn (x1, e1) => x1 = x2 andalso eq' (e1, e2)) xes2) xes1
376 | (Proj (e1, x1), Proj (e2, x2)) => eq' (e1, e2) andalso x1 = x2
377 | (Finish, Finish) => true
378 | _ => false
379
380 fun eq (e1, e2) = eq' (simplify e1, simplify e2)
381 392
382 type t = (exp * exp) list 393 type t = (exp * exp) list
383 394
384 val empty = [] 395 val empty = []
385 396
473 let 484 let
474 fun matches e = 485 fun matches e =
475 case e of 486 case e of
476 Var v' => v' = v 487 Var v' => v' = v
477 | Proj (e, _) => matches e 488 | Proj (e, _) => matches e
489 | Func (f, [e]) => String.isPrefix "un" f andalso matches e
478 | _ => false 490 | _ => false
479 in 491 in
480 List.exists matches (Cc.allPeers (cc, e2)) 492 List.exists matches (Cc.allPeers (cc, e2))
481 end 493 end
482 | _ => false) 494 | _ => false)
526 (Eq, [e1, e2]) => Cc.query (cc, e1, e2) 538 (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
527 | _ => false) 539 | _ => false)
528 orelse hps hyps 540 orelse hps hyps
529 end 541 end
530 in 542 in
531 gls goals (fn () => false) 543 if List.exists (fn (DtCon c1, [e]) =>
544 List.exists (fn (DtCon c2, [e']) =>
545 c1 <> c2 andalso
546 Cc.query (cc, e, e')
547 | _ => false) hyps
548 orelse List.exists (fn Func (c2, []) => c1 <> c2
549 | Finish => true
550 | _ => false)
551 (Cc.allPeers (cc, e))
552 | _ => false) hyps
553 orelse gls goals (fn () => false) then
554 true
555 else
556 (Print.prefaces "Can't prove"
557 [("hyps", Print.p_list (fn x => p_prop (Reln x)) hyps),
558 ("goals", Print.p_list (fn x => p_prop (Reln x)) goals)];
559 false)
532 end)) 560 end))
533 in 561 in
534 reset (); 562 reset ();
535 doOne false; 563 doOne false;
536 doOne true 564 doOne true
666 wrap (ws p) (fn v => [v]), 694 wrap (ws p) (fn v => [v]),
667 always []] chs 695 always []] chs
668 696
669 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_") 697 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
670 698
671 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then 699 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
672 String.extract (s, 2, NONE) 700 SOME (String.extract (s, 2, NONE))
673 else
674 raise Fail "Iflow: Bad table variable")
675 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
676 str (Char.toUpper (String.sub (s, 3)))
677 ^ String.extract (s, 4, NONE)
678 else 701 else
679 raise Fail "Iflow: Bad uw_* variable") 702 NONE)
680 703 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
681 val sitem = wrap (follow t_ident 704 SOME (str (Char.toUpper (String.sub (s, 3)))
705 ^ String.extract (s, 4, NONE))
706 else
707 NONE)
708
709 val field = wrap (follow t_ident
682 (follow (const ".") 710 (follow (const ".")
683 uw_ident)) 711 uw_ident))
684 (fn (t, ((), f)) => (t, f)) 712 (fn (t, ((), f)) => (t, f))
685 713
686 datatype Rel = 714 datatype Rel =
691 SqConst of Prim.t 719 SqConst of Prim.t
692 | Field of string * string 720 | Field of string * string
693 | Binop of Rel * sqexp * sqexp 721 | Binop of Rel * sqexp * sqexp
694 | SqKnown of sqexp 722 | SqKnown of sqexp
695 | Inj of Mono.exp 723 | Inj of Mono.exp
724 | SqFunc of string * sqexp
725 | Count
696 726
697 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2]))) 727 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
698 728
699 val sqbrel = altL [cmp "=" Eq, 729 val sqbrel = altL [cmp "=" Eq,
700 cmp "<>" Ne, 730 cmp "<>" Ne,
756 SOME (e, chs) 786 SOME (e, chs)
757 else 787 else
758 NONE 788 NONE
759 | _ => NONE 789 | _ => NONE
760 790
791 fun constK s = wrap (const s) (fn () => s)
792
793 val funcName = altL [constK "COUNT",
794 constK "MIN",
795 constK "MAX",
796 constK "SUM",
797 constK "AVG"]
798
761 fun sqexp chs = 799 fun sqexp chs =
762 log "sqexp" 800 log "sqexp"
763 (altL [wrap prim SqConst, 801 (altL [wrap prim SqConst,
764 wrap sitem Field, 802 wrap field Field,
765 wrap known SqKnown, 803 wrap known SqKnown,
804 wrap func SqFunc,
805 wrap (const "COUNT(*)") (fn () => Count),
766 wrap sqlify Inj, 806 wrap sqlify Inj,
807 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
808 (follow (keep (fn ch => ch <> #")")) (const ")")))))
809 (fn ((), (e, _)) => e),
767 wrap (follow (ws (const "(")) 810 wrap (follow (ws (const "("))
768 (follow (wrap 811 (follow (wrap
769 (follow sqexp 812 (follow sqexp
770 (alt 813 (alt
771 (wrap 814 (wrap
780 (const ")"))) 823 (const ")")))
781 (fn ((), (e, ())) => e)]) 824 (fn ((), (e, ())) => e)])
782 chs 825 chs
783 826
784 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")")))) 827 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
785 (fn ((), ((), (e, ()))) => e) chs 828 (fn ((), ((), (e, ()))) => e) chs
829
830 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
831 (fn (f, ((), (e, ()))) => (f, e)) chs
832
833 datatype sitem =
834 SqField of string * string
835 | SqExp of sqexp * string
836
837 val sitem = alt (wrap field SqField)
838 (wrap (follow sqexp (follow (const " AS ") uw_ident))
839 (fn (e, ((), s)) => SqExp (e, s)))
786 840
787 val select = log "select" 841 val select = log "select"
788 (wrap (follow (const "SELECT ") (list sitem)) 842 (wrap (follow (const "SELECT ") (list sitem))
789 (fn ((), ls) => ls)) 843 (fn ((), ls) => ls))
790 844
801 (fn ((), ls) => ls) 855 (fn ((), ls) => ls)
802 856
803 val query = log "query" 857 val query = log "query"
804 (wrap (follow (follow select from) (opt wher)) 858 (wrap (follow (follow select from) (opt wher))
805 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) 859 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
860
861 fun removeDups ls =
862 case ls of
863 [] => []
864 | x :: ls =>
865 let
866 val ls = removeDups ls
867 in
868 if List.exists (fn x' => x' = x) ls then
869 ls
870 else
871 x :: ls
872 end
806 873
807 fun queryProp env rv oe e = 874 fun queryProp env rv oe e =
808 case parse query e of 875 case parse query e of
809 NONE => (print ("Warning: Information flow checker can't parse SQL query at " 876 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
810 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 877 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
811 (Unknown, [])) 878 (Unknown, []))
812 | SOME r => 879 | SOME r =>
813 let 880 let
881 fun usedFields e =
882 case e of
883 SqConst _ => []
884 | Field (v, f) => [(v, f)]
885 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
886 | SqKnown _ => []
887 | Inj _ => []
888 | SqFunc (_, e) => usedFields e
889 | Count => []
890
891 val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r)
892 @ (case #Where r of
893 NONE => []
894 | SOME e => usedFields e))
895
814 val p = 896 val p =
815 foldl (fn ((t, v), p) => 897 foldl (fn ((t, v), p) =>
816 And (p, 898 And (p,
817 Reln (Sql t, 899 Reln (Sql t,
818 [Recd (foldl (fn ((v', f), fs) => 900 [Recd (foldl (fn ((v', f), fs) =>
819 if v' = v then 901 if v' = v then
820 (f, Proj (Proj (Lvar rv, v), f)) :: fs 902 (f, Proj (Proj (Lvar rv, v), f)) :: fs
821 else 903 else
822 fs) [] (#Select r))]))) 904 fs) [] allUsed)])))
823 True (#From r) 905 True (#From r)
824 906
825 fun expIn e = 907 fun expIn e =
826 case e of 908 case e of
827 SqConst p => inl (Const p) 909 SqConst p => inl (Const p)
843 | EField (e, f) => Proj (deinj e, f) 925 | EField (e, f) => Proj (deinj e, f)
844 | _ => raise Fail "Iflow: non-variable injected into query" 926 | _ => raise Fail "Iflow: non-variable injected into query"
845 in 927 in
846 inl (deinj e) 928 inl (deinj e)
847 end 929 end
848 930 | SqFunc (f, e) =>
849 fun usedFields e = 931 inl (case expIn e of
850 case e of 932 inl e => Func (f, [e])
851 SqConst _ => [] 933 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
852 | Field (v, f) => [Proj (Proj (Lvar rv, v), f)] 934 | Count => inl (Func ("COUNT", []))
853 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
854 | SqKnown _ => []
855 | Inj _ => []
856 935
857 val p = case #Where r of 936 val p = case #Where r of
858 NONE => p 937 NONE => p
859 | SOME e => 938 | SOME e =>
860 case expIn e of 939 case expIn e of
862 | _ => p 941 | _ => p
863 in 942 in
864 (case oe of 943 (case oe of
865 NONE => p 944 NONE => p
866 | SOME oe => 945 | SOME oe =>
867 And (p, foldl (fn ((v, f), p) => 946 And (p, foldl (fn (si, p) =>
868 Or (p, 947 let
869 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) 948 val p' = case si of
949 SqField (v, f) => Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])
950 | SqExp (e, f) =>
951 case expIn e of
952 inr _ => Unknown
953 | inl e => Reln (Eq, [oe, e])
954 in
955 Or (p, p')
956 end)
870 False (#Select r)), 957 False (#Select r)),
871 958
872 case #Where r of 959 case #Where r of
873 NONE => [] 960 NONE => []
874 | SOME e => usedFields e) 961 | SOME e => map (fn (v, f) => Proj (Proj (Lvar rv, v), f)) (usedFields e))
875 end 962 end
963
964 fun evalPat env e (pt, _) =
965 case pt of
966 PWild => (env, True)
967 | PVar _ => (e :: env, True)
968 | PPrim _ => (env, True)
969 | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e]))
970 | PCon (_, pc, SOME pt) =>
971 let
972 val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt
973 in
974 (env, And (p, Reln (DtCon (patCon pc), [e])))
975 end
976 | PRecord xpts =>
977 foldl (fn ((x, pt, _), (env, p)) =>
978 let
979 val (env, p') = evalPat env (Proj (e, x)) pt
980 in
981 (env, And (p', p))
982 end) (env, True) xpts
983 | PNone _ => (env, Reln (DtCon "None", [e]))
984 | PSome (_, pt) =>
985 let
986 val (env, p) = evalPat env (Func ("unSome", [e])) pt
987 in
988 (env, And (p, Reln (DtCon "Some", [e])))
989 end
990
991 fun peq (p1, p2) =
992 case (p1, p2) of
993 (True, True) => true
994 | (False, False) => true
995 | (Unknown, Unknown) => true
996 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
997 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
998 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
999 | (Select (n1, n2, n3, p1, e1), Select (n1', n2', n3', p2, e2)) =>
1000 n1 = n1' andalso n2 = n2' andalso n3 = n3'
1001 andalso peq (p1, p2) andalso eeq (e1, e2)
1002 | _ => false
1003
1004 fun removeRedundant p1 =
1005 let
1006 fun rr p2 =
1007 if peq (p1, p2) then
1008 True
1009 else
1010 case p2 of
1011 And (x, y) => And (rr x, rr y)
1012 | Or (x, y) => Or (rr x, rr y)
1013 | Select (n1, n2, n3, p, e) => Select (n1, n2, n3, rr p, e)
1014 | _ => p2
1015 in
1016 rr
1017 end
876 1018
877 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = 1019 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
878 let 1020 let
879 fun default () = 1021 fun default () =
880 (Var nv, (nv+1, p, sent)) 1022 (Var nv, (nv+1, p, sent))
949 let 1091 let
950 val (e, st) = evalExp env (e, st) 1092 val (e, st) = evalExp env (e, st)
951 in 1093 in
952 (Proj (e, s), st) 1094 (Proj (e, s), st)
953 end 1095 end
954 | ECase _ => default () 1096 | ECase (e, pes, _) =>
1097 let
1098 val (e, st) = evalExp env (e, st)
1099 val r = #1 st
1100 val st = (r + 1, #2 st, #3 st)
1101 val orig = #2 st
1102
1103 val st = foldl (fn ((pt, pe), st) =>
1104 let
1105 val (env, pp) = evalPat env e pt
1106 val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st))
1107
1108 val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe]))
1109 in
1110 (#1 st', Or (#2 st, this), #3 st')
1111 end) (#1 st, False, #3 st) pes
1112 in
1113 (Var r, (#1 st, And (orig, #2 st), #3 st))
1114 end
955 | EStrcat (e1, e2) => 1115 | EStrcat (e1, e2) =>
956 let 1116 let
957 val (e1, st) = evalExp env (e1, st) 1117 val (e1, st) = evalExp env (e1, st)
958 val (e2, st) = evalExp env (e2, st) 1118 val (e2, st) = evalExp env (e2, st)
959 in 1119 in