Mercurial > urweb

comparison src/iflow.sml @ 1214:648e6b087dfb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change query_policy to sendClient; all arguments passed to SQL predicates are variables
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Apr 2010 09:57:37 -0400
parents e791d93d4616
children 360f1ed0a969
comparison
equal deleted inserted replaced
1213:e791d93d4616 1214:648e6b087dfb
410 type t 410 type t
411 val empty : t 411 val empty : t
412 val assert : t * exp * exp -> t 412 val assert : t * exp * exp -> t
413 val query : t * exp * exp -> bool 413 val query : t * exp * exp -> bool
414 val allPeers : t * exp -> exp list 414 val allPeers : t * exp -> exp list
415 val p_t : t Print.printer
415 end = struct 416 end = struct
416 417
417 fun eq (e1, e2) = eeq (simplify e1, simplify e2) 418 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
418 419
419 type t = (exp * exp) list 420 type t = (exp * exp) list
438 else 439 else
439 NONE 440 NONE
440 end) t 441 end) t
441 end 442 end
442 443
444 open Print
445
446 val p_t = p_list (fn (e1, e2) => box [p_exp (simplify e1),
447 space,
448 PD.string "->",
449 space,
450 p_exp (simplify e2)])
451
452 fun query (t, e1, e2) =
453 let
454 fun doUn e =
455 case e of
456 Func (f, [e1]) =>
457 if String.isPrefix "un" f then
458 let
459 val s = String.extract (f, 2, NONE)
460 in
461 case ListUtil.search (fn e =>
462 case e of
463 Func (f', [e']) =>
464 if f' = s then
465 SOME e'
466 else
467 NONE
468 | _ => NONE) (allPeers (t, e1)) of
469 NONE => e
470 | SOME e => doUn e
471 end
472 else
473 e
474 | _ => e
475
476 val e1' = doUn (lookup (t, doUn (simplify e1)))
477 val e2' = doUn (lookup (t, doUn (simplify e2)))
478 in
479 (*prefaces "CC query" [("e1", p_exp (simplify e1)),
480 ("e2", p_exp (simplify e2)),
481 ("e1'", p_exp (simplify e1')),
482 ("e2'", p_exp (simplify e2')),
483 ("t", p_t t)];*)
484 eq (e1', e2')
485 end
486
443 fun assert (t, e1, e2) = 487 fun assert (t, e1, e2) =
444 let 488 let
445 val r1 = lookup (t, e1) 489 val r1 = lookup (t, e1)
446 val r2 = lookup (t, e2) 490 val r2 = lookup (t, e2)
447
448 fun doUn k (t', e1, e2) =
449 case e2 of
450 Func (f, [e]) =>
451 if String.isPrefix "un" f then
452 let
453 val f' = String.extract (f, 2, NONE)
454 in
455 foldl (fn (e', t') =>
456 case e' of
457 Func (f'', [e'']) =>
458 if f'' = f' then
459 (lookup (t', e1), k e'') :: t'
460 else
461 t'
462 | _ => t') t' (allPeers (t, e))
463 end
464 else
465 t'
466 | Proj (e2, f) => doUn (fn e' => k (Proj (e', f))) (t', e1, e2)
467 | _ => t'
468 in 491 in
469 if eq (r1, r2) then 492 if eq (r1, r2) then
470 t 493 t
471 else 494 else
472 doUn (fn x => x) (doUn (fn x => x) ((r1, r2) :: t, e1, e2), e2, e1) 495 let
496 fun doUn (t, e1, e2) =
497 case e1 of
498 Func (f, [e]) => if String.isPrefix "un" f then
499 let
500 val s = String.extract (f, 2, NONE)
501 in
502 foldl (fn (e', t) =>
503 case e' of
504 Func (f', [e']) =>
505 if f' = s then
506 assert (assert (t, e', e1), e', e2)
507 else
508 t
509 | _ => t) t (allPeers (t, e))
510 end
511 else
512 t
513 | _ => t
514
515 fun doProj (t, e1, e2) =
516 foldl (fn ((e1', e2'), t) =>
517 let
518 fun doOne (e, t) =
519 case e of
520 Proj (e', f) =>
521 if query (t, e1, e') then
522 assert (t, e, Proj (e2, f))
523 else
524 t
525 | _ => t
526 in
527 doOne (e1', doOne (e2', t))
528 end) t t
529
530 val t = (r1, r2) :: t
531 val t = doUn (t, r1, r2)
532 val t = doUn (t, r2, r1)
533 val t = doProj (t, r1, r2)
534 val t = doProj (t, r2, r1)
535 in
536 t
537 end
473 end 538 end
474
475 open Print
476
477 fun query (t, e1, e2) =
478 ((*prefaces "CC query" [("e1", p_exp (simplify e1)),
479 ("e2", p_exp (simplify e2)),
480 ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
481 space,
482 PD.string "->",
483 space,
484 p_exp (simplify e2)]) t)];*)
485 eq (lookup (t, e1), lookup (t, e2)))
486 539
487 end 540 end
488 541
489 fun rimp cc ((r1, es1), (r2, es2)) = 542 fun rimp cc ((r1, es1), (r2, es2)) =
490 case (r1, r2) of 543 case (r1, r2) of
491 (Sql r1', Sql r2') => 544 (Sql r1', Sql r2') =>
492 r1' = r2' andalso 545 r1' = r2' andalso
493 (case (es1, es2) of 546 (case (es1, es2) of
494 ([Recd xes1], [Recd xes2]) => 547 ([e1], [e2]) => eq (e1, e2)
495 let
496 val saved = save ()
497 in
498 if List.all (fn (f, e2) =>
499 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
500 NONE => true
501 | SOME e1 => eq (e1, e2)) xes2 then
502 true
503 else
504 (restore saved;
505 false)
506 end
507 | _ => false) 548 | _ => false)
508 | (Eq, Eq) => 549 | (Eq, Eq) =>
509 (case (es1, es2) of 550 (case (es1, es2) of
510 ([x1, y1], [x2, y2]) => 551 ([x1, y1], [x2, y2]) =>
511 let 552 let
531 Var v' => v' = v 572 Var v' => v' = v
532 | Proj (e, _) => matches e 573 | Proj (e, _) => matches e
533 | Func (f, [e]) => String.isPrefix "un" f andalso matches e 574 | Func (f, [e]) => String.isPrefix "un" f andalso matches e
534 | _ => false 575 | _ => false
535 in 576 in
577 (*Print.prefaces "Checking peers" [("e2", p_exp e2),
578 ("peers", Print.p_list p_exp (Cc.allPeers (cc, e2))),
579 ("db", Cc.p_t cc)];*)
536 List.exists matches (Cc.allPeers (cc, e2)) 580 List.exists matches (Cc.allPeers (cc, e2))
537 end 581 end
538 | _ => false) 582 | _ => false)
539 | _ => false 583 | _ => false
540 584
560 (false, (Known, _)) => gls goals onFail 604 (false, (Known, _)) => gls goals onFail
561 | _ => 605 | _ =>
562 let 606 let
563 fun hps hyps = 607 fun hps hyps =
564 case hyps of 608 case hyps of
565 [] => ((*Print.preface ("Fail", p_prop (Reln g));*) 609 [] => ((*Print.prefaces "Fail" [("g", p_prop (Reln g)),
610 ("db", Cc.p_t cc)];*)
566 onFail ()) 611 onFail ())
567 | ACond _ :: hyps => hps hyps 612 | ACond _ :: hyps => hps hyps
568 | AReln h :: hyps => 613 | AReln h :: hyps =>
569 let 614 let
570 val saved = save () 615 val saved = save ()
923 968
924 datatype queryMode = 969 datatype queryMode =
925 SomeCol of exp 970 SomeCol of exp
926 | AllCols of exp 971 | AllCols of exp
927 972
928 fun queryProp env rv oe e = 973 fun queryProp env rvN rv oe e =
929 case parse query e of 974 case parse query e of
930 NONE => (print ("Warning: Information flow checker can't parse SQL query at " 975 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
931 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 976 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
932 (Unknown, [])) 977 (rvN, Var 0, Unknown, []))
933 | SOME r => 978 | SOME r =>
934 let 979 let
980 val (rvN, count) = rv rvN
981
982 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
983 let
984 val (rvN, e) = rv rvN
985 in
986 ((v, e), rvN)
987 end) rvN (#From r)
988
989 fun rvOf v =
990 case List.find (fn (v', _) => v' = v) rvs of
991 NONE => raise Fail "Iflow.queryProp: Bad table variable"
992 | SOME (_, e) => e
993
935 fun usedFields e = 994 fun usedFields e =
936 case e of 995 case e of
937 SqConst _ => [] 996 SqConst _ => []
938 | Field (v, f) => [(v, f)] 997 | Field (v, f) => [(v, f)]
939 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2) 998 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
940 | SqKnown _ => [] 999 | SqKnown _ => []
941 | Inj _ => [] 1000 | Inj _ => []
942 | SqFunc (_, e) => usedFields e 1001 | SqFunc (_, e) => usedFields e
943 | Count => [] 1002 | Count => []
944 1003
945 val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r)
946 @ (case #Where r of
947 NONE => []
948 | SOME e => usedFields e))
949
950 val p = 1004 val p =
951 foldl (fn ((t, v), p) => 1005 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
952 And (p,
953 Reln (Sql t,
954 [Recd (foldl (fn ((v', f), fs) =>
955 if v' = v then
956 (f, Proj (Proj (rv, v), f)) :: fs
957 else
958 fs) [] allUsed)])))
959 True (#From r)
960 1006
961 fun expIn e = 1007 fun expIn e =
962 case e of 1008 case e of
963 SqConst p => inl (Const p) 1009 SqConst p => inl (Const p)
964 | Field (v, f) => inl (Proj (Proj (rv, v), f)) 1010 | Field (v, f) => inl (Proj (rvOf v, f))
965 | Binop (bo, e1, e2) => 1011 | Binop (bo, e1, e2) =>
966 inr (case (bo, expIn e1, expIn e2) of 1012 inr (case (bo, expIn e1, expIn e2) of
967 (Exps f, inl e1, inl e2) => f (e1, e2) 1013 (Exps f, inl e1, inl e2) => f (e1, e2)
968 | (Props f, inr p1, inr p2) => f (p1, p2) 1014 | (Props f, inr p1, inr p2) => f (p1, p2)
969 | _ => Unknown) 1015 | _ => Unknown)
983 end 1029 end
984 | SqFunc (f, e) => 1030 | SqFunc (f, e) =>
985 inl (case expIn e of 1031 inl (case expIn e of
986 inl e => Func (f, [e]) 1032 inl e => Func (f, [e])
987 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f)) 1033 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
988 | Count => inl (Proj (rv, "$COUNT")) 1034 | Count => inl count
989 1035
990 val p = case #Where r of 1036 val p = case #Where r of
991 NONE => p 1037 NONE => p
992 | SOME e => 1038 | SOME e =>
993 case expIn e of 1039 case expIn e of
994 inr p' => And (p, p') 1040 inr p' => And (p, p')
995 | _ => p 1041 | _ => p
996 in 1042 in
997 (And (p, case oe of 1043 (rvN,
1044 count,
1045 And (p, case oe of
998 SomeCol oe => 1046 SomeCol oe =>
999 foldl (fn (si, p) => 1047 foldl (fn (si, p) =>
1000 let 1048 let
1001 val p' = case si of 1049 val p' = case si of
1002 SqField (v, f) => Reln (Eq, [oe, Proj (Proj (rv, v), f)]) 1050 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
1003 | SqExp (e, f) => 1051 | SqExp (e, f) =>
1004 case expIn e of 1052 case expIn e of
1005 inr _ => Unknown 1053 inr _ => Unknown
1006 | inl e => Reln (Eq, [oe, e]) 1054 | inl e => Reln (Eq, [oe, e])
1007 in 1055 in
1011 | AllCols oe => 1059 | AllCols oe =>
1012 foldl (fn (si, p) => 1060 foldl (fn (si, p) =>
1013 let 1061 let
1014 val p' = case si of 1062 val p' = case si of
1015 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f), 1063 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
1016 Proj (Proj (rv, v), f)]) 1064 Proj (rvOf v, f)])
1017 | SqExp (e, f) => 1065 | SqExp (e, f) =>
1018 case expIn e of 1066 case expIn e of
1019 inr p => Cond (Proj (oe, f), p) 1067 inr p => Cond (Proj (oe, f), p)
1020 | inl e => Reln (Eq, [Proj (oe, f), e]) 1068 | inl e => Reln (Eq, [Proj (oe, f), e])
1021 in 1069 in
1023 end) 1071 end)
1024 True (#Select r)), 1072 True (#Select r)),
1025 1073
1026 case #Where r of 1074 case #Where r of
1027 NONE => [] 1075 NONE => []
1028 | SOME e => map (fn (v, f) => Proj (Proj (rv, v), f)) (usedFields e)) 1076 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
1029 end 1077 end
1030 1078
1031 fun evalPat env e (pt, _) = 1079 fun evalPat env e (pt, _) =
1032 case pt of 1080 case pt of
1033 PWild => (env, True) 1081 PWild => (env, True)
1116 | EFfiApp (m, s, es) => 1164 | EFfiApp (m, s, es) =>
1117 if m = "Basis" andalso SS.member (writers, s) then 1165 if m = "Basis" andalso SS.member (writers, s) then
1118 let 1166 let
1119 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1167 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1120 in 1168 in
1121 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es)) 1169 (Recd [], (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
1122 end 1170 end
1123 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then 1171 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
1124 default () 1172 default ()
1125 else 1173 else
1126 let 1174 let
1211 end 1259 end
1212 | EWrite e => 1260 | EWrite e =>
1213 let 1261 let
1214 val (e, st) = evalExp env (e, st) 1262 val (e, st) = evalExp env (e, st)
1215 in 1263 in
1216 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent))) 1264 (Recd [], (#1 st, p, addSent (#2 st, e, sent)))
1217 end 1265 end
1218 | ESeq (e1, e2) => 1266 | ESeq (e1, e2) =>
1219 let 1267 let
1220 val (_, st) = evalExp env (e1, st) 1268 val (_, st) = evalExp env (e1, st)
1221 in 1269 in
1238 let 1286 let
1239 val (_, st) = evalExp env (q, st) 1287 val (_, st) = evalExp env (q, st)
1240 val (i, st) = evalExp env (i, st) 1288 val (i, st) = evalExp env (i, st)
1241 1289
1242 val r = #1 st 1290 val r = #1 st
1243 val rv = #1 st + 1 1291 val acc = #1 st + 1
1244 val acc = #1 st + 2 1292 val st' = (#1 st + 2, #2 st, #3 st)
1245 val st' = (#1 st + 3, #2 st, #3 st)
1246 1293
1247 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1294 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
1248 1295
1249 val (qp, used) = queryProp env (Var rv) (AllCols (Var r)) q 1296 val (rvN, count, qp, used) =
1297 queryProp env
1298 (#1 st') (fn rvN => (rvN + 1, Var rvN))
1299 (AllCols (Var r)) q
1250 1300
1251 val p' = And (qp, #2 st') 1301 val p' = And (qp, #2 st')
1252 1302
1253 val (nvs, p, res) = if varInP acc (#2 st') then 1303 val (nvs, p, res) = if varInP acc (#2 st') then
1254 (#1 st + 1, #2 st, Var r) 1304 (#1 st + 1, #2 st, Var r)
1255 else 1305 else
1256 let 1306 let
1257 val out = #1 st' 1307 val out = rvN
1258 1308
1259 val p = Or (Reln (Eq, [Var out, i]), 1309 val p = Or (Reln (Eq, [Var out, i]),
1260 And (Reln (Eq, [Var out, b]), 1310 And (Reln (Eq, [Var out, b]),
1261 And (Reln (Gt, [Proj (Var rv, "$COUNT"), 1311 And (Reln (Gt, [count,
1262 Const (Prim.Int 0)]), 1312 Const (Prim.Int 0)]),
1263 p'))) 1313 p')))
1264 in 1314 in
1265 (out + 1, p, Var out) 1315 (out + 1, p, Var out)
1266 end 1316 end
1321 val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) 1371 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
1322 in 1372 in
1323 (sent @ vals, pols) 1373 (sent @ vals, pols)
1324 end 1374 end
1325 1375
1326 | DPolicy (PolQuery e) => (vals, #1 (queryProp [] (Lvar 0) (SomeCol (Var 0)) e) :: pols) 1376 | DPolicy (PolClient e) => (vals, #3 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
1327 1377 (SomeCol (Var 0)) e) :: pols)
1378
1328 | _ => (vals, pols) 1379 | _ => (vals, pols)
1329 1380
1330 val () = reset () 1381 val () = reset ()
1331 1382
1332 val (vals, pols) = foldl decl ([], []) file 1383 val (vals, pols) = foldl decl ([], []) file