From 431abe6b2d53ed42d5019a5263e8014de8920eb4 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 16 Apr 2009 15:29:39 -0400 Subject: Effectness analysis --- demo/chat.ur | 9 +++-- demo/crud.ur | 2 +- demo/ref.ur | 6 ++- demo/sql.ur | 4 +- demo/tree.ur | 4 +- src/compiler.sig | 2 + src/compiler.sml | 9 ++++- src/core_print.sig | 1 - src/core_print.sml | 8 +--- src/effectize.sig | 32 ++++++++++++++++ src/effectize.sml | 109 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/export.sig | 42 +++++++++++++++++++++ src/export.sml | 14 +++++++ src/mono_print.sml | 2 +- src/sources | 5 +++ 15 files changed, 229 insertions(+), 20 deletions(-) create mode 100644 src/effectize.sig create mode 100644 src/effectize.sml create mode 100644 src/export.sig diff --git a/demo/chat.ur b/demo/chat.ur index 067397eb..52c344be 100644 --- a/demo/chat.ur +++ b/demo/chat.ur @@ -6,7 +6,7 @@ sequence s table t : { Id : int, Title : string, Room : Room.topic } PRIMARY KEY Id -fun chat id = +fun chat id () = r <- oneRow (SELECT t.Title, t.Room FROM t WHERE t.Id = {[id]}); ch <- Room.subscribe r.T.Room; @@ -55,12 +55,13 @@ fun list () = count <- Room.subscribers r.T.Room; return {[r.T.Id]} - {[r.T.Title]} + {[r.T.Title]} {[count]} - [delete] + ) -and delete id = +and delete id () = dml (DELETE FROM t WHERE Id = {[id]}); main () diff --git a/demo/crud.ur b/demo/crud.ur index cf120697..0b937ff1 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -167,7 +167,7 @@ functor Make(M : sig return

Are you sure you want to delete ID #{[id]}?

+ end diff --git a/demo/ref.ur b/demo/ref.ur index 983cc814..b21d40a2 100644 --- a/demo/ref.ur +++ b/demo/ref.ur @@ -6,7 +6,7 @@ structure SR = RefFun.Make(struct type data = string end) -fun main () = +fun mutate () = ir <- IR.new 3; ir' <- IR.new 7; sr <- SR.new "hi"; @@ -24,3 +24,7 @@ fun main () = return {[iv]}, {[iv']}, {[sv]} + +fun main () = return + diff --git a/demo/sql.ur b/demo/sql.ur index bbfec24a..adfc5909 100644 --- a/demo/sql.ur +++ b/demo/sql.ur @@ -5,7 +5,7 @@ fun list () = rows <- queryX (SELECT * FROM t) (fn row => {[row.T.A]} {[row.T.B]} {[row.T.C]} {[row.T.D]} - [delete] + ); return @@ -36,7 +36,7 @@ and add r = {xml} -and delete a = +and delete a () = dml (DELETE FROM t WHERE t.A = {[a]}); xml <- list (); diff --git a/demo/tree.ur b/demo/tree.ur index b02e1f00..d7b0919e 100644 --- a/demo/tree.ur +++ b/demo/tree.ur @@ -8,7 +8,7 @@ open TreeFun.Make(struct end) fun row r = - #{[r.Id]}: {[r.Nam]} [Delete] + #{[r.Id]}: {[r.Nam]} Add child: @@ -30,6 +30,6 @@ and add parent r = dml (INSERT INTO t (Id, Parent, Nam) VALUES ({[id]}, {[parent]}, {[r.Nam]})); main () -and del id = +and del id () = dml (DELETE FROM t WHERE Id = {[id]}); main () diff --git a/src/compiler.sig b/src/compiler.sig index 94dac67a..e685ffe5 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -73,6 +73,7 @@ signature COMPILER = sig val unpoly : (Core.file, Core.file) phase val specialize : (Core.file, Core.file) phase val marshalcheck : (Core.file, Core.file) phase + val effectize : (Core.file, Core.file) phase val monoize : (Core.file, Mono.file) phase val mono_opt : (Mono.file, Mono.file) phase val untangle : (Mono.file, Mono.file) phase @@ -105,6 +106,7 @@ signature COMPILER = sig val toSpecialize : (string, Core.file) transform val toShake3 : (string, Core.file) transform val toMarshalcheck : (string, Core.file) transform + val toEffectize : (string, Core.file) transform val toMonoize : (string, Mono.file) transform val toMono_opt1 : (string, Mono.file) transform val toUntangle : (string, Mono.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 6a43d94e..5223abe9 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -505,12 +505,19 @@ val marshalcheck = { val toMarshalcheck = transform marshalcheck "marshalcheck" o toShake3 +val effectize = { + func = Effective.effectize, + print = CorePrint.p_file CoreEnv.empty +} + +val toEffectize = transform effectize "effectize" o toMarshalcheck + val monoize = { func = Monoize.monoize CoreEnv.empty, print = MonoPrint.p_file MonoEnv.empty } -val toMonoize = transform monoize "monoize" o toMarshalcheck +val toMonoize = transform monoize "monoize" o toEffectize val mono_opt = { func = MonoOpt.optimize, diff --git a/src/core_print.sig b/src/core_print.sig index 64a73a46..b7b41e28 100644 --- a/src/core_print.sig +++ b/src/core_print.sig @@ -34,7 +34,6 @@ signature CORE_PRINT = sig val p_exp : CoreEnv.env -> Core.exp Print.printer val p_decl : CoreEnv.env -> Core.decl Print.printer val p_file : CoreEnv.env -> Core.file Print.printer - val p_export_kind : Core.export_kind Print.printer val debug : bool ref end diff --git a/src/core_print.sml b/src/core_print.sml index 683b1b90..9c1c72cd 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -467,12 +467,6 @@ fun p_vali env (x, n, t, e, s) = p_exp env e] end -fun p_export_kind ck = - case ck of - Link => string "link" - | Action _ => string "action" - | Rpc _ => string "rpc" - fun p_datatype env (x, n, xs, cons) = let val k = (KType, ErrorMsg.dummySpan) @@ -538,7 +532,7 @@ fun p_decl env (dAll as (d, _) : decl) = end | DExport (ek, n) => box [string "export", space, - p_export_kind ek, + Export.p_export_kind ek, space, p_enamed env n, space, diff --git a/src/effectize.sig b/src/effectize.sig new file mode 100644 index 00000000..1b638a31 --- /dev/null +++ b/src/effectize.sig @@ -0,0 +1,32 @@ +(* Copyright (c) 2009, 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 EFFECTIZE = sig + + val effectize : Core.file -> Core.file + +end diff --git a/src/effectize.sml b/src/effectize.sml new file mode 100644 index 00000000..f33b4eb8 --- /dev/null +++ b/src/effectize.sml @@ -0,0 +1,109 @@ +(* Copyright (c) 2009, 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 Effective :> EFFECTIZE = struct + +open Core + +structure U = CoreUtil + +structure IM = IntBinaryMap +structure SS = BinarySetFn(struct + type ord_key = string + val compare = String.compare + end) + +val effectful = ["dml", "nextval", "send"] +val effectful = SS.addList (SS.empty, effectful) + +fun effectize file = + let + fun exp evs e = + case e of + EFfi ("Basis", s) => SS.member (effectful, s) + | EFfiApp ("Basis", s, _) => SS.member (effectful, s) + | ENamed n => IM.inDomain (evs, n) + | EServerCall (n, _, _, _) => IM.inDomain (evs, n) + | _ => false + + fun couldWrite evs = U.Exp.exists {kind = fn _ => false, + con = fn _ => false, + exp = exp evs} + + fun doDecl (d, evs) = + case #1 d of + DVal (x, n, t, e, s) => + (d, if couldWrite evs e then + IM.insert (evs, n, (#2 d, s)) + else + evs) + | DValRec vis => + let + fun oneRound evs = + foldl (fn ((_, n, _, e, s), (changed, evs)) => + if couldWrite evs e andalso not (IM.inDomain (evs, n)) then + (true, IM.insert (evs, n, (#2 d, s))) + else + (changed, evs)) (false, evs) vis + + fun loop evs = + let + val (b, evs) = oneRound evs + in + if b then + loop evs + else + evs + end + in + (d, loop evs) + end + | DExport (Link, n) => + (case IM.find (evs, n) of + NONE => () + | SOME (loc, s) => ErrorMsg.errorAt loc ("A link (" ^ s ^ ") could cause side effects; try implementing it with a form instead"); + (d, evs)) + | DExport (Action _, n) => + ((DExport (Action (if IM.inDomain (evs, n) then + ReadWrite + else + ReadOnly), n), #2 d), + evs) + | DExport (Rpc _, n) => + ((DExport (Rpc (if IM.inDomain (evs, n) then + ReadWrite + else + ReadOnly), n), #2 d), + evs) + | _ => (d, evs) + + val (file, _) = ListUtil.foldlMap doDecl IM.empty file + in + file + end + +end diff --git a/src/export.sig b/src/export.sig new file mode 100644 index 00000000..4c46e751 --- /dev/null +++ b/src/export.sig @@ -0,0 +1,42 @@ +(* Copyright (c) 2009, 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 EXPORT = sig + +datatype effect = + ReadOnly + | ReadWrite + +datatype export_kind = + Link + | Action of effect + | Rpc of effect + +val p_effect : effect Print.printer +val p_export_kind : export_kind Print.printer + +end diff --git a/src/export.sml b/src/export.sml index 4aae9b08..8e3e3331 100644 --- a/src/export.sml +++ b/src/export.sml @@ -27,6 +27,9 @@ structure Export = struct +open Print.PD +open Print + datatype effect = ReadOnly | ReadWrite @@ -36,4 +39,15 @@ datatype export_kind = | Action of effect | Rpc of effect +fun p_effect ef = + case ef of + ReadOnly => string "r" + | ReadWrite => string "rw" + +fun p_export_kind ck = + case ck of + Link => string "link" + | Action ef => box [string "action(", p_effect ef, string ")"] + | Rpc ef => box [string "rpc(", p_effect ef, string ")"] + end diff --git a/src/mono_print.sml b/src/mono_print.sml index 7ad8dada..9e819e5f 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -387,7 +387,7 @@ fun p_decl env (dAll as (d, _) : decl) = | DExport (ek, s, n, ts, t) => box [string "export", space, - CorePrint.p_export_kind ek, + Export.p_export_kind ek, space, p_enamed env n, space, diff --git a/src/sources b/src/sources index 19e4e102..43ee21b3 100644 --- a/src/sources +++ b/src/sources @@ -20,6 +20,8 @@ prim.sig prim.sml datatype_kind.sml + +export.sig export.sml source.sml @@ -114,6 +116,9 @@ rpcify.sml tag.sig tag.sml +effectize.sig +effectize.sml + marshalcheck.sig marshalcheck.sml -- cgit v1.2.3