Mercurial > urweb

comparison src/iflow.sml @ 1242:4ed556678214

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
At loop heads, havoc relations that might be changed by the loop
author Adam Chlipala <adamc@hcoop.net>
date Sat, 17 Apr 2010 14:26:52 -0400
parents 58f5ac1bb849
children e754dc92c47c
comparison
equal deleted inserted replaced
1241:58f5ac1bb849 1242:4ed556678214
1835 handle Cc.Contradiction => () 1835 handle Cc.Contradiction => ()
1836 val () = St.reinstate saved 1836 val () = St.reinstate saved
1837 1837
1838 val r = Var (St.nextVar ()) 1838 val r = Var (St.nextVar ())
1839 val acc = Var (St.nextVar ()) 1839 val acc = Var (St.nextVar ())
1840
1841 val touched = MonoUtil.Exp.fold {typ = fn (_, touched) => touched,
1842 exp = fn (e, touched) =>
1843 case e of
1844 EDml e =>
1845 (case parse dml e of
1846 NONE => touched
1847 | SOME c =>
1848 case c of
1849 Insert _ => touched
1850 | Delete (tab, _) =>
1851 SS.add (touched, tab)
1852 | Update (tab, _, _) =>
1853 SS.add (touched, tab))
1854 | _ => touched}
1855 SS.empty b
1840 in 1856 in
1841 if MonoUtil.Exp.existsB {typ = fn _ => false, 1857 SS.app (St.havocReln o Sql) touched;
1842 exp = fn (n, e) => 1858
1843 case e of 1859 doQuery {Env = env,
1844 ERel n' => n' = n 1860 NextVar = Var o St.nextVar,
1845 | _ => false, 1861 Add = fn a => St.assert [a],
1846 bind = fn (n, b) => 1862 Save = St.stash,
1847 case b of 1863 Restore = St.reinstate,
1848 MonoUtil.Exp.RelE _ => n + 1 1864 UsedExp = fn (b, e) => St.send b (e, loc),
1849 | _ => n} 1865 Cont = AllCols (fn x =>
1850 0 b then 1866 (St.assert [AReln (Eq, [r, x])];
1851 doQuery {Env = env, 1867 evalExp (acc :: r :: env) b k))} q
1852 NextVar = Var o St.nextVar,
1853 Add = fn a => St.assert [a],
1854 Save = St.stash,
1855 Restore = St.reinstate,
1856 UsedExp = fn (b, e) => St.send b (e, loc),
1857 Cont = AllCols (fn _ => evalExp
1858 (acc :: r :: env)
1859 b (fn _ => default ()))} q
1860 else
1861 doQuery {Env = env,
1862 NextVar = Var o St.nextVar,
1863 Add = fn a => St.assert [a],
1864 Save = St.stash,
1865 Restore = St.reinstate,
1866 UsedExp = fn (b, e) => St.send b (e, loc),
1867 Cont = AllCols (fn x =>
1868 (St.assert [AReln (Eq, [r, x])];
1869 evalExp (acc :: r :: env) b k))} q
1870 end) 1868 end)
1871 | EDml e => 1869 | EDml e =>
1872 (case parse dml e of 1870 (case parse dml e of
1873 NONE => (print ("Warning: Information flow checker can't parse DML command at " 1871 NONE => (print ("Warning: Information flow checker can't parse DML command at "
1874 ^ ErrorMsg.spanToString loc ^ "\n"); 1872 ^ ErrorMsg.spanToString loc ^ "\n");