adamc@680
|
1 (* Copyright (c) 2009, Adam Chlipala
|
adamc@680
|
2 * All rights reserved.
|
adamc@680
|
3 *
|
adamc@680
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@680
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@680
|
6 *
|
adamc@680
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@680
|
8 * this list of conditions and the following disclaimer.
|
adamc@680
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@680
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@680
|
11 * and/or other materials provided with the distribution.
|
adamc@680
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@680
|
13 * derived from this software without specific prior written permission.
|
adamc@680
|
14 *
|
adamc@680
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@680
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@680
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@680
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@680
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@680
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@680
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@680
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@680
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@680
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@680
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@680
|
26 *)
|
adamc@680
|
27
|
adamc@680
|
28 structure MarshalCheck :> MARSHAL_CHECK = struct
|
adamc@680
|
29
|
adamc@680
|
30 open Core
|
adamc@680
|
31
|
adamc@680
|
32 structure U = CoreUtil
|
adamc@680
|
33 structure E = ErrorMsg
|
adamc@680
|
34
|
adamc@680
|
35 structure PK = struct
|
adamc@680
|
36 open Order
|
adamc@680
|
37 type ord_key = string * string
|
adamc@680
|
38 fun compare ((m1, x1), (m2, x2)) =
|
adamc@680
|
39 join (String.compare (m1, m2),
|
adamc@680
|
40 fn () => String.compare (x1, x2))
|
adamc@680
|
41 end
|
adamc@680
|
42
|
adamc@680
|
43 structure PS = BinarySetFn(PK)
|
adamc@680
|
44 structure PS = struct
|
adamc@680
|
45 open PS
|
adamc@680
|
46 fun toString' (m, x) = m ^ "." ^ x
|
adamc@680
|
47 fun toString set =
|
adamc@680
|
48 case PS.listItems set of
|
adamc@680
|
49 [] => "{}"
|
adamc@680
|
50 | [x] => toString' x
|
adamc@680
|
51 | x :: xs => List.foldl (fn (x, s) => s ^ ", " ^ toString' x) (toString' x) xs
|
adamc@680
|
52 end
|
adamc@680
|
53
|
adamc@680
|
54 structure IM = IntBinaryMap
|
adamc@680
|
55
|
adamc@680
|
56 val clientToServer = [("Basis", "int"),
|
adamc@680
|
57 ("Basis", "float"),
|
adamc@680
|
58 ("Basis", "string"),
|
adamc@680
|
59 ("Basis", "time"),
|
adamc@680
|
60 ("Basis", "unit"),
|
adamc@680
|
61 ("Basis", "option")]
|
adamc@680
|
62
|
adamc@680
|
63 val clientToServer = PS.addList (PS.empty, clientToServer)
|
adamc@680
|
64
|
adamc@680
|
65 fun check file =
|
adamc@680
|
66 let
|
adamc@680
|
67 fun kind (_, st) = st
|
adamc@680
|
68
|
adamc@680
|
69 fun con cmap (c, st) =
|
adamc@680
|
70 case c of
|
adamc@680
|
71 CFfi mx =>
|
adamc@680
|
72 if PS.member (clientToServer, mx) then
|
adamc@680
|
73 st
|
adamc@680
|
74 else
|
adamc@680
|
75 PS.add (st, mx)
|
adamc@680
|
76 | CNamed n =>
|
adamc@680
|
77 (case IM.find (cmap, n) of
|
adamc@680
|
78 NONE => st
|
adamc@680
|
79 | SOME st' => PS.union (st, st'))
|
adamc@680
|
80 | _ => st
|
adamc@680
|
81
|
adamc@680
|
82 fun sins cmap = U.Con.fold {kind = kind, con = con cmap} PS.empty
|
adamc@680
|
83 in
|
adamc@680
|
84 ignore (foldl (fn ((d, _), (cmap, emap)) =>
|
adamc@680
|
85 case d of
|
adamc@680
|
86 DCon (_, n, _, c) => (IM.insert (cmap, n, sins cmap c), emap)
|
adamc@680
|
87 | DDatatype (_, n, _, xncs) =>
|
adamc@680
|
88 (IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
|
adamc@680
|
89 case co of
|
adamc@680
|
90 NONE => s
|
adamc@680
|
91 | SOME c => PS.union (s, sins cmap c))
|
adamc@680
|
92 PS.empty xncs),
|
adamc@680
|
93 emap)
|
adamc@680
|
94
|
adamc@680
|
95 | DVal (_, n, t, _, tag) => (cmap, IM.insert (emap, n, (t, tag)))
|
adamc@680
|
96 | DValRec vis => (cmap,
|
adamc@680
|
97 foldl (fn ((_, n, t, _, tag), emap) => IM.insert (emap, n, (t, tag)))
|
adamc@680
|
98 emap vis)
|
adamc@680
|
99
|
adamc@680
|
100 | DExport (_, n) =>
|
adamc@680
|
101 (case IM.find (emap, n) of
|
adamc@680
|
102 NONE => raise Fail "MarshalCheck: Unknown export"
|
adamc@680
|
103 | SOME (t, tag) =>
|
adamc@680
|
104 let
|
adamc@680
|
105 fun makeS (t, _) =
|
adamc@680
|
106 case t of
|
adamc@680
|
107 TFun (dom, ran) => PS.union (sins cmap dom, makeS ran)
|
adamc@680
|
108 | _ => PS.empty
|
adamc@680
|
109 val s = makeS t
|
adamc@680
|
110 in
|
adamc@680
|
111 if PS.isEmpty s then
|
adamc@680
|
112 ()
|
adamc@680
|
113 else
|
adamc@680
|
114 E.error ("Input to exported function '"
|
adamc@680
|
115 ^ tag ^ "' involves one or more disallowed types: "
|
adamc@680
|
116 ^ PS.toString s);
|
adamc@680
|
117 (cmap, emap)
|
adamc@680
|
118 end)
|
adamc@680
|
119
|
adamc@680
|
120 | DCookie (_, _, t, tag) =>
|
adamc@680
|
121 let
|
adamc@680
|
122 val s = sins cmap t
|
adamc@680
|
123 in
|
adamc@680
|
124 if PS.isEmpty s then
|
adamc@680
|
125 ()
|
adamc@680
|
126 else
|
adamc@680
|
127 E.error ("Cookie '" ^ tag ^ "' includes one or more disallowed types: "
|
adamc@680
|
128 ^ PS.toString s);
|
adamc@680
|
129 (cmap, emap)
|
adamc@680
|
130 end
|
adamc@680
|
131
|
adamc@680
|
132 | _ => (cmap, emap))
|
adamc@680
|
133 (IM.empty, IM.empty) file)
|
adamc@680
|
134 end
|
adamc@680
|
135
|
adamc@680
|
136 end
|