summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-18 10:56:31 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-18 10:56:31 -0500
commitc71de1db0cf31466bfc5fe7e96021e5d3cba6979 (patch)
tree294baafc0fd3480fdce266c71f27090164d2114c
parentf08b20b1ecc66389fc6a829cf3819b3b38b07c48 (diff)
postBody type
-rw-r--r--doc/manual.tex4
-rw-r--r--include/types.h4
-rw-r--r--include/urweb.h7
-rw-r--r--lib/ur/basis.urs4
-rw-r--r--src/c/request.c5
-rw-r--r--src/c/urweb.c34
-rw-r--r--src/cjr_print.sml107
-rw-r--r--src/corify.sml10
-rw-r--r--src/effectize.sml9
-rw-r--r--src/elaborate.sml8
-rw-r--r--src/export.sig1
-rw-r--r--src/export.sml2
-rw-r--r--src/marshalcheck.sml7
-rw-r--r--tests/post.ur5
-rw-r--r--tests/post.urp1
-rw-r--r--tests/post.urs1
16 files changed, 150 insertions, 59 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 58fbc84d..a8d799d8 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2077,6 +2077,8 @@ $$\begin{array}{rrcll}
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 @@ Ur/Web programs generally mix server- and client-side code in a fairly transpare
\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{<body onload=\{...\}>} 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{<body onload=\{...\}>} 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 --git a/include/types.h b/include/types.h
index e5edab96..2adda753 100644
--- a/include/types.h
+++ b/include/types.h
@@ -40,6 +40,10 @@ typedef struct uw_Basis_file {
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 --git a/include/urweb.h b/include/urweb.h
index 9527fac1..a0decd11 100644
--- a/include/urweb.h
+++ b/include/urweb.h
@@ -221,6 +221,13 @@ uw_Basis_blob uw_Basis_fileData(uw_context, uw_Basis_file);
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 --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 6cd9915e..6fa92a7c 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -737,6 +737,10 @@ val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
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 --git a/src/c/request.c b/src/c/request.c
index bcfec5e9..e51f95ae 100644
--- a/src/c/request.c
+++ b/src/c/request.c
@@ -192,6 +192,9 @@ request_result uw_request(uw_request_context rc, uw_context ctx,
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 @@ request_result uw_request(uw_request_context rc, uw_context ctx,
}
}
}
- else {
+ else if (!uw_hasPostBody(ctx)) {
inputs = is_post ? body : query_string;
if (inputs) {
diff --git a/src/c/urweb.c b/src/c/urweb.c
index 47c6dadf..2b54e87c 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -445,6 +445,9 @@ struct uw_context {
void *logger_data;
uw_logger log_debug;
+ int hasPostBody;
+ uw_Basis_postBody postBody;
+
char error_message[ERROR_BUF_LEN];
};
@@ -507,6 +510,8 @@ uw_context uw_init(void *logger_data, uw_logger log_debug) {
ctx->logger_data = logger_data;
ctx->log_debug = log_debug;
+ ctx->hasPostBody = 0;
+
return ctx;
}
@@ -583,6 +588,7 @@ void uw_reset_keep_error_message(uw_context ctx) {
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 @@ uw_Basis_blob uw_Basis_fileData(uw_context ctx, uw_Basis_file f) {
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 uw_Basis_rand(uw_context ctx) {
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 --git a/src/cjr_print.sml b/src/cjr_print.sml
index df11737e..fbbbc548 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2246,22 +2246,21 @@ fun p_file env (ds, ps) =
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 @@ fun p_file env (ds, ps) =
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 @@ fun p_file env (ds, ps) =
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 --git a/src/corify.sml b/src/corify.sml
index c3a53094..075047a2 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -1011,11 +1011,19 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
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 --git a/src/effectize.sml b/src/effectize.sml
index 7f148476..4601f301 100644
--- a/src/effectize.sml
+++ b/src/effectize.sml
@@ -168,6 +168,15 @@ fun effectize file =
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 --git a/src/elaborate.sml b/src/elaborate.sml
index 008529ea..b1515b6e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3834,8 +3834,14 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
(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 --git a/src/export.sig b/src/export.sig
index 0bbdd1ac..9bcfa0d4 100644
--- a/src/export.sig
+++ b/src/export.sig
@@ -36,6 +36,7 @@ datatype export_kind =
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 --git a/src/export.sml b/src/export.sml
index ad604e16..5d200894 100644
--- a/src/export.sml
+++ b/src/export.sml
@@ -39,6 +39,7 @@ datatype export_kind =
Link
| Action of effect
| Rpc of effect
+ | Extern of effect
fun p_effect ef =
case ef of
@@ -51,5 +52,6 @@ fun p_export_kind ck =
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 --git a/src/marshalcheck.sml b/src/marshalcheck.sml
index de6879ae..c7a274de 100644
--- a/src/marshalcheck.sml
+++ b/src/marshalcheck.sml
@@ -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 @@ fun check file =
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 --git a/tests/post.ur b/tests/post.ur
new file mode 100644
index 00000000..4cee7a45
--- /dev/null
+++ b/tests/post.ur
@@ -0,0 +1,5 @@
+fun callMe n s pb = return <xml><body>
+ n = {[n]}<br/>
+ s = {[s]}<br/>
+ pb : {[postType pb]} = {[postData pb]}
+</body></xml>
diff --git a/tests/post.urp b/tests/post.urp
new file mode 100644
index 00000000..8b1e502f
--- /dev/null
+++ b/tests/post.urp
@@ -0,0 +1 @@
+post
diff --git a/tests/post.urs b/tests/post.urs
new file mode 100644
index 00000000..5d6e6460
--- /dev/null
+++ b/tests/post.urs
@@ -0,0 +1 @@
+val callMe : int -> string -> postBody -> transaction page