diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-12-23 18:07:05 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-12-23 18:07:05 -0500 |
| commit | f7fb87aa9fdff765a3b0c862a3d262968b2977f1 (patch) | |
| tree | 2b2550c3f5233ff4da0421b0c0bdd602b43f0fc9 /src/effectize.sml | |
| parent | 38d3bc508b3b882e81599bdb0e1d4a2572c23dd0 (diff) | |
Fix soundness bug in Effectize, where it missed some functions that might have effectful RPCs
Diffstat (limited to 'src/effectize.sml')
| -rw-r--r-- | src/effectize.sml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/effectize.sml b/src/effectize.sml index 4601f301..aba8bc58 100644 --- a/src/effectize.sml +++ b/src/effectize.sml @@ -66,14 +66,15 @@ fun effectize file = con = fn _ => false, exp = exp evs} - fun exp writers readers e = + fun exp writers readers pushers e = case e of - EServerCall (n, _, _) => IM.inDomain (writers, n) andalso IM.inDomain (readers, n) + ENamed n => IM.inDomain (pushers, n) + | EServerCall (n, _, _) => IM.inDomain (writers, n) andalso IM.inDomain (readers, n) | _ => false - fun couldWriteWithRpc writers readers = U.Exp.exists {kind = fn _ => false, - con = fn _ => false, - exp = exp writers readers} + fun couldWriteWithRpc writers readers pushers = U.Exp.exists {kind = fn _ => false, + con = fn _ => false, + exp = exp writers readers pushers} fun exp evs e = case e of @@ -97,7 +98,7 @@ fun effectize file = IM.insert (readers, n, (#2 d, s)) else readers, - if couldWriteWithRpc writers readers e then + if couldWriteWithRpc writers readers pushers e then IM.insert (pushers, n, (#2 d, s)) else pushers)) @@ -119,7 +120,7 @@ fun effectize file = (changed, readers) val (changed, pushers) = - if couldWriteWithRpc writers readers e + if couldWriteWithRpc writers readers pushers e andalso not (IM.inDomain (pushers, n)) then (true, IM.insert (pushers, n, (#2 d, s))) else |