Mercurial > urweb

annotate src/iflow.sml @ 1327:1cc67fdac4d3

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