adam@1848
|
1 (* Copyright (c) 2009-2010, 2013, Adam Chlipala
|
adamc@732
|
2 * All rights reserved.
|
adamc@732
|
3 *
|
adamc@732
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@732
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@732
|
6 *
|
adamc@732
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@732
|
8 * this list of conditions and the following disclaimer.
|
adamc@732
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@732
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@732
|
11 * and/or other materials provided with the distribution.
|
adamc@732
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@732
|
13 * derived from this software without specific prior written permission.
|
adamc@732
|
14 *
|
adamc@732
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@732
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@732
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@732
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@732
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@732
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@732
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@732
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@732
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@732
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@732
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@732
|
26 *)
|
adamc@732
|
27
|
adamc@732
|
28 structure Effective :> EFFECTIZE = struct
|
adamc@732
|
29
|
adamc@732
|
30 open Core
|
adamc@732
|
31
|
adamc@732
|
32 structure U = CoreUtil
|
adamc@732
|
33
|
adamc@732
|
34 structure IM = IntBinaryMap
|
adamc@732
|
35 structure SS = BinarySetFn(struct
|
adamc@732
|
36 type ord_key = string
|
adamc@732
|
37 val compare = String.compare
|
adamc@732
|
38 end)
|
adamc@732
|
39
|
adamc@765
|
40 fun effectful x = Settings.isEffectful x andalso not (Settings.isClientOnly x)
|
adamc@732
|
41
|
adamc@732
|
42 fun effectize file =
|
adamc@732
|
43 let
|
adamc@782
|
44 fun expOnload evs e =
|
adamc@782
|
45 case e of
|
adamc@782
|
46 EFfi f => effectful f
|
adamc@782
|
47 | EFfiApp (m, x, _) => effectful (m, x)
|
adamc@782
|
48 | ENamed n => IM.inDomain (evs, n)
|
adam@1848
|
49 | EServerCall (n, _, _, _) => IM.inDomain (evs, n)
|
adamc@782
|
50 | _ => false
|
adamc@782
|
51
|
adamc@782
|
52 fun couldWriteOnload evs = U.Exp.exists {kind = fn _ => false,
|
adamc@782
|
53 con = fn _ => false,
|
adamc@782
|
54 exp = expOnload evs}
|
adamc@782
|
55
|
adamc@732
|
56 fun exp evs e =
|
adamc@732
|
57 case e of
|
adamc@765
|
58 EFfi f => effectful f
|
adamc@765
|
59 | EFfiApp (m, x, _) => effectful (m, x)
|
adamc@732
|
60 | ENamed n => IM.inDomain (evs, n)
|
adamc@782
|
61 | ERecord xets => List.exists (fn ((CName "Onload", _), e, _) => couldWriteOnload evs e
|
adamc@782
|
62 | _ => false) xets
|
adamc@732
|
63 | _ => false
|
adamc@732
|
64
|
adamc@732
|
65 fun couldWrite evs = U.Exp.exists {kind = fn _ => false,
|
adamc@732
|
66 con = fn _ => false,
|
adamc@732
|
67 exp = exp evs}
|
adamc@732
|
68
|
adam@1361
|
69 fun exp writers readers pushers e =
|
adamc@1104
|
70 case e of
|
adam@1361
|
71 ENamed n => IM.inDomain (pushers, n)
|
adam@1848
|
72 | EServerCall (n, _, _, _) => IM.inDomain (writers, n) andalso IM.inDomain (readers, n)
|
adamc@1104
|
73 | _ => false
|
adamc@1104
|
74
|
adam@1361
|
75 fun couldWriteWithRpc writers readers pushers = U.Exp.exists {kind = fn _ => false,
|
adam@1361
|
76 con = fn _ => false,
|
adam@1361
|
77 exp = exp writers readers pushers}
|
adamc@1104
|
78
|
adamc@735
|
79 fun exp evs e =
|
adamc@735
|
80 case e of
|
adamc@735
|
81 EFfi ("Basis", "getCookie") => true
|
adamc@735
|
82 | ENamed n => IM.inDomain (evs, n)
|
adam@1848
|
83 | EServerCall (n, _, _, _) => IM.inDomain (evs, n)
|
adamc@735
|
84 | _ => false
|
adamc@735
|
85
|
adamc@735
|
86 fun couldReadCookie evs = U.Exp.exists {kind = fn _ => false,
|
adamc@735
|
87 con = fn _ => false,
|
adamc@735
|
88 exp = exp evs}
|
adamc@735
|
89
|
adam@1433
|
90 val dejs = U.Exp.map {kind = fn x => x,
|
adam@1433
|
91 con = fn c => c,
|
adam@1433
|
92 exp = fn ERecord xets => ERecord (List.filter (fn ((CName x, _), _ , _) => x = "Onload" orelse not (String.isPrefix "On" x)
|
adam@1433
|
93 | _ => true) xets)
|
adam@1433
|
94 | e => e}
|
adam@1433
|
95
|
adamc@1104
|
96 fun doDecl (d, evs as (writers, readers, pushers)) =
|
adamc@732
|
97 case #1 d of
|
adamc@732
|
98 DVal (x, n, t, e, s) =>
|
adam@1433
|
99 let
|
adam@1438
|
100 val e' = dejs e
|
adam@1433
|
101 in
|
adam@1438
|
102 (d, (if couldWrite writers e' then
|
adam@1433
|
103 IM.insert (writers, n, (#2 d, s))
|
adam@1433
|
104 else
|
adam@1433
|
105 writers,
|
adam@1438
|
106 if couldReadCookie readers e' then
|
adam@1433
|
107 IM.insert (readers, n, (#2 d, s))
|
adam@1433
|
108 else
|
adam@1433
|
109 readers,
|
adam@1433
|
110 if couldWriteWithRpc writers readers pushers e then
|
adam@1433
|
111 IM.insert (pushers, n, (#2 d, s))
|
adam@1433
|
112 else
|
adam@1433
|
113 pushers))
|
adam@1433
|
114 end
|
adamc@732
|
115 | DValRec vis =>
|
adamc@732
|
116 let
|
adamc@732
|
117 fun oneRound evs =
|
adamc@1104
|
118 foldl (fn ((_, n, _, e, s), (changed, (writers, readers, pushers))) =>
|
adamc@735
|
119 let
|
adam@1438
|
120 val e' = dejs e
|
adam@1433
|
121
|
adamc@735
|
122 val (changed, writers) =
|
adam@1438
|
123 if couldWrite writers e' andalso not (IM.inDomain (writers, n)) then
|
adamc@735
|
124 (true, IM.insert (writers, n, (#2 d, s)))
|
adamc@735
|
125 else
|
adamc@735
|
126 (changed, writers)
|
adamc@735
|
127
|
adamc@735
|
128 val (changed, readers) =
|
adam@1438
|
129 if couldReadCookie readers e' andalso not (IM.inDomain (readers, n)) then
|
adamc@735
|
130 (true, IM.insert (readers, n, (#2 d, s)))
|
adamc@735
|
131 else
|
adamc@735
|
132 (changed, readers)
|
adamc@1104
|
133
|
adamc@1104
|
134 val (changed, pushers) =
|
adam@1361
|
135 if couldWriteWithRpc writers readers pushers e
|
adamc@1104
|
136 andalso not (IM.inDomain (pushers, n)) then
|
adamc@1104
|
137 (true, IM.insert (pushers, n, (#2 d, s)))
|
adamc@1104
|
138 else
|
adamc@1104
|
139 (changed, pushers)
|
adamc@735
|
140 in
|
adamc@1104
|
141 (changed, (writers, readers, pushers))
|
adamc@735
|
142 end) (false, evs) vis
|
adamc@732
|
143
|
adamc@732
|
144 fun loop evs =
|
adamc@732
|
145 let
|
adamc@732
|
146 val (b, evs) = oneRound evs
|
adamc@732
|
147 in
|
adamc@732
|
148 if b then
|
adamc@732
|
149 loop evs
|
adamc@732
|
150 else
|
adamc@732
|
151 evs
|
adamc@732
|
152 end
|
adamc@732
|
153 in
|
adamc@1104
|
154 (d, loop (writers, readers, pushers))
|
adamc@732
|
155 end
|
adam@1936
|
156 | DExport (Link _, n, t) =>
|
adamc@735
|
157 (case IM.find (writers, n) of
|
adamc@732
|
158 NONE => ()
|
adamc@1183
|
159 | SOME (loc, s) =>
|
adamc@1183
|
160 if Settings.isSafeGet s then
|
adamc@1183
|
161 ()
|
adamc@1183
|
162 else
|
adam@1860
|
163 ErrorMsg.errorAt loc ("A handler (URI prefix \"" ^ s
|
adam@1860
|
164 ^ "\") accessible via GET could cause side effects; try accessing it only via forms, removing it from the signature of the main program module, or whitelisting it with the 'safeGet' .urp directive");
|
adam@1936
|
165 ((DExport (Link (if IM.inDomain (writers, n) then
|
adam@1936
|
166 if IM.inDomain (readers, n) then
|
adam@1936
|
167 ReadCookieWrite
|
adam@1936
|
168 else
|
adam@1936
|
169 ReadWrite
|
adam@1936
|
170 else
|
adam@1936
|
171 ReadOnly), n, IM.inDomain (pushers, n)), #2 d), evs))
|
adamc@1104
|
172 | DExport (Action _, n, _) =>
|
adamc@735
|
173 ((DExport (Action (if IM.inDomain (writers, n) then
|
adamc@735
|
174 if IM.inDomain (readers, n) then
|
adamc@735
|
175 ReadCookieWrite
|
adamc@735
|
176 else
|
adamc@735
|
177 ReadWrite
|
adamc@732
|
178 else
|
adamc@1104
|
179 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
|
adamc@732
|
180 evs)
|
adamc@1104
|
181 | DExport (Rpc _, n, _) =>
|
adamc@735
|
182 ((DExport (Rpc (if IM.inDomain (writers, n) then
|
adamc@735
|
183 if IM.inDomain (readers, n) then
|
adamc@735
|
184 ReadCookieWrite
|
adamc@735
|
185 else
|
adamc@735
|
186 ReadWrite
|
adamc@732
|
187 else
|
adamc@1104
|
188 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
|
adamc@732
|
189 evs)
|
adam@1347
|
190 | DExport (Extern _, n, _) =>
|
adam@1347
|
191 ((DExport (Extern (if IM.inDomain (writers, n) then
|
adam@1347
|
192 if IM.inDomain (readers, n) then
|
adam@1347
|
193 ReadCookieWrite
|
adam@1347
|
194 else
|
adam@1347
|
195 ReadWrite
|
adam@1347
|
196 else
|
adam@1347
|
197 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
|
adam@1347
|
198 evs)
|
adamc@732
|
199 | _ => (d, evs)
|
adamc@732
|
200
|
adamc@1104
|
201 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty, IM.empty) file
|
adamc@732
|
202 in
|
adamc@732
|
203 file
|
adamc@732
|
204 end
|
adamc@732
|
205
|
adamc@732
|
206 end
|