Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
1360:02fc16faecf3 1361:7a436b6267ab
64 64
65 fun couldWrite evs = U.Exp.exists {kind = fn _ => false, 65 fun couldWrite evs = U.Exp.exists {kind = fn _ => false,
66 con = fn _ => false, 66 con = fn _ => false,
67 exp = exp evs} 67 exp = exp evs}
68 68
69 fun exp writers readers e = 69 fun exp writers readers pushers e =
70 case e of 70 case e of
71 EServerCall (n, _, _) => IM.inDomain (writers, n) andalso IM.inDomain (readers, n) 71 ENamed n => IM.inDomain (pushers, n)
72 | EServerCall (n, _, _) => IM.inDomain (writers, n) andalso IM.inDomain (readers, n)
72 | _ => false 73 | _ => false
73 74
74 fun couldWriteWithRpc writers readers = U.Exp.exists {kind = fn _ => false, 75 fun couldWriteWithRpc writers readers pushers = U.Exp.exists {kind = fn _ => false,
75 con = fn _ => false, 76 con = fn _ => false,
76 exp = exp writers readers} 77 exp = exp writers readers pushers}
77 78
78 fun exp evs e = 79 fun exp evs e =
79 case e of 80 case e of
80 EFfi ("Basis", "getCookie") => true 81 EFfi ("Basis", "getCookie") => true
81 | ENamed n => IM.inDomain (evs, n) 82 | ENamed n => IM.inDomain (evs, n)
95 writers, 96 writers,
96 if couldReadCookie readers e then 97 if couldReadCookie readers e then
97 IM.insert (readers, n, (#2 d, s)) 98 IM.insert (readers, n, (#2 d, s))
98 else 99 else
99 readers, 100 readers,
100 if couldWriteWithRpc writers readers e then 101 if couldWriteWithRpc writers readers pushers e then
101 IM.insert (pushers, n, (#2 d, s)) 102 IM.insert (pushers, n, (#2 d, s))
102 else 103 else
103 pushers)) 104 pushers))
104 | DValRec vis => 105 | DValRec vis =>
105 let 106 let
117 (true, IM.insert (readers, n, (#2 d, s))) 118 (true, IM.insert (readers, n, (#2 d, s)))
118 else 119 else
119 (changed, readers) 120 (changed, readers)
120 121
121 val (changed, pushers) = 122 val (changed, pushers) =
122 if couldWriteWithRpc writers readers e 123 if couldWriteWithRpc writers readers pushers e
123 andalso not (IM.inDomain (pushers, n)) then 124 andalso not (IM.inDomain (pushers, n)) then
124 (true, IM.insert (pushers, n, (#2 d, s))) 125 (true, IM.insert (pushers, n, (#2 d, s)))
125 else 126 else
126 (changed, pushers) 127 (changed, pushers)
127 in 128 in