Mercurial > urweb

comparison src/iflow.sml @ 1249:7c6fc92f6c31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 11:47:24 -0400
parents cf9a636f9b15
children e80582b927f2
comparison
equal deleted inserted replaced
1248:cf9a636f9b15 1249:7c6fc92f6c31
1203 1203
1204 type stashed 1204 type stashed
1205 val stash : unit -> stashed 1205 val stash : unit -> stashed
1206 val reinstate : stashed -> unit 1206 val reinstate : stashed -> unit
1207 1207
1208 type stashedPath
1209 val stashPath : unit -> stashedPath
1210 val reinstatePath : stashedPath -> unit
1211
1208 val nextVar : unit -> int 1212 val nextVar : unit -> int
1209 1213
1210 val assert : atom list -> unit 1214 val assert : atom list -> unit
1211 1215
1212 val addPath : check -> unit 1216 val addPath : check -> unit
1332 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps))) 1336 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
1333 fun reinstate (nv, p, h) = 1337 fun reinstate (nv, p, h) =
1334 (nvar := nv; 1338 (nvar := nv;
1335 path := p; 1339 path := p;
1336 setHyps h) 1340 setHyps h)
1341
1342 type stashedPath = ((int * atom list) * check) option ref list
1343 fun stashPath () = !path
1344 fun reinstatePath p = path := p
1337 1345
1338 fun nextVar () = 1346 fun nextVar () =
1339 let 1347 let
1340 val n = !nvar 1348 val n = !nvar
1341 in 1349 in
1910 evalExp env e (fn e => St.send true (e, loc)) 1918 evalExp env e (fn e => St.send true (e, loc))
1911 | EWrite e => 1919 | EWrite e =>
1912 evalExp env e (fn e => (St.send true (e, loc); 1920 evalExp env e (fn e => (St.send true (e, loc);
1913 k (Recd []))) 1921 k (Recd [])))
1914 | ESeq (e1, e2) => 1922 | ESeq (e1, e2) =>
1915 evalExp env e1 (fn _ => evalExp env e2 k) 1923 let
1924 val path = St.stashPath ()
1925 in
1926 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
1927 end
1916 | ELet (_, _, e1, e2) => 1928 | ELet (_, _, e1, e2) =>
1917 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k) 1929 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
1918 | EClosure (n, es) => 1930 | EClosure (n, es) =>
1919 let 1931 let
1920 fun doArgs (es, acc) = 1932 fun doArgs (es, acc) =
1927 end 1939 end
1928 1940
1929 | EQuery {query = q, body = b, initial = i, state = state, ...} => 1941 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
1930 evalExp env i (fn i => 1942 evalExp env i (fn i =>
1931 let 1943 let
1932 val saved = St.stash ()
1933
1934 val () = (k i)
1935 handle Cc.Contradiction => ()
1936 val () = St.reinstate saved
1937
1938 val r = Var (St.nextVar ()) 1944 val r = Var (St.nextVar ())
1939 val acc = Var (St.nextVar ()) 1945 val acc = Var (St.nextVar ())
1940 1946
1941 val touched = MonoUtil.Exp.fold {typ = fn (_, touched) => touched, 1947 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
1942 exp = fn (e, touched) => 1948 exp = fn (e, st as (cs, ts)) =>
1943 case e of 1949 case e of
1944 EDml e => 1950 EDml e =>
1945 (case parse dml e of 1951 (case parse dml e of
1946 NONE => touched 1952 NONE => st
1947 | SOME c => 1953 | SOME c =>
1948 case c of 1954 case c of
1949 Insert _ => touched 1955 Insert _ => st
1950 | Delete (tab, _) => 1956 | Delete (tab, _) =>
1951 SS.add (touched, tab) 1957 (cs, SS.add (ts, tab))
1952 | Update (tab, _, _) => 1958 | Update (tab, _, _) =>
1953 SS.add (touched, tab)) 1959 (cs, SS.add (ts, tab)))
1954 | _ => touched} 1960 | EFfiApp ("Basis", "set_cookie",
1955 SS.empty b 1961 [_, (EPrim (Prim.String cname), _),
1962 _, _, _]) =>
1963 (SS.add (cs, cname), ts)
1964 | _ => st}
1965 (SS.empty, SS.empty) b
1956 in 1966 in
1957 SS.app (St.havocReln o Sql) touched; 1967 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
1968 (TRecord [], true, true) => ()
1969 | _ =>
1970 let
1971 val saved = St.stash ()
1972 in
1973 (k i)
1974 handle Cc.Contradiction => ();
1975 St.reinstate saved
1976 end;
1977
1978 SS.app (St.havocReln o Sql) ts;
1979 SS.app St.havocCookie cs;
1958 1980
1959 doQuery {Env = env, 1981 doQuery {Env = env,
1960 NextVar = Var o St.nextVar, 1982 NextVar = Var o St.nextVar,
1961 Add = fn a => St.assert [a], 1983 Add = fn a => St.assert [a],
1962 Save = St.stash, 1984 Save = St.stash,
2108 val exptd = foldl (fn ((d, _), exptd) => 2130 val exptd = foldl (fn ((d, _), exptd) =>
2109 case d of 2131 case d of
2110 DExport (_, _, n, _, _, _) => IS.add (exptd, n) 2132 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
2111 | _ => exptd) IS.empty file 2133 | _ => exptd) IS.empty file
2112 2134
2113 fun decl (d, _) = 2135 fun decl (d, loc) =
2114 case d of 2136 case d of
2115 DTable (tab, fs, pk, _) => 2137 DTable (tab, fs, pk, _) =>
2116 let 2138 let
2117 val ks = 2139 val ks =
2118 case #1 pk of 2140 case #1 pk of
2156 in 2178 in
2157 St.assert ps; 2179 St.assert ps;
2158 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ()); 2180 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
2159 St.reinstate saved 2181 St.reinstate saved
2160 end 2182 end
2183
2184 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check recursive functions."
2161 2185
2162 | DPolicy pol => 2186 | DPolicy pol =>
2163 let 2187 let
2164 val rvN = ref 0 2188 val rvN = ref 0
2165 fun rv () = 2189 fun rv () =