Mercurial > urweb

annotate src/iflow.sml @ 1281:60e19545841b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalAny policies
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 12:12:08 -0400
parents 3d06e0f7a6f3
children a9a500d22ebc
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
adam@1281 1231 val allowEqual : { table : string, field : string, known : bool } -> unit
adam@1280 1232 val mayTest : prop -> bool
adam@1280 1233
adamc@1236 1234 val allowInsert : atom list -> unit
adamc@1236 1235 val insert : ErrorMsg.span -> unit
adamc@1236 1236
adamc@1236 1237 val allowDelete : atom list -> unit
adamc@1236 1238 val delete : ErrorMsg.span -> unit
adamc@1236 1239
adamc@1236 1240 val allowUpdate : atom list -> unit
adamc@1236 1241 val update : ErrorMsg.span -> unit
adamc@1236 1242
adamc@1236 1243 val havocReln : reln -> unit
adamc@1245 1244 val havocCookie : string -> unit
adamc@1238 1245
adamc@1251 1246 val check : atom -> bool
adamc@1251 1247
adamc@1238 1248 val debug : unit -> unit
adamc@1236 1249 end = struct
adamc@1236 1250
adamc@1236 1251 val hnames = ref 1
adamc@1236 1252
adamc@1244 1253 type hyps = int * atom list * bool ref
adamc@1236 1254
adamc@1236 1255 val db = Cc.database ()
adamc@1244 1256 val path = ref ([] : ((int * atom list) * check) option ref list)
adamc@1244 1257 val hyps = ref (0, [] : atom list, ref false)
adamc@1236 1258 val nvar = ref 0
adamc@1236 1259
adamc@1244 1260 fun setHyps (n', hs) =
adamc@1236 1261 let
adamc@1244 1262 val (n, _, _) = !hyps
adamc@1236 1263 in
adamc@1236 1264 if n' = n then
adamc@1236 1265 ()
adamc@1236 1266 else
adamc@1244 1267 (hyps := (n', hs, ref false);
adamc@1236 1268 Cc.clear db;
adamc@1236 1269 app (fn a => Cc.assert (db, a)) hs)
adamc@1236 1270 end
adamc@1236 1271
adamc@1244 1272 fun useKeys () =
adamc@1244 1273 let
adamc@1244 1274 val changed = ref false
adamc@1244 1275
adamc@1244 1276 fun findKeys (hyps, acc) =
adamc@1244 1277 case hyps of
adamc@1247 1278 [] => rev acc
adamc@1244 1279 | (a as AReln (Sql tab, [r1])) :: hyps =>
adamc@1244 1280 (case SM.find (!tabs, tab) of
adamc@1244 1281 NONE => findKeys (hyps, a :: acc)
adamc@1244 1282 | SOME (_, []) => findKeys (hyps, a :: acc)
adamc@1244 1283 | SOME (_, ks) =>
adamc@1244 1284 let
adamc@1244 1285 fun finder (hyps, acc) =
adamc@1244 1286 case hyps of
adamc@1247 1287 [] => rev acc
adamc@1244 1288 | (a as AReln (Sql tab', [r2])) :: hyps =>
adamc@1244 1289 if tab' = tab andalso
adamc@1244 1290 List.exists (List.all (fn f =>
adamc@1244 1291 let
adamc@1244 1292 val r =
adamc@1244 1293 Cc.check (db,
adamc@1244 1294 AReln (Eq, [Proj (r1, f),
adamc@1244 1295 Proj (r2, f)]))
adamc@1244 1296 in
adamc@1244 1297 (*Print.prefaces "Fs"
adamc@1244 1298 [("tab",
adamc@1244 1299 Print.PD.string tab),
adamc@1244 1300 ("r1",
adamc@1244 1301 p_exp (Proj (r1, f))),
adamc@1244 1302 ("r2",
adamc@1244 1303 p_exp (Proj (r2, f))),
adamc@1244 1304 ("r",
adamc@1244 1305 Print.PD.string
adamc@1244 1306 (Bool.toString r))];*)
adamc@1244 1307 r
adamc@1244 1308 end)) ks then
adamc@1244 1309 (changed := true;
adamc@1244 1310 Cc.assert (db, AReln (Eq, [r1, r2]));
adamc@1244 1311 finder (hyps, acc))
adamc@1244 1312 else
adamc@1244 1313 finder (hyps, a :: acc)
adamc@1244 1314 | a :: hyps => finder (hyps, a :: acc)
adamc@1244 1315
adamc@1244 1316 val hyps = finder (hyps, [])
adamc@1244 1317 in
adamc@1246 1318 findKeys (hyps, a :: acc)
adamc@1244 1319 end)
adamc@1244 1320 | a :: hyps => findKeys (hyps, a :: acc)
adamc@1244 1321
adamc@1244 1322 fun loop hs =
adamc@1244 1323 let
adamc@1244 1324 val hs = findKeys (hs, [])
adamc@1244 1325 in
adamc@1244 1326 if !changed then
adamc@1244 1327 (changed := false;
adamc@1244 1328 loop hs)
adamc@1244 1329 else
adamc@1244 1330 ()
adamc@1244 1331 end
adamc@1244 1332
adamc@1244 1333 val (_, hs, _) = !hyps
adamc@1244 1334 in
adamc@1246 1335 (*print "useKeys\n";*)
adamc@1244 1336 loop hs
adamc@1244 1337 end
adamc@1244 1338
adamc@1244 1339 fun complete () =
adamc@1244 1340 let
adamc@1244 1341 val (_, _, bf) = !hyps
adamc@1244 1342 in
adamc@1244 1343 if !bf then
adamc@1244 1344 ()
adamc@1244 1345 else
adamc@1244 1346 (bf := true;
adamc@1244 1347 useKeys ())
adamc@1244 1348 end
adamc@1244 1349
adamc@1244 1350 type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
adamc@1244 1351 fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
adamc@1236 1352 fun reinstate (nv, p, h) =
adamc@1236 1353 (nvar := nv;
adamc@1236 1354 path := p;
adamc@1236 1355 setHyps h)
adamc@1236 1356
adamc@1249 1357 type stashedPath = ((int * atom list) * check) option ref list
adamc@1249 1358 fun stashPath () = !path
adamc@1249 1359 fun reinstatePath p = path := p
adamc@1249 1360
adamc@1236 1361 fun nextVar () =
adamc@1236 1362 let
adamc@1236 1363 val n = !nvar
adamc@1236 1364 in
adamc@1236 1365 nvar := n + 1;
adamc@1236 1366 n
adamc@1236 1367 end
adamc@1236 1368
adamc@1236 1369 fun assert ats =
adamc@1236 1370 let
adamc@1236 1371 val n = !hnames
adamc@1244 1372 val (_, hs, _) = !hyps
adamc@1236 1373 in
adamc@1236 1374 hnames := n + 1;
adamc@1244 1375 hyps := (n, ats @ hs, ref false);
adamc@1236 1376 app (fn a => Cc.assert (db, a)) ats
adamc@1236 1377 end
adamc@1236 1378
adamc@1244 1379 fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
adamc@1236 1380
adamc@1236 1381 val sendable = ref ([] : (atom list * exp list) list)
adamc@1236 1382
adamc@1238 1383 fun checkGoals goals k =
adamc@1238 1384 let
adamc@1238 1385 fun checkGoals goals unifs =
adamc@1238 1386 case goals of
adamc@1238 1387 [] => k unifs
adamc@1238 1388 | AReln (Sql tab, [Lvar lv]) :: goals =>
adamc@1238 1389 let
adamc@1238 1390 val saved = stash ()
adamc@1244 1391 val (_, hyps, _) = !hyps
adamc@1236 1392
adamc@1238 1393 fun tryAll unifs hyps =
adamc@1238 1394 case hyps of
adamc@1238 1395 [] => false
adamc@1238 1396 | AReln (Sql tab', [e]) :: hyps =>
adamc@1238 1397 (tab' = tab andalso
adamc@1238 1398 checkGoals goals (IM.insert (unifs, lv, e)))
adamc@1238 1399 orelse tryAll unifs hyps
adamc@1238 1400 | _ :: hyps => tryAll unifs hyps
adamc@1238 1401 in
adamc@1238 1402 tryAll unifs hyps
adamc@1238 1403 end
adamc@1243 1404 | (g as AReln (r, es)) :: goals =>
adamc@1244 1405 (complete ();
adamc@1245 1406 (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
adamc@1245 1407 true
adamc@1245 1408 else
adamc@1245 1409 ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
adamc@1245 1410 false))
adamc@1244 1411 andalso checkGoals goals unifs)
adamc@1238 1412 | ACond _ :: _ => false
adamc@1238 1413 in
adamc@1238 1414 checkGoals goals IM.empty
adamc@1238 1415 end
adamc@1236 1416
adamc@1253 1417 fun buildable (e, loc) =
adamc@1238 1418 let
adamc@1238 1419 fun doPols pols acc =
adamc@1236 1420 case pols of
adamc@1253 1421 [] =>
adamc@1253 1422 let
adamc@1253 1423 val b = Cc.builtFrom (db, {Base = acc, Derived = e})
adamc@1253 1424 in
adamc@1253 1425 (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
adamc@1253 1426 ("Derived", p_exp e),
adamc@1253 1427 ("Hyps", Print.p_list p_atom (#2 (!hyps))),
adamc@1253 1428 ("Good", Print.PD.string (Bool.toString b))];*)
adamc@1253 1429 b
adamc@1253 1430 end
adamc@1236 1431 | (goals, es) :: pols =>
adamc@1238 1432 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
adamc@1238 1433 orelse doPols pols acc
adamc@1236 1434 in
adamc@1238 1435 if doPols (!sendable) [] then
adamc@1238 1436 ()
adamc@1238 1437 else
adamc@1238 1438 let
adamc@1244 1439 val (_, hs, _) = !hyps
adamc@1238 1440 in
adamc@1238 1441 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1245 1442 Print.prefaces "Situation" [("User learns", p_exp e),
adamc@1253 1443 ("Hypotheses", Print.p_list p_atom hs),
adamc@1253 1444 ("E-graph", Cc.p_database db)]
adamc@1238 1445 end
adamc@1246 1446 end
adamc@1236 1447
adamc@1236 1448 fun checkPaths () =
adamc@1236 1449 let
adamc@1244 1450 val (n, hs, _) = !hyps
adamc@1244 1451 val hs = (n, hs)
adamc@1236 1452 in
adamc@1236 1453 app (fn r =>
adamc@1236 1454 case !r of
adamc@1236 1455 NONE => ()
adamc@1236 1456 | SOME (hs, e) =>
adamc@1236 1457 (r := NONE;
adamc@1236 1458 setHyps hs;
adamc@1253 1459 buildable e)) (!path);
adamc@1236 1460 setHyps hs
adamc@1236 1461 end
adamc@1236 1462
adamc@1238 1463 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
adamc@1243 1464 ("exps", Print.p_list p_exp (#2 v))];*)
adamc@1238 1465 sendable := v :: !sendable)
adamc@1236 1466
adamc@1253 1467 fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
adamc@1253 1468 complete ();
adamc@1253 1469 checkPaths ();
adamc@1253 1470 if isKnown e then
adamc@1253 1471 ()
adamc@1253 1472 else
adamc@1253 1473 buildable (e, loc))
adamc@1236 1474
adamc@1236 1475 fun doable pols (loc : ErrorMsg.span) =
adamc@1236 1476 let
adamc@1236 1477 val pols = !pols
adamc@1236 1478 in
adamc@1244 1479 complete ();
adamc@1236 1480 if List.exists (fn goals =>
adamc@1238 1481 if checkGoals goals (fn _ => true) then
adamc@1238 1482 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
adamc@1238 1483 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
adamc@1238 1484 true)
adamc@1238 1485 else
adamc@1246 1486 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
adamc@1246 1487 ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
adamc@1238 1488 false)) pols then
adamc@1236 1489 ()
adamc@1236 1490 else
adamc@1236 1491 let
adamc@1244 1492 val (_, hs, _) = !hyps
adamc@1236 1493 in
adamc@1236 1494 ErrorMsg.errorAt loc "The database update policy may be violated here.";
adamc@1250 1495 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
adamc@1250 1496 ("E-graph", Cc.p_database db)*)]
adamc@1236 1497 end
adamc@1236 1498 end
adamc@1236 1499
adamc@1236 1500 val insertable = ref ([] : atom list list)
adamc@1236 1501 fun allowInsert v = insertable := v :: !insertable
adamc@1236 1502 val insert = doable insertable
adamc@1236 1503
adamc@1236 1504 val updatable = ref ([] : atom list list)
adamc@1236 1505 fun allowUpdate v = updatable := v :: !updatable
adamc@1236 1506 val update = doable updatable
adamc@1236 1507
adamc@1236 1508 val deletable = ref ([] : atom list list)
adamc@1236 1509 fun allowDelete v = deletable := v :: !deletable
adamc@1236 1510 val delete = doable deletable
adamc@1236 1511
adam@1281 1512 val testable = ref ([] : { table : string, field : string, known : bool } list)
adam@1281 1513 fun allowEqual v = testable := v :: !testable
adam@1280 1514 fun mayTest p =
adam@1280 1515 case p of
adam@1280 1516 Reln (Eq, [e1, e2]) =>
adam@1280 1517 let
adam@1280 1518 val (_, hs, _) = !hyps
adam@1280 1519
adam@1280 1520 fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x
adam@1280 1521 | _ => false) hs
adam@1280 1522
adam@1280 1523 fun allowed (tab, v) =
adam@1280 1524 case tab of
adam@1280 1525 Proj (Var tab, fd) =>
adam@1281 1526 List.exists (fn {table = tab', field = fd', known} =>
adam@1280 1527 fd' = fd
adam@1281 1528 andalso tableInHyps (tab', tab)
adam@1281 1529 andalso (not known orelse Cc.check (db, AReln (Known, [v])))) (!testable)
adam@1280 1530 | _ => false
adam@1280 1531 in
adam@1280 1532 if allowed (e1, e2) orelse allowed (e2, e1) then
adam@1281 1533 (assert [AReln (Eq, [e1, e2])];
adam@1280 1534 true)
adam@1280 1535 else
adam@1280 1536 false
adam@1280 1537 end
adam@1280 1538 | _ => false
adam@1280 1539
adamc@1238 1540 fun reset () = (Cc.clear db;
adamc@1238 1541 path := [];
adamc@1244 1542 hyps := (0, [], ref false);
adamc@1238 1543 nvar := 0;
adamc@1238 1544 sendable := [];
adam@1280 1545 testable := [];
adamc@1238 1546 insertable := [];
adamc@1238 1547 updatable := [];
adamc@1238 1548 deletable := [])
adamc@1238 1549
adamc@1236 1550 fun havocReln r =
adamc@1236 1551 let
adamc@1236 1552 val n = !hnames
adamc@1244 1553 val (_, hs, _) = !hyps
adamc@1236 1554 in
adamc@1236 1555 hnames := n + 1;
adamc@1244 1556 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
adamc@1236 1557 end
adamc@1236 1558
adamc@1245 1559 fun havocCookie cname =
adamc@1245 1560 let
adamc@1245 1561 val cname = "cookie/" ^ cname
adamc@1245 1562 val n = !hnames
adamc@1245 1563 val (_, hs, _) = !hyps
adamc@1245 1564 in
adamc@1245 1565 hnames := n + 1;
adamc@1245 1566 hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
adamc@1245 1567 end
adamc@1245 1568
adamc@1251 1569 fun check a = Cc.check (db, a)
adamc@1251 1570
adamc@1238 1571 fun debug () =
adamc@1238 1572 let
adamc@1244 1573 val (_, hs, _) = !hyps
adamc@1238 1574 in
adamc@1238 1575 Print.preface ("Hyps", Print.p_list p_atom hs)
adamc@1238 1576 end
adamc@1238 1577
adamc@1236 1578 end
adamc@1236 1579
adamc@1236 1580
adamc@1215 1581 fun removeDups (ls : (string * string) list) =
adamc@1211 1582 case ls of
adamc@1211 1583 [] => []
adamc@1211 1584 | x :: ls =>
adamc@1211 1585 let
adamc@1211 1586 val ls = removeDups ls
adamc@1211 1587 in
adamc@1211 1588 if List.exists (fn x' => x' = x) ls then
adamc@1211 1589 ls
adamc@1211 1590 else
adamc@1211 1591 x :: ls
adamc@1211 1592 end
adamc@1211 1593
adamc@1241 1594 fun deinj env e =
adamc@1241 1595 case #1 e of
adamc@1241 1596 ERel n => SOME (List.nth (env, n))
adamc@1241 1597 | EField (e, f) =>
adamc@1241 1598 (case deinj env e of
adamc@1241 1599 NONE => NONE
adamc@1241 1600 | SOME e => SOME (Proj (e, f)))
adamc@1251 1601 | EApp ((EFfi mf, _), e) =>
adamc@1251 1602 if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
adamc@1251 1603 NONE
adamc@1251 1604 else (case deinj env e of
adamc@1251 1605 NONE => NONE
adamc@1251 1606 | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
adamc@1241 1607 | _ => NONE
adamc@1241 1608
adamc@1220 1609 fun expIn rv env rvOf =
adamc@1220 1610 let
adamc@1236 1611 fun expIn e =
adamc@1220 1612 let
adamc@1236 1613 fun default () = inl (rv ())
adamc@1220 1614 in
adamc@1220 1615 case e of
adamc@1236 1616 SqConst p => inl (Const p)
adamc@1243 1617 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
adamc@1243 1618 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
adamc@1253 1619 | Null => inl (Func (DtCon0 "None", []))
adamc@1250 1620 | SqNot e =>
adamc@1250 1621 inr (case expIn e of
adamc@1250 1622 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
adamc@1250 1623 | inr _ => Unknown)
adamc@1236 1624 | Field (v, f) => inl (Proj (rvOf v, f))
adamc@1239 1625 | Computed _ => default ()
adamc@1220 1626 | Binop (bo, e1, e2) =>
adamc@1220 1627 let
adamc@1236 1628 val e1 = expIn e1
adamc@1236 1629 val e2 = expIn e2
adamc@1220 1630 in
adamc@1236 1631 inr (case (bo, e1, e2) of
adamc@1236 1632 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1243 1633 | (Props f, v1, v2) =>
adamc@1243 1634 let
adamc@1243 1635 fun pin v =
adamc@1243 1636 case v of
adamc@1243 1637 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
adamc@1243 1638 | inr p => p
adamc@1243 1639 in
adamc@1243 1640 f (pin v1, pin v2)
adamc@1243 1641 end
adamc@1236 1642 | _ => Unknown)
adamc@1220 1643 end
adamc@1220 1644 | SqKnown e =>
adamc@1236 1645 (case expIn e of
adamc@1236 1646 inl e => inr (Reln (Known, [e]))
adamc@1236 1647 | _ => inr Unknown)
adamc@1220 1648 | Inj e =>
adamc@1241 1649 inl (case deinj env e of
adamc@1241 1650 NONE => rv ()
adamc@1241 1651 | SOME e => e)
adamc@1220 1652 | SqFunc (f, e) =>
adamc@1236 1653 (case expIn e of
adamc@1236 1654 inl e => inl (Func (Other f, [e]))
adamc@1220 1655 | _ => default ())
adamc@1220 1656
adamc@1252 1657 | Unmodeled => inl (Func (Other "allow", [rv ()]))
adamc@1220 1658 end
adamc@1220 1659 in
adamc@1220 1660 expIn
adamc@1220 1661 end
adamc@1216 1662
adamc@1236 1663 fun decomp {Save = save, Restore = restore, Add = add} =
adamc@1216 1664 let
adamc@1236 1665 fun go p k =
adamc@1236 1666 case p of
adamc@1238 1667 True => (k () handle Cc.Contradiction => ())
adamc@1236 1668 | False => ()
adamc@1236 1669 | Unknown => ()
adamc@1236 1670 | And (p1, p2) => go p1 (fn () => go p2 k)
adamc@1236 1671 | Or (p1, p2) =>
adamc@1236 1672 let
adamc@1236 1673 val saved = save ()
adamc@1236 1674 in
adamc@1236 1675 go p1 k;
adamc@1236 1676 restore saved;
adamc@1236 1677 go p2 k
adamc@1236 1678 end
adamc@1236 1679 | Reln x => (add (AReln x); k ())
adamc@1236 1680 | Cond x => (add (ACond x); k ())
adamc@1236 1681 in
adamc@1236 1682 go
adamc@1236 1683 end
adamc@1236 1684
adamc@1236 1685 datatype queryMode =
adamc@1238 1686 SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
adamc@1236 1687 | AllCols of exp -> unit
adamc@1236 1688
adamc@1236 1689 type 'a doQuery = {
adamc@1236 1690 Env : exp list,
adamc@1236 1691 NextVar : unit -> exp,
adamc@1236 1692 Add : atom -> unit,
adamc@1236 1693 Save : unit -> 'a,
adamc@1236 1694 Restore : 'a -> unit,
adam@1280 1695 Cont : queryMode,
adam@1280 1696 Send : exp -> unit
adamc@1236 1697 }
adamc@1236 1698
adamc@1241 1699 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
adamc@1236 1700 let
adamc@1241 1701 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
adamc@1216 1702 in
adamc@1216 1703 case parse query e of
adamc@1216 1704 NONE => default ()
adamc@1227 1705 | SOME q =>
adamc@1216 1706 let
adamc@1236 1707 fun doQuery q =
adamc@1227 1708 case q of
adamc@1227 1709 Query1 r =>
adamc@1227 1710 let
adamc@1238 1711 val new = ref NONE
adamc@1238 1712 val old = ref NONE
adamc@1238 1713
adamc@1238 1714 val rvs = map (fn (tab, v) =>
adamc@1238 1715 let
adamc@1238 1716 val nv = #NextVar arg ()
adamc@1238 1717 in
adamc@1238 1718 case v of
adamc@1238 1719 "New" => new := SOME (tab, nv)
adamc@1238 1720 | "Old" => old := SOME (tab, nv)
adamc@1238 1721 | _ => ();
adamc@1238 1722 (v, nv)
adamc@1238 1723 end) (#From r)
adamc@1214 1724
adamc@1227 1725 fun rvOf v =
adamc@1227 1726 case List.find (fn (v', _) => v' = v) rvs of
adamc@1227 1727 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1227 1728 | SOME (_, e) => e
adamc@1214 1729
adamc@1236 1730 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
adamc@1236 1731
adamc@1236 1732 val saved = #Save arg ()
adamc@1236 1733 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
adamc@1236 1734
adam@1280 1735 fun leavesE e =
adamc@1227 1736 case e of
adam@1280 1737 Const _ => []
adam@1280 1738 | Var _ => []
adam@1280 1739 | Lvar _ => []
adam@1280 1740 | Func (_, es) => List.concat (map leavesE es)
adam@1280 1741 | Recd xes => List.concat (map (leavesE o #2) xes)
adam@1280 1742 | Proj _ => [e]
adam@1280 1743
adam@1280 1744 fun leavesP p =
adam@1280 1745 case p of
adam@1280 1746 True => []
adam@1280 1747 | False => []
adam@1280 1748 | Unknown => []
adam@1280 1749 | And (p1, p2) => leavesP p1 @ leavesP p2
adam@1280 1750 | Or (p1, p2) => leavesP p1 @ leavesP p2
adam@1280 1751 | Reln (_, es) => List.concat (map leavesE es)
adam@1280 1752 | Cond (e, p) => e :: leavesP p
adamc@1214 1753
adamc@1236 1754 fun normal' () =
adamc@1236 1755 case #Cont arg of
adamc@1236 1756 SomeCol k =>
adamc@1227 1757 let
adamc@1236 1758 val sis = map (fn si =>
adamc@1236 1759 case si of
adamc@1236 1760 SqField (v, f) => Proj (rvOf v, f)
adamc@1236 1761 | SqExp (e, f) =>
adamc@1236 1762 case expIn e of
adamc@1236 1763 inr _ => #NextVar arg ()
adamc@1236 1764 | inl e => e) (#Select r)
adamc@1227 1765 in
adamc@1238 1766 k {New = !new, Old = !old, Outs = sis}
adamc@1227 1767 end
adamc@1236 1768 | AllCols k =>
adamc@1227 1769 let
adamc@1236 1770 val (ts, es) =
adamc@1236 1771 foldl (fn (si, (ts, es)) =>
adamc@1227 1772 case si of
adamc@1227 1773 SqField (v, f) =>
adamc@1227 1774 let
adamc@1227 1775 val fs = getOpt (SM.find (ts, v), SM.empty)
adamc@1227 1776 in
adamc@1236 1777 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
adamc@1227 1778 end
adamc@1227 1779 | SqExp (e, f) =>
adamc@1227 1780 let
adamc@1236 1781 val e =
adamc@1236 1782 case expIn e of
adamc@1236 1783 inr _ => #NextVar arg ()
adamc@1236 1784 | inl e => e
adamc@1227 1785 in
adamc@1236 1786 (ts, SM.insert (es, f, e))
adamc@1227 1787 end)
adamc@1236 1788 (SM.empty, SM.empty) (#Select r)
adamc@1227 1789 in
adamc@1236 1790 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
adamc@1236 1791 (SM.listItemsi ts)
adamc@1236 1792 @ SM.listItemsi es))
adamc@1227 1793 end
adamc@1227 1794
adamc@1236 1795 fun doWhere final =
adamc@1236 1796 (addFrom ();
adamc@1236 1797 case #Where r of
adamc@1253 1798 NONE => final ()
adamc@1236 1799 | SOME e =>
adamc@1243 1800 let
adamc@1243 1801 val p = case expIn e of
adamc@1243 1802 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
adamc@1243 1803 | inr p => p
adamc@1243 1804
adam@1280 1805 fun getConjuncts p =
adam@1280 1806 case p of
adam@1280 1807 And (p1, p2) => getConjuncts p1 @ getConjuncts p2
adam@1280 1808 | _ => [p]
adam@1280 1809
adamc@1243 1810 val saved = #Save arg ()
adam@1280 1811
adam@1280 1812 val conjs = getConjuncts p
adam@1280 1813 val conjs = List.filter (not o St.mayTest) conjs
adamc@1243 1814 in
adam@1280 1815 app (fn p => app (#Send arg) (leavesP p)) conjs;
adamc@1243 1816 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
adamc@1253 1817 p (fn () => final () handle Cc.Contradiction => ());
adamc@1243 1818 #Restore arg saved
adamc@1243 1819 end)
adamc@1236 1820 handle Cc.Contradiction => ()
adamc@1236 1821
adamc@1236 1822 fun normal () = doWhere normal'
adamc@1227 1823 in
adamc@1236 1824 (case #Select r of
adamc@1236 1825 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1236 1826 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1236 1827 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1236 1828 (case #Cont arg of
adamc@1236 1829 SomeCol _ => ()
adamc@1236 1830 | AllCols k =>
adamc@1236 1831 let
adamc@1236 1832 fun answer e = k (Recd [(f, e)])
adamc@1236 1833
adamc@1236 1834 val saved = #Save arg ()
adamc@1238 1835 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
adamc@1238 1836 handle Cc.Contradiction => ()
adamc@1236 1837 in
adamc@1238 1838 #Restore arg saved;
adamc@1238 1839 (*print "True time!\n";*)
adamc@1236 1840 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
adamc@1236 1841 #Restore arg saved
adamc@1236 1842 end)
adamc@1236 1843 | _ => normal ())
adamc@1236 1844 | _ => normal ())
adamc@1236 1845 before #Restore arg saved
adamc@1227 1846 end
adamc@1227 1847 | Union (q1, q2) =>
adamc@1220 1848 let
adamc@1236 1849 val saved = #Save arg ()
adamc@1220 1850 in
adamc@1236 1851 doQuery q1;
adamc@1236 1852 #Restore arg saved;
adamc@1236 1853 doQuery q2;
adamc@1236 1854 #Restore arg saved
adamc@1220 1855 end
adamc@1216 1856 in
adamc@1236 1857 doQuery q
adamc@1216 1858 end
adamc@1220 1859 end
adamc@1220 1860
adamc@1211 1861 fun evalPat env e (pt, _) =
adamc@1211 1862 case pt of
adamc@1236 1863 PWild => env
adamc@1236 1864 | PVar _ => e :: env
adamc@1236 1865 | PPrim _ => env
adamc@1236 1866 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
adamc@1211 1867 | PCon (_, pc, SOME pt) =>
adamc@1211 1868 let
adamc@1236 1869 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211 1870 in
adamc@1236 1871 St.assert [AReln (PCon1 (patCon pc), [e])];
adamc@1236 1872 env
adamc@1211 1873 end
adamc@1211 1874 | PRecord xpts =>
adamc@1236 1875 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
adamc@1236 1876 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
adamc@1211 1877 | PSome (_, pt) =>
adamc@1211 1878 let
adamc@1236 1879 val env = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211 1880 in
adamc@1236 1881 St.assert [AReln (PCon1 "Some", [e])];
adamc@1236 1882 env
adamc@1211 1883 end
adamc@1211 1884
adamc@1251 1885 datatype arg_mode = Fixed | Decreasing | Arbitrary
adamc@1251 1886 type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
adamc@1251 1887 val rfuns = ref (IM.empty : rfun IM.map)
adamc@1251 1888
adamc@1236 1889 fun evalExp env (e as (_, loc)) k =
adamc@1236 1890 let
adamc@1238 1891 (*val () = St.debug ()*)
adamc@1236 1892 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
adamc@1211 1893
adamc@1236 1894 fun default () = k (Var (St.nextVar ()))
adamc@1234 1895
adamc@1234 1896 fun doFfi (m, s, es) =
adamc@1234 1897 if m = "Basis" andalso SS.member (writers, s) then
adamc@1234 1898 let
adamc@1236 1899 fun doArgs es =
adamc@1236 1900 case es of
adamc@1245 1901 [] =>
adamc@1245 1902 (if s = "set_cookie" then
adamc@1245 1903 case es of
adamc@1245 1904 [_, cname, _, _, _] =>
adamc@1245 1905 (case #1 cname of
adamc@1245 1906 EPrim (Prim.String cname) =>
adamc@1245 1907 St.havocCookie cname
adamc@1245 1908 | _ => ())
adamc@1245 1909 | _ => ()
adamc@1245 1910 else
adamc@1245 1911 ();
adamc@1245 1912 k (Recd []))
adamc@1236 1913 | e :: es =>
adamc@1253 1914 evalExp env e (fn e => (St.send (e, loc); doArgs es))
adamc@1234 1915 in
adamc@1236 1916 doArgs es
adamc@1234 1917 end
adamc@1234 1918 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1234 1919 default ()
adamc@1234 1920 else
adamc@1234 1921 let
adamc@1236 1922 fun doArgs (es, acc) =
adamc@1236 1923 case es of
adamc@1236 1924 [] => k (Func (Other (m ^ "." ^ s), rev acc))
adamc@1236 1925 | e :: es =>
adamc@1236 1926 evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1234 1927 in
adamc@1236 1928 doArgs (es, [])
adamc@1234 1929 end
adamc@1200 1930 in
adamc@1200 1931 case #1 e of
adamc@1236 1932 EPrim p => k (Const p)
adamc@1236 1933 | ERel n => k (List.nth (env, n))
adamc@1200 1934 | ENamed _ => default ()
adamc@1236 1935 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
adamc@1236 1936 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
adamc@1236 1937 | ENone _ => k (Func (DtCon0 "None", []))
adamc@1236 1938 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
adamc@1200 1939 | EFfi _ => default ()
adamc@1213 1940
adamc@1250 1941 | EFfiApp ("Basis", "rand", []) =>
adamc@1250 1942 let
adamc@1250 1943 val e = Var (St.nextVar ())
adamc@1250 1944 in
adamc@1250 1945 St.assert [AReln (Known, [e])];
adamc@1250 1946 k e
adamc@1250 1947 end
adamc@1234 1948 | EFfiApp x => doFfi x
adamc@1234 1949 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
adamc@1213 1950
adamc@1251 1951 | EApp (e1 as (EError _, _), _) => evalExp env e1 k
adamc@1251 1952
adamc@1251 1953 | EApp (e1, e2) =>
adamc@1251 1954 let
adamc@1251 1955 fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
adamc@1251 1956 Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
adamc@1251 1957 default ())
adamc@1251 1958
adamc@1251 1959 fun doArgs (e, args) =
adamc@1251 1960 case #1 e of
adamc@1251 1961 EApp (e1, e2) => doArgs (e1, e2 :: args)
adamc@1251 1962 | ENamed n =>
adamc@1251 1963 (case IM.find (!rfuns, n) of
adamc@1251 1964 NONE => adefault ()
adamc@1251 1965 | SOME rf =>
adamc@1251 1966 if length (#args rf) <> length args then
adamc@1251 1967 adefault ()
adamc@1251 1968 else
adamc@1251 1969 let
adamc@1251 1970 val () = (SS.app (St.havocReln o Sql) (#tables rf);
adamc@1251 1971 SS.app St.havocCookie (#cookies rf))
adamc@1251 1972 val saved = St.stash ()
adamc@1251 1973
adamc@1251 1974 fun doArgs (args, modes, env') =
adamc@1251 1975 case (args, modes) of
adamc@1251 1976 ([], []) => (evalExp env' (#body rf) (fn _ => ());
adamc@1251 1977 St.reinstate saved;
adamc@1251 1978 default ())
adamc@1251 1979
adamc@1251 1980 | (arg :: args, mode :: modes) =>
adamc@1251 1981 evalExp env arg (fn arg =>
adamc@1251 1982 let
adamc@1251 1983 val v = case mode of
adamc@1251 1984 Arbitrary => Var (St.nextVar ())
adamc@1251 1985 | Fixed => arg
adamc@1251 1986 | Decreasing =>
adamc@1251 1987 let
adamc@1251 1988 val v = Var (St.nextVar ())
adamc@1251 1989 in
adamc@1251 1990 if St.check (AReln (Known, [arg])) then
adamc@1251 1991 St.assert [(AReln (Known, [v]))]
adamc@1251 1992 else
adamc@1251 1993 ();
adamc@1251 1994 v
adamc@1251 1995 end
adamc@1251 1996 in
adamc@1251 1997 doArgs (args, modes, v :: env')
adamc@1251 1998 end)
adamc@1251 1999 | _ => raise Fail "Iflow.doArgs: Impossible"
adamc@1251 2000 in
adamc@1251 2001 doArgs (args, #args rf, [])
adamc@1251 2002 end)
adamc@1251 2003 | _ => adefault ()
adamc@1251 2004 in
adamc@1251 2005 doArgs (e, [])
adamc@1251 2006 end
adamc@1213 2007
adamc@1200 2008 | EAbs _ => default ()
adamc@1236 2009 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
adamc@1236 2010 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
adamc@1200 2011 | ERecord xets =>
adamc@1200 2012 let
adamc@1236 2013 fun doFields (xes, acc) =
adamc@1236 2014 case xes of
adamc@1236 2015 [] => k (Recd (rev acc))
adamc@1236 2016 | (x, e, _) :: xes =>
adamc@1236 2017 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
adamc@1200 2018 in
adamc@1236 2019 doFields (xets, [])
adamc@1200 2020 end
adamc@1236 2021 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
adamc@1218 2022 | ECase (e, pes, {result = res, ...}) =>
adamc@1236 2023 evalExp env e (fn e =>
adamc@1248 2024 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
adamc@1248 2025 | _ => false) pes then
adamc@1253 2026 (St.send (e, loc);
adamc@1248 2027 k (Recd []))
adamc@1248 2028 else
adamc@1248 2029 (St.addPath (e, loc);
adamc@1248 2030 app (fn (p, pe) =>
adamc@1248 2031 let
adamc@1248 2032 val saved = St.stash ()
adamc@1248 2033 in
adamc@1248 2034 let
adamc@1248 2035 val env = evalPat env e p
adamc@1248 2036 in
adamc@1248 2037 evalExp env pe k;
adamc@1248 2038 St.reinstate saved
adamc@1248 2039 end
adamc@1248 2040 handle Cc.Contradiction => St.reinstate saved
adamc@1248 2041 end) pes))
adamc@1200 2042 | EStrcat (e1, e2) =>
adamc@1236 2043 evalExp env e1 (fn e1 =>
adamc@1236 2044 evalExp env e2 (fn e2 =>
adamc@1236 2045 k (Func (Other "cat", [e1, e2]))))
adamc@1253 2046 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
adamc@1200 2047 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1236 2048 evalExp env b (fn b =>
adamc@1253 2049 (St.send (b, loc);
adamc@1236 2050 evalExp env m
adamc@1253 2051 (fn m => St.send (m, loc))))
adamc@1200 2052 | ERedirect (e, _) =>
adamc@1253 2053 evalExp env e (fn e => St.send (e, loc))
adamc@1200 2054 | EWrite e =>
adamc@1253 2055 evalExp env e (fn e => (St.send (e, loc);
adamc@1236 2056 k (Recd [])))
adamc@1200 2057 | ESeq (e1, e2) =>
adamc@1249 2058 let
adamc@1249 2059 val path = St.stashPath ()
adamc@1249 2060 in
adamc@1249 2061 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
adamc@1249 2062 end
adamc@1200 2063 | ELet (_, _, e1, e2) =>
adamc@1236 2064 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
adamc@1200 2065 | EClosure (n, es) =>
adamc@1200 2066 let
adamc@1236 2067 fun doArgs (es, acc) =
adamc@1236 2068 case es of
adamc@1236 2069 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
adamc@1236 2070 | e :: es =>
adamc@1236 2071 evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1200 2072 in
adamc@1236 2073 doArgs (es, [])
adamc@1200 2074 end
adamc@1200 2075
adamc@1235 2076 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
adamc@1238 2077 evalExp env i (fn i =>
adamc@1238 2078 let
adamc@1238 2079 val r = Var (St.nextVar ())
adamc@1238 2080 val acc = Var (St.nextVar ())
adamc@1242 2081
adamc@1249 2082 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
adamc@1249 2083 exp = fn (e, st as (cs, ts)) =>
adamc@1242 2084 case e of
adamc@1242 2085 EDml e =>
adamc@1242 2086 (case parse dml e of
adamc@1249 2087 NONE => st
adamc@1242 2088 | SOME c =>
adamc@1242 2089 case c of
adamc@1249 2090 Insert _ => st
adamc@1242 2091 | Delete (tab, _) =>
adamc@1249 2092 (cs, SS.add (ts, tab))
adamc@1242 2093 | Update (tab, _, _) =>
adamc@1249 2094 (cs, SS.add (ts, tab)))
adamc@1249 2095 | EFfiApp ("Basis", "set_cookie",
adamc@1249 2096 [_, (EPrim (Prim.String cname), _),
adamc@1249 2097 _, _, _]) =>
adamc@1249 2098 (SS.add (cs, cname), ts)
adamc@1249 2099 | _ => st}
adamc@1249 2100 (SS.empty, SS.empty) b
adamc@1238 2101 in
adamc@1249 2102 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
adamc@1249 2103 (TRecord [], true, true) => ()
adamc@1249 2104 | _ =>
adamc@1249 2105 let
adamc@1249 2106 val saved = St.stash ()
adamc@1249 2107 in
adamc@1249 2108 (k i)
adamc@1249 2109 handle Cc.Contradiction => ();
adamc@1249 2110 St.reinstate saved
adamc@1249 2111 end;
adamc@1249 2112
adamc@1249 2113 SS.app (St.havocReln o Sql) ts;
adamc@1249 2114 SS.app St.havocCookie cs;
adamc@1242 2115
adamc@1242 2116 doQuery {Env = env,
adamc@1242 2117 NextVar = Var o St.nextVar,
adamc@1242 2118 Add = fn a => St.assert [a],
adamc@1242 2119 Save = St.stash,
adamc@1242 2120 Restore = St.reinstate,
adam@1280 2121 Send = fn e => St.send (e, loc),
adamc@1242 2122 Cont = AllCols (fn x =>
adamc@1242 2123 (St.assert [AReln (Eq, [r, x])];
adamc@1242 2124 evalExp (acc :: r :: env) b k))} q
adamc@1238 2125 end)
adamc@1220 2126 | EDml e =>
adamc@1220 2127 (case parse dml e of
adamc@1220 2128 NONE => (print ("Warning: Information flow checker can't parse DML command at "
adamc@1220 2129 ^ ErrorMsg.spanToString loc ^ "\n");
adamc@1220 2130 default ())
adamc@1220 2131 | SOME d =>
adamc@1220 2132 case d of
adamc@1220 2133 Insert (tab, es) =>
adamc@1220 2134 let
adamc@1236 2135 val new = St.nextVar ()
adamc@1220 2136
adamc@1236 2137 val expIn = expIn (Var o St.nextVar) env
adamc@1236 2138 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
adamc@1220 2139
adamc@1236 2140 val es = map (fn (x, e) =>
adamc@1236 2141 case expIn e of
adamc@1236 2142 inl e => (x, e)
adamc@1236 2143 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
adamc@1236 2144 es
adamc@1220 2145
adamc@1236 2146 val saved = St.stash ()
adamc@1220 2147 in
adamc@1236 2148 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
adamc@1236 2149 St.insert loc;
adamc@1236 2150 St.reinstate saved;
adamc@1251 2151 St.assert [AReln (Sql tab, [Recd es])];
adamc@1236 2152 k (Recd [])
adamc@1221 2153 end
adamc@1221 2154 | Delete (tab, e) =>
adamc@1221 2155 let
adamc@1236 2156 val old = St.nextVar ()
adamc@1236 2157
adamc@1236 2158 val expIn = expIn (Var o St.nextVar) env
adamc@1236 2159 (fn "T" => Var old
adamc@1236 2160 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221 2161
adamc@1236 2162 val p = case expIn e of
adamc@1236 2163 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
adamc@1236 2164 | inr p => p
adamc@1236 2165
adamc@1236 2166 val saved = St.stash ()
adamc@1221 2167 in
adamc@1246 2168 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
adamc@1246 2169 AReln (Sql (tab), [Var old])];
adamc@1236 2170 decomp {Save = St.stash,
adamc@1236 2171 Restore = St.reinstate,
adamc@1236 2172 Add = fn a => St.assert [a]} p
adamc@1236 2173 (fn () => (St.delete loc;
adamc@1236 2174 St.reinstate saved;
adamc@1236 2175 St.havocReln (Sql tab);
adamc@1236 2176 k (Recd []))
adamc@1236 2177 handle Cc.Contradiction => ())
adamc@1223 2178 end
adamc@1223 2179 | Update (tab, fs, e) =>
adamc@1223 2180 let
adamc@1236 2181 val new = St.nextVar ()
adamc@1236 2182 val old = St.nextVar ()
adamc@1223 2183
adamc@1236 2184 val expIn = expIn (Var o St.nextVar) env
adamc@1236 2185 (fn "T" => Var old
adamc@1236 2186 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1223 2187
adamc@1236 2188 val fs = map
adamc@1236 2189 (fn (x, e) =>
adamc@1236 2190 (x, case expIn e of
adamc@1236 2191 inl e => e
adamc@1236 2192 | inr _ => raise Fail
adamc@1236 2193 ("Iflow.evalExp: Selecting "
adamc@1236 2194 ^ "boolean expression")))
adamc@1236 2195 fs
adamc@1223 2196
adamc@1226 2197 val fs' = case SM.find (!tabs, tab) of
adamc@1224 2198 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
adamc@1226 2199 | SOME (fs', _) => fs'
adamc@1224 2200
adamc@1224 2201 val fs = foldl (fn (f, fs) =>
adamc@1224 2202 if List.exists (fn (f', _) => f' = f) fs then
adamc@1224 2203 fs
adamc@1224 2204 else
adamc@1224 2205 (f, Proj (Var old, f)) :: fs) fs fs'
adamc@1224 2206
adamc@1236 2207 val p = case expIn e of
adamc@1236 2208 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
adamc@1236 2209 | inr p => p
adamc@1236 2210 val saved = St.stash ()
adamc@1223 2211 in
adamc@1236 2212 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
adamc@1246 2213 AReln (Sql (tab ^ "$Old"), [Var old]),
adamc@1246 2214 AReln (Sql tab, [Var old])];
adamc@1236 2215 decomp {Save = St.stash,
adamc@1236 2216 Restore = St.reinstate,
adamc@1236 2217 Add = fn a => St.assert [a]} p
adamc@1236 2218 (fn () => (St.update loc;
adamc@1236 2219 St.reinstate saved;
adamc@1236 2220 St.havocReln (Sql tab);
adamc@1236 2221 k (Recd []))
adamc@1236 2222 handle Cc.Contradiction => ())
adamc@1220 2223 end)
adamc@1220 2224
adamc@1229 2225 | ENextval (EPrim (Prim.String seq), _) =>
adamc@1229 2226 let
adamc@1236 2227 val nv = St.nextVar ()
adamc@1229 2228 in
adamc@1236 2229 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
adamc@1236 2230 k (Var nv)
adamc@1229 2231 end
adamc@1200 2232 | ENextval _ => default ()
adamc@1200 2233 | ESetval _ => default ()
adamc@1200 2234
adamc@1238 2235 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
adamc@1217 2236 let
adamc@1238 2237 val e = Var (St.nextVar ())
adamc@1245 2238 val e' = Func (Other ("cookie/" ^ cname), [])
adamc@1217 2239 in
adamc@1245 2240 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
adamc@1238 2241 k e
adamc@1217 2242 end
adamc@1213 2243
adamc@1200 2244 | EUnurlify _ => default ()
adamc@1200 2245 | EJavaScript _ => default ()
adamc@1200 2246 | ESignalReturn _ => default ()
adamc@1200 2247 | ESignalBind _ => default ()
adamc@1200 2248 | ESignalSource _ => default ()
adamc@1200 2249 | EServerCall _ => default ()
adamc@1200 2250 | ERecv _ => default ()
adamc@1200 2251 | ESleep _ => default ()
adamc@1200 2252 | ESpawn _ => default ()
adamc@1200 2253 end
adamc@1200 2254
adamc@1251 2255 datatype var_source = Input of int | SubInput of int | Unknown
adamc@1251 2256
adamc@1200 2257 fun check file =
adamc@1200 2258 let
adamc@1251 2259 val () = (St.reset ();
adamc@1251 2260 rfuns := IM.empty)
adamc@1236 2261
adamc@1213 2262 val file = MonoReduce.reduce file
adamc@1213 2263 val file = MonoOpt.optimize file
adamc@1213 2264 val file = Fuse.fuse file
adamc@1213 2265 val file = MonoOpt.optimize file
adamc@1216 2266 val file = MonoShake.shake file
adamc@1213 2267 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 2268
adamc@1207 2269 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 2270 case d of
adamc@1207 2271 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 2272 | _ => exptd) IS.empty file
adamc@1207 2273
adamc@1249 2274 fun decl (d, loc) =
adamc@1200 2275 case d of
adamc@1226 2276 DTable (tab, fs, pk, _) =>
adamc@1226 2277 let
adamc@1226 2278 val ks =
adamc@1226 2279 case #1 pk of
adamc@1226 2280 EPrim (Prim.String s) =>
adamc@1226 2281 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
adamc@1226 2282 [] => []
adamc@1226 2283 | pk => [pk])
adamc@1226 2284 | _ => []
adamc@1226 2285 in
adamc@1226 2286 if size tab >= 3 then
adamc@1236 2287 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
adamc@1236 2288 (map #1 fs,
adamc@1236 2289 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
adamc@1236 2290 ^ String.extract (s, 4, NONE))) ks))
adamc@1226 2291 else
adamc@1226 2292 raise Fail "Table name does not begin with uw_"
adamc@1226 2293 end
adamc@1238 2294 | DVal (x, n, _, e, _) =>
adamc@1200 2295 let
adamc@1238 2296 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
adamc@1238 2297
adamc@1207 2298 val isExptd = IS.member (exptd, n)
adamc@1207 2299
adamc@1236 2300 val saved = St.stash ()
adamc@1236 2301
adamc@1236 2302 fun deAbs (e, env, ps) =
adamc@1200 2303 case #1 e of
adamc@1236 2304 EAbs (_, _, _, e) =>
adamc@1236 2305 let
adamc@1236 2306 val nv = Var (St.nextVar ())
adamc@1236 2307 in
adamc@1236 2308 deAbs (e, nv :: env,
adamc@1236 2309 if isExptd then
adamc@1236 2310 AReln (Known, [nv]) :: ps
adamc@1236 2311 else
adamc@1236 2312 ps)
adamc@1236 2313 end
adamc@1236 2314 | _ => (e, env, ps)
adamc@1200 2315
adamc@1236 2316 val (e, env, ps) = deAbs (e, [], [])
adamc@1200 2317 in
adamc@1236 2318 St.assert ps;
adamc@1236 2319 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
adamc@1236 2320 St.reinstate saved
adamc@1200 2321 end
adamc@1202 2322
adamc@1251 2323 | DValRec [(x, n, _, e, _)] =>
adamc@1251 2324 let
adamc@1251 2325 val tables = ref SS.empty
adamc@1251 2326 val cookies = ref SS.empty
adamc@1251 2327
adamc@1251 2328 fun deAbs (e, env, modes) =
adamc@1251 2329 case #1 e of
adamc@1251 2330 EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
adamc@1251 2331 | _ => (e, env, rev modes)
adamc@1251 2332
adamc@1251 2333 val (e, env, modes) = deAbs (e, [], [])
adamc@1251 2334
adamc@1251 2335 fun doExp env (e as (_, loc)) =
adamc@1251 2336 case #1 e of
adamc@1251 2337 EPrim _ => e
adamc@1251 2338 | ERel _ => e
adamc@1251 2339 | ENamed _ => e
adamc@1251 2340 | ECon (_, _, NONE) => e
adamc@1251 2341 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
adamc@1251 2342 | ENone _ => e
adamc@1251 2343 | ESome (t, e) => (ESome (t, doExp env e), loc)
adamc@1251 2344 | EFfi _ => e
adamc@1251 2345 | EFfiApp (m, f, es) =>
adamc@1251 2346 (case (m, f, es) of
adamc@1251 2347 ("Basis", "set_cookie", [_, (EPrim (Prim.String cname), _), _, _, _]) =>
adamc@1251 2348 cookies := SS.add (!cookies, cname)
adamc@1251 2349 | _ => ();
adamc@1251 2350 (EFfiApp (m, f, map (doExp env) es), loc))
adamc@1251 2351
adamc@1251 2352 | EApp (e1, e2) =>
adamc@1251 2353 let
adamc@1251 2354 fun default () = (EApp (doExp env e1, doExp env e2), loc)
adamc@1251 2355
adamc@1251 2356 fun explore (e, args) =
adamc@1251 2357 case #1 e of
adamc@1251 2358 EApp (e1, e2) => explore (e1, e2 :: args)
adamc@1251 2359 | ENamed n' =>
adamc@1251 2360 if n' = n then
adamc@1251 2361 let
adamc@1251 2362 fun doArgs (pos, args, modes) =
adamc@1251 2363 case (args, modes) of
adamc@1251 2364 ((e1, _) :: args, m1 :: modes) =>
adamc@1251 2365 (case e1 of
adamc@1251 2366 ERel n =>
adamc@1251 2367 (case List.nth (env, n) of
adamc@1251 2368 Input pos' =>
adamc@1251 2369 if pos' = pos then
adamc@1251 2370 ()
adamc@1251 2371 else
adamc@1251 2372 m1 := Arbitrary
adamc@1251 2373 | SubInput pos' =>
adamc@1251 2374 if pos' = pos then
adamc@1251 2375 if !m1 = Arbitrary then
adamc@1251 2376 ()
adamc@1251 2377 else
adamc@1251 2378 m1 := Decreasing
adamc@1251 2379 else
adamc@1251 2380 m1 := Arbitrary
adamc@1251 2381 | Unknown => m1 := Arbitrary)
adamc@1251 2382 | _ => m1 := Arbitrary;
adamc@1251 2383 doArgs (pos + 1, args, modes))
adamc@1251 2384 | (_ :: _, []) => ()
adamc@1251 2385 | ([], ms) => app (fn m => m := Arbitrary) ms
adamc@1251 2386 in
adamc@1251 2387 doArgs (0, args, modes);
adamc@1251 2388 (EFfi ("Basis", "?"), loc)
adamc@1251 2389 end
adamc@1251 2390 else
adamc@1251 2391 default ()
adamc@1251 2392 | _ => default ()
adamc@1251 2393 in
adamc@1251 2394 explore (e, [])
adamc@1251 2395 end
adamc@1251 2396 | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
adamc@1251 2397 | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
adamc@1251 2398 | EBinop (bo, e1, e2) => (EBinop (bo, doExp env e1, doExp env e2), loc)
adamc@1251 2399 | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
adamc@1251 2400 | EField (e1, f) => (EField (doExp env e1, f), loc)
adamc@1251 2401 | ECase (e, pes, ts) =>
adamc@1251 2402 let
adamc@1251 2403 val source =
adamc@1251 2404 case #1 e of
adamc@1251 2405 ERel n =>
adamc@1251 2406 (case List.nth (env, n) of
adamc@1251 2407 Input n => SOME n
adamc@1251 2408 | SubInput n => SOME n
adamc@1251 2409 | Unknown => NONE)
adamc@1251 2410 | _ => NONE
adamc@1251 2411
adamc@1251 2412 fun doV v =
adamc@1251 2413 let
adamc@1251 2414 fun doPat (p, env) =
adamc@1251 2415 case #1 p of
adamc@1251 2416 PWild => env
adamc@1251 2417 | PVar _ => v :: env
adamc@1251 2418 | PPrim _ => env
adamc@1251 2419 | PCon (_, _, NONE) => env
adamc@1251 2420 | PCon (_, _, SOME p) => doPat (p, env)
adamc@1251 2421 | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
adamc@1251 2422 | PNone _ => env
adamc@1251 2423 | PSome (_, p) => doPat (p, env)
adamc@1251 2424 in
adamc@1251 2425 (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
adamc@1251 2426 end
adamc@1251 2427 in
adamc@1251 2428 case source of
adamc@1251 2429 NONE => doV Unknown
adamc@1251 2430 | SOME inp => doV (SubInput inp)
adamc@1251 2431 end
adamc@1251 2432 | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
adamc@1251 2433 | EError (e1, t) => (EError (doExp env e1, t), loc)
adamc@1251 2434 | EReturnBlob {blob = b, mimeType = m, t} =>
adamc@1251 2435 (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
adamc@1251 2436 | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
adamc@1251 2437 | EWrite e1 => (EWrite (doExp env e1), loc)
adamc@1251 2438 | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
adamc@1251 2439 | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
adamc@1251 2440 | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
adamc@1251 2441 | EQuery {exps, tables, state, query, body, initial} =>
adamc@1251 2442 (EQuery {exps = exps, tables = tables, state = state,
adamc@1251 2443 query = doExp env query,
adamc@1251 2444 body = doExp (Unknown :: Unknown :: env) body,
adamc@1251 2445 initial = doExp env initial}, loc)
adamc@1251 2446 | EDml e1 =>
adamc@1251 2447 (case parse dml e1 of
adamc@1251 2448 NONE => ()
adamc@1251 2449 | SOME c =>
adamc@1251 2450 case c of
adamc@1251 2451 Insert _ => ()
adamc@1251 2452 | Delete (tab, _) =>
adamc@1251 2453 tables := SS.add (!tables, tab)
adamc@1251 2454 | Update (tab, _, _) =>
adamc@1251 2455 tables := SS.add (!tables, tab);
adamc@1251 2456 (EDml (doExp env e1), loc))
adamc@1251 2457 | ENextval e1 => (ENextval (doExp env e1), loc)
adamc@1251 2458 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
adamc@1251 2459 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
adamc@1251 2460 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
adamc@1251 2461 | ESignalReturn _ => e
adamc@1251 2462 | ESignalBind _ => e
adamc@1251 2463 | ESignalSource _ => e
adamc@1251 2464 | EServerCall _ => e
adamc@1251 2465 | ERecv _ => e
adamc@1251 2466 | ESleep _ => e
adamc@1251 2467 | ESpawn _ => e
adamc@1251 2468
adamc@1251 2469 val e = doExp env e
adamc@1251 2470 in
adamc@1251 2471 rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
adamc@1251 2472 args = map (fn r => !r) modes, body = e})
adamc@1251 2473 end
adamc@1251 2474
adamc@1251 2475 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
adamc@1249 2476
adamc@1220 2477 | DPolicy pol =>
adamc@1218 2478 let
adamc@1236 2479 val rvN = ref 0
adamc@1236 2480 fun rv () =
adamc@1236 2481 let
adamc@1236 2482 val n = !rvN
adamc@1236 2483 in
adamc@1236 2484 rvN := n + 1;
adamc@1236 2485 Lvar n
adamc@1236 2486 end
adamc@1236 2487
adamc@1236 2488 val atoms = ref ([] : atom list)
adamc@1236 2489 fun doQ k = doQuery {Env = [],
adamc@1236 2490 NextVar = rv,
adamc@1236 2491 Add = fn a => atoms := a :: !atoms,
adamc@1236 2492 Save = fn () => !atoms,
adamc@1236 2493 Restore = fn ls => atoms := ls,
adam@1280 2494 Send = fn _ => (),
adamc@1238 2495 Cont = SomeCol (fn r => k (rev (!atoms), r))}
adamc@1238 2496
adamc@1247 2497 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
adamc@1247 2498 tab' <> tab
adamc@1247 2499 orelse List.all (fn Lvar lv' => lv' <> lv
adamc@1247 2500 | _ => false) nams
adamc@1247 2501 | _ => true)
adamc@1218 2502 in
adamc@1220 2503 case pol of
adamc@1220 2504 PolClient e =>
adamc@1238 2505 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
adamc@1220 2506 | PolInsert e =>
adamc@1238 2507 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
adamc@1247 2508 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
adamc@1238 2509 | _ => raise Fail "Iflow: No New in mayInsert policy") e
adamc@1221 2510 | PolDelete e =>
adamc@1238 2511 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
adamc@1247 2512 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
adamc@1238 2513 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
adamc@1223 2514 | PolUpdate e =>
adamc@1238 2515 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
adamc@1238 2516 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
adamc@1238 2517 :: AReln (Sql (tab ^ "$New"), [new])
adamc@1247 2518 :: untab (tab, [new, old]) ats)
adamc@1238 2519 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
adamc@1229 2520 | PolSequence e =>
adamc@1229 2521 (case #1 e of
adamc@1229 2522 EPrim (Prim.String seq) =>
adamc@1229 2523 let
adamc@1236 2524 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
adamc@1229 2525 val outs = [Lvar 0]
adamc@1229 2526 in
adamc@1236 2527 St.allowSend ([p], outs)
adamc@1229 2528 end
adamc@1236 2529 | _ => ())
adam@1281 2530 | PolEqual {table = tab, field = nm, known} =>
adam@1280 2531 (case #1 tab of
adam@1281 2532 EPrim (Prim.String tab) => St.allowEqual {table = String.extract (tab, 3, NONE),
adam@1281 2533 field = nm,
adam@1281 2534 known = known}
adam@1280 2535 | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
adamc@1218 2536 end
adamc@1214 2537
adamc@1236 2538 | _ => ()
adamc@1200 2539 in
adamc@1236 2540 app decl file
adamc@1200 2541 end
adamc@1200 2542
adamc@1213 2543 val check = fn file =>
adamc@1213 2544 let
adamc@1213 2545 val oldInline = Settings.getMonoInline ()
adamc@1213 2546 in
adamc@1213 2547 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 2548 NONE => 1000000
adamc@1213 2549 | SOME n => n);
adamc@1213 2550 check file;
adamc@1213 2551 Settings.setMonoInline oldInline)
adamc@1213 2552 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 2553 raise ex)
adamc@1213 2554 end
adamc@1213 2555
adamc@1200 2556 end