Mercurial > urweb

annotate src/iflow.sml @ 1231:5fa8ae2a34e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Avoid pointless rebuilding of hypothesis E-graphs
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:25:45 -0400
parents 8768145eed1e
children efbefd6e3f6c
rev   line source
adamc@1200 1 (* Copyright (c) 2010, Adam Chlipala
adamc@1200 2 * All rights reserved.
adamc@1200 3 *
adamc@1200 4 * Redistribution and use in source and binary forms, with or without
adamc@1200 5 * modification, are permitted provided that the following conditions are met:
adamc@1200 6 *
adamc@1200 7 * - Redistributions of source code must retain the above copyright notice,
adamc@1200 8 * this list of conditions and the following disclaimer.
adamc@1200 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200 10 * this list of conditions and the following disclaimer in the documentation
adamc@1200 11 * and/or other materials provided with the distribution.
adamc@1200 12 * - The names of contributors may not be used to endorse or promote products
adamc@1200 13 * derived from this software without specific prior written permission.
adamc@1200 14 *
adamc@1200 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@1200 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@1200 26 *)
adamc@1200 27
adamc@1200 28 structure Iflow :> IFLOW = struct
adamc@1200 29
adamc@1200 30 open Mono
adamc@1200 31
adamc@1207 32 structure IS = IntBinarySet
adamc@1202 33 structure IM = IntBinaryMap
adamc@1202 34
adamc@1215 35 structure SK = struct
adamc@1215 36 type ord_key = string
adamc@1215 37 val compare = String.compare
adamc@1215 38 end
adamc@1215 39
adamc@1215 40 structure SS = BinarySetFn(SK)
adamc@1215 41 structure SM = BinaryMapFn(SK)
adamc@1200 42
adamc@1200 43 val writers = ["htmlifyInt_w",
adamc@1200 44 "htmlifyFloat_w",
adamc@1200 45 "htmlifyString_w",
adamc@1200 46 "htmlifyBool_w",
adamc@1200 47 "htmlifyTime_w",
adamc@1200 48 "attrifyInt_w",
adamc@1200 49 "attrifyFloat_w",
adamc@1200 50 "attrifyString_w",
adamc@1200 51 "attrifyChar_w",
adamc@1200 52 "urlifyInt_w",
adamc@1200 53 "urlifyFloat_w",
adamc@1200 54 "urlifyString_w",
adamc@1213 55 "urlifyBool_w",
adamc@1213 56 "set_cookie"]
adamc@1200 57
adamc@1200 58 val writers = SS.addList (SS.empty, writers)
adamc@1200 59
adamc@1200 60 type lvar = int
adamc@1200 61
adamc@1215 62 datatype func =
adamc@1215 63 DtCon0 of string
adamc@1215 64 | DtCon1 of string
adamc@1215 65 | UnCon of string
adamc@1215 66 | Other of string
adamc@1215 67
adamc@1200 68 datatype exp =
adamc@1200 69 Const of Prim.t
adamc@1200 70 | Var of int
adamc@1200 71 | Lvar of lvar
adamc@1215 72 | Func of func * exp list
adamc@1200 73 | Recd of (string * exp) list
adamc@1200 74 | Proj of exp * string
adamc@1200 75 | Finish
adamc@1200 76
adamc@1200 77 datatype reln =
adamc@1207 78 Known
adamc@1207 79 | Sql of string
adamc@1215 80 | PCon0 of string
adamc@1215 81 | PCon1 of string
adamc@1200 82 | Eq
adamc@1210 83 | Ne
adamc@1210 84 | Lt
adamc@1210 85 | Le
adamc@1210 86 | Gt
adamc@1210 87 | Ge
adamc@1200 88
adamc@1200 89 datatype prop =
adamc@1200 90 True
adamc@1200 91 | False
adamc@1200 92 | Unknown
adamc@1200 93 | And of prop * prop
adamc@1200 94 | Or of prop * prop
adamc@1200 95 | Reln of reln * exp list
adamc@1212 96 | Cond of exp * prop
adamc@1200 97
adamc@1215 98 val unif = ref (IM.empty : exp IM.map)
adamc@1215 99
adamc@1215 100 fun reset () = unif := IM.empty
adamc@1215 101 fun save () = !unif
adamc@1215 102 fun restore x = unif := x
adamc@1215 103
adamc@1200 104 local
adamc@1207 105 open Print
adamc@1207 106 val string = PD.string
adamc@1207 107 in
adamc@1207 108
adamc@1215 109 fun p_func f =
adamc@1215 110 string (case f of
adamc@1215 111 DtCon0 s => s
adamc@1215 112 | DtCon1 s => s
adamc@1215 113 | UnCon s => "un" ^ s
adamc@1215 114 | Other s => s)
adamc@1215 115
adamc@1207 116 fun p_exp e =
adamc@1207 117 case e of
adamc@1207 118 Const p => Prim.p_t p
adamc@1207 119 | Var n => string ("x" ^ Int.toString n)
adamc@1215 120 | Lvar n =>
adamc@1215 121 (case IM.find (!unif, n) of
adamc@1215 122 NONE => string ("X" ^ Int.toString n)
adamc@1215 123 | SOME e => p_exp e)
adamc@1215 124 | Func (f, es) => box [p_func f,
adamc@1215 125 string "(",
adamc@1207 126 p_list p_exp es,
adamc@1207 127 string ")"]
adamc@1207 128 | Recd xes => box [string "{",
adamc@1210 129 p_list (fn (x, e) => box [string x,
adamc@1207 130 space,
adamc@1207 131 string "=",
adamc@1207 132 space,
adamc@1207 133 p_exp e]) xes,
adamc@1207 134 string "}"]
adamc@1207 135 | Proj (e, x) => box [p_exp e,
adamc@1207 136 string ("." ^ x)]
adamc@1207 137 | Finish => string "FINISH"
adamc@1207 138
adamc@1210 139 fun p_bop s es =
adamc@1210 140 case es of
adamc@1210 141 [e1, e2] => box [p_exp e1,
adamc@1210 142 space,
adamc@1210 143 string s,
adamc@1210 144 space,
adamc@1210 145 p_exp e2]
adamc@1210 146 | _ => raise Fail "Iflow.p_bop"
adamc@1210 147
adamc@1207 148 fun p_reln r es =
adamc@1207 149 case r of
adamc@1207 150 Known =>
adamc@1207 151 (case es of
adamc@1207 152 [e] => box [string "known(",
adamc@1207 153 p_exp e,
adamc@1207 154 string ")"]
adamc@1207 155 | _ => raise Fail "Iflow.p_reln: Known")
adamc@1207 156 | Sql s => box [string (s ^ "("),
adamc@1207 157 p_list p_exp es,
adamc@1207 158 string ")"]
adamc@1215 159 | PCon0 s => box [string (s ^ "("),
adamc@1215 160 p_list p_exp es,
adamc@1215 161 string ")"]
adamc@1215 162 | PCon1 s => box [string (s ^ "("),
adamc@1211 163 p_list p_exp es,
adamc@1211 164 string ")"]
adamc@1210 165 | Eq => p_bop "=" es
adamc@1210 166 | Ne => p_bop "<>" es
adamc@1210 167 | Lt => p_bop "<" es
adamc@1210 168 | Le => p_bop "<=" es
adamc@1210 169 | Gt => p_bop ">" es
adamc@1210 170 | Ge => p_bop ">=" es
adamc@1207 171
adamc@1207 172 fun p_prop p =
adamc@1207 173 case p of
adamc@1207 174 True => string "True"
adamc@1207 175 | False => string "False"
adamc@1207 176 | Unknown => string "??"
adamc@1207 177 | And (p1, p2) => box [string "(",
adamc@1207 178 p_prop p1,
adamc@1207 179 string ")",
adamc@1207 180 space,
adamc@1207 181 string "&&",
adamc@1207 182 space,
adamc@1207 183 string "(",
adamc@1207 184 p_prop p2,
adamc@1207 185 string ")"]
adamc@1207 186 | Or (p1, p2) => box [string "(",
adamc@1207 187 p_prop p1,
adamc@1207 188 string ")",
adamc@1207 189 space,
adamc@1207 190 string "||",
adamc@1207 191 space,
adamc@1207 192 string "(",
adamc@1207 193 p_prop p2,
adamc@1207 194 string ")"]
adamc@1207 195 | Reln (r, es) => p_reln r es
adamc@1212 196 | Cond (e, p) => box [string "(",
adamc@1212 197 p_exp e,
adamc@1212 198 space,
adamc@1212 199 string "==",
adamc@1212 200 space,
adamc@1212 201 p_prop p,
adamc@1212 202 string ")"]
adamc@1207 203
adamc@1207 204 end
adamc@1207 205
adamc@1207 206 local
adamc@1202 207 val count = ref 1
adamc@1200 208 in
adamc@1200 209 fun newLvar () =
adamc@1200 210 let
adamc@1200 211 val n = !count
adamc@1200 212 in
adamc@1200 213 count := n + 1;
adamc@1200 214 n
adamc@1200 215 end
adamc@1200 216 end
adamc@1200 217
adamc@1200 218 fun isKnown e =
adamc@1200 219 case e of
adamc@1200 220 Const _ => true
adamc@1200 221 | Func (_, es) => List.all isKnown es
adamc@1200 222 | Recd xes => List.all (isKnown o #2) xes
adamc@1200 223 | Proj (e, _) => isKnown e
adamc@1200 224 | _ => false
adamc@1200 225
adamc@1200 226 fun isFinish e =
adamc@1200 227 case e of
adamc@1200 228 Finish => true
adamc@1200 229 | _ => false
adamc@1200 230
adamc@1200 231 fun simplify e =
adamc@1200 232 case e of
adamc@1200 233 Const _ => e
adamc@1200 234 | Var _ => e
adamc@1208 235 | Lvar n =>
adamc@1208 236 (case IM.find (!unif, n) of
adamc@1208 237 NONE => e
adamc@1208 238 | SOME e => simplify e)
adamc@1215 239 | Func (f, es) => Func (f, map simplify es)
adamc@1215 240 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
adamc@1215 241 | Proj (e, s) => Proj (simplify e, s)
adamc@1200 242 | Finish => Finish
adamc@1200 243
adamc@1212 244 datatype atom =
adamc@1212 245 AReln of reln * exp list
adamc@1212 246 | ACond of exp * prop
adamc@1212 247
adamc@1212 248 fun p_atom a =
adamc@1212 249 p_prop (case a of
adamc@1212 250 AReln x => Reln x
adamc@1212 251 | ACond x => Cond x)
adamc@1212 252
adamc@1202 253 fun lvarIn lv =
adamc@1202 254 let
adamc@1202 255 fun lvi e =
adamc@1202 256 case e of
adamc@1202 257 Const _ => false
adamc@1202 258 | Var _ => false
adamc@1202 259 | Lvar lv' => lv' = lv
adamc@1202 260 | Func (_, es) => List.exists lvi es
adamc@1202 261 | Recd xes => List.exists (lvi o #2) xes
adamc@1202 262 | Proj (e, _) => lvi e
adamc@1202 263 | Finish => false
adamc@1202 264 in
adamc@1202 265 lvi
adamc@1202 266 end
adamc@1202 267
adamc@1212 268 fun lvarInP lv =
adamc@1212 269 let
adamc@1212 270 fun lvi p =
adamc@1212 271 case p of
adamc@1212 272 True => false
adamc@1212 273 | False => false
adamc@1212 274 | Unknown => true
adamc@1212 275 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 276 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 277 | Reln (_, es) => List.exists (lvarIn lv) es
adamc@1212 278 | Cond (e, p) => lvarIn lv e orelse lvi p
adamc@1212 279 in
adamc@1212 280 lvi
adamc@1212 281 end
adamc@1212 282
adamc@1212 283 fun varIn lv =
adamc@1212 284 let
adamc@1212 285 fun lvi e =
adamc@1212 286 case e of
adamc@1212 287 Const _ => false
adamc@1212 288 | Lvar _ => false
adamc@1212 289 | Var lv' => lv' = lv
adamc@1212 290 | Func (_, es) => List.exists lvi es
adamc@1212 291 | Recd xes => List.exists (lvi o #2) xes
adamc@1212 292 | Proj (e, _) => lvi e
adamc@1212 293 | Finish => false
adamc@1212 294 in
adamc@1212 295 lvi
adamc@1212 296 end
adamc@1212 297
adamc@1212 298 fun varInP lv =
adamc@1212 299 let
adamc@1212 300 fun lvi p =
adamc@1212 301 case p of
adamc@1212 302 True => false
adamc@1212 303 | False => false
adamc@1212 304 | Unknown => false
adamc@1212 305 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 306 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 307 | Reln (_, es) => List.exists (varIn lv) es
adamc@1212 308 | Cond (e, p) => varIn lv e orelse lvi p
adamc@1212 309 in
adamc@1212 310 lvi
adamc@1212 311 end
adamc@1212 312
adamc@1228 313 fun bumpLvars by =
adamc@1228 314 let
adamc@1228 315 fun lvi e =
adamc@1228 316 case e of
adamc@1228 317 Const _ => e
adamc@1228 318 | Var _ => e
adamc@1228 319 | Lvar lv => Lvar (lv + by)
adamc@1228 320 | Func (f, es) => Func (f, map lvi es)
adamc@1228 321 | Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes)
adamc@1228 322 | Proj (e, f) => Proj (lvi e, f)
adamc@1228 323 | Finish => e
adamc@1228 324 in
adamc@1228 325 lvi
adamc@1228 326 end
adamc@1228 327
adamc@1228 328 fun bumpLvarsP by =
adamc@1228 329 let
adamc@1228 330 fun lvi p =
adamc@1228 331 case p of
adamc@1228 332 True => p
adamc@1228 333 | False => p
adamc@1228 334 | Unknown => p
adamc@1228 335 | And (p1, p2) => And (lvi p1, lvi p2)
adamc@1228 336 | Or (p1, p2) => And (lvi p1, lvi p2)
adamc@1228 337 | Reln (r, es) => Reln (r, map (bumpLvars by) es)
adamc@1228 338 | Cond (e, p) => Cond (bumpLvars by e, lvi p)
adamc@1228 339 in
adamc@1228 340 lvi
adamc@1228 341 end
adamc@1228 342
adamc@1228 343 fun maxLvar e =
adamc@1228 344 let
adamc@1228 345 fun lvi e =
adamc@1228 346 case e of
adamc@1228 347 Const _ => 0
adamc@1228 348 | Var _ => 0
adamc@1228 349 | Lvar lv => lv
adamc@1228 350 | Func (f, es) => foldl Int.max 0 (map lvi es)
adamc@1228 351 | Recd xes => foldl Int.max 0 (map (lvi o #2) xes)
adamc@1228 352 | Proj (e, f) => lvi e
adamc@1228 353 | Finish => 0
adamc@1228 354 in
adamc@1228 355 lvi e
adamc@1228 356 end
adamc@1228 357
adamc@1228 358 fun maxLvarP p =
adamc@1228 359 let
adamc@1228 360 fun lvi p =
adamc@1228 361 case p of
adamc@1228 362 True => 0
adamc@1228 363 | False => 0
adamc@1228 364 | Unknown => 0
adamc@1228 365 | And (p1, p2) => Int.max (lvi p1, lvi p2)
adamc@1228 366 | Or (p1, p2) => Int.max (lvi p1, lvi p2)
adamc@1228 367 | Reln (r, es) => foldl Int.max 0 (map maxLvar es)
adamc@1228 368 | Cond (e, p) => Int.max (maxLvar e, lvi p)
adamc@1228 369 in
adamc@1228 370 lvi p
adamc@1228 371 end
adamc@1228 372
adamc@1202 373 fun eq' (e1, e2) =
adamc@1202 374 case (e1, e2) of
adamc@1202 375 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202 376 | (Var n1, Var n2) => n1 = n2
adamc@1202 377
adamc@1202 378 | (Lvar n1, _) =>
adamc@1202 379 (case IM.find (!unif, n1) of
adamc@1202 380 SOME e1 => eq' (e1, e2)
adamc@1202 381 | NONE =>
adamc@1202 382 case e2 of
adamc@1202 383 Lvar n2 =>
adamc@1202 384 (case IM.find (!unif, n2) of
adamc@1202 385 SOME e2 => eq' (e1, e2)
adamc@1202 386 | NONE => n1 = n2
adamc@1208 387 orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202 388 true))
adamc@1202 389 | _ =>
adamc@1202 390 if lvarIn n1 e2 then
adamc@1202 391 false
adamc@1202 392 else
adamc@1202 393 (unif := IM.insert (!unif, n1, e2);
adamc@1202 394 true))
adamc@1202 395
adamc@1202 396 | (_, Lvar n2) =>
adamc@1202 397 (case IM.find (!unif, n2) of
adamc@1202 398 SOME e2 => eq' (e1, e2)
adamc@1202 399 | NONE =>
adamc@1202 400 if lvarIn n2 e1 then
adamc@1202 401 false
adamc@1202 402 else
adamc@1213 403 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
adamc@1213 404 ("e1", p_exp e1)];*)
adamc@1213 405 unif := IM.insert (!unif, n2, e1);
adamc@1202 406 true))
adamc@1202 407
adamc@1202 408 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202 409 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202 410 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202 411 | (Finish, Finish) => true
adamc@1202 412 | _ => false
adamc@1202 413
adamc@1202 414 fun eq (e1, e2) =
adamc@1202 415 let
adamc@1203 416 val saved = save ()
adamc@1202 417 in
adamc@1202 418 if eq' (simplify e1, simplify e2) then
adamc@1202 419 true
adamc@1202 420 else
adamc@1203 421 (restore saved;
adamc@1202 422 false)
adamc@1202 423 end
adamc@1202 424
adamc@1208 425 val debug = ref false
adamc@1208 426
adamc@1211 427 fun eeq (e1, e2) =
adamc@1211 428 case (e1, e2) of
adamc@1211 429 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211 430 | (Var n1, Var n2) => n1 = n2
adamc@1211 431 | (Lvar n1, Lvar n2) => n1 = n2
adamc@1211 432 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211 433 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211 434 List.all (fn (x2, e2) =>
adamc@1211 435 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211 436 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211 437 | (Finish, Finish) => true
adamc@1211 438 | _ => false
adamc@1211 439
adamc@1208 440 (* Congruence closure *)
adamc@1208 441 structure Cc :> sig
adamc@1215 442 type database
adamc@1215 443
adamc@1215 444 exception Contradiction
adamc@1215 445 exception Undetermined
adamc@1215 446
adamc@1215 447 val database : unit -> database
adamc@1215 448
adamc@1215 449 val assert : database * atom -> unit
adamc@1215 450 val check : database * atom -> bool
adamc@1215 451
adamc@1215 452 val p_database : database Print.printer
adamc@1218 453
adamc@1218 454 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
adamc@1226 455
adamc@1226 456 val p_repOf : database -> exp Print.printer
adamc@1208 457 end = struct
adamc@1208 458
adamc@1215 459 exception Contradiction
adamc@1215 460 exception Undetermined
adamc@1208 461
adamc@1215 462 structure CM = BinaryMapFn(struct
adamc@1215 463 type ord_key = Prim.t
adamc@1215 464 val compare = Prim.compare
adamc@1215 465 end)
adamc@1208 466
adamc@1215 467 datatype node = Node of {Rep : node ref option ref,
adamc@1215 468 Cons : node ref SM.map ref,
adamc@1215 469 Variety : variety,
adamc@1215 470 Known : bool ref}
adamc@1208 471
adamc@1215 472 and variety =
adamc@1215 473 Dt0 of string
adamc@1215 474 | Dt1 of string * node ref
adamc@1215 475 | Prim of Prim.t
adamc@1221 476 | Recrd of node ref SM.map ref * bool
adamc@1215 477 | Nothing
adamc@1208 478
adamc@1215 479 type representative = node ref
adamc@1215 480
adamc@1215 481 type database = {Vars : representative IM.map ref,
adamc@1215 482 Consts : representative CM.map ref,
adamc@1215 483 Con0s : representative SM.map ref,
adamc@1215 484 Records : (representative SM.map * representative) list ref,
adamc@1229 485 Funcs : ((string * representative list) * representative) list ref}
adamc@1215 486
adamc@1215 487 fun database () = {Vars = ref IM.empty,
adamc@1215 488 Consts = ref CM.empty,
adamc@1215 489 Con0s = ref SM.empty,
adamc@1215 490 Records = ref [],
adamc@1215 491 Funcs = ref []}
adamc@1215 492
adamc@1215 493 fun unNode n =
adamc@1215 494 case !n of
adamc@1215 495 Node r => r
adamc@1215 496
adamc@1215 497 open Print
adamc@1215 498 val string = PD.string
adamc@1215 499 val newline = PD.newline
adamc@1215 500
adamc@1215 501 fun p_rep n =
adamc@1215 502 case !(#Rep (unNode n)) of
adamc@1215 503 SOME n => p_rep n
adamc@1215 504 | NONE =>
adamc@1221 505 box [string (Int.toString (Unsafe.cast n) ^ ":"),
adamc@1221 506 space,
adamc@1221 507 case #Variety (unNode n) of
adamc@1221 508 Nothing => string "?"
adamc@1221 509 | Dt0 s => string ("Dt0(" ^ s ^ ")")
adamc@1221 510 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
adamc@1221 511 space,
adamc@1221 512 p_rep n,
adamc@1221 513 string ")"]
adamc@1221 514 | Prim p => Prim.p_t p
adamc@1221 515 | Recrd (ref m, b) => box [string "{",
adamc@1221 516 p_list (fn (x, n) => box [string x,
adamc@1221 517 space,
adamc@1221 518 string "=",
adamc@1221 519 space,
adamc@1221 520 p_rep n]) (SM.listItemsi m),
adamc@1221 521 string "}",
adamc@1221 522 if b then
adamc@1221 523 box [space,
adamc@1221 524 string "(complete)"]
adamc@1221 525 else
adamc@1226 526 box []]]
adamc@1215 527
adamc@1215 528 fun p_database (db : database) =
adamc@1215 529 box [string "Vars:",
adamc@1215 530 newline,
adamc@1215 531 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
adamc@1215 532 space,
adamc@1215 533 string "=",
adamc@1215 534 space,
adamc@1218 535 p_rep n,
adamc@1218 536 if !(#Known (unNode n)) then
adamc@1218 537 box [space,
adamc@1218 538 string "(known)"]
adamc@1218 539 else
adamc@1218 540 box []]) (IM.listItemsi (!(#Vars db)))]
adamc@1215 541
adamc@1215 542 fun repOf (n : representative) : representative =
adamc@1215 543 case !(#Rep (unNode n)) of
adamc@1215 544 NONE => n
adamc@1215 545 | SOME r =>
adamc@1215 546 let
adamc@1215 547 val r = repOf r
adamc@1215 548 in
adamc@1215 549 #Rep (unNode n) := SOME r;
adamc@1215 550 r
adamc@1215 551 end
adamc@1215 552
adamc@1215 553 fun markKnown r =
adamc@1221 554 let
adamc@1221 555 val r = repOf r
adamc@1221 556 in
adamc@1221 557 (*Print.preface ("markKnown", p_rep r);*)
adamc@1221 558 if !(#Known (unNode r)) then
adamc@1221 559 ()(*TextIO.print "Already known\n"*)
adamc@1221 560 else
adamc@1221 561 (#Known (unNode r) := true;
adamc@1221 562 SM.app markKnown (!(#Cons (unNode r)));
adamc@1221 563 case #Variety (unNode r) of
adamc@1221 564 Dt1 (_, r) => markKnown r
adamc@1221 565 | Recrd (xes, _) => SM.app markKnown (!xes)
adamc@1221 566 | _ => ())
adamc@1221 567 end
adamc@1215 568
adamc@1215 569 fun representative (db : database, e) =
adamc@1208 570 let
adamc@1215 571 fun rep e =
adamc@1215 572 case e of
adamc@1215 573 Const p => (case CM.find (!(#Consts db), p) of
adamc@1215 574 SOME r => repOf r
adamc@1215 575 | NONE =>
adamc@1215 576 let
adamc@1215 577 val r = ref (Node {Rep = ref NONE,
adamc@1215 578 Cons = ref SM.empty,
adamc@1215 579 Variety = Prim p,
adamc@1219 580 Known = ref true})
adamc@1215 581 in
adamc@1215 582 #Consts db := CM.insert (!(#Consts db), p, r);
adamc@1215 583 r
adamc@1215 584 end)
adamc@1215 585 | Var n => (case IM.find (!(#Vars db), n) of
adamc@1215 586 SOME r => repOf r
adamc@1215 587 | NONE =>
adamc@1215 588 let
adamc@1215 589 val r = ref (Node {Rep = ref NONE,
adamc@1215 590 Cons = ref SM.empty,
adamc@1215 591 Variety = Nothing,
adamc@1215 592 Known = ref false})
adamc@1215 593 in
adamc@1215 594 #Vars db := IM.insert (!(#Vars db), n, r);
adamc@1215 595 r
adamc@1215 596 end)
adamc@1215 597 | Lvar n =>
adamc@1215 598 (case IM.find (!unif, n) of
adamc@1215 599 NONE => raise Undetermined
adamc@1215 600 | SOME e => rep e)
adamc@1215 601 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
adamc@1215 602 SOME r => repOf r
adamc@1215 603 | NONE =>
adamc@1215 604 let
adamc@1215 605 val r = ref (Node {Rep = ref NONE,
adamc@1215 606 Cons = ref SM.empty,
adamc@1215 607 Variety = Dt0 f,
adamc@1218 608 Known = ref true})
adamc@1215 609 in
adamc@1215 610 #Con0s db := SM.insert (!(#Con0s db), f, r);
adamc@1215 611 r
adamc@1215 612 end)
adamc@1215 613 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
adamc@1215 614 | Func (DtCon1 f, [e]) =>
adamc@1215 615 let
adamc@1215 616 val r = rep e
adamc@1215 617 in
adamc@1215 618 case SM.find (!(#Cons (unNode r)), f) of
adamc@1215 619 SOME r => repOf r
adamc@1215 620 | NONE =>
adamc@1215 621 let
adamc@1215 622 val r' = ref (Node {Rep = ref NONE,
adamc@1215 623 Cons = ref SM.empty,
adamc@1215 624 Variety = Dt1 (f, r),
adamc@1221 625 Known = ref (!(#Known (unNode r)))})
adamc@1215 626 in
adamc@1215 627 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
adamc@1215 628 r'
adamc@1215 629 end
adamc@1215 630 end
adamc@1215 631 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
adamc@1215 632 | Func (UnCon f, [e]) =>
adamc@1215 633 let
adamc@1215 634 val r = rep e
adamc@1215 635 in
adamc@1215 636 case #Variety (unNode r) of
adamc@1215 637 Dt1 (f', n) => if f' = f then
adamc@1215 638 repOf n
adamc@1215 639 else
adamc@1215 640 raise Contradiction
adamc@1215 641 | Nothing =>
adamc@1215 642 let
adamc@1215 643 val cons = ref SM.empty
adamc@1215 644 val r' = ref (Node {Rep = ref NONE,
adamc@1215 645 Cons = cons,
adamc@1215 646 Variety = Nothing,
adamc@1221 647 Known = ref (!(#Known (unNode r)))})
adamc@1215 648
adamc@1215 649 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 650 Cons = #Cons (unNode r),
adamc@1215 651 Variety = Dt1 (f, r'),
adamc@1215 652 Known = #Known (unNode r)})
adamc@1215 653 in
adamc@1215 654 cons := SM.insert (!cons, f, r'');
adamc@1215 655 #Rep (unNode r) := SOME r'';
adamc@1215 656 r'
adamc@1215 657 end
adamc@1215 658 | _ => raise Contradiction
adamc@1215 659 end
adamc@1215 660 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
adamc@1215 661 | Func (Other f, es) =>
adamc@1215 662 let
adamc@1215 663 val rs = map rep es
adamc@1215 664 in
adamc@1215 665 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
adamc@1215 666 NONE =>
adamc@1215 667 let
adamc@1215 668 val r = ref (Node {Rep = ref NONE,
adamc@1215 669 Cons = ref SM.empty,
adamc@1215 670 Variety = Nothing,
adamc@1215 671 Known = ref false})
adamc@1215 672 in
adamc@1215 673 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
adamc@1215 674 r
adamc@1215 675 end
adamc@1215 676 | SOME (_, r) => repOf r
adamc@1215 677 end
adamc@1215 678 | Recd xes =>
adamc@1215 679 let
adamc@1215 680 val xes = map (fn (x, e) => (x, rep e)) xes
adamc@1215 681 val len = length xes
adamc@1215 682 in
adamc@1215 683 case List.find (fn (xes', _) =>
adamc@1215 684 SM.numItems xes' = len
adamc@1215 685 andalso List.all (fn (x, n) =>
adamc@1215 686 case SM.find (xes', x) of
adamc@1215 687 NONE => false
adamc@1215 688 | SOME n' => n = repOf n') xes)
adamc@1215 689 (!(#Records db)) of
adamc@1215 690 SOME (_, r) => repOf r
adamc@1215 691 | NONE =>
adamc@1215 692 let
adamc@1215 693 val xes = foldl SM.insert' SM.empty xes
adamc@1215 694
adamc@1215 695 val r' = ref (Node {Rep = ref NONE,
adamc@1215 696 Cons = ref SM.empty,
adamc@1221 697 Variety = Recrd (ref xes, true),
adamc@1215 698 Known = ref false})
adamc@1215 699 in
adamc@1215 700 #Records db := (xes, r') :: (!(#Records db));
adamc@1215 701 r'
adamc@1215 702 end
adamc@1215 703 end
adamc@1215 704 | Proj (e, f) =>
adamc@1215 705 let
adamc@1215 706 val r = rep e
adamc@1215 707 in
adamc@1215 708 case #Variety (unNode r) of
adamc@1221 709 Recrd (xes, _) =>
adamc@1215 710 (case SM.find (!xes, f) of
adamc@1215 711 SOME r => repOf r
adamc@1216 712 | NONE => let
adamc@1215 713 val r = ref (Node {Rep = ref NONE,
adamc@1215 714 Cons = ref SM.empty,
adamc@1215 715 Variety = Nothing,
adamc@1221 716 Known = ref (!(#Known (unNode r)))})
adamc@1215 717 in
adamc@1215 718 xes := SM.insert (!xes, f, r);
adamc@1215 719 r
adamc@1215 720 end)
adamc@1215 721 | Nothing =>
adamc@1215 722 let
adamc@1215 723 val r' = ref (Node {Rep = ref NONE,
adamc@1215 724 Cons = ref SM.empty,
adamc@1215 725 Variety = Nothing,
adamc@1221 726 Known = ref (!(#Known (unNode r)))})
adamc@1215 727
adamc@1215 728 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 729 Cons = #Cons (unNode r),
adamc@1221 730 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
adamc@1215 731 Known = #Known (unNode r)})
adamc@1215 732 in
adamc@1215 733 #Rep (unNode r) := SOME r'';
adamc@1215 734 r'
adamc@1215 735 end
adamc@1215 736 | _ => raise Contradiction
adamc@1215 737 end
adamc@1226 738 | Finish => raise Contradiction
adamc@1208 739 in
adamc@1215 740 rep e
adamc@1208 741 end
adamc@1208 742
adamc@1226 743 fun p_repOf db e = p_rep (representative (db, e))
adamc@1226 744
adamc@1215 745 fun assert (db, a) =
adamc@1215 746 case a of
adamc@1215 747 ACond _ => ()
adamc@1215 748 | AReln x =>
adamc@1215 749 case x of
adamc@1221 750 (Known, [e]) =>
adamc@1221 751 ((*Print.prefaces "Before" [("e", p_exp e),
adamc@1221 752 ("db", p_database db)];*)
adamc@1221 753 markKnown (representative (db, e))(*;
adamc@1221 754 Print.prefaces "After" [("e", p_exp e),
adamc@1221 755 ("db", p_database db)]*))
adamc@1215 756 | (PCon0 f, [e]) =>
adamc@1215 757 let
adamc@1215 758 val r = representative (db, e)
adamc@1215 759 in
adamc@1215 760 case #Variety (unNode r) of
adamc@1215 761 Dt0 f' => if f = f' then
adamc@1215 762 ()
adamc@1215 763 else
adamc@1215 764 raise Contradiction
adamc@1215 765 | Nothing =>
adamc@1215 766 let
adamc@1215 767 val r' = ref (Node {Rep = ref NONE,
adamc@1215 768 Cons = ref SM.empty,
adamc@1215 769 Variety = Dt0 f,
adamc@1215 770 Known = ref false})
adamc@1215 771 in
adamc@1215 772 #Rep (unNode r) := SOME r'
adamc@1215 773 end
adamc@1215 774 | _ => raise Contradiction
adamc@1215 775 end
adamc@1215 776 | (PCon1 f, [e]) =>
adamc@1215 777 let
adamc@1215 778 val r = representative (db, e)
adamc@1215 779 in
adamc@1215 780 case #Variety (unNode r) of
adamc@1215 781 Dt1 (f', e') => if f = f' then
adamc@1215 782 ()
adamc@1215 783 else
adamc@1215 784 raise Contradiction
adamc@1215 785 | Nothing =>
adamc@1215 786 let
adamc@1215 787 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 788 Cons = ref SM.empty,
adamc@1215 789 Variety = Nothing,
adamc@1215 790 Known = ref false})
adamc@1214 791
adamc@1215 792 val r' = ref (Node {Rep = ref NONE,
adamc@1215 793 Cons = ref SM.empty,
adamc@1215 794 Variety = Dt1 (f, r''),
adamc@1215 795 Known = ref false})
adamc@1215 796 in
adamc@1215 797 #Rep (unNode r) := SOME r'
adamc@1215 798 end
adamc@1215 799 | _ => raise Contradiction
adamc@1215 800 end
adamc@1215 801 | (Eq, [e1, e2]) =>
adamc@1215 802 let
adamc@1215 803 fun markEq (r1, r2) =
adamc@1226 804 let
adamc@1226 805 val r1 = repOf r1
adamc@1226 806 val r2 = repOf r2
adamc@1226 807 in
adamc@1226 808 if r1 = r2 then
adamc@1226 809 ()
adamc@1226 810 else case (#Variety (unNode r1), #Variety (unNode r2)) of
adamc@1226 811 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
adamc@1226 812 ()
adamc@1226 813 else
adamc@1226 814 raise Contradiction
adamc@1226 815 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
adamc@1226 816 ()
adamc@1226 817 else
adamc@1226 818 raise Contradiction
adamc@1226 819 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
adamc@1226 820 markEq (r1, r2)
adamc@1226 821 else
adamc@1226 822 raise Contradiction
adamc@1226 823 | (Recrd (xes1, _), Recrd (xes2, _)) =>
adamc@1226 824 let
adamc@1226 825 fun unif (xes1, xes2) =
adamc@1226 826 SM.appi (fn (x, r1) =>
adamc@1226 827 case SM.find (!xes2, x) of
adamc@1226 828 NONE => xes2 := SM.insert (!xes2, x, r1)
adamc@1226 829 | SOME r2 => markEq (r1, r2)) (!xes1)
adamc@1226 830 in
adamc@1226 831 unif (xes1, xes2);
adamc@1226 832 unif (xes2, xes1)
adamc@1226 833 end
adamc@1226 834 | (Nothing, _) => mergeNodes (r1, r2)
adamc@1226 835 | (_, Nothing) => mergeNodes (r2, r1)
adamc@1226 836 | _ => raise Contradiction
adamc@1226 837 end
adamc@1214 838
adamc@1218 839 and mergeNodes (r1, r2) =
adamc@1218 840 (#Rep (unNode r1) := SOME r2;
adamc@1218 841 if !(#Known (unNode r1)) then
adamc@1218 842 markKnown r2
adamc@1218 843 else
adamc@1218 844 ();
adamc@1218 845 if !(#Known (unNode r2)) then
adamc@1218 846 markKnown r1
adamc@1218 847 else
adamc@1218 848 ();
adamc@1218 849 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
adamc@1229 850
adamc@1218 851 compactFuncs ())
adamc@1218 852
adamc@1215 853 and compactFuncs () =
adamc@1214 854 let
adamc@1215 855 fun loop funcs =
adamc@1215 856 case funcs of
adamc@1215 857 [] => []
adamc@1215 858 | (fr as ((f, rs), r)) :: rest =>
adamc@1215 859 let
adamc@1215 860 val rest = List.filter (fn ((f' : string, rs'), r') =>
adamc@1215 861 if f' = f
adamc@1215 862 andalso ListPair.allEq (fn (r1, r2) =>
adamc@1215 863 repOf r1 = repOf r2)
adamc@1215 864 (rs, rs') then
adamc@1215 865 (markEq (r, r');
adamc@1215 866 false)
adamc@1215 867 else
adamc@1215 868 true) rest
adamc@1215 869 in
adamc@1215 870 fr :: loop rest
adamc@1215 871 end
adamc@1214 872 in
adamc@1215 873 #Funcs db := loop (!(#Funcs db))
adamc@1214 874 end
adamc@1215 875 in
adamc@1215 876 markEq (representative (db, e1), representative (db, e2))
adamc@1215 877 end
adamc@1215 878 | _ => ()
adamc@1214 879
adamc@1215 880 fun check (db, a) =
adamc@1215 881 case a of
adamc@1215 882 ACond _ => false
adamc@1215 883 | AReln x =>
adamc@1215 884 case x of
adamc@1221 885 (Known, [e]) =>
adamc@1221 886 let
adamc@1221 887 fun isKnown r =
adamc@1221 888 let
adamc@1221 889 val r = repOf r
adamc@1221 890 in
adamc@1221 891 !(#Known (unNode r))
adamc@1221 892 orelse case #Variety (unNode r) of
adamc@1221 893 Dt1 (_, r) => isKnown r
adamc@1221 894 | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
adamc@1221 895 | _ => false
adamc@1221 896 end
adamc@1221 897
adamc@1221 898 val r = representative (db, e)
adamc@1221 899 in
adamc@1221 900 isKnown r
adamc@1221 901 end
adamc@1215 902 | (PCon0 f, [e]) =>
adamc@1215 903 (case #Variety (unNode (representative (db, e))) of
adamc@1215 904 Dt0 f' => f' = f
adamc@1215 905 | _ => false)
adamc@1215 906 | (PCon1 f, [e]) =>
adamc@1215 907 (case #Variety (unNode (representative (db, e))) of
adamc@1215 908 Dt1 (f', _) => f' = f
adamc@1215 909 | _ => false)
adamc@1215 910 | (Eq, [e1, e2]) =>
adamc@1214 911 let
adamc@1215 912 val r1 = representative (db, e1)
adamc@1215 913 val r2 = representative (db, e2)
adamc@1214 914 in
adamc@1215 915 repOf r1 = repOf r2
adamc@1214 916 end
adamc@1215 917 | _ => false
adamc@1212 918
adamc@1218 919 fun builtFrom (db, {Base = bs, Derived = d}) =
adamc@1218 920 let
adamc@1218 921 val bs = map (fn b => representative (db, b)) bs
adamc@1218 922
adamc@1218 923 fun loop d =
adamc@1218 924 let
adamc@1218 925 val d = repOf d
adamc@1218 926 in
adamc@1218 927 List.exists (fn b => repOf b = d) bs
adamc@1218 928 orelse case #Variety (unNode d) of
adamc@1218 929 Dt0 _ => true
adamc@1218 930 | Dt1 (_, d) => loop d
adamc@1218 931 | Prim _ => true
adamc@1221 932 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
adamc@1218 933 | Nothing => false
adamc@1218 934 end
adamc@1218 935 in
adamc@1218 936 loop (representative (db, d))
adamc@1218 937 end
adamc@1218 938
adamc@1208 939 end
adamc@1208 940
adamc@1215 941 fun decomp fals or =
adamc@1215 942 let
adamc@1215 943 fun decomp p k =
adamc@1215 944 case p of
adamc@1215 945 True => k []
adamc@1215 946 | False => fals
adamc@1215 947 | Unknown => k []
adamc@1215 948 | And (p1, p2) =>
adamc@1215 949 decomp p1 (fn ps1 =>
adamc@1215 950 decomp p2 (fn ps2 =>
adamc@1215 951 k (ps1 @ ps2)))
adamc@1215 952 | Or (p1, p2) =>
adamc@1215 953 or (decomp p1 k, fn () => decomp p2 k)
adamc@1215 954 | Reln x => k [AReln x]
adamc@1215 955 | Cond x => k [ACond x]
adamc@1215 956 in
adamc@1215 957 decomp
adamc@1215 958 end
adamc@1202 959
adamc@1226 960 val tabs = ref (SM.empty : (string list * string list list) SM.map)
adamc@1226 961
adamc@1231 962 fun ccOf hyps =
adamc@1231 963 let
adamc@1231 964 val cc = Cc.database ()
adamc@1231 965 val () = app (fn a => Cc.assert (cc, a)) hyps
adamc@1231 966
adamc@1231 967 (* Take advantage of table key information *)
adamc@1231 968 fun findKeys hyps =
adamc@1231 969 case hyps of
adamc@1231 970 [] => ()
adamc@1231 971 | AReln (Sql tab, [r1]) :: hyps =>
adamc@1231 972 (case SM.find (!tabs, tab) of
adamc@1231 973 NONE => findKeys hyps
adamc@1231 974 | SOME (_, []) => findKeys hyps
adamc@1231 975 | SOME (_, ks) =>
adamc@1231 976 let
adamc@1231 977 fun finder hyps =
adamc@1231 978 case hyps of
adamc@1231 979 [] => ()
adamc@1231 980 | AReln (Sql tab', [r2]) :: hyps =>
adamc@1231 981 (if tab' = tab andalso
adamc@1231 982 List.exists (List.all (fn f =>
adamc@1231 983 let
adamc@1231 984 val r =
adamc@1231 985 Cc.check (cc,
adamc@1231 986 AReln (Eq, [Proj (r1, f),
adamc@1231 987 Proj (r2, f)]))
adamc@1231 988 in
adamc@1231 989 (*Print.prefaces "Fs"
adamc@1231 990 [("tab",
adamc@1231 991 Print.PD.string tab),
adamc@1231 992 ("r1",
adamc@1231 993 p_exp (Proj (r1, f))),
adamc@1231 994 ("r2",
adamc@1231 995 p_exp (Proj (r2, f))),
adamc@1231 996 ("r",
adamc@1231 997 Print.PD.string
adamc@1231 998 (Bool.toString r))];*)
adamc@1231 999 r
adamc@1231 1000 end)) ks then
adamc@1231 1001 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
adamc@1231 1002 ("r1", p_exp r1),
adamc@1231 1003 ("r2", p_exp r2),
adamc@1231 1004 ("rp1", Cc.p_repOf cc r1),
adamc@1231 1005 ("rp2", Cc.p_repOf cc r2)];*)
adamc@1231 1006 Cc.assert (cc, AReln (Eq, [r1, r2])))
adamc@1231 1007 else
adamc@1231 1008 ();
adamc@1231 1009 finder hyps)
adamc@1231 1010 | _ :: hyps => finder hyps
adamc@1231 1011 in
adamc@1231 1012 finder hyps;
adamc@1231 1013 findKeys hyps
adamc@1231 1014 end)
adamc@1231 1015 | _ :: hyps => findKeys hyps
adamc@1231 1016 in
adamc@1231 1017 findKeys hyps;
adamc@1231 1018 cc
adamc@1231 1019 end
adamc@1231 1020
adamc@1231 1021 fun imply (cc, hyps, goals, outs) =
adamc@1218 1022 let
adamc@1218 1023 fun gls goals onFail acc =
adamc@1218 1024 case goals of
adamc@1218 1025 [] =>
adamc@1231 1026 ((List.all (fn a =>
adamc@1231 1027 if Cc.check (cc, a) then
adamc@1231 1028 true
adamc@1231 1029 else
adamc@1231 1030 ((*Print.prefaces "Can't prove"
adamc@1231 1031 [("a", p_atom a),
adamc@1231 1032 ("hyps", Print.p_list p_atom hyps),
adamc@1231 1033 ("db", Cc.p_database cc)];*)
adamc@1231 1034 false)) acc
adamc@1231 1035 andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
adamc@1231 1036 andalso (case outs of
adamc@1231 1037 NONE => true
adamc@1231 1038 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
adamc@1231 1039 Base = outs})))
adamc@1231 1040 handle Cc.Contradiction => false
adamc@1231 1041 | Cc.Undetermined => false)
adamc@1218 1042 orelse onFail ()
adamc@1218 1043 | (g as AReln (Sql gf, [ge])) :: goals =>
adamc@1218 1044 let
adamc@1218 1045 fun hps hyps =
adamc@1218 1046 case hyps of
adamc@1218 1047 [] => gls goals onFail (g :: acc)
adamc@1218 1048 | (h as AReln (Sql hf, [he])) :: hyps =>
adamc@1218 1049 if gf = hf then
adamc@1218 1050 let
adamc@1218 1051 val saved = save ()
adamc@1218 1052 in
adamc@1218 1053 if eq (ge, he) then
adamc@1218 1054 let
adamc@1218 1055 val changed = IM.numItems (!unif)
adamc@1218 1056 <> IM.numItems saved
adamc@1218 1057 in
adamc@1218 1058 gls goals (fn () => (restore saved;
adamc@1218 1059 changed
adamc@1218 1060 andalso hps hyps))
adamc@1218 1061 acc
adamc@1218 1062 end
adamc@1218 1063 else
adamc@1218 1064 hps hyps
adamc@1218 1065 end
adamc@1218 1066 else
adamc@1218 1067 hps hyps
adamc@1218 1068 | _ :: hyps => hps hyps
adamc@1218 1069 in
adamc@1218 1070 hps hyps
adamc@1218 1071 end
adamc@1218 1072 | g :: goals => gls goals onFail (g :: acc)
adamc@1218 1073 in
adamc@1218 1074 reset ();
adamc@1218 1075 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
adamc@1223 1076 ("goals", Print.p_list p_atom goals)];*)
adamc@1218 1077 gls goals (fn () => false) []
adamc@1231 1078 end
adamc@1200 1079
adamc@1200 1080 fun patCon pc =
adamc@1200 1081 case pc of
adamc@1200 1082 PConVar n => "C" ^ Int.toString n
adamc@1200 1083 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 1084
adamc@1200 1085 datatype chunk =
adamc@1200 1086 String of string
adamc@1200 1087 | Exp of Mono.exp
adamc@1200 1088
adamc@1200 1089 fun chunkify e =
adamc@1200 1090 case #1 e of
adamc@1200 1091 EPrim (Prim.String s) => [String s]
adamc@1207 1092 | EStrcat (e1, e2) =>
adamc@1207 1093 let
adamc@1207 1094 val chs1 = chunkify e1
adamc@1207 1095 val chs2 = chunkify e2
adamc@1207 1096 in
adamc@1207 1097 case chs2 of
adamc@1207 1098 String s2 :: chs2' =>
adamc@1207 1099 (case List.last chs1 of
adamc@1207 1100 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207 1101 | _ => chs1 @ chs2)
adamc@1207 1102 | _ => chs1 @ chs2
adamc@1207 1103 end
adamc@1200 1104 | _ => [Exp e]
adamc@1200 1105
adamc@1201 1106 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 1107
adamc@1201 1108 fun always v chs = SOME (v, chs)
adamc@1201 1109
adamc@1202 1110 fun parse p s =
adamc@1202 1111 case p (chunkify s) of
adamc@1201 1112 SOME (v, []) => SOME v
adamc@1201 1113 | _ => NONE
adamc@1201 1114
adamc@1201 1115 fun const s chs =
adamc@1201 1116 case chs of
adamc@1201 1117 String s' :: chs => if String.isPrefix s s' then
adamc@1201 1118 SOME ((), if size s = size s' then
adamc@1201 1119 chs
adamc@1201 1120 else
adamc@1201 1121 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 1122 else
adamc@1201 1123 NONE
adamc@1201 1124 | _ => NONE
adamc@1201 1125
adamc@1201 1126 fun follow p1 p2 chs =
adamc@1201 1127 case p1 chs of
adamc@1201 1128 NONE => NONE
adamc@1201 1129 | SOME (v1, chs) =>
adamc@1201 1130 case p2 chs of
adamc@1201 1131 NONE => NONE
adamc@1201 1132 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 1133
adamc@1201 1134 fun wrap p f chs =
adamc@1201 1135 case p chs of
adamc@1201 1136 NONE => NONE
adamc@1201 1137 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 1138
adamc@1209 1139 fun wrapP p f chs =
adamc@1209 1140 case p chs of
adamc@1209 1141 NONE => NONE
adamc@1209 1142 | SOME (v, chs) =>
adamc@1209 1143 case f v of
adamc@1209 1144 NONE => NONE
adamc@1209 1145 | SOME r => SOME (r, chs)
adamc@1209 1146
adamc@1201 1147 fun alt p1 p2 chs =
adamc@1201 1148 case p1 chs of
adamc@1201 1149 NONE => p2 chs
adamc@1201 1150 | v => v
adamc@1201 1151
adamc@1207 1152 fun altL ps =
adamc@1207 1153 case rev ps of
adamc@1207 1154 [] => (fn _ => NONE)
adamc@1207 1155 | p :: ps =>
adamc@1207 1156 foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207 1157
adamc@1204 1158 fun opt p chs =
adamc@1204 1159 case p chs of
adamc@1204 1160 NONE => SOME (NONE, chs)
adamc@1204 1161 | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204 1162
adamc@1201 1163 fun skip cp chs =
adamc@1201 1164 case chs of
adamc@1201 1165 String "" :: chs => skip cp chs
adamc@1201 1166 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 1167 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 1168 else
adamc@1201 1169 SOME ((), chs)
adamc@1201 1170 | _ => SOME ((), chs)
adamc@1201 1171
adamc@1201 1172 fun keep cp chs =
adamc@1201 1173 case chs of
adamc@1201 1174 String "" :: chs => keep cp chs
adamc@1201 1175 | String s :: chs' =>
adamc@1201 1176 let
adamc@1201 1177 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 1178 in
adamc@1201 1179 if Substring.isEmpty befor then
adamc@1201 1180 NONE
adamc@1201 1181 else
adamc@1201 1182 SOME (Substring.string befor,
adamc@1201 1183 if Substring.isEmpty after then
adamc@1201 1184 chs'
adamc@1201 1185 else
adamc@1201 1186 String (Substring.string after) :: chs')
adamc@1201 1187 end
adamc@1201 1188 | _ => NONE
adamc@1201 1189
adamc@1204 1190 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204 1191 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204 1192
adamc@1204 1193 fun log name p chs =
adamc@1206 1194 (if !debug then
adamc@1227 1195 (print (name ^ ": ");
adamc@1227 1196 app (fn String s => print s
adamc@1227 1197 | _ => print "???") chs;
adamc@1227 1198 print "\n")
adamc@1206 1199 else
adamc@1206 1200 ();
adamc@1204 1201 p chs)
adamc@1201 1202
adamc@1201 1203 fun list p chs =
adamc@1207 1204 altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207 1205 (fn (v, ((), ls)) => v :: ls),
adamc@1207 1206 wrap (ws p) (fn v => [v]),
adamc@1207 1207 always []] chs
adamc@1201 1208
adamc@1201 1209 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 1210
adamc@1211 1211 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211 1212 SOME (String.extract (s, 2, NONE))
adamc@1201 1213 else
adamc@1211 1214 NONE)
adamc@1211 1215 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211 1216 SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211 1217 ^ String.extract (s, 4, NONE))
adamc@1211 1218 else
adamc@1211 1219 NONE)
adamc@1201 1220
adamc@1211 1221 val field = wrap (follow t_ident
adamc@1201 1222 (follow (const ".")
adamc@1201 1223 uw_ident))
adamc@1201 1224 (fn (t, ((), f)) => (t, f))
adamc@1201 1225
adamc@1206 1226 datatype Rel =
adamc@1206 1227 Exps of exp * exp -> prop
adamc@1206 1228 | Props of prop * prop -> prop
adamc@1206 1229
adamc@1204 1230 datatype sqexp =
adamc@1206 1231 SqConst of Prim.t
adamc@1206 1232 | Field of string * string
adamc@1206 1233 | Binop of Rel * sqexp * sqexp
adamc@1207 1234 | SqKnown of sqexp
adamc@1207 1235 | Inj of Mono.exp
adamc@1211 1236 | SqFunc of string * sqexp
adamc@1211 1237 | Count
adamc@1204 1238
adamc@1210 1239 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210 1240
adamc@1210 1241 val sqbrel = altL [cmp "=" Eq,
adamc@1210 1242 cmp "<>" Ne,
adamc@1210 1243 cmp "<=" Le,
adamc@1210 1244 cmp "<" Lt,
adamc@1210 1245 cmp ">=" Ge,
adamc@1210 1246 cmp ">" Gt,
adamc@1207 1247 wrap (const "AND") (fn () => Props And),
adamc@1207 1248 wrap (const "OR") (fn () => Props Or)]
adamc@1204 1249
adamc@1204 1250 datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204 1251
adamc@1209 1252 fun string chs =
adamc@1206 1253 case chs of
adamc@1209 1254 String s :: chs =>
adamc@1209 1255 if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209 1256 let
adamc@1209 1257 fun loop (cs, acc) =
adamc@1209 1258 case cs of
adamc@1209 1259 [] => NONE
adamc@1209 1260 | c :: cs =>
adamc@1209 1261 if c = #"'" then
adamc@1209 1262 SOME (String.implode (rev acc), cs)
adamc@1209 1263 else if c = #"\\" then
adamc@1209 1264 case cs of
adamc@1209 1265 c :: cs => loop (cs, c :: acc)
adamc@1209 1266 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209 1267 else
adamc@1209 1268 loop (cs, c :: acc)
adamc@1209 1269 in
adamc@1209 1270 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209 1271 NONE => NONE
adamc@1209 1272 | SOME (s, []) => SOME (s, chs)
adamc@1209 1273 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209 1274 end
adamc@1209 1275 else
adamc@1209 1276 NONE
adamc@1209 1277 | _ => NONE
adamc@1206 1278
adamc@1209 1279 val prim =
adamc@1209 1280 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209 1281 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209 1282 (opt (const "::float8"))) #1,
adamc@1209 1283 wrap (follow (wrapP (keep Char.isDigit)
adamc@1209 1284 (Option.map Prim.Int o Int64.fromString))
adamc@1209 1285 (opt (const "::int8"))) #1,
adamc@1209 1286 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209 1287 (Prim.String o #1 o #2)]
adamc@1206 1288
adamc@1207 1289 fun known' chs =
adamc@1207 1290 case chs of
adamc@1207 1291 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207 1292 | _ => NONE
adamc@1207 1293
adamc@1207 1294 fun sqlify chs =
adamc@1207 1295 case chs of
adamc@1207 1296 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207 1297 if String.isPrefix "sqlify" f then
adamc@1207 1298 SOME (e, chs)
adamc@1207 1299 else
adamc@1207 1300 NONE
adamc@1207 1301 | _ => NONE
adamc@1207 1302
adamc@1211 1303 fun constK s = wrap (const s) (fn () => s)
adamc@1211 1304
adamc@1211 1305 val funcName = altL [constK "COUNT",
adamc@1211 1306 constK "MIN",
adamc@1211 1307 constK "MAX",
adamc@1211 1308 constK "SUM",
adamc@1211 1309 constK "AVG"]
adamc@1211 1310
adamc@1204 1311 fun sqexp chs =
adamc@1206 1312 log "sqexp"
adamc@1207 1313 (altL [wrap prim SqConst,
adamc@1211 1314 wrap field Field,
adamc@1207 1315 wrap known SqKnown,
adamc@1211 1316 wrap func SqFunc,
adamc@1211 1317 wrap (const "COUNT(*)") (fn () => Count),
adamc@1207 1318 wrap sqlify Inj,
adamc@1211 1319 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211 1320 (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211 1321 (fn ((), (e, _)) => e),
adamc@1207 1322 wrap (follow (ws (const "("))
adamc@1207 1323 (follow (wrap
adamc@1207 1324 (follow sqexp
adamc@1207 1325 (alt
adamc@1207 1326 (wrap
adamc@1207 1327 (follow (ws sqbrel)
adamc@1207 1328 (ws sqexp))
adamc@1207 1329 inl)
adamc@1207 1330 (always (inr ()))))
adamc@1207 1331 (fn (e1, sm) =>
adamc@1207 1332 case sm of
adamc@1207 1333 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207 1334 | inr () => e1))
adamc@1207 1335 (const ")")))
adamc@1207 1336 (fn ((), (e, ())) => e)])
adamc@1207 1337 chs
adamc@1206 1338
adamc@1207 1339 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 1340 (fn ((), ((), (e, ()))) => e) chs
adamc@1211 1341
adamc@1211 1342 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 1343 (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211 1344
adamc@1211 1345 datatype sitem =
adamc@1211 1346 SqField of string * string
adamc@1211 1347 | SqExp of sqexp * string
adamc@1211 1348
adamc@1211 1349 val sitem = alt (wrap field SqField)
adamc@1211 1350 (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211 1351 (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207 1352
adamc@1207 1353 val select = log "select"
adamc@1207 1354 (wrap (follow (const "SELECT ") (list sitem))
adamc@1207 1355 (fn ((), ls) => ls))
adamc@1201 1356
adamc@1201 1357 val fitem = wrap (follow uw_ident
adamc@1201 1358 (follow (const " AS ")
adamc@1201 1359 t_ident))
adamc@1201 1360 (fn (t, ((), f)) => (t, f))
adamc@1201 1361
adamc@1207 1362 val from = log "from"
adamc@1207 1363 (wrap (follow (const "FROM ") (list fitem))
adamc@1207 1364 (fn ((), ls) => ls))
adamc@1201 1365
adamc@1204 1366 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204 1367 (fn ((), ls) => ls)
adamc@1204 1368
adamc@1227 1369 type query1 = {Select : sitem list,
adamc@1227 1370 From : (string * string) list,
adamc@1227 1371 Where : sqexp option}
adamc@1227 1372
adamc@1227 1373 val query1 = log "query1"
adamc@1207 1374 (wrap (follow (follow select from) (opt wher))
adamc@1207 1375 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201 1376
adamc@1227 1377 datatype query =
adamc@1227 1378 Query1 of query1
adamc@1227 1379 | Union of query * query
adamc@1227 1380
adamc@1227 1381 fun query chs = log "query"
adamc@1227 1382 (alt (wrap (follow (const "((")
adamc@1227 1383 (follow query
adamc@1227 1384 (follow (const ") UNION (")
adamc@1227 1385 (follow query (const "))")))))
adamc@1227 1386 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
adamc@1227 1387 (wrap query1 Query1))
adamc@1227 1388 chs
adamc@1227 1389
adamc@1220 1390 datatype dml =
adamc@1220 1391 Insert of string * (string * sqexp) list
adamc@1221 1392 | Delete of string * sqexp
adamc@1223 1393 | Update of string * (string * sqexp) list * sqexp
adamc@1220 1394
adamc@1220 1395 val insert = log "insert"
adamc@1220 1396 (wrapP (follow (const "INSERT INTO ")
adamc@1220 1397 (follow uw_ident
adamc@1220 1398 (follow (const " (")
adamc@1220 1399 (follow (list uw_ident)
adamc@1220 1400 (follow (const ") VALUES (")
adamc@1220 1401 (follow (list sqexp)
adamc@1220 1402 (const ")")))))))
adamc@1220 1403 (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
adamc@1221 1404 (SOME (tab, ListPair.zipEq (fs, es)))
adamc@1220 1405 handle ListPair.UnequalLengths => NONE))
adamc@1220 1406
adamc@1221 1407 val delete = log "delete"
adamc@1221 1408 (wrap (follow (const "DELETE FROM ")
adamc@1221 1409 (follow uw_ident
adamc@1221 1410 (follow (const " AS T_T WHERE ")
adamc@1221 1411 sqexp)))
adamc@1221 1412 (fn ((), (tab, ((), es))) => (tab, es)))
adamc@1221 1413
adamc@1223 1414 val setting = log "setting"
adamc@1223 1415 (wrap (follow uw_ident (follow (const " = ") sqexp))
adamc@1223 1416 (fn (f, ((), e)) => (f, e)))
adamc@1223 1417
adamc@1223 1418 val update = log "update"
adamc@1223 1419 (wrap (follow (const "UPDATE ")
adamc@1223 1420 (follow uw_ident
adamc@1223 1421 (follow (const " AS T_T SET ")
adamc@1223 1422 (follow (list setting)
adamc@1223 1423 (follow (ws (const "WHERE "))
adamc@1223 1424 sqexp)))))
adamc@1223 1425 (fn ((), (tab, ((), (fs, ((), e))))) =>
adamc@1223 1426 (tab, fs, e)))
adamc@1223 1427
adamc@1220 1428 val dml = log "dml"
adamc@1221 1429 (altL [wrap insert Insert,
adamc@1223 1430 wrap delete Delete,
adamc@1223 1431 wrap update Update])
adamc@1220 1432
adamc@1215 1433 fun removeDups (ls : (string * string) list) =
adamc@1211 1434 case ls of
adamc@1211 1435 [] => []
adamc@1211 1436 | x :: ls =>
adamc@1211 1437 let
adamc@1211 1438 val ls = removeDups ls
adamc@1211 1439 in
adamc@1211 1440 if List.exists (fn x' => x' = x) ls then
adamc@1211 1441 ls
adamc@1211 1442 else
adamc@1211 1443 x :: ls
adamc@1211 1444 end
adamc@1211 1445
adamc@1212 1446 datatype queryMode =
adamc@1218 1447 SomeCol
adamc@1212 1448 | AllCols of exp
adamc@1212 1449
adamc@1220 1450 fun expIn rv env rvOf =
adamc@1220 1451 let
adamc@1220 1452 fun expIn (e, rvN) =
adamc@1220 1453 let
adamc@1220 1454 fun default () =
adamc@1220 1455 let
adamc@1229 1456 val (rvN, e') = rv rvN
adamc@1220 1457 in
adamc@1229 1458 (inl e', rvN)
adamc@1220 1459 end
adamc@1220 1460 in
adamc@1220 1461 case e of
adamc@1220 1462 SqConst p => (inl (Const p), rvN)
adamc@1220 1463 | Field (v, f) => (inl (Proj (rvOf v, f)), rvN)
adamc@1220 1464 | Binop (bo, e1, e2) =>
adamc@1220 1465 let
adamc@1220 1466 val (e1, rvN) = expIn (e1, rvN)
adamc@1220 1467 val (e2, rvN) = expIn (e2, rvN)
adamc@1220 1468 in
adamc@1220 1469 (inr (case (bo, e1, e2) of
adamc@1220 1470 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1220 1471 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1220 1472 | _ => Unknown), rvN)
adamc@1220 1473 end
adamc@1220 1474 | SqKnown e =>
adamc@1220 1475 (case expIn (e, rvN) of
adamc@1220 1476 (inl e, rvN) => (inr (Reln (Known, [e])), rvN)
adamc@1220 1477 | _ => (inr Unknown, rvN))
adamc@1220 1478 | Inj e =>
adamc@1220 1479 let
adamc@1220 1480 fun deinj e =
adamc@1220 1481 case #1 e of
adamc@1220 1482 ERel n => (List.nth (env, n), rvN)
adamc@1220 1483 | EField (e, f) =>
adamc@1220 1484 let
adamc@1220 1485 val (e, rvN) = deinj e
adamc@1220 1486 in
adamc@1220 1487 (Proj (e, f), rvN)
adamc@1220 1488 end
adamc@1220 1489 | _ =>
adamc@1220 1490 let
adamc@1220 1491 val (rvN, e) = rv rvN
adamc@1220 1492 in
adamc@1220 1493 (e, rvN)
adamc@1220 1494 end
adamc@1220 1495
adamc@1220 1496 val (e, rvN) = deinj e
adamc@1220 1497 in
adamc@1220 1498 (inl e, rvN)
adamc@1220 1499 end
adamc@1220 1500 | SqFunc (f, e) =>
adamc@1220 1501 (case expIn (e, rvN) of
adamc@1220 1502 (inl e, rvN) => (inl (Func (Other f, [e])), rvN)
adamc@1220 1503 | _ => default ())
adamc@1220 1504
adamc@1220 1505 | Count => default ()
adamc@1220 1506 end
adamc@1220 1507 in
adamc@1220 1508 expIn
adamc@1220 1509 end
adamc@1216 1510
adamc@1214 1511 fun queryProp env rvN rv oe e =
adamc@1216 1512 let
adamc@1216 1513 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1216 1514 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1227 1515 (rvN, Unknown, [], []))
adamc@1216 1516 in
adamc@1216 1517 case parse query e of
adamc@1216 1518 NONE => default ()
adamc@1227 1519 | SOME q =>
adamc@1216 1520 let
adamc@1227 1521 fun doQuery (q, rvN) =
adamc@1227 1522 case q of
adamc@1227 1523 Query1 r =>
adamc@1227 1524 let
adamc@1227 1525 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1227 1526 let
adamc@1227 1527 val (rvN, e) = rv rvN
adamc@1227 1528 in
adamc@1227 1529 ((v, e), rvN)
adamc@1227 1530 end) rvN (#From r)
adamc@1214 1531
adamc@1227 1532 fun rvOf v =
adamc@1227 1533 case List.find (fn (v', _) => v' = v) rvs of
adamc@1227 1534 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1227 1535 | SOME (_, e) => e
adamc@1214 1536
adamc@1227 1537 fun usedFields e =
adamc@1227 1538 case e of
adamc@1227 1539 SqConst _ => []
adamc@1227 1540 | Field (v, f) => [(v, f)]
adamc@1227 1541 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1227 1542 | SqKnown _ => []
adamc@1227 1543 | Inj _ => []
adamc@1227 1544 | SqFunc (_, e) => usedFields e
adamc@1227 1545 | Count => []
adamc@1214 1546
adamc@1227 1547 val p =
adamc@1227 1548 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1211 1549
adamc@1227 1550 val expIn = expIn rv env rvOf
adamc@1205 1551
adamc@1227 1552 val (p, rvN) = case #Where r of
adamc@1227 1553 NONE => (p, rvN)
adamc@1227 1554 | SOME e =>
adamc@1227 1555 case expIn (e, rvN) of
adamc@1227 1556 (inr p', rvN) => (And (p, p'), rvN)
adamc@1227 1557 | _ => (p, rvN)
adamc@1210 1558
adamc@1227 1559 fun normal () =
adamc@1227 1560 case oe of
adamc@1227 1561 SomeCol =>
adamc@1227 1562 let
adamc@1227 1563 val (sis, rvN) =
adamc@1227 1564 ListUtil.foldlMap
adamc@1227 1565 (fn (si, rvN) =>
adamc@1227 1566 case si of
adamc@1227 1567 SqField (v, f) => (Proj (rvOf v, f), rvN)
adamc@1227 1568 | SqExp (e, f) =>
adamc@1227 1569 case expIn (e, rvN) of
adamc@1227 1570 (inr _, _) =>
adamc@1227 1571 let
adamc@1227 1572 val (rvN, e) = rv rvN
adamc@1227 1573 in
adamc@1227 1574 (e, rvN)
adamc@1227 1575 end
adamc@1227 1576 | (inl e, rvN) => (e, rvN)) rvN (#Select r)
adamc@1227 1577 in
adamc@1227 1578 (rvN, p, True, sis)
adamc@1227 1579 end
adamc@1227 1580 | AllCols oe =>
adamc@1227 1581 let
adamc@1227 1582 val (ts, es, rvN) =
adamc@1227 1583 foldl (fn (si, (ts, es, rvN)) =>
adamc@1227 1584 case si of
adamc@1227 1585 SqField (v, f) =>
adamc@1227 1586 let
adamc@1227 1587 val fs = getOpt (SM.find (ts, v), SM.empty)
adamc@1227 1588 in
adamc@1227 1589 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN)
adamc@1227 1590 end
adamc@1227 1591 | SqExp (e, f) =>
adamc@1227 1592 let
adamc@1227 1593 val (e, rvN) =
adamc@1227 1594 case expIn (e, rvN) of
adamc@1227 1595 (inr _, rvN) =>
adamc@1227 1596 let
adamc@1227 1597 val (rvN, e) = rv rvN
adamc@1227 1598 in
adamc@1227 1599 (e, rvN)
adamc@1227 1600 end
adamc@1227 1601 | (inl e, rvN) => (e, rvN)
adamc@1227 1602 in
adamc@1227 1603 (ts, SM.insert (es, f, e), rvN)
adamc@1227 1604 end)
adamc@1227 1605 (SM.empty, SM.empty, rvN) (#Select r)
adamc@1227 1606
adamc@1227 1607 val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
adamc@1227 1608 (SM.listItemsi ts)
adamc@1227 1609 @ SM.listItemsi es)])
adamc@1227 1610 in
adamc@1227 1611 (rvN, And (p, p'), True, [])
adamc@1227 1612 end
adamc@1227 1613
adamc@1227 1614 val (rvN, p, wp, outs) =
adamc@1227 1615 case #Select r of
adamc@1227 1616 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1227 1617 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1227 1618 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1227 1619 (case oe of
adamc@1227 1620 SomeCol =>
adamc@1227 1621 let
adamc@1227 1622 val (rvN, oe) = rv rvN
adamc@1227 1623 in
adamc@1227 1624 (rvN,
adamc@1227 1625 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
adamc@1227 1626 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1227 1627 p)),
adamc@1227 1628 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1227 1629 [oe])
adamc@1227 1630 end
adamc@1227 1631 | AllCols oe =>
adamc@1227 1632 let
adamc@1227 1633 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
adamc@1227 1634 in
adamc@1227 1635 (rvN,
adamc@1227 1636 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
adamc@1227 1637 And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1227 1638 p)),
adamc@1227 1639 oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1227 1640 [])
adamc@1227 1641 end)
adamc@1227 1642 | _ => normal ())
adamc@1227 1643 | _ => normal ()
adamc@1227 1644 in
adamc@1227 1645 (rvN, p, map (fn x => (wp, x))
adamc@1227 1646 (case #Where r of
adamc@1227 1647 NONE => []
adamc@1227 1648 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)), outs)
adamc@1227 1649 end
adamc@1227 1650 | Union (q1, q2) =>
adamc@1220 1651 let
adamc@1227 1652 val (rvN, p1, used1, outs1) = doQuery (q1, rvN)
adamc@1227 1653 val (rvN, p2, used2, outs2) = doQuery (q2, rvN)
adamc@1220 1654 in
adamc@1227 1655 case (outs1, outs2) of
adamc@1227 1656 ([], []) => (rvN, Or (p1, p2),
adamc@1227 1657 map (fn (p, e) => (And (p1, p), e)) used1
adamc@1227 1658 @ map (fn (p, e) => (And (p2, p), e)) used2, [])
adamc@1227 1659 | _ => default ()
adamc@1220 1660 end
adamc@1216 1661 in
adamc@1227 1662 doQuery (q, rvN)
adamc@1216 1663 end
adamc@1220 1664 end
adamc@1220 1665
adamc@1220 1666 fun insertProp rvN rv e =
adamc@1220 1667 let
adamc@1220 1668 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1220 1669 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1220 1670 Unknown)
adamc@1220 1671 in
adamc@1220 1672 case parse query e of
adamc@1227 1673 SOME (Query1 r) =>
adamc@1220 1674 let
adamc@1220 1675 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1220 1676 let
adamc@1220 1677 val (rvN, e) = rv rvN
adamc@1220 1678 in
adamc@1220 1679 ((v, e), rvN)
adamc@1220 1680 end) rvN (#From r)
adamc@1220 1681
adamc@1220 1682 fun rvOf v =
adamc@1220 1683 case List.find (fn (v', _) => v' = v) rvs of
adamc@1220 1684 NONE => raise Fail "Iflow.insertProp: Bad table variable"
adamc@1220 1685 | SOME (_, e) => e
adamc@1220 1686
adamc@1220 1687 val p =
adamc@1220 1688 foldl (fn ((t, v), p) =>
adamc@1220 1689 let
adamc@1220 1690 val t =
adamc@1220 1691 case v of
adamc@1229 1692 "New" => t ^ "$New"
adamc@1220 1693 | _ => t
adamc@1220 1694 in
adamc@1220 1695 And (p, Reln (Sql t, [rvOf v]))
adamc@1220 1696 end) True (#From r)
adamc@1220 1697
adamc@1220 1698 val expIn = expIn rv [] rvOf
adamc@1220 1699 in
adamc@1220 1700 case #Where r of
adamc@1220 1701 NONE => p
adamc@1220 1702 | SOME e =>
adamc@1220 1703 case expIn (e, rvN) of
adamc@1220 1704 (inr p', _) => And (p, p')
adamc@1220 1705 | _ => p
adamc@1220 1706 end
adamc@1227 1707 | _ => default ()
adamc@1216 1708 end
adamc@1200 1709
adamc@1221 1710 fun deleteProp rvN rv e =
adamc@1221 1711 let
adamc@1221 1712 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1221 1713 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1221 1714 Unknown)
adamc@1221 1715 in
adamc@1221 1716 case parse query e of
adamc@1227 1717 SOME (Query1 r) =>
adamc@1221 1718 let
adamc@1221 1719 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1221 1720 let
adamc@1221 1721 val (rvN, e) = rv rvN
adamc@1221 1722 in
adamc@1221 1723 ((v, e), rvN)
adamc@1221 1724 end) rvN (#From r)
adamc@1221 1725
adamc@1221 1726 fun rvOf v =
adamc@1221 1727 case List.find (fn (v', _) => v' = v) rvs of
adamc@1221 1728 NONE => raise Fail "Iflow.deleteProp: Bad table variable"
adamc@1221 1729 | SOME (_, e) => e
adamc@1221 1730
adamc@1221 1731 val p =
adamc@1221 1732 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1221 1733
adamc@1221 1734 val expIn = expIn rv [] rvOf
adamc@1221 1735 in
adamc@1221 1736 And (Reln (Sql "$Old", [rvOf "Old"]),
adamc@1221 1737 case #Where r of
adamc@1221 1738 NONE => p
adamc@1221 1739 | SOME e =>
adamc@1221 1740 case expIn (e, rvN) of
adamc@1221 1741 (inr p', _) => And (p, p')
adamc@1221 1742 | _ => p)
adamc@1221 1743 end
adamc@1227 1744 | _ => default ()
adamc@1221 1745 end
adamc@1221 1746
adamc@1223 1747 fun updateProp rvN rv e =
adamc@1223 1748 let
adamc@1223 1749 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1223 1750 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1223 1751 Unknown)
adamc@1223 1752 in
adamc@1223 1753 case parse query e of
adamc@1227 1754 SOME (Query1 r) =>
adamc@1223 1755 let
adamc@1223 1756 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1223 1757 let
adamc@1223 1758 val (rvN, e) = rv rvN
adamc@1223 1759 in
adamc@1223 1760 ((v, e), rvN)
adamc@1223 1761 end) rvN (#From r)
adamc@1223 1762
adamc@1223 1763 fun rvOf v =
adamc@1223 1764 case List.find (fn (v', _) => v' = v) rvs of
adamc@1223 1765 NONE => raise Fail "Iflow.insertProp: Bad table variable"
adamc@1223 1766 | SOME (_, e) => e
adamc@1223 1767
adamc@1223 1768 val p =
adamc@1223 1769 foldl (fn ((t, v), p) =>
adamc@1223 1770 let
adamc@1223 1771 val t =
adamc@1223 1772 case v of
adamc@1229 1773 "New" => t ^ "$New"
adamc@1223 1774 | _ => t
adamc@1223 1775 in
adamc@1223 1776 And (p, Reln (Sql t, [rvOf v]))
adamc@1223 1777 end) True (#From r)
adamc@1223 1778
adamc@1223 1779 val expIn = expIn rv [] rvOf
adamc@1223 1780 in
adamc@1223 1781 And (Reln (Sql "$Old", [rvOf "Old"]),
adamc@1223 1782 case #Where r of
adamc@1223 1783 NONE => p
adamc@1223 1784 | SOME e =>
adamc@1223 1785 case expIn (e, rvN) of
adamc@1223 1786 (inr p', _) => And (p, p')
adamc@1223 1787 | _ => p)
adamc@1223 1788 end
adamc@1227 1789 | _ => default ()
adamc@1223 1790 end
adamc@1223 1791
adamc@1211 1792 fun evalPat env e (pt, _) =
adamc@1211 1793 case pt of
adamc@1211 1794 PWild => (env, True)
adamc@1211 1795 | PVar _ => (e :: env, True)
adamc@1211 1796 | PPrim _ => (env, True)
adamc@1215 1797 | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
adamc@1211 1798 | PCon (_, pc, SOME pt) =>
adamc@1211 1799 let
adamc@1215 1800 val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211 1801 in
adamc@1215 1802 (env, And (p, Reln (PCon1 (patCon pc), [e])))
adamc@1211 1803 end
adamc@1211 1804 | PRecord xpts =>
adamc@1211 1805 foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211 1806 let
adamc@1211 1807 val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211 1808 in
adamc@1211 1809 (env, And (p', p))
adamc@1211 1810 end) (env, True) xpts
adamc@1215 1811 | PNone _ => (env, Reln (PCon0 "None", [e]))
adamc@1211 1812 | PSome (_, pt) =>
adamc@1211 1813 let
adamc@1215 1814 val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211 1815 in
adamc@1215 1816 (env, And (p, Reln (PCon1 "Some", [e])))
adamc@1211 1817 end
adamc@1211 1818
adamc@1211 1819 fun peq (p1, p2) =
adamc@1211 1820 case (p1, p2) of
adamc@1211 1821 (True, True) => true
adamc@1211 1822 | (False, False) => true
adamc@1211 1823 | (Unknown, Unknown) => true
adamc@1211 1824 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1825 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1826 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212 1827 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211 1828 | _ => false
adamc@1211 1829
adamc@1211 1830 fun removeRedundant p1 =
adamc@1211 1831 let
adamc@1211 1832 fun rr p2 =
adamc@1211 1833 if peq (p1, p2) then
adamc@1211 1834 True
adamc@1211 1835 else
adamc@1211 1836 case p2 of
adamc@1211 1837 And (x, y) => And (rr x, rr y)
adamc@1211 1838 | Or (x, y) => Or (rr x, rr y)
adamc@1211 1839 | _ => p2
adamc@1211 1840 in
adamc@1211 1841 rr
adamc@1211 1842 end
adamc@1211 1843
adamc@1218 1844 datatype cflow = Case | Where
adamc@1218 1845 datatype flow = Data | Control of cflow
adamc@1218 1846 type check = ErrorMsg.span * exp * prop
adamc@1221 1847 type dml = ErrorMsg.span * prop
adamc@1218 1848
adamc@1217 1849 structure St :> sig
adamc@1217 1850 type t
adamc@1217 1851 val create : {Var : int,
adamc@1217 1852 Ambient : prop} -> t
adamc@1217 1853
adamc@1217 1854 val curVar : t -> int
adamc@1217 1855 val nextVar : t -> t * int
adamc@1217 1856
adamc@1217 1857 val ambient : t -> prop
adamc@1217 1858 val setAmbient : t * prop -> t
adamc@1217 1859
adamc@1218 1860 val paths : t -> (check * cflow) list
adamc@1218 1861 val addPath : t * (check * cflow) -> t
adamc@1218 1862 val addPaths : t * (check * cflow) list -> t
adamc@1218 1863 val clearPaths : t -> t
adamc@1218 1864 val setPaths : t * (check * cflow) list -> t
adamc@1217 1865
adamc@1218 1866 val sent : t -> (check * flow) list
adamc@1218 1867 val addSent : t * (check * flow) -> t
adamc@1218 1868 val setSent : t * (check * flow) list -> t
adamc@1220 1869
adamc@1221 1870 val inserted : t -> dml list
adamc@1221 1871 val addInsert : t * dml -> t
adamc@1221 1872
adamc@1221 1873 val deleted : t -> dml list
adamc@1221 1874 val addDelete : t * dml -> t
adamc@1223 1875
adamc@1223 1876 val updated : t -> dml list
adamc@1223 1877 val addUpdate : t * dml -> t
adamc@1217 1878 end = struct
adamc@1217 1879
adamc@1217 1880 type t = {Var : int,
adamc@1217 1881 Ambient : prop,
adamc@1218 1882 Path : (check * cflow) list,
adamc@1220 1883 Sent : (check * flow) list,
adamc@1221 1884 Insert : dml list,
adamc@1223 1885 Delete : dml list,
adamc@1223 1886 Update : dml list}
adamc@1217 1887
adamc@1217 1888 fun create {Var = v, Ambient = p} = {Var = v,
adamc@1217 1889 Ambient = p,
adamc@1217 1890 Path = [],
adamc@1220 1891 Sent = [],
adamc@1221 1892 Insert = [],
adamc@1223 1893 Delete = [],
adamc@1223 1894 Update = []}
adamc@1217 1895
adamc@1217 1896 fun curVar (t : t) = #Var t
adamc@1217 1897 fun nextVar (t : t) = ({Var = #Var t + 1,
adamc@1217 1898 Ambient = #Ambient t,
adamc@1217 1899 Path = #Path t,
adamc@1220 1900 Sent = #Sent t,
adamc@1221 1901 Insert = #Insert t,
adamc@1223 1902 Delete = #Delete t,
adamc@1223 1903 Update = #Update t}, #Var t)
adamc@1217 1904
adamc@1217 1905 fun ambient (t : t) = #Ambient t
adamc@1217 1906 fun setAmbient (t : t, p) = {Var = #Var t,
adamc@1217 1907 Ambient = p,
adamc@1217 1908 Path = #Path t,
adamc@1220 1909 Sent = #Sent t,
adamc@1221 1910 Insert = #Insert t,
adamc@1223 1911 Delete = #Delete t,
adamc@1223 1912 Update = #Update t}
adamc@1217 1913
adamc@1218 1914 fun paths (t : t) = #Path t
adamc@1217 1915 fun addPath (t : t, c) = {Var = #Var t,
adamc@1217 1916 Ambient = #Ambient t,
adamc@1217 1917 Path = c :: #Path t,
adamc@1220 1918 Sent = #Sent t,
adamc@1221 1919 Insert = #Insert t,
adamc@1223 1920 Delete = #Delete t,
adamc@1223 1921 Update = #Update t}
adamc@1218 1922 fun addPaths (t : t, cs) = {Var = #Var t,
adamc@1218 1923 Ambient = #Ambient t,
adamc@1218 1924 Path = cs @ #Path t,
adamc@1220 1925 Sent = #Sent t,
adamc@1221 1926 Insert = #Insert t,
adamc@1223 1927 Delete = #Delete t,
adamc@1223 1928 Update = #Update t}
adamc@1218 1929 fun clearPaths (t : t) = {Var = #Var t,
adamc@1218 1930 Ambient = #Ambient t,
adamc@1218 1931 Path = [],
adamc@1220 1932 Sent = #Sent t,
adamc@1221 1933 Insert = #Insert t,
adamc@1223 1934 Delete = #Delete t,
adamc@1223 1935 Update = #Update t}
adamc@1218 1936 fun setPaths (t : t, cs) = {Var = #Var t,
adamc@1218 1937 Ambient = #Ambient t,
adamc@1218 1938 Path = cs,
adamc@1220 1939 Sent = #Sent t,
adamc@1221 1940 Insert = #Insert t,
adamc@1223 1941 Delete = #Delete t,
adamc@1223 1942 Update = #Update t}
adamc@1217 1943
adamc@1217 1944 fun sent (t : t) = #Sent t
adamc@1217 1945 fun addSent (t : t, c) = {Var = #Var t,
adamc@1217 1946 Ambient = #Ambient t,
adamc@1217 1947 Path = #Path t,
adamc@1220 1948 Sent = c :: #Sent t,
adamc@1221 1949 Insert = #Insert t,
adamc@1223 1950 Delete = #Delete t,
adamc@1223 1951 Update = #Update t}
adamc@1217 1952 fun setSent (t : t, cs) = {Var = #Var t,
adamc@1217 1953 Ambient = #Ambient t,
adamc@1217 1954 Path = #Path t,
adamc@1220 1955 Sent = cs,
adamc@1221 1956 Insert = #Insert t,
adamc@1223 1957 Delete = #Delete t,
adamc@1223 1958 Update = #Update t}
adamc@1220 1959
adamc@1220 1960 fun inserted (t : t) = #Insert t
adamc@1220 1961 fun addInsert (t : t, c) = {Var = #Var t,
adamc@1220 1962 Ambient = #Ambient t,
adamc@1220 1963 Path = #Path t,
adamc@1220 1964 Sent = #Sent t,
adamc@1221 1965 Insert = c :: #Insert t,
adamc@1223 1966 Delete = #Delete t,
adamc@1223 1967 Update = #Update t}
adamc@1221 1968
adamc@1221 1969 fun deleted (t : t) = #Delete t
adamc@1221 1970 fun addDelete (t : t, c) = {Var = #Var t,
adamc@1221 1971 Ambient = #Ambient t,
adamc@1221 1972 Path = #Path t,
adamc@1221 1973 Sent = #Sent t,
adamc@1221 1974 Insert = #Insert t,
adamc@1223 1975 Delete = c :: #Delete t,
adamc@1223 1976 Update = #Update t}
adamc@1223 1977
adamc@1223 1978 fun updated (t : t) = #Update t
adamc@1223 1979 fun addUpdate (t : t, c) = {Var = #Var t,
adamc@1223 1980 Ambient = #Ambient t,
adamc@1223 1981 Path = #Path t,
adamc@1223 1982 Sent = #Sent t,
adamc@1223 1983 Insert = #Insert t,
adamc@1223 1984 Delete = #Delete t,
adamc@1223 1985 Update = c :: #Update t}
adamc@1217 1986
adamc@1217 1987 end
adamc@1217 1988
adamc@1230 1989 fun havocReln r =
adamc@1230 1990 let
adamc@1230 1991 fun hr p =
adamc@1230 1992 case p of
adamc@1230 1993 True => p
adamc@1230 1994 | False => p
adamc@1230 1995 | Unknown => p
adamc@1230 1996 | And (p1, p2) => And (hr p1, hr p2)
adamc@1230 1997 | Or (p1, p2) => Or (hr p1, hr p2)
adamc@1230 1998 | Reln (r', _) => if r' = r then True else p
adamc@1230 1999 | Cond (e, p) => Cond (e, hr p)
adamc@1230 2000 in
adamc@1230 2001 hr
adamc@1230 2002 end
adamc@1230 2003
adamc@1217 2004 fun evalExp env (e as (_, loc), st) =
adamc@1200 2005 let
adamc@1200 2006 fun default () =
adamc@1217 2007 let
adamc@1217 2008 val (st, nv) = St.nextVar st
adamc@1217 2009 in
adamc@1229 2010 (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
adamc@1229 2011 ("nv", p_exp (Var nv))];*)
adamc@1217 2012 (Var nv, st)
adamc@1217 2013 end
adamc@1200 2014
adamc@1217 2015 fun addSent (p, e, st) =
adamc@1218 2016 let
adamc@1218 2017 val st = if isKnown e then
adamc@1218 2018 st
adamc@1218 2019 else
adamc@1218 2020 St.addSent (st, ((loc, e, p), Data))
adamc@1218 2021
adamc@1218 2022 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
adamc@1218 2023 in
adamc@1218 2024 St.clearPaths st
adamc@1218 2025 end
adamc@1200 2026 in
adamc@1200 2027 case #1 e of
adamc@1200 2028 EPrim p => (Const p, st)
adamc@1200 2029 | ERel n => (List.nth (env, n), st)
adamc@1200 2030 | ENamed _ => default ()
adamc@1215 2031 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
adamc@1200 2032 | ECon (_, pc, SOME e) =>
adamc@1200 2033 let
adamc@1200 2034 val (e, st) = evalExp env (e, st)
adamc@1200 2035 in
adamc@1215 2036 (Func (DtCon1 (patCon pc), [e]), st)
adamc@1200 2037 end
adamc@1215 2038 | ENone _ => (Func (DtCon0 "None", []), st)
adamc@1200 2039 | ESome (_, e) =>
adamc@1200 2040 let
adamc@1200 2041 val (e, st) = evalExp env (e, st)
adamc@1200 2042 in
adamc@1215 2043 (Func (DtCon1 "Some", [e]), st)
adamc@1200 2044 end
adamc@1200 2045 | EFfi _ => default ()
adamc@1213 2046
adamc@1200 2047 | EFfiApp (m, s, es) =>
adamc@1200 2048 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 2049 let
adamc@1200 2050 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 2051 in
adamc@1217 2052 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
adamc@1200 2053 end
adamc@1200 2054 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 2055 default ()
adamc@1200 2056 else
adamc@1200 2057 let
adamc@1200 2058 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 2059 in
adamc@1215 2060 (Func (Other (m ^ "." ^ s), es), st)
adamc@1200 2061 end
adamc@1213 2062
adamc@1213 2063 | EApp (e1, e2) =>
adamc@1213 2064 let
adamc@1213 2065 val (e1, st) = evalExp env (e1, st)
adamc@1213 2066 in
adamc@1213 2067 case e1 of
adamc@1213 2068 Finish => (Finish, st)
adamc@1213 2069 | _ => default ()
adamc@1213 2070 end
adamc@1213 2071
adamc@1200 2072 | EAbs _ => default ()
adamc@1200 2073 | EUnop (s, e1) =>
adamc@1200 2074 let
adamc@1200 2075 val (e1, st) = evalExp env (e1, st)
adamc@1200 2076 in
adamc@1215 2077 (Func (Other s, [e1]), st)
adamc@1200 2078 end
adamc@1200 2079 | EBinop (s, e1, e2) =>
adamc@1200 2080 let
adamc@1200 2081 val (e1, st) = evalExp env (e1, st)
adamc@1200 2082 val (e2, st) = evalExp env (e2, st)
adamc@1200 2083 in
adamc@1215 2084 (Func (Other s, [e1, e2]), st)
adamc@1200 2085 end
adamc@1200 2086 | ERecord xets =>
adamc@1200 2087 let
adamc@1200 2088 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 2089 let
adamc@1200 2090 val (e, st) = evalExp env (e, st)
adamc@1200 2091 in
adamc@1200 2092 ((x, e), st)
adamc@1200 2093 end) st xets
adamc@1200 2094 in
adamc@1200 2095 (Recd xes, st)
adamc@1200 2096 end
adamc@1200 2097 | EField (e, s) =>
adamc@1200 2098 let
adamc@1200 2099 val (e, st) = evalExp env (e, st)
adamc@1200 2100 in
adamc@1200 2101 (Proj (e, s), st)
adamc@1200 2102 end
adamc@1218 2103 | ECase (e, pes, {result = res, ...}) =>
adamc@1211 2104 let
adamc@1211 2105 val (e, st) = evalExp env (e, st)
adamc@1217 2106 val (st, r) = St.nextVar st
adamc@1217 2107 val orig = St.ambient st
adamc@1218 2108 val origPaths = St.paths st
adamc@1211 2109
adamc@1218 2110 val st = St.addPath (st, ((loc, e, orig), Case))
adamc@1218 2111
adamc@1218 2112 val (st, paths) =
adamc@1218 2113 foldl (fn ((pt, pe), (st, paths)) =>
adamc@1218 2114 let
adamc@1218 2115 val (env, pp) = evalPat env e pt
adamc@1218 2116 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
adamc@1218 2117
adamc@1218 2118 val this = And (removeRedundant orig (St.ambient st'),
adamc@1218 2119 Reln (Eq, [Var r, pe]))
adamc@1218 2120 in
adamc@1218 2121 (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths),
adamc@1218 2122 St.paths st' @ paths)
adamc@1218 2123 end) (St.setAmbient (st, False), []) pes
adamc@1218 2124
adamc@1218 2125 val st = case #1 res of
adamc@1218 2126 TRecord [] => St.setPaths (st, origPaths)
adamc@1218 2127 | _ => St.setPaths (st, paths)
adamc@1211 2128 in
adamc@1217 2129 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
adamc@1211 2130 end
adamc@1200 2131 | EStrcat (e1, e2) =>
adamc@1200 2132 let
adamc@1200 2133 val (e1, st) = evalExp env (e1, st)
adamc@1200 2134 val (e2, st) = evalExp env (e2, st)
adamc@1200 2135 in
adamc@1215 2136 (Func (Other "cat", [e1, e2]), st)
adamc@1200 2137 end
adamc@1200 2138 | EError _ => (Finish, st)
adamc@1200 2139 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 2140 let
adamc@1200 2141 val (b, st) = evalExp env (b, st)
adamc@1200 2142 val (m, st) = evalExp env (m, st)
adamc@1200 2143 in
adamc@1217 2144 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
adamc@1200 2145 end
adamc@1200 2146 | ERedirect (e, _) =>
adamc@1200 2147 let
adamc@1200 2148 val (e, st) = evalExp env (e, st)
adamc@1200 2149 in
adamc@1217 2150 (Finish, addSent (St.ambient st, e, st))
adamc@1200 2151 end
adamc@1200 2152 | EWrite e =>
adamc@1200 2153 let
adamc@1200 2154 val (e, st) = evalExp env (e, st)
adamc@1200 2155 in
adamc@1217 2156 (Recd [], addSent (St.ambient st, e, st))
adamc@1200 2157 end
adamc@1200 2158 | ESeq (e1, e2) =>
adamc@1200 2159 let
adamc@1200 2160 val (_, st) = evalExp env (e1, st)
adamc@1200 2161 in
adamc@1200 2162 evalExp env (e2, st)
adamc@1200 2163 end
adamc@1200 2164 | ELet (_, _, e1, e2) =>
adamc@1200 2165 let
adamc@1200 2166 val (e1, st) = evalExp env (e1, st)
adamc@1200 2167 in
adamc@1200 2168 evalExp (e1 :: env) (e2, st)
adamc@1200 2169 end
adamc@1200 2170 | EClosure (n, es) =>
adamc@1200 2171 let
adamc@1200 2172 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 2173 in
adamc@1215 2174 (Func (Other ("Cl" ^ Int.toString n), es), st)
adamc@1200 2175 end
adamc@1200 2176
adamc@1200 2177 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 2178 let
adamc@1200 2179 val (_, st) = evalExp env (q, st)
adamc@1200 2180 val (i, st) = evalExp env (i, st)
adamc@1200 2181
adamc@1217 2182 val (st', r) = St.nextVar st
adamc@1217 2183 val (st', acc) = St.nextVar st'
adamc@1200 2184
adamc@1200 2185 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 2186
adamc@1227 2187 val (st', qp, used, _) =
adamc@1214 2188 queryProp env
adamc@1217 2189 st' (fn st' =>
adamc@1217 2190 let
adamc@1217 2191 val (st', rv) = St.nextVar st'
adamc@1217 2192 in
adamc@1217 2193 (st', Var rv)
adamc@1217 2194 end)
adamc@1214 2195 (AllCols (Var r)) q
adamc@1200 2196
adamc@1217 2197 val p' = And (qp, St.ambient st')
adamc@1200 2198
adamc@1217 2199 val (st, res) = if varInP acc (St.ambient st') then
adamc@1217 2200 let
adamc@1217 2201 val (st, r) = St.nextVar st
adamc@1217 2202 in
adamc@1217 2203 (st, Var r)
adamc@1217 2204 end
adamc@1217 2205 else
adamc@1217 2206 let
adamc@1217 2207 val (st, out) = St.nextVar st'
adamc@1217 2208
adamc@1217 2209 val p = Or (Reln (Eq, [Var out, i]),
adamc@1217 2210 And (Reln (Eq, [Var out, b]),
adamc@1217 2211 p'))
adamc@1217 2212 in
adamc@1217 2213 (St.setAmbient (st, p), Var out)
adamc@1217 2214 end
adamc@1210 2215
adamc@1218 2216 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
adamc@1212 2217
adamc@1227 2218 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
adamc@1200 2219 in
adamc@1218 2220 (res, St.addPaths (St.setSent (st, sent), paths))
adamc@1200 2221 end
adamc@1220 2222 | EDml e =>
adamc@1220 2223 (case parse dml e of
adamc@1220 2224 NONE => (print ("Warning: Information flow checker can't parse DML command at "
adamc@1220 2225 ^ ErrorMsg.spanToString loc ^ "\n");
adamc@1220 2226 default ())
adamc@1220 2227 | SOME d =>
adamc@1220 2228 case d of
adamc@1220 2229 Insert (tab, es) =>
adamc@1220 2230 let
adamc@1220 2231 val (st, new) = St.nextVar st
adamc@1220 2232
adamc@1220 2233 fun rv st =
adamc@1220 2234 let
adamc@1220 2235 val (st, n) = St.nextVar st
adamc@1220 2236 in
adamc@1220 2237 (st, Var n)
adamc@1220 2238 end
adamc@1220 2239
adamc@1223 2240 val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT")
adamc@1220 2241
adamc@1220 2242 val (es, st) = ListUtil.foldlMap
adamc@1220 2243 (fn ((x, e), st) =>
adamc@1220 2244 let
adamc@1220 2245 val (e, st) = case expIn (e, st) of
adamc@1220 2246 (inl e, st) => (e, st)
adamc@1220 2247 | (inr _, _) => raise Fail
adamc@1220 2248 ("Iflow.evalExp: Selecting "
adamc@1220 2249 ^ "boolean expression")
adamc@1220 2250 in
adamc@1220 2251 ((x, e), st)
adamc@1220 2252 end)
adamc@1220 2253 st es
adamc@1220 2254 in
adamc@1220 2255 (Recd [], St.addInsert (st, (loc, And (St.ambient st,
adamc@1229 2256 Reln (Sql (tab ^ "$New"), [Recd es])))))
adamc@1221 2257 end
adamc@1221 2258 | Delete (tab, e) =>
adamc@1221 2259 let
adamc@1221 2260 val (st, old) = St.nextVar st
adamc@1221 2261
adamc@1221 2262 fun rv st =
adamc@1221 2263 let
adamc@1221 2264 val (st, n) = St.nextVar st
adamc@1221 2265 in
adamc@1221 2266 (st, Var n)
adamc@1221 2267 end
adamc@1221 2268
adamc@1221 2269 val expIn = expIn rv env (fn "T" => Var old
adamc@1221 2270 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221 2271
adamc@1221 2272 val (p, st) = case expIn (e, st) of
adamc@1221 2273 (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean"
adamc@1221 2274 | (inr p, st) => (p, st)
adamc@1221 2275
adamc@1221 2276 val p = And (p,
adamc@1221 2277 And (Reln (Sql "$Old", [Var old]),
adamc@1221 2278 Reln (Sql tab, [Var old])))
adamc@1230 2279
adamc@1230 2280 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
adamc@1221 2281 in
adamc@1221 2282 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
adamc@1223 2283 end
adamc@1223 2284 | Update (tab, fs, e) =>
adamc@1223 2285 let
adamc@1223 2286 val (st, new) = St.nextVar st
adamc@1223 2287 val (st, old) = St.nextVar st
adamc@1223 2288
adamc@1223 2289 fun rv st =
adamc@1223 2290 let
adamc@1223 2291 val (st, n) = St.nextVar st
adamc@1223 2292 in
adamc@1223 2293 (st, Var n)
adamc@1223 2294 end
adamc@1223 2295
adamc@1223 2296 val expIn = expIn rv env (fn "T" => Var old
adamc@1223 2297 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1223 2298
adamc@1223 2299 val (fs, st) = ListUtil.foldlMap
adamc@1223 2300 (fn ((x, e), st) =>
adamc@1223 2301 let
adamc@1223 2302 val (e, st) = case expIn (e, st) of
adamc@1223 2303 (inl e, st) => (e, st)
adamc@1223 2304 | (inr _, _) => raise Fail
adamc@1223 2305 ("Iflow.evalExp: Selecting "
adamc@1223 2306 ^ "boolean expression")
adamc@1223 2307 in
adamc@1223 2308 ((x, e), st)
adamc@1223 2309 end)
adamc@1223 2310 st fs
adamc@1223 2311
adamc@1226 2312 val fs' = case SM.find (!tabs, tab) of
adamc@1224 2313 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
adamc@1226 2314 | SOME (fs', _) => fs'
adamc@1224 2315
adamc@1224 2316 val fs = foldl (fn (f, fs) =>
adamc@1224 2317 if List.exists (fn (f', _) => f' = f) fs then
adamc@1224 2318 fs
adamc@1224 2319 else
adamc@1224 2320 (f, Proj (Var old, f)) :: fs) fs fs'
adamc@1224 2321
adamc@1223 2322 val (p, st) = case expIn (e, st) of
adamc@1223 2323 (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
adamc@1223 2324 | (inr p, st) => (p, st)
adamc@1223 2325
adamc@1223 2326 val p = And (p,
adamc@1229 2327 And (Reln (Sql (tab ^ "$New"), [Recd fs]),
adamc@1223 2328 And (Reln (Sql "$Old", [Var old]),
adamc@1223 2329 Reln (Sql tab, [Var old]))))
adamc@1230 2330
adamc@1230 2331 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
adamc@1223 2332 in
adamc@1223 2333 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
adamc@1220 2334 end)
adamc@1220 2335
adamc@1229 2336 | ENextval (EPrim (Prim.String seq), _) =>
adamc@1229 2337 let
adamc@1229 2338 val (st, nv) = St.nextVar st
adamc@1229 2339 in
adamc@1229 2340 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv]))))
adamc@1229 2341 end
adamc@1200 2342 | ENextval _ => default ()
adamc@1200 2343 | ESetval _ => default ()
adamc@1200 2344
adamc@1213 2345 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1217 2346 let
adamc@1217 2347 val (st, nv) = St.nextVar st
adamc@1217 2348 in
adamc@1217 2349 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
adamc@1217 2350 end
adamc@1213 2351
adamc@1200 2352 | EUnurlify _ => default ()
adamc@1200 2353 | EJavaScript _ => default ()
adamc@1200 2354 | ESignalReturn _ => default ()
adamc@1200 2355 | ESignalBind _ => default ()
adamc@1200 2356 | ESignalSource _ => default ()
adamc@1200 2357 | EServerCall _ => default ()
adamc@1200 2358 | ERecv _ => default ()
adamc@1200 2359 | ESleep _ => default ()
adamc@1200 2360 | ESpawn _ => default ()
adamc@1200 2361 end
adamc@1200 2362
adamc@1200 2363 fun check file =
adamc@1200 2364 let
adamc@1213 2365 val file = MonoReduce.reduce file
adamc@1213 2366 val file = MonoOpt.optimize file
adamc@1213 2367 val file = Fuse.fuse file
adamc@1213 2368 val file = MonoOpt.optimize file
adamc@1216 2369 val file = MonoShake.shake file
adamc@1213 2370 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 2371
adamc@1207 2372 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 2373 case d of
adamc@1207 2374 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 2375 | _ => exptd) IS.empty file
adamc@1207 2376
adamc@1223 2377 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
adamc@1200 2378 case d of
adamc@1226 2379 DTable (tab, fs, pk, _) =>
adamc@1226 2380 let
adamc@1226 2381 val ks =
adamc@1226 2382 case #1 pk of
adamc@1226 2383 EPrim (Prim.String s) =>
adamc@1226 2384 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
adamc@1226 2385 [] => []
adamc@1226 2386 | pk => [pk])
adamc@1226 2387 | _ => []
adamc@1226 2388 in
adamc@1226 2389 if size tab >= 3 then
adamc@1226 2390 (tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
adamc@1226 2391 (map #1 fs,
adamc@1226 2392 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
adamc@1226 2393 ^ String.extract (s, 4, NONE))) ks));
adamc@1226 2394 (vals, inserts, deletes, updates, client, insert, delete, update))
adamc@1226 2395 else
adamc@1226 2396 raise Fail "Table name does not begin with uw_"
adamc@1226 2397 end
adamc@1224 2398 | DVal (_, n, _, e, _) =>
adamc@1200 2399 let
adamc@1207 2400 val isExptd = IS.member (exptd, n)
adamc@1207 2401
adamc@1207 2402 fun deAbs (e, env, nv, p) =
adamc@1200 2403 case #1 e of
adamc@1207 2404 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207 2405 if isExptd then
adamc@1207 2406 And (p, Reln (Known, [Var nv]))
adamc@1207 2407 else
adamc@1207 2408 p)
adamc@1207 2409 | _ => (e, env, nv, p)
adamc@1200 2410
adamc@1207 2411 val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200 2412
adamc@1217 2413 val (_, st) = evalExp env (e, St.create {Var = nv,
adamc@1217 2414 Ambient = p})
adamc@1200 2415 in
adamc@1223 2416 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates,
adamc@1223 2417 client, insert, delete, update)
adamc@1200 2418 end
adamc@1202 2419
adamc@1220 2420 | DPolicy pol =>
adamc@1218 2421 let
adamc@1220 2422 fun rv rvN = (rvN + 1, Lvar rvN)
adamc@1218 2423 in
adamc@1220 2424 case pol of
adamc@1220 2425 PolClient e =>
adamc@1220 2426 let
adamc@1227 2427 val (_, p, _, outs) = queryProp [] 0 rv SomeCol e
adamc@1220 2428 in
adamc@1223 2429 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
adamc@1220 2430 end
adamc@1220 2431 | PolInsert e =>
adamc@1220 2432 let
adamc@1220 2433 val p = insertProp 0 rv e
adamc@1220 2434 in
adamc@1223 2435 (vals, inserts, deletes, updates, client, p :: insert, delete, update)
adamc@1221 2436 end
adamc@1221 2437 | PolDelete e =>
adamc@1221 2438 let
adamc@1221 2439 val p = deleteProp 0 rv e
adamc@1221 2440 in
adamc@1223 2441 (vals, inserts, deletes, updates, client, insert, p :: delete, update)
adamc@1223 2442 end
adamc@1223 2443 | PolUpdate e =>
adamc@1223 2444 let
adamc@1223 2445 val p = updateProp 0 rv e
adamc@1223 2446 in
adamc@1223 2447 (vals, inserts, deletes, updates, client, insert, delete, p :: update)
adamc@1220 2448 end
adamc@1229 2449 | PolSequence e =>
adamc@1229 2450 (case #1 e of
adamc@1229 2451 EPrim (Prim.String seq) =>
adamc@1229 2452 let
adamc@1229 2453 val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
adamc@1229 2454 val outs = [Lvar 0]
adamc@1229 2455 in
adamc@1229 2456 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
adamc@1229 2457 end
adamc@1229 2458 | _ => (vals, inserts, deletes, updates, client, insert, delete, update))
adamc@1218 2459 end
adamc@1214 2460
adamc@1223 2461 | _ => (vals, inserts, deletes, updates, client, insert, delete, update)
adamc@1202 2462
adamc@1203 2463 val () = reset ()
adamc@1202 2464
adamc@1223 2465 val (vals, inserts, deletes, updates, client, insert, delete, update) =
adamc@1223 2466 foldl decl ([], [], [], [], [], [], [], []) file
adamc@1220 2467
adamc@1224 2468
adamc@1220 2469 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
adamc@1220 2470 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
adamc@1221 2471
adamc@1221 2472 fun doDml (cmds, pols) =
adamc@1221 2473 app (fn (loc, p) =>
adamc@1221 2474 if decompH p
adamc@1221 2475 (fn hyps =>
adamc@1231 2476 let
adamc@1231 2477 val cc = ccOf hyps
adamc@1231 2478 in
adamc@1231 2479 List.exists (fn p' =>
adamc@1231 2480 if decompG p'
adamc@1231 2481 (fn goals => imply (cc, hyps, goals, NONE)) then
adamc@1231 2482 ((*reset ();
adamc@1231 2483 Print.prefaces "Match" [("hyp", p_prop p),
adamc@1231 2484 ("goal", p_prop p')];*)
adamc@1231 2485 true)
adamc@1231 2486 else
adamc@1231 2487 false)
adamc@1231 2488 pols
adamc@1231 2489 end handle Cc.Contradiction => true) then
adamc@1221 2490 ()
adamc@1221 2491 else
adamc@1221 2492 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1221 2493 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
adamc@1200 2494 in
adamc@1218 2495 app (fn ((loc, e, p), fl) =>
adamc@1207 2496 let
adamc@1213 2497 fun doOne e =
adamc@1213 2498 let
adamc@1213 2499 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213 2500 in
adamc@1220 2501 if decompH p
adamc@1220 2502 (fn hyps =>
adamc@1228 2503 let
adamc@1231 2504 val cc = ccOf hyps
adamc@1231 2505
adamc@1228 2506 val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab)
adamc@1228 2507 | (_, avail) => avail) SS.empty hyps
adamc@1228 2508
adamc@1228 2509 fun tryCombos (maxLv, pols, g, outs) =
adamc@1228 2510 case pols of
adamc@1228 2511 [] =>
adamc@1228 2512 decompG g
adamc@1231 2513 (fn goals => imply (cc, hyps, goals, SOME outs))
adamc@1228 2514 | (g1, outs1) :: pols =>
adamc@1228 2515 let
adamc@1228 2516 val g1 = bumpLvarsP (maxLv + 1) g1
adamc@1228 2517 val outs1 = map (bumpLvars (maxLv + 1)) outs1
adamc@1228 2518 fun skip () = tryCombos (maxLv, pols, g, outs)
adamc@1228 2519 in
adamc@1228 2520 if decompG g1
adamc@1228 2521 (List.all (fn AReln (Sql tab, _) =>
adamc@1228 2522 SS.member (avail, tab)
adamc@1228 2523 | _ => true)) then
adamc@1228 2524 skip ()
adamc@1228 2525 orelse tryCombos (Int.max (maxLv,
adamc@1228 2526 maxLvarP g1),
adamc@1228 2527 pols,
adamc@1228 2528 And (g1, g),
adamc@1228 2529 outs1 @ outs)
adamc@1228 2530 else
adamc@1228 2531 skip ()
adamc@1228 2532 end
adamc@1228 2533 in
adamc@1228 2534 (fl <> Control Where
adamc@1231 2535 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
adamc@1228 2536 orelse List.exists (fn (p', outs) =>
adamc@1228 2537 decompG p'
adamc@1231 2538 (fn goals => imply (cc, hyps, goals,
adamc@1231 2539 SOME outs)))
adamc@1228 2540 client
adamc@1228 2541 orelse tryCombos (0, client, True, [])
adamc@1228 2542 orelse (reset ();
adamc@1229 2543 Print.preface ("Untenable hypotheses"
adamc@1229 2544 ^ (case fl of
adamc@1229 2545 Control Where => " (WHERE clause)"
adamc@1229 2546 | Control Case => " (case discriminee)"
adamc@1229 2547 | Data => " (returned data value)"),
adamc@1228 2548 Print.p_list p_atom hyps);
adamc@1228 2549 false)
adamc@1231 2550 end handle Cc.Contradiction => true) then
adamc@1213 2551 ()
adamc@1213 2552 else
adamc@1228 2553 ErrorMsg.errorAt loc "The information flow policy may be violated here."
adamc@1213 2554 end
adamc@1213 2555
adamc@1213 2556 fun doAll e =
adamc@1213 2557 case e of
adamc@1213 2558 Const _ => ()
adamc@1213 2559 | Var _ => doOne e
adamc@1213 2560 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1216 2561 | Func (UnCon _, [_]) => doOne e
adamc@1215 2562 | Func (_, es) => app doAll es
adamc@1213 2563 | Recd xes => app (doAll o #2) xes
adamc@1213 2564 | Proj _ => doOne e
adamc@1213 2565 | Finish => ()
adamc@1207 2566 in
adamc@1213 2567 doAll e
adamc@1220 2568 end) vals;
adamc@1220 2569
adamc@1221 2570 doDml (inserts, insert);
adamc@1223 2571 doDml (deletes, delete);
adamc@1223 2572 doDml (updates, update)
adamc@1200 2573 end
adamc@1200 2574
adamc@1213 2575 val check = fn file =>
adamc@1213 2576 let
adamc@1213 2577 val oldInline = Settings.getMonoInline ()
adamc@1213 2578 in
adamc@1213 2579 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 2580 NONE => 1000000
adamc@1213 2581 | SOME n => n);
adamc@1213 2582 check file;
adamc@1213 2583 Settings.setMonoInline oldInline)
adamc@1213 2584 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 2585 raise ex)
adamc@1213 2586 end
adamc@1213 2587
adamc@1200 2588 end