comparison src/effectize.sml @ 732:5819fb63c93a

Effectness analysis
author Adam Chlipala <adamc@hcoop.net>
date Thu, 16 Apr 2009 15:29:39 -0400
parents
children 5ccb67665d05
comparison
equal deleted inserted replaced
731:e0dd85ea58e1 732:5819fb63c93a
1 (* Copyright (c) 2009, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure Effective :> EFFECTIZE = struct
29
30 open Core
31
32 structure U = CoreUtil
33
34 structure IM = IntBinaryMap
35 structure SS = BinarySetFn(struct
36 type ord_key = string
37 val compare = String.compare
38 end)
39
40 val effectful = ["dml", "nextval", "send"]
41 val effectful = SS.addList (SS.empty, effectful)
42
43 fun effectize file =
44 let
45 fun exp evs e =
46 case e of
47 EFfi ("Basis", s) => SS.member (effectful, s)
48 | EFfiApp ("Basis", s, _) => SS.member (effectful, s)
49 | ENamed n => IM.inDomain (evs, n)
50 | EServerCall (n, _, _, _) => IM.inDomain (evs, n)
51 | _ => false
52
53 fun couldWrite evs = U.Exp.exists {kind = fn _ => false,
54 con = fn _ => false,
55 exp = exp evs}
56
57 fun doDecl (d, evs) =
58 case #1 d of
59 DVal (x, n, t, e, s) =>
60 (d, if couldWrite evs e then
61 IM.insert (evs, n, (#2 d, s))
62 else
63 evs)
64 | DValRec vis =>
65 let
66 fun oneRound evs =
67 foldl (fn ((_, n, _, e, s), (changed, evs)) =>
68 if couldWrite evs e andalso not (IM.inDomain (evs, n)) then
69 (true, IM.insert (evs, n, (#2 d, s)))
70 else
71 (changed, evs)) (false, evs) vis
72
73 fun loop evs =
74 let
75 val (b, evs) = oneRound evs
76 in
77 if b then
78 loop evs
79 else
80 evs
81 end
82 in
83 (d, loop evs)
84 end
85 | DExport (Link, n) =>
86 (case IM.find (evs, n) of
87 NONE => ()
88 | SOME (loc, s) => ErrorMsg.errorAt loc ("A link (" ^ s ^ ") could cause side effects; try implementing it with a form instead");
89 (d, evs))
90 | DExport (Action _, n) =>
91 ((DExport (Action (if IM.inDomain (evs, n) then
92 ReadWrite
93 else
94 ReadOnly), n), #2 d),
95 evs)
96 | DExport (Rpc _, n) =>
97 ((DExport (Rpc (if IM.inDomain (evs, n) then
98 ReadWrite
99 else
100 ReadOnly), n), #2 d),
101 evs)
102 | _ => (d, evs)
103
104 val (file, _) = ListUtil.foldlMap doDecl IM.empty file
105 in
106 file
107 end
108
109 end