summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-04 14:37:19 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-04 14:37:19 -0400
commitfa5e621ba0ba9058334b0063e9dc841dcb61433a (patch)
tree92dc9593a0b4e0f22cbe699ae412b79ddf11570e /src
parent77f1c289bcb9228ca9605913316405c7cb63fecc (diff)
Generated basic dummy Iflow conditions
Diffstat (limited to 'src')
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml9
-rw-r--r--src/iflow.sig58
-rw-r--r--src/iflow.sml422
-rw-r--r--src/settings.sml16
-rw-r--r--src/sources3
6 files changed, 508 insertions, 2 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index 1d575a2b..d3b4e696 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -100,6 +100,7 @@ signature COMPILER = sig
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 @@ signature COMPILER = sig
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 --git a/src/compiler.sml b/src/compiler.sml
index a2fcd346..bb55dfce 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -1071,12 +1071,19 @@ val toMono_shake = transform mono_shake "mono_shake1" o toMono_reduce
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 --git a/src/iflow.sig b/src/iflow.sig
new file mode 100644
index 00000000..8a11a008
--- /dev/null
+++ b/src/iflow.sig
@@ -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 --git a/src/iflow.sml b/src/iflow.sml
new file mode 100644
index 00000000..39b5610f
--- /dev/null
+++ b/src/iflow.sml
@@ -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 --git a/src/settings.sml b/src/settings.sml
index b9056c5b..3d163ca5 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -83,7 +83,21 @@ val effectfulBase = basis ["dml",
"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 --git a/src/sources b/src/sources
index 67c2e45a..ba8dac38 100644
--- a/src/sources
+++ b/src/sources
@@ -169,6 +169,9 @@ untangle.sml
mono_shake.sig
mono_shake.sml
+iflow.sig
+iflow.sml
+
jscomp.sig
jscomp.sml