# HG changeset patch # User Adam Chlipala # Date 1292687791 18000 # Node ID b106ca8200b1e33267ad965ace42319408121357 # Parent faad7d01b200b0c73d0e4de77773477fbfa73fd1 postBody type diff -r faad7d01b200 -r b106ca8200b1 doc/manual.tex --- a/doc/manual.tex Thu Dec 16 18:40:49 2010 -0500 +++ b/doc/manual.tex Sat Dec 18 10:56:31 2010 -0500 @@ -2077,6 +2077,8 @@ A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module. The signature of the main module determines the URL entry points to the application. Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$. If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply-nested functions, as described in Section \ref{tag} below. Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}. +Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects. To export a page which may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$. When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$). This kind of handler will only work with \texttt{POST} payloads of MIME types besides those associated with HTML forms; for these, use Ur/Web's built-in support, as described below. + When the standalone web server receives a request for a known page, it calls the function for that page, ``running'' the resulting transaction to produce the page to return to the client. Pages link to other pages with the \texttt{link} attribute of the \texttt{a} HTML tag. A link has type $\mt{transaction} \; \mt{page}$, and the semantics of a link are that this transaction should be run to compute the result page, when the link is followed. Link targets are assigned URL names in the same way as top-level entry points. HTML forms are handled in a similar way. The $\mt{action}$ attribute of a $\mt{submit}$ form tag takes a value of type $\$\mt{use} \to \mt{transaction} \; \mt{page}$, where $\mt{use}$ is a kind-$\{\mt{Type}\}$ record of the form fields used by this action handler. Action handlers are assigned URL patterns in the same way as above. @@ -2087,7 +2089,7 @@ \medskip -The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers. +The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers. Ur/Web includes a kind of automatic protection against cross site request forgery attacks. Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server. Signing and signature checking are inserted automatically by the compiler. This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect. diff -r faad7d01b200 -r b106ca8200b1 include/types.h --- a/include/types.h Thu Dec 16 18:40:49 2010 -0500 +++ b/include/types.h Sat Dec 18 10:56:31 2010 -0500 @@ -40,6 +40,10 @@ uw_Basis_blob data; } uw_Basis_file; +typedef struct uw_Basis_postBody { + uw_Basis_string type, data; +} uw_Basis_postBody; + typedef enum { SUCCESS, FATAL, BOUNDED_RETRY, UNLIMITED_RETRY, RETURN_INDIRECTLY } failure_kind; typedef enum { SERVED, KEEP_OPEN, FAILED } request_result; diff -r faad7d01b200 -r b106ca8200b1 include/urweb.h --- a/include/urweb.h Thu Dec 16 18:40:49 2010 -0500 +++ b/include/urweb.h Sat Dec 18 10:56:31 2010 -0500 @@ -221,6 +221,13 @@ uw_Basis_int uw_Basis_blobSize(uw_context, uw_Basis_blob); uw_Basis_blob uw_Basis_textBlob(uw_context, uw_Basis_string); +uw_Basis_string uw_Basis_postType(uw_context, uw_Basis_postBody); +uw_Basis_string uw_Basis_postData(uw_context, uw_Basis_postBody); +void uw_noPostBody(uw_context); +void uw_postBody(uw_context, uw_Basis_postBody); +int uw_hasPostBody(uw_context); +uw_Basis_postBody uw_getPostBody(uw_context); + __attribute__((noreturn)) void uw_return_blob(uw_context, uw_Basis_blob, uw_Basis_string mimeType); __attribute__((noreturn)) void uw_redirect(uw_context, uw_Basis_string url); diff -r faad7d01b200 -r b106ca8200b1 lib/ur/basis.urs --- a/lib/ur/basis.urs Thu Dec 16 18:40:49 2010 -0500 +++ b/lib/ur/basis.urs Sat Dec 18 10:56:31 2010 -0500 @@ -737,6 +737,10 @@ val blobSize : blob -> int val textBlob : string -> blob +type postBody +val postType : postBody -> string +val postData : postBody -> string + con radio = [Body, Radio] val radio : formTag string radio [Id = string] val radioOption : unit -> tag ([Value = string, Checked = bool] ++ boxAttrs) radio [] [] [] diff -r faad7d01b200 -r b106ca8200b1 src/c/request.c --- a/src/c/request.c Thu Dec 16 18:40:49 2010 -0500 +++ b/src/c/request.c Sat Dec 18 10:56:31 2010 -0500 @@ -192,6 +192,9 @@ boundary[0] = '-'; boundary[1] = '-'; boundary_len = strlen(boundary); + } else if (clen_s && strcasecmp(clen_s, "application/x-www-form-urlencoded")) { + uw_Basis_postBody pb = {clen_s, body}; + uw_postBody(ctx, pb); } } else if (strcmp(method, "GET")) { log_error(logger_data, "Not ready for non-GET/POST command: %s\n", method); @@ -325,7 +328,7 @@ } } } - else { + else if (!uw_hasPostBody(ctx)) { inputs = is_post ? body : query_string; if (inputs) { diff -r faad7d01b200 -r b106ca8200b1 src/c/urweb.c --- a/src/c/urweb.c Thu Dec 16 18:40:49 2010 -0500 +++ b/src/c/urweb.c Sat Dec 18 10:56:31 2010 -0500 @@ -445,6 +445,9 @@ void *logger_data; uw_logger log_debug; + int hasPostBody; + uw_Basis_postBody postBody; + char error_message[ERROR_BUF_LEN]; }; @@ -507,6 +510,8 @@ ctx->logger_data = logger_data; ctx->log_debug = log_debug; + ctx->hasPostBody = 0; + return ctx; } @@ -583,6 +588,7 @@ ctx->cur_container = NULL; ctx->used_transactionals = 0; ctx->script_header = ""; + ctx->hasPostBody = 0; } void uw_reset_keep_request(uw_context ctx) { @@ -3200,6 +3206,14 @@ return f.data; } +uw_Basis_string uw_Basis_postType(uw_context ctx, uw_Basis_postBody pb) { + return pb.type; +} + +uw_Basis_string uw_Basis_postData(uw_context ctx, uw_Basis_postBody pb) { + return pb.data; +} + __attribute__((noreturn)) void uw_return_blob(uw_context ctx, uw_Basis_blob b, uw_Basis_string mimeType) { cleanup *cl; int len; @@ -3458,3 +3472,23 @@ uw_Basis_int n = abs(rand()); return n; } + +void uw_noPostBody(uw_context ctx) { + ctx->hasPostBody = 0; +} + +void uw_postBody(uw_context ctx, uw_Basis_postBody pb) { + ctx->hasPostBody = 1; + ctx->postBody = pb; +} + +int uw_hasPostBody(uw_context ctx) { + return ctx->hasPostBody; +} + +uw_Basis_postBody uw_getPostBody(uw_context ctx) { + if (ctx->hasPostBody) + return ctx->postBody; + else + uw_error(ctx, FATAL, "Asked for POST body when none exists"); +} diff -r faad7d01b200 -r b106ca8200b1 src/cjr_print.sml --- a/src/cjr_print.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/cjr_print.sml Sat Dec 18 10:56:31 2010 -0500 @@ -2246,22 +2246,21 @@ val fields = foldl (fn ((ek, _, _, ts, _, _, _), fields) => case ek of - Link => fields - | Rpc _ => fields - | Action eff => - case List.nth (ts, length ts - 2) of - (TRecord i, loc) => - let - val xts = E.lookupStruct env i - val extra = case eff of - ReadCookieWrite => [sigName xts] - | _ => [] - in - case flatFields extra (TRecord i, loc) of - NONE => raise Fail "CjrPrint: flatFields impossible" - | SOME fields' => List.revAppend (fields', fields) - end - | _ => raise Fail "CjrPrint: Last argument of action isn't record") + Action eff => + (case List.nth (ts, length ts - 2) of + (TRecord i, loc) => + let + val xts = E.lookupStruct env i + val extra = case eff of + ReadCookieWrite => [sigName xts] + | _ => [] + in + case flatFields extra (TRecord i, loc) of + NONE => raise Fail "CjrPrint: flatFields impossible" + | SOME fields' => List.revAppend (fields', fields) + end + | _ => raise Fail "CjrPrint: Last argument of action isn't record") + | _ => fields) [] ps val fields = foldl (fn (xts, fields) => @@ -2544,49 +2543,49 @@ let val (ts, defInputs, inputsVar, fields) = case ek of - Core.Link => (List.take (ts, length ts - 1), string "", string "", NONE) - | Core.Rpc _ => (List.take (ts, length ts - 1), string "", string "", NONE) - | Core.Action _ => - case List.nth (ts, length ts - 2) of - (TRecord i, _) => - let - val xts = E.lookupStruct env i - in - (List.take (ts, length ts - 2), - box [box (map (fn (x, t) => box [p_typ env t, - space, - string "uw_input_", - p_ident x, - string ";", - newline]) xts), - newline, - box (map getInput xts), - string "struct __uws_", - string (Int.toString i), - space, - string "uw_inputs", - space, - string "= {", - newline, - box (map (fn (x, _) => box [string "uw_input_", - p_ident x, - string ",", - newline]) xts), - string "};", - newline], - box [string ",", - space, - string "uw_inputs"], - SOME xts) - end + Core.Action _ => + (case List.nth (ts, length ts - 2) of + (TRecord i, _) => + let + val xts = E.lookupStruct env i + in + (List.take (ts, length ts - 2), + box [box (map (fn (x, t) => box [p_typ env t, + space, + string "uw_input_", + p_ident x, + string ";", + newline]) xts), + newline, + box (map getInput xts), + string "struct __uws_", + string (Int.toString i), + space, + string "uw_inputs", + space, + string "= {", + newline, + box (map (fn (x, _) => box [string "uw_input_", + p_ident x, + string ",", + newline]) xts), + string "};", + newline], + box [string ",", + space, + string "uw_inputs"], + SOME xts) + end - | _ => raise Fail "CjrPrint: Last argument to an action isn't a record" + | _ => raise Fail "CjrPrint: Last argument to an action isn't a record") + | _ => (List.take (ts, length ts - 1), string "", string "", NONE) fun couldWrite ek = case ek of Link => false | Action ef => ef = ReadCookieWrite | Rpc ef => ef = ReadCookieWrite + | Extern ef => ef = ReadCookieWrite val s = case Settings.getUrlPrefix () of @@ -2693,7 +2692,9 @@ space, string "=", space, - unurlify false env t, + case #1 t of + TFfi ("Basis", "postBody") => string "uw_getPostBody(ctx)" + | _ => unurlify false env t, string ";", newline]) ts), defInputs, diff -r faad7d01b200 -r b106ca8200b1 src/corify.sml --- a/src/corify.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/corify.sml Sat Dec 18 10:56:31 2010 -0500 @@ -1011,11 +1011,19 @@ t, tf, e), loc), (L.TFun (t, tf), loc))) ((L.EApp (ef, ea), loc), ranT) args + + val expKind = if List.exists (fn t => + case corifyCon st t of + (L'.CFfi ("Basis", "postBody"), _) => true + | _ => false) args then + L'.Extern L'.ReadCookieWrite + else + L'.Link in ((L.DVal ("wrap_" ^ s, 0, tf, e), loc) :: wds, (fn st => case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of - L'.ENamed n => (L'.DExport (L'.Link, n, false), loc) + L'.ENamed n => (L'.DExport (expKind, n, false), loc) | _ => raise Fail "Corify: Value to export didn't corify properly") :: eds) end diff -r faad7d01b200 -r b106ca8200b1 src/effectize.sml --- a/src/effectize.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/effectize.sml Sat Dec 18 10:56:31 2010 -0500 @@ -168,6 +168,15 @@ else ReadOnly), n, IM.inDomain (pushers, n)), #2 d), evs) + | DExport (Extern _, n, _) => + ((DExport (Extern (if IM.inDomain (writers, n) then + if IM.inDomain (readers, n) then + ReadCookieWrite + else + ReadWrite + else + ReadOnly), n, IM.inDomain (pushers, n)), #2 d), + evs) | _ => (d, evs) val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty, IM.empty) file diff -r faad7d01b200 -r b106ca8200b1 src/elaborate.sml --- a/src/elaborate.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/elaborate.sml Sat Dec 18 10:56:31 2010 -0500 @@ -3834,8 +3834,14 @@ (L'.CModProj (basis, [], "transaction"), loc), t), loc) + + fun normArgs t = + case hnormCon env t of + (L'.TFun (dom, ran), loc) => + (L'.TFun (hnormCon env dom, normArgs ran), loc) + | t' => t' in - (L'.SgiVal (x, n, makeRes t), loc) + (L'.SgiVal (x, n, normArgs (makeRes t)), loc) end | _ => all) | _ => all) diff -r faad7d01b200 -r b106ca8200b1 src/export.sig --- a/src/export.sig Thu Dec 16 18:40:49 2010 -0500 +++ b/src/export.sig Sat Dec 18 10:56:31 2010 -0500 @@ -36,6 +36,7 @@ Link | Action of effect | Rpc of effect + | Extern of effect val p_effect : effect Print.printer val p_export_kind : export_kind Print.printer diff -r faad7d01b200 -r b106ca8200b1 src/export.sml --- a/src/export.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/export.sml Sat Dec 18 10:56:31 2010 -0500 @@ -39,6 +39,7 @@ Link | Action of effect | Rpc of effect + | Extern of effect fun p_effect ef = case ef of @@ -51,5 +52,6 @@ Link => string "link" | Action ef => box [string "action(", p_effect ef, string ")"] | Rpc ef => box [string "rpc(", p_effect ef, string ")"] + | Extern ef => box [string "extern(", p_effect ef, string ")"] end diff -r faad7d01b200 -r b106ca8200b1 src/marshalcheck.sml --- a/src/marshalcheck.sml Thu Dec 16 18:40:49 2010 -0500 +++ b/src/marshalcheck.sml Sat Dec 18 10:56:31 2010 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2009, Adam Chlipala +(* Copyright (c) 2009-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -96,7 +96,10 @@ let fun makeS (t, _) = case t of - TFun (dom, ran) => PS.union (sins cmap dom, makeS ran) + TFun (dom, ran) => + (case #1 dom of + CFfi ("Basis", "postBody") => makeS ran + | _ => PS.union (sins cmap dom, makeS ran)) | _ => PS.empty val s = makeS t in diff -r faad7d01b200 -r b106ca8200b1 tests/post.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/post.ur Sat Dec 18 10:56:31 2010 -0500 @@ -0,0 +1,5 @@ +fun callMe n s pb = return + n = {[n]}
+ s = {[s]}
+ pb : {[postType pb]} = {[postData pb]} + diff -r faad7d01b200 -r b106ca8200b1 tests/post.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/post.urp Sat Dec 18 10:56:31 2010 -0500 @@ -0,0 +1,1 @@ +post diff -r faad7d01b200 -r b106ca8200b1 tests/post.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/post.urs Sat Dec 18 10:56:31 2010 -0500 @@ -0,0 +1,1 @@ +val callMe : int -> string -> postBody -> transaction page