diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-04-29 11:47:24 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-04-29 11:47:24 -0400 |
| commit | 05f75f15e2207afeeb97fec40ef0fd10d2befef8 (patch) | |
| tree | c8530e133c3005183399ae0e358913d05cf46370 /src/iflow.sml | |
| parent | a4b12519973682177c23c387b663d55a51dacab0 (diff) | |
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
Diffstat (limited to 'src/iflow.sml')
| -rw-r--r-- | src/iflow.sml | 58 |
1 files changed, 41 insertions, 17 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index 87103aeb..1e6d2411 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -1205,6 +1205,10 @@ structure St :> sig 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 @@ fun reinstate (nv, p, h) = 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 @@ fun evalExp env (e as (_, loc)) k = 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 @@ fun evalExp env (e as (_, loc)) k = | 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 @@ fun check file = 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 @@ fun check file = St.reinstate saved end + | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check recursive functions." + | DPolicy pol => let val rvN = ref 0 |