summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 12:38:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-11 12:38:21 -0400
commit5f19e17c3423f845777bab953275535a912a6e48 (patch)
treec7a250099af040fd7ee16b03be72b7037e71d515
parentc53ff24e7f0d2c57713a4dfcb8c17b7a1ea82507 (diff)
Delete policies
-rw-r--r--lib/ur/basis.urs4
-rw-r--r--src/iflow.sml286
-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, 225 insertions, 75 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 8ae6597e..501284b7 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -808,5 +808,9 @@ val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
=> sql_query [] ([New = fs] ++ tables) []
-> sql_policy
+val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
+ => sql_query [] ([Old = fs] ++ tables) []
+ -> sql_policy
+
val debug : string -> transaction unit
diff --git a/src/iflow.sml b/src/iflow.sml
index cce52fec..f275d013 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -411,7 +411,7 @@ datatype node = Node of {Rep : node ref option ref,
Dt0 of string
| Dt1 of string * node ref
| Prim of Prim.t
- | Recrd of node ref SM.map ref
+ | Recrd of node ref SM.map ref * bool
| VFinish
| Nothing
@@ -446,22 +446,29 @@ fun p_rep n =
case !(#Rep (unNode n)) of
SOME n => p_rep n
| NONE =>
- case #Variety (unNode n) of
- Nothing => string ("?" ^ Int.toString (Unsafe.cast n))
- | Dt0 s => string ("Dt0(" ^ s ^ ")")
- | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
- space,
- p_rep n,
- string ")"]
- | Prim p => Prim.p_t p
- | Recrd (ref m) => box [string "{",
- p_list (fn (x, n) => box [string x,
- space,
- string "=",
- space,
- p_rep n]) (SM.listItemsi m),
- string "}"]
- | VFinish => string "FINISH"
+ box [string (Int.toString (Unsafe.cast n) ^ ":"),
+ space,
+ case #Variety (unNode n) of
+ Nothing => string "?"
+ | Dt0 s => string ("Dt0(" ^ s ^ ")")
+ | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
+ space,
+ p_rep n,
+ string ")"]
+ | Prim p => Prim.p_t p
+ | Recrd (ref m, b) => box [string "{",
+ p_list (fn (x, n) => box [string x,
+ space,
+ string "=",
+ space,
+ p_rep n]) (SM.listItemsi m),
+ string "}",
+ if b then
+ box [space,
+ string "(complete)"]
+ else
+ box []]
+ | VFinish => string "FINISH"]
fun p_database (db : database) =
box [string "Vars:",
@@ -489,15 +496,20 @@ fun repOf (n : representative) : representative =
end
fun markKnown r =
- if !(#Known (unNode r)) then
- ()
- else
- (#Known (unNode r) := true;
- SM.app markKnown (!(#Cons (unNode r)));
- case #Variety (unNode r) of
- Dt1 (_, r) => markKnown r
- | Recrd xes => SM.app markKnown (!xes)
- | _ => ())
+ let
+ val r = repOf r
+ in
+ (*Print.preface ("markKnown", p_rep r);*)
+ if !(#Known (unNode r)) then
+ ()(*TextIO.print "Already known\n"*)
+ else
+ (#Known (unNode r) := true;
+ SM.app markKnown (!(#Cons (unNode r)));
+ case #Variety (unNode r) of
+ Dt1 (_, r) => markKnown r
+ | Recrd (xes, _) => SM.app markKnown (!xes)
+ | _ => ())
+ end
fun representative (db : database, e) =
let
@@ -555,7 +567,7 @@ fun representative (db : database, e) =
val r' = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
Variety = Dt1 (f, r),
- Known = #Known (unNode r)})
+ Known = ref (!(#Known (unNode r)))})
in
#Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
r'
@@ -577,7 +589,7 @@ fun representative (db : database, e) =
val r' = ref (Node {Rep = ref NONE,
Cons = cons,
Variety = Nothing,
- Known = #Known (unNode r)})
+ Known = ref (!(#Known (unNode r)))})
val r'' = ref (Node {Rep = ref NONE,
Cons = #Cons (unNode r),
@@ -628,7 +640,7 @@ fun representative (db : database, e) =
val r' = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
- Variety = Recrd (ref xes),
+ Variety = Recrd (ref xes, true),
Known = ref false})
in
#Records db := (xes, r') :: (!(#Records db));
@@ -640,14 +652,14 @@ fun representative (db : database, e) =
val r = rep e
in
case #Variety (unNode r) of
- Recrd xes =>
+ Recrd (xes, _) =>
(case SM.find (!xes, f) of
SOME r => repOf r
| NONE => let
val r = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
Variety = Nothing,
- Known = #Known (unNode r)})
+ Known = ref (!(#Known (unNode r)))})
in
xes := SM.insert (!xes, f, r);
r
@@ -657,11 +669,11 @@ fun representative (db : database, e) =
val r' = ref (Node {Rep = ref NONE,
Cons = ref SM.empty,
Variety = Nothing,
- Known = #Known (unNode r)})
+ Known = ref (!(#Known (unNode r)))})
val r'' = ref (Node {Rep = ref NONE,
Cons = #Cons (unNode r),
- Variety = Recrd (ref (SM.insert (SM.empty, f, r'))),
+ Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
Known = #Known (unNode r)})
in
#Rep (unNode r) := SOME r'';
@@ -680,7 +692,12 @@ fun assert (db, a) =
ACond _ => ()
| AReln x =>
case x of
- (Known, [e]) => markKnown (representative (db, e))
+ (Known, [e]) =>
+ ((*Print.prefaces "Before" [("e", p_exp e),
+ ("db", p_database db)];*)
+ markKnown (representative (db, e))(*;
+ Print.prefaces "After" [("e", p_exp e),
+ ("db", p_database db)]*))
| (PCon0 f, [e]) =>
let
val r = representative (db, e)
@@ -744,7 +761,7 @@ fun assert (db, a) =
markEq (r1, r2)
else
raise Contradiction
- | (Recrd xes1, Recrd xes2) =>
+ | (Recrd (xes1, _), Recrd (xes2, _)) =>
let
fun unif (xes1, xes2) =
SM.appi (fn (x, r1) =>
@@ -805,7 +822,23 @@ fun check (db, a) =
ACond _ => false
| AReln x =>
case x of
- (Known, [e]) => !(#Known (unNode (representative (db, e))))
+ (Known, [e]) =>
+ let
+ fun isKnown r =
+ let
+ val r = repOf r
+ in
+ !(#Known (unNode r))
+ orelse case #Variety (unNode r) of
+ Dt1 (_, r) => isKnown r
+ | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
+ | _ => false
+ end
+
+ val r = representative (db, e)
+ in
+ isKnown r
+ end
| (PCon0 f, [e]) =>
(case #Variety (unNode (representative (db, e))) of
Dt0 f' => f' = f
@@ -836,7 +869,7 @@ fun builtFrom (db, {Base = bs, Derived = d}) =
Dt0 _ => true
| Dt1 (_, d) => loop d
| Prim _ => true
- | Recrd xes => List.all loop (SM.listItems (!xes))
+ | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
| VFinish => true
| Nothing => false
end
@@ -874,6 +907,7 @@ fun imply (hyps, goals, outs) =
val cc = Cc.database ()
val () = app (fn a => Cc.assert (cc, a)) hyps
in
+ (*Print.preface ("db", Cc.p_database cc);*)
(List.all (fn a =>
if Cc.check (cc, a) then
true
@@ -1222,6 +1256,7 @@ val query = log "query"
datatype dml =
Insert of string * (string * sqexp) list
+ | Delete of string * sqexp
val insert = log "insert"
(wrapP (follow (const "INSERT INTO ")
@@ -1232,11 +1267,19 @@ val insert = log "insert"
(follow (list sqexp)
(const ")")))))))
(fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
- (SOME (Insert (tab, ListPair.zipEq (fs, es))))
+ (SOME (tab, ListPair.zipEq (fs, es)))
handle ListPair.UnequalLengths => NONE))
+val delete = log "delete"
+ (wrap (follow (const "DELETE FROM ")
+ (follow uw_ident
+ (follow (const " AS T_T WHERE ")
+ sqexp)))
+ (fn ((), (tab, ((), es))) => (tab, es)))
+
val dml = log "dml"
- insert
+ (altL [wrap insert Insert,
+ wrap delete Delete])
fun removeDups (ls : (string * string) list) =
case ls of
@@ -1421,13 +1464,13 @@ fun queryProp env rvN rv oe e =
end
| AllCols oe =>
let
- val oe = Proj (oe, f)
+ fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
in
(rvN,
- Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
- And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
+ Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
+ And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
p)),
- Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
+ oeEq (Func (DtCon0 "Basis.bool.True", [])),
[])
end)
| _ => normal ())
@@ -1483,6 +1526,43 @@ fun insertProp rvN rv e =
end
end
+fun deleteProp 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.deleteProp: Bad table variable"
+ | SOME (_, e) => e
+
+ val p =
+ foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) 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)
@@ -1538,7 +1618,7 @@ fun removeRedundant p1 =
datatype cflow = Case | Where
datatype flow = Data | Control of cflow
type check = ErrorMsg.span * exp * prop
-type insert = ErrorMsg.span * prop
+type dml = ErrorMsg.span * prop
structure St :> sig
type t
@@ -1561,76 +1641,98 @@ structure St :> sig
val addSent : t * (check * flow) -> t
val setSent : t * (check * flow) list -> t
- val inserted : t -> insert list
- val addInsert : t * insert -> t
+ val inserted : t -> dml list
+ val addInsert : t * dml -> t
+
+ val deleted : t -> dml list
+ val addDelete : t * dml -> t
end = struct
type t = {Var : int,
Ambient : prop,
Path : (check * cflow) list,
Sent : (check * flow) list,
- Insert : insert list}
+ Insert : dml list,
+ Delete : dml list}
fun create {Var = v, Ambient = p} = {Var = v,
Ambient = p,
Path = [],
Sent = [],
- Insert = []}
+ Insert = [],
+ Delete = []}
fun curVar (t : t) = #Var t
fun nextVar (t : t) = ({Var = #Var t + 1,
Ambient = #Ambient t,
Path = #Path t,
Sent = #Sent t,
- Insert = #Insert t}, #Var t)
+ Insert = #Insert t,
+ Delete = #Delete t}, #Var t)
fun ambient (t : t) = #Ambient t
fun setAmbient (t : t, p) = {Var = #Var t,
Ambient = p,
Path = #Path t,
Sent = #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun paths (t : t) = #Path t
fun addPath (t : t, c) = {Var = #Var t,
Ambient = #Ambient t,
Path = c :: #Path t,
Sent = #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun addPaths (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = cs @ #Path t,
Sent = #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun clearPaths (t : t) = {Var = #Var t,
Ambient = #Ambient t,
Path = [],
Sent = #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun setPaths (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = cs,
Sent = #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun sent (t : t) = #Sent t
fun addSent (t : t, c) = {Var = #Var t,
Ambient = #Ambient t,
Path = #Path t,
Sent = c :: #Sent t,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun setSent (t : t, cs) = {Var = #Var t,
Ambient = #Ambient t,
Path = #Path t,
Sent = cs,
- Insert = #Insert t}
+ Insert = #Insert t,
+ Delete = #Delete t}
fun inserted (t : t) = #Insert t
fun addInsert (t : t, c) = {Var = #Var t,
Ambient = #Ambient t,
Path = #Path t,
Sent = #Sent t,
- Insert = c :: #Insert t}
+ Insert = c :: #Insert t,
+ Delete = #Delete t}
+
+fun deleted (t : t) = #Delete t
+fun addDelete (t : t, c) = {Var = #Var t,
+ Ambient = #Ambient t,
+ Path = #Path t,
+ Sent = #Sent t,
+ Insert = #Insert t,
+ Delete = c :: #Delete t}
end
@@ -1870,7 +1972,7 @@ fun evalExp env (e as (_, loc), st) =
end
val expIn = expIn rv env (fn "New" => Var new
- | _ => raise Fail "Iflow.evalExp: Bad field expression in EDml")
+ | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
val (es, st) = ListUtil.foldlMap
(fn ((x, e), st) =>
@@ -1887,6 +1989,30 @@ fun evalExp env (e as (_, loc), st) =
in
(Recd [], St.addInsert (st, (loc, And (St.ambient st,
Reln (Sql "$New", [Recd es])))))
+ end
+ | Delete (tab, e) =>
+ let
+ 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 DELETE")
+
+ val (p, st) = case expIn (e, st) of
+ (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean"
+ | (inr p, st) => (p, st)
+
+ val p = And (p,
+ And (Reln (Sql "$Old", [Var old]),
+ Reln (Sql tab, [Var old])))
+ in
+ (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
end)
| ENextval _ => default ()
@@ -1924,7 +2050,7 @@ fun check file =
DExport (_, _, n, _, _, _) => IS.add (exptd, n)
| _ => exptd) IS.empty file
- fun decl ((d, _), (vals, inserts, client, insert)) =
+ fun decl ((d, _), (vals, inserts, deletes, client, insert, delete)) =
case d of
DVal (_, n, _, e, _) =>
let
@@ -1944,7 +2070,7 @@ fun check file =
val (_, st) = evalExp env (e, St.create {Var = nv,
Ambient = p})
in
- (St.sent st @ vals, St.inserted st @ inserts, client, insert)
+ (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, client, insert, delete)
end
| DPolicy pol =>
@@ -1956,24 +2082,43 @@ fun check file =
let
val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e
in
- (vals, inserts, (p, outs) :: client, insert)
+ (vals, inserts, deletes, (p, outs) :: client, insert, delete)
end
| PolInsert e =>
let
val p = insertProp 0 rv e
in
- (vals, inserts,client, p :: insert)
+ (vals, inserts, deletes, client, p :: insert, delete)
+ end
+ | PolDelete e =>
+ let
+ val p = deleteProp 0 rv e
+ in
+ (vals, inserts, deletes, client, insert, p :: delete)
end
end
- | _ => (vals, inserts, client, insert)
+ | _ => (vals, inserts, deletes, client, insert, delete)
val () = reset ()
- val (vals, inserts, client, insert) = foldl decl ([], [], [], []) file
+ val (vals, inserts, deletes, client, insert, delete) = foldl decl ([], [], [], [], [], []) file
val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
+
+ fun doDml (cmds, pols) =
+ app (fn (loc, p) =>
+ if decompH p
+ (fn hyps =>
+ List.exists (fn p' =>
+ decompG p'
+ (fn goals => imply (hyps, goals, NONE)))
+ pols) then
+ ()
+ else
+ (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
+ Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
in
app (fn ((loc, e, p), fl) =>
let
@@ -2009,17 +2154,8 @@ fun check file =
doAll e
end) vals;
- app (fn (loc, p) =>
- if decompH p
- (fn hyps =>
- List.exists (fn p' =>
- decompG p'
- (fn goals => imply (hyps, goals, NONE)))
- insert) then
- ()
- else
- (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
- Print.preface ("The state satisifies this predicate:", p_prop p))) inserts
+ doDml (inserts, insert);
+ doDml (deletes, delete)
end
val check = fn file =>
diff --git a/src/mono.sml b/src/mono.sml
index 9585fbc1..284d4cd3 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -126,6 +126,7 @@ withtype exp = exp' located
datatype policy =
PolClient of exp
| PolInsert of exp
+ | PolDelete 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 e98fc924..b1b3a8e0 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -420,6 +420,9 @@ fun p_policy env pol =
| PolInsert e => box [string "mayInsert",
space,
p_exp env e]
+ | PolDelete e => box [string "mayDelete",
+ 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 4df9a6a0..f1c2d70f 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -63,6 +63,7 @@ fun shake file =
val e1 = case pol of
PolClient e1 => e1
| PolInsert e1 => e1
+ | PolDelete e1 => e1
in
usedVars st e1
end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index fa019b00..af01f560 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -547,6 +547,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
| PolInsert e =>
S.map2 (mfe ctx e,
PolInsert)
+ | PolDelete e =>
+ S.map2 (mfe ctx e,
+ PolDelete)
and mfvi ctx (x, n, t, e, s) =
S.bind2 (mft t,
diff --git a/src/monoize.sml b/src/monoize.sml
index 5bdc2aa2..4a11b12d 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3748,6 +3748,8 @@ fun monoDecl (env, fm) (all as (d, loc)) =
(e, L'.PolClient)
| L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayInsert"), _), _), _), _), _), e) =>
(e, L'.PolInsert)
+ | L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayDelete"), _), _), _), _), _), e) =>
+ (e, L'.PolDelete)
| _ => (poly (); (e, L'.PolClient))
val (e, fm) = monoExp (env, St.empty, fm) e