Mercurial > urweb
changeset 1220:526575a9537a
Insert policies
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 11 Apr 2010 10:57:52 -0400 |
| parents | 3224faec752d |
| children | 00e628854005 |
| files | lib/ur/basis.urs src/iflow.sml src/mono.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml |
| diffstat | 7 files changed, 298 insertions(+), 88 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Sat Apr 10 13:12:42 2010 -0400 +++ b/lib/ur/basis.urs Sun Apr 11 10:57:52 2010 -0400 @@ -804,5 +804,9 @@ -> [tables ~ exps] => sql_query [] tables exps -> sql_policy +val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables] + => sql_query [] ([New = fs] ++ tables) [] + -> sql_policy + val debug : string -> transaction unit
--- a/src/iflow.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/iflow.sml Sun Apr 11 10:57:52 2010 -0400 @@ -884,8 +884,10 @@ ("db", Cc.p_database cc)];*) false)) acc (*andalso (Print.preface ("Finding", Cc.p_database cc); true)*) - andalso Cc.builtFrom (cc, {Derived = Var 0, - Base = outs})) + andalso (case outs of + NONE => true + | SOME outs => Cc.builtFrom (cc, {Derived = Var 0, + Base = outs}))) handle Cc.Contradiction => false end handle Cc.Undetermined => false) orelse onFail () @@ -1218,6 +1220,24 @@ (wrap (follow (follow select from) (opt wher)) (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) +datatype dml = + Insert of string * (string * sqexp) list + +val insert = log "insert" + (wrapP (follow (const "INSERT INTO ") + (follow uw_ident + (follow (const " (") + (follow (list uw_ident) + (follow (const ") VALUES (") + (follow (list sqexp) + (const ")"))))))) + (fn ((), (tab, ((), (fs, ((), (es, ())))))) => + (SOME (Insert (tab, ListPair.zipEq (fs, es)))) + handle ListPair.UnequalLengths => NONE)) + +val dml = log "dml" + insert + fun removeDups (ls : (string * string) list) = case ls of [] => [] @@ -1235,7 +1255,66 @@ SomeCol | AllCols of exp -exception Default +fun expIn rv env rvOf = + let + fun expIn (e, rvN) = + let + fun default () = + let + val (rvN, e) = rv rvN + in + (inl e, rvN) + end + in + case e of + SqConst p => (inl (Const p), rvN) + | Field (v, f) => (inl (Proj (rvOf v, f)), rvN) + | Binop (bo, e1, e2) => + let + val (e1, rvN) = expIn (e1, rvN) + val (e2, rvN) = expIn (e2, rvN) + in + (inr (case (bo, e1, e2) of + (Exps f, inl e1, inl e2) => f (e1, e2) + | (Props f, inr p1, inr p2) => f (p1, p2) + | _ => Unknown), rvN) + end + | SqKnown e => + (case expIn (e, rvN) of + (inl e, rvN) => (inr (Reln (Known, [e])), rvN) + | _ => (inr Unknown, rvN)) + | Inj e => + let + fun deinj e = + case #1 e of + ERel n => (List.nth (env, n), rvN) + | EField (e, f) => + let + val (e, rvN) = deinj e + in + (Proj (e, f), rvN) + end + | _ => + let + val (rvN, e) = rv rvN + in + (e, rvN) + end + + val (e, rvN) = deinj e + in + (inl e, rvN) + end + | SqFunc (f, e) => + (case expIn (e, rvN) of + (inl e, rvN) => (inl (Func (Other f, [e])), rvN) + | _ => default ()) + + | Count => default () + end + in + expIn + end fun queryProp env rvN rv oe e = let @@ -1272,68 +1351,56 @@ val p = foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r) - fun expIn e = - case e of - SqConst p => inl (Const p) - | Field (v, f) => inl (Proj (rvOf v, f)) - | Binop (bo, e1, e2) => - inr (case (bo, expIn e1, expIn e2) of - (Exps f, inl e1, inl e2) => f (e1, e2) - | (Props f, inr p1, inr p2) => f (p1, p2) - | _ => Unknown) - | SqKnown e => - inr (case expIn e of - inl e => Reln (Known, [e]) - | _ => Unknown) - | Inj e => - let - fun deinj (e, _) = - case e of - ERel n => List.nth (env, n) - | EField (e, f) => Proj (deinj e, f) - | _ => raise Fail "Iflow: non-variable injected into query" - in - inl (deinj e) - end - | SqFunc (f, e) => - inl (case expIn e of - inl e => Func (Other f, [e]) - | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f)) - | Count => raise Default + val expIn = expIn rv env rvOf - val p = case #Where r of - NONE => p - | SOME e => - case expIn e of - inr p' => And (p, p') - | _ => p + val (p, rvN) = case #Where r of + NONE => (p, rvN) + | SOME e => + case expIn (e, rvN) of + (inr p', rvN) => (And (p, p'), rvN) + | _ => (p, rvN) fun normal () = case oe of SomeCol => - (rvN, p, True, - List.mapPartial (fn si => - case si of - SqField (v, f) => SOME (Proj (rvOf v, f)) - | SqExp (e, f) => - case expIn e of - inr _ => NONE - | inl e => SOME e) (#Select r)) + let + val (sis, rvN) = + ListUtil.foldlMap + (fn (si, rvN) => + case si of + SqField (v, f) => (Proj (rvOf v, f), rvN) + | SqExp (e, f) => + case expIn (e, rvN) of + (inr _, _) => + let + val (rvN, e) = rv rvN + in + (e, rvN) + end + | (inl e, rvN) => (e, rvN)) rvN (#Select r) + in + (rvN, p, True, sis) + end | AllCols oe => - (rvN, And (p, foldl (fn (si, p) => - let - val p' = case si of - SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f), - Proj (rvOf v, f)]) - | SqExp (e, f) => - case expIn e of - inr p => Cond (Proj (oe, f), p) - | inl e => Reln (Eq, [Proj (oe, f), e]) - in - And (p, p') - end) - True (#Select r)), - True, []) + let + val (p', rvN) = + foldl (fn (si, (p, rvN)) => + let + val (p', rvN) = + case si of + SqField (v, f) => (Reln (Eq, [Proj (Proj (oe, v), f), + Proj (rvOf v, f)]), rvN) + | SqExp (e, f) => + case expIn (e, rvN) of + (inr p, rvN) => (Cond (Proj (oe, f), p), rvN) + | (inl e, rvN) => (Reln (Eq, [Proj (oe, f), e]), rvN) + in + (And (p, p'), rvN) + end) + (True, rvN) (#Select r) + in + (rvN, And (p, p'), True, []) + end val (rvN, p, wp, outs) = case #Select r of @@ -1370,7 +1437,50 @@ NONE => [] | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e), outs) end - handle Default => default () + end + +fun insertProp 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 + 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, _) = @@ -1428,6 +1538,7 @@ datatype cflow = Case | Where datatype flow = Data | Control of cflow type check = ErrorMsg.span * exp * prop +type insert = ErrorMsg.span * prop structure St :> sig type t @@ -1449,57 +1560,77 @@ val sent : t -> (check * flow) list val addSent : t * (check * flow) -> t val setSent : t * (check * flow) list -> t + + val inserted : t -> insert list + val addInsert : t * insert -> t end = struct type t = {Var : int, Ambient : prop, Path : (check * cflow) list, - Sent : (check * flow) list} + Sent : (check * flow) list, + Insert : insert list} fun create {Var = v, Ambient = p} = {Var = v, Ambient = p, Path = [], - Sent = []} + Sent = [], + Insert = []} fun curVar (t : t) = #Var t fun nextVar (t : t) = ({Var = #Var t + 1, Ambient = #Ambient t, Path = #Path t, - Sent = #Sent t}, #Var t) + Sent = #Sent t, + Insert = #Insert 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} + Sent = #Sent t, + Insert = #Insert 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} + Sent = #Sent t, + Insert = #Insert t} fun addPaths (t : t, cs) = {Var = #Var t, Ambient = #Ambient t, Path = cs @ #Path t, - Sent = #Sent t} + Sent = #Sent t, + Insert = #Insert t} fun clearPaths (t : t) = {Var = #Var t, Ambient = #Ambient t, Path = [], - Sent = #Sent t} + Sent = #Sent t, + Insert = #Insert t} fun setPaths (t : t, cs) = {Var = #Var t, Ambient = #Ambient t, Path = cs, - Sent = #Sent t} + Sent = #Sent t, + Insert = #Insert 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} + Sent = c :: #Sent t, + Insert = #Insert t} fun setSent (t : t, cs) = {Var = #Var t, Ambient = #Ambient t, Path = #Path t, - Sent = cs} + Sent = cs, + Insert = #Insert 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} end @@ -1720,7 +1851,44 @@ in (res, St.addPaths (St.setSent (st, sent), paths)) end - | EDml _ => default () + | EDml e => + (case parse dml e of + NONE => (print ("Warning: Information flow checker can't parse DML command at " + ^ ErrorMsg.spanToString loc ^ "\n"); + default ()) + | SOME d => + case d of + Insert (tab, es) => + let + val (st, new) = St.nextVar st + + fun rv st = + let + val (st, n) = St.nextVar st + in + (st, Var n) + end + + val expIn = expIn rv env (fn "New" => Var new + | _ => raise Fail "Iflow.evalExp: Bad field expression in EDml") + + val (es, 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 es + in + (Recd [], St.addInsert (st, (loc, And (St.ambient st, + Reln (Sql "$New", [Recd es]))))) + end) + | ENextval _ => default () | ESetval _ => default () @@ -1756,7 +1924,7 @@ DExport (_, _, n, _, _, _) => IS.add (exptd, n) | _ => exptd) IS.empty file - fun decl ((d, _), (vals, pols)) = + fun decl ((d, _), (vals, inserts, client, insert)) = case d of DVal (_, n, _, e, _) => let @@ -1776,21 +1944,36 @@ val (_, st) = evalExp env (e, St.create {Var = nv, Ambient = p}) in - (St.sent st @ vals, pols) + (St.sent st @ vals, St.inserted st @ inserts, client, insert) end - | DPolicy (PolClient e) => + | DPolicy pol => let - val (_, p, _, _, outs) = queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN)) SomeCol e + fun rv rvN = (rvN + 1, Lvar rvN) in - (vals, (p, outs) :: pols) + case pol of + PolClient e => + let + val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e + in + (vals, inserts, (p, outs) :: client, insert) + end + | PolInsert e => + let + val p = insertProp 0 rv e + in + (vals, inserts,client, p :: insert) + end end - | _ => (vals, pols) + | _ => (vals, inserts, client, insert) val () = reset () - val (vals, pols) = foldl decl ([], []) file + val (vals, inserts, client, insert) = foldl decl ([], [], [], []) file + + val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ()) + val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ()) in app (fn ((loc, e, p), fl) => let @@ -1798,14 +1981,14 @@ let val p = And (p, Reln (Eq, [Var 0, e])) in - if decomp true (fn (e1, e2) => e1 andalso e2 ()) p - (fn hyps => - (fl <> Control Where - andalso imply (hyps, [AReln (Known, [Var 0])], [Var 0])) - orelse List.exists (fn (p', outs) => - decomp false (fn (e1, e2) => e1 orelse e2 ()) p' - (fn goals => imply (hyps, goals, outs))) - pols) then + if decompH p + (fn hyps => + (fl <> Control Where + andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) + orelse List.exists (fn (p', outs) => + decompG p' + (fn goals => imply (hyps, goals, SOME outs))) + client) then () else (ErrorMsg.errorAt loc "The information flow policy may be violated here."; @@ -1824,7 +2007,19 @@ | Finish => () in doAll e - end) vals + 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 end val check = fn file =>
--- a/src/mono.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/mono.sml Sun Apr 11 10:57:52 2010 -0400 @@ -123,7 +123,9 @@ withtype exp = exp' located -datatype policy = PolClient of exp +datatype policy = + PolClient of exp + | PolInsert of exp datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list
--- a/src/mono_print.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/mono_print.sml Sun Apr 11 10:57:52 2010 -0400 @@ -417,6 +417,9 @@ PolClient e => box [string "sendClient", space, p_exp env e] + | PolInsert e => box [string "mayInsert", + space, + p_exp env e] fun p_decl env (dAll as (d, _) : decl) = case d of
--- a/src/mono_shake.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/mono_shake.sml Sun Apr 11 10:57:52 2010 -0400 @@ -62,6 +62,7 @@ let val e1 = case pol of PolClient e1 => e1 + | PolInsert e1 => e1 in usedVars st e1 end
--- a/src/mono_util.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/mono_util.sml Sun Apr 11 10:57:52 2010 -0400 @@ -544,6 +544,9 @@ PolClient e => S.map2 (mfe ctx e, PolClient) + | PolInsert e => + S.map2 (mfe ctx e, + PolInsert) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t,
--- a/src/monoize.sml Sat Apr 10 13:12:42 2010 -0400 +++ b/src/monoize.sml Sun Apr 11 10:57:52 2010 -0400 @@ -3746,6 +3746,8 @@ case #1 e of L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sendClient"), _), _), _), _), _), e) => (e, L'.PolClient) + | L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayInsert"), _), _), _), _), _), e) => + (e, L'.PolInsert) | _ => (poly (); (e, L'.PolClient)) val (e, fm) = monoExp (env, St.empty, fm) e