Mercurial > urweb

annotate src/effectize.sml @ 1361:7a436b6267ab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix soundness bug in Effectize, where it missed some functions that might have effectful RPCs
author Adam Chlipala <adam@chlipala.net>
date Thu, 23 Dec 2010 18:07:05 -0500
parents b106ca8200b1
children 44a12a321150
rev   line source
adamc@732 1 (* Copyright (c) 2009, 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)
adamc@1020 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@1361 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)
adamc@1020 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
adamc@1104 90 fun doDecl (d, evs as (writers, readers, pushers)) =
adamc@732 91 case #1 d of
adamc@732 92 DVal (x, n, t, e, s) =>
adamc@735 93 (d, (if couldWrite writers e then
adamc@735 94 IM.insert (writers, n, (#2 d, s))
adamc@735 95 else
adamc@735 96 writers,
adamc@735 97 if couldReadCookie readers e then
adamc@735 98 IM.insert (readers, n, (#2 d, s))
adamc@735 99 else
adamc@1104 100 readers,
adam@1361 101 if couldWriteWithRpc writers readers pushers e then
adamc@1104 102 IM.insert (pushers, n, (#2 d, s))
adamc@1104 103 else
adamc@1104 104 pushers))
adamc@732 105 | DValRec vis =>
adamc@732 106 let
adamc@732 107 fun oneRound evs =
adamc@1104 108 foldl (fn ((_, n, _, e, s), (changed, (writers, readers, pushers))) =>
adamc@735 109 let
adamc@735 110 val (changed, writers) =
adamc@735 111 if couldWrite writers e andalso not (IM.inDomain (writers, n)) then
adamc@735 112 (true, IM.insert (writers, n, (#2 d, s)))
adamc@735 113 else
adamc@735 114 (changed, writers)
adamc@735 115
adamc@735 116 val (changed, readers) =
adamc@735 117 if couldReadCookie readers e andalso not (IM.inDomain (readers, n)) then
adamc@735 118 (true, IM.insert (readers, n, (#2 d, s)))
adamc@735 119 else
adamc@735 120 (changed, readers)
adamc@1104 121
adamc@1104 122 val (changed, pushers) =
adam@1361 123 if couldWriteWithRpc writers readers pushers e
adamc@1104 124 andalso not (IM.inDomain (pushers, n)) then
adamc@1104 125 (true, IM.insert (pushers, n, (#2 d, s)))
adamc@1104 126 else
adamc@1104 127 (changed, pushers)
adamc@735 128 in
adamc@1104 129 (changed, (writers, readers, pushers))
adamc@735 130 end) (false, evs) vis
adamc@732 131
adamc@732 132 fun loop evs =
adamc@732 133 let
adamc@732 134 val (b, evs) = oneRound evs
adamc@732 135 in
adamc@732 136 if b then
adamc@732 137 loop evs
adamc@732 138 else
adamc@732 139 evs
adamc@732 140 end
adamc@732 141 in
adamc@1104 142 (d, loop (writers, readers, pushers))
adamc@732 143 end
adamc@1104 144 | DExport (Link, n, _) =>
adamc@735 145 (case IM.find (writers, n) of
adamc@732 146 NONE => ()
adamc@1183 147 | SOME (loc, s) =>
adamc@1183 148 if Settings.isSafeGet s then
adamc@1183 149 ()
adamc@1183 150 else
adamc@1183 151 ErrorMsg.errorAt loc ("A link (" ^ s
adamc@1183 152 ^ ") could cause side effects; try implementing it with a form instead");
adamc@1104 153 ((DExport (Link, n, IM.inDomain (pushers, n)), #2 d), evs))
adamc@1104 154 | DExport (Action _, n, _) =>
adamc@735 155 ((DExport (Action (if IM.inDomain (writers, n) then
adamc@735 156 if IM.inDomain (readers, n) then
adamc@735 157 ReadCookieWrite
adamc@735 158 else
adamc@735 159 ReadWrite
adamc@732 160 else
adamc@1104 161 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
adamc@732 162 evs)
adamc@1104 163 | DExport (Rpc _, n, _) =>
adamc@735 164 ((DExport (Rpc (if IM.inDomain (writers, n) then
adamc@735 165 if IM.inDomain (readers, n) then
adamc@735 166 ReadCookieWrite
adamc@735 167 else
adamc@735 168 ReadWrite
adamc@732 169 else
adamc@1104 170 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
adamc@732 171 evs)
adam@1347 172 | DExport (Extern _, n, _) =>
adam@1347 173 ((DExport (Extern (if IM.inDomain (writers, n) then
adam@1347 174 if IM.inDomain (readers, n) then
adam@1347 175 ReadCookieWrite
adam@1347 176 else
adam@1347 177 ReadWrite
adam@1347 178 else
adam@1347 179 ReadOnly), n, IM.inDomain (pushers, n)), #2 d),
adam@1347 180 evs)
adamc@732 181 | _ => (d, evs)
adamc@732 182
adamc@1104 183 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty, IM.empty) file
adamc@732 184 in
adamc@732 185 file
adamc@732 186 end
adamc@732 187
adamc@732 188 end