Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1221:00e628854005

Delete policies

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 11 Apr 2010 12:38:21 -0400
parents	526575a9537a
children	117f13bdc1fd

comparison

equal deleted inserted replaced

-:526575a9537a
+:00e628854005
 and variety =
 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
 type representative = node ref
 fun p_rep n =
 case !(#Rep (unNode n)) of
 SOME n => p_rep n
 | NONE =>
-case #Variety (unNode n) of
+box [string (Int.toString (Unsafe.cast n) ^ ":"),
-Nothing => string ("?" ^ Int.toString (Unsafe.cast n))
+space,
-| Dt0 s => string ("Dt0(" ^ s ^ ")")
+case #Variety (unNode n) of
-| Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
+Nothing => string "?"
-space,
+| Dt0 s => string ("Dt0(" ^ s ^ ")")
-p_rep n,
+| Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
-string ")"]
+space,
-| Prim p => Prim.p_t p
+p_rep n,
-| Recrd (ref m) => box [string "{",
+string ")"]
-p_list (fn (x, n) => box [string x,
+| Prim p => Prim.p_t p
-space,
+| Recrd (ref m, b) => box [string "{",
-string "=",
+p_list (fn (x, n) => box [string x,
 space,
-p_rep n]) (SM.listItemsi m),
+string "=",
-string "}"]
+space,
-| VFinish => string "FINISH"
+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:",
 newline,
 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
 #Rep (unNode n) := SOME r;
 r
 end
 fun markKnown r =
-if !(#Known (unNode r)) then
+let
-()
+val r = repOf r
-else
+in
-(#Known (unNode r) := true;
+(*Print.preface ("markKnown", p_rep r);*)
-SM.app markKnown (!(#Cons (unNode r)));
+if !(#Known (unNode r)) then
-case #Variety (unNode r) of
+()(*TextIO.print "Already known\n"*)
-Dt1 (_, r) => markKnown r
+else
-| Recrd xes => SM.app markKnown (!xes)
+(#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
 fun rep e =
 case e of
 | NONE =>
 let
 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'
 end
 end
 let
 val cons = ref SM.empty
 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),
 Variety = Dt1 (f, r'),
 Known = #Known (unNode r)})
 let
 val xes = foldl SM.insert' SM.empty xes
 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));
 r'
 end
 | Proj (e, f) =>
 let
 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
 end)
 | Nothing =>
 let
 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'';
 r'
 end
 fun assert (db, a) =
 case a of
 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)
 in
 case #Variety (unNode r) of
 raise Contradiction
 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
 markEq (r1, r2)
 else
 raise Contradiction
-| (Recrd xes1, Recrd xes2) =>
+| (Recrd (xes1, _), Recrd (xes2, _)) =>
 let
 fun unif (xes1, xes2) =
 SM.appi (fn (x, r1) =>
 case SM.find (xes2, x) of
 NONE => ()
 fun check (db, a) =
 case a of
 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
 | _ => false)
 | (PCon1 f, [e]) =>
 List.exists (fn b => repOf b = d) bs
 orelse case #Variety (unNode d) of
 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
 in
 loop (representative (db, d))
 [] =>
 (let
 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
 else
 ((*Print.prefaces "Can't prove"
 (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
+| Delete of string * sqexp
 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))))
+(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
 [] => []
 | x :: ls =>
 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
 [oe])
 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", [])]),
+Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
-And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
+And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
 p)),
-Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
+oeEq (Func (DtCon0 "Basis.bool.True", [])),
 [])
 end)
 | _ => normal ())
 | _ => normal ()
 in
 NONE => p
 | SOME e =>
 case expIn (e, rvN) of
 (inr p', _) => And (p, p')
 | _ => p
+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
 end
 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
 val create : {Var : int,
 Ambient : prop} -> t
 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 inserted : t -> dml list
-val addInsert : t * insert -> t
+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
 fun evalExp env (e as (_, loc), st) =
 let
 in
 (st, Var n)
 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) =>
 let
 val (e, st) = case expIn (e, st) of
 end)
 st es
 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 ()
 | ESetval _ => default ()
 val exptd = foldl (fn ((d, _), exptd) =>
 case d of
 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
 val isExptd = IS.member (exptd, n)
 val (e, env, nv, p) = deAbs (e, [], 1, True)
 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 =>
 let
 fun rv rvN = (rvN + 1, Lvar rvN)
 case pol of
 PolClient e =>
 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
 fun doOne e =
 let
 | Finish => ()
 in
 doAll e
 end) vals;
-app (fn (loc, p) =>
+doDml (inserts, insert);
-if decompH p
+doDml (deletes, delete)
-(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 =>
 let
 val oldInline = Settings.getMonoInline ()

Mercurial > urweb

comparison src/iflow.sml @ 1221:00e628854005