# HG changeset patch # User Adam Chlipala # Date 1293145625 18000 # Node ID 7a436b6267ab763ca659add58407b088c69e9fb2 # Parent 02fc16faecf30702655e0f9cdb612df1c7eacc47 Fix soundness bug in Effectize, where it missed some functions that might have effectful RPCs diff -r 02fc16faecf3 -r 7a436b6267ab src/effectize.sml --- 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