From 0c83e8f7c345a27be3cae77eeb2d7cb8658e5e9c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 2 May 2014 19:19:09 -0400 Subject: New lessSafeFfi --- doc/manual.tex | 18 ++++++++++++ src/compiler.sml | 1 + src/corify.sml | 75 ++++++++++++++++++++++++++++++++++++++++++++----- src/elab.sml | 3 +- src/elab_env.sml | 1 + src/elab_print.sml | 1 + src/elab_util.sml | 8 +++++- src/elaborate.sml | 15 ++++++++++ src/elisp/urweb-mode.el | 2 +- src/expl.sml | 1 + src/expl_env.sml | 1 + src/expl_print.sml | 1 + src/expl_rename.sml | 10 +++++++ src/explify.sml | 1 + src/settings.sig | 7 +++++ src/settings.sml | 8 ++++++ src/source.sml | 8 ++++++ src/source_print.sml | 1 + src/unnest.sml | 1 + src/urweb.grm | 21 ++++++++++++-- src/urweb.lex | 1 + tests/lessSafeFfi.ur | 19 +++++++++++++ tests/lessSafeFfi.urp | 5 ++++ tests/lessSafeFfi.urs | 1 + 24 files changed, 198 insertions(+), 12 deletions(-) create mode 100644 tests/lessSafeFfi.ur create mode 100644 tests/lessSafeFfi.urp create mode 100644 tests/lessSafeFfi.urs diff --git a/doc/manual.tex b/doc/manual.tex index db4994a5..b233473e 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2530,6 +2530,24 @@ FFI modules may introduce new tags as values with $\mt{Basis.tag}$ types. See \ 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 --git a/src/compiler.sml b/src/compiler.sml index cc4e33c5..269a7824 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -874,6 +874,7 @@ fun parseUrp' accLibs fname = | "timeFormat" => Settings.setTimeFormat arg | "noMangleSql" => Settings.setMangleSql false | "html5" => Settings.setIsHtml5 true + | "lessSafeFfi" => Settings.setLessSafeFfi true | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); read () diff --git a/src/corify.sml b/src/corify.sml index 085b2eb8..b08ef7eb 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -643,6 +643,12 @@ fun corifyExp st (e, loc) = | 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 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) = 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 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) = ([], 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 @@ fun maxName ds = foldl (fn ((d, _), n) => | 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 --git a/src/elab.sml b/src/elab.sml index 2dab5c34..249531f1 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -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 @@ datatype decl' = | 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 --git a/src/elab_env.sml b/src/elab_env.sml index 465fb7e4..9fbe7bd7 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1681,5 +1681,6 @@ fun declBinds env (d, loc) = | DTask _ => env | DPolicy _ => env | DOnError _ => env + | DFfi (x, n, _, t) => pushENamedAs env x n t end diff --git a/src/elab_print.sml b/src/elab_print.sml index 7ce94c97..957d4646 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -852,6 +852,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, p_exp env e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str env (str, _) = case str of diff --git a/src/elab_util.sml b/src/elab_util.sml index 60245585..fef55852 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -927,7 +927,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ and maxNameDecl (d, _) = | DTask _ => 0 | DPolicy _ => 0 | DOnError _ => 0 + | DFfi (_, n, _, _) => n and maxNameStr (str, _) = case str of StrConst ds => maxName ds diff --git a/src/elaborate.sml b/src/elaborate.sml index 97ac610b..d492883f 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2999,6 +2999,7 @@ and sgiOfDecl (d, loc) = | 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 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = ([(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 --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el index f183a9ab..edbff1b0 100644 --- a/src/elisp/urweb-mode.el +++ b/src/elisp/urweb-mode.el @@ -139,7 +139,7 @@ See doc for the variable `urweb-mode-info'." "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 --git a/src/expl.sml b/src/expl.sml index 0d4e63cc..3d784e3f 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -150,6 +150,7 @@ datatype decl' = | 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 --git a/src/expl_env.sml b/src/expl_env.sml index f5a5eb0a..5712a72d 100644 --- a/src/expl_env.sml +++ b/src/expl_env.sml @@ -346,6 +346,7 @@ fun declBinds env (d, loc) = | DTask _ => env | DPolicy _ => env | DOnError _ => env + | DFfi (x, n, _, t) => pushENamed env x n t fun sgiBinds env (sgi, loc) = case sgi of diff --git a/src/expl_print.sml b/src/expl_print.sml index a830dccb..22d246e2 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -731,6 +731,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, p_exp env e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str env (str, _) = case str of diff --git a/src/expl_rename.sml b/src/expl_rename.sml index 7e7a155a..bb763a60 100644 --- a/src/expl_rename.sml +++ b/src/expl_rename.sml @@ -219,6 +219,7 @@ fun renameDecl st (all as (d, loc)) = (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 @@ fun dupDecl (all as (d, loc), st) = (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 --git a/src/explify.sml b/src/explify.sml index 4c60bd20..fd0f3277 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -198,6 +198,7 @@ fun explifyDecl (d, loc : EM.span) = | 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 --git a/src/settings.sig b/src/settings.sig index 20dd00c2..29c4c506 100644 --- a/src/settings.sig +++ b/src/settings.sig @@ -78,18 +78,22 @@ signature SETTINGS = sig (* 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 @@ signature SETTINGS = sig val setIsHtml5 : bool -> unit val getIsHtml5 : unit -> bool + + val setLessSafeFfi : bool -> unit + val getLessSafeFfi : unit -> bool end diff --git a/src/settings.sml b/src/settings.sml index 4cdb4119..f00a4853 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -194,6 +194,7 @@ val benignBase = basis ["get_cookie", 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 @@ val clientBase = basis ["get_client_source", "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 @@ val serverBase = basis ["requestHeader", "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 jsFuncsBase = basisM [("alert", "alert"), 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 @@ val html5 = ref false fun setIsHtml5 b = html5 := b fun getIsHtml5 () = !html5 +val less = ref false +fun setLessSafeFfi b = less := b +fun getLessSafeFfi () = !less + end diff --git a/src/source.sml b/src/source.sml index eea7ad4c..2a741dd9 100644 --- a/src/source.sml +++ b/src/source.sml @@ -147,6 +147,13 @@ and pat = pat' located 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 @@ datatype decl' = | 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 --git a/src/source_print.sml b/src/source_print.sml index fdacfe6c..db56a0db 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -674,6 +674,7 @@ fun p_decl ((d, _) : decl) = space, p_exp e1] | DOnError _ => string "ONERROR" + | DFfi _ => string "FFI" and p_str (str, _) = case str of diff --git a/src/unnest.sml b/src/unnest.sml index 17bfd39f..fceb5026 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -452,6 +452,7 @@ fun unnest file = | DTask _ => explore () | DPolicy _ => explore () | DOnError _ => default () + | DFfi _ => default () end and doStr (all as (str, loc), st) = diff --git a/src/urweb.grm b/src/urweb.grm index 7aec9492..157ecfac 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -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 @@ fun patternOut (e : exp) = | 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 @@ fun patternOut (e : exp) = | 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 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let | 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 @@ sqlagg : AVG ("avg") | 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 --git a/src/urweb.lex b/src/urweb.lex index 293c6dc6..15ae448e 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -445,6 +445,7 @@ xint = x[0-9a-fA-F][0-9a-fA-F]; "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 --git a/tests/lessSafeFfi.ur b/tests/lessSafeFfi.ur new file mode 100644 index 00000000..da79bfdc --- /dev/null +++ b/tests/lessSafeFfi.ur @@ -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]}*) +