Mercurial > urweb

comparison src/iflow.sml @ 1236:d5ecceb7d1a1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Completely redid main Iflow logic; so far, policy and policy2 work
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 16:30:46 -0400
parents a7b773f1d053
children a9c200f73f24
comparison
equal deleted inserted replaced
1235:a7b773f1d053 1236:d5ecceb7d1a1
70 | Var of int 70 | Var of int
71 | Lvar of lvar 71 | Lvar of lvar
72 | Func of func * exp list 72 | Func of func * exp list
73 | Recd of (string * exp) list 73 | Recd of (string * exp) list
74 | Proj of exp * string 74 | Proj of exp * string
75 | Finish
76 75
77 datatype reln = 76 datatype reln =
78 Known 77 Known
79 | Sql of string 78 | Sql of string
80 | PCon0 of string 79 | PCon0 of string
93 | And of prop * prop 92 | And of prop * prop
94 | Or of prop * prop 93 | Or of prop * prop
95 | Reln of reln * exp list 94 | Reln of reln * exp list
96 | Cond of exp * prop 95 | Cond of exp * prop
97 96
98 val unif = ref (IM.empty : exp IM.map)
99
100 fun reset () = unif := IM.empty
101 fun save () = !unif
102 fun restore x = unif := x
103
104 local 97 local
105 open Print 98 open Print
106 val string = PD.string 99 val string = PD.string
107 in 100 in
108 101
115 108
116 fun p_exp e = 109 fun p_exp e =
117 case e of 110 case e of
118 Const p => Prim.p_t p 111 Const p => Prim.p_t p
119 | Var n => string ("x" ^ Int.toString n) 112 | Var n => string ("x" ^ Int.toString n)
120 | Lvar n => 113 | Lvar n => string ("X" ^ Int.toString n)
121 (case IM.find (!unif, n) of
122 NONE => string ("X" ^ Int.toString n)
123 | SOME e => p_exp e)
124 | Func (f, es) => box [p_func f, 114 | Func (f, es) => box [p_func f,
125 string "(", 115 string "(",
126 p_list p_exp es, 116 p_list p_exp es,
127 string ")"] 117 string ")"]
128 | Recd xes => box [string "{", 118 | Recd xes => box [string "{",
132 space, 122 space,
133 p_exp e]) xes, 123 p_exp e]) xes,
134 string "}"] 124 string "}"]
135 | Proj (e, x) => box [p_exp e, 125 | Proj (e, x) => box [p_exp e,
136 string ("." ^ x)] 126 string ("." ^ x)]
137 | Finish => string "FINISH"
138 127
139 fun p_bop s es = 128 fun p_bop s es =
140 case es of 129 case es of
141 [e1, e2] => box [p_exp e1, 130 [e1, e2] => box [p_exp e1,
142 space, 131 space,
201 p_prop p, 190 p_prop p,
202 string ")"] 191 string ")"]
203 192
204 end 193 end
205 194
206 local
207 val count = ref 1
208 in
209 fun newLvar () =
210 let
211 val n = !count
212 in
213 count := n + 1;
214 n
215 end
216 end
217
218 fun isKnown e = 195 fun isKnown e =
219 case e of 196 case e of
220 Const _ => true 197 Const _ => true
221 | Func (_, es) => List.all isKnown es 198 | Func (_, es) => List.all isKnown es
222 | Recd xes => List.all (isKnown o #2) xes 199 | Recd xes => List.all (isKnown o #2) xes
223 | Proj (e, _) => isKnown e 200 | Proj (e, _) => isKnown e
224 | _ => false 201 | _ => false
225 202
226 fun isFinish e = 203 fun simplify unif =
227 case e of 204 let
228 Finish => true 205 fun simplify e =
229 | _ => false 206 case e of
230 207 Const _ => e
231 fun simplify e = 208 | Var _ => e
232 case e of 209 | Lvar n =>
233 Const _ => e 210 (case IM.find (unif, n) of
234 | Var _ => e 211 NONE => e
235 | Lvar n => 212 | SOME e => simplify e)
236 (case IM.find (!unif, n) of 213 | Func (f, es) => Func (f, map simplify es)
237 NONE => e 214 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
238 | SOME e => simplify e) 215 | Proj (e, s) => Proj (simplify e, s)
239 | Func (f, es) => Func (f, map simplify es) 216 in
240 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes) 217 simplify
241 | Proj (e, s) => Proj (simplify e, s) 218 end
242 | Finish => Finish
243 219
244 datatype atom = 220 datatype atom =
245 AReln of reln * exp list 221 AReln of reln * exp list
246 | ACond of exp * prop 222 | ACond of exp * prop
247 223
248 fun p_atom a = 224 fun p_atom a =
249 p_prop (case a of 225 p_prop (case a of
250 AReln x => Reln x 226 AReln x => Reln x
251 | ACond x => Cond x) 227 | ACond x => Cond x)
252 228
253 fun lvarIn lv =
254 let
255 fun lvi e =
256 case e of
257 Const _ => false
258 | Var _ => false
259 | Lvar lv' => lv' = lv
260 | Func (_, es) => List.exists lvi es
261 | Recd xes => List.exists (lvi o #2) xes
262 | Proj (e, _) => lvi e
263 | Finish => false
264 in
265 lvi
266 end
267
268 fun lvarInP lv =
269 let
270 fun lvi p =
271 case p of
272 True => false
273 | False => false
274 | Unknown => true
275 | And (p1, p2) => lvi p1 orelse lvi p2
276 | Or (p1, p2) => lvi p1 orelse lvi p2
277 | Reln (_, es) => List.exists (lvarIn lv) es
278 | Cond (e, p) => lvarIn lv e orelse lvi p
279 in
280 lvi
281 end
282
283 fun varIn lv =
284 let
285 fun lvi e =
286 case e of
287 Const _ => false
288 | Lvar _ => false
289 | Var lv' => lv' = lv
290 | Func (_, es) => List.exists lvi es
291 | Recd xes => List.exists (lvi o #2) xes
292 | Proj (e, _) => lvi e
293 | Finish => false
294 in
295 lvi
296 end
297
298 fun varInP lv =
299 let
300 fun lvi p =
301 case p of
302 True => false
303 | False => false
304 | Unknown => false
305 | And (p1, p2) => lvi p1 orelse lvi p2
306 | Or (p1, p2) => lvi p1 orelse lvi p2
307 | Reln (_, es) => List.exists (varIn lv) es
308 | Cond (e, p) => varIn lv e orelse lvi p
309 in
310 lvi
311 end
312
313 fun bumpLvars by =
314 let
315 fun lvi e =
316 case e of
317 Const _ => e
318 | Var _ => e
319 | Lvar lv => Lvar (lv + by)
320 | Func (f, es) => Func (f, map lvi es)
321 | Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes)
322 | Proj (e, f) => Proj (lvi e, f)
323 | Finish => e
324 in
325 lvi
326 end
327
328 fun bumpLvarsP by =
329 let
330 fun lvi p =
331 case p of
332 True => p
333 | False => p
334 | Unknown => p
335 | And (p1, p2) => And (lvi p1, lvi p2)
336 | Or (p1, p2) => And (lvi p1, lvi p2)
337 | Reln (r, es) => Reln (r, map (bumpLvars by) es)
338 | Cond (e, p) => Cond (bumpLvars by e, lvi p)
339 in
340 lvi
341 end
342
343 fun maxLvar e =
344 let
345 fun lvi e =
346 case e of
347 Const _ => 0
348 | Var _ => 0
349 | Lvar lv => lv
350 | Func (f, es) => foldl Int.max 0 (map lvi es)
351 | Recd xes => foldl Int.max 0 (map (lvi o #2) xes)
352 | Proj (e, f) => lvi e
353 | Finish => 0
354 in
355 lvi e
356 end
357
358 fun maxLvarP p =
359 let
360 fun lvi p =
361 case p of
362 True => 0
363 | False => 0
364 | Unknown => 0
365 | And (p1, p2) => Int.max (lvi p1, lvi p2)
366 | Or (p1, p2) => Int.max (lvi p1, lvi p2)
367 | Reln (r, es) => foldl Int.max 0 (map maxLvar es)
368 | Cond (e, p) => Int.max (maxLvar e, lvi p)
369 in
370 lvi p
371 end
372
373 fun eq' (e1, e2) =
374 case (e1, e2) of
375 (Const p1, Const p2) => Prim.equal (p1, p2)
376 | (Var n1, Var n2) => n1 = n2
377
378 | (Lvar n1, _) =>
379 (case IM.find (!unif, n1) of
380 SOME e1 => eq' (e1, e2)
381 | NONE =>
382 case e2 of
383 Lvar n2 =>
384 (case IM.find (!unif, n2) of
385 SOME e2 => eq' (e1, e2)
386 | NONE => n1 = n2
387 orelse (unif := IM.insert (!unif, n2, e1);
388 true))
389 | _ =>
390 if lvarIn n1 e2 then
391 false
392 else
393 (unif := IM.insert (!unif, n1, e2);
394 true))
395
396 | (_, Lvar n2) =>
397 (case IM.find (!unif, n2) of
398 SOME e2 => eq' (e1, e2)
399 | NONE =>
400 if lvarIn n2 e1 then
401 false
402 else
403 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
404 ("e1", p_exp e1)];*)
405 unif := IM.insert (!unif, n2, e1);
406 true))
407
408 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
409 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
410 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
411 | (Finish, Finish) => true
412 | _ => false
413
414 fun eq (e1, e2) =
415 let
416 val saved = save ()
417 in
418 if eq' (simplify e1, simplify e2) then
419 true
420 else
421 (restore saved;
422 false)
423 end
424
425 val debug = ref false 229 val debug = ref false
426
427 fun eeq (e1, e2) =
428 case (e1, e2) of
429 (Const p1, Const p2) => Prim.equal (p1, p2)
430 | (Var n1, Var n2) => n1 = n2
431 | (Lvar n1, Lvar n2) => n1 = n2
432 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
433 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
434 List.all (fn (x2, e2) =>
435 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
436 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
437 | (Finish, Finish) => true
438 | _ => false
439 230
440 (* Congruence closure *) 231 (* Congruence closure *)
441 structure Cc :> sig 232 structure Cc :> sig
442 type database 233 type database
443 234
444 exception Contradiction 235 exception Contradiction
445 exception Undetermined 236 exception Undetermined
446 237
447 val database : unit -> database 238 val database : unit -> database
239 val clear : database -> unit
448 240
449 val assert : database * atom -> unit 241 val assert : database * atom -> unit
450 val check : database * atom -> bool 242 val check : database * atom -> bool
451 243
452 val p_database : database Print.printer 244 val p_database : database Print.printer
487 fun database () = {Vars = ref IM.empty, 279 fun database () = {Vars = ref IM.empty,
488 Consts = ref CM.empty, 280 Consts = ref CM.empty,
489 Con0s = ref SM.empty, 281 Con0s = ref SM.empty,
490 Records = ref [], 282 Records = ref [],
491 Funcs = ref []} 283 Funcs = ref []}
284
285 fun clear (t : database) = (#Vars t := IM.empty;
286 #Consts t := CM.empty;
287 #Con0s t := SM.empty;
288 #Records t := [];
289 #Funcs t := [])
492 290
493 fun unNode n = 291 fun unNode n =
494 case !n of 292 case !n of
495 Node r => r 293 Node r => r
496 294
592 Known = ref false}) 390 Known = ref false})
593 in 391 in
594 #Vars db := IM.insert (!(#Vars db), n, r); 392 #Vars db := IM.insert (!(#Vars db), n, r);
595 r 393 r
596 end) 394 end)
597 | Lvar n => 395 | Lvar _ => raise Undetermined
598 (case IM.find (!unif, n) of
599 NONE => raise Undetermined
600 | SOME e => rep e)
601 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of 396 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
602 SOME r => repOf r 397 SOME r => repOf r
603 | NONE => 398 | NONE =>
604 let 399 let
605 val r = ref (Node {Rep = ref NONE, 400 val r = ref (Node {Rep = ref NONE,
733 #Rep (unNode r) := SOME r''; 528 #Rep (unNode r) := SOME r'';
734 r' 529 r'
735 end 530 end
736 | _ => raise Contradiction 531 | _ => raise Contradiction
737 end 532 end
738 | Finish => raise Contradiction
739 in 533 in
740 rep e 534 rep e
741 end 535 end
742 536
743 fun p_repOf db e = p_rep (representative (db, e)) 537 fun p_repOf db e = p_rep (representative (db, e))
935 in 729 in
936 loop (representative (db, d)) 730 loop (representative (db, d))
937 end 731 end
938 732
939 end 733 end
940
941 fun decomp fals or =
942 let
943 fun decomp p k =
944 case p of
945 True => k []
946 | False => fals
947 | Unknown => k []
948 | And (p1, p2) =>
949 decomp p1 (fn ps1 =>
950 decomp p2 (fn ps2 =>
951 k (ps1 @ ps2)))
952 | Or (p1, p2) =>
953 or (decomp p1 k, fn () => decomp p2 k)
954 | Reln x => k [AReln x]
955 | Cond x => k [ACond x]
956 in
957 decomp
958 end
959 734
960 val tabs = ref (SM.empty : (string list * string list list) SM.map) 735 val tabs = ref (SM.empty : (string list * string list list) SM.map)
961 736
962 fun ccOf hyps = 737 fun ccOf hyps =
963 let 738 let
1016 in 791 in
1017 findKeys hyps; 792 findKeys hyps;
1018 cc 793 cc
1019 end 794 end
1020 795
1021 fun imply (cc, hyps, goals, outs) =
1022 let
1023 fun gls goals onFail acc =
1024 case goals of
1025 [] =>
1026 ((List.all (fn a =>
1027 if Cc.check (cc, a) then
1028 true
1029 else
1030 ((*Print.prefaces "Can't prove"
1031 [("a", p_atom a),
1032 ("hyps", Print.p_list p_atom hyps),
1033 ("db", Cc.p_database cc)];*)
1034 false)) acc
1035 andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
1036 andalso (case outs of
1037 NONE => true
1038 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
1039 Base = outs})))
1040 handle Cc.Contradiction => false
1041 | Cc.Undetermined => false)
1042 orelse onFail ()
1043 | (g as AReln (Sql gf, [ge])) :: goals =>
1044 let
1045 fun hps hyps =
1046 case hyps of
1047 [] => gls goals onFail (g :: acc)
1048 | (h as AReln (Sql hf, [he])) :: hyps =>
1049 if gf = hf then
1050 let
1051 val saved = save ()
1052 in
1053 if eq (ge, he) then
1054 let
1055 val changed = IM.numItems (!unif)
1056 <> IM.numItems saved
1057 in
1058 gls goals (fn () => (restore saved;
1059 changed
1060 andalso hps hyps))
1061 acc
1062 end
1063 else
1064 hps hyps
1065 end
1066 else
1067 hps hyps
1068 | _ :: hyps => hps hyps
1069 in
1070 hps hyps
1071 end
1072 | g :: goals => gls goals onFail (g :: acc)
1073 in
1074 reset ();
1075 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
1076 ("goals", Print.p_list p_atom goals)];*)
1077 gls goals (fn () => false) []
1078 end
1079
1080 fun patCon pc = 796 fun patCon pc =
1081 case pc of 797 case pc of
1082 PConVar n => "C" ^ Int.toString n 798 PConVar n => "C" ^ Int.toString n
1083 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 799 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
1084 800
1428 val dml = log "dml" 1144 val dml = log "dml"
1429 (altL [wrap insert Insert, 1145 (altL [wrap insert Insert,
1430 wrap delete Delete, 1146 wrap delete Delete,
1431 wrap update Update]) 1147 wrap update Update])
1432 1148
1149 type check = exp * ErrorMsg.span
1150
1151 structure St :> sig
1152 val reset : unit -> unit
1153
1154 type stashed
1155 val stash : unit -> stashed
1156 val reinstate : stashed -> unit
1157
1158 val nextVar : unit -> int
1159
1160 val assert : atom list -> unit
1161
1162 val addPath : check -> unit
1163
1164 val allowSend : atom list * exp list -> unit
1165 val send : check -> unit
1166
1167 val allowInsert : atom list -> unit
1168 val insert : ErrorMsg.span -> unit
1169
1170 val allowDelete : atom list -> unit
1171 val delete : ErrorMsg.span -> unit
1172
1173 val allowUpdate : atom list -> unit
1174 val update : ErrorMsg.span -> unit
1175
1176 val havocReln : reln -> unit
1177 end = struct
1178
1179 val hnames = ref 1
1180
1181 type hyps = int * atom list
1182
1183 val db = Cc.database ()
1184 val path = ref ([] : (hyps * check) option ref list)
1185 val hyps = ref (0, [] : atom list)
1186 val nvar = ref 0
1187
1188 fun reset () = (Cc.clear db;
1189 path := [];
1190 hyps := (0, []);
1191 nvar := 0)
1192
1193 fun setHyps (h as (n', hs)) =
1194 let
1195 val (n, _) = !hyps
1196 in
1197 if n' = n then
1198 ()
1199 else
1200 (hyps := h;
1201 Cc.clear db;
1202 app (fn a => Cc.assert (db, a)) hs)
1203 end
1204
1205 type stashed = int * (hyps * check) option ref list * (int * atom list)
1206 fun stash () = (!nvar, !path, !hyps)
1207 fun reinstate (nv, p, h) =
1208 (nvar := nv;
1209 path := p;
1210 setHyps h)
1211
1212 fun nextVar () =
1213 let
1214 val n = !nvar
1215 in
1216 nvar := n + 1;
1217 n
1218 end
1219
1220 fun assert ats =
1221 let
1222 val n = !hnames
1223 val (_, hs) = !hyps
1224 in
1225 hnames := n + 1;
1226 hyps := (n, ats @ hs);
1227 app (fn a => Cc.assert (db, a)) ats
1228 end
1229
1230 fun addPath c = path := ref (SOME (!hyps, c)) :: !path
1231
1232 val sendable = ref ([] : (atom list * exp list) list)
1233
1234 fun checkGoals goals unifs succ fail =
1235 case goals of
1236 [] => succ (unifs, [])
1237 | AReln (Sql tab, [Lvar lv]) :: goals =>
1238 let
1239 val saved = stash ()
1240 val (_, hyps) = !hyps
1241
1242 fun tryAll unifs hyps =
1243 case hyps of
1244 [] => fail ()
1245 | AReln (Sql tab', [e]) :: hyps =>
1246 if tab' = tab then
1247 checkGoals goals (IM.insert (unifs, lv, e)) succ
1248 (fn () => tryAll unifs hyps)
1249 else
1250 tryAll unifs hyps
1251 | _ :: hyps => tryAll unifs hyps
1252 in
1253 tryAll unifs hyps
1254 end
1255 | AReln (r, es) :: goals => checkGoals goals unifs
1256 (fn (unifs, ls) => succ (unifs, AReln (r, map (simplify unifs) es) :: ls))
1257 fail
1258 | ACond _ :: _ => fail ()
1259
1260 fun buildable (e, loc) =
1261 let
1262 fun doPols pols acc fail =
1263 case pols of
1264 [] => ((*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
1265 ("Derived", p_exp e),
1266 ("Hyps", Print.p_list p_atom (#2 (!hyps)))];*)
1267 if Cc.builtFrom (db, {Base = acc, Derived = e}) then
1268 ()
1269 else
1270 fail ())
1271 | (goals, es) :: pols =>
1272 checkGoals goals IM.empty
1273 (fn (unifs, goals) =>
1274 if List.all (fn a => Cc.check (db, a)) goals then
1275 doPols pols (map (simplify unifs) es @ acc) fail
1276 else
1277 doPols pols acc fail)
1278 (fn () => doPols pols acc fail)
1279 in
1280 doPols (!sendable) []
1281 (fn () => let
1282 val (_, hs) = !hyps
1283 in
1284 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1285 Print.preface ("Hypotheses", Print.p_list p_atom hs)
1286 end)
1287 end
1288
1289 fun checkPaths () =
1290 let
1291 val hs = !hyps
1292 in
1293 app (fn r =>
1294 case !r of
1295 NONE => ()
1296 | SOME (hs, e) =>
1297 (r := NONE;
1298 setHyps hs;
1299 buildable e)) (!path);
1300 setHyps hs
1301 end
1302
1303 fun allowSend v = sendable := v :: !sendable
1304
1305 fun send (e, loc) = ((*Print.preface ("Send", p_exp e);*)
1306 checkPaths ();
1307 if isKnown e then
1308 ()
1309 else
1310 buildable (e, loc))
1311
1312 fun doable pols (loc : ErrorMsg.span) =
1313 let
1314 val pols = !pols
1315 in
1316 if List.exists (fn goals =>
1317 checkGoals goals IM.empty
1318 (fn (_, goals) => List.all (fn a => Cc.check (db, a)) goals)
1319 (fn () => false)) pols then
1320 ()
1321 else
1322 let
1323 val (_, hs) = !hyps
1324 in
1325 ErrorMsg.errorAt loc "The database update policy may be violated here.";
1326 Print.preface ("Hypotheses", Print.p_list p_atom hs)
1327 end
1328 end
1329
1330 val insertable = ref ([] : atom list list)
1331 fun allowInsert v = insertable := v :: !insertable
1332 val insert = doable insertable
1333
1334 val updatable = ref ([] : atom list list)
1335 fun allowUpdate v = updatable := v :: !updatable
1336 val update = doable updatable
1337
1338 val deletable = ref ([] : atom list list)
1339 fun allowDelete v = deletable := v :: !deletable
1340 val delete = doable deletable
1341
1342 fun havocReln r =
1343 let
1344 val n = !hnames
1345 val (_, hs) = !hyps
1346 in
1347 hnames := n + 1;
1348 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs)
1349 end
1350
1351 end
1352
1353
1433 fun removeDups (ls : (string * string) list) = 1354 fun removeDups (ls : (string * string) list) =
1434 case ls of 1355 case ls of
1435 [] => [] 1356 [] => []
1436 | x :: ls => 1357 | x :: ls =>
1437 let 1358 let
1441 ls 1362 ls
1442 else 1363 else
1443 x :: ls 1364 x :: ls
1444 end 1365 end
1445 1366
1446 datatype queryMode =
1447 SomeCol
1448 | AllCols of exp
1449
1450 fun expIn rv env rvOf = 1367 fun expIn rv env rvOf =
1451 let 1368 let
1452 fun expIn (e, rvN) = 1369 fun expIn e =
1453 let 1370 let
1454 fun default () = 1371 fun default () = inl (rv ())
1455 let
1456 val (rvN, e') = rv rvN
1457 in
1458 (inl e', rvN)
1459 end
1460 in 1372 in
1461 case e of 1373 case e of
1462 SqConst p => (inl (Const p), rvN) 1374 SqConst p => inl (Const p)
1463 | Field (v, f) => (inl (Proj (rvOf v, f)), rvN) 1375 | Field (v, f) => inl (Proj (rvOf v, f))
1464 | Binop (bo, e1, e2) => 1376 | Binop (bo, e1, e2) =>
1465 let 1377 let
1466 val (e1, rvN) = expIn (e1, rvN) 1378 val e1 = expIn e1
1467 val (e2, rvN) = expIn (e2, rvN) 1379 val e2 = expIn e2
1468 in 1380 in
1469 (inr (case (bo, e1, e2) of 1381 inr (case (bo, e1, e2) of
1470 (Exps f, inl e1, inl e2) => f (e1, e2) 1382 (Exps f, inl e1, inl e2) => f (e1, e2)
1471 | (Props f, inr p1, inr p2) => f (p1, p2) 1383 | (Props f, inr p1, inr p2) => f (p1, p2)
1472 | _ => Unknown), rvN) 1384 | _ => Unknown)
1473 end 1385 end
1474 | SqKnown e => 1386 | SqKnown e =>
1475 (case expIn (e, rvN) of 1387 (case expIn e of
1476 (inl e, rvN) => (inr (Reln (Known, [e])), rvN) 1388 inl e => inr (Reln (Known, [e]))
1477 | _ => (inr Unknown, rvN)) 1389 | _ => inr Unknown)
1478 | Inj e => 1390 | Inj e =>
1479 let 1391 let
1480 fun deinj e = 1392 fun deinj e =
1481 case #1 e of 1393 case #1 e of
1482 ERel n => (List.nth (env, n), rvN) 1394 ERel n => List.nth (env, n)
1483 | EField (e, f) => 1395 | EField (e, f) => Proj (deinj e, f)
1484 let 1396 | _ => rv ()
1485 val (e, rvN) = deinj e
1486 in
1487 (Proj (e, f), rvN)
1488 end
1489 | _ =>
1490 let
1491 val (rvN, e) = rv rvN
1492 in
1493 (e, rvN)
1494 end
1495
1496 val (e, rvN) = deinj e
1497 in 1397 in
1498 (inl e, rvN) 1398 inl (deinj e)
1499 end 1399 end
1500 | SqFunc (f, e) => 1400 | SqFunc (f, e) =>
1501 (case expIn (e, rvN) of 1401 (case expIn e of
1502 (inl e, rvN) => (inl (Func (Other f, [e])), rvN) 1402 inl e => inl (Func (Other f, [e]))
1503 | _ => default ()) 1403 | _ => default ())
1504 1404
1505 | Count => default () 1405 | Count => default ()
1506 end 1406 end
1507 in 1407 in
1508 expIn 1408 expIn
1509 end 1409 end
1510 1410
1511 fun queryProp env rvN rv oe e = 1411 fun decomp {Save = save, Restore = restore, Add = add} =
1512 let 1412 let
1513 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1413 fun go p k =
1514 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1414 case p of
1515 (rvN, Unknown, [], [])) 1415 True => k ()
1416 | False => ()
1417 | Unknown => ()
1418 | And (p1, p2) => go p1 (fn () => go p2 k)
1419 | Or (p1, p2) =>
1420 let
1421 val saved = save ()
1422 in
1423 go p1 k;
1424 restore saved;
1425 go p2 k
1426 end
1427 | Reln x => (add (AReln x); k ())
1428 | Cond x => (add (ACond x); k ())
1429 in
1430 go
1431 end
1432
1433 datatype queryMode =
1434 SomeCol of exp list -> unit
1435 | AllCols of exp -> unit
1436
1437 type 'a doQuery = {
1438 Env : exp list,
1439 NextVar : unit -> exp,
1440 Add : atom -> unit,
1441 Save : unit -> 'a,
1442 Restore : 'a -> unit,
1443 UsedExp : exp -> unit,
1444 Cont : queryMode
1445 }
1446
1447 fun doQuery (arg : 'a doQuery) e =
1448 let
1449 fun default () = print ("Warning: Information flow checker can't parse SQL query at "
1450 ^ ErrorMsg.spanToString (#2 e) ^ "\n")
1516 in 1451 in
1517 case parse query e of 1452 case parse query e of
1518 NONE => default () 1453 NONE => default ()
1519 | SOME q => 1454 | SOME q =>
1520 let 1455 let
1521 fun doQuery (q, rvN) = 1456 fun doQuery q =
1522 case q of 1457 case q of
1523 Query1 r => 1458 Query1 r =>
1524 let 1459 let
1525 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => 1460 val rvs = map (fn (_, v) => (v, #NextVar arg ())) (#From r)
1526 let
1527 val (rvN, e) = rv rvN
1528 in
1529 ((v, e), rvN)
1530 end) rvN (#From r)
1531 1461
1532 fun rvOf v = 1462 fun rvOf v =
1533 case List.find (fn (v', _) => v' = v) rvs of 1463 case List.find (fn (v', _) => v' = v) rvs of
1534 NONE => raise Fail "Iflow.queryProp: Bad table variable" 1464 NONE => raise Fail "Iflow.queryProp: Bad table variable"
1535 | SOME (_, e) => e 1465 | SOME (_, e) => e
1466
1467 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
1468
1469 val saved = #Save arg ()
1470 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
1536 1471
1537 fun usedFields e = 1472 fun usedFields e =
1538 case e of 1473 case e of
1539 SqConst _ => [] 1474 SqConst _ => []
1540 | Field (v, f) => [(v, f)] 1475 | Field (v, f) => [(v, f)]
1542 | SqKnown _ => [] 1477 | SqKnown _ => []
1543 | Inj _ => [] 1478 | Inj _ => []
1544 | SqFunc (_, e) => usedFields e 1479 | SqFunc (_, e) => usedFields e
1545 | Count => [] 1480 | Count => []
1546 1481
1547 val p = 1482 fun doUsed () = case #Where r of
1548 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r) 1483 NONE => ()
1549 1484 | SOME e =>
1550 val expIn = expIn rv env rvOf 1485 #UsedExp arg (Recd (ListUtil.mapi
1551 1486 (fn (n, (v, f)) => (Int.toString n,
1552 val (p, rvN) = case #Where r of 1487 Proj (rvOf v, f)))
1553 NONE => (p, rvN) 1488 (usedFields e)))
1554 | SOME e => 1489
1555 case expIn (e, rvN) of 1490 fun normal' () =
1556 (inr p', rvN) => (And (p, p'), rvN) 1491 case #Cont arg of
1557 | _ => (p, rvN) 1492 SomeCol k =>
1558
1559 fun normal () =
1560 case oe of
1561 SomeCol =>
1562 let 1493 let
1563 val (sis, rvN) = 1494 val sis = map (fn si =>
1564 ListUtil.foldlMap 1495 case si of
1565 (fn (si, rvN) => 1496 SqField (v, f) => Proj (rvOf v, f)
1566 case si of 1497 | SqExp (e, f) =>
1567 SqField (v, f) => (Proj (rvOf v, f), rvN) 1498 case expIn e of
1568 | SqExp (e, f) => 1499 inr _ => #NextVar arg ()
1569 case expIn (e, rvN) of 1500 | inl e => e) (#Select r)
1570 (inr _, _) =>
1571 let
1572 val (rvN, e) = rv rvN
1573 in
1574 (e, rvN)
1575 end
1576 | (inl e, rvN) => (e, rvN)) rvN (#Select r)
1577 in 1501 in
1578 (rvN, p, True, sis) 1502 k sis
1579 end 1503 end
1580 | AllCols oe => 1504 | AllCols k =>
1581 let 1505 let
1582 val (ts, es, rvN) = 1506 val (ts, es) =
1583 foldl (fn (si, (ts, es, rvN)) => 1507 foldl (fn (si, (ts, es)) =>
1584 case si of 1508 case si of
1585 SqField (v, f) => 1509 SqField (v, f) =>
1586 let 1510 let
1587 val fs = getOpt (SM.find (ts, v), SM.empty) 1511 val fs = getOpt (SM.find (ts, v), SM.empty)
1588 in 1512 in
1589 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN) 1513 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
1590 end 1514 end
1591 | SqExp (e, f) => 1515 | SqExp (e, f) =>
1592 let 1516 let
1593 val (e, rvN) = 1517 val e =
1594 case expIn (e, rvN) of 1518 case expIn e of
1595 (inr _, rvN) => 1519 inr _ => #NextVar arg ()
1596 let 1520 | inl e => e
1597 val (rvN, e) = rv rvN
1598 in
1599 (e, rvN)
1600 end
1601 | (inl e, rvN) => (e, rvN)
1602 in 1521 in
1603 (ts, SM.insert (es, f, e), rvN) 1522 (ts, SM.insert (es, f, e))
1604 end) 1523 end)
1605 (SM.empty, SM.empty, rvN) (#Select r) 1524 (SM.empty, SM.empty) (#Select r)
1606
1607 val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
1608 (SM.listItemsi ts)
1609 @ SM.listItemsi es)])
1610 in 1525 in
1611 (rvN, And (p, p'), True, []) 1526 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
1527 (SM.listItemsi ts)
1528 @ SM.listItemsi es))
1612 end 1529 end
1613 1530
1614 val (rvN, p, wp, outs) = 1531 fun doWhere final =
1615 case #Select r of 1532 (addFrom ();
1616 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => 1533 case #Where r of
1617 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of 1534 NONE => (doUsed (); final ())
1618 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => 1535 | SOME e =>
1619 (case oe of 1536 case expIn e of
1620 SomeCol => 1537 inl _ => (doUsed (); final ())
1621 let 1538 | inr p =>
1622 val (rvN, oe) = rv rvN 1539 let
1623 in 1540 val saved = #Save arg ()
1624 (rvN, 1541 in
1625 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]), 1542 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
1626 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), 1543 p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
1627 p)), 1544 #Restore arg saved
1628 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), 1545 end)
1629 [oe]) 1546 handle Cc.Contradiction => ()
1630 end 1547
1631 | AllCols oe => 1548 fun normal () = doWhere normal'
1632 let
1633 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
1634 in
1635 (rvN,
1636 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
1637 And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
1638 p)),
1639 oeEq (Func (DtCon0 "Basis.bool.True", [])),
1640 [])
1641 end)
1642 | _ => normal ())
1643 | _ => normal ()
1644 in 1549 in
1645 (rvN, p, map (fn x => (wp, x)) 1550 (case #Select r of
1646 (case #Where r of 1551 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1647 NONE => [] 1552 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1648 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)), outs) 1553 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1554 (case #Cont arg of
1555 SomeCol _ => ()
1556 | AllCols k =>
1557 let
1558 fun answer e = k (Recd [(f, e)])
1559
1560 val () = answer (Func (DtCon0 "Basis.bool.False", []))
1561 val saved = #Save arg ()
1562 in
1563 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
1564 #Restore arg saved
1565 end)
1566 | _ => normal ())
1567 | _ => normal ())
1568 before #Restore arg saved
1649 end 1569 end
1650 | Union (q1, q2) => 1570 | Union (q1, q2) =>
1651 let 1571 let
1652 val (rvN, p1, used1, outs1) = doQuery (q1, rvN) 1572 val saved = #Save arg ()
1653 val (rvN, p2, used2, outs2) = doQuery (q2, rvN)
1654 in 1573 in
1655 case (outs1, outs2) of 1574 doQuery q1;
1656 ([], []) => (rvN, Or (p1, p2), 1575 #Restore arg saved;
1657 map (fn (p, e) => (And (p1, p), e)) used1 1576 doQuery q2;
1658 @ map (fn (p, e) => (And (p2, p), e)) used2, []) 1577 #Restore arg saved
1659 | _ => default ()
1660 end 1578 end
1661 in 1579 in
1662 doQuery (q, rvN) 1580 doQuery q
1663 end 1581 end
1664 end 1582 end
1665 1583
1666 fun insertProp rvN rv e =
1667 let
1668 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1669 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1670 Unknown)
1671 in
1672 case parse query e of
1673 SOME (Query1 r) =>
1674 let
1675 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1676 let
1677 val (rvN, e) = rv rvN
1678 in
1679 ((v, e), rvN)
1680 end) rvN (#From r)
1681
1682 fun rvOf v =
1683 case List.find (fn (v', _) => v' = v) rvs of
1684 NONE => raise Fail "Iflow.insertProp: Bad table variable"
1685 | SOME (_, e) => e
1686
1687 val p =
1688 foldl (fn ((t, v), p) =>
1689 let
1690 val t =
1691 case v of
1692 "New" => t ^ "$New"
1693 | _ => t
1694 in
1695 And (p, Reln (Sql t, [rvOf v]))
1696 end) True (#From r)
1697
1698 val expIn = expIn rv [] rvOf
1699 in
1700 case #Where r of
1701 NONE => p
1702 | SOME e =>
1703 case expIn (e, rvN) of
1704 (inr p', _) => And (p, p')
1705 | _ => p
1706 end
1707 | _ => default ()
1708 end
1709
1710 fun deleteProp rvN rv e =
1711 let
1712 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1713 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1714 Unknown)
1715 in
1716 case parse query e of
1717 SOME (Query1 r) =>
1718 let
1719 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1720 let
1721 val (rvN, e) = rv rvN
1722 in
1723 ((v, e), rvN)
1724 end) rvN (#From r)
1725
1726 fun rvOf v =
1727 case List.find (fn (v', _) => v' = v) rvs of
1728 NONE => raise Fail "Iflow.deleteProp: Bad table variable"
1729 | SOME (_, e) => e
1730
1731 val p =
1732 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
1733
1734 val expIn = expIn rv [] rvOf
1735 in
1736 And (Reln (Sql "$Old", [rvOf "Old"]),
1737 case #Where r of
1738 NONE => p
1739 | SOME e =>
1740 case expIn (e, rvN) of
1741 (inr p', _) => And (p, p')
1742 | _ => p)
1743 end
1744 | _ => default ()
1745 end
1746
1747 fun updateProp rvN rv e =
1748 let
1749 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1750 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1751 Unknown)
1752 in
1753 case parse query e of
1754 SOME (Query1 r) =>
1755 let
1756 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1757 let
1758 val (rvN, e) = rv rvN
1759 in
1760 ((v, e), rvN)
1761 end) rvN (#From r)
1762
1763 fun rvOf v =
1764 case List.find (fn (v', _) => v' = v) rvs of
1765 NONE => raise Fail "Iflow.insertProp: Bad table variable"
1766 | SOME (_, e) => e
1767
1768 val p =
1769 foldl (fn ((t, v), p) =>
1770 let
1771 val t =
1772 case v of
1773 "New" => t ^ "$New"
1774 | _ => t
1775 in
1776 And (p, Reln (Sql t, [rvOf v]))
1777 end) True (#From r)
1778
1779 val expIn = expIn rv [] rvOf
1780 in
1781 And (Reln (Sql "$Old", [rvOf "Old"]),
1782 case #Where r of
1783 NONE => p
1784 | SOME e =>
1785 case expIn (e, rvN) of
1786 (inr p', _) => And (p, p')
1787 | _ => p)
1788 end
1789 | _ => default ()
1790 end
1791
1792 fun evalPat env e (pt, _) = 1584 fun evalPat env e (pt, _) =
1793 case pt of 1585 case pt of
1794 PWild => (env, True) 1586 PWild => env
1795 | PVar _ => (e :: env, True) 1587 | PVar _ => e :: env
1796 | PPrim _ => (env, True) 1588 | PPrim _ => env
1797 | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e])) 1589 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
1798 | PCon (_, pc, SOME pt) => 1590 | PCon (_, pc, SOME pt) =>
1799 let 1591 let
1800 val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt 1592 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
1801 in 1593 in
1802 (env, And (p, Reln (PCon1 (patCon pc), [e]))) 1594 St.assert [AReln (PCon1 (patCon pc), [e])];
1595 env
1803 end 1596 end
1804 | PRecord xpts => 1597 | PRecord xpts =>
1805 foldl (fn ((x, pt, _), (env, p)) => 1598 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
1806 let 1599 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
1807 val (env, p') = evalPat env (Proj (e, x)) pt
1808 in
1809 (env, And (p', p))
1810 end) (env, True) xpts
1811 | PNone _ => (env, Reln (PCon0 "None", [e]))
1812 | PSome (_, pt) => 1600 | PSome (_, pt) =>
1813 let 1601 let
1814 val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt 1602 val env = evalPat env (Func (UnCon "Some", [e])) pt
1815 in 1603 in
1816 (env, And (p, Reln (PCon1 "Some", [e]))) 1604 St.assert [AReln (PCon1 "Some", [e])];
1605 env
1817 end 1606 end
1818 1607
1819 fun peq (p1, p2) = 1608 fun evalExp env (e as (_, loc)) k =
1820 case (p1, p2) of
1821 (True, True) => true
1822 | (False, False) => true
1823 | (Unknown, Unknown) => true
1824 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
1825 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
1826 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
1827 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
1828 | _ => false
1829
1830 fun removeRedundant p1 =
1831 let 1609 let
1832 fun rr p2 = 1610 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
1833 if peq (p1, p2) then 1611
1834 True 1612 fun default () = k (Var (St.nextVar ()))
1835 else
1836 case p2 of
1837 And (x, y) => And (rr x, rr y)
1838 | Or (x, y) => Or (rr x, rr y)
1839 | _ => p2
1840 in
1841 rr
1842 end
1843
1844 datatype cflow = Case | Where
1845 datatype flow = Data | Control of cflow
1846 type check = ErrorMsg.span * exp * prop
1847 type dml = ErrorMsg.span * prop
1848
1849 structure St :> sig
1850 type t
1851 val create : {Var : int,
1852 Ambient : prop} -> t
1853
1854 val curVar : t -> int
1855 val nextVar : t -> t * int
1856
1857 val ambient : t -> prop
1858 val setAmbient : t * prop -> t
1859
1860 val paths : t -> (check * cflow) list
1861 val addPath : t * (check * cflow) -> t
1862 val addPaths : t * (check * cflow) list -> t
1863 val clearPaths : t -> t
1864 val setPaths : t * (check * cflow) list -> t
1865
1866 val sent : t -> (check * flow) list
1867 val addSent : t * (check * flow) -> t
1868 val setSent : t * (check * flow) list -> t
1869
1870 val inserted : t -> dml list
1871 val addInsert : t * dml -> t
1872
1873 val deleted : t -> dml list
1874 val addDelete : t * dml -> t
1875
1876 val updated : t -> dml list
1877 val addUpdate : t * dml -> t
1878 end = struct
1879
1880 type t = {Var : int,
1881 Ambient : prop,
1882 Path : (check * cflow) list,
1883 Sent : (check * flow) list,
1884 Insert : dml list,
1885 Delete : dml list,
1886 Update : dml list}
1887
1888 fun create {Var = v, Ambient = p} = {Var = v,
1889 Ambient = p,
1890 Path = [],
1891 Sent = [],
1892 Insert = [],
1893 Delete = [],
1894 Update = []}
1895
1896 fun curVar (t : t) = #Var t
1897 fun nextVar (t : t) = ({Var = #Var t + 1,
1898 Ambient = #Ambient t,
1899 Path = #Path t,
1900 Sent = #Sent t,
1901 Insert = #Insert t,
1902 Delete = #Delete t,
1903 Update = #Update t}, #Var t)
1904
1905 fun ambient (t : t) = #Ambient t
1906 fun setAmbient (t : t, p) = {Var = #Var t,
1907 Ambient = p,
1908 Path = #Path t,
1909 Sent = #Sent t,
1910 Insert = #Insert t,
1911 Delete = #Delete t,
1912 Update = #Update t}
1913
1914 fun paths (t : t) = #Path t
1915 fun addPath (t : t, c) = {Var = #Var t,
1916 Ambient = #Ambient t,
1917 Path = c :: #Path t,
1918 Sent = #Sent t,
1919 Insert = #Insert t,
1920 Delete = #Delete t,
1921 Update = #Update t}
1922 fun addPaths (t : t, cs) = {Var = #Var t,
1923 Ambient = #Ambient t,
1924 Path = cs @ #Path t,
1925 Sent = #Sent t,
1926 Insert = #Insert t,
1927 Delete = #Delete t,
1928 Update = #Update t}
1929 fun clearPaths (t : t) = {Var = #Var t,
1930 Ambient = #Ambient t,
1931 Path = [],
1932 Sent = #Sent t,
1933 Insert = #Insert t,
1934 Delete = #Delete t,
1935 Update = #Update t}
1936 fun setPaths (t : t, cs) = {Var = #Var t,
1937 Ambient = #Ambient t,
1938 Path = cs,
1939 Sent = #Sent t,
1940 Insert = #Insert t,
1941 Delete = #Delete t,
1942 Update = #Update t}
1943
1944 fun sent (t : t) = #Sent t
1945 fun addSent (t : t, c) = {Var = #Var t,
1946 Ambient = #Ambient t,
1947 Path = #Path t,
1948 Sent = c :: #Sent t,
1949 Insert = #Insert t,
1950 Delete = #Delete t,
1951 Update = #Update t}
1952 fun setSent (t : t, cs) = {Var = #Var t,
1953 Ambient = #Ambient t,
1954 Path = #Path t,
1955 Sent = cs,
1956 Insert = #Insert t,
1957 Delete = #Delete t,
1958 Update = #Update t}
1959
1960 fun inserted (t : t) = #Insert t
1961 fun addInsert (t : t, c) = {Var = #Var t,
1962 Ambient = #Ambient t,
1963 Path = #Path t,
1964 Sent = #Sent t,
1965 Insert = c :: #Insert t,
1966 Delete = #Delete t,
1967 Update = #Update t}
1968
1969 fun deleted (t : t) = #Delete t
1970 fun addDelete (t : t, c) = {Var = #Var t,
1971 Ambient = #Ambient t,
1972 Path = #Path t,
1973 Sent = #Sent t,
1974 Insert = #Insert t,
1975 Delete = c :: #Delete t,
1976 Update = #Update t}
1977
1978 fun updated (t : t) = #Update t
1979 fun addUpdate (t : t, c) = {Var = #Var t,
1980 Ambient = #Ambient t,
1981 Path = #Path t,
1982 Sent = #Sent t,
1983 Insert = #Insert t,
1984 Delete = #Delete t,
1985 Update = c :: #Update t}
1986
1987 end
1988
1989 fun havocReln r =
1990 let
1991 fun hr p =
1992 case p of
1993 True => p
1994 | False => p
1995 | Unknown => p
1996 | And (p1, p2) => And (hr p1, hr p2)
1997 | Or (p1, p2) => Or (hr p1, hr p2)
1998 | Reln (r', _) => if r' = r then True else p
1999 | Cond (e, p) => Cond (e, hr p)
2000 in
2001 hr
2002 end
2003
2004 fun evalExp env (e as (_, loc), st) =
2005 let
2006 fun default () =
2007 let
2008 val (st, nv) = St.nextVar st
2009 in
2010 (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
2011 ("nv", p_exp (Var nv))];*)
2012 (Var nv, st)
2013 end
2014
2015 fun addSent (p, e, st) =
2016 let
2017 val st = if isKnown e then
2018 st
2019 else
2020 St.addSent (st, ((loc, e, p), Data))
2021
2022 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
2023 in
2024 St.clearPaths st
2025 end
2026 1613
2027 fun doFfi (m, s, es) = 1614 fun doFfi (m, s, es) =
2028 if m = "Basis" andalso SS.member (writers, s) then 1615 if m = "Basis" andalso SS.member (writers, s) then
2029 let 1616 let
2030 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1617 fun doArgs es =
1618 case es of
1619 [] => k (Recd [])
1620 | e :: es =>
1621 evalExp env e (fn e => (St.send (e, loc); doArgs es))
2031 in 1622 in
2032 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es) 1623 doArgs es
2033 end 1624 end
2034 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then 1625 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
2035 default () 1626 default ()
2036 else 1627 else
2037 let 1628 let
2038 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1629 fun doArgs (es, acc) =
1630 case es of
1631 [] => k (Func (Other (m ^ "." ^ s), rev acc))
1632 | e :: es =>
1633 evalExp env e (fn e => doArgs (es, e :: acc))
2039 in 1634 in
2040 (Func (Other (m ^ "." ^ s), es), st) 1635 doArgs (es, [])
2041 end 1636 end
2042 in 1637 in
2043 case #1 e of 1638 case #1 e of
2044 EPrim p => (Const p, st) 1639 EPrim p => k (Const p)
2045 | ERel n => (List.nth (env, n), st) 1640 | ERel n => k (List.nth (env, n))
2046 | ENamed _ => default () 1641 | ENamed _ => default ()
2047 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st) 1642 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
2048 | ECon (_, pc, SOME e) => 1643 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
2049 let 1644 | ENone _ => k (Func (DtCon0 "None", []))
2050 val (e, st) = evalExp env (e, st) 1645 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
2051 in
2052 (Func (DtCon1 (patCon pc), [e]), st)
2053 end
2054 | ENone _ => (Func (DtCon0 "None", []), st)
2055 | ESome (_, e) =>
2056 let
2057 val (e, st) = evalExp env (e, st)
2058 in
2059 (Func (DtCon1 "Some", [e]), st)
2060 end
2061 | EFfi _ => default () 1646 | EFfi _ => default ()
2062 1647
2063 | EFfiApp x => doFfi x 1648 | EFfiApp x => doFfi x
2064 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e]) 1649 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
2065 1650
2066 | EApp (e1, e2) => 1651 | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
2067 let
2068 val (e1, st) = evalExp env (e1, st)
2069 in
2070 case e1 of
2071 Finish => (Finish, st)
2072 | _ => default ()
2073 end
2074 1652
2075 | EAbs _ => default () 1653 | EAbs _ => default ()
2076 | EUnop (s, e1) => 1654 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
2077 let 1655 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
2078 val (e1, st) = evalExp env (e1, st)
2079 in
2080 (Func (Other s, [e1]), st)
2081 end
2082 | EBinop (s, e1, e2) =>
2083 let
2084 val (e1, st) = evalExp env (e1, st)
2085 val (e2, st) = evalExp env (e2, st)
2086 in
2087 (Func (Other s, [e1, e2]), st)
2088 end
2089 | ERecord xets => 1656 | ERecord xets =>
2090 let 1657 let
2091 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) => 1658 fun doFields (xes, acc) =
2092 let 1659 case xes of
2093 val (e, st) = evalExp env (e, st) 1660 [] => k (Recd (rev acc))
2094 in 1661 | (x, e, _) :: xes =>
2095 ((x, e), st) 1662 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
2096 end) st xets
2097 in 1663 in
2098 (Recd xes, st) 1664 doFields (xets, [])
2099 end 1665 end
2100 | EField (e, s) => 1666 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
2101 let
2102 val (e, st) = evalExp env (e, st)
2103 in
2104 (Proj (e, s), st)
2105 end
2106 | ECase (e, pes, {result = res, ...}) => 1667 | ECase (e, pes, {result = res, ...}) =>
2107 let 1668 evalExp env e (fn e =>
2108 val (e, st) = evalExp env (e, st)
2109 val (st, r) = St.nextVar st
2110 val orig = St.ambient st
2111 val origPaths = St.paths st
2112
2113 val st = St.addPath (st, ((loc, e, orig), Case))
2114
2115 (*val () = Print.prefaces "Case" [("loc", Print.PD.string (ErrorMsg.spanToString loc)),
2116 ("e", Print.p_list (MonoPrint.p_exp MonoEnv.empty o #2) pes),
2117 ("orig", p_prop orig)]*)
2118
2119 val (st, ambients, paths) =
2120 foldl (fn ((pt, pe), (st, ambients, paths)) =>
2121 let 1669 let
2122 val (env, pp) = evalPat env e pt 1670 val () = St.addPath (e, loc)
2123 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
2124
2125 val this = And (removeRedundant orig (St.ambient st'),
2126 Reln (Eq, [Var r, pe]))
2127 in 1671 in
2128 (St.setPaths (st', origPaths), 1672 app (fn (p, pe) =>
2129 Or (ambients, this), 1673 let
2130 St.paths st' @ paths) 1674 val saved = St.stash ()
2131 end) (st, False, []) pes 1675
2132 1676 val env = evalPat env e p
2133 val st = case #1 res of 1677 in
2134 TRecord [] => St.setPaths (st, origPaths) 1678 evalExp env pe k;
2135 | _ => St.setPaths (st, paths) 1679 St.reinstate saved
2136 in 1680 end) pes
2137 (Var r, St.setAmbient (st, And (orig, ambients))) 1681 end handle Cc.Contradiction => ())
2138 end
2139 | EStrcat (e1, e2) => 1682 | EStrcat (e1, e2) =>
2140 let 1683 evalExp env e1 (fn e1 =>
2141 val (e1, st) = evalExp env (e1, st) 1684 evalExp env e2 (fn e2 =>
2142 val (e2, st) = evalExp env (e2, st) 1685 k (Func (Other "cat", [e1, e2]))))
2143 in 1686 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
2144 (Func (Other "cat", [e1, e2]), st)
2145 end
2146 | EError _ => (Finish, st)
2147 | EReturnBlob {blob = b, mimeType = m, ...} => 1687 | EReturnBlob {blob = b, mimeType = m, ...} =>
2148 let 1688 evalExp env b (fn b =>
2149 val (b, st) = evalExp env (b, st) 1689 (St.send (b, loc);
2150 val (m, st) = evalExp env (m, st) 1690 evalExp env m
2151 in 1691 (fn m => St.send (m, loc))))
2152 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
2153 end
2154 | ERedirect (e, _) => 1692 | ERedirect (e, _) =>
2155 let 1693 evalExp env e (fn e => St.send (e, loc))
2156 val (e, st) = evalExp env (e, st)
2157 in
2158 (Finish, addSent (St.ambient st, e, st))
2159 end
2160 | EWrite e => 1694 | EWrite e =>
2161 let 1695 evalExp env e (fn e => (St.send (e, loc);
2162 val (e, st) = evalExp env (e, st) 1696 k (Recd [])))
2163 in
2164 (Recd [], addSent (St.ambient st, e, st))
2165 end
2166 | ESeq (e1, e2) => 1697 | ESeq (e1, e2) =>
2167 let 1698 evalExp env e1 (fn _ => evalExp env e2 k)
2168 val (_, st) = evalExp env (e1, st)
2169 in
2170 evalExp env (e2, st)
2171 end
2172 | ELet (_, _, e1, e2) => 1699 | ELet (_, _, e1, e2) =>
2173 let 1700 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
2174 val (e1, st) = evalExp env (e1, st)
2175 in
2176 evalExp (e1 :: env) (e2, st)
2177 end
2178 | EClosure (n, es) => 1701 | EClosure (n, es) =>
2179 let 1702 let
2180 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1703 fun doArgs (es, acc) =
1704 case es of
1705 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
1706 | e :: es =>
1707 evalExp env e (fn e => doArgs (es, e :: acc))
2181 in 1708 in
2182 (Func (Other ("Cl" ^ Int.toString n), es), st) 1709 doArgs (es, [])
2183 end 1710 end
2184 1711
2185 | EQuery {query = q, body = b, initial = i, state = state, ...} => 1712 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
2186 let 1713 evalExp env q (fn _ =>
2187 val (_, st) = evalExp env (q, st) 1714 evalExp env i (fn i =>
2188 val (i, st) = evalExp env (i, st) 1715 let
2189 1716 val saved = St.stash ()
2190 val (st', r) = St.nextVar st 1717
2191 val (st', acc) = St.nextVar st' 1718 val r = Var (St.nextVar ())
2192 1719 val acc = Var (St.nextVar ())
2193 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1720 in
2194 val amb = removeRedundant (St.ambient st) (St.ambient st') 1721 if MonoUtil.Exp.existsB {typ = fn _ => false,
2195 1722 exp = fn (n, e) =>
2196 val (st', qp, used, _) = 1723 case e of
2197 queryProp env 1724 ERel n' => n' = n
2198 st' (fn st' => 1725 | _ => false,
2199 let 1726 bind = fn (n, b) =>
2200 val (st', rv) = St.nextVar st' 1727 case b of
2201 in 1728 MonoUtil.Exp.RelE _ => n + 1
2202 (st', Var rv) 1729 | _ => n}
2203 end) 1730 0 b then
2204 (AllCols (Var r)) q 1731 doQuery {Env = env,
2205 1732 NextVar = Var o St.nextVar,
2206 val (st, res) = 1733 Add = fn a => St.assert [a],
2207 case #1 state of 1734 Save = St.stash,
2208 TRecord [] => 1735 Restore = St.reinstate,
2209 (st, Func (DtCon0 "unit", [])) 1736 UsedExp = fn e => St.send (e, loc),
2210 | _ => 1737 Cont = AllCols (fn _ => (St.reinstate saved;
2211 if varInP acc (St.ambient st') then 1738 evalExp
2212 let 1739 (acc :: r :: env)
2213 val (st, r) = St.nextVar st 1740 b (fn _ => default ())))} q
2214 in 1741 else
2215 (st, Var r) 1742 doQuery {Env = env,
2216 end 1743 NextVar = Var o St.nextVar,
2217 else 1744 Add = fn a => St.assert [a],
2218 let 1745 Save = St.stash,
2219 val (st', out) = St.nextVar st' 1746 Restore = St.reinstate,
2220 1747 UsedExp = fn e => St.send (e, loc),
2221 val p = And (St.ambient st, 1748 Cont = AllCols (fn x =>
2222 Or (Reln (Eq, [Var out, i]), 1749 (St.assert [AReln (Eq, [r, x])];
2223 And (Reln (Eq, [Var out, b]), 1750 evalExp (acc :: r :: env) b k))} q
2224 And (qp, amb)))) 1751 end))
2225 in
2226 (St.setAmbient (st', p), Var out)
2227 end
2228
2229 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
2230
2231 val p' = And (qp, St.ambient st')
2232 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
2233 in
2234 (res, St.addPaths (St.setSent (st, sent), paths))
2235 end
2236 | EDml e => 1752 | EDml e =>
2237 (case parse dml e of 1753 (case parse dml e of
2238 NONE => (print ("Warning: Information flow checker can't parse DML command at " 1754 NONE => (print ("Warning: Information flow checker can't parse DML command at "
2239 ^ ErrorMsg.spanToString loc ^ "\n"); 1755 ^ ErrorMsg.spanToString loc ^ "\n");
2240 default ()) 1756 default ())
2241 | SOME d => 1757 | SOME d =>
2242 case d of 1758 case d of
2243 Insert (tab, es) => 1759 Insert (tab, es) =>
2244 let 1760 let
2245 val (st, new) = St.nextVar st 1761 val new = St.nextVar ()
2246 1762
2247 fun rv st = 1763 val expIn = expIn (Var o St.nextVar) env
2248 let 1764 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
2249 val (st, n) = St.nextVar st 1765
2250 in 1766 val es = map (fn (x, e) =>
2251 (st, Var n) 1767 case expIn e of
2252 end 1768 inl e => (x, e)
2253 1769 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
2254 val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT") 1770 es
2255 1771
2256 val (es, st) = ListUtil.foldlMap 1772 val saved = St.stash ()
2257 (fn ((x, e), st) =>
2258 let
2259 val (e, st) = case expIn (e, st) of
2260 (inl e, st) => (e, st)
2261 | (inr _, _) => raise Fail
2262 ("Iflow.evalExp: Selecting "
2263 ^ "boolean expression")
2264 in
2265 ((x, e), st)
2266 end)
2267 st es
2268 in 1773 in
2269 (Recd [], St.addInsert (st, (loc, And (St.ambient st, 1774 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
2270 Reln (Sql (tab ^ "$New"), [Recd es]))))) 1775 St.insert loc;
1776 St.reinstate saved;
1777 k (Recd [])
2271 end 1778 end
2272 | Delete (tab, e) => 1779 | Delete (tab, e) =>
2273 let 1780 let
2274 val (st, old) = St.nextVar st 1781 val old = St.nextVar ()
2275 1782
2276 fun rv st = 1783 val expIn = expIn (Var o St.nextVar) env
2277 let 1784 (fn "T" => Var old
2278 val (st, n) = St.nextVar st 1785 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
2279 in 1786
2280 (st, Var n) 1787 val p = case expIn e of
2281 end 1788 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
2282 1789 | inr p => p
2283 val expIn = expIn rv env (fn "T" => Var old 1790
2284 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE") 1791 val saved = St.stash ()
2285
2286 val (p, st) = case expIn (e, st) of
2287 (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean"
2288 | (inr p, st) => (p, st)
2289
2290 val p = And (p,
2291 And (Reln (Sql "$Old", [Var old]),
2292 Reln (Sql tab, [Var old])))
2293
2294 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
2295 in 1792 in
2296 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p)))) 1793 St.assert [AReln (Sql "$Old", [Var old]),
1794 AReln (Sql tab, [Var old])];
1795 decomp {Save = St.stash,
1796 Restore = St.reinstate,
1797 Add = fn a => St.assert [a]} p
1798 (fn () => (St.delete loc;
1799 St.reinstate saved;
1800 St.havocReln (Sql tab);
1801 k (Recd []))
1802 handle Cc.Contradiction => ())
2297 end 1803 end
2298 | Update (tab, fs, e) => 1804 | Update (tab, fs, e) =>
2299 let 1805 let
2300 val (st, new) = St.nextVar st 1806 val new = St.nextVar ()
2301 val (st, old) = St.nextVar st 1807 val old = St.nextVar ()
2302 1808
2303 fun rv st = 1809 val expIn = expIn (Var o St.nextVar) env
2304 let 1810 (fn "T" => Var old
2305 val (st, n) = St.nextVar st 1811 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
2306 in 1812
2307 (st, Var n) 1813 val fs = map
2308 end 1814 (fn (x, e) =>
2309 1815 (x, case expIn e of
2310 val expIn = expIn rv env (fn "T" => Var old 1816 inl e => e
2311 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE") 1817 | inr _ => raise Fail
2312 1818 ("Iflow.evalExp: Selecting "
2313 val (fs, st) = ListUtil.foldlMap 1819 ^ "boolean expression")))
2314 (fn ((x, e), st) => 1820 fs
2315 let
2316 val (e, st) = case expIn (e, st) of
2317 (inl e, st) => (e, st)
2318 | (inr _, _) => raise Fail
2319 ("Iflow.evalExp: Selecting "
2320 ^ "boolean expression")
2321 in
2322 ((x, e), st)
2323 end)
2324 st fs
2325 1821
2326 val fs' = case SM.find (!tabs, tab) of 1822 val fs' = case SM.find (!tabs, tab) of
2327 NONE => raise Fail "Iflow.evalExp: Updating unknown table" 1823 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
2328 | SOME (fs', _) => fs' 1824 | SOME (fs', _) => fs'
2329 1825
2331 if List.exists (fn (f', _) => f' = f) fs then 1827 if List.exists (fn (f', _) => f' = f) fs then
2332 fs 1828 fs
2333 else 1829 else
2334 (f, Proj (Var old, f)) :: fs) fs fs' 1830 (f, Proj (Var old, f)) :: fs) fs fs'
2335 1831
2336 val (p, st) = case expIn (e, st) of 1832 val p = case expIn e of
2337 (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean" 1833 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
2338 | (inr p, st) => (p, st) 1834 | inr p => p
2339 1835 val saved = St.stash ()
2340 val p = And (p,
2341 And (Reln (Sql (tab ^ "$New"), [Recd fs]),
2342 And (Reln (Sql "$Old", [Var old]),
2343 Reln (Sql tab, [Var old]))))
2344
2345 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
2346 in 1836 in
2347 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p)))) 1837 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
1838 AReln (Sql "$Old", [Var old]),
1839 AReln (Sql tab, [Var old])];
1840 decomp {Save = St.stash,
1841 Restore = St.reinstate,
1842 Add = fn a => St.assert [a]} p
1843 (fn () => (St.update loc;
1844 St.reinstate saved;
1845 St.havocReln (Sql tab);
1846 k (Recd []))
1847 handle Cc.Contradiction => ())
2348 end) 1848 end)
2349 1849
2350 | ENextval (EPrim (Prim.String seq), _) => 1850 | ENextval (EPrim (Prim.String seq), _) =>
2351 let 1851 let
2352 val (st, nv) = St.nextVar st 1852 val nv = St.nextVar ()
2353 in 1853 in
2354 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv])))) 1854 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
1855 k (Var nv)
2355 end 1856 end
2356 | ENextval _ => default () 1857 | ENextval _ => default ()
2357 | ESetval _ => default () 1858 | ESetval _ => default ()
2358 1859
2359 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) => 1860 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
2360 let 1861 let
2361 val (st, nv) = St.nextVar st 1862 val nv = St.nextVar ()
2362 in 1863 in
2363 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv])))) 1864 St.assert [AReln (Known, [Var nv])];
1865 k (Var nv)
2364 end 1866 end
2365 1867
2366 | EUnurlify _ => default () 1868 | EUnurlify _ => default ()
2367 | EJavaScript _ => default () 1869 | EJavaScript _ => default ()
2368 | ESignalReturn _ => default () 1870 | ESignalReturn _ => default ()
2374 | ESpawn _ => default () 1876 | ESpawn _ => default ()
2375 end 1877 end
2376 1878
2377 fun check file = 1879 fun check file =
2378 let 1880 let
1881 val () = St.reset ()
1882
2379 val file = MonoReduce.reduce file 1883 val file = MonoReduce.reduce file
2380 val file = MonoOpt.optimize file 1884 val file = MonoOpt.optimize file
2381 val file = Fuse.fuse file 1885 val file = Fuse.fuse file
2382 val file = MonoOpt.optimize file 1886 val file = MonoOpt.optimize file
2383 val file = MonoShake.shake file 1887 val file = MonoShake.shake file
2386 val exptd = foldl (fn ((d, _), exptd) => 1890 val exptd = foldl (fn ((d, _), exptd) =>
2387 case d of 1891 case d of
2388 DExport (_, _, n, _, _, _) => IS.add (exptd, n) 1892 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
2389 | _ => exptd) IS.empty file 1893 | _ => exptd) IS.empty file
2390 1894
2391 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) = 1895 fun decl (d, _) =
2392 case d of 1896 case d of
2393 DTable (tab, fs, pk, _) => 1897 DTable (tab, fs, pk, _) =>
2394 let 1898 let
2395 val ks = 1899 val ks =
2396 case #1 pk of 1900 case #1 pk of
2399 [] => [] 1903 [] => []
2400 | pk => [pk]) 1904 | pk => [pk])
2401 | _ => [] 1905 | _ => []
2402 in 1906 in
2403 if size tab >= 3 then 1907 if size tab >= 3 then
2404 (tabs := SM.insert (!tabs, String.extract (tab, 3, NONE), 1908 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
2405 (map #1 fs, 1909 (map #1 fs,
2406 map (map (fn s => str (Char.toUpper (String.sub (s, 3))) 1910 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
2407 ^ String.extract (s, 4, NONE))) ks)); 1911 ^ String.extract (s, 4, NONE))) ks))
2408 (vals, inserts, deletes, updates, client, insert, delete, update))
2409 else 1912 else
2410 raise Fail "Table name does not begin with uw_" 1913 raise Fail "Table name does not begin with uw_"
2411 end 1914 end
2412 | DVal (_, n, _, e, _) => 1915 | DVal (_, n, _, e, _) =>
2413 let 1916 let
2414 val isExptd = IS.member (exptd, n) 1917 val isExptd = IS.member (exptd, n)
2415 1918
2416 fun deAbs (e, env, nv, p) = 1919 val saved = St.stash ()
1920
1921 fun deAbs (e, env, ps) =
2417 case #1 e of 1922 case #1 e of
2418 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1, 1923 EAbs (_, _, _, e) =>
2419 if isExptd then 1924 let
2420 And (p, Reln (Known, [Var nv])) 1925 val nv = Var (St.nextVar ())
2421 else 1926 in
2422 p) 1927 deAbs (e, nv :: env,
2423 | _ => (e, env, nv, p) 1928 if isExptd then
2424 1929 AReln (Known, [nv]) :: ps
2425 val (e, env, nv, p) = deAbs (e, [], 1, True) 1930 else
2426 1931 ps)
2427 val (_, st) = evalExp env (e, St.create {Var = nv, 1932 end
2428 Ambient = p}) 1933 | _ => (e, env, ps)
1934
1935 val (e, env, ps) = deAbs (e, [], [])
2429 in 1936 in
2430 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates, 1937 St.assert ps;
2431 client, insert, delete, update) 1938 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
1939 St.reinstate saved
2432 end 1940 end
2433 1941
2434 | DPolicy pol => 1942 | DPolicy pol =>
2435 let 1943 let
2436 fun rv rvN = (rvN + 1, Lvar rvN) 1944 val rvN = ref 0
1945 fun rv () =
1946 let
1947 val n = !rvN
1948 in
1949 rvN := n + 1;
1950 Lvar n
1951 end
1952
1953 val atoms = ref ([] : atom list)
1954 fun doQ k = doQuery {Env = [],
1955 NextVar = rv,
1956 Add = fn a => atoms := a :: !atoms,
1957 Save = fn () => !atoms,
1958 Restore = fn ls => atoms := ls,
1959 UsedExp = fn _ => (),
1960 Cont = SomeCol (fn es => k (!atoms, es))}
2437 in 1961 in
2438 case pol of 1962 case pol of
2439 PolClient e => 1963 PolClient e =>
2440 let 1964 doQ (fn (ats, es) => St.allowSend (ats, es)) e
2441 val (_, p, _, outs) = queryProp [] 0 rv SomeCol e
2442 in
2443 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
2444 end
2445 | PolInsert e => 1965 | PolInsert e =>
2446 let 1966 doQ (fn (ats, _) => St.allowInsert ats) e
2447 val p = insertProp 0 rv e
2448 in
2449 (vals, inserts, deletes, updates, client, p :: insert, delete, update)
2450 end
2451 | PolDelete e => 1967 | PolDelete e =>
2452 let 1968 doQ (fn (ats, _) => St.allowDelete ats) e
2453 val p = deleteProp 0 rv e
2454 in
2455 (vals, inserts, deletes, updates, client, insert, p :: delete, update)
2456 end
2457 | PolUpdate e => 1969 | PolUpdate e =>
2458 let 1970 doQ (fn (ats, _) => St.allowUpdate ats) e
2459 val p = updateProp 0 rv e
2460 in
2461 (vals, inserts, deletes, updates, client, insert, delete, p :: update)
2462 end
2463 | PolSequence e => 1971 | PolSequence e =>
2464 (case #1 e of 1972 (case #1 e of
2465 EPrim (Prim.String seq) => 1973 EPrim (Prim.String seq) =>
2466 let 1974 let
2467 val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0]) 1975 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
2468 val outs = [Lvar 0] 1976 val outs = [Lvar 0]
2469 in 1977 in
2470 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update) 1978 St.allowSend ([p], outs)
2471 end 1979 end
2472 | _ => (vals, inserts, deletes, updates, client, insert, delete, update)) 1980 | _ => ())
2473 end 1981 end
2474 1982
2475 | _ => (vals, inserts, deletes, updates, client, insert, delete, update) 1983 | _ => ()
2476
2477 val () = reset ()
2478
2479 val (vals, inserts, deletes, updates, client, insert, delete, update) =
2480 foldl decl ([], [], [], [], [], [], [], []) file
2481
2482
2483 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
2484 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
2485
2486 fun doDml (cmds, pols) =
2487 app (fn (loc, p) =>
2488 if decompH p
2489 (fn hyps =>
2490 let
2491 val cc = ccOf hyps
2492 in
2493 List.exists (fn p' =>
2494 if decompG p'
2495 (fn goals => imply (cc, hyps, goals, NONE)) then
2496 ((*reset ();
2497 Print.prefaces "Match" [("hyp", p_prop p),
2498 ("goal", p_prop p')];*)
2499 true)
2500 else
2501 false)
2502 pols
2503 end handle Cc.Contradiction => true) then
2504 ()
2505 else
2506 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
2507 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
2508 in 1984 in
2509 app (fn ((loc, e, p), fl) => 1985 app decl file
2510 let
2511 fun doOne e =
2512 let
2513 val p = And (p, Reln (Eq, [Var 0, e]))
2514 in
2515 if decompH p
2516 (fn hyps =>
2517 let
2518 val cc = ccOf hyps
2519
2520 fun relevant () =
2521 let
2522 val avail = foldl (fn (AReln (Sql tab, _), avail) =>
2523 SS.add (avail, tab)
2524 | (_, avail) => avail) SS.empty hyps
2525
2526 val ls = List.filter
2527 (fn (g1, _) =>
2528 decompG g1
2529 (List.all (fn AReln (Sql tab, _) =>
2530 SS.member (avail, tab)
2531 | _ => true))) client
2532 in
2533 (*print ("Max: " ^ Int.toString (length ls) ^ "\n");*)
2534 ls
2535 end
2536
2537 fun tryCombos (maxLv, pols, g, outs) =
2538 case pols of
2539 [] =>
2540 decompG g
2541 (fn goals => imply (cc, hyps, goals, SOME outs))
2542 | (g1, outs1) :: pols =>
2543 let
2544 val g1 = bumpLvarsP (maxLv + 1) g1
2545 val outs1 = map (bumpLvars (maxLv + 1)) outs1
2546 fun skip () = tryCombos (maxLv, pols, g, outs)
2547 in
2548 skip ()
2549 orelse tryCombos (Int.max (maxLv,
2550 maxLvarP g1),
2551 pols,
2552 And (g1, g),
2553 outs1 @ outs)
2554 end
2555 in
2556 (fl <> Control Where
2557 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
2558 orelse List.exists (fn (p', outs) =>
2559 decompG p'
2560 (fn goals => imply (cc, hyps, goals,
2561 SOME outs)))
2562 client
2563 orelse tryCombos (0, relevant (), True, [])
2564 orelse (reset ();
2565 Print.preface ("Untenable hypotheses"
2566 ^ (case fl of
2567 Control Where => " (WHERE clause)"
2568 | Control Case => " (case discriminee)"
2569 | Data => " (returned data value)"),
2570 Print.p_list p_atom hyps);
2571 (*Print.preface ("DB", Cc.p_database cc);*)
2572 false)
2573 end handle Cc.Contradiction => true) then
2574 ()
2575 else
2576 ErrorMsg.errorAt loc "The information flow policy may be violated here."
2577 end
2578
2579 fun doAll e =
2580 case e of
2581 Const _ => ()
2582 | Var _ => doOne e
2583 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
2584 | Func (UnCon _, [_]) => doOne e
2585 | Func (_, es) => app doAll es
2586 | Recd xes => app (doAll o #2) xes
2587 | Proj _ => doOne e
2588 | Finish => ()
2589 in
2590 doAll e
2591 end) vals;
2592
2593 doDml (inserts, insert);
2594 doDml (deletes, delete);
2595 doDml (updates, update)
2596 end 1986 end
2597 1987
2598 val check = fn file => 1988 val check = fn file =>
2599 let 1989 let
2600 val oldInline = Settings.getMonoInline () 1990 val oldInline = Settings.getMonoInline ()