Mercurial > urweb

comparison src/iflow.sml @ 1282:a9a500d22ebc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Roll back WHERE checking
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 14:04:09 -0400
parents 60e19545841b
children acabf3935060
comparison
equal deleted inserted replaced
1281:60e19545841b 1282:a9a500d22ebc
1226 val addPath : check -> unit 1226 val addPath : check -> unit
1227 1227
1228 val allowSend : atom list * exp list -> unit 1228 val allowSend : atom list * exp list -> unit
1229 val send : check -> unit 1229 val send : check -> unit
1230 1230
1231 val allowEqual : { table : string, field : string, known : bool } -> unit
1232 val mayTest : prop -> bool
1233
1234 val allowInsert : atom list -> unit 1231 val allowInsert : atom list -> unit
1235 val insert : ErrorMsg.span -> unit 1232 val insert : ErrorMsg.span -> unit
1236 1233
1237 val allowDelete : atom list -> unit 1234 val allowDelete : atom list -> unit
1238 val delete : ErrorMsg.span -> unit 1235 val delete : ErrorMsg.span -> unit
1507 1504
1508 val deletable = ref ([] : atom list list) 1505 val deletable = ref ([] : atom list list)
1509 fun allowDelete v = deletable := v :: !deletable 1506 fun allowDelete v = deletable := v :: !deletable
1510 val delete = doable deletable 1507 val delete = doable deletable
1511 1508
1512 val testable = ref ([] : { table : string, field : string, known : bool } list)
1513 fun allowEqual v = testable := v :: !testable
1514 fun mayTest p =
1515 case p of
1516 Reln (Eq, [e1, e2]) =>
1517 let
1518 val (_, hs, _) = !hyps
1519
1520 fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x
1521 | _ => false) hs
1522
1523 fun allowed (tab, v) =
1524 case tab of
1525 Proj (Var tab, fd) =>
1526 List.exists (fn {table = tab', field = fd', known} =>
1527 fd' = fd
1528 andalso tableInHyps (tab', tab)
1529 andalso (not known orelse Cc.check (db, AReln (Known, [v])))) (!testable)
1530 | _ => false
1531 in
1532 if allowed (e1, e2) orelse allowed (e2, e1) then
1533 (assert [AReln (Eq, [e1, e2])];
1534 true)
1535 else
1536 false
1537 end
1538 | _ => false
1539
1540 fun reset () = (Cc.clear db; 1509 fun reset () = (Cc.clear db;
1541 path := []; 1510 path := [];
1542 hyps := (0, [], ref false); 1511 hyps := (0, [], ref false);
1543 nvar := 0; 1512 nvar := 0;
1544 sendable := []; 1513 sendable := [];
1545 testable := [];
1546 insertable := []; 1514 insertable := [];
1547 updatable := []; 1515 updatable := [];
1548 deletable := []) 1516 deletable := [])
1549 1517
1550 fun havocReln r = 1518 fun havocReln r =
1690 Env : exp list, 1658 Env : exp list,
1691 NextVar : unit -> exp, 1659 NextVar : unit -> exp,
1692 Add : atom -> unit, 1660 Add : atom -> unit,
1693 Save : unit -> 'a, 1661 Save : unit -> 'a,
1694 Restore : 'a -> unit, 1662 Restore : 'a -> unit,
1695 Cont : queryMode, 1663 Cont : queryMode
1696 Send : exp -> unit
1697 } 1664 }
1698 1665
1699 fun doQuery (arg : 'a doQuery) (e as (_, loc)) = 1666 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
1700 let 1667 let
1701 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query" 1668 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
1730 val expIn = expIn (#NextVar arg) (#Env arg) rvOf 1697 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
1731 1698
1732 val saved = #Save arg () 1699 val saved = #Save arg ()
1733 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) 1700 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1734 1701
1735 fun leavesE e = 1702 fun usedFields e =
1736 case e of 1703 case e of
1737 Const _ => [] 1704 SqConst _ => []
1738 | Var _ => [] 1705 | SqTrue => []
1739 | Lvar _ => [] 1706 | SqFalse => []
1740 | Func (_, es) => List.concat (map leavesE es) 1707 | Null => []
1741 | Recd xes => List.concat (map (leavesE o #2) xes) 1708 | SqNot e => usedFields e
1742 | Proj _ => [e] 1709 | Field (v, f) => [(false, Proj (rvOf v, f))]
1743 1710 | Computed _ => []
1744 fun leavesP p = 1711 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
1745 case p of 1712 | SqKnown _ => []
1746 True => [] 1713 | Inj e =>
1747 | False => [] 1714 (case deinj (#Env arg) e of
1748 | Unknown => [] 1715 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
1749 | And (p1, p2) => leavesP p1 @ leavesP p2 1716 [])
1750 | Or (p1, p2) => leavesP p1 @ leavesP p2 1717 | SOME e => [(true, e)])
1751 | Reln (_, es) => List.concat (map leavesE es) 1718 | SqFunc (_, e) => usedFields e
1752 | Cond (e, p) => e :: leavesP p 1719 | Unmodeled => []
1753 1720
1754 fun normal' () = 1721 fun normal' () =
1755 case #Cont arg of 1722 case #Cont arg of
1756 SomeCol k => 1723 SomeCol k =>
1757 let 1724 let
1800 let 1767 let
1801 val p = case expIn e of 1768 val p = case expIn e of
1802 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) 1769 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
1803 | inr p => p 1770 | inr p => p
1804 1771
1805 fun getConjuncts p =
1806 case p of
1807 And (p1, p2) => getConjuncts p1 @ getConjuncts p2
1808 | _ => [p]
1809
1810 val saved = #Save arg () 1772 val saved = #Save arg ()
1811
1812 val conjs = getConjuncts p
1813 val conjs = List.filter (not o St.mayTest) conjs
1814 in 1773 in
1815 app (fn p => app (#Send arg) (leavesP p)) conjs;
1816 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} 1774 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
1817 p (fn () => final () handle Cc.Contradiction => ()); 1775 p (fn () => final () handle Cc.Contradiction => ());
1818 #Restore arg saved 1776 #Restore arg saved
1819 end) 1777 end)
1820 handle Cc.Contradiction => () 1778 handle Cc.Contradiction => ()
2116 doQuery {Env = env, 2074 doQuery {Env = env,
2117 NextVar = Var o St.nextVar, 2075 NextVar = Var o St.nextVar,
2118 Add = fn a => St.assert [a], 2076 Add = fn a => St.assert [a],
2119 Save = St.stash, 2077 Save = St.stash,
2120 Restore = St.reinstate, 2078 Restore = St.reinstate,
2121 Send = fn e => St.send (e, loc),
2122 Cont = AllCols (fn x => 2079 Cont = AllCols (fn x =>
2123 (St.assert [AReln (Eq, [r, x])]; 2080 (St.assert [AReln (Eq, [r, x])];
2124 evalExp (acc :: r :: env) b k))} q 2081 evalExp (acc :: r :: env) b k))} q
2125 end) 2082 end)
2126 | EDml e => 2083 | EDml e =>
2489 fun doQ k = doQuery {Env = [], 2446 fun doQ k = doQuery {Env = [],
2490 NextVar = rv, 2447 NextVar = rv,
2491 Add = fn a => atoms := a :: !atoms, 2448 Add = fn a => atoms := a :: !atoms,
2492 Save = fn () => !atoms, 2449 Save = fn () => !atoms,
2493 Restore = fn ls => atoms := ls, 2450 Restore = fn ls => atoms := ls,
2494 Send = fn _ => (),
2495 Cont = SomeCol (fn r => k (rev (!atoms), r))} 2451 Cont = SomeCol (fn r => k (rev (!atoms), r))}
2496 2452
2497 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) => 2453 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
2498 tab' <> tab 2454 tab' <> tab
2499 orelse List.all (fn Lvar lv' => lv' <> lv 2455 orelse List.all (fn Lvar lv' => lv' <> lv
2525 val outs = [Lvar 0] 2481 val outs = [Lvar 0]
2526 in 2482 in
2527 St.allowSend ([p], outs) 2483 St.allowSend ([p], outs)
2528 end 2484 end
2529 | _ => ()) 2485 | _ => ())
2530 | PolEqual {table = tab, field = nm, known} =>
2531 (case #1 tab of
2532 EPrim (Prim.String tab) => St.allowEqual {table = String.extract (tab, 3, NONE),
2533 field = nm,
2534 known = known}
2535 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
2536 end 2486 end
2537 2487
2538 | _ => () 2488 | _ => ()
2539 in 2489 in
2540 app decl file 2490 app decl file