Mercurial > urweb

comparison src/iflow.sml @ 1223:62af4cacd191

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update policies
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 13:11:25 -0400
parents 117f13bdc1fd
children 3950cf1f5736
comparison
equal deleted inserted replaced
1222:117f13bdc1fd 1223:62af4cacd191
956 end 956 end
957 | g :: goals => gls goals onFail (g :: acc) 957 | g :: goals => gls goals onFail (g :: acc)
958 in 958 in
959 reset (); 959 reset ();
960 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps), 960 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
961 ("goals", Print.p_list p_atom goals)];*) 961 ("goals", Print.p_list p_atom goals)];*)
962 gls goals (fn () => false) [] 962 gls goals (fn () => false) []
963 end handle Cc.Contradiction => true 963 end handle Cc.Contradiction => true
964 964
965 fun patCon pc = 965 fun patCon pc =
966 case pc of 966 case pc of
1255 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) 1255 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
1256 1256
1257 datatype dml = 1257 datatype dml =
1258 Insert of string * (string * sqexp) list 1258 Insert of string * (string * sqexp) list
1259 | Delete of string * sqexp 1259 | Delete of string * sqexp
1260 | Update of string * (string * sqexp) list * sqexp
1260 1261
1261 val insert = log "insert" 1262 val insert = log "insert"
1262 (wrapP (follow (const "INSERT INTO ") 1263 (wrapP (follow (const "INSERT INTO ")
1263 (follow uw_ident 1264 (follow uw_ident
1264 (follow (const " (") 1265 (follow (const " (")
1275 (follow uw_ident 1276 (follow uw_ident
1276 (follow (const " AS T_T WHERE ") 1277 (follow (const " AS T_T WHERE ")
1277 sqexp))) 1278 sqexp)))
1278 (fn ((), (tab, ((), es))) => (tab, es))) 1279 (fn ((), (tab, ((), es))) => (tab, es)))
1279 1280
1281 val setting = log "setting"
1282 (wrap (follow uw_ident (follow (const " = ") sqexp))
1283 (fn (f, ((), e)) => (f, e)))
1284
1285 val update = log "update"
1286 (wrap (follow (const "UPDATE ")
1287 (follow uw_ident
1288 (follow (const " AS T_T SET ")
1289 (follow (list setting)
1290 (follow (ws (const "WHERE "))
1291 sqexp)))))
1292 (fn ((), (tab, ((), (fs, ((), e))))) =>
1293 (tab, fs, e)))
1294
1280 val dml = log "dml" 1295 val dml = log "dml"
1281 (altL [wrap insert Insert, 1296 (altL [wrap insert Insert,
1282 wrap delete Delete]) 1297 wrap delete Delete,
1298 wrap update Update])
1283 1299
1284 fun removeDups (ls : (string * string) list) = 1300 fun removeDups (ls : (string * string) list) =
1285 case ls of 1301 case ls of
1286 [] => [] 1302 [] => []
1287 | x :: ls => 1303 | x :: ls =>
1574 (inr p', _) => And (p, p') 1590 (inr p', _) => And (p, p')
1575 | _ => p) 1591 | _ => p)
1576 end 1592 end
1577 end 1593 end
1578 1594
1595 fun updateProp rvN rv e =
1596 let
1597 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1598 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1599 Unknown)
1600 in
1601 case parse query e of
1602 NONE => default ()
1603 | SOME r =>
1604 let
1605 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1606 let
1607 val (rvN, e) = rv rvN
1608 in
1609 ((v, e), rvN)
1610 end) rvN (#From r)
1611
1612 fun rvOf v =
1613 case List.find (fn (v', _) => v' = v) rvs of
1614 NONE => raise Fail "Iflow.insertProp: Bad table variable"
1615 | SOME (_, e) => e
1616
1617 val p =
1618 foldl (fn ((t, v), p) =>
1619 let
1620 val t =
1621 case v of
1622 "New" => "$New"
1623 | _ => t
1624 in
1625 And (p, Reln (Sql t, [rvOf v]))
1626 end) True (#From r)
1627
1628 val expIn = expIn rv [] rvOf
1629 in
1630 And (Reln (Sql "$Old", [rvOf "Old"]),
1631 case #Where r of
1632 NONE => p
1633 | SOME e =>
1634 case expIn (e, rvN) of
1635 (inr p', _) => And (p, p')
1636 | _ => p)
1637 end
1638 end
1639
1579 fun evalPat env e (pt, _) = 1640 fun evalPat env e (pt, _) =
1580 case pt of 1641 case pt of
1581 PWild => (env, True) 1642 PWild => (env, True)
1582 | PVar _ => (e :: env, True) 1643 | PVar _ => (e :: env, True)
1583 | PPrim _ => (env, True) 1644 | PPrim _ => (env, True)
1657 val inserted : t -> dml list 1718 val inserted : t -> dml list
1658 val addInsert : t * dml -> t 1719 val addInsert : t * dml -> t
1659 1720
1660 val deleted : t -> dml list 1721 val deleted : t -> dml list
1661 val addDelete : t * dml -> t 1722 val addDelete : t * dml -> t
1723
1724 val updated : t -> dml list
1725 val addUpdate : t * dml -> t
1662 end = struct 1726 end = struct
1663 1727
1664 type t = {Var : int, 1728 type t = {Var : int,
1665 Ambient : prop, 1729 Ambient : prop,
1666 Path : (check * cflow) list, 1730 Path : (check * cflow) list,
1667 Sent : (check * flow) list, 1731 Sent : (check * flow) list,
1668 Insert : dml list, 1732 Insert : dml list,
1669 Delete : dml list} 1733 Delete : dml list,
1734 Update : dml list}
1670 1735
1671 fun create {Var = v, Ambient = p} = {Var = v, 1736 fun create {Var = v, Ambient = p} = {Var = v,
1672 Ambient = p, 1737 Ambient = p,
1673 Path = [], 1738 Path = [],
1674 Sent = [], 1739 Sent = [],
1675 Insert = [], 1740 Insert = [],
1676 Delete = []} 1741 Delete = [],
1742 Update = []}
1677 1743
1678 fun curVar (t : t) = #Var t 1744 fun curVar (t : t) = #Var t
1679 fun nextVar (t : t) = ({Var = #Var t + 1, 1745 fun nextVar (t : t) = ({Var = #Var t + 1,
1680 Ambient = #Ambient t, 1746 Ambient = #Ambient t,
1681 Path = #Path t, 1747 Path = #Path t,
1682 Sent = #Sent t, 1748 Sent = #Sent t,
1683 Insert = #Insert t, 1749 Insert = #Insert t,
1684 Delete = #Delete t}, #Var t) 1750 Delete = #Delete t,
1751 Update = #Update t}, #Var t)
1685 1752
1686 fun ambient (t : t) = #Ambient t 1753 fun ambient (t : t) = #Ambient t
1687 fun setAmbient (t : t, p) = {Var = #Var t, 1754 fun setAmbient (t : t, p) = {Var = #Var t,
1688 Ambient = p, 1755 Ambient = p,
1689 Path = #Path t, 1756 Path = #Path t,
1690 Sent = #Sent t, 1757 Sent = #Sent t,
1691 Insert = #Insert t, 1758 Insert = #Insert t,
1692 Delete = #Delete t} 1759 Delete = #Delete t,
1760 Update = #Update t}
1693 1761
1694 fun paths (t : t) = #Path t 1762 fun paths (t : t) = #Path t
1695 fun addPath (t : t, c) = {Var = #Var t, 1763 fun addPath (t : t, c) = {Var = #Var t,
1696 Ambient = #Ambient t, 1764 Ambient = #Ambient t,
1697 Path = c :: #Path t, 1765 Path = c :: #Path t,
1698 Sent = #Sent t, 1766 Sent = #Sent t,
1699 Insert = #Insert t, 1767 Insert = #Insert t,
1700 Delete = #Delete t} 1768 Delete = #Delete t,
1769 Update = #Update t}
1701 fun addPaths (t : t, cs) = {Var = #Var t, 1770 fun addPaths (t : t, cs) = {Var = #Var t,
1702 Ambient = #Ambient t, 1771 Ambient = #Ambient t,
1703 Path = cs @ #Path t, 1772 Path = cs @ #Path t,
1704 Sent = #Sent t, 1773 Sent = #Sent t,
1705 Insert = #Insert t, 1774 Insert = #Insert t,
1706 Delete = #Delete t} 1775 Delete = #Delete t,
1776 Update = #Update t}
1707 fun clearPaths (t : t) = {Var = #Var t, 1777 fun clearPaths (t : t) = {Var = #Var t,
1708 Ambient = #Ambient t, 1778 Ambient = #Ambient t,
1709 Path = [], 1779 Path = [],
1710 Sent = #Sent t, 1780 Sent = #Sent t,
1711 Insert = #Insert t, 1781 Insert = #Insert t,
1712 Delete = #Delete t} 1782 Delete = #Delete t,
1783 Update = #Update t}
1713 fun setPaths (t : t, cs) = {Var = #Var t, 1784 fun setPaths (t : t, cs) = {Var = #Var t,
1714 Ambient = #Ambient t, 1785 Ambient = #Ambient t,
1715 Path = cs, 1786 Path = cs,
1716 Sent = #Sent t, 1787 Sent = #Sent t,
1717 Insert = #Insert t, 1788 Insert = #Insert t,
1718 Delete = #Delete t} 1789 Delete = #Delete t,
1790 Update = #Update t}
1719 1791
1720 fun sent (t : t) = #Sent t 1792 fun sent (t : t) = #Sent t
1721 fun addSent (t : t, c) = {Var = #Var t, 1793 fun addSent (t : t, c) = {Var = #Var t,
1722 Ambient = #Ambient t, 1794 Ambient = #Ambient t,
1723 Path = #Path t, 1795 Path = #Path t,
1724 Sent = c :: #Sent t, 1796 Sent = c :: #Sent t,
1725 Insert = #Insert t, 1797 Insert = #Insert t,
1726 Delete = #Delete t} 1798 Delete = #Delete t,
1799 Update = #Update t}
1727 fun setSent (t : t, cs) = {Var = #Var t, 1800 fun setSent (t : t, cs) = {Var = #Var t,
1728 Ambient = #Ambient t, 1801 Ambient = #Ambient t,
1729 Path = #Path t, 1802 Path = #Path t,
1730 Sent = cs, 1803 Sent = cs,
1731 Insert = #Insert t, 1804 Insert = #Insert t,
1732 Delete = #Delete t} 1805 Delete = #Delete t,
1806 Update = #Update t}
1733 1807
1734 fun inserted (t : t) = #Insert t 1808 fun inserted (t : t) = #Insert t
1735 fun addInsert (t : t, c) = {Var = #Var t, 1809 fun addInsert (t : t, c) = {Var = #Var t,
1736 Ambient = #Ambient t, 1810 Ambient = #Ambient t,
1737 Path = #Path t, 1811 Path = #Path t,
1738 Sent = #Sent t, 1812 Sent = #Sent t,
1739 Insert = c :: #Insert t, 1813 Insert = c :: #Insert t,
1740 Delete = #Delete t} 1814 Delete = #Delete t,
1815 Update = #Update t}
1741 1816
1742 fun deleted (t : t) = #Delete t 1817 fun deleted (t : t) = #Delete t
1743 fun addDelete (t : t, c) = {Var = #Var t, 1818 fun addDelete (t : t, c) = {Var = #Var t,
1744 Ambient = #Ambient t, 1819 Ambient = #Ambient t,
1745 Path = #Path t, 1820 Path = #Path t,
1746 Sent = #Sent t, 1821 Sent = #Sent t,
1747 Insert = #Insert t, 1822 Insert = #Insert t,
1748 Delete = c :: #Delete t} 1823 Delete = c :: #Delete t,
1824 Update = #Update t}
1825
1826 fun updated (t : t) = #Update t
1827 fun addUpdate (t : t, c) = {Var = #Var t,
1828 Ambient = #Ambient t,
1829 Path = #Path t,
1830 Sent = #Sent t,
1831 Insert = #Insert t,
1832 Delete = #Delete t,
1833 Update = c :: #Update t}
1749 1834
1750 end 1835 end
1751 1836
1752 fun evalExp env (e as (_, loc), st) = 1837 fun evalExp env (e as (_, loc), st) =
1753 let 1838 let
1982 val (st, n) = St.nextVar st 2067 val (st, n) = St.nextVar st
1983 in 2068 in
1984 (st, Var n) 2069 (st, Var n)
1985 end 2070 end
1986 2071
1987 val expIn = expIn rv env (fn "New" => Var new 2072 val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT")
1988 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
1989 2073
1990 val (es, st) = ListUtil.foldlMap 2074 val (es, st) = ListUtil.foldlMap
1991 (fn ((x, e), st) => 2075 (fn ((x, e), st) =>
1992 let 2076 let
1993 val (e, st) = case expIn (e, st) of 2077 val (e, st) = case expIn (e, st) of
2024 val p = And (p, 2108 val p = And (p,
2025 And (Reln (Sql "$Old", [Var old]), 2109 And (Reln (Sql "$Old", [Var old]),
2026 Reln (Sql tab, [Var old]))) 2110 Reln (Sql tab, [Var old])))
2027 in 2111 in
2028 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p)))) 2112 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
2113 end
2114 | Update (tab, fs, e) =>
2115 let
2116 val (st, new) = St.nextVar st
2117 val (st, old) = St.nextVar st
2118
2119 fun rv st =
2120 let
2121 val (st, n) = St.nextVar st
2122 in
2123 (st, Var n)
2124 end
2125
2126 val expIn = expIn rv env (fn "T" => Var old
2127 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
2128
2129 val (fs, st) = ListUtil.foldlMap
2130 (fn ((x, e), st) =>
2131 let
2132 val (e, st) = case expIn (e, st) of
2133 (inl e, st) => (e, st)
2134 | (inr _, _) => raise Fail
2135 ("Iflow.evalExp: Selecting "
2136 ^ "boolean expression")
2137 in
2138 ((x, e), st)
2139 end)
2140 st fs
2141
2142 val (p, st) = case expIn (e, st) of
2143 (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
2144 | (inr p, st) => (p, st)
2145
2146 val p = And (p,
2147 And (Reln (Sql "$New", [Recd fs]),
2148 And (Reln (Sql "$Old", [Var old]),
2149 Reln (Sql tab, [Var old]))))
2150 in
2151 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
2029 end) 2152 end)
2030 2153
2031 | ENextval _ => default () 2154 | ENextval _ => default ()
2032 | ESetval _ => default () 2155 | ESetval _ => default ()
2033 2156
2061 val exptd = foldl (fn ((d, _), exptd) => 2184 val exptd = foldl (fn ((d, _), exptd) =>
2062 case d of 2185 case d of
2063 DExport (_, _, n, _, _, _) => IS.add (exptd, n) 2186 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
2064 | _ => exptd) IS.empty file 2187 | _ => exptd) IS.empty file
2065 2188
2066 fun decl ((d, _), (vals, inserts, deletes, client, insert, delete)) = 2189 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
2067 case d of 2190 case d of
2068 DVal (_, n, _, e, _) => 2191 DVal (_, n, _, e, _) =>
2069 let 2192 let
2070 val isExptd = IS.member (exptd, n) 2193 val isExptd = IS.member (exptd, n)
2071 2194
2081 val (e, env, nv, p) = deAbs (e, [], 1, True) 2204 val (e, env, nv, p) = deAbs (e, [], 1, True)
2082 2205
2083 val (_, st) = evalExp env (e, St.create {Var = nv, 2206 val (_, st) = evalExp env (e, St.create {Var = nv,
2084 Ambient = p}) 2207 Ambient = p})
2085 in 2208 in
2086 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, client, insert, delete) 2209 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates,
2210 client, insert, delete, update)
2087 end 2211 end
2088 2212
2089 | DPolicy pol => 2213 | DPolicy pol =>
2090 let 2214 let
2091 fun rv rvN = (rvN + 1, Lvar rvN) 2215 fun rv rvN = (rvN + 1, Lvar rvN)
2093 case pol of 2217 case pol of
2094 PolClient e => 2218 PolClient e =>
2095 let 2219 let
2096 val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e 2220 val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e
2097 in 2221 in
2098 (vals, inserts, deletes, (p, outs) :: client, insert, delete) 2222 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
2099 end 2223 end
2100 | PolInsert e => 2224 | PolInsert e =>
2101 let 2225 let
2102 val p = insertProp 0 rv e 2226 val p = insertProp 0 rv e
2103 in 2227 in
2104 (vals, inserts, deletes, client, p :: insert, delete) 2228 (vals, inserts, deletes, updates, client, p :: insert, delete, update)
2105 end 2229 end
2106 | PolDelete e => 2230 | PolDelete e =>
2107 let 2231 let
2108 val p = deleteProp 0 rv e 2232 val p = deleteProp 0 rv e
2109 in 2233 in
2110 (vals, inserts, deletes, client, insert, p :: delete) 2234 (vals, inserts, deletes, updates, client, insert, p :: delete, update)
2235 end
2236 | PolUpdate e =>
2237 let
2238 val p = updateProp 0 rv e
2239 in
2240 (vals, inserts, deletes, updates, client, insert, delete, p :: update)
2111 end 2241 end
2112 end 2242 end
2113 2243
2114 | _ => (vals, inserts, deletes, client, insert, delete) 2244 | _ => (vals, inserts, deletes, updates, client, insert, delete, update)
2115 2245
2116 val () = reset () 2246 val () = reset ()
2117 2247
2118 val (vals, inserts, deletes, client, insert, delete) = foldl decl ([], [], [], [], [], []) file 2248 val (vals, inserts, deletes, updates, client, insert, delete, update) =
2249 foldl decl ([], [], [], [], [], [], [], []) file
2119 2250
2120 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ()) 2251 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
2121 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ()) 2252 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
2122 2253
2123 fun doDml (cmds, pols) = 2254 fun doDml (cmds, pols) =
2166 in 2297 in
2167 doAll e 2298 doAll e
2168 end) vals; 2299 end) vals;
2169 2300
2170 doDml (inserts, insert); 2301 doDml (inserts, insert);
2171 doDml (deletes, delete) 2302 doDml (deletes, delete);
2303 doDml (updates, update)
2172 end 2304 end
2173 2305
2174 val check = fn file => 2306 val check = fn file =>
2175 let 2307 let
2176 val oldInline = Settings.getMonoInline () 2308 val oldInline = Settings.getMonoInline ()