# HG changeset patch # User Adam Chlipala # Date 1408895029 14400 # Node ID 3dd041b0008729ee6480b7d2ec8c54037d84ccfc # Parent 83bdb52962c901eac6c6294ce1590490ab593711 Extend ScriptCheck to take RPCs into account diff -r 83bdb52962c9 -r 3dd041b00087 src/scriptcheck.sml --- a/src/scriptcheck.sml Sat Aug 23 11:59:34 2014 +0000 +++ b/src/scriptcheck.sml Sun Aug 24 11:43:49 2014 -0400 @@ -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 @@ 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 @@ ["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 "\n"; + SM.appi (fn (k, r') => (print (k ^ ":\n"); + dump r')) m; + print "\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 -r 83bdb52962c9 -r 3dd041b00087 tests/DynChannel.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/DynChannel.ur Sun Aug 24 11:43:49 2014 -0400 @@ -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 {[s]} + +fun mkchannel {} : transaction xbody = + c <- channel; + s <- source ; + dml( DELETE FROM channels WHERE Id >= 0); + dml( INSERT INTO channels(Id, Channel) VALUES(0, {[c]}) ); + return + + +
+ +
diff -r 83bdb52962c9 -r 3dd041b00087 tests/rpchan.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/rpchan.urs Sun Aug 24 11:43:49 2014 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page