# HG changeset patch # User Adam Chlipala # Date 1270569848 14400 # Node ID c5bd970e77a54ce895578356b1f5a19484b65288 # Parent 775357041e483f658c63117bb1afb83e244ec57e Parsing more comparison operators diff -r 775357041e48 -r c5bd970e77a5 src/iflow.sig --- a/src/iflow.sig Tue Apr 06 11:07:19 2010 -0400 +++ b/src/iflow.sig Tue Apr 06 12:04:08 2010 -0400 @@ -42,6 +42,11 @@ Known | Sql of string | Eq + | Ne + | Lt + | Le + | Gt + | Ge datatype prop = True diff -r 775357041e48 -r c5bd970e77a5 src/iflow.sml --- a/src/iflow.sml Tue Apr 06 11:07:19 2010 -0400 +++ b/src/iflow.sml Tue Apr 06 12:04:08 2010 -0400 @@ -68,6 +68,11 @@ Known | Sql of string | Eq + | Ne + | Lt + | Le + | Gt + | Ge datatype prop = True @@ -92,7 +97,7 @@ 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 @@ 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 @@ | 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 @@ 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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ (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 -r 775357041e48 -r c5bd970e77a5 tests/policy.ur --- a/tests/policy.ur Tue Apr 06 11:07:19 2010 -0400 +++ b/tests/policy.ur Tue Apr 06 12:04:08 2010 -0400 @@ -13,7 +13,7 @@ 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 @@ 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 => Weight is {[r.Fruit.Weight]}); return @@ -36,8 +41,7 @@ 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 =>
  • {[x.Fruit.Id]}: {[x.Fruit.Nam]}
    • ); x2 <- queryX (SELECT fruit.Nam, order.Qty @@ -48,6 +52,7 @@ return
      {x1}
    +
      {x2}