Mercurial > urweb
comparison src/iflow.sml @ 1221:00e628854005
Delete policies
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 11 Apr 2010 12:38:21 -0400 |
parents | 526575a9537a |
children | 117f13bdc1fd |
comparison
equal
deleted
inserted
replaced
1220:526575a9537a | 1221:00e628854005 |
---|---|
409 | 409 |
410 and variety = | 410 and variety = |
411 Dt0 of string | 411 Dt0 of string |
412 | Dt1 of string * node ref | 412 | Dt1 of string * node ref |
413 | Prim of Prim.t | 413 | Prim of Prim.t |
414 | Recrd of node ref SM.map ref | 414 | Recrd of node ref SM.map ref * bool |
415 | VFinish | 415 | VFinish |
416 | Nothing | 416 | Nothing |
417 | 417 |
418 type representative = node ref | 418 type representative = node ref |
419 | 419 |
444 | 444 |
445 fun p_rep n = | 445 fun p_rep n = |
446 case !(#Rep (unNode n)) of | 446 case !(#Rep (unNode n)) of |
447 SOME n => p_rep n | 447 SOME n => p_rep n |
448 | NONE => | 448 | NONE => |
449 case #Variety (unNode n) of | 449 box [string (Int.toString (Unsafe.cast n) ^ ":"), |
450 Nothing => string ("?" ^ Int.toString (Unsafe.cast n)) | 450 space, |
451 | Dt0 s => string ("Dt0(" ^ s ^ ")") | 451 case #Variety (unNode n) of |
452 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), | 452 Nothing => string "?" |
453 space, | 453 | Dt0 s => string ("Dt0(" ^ s ^ ")") |
454 p_rep n, | 454 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), |
455 string ")"] | 455 space, |
456 | Prim p => Prim.p_t p | 456 p_rep n, |
457 | Recrd (ref m) => box [string "{", | 457 string ")"] |
458 p_list (fn (x, n) => box [string x, | 458 | Prim p => Prim.p_t p |
459 space, | 459 | Recrd (ref m, b) => box [string "{", |
460 string "=", | 460 p_list (fn (x, n) => box [string x, |
461 space, | 461 space, |
462 p_rep n]) (SM.listItemsi m), | 462 string "=", |
463 string "}"] | 463 space, |
464 | VFinish => string "FINISH" | 464 p_rep n]) (SM.listItemsi m), |
465 string "}", | |
466 if b then | |
467 box [space, | |
468 string "(complete)"] | |
469 else | |
470 box []] | |
471 | VFinish => string "FINISH"] | |
465 | 472 |
466 fun p_database (db : database) = | 473 fun p_database (db : database) = |
467 box [string "Vars:", | 474 box [string "Vars:", |
468 newline, | 475 newline, |
469 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i), | 476 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i), |
487 #Rep (unNode n) := SOME r; | 494 #Rep (unNode n) := SOME r; |
488 r | 495 r |
489 end | 496 end |
490 | 497 |
491 fun markKnown r = | 498 fun markKnown r = |
492 if !(#Known (unNode r)) then | 499 let |
493 () | 500 val r = repOf r |
494 else | 501 in |
495 (#Known (unNode r) := true; | 502 (*Print.preface ("markKnown", p_rep r);*) |
496 SM.app markKnown (!(#Cons (unNode r))); | 503 if !(#Known (unNode r)) then |
497 case #Variety (unNode r) of | 504 ()(*TextIO.print "Already known\n"*) |
498 Dt1 (_, r) => markKnown r | 505 else |
499 | Recrd xes => SM.app markKnown (!xes) | 506 (#Known (unNode r) := true; |
500 | _ => ()) | 507 SM.app markKnown (!(#Cons (unNode r))); |
508 case #Variety (unNode r) of | |
509 Dt1 (_, r) => markKnown r | |
510 | Recrd (xes, _) => SM.app markKnown (!xes) | |
511 | _ => ()) | |
512 end | |
501 | 513 |
502 fun representative (db : database, e) = | 514 fun representative (db : database, e) = |
503 let | 515 let |
504 fun rep e = | 516 fun rep e = |
505 case e of | 517 case e of |
553 | NONE => | 565 | NONE => |
554 let | 566 let |
555 val r' = ref (Node {Rep = ref NONE, | 567 val r' = ref (Node {Rep = ref NONE, |
556 Cons = ref SM.empty, | 568 Cons = ref SM.empty, |
557 Variety = Dt1 (f, r), | 569 Variety = Dt1 (f, r), |
558 Known = #Known (unNode r)}) | 570 Known = ref (!(#Known (unNode r)))}) |
559 in | 571 in |
560 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r'); | 572 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r'); |
561 r' | 573 r' |
562 end | 574 end |
563 end | 575 end |
575 let | 587 let |
576 val cons = ref SM.empty | 588 val cons = ref SM.empty |
577 val r' = ref (Node {Rep = ref NONE, | 589 val r' = ref (Node {Rep = ref NONE, |
578 Cons = cons, | 590 Cons = cons, |
579 Variety = Nothing, | 591 Variety = Nothing, |
580 Known = #Known (unNode r)}) | 592 Known = ref (!(#Known (unNode r)))}) |
581 | 593 |
582 val r'' = ref (Node {Rep = ref NONE, | 594 val r'' = ref (Node {Rep = ref NONE, |
583 Cons = #Cons (unNode r), | 595 Cons = #Cons (unNode r), |
584 Variety = Dt1 (f, r'), | 596 Variety = Dt1 (f, r'), |
585 Known = #Known (unNode r)}) | 597 Known = #Known (unNode r)}) |
626 let | 638 let |
627 val xes = foldl SM.insert' SM.empty xes | 639 val xes = foldl SM.insert' SM.empty xes |
628 | 640 |
629 val r' = ref (Node {Rep = ref NONE, | 641 val r' = ref (Node {Rep = ref NONE, |
630 Cons = ref SM.empty, | 642 Cons = ref SM.empty, |
631 Variety = Recrd (ref xes), | 643 Variety = Recrd (ref xes, true), |
632 Known = ref false}) | 644 Known = ref false}) |
633 in | 645 in |
634 #Records db := (xes, r') :: (!(#Records db)); | 646 #Records db := (xes, r') :: (!(#Records db)); |
635 r' | 647 r' |
636 end | 648 end |
638 | Proj (e, f) => | 650 | Proj (e, f) => |
639 let | 651 let |
640 val r = rep e | 652 val r = rep e |
641 in | 653 in |
642 case #Variety (unNode r) of | 654 case #Variety (unNode r) of |
643 Recrd xes => | 655 Recrd (xes, _) => |
644 (case SM.find (!xes, f) of | 656 (case SM.find (!xes, f) of |
645 SOME r => repOf r | 657 SOME r => repOf r |
646 | NONE => let | 658 | NONE => let |
647 val r = ref (Node {Rep = ref NONE, | 659 val r = ref (Node {Rep = ref NONE, |
648 Cons = ref SM.empty, | 660 Cons = ref SM.empty, |
649 Variety = Nothing, | 661 Variety = Nothing, |
650 Known = #Known (unNode r)}) | 662 Known = ref (!(#Known (unNode r)))}) |
651 in | 663 in |
652 xes := SM.insert (!xes, f, r); | 664 xes := SM.insert (!xes, f, r); |
653 r | 665 r |
654 end) | 666 end) |
655 | Nothing => | 667 | Nothing => |
656 let | 668 let |
657 val r' = ref (Node {Rep = ref NONE, | 669 val r' = ref (Node {Rep = ref NONE, |
658 Cons = ref SM.empty, | 670 Cons = ref SM.empty, |
659 Variety = Nothing, | 671 Variety = Nothing, |
660 Known = #Known (unNode r)}) | 672 Known = ref (!(#Known (unNode r)))}) |
661 | 673 |
662 val r'' = ref (Node {Rep = ref NONE, | 674 val r'' = ref (Node {Rep = ref NONE, |
663 Cons = #Cons (unNode r), | 675 Cons = #Cons (unNode r), |
664 Variety = Recrd (ref (SM.insert (SM.empty, f, r'))), | 676 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false), |
665 Known = #Known (unNode r)}) | 677 Known = #Known (unNode r)}) |
666 in | 678 in |
667 #Rep (unNode r) := SOME r''; | 679 #Rep (unNode r) := SOME r''; |
668 r' | 680 r' |
669 end | 681 end |
678 fun assert (db, a) = | 690 fun assert (db, a) = |
679 case a of | 691 case a of |
680 ACond _ => () | 692 ACond _ => () |
681 | AReln x => | 693 | AReln x => |
682 case x of | 694 case x of |
683 (Known, [e]) => markKnown (representative (db, e)) | 695 (Known, [e]) => |
696 ((*Print.prefaces "Before" [("e", p_exp e), | |
697 ("db", p_database db)];*) | |
698 markKnown (representative (db, e))(*; | |
699 Print.prefaces "After" [("e", p_exp e), | |
700 ("db", p_database db)]*)) | |
684 | (PCon0 f, [e]) => | 701 | (PCon0 f, [e]) => |
685 let | 702 let |
686 val r = representative (db, e) | 703 val r = representative (db, e) |
687 in | 704 in |
688 case #Variety (unNode r) of | 705 case #Variety (unNode r) of |
742 raise Contradiction | 759 raise Contradiction |
743 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then | 760 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then |
744 markEq (r1, r2) | 761 markEq (r1, r2) |
745 else | 762 else |
746 raise Contradiction | 763 raise Contradiction |
747 | (Recrd xes1, Recrd xes2) => | 764 | (Recrd (xes1, _), Recrd (xes2, _)) => |
748 let | 765 let |
749 fun unif (xes1, xes2) = | 766 fun unif (xes1, xes2) = |
750 SM.appi (fn (x, r1) => | 767 SM.appi (fn (x, r1) => |
751 case SM.find (xes2, x) of | 768 case SM.find (xes2, x) of |
752 NONE => () | 769 NONE => () |
803 fun check (db, a) = | 820 fun check (db, a) = |
804 case a of | 821 case a of |
805 ACond _ => false | 822 ACond _ => false |
806 | AReln x => | 823 | AReln x => |
807 case x of | 824 case x of |
808 (Known, [e]) => !(#Known (unNode (representative (db, e)))) | 825 (Known, [e]) => |
826 let | |
827 fun isKnown r = | |
828 let | |
829 val r = repOf r | |
830 in | |
831 !(#Known (unNode r)) | |
832 orelse case #Variety (unNode r) of | |
833 Dt1 (_, r) => isKnown r | |
834 | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes)) | |
835 | _ => false | |
836 end | |
837 | |
838 val r = representative (db, e) | |
839 in | |
840 isKnown r | |
841 end | |
809 | (PCon0 f, [e]) => | 842 | (PCon0 f, [e]) => |
810 (case #Variety (unNode (representative (db, e))) of | 843 (case #Variety (unNode (representative (db, e))) of |
811 Dt0 f' => f' = f | 844 Dt0 f' => f' = f |
812 | _ => false) | 845 | _ => false) |
813 | (PCon1 f, [e]) => | 846 | (PCon1 f, [e]) => |
834 List.exists (fn b => repOf b = d) bs | 867 List.exists (fn b => repOf b = d) bs |
835 orelse case #Variety (unNode d) of | 868 orelse case #Variety (unNode d) of |
836 Dt0 _ => true | 869 Dt0 _ => true |
837 | Dt1 (_, d) => loop d | 870 | Dt1 (_, d) => loop d |
838 | Prim _ => true | 871 | Prim _ => true |
839 | Recrd xes => List.all loop (SM.listItems (!xes)) | 872 | Recrd (xes, _) => List.all loop (SM.listItems (!xes)) |
840 | VFinish => true | 873 | VFinish => true |
841 | Nothing => false | 874 | Nothing => false |
842 end | 875 end |
843 in | 876 in |
844 loop (representative (db, d)) | 877 loop (representative (db, d)) |
872 [] => | 905 [] => |
873 (let | 906 (let |
874 val cc = Cc.database () | 907 val cc = Cc.database () |
875 val () = app (fn a => Cc.assert (cc, a)) hyps | 908 val () = app (fn a => Cc.assert (cc, a)) hyps |
876 in | 909 in |
910 (*Print.preface ("db", Cc.p_database cc);*) | |
877 (List.all (fn a => | 911 (List.all (fn a => |
878 if Cc.check (cc, a) then | 912 if Cc.check (cc, a) then |
879 true | 913 true |
880 else | 914 else |
881 ((*Print.prefaces "Can't prove" | 915 ((*Print.prefaces "Can't prove" |
1220 (wrap (follow (follow select from) (opt wher)) | 1254 (wrap (follow (follow select from) (opt wher)) |
1221 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) | 1255 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) |
1222 | 1256 |
1223 datatype dml = | 1257 datatype dml = |
1224 Insert of string * (string * sqexp) list | 1258 Insert of string * (string * sqexp) list |
1259 | Delete of string * sqexp | |
1225 | 1260 |
1226 val insert = log "insert" | 1261 val insert = log "insert" |
1227 (wrapP (follow (const "INSERT INTO ") | 1262 (wrapP (follow (const "INSERT INTO ") |
1228 (follow uw_ident | 1263 (follow uw_ident |
1229 (follow (const " (") | 1264 (follow (const " (") |
1230 (follow (list uw_ident) | 1265 (follow (list uw_ident) |
1231 (follow (const ") VALUES (") | 1266 (follow (const ") VALUES (") |
1232 (follow (list sqexp) | 1267 (follow (list sqexp) |
1233 (const ")"))))))) | 1268 (const ")"))))))) |
1234 (fn ((), (tab, ((), (fs, ((), (es, ())))))) => | 1269 (fn ((), (tab, ((), (fs, ((), (es, ())))))) => |
1235 (SOME (Insert (tab, ListPair.zipEq (fs, es)))) | 1270 (SOME (tab, ListPair.zipEq (fs, es))) |
1236 handle ListPair.UnequalLengths => NONE)) | 1271 handle ListPair.UnequalLengths => NONE)) |
1237 | 1272 |
1273 val delete = log "delete" | |
1274 (wrap (follow (const "DELETE FROM ") | |
1275 (follow uw_ident | |
1276 (follow (const " AS T_T WHERE ") | |
1277 sqexp))) | |
1278 (fn ((), (tab, ((), es))) => (tab, es))) | |
1279 | |
1238 val dml = log "dml" | 1280 val dml = log "dml" |
1239 insert | 1281 (altL [wrap insert Insert, |
1282 wrap delete Delete]) | |
1240 | 1283 |
1241 fun removeDups (ls : (string * string) list) = | 1284 fun removeDups (ls : (string * string) list) = |
1242 case ls of | 1285 case ls of |
1243 [] => [] | 1286 [] => [] |
1244 | x :: ls => | 1287 | x :: ls => |
1419 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), | 1462 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), |
1420 [oe]) | 1463 [oe]) |
1421 end | 1464 end |
1422 | AllCols oe => | 1465 | AllCols oe => |
1423 let | 1466 let |
1424 val oe = Proj (oe, f) | 1467 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]]) |
1425 in | 1468 in |
1426 (rvN, | 1469 (rvN, |
1427 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]), | 1470 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])), |
1428 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), | 1471 And (oeEq (Func (DtCon0 "Basis.bool.True", [])), |
1429 p)), | 1472 p)), |
1430 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), | 1473 oeEq (Func (DtCon0 "Basis.bool.True", [])), |
1431 []) | 1474 []) |
1432 end) | 1475 end) |
1433 | _ => normal ()) | 1476 | _ => normal ()) |
1434 | _ => normal () | 1477 | _ => normal () |
1435 in | 1478 in |
1478 NONE => p | 1521 NONE => p |
1479 | SOME e => | 1522 | SOME e => |
1480 case expIn (e, rvN) of | 1523 case expIn (e, rvN) of |
1481 (inr p', _) => And (p, p') | 1524 (inr p', _) => And (p, p') |
1482 | _ => p | 1525 | _ => p |
1526 end | |
1527 end | |
1528 | |
1529 fun deleteProp rvN rv e = | |
1530 let | |
1531 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " | |
1532 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); | |
1533 Unknown) | |
1534 in | |
1535 case parse query e of | |
1536 NONE => default () | |
1537 | SOME r => | |
1538 let | |
1539 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => | |
1540 let | |
1541 val (rvN, e) = rv rvN | |
1542 in | |
1543 ((v, e), rvN) | |
1544 end) rvN (#From r) | |
1545 | |
1546 fun rvOf v = | |
1547 case List.find (fn (v', _) => v' = v) rvs of | |
1548 NONE => raise Fail "Iflow.deleteProp: Bad table variable" | |
1549 | SOME (_, e) => e | |
1550 | |
1551 val p = | |
1552 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r) | |
1553 | |
1554 val expIn = expIn rv [] rvOf | |
1555 in | |
1556 And (Reln (Sql "$Old", [rvOf "Old"]), | |
1557 case #Where r of | |
1558 NONE => p | |
1559 | SOME e => | |
1560 case expIn (e, rvN) of | |
1561 (inr p', _) => And (p, p') | |
1562 | _ => p) | |
1483 end | 1563 end |
1484 end | 1564 end |
1485 | 1565 |
1486 fun evalPat env e (pt, _) = | 1566 fun evalPat env e (pt, _) = |
1487 case pt of | 1567 case pt of |
1536 end | 1616 end |
1537 | 1617 |
1538 datatype cflow = Case | Where | 1618 datatype cflow = Case | Where |
1539 datatype flow = Data | Control of cflow | 1619 datatype flow = Data | Control of cflow |
1540 type check = ErrorMsg.span * exp * prop | 1620 type check = ErrorMsg.span * exp * prop |
1541 type insert = ErrorMsg.span * prop | 1621 type dml = ErrorMsg.span * prop |
1542 | 1622 |
1543 structure St :> sig | 1623 structure St :> sig |
1544 type t | 1624 type t |
1545 val create : {Var : int, | 1625 val create : {Var : int, |
1546 Ambient : prop} -> t | 1626 Ambient : prop} -> t |
1559 | 1639 |
1560 val sent : t -> (check * flow) list | 1640 val sent : t -> (check * flow) list |
1561 val addSent : t * (check * flow) -> t | 1641 val addSent : t * (check * flow) -> t |
1562 val setSent : t * (check * flow) list -> t | 1642 val setSent : t * (check * flow) list -> t |
1563 | 1643 |
1564 val inserted : t -> insert list | 1644 val inserted : t -> dml list |
1565 val addInsert : t * insert -> t | 1645 val addInsert : t * dml -> t |
1646 | |
1647 val deleted : t -> dml list | |
1648 val addDelete : t * dml -> t | |
1566 end = struct | 1649 end = struct |
1567 | 1650 |
1568 type t = {Var : int, | 1651 type t = {Var : int, |
1569 Ambient : prop, | 1652 Ambient : prop, |
1570 Path : (check * cflow) list, | 1653 Path : (check * cflow) list, |
1571 Sent : (check * flow) list, | 1654 Sent : (check * flow) list, |
1572 Insert : insert list} | 1655 Insert : dml list, |
1656 Delete : dml list} | |
1573 | 1657 |
1574 fun create {Var = v, Ambient = p} = {Var = v, | 1658 fun create {Var = v, Ambient = p} = {Var = v, |
1575 Ambient = p, | 1659 Ambient = p, |
1576 Path = [], | 1660 Path = [], |
1577 Sent = [], | 1661 Sent = [], |
1578 Insert = []} | 1662 Insert = [], |
1663 Delete = []} | |
1579 | 1664 |
1580 fun curVar (t : t) = #Var t | 1665 fun curVar (t : t) = #Var t |
1581 fun nextVar (t : t) = ({Var = #Var t + 1, | 1666 fun nextVar (t : t) = ({Var = #Var t + 1, |
1582 Ambient = #Ambient t, | 1667 Ambient = #Ambient t, |
1583 Path = #Path t, | 1668 Path = #Path t, |
1584 Sent = #Sent t, | 1669 Sent = #Sent t, |
1585 Insert = #Insert t}, #Var t) | 1670 Insert = #Insert t, |
1671 Delete = #Delete t}, #Var t) | |
1586 | 1672 |
1587 fun ambient (t : t) = #Ambient t | 1673 fun ambient (t : t) = #Ambient t |
1588 fun setAmbient (t : t, p) = {Var = #Var t, | 1674 fun setAmbient (t : t, p) = {Var = #Var t, |
1589 Ambient = p, | 1675 Ambient = p, |
1590 Path = #Path t, | 1676 Path = #Path t, |
1591 Sent = #Sent t, | 1677 Sent = #Sent t, |
1592 Insert = #Insert t} | 1678 Insert = #Insert t, |
1679 Delete = #Delete t} | |
1593 | 1680 |
1594 fun paths (t : t) = #Path t | 1681 fun paths (t : t) = #Path t |
1595 fun addPath (t : t, c) = {Var = #Var t, | 1682 fun addPath (t : t, c) = {Var = #Var t, |
1596 Ambient = #Ambient t, | 1683 Ambient = #Ambient t, |
1597 Path = c :: #Path t, | 1684 Path = c :: #Path t, |
1598 Sent = #Sent t, | 1685 Sent = #Sent t, |
1599 Insert = #Insert t} | 1686 Insert = #Insert t, |
1687 Delete = #Delete t} | |
1600 fun addPaths (t : t, cs) = {Var = #Var t, | 1688 fun addPaths (t : t, cs) = {Var = #Var t, |
1601 Ambient = #Ambient t, | 1689 Ambient = #Ambient t, |
1602 Path = cs @ #Path t, | 1690 Path = cs @ #Path t, |
1603 Sent = #Sent t, | 1691 Sent = #Sent t, |
1604 Insert = #Insert t} | 1692 Insert = #Insert t, |
1693 Delete = #Delete t} | |
1605 fun clearPaths (t : t) = {Var = #Var t, | 1694 fun clearPaths (t : t) = {Var = #Var t, |
1606 Ambient = #Ambient t, | 1695 Ambient = #Ambient t, |
1607 Path = [], | 1696 Path = [], |
1608 Sent = #Sent t, | 1697 Sent = #Sent t, |
1609 Insert = #Insert t} | 1698 Insert = #Insert t, |
1699 Delete = #Delete t} | |
1610 fun setPaths (t : t, cs) = {Var = #Var t, | 1700 fun setPaths (t : t, cs) = {Var = #Var t, |
1611 Ambient = #Ambient t, | 1701 Ambient = #Ambient t, |
1612 Path = cs, | 1702 Path = cs, |
1613 Sent = #Sent t, | 1703 Sent = #Sent t, |
1614 Insert = #Insert t} | 1704 Insert = #Insert t, |
1705 Delete = #Delete t} | |
1615 | 1706 |
1616 fun sent (t : t) = #Sent t | 1707 fun sent (t : t) = #Sent t |
1617 fun addSent (t : t, c) = {Var = #Var t, | 1708 fun addSent (t : t, c) = {Var = #Var t, |
1618 Ambient = #Ambient t, | 1709 Ambient = #Ambient t, |
1619 Path = #Path t, | 1710 Path = #Path t, |
1620 Sent = c :: #Sent t, | 1711 Sent = c :: #Sent t, |
1621 Insert = #Insert t} | 1712 Insert = #Insert t, |
1713 Delete = #Delete t} | |
1622 fun setSent (t : t, cs) = {Var = #Var t, | 1714 fun setSent (t : t, cs) = {Var = #Var t, |
1623 Ambient = #Ambient t, | 1715 Ambient = #Ambient t, |
1624 Path = #Path t, | 1716 Path = #Path t, |
1625 Sent = cs, | 1717 Sent = cs, |
1626 Insert = #Insert t} | 1718 Insert = #Insert t, |
1719 Delete = #Delete t} | |
1627 | 1720 |
1628 fun inserted (t : t) = #Insert t | 1721 fun inserted (t : t) = #Insert t |
1629 fun addInsert (t : t, c) = {Var = #Var t, | 1722 fun addInsert (t : t, c) = {Var = #Var t, |
1630 Ambient = #Ambient t, | 1723 Ambient = #Ambient t, |
1631 Path = #Path t, | 1724 Path = #Path t, |
1632 Sent = #Sent t, | 1725 Sent = #Sent t, |
1633 Insert = c :: #Insert t} | 1726 Insert = c :: #Insert t, |
1727 Delete = #Delete t} | |
1728 | |
1729 fun deleted (t : t) = #Delete t | |
1730 fun addDelete (t : t, c) = {Var = #Var t, | |
1731 Ambient = #Ambient t, | |
1732 Path = #Path t, | |
1733 Sent = #Sent t, | |
1734 Insert = #Insert t, | |
1735 Delete = c :: #Delete t} | |
1634 | 1736 |
1635 end | 1737 end |
1636 | 1738 |
1637 fun evalExp env (e as (_, loc), st) = | 1739 fun evalExp env (e as (_, loc), st) = |
1638 let | 1740 let |
1868 in | 1970 in |
1869 (st, Var n) | 1971 (st, Var n) |
1870 end | 1972 end |
1871 | 1973 |
1872 val expIn = expIn rv env (fn "New" => Var new | 1974 val expIn = expIn rv env (fn "New" => Var new |
1873 | _ => raise Fail "Iflow.evalExp: Bad field expression in EDml") | 1975 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE") |
1874 | 1976 |
1875 val (es, st) = ListUtil.foldlMap | 1977 val (es, st) = ListUtil.foldlMap |
1876 (fn ((x, e), st) => | 1978 (fn ((x, e), st) => |
1877 let | 1979 let |
1878 val (e, st) = case expIn (e, st) of | 1980 val (e, st) = case expIn (e, st) of |
1885 end) | 1987 end) |
1886 st es | 1988 st es |
1887 in | 1989 in |
1888 (Recd [], St.addInsert (st, (loc, And (St.ambient st, | 1990 (Recd [], St.addInsert (st, (loc, And (St.ambient st, |
1889 Reln (Sql "$New", [Recd es]))))) | 1991 Reln (Sql "$New", [Recd es]))))) |
1992 end | |
1993 | Delete (tab, e) => | |
1994 let | |
1995 val (st, old) = St.nextVar st | |
1996 | |
1997 fun rv st = | |
1998 let | |
1999 val (st, n) = St.nextVar st | |
2000 in | |
2001 (st, Var n) | |
2002 end | |
2003 | |
2004 val expIn = expIn rv env (fn "T" => Var old | |
2005 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE") | |
2006 | |
2007 val (p, st) = case expIn (e, st) of | |
2008 (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean" | |
2009 | (inr p, st) => (p, st) | |
2010 | |
2011 val p = And (p, | |
2012 And (Reln (Sql "$Old", [Var old]), | |
2013 Reln (Sql tab, [Var old]))) | |
2014 in | |
2015 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p)))) | |
1890 end) | 2016 end) |
1891 | 2017 |
1892 | ENextval _ => default () | 2018 | ENextval _ => default () |
1893 | ESetval _ => default () | 2019 | ESetval _ => default () |
1894 | 2020 |
1922 val exptd = foldl (fn ((d, _), exptd) => | 2048 val exptd = foldl (fn ((d, _), exptd) => |
1923 case d of | 2049 case d of |
1924 DExport (_, _, n, _, _, _) => IS.add (exptd, n) | 2050 DExport (_, _, n, _, _, _) => IS.add (exptd, n) |
1925 | _ => exptd) IS.empty file | 2051 | _ => exptd) IS.empty file |
1926 | 2052 |
1927 fun decl ((d, _), (vals, inserts, client, insert)) = | 2053 fun decl ((d, _), (vals, inserts, deletes, client, insert, delete)) = |
1928 case d of | 2054 case d of |
1929 DVal (_, n, _, e, _) => | 2055 DVal (_, n, _, e, _) => |
1930 let | 2056 let |
1931 val isExptd = IS.member (exptd, n) | 2057 val isExptd = IS.member (exptd, n) |
1932 | 2058 |
1942 val (e, env, nv, p) = deAbs (e, [], 1, True) | 2068 val (e, env, nv, p) = deAbs (e, [], 1, True) |
1943 | 2069 |
1944 val (_, st) = evalExp env (e, St.create {Var = nv, | 2070 val (_, st) = evalExp env (e, St.create {Var = nv, |
1945 Ambient = p}) | 2071 Ambient = p}) |
1946 in | 2072 in |
1947 (St.sent st @ vals, St.inserted st @ inserts, client, insert) | 2073 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, client, insert, delete) |
1948 end | 2074 end |
1949 | 2075 |
1950 | DPolicy pol => | 2076 | DPolicy pol => |
1951 let | 2077 let |
1952 fun rv rvN = (rvN + 1, Lvar rvN) | 2078 fun rv rvN = (rvN + 1, Lvar rvN) |
1954 case pol of | 2080 case pol of |
1955 PolClient e => | 2081 PolClient e => |
1956 let | 2082 let |
1957 val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e | 2083 val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e |
1958 in | 2084 in |
1959 (vals, inserts, (p, outs) :: client, insert) | 2085 (vals, inserts, deletes, (p, outs) :: client, insert, delete) |
1960 end | 2086 end |
1961 | PolInsert e => | 2087 | PolInsert e => |
1962 let | 2088 let |
1963 val p = insertProp 0 rv e | 2089 val p = insertProp 0 rv e |
1964 in | 2090 in |
1965 (vals, inserts,client, p :: insert) | 2091 (vals, inserts, deletes, client, p :: insert, delete) |
2092 end | |
2093 | PolDelete e => | |
2094 let | |
2095 val p = deleteProp 0 rv e | |
2096 in | |
2097 (vals, inserts, deletes, client, insert, p :: delete) | |
1966 end | 2098 end |
1967 end | 2099 end |
1968 | 2100 |
1969 | _ => (vals, inserts, client, insert) | 2101 | _ => (vals, inserts, deletes, client, insert, delete) |
1970 | 2102 |
1971 val () = reset () | 2103 val () = reset () |
1972 | 2104 |
1973 val (vals, inserts, client, insert) = foldl decl ([], [], [], []) file | 2105 val (vals, inserts, deletes, client, insert, delete) = foldl decl ([], [], [], [], [], []) file |
1974 | 2106 |
1975 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ()) | 2107 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ()) |
1976 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ()) | 2108 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ()) |
2109 | |
2110 fun doDml (cmds, pols) = | |
2111 app (fn (loc, p) => | |
2112 if decompH p | |
2113 (fn hyps => | |
2114 List.exists (fn p' => | |
2115 decompG p' | |
2116 (fn goals => imply (hyps, goals, NONE))) | |
2117 pols) then | |
2118 () | |
2119 else | |
2120 (ErrorMsg.errorAt loc "The information flow policy may be violated here."; | |
2121 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds | |
1977 in | 2122 in |
1978 app (fn ((loc, e, p), fl) => | 2123 app (fn ((loc, e, p), fl) => |
1979 let | 2124 let |
1980 fun doOne e = | 2125 fun doOne e = |
1981 let | 2126 let |
2007 | Finish => () | 2152 | Finish => () |
2008 in | 2153 in |
2009 doAll e | 2154 doAll e |
2010 end) vals; | 2155 end) vals; |
2011 | 2156 |
2012 app (fn (loc, p) => | 2157 doDml (inserts, insert); |
2013 if decompH p | 2158 doDml (deletes, delete) |
2014 (fn hyps => | |
2015 List.exists (fn p' => | |
2016 decompG p' | |
2017 (fn goals => imply (hyps, goals, NONE))) | |
2018 insert) then | |
2019 () | |
2020 else | |
2021 (ErrorMsg.errorAt loc "The information flow policy may be violated here."; | |
2022 Print.preface ("The state satisifies this predicate:", p_prop p))) inserts | |
2023 end | 2159 end |
2024 | 2160 |
2025 val check = fn file => | 2161 val check = fn file => |
2026 let | 2162 let |
2027 val oldInline = Settings.getMonoInline () | 2163 val oldInline = Settings.getMonoInline () |