Mercurial > urweb

annotate src/iflow.sml @ 1866:9fc086e3c95a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add hex SQL syntax for blobs, such as X'0ABC12343'. Works with sqlite.
author Sergey Mironov <grrwlf@gmail.com>
date Fri, 13 Sep 2013 10:09:15 -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