Extend ScriptCheck to take RPCs into account

5 files changed, 142 insertions, 13 deletions

diff --git a/src/scriptcheck.sml b/src/scriptcheck.sml
index 4bc2a4cf..0d30ebcb 100644
--- a/src/scriptcheck.sml
+++ b/src/scriptcheck.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2009, Adam Chlipala
+(* Copyright (c) 2009, 2014, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -29,6 +29,10 @@ structure ScriptCheck :> SCRIPT_CHECK = struct
 
 open Mono
 
+structure SM = BinaryMapFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
 structure SS = BinarySetFn(struct
                            type ord_key = string
                            val compare = String.compare
@@ -39,37 +43,108 @@ val pushBasis = SS.addList (SS.empty,
                             ["new_channel",
                              "self"])
 
+datatype rpcmap =
+         Rpc of int (* ID of function definition *)
+       | Module of rpcmap SM.map
+
+fun lookup (r : rpcmap, k : string) =
+    let
+        fun lookup' (r, ks) =
+            case r of
+                Rpc x => SOME x
+              | Module m =>
+                case ks of
+                    [] => NONE
+                  | k :: ks' =>
+                    case SM.find (m, k) of
+                        NONE => NONE
+                      | SOME r' => lookup' (r', ks')
+    in
+        lookup' (r, String.tokens (fn ch => ch = #"/") k)
+    end
+
+fun insert (r : rpcmap, k : string, v) =
+    let
+        fun insert' (r, ks) =
+            case r of
+                Rpc _ => Rpc v
+              | Module m =>
+                case ks of
+                    [] => Rpc v
+                  | k :: ks' =>
+                    let
+                        val r' = case SM.find (m, k) of
+                                     NONE => Module SM.empty
+                                   | SOME r' => r'
+                    in
+                        Module (SM.insert (m, k, insert' (r', ks')))
+                    end
+    in
+        insert' (r, String.tokens (fn ch => ch = #"/") k)
+    end
+
+fun dump (r : rpcmap) =
+    case r of
+        Rpc _ => print "ROOT\n"
+      | Module m => (print "<Module>\n";
+                     SM.appi (fn (k, r') => (print (k ^ ":\n");
+                                             dump r')) m;
+                     print "</Module>\n")
+
 fun classify (ds, ps) =
     let
         val proto = Settings.currentProtocol ()
 
         fun inString {needle, haystack} = String.isSubstring needle haystack
 
-        fun hasClient {basis, funcs, push} =
+        fun hasClient {basis, rpcs, funcs, push} =
             MonoUtil.Exp.exists {typ = fn _ => false,
                                  exp = fn ERecv _ => push
                                         | EFfiApp ("Basis", x, _) => SS.member (basis, x) 
                                         | EJavaScript _ => not push
                                         | ENamed n => IS.member (funcs, n)
+                                        | EServerCall (e, _, _, _) =>
+                                          let
+                                              fun head (e : exp) =
+                                                  case #1 e of
+                                                      EStrcat (e1, _) => head e1
+                                                    | EPrim (Prim.String (_, s)) => SOME s
+                                                    | _ => NONE
+                                          in
+                                              case head e of
+                                                  NONE => true
+                                                | SOME fcall =>
+                                                  case lookup (rpcs, fcall) of
+                                                      NONE => true
+                                                    | SOME n => IS.member (funcs, n)
+                                          end
                                         | _ => false}
 
+        fun decl ((d, _), rpcs) =
+            case d of
+                DExport (Mono.Rpc _, fcall, n, _, _, _) =>
+                insert (rpcs, fcall, n)
+              | _ => rpcs
+
+        val rpcs = foldl decl (Module SM.empty) ds
+
         fun decl ((d, _), (pull_ids, push_ids)) =
             let
-                val hasClientPull = hasClient {basis = SS.empty, funcs = pull_ids, push = false}
-                val hasClientPush = hasClient {basis = pushBasis, funcs = push_ids, push = true}
+                val hasClientPull = hasClient {basis = SS.empty, rpcs = rpcs, funcs = pull_ids, push = false}
+                val hasClientPush = hasClient {basis = pushBasis, rpcs = rpcs, funcs = push_ids, push = true}
             in
                 case d of
                     DVal (_, n, _, e, _) => (if hasClientPull e then
-                                             IS.add (pull_ids, n)
-                                          else
-                                              pull_ids,
-                                          if hasClientPush e then
-                                              IS.add (push_ids, n)
-                                          else
-                                              push_ids)
+                                                 IS.add (pull_ids, n)
+                                             else
+                                                 pull_ids,
+                                             if hasClientPush e then
+                                                 IS.add (push_ids, n)
+                                             else
+                                                 push_ids)
                   | DValRec xes => (if List.exists (fn (_, _, _, e, _) => hasClientPull e) xes then
-                                       foldl (fn ((_, n, _, _, _), pull_ids) => IS.add (pull_ids, n))
-                                             pull_ids xes
+                                        foldl (fn ((_, n, _, _, _), pull_ids) => IS.add (pull_ids, n))
+                                              pull_ids xes
                                     else
                                         pull_ids,
                                     if List.exists (fn (_, _, _, e, _) => hasClientPush e) xes then
diff --git a/tests/DynChannel.ur b/tests/DynChannel.ur
new file mode 100644
index 00000000..d3688781
--- /dev/null
+++ b/tests/DynChannel.ur
@@ -0,0 +1,29 @@
+table channels : {Id : int, Channel:channel xbody}
+
+fun dosend (s:string) : transaction unit =
+  c <- oneRow1 (SELECT * FROM channels);
+  debug ("Sending " ^ s ^ " through the channel...");
+  send c.Channel <xml>{[s]}</xml>
+
+fun mkchannel {} : transaction xbody =
+  c <- channel;
+  s <- source <xml/>;
+  dml( DELETE FROM channels WHERE Id >= 0);
+  dml( INSERT INTO channels(Id, Channel) VALUES(0, {[c]}) );
+  return <xml>
+    <button value="Send" onclick={fn _ => rpc(dosend "blabla")}/>
+    <active code={spawn(x <- recv c; alert ("Got something from the channel"); set s x); return <xml/>}/>
+    <dyn signal={signal s}/>
+  </xml>
+
+fun main {} : transaction page =
+  s <- source <xml/>;
+  return <xml>
+    <head/>
+    <body>
+      <button value="Register" onclick={fn _ =>
+        x <- rpc(mkchannel {}); set s x
+      }/>
+      <dyn signal={signal s}/>
+    </body>
+  </xml>
diff --git a/tests/DynChannel.urp b/tests/DynChannel.urp
new file mode 100644
index 00000000..08d6d1a5
--- /dev/null
+++ b/tests/DynChannel.urp
@@ -0,0 +1,6 @@
+database dbname=DynChannel.db
+sql DynChannel.sql
+debug
+
+$/list
+DynChannel
diff --git a/tests/rpchan.ur b/tests/rpchan.ur
new file mode 100644
index 00000000..08308d90
--- /dev/null
+++ b/tests/rpchan.ur
@@ -0,0 +1,18 @@
+fun remote () =
+    ch <- channel;
+    send ch "Hello World!";
+    return ch
+
+fun remoter () =
+    ch <- channel;
+    send ch "Hello World!";
+    return <xml><active code={spawn (s <- recv ch; alert s); return <xml/>}/></xml>
+
+fun main () =
+    x <- source <xml/>;
+    return <xml><body>
+      <button onclick={fn _ => ch <- rpc (remote ()); s <- recv ch; alert s}>TEST</button>
+      <button onclick={fn _ => y <- rpc (remoter ()); set x y}>TESTER</button>
+      <hr/>
+      <dyn signal={signal x}/>
+    </body></xml>
diff --git a/tests/rpchan.urs b/tests/rpchan.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/rpchan.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page