Mercurial > urweb
changeset 1199:c316ca3c9ec6
Pushing policies through
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 04 Apr 2010 12:29:34 -0400 |
| parents | 6d8e3dcb9713 |
| children | 5eac14322548 |
| files | lib/ur/basis.urs src/cjrize.sml src/core.sml src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/css.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/elisp/urweb-defs.el src/elisp/urweb-mode.el src/expl.sml src/expl_env.sml src/expl_print.sml src/explify.sml src/mono.sml src/mono_env.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml src/reduce.sml src/reduce_local.sml src/shake.sml src/source.sml src/source_print.sml src/unnest.sml src/urweb.grm src/urweb.lex tests/policy.ur tests/policy.urp |
| diffstat | 35 files changed, 145 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Thu Apr 01 17:23:17 2010 -0400 +++ b/lib/ur/basis.urs Sun Apr 04 12:29:34 2010 -0400 @@ -795,4 +795,13 @@ val initialize : task_kind +(** Information flow security *) + +type sql_policy + +val query_policy : tables ::: {{Type}} -> exps ::: {Type} + -> [tables ~ exps] => sql_query [] tables exps + -> sql_policy + + val debug : string -> transaction unit
--- a/src/cjrize.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/cjrize.sml Sun Apr 04 12:29:34 2010 -0400 @@ -674,6 +674,7 @@ end | _ => (ErrorMsg.errorAt loc "Initializer has not been fully determined"; (NONE, NONE, sm))) + | L.DPolicy _ => (NONE, NONE, sm) fun cjrize ds = let
--- a/src/core.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/core.sml Sun Apr 04 12:29:34 2010 -0400 @@ -135,6 +135,7 @@ | DCookie of string * int * con * string | DStyle of string * int * string | DTask of exp * exp + | DPolicy of exp withtype decl = decl' located
--- a/src/core_env.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/core_env.sml Sun Apr 04 12:29:34 2010 -0400 @@ -349,6 +349,7 @@ pushENamed env x n t NONE s end | DTask _ => env + | DPolicy _ => env fun patBinds env (p, loc) = case p of
--- a/src/core_print.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/core_print.sml Sun Apr 04 12:29:34 2010 -0400 @@ -618,6 +618,9 @@ string "=", space, p_exp env e2] + | DPolicy e1 => box [string "policy", + space, + p_exp env e1] fun p_file env file = let
--- a/src/core_util.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/core_util.sml Sun Apr 04 12:29:34 2010 -0400 @@ -992,6 +992,10 @@ S.map2 (mfe ctx e2, fn e2' => (DTask (e1', e2'), loc))) + | DPolicy e => + S.map2 (mfe ctx e, + fn e' => + (DPolicy e', loc)) and mfvi ctx (x, n, t, e, s) = S.bind2 (mfc ctx t, @@ -1147,6 +1151,7 @@ bind (ctx, NamedE (x, n, t, NONE, s)) end | DTask _ => ctx + | DPolicy _ => ctx in S.map2 (mff ctx' ds', fn ds' => @@ -1210,7 +1215,8 @@ | DDatabase _ => count | DCookie (_, n, _, _) => Int.max (n, count) | DStyle (_, n, _) => Int.max (n, count) - | DTask _ => count) 0 + | DTask _ => count + | DPolicy _ => count) 0 end
--- a/src/corify.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/corify.sml Sun Apr 04 12:29:34 2010 -0400 @@ -1080,6 +1080,9 @@ | L.DTask (e1, e2) => ([(L'.DTask (corifyExp st e1, corifyExp st e2), loc)], st) + | L.DPolicy e1 => + ([(L'.DPolicy (corifyExp st e1), loc)], st) + and corifyStr mods ((str, _), st) = case str of L.StrConst ds => @@ -1137,7 +1140,8 @@ | L.DDatabase _ => n | L.DCookie (_, _, n', _) => Int.max (n, n') | L.DStyle (_, _, n') => Int.max (n, n') - | L.DTask _ => n) + | L.DTask _ => n + | L.DPolicy _ => n) 0 ds and maxNameStr (str, _) =
--- a/src/css.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/css.sml Sun Apr 04 12:29:34 2010 -0400 @@ -287,6 +287,7 @@ | DCookie _ => st | DStyle (_, n, s) => (IM.insert (globals, n, (SOME s, [])), classes) | DTask _ => st + | DPolicy _ => st end val (globals, classes) = foldl decl (IM.empty, IM.empty) file
--- a/src/elab.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elab.sml Sun Apr 04 12:29:34 2010 -0400 @@ -171,6 +171,7 @@ | DCookie of int * string * int * con | DStyle of int * string * int | DTask of exp * exp + | DPolicy of exp and str' = StrConst of decl list
--- a/src/elab_env.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elab_env.sml Sun Apr 04 12:29:34 2010 -0400 @@ -1623,5 +1623,6 @@ pushENamedAs env x n t end | DTask _ => env + | DPolicy _ => env end
--- a/src/elab_print.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elab_print.sml Sun Apr 04 12:29:34 2010 -0400 @@ -806,6 +806,9 @@ string "=", space, p_exp env e2] + | DPolicy e1 => box [string "policy", + space, + p_exp env e1] and p_str env (str, _) = case str of
--- a/src/elab_util.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elab_util.sml Sun Apr 04 12:29:34 2010 -0400 @@ -854,7 +854,8 @@ c), loc))) | DStyle (tn, x, n) => bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc))) - | DTask _ => ctx, + | DTask _ => ctx + | DPolicy _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -985,6 +986,10 @@ S.map2 (mfe ctx e2, fn e2' => (DTask (e1', e2'), loc))) + | DPolicy e1 => + S.map2 (mfe ctx e1, + fn e1' => + (DPolicy e1', loc)) and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, @@ -1128,6 +1133,7 @@ | DCookie (n1, _, n2, _) => Int.max (n1, n2) | DStyle (n1, _, n2) => Int.max (n1, n2) | DTask _ => 0 + | DPolicy _ => 0 and maxNameStr (str, _) = case str of StrConst ds => maxName ds
--- a/src/elaborate.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elaborate.sml Sun Apr 04 12:29:34 2010 -0400 @@ -2595,6 +2595,7 @@ | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] | L'.DTask _ => [] + | L'.DPolicy _ => [] and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), @@ -3729,6 +3730,15 @@ checkCon env e2' t2 t2'; ([(L'.DTask (e1', e2'), loc)], (env, denv, gs2 @ gs1 @ gs)) end + | L.DPolicy e1 => + let + val (e1', t1, gs1) = elabExp (env, denv) e1 + + val t1' = (L'.CModProj (!basis_r, [], "sql_policy"), loc) + in + checkCon env e1' t1 t1'; + ([(L'.DPolicy e1', loc)], (env, denv, gs1 @ gs)) + end (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) in
--- a/src/elisp/urweb-defs.el Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elisp/urweb-defs.el Sun Apr 04 12:29:34 2010 -0400 @@ -108,7 +108,7 @@ "datatype" "type" "open" "include" urweb-module-head-syms "con" "map" "where" "extern" "constraint" "constraints" - "table" "sequence" "class" "cookie" "task") + "table" "sequence" "class" "cookie" "task" "policy") "Symbols starting an sexp.") ;; (defconst urweb-not-arg-start-re @@ -135,7 +135,7 @@ (("case" "datatype" "if" "then" "else" "let" "open" "sig" "struct" "type" "val" "con" "constraint" "table" "sequence" "class" "cookie" - "task"))))) + "task" "policy"))))) (defconst urweb-starters-indent-after (urweb-syms-re "let" "in" "struct" "sig") @@ -190,7 +190,7 @@ '("datatype" "fun" "open" "type" "val" "and" "con" "constraint" "table" "sequence" "class" "cookie" - "task")) + "task" "policy")) "The starters of new expressions.") (defconst urweb-exptrail-syms
--- a/src/elisp/urweb-mode.el Thu Apr 01 17:23:17 2010 -0400 +++ b/src/elisp/urweb-mode.el Sun Apr 04 12:29:34 2010 -0400 @@ -136,7 +136,7 @@ "datatype" "else" "end" "extern" "fn" "map" "fun" "functor" "if" "include" "of" "open" "let" "in" - "rec" "sequence" "sig" "signature" "cookie" "style" "task" + "rec" "sequence" "sig" "signature" "cookie" "style" "task" "policy" "struct" "structure" "table" "view" "then" "type" "val" "where" "with" @@ -226,7 +226,7 @@ ("\\<\\(\\(data\\)?type\\|con\\|class\\)\\s-+\\(\\sw+\\)" (1 font-lock-keyword-face) (3 (amAttribute font-lock-type-def-face))) - ("\\<\\(val\\|table\\|sequence\\|cookie\\|style\\|task\\)\\s-+\\(\\sw+\\>\\s-*\\)?\\(\\sw+\\)\\s-*[=:]" + ("\\<\\(val\\|table\\|sequence\\|cookie\\|style\\|task\\|policy\\)\\s-+\\(\\sw+\\>\\s-*\\)?\\(\\sw+\\)\\s-*[=:]" (1 font-lock-keyword-face) (3 (amAttribute font-lock-variable-name-face))) ("\\<\\(structure\\|functor\\)\\s-+\\(\\sw+\\)"
--- a/src/expl.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/expl.sml Sun Apr 04 12:29:34 2010 -0400 @@ -148,6 +148,7 @@ | DCookie of int * string * int * con | DStyle of int * string * int | DTask of exp * exp + | DPolicy of exp and str' = StrConst of decl list
--- a/src/expl_env.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/expl_env.sml Sun Apr 04 12:29:34 2010 -0400 @@ -344,6 +344,7 @@ pushENamed env x n t end | DTask _ => env + | DPolicy _ => env fun sgiBinds env (sgi, loc) = case sgi of
--- a/src/expl_print.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/expl_print.sml Sun Apr 04 12:29:34 2010 -0400 @@ -720,6 +720,9 @@ string "=", space, p_exp env e2] + | DPolicy e1 => box [string "policy", + space, + p_exp env e1] and p_str env (str, _) = case str of
--- a/src/explify.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/explify.sml Sun Apr 04 12:29:34 2010 -0400 @@ -196,6 +196,7 @@ | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc) | L.DStyle (nt, x, n) => SOME (L'.DStyle (nt, x, n), loc) | L.DTask (e1, e2) => SOME (L'.DTask (explifyExp e1, explifyExp e2), loc) + | L.DPolicy e1 => SOME (L'.DPolicy (explifyExp e1), loc) and explifyStr (str, loc) = case str of
--- a/src/mono.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/mono.sml Sun Apr 04 12:29:34 2010 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -123,6 +123,8 @@ withtype exp = exp' located +datatype policy = PolQuery of exp + datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list | DVal of string * int * typ * exp * string @@ -141,6 +143,8 @@ | DTask of exp * exp + | DPolicy of policy + withtype decl = decl' located type file = decl list
--- a/src/mono_env.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/mono_env.sml Sun Apr 04 12:29:34 2010 -0400 @@ -130,6 +130,7 @@ | DCookie _ => env | DStyle _ => env | DTask _ => env + | DPolicy _ => env fun patBinds env (p, loc) = case p of
--- a/src/mono_print.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/mono_print.sml Sun Apr 04 12:29:34 2010 -0400 @@ -412,6 +412,12 @@ cons] end +fun p_policy env pol = + case pol of + PolQuery e => box [string "query", + space, + p_exp env e] + fun p_decl env (dAll as (d, _) : decl) = case d of DDatatype x => box [string "datatype", @@ -506,6 +512,9 @@ string "=", space, p_exp env e2] + | DPolicy p => box [string "policy", + space, + p_policy env p] fun p_file env file =
--- a/src/mono_shake.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/mono_shake.sml Sun Apr 04 12:29:34 2010 -0400 @@ -58,6 +58,13 @@ | ((DDatabase {expunge = n1, initialize = n2, ...}, _), (page_cs, page_es)) => (page_cs, IS.addList (page_es, [n1, n2])) | ((DTask (e1, e2), _), st) => usedVars (usedVars st e2) e1 + | ((DPolicy pol, _), st) => + let + val e1 = case pol of + PolQuery e1 => e1 + in + usedVars st e1 + end | (_, st) => st) (IS.empty, IS.empty) file val (cdef, edef) = foldl (fn ((DDatatype dts, _), (cdef, edef)) => @@ -74,7 +81,8 @@ | ((DJavaScript _, _), acc) => acc | ((DCookie _, _), acc) => acc | ((DStyle _, _), acc) => acc - | ((DTask _, _), acc) => acc) + | ((DTask _, _), acc) => acc + | ((DPolicy _, _), acc) => acc) (IM.empty, IM.empty) file fun typ (c, s) = @@ -141,7 +149,8 @@ | (DJavaScript _, _) => true | (DCookie _, _) => true | (DStyle _, _) => true - | (DTask _, _) => true) file + | (DTask _, _) => true + | (DPolicy _, _) => true) file end end
--- a/src/mono_util.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/mono_util.sml Sun Apr 04 12:29:34 2010 -0400 @@ -534,6 +534,16 @@ S.map2 (mfe ctx e2, fn e2' => (DTask (e1', e2'), loc))) + | DPolicy pol => + S.map2 (mfpol ctx pol, + fn p' => + (DPolicy p', loc)) + + and mfpol ctx pol = + case pol of + PolQuery e => + S.map2 (mfe ctx e, + PolQuery) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t, @@ -621,6 +631,7 @@ | DCookie _ => ctx | DStyle _ => ctx | DTask _ => ctx + | DPolicy _ => ctx in S.map2 (mff ctx' ds', fn ds' => @@ -674,7 +685,8 @@ | DJavaScript _ => count | DCookie _ => count | DStyle _ => count - | DTask _ => count) 0 + | DTask _ => count + | DPolicy _ => count) 0 end
--- a/src/monoize.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/monoize.sml Sun Apr 04 12:29:34 2010 -0400 @@ -3738,6 +3738,20 @@ fm, [(L'.DTask (e1, e2), loc)]) end + | L.DPolicy e => + 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)) + + val (e, fm) = monoExp (env, St.empty, fm) e + in + SOME (env, + fm, + [(L'.DPolicy (make e), loc)]) + end end datatype expungable = Client | Channel
--- a/src/reduce.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/reduce.sml Sun Apr 04 12:29:34 2010 -0400 @@ -746,6 +746,15 @@ namedC, namedE)) end + | DPolicy e1 => + let + val e1 = exp (namedC, namedE) [] e1 + in + ((DPolicy e1, loc), + (polyC, + namedC, + namedE)) + end val (file, _) = ListUtil.foldlMap doDecl (IS.empty, IM.empty, IM.empty) file in
--- a/src/reduce_local.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/reduce_local.sml Sun Apr 04 12:29:34 2010 -0400 @@ -252,6 +252,7 @@ | DCookie _ => d | DStyle _ => d | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc) + | DPolicy e1 => (DPolicy (exp [] e1), loc) in map doDecl file end
--- a/src/shake.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/shake.sml Sun Apr 04 12:29:34 2010 -0400 @@ -90,6 +90,11 @@ st else usedVars (usedVars st e1) e2 + | ((DPolicy e1, _), st) => + if !sliceDb then + st + else + usedVars st e1 | (_, acc) => acc) (IS.empty, IS.empty) file val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, [c]), edef) @@ -116,7 +121,8 @@ (cdef, IM.insert (edef, n, ([], c, dummye))) | ((DStyle (_, n, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], dummyt, dummye))) - | ((DTask _, _), acc) => acc) + | ((DTask _, _), acc) => acc + | ((DPolicy _, _), acc) => acc) (IM.empty, IM.empty) file fun kind (_, s) = s @@ -203,7 +209,8 @@ | (DDatabase _, _) => not (!sliceDb) | (DCookie _, _) => not (!sliceDb) | (DStyle _, _) => not (!sliceDb) - | (DTask _, _) => not (!sliceDb)) file + | (DTask _, _) => not (!sliceDb) + | (DPolicy _, _) => not (!sliceDb)) file end end
--- a/src/source.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/source.sml Sun Apr 04 12:29:34 2010 -0400 @@ -168,6 +168,7 @@ | DCookie of string * con | DStyle of string | DTask of exp * exp + | DPolicy of exp and str' = StrConst of decl list
--- a/src/source_print.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/source_print.sml Sun Apr 04 12:29:34 2010 -0400 @@ -669,6 +669,9 @@ string "=", space, p_exp e2] + | DPolicy e1 => box [string "policy", + space, + p_exp e1] and p_str (str, _) = case str of
--- a/src/unnest.sml Thu Apr 01 17:23:17 2010 -0400 +++ b/src/unnest.sml Sun Apr 04 12:29:34 2010 -0400 @@ -423,6 +423,7 @@ | DCookie _ => default () | DStyle _ => default () | DTask _ => explore () + | DPolicy _ => explore () end and doStr (all as (str, loc), st) =
--- a/src/urweb.grm Thu Apr 01 17:23:17 2010 -0400 +++ b/src/urweb.grm Sun Apr 04 12:29:34 2010 -0400 @@ -202,7 +202,7 @@ | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | SELECT1 | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE | VIEW - | COOKIE | STYLE | TASK + | COOKIE | STYLE | TASK | POLICY | CASE | IF | THEN | ELSE | ANDALSO | ORELSE | XML_BEGIN of string | XML_END | XML_BEGIN_END of string @@ -481,6 +481,7 @@ | COOKIE SYMBOL COLON cexp ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))]) | STYLE SYMBOL ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))]) | TASK eapps EQ eexp ([(DTask (eapps, eexp), s (TASKleft, eexpright))]) + | POLICY eexp ([(DPolicy eexp, s (POLICYleft, eexpright))]) dtype : SYMBOL dargs EQ barOpt dcons (SYMBOL, dargs, dcons)
--- a/src/urweb.lex Thu Apr 01 17:23:17 2010 -0400 +++ b/src/urweb.lex Sun Apr 04 12:29:34 2010 -0400 @@ -416,6 +416,7 @@ <INITIAL> "cookie" => (Tokens.COOKIE (pos yypos, pos yypos + size yytext)); <INITIAL> "style" => (Tokens.STYLE (pos yypos, pos yypos + size yytext)); <INITIAL> "task" => (Tokens.TASK (pos yypos, pos yypos + size yytext)); +<INITIAL> "policy" => (Tokens.POLICY (pos yypos, pos yypos + size yytext)); <INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); <INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));