# HG changeset patch # User Adam Chlipala # Date 1399072749 14400 # Node ID 403f0cc65b9c87ce5b77e456b1cb4d9addc01680 # Parent 799be3911ce3ad267f605d2bd96477199b199a07 New lessSafeFfi diff -r 799be3911ce3 -r 403f0cc65b9c doc/manual.tex --- 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} diff -r 799be3911ce3 -r 403f0cc65b9c src/compiler.sml --- 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 () diff -r 799be3911ce3 -r 403f0cc65b9c src/corify.sml --- 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, _) = diff -r 799be3911ce3 -r 403f0cc65b9c src/elab.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/elab_env.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/elab_print.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/elab_util.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/elaborate.sml --- 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), diff -r 799be3911ce3 -r 403f0cc65b9c src/elisp/urweb-mode.el --- 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.") diff -r 799be3911ce3 -r 403f0cc65b9c src/expl.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/expl_env.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/expl_print.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/expl_rename.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/explify.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/settings.sig --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/settings.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/source.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/source_print.sml --- 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 diff -r 799be3911ce3 -r 403f0cc65b9c src/unnest.sml --- 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) = diff -r 799be3911ce3 -r 403f0cc65b9c src/urweb.grm --- 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) diff -r 799be3911ce3 -r 403f0cc65b9c src/urweb.lex --- 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 @@ "style" => (Tokens.STYLE (pos yypos, pos yypos + size yytext)); "task" => (Tokens.TASK (pos yypos, pos yypos + size yytext)); "policy" => (Tokens.POLICY (pos yypos, pos yypos + size yytext)); + "ffi" => (Tokens.FFI (pos yypos, pos yypos + size yytext)); "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext)); diff -r 799be3911ce3 -r 403f0cc65b9c tests/lessSafeFfi.ur --- /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 + (*{[foo 42]}, {[q]}*) +