Mercurial > urweb
changeset 1249:7c6fc92f6c31
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 |
| files | src/iflow.sml |
| diffstat | 1 files changed, 41 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/src/iflow.sml Sun Apr 18 20:06:15 2010 -0400 +++ b/src/iflow.sml Thu Apr 29 11:47:24 2010 -0400 @@ -1205,6 +1205,10 @@ val stash : unit -> stashed val reinstate : stashed -> unit + type stashedPath + val stashPath : unit -> stashedPath + val reinstatePath : stashedPath -> unit + val nextVar : unit -> int val assert : atom list -> unit @@ -1335,6 +1339,10 @@ path := p; setHyps h) +type stashedPath = ((int * atom list) * check) option ref list +fun stashPath () = !path +fun reinstatePath p = path := p + fun nextVar () = let val n = !nvar @@ -1912,7 +1920,11 @@ evalExp env e (fn e => (St.send true (e, loc); k (Recd []))) | ESeq (e1, e2) => - evalExp env e1 (fn _ => evalExp env e2 k) + let + val path = St.stashPath () + in + evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k)) + end | ELet (_, _, e1, e2) => evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k) | EClosure (n, es) => @@ -1929,32 +1941,42 @@ | EQuery {query = q, body = b, initial = i, state = state, ...} => evalExp env i (fn i => let - val saved = St.stash () - - val () = (k i) - handle Cc.Contradiction => () - val () = St.reinstate saved - val r = Var (St.nextVar ()) val acc = Var (St.nextVar ()) - val touched = MonoUtil.Exp.fold {typ = fn (_, touched) => touched, - exp = fn (e, touched) => + val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st, + exp = fn (e, st as (cs, ts)) => case e of EDml e => (case parse dml e of - NONE => touched + NONE => st | SOME c => case c of - Insert _ => touched + Insert _ => st | Delete (tab, _) => - SS.add (touched, tab) + (cs, SS.add (ts, tab)) | Update (tab, _, _) => - SS.add (touched, tab)) - | _ => touched} - SS.empty b + (cs, SS.add (ts, tab))) + | EFfiApp ("Basis", "set_cookie", + [_, (EPrim (Prim.String cname), _), + _, _, _]) => + (SS.add (cs, cname), ts) + | _ => st} + (SS.empty, SS.empty) b in - SS.app (St.havocReln o Sql) touched; + case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of + (TRecord [], true, true) => () + | _ => + let + val saved = St.stash () + in + (k i) + handle Cc.Contradiction => (); + St.reinstate saved + end; + + SS.app (St.havocReln o Sql) ts; + SS.app St.havocCookie cs; doQuery {Env = env, NextVar = Var o St.nextVar, @@ -2110,7 +2132,7 @@ DExport (_, _, n, _, _, _) => IS.add (exptd, n) | _ => exptd) IS.empty file - fun decl (d, _) = + fun decl (d, loc) = case d of DTable (tab, fs, pk, _) => let @@ -2159,6 +2181,8 @@ St.reinstate saved end + | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check recursive functions." + | DPolicy pol => let val rvN = ref 0