# HG changeset patch # User Adam Chlipala # Date 1280245350 14400 # Node ID 3d06e0f7a6f33f0872e15f729666e87a3ecaf383 # Parent 4c367c8f5b2db28b799797612639b348523e673d Initial version of equalKnown working for secret diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 lib/ur/basis.urs --- a/lib/ur/basis.urs Sun Jun 13 14:13:47 2010 -0400 +++ b/lib/ur/basis.urs Tue Jul 27 11:42:30 2010 -0400 @@ -819,6 +819,9 @@ => sql_query [] ([Old = fs, New = fs] ++ tables) [] -> sql_policy +val equalKnown : nm :: Name -> t ::: Type -> fs ::: {Type} -> ks ::: {{Unit}} + -> [[nm] ~ fs] => sql_table ([nm = t] ++ fs) ks -> sql_policy + val also : sql_policy -> sql_policy -> sql_policy val debug : string -> transaction unit diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/iflow.sml --- a/src/iflow.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/iflow.sml Tue Jul 27 11:42:30 2010 -0400 @@ -1228,6 +1228,9 @@ val allowSend : atom list * exp list -> unit val send : check -> unit + val allowEqualKnown : { table : string, field : string } -> unit + val mayTest : prop -> bool + val allowInsert : atom list -> unit val insert : ErrorMsg.span -> unit @@ -1506,11 +1509,40 @@ fun allowDelete v = deletable := v :: !deletable val delete = doable deletable +val testable = ref ([] : { table : string, field : string } list) +fun allowEqualKnown v = testable := v :: !testable +fun mayTest p = + case p of + Reln (Eq, [e1, e2]) => + let + val (_, hs, _) = !hyps + + fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x + | _ => false) hs + + fun allowed (tab, v) = + case tab of + Proj (Var tab, fd) => + List.exists (fn {table = tab', field = fd'} => + fd' = fd + andalso tableInHyps (tab', tab)) (!testable) + andalso Cc.check (db, AReln (Known, [v])) + | _ => false + in + if allowed (e1, e2) orelse allowed (e2, e1) then + (Cc.assert (db, AReln (Eq, [e1, e2])); + true) + else + false + end + | _ => false + fun reset () = (Cc.clear db; path := []; hyps := (0, [], ref false); nvar := 0; sendable := []; + testable := []; insertable := []; updatable := []; deletable := []) @@ -1660,7 +1692,8 @@ Add : atom -> unit, Save : unit -> 'a, Restore : 'a -> unit, - Cont : queryMode + Cont : queryMode, + Send : exp -> unit } fun doQuery (arg : 'a doQuery) (e as (_, loc)) = @@ -1699,24 +1732,24 @@ val saved = #Save arg () fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) - fun usedFields e = + fun leavesE e = case e of - SqConst _ => [] - | SqTrue => [] - | SqFalse => [] - | Null => [] - | SqNot e => usedFields e - | Field (v, f) => [(false, Proj (rvOf v, f))] - | Computed _ => [] - | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 - | SqKnown _ => [] - | Inj e => - (case deinj (#Env arg) e of - NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated"; - []) - | SOME e => [(true, e)]) - | SqFunc (_, e) => usedFields e - | Unmodeled => [] + Const _ => [] + | Var _ => [] + | Lvar _ => [] + | Func (_, es) => List.concat (map leavesE es) + | Recd xes => List.concat (map (leavesE o #2) xes) + | Proj _ => [e] + + fun leavesP p = + case p of + True => [] + | False => [] + | Unknown => [] + | And (p1, p2) => leavesP p1 @ leavesP p2 + | Or (p1, p2) => leavesP p1 @ leavesP p2 + | Reln (_, es) => List.concat (map leavesE es) + | Cond (e, p) => e :: leavesP p fun normal' () = case #Cont arg of @@ -1769,8 +1802,17 @@ inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) | inr p => p + fun getConjuncts p = + case p of + And (p1, p2) => getConjuncts p1 @ getConjuncts p2 + | _ => [p] + val saved = #Save arg () + + val conjs = getConjuncts p + val conjs = List.filter (not o St.mayTest) conjs in + app (fn p => app (#Send arg) (leavesP p)) conjs; decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} p (fn () => final () handle Cc.Contradiction => ()); #Restore arg saved @@ -2076,6 +2118,7 @@ Add = fn a => St.assert [a], Save = St.stash, Restore = St.reinstate, + Send = fn e => St.send (e, loc), Cont = AllCols (fn x => (St.assert [AReln (Eq, [r, x])]; evalExp (acc :: r :: env) b k))} q @@ -2448,6 +2491,7 @@ Add = fn a => atoms := a :: !atoms, Save = fn () => !atoms, Restore = fn ls => atoms := ls, + Send = fn _ => (), Cont = SomeCol (fn r => k (rev (!atoms), r))} fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) => @@ -2483,6 +2527,11 @@ St.allowSend ([p], outs) end | _ => ()) + | PolEqualKnown {table = tab, field = nm} => + (case #1 tab of + EPrim (Prim.String tab) => St.allowEqualKnown {table = String.extract (tab, 3, NONE), + field = nm} + | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.") end | _ => () diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/mono.sml --- a/src/mono.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/mono.sml Tue Jul 27 11:42:30 2010 -0400 @@ -129,6 +129,7 @@ | PolDelete of exp | PolUpdate of exp | PolSequence of exp + | PolEqualKnown of {table : exp, field : string} datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/mono_print.sml --- a/src/mono_print.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/mono_print.sml Tue Jul 27 11:42:30 2010 -0400 @@ -429,6 +429,11 @@ | PolSequence e => box [string "sendOwnIds", space, p_exp env e] + | PolEqualKnown {table = tab, field = nm} => box [string "equalKnown[", + string nm, + string "]", + space, + p_exp env tab] fun p_decl env (dAll as (d, _) : decl) = case d of diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/mono_shake.sml --- a/src/mono_shake.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/mono_shake.sml Tue Jul 27 11:42:30 2010 -0400 @@ -67,6 +67,7 @@ | PolDelete e1 => e1 | PolUpdate e1 => e1 | PolSequence e1 => e1 + | PolEqualKnown {table = e1, ...} => e1 in usedVars st e1 end diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/mono_util.sml --- a/src/mono_util.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/mono_util.sml Tue Jul 27 11:42:30 2010 -0400 @@ -556,6 +556,9 @@ | PolSequence e => S.map2 (mfe ctx e, PolSequence) + | PolEqualKnown {table = tab, field = nm} => + S.map2 (mfe ctx tab, + fn tab => PolEqualKnown {table = tab, field = nm}) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t, diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 src/monoize.sml --- a/src/monoize.sml Sun Jun 13 14:13:47 2010 -0400 +++ b/src/monoize.sml Tue Jul 27 11:42:30 2010 -0400 @@ -3804,6 +3804,15 @@ (e, L'.PolUpdate) | L.EFfiApp ("Basis", "sendOwnIds", [e]) => (e, L'.PolSequence) + | L.EApp ((L.ECApp + ((L.ECApp + ((L.ECApp + ((L.ECApp + ((L.EFfi ("Basis", "equalKnown"), _), nm), _), _), _), + _), _), _), _), tab) => + (case #1 nm of + L.CName nm => (tab, fn tab => L'.PolEqualKnown {table = tab, field = nm}) + | _ => (poly (); (e, L'.PolClient))) | _ => (poly (); (e, L'.PolClient)) val (e, fm) = monoExp (env, St.empty, fm) e diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 tests/equalKnown.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/equalKnown.ur Tue Jul 27 11:42:30 2010 -0400 @@ -0,0 +1,24 @@ +type fruit = int +table fruit : { Id : fruit, Nam : string, Weight : float, Secret : string } + PRIMARY KEY Id, + CONSTRAINT Nam UNIQUE Nam + +policy sendClient (SELECT fruit.Id, fruit.Nam + FROM fruit) + +policy sendClient (SELECT fruit.Weight + FROM fruit + WHERE known(fruit.Secret)) + +policy equalKnown[#Secret] fruit + +fun main () = + x1 <- queryX (SELECT fruit.Id, fruit.Nam, fruit.Weight + FROM fruit + WHERE fruit.Nam = "apple" + AND fruit.Secret = "tasty") + (fn x =>
  • {[x.Fruit.Id]}: {[x.Fruit.Nam]}, {[x.Fruit.Weight]}
    • ); + + return + + diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 tests/equalKnown.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/equalKnown.urp Tue Jul 27 11:42:30 2010 -0400 @@ -0,0 +1,1 @@ +equalKnown diff -r 4c367c8f5b2d -r 3d06e0f7a6f3 tests/equalKnown.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/equalKnown.urs Tue Jul 27 11:42:30 2010 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page