changeset 1361:7a436b6267ab

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 02fc16faecf3
children fd34210bc3e5
files src/effectize.sml
diffstat 1 files changed, 8 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/effectize.sml	Thu Dec 23 17:46:40 2010 -0500
+++ b/src/effectize.sml	Thu Dec 23 18:07:05 2010 -0500
@@ -66,14 +66,15 @@
                                            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 @@
                          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 @@
                                               (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