summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 13:11:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 13:11:25 -0400
commit30b7dba0eaa5a961ded15729ba64bbf67ce8903e (patch)
tree95861c082c2ded5a4d08911b8180b311fced7d24
parentefb882576e0fe75fa25829b417ea909b572634a5 (diff)
Update policies
-rw-r--r--lib/ur/basis.urs4
-rw-r--r--src/iflow.sml180
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_print.sml3
-rw-r--r--src/mono_shake.sml1
-rw-r--r--src/mono_util.sml3
-rw-r--r--src/monoize.sml2
7 files changed, 170 insertions, 24 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 501284b7..3241cc9a 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -812,5 +812,9 @@ val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
=> sql_query [] ([Old = fs] ++ tables) []
-> sql_policy
+val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
+ => sql_query [] ([Old = fs, New = fs] ++ tables) []
+ -> sql_policy
+
val debug : string -> transaction unit
diff --git a/src/iflow.sml b/src/iflow.sml
index 2b67b9ea..564cd20b 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -958,7 +958,7 @@ fun imply (hyps, goals, outs) =
in
reset ();
(*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
- ("goals", Print.p_list p_atom goals)];*)
+ ("goals", Print.p_list p_atom goals)];*)
gls goals (fn () => false) []
end handle Cc.Contradiction => true
@@ -1257,6 +1257,7 @@ val query = log "query"
datatype dml =
Insert of string * (string * sqexp) list
| Delete of string * sqexp
+ | Update of string * (string * sqexp) list * sqexp
val insert = log "insert"
(wrapP (follow (const "INSERT INTO ")
@@ -1277,9 +1278,24 @@ val delete = log "delete"
sqexp)))
(fn ((), (tab, ((), es))) => (tab, es)))
+val setting = log "setting"
+ (wrap (follow uw_ident (follow (const " = ") sqexp))
+ (fn (f, ((), e)) => (f, e)))
+
+val update = log "update"
+ (wrap (follow (const "UPDATE ")
+ (follow uw_ident
+ (follow (const " AS T_T SET ")
+ (follow (list setting)
+ (follow (ws (const "WHERE "))
+ sqexp)))))
+ (fn ((), (tab, ((), (fs, ((), e))))) =>
+ (tab, fs, e)))
+
val dml = log "dml"
(altL [wrap insert Insert,
- wrap delete Delete])
+ wrap delete Delete,
+ wrap update Update])
fun removeDups (ls : (string * string) list) =
case ls of
@@ -1576,6 +1592,51 @@ fun deleteProp rvN rv e =
end
end
+fun updateProp rvN rv e =
+ let
+ fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
+ ^ ErrorMsg.spanToString (#2 e) ^ "\n");
+ Unknown)
+ in
+ case parse query e of
+ NONE => default ()
+ | SOME r =>
+ let
+ val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
+ let
+ val (rvN, e) = rv rvN
+ in
+ ((v, e), rvN)
+ end) rvN (#From r)
+
+ fun rvOf v =
+ case List.find (fn (v', _) => v' = v) rvs of
+ NONE => raise Fail "Iflow.insertProp: Bad table variable"
+ | SOME (_, e) => e
+
+ val p =
+ foldl (fn ((t, v), p) =>
+ let
+ val t =
+ case v of
+ "New" => "$New"
+ | _ => t
+ in
+ And (p, Reln (Sql t, [rvOf v]))
+ end) True (#From r)
+
+ val expIn = expIn rv [] rvOf
+ in
+ And (Reln (Sql "$Old", [rvOf "Old"]),
+ case #Where r of
+ NONE => p
+ | SOME e =>
+ case expIn (e, rvN) of
+ (inr p', _) => And (p, p')
+ | _ => p)
+ end
+ end
+
fun evalPat env e (pt, _) =
case pt of
PWild => (env, True)
@@ -1659,6 +1720,9 @@ structure St :> sig
val deleted : t -> dml list
val addDelete : t * dml -> t
+
+ val updated : t -> dml list
+ val addUpdate : t * dml -> t
end = struct
type t = {Var : int,
@@ -1666,14 +1730,16 @@ type t = {Var : int,
Path : (check * cflow) list,
Sent : (check * flow) list,
Insert : dml list,
- Delete : dml list}
+ Delete : dml list,
+ Update : dml list}
fun create {Var = v, Ambient = p} = {Var = v,
Ambient = p,
Path = [],
Sent = [],
Insert = [],
- Delete = []}
+ Delete = [],
+ Update = []}
fun curVar (t : t) = #Var t
fun nextVar (t : t) = ({Var = #Var t + 1,
@@ -1681,7 +1747,8 @@ fun nextVar (t : t) = ({Var = #Var t + 1,
Path = #Path t,
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}, #Var t)
+ Delete = #Delete t,
+ Update = #Update t}, #Var t)
fun ambient (t : t) = #Ambient t
fun setAmbient (t : t, p) = {Var = #Var t,
@@ -1689,7 +1756,8 @@ fun setAmbient (t : t, p) = {Var = #Var t,
Path = #Path t,
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun paths (t : t) = #Path t
fun addPath (t : t, c) = {Var = #Var t,
@@ -1697,25 +1765,29 @@ fun addPath (t : t, c) = {Var = #Var t,
Path = c :: #Path t,
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun addPaths (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = cs @ #Path t,
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun clearPaths (t : t) = {Var = #Var t,
Ambient = #Ambient t,
Path = [],
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun setPaths (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = cs,
Sent = #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun sent (t : t) = #Sent t
fun addSent (t : t, c) = {Var = #Var t,
@@ -1723,13 +1795,15 @@ fun addSent (t : t, c) = {Var = #Var t,
Path = #Path t,
Sent = c :: #Sent t,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun setSent (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = #Path t,
Sent = cs,
Insert = #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun inserted (t : t) = #Insert t
fun addInsert (t : t, c) = {Var = #Var t,
@@ -1737,7 +1811,8 @@ fun addInsert (t : t, c) = {Var = #Var t,
Path = #Path t,
Sent = #Sent t,
Insert = c :: #Insert t,
- Delete = #Delete t}
+ Delete = #Delete t,
+ Update = #Update t}
fun deleted (t : t) = #Delete t
fun addDelete (t : t, c) = {Var = #Var t,
@@ -1745,7 +1820,17 @@ fun addDelete (t : t, c) = {Var = #Var t,
Path = #Path t,
Sent = #Sent t,
Insert = #Insert t,
- Delete = c :: #Delete t}
+ Delete = c :: #Delete t,
+ Update = #Update t}
+
+fun updated (t : t) = #Update t
+fun addUpdate (t : t, c) = {Var = #Var t,
+ Ambient = #Ambient t,
+ Path = #Path t,
+ Sent = #Sent t,
+ Insert = #Insert t,
+ Delete = #Delete t,
+ Update = c :: #Update t}
end
@@ -1984,8 +2069,7 @@ fun evalExp env (e as (_, loc), st) =
(st, Var n)
end
- val expIn = expIn rv env (fn "New" => Var new
- | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
+ val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT")
val (es, st) = ListUtil.foldlMap
(fn ((x, e), st) =>
@@ -2026,6 +2110,45 @@ fun evalExp env (e as (_, loc), st) =
Reln (Sql tab, [Var old])))
in
(Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
+ end
+ | Update (tab, fs, e) =>
+ let
+ val (st, new) = St.nextVar st
+ val (st, old) = St.nextVar st
+
+ fun rv st =
+ let
+ val (st, n) = St.nextVar st
+ in
+ (st, Var n)
+ end
+
+ val expIn = expIn rv env (fn "T" => Var old
+ | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
+
+ val (fs, st) = ListUtil.foldlMap
+ (fn ((x, e), st) =>
+ let
+ val (e, st) = case expIn (e, st) of
+ (inl e, st) => (e, st)
+ | (inr _, _) => raise Fail
+ ("Iflow.evalExp: Selecting "
+ ^ "boolean expression")
+ in
+ ((x, e), st)
+ end)
+ st fs
+
+ val (p, st) = case expIn (e, st) of
+ (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
+ | (inr p, st) => (p, st)
+
+ val p = And (p,
+ And (Reln (Sql "$New", [Recd fs]),
+ And (Reln (Sql "$Old", [Var old]),
+ Reln (Sql tab, [Var old]))))
+ in
+ (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
end)
| ENextval _ => default ()
@@ -2063,7 +2186,7 @@ fun check file =
DExport (_, _, n, _, _, _) => IS.add (exptd, n)
| _ => exptd) IS.empty file
- fun decl ((d, _), (vals, inserts, deletes, client, insert, delete)) =
+ fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
case d of
DVal (_, n, _, e, _) =>
let
@@ -2083,7 +2206,8 @@ fun check file =
val (_, st) = evalExp env (e, St.create {Var = nv,
Ambient = p})
in
- (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, client, insert, delete)
+ (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates,
+ client, insert, delete, update)
end
| DPolicy pol =>
@@ -2095,27 +2219,34 @@ fun check file =
let
val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e
in
- (vals, inserts, deletes, (p, outs) :: client, insert, delete)
+ (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
end
| PolInsert e =>
let
val p = insertProp 0 rv e
in
- (vals, inserts, deletes, client, p :: insert, delete)
+ (vals, inserts, deletes, updates, client, p :: insert, delete, update)
end
| PolDelete e =>
let
val p = deleteProp 0 rv e
in
- (vals, inserts, deletes, client, insert, p :: delete)
+ (vals, inserts, deletes, updates, client, insert, p :: delete, update)
+ end
+ | PolUpdate e =>
+ let
+ val p = updateProp 0 rv e
+ in
+ (vals, inserts, deletes, updates, client, insert, delete, p :: update)
end
end
- | _ => (vals, inserts, deletes, client, insert, delete)
+ | _ => (vals, inserts, deletes, updates, client, insert, delete, update)
val () = reset ()
- val (vals, inserts, deletes, client, insert, delete) = foldl decl ([], [], [], [], [], []) file
+ val (vals, inserts, deletes, updates, client, insert, delete, update) =
+ foldl decl ([], [], [], [], [], [], [], []) file
val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
@@ -2168,7 +2299,8 @@ fun check file =
end) vals;
doDml (inserts, insert);
- doDml (deletes, delete)
+ doDml (deletes, delete);
+ doDml (updates, update)
end
val check = fn file =>
diff --git a/src/mono.sml b/src/mono.sml
index 284d4cd3..79cde237 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -127,6 +127,7 @@ datatype policy =
PolClient of exp
| PolInsert of exp
| PolDelete of exp
+ | PolUpdate of exp
datatype decl' =
DDatatype of (string * int * (string * int * typ option) list) list
diff --git a/src/mono_print.sml b/src/mono_print.sml
index b1b3a8e0..b8016ff8 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -423,6 +423,9 @@ fun p_policy env pol =
| PolDelete e => box [string "mayDelete",
space,
p_exp env e]
+ | PolUpdate e => box [string "mayUpdate",
+ space,
+ p_exp env e]
fun p_decl env (dAll as (d, _) : decl) =
case d of
diff --git a/src/mono_shake.sml b/src/mono_shake.sml
index f1c2d70f..6b248636 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -64,6 +64,7 @@ fun shake file =
PolClient e1 => e1
| PolInsert e1 => e1
| PolDelete e1 => e1
+ | PolUpdate e1 => e1
in
usedVars st e1
end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index af01f560..085b68f8 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -550,6 +550,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
| PolDelete e =>
S.map2 (mfe ctx e,
PolDelete)
+ | PolUpdate e =>
+ S.map2 (mfe ctx e,
+ PolUpdate)
and mfvi ctx (x, n, t, e, s) =
S.bind2 (mft t,
diff --git a/src/monoize.sml b/src/monoize.sml
index 4a11b12d..601b690f 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3750,6 +3750,8 @@ fun monoDecl (env, fm) (all as (d, loc)) =
(e, L'.PolInsert)
| L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayDelete"), _), _), _), _), _), e) =>
(e, L'.PolDelete)
+ | L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayUpdate"), _), _), _), _), _), e) =>
+ (e, L'.PolUpdate)
| _ => (poly (); (e, L'.PolClient))
val (e, fm) = monoExp (env, St.empty, fm) e