Mercurial > urweb

annotate src/iflow.sml @ 1876:fdafa3f92e40

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