Mercurial > urweb
changeset 2010:403f0cc65b9c
New lessSafeFfi
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 02 May 2014 19:19:09 -0400 |
parents | 799be3911ce3 |
children | cfd604842006 |
files | doc/manual.tex src/compiler.sml src/corify.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/elisp/urweb-mode.el src/expl.sml src/expl_env.sml src/expl_print.sml src/expl_rename.sml src/explify.sml src/settings.sig src/settings.sml src/source.sml src/source_print.sml src/unnest.sml src/urweb.grm src/urweb.lex tests/lessSafeFfi.ur tests/lessSafeFfi.urp tests/lessSafeFfi.urs |
diffstat | 24 files changed, 198 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Fri May 02 17:16:02 2014 -0400 +++ b/doc/manual.tex Fri May 02 19:19:09 2014 -0400 @@ -2530,6 +2530,24 @@ The onus is on the coder of a new tag's interface to think about consequences for code injection attacks, messing with the DOM in ways that may break Ur/Web reactive programming, etc. +\subsection{The Less Safe FFI} + +An alternative interface is provided for declaring FFI functions inline within normal Ur/Web modules. This facility must be opted into with the \texttt{lessSafeFfi} \texttt{.urp} directive, since it breaks a crucial property, allowing code in a \texttt{.ur} file to break basic invariants of the Ur/Web type system. Without this option, one only needs to audit \texttt{.urp} files to be sure an application obeys the type-system rules. The alternative interface may be more convenient for such purposes as declaring an FFI function typed in terms of some type local to a module. + +When the less safe mode is enabled, declarations like this one are accepted, at the top level of a \texttt{.ur} file: +\begin{verbatim} + ffi foo : int -> int +\end{verbatim} + +Now \texttt{foo} is available as a normal function. If called in server-side code, and if the above declaration appeared in \texttt{bar.ur}, the C function will be linked as \texttt{uw\_Bar\_foo()}. It is also possible to declare an FFI function to be implemented in JavaScript, using a general facility for including modifiers in an FFI declaration. The modifiers appear before the colon, separated by spaces. Here are the available ones, which have the same semantics as corresponding \texttt{.urp} directives. +\begin{itemize} +\item \texttt{effectful} +\item \texttt{benignEffectful} +\item \texttt{clientOnly} +\item \texttt{serverOnly} +\item \texttt{jsFunc "putJsFuncNameHere"} +\end{itemize} + \section{Compiler Phases}
--- a/src/compiler.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/compiler.sml Fri May 02 19:19:09 2014 -0400 @@ -874,6 +874,7 @@ | "timeFormat" => Settings.setTimeFormat arg | "noMangleSql" => Settings.setMangleSql false | "html5" => Settings.setIsHtml5 true + | "lessSafeFfi" => Settings.setLessSafeFfi true | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); read ()
--- a/src/corify.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/corify.sml Fri May 02 19:19:09 2014 -0400 @@ -643,6 +643,12 @@ | L.ELet (x, t, e1, e2) => (L'.ELet (x, corifyCon st t, corifyExp st e1, corifyExp st e2), loc) +fun isTransactional (c, _) = + case c of + L'.TFun (_, c) => isTransactional c + | L'.CApp ((L'.CFfi ("Basis", "transaction"), _), _) => true + | _ => false + fun corifyDecl mods (all as (d, loc : EM.span), st) = case d of L.DCon (x, n, k, c) => @@ -970,12 +976,6 @@ in transactify c end - - fun isTransactional (c, _) = - case c of - L'.TFun (_, c) => isTransactional c - | L'.CApp ((L'.CFfi ("Basis", "transaction"), _), _) => true - | _ => false in if isTransactional c then let @@ -1164,6 +1164,66 @@ ([], st)) end + | L.DFfi (x, n, modes, t) => + let + val m = case St.name st of + [m] => m + | _ => (ErrorMsg.errorAt loc "Used 'ffi' declaration beneath module top level"; + "") + + val name = (m, x) + + val (st, n) = St.bindVal st x n + val s = doRestify Settings.Url (mods, x) + + val t' = corifyCon st t + + fun numArgs (t : L'.con) = + case #1 t of + L'.TFun (_, ran) => 1 + numArgs ran + | _ => 0 + + fun makeArgs (i, t : L'.con, acc) = + case #1 t of + L'.TFun (dom, ran) => makeArgs (i-1, ran, ((L'.ERel i, loc), dom) :: acc) + | _ => rev acc + + fun wrapAbs (i, t : L'.con, tTrans, e) = + case (#1 t, #1 tTrans) of + (L'.TFun (dom, ran), L'.TFun (_, ran')) => (L'.EAbs ("x" ^ Int.toString i, dom, ran, wrapAbs (i+1, ran, ran', e)), loc) + | _ => e + + fun getRan (t : L'.con) = + case #1 t of + L'.TFun (_, ran) => getRan ran + | _ => t + + fun addLastBit (t : L'.con) = + case #1 t of + L'.TFun (dom, ran) => (L'.TFun (dom, addLastBit ran), #2 t) + | _ => (L'.TFun ((L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc), t), loc) + + val e = (L'.EFfiApp (m, x, makeArgs (numArgs t' - 1, t', [])), loc) + val (e, tTrans) = if isTransactional t' then + ((L'.EAbs ("_", (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc), getRan t', e), loc), addLastBit t') + else + (e, t') + val e = wrapAbs (0, t', tTrans, e) + in + app (fn Source.Effectful => Settings.addEffectful name + | Source.BenignEffectful => Settings.addBenignEffectful name + | Source.ClientOnly => Settings.addClientOnly name + | Source.ServerOnly => Settings.addServerOnly name + | Source.JsFunc s => Settings.addJsFunc (name, s)) modes; + + if isTransactional t' andalso not (Settings.isBenignEffectful name) then + Settings.addEffectful name + else + (); + + ([(L'.DVal (x, n, t', e, s), loc)], st) + end + and corifyStr mods ((str, loc), st) = case str of L.StrConst ds => @@ -1237,7 +1297,8 @@ | L.DStyle (_, _, n') => Int.max (n, n') | L.DTask _ => n | L.DPolicy _ => n - | L.DOnError _ => n) + | L.DOnError _ => n + | L.DFfi (_, n', _, _) => Int.max (n, n')) 0 ds and maxNameStr (str, _) =
--- a/src/elab.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/elab.sml Fri May 02 19:19:09 2014 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2011, Adam Chlipala +(* Copyright (c) 2008-2011, 2014, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -181,6 +181,7 @@ | DTask of exp * exp | DPolicy of exp | DOnError of int * string list * string + | DFfi of string * int * Source.ffi_mode list * con and str' = StrConst of decl list
--- a/src/elab_env.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/elab_env.sml Fri May 02 19:19:09 2014 -0400 @@ -1681,5 +1681,6 @@ | DTask _ => env | DPolicy _ => env | DOnError _ => env + | DFfi (x, n, _, t) => pushENamedAs env x n t end
--- a/src/elab_print.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/elab_print.sml Fri May 02 19:19:09 2014 -0400 @@ -852,6 +852,7 @@ space, p_exp env e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str env (str, _) = case str of
--- a/src/elab_util.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/elab_util.sml Fri May 02 19:19:09 2014 -0400 @@ -927,7 +927,8 @@ bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc))) | DTask _ => ctx | DPolicy _ => ctx - | DOnError _ => ctx, + | DOnError _ => ctx + | DFfi (x, _, _, t) => bind (ctx, NamedE (x, t)), mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -1056,6 +1057,10 @@ fn e1' => (DPolicy e1', loc)) | DOnError _ => S.return2 dAll + | DFfi (x, n, modes, t) => + S.map2 (mfc ctx t, + fn t' => + (DFfi (x, n, modes, t'), loc)) and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, @@ -1234,6 +1239,7 @@ | DTask _ => 0 | DPolicy _ => 0 | DOnError _ => 0 + | DFfi (_, n, _, _) => n and maxNameStr (str, _) = case str of StrConst ds => maxName ds
--- a/src/elaborate.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/elaborate.sml Fri May 02 19:19:09 2014 -0400 @@ -2999,6 +2999,7 @@ | L'.DTask _ => [] | L'.DPolicy _ => [] | L'.DOnError _ => [] + | L'.DFfi (x, n, _, t) => [(L'.SgiVal (x, n, t), loc)] and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), @@ -4298,6 +4299,20 @@ ([(L'.DOnError (n, ms, s), loc)], (env, denv, gs)) end) + | L.DFfi (x, modes, t) => + let + val () = if Settings.getLessSafeFfi () then + () + else + ErrorMsg.errorAt loc "To enable 'ffi' declarations, the .urp directive 'lessSafeFfi' is mandatory." + + val (t', _, gs1) = elabCon (env, denv) t + val t' = normClassConstraint env t' + val (env', n) = E.pushENamed env x t' + in + ([(L'.DFfi (x, n, modes, t'), loc)], (env', denv, enD gs1 @ gs)) + end + (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) in (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll),
--- a/src/elisp/urweb-mode.el Fri May 02 17:16:02 2014 -0400 +++ b/src/elisp/urweb-mode.el Fri May 02 19:19:09 2014 -0400 @@ -139,7 +139,7 @@ "of" "open" "let" "in" "rec" "sequence" "sig" "signature" "cookie" "style" "task" "policy" "struct" "structure" "table" "view" "then" "type" "val" "where" - "with" + "with" "ffi" "Name" "Type" "Unit") "A regexp that matches any non-SQL keywords of Ur/Web.")
--- a/src/expl.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/expl.sml Fri May 02 19:19:09 2014 -0400 @@ -150,6 +150,7 @@ | DTask of exp * exp | DPolicy of exp | DOnError of int * string list * string + | DFfi of string * int * Source.ffi_mode list * con and str' = StrConst of decl list
--- a/src/expl_env.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/expl_env.sml Fri May 02 19:19:09 2014 -0400 @@ -346,6 +346,7 @@ | DTask _ => env | DPolicy _ => env | DOnError _ => env + | DFfi (x, n, _, t) => pushENamed env x n t fun sgiBinds env (sgi, loc) = case sgi of
--- a/src/expl_print.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/expl_print.sml Fri May 02 19:19:09 2014 -0400 @@ -731,6 +731,7 @@ space, p_exp env e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str env (str, _) = case str of
--- a/src/expl_rename.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/expl_rename.sml Fri May 02 19:19:09 2014 -0400 @@ -219,6 +219,7 @@ (case St.lookup (st, n) of NONE => all | SOME n' => (DOnError (n', xs, x), loc)) + | DFfi (x, n, modes, t) => (DFfi (x, n, modes, renameCon st t), loc) and renameStr st (all as (str, loc)) = case str of @@ -413,6 +414,15 @@ (case St.lookup (st, n) of NONE => ([all], st) | SOME n' => ([(DOnError (n', xs, x), loc)], st)) + | DFfi (x, n, modes, t) => + let + val (st, n') = St.bind (st, n) + val t' = renameCon st t + in + ([(DFfi (x, n, modes, t'), loc), + (DVal (x, n', t', (ENamed n, loc)), loc)], + st) + end fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} = case str of
--- a/src/explify.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/explify.sml Fri May 02 19:19:09 2014 -0400 @@ -198,6 +198,7 @@ | L.DTask (e1, e2) => SOME (L'.DTask (explifyExp e1, explifyExp e2), loc) | L.DPolicy e1 => SOME (L'.DPolicy (explifyExp e1), loc) | L.DOnError v => SOME (L'.DOnError v, loc) + | L.DFfi (x, n, modes, t) => SOME (L'.DFfi (x, n, modes, explifyCon t), loc) and explifyStr (str, loc) = case str of
--- a/src/settings.sig Fri May 02 17:16:02 2014 -0400 +++ b/src/settings.sig Fri May 02 19:19:09 2014 -0400 @@ -78,18 +78,22 @@ (* Which FFI functions should not have their calls removed or reordered, but cause no lasting effects? *) val setBenignEffectful : ffi list -> unit + val addBenignEffectful : ffi -> unit val isBenignEffectful : ffi -> bool (* Which FFI functions may only be run in clients? *) val setClientOnly : ffi list -> unit + val addClientOnly : ffi -> unit val isClientOnly : ffi -> bool (* Which FFI functions may only be run on servers? *) val setServerOnly : ffi list -> unit + val addServerOnly : ffi -> unit val isServerOnly : ffi -> bool (* Which FFI functions may be run in JavaScript? (JavaScript function names included) *) val setJsFuncs : (ffi * string) list -> unit + val addJsFunc : ffi * string -> unit val jsFunc : ffi -> string option val allJsFuncs : unit -> (ffi * string) list @@ -271,4 +275,7 @@ val setIsHtml5 : bool -> unit val getIsHtml5 : unit -> bool + + val setLessSafeFfi : bool -> unit + val getLessSafeFfi : unit -> bool end
--- a/src/settings.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/settings.sml Fri May 02 19:19:09 2014 -0400 @@ -194,6 +194,7 @@ val benign = ref benignBase fun setBenignEffectful ls = benign := S.addList (benignBase, ls) +fun addBenignEffectful x = benign := S.add (!benign, x) fun isBenignEffectful x = S.member (!benign, x) val clientBase = basis ["get_client_source", @@ -225,6 +226,7 @@ "giveFocus"] val client = ref clientBase fun setClientOnly ls = client := S.addList (clientBase, ls) +fun addClientOnly x = client := S.add (!client, x) fun isClientOnly x = S.member (!client, x) val serverBase = basis ["requestHeader", @@ -240,6 +242,7 @@ "firstFormField"] val server = ref serverBase fun setServerOnly ls = server := S.addList (serverBase, ls) +fun addServerOnly x = server := S.add (!server, x) fun isServerOnly x = S.member (!server, x) val basisM = foldl (fn ((k, v : string), m) => M.insert (m, ("Basis", k), v)) M.empty @@ -364,6 +367,7 @@ val jsFuncs = ref jsFuncsBase fun setJsFuncs ls = jsFuncs := foldl (fn ((k, v), m) => M.insert (m, k, v)) jsFuncsBase ls fun jsFunc x = M.find (!jsFuncs, x) +fun addJsFunc (k, v) = jsFuncs := M.insert (!jsFuncs, k, v) fun allJsFuncs () = M.listItemsi (!jsFuncs) datatype pattern_kind = Exact | Prefix @@ -735,4 +739,8 @@ fun setIsHtml5 b = html5 := b fun getIsHtml5 () = !html5 +val less = ref false +fun setLessSafeFfi b = less := b +fun getLessSafeFfi () = !less + end
--- a/src/source.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/source.sml Fri May 02 19:19:09 2014 -0400 @@ -147,6 +147,13 @@ and exp = exp' located and edecl = edecl' located +datatype ffi_mode = + Effectful + | BenignEffectful + | ClientOnly + | ServerOnly + | JsFunc of string + datatype decl' = DCon of string * kind option * con | DDatatype of (string * string list * (string * con option) list) list @@ -169,6 +176,7 @@ | DTask of exp * exp | DPolicy of exp | DOnError of string * string list * string + | DFfi of string * ffi_mode list * con and str' = StrConst of decl list
--- a/src/source_print.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/source_print.sml Fri May 02 19:19:09 2014 -0400 @@ -674,6 +674,7 @@ space, p_exp e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str (str, _) = case str of
--- a/src/unnest.sml Fri May 02 17:16:02 2014 -0400 +++ b/src/unnest.sml Fri May 02 19:19:09 2014 -0400 @@ -452,6 +452,7 @@ | DTask _ => explore () | DPolicy _ => explore () | DOnError _ => default () + | DFfi _ => default () end and doStr (all as (str, loc), st) =
--- a/src/urweb.grm Fri May 02 17:16:02 2014 -0400 +++ b/src/urweb.grm Fri May 02 19:19:09 2014 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2012, Adam Chlipala +(* Copyright (c) 2008-2014, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -365,7 +365,7 @@ | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | TCOLONWILD | DOT | HASH | UNDER | UNDERUNDER | BAR | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT - | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS + | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS | FFI | DATATYPE | OF | TYPE | NAME | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG @@ -532,6 +532,9 @@ | enterDml of unit | leaveDml of unit + | ffi_mode of ffi_mode + | ffi_modes of ffi_mode list + %verbose (* print summary of errors *) %pos int (* positions *) @@ -645,6 +648,7 @@ | STYLE SYMBOL ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))]) | TASK eapps EQ eexp ([(DTask (eapps, eexp), s (TASKleft, eexpright))]) | POLICY eexp ([(DPolicy eexp, s (POLICYleft, eexpright))]) + | FFI SYMBOL ffi_modes COLON cexp([(DFfi (SYMBOL, ffi_modes, cexp), s (FFIleft, cexpright))]) dtype : SYMBOL dargs EQ barOpt dcons (SYMBOL, dargs, dcons) @@ -2267,3 +2271,16 @@ | SUM ("sum") | MIN ("min") | MAX ("max") + +ffi_mode : SYMBOL (case SYMBOL of + "effectful" => Effectful + | "benignEffectful" => BenignEffectful + | "clientOnly" => ClientOnly + | "serverOnly" => ServerOnly + | _ => (ErrorMsg.errorAt (s (SYMBOLleft, SYMBOLright)) "Invalid FFI mode"; Effectful)) + | SYMBOL STRING (case SYMBOL of + "jsFunc" => JsFunc STRING + | _ => (ErrorMsg.errorAt (s (SYMBOLleft, SYMBOLright)) "Invalid FFI mode"; Effectful)) + +ffi_modes : ([]) + | ffi_mode ffi_modes (ffi_mode :: ffi_modes)
--- a/src/urweb.lex Fri May 02 17:16:02 2014 -0400 +++ b/src/urweb.lex Fri May 02 19:19:09 2014 -0400 @@ -445,6 +445,7 @@ <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> "ffi" => (Tokens.FFI (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));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/lessSafeFfi.ur Fri May 02 19:19:09 2014 -0400 @@ -0,0 +1,19 @@ +ffi foo : int -> int +ffi bar serverOnly benignEffectful : int -> transaction unit +ffi baz : transaction int + +ffi bup jsFunc "jsbup" : int -> transaction unit + +fun other () : transaction page = + (*bar 17; + q <- baz;*) + return <xml><body> + (*{[foo 42]}, {[q]}*) + <button onclick={fn _ => bup 32}/> + </body></xml> + +fun main () = return <xml><body> + <form> + <submit action={other}/> + </form> +</body></xml>