comparison src/iflow.sml @ 2048:4d64af730e35

Differentiate between HTML and normal string literals
author Adam Chlipala <adam@chlipala.net>
date Fri, 01 Aug 2014 15:44:17 -0400
parents 98895243b5b6
children 70ec9bb337be
comparison
equal deleted inserted replaced
2047:6be31671911b 2048:4d64af730e35
1444 [] => 1444 [] =>
1445 (if s = "set_cookie" then 1445 (if s = "set_cookie" then
1446 case es of 1446 case es of
1447 [_, (cname, _), _, _, _] => 1447 [_, (cname, _), _, _, _] =>
1448 (case #1 cname of 1448 (case #1 cname of
1449 EPrim (Prim.String cname) => 1449 EPrim (Prim.String (_, cname)) =>
1450 St.havocCookie cname 1450 St.havocCookie cname
1451 | _ => ()) 1451 | _ => ())
1452 | _ => () 1452 | _ => ()
1453 else 1453 else
1454 (); 1454 ();
1635 | Delete (tab, _) => 1635 | Delete (tab, _) =>
1636 (cs, SS.add (ts, tab)) 1636 (cs, SS.add (ts, tab))
1637 | Update (tab, _, _) => 1637 | Update (tab, _, _) =>
1638 (cs, SS.add (ts, tab))) 1638 (cs, SS.add (ts, tab)))
1639 | EFfiApp ("Basis", "set_cookie", 1639 | EFfiApp ("Basis", "set_cookie",
1640 [_, ((EPrim (Prim.String cname), _), _), 1640 [_, ((EPrim (Prim.String (_, cname)), _), _),
1641 _, _, _]) => 1641 _, _, _]) =>
1642 (SS.add (cs, cname), ts) 1642 (SS.add (cs, cname), ts)
1643 | _ => st} 1643 | _ => st}
1644 (SS.empty, SS.empty) b 1644 (SS.empty, SS.empty) b
1645 in 1645 in
1763 St.havocReln (Sql tab); 1763 St.havocReln (Sql tab);
1764 k (Recd [])) 1764 k (Recd []))
1765 handle Cc.Contradiction => ()) 1765 handle Cc.Contradiction => ())
1766 end) 1766 end)
1767 1767
1768 | ENextval (EPrim (Prim.String seq), _) => 1768 | ENextval (EPrim (Prim.String (_, seq)), _) =>
1769 let 1769 let
1770 val nv = St.nextVar () 1770 val nv = St.nextVar ()
1771 in 1771 in
1772 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])]; 1772 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
1773 k (Var nv) 1773 k (Var nv)
1774 end 1774 end
1775 | ENextval _ => default () 1775 | ENextval _ => default ()
1776 | ESetval _ => default () 1776 | ESetval _ => default ()
1777 1777
1778 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String cname), _), _)]), _), _, _) => 1778 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String (_, cname)), _), _)]), _), _, _) =>
1779 let 1779 let
1780 val e = Var (St.nextVar ()) 1780 val e = Var (St.nextVar ())
1781 val e' = Func (Other ("cookie/" ^ cname), []) 1781 val e' = Func (Other ("cookie/" ^ cname), [])
1782 in 1782 in
1783 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])]; 1783 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
1841 (e, fn x => x) 1841 (e, fn x => x)
1842 else 1842 else
1843 (e', fn e' => (EFfiApp (m, f, [(e', t)]), #2 e)) 1843 (e', fn e' => (EFfiApp (m, f, [(e', t)]), #2 e))
1844 | ECase (e', ps as 1844 | ECase (e', ps as
1845 [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _), 1845 [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
1846 (EPrim (Prim.String "TRUE"), _)), 1846 (EPrim (Prim.String (_, "TRUE")), _)),
1847 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _), 1847 ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
1848 (EPrim (Prim.String "FALSE"), _))], q) => 1848 (EPrim (Prim.String (_, "FALSE")), _))], q) =>
1849 (e', fn e' => (ECase (e', ps, q), #2 e)) 1849 (e', fn e' => (ECase (e', ps, q), #2 e))
1850 | _ => (e, fn x => x) 1850 | _ => (e, fn x => x)
1851 in 1851 in
1852 ([e'], k (ERel x, #2 e)) 1852 ([e'], k (ERel x, #2 e))
1853 end 1853 end
1905 case d of 1905 case d of
1906 DTable (tab, fs, pk, _) => 1906 DTable (tab, fs, pk, _) =>
1907 let 1907 let
1908 val ks = 1908 val ks =
1909 case #1 pk of 1909 case #1 pk of
1910 EPrim (Prim.String s) => 1910 EPrim (Prim.String (_, s)) =>
1911 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of 1911 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
1912 [] => [] 1912 [] => []
1913 | pk => [pk]) 1913 | pk => [pk])
1914 | _ => [] 1914 | _ => []
1915 in 1915 in
1972 | ENone _ => e 1972 | ENone _ => e
1973 | ESome (t, e) => (ESome (t, doExp env e), loc) 1973 | ESome (t, e) => (ESome (t, doExp env e), loc)
1974 | EFfi _ => e 1974 | EFfi _ => e
1975 | EFfiApp (m, f, es) => 1975 | EFfiApp (m, f, es) =>
1976 (case (m, f, es) of 1976 (case (m, f, es) of
1977 ("Basis", "set_cookie", [_, ((EPrim (Prim.String cname), _), _), _, _, _]) => 1977 ("Basis", "set_cookie", [_, ((EPrim (Prim.String (_, cname)), _), _), _, _, _]) =>
1978 cookies := SS.add (!cookies, cname) 1978 cookies := SS.add (!cookies, cname)
1979 | _ => (); 1979 | _ => ();
1980 (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc)) 1980 (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc))
1981 1981
1982 | EApp (e1, e2) => 1982 | EApp (e1, e2) =>
2148 :: AReln (Sql (tab ^ "$New"), [new]) 2148 :: AReln (Sql (tab ^ "$New"), [new])
2149 :: untab (tab, [new, old]) ats) 2149 :: untab (tab, [new, old]) ats)
2150 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e 2150 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
2151 | PolSequence e => 2151 | PolSequence e =>
2152 (case #1 e of 2152 (case #1 e of
2153 EPrim (Prim.String seq) => 2153 EPrim (Prim.String (_, seq)) =>
2154 let 2154 let
2155 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0]) 2155 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
2156 val outs = [Lvar 0] 2156 val outs = [Lvar 0]
2157 in 2157 in
2158 St.allowSend ([p], outs) 2158 St.allowSend ([p], outs)