Change query_policy to sendClient; all arguments passed to SQL predicates are variables

9 files changed, 162 insertions, 108 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 72970351..959a050d 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -800,9 +800,9 @@ val initialize : task_kind
 
 type sql_policy
 
-val query_policy : tables ::: {{Type}} -> exps ::: {Type}
-                   -> [tables ~ exps] => sql_query [] tables exps
-                   -> sql_policy
+val sendClient : tables ::: {{Type}} -> exps ::: {Type}
+                 -> [tables ~ exps] => sql_query [] tables exps
+                 -> sql_policy
 
 
 val debug : string -> transaction unit
diff --git a/src/iflow.sml b/src/iflow.sml
index 92181d87..e49700cf 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -412,6 +412,7 @@ structure Cc :> sig
     val assert : t * exp * exp -> t
     val query : t * exp * exp -> bool
     val allPeers : t * exp -> exp list
+    val p_t : t Print.printer
 end = struct
 
 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
@@ -440,50 +441,102 @@ fun allPeers (t, e) =
                                  end) t
     end
 
-fun assert (t, e1, e2) =
-    let
-        val r1 = lookup (t, e1)
-        val r2 = lookup (t, e2)
+open Print
 
-        fun doUn k (t', e1, e2) =
-            case e2 of
-                Func (f, [e]) =>
+val p_t = p_list (fn (e1, e2) => box [p_exp (simplify e1),
+                                      space,
+                                      PD.string "->",
+                                      space,
+                                      p_exp (simplify e2)])
+
+fun query (t, e1, e2) =
+    let
+        fun doUn e =
+            case e of
+                Func (f, [e1]) =>
                 if String.isPrefix "un" f then
                     let
-                        val f' = String.extract (f, 2, NONE)
+                        val s = String.extract (f, 2, NONE)
                     in
-                        foldl (fn (e', t') =>
-                                  case e' of
-                                      Func (f'', [e'']) =>
-                                      if f'' = f' then
-                                          (lookup (t', e1), k e'') :: t'
-                                      else
-                                          t'
-                                    | _ => t') t' (allPeers (t, e))
+                        case ListUtil.search (fn e =>
+                                                 case e of
+                                                     Func (f', [e']) =>
+                                                     if f' = s then
+                                                         SOME e'
+                                                     else
+                                                         NONE
+                                                   | _ => NONE) (allPeers (t, e1)) of
+                            NONE => e
+                          | SOME e => doUn e
                     end
                 else
-                    t'
-              | Proj (e2, f) => doUn (fn e' => k (Proj (e', f))) (t', e1, e2)
-              | _ => t'
+                    e
+              | _ => e
+
+        val e1' = doUn (lookup (t, doUn (simplify e1)))
+        val e2' = doUn (lookup (t, doUn (simplify e2)))
+    in
+        (*prefaces "CC query" [("e1", p_exp (simplify e1)),
+                             ("e2", p_exp (simplify e2)),
+                             ("e1'", p_exp (simplify e1')),
+                             ("e2'", p_exp (simplify e2')),
+                             ("t", p_t t)];*)
+        eq (e1', e2')
+    end
+
+fun assert (t, e1, e2) =
+    let
+        val r1 = lookup (t, e1)
+        val r2 = lookup (t, e2)
     in
         if eq (r1, r2) then
             t
         else
-            doUn (fn x => x) (doUn (fn x => x) ((r1, r2) :: t, e1, e2), e2, e1)
+            let
+                fun doUn (t, e1, e2) =
+                    case e1 of
+                        Func (f, [e]) => if String.isPrefix "un" f then
+                                             let
+                                                 val s = String.extract (f, 2, NONE)
+                                             in
+                                                 foldl (fn (e', t) =>
+                                                           case e' of
+                                                               Func (f', [e']) =>
+                                                               if f' = s then
+                                                                   assert (assert (t, e', e1), e', e2)
+                                                               else
+                                                                   t
+                                                             | _ => t) t (allPeers (t, e))
+                                             end
+                                         else
+                                             t
+                      | _ => t
+
+                fun doProj (t, e1, e2) =
+                    foldl (fn ((e1', e2'), t) =>
+                              let
+                                  fun doOne (e, t) =
+                                      case e of
+                                          Proj (e', f) =>
+                                          if query (t, e1, e') then
+                                              assert (t, e, Proj (e2, f))
+                                          else
+                                              t
+                                        | _ => t
+                              in
+                                  doOne (e1', doOne (e2', t))
+                              end) t t
+
+                val t = (r1, r2) :: t
+                val t = doUn (t, r1, r2)
+                val t = doUn (t, r2, r1)
+                val t = doProj (t, r1, r2)
+                val t = doProj (t, r2, r1)
+            in
+                t
+            end
     end
 
-open Print
-
-fun query (t, e1, e2) =
-    ((*prefaces "CC query" [("e1", p_exp (simplify e1)),
-                          ("e2", p_exp (simplify e2)),
-                          ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
-                                                            space,
-                                                            PD.string "->",
-                                                            space,
-                                                            p_exp (simplify e2)]) t)];*)
-     eq (lookup (t, e1), lookup (t, e2)))
-
 end
 
 fun rimp cc ((r1, es1), (r2, es2)) =
@@ -491,19 +544,7 @@ fun rimp cc ((r1, es1), (r2, es2)) =
         (Sql r1', Sql r2') =>
         r1' = r2' andalso
         (case (es1, es2) of
-             ([Recd xes1], [Recd xes2]) =>
-             let
-                 val saved = save ()
-             in
-                 if List.all (fn (f, e2) =>
-                                 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
-                                     NONE => true
-                                   | SOME e1 => eq (e1, e2)) xes2 then
-                     true
-                 else
-                     (restore saved;
-                      false)
-             end
+             ([e1], [e2]) => eq (e1, e2)
            | _ => false)
       | (Eq, Eq) =>
         (case (es1, es2) of
@@ -533,6 +574,9 @@ fun rimp cc ((r1, es1), (r2, es2)) =
                        | Func (f, [e]) => String.isPrefix "un" f andalso matches e
                        | _ => false
              in
+                 (*Print.prefaces "Checking peers" [("e2", p_exp e2),
+                                                  ("peers", Print.p_list p_exp (Cc.allPeers (cc, e2))),
+                                                  ("db", Cc.p_t cc)];*)
                  List.exists matches (Cc.allPeers (cc, e2))
              end
            | _ => false)
@@ -562,7 +606,8 @@ fun imply (p1, p2) =
                                                   let
                                                       fun hps hyps =
                                                           case hyps of
-                                                              [] => ((*Print.preface ("Fail", p_prop (Reln g));*)
+                                                              [] => ((*Print.prefaces "Fail" [("g", p_prop (Reln g)),
+                                                                                            ("db", Cc.p_t cc)];*)
                                                                      onFail ())
                                                             | ACond _ :: hyps => hps hyps
                                                             | AReln h :: hyps =>
@@ -925,13 +970,27 @@ datatype queryMode =
          SomeCol of exp
        | AllCols of exp
 
-fun queryProp env rv oe e =
+fun queryProp env rvN rv oe e =
     case parse query e of
         NONE => (print ("Warning: Information flow checker can't parse SQL query at "
                         ^ ErrorMsg.spanToString (#2 e) ^ "\n");
-                 (Unknown, []))
+                 (rvN, Var 0, Unknown, []))
       | SOME r =>
         let
+            val (rvN, count) = rv rvN
+
+            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.queryProp: Bad table variable"
+                  | SOME (_, e) => e
+
             fun usedFields e =
                 case e of
                     SqConst _ => []
@@ -942,26 +1001,13 @@ fun queryProp env rv oe e =
                   | SqFunc (_, e) => usedFields e
                   | Count => []
 
-            val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r)
-                                      @ (case #Where r of
-                                             NONE => []
-                                           | SOME e => usedFields e))
-
             val p =
-                foldl (fn ((t, v), p) =>
-                          And (p,
-                               Reln (Sql t,
-                                     [Recd (foldl (fn ((v', f), fs) =>
-                                                      if v' = v then
-                                                          (f, Proj (Proj (rv, v), f)) :: fs
-                                                      else
-                                                          fs) [] allUsed)])))
-                      True (#From r)
+                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 (Proj (rv, v), f))
+                  | 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)
@@ -985,7 +1031,7 @@ fun queryProp env rv oe e =
                     inl (case expIn e of
                          inl e => Func (f, [e])
                        | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
-                  | Count => inl (Proj (rv, "$COUNT"))
+                  | Count => inl count
 
             val p = case #Where r of
                         NONE => p
@@ -994,12 +1040,14 @@ fun queryProp env rv oe e =
                             inr p' => And (p, p')
                           | _ => p
         in
-            (And (p, case oe of
+            (rvN,
+             count,
+             And (p, case oe of
                          SomeCol oe =>
                          foldl (fn (si, p) =>
                                    let
                                        val p' = case si of
-                                                    SqField (v, f) => Reln (Eq, [oe, Proj (Proj (rv, v), f)])
+                                                    SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
                                                   | SqExp (e, f) =>
                                                     case expIn e of
                                                         inr _ => Unknown
@@ -1013,7 +1061,7 @@ fun queryProp env rv oe e =
                                    let
                                        val p' = case si of
                                                     SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
-                                                                                 Proj (Proj (rv, v), f)])
+                                                                                 Proj (rvOf v, f)])
                                                   | SqExp (e, f) =>
                                                     case expIn e of
                                                         inr p => Cond (Proj (oe, f), p)
@@ -1025,7 +1073,7 @@ fun queryProp env rv oe e =
              
              case #Where r of
                  NONE => []
-               | SOME e => map (fn (v, f) => Proj (Proj (rv, v), f)) (usedFields e))
+               | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
         end
 
 fun evalPat env e (pt, _) =
@@ -1118,7 +1166,7 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
                 let
                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
                 in
-                    (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
+                    (Recd [], (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
                 end
             else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
                 default ()
@@ -1213,7 +1261,7 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
             let
                 val (e, st) = evalExp env (e, st)
             in
-                (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
+                (Recd [], (#1 st, p, addSent (#2 st, e, sent)))
             end
           | ESeq (e1, e2) =>
             let
@@ -1240,13 +1288,15 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
                 val (i, st) = evalExp env (i, st)
 
                 val r = #1 st
-                val rv = #1 st + 1
-                val acc = #1 st + 2
-                val st' = (#1 st + 3, #2 st, #3 st)
+                val acc = #1 st + 1
+                val st' = (#1 st + 2, #2 st, #3 st)
 
                 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
 
-                val (qp, used) = queryProp env (Var rv) (AllCols (Var r)) q
+                val (rvN, count, qp, used) =
+                    queryProp env
+                              (#1 st') (fn rvN => (rvN + 1, Var rvN))
+                              (AllCols (Var r)) q
 
                 val p' = And (qp, #2 st')
 
@@ -1254,11 +1304,11 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
                                         (#1 st + 1, #2 st, Var r)
                                     else
                                         let
-                                            val out = #1 st'
+                                            val out = rvN
 
                                             val p = Or (Reln (Eq, [Var out, i]),
                                                         And (Reln (Eq, [Var out, b]),
-                                                             And (Reln (Gt, [Proj (Var rv, "$COUNT"),
+                                                             And (Reln (Gt, [count,
                                                                              Const (Prim.Int 0)]),
                                                                   p')))
                                         in
@@ -1323,8 +1373,9 @@ fun check file =
                     (sent @ vals, pols)
                 end
 
-              | DPolicy (PolQuery e) => (vals, #1 (queryProp [] (Lvar 0) (SomeCol (Var 0)) e) :: pols)
-
+              | DPolicy (PolClient e) => (vals, #3 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
+                                                              (SomeCol (Var 0)) e) :: pols)
+                                        
               | _ => (vals, pols)
 
         val () = reset ()
diff --git a/src/mono.sml b/src/mono.sml
index 33ab5bd4..f8f57ae7 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -123,7 +123,7 @@ datatype exp' =
 
 withtype exp = exp' located
 
-datatype policy = PolQuery of exp
+datatype policy = PolClient of exp
 
 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 50c4717a..76a89cc7 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -414,9 +414,9 @@ fun p_datatype env (x, n, cons) =
 
 fun p_policy env pol =
     case pol of
-        PolQuery e => box [string "query",
-                           space,
-                           p_exp env e]
+        PolClient e => box [string "sendClient",
+                            space,
+                            p_exp env e]
 
 fun p_decl env (dAll as (d, _) : decl) =
     case d of
diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml
index e5dd3213..bb23a21a 100644
--- a/src/mono_reduce.sml
+++ b/src/mono_reduce.sml
@@ -423,18 +423,21 @@ fun reduce file =
                       | ERecord xets => List.concat (map (summarize d o #2) xets)
                       | EField (e, _) => summarize d e
 
-                      | ECase (e, pes, _) => summarize d e @ [Unsure]
-                        (*let
+                      | ECase (e, pes, _) =>
+                        let
                             val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
                         in
                             case lss of
                                 [] => raise Fail "Empty pattern match"
                               | ls :: lss =>
-                                if List.all (fn ls' => ls' = ls) lss then
-                                    summarize d e @ ls
-                                else
-                                    [Unsure]
-                        end*)
+                                summarize d e
+                                @ (if List.all (fn ls' => ls' = ls) lss then
+                                       ls
+                                   else if length (List.filter (not o List.null) (ls :: lss)) <= 1 then
+                                       valOf (List.find (not o List.null) (ls :: lss))
+                                   else
+                                       [Unsure])
+                        end
                       | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
 
                       | EError (e, _) => summarize d e @ [Unsure]
diff --git a/src/mono_shake.sml b/src/mono_shake.sml
index 358b31d2..3a681302 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -61,7 +61,7 @@ fun shake file =
                   | ((DPolicy pol, _), st) =>
                     let
                         val e1 = case pol of
-                                     PolQuery e1 => e1
+                                     PolClient e1 => e1
                     in
                         usedVars st e1
                     end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 094f216b..a7f27fd8 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -541,9 +541,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
 
         and mfpol ctx pol =
             case pol of
-                PolQuery e =>
+                PolClient e =>
                 S.map2 (mfe ctx e,
-                        PolQuery)
+                        PolClient)
 
         and mfvi ctx (x, n, t, e, s) =
             S.bind2 (mft t,
diff --git a/src/monoize.sml b/src/monoize.sml
index 073c26de..a4e6a37c 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3744,9 +3744,9 @@ fun monoDecl (env, fm) (all as (d, loc)) =
             let
                 val (e, make) =
                     case #1 e of
-                        L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "query_policy"), _), _), _), _), _), e) =>
-                        (e, L'.PolQuery)
-                      | _ => (poly (); (e, L'.PolQuery))
+                        L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sendClient"), _), _), _), _), _), e) =>
+                        (e, L'.PolClient)
+                      | _ => (poly (); (e, L'.PolClient))
 
                 val (e, fm) = monoExp (env, St.empty, fm) e
             in
diff --git a/tests/policy.ur b/tests/policy.ur
index 40850393..6d4e341e 100644
--- a/tests/policy.ur
+++ b/tests/policy.ur
@@ -9,18 +9,18 @@ table order : { Id : order, Fruit : fruit, Qty : int, Code : int }
   CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id)
 
 (* Everyone may knows IDs and names. *)
-policy query_policy (SELECT fruit.Id, fruit.Nam
-                     FROM fruit)
+policy sendClient (SELECT fruit.Id, fruit.Nam
+                   FROM fruit)
 
 (* The weight is sensitive information; you must know the secret. *)
-policy query_policy (SELECT fruit.Weight, fruit.Secret
-                     FROM fruit
-                     WHERE known(fruit.Secret))
-
-policy query_policy (SELECT order.Id, order.Fruit, order.Qty
-                     FROM order, fruit
-                     WHERE order.Fruit = fruit.Id
-                       AND order.Qty = 13)
+policy sendClient (SELECT fruit.Weight, fruit.Secret
+                   FROM fruit
+                   WHERE known(fruit.Secret))
+
+policy sendClient (SELECT order.Id, order.Fruit, order.Qty
+                   FROM order, fruit
+                   WHERE order.Fruit = fruit.Id
+                     AND order.Qty = 13)
 
 fun fname r =
     x <- queryX (SELECT fruit.Weight