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 fun check file =
|
adamc@680
|
57 let
|
adamc@680
|
58 fun kind (_, st) = st
|
adamc@680
|
59
|
adamc@680
|
60 fun con cmap (c, st) =
|
adamc@680
|
61 case c of
|
adamc@680
|
62 CFfi mx =>
|
adamc@765
|
63 if Settings.mayClientToServer mx then
|
adamc@680
|
64 st
|
adamc@680
|
65 else
|
adamc@680
|
66 PS.add (st, mx)
|
adamc@680
|
67 | CNamed n =>
|
adamc@680
|
68 (case IM.find (cmap, n) of
|
adamc@680
|
69 NONE => st
|
adamc@680
|
70 | SOME st' => PS.union (st, st'))
|
adamc@680
|
71 | _ => st
|
adamc@680
|
72
|
adamc@680
|
73 fun sins cmap = U.Con.fold {kind = kind, con = con cmap} PS.empty
|
adamc@680
|
74 in
|
adamc@680
|
75 ignore (foldl (fn ((d, _), (cmap, emap)) =>
|
adamc@680
|
76 case d of
|
adamc@680
|
77 DCon (_, n, _, c) => (IM.insert (cmap, n, sins cmap c), emap)
|
adamc@807
|
78 | DDatatype dts =>
|
adamc@807
|
79 (foldl (fn ((_, n, _, xncs), cmap) =>
|
adamc@807
|
80 IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
|
adamc@807
|
81 case co of
|
adamc@807
|
82 NONE => s
|
adamc@807
|
83 | SOME c => PS.union (s, sins cmap c))
|
adamc@807
|
84 PS.empty xncs)) cmap dts,
|
adamc@680
|
85 emap)
|
adamc@680
|
86
|
adamc@680
|
87 | DVal (_, n, t, _, tag) => (cmap, IM.insert (emap, n, (t, tag)))
|
adamc@680
|
88 | DValRec vis => (cmap,
|
adamc@680
|
89 foldl (fn ((_, n, t, _, tag), emap) => IM.insert (emap, n, (t, tag)))
|
adamc@680
|
90 emap vis)
|
adamc@680
|
91
|
adamc@1104
|
92 | DExport (_, n, _) =>
|
adamc@680
|
93 (case IM.find (emap, n) of
|
adamc@680
|
94 NONE => raise Fail "MarshalCheck: Unknown export"
|
adamc@680
|
95 | SOME (t, tag) =>
|
adamc@680
|
96 let
|
adamc@680
|
97 fun makeS (t, _) =
|
adamc@680
|
98 case t of
|
adamc@680
|
99 TFun (dom, ran) => PS.union (sins cmap dom, makeS ran)
|
adamc@680
|
100 | _ => PS.empty
|
adamc@680
|
101 val s = makeS t
|
adamc@680
|
102 in
|
adamc@680
|
103 if PS.isEmpty s then
|
adamc@680
|
104 ()
|
adamc@680
|
105 else
|
adamc@680
|
106 E.error ("Input to exported function '"
|
adamc@680
|
107 ^ tag ^ "' involves one or more disallowed types: "
|
adamc@680
|
108 ^ PS.toString s);
|
adamc@680
|
109 (cmap, emap)
|
adamc@680
|
110 end)
|
adamc@680
|
111
|
adamc@680
|
112 | DCookie (_, _, t, tag) =>
|
adamc@680
|
113 let
|
adamc@680
|
114 val s = sins cmap t
|
adamc@680
|
115 in
|
adamc@680
|
116 if PS.isEmpty s then
|
adamc@680
|
117 ()
|
adamc@680
|
118 else
|
adamc@680
|
119 E.error ("Cookie '" ^ tag ^ "' includes one or more disallowed types: "
|
adamc@680
|
120 ^ PS.toString s);
|
adamc@680
|
121 (cmap, emap)
|
adamc@680
|
122 end
|
adamc@680
|
123
|
adamc@680
|
124 | _ => (cmap, emap))
|
adamc@680
|
125 (IM.empty, IM.empty) file)
|
adamc@680
|
126 end
|
adamc@680
|
127
|
adamc@680
|
128 end
|