summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/basis.urs3
-rw-r--r--src/iflow.sml85
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_print.sml5
-rw-r--r--src/mono_shake.sml1
-rw-r--r--src/mono_util.sml3
-rw-r--r--src/monoize.sml9
-rw-r--r--tests/equalKnown.ur24
-rw-r--r--tests/equalKnown.urp1
-rw-r--r--tests/equalKnown.urs1
10 files changed, 115 insertions, 18 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index f6141bc7..7b17dd05 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -819,6 +819,9 @@ val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
=> 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 --git a/src/iflow.sml b/src/iflow.sml
index 92e568a1..bf75775b 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1228,6 +1228,9 @@ structure St :> sig
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 @@ val deletable = ref ([] : atom list list)
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 @@ type 'a doQuery = {
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 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
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 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
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 @@ fun evalExp env (e as (_, loc)) k =
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 @@ fun check file =
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 @@ fun check file =
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 --git a/src/mono.sml b/src/mono.sml
index 9a960cd0..2f5ab117 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -129,6 +129,7 @@ datatype policy =
| 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 --git a/src/mono_print.sml b/src/mono_print.sml
index 25a8e9d8..693b5e3e 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -429,6 +429,11 @@ fun p_policy env pol =
| 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 --git a/src/mono_shake.sml b/src/mono_shake.sml
index 50c4b387..6a5aefae 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -67,6 +67,7 @@ fun shake file =
| PolDelete e1 => e1
| PolUpdate e1 => e1
| PolSequence e1 => e1
+ | PolEqualKnown {table = e1, ...} => e1
in
usedVars st e1
end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 6bbbecb1..cb01a958 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -556,6 +556,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
| 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 --git a/src/monoize.sml b/src/monoize.sml
index d43002cb..5054cc9f 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3804,6 +3804,15 @@ fun monoDecl (env, fm) (all as (d, loc)) =
(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 --git a/tests/equalKnown.ur b/tests/equalKnown.ur
new file mode 100644
index 00000000..4af32490
--- /dev/null
+++ b/tests/equalKnown.ur
@@ -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 => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}, {[x.Fruit.Weight]}</li></xml>);
+
+ return <xml><body>
+ <ul>{x1}</ul>
+ </body></xml>
diff --git a/tests/equalKnown.urp b/tests/equalKnown.urp
new file mode 100644
index 00000000..380321fd
--- /dev/null
+++ b/tests/equalKnown.urp
@@ -0,0 +1 @@
+equalKnown
diff --git a/tests/equalKnown.urs b/tests/equalKnown.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/equalKnown.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-10 08:00:11 +0000