Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1247:0c643f51fbc0

Fix innappropriate removal of duplicate tables from DML policies

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 18 Apr 2010 15:54:37 -0400
parents	fd4028a594a9
children	cf9a636f9b15

comparison

equal deleted inserted replaced

-:fd4028a594a9
+:0c643f51fbc0
 (* Congruence closure *)
 structure Cc :> sig
 type database
 exception Contradiction
-exception Undetermined
 val database : unit -> database
 val clear : database -> unit
 val assert : database * atom -> unit
 case !(#Ge (unNode (repOf r1))) of
 NONE => #Ge (unNode (repOf r1)) := SOME n2
 | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
 end
 | _ => ()
-end
+end handle Undetermined => ()
 fun check (db, a) =
-case a of
+(case a of
 ACond _ => false
 | AReln x =>
 case x of
 (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]) =>
 (case #Variety (unNode (representative (db, e))) of
 Dt1 (f', _) => f' = f
 | _ => false)
 | (Eq, [e1, e2]) =>
 let
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 repOf r1 = repOf r2
 end
 | (Ge, [e1, e2]) =>
 let
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
 (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
 | _ => false
 end
-| _ => false
+| _ => false)
+handle Undetermined => false
 fun builtFrom (db, {UseKnown = uk, Base = bs, Derived = d}) =
 let
 val bs = map (fn b => representative (db, b)) bs
 case e of
 Func (Other _, es) => List.all decomp es
 | _ => loop (representative (db, e))
 in
 decomp d
-end
+end handle Undetermined => false
 end
 val tabs = ref (SM.empty : (string list * string list list) SM.map)
 let
 val changed = ref false
 fun findKeys (hyps, acc) =
 case hyps of
-[] => acc
+[] => rev acc
 | (a as AReln (Sql tab, [r1])) :: hyps =>
 (case SM.find (!tabs, tab) of
 NONE => findKeys (hyps, a :: acc)
 | SOME (_, []) => findKeys (hyps, a :: acc)
 | SOME (_, ks) =>
 let
 fun finder (hyps, acc) =
 case hyps of
-[] => acc
+[] => rev acc
 | (a as AReln (Sql tab', [r2])) :: hyps =>
 if tab' = tab andalso
 List.exists (List.all (fn f =>
 let
 val r =
 let
 val (_, hs, _) = !hyps
 in
 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
 Print.prefaces "Situation" [("User learns", p_exp e),
-("Hypotheses", Print.p_list p_atom hs),
+("Hypotheses", Print.p_list p_atom hs)(*,
-("E-graph", Cc.p_database db)]
+("E-graph", Cc.p_database db)*)]
 end
 end
 fun checkPaths () =
 let
 else
 let
 val (_, hs, _) = !hyps
 in
 ErrorMsg.errorAt loc "The database update policy may be violated here.";
-Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
+Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
-("E-graph", Cc.p_database db)*)]
+("E-graph", Cc.p_database db)]
 end
 end
 val insertable = ref ([] : atom list list)
 fun allowInsert v = insertable := v :: !insertable
 Save = fn () => !atoms,
 Restore = fn ls => atoms := ls,
 UsedExp = fn _ => (),
 Cont = SomeCol (fn r => k (rev (!atoms), r))}
-fun untab tab = List.filter (fn AReln (Sql tab', _) => tab' <> tab
+fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
-| _ => true)
+tab' <> tab
+orelse List.all (fn Lvar lv' => lv' <> lv
+| _ => false) nams
+| _ => true)
 in
 case pol of
 PolClient e =>
 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
 | PolInsert e =>
 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
-St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab tab ats)
+St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
 | _ => raise Fail "Iflow: No New in mayInsert policy") e
 | PolDelete e =>
 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
-St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab tab ats)
+St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
 | PolUpdate e =>
 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
 :: AReln (Sql (tab ^ "$New"), [new])
-:: untab tab ats)
+:: untab (tab, [new, old]) ats)
 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
 | PolSequence e =>
 (case #1 e of
 EPrim (Prim.String seq) =>
 let

Mercurial > urweb

comparison src/iflow.sml @ 1247:0c643f51fbc0