Parsing more comparison operators

3 files changed, 76 insertions, 31 deletions

diff --git a/src/iflow.sig b/src/iflow.sig
index bc481022..f85322ef 100644
--- a/src/iflow.sig
+++ b/src/iflow.sig
@@ -42,6 +42,11 @@ signature IFLOW = sig
              Known
            | Sql of string
            | Eq
+           | Ne
+           | Lt
+           | Le
+           | Gt
+           | Ge
 
     datatype prop =
              True
diff --git a/src/iflow.sml b/src/iflow.sml
index 58b38e6c..4dfa4e8d 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -68,6 +68,11 @@ datatype reln =
          Known
        | Sql of string
        | Eq
+       | Ne
+       | Lt
+       | Le
+       | Gt
+       | Ge
 
 datatype prop =
          True
@@ -92,7 +97,7 @@ fun p_exp e =
                              p_list p_exp es,
                              string ")"]
       | Recd xes => box [string "{",
-                         p_list (fn (x, e) => box [string "x",
+                         p_list (fn (x, e) => box [string x,
                                                    space,
                                                    string "=",
                                                    space,
@@ -102,6 +107,15 @@ fun p_exp e =
                             string ("." ^ x)]
       | Finish => string "FINISH"
 
+fun p_bop s es =
+    case es of
+        [e1, e2] => box [p_exp e1,
+                         space,
+                         string s,
+                         space,
+                         p_exp e2]
+      | _ => raise Fail "Iflow.p_bop"
+
 fun p_reln r es =
     case r of
         Known =>
@@ -113,14 +127,12 @@ fun p_reln r es =
       | Sql s => box [string (s ^ "("),
                       p_list p_exp es,
                       string ")"]
-      | Eq =>
-        (case es of
-             [e1, e2] => box [p_exp e1,
-                              space,
-                              string "=",
-                              space,
-                              p_exp e2]
-           | _ => raise Fail "Iflow.p_reln: Eq")
+      | Eq => p_bop "=" es
+      | Ne => p_bop "<>" es
+      | Lt => p_bop "<" es
+      | Le => p_bop "<=" es
+      | Gt => p_bop ">" es
+      | Ge => p_bop ">=" es
 
 fun p_prop p =
     case p of
@@ -660,8 +672,9 @@ val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
                                       String.extract (s, 2, NONE)
                                   else
                                       raise Fail "Iflow: Bad table variable")
-val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then
-                                       String.extract (s, 3, NONE)
+val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
+                                       str (Char.toUpper (String.sub (s, 3)))
+                                       ^ String.extract (s, 4, NONE)
                                    else
                                        raise Fail "Iflow: Bad uw_* variable")
 
@@ -681,7 +694,14 @@ datatype sqexp =
        | SqKnown of sqexp
        | Inj of Mono.exp
 
-val sqbrel = altL [wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))),
+fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
+
+val sqbrel = altL [cmp "=" Eq,
+                   cmp "<>" Ne,
+                   cmp "<=" Le,
+                   cmp "<" Lt,
+                   cmp ">=" Ge,
+                   cmp ">" Gt,
                    wrap (const "AND") (fn () => Props And),
                    wrap (const "OR") (fn () => Props Or)]
 
@@ -788,7 +808,7 @@ fun queryProp env 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)
+                 (Unknown, []))
       | SOME r =>
         let
             val p =
@@ -826,6 +846,14 @@ fun queryProp env rv oe e =
                         inl (deinj e)
                     end
 
+            fun usedFields e =
+                case e of
+                    SqConst _ => []
+                  | Field (v, f) => [Proj (Proj (Lvar rv, v), f)]
+                  | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
+                  | SqKnown _ => []
+                  | Inj _ => []
+
             val p = case #Where r of
                         NONE => p
                       | SOME e =>
@@ -833,13 +861,17 @@ fun queryProp env rv oe e =
                             inr p' => And (p, p')
                           | _ => p
         in
-            case oe of
-                NONE => p
-              | SOME oe =>
-                And (p, foldl (fn ((v, f), p) =>
-                                  Or (p,
-                                      Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
-                              False (#Select r))
+            (case oe of
+                 NONE => p
+               | SOME oe =>
+                 And (p, foldl (fn ((v, f), p) =>
+                                   Or (p,
+                                       Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
+                               False (#Select r)),
+             
+             case #Where r of
+                 NONE => []
+               | SOME e => usedFields e)
         end
 
 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
@@ -979,18 +1011,21 @@ fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
 
                 val r' = newLvar ()
                 val acc' = newLvar ()
-                val qp = queryProp env r' NONE q
+                val (qp, used) = queryProp env r' NONE q
 
                 val doSubExp = subExp (r, r') o subExp (acc, acc')
                 val doSubProp = subProp (r, r') o subProp (acc, acc')
 
                 val p = doSubProp (#2 st')
-                val p = And (p, qp)
-                val p = Select (r, r', acc', p, doSubExp b)
+                val p' = And (p, qp)
+                val p = Select (r, r', acc', p', doSubExp b)
+
+                val sent = map (fn (loc, e, p) => (loc,
+                                                   doSubExp e,
+                                                   And (qp, doSubProp p))) (#3 st')
+                val sent = map (fn e => (loc, e, p')) used @ sent
             in
-                (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc,
-                                                                            doSubExp e,
-                                                                            And (qp, doSubProp p))) (#3 st')))
+                (Var r, (#1 st + 1, And (#2 st, p), sent))
             end
           | EDml _ => default ()
           | ENextval _ => default ()
@@ -1036,7 +1071,7 @@ fun check file =
                     (sent @ vals, pols)
                 end
 
-              | DPolicy (PolQuery e) => (vals, queryProp [] 0 (SOME (Var 0)) e :: pols)
+              | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols)
 
               | _ => (vals, pols)
 
diff --git a/tests/policy.ur b/tests/policy.ur
index 6f2d2d5b..40850393 100644
--- a/tests/policy.ur
+++ b/tests/policy.ur
@@ -13,7 +13,7 @@ policy query_policy (SELECT fruit.Id, fruit.Nam
                      FROM fruit)
 
 (* The weight is sensitive information; you must know the secret. *)
-policy query_policy (SELECT fruit.Weight
+policy query_policy (SELECT fruit.Weight, fruit.Secret
                      FROM fruit
                      WHERE known(fruit.Secret))
 
@@ -26,7 +26,12 @@ fun fname r =
     x <- queryX (SELECT fruit.Weight
                  FROM fruit
                  WHERE fruit.Nam = {[r.Nam]}
-                   AND fruit.Secret = {[r.Secret]})
+                   AND fruit.Secret = {[r.Secret]}
+                   AND fruit.Weight <> 3.14
+                   AND fruit.Weight < 100.0
+                   AND fruit.Weight <= 200.1
+                   AND fruit.Weight > 1.23
+                   AND fruit.Weight >= 1.24)
          (fn r => <xml>Weight is {[r.Fruit.Weight]}</xml>);
 
     return <xml><body>
@@ -36,8 +41,7 @@ fun fname r =
 fun main () =
     x1 <- queryX (SELECT fruit.Id, fruit.Nam
                   FROM fruit
-                  WHERE fruit.Nam = "apple"
-                    AND fruit.Weight = 1.23)
+                  WHERE fruit.Nam = "apple")
                  (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
 
     x2 <- queryX (SELECT fruit.Nam, order.Qty
@@ -48,6 +52,7 @@ fun main () =
 
     return <xml><body>
       <ul>{x1}</ul>
+
       <ul>{x2}</ul>
 
       <form>