Mercurial > urweb

comparison src/iflow.sml @ 1243:e754dc92c47c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing boolean SQL constants and fixing a related prover bug
author Adam Chlipala <adamc@hcoop.net>
date Sun, 18 Apr 2010 10:56:39 -0400
parents 4ed556678214
children 1eedc9086e6c
comparison
equal deleted inserted replaced
1242:4ed556678214 1243:e754dc92c47c
298 298
299 fun p_rep n = 299 fun p_rep n =
300 case !(#Rep (unNode n)) of 300 case !(#Rep (unNode n)) of
301 SOME n => p_rep n 301 SOME n => p_rep n
302 | NONE => 302 | NONE =>
303 box [string (Int.toString 0(*Unsafe.cast n*) ^ ":"), 303 box [(*string (Int.toString (Unsafe.cast n) ^ ":"),
304 space, 304 space,*)
305 case #Variety (unNode n) of 305 case #Variety (unNode n) of
306 Nothing => string "?" 306 Nothing => string "?"
307 | Dt0 s => string ("Dt0(" ^ s ^ ")") 307 | Dt0 s => string ("Dt0(" ^ s ^ ")")
308 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), 308 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
309 space, 309 space,
535 end 535 end
536 536
537 fun p_repOf db e = p_rep (representative (db, e)) 537 fun p_repOf db e = p_rep (representative (db, e))
538 538
539 fun assert (db, a) = 539 fun assert (db, a) =
540 case a of 540 let
541 ACond _ => () 541 fun markEq (r1, r2) =
542 | AReln x =>
543 case x of
544 (Known, [e]) =>
545 ((*Print.prefaces "Before" [("e", p_exp e),
546 ("db", p_database db)];*)
547 markKnown (representative (db, e))(*;
548 Print.prefaces "After" [("e", p_exp e),
549 ("db", p_database db)]*))
550 | (PCon0 f, [e]) =>
551 let 542 let
552 val r = representative (db, e) 543 val r1 = repOf r1
544 val r2 = repOf r2
553 in 545 in
554 case #Variety (unNode r) of 546 if r1 = r2 then
555 Dt0 f' => if f = f' then 547 ()
556 () 548 else case (#Variety (unNode r1), #Variety (unNode r2)) of
557 else 549 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
558 raise Contradiction 550 ()
559 | Nothing => 551 else
560 let 552 raise Contradiction
561 val r' = ref (Node {Rep = ref NONE, 553 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
562 Cons = ref SM.empty, 554 ()
563 Variety = Dt0 f, 555 else
564 Known = ref false}) 556 raise Contradiction
565 in 557 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
566 #Rep (unNode r) := SOME r' 558 markEq (r1, r2)
567 end 559 else
568 | _ => raise Contradiction 560 raise Contradiction
561 | (Recrd (xes1, _), Recrd (xes2, _)) =>
562 let
563 fun unif (xes1, xes2) =
564 SM.appi (fn (x, r1) =>
565 case SM.find (!xes2, x) of
566 NONE => xes2 := SM.insert (!xes2, x, r1)
567 | SOME r2 => markEq (r1, r2)) (!xes1)
568 in
569 unif (xes1, xes2);
570 unif (xes2, xes1)
571 end
572 | (Nothing, _) => mergeNodes (r1, r2)
573 | (_, Nothing) => mergeNodes (r2, r1)
574 | _ => raise Contradiction
569 end 575 end
570 | (PCon1 f, [e]) => 576
577 and mergeNodes (r1, r2) =
578 (#Rep (unNode r1) := SOME r2;
579 if !(#Known (unNode r1)) then
580 markKnown r2
581 else
582 ();
583 if !(#Known (unNode r2)) then
584 markKnown r1
585 else
586 ();
587 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
588
589 compactFuncs ())
590
591 and compactFuncs () =
571 let 592 let
572 val r = representative (db, e) 593 fun loop funcs =
594 case funcs of
595 [] => []
596 | (fr as ((f, rs), r)) :: rest =>
597 let
598 val rest = List.filter (fn ((f' : string, rs'), r') =>
599 if f' = f
600 andalso ListPair.allEq (fn (r1, r2) =>
601 repOf r1 = repOf r2)
602 (rs, rs') then
603 (markEq (r, r');
604 false)
605 else
606 true) rest
607 in
608 fr :: loop rest
609 end
573 in 610 in
574 case #Variety (unNode r) of 611 #Funcs db := loop (!(#Funcs db))
575 Dt1 (f', e') => if f = f' then
576 ()
577 else
578 raise Contradiction
579 | Nothing =>
580 let
581 val r'' = ref (Node {Rep = ref NONE,
582 Cons = ref SM.empty,
583 Variety = Nothing,
584 Known = ref (!(#Known (unNode r)))})
585
586 val r' = ref (Node {Rep = ref NONE,
587 Cons = ref SM.empty,
588 Variety = Dt1 (f, r''),
589 Known = #Known (unNode r)})
590 in
591 #Rep (unNode r) := SOME r'
592 end
593 | _ => raise Contradiction
594 end 612 end
595 | (Eq, [e1, e2]) => 613 in
596 let 614 case a of
597 fun markEq (r1, r2) = 615 ACond _ => ()
598 let 616 | AReln x =>
599 val r1 = repOf r1 617 case x of
600 val r2 = repOf r2 618 (Known, [e]) =>
601 in 619 ((*Print.prefaces "Before" [("e", p_exp e),
602 if r1 = r2 then 620 ("db", p_database db)];*)
603 () 621 markKnown (representative (db, e))(*;
604 else case (#Variety (unNode r1), #Variety (unNode r2)) of 622 Print.prefaces "After" [("e", p_exp e),
605 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then 623 ("db", p_database db)]*))
606 () 624 | (PCon0 f, [e]) =>
607 else 625 let
608 raise Contradiction 626 val r = representative (db, e)
609 | (Dt0 f1, Dt0 f2) => if f1 = f2 then 627 in
610 () 628 case #Variety (unNode r) of
611 else 629 Dt0 f' => if f = f' then
612 raise Contradiction 630 ()
613 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then 631 else
614 markEq (r1, r2) 632 raise Contradiction
615 else 633 | Nothing =>
616 raise Contradiction 634 (case SM.find (!(#Con0s db), f) of
617 | (Recrd (xes1, _), Recrd (xes2, _)) => 635 SOME r' => markEq (r, r')
618 let 636 | NONE =>
619 fun unif (xes1, xes2) = 637 let
620 SM.appi (fn (x, r1) => 638 val r' = ref (Node {Rep = ref NONE,
621 case SM.find (!xes2, x) of 639 Cons = ref SM.empty,
622 NONE => xes2 := SM.insert (!xes2, x, r1) 640 Variety = Dt0 f,
623 | SOME r2 => markEq (r1, r2)) (!xes1) 641 Known = ref false})
624 in 642 in
625 unif (xes1, xes2); 643 #Rep (unNode r) := SOME r';
626 unif (xes2, xes1) 644 #Con0s db := SM.insert (!(#Con0s db), f, r')
627 end 645 end)
628 | (Nothing, _) => mergeNodes (r1, r2) 646 | _ => raise Contradiction
629 | (_, Nothing) => mergeNodes (r2, r1) 647 end
630 | _ => raise Contradiction 648 | (PCon1 f, [e]) =>
631 end 649 let
632 650 val r = representative (db, e)
633 and mergeNodes (r1, r2) = 651 in
634 (#Rep (unNode r1) := SOME r2; 652 case #Variety (unNode r) of
635 if !(#Known (unNode r1)) then 653 Dt1 (f', e') => if f = f' then
636 markKnown r2 654 ()
637 else 655 else
638 (); 656 raise Contradiction
639 if !(#Known (unNode r2)) then 657 | Nothing =>
640 markKnown r1 658 let
641 else 659 val r'' = ref (Node {Rep = ref NONE,
642 (); 660 Cons = ref SM.empty,
643 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1))); 661 Variety = Nothing,
644 662 Known = ref (!(#Known (unNode r)))})
645 compactFuncs ()) 663
646 664 val r' = ref (Node {Rep = ref NONE,
647 and compactFuncs () = 665 Cons = ref SM.empty,
648 let 666 Variety = Dt1 (f, r''),
649 fun loop funcs = 667 Known = #Known (unNode r)})
650 case funcs of 668 in
651 [] => [] 669 #Rep (unNode r) := SOME r'
652 | (fr as ((f, rs), r)) :: rest => 670 end
653 let 671 | _ => raise Contradiction
654 val rest = List.filter (fn ((f' : string, rs'), r') => 672 end
655 if f' = f 673 | (Eq, [e1, e2]) =>
656 andalso ListPair.allEq (fn (r1, r2) =>
657 repOf r1 = repOf r2)
658 (rs, rs') then
659 (markEq (r, r');
660 false)
661 else
662 true) rest
663 in
664 fr :: loop rest
665 end
666 in
667 #Funcs db := loop (!(#Funcs db))
668 end
669 in
670 markEq (representative (db, e1), representative (db, e2)) 674 markEq (representative (db, e1), representative (db, e2))
671 end 675 | _ => ()
672 | _ => () 676 end
673 677
674 fun check (db, a) = 678 fun check (db, a) =
675 case a of 679 case a of
676 ACond _ => false 680 ACond _ => false
677 | AReln x => 681 | AReln x =>
949 Exps of exp * exp -> prop 953 Exps of exp * exp -> prop
950 | Props of prop * prop -> prop 954 | Props of prop * prop -> prop
951 955
952 datatype sqexp = 956 datatype sqexp =
953 SqConst of Prim.t 957 SqConst of Prim.t
958 | SqTrue
959 | SqFalse
954 | Field of string * string 960 | Field of string * string
955 | Computed of string 961 | Computed of string
956 | Binop of Rel * sqexp * sqexp 962 | Binop of Rel * sqexp * sqexp
957 | SqKnown of sqexp 963 | SqKnown of sqexp
958 | Inj of Mono.exp 964 | Inj of Mono.exp
1019 Exp (EFfiApp ("Basis", f, [e]), _) :: chs => 1025 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
1020 if String.isPrefix "sqlify" f then 1026 if String.isPrefix "sqlify" f then
1021 SOME (e, chs) 1027 SOME (e, chs)
1022 else 1028 else
1023 NONE 1029 NONE
1030 | Exp (ECase (e, [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
1031 (EPrim (Prim.String "TRUE"), _)),
1032 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
1033 (EPrim (Prim.String "FALSE"), _))], _), _) :: chs =>
1034 SOME (e, chs)
1035
1024 | _ => NONE 1036 | _ => NONE
1025 1037
1026 fun constK s = wrap (const s) (fn () => s) 1038 fun constK s = wrap (const s) (fn () => s)
1027 1039
1028 val funcName = altL [constK "COUNT", 1040 val funcName = altL [constK "COUNT",
1032 constK "AVG"] 1044 constK "AVG"]
1033 1045
1034 fun sqexp chs = 1046 fun sqexp chs =
1035 log "sqexp" 1047 log "sqexp"
1036 (altL [wrap prim SqConst, 1048 (altL [wrap prim SqConst,
1049 wrap (const "TRUE") (fn () => SqTrue),
1050 wrap (const "FALSE") (fn () => SqFalse),
1037 wrap field Field, 1051 wrap field Field,
1038 wrap uw_ident Computed, 1052 wrap uw_ident Computed,
1039 wrap known SqKnown, 1053 wrap known SqKnown,
1040 wrap func SqFunc, 1054 wrap func SqFunc,
1041 wrap (const "COUNT(*)") (fn () => Count), 1055 wrap (const "COUNT(*)") (fn () => Count),
1102 Query1 of query1 1116 Query1 of query1
1103 | Union of query * query 1117 | Union of query * query
1104 1118
1105 val orderby = log "orderby" 1119 val orderby = log "orderby"
1106 (wrap (follow (ws (const "ORDER BY ")) 1120 (wrap (follow (ws (const "ORDER BY "))
1107 (list sqexp)) 1121 (follow (list sqexp)
1108 ignore) 1122 (opt (ws (const "DESC")))))
1123 ignore)
1109 1124
1110 fun query chs = log "query" 1125 fun query chs = log "query"
1111 (wrap 1126 (wrap
1112 (follow 1127 (follow
1113 (alt (wrap (follow (const "((") 1128 (alt (wrap (follow (const "((")
1264 orelse tryAll unifs hyps 1279 orelse tryAll unifs hyps
1265 | _ :: hyps => tryAll unifs hyps 1280 | _ :: hyps => tryAll unifs hyps
1266 in 1281 in
1267 tryAll unifs hyps 1282 tryAll unifs hyps
1268 end 1283 end
1269 | AReln (r, es) :: goals => 1284 | (g as AReln (r, es)) :: goals =>
1270 Cc.check (db, AReln (r, map (simplify unifs) es)) 1285 Cc.check (db, AReln (r, map (simplify unifs) es))
1271 andalso checkGoals goals unifs 1286 andalso checkGoals goals unifs
1272 | ACond _ :: _ => false 1287 | ACond _ :: _ => false
1273 in 1288 in
1274 checkGoals goals IM.empty 1289 checkGoals goals IM.empty
1350 let 1365 let
1351 val (_, hs) = !hyps 1366 val (_, hs) = !hyps
1352 in 1367 in
1353 ErrorMsg.errorAt loc "The information flow policy may be violated here."; 1368 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1354 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs), 1369 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
1355 ("User learns", p_exp e)] 1370 ("User learns", p_exp e),
1371 ("E-graph", Cc.p_database db)]
1356 end 1372 end
1357 end 1373 end
1358 1374
1359 fun checkPaths () = 1375 fun checkPaths () =
1360 let 1376 let
1369 buildable true e)) (!path); 1385 buildable true e)) (!path);
1370 setHyps hs 1386 setHyps hs
1371 end 1387 end
1372 1388
1373 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)), 1389 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
1374 ("exps", Print.p_list p_exp (#2 v))];*) 1390 ("exps", Print.p_list p_exp (#2 v))];*)
1375 sendable := v :: !sendable) 1391 sendable := v :: !sendable)
1376 1392
1377 fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*) 1393 fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*)
1378 checkPaths (); 1394 checkPaths ();
1379 if isKnown e then 1395 if isKnown e then
1472 let 1488 let
1473 fun default () = inl (rv ()) 1489 fun default () = inl (rv ())
1474 in 1490 in
1475 case e of 1491 case e of
1476 SqConst p => inl (Const p) 1492 SqConst p => inl (Const p)
1493 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
1494 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
1477 | Field (v, f) => inl (Proj (rvOf v, f)) 1495 | Field (v, f) => inl (Proj (rvOf v, f))
1478 | Computed _ => default () 1496 | Computed _ => default ()
1479 | Binop (bo, e1, e2) => 1497 | Binop (bo, e1, e2) =>
1480 let 1498 let
1481 val e1 = expIn e1 1499 val e1 = expIn e1
1482 val e2 = expIn e2 1500 val e2 = expIn e2
1483 in 1501 in
1484 inr (case (bo, e1, e2) of 1502 inr (case (bo, e1, e2) of
1485 (Exps f, inl e1, inl e2) => f (e1, e2) 1503 (Exps f, inl e1, inl e2) => f (e1, e2)
1486 | (Props f, inr p1, inr p2) => f (p1, p2) 1504 | (Props f, v1, v2) =>
1505 let
1506 fun pin v =
1507 case v of
1508 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1509 | inr p => p
1510 in
1511 f (pin v1, pin v2)
1512 end
1487 | _ => Unknown) 1513 | _ => Unknown)
1488 end 1514 end
1489 | SqKnown e => 1515 | SqKnown e =>
1490 (case expIn e of 1516 (case expIn e of
1491 inl e => inr (Reln (Known, [e])) 1517 inl e => inr (Reln (Known, [e]))
1578 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) 1604 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1579 1605
1580 fun usedFields e = 1606 fun usedFields e =
1581 case e of 1607 case e of
1582 SqConst _ => [] 1608 SqConst _ => []
1609 | SqTrue => []
1610 | SqFalse => []
1583 | Field (v, f) => [(false, Proj (rvOf v, f))] 1611 | Field (v, f) => [(false, Proj (rvOf v, f))]
1584 | Computed _ => [] 1612 | Computed _ => []
1585 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 1613 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
1586 | SqKnown _ => [] 1614 | SqKnown _ => []
1587 | Inj e => 1615 | Inj e =>
1641 fun doWhere final = 1669 fun doWhere final =
1642 (addFrom (); 1670 (addFrom ();
1643 case #Where r of 1671 case #Where r of
1644 NONE => (doUsed (); final ()) 1672 NONE => (doUsed (); final ())
1645 | SOME e => 1673 | SOME e =>
1646 case expIn e of 1674 let
1647 inl _ => (doUsed (); final ()) 1675 val p = case expIn e of
1648 | inr p => 1676 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1649 let 1677 | inr p => p
1650 val saved = #Save arg () 1678
1651 in 1679 val saved = #Save arg ()
1652 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} 1680 in
1653 p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ()); 1681 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
1654 #Restore arg saved 1682 p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
1655 end) 1683 #Restore arg saved
1684 end)
1656 handle Cc.Contradiction => () 1685 handle Cc.Contradiction => ()
1657 1686
1658 fun normal () = doWhere normal' 1687 fun normal () = doWhere normal'
1659 in 1688 in
1660 (case #Select r of 1689 (case #Select r of