summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-29 11:47:24 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-29 11:47:24 -0400
commit05f75f15e2207afeeb97fec40ef0fd10d2befef8 (patch)
treec8530e133c3005183399ae0e358913d05cf46370
parenta4b12519973682177c23c387b663d55a51dacab0 (diff)
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
-rw-r--r--src/iflow.sml58
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