# HG changeset patch # User Adam Chlipala # Date 1270406239 14400 # Node ID 5eac14322548429744dd490806047537c4fa1524 # Parent c316ca3c9ec6980311eeb23e09b65fc99886a6df Generated basic dummy Iflow conditions diff -r c316ca3c9ec6 -r 5eac14322548 src/compiler.sig --- a/src/compiler.sig Sun Apr 04 12:29:34 2010 -0400 +++ b/src/compiler.sig Sun Apr 04 14:37:19 2010 -0400 @@ -100,6 +100,7 @@ val untangle : (Mono.file, Mono.file) phase val mono_reduce : (Mono.file, Mono.file) phase val mono_shake : (Mono.file, Mono.file) phase + val iflow : (Mono.file, Mono.file) phase val jscomp : (Mono.file, Mono.file) phase val fuse : (Mono.file, Mono.file) phase val pathcheck : (Mono.file, Mono.file) phase @@ -143,6 +144,7 @@ val toMono_reduce : (string, Mono.file) transform val toMono_shake : (string, Mono.file) transform val toMono_opt2 : (string, Mono.file) transform + val toIflow : (string, Mono.file) transform val toJscomp : (string, Mono.file) transform val toMono_opt3 : (string, Mono.file) transform val toFuse : (string, Mono.file) transform diff -r c316ca3c9ec6 -r 5eac14322548 src/compiler.sml --- a/src/compiler.sml Sun Apr 04 12:29:34 2010 -0400 +++ b/src/compiler.sml Sun Apr 04 14:37:19 2010 -0400 @@ -1071,12 +1071,19 @@ val toMono_opt2 = transform mono_opt "mono_opt2" o toMono_shake +val iflow = { + func = (fn file => (Iflow.check file; file)), + print = MonoPrint.p_file MonoEnv.empty +} + +val toIflow = transform iflow "iflow" o toMono_opt2 + val jscomp = { func = JsComp.process, print = MonoPrint.p_file MonoEnv.empty } -val toJscomp = transform jscomp "jscomp" o toMono_opt2 +val toJscomp = transform jscomp "jscomp" o toIflow val toMono_opt3 = transform mono_opt "mono_opt3" o toJscomp diff -r c316ca3c9ec6 -r 5eac14322548 src/iflow.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/iflow.sig Sun Apr 04 14:37:19 2010 -0400 @@ -0,0 +1,58 @@ +(* Copyright (c) 2010, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature IFLOW = sig + + type lvar = int + + datatype exp = + Const of Prim.t + | Var of int + | Lvar of int + | Func of string * exp list + | Recd of (string * exp) list + | Proj of exp * string + | Finish + + datatype reln = + Sql of string + | Eq + + datatype prop = + True + | False + | Unknown + | And of prop * prop + | Or of prop * prop + | Reln of reln * exp list + | Select of int * lvar * lvar * prop * exp + + exception Summaries of (string * exp * prop * (exp * prop) list) list + + val check : Mono.file -> unit + +end diff -r c316ca3c9ec6 -r 5eac14322548 src/iflow.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/iflow.sml Sun Apr 04 14:37:19 2010 -0400 @@ -0,0 +1,422 @@ +(* Copyright (c) 2010, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Iflow :> IFLOW = struct + +open Mono + +structure SS = BinarySetFn(struct + type ord_key = string + val compare = String.compare + end) + +val writers = ["htmlifyInt_w", + "htmlifyFloat_w", + "htmlifyString_w", + "htmlifyBool_w", + "htmlifyTime_w", + "attrifyInt_w", + "attrifyFloat_w", + "attrifyString_w", + "attrifyChar_w", + "urlifyInt_w", + "urlifyFloat_w", + "urlifyString_w", + "urlifyBool_w"] + +val writers = SS.addList (SS.empty, writers) + +type lvar = int + +datatype exp = + Const of Prim.t + | Var of int + | Lvar of lvar + | Func of string * exp list + | Recd of (string * exp) list + | Proj of exp * string + | Finish + +datatype reln = + Sql of string + | Eq + +datatype prop = + True + | False + | Unknown + | And of prop * prop + | Or of prop * prop + | Reln of reln * exp list + | Select of int * lvar * lvar * prop * exp + +local + val count = ref 0 +in +fun newLvar () = + let + val n = !count + in + count := n + 1; + n + end +end + +fun subExp (v, lv) = + let + fun sub e = + case e of + Const _ => e + | Var v' => if v' = v then Lvar lv else e + | Lvar _ => e + | Func (f, es) => Func (f, map sub es) + | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes) + | Proj (e, s) => Proj (sub e, s) + | Finish => Finish + in + sub + end + +fun subProp (v, lv) = + let + fun sub p = + case p of + True => p + | False => p + | Unknown => p + | And (p1, p2) => And (sub p1, sub p2) + | Or (p1, p2) => Or (sub p1, sub p2) + | Reln (r, es) => Reln (r, map (subExp (v, lv)) es) + | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e) + in + sub + end + +fun eq' (e1, e2) = + case (e1, e2) of + (Const p1, Const p2) => Prim.equal (p1, p2) + | (Var n1, Var n2) => n1 = n2 + | (Lvar n1, Lvar n2) => n1 = n2 + | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2) + | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2) + | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2 + | (Finish, Finish) => true + | _ => false + +fun isKnown e = + case e of + Const _ => true + | Func (_, es) => List.all isKnown es + | Recd xes => List.all (isKnown o #2) xes + | Proj (e, _) => isKnown e + | _ => false + +fun isFinish e = + case e of + Finish => true + | _ => false + +fun simplify e = + case e of + Const _ => e + | Var _ => e + | Lvar _ => e + | Func (f, es) => + let + val es = map simplify es + in + if List.exists isFinish es then + Finish + else + Func (f, es) + end + | Recd xes => + let + val xes = map (fn (x, e) => (x, simplify e)) xes + in + if List.exists (isFinish o #2) xes then + Finish + else + Recd xes + end + | Proj (e, s) => + (case simplify e of + Recd xes => + getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes) + | e' => + if isFinish e' then + Finish + else + Proj (e', s)) + | Finish => Finish + +fun eq (e1, e2) = eq' (simplify e1, simplify e2) + +fun decomp or = + let + fun decomp p k = + case p of + True => k [] + | False => true + | Unknown => k [] + | And (p1, p2) => + decomp p1 (fn ps1 => + decomp p2 (fn ps2 => + k (ps1 @ ps2))) + | Or (p1, p2) => + or (decomp p1 k, fn () => decomp p2 k) + | Reln x => k [x] + | Select _ => k [] + in + decomp + end + +fun rimp ((r1 : reln, es1), (r2, es2)) = + r1 = r2 andalso ListPair.allEq eq (es1, es2) + +fun imp (p1, p2) = + decomp (fn (e1, e2) => e1 andalso e2 ()) p1 + (fn hyps => + decomp (fn (e1, e2) => e1 orelse e2 ()) p2 + (fn goals => + List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals)) + +fun patCon pc = + case pc of + PConVar n => "C" ^ Int.toString n + | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c + +exception Summaries of (string * exp * prop * (exp * prop) list) list + +datatype chunk = + String of string + | Exp of Mono.exp + +fun chunkify e = + case #1 e of + EPrim (Prim.String s) => [String s] + | EStrcat (e1, e2) => chunkify e1 @ chunkify e2 + | _ => [Exp e] + +fun queryProp rv e = + let + fun query chs = + case chs of + [] => raise Fail "Iflow: Empty query" + | Exp _ :: _ => Unknown + | String "" :: chs => query chs + | String s :: chs => True + in + query (chunkify e) + end + +fun evalExp env (e : Mono.exp, st as (nv, p, sent)) = + let + fun default () = + (Var nv, (nv+1, p, sent)) + + fun addSent (p, e, sent) = + if isKnown e then + sent + else + (e, p) :: sent + in + case #1 e of + EPrim p => (Const p, st) + | ERel n => (List.nth (env, n), st) + | ENamed _ => default () + | ECon (_, pc, NONE) => (Func (patCon pc, []), st) + | ECon (_, pc, SOME e) => + let + val (e, st) = evalExp env (e, st) + in + (Func (patCon pc, [e]), st) + end + | ENone _ => (Func ("None", []), st) + | ESome (_, e) => + let + val (e, st) = evalExp env (e, st) + in + (Func ("Some", [e]), st) + end + | EFfi _ => default () + | EFfiApp (m, s, es) => + if m = "Basis" andalso SS.member (writers, s) then + let + val (es, st) = ListUtil.foldlMap (evalExp env) st es + in + (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es)) + end + else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then + default () + else + let + val (es, st) = ListUtil.foldlMap (evalExp env) st es + in + (Func (m ^ "." ^ s, es), st) + end + | EApp _ => default () + | EAbs _ => default () + | EUnop (s, e1) => + let + val (e1, st) = evalExp env (e1, st) + in + (Func (s, [e1]), st) + end + | EBinop (s, e1, e2) => + let + val (e1, st) = evalExp env (e1, st) + val (e2, st) = evalExp env (e2, st) + in + (Func (s, [e1, e2]), st) + end + | ERecord xets => + let + val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) => + let + val (e, st) = evalExp env (e, st) + in + ((x, e), st) + end) st xets + in + (Recd xes, st) + end + | EField (e, s) => + let + val (e, st) = evalExp env (e, st) + in + (Proj (e, s), st) + end + | ECase _ => default () + | EStrcat (e1, e2) => + let + val (e1, st) = evalExp env (e1, st) + val (e2, st) = evalExp env (e2, st) + in + (Func ("cat", [e1, e2]), st) + end + | EError _ => (Finish, st) + | EReturnBlob {blob = b, mimeType = m, ...} => + let + val (b, st) = evalExp env (b, st) + val (m, st) = evalExp env (m, st) + in + (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent)))) + end + | ERedirect (e, _) => + let + val (e, st) = evalExp env (e, st) + in + (Finish, (#1 st, p, addSent (#2 st, e, sent))) + end + | EWrite e => + let + val (e, st) = evalExp env (e, st) + in + (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent))) + end + | ESeq (e1, e2) => + let + val (_, st) = evalExp env (e1, st) + in + evalExp env (e2, st) + end + | ELet (_, _, e1, e2) => + let + val (e1, st) = evalExp env (e1, st) + in + evalExp (e1 :: env) (e2, st) + end + | EClosure (n, es) => + let + val (es, st) = ListUtil.foldlMap (evalExp env) st es + in + (Func ("Cl" ^ Int.toString n, es), st) + end + + | EQuery {query = q, body = b, initial = i, ...} => + let + val (_, st) = evalExp env (q, st) + val (i, st) = evalExp env (i, st) + + val r = #1 st + val acc = #1 st + 1 + val st' = (#1 st + 2, #2 st, #3 st) + + val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') + + val r' = newLvar () + val acc' = newLvar () + val qp = queryProp r' q + + val doSubExp = subExp (r, r') o subExp (acc, acc') + val doSubProp = subProp (r, r') o subProp (acc, acc') + + val p = doSubProp (#2 st') + val p = And (p, qp) + val p = Select (r, r', acc', p, doSubExp b) + in + (Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st'))) + end + | EDml _ => default () + | ENextval _ => default () + | ESetval _ => default () + + | EUnurlify _ => default () + | EJavaScript _ => default () + | ESignalReturn _ => default () + | ESignalBind _ => default () + | ESignalSource _ => default () + | EServerCall _ => default () + | ERecv _ => default () + | ESleep _ => default () + | ESpawn _ => default () + end + +fun check file = + let + fun decl ((d, _), summaries) = + case d of + DVal (x, _, _, e, _) => + let + fun deAbs (e, env, nv) = + case #1 e of + EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1) + | _ => (e, env, nv) + + val (e, env, nv) = deAbs (e, [], 0) + + val (e, (_, p, sent)) = evalExp env (e, (nv, True, [])) + in + (x, e, p, sent) :: summaries + end + | _ => summaries + in + raise Summaries (foldl decl [] file) + end + +end diff -r c316ca3c9ec6 -r 5eac14322548 src/settings.sml --- a/src/settings.sml Sun Apr 04 12:29:34 2010 -0400 +++ b/src/settings.sml Sun Apr 04 14:37:19 2010 -0400 @@ -83,7 +83,21 @@ "set_cookie", "clear_cookie", "new_channel", - "send"] + "send", + "htmlifyInt_w", + "htmlifyFloat_w", + "htmlifyString_w", + "htmlifyBool_w", + "htmlifyTime_w", + "attrifyInt_w", + "attrifyFloat_w", + "attrifyString_w", + "attrifyChar_w", + "urlifyInt_w", + "urlifyFloat_w", + "urlifyString_w", + "urlifyBool_w", + "urlifyChannel_w"] val effectful = ref effectfulBase fun setEffectful ls = effectful := S.addList (effectfulBase, ls) diff -r c316ca3c9ec6 -r 5eac14322548 src/sources --- a/src/sources Sun Apr 04 12:29:34 2010 -0400 +++ b/src/sources Sun Apr 04 14:37:19 2010 -0400 @@ -169,6 +169,9 @@ mono_shake.sig mono_shake.sml +iflow.sig +iflow.sml + jscomp.sig jscomp.sml diff -r c316ca3c9ec6 -r 5eac14322548 tests/policy.ur --- a/tests/policy.ur Sun Apr 04 12:29:34 2010 -0400 +++ b/tests/policy.ur Sun Apr 04 14:37:19 2010 -0400 @@ -1,3 +1,13 @@ -table fruit : { Id : int, Nam : string, Weight : float } +table fruit : { Id : int, Nam : string, Weight : float, Secret : string } -policy query_policy (SELECT * FROM fruit) +policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight FROM fruit) + +fun main () = + xml <- queryX (SELECT fruit.Nam + FROM fruit + ORDER BY fruit.Nam) + (fn x =>
  • {[x.Fruit.Nam]}
    • ); + + return + {xml} + diff -r c316ca3c9ec6 -r 5eac14322548 tests/policy.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/policy.urs Sun Apr 04 14:37:19 2010 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page