Mercurial > urweb

comparison src/iflow.sml @ 1212:fc33072c4d33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced Select predicate with special-case handling for one-or-no-rows queries
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 15:17:28 -0400
parents 1d4d65245dd3
children e791d93d4616
comparison
equal deleted inserted replaced
1211:1d4d65245dd3 1212:fc33072c4d33
80 | False 80 | False
81 | Unknown 81 | Unknown
82 | And of prop * prop 82 | And of prop * prop
83 | Or of prop * prop 83 | Or of prop * prop
84 | Reln of reln * exp list 84 | Reln of reln * exp list
85 | Select of int * lvar * lvar * prop * exp 85 | Cond of exp * prop
86 86
87 local 87 local
88 open Print 88 open Print
89 val string = PD.string 89 val string = PD.string
90 in 90 in
160 space, 160 space,
161 string "(", 161 string "(",
162 p_prop p2, 162 p_prop p2,
163 string ")"] 163 string ")"]
164 | Reln (r, es) => p_reln r es 164 | Reln (r, es) => p_reln r es
165 | Select (n1, n2, n3, p, e) => box [string ("select(x" ^ Int.toString n1 165 | Cond (e, p) => box [string "(",
166 ^ ",X" ^ Int.toString n2 166 p_exp e,
167 ^ ",X" ^ Int.toString n3 167 space,
168 ^ "){"), 168 string "==",
169 p_prop p, 169 space,
170 string "}{", 170 p_prop p,
171 p_exp e, 171 string ")"]
172 string "}"]
173 172
174 end 173 end
175 174
176 local 175 local
177 val count = ref 1 176 val count = ref 1
182 in 181 in
183 count := n + 1; 182 count := n + 1;
184 n 183 n
185 end 184 end
186 end 185 end
187
188 fun subExp (v, lv) =
189 let
190 fun sub e =
191 case e of
192 Const _ => e
193 | Var v' => if v' = v then Lvar lv else e
194 | Lvar _ => e
195 | Func (f, es) => Func (f, map sub es)
196 | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
197 | Proj (e, s) => Proj (sub e, s)
198 | Finish => Finish
199 in
200 sub
201 end
202
203 fun subProp (v, lv) =
204 let
205 fun sub p =
206 case p of
207 True => p
208 | False => p
209 | Unknown => p
210 | And (p1, p2) => And (sub p1, sub p2)
211 | Or (p1, p2) => Or (sub p1, sub p2)
212 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
213 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
214 in
215 sub
216 end
217 186
218 fun isKnown e = 187 fun isKnown e =
219 case e of 188 case e of
220 Const _ => true 189 Const _ => true
221 | Func (_, es) => List.all isKnown es 190 | Func (_, es) => List.all isKnown es
278 Finish 247 Finish
279 else 248 else
280 Proj (e', s)) 249 Proj (e', s))
281 | Finish => Finish 250 | Finish => Finish
282 251
252 datatype atom =
253 AReln of reln * exp list
254 | ACond of exp * prop
255
256 fun p_atom a =
257 p_prop (case a of
258 AReln x => Reln x
259 | ACond x => Cond x)
260
283 fun decomp fals or = 261 fun decomp fals or =
284 let 262 let
285 fun decomp p k = 263 fun decomp p k =
286 case p of 264 case p of
287 True => k [] 265 True => k []
291 decomp p1 (fn ps1 => 269 decomp p1 (fn ps1 =>
292 decomp p2 (fn ps2 => 270 decomp p2 (fn ps2 =>
293 k (ps1 @ ps2))) 271 k (ps1 @ ps2)))
294 | Or (p1, p2) => 272 | Or (p1, p2) =>
295 or (decomp p1 k, fn () => decomp p2 k) 273 or (decomp p1 k, fn () => decomp p2 k)
296 | Reln x => k [x] 274 | Reln x => k [AReln x]
297 | Select _ => k [] 275 | Cond x => k [ACond x]
298 in 276 in
299 decomp 277 decomp
300 end 278 end
301 279
302 fun lvarIn lv = 280 fun lvarIn lv =
308 | Lvar lv' => lv' = lv 286 | Lvar lv' => lv' = lv
309 | Func (_, es) => List.exists lvi es 287 | Func (_, es) => List.exists lvi es
310 | Recd xes => List.exists (lvi o #2) xes 288 | Recd xes => List.exists (lvi o #2) xes
311 | Proj (e, _) => lvi e 289 | Proj (e, _) => lvi e
312 | Finish => false 290 | Finish => false
291 in
292 lvi
293 end
294
295 fun lvarInP lv =
296 let
297 fun lvi p =
298 case p of
299 True => false
300 | False => false
301 | Unknown => true
302 | And (p1, p2) => lvi p1 orelse lvi p2
303 | Or (p1, p2) => lvi p1 orelse lvi p2
304 | Reln (_, es) => List.exists (lvarIn lv) es
305 | Cond (e, p) => lvarIn lv e orelse lvi p
306 in
307 lvi
308 end
309
310 fun varIn lv =
311 let
312 fun lvi e =
313 case e of
314 Const _ => false
315 | Lvar _ => false
316 | Var lv' => lv' = lv
317 | Func (_, es) => List.exists lvi es
318 | Recd xes => List.exists (lvi o #2) xes
319 | Proj (e, _) => lvi e
320 | Finish => false
321 in
322 lvi
323 end
324
325 fun varInP lv =
326 let
327 fun lvi p =
328 case p of
329 True => false
330 | False => false
331 | Unknown => false
332 | And (p1, p2) => lvi p1 orelse lvi p2
333 | Or (p1, p2) => lvi p1 orelse lvi p2
334 | Reln (_, es) => List.exists (varIn lv) es
335 | Cond (e, p) => varIn lv e orelse lvi p
313 in 336 in
314 lvi 337 lvi
315 end 338 end
316 339
317 fun eq' (e1, e2) = 340 fun eq' (e1, e2) =
397 fun lookup (t, e) = 420 fun lookup (t, e) =
398 case List.find (fn (e', _) => eq (e', e)) t of 421 case List.find (fn (e', _) => eq (e', e)) t of
399 NONE => e 422 NONE => e
400 | SOME (_, e2) => lookup (t, e2) 423 | SOME (_, e2) => lookup (t, e2)
401 424
402 fun assert (t, e1, e2) =
403 let
404 val r1 = lookup (t, e1)
405 val r2 = lookup (t, e2)
406 in
407 if eq (r1, r2) then
408 t
409 else
410 (r1, r2) :: t
411 end
412
413 open Print
414
415 fun query (t, e1, e2) =
416 (if !debug then
417 prefaces "CC query" [("e1", p_exp (simplify e1)),
418 ("e2", p_exp (simplify e2)),
419 ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
420 space,
421 PD.string "->",
422 space,
423 p_exp (simplify e2)]) t)]
424 else
425 ();
426 eq (lookup (t, e1), lookup (t, e2)))
427
428 fun allPeers (t, e) = 425 fun allPeers (t, e) =
429 let 426 let
430 val r = lookup (t, e) 427 val r = lookup (t, e)
431 in 428 in
432 r :: List.mapPartial (fn (e1, e2) => 429 r :: List.mapPartial (fn (e1, e2) =>
437 SOME e1 434 SOME e1
438 else 435 else
439 NONE 436 NONE
440 end) t 437 end) t
441 end 438 end
439
440 fun assert (t, e1, e2) =
441 let
442 val r1 = lookup (t, e1)
443 val r2 = lookup (t, e2)
444
445 fun doUn (t', e1, e2) =
446 case e2 of
447 Func (f, [e]) =>
448 if String.isPrefix "un" f then
449 let
450 val f' = String.extract (f, 2, NONE)
451 in
452 foldl (fn (e', t') =>
453 case e' of
454 Func (f'', [e'']) =>
455 if f'' = f' then
456 (lookup (t', e1), e'') :: t'
457 else
458 t'
459 | _ => t') t' (allPeers (t, e))
460 end
461 else
462 t'
463 | _ => t'
464 in
465 if eq (r1, r2) then
466 t
467 else
468 doUn (doUn ((r1, r2) :: t, e1, e2), e2, e1)
469 end
470
471 open Print
472
473 fun query (t, e1, e2) =
474 ((*prefaces "CC query" [("e1", p_exp (simplify e1)),
475 ("e2", p_exp (simplify e2)),
476 ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
477 space,
478 PD.string "->",
479 space,
480 p_exp (simplify e2)]) t)];*)
481 eq (lookup (t, e1), lookup (t, e2)))
442 482
443 end 483 end
444 484
445 fun rimp cc ((r1, es1), (r2, es2)) = 485 fun rimp cc ((r1, es1), (r2, es2)) =
446 case (r1, r2) of 486 case (r1, r2) of
502 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 542 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
503 (fn goals => 543 (fn goals =>
504 let 544 let
505 val cc = foldl (fn (p, cc) => 545 val cc = foldl (fn (p, cc) =>
506 case p of 546 case p of
507 (Eq, [e1, e2]) => Cc.assert (cc, e1, e2) 547 AReln (Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
508 | _ => cc) Cc.empty hyps 548 | _ => cc) Cc.empty hyps
509 549
510 fun gls goals onFail = 550 fun gls goals onFail =
511 case goals of 551 case goals of
512 [] => true 552 [] => true
513 | g :: goals => 553 | ACond _ :: _ => false
554 | AReln g :: goals =>
514 case (doKnown, g) of 555 case (doKnown, g) of
515 (false, (Known, _)) => gls goals onFail 556 (false, (Known, _)) => gls goals onFail
516 | _ => 557 | _ =>
517 let 558 let
518 fun hps hyps = 559 fun hps hyps =
519 case hyps of 560 case hyps of
520 [] => onFail () 561 [] => onFail ()
521 | h :: hyps => 562 | ACond _ :: hyps => hps hyps
563 | AReln h :: hyps =>
522 let 564 let
523 val saved = save () 565 val saved = save ()
524 in 566 in
525 if rimp cc (h, g) then 567 if rimp cc (h, g) then
526 let 568 let
538 (Eq, [e1, e2]) => Cc.query (cc, e1, e2) 580 (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
539 | _ => false) 581 | _ => false)
540 orelse hps hyps 582 orelse hps hyps
541 end 583 end
542 in 584 in
543 if List.exists (fn (DtCon c1, [e]) => 585 if List.exists (fn AReln (DtCon c1, [e]) =>
544 List.exists (fn (DtCon c2, [e']) => 586 List.exists (fn AReln (DtCon c2, [e']) =>
545 c1 <> c2 andalso 587 c1 <> c2 andalso
546 Cc.query (cc, e, e') 588 Cc.query (cc, e, e')
547 | _ => false) hyps 589 | _ => false) hyps
548 orelse List.exists (fn Func (c2, []) => c1 <> c2 590 orelse List.exists (fn Func (c2, []) => c1 <> c2
549 | Finish => true 591 | Finish => true
551 (Cc.allPeers (cc, e)) 593 (Cc.allPeers (cc, e))
552 | _ => false) hyps 594 | _ => false) hyps
553 orelse gls goals (fn () => false) then 595 orelse gls goals (fn () => false) then
554 true 596 true
555 else 597 else
556 (Print.prefaces "Can't prove" 598 ((*Print.prefaces "Can't prove"
557 [("hyps", Print.p_list (fn x => p_prop (Reln x)) hyps), 599 [("hyps", Print.p_list p_atom hyps),
558 ("goals", Print.p_list (fn x => p_prop (Reln x)) goals)]; 600 ("goals", Print.p_list p_atom goals)];*)
559 false) 601 false)
560 end)) 602 end))
561 in 603 in
562 reset (); 604 reset ();
563 doOne false; 605 doOne false;
566 608
567 fun patCon pc = 609 fun patCon pc =
568 case pc of 610 case pc of
569 PConVar n => "C" ^ Int.toString n 611 PConVar n => "C" ^ Int.toString n
570 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 612 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
571
572
573 613
574 datatype chunk = 614 datatype chunk =
575 String of string 615 String of string
576 | Exp of Mono.exp 616 | Exp of Mono.exp
577 617
869 ls 909 ls
870 else 910 else
871 x :: ls 911 x :: ls
872 end 912 end
873 913
914 datatype queryMode =
915 SomeCol of exp
916 | AllCols of exp
917
874 fun queryProp env rv oe e = 918 fun queryProp env rv oe e =
875 case parse query e of 919 case parse query e of
876 NONE => (print ("Warning: Information flow checker can't parse SQL query at " 920 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
877 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 921 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
878 (Unknown, [])) 922 (Unknown, []))
897 foldl (fn ((t, v), p) => 941 foldl (fn ((t, v), p) =>
898 And (p, 942 And (p,
899 Reln (Sql t, 943 Reln (Sql t,
900 [Recd (foldl (fn ((v', f), fs) => 944 [Recd (foldl (fn ((v', f), fs) =>
901 if v' = v then 945 if v' = v then
902 (f, Proj (Proj (Lvar rv, v), f)) :: fs 946 (f, Proj (Proj (rv, v), f)) :: fs
903 else 947 else
904 fs) [] allUsed)]))) 948 fs) [] allUsed)])))
905 True (#From r) 949 True (#From r)
906 950
907 fun expIn e = 951 fun expIn e =
908 case e of 952 case e of
909 SqConst p => inl (Const p) 953 SqConst p => inl (Const p)
910 | Field (v, f) => inl (Proj (Proj (Lvar rv, v), f)) 954 | Field (v, f) => inl (Proj (Proj (rv, v), f))
911 | Binop (bo, e1, e2) => 955 | Binop (bo, e1, e2) =>
912 inr (case (bo, expIn e1, expIn e2) of 956 inr (case (bo, expIn e1, expIn e2) of
913 (Exps f, inl e1, inl e2) => f (e1, e2) 957 (Exps f, inl e1, inl e2) => f (e1, e2)
914 | (Props f, inr p1, inr p2) => f (p1, p2) 958 | (Props f, inr p1, inr p2) => f (p1, p2)
915 | _ => Unknown) 959 | _ => Unknown)
929 end 973 end
930 | SqFunc (f, e) => 974 | SqFunc (f, e) =>
931 inl (case expIn e of 975 inl (case expIn e of
932 inl e => Func (f, [e]) 976 inl e => Func (f, [e])
933 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f)) 977 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
934 | Count => inl (Func ("COUNT", [])) 978 | Count => inl (Proj (rv, "$COUNT"))
935 979
936 val p = case #Where r of 980 val p = case #Where r of
937 NONE => p 981 NONE => p
938 | SOME e => 982 | SOME e =>
939 case expIn e of 983 case expIn e of
940 inr p' => And (p, p') 984 inr p' => And (p, p')
941 | _ => p 985 | _ => p
942 in 986 in
943 (case oe of 987 (And (p, case oe of
944 NONE => p 988 SomeCol oe =>
945 | SOME oe => 989 foldl (fn (si, p) =>
946 And (p, foldl (fn (si, p) =>
947 let 990 let
948 val p' = case si of 991 val p' = case si of
949 SqField (v, f) => Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]) 992 SqField (v, f) => Reln (Eq, [oe, Proj (Proj (rv, v), f)])
950 | SqExp (e, f) => 993 | SqExp (e, f) =>
951 case expIn e of 994 case expIn e of
952 inr _ => Unknown 995 inr _ => Unknown
953 | inl e => Reln (Eq, [oe, e]) 996 | inl e => Reln (Eq, [oe, e])
954 in 997 in
955 Or (p, p') 998 Or (p, p')
956 end) 999 end)
957 False (#Select r)), 1000 False (#Select r)
1001 | AllCols oe =>
1002 foldl (fn (si, p) =>
1003 let
1004 val p' = case si of
1005 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
1006 Proj (Proj (rv, v), f)])
1007 | SqExp (e, f) =>
1008 case expIn e of
1009 inr p => Cond (Proj (oe, f), p)
1010 | inl e => Reln (Eq, [Proj (oe, f), e])
1011 in
1012 And (p, p')
1013 end)
1014 True (#Select r)),
958 1015
959 case #Where r of 1016 case #Where r of
960 NONE => [] 1017 NONE => []
961 | SOME e => map (fn (v, f) => Proj (Proj (Lvar rv, v), f)) (usedFields e)) 1018 | SOME e => map (fn (v, f) => Proj (Proj (rv, v), f)) (usedFields e))
962 end 1019 end
963 1020
964 fun evalPat env e (pt, _) = 1021 fun evalPat env e (pt, _) =
965 case pt of 1022 case pt of
966 PWild => (env, True) 1023 PWild => (env, True)
994 | (False, False) => true 1051 | (False, False) => true
995 | (Unknown, Unknown) => true 1052 | (Unknown, Unknown) => true
996 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2) 1053 | (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) 1054 | (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) 1055 | (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)) => 1056 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
1000 n1 = n1' andalso n2 = n2' andalso n3 = n3'
1001 andalso peq (p1, p2) andalso eeq (e1, e2)
1002 | _ => false 1057 | _ => false
1003 1058
1004 fun removeRedundant p1 = 1059 fun removeRedundant p1 =
1005 let 1060 let
1006 fun rr p2 = 1061 fun rr p2 =
1008 True 1063 True
1009 else 1064 else
1010 case p2 of 1065 case p2 of
1011 And (x, y) => And (rr x, rr y) 1066 And (x, y) => And (rr x, rr y)
1012 | Or (x, y) => Or (rr x, rr y) 1067 | Or (x, y) => Or (rr x, rr y)
1013 | Select (n1, n2, n3, p, e) => Select (n1, n2, n3, rr p, e)
1014 | _ => p2 1068 | _ => p2
1015 in 1069 in
1016 rr 1070 rr
1017 end 1071 end
1018 1072
1162 let 1216 let
1163 val (_, st) = evalExp env (q, st) 1217 val (_, st) = evalExp env (q, st)
1164 val (i, st) = evalExp env (i, st) 1218 val (i, st) = evalExp env (i, st)
1165 1219
1166 val r = #1 st 1220 val r = #1 st
1167 val acc = #1 st + 1 1221 val rv = #1 st + 1
1168 val st' = (#1 st + 2, #2 st, #3 st) 1222 val acc = #1 st + 2
1223 val st' = (#1 st + 3, #2 st, #3 st)
1169 1224
1170 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1225 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
1171 1226
1172 val r' = newLvar () 1227 val (qp, used) = queryProp env (Var rv) (AllCols (Var r)) q
1173 val acc' = newLvar () 1228
1174 val (qp, used) = queryProp env r' NONE q 1229 val p' = And (qp, #2 st')
1175 1230
1176 val doSubExp = subExp (r, r') o subExp (acc, acc') 1231 val (nvs, p, res) = if varInP acc (#2 st') then
1177 val doSubProp = subProp (r, r') o subProp (acc, acc') 1232 (#1 st + 1, #2 st, Var r)
1178 1233 else
1179 val p = doSubProp (#2 st') 1234 let
1180 val p' = And (p, qp) 1235 val out = #1 st'
1181 val p = Select (r, r', acc', p', doSubExp b) 1236
1182 1237 val p = Or (Reln (Eq, [Var out, i]),
1183 val sent = map (fn (loc, e, p) => (loc, 1238 And (Reln (Eq, [Var out, b]),
1184 doSubExp e, 1239 And (Reln (Gt, [Proj (Var rv, "$COUNT"),
1185 And (qp, doSubProp p))) (#3 st') 1240 Const (Prim.Int 0)]),
1241 p')))
1242 in
1243 (out + 1, p, Var out)
1244 end
1245
1246 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (#3 st')
1186 val sent = map (fn e => (loc, e, p')) used @ sent 1247 val sent = map (fn e => (loc, e, p')) used @ sent
1187 in 1248 in
1188 (Var r, (#1 st + 1, And (#2 st, p), sent)) 1249 (res, (nvs, p, sent))
1189 end 1250 end
1190 | EDml _ => default () 1251 | EDml _ => default ()
1191 | ENextval _ => default () 1252 | ENextval _ => default ()
1192 | ESetval _ => default () 1253 | ESetval _ => default ()
1193 1254
1229 val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) 1290 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
1230 in 1291 in
1231 (sent @ vals, pols) 1292 (sent @ vals, pols)
1232 end 1293 end
1233 1294
1234 | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols) 1295 | DPolicy (PolQuery e) => (vals, #1 (queryProp [] (Lvar 0) (SomeCol (Var 0)) e) :: pols)
1235 1296
1236 | _ => (vals, pols) 1297 | _ => (vals, pols)
1237 1298
1238 val () = reset () 1299 val () = reset ()
1239 1300