Mercurial > urweb

annotate src/iflow.sml @ 1739:c414850f206f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add support for -boot flag, which allows in-tree execution of Ur/Web The boot flag rewrites most hardcoded paths to point to the build directory, and also forces static compilation. This is convenient for developing Ur/Web, or if you cannot 'sudo make install' Ur/Web. The following changes were made: * Header files were moved to include/urweb instead of include; this lets FFI users point their C_INCLUDE_PATH at this directory at write <urweb/urweb.h>. For internal Ur/Web executables, we simply pass -I$PATH/include/urweb as normal. * Differentiate between LIB and SRCLIB; SRCLIB is Ur and JavaScript source files, while LIB is compiled products from libtool. For in-tree compilation these live in different places. * No longer reference Config for paths; instead use Settings; these settings can be changed dynamically by Compiler.enableBoot () (TODO: add a disableBoot function.) * config.h is now generated directly in include/urweb/config.h, for consistency's sake (especially since it gets installed along with the rest of the headers!) * All of the autotools build products got updated. * The linkStatic field in protocols now only contains the name of the build product, and not the absolute path. Future users have to be careful not to reference the Settings files to early, lest they get an old version (this was the source of two bugs during development of this patch.)
author Edward Z. Yang <ezyang@mit.edu>
date Wed, 02 May 2012 17:17:57 -0400
parents cb0f05bdc183
children c1e3805e604e
rev   line source
adamc@1200 1 (* Copyright (c) 2010, Adam Chlipala
adamc@1200 2 * All rights reserved.
adamc@1200 3 *
adamc@1200 4 * Redistribution and use in source and binary forms, with or without
adamc@1200 5 * modification, are permitted provided that the following conditions are met:
adamc@1200 6 *
adamc@1200 7 * - Redistributions of source code must retain the above copyright notice,
adamc@1200 8 * this list of conditions and the following disclaimer.
adamc@1200 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200 10 * this list of conditions and the following disclaimer in the documentation
adamc@1200 11 * and/or other materials provided with the distribution.
adamc@1200 12 * - The names of contributors may not be used to endorse or promote products
adamc@1200 13 * derived from this software without specific prior written permission.
adamc@1200 14 *
adamc@1200 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@1200 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@1200 26 *)
adamc@1200 27
adamc@1200 28 structure Iflow :> IFLOW = struct
adamc@1200 29
adamc@1200 30 open Mono
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
adamc@1241 1252 fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
adamc@1216 1253 in
adamc@1216 1254 case parse query e of
adamc@1216 1255 NONE => default ()
adamc@1227 1256 | SOME q =>
adamc@1216 1257 let
adamc@1236 1258 fun doQuery q =
adamc@1227 1259 case q of
adamc@1227 1260 Query1 r =>
adamc@1227 1261 let
adamc@1238 1262 val new = ref NONE
adamc@1238 1263 val old = ref NONE
adamc@1238 1264
adamc@1238 1265 val rvs = map (fn (tab, v) =>
adamc@1238 1266 let
adamc@1238 1267 val nv = #NextVar arg ()
adamc@1238 1268 in
adamc@1238 1269 case v of
adamc@1238 1270 "New" => new := SOME (tab, nv)
adamc@1238 1271 | "Old" => old := SOME (tab, nv)
adamc@1238 1272 | _ => ();
adamc@1238 1273 (v, nv)
adamc@1238 1274 end) (#From r)
adamc@1214 1275
adamc@1227 1276 fun rvOf v =
adamc@1227 1277 case List.find (fn (v', _) => v' = v) rvs of
adamc@1227 1278 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1227 1279 | SOME (_, e) => e
adamc@1214 1280
adamc@1236 1281 val expIn = expIn (#NextVar arg) (#Env arg) rvOf
adamc@1236 1282
adamc@1236 1283 val saved = #Save arg ()
adamc@1236 1284 fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
adamc@1236 1285
adam@1282 1286 fun usedFields e =
adamc@1227 1287 case e of
adam@1282 1288 SqConst _ => []
adam@1282 1289 | SqTrue => []
adam@1282 1290 | SqFalse => []
adam@1282 1291 | Null => []
adam@1282 1292 | SqNot e => usedFields e
adam@1282 1293 | Field (v, f) => [(false, Proj (rvOf v, f))]
adam@1282 1294 | Computed _ => []
adam@1282 1295 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
adam@1282 1296 | SqKnown _ => []
adam@1282 1297 | Inj e =>
adam@1282 1298 (case deinj (#Env arg) e of
adam@1282 1299 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
adam@1282 1300 [])
adam@1282 1301 | SOME e => [(true, e)])
adam@1282 1302 | SqFunc (_, e) => usedFields e
adam@1282 1303 | Unmodeled => []
adamc@1214 1304
adamc@1236 1305 fun normal' () =
adamc@1236 1306 case #Cont arg of
adamc@1236 1307 SomeCol k =>
adamc@1227 1308 let
adamc@1236 1309 val sis = map (fn si =>
adamc@1236 1310 case si of
adamc@1236 1311 SqField (v, f) => Proj (rvOf v, f)
adamc@1236 1312 | SqExp (e, f) =>
adamc@1236 1313 case expIn e of
adamc@1236 1314 inr _ => #NextVar arg ()
adamc@1236 1315 | inl e => e) (#Select r)
adamc@1227 1316 in
adamc@1238 1317 k {New = !new, Old = !old, Outs = sis}
adamc@1227 1318 end
adamc@1236 1319 | AllCols k =>
adamc@1227 1320 let
adamc@1236 1321 val (ts, es) =
adamc@1236 1322 foldl (fn (si, (ts, es)) =>
adamc@1227 1323 case si of
adamc@1227 1324 SqField (v, f) =>
adamc@1227 1325 let
adamc@1227 1326 val fs = getOpt (SM.find (ts, v), SM.empty)
adamc@1227 1327 in
adamc@1236 1328 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
adamc@1227 1329 end
adamc@1227 1330 | SqExp (e, f) =>
adamc@1227 1331 let
adamc@1236 1332 val e =
adamc@1236 1333 case expIn e of
adamc@1236 1334 inr _ => #NextVar arg ()
adamc@1236 1335 | inl e => e
adamc@1227 1336 in
adamc@1236 1337 (ts, SM.insert (es, f, e))
adamc@1227 1338 end)
adamc@1236 1339 (SM.empty, SM.empty) (#Select r)
adamc@1227 1340 in
adamc@1236 1341 k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
adamc@1236 1342 (SM.listItemsi ts)
adamc@1236 1343 @ SM.listItemsi es))
adamc@1227 1344 end
adamc@1227 1345
adamc@1236 1346 fun doWhere final =
adamc@1236 1347 (addFrom ();
adamc@1236 1348 case #Where r of
adamc@1253 1349 NONE => final ()
adamc@1236 1350 | SOME e =>
adamc@1243 1351 let
adamc@1243 1352 val p = case expIn e of
adamc@1243 1353 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
adamc@1243 1354 | inr p => p
adamc@1243 1355
adamc@1243 1356 val saved = #Save arg ()
adamc@1243 1357 in
adamc@1243 1358 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
adamc@1253 1359 p (fn () => final () handle Cc.Contradiction => ());
adamc@1243 1360 #Restore arg saved
adamc@1243 1361 end)
adamc@1236 1362 handle Cc.Contradiction => ()
adamc@1236 1363
adamc@1236 1364 fun normal () = doWhere normal'
adamc@1227 1365 in
adamc@1236 1366 (case #Select r of
adamc@1236 1367 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1236 1368 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1236 1369 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1236 1370 (case #Cont arg of
adamc@1236 1371 SomeCol _ => ()
adamc@1236 1372 | AllCols k =>
adamc@1236 1373 let
adamc@1236 1374 fun answer e = k (Recd [(f, e)])
adamc@1236 1375
adamc@1236 1376 val saved = #Save arg ()
adamc@1238 1377 val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
adamc@1238 1378 handle Cc.Contradiction => ()
adamc@1236 1379 in
adamc@1238 1380 #Restore arg saved;
adamc@1238 1381 (*print "True time!\n";*)
adamc@1236 1382 doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
adamc@1236 1383 #Restore arg saved
adamc@1236 1384 end)
adamc@1236 1385 | _ => normal ())
adamc@1236 1386 | _ => normal ())
adamc@1236 1387 before #Restore arg saved
adamc@1227 1388 end
adamc@1227 1389 | Union (q1, q2) =>
adamc@1220 1390 let
adamc@1236 1391 val saved = #Save arg ()
adamc@1220 1392 in
adamc@1236 1393 doQuery q1;
adamc@1236 1394 #Restore arg saved;
adamc@1236 1395 doQuery q2;
adamc@1236 1396 #Restore arg saved
adamc@1220 1397 end
adamc@1216 1398 in
adamc@1236 1399 doQuery q
adamc@1216 1400 end
adamc@1220 1401 end
adamc@1220 1402
adamc@1211 1403 fun evalPat env e (pt, _) =
adamc@1211 1404 case pt of
adamc@1236 1405 PWild => env
adamc@1236 1406 | PVar _ => e :: env
adamc@1236 1407 | PPrim _ => env
adamc@1236 1408 | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
adamc@1211 1409 | PCon (_, pc, SOME pt) =>
adamc@1211 1410 let
adamc@1236 1411 val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211 1412 in
adamc@1236 1413 St.assert [AReln (PCon1 (patCon pc), [e])];
adamc@1236 1414 env
adamc@1211 1415 end
adamc@1211 1416 | PRecord xpts =>
adamc@1236 1417 foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
adamc@1236 1418 | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
adamc@1211 1419 | PSome (_, pt) =>
adamc@1211 1420 let
adamc@1236 1421 val env = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211 1422 in
adamc@1236 1423 St.assert [AReln (PCon1 "Some", [e])];
adamc@1236 1424 env
adamc@1211 1425 end
adamc@1211 1426
adamc@1251 1427 datatype arg_mode = Fixed | Decreasing | Arbitrary
adamc@1251 1428 type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
adamc@1251 1429 val rfuns = ref (IM.empty : rfun IM.map)
adamc@1251 1430
adamc@1236 1431 fun evalExp env (e as (_, loc)) k =
adamc@1236 1432 let
adamc@1238 1433 (*val () = St.debug ()*)
adamc@1236 1434 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
adamc@1211 1435
adamc@1236 1436 fun default () = k (Var (St.nextVar ()))
adamc@1234 1437
adamc@1234 1438 fun doFfi (m, s, es) =
adamc@1234 1439 if m = "Basis" andalso SS.member (writers, s) then
adamc@1234 1440 let
adamc@1236 1441 fun doArgs es =
adamc@1236 1442 case es of
adamc@1245 1443 [] =>
adamc@1245 1444 (if s = "set_cookie" then
adamc@1245 1445 case es of
adam@1663 1446 [_, (cname, _), _, _, _] =>
adamc@1245 1447 (case #1 cname of
adamc@1245 1448 EPrim (Prim.String cname) =>
adamc@1245 1449 St.havocCookie cname
adamc@1245 1450 | _ => ())
adamc@1245 1451 | _ => ()
adamc@1245 1452 else
adamc@1245 1453 ();
adamc@1245 1454 k (Recd []))
adam@1663 1455 | (e, _) :: es =>
adamc@1253 1456 evalExp env e (fn e => (St.send (e, loc); doArgs es))
adamc@1234 1457 in
adamc@1236 1458 doArgs es
adamc@1234 1459 end
adamc@1234 1460 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1234 1461 default ()
adamc@1234 1462 else
adamc@1234 1463 let
adamc@1236 1464 fun doArgs (es, acc) =
adamc@1236 1465 case es of
adamc@1236 1466 [] => k (Func (Other (m ^ "." ^ s), rev acc))
adam@1663 1467 | (e, _) :: es =>
adamc@1236 1468 evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1234 1469 in
adamc@1236 1470 doArgs (es, [])
adamc@1234 1471 end
adamc@1200 1472 in
adamc@1200 1473 case #1 e of
adamc@1236 1474 EPrim p => k (Const p)
adamc@1236 1475 | ERel n => k (List.nth (env, n))
adamc@1200 1476 | ENamed _ => default ()
adamc@1236 1477 | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
adamc@1236 1478 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
adamc@1236 1479 | ENone _ => k (Func (DtCon0 "None", []))
adamc@1236 1480 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
adamc@1200 1481 | EFfi _ => default ()
adamc@1213 1482
adamc@1250 1483 | EFfiApp ("Basis", "rand", []) =>
adamc@1250 1484 let
adamc@1250 1485 val e = Var (St.nextVar ())
adamc@1250 1486 in
adamc@1250 1487 St.assert [AReln (Known, [e])];
adamc@1250 1488 k e
adamc@1250 1489 end
adamc@1234 1490 | EFfiApp x => doFfi x
adam@1663 1491 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [(e, (TRecord [], loc))])
adamc@1213 1492
adamc@1251 1493 | EApp (e1 as (EError _, _), _) => evalExp env e1 k
adamc@1251 1494
adamc@1251 1495 | EApp (e1, e2) =>
adamc@1251 1496 let
adamc@1251 1497 fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
adamc@1251 1498 Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
adamc@1251 1499 default ())
adamc@1251 1500
adamc@1251 1501 fun doArgs (e, args) =
adamc@1251 1502 case #1 e of
adamc@1251 1503 EApp (e1, e2) => doArgs (e1, e2 :: args)
adamc@1251 1504 | ENamed n =>
adamc@1251 1505 (case IM.find (!rfuns, n) of
adamc@1251 1506 NONE => adefault ()
adamc@1251 1507 | SOME rf =>
adamc@1251 1508 if length (#args rf) <> length args then
adamc@1251 1509 adefault ()
adamc@1251 1510 else
adamc@1251 1511 let
adamc@1251 1512 val () = (SS.app (St.havocReln o Sql) (#tables rf);
adamc@1251 1513 SS.app St.havocCookie (#cookies rf))
adamc@1251 1514 val saved = St.stash ()
adamc@1251 1515
adamc@1251 1516 fun doArgs (args, modes, env') =
adamc@1251 1517 case (args, modes) of
adamc@1251 1518 ([], []) => (evalExp env' (#body rf) (fn _ => ());
adamc@1251 1519 St.reinstate saved;
adamc@1251 1520 default ())
adamc@1251 1521
adamc@1251 1522 | (arg :: args, mode :: modes) =>
adamc@1251 1523 evalExp env arg (fn arg =>
adamc@1251 1524 let
adamc@1251 1525 val v = case mode of
adamc@1251 1526 Arbitrary => Var (St.nextVar ())
adamc@1251 1527 | Fixed => arg
adamc@1251 1528 | Decreasing =>
adamc@1251 1529 let
adamc@1251 1530 val v = Var (St.nextVar ())
adamc@1251 1531 in
adamc@1251 1532 if St.check (AReln (Known, [arg])) then
adamc@1251 1533 St.assert [(AReln (Known, [v]))]
adamc@1251 1534 else
adamc@1251 1535 ();
adamc@1251 1536 v
adamc@1251 1537 end
adamc@1251 1538 in
adamc@1251 1539 doArgs (args, modes, v :: env')
adamc@1251 1540 end)
adamc@1251 1541 | _ => raise Fail "Iflow.doArgs: Impossible"
adamc@1251 1542 in
adamc@1251 1543 doArgs (args, #args rf, [])
adamc@1251 1544 end)
adamc@1251 1545 | _ => adefault ()
adamc@1251 1546 in
adamc@1251 1547 doArgs (e, [])
adamc@1251 1548 end
adamc@1213 1549
adamc@1200 1550 | EAbs _ => default ()
adamc@1236 1551 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
adam@1360 1552 | EBinop (_, s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
adamc@1200 1553 | ERecord xets =>
adamc@1200 1554 let
adamc@1236 1555 fun doFields (xes, acc) =
adamc@1236 1556 case xes of
adamc@1236 1557 [] => k (Recd (rev acc))
adamc@1236 1558 | (x, e, _) :: xes =>
adamc@1236 1559 evalExp env e (fn e => doFields (xes, (x, e) :: acc))
adamc@1200 1560 in
adamc@1236 1561 doFields (xets, [])
adamc@1200 1562 end
adamc@1236 1563 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
adamc@1218 1564 | ECase (e, pes, {result = res, ...}) =>
adamc@1236 1565 evalExp env e (fn e =>
adamc@1248 1566 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
adamc@1248 1567 | _ => false) pes then
adamc@1253 1568 (St.send (e, loc);
adamc@1248 1569 k (Recd []))
adamc@1248 1570 else
adamc@1248 1571 (St.addPath (e, loc);
adamc@1248 1572 app (fn (p, pe) =>
adamc@1248 1573 let
adamc@1248 1574 val saved = St.stash ()
adamc@1248 1575 in
adamc@1248 1576 let
adamc@1248 1577 val env = evalPat env e p
adamc@1248 1578 in
adamc@1248 1579 evalExp env pe k;
adamc@1248 1580 St.reinstate saved
adamc@1248 1581 end
adamc@1248 1582 handle Cc.Contradiction => St.reinstate saved
adamc@1248 1583 end) pes))
adamc@1200 1584 | EStrcat (e1, e2) =>
adamc@1236 1585 evalExp env e1 (fn e1 =>
adamc@1236 1586 evalExp env e2 (fn e2 =>
adamc@1236 1587 k (Func (Other "cat", [e1, e2]))))
adamc@1253 1588 | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
adamc@1200 1589 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1236 1590 evalExp env b (fn b =>
adamc@1253 1591 (St.send (b, loc);
adamc@1236 1592 evalExp env m
adamc@1253 1593 (fn m => St.send (m, loc))))
adamc@1200 1594 | ERedirect (e, _) =>
adamc@1253 1595 evalExp env e (fn e => St.send (e, loc))
adamc@1200 1596 | EWrite e =>
adamc@1253 1597 evalExp env e (fn e => (St.send (e, loc);
adamc@1236 1598 k (Recd [])))
adamc@1200 1599 | ESeq (e1, e2) =>
adamc@1249 1600 let
adamc@1249 1601 val path = St.stashPath ()
adamc@1249 1602 in
adamc@1249 1603 evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
adamc@1249 1604 end
adamc@1200 1605 | ELet (_, _, e1, e2) =>
adamc@1236 1606 evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
adamc@1200 1607 | EClosure (n, es) =>
adamc@1200 1608 let
adamc@1236 1609 fun doArgs (es, acc) =
adamc@1236 1610 case es of
adamc@1236 1611 [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
adamc@1236 1612 | e :: es =>
adamc@1236 1613 evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1200 1614 in
adamc@1236 1615 doArgs (es, [])
adamc@1200 1616 end
adamc@1200 1617
adamc@1235 1618 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
adamc@1238 1619 evalExp env i (fn i =>
adamc@1238 1620 let
adamc@1238 1621 val r = Var (St.nextVar ())
adamc@1238 1622 val acc = Var (St.nextVar ())
adamc@1242 1623
adamc@1249 1624 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
adamc@1249 1625 exp = fn (e, st as (cs, ts)) =>
adamc@1242 1626 case e of
adam@1293 1627 EDml (e, _) =>
adamc@1242 1628 (case parse dml e of
adamc@1249 1629 NONE => st
adamc@1242 1630 | SOME c =>
adamc@1242 1631 case c of
adamc@1249 1632 Insert _ => st
adamc@1242 1633 | Delete (tab, _) =>
adamc@1249 1634 (cs, SS.add (ts, tab))
adamc@1242 1635 | Update (tab, _, _) =>
adamc@1249 1636 (cs, SS.add (ts, tab)))
adamc@1249 1637 | EFfiApp ("Basis", "set_cookie",
adam@1663 1638 [_, ((EPrim (Prim.String cname), _), _),
adamc@1249 1639 _, _, _]) =>
adamc@1249 1640 (SS.add (cs, cname), ts)
adamc@1249 1641 | _ => st}
adamc@1249 1642 (SS.empty, SS.empty) b
adamc@1238 1643 in
adamc@1249 1644 case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
adamc@1249 1645 (TRecord [], true, true) => ()
adamc@1249 1646 | _ =>
adamc@1249 1647 let
adamc@1249 1648 val saved = St.stash ()
adamc@1249 1649 in
adamc@1249 1650 (k i)
adamc@1249 1651 handle Cc.Contradiction => ();
adamc@1249 1652 St.reinstate saved
adamc@1249 1653 end;
adamc@1249 1654
adamc@1249 1655 SS.app (St.havocReln o Sql) ts;
adamc@1249 1656 SS.app St.havocCookie cs;
adamc@1242 1657
adamc@1242 1658 doQuery {Env = env,
adamc@1242 1659 NextVar = Var o St.nextVar,
adamc@1242 1660 Add = fn a => St.assert [a],
adamc@1242 1661 Save = St.stash,
adamc@1242 1662 Restore = St.reinstate,
adamc@1242 1663 Cont = AllCols (fn x =>
adamc@1242 1664 (St.assert [AReln (Eq, [r, x])];
adamc@1242 1665 evalExp (acc :: r :: env) b k))} q
adamc@1238 1666 end)
adam@1293 1667 | EDml (e, _) =>
adamc@1220 1668 (case parse dml e of
adamc@1220 1669 NONE => (print ("Warning: Information flow checker can't parse DML command at "
adamc@1220 1670 ^ ErrorMsg.spanToString loc ^ "\n");
adamc@1220 1671 default ())
adamc@1220 1672 | SOME d =>
adamc@1220 1673 case d of
adamc@1220 1674 Insert (tab, es) =>
adamc@1220 1675 let
adamc@1236 1676 val new = St.nextVar ()
adamc@1220 1677
adamc@1236 1678 val expIn = expIn (Var o St.nextVar) env
adamc@1236 1679 (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
adamc@1220 1680
adamc@1236 1681 val es = map (fn (x, e) =>
adamc@1236 1682 case expIn e of
adamc@1236 1683 inl e => (x, e)
adamc@1236 1684 | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
adamc@1236 1685 es
adamc@1220 1686
adamc@1236 1687 val saved = St.stash ()
adamc@1220 1688 in
adamc@1236 1689 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
adamc@1236 1690 St.insert loc;
adamc@1236 1691 St.reinstate saved;
adamc@1251 1692 St.assert [AReln (Sql tab, [Recd es])];
adamc@1236 1693 k (Recd [])
adamc@1221 1694 end
adamc@1221 1695 | Delete (tab, e) =>
adamc@1221 1696 let
adamc@1236 1697 val old = St.nextVar ()
adamc@1236 1698
adamc@1236 1699 val expIn = expIn (Var o St.nextVar) env
adamc@1236 1700 (fn "T" => Var old
adamc@1236 1701 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221 1702
adamc@1236 1703 val p = case expIn e of
adamc@1236 1704 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
adamc@1236 1705 | inr p => p
adamc@1236 1706
adamc@1236 1707 val saved = St.stash ()
adamc@1221 1708 in
adamc@1246 1709 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
adamc@1246 1710 AReln (Sql (tab), [Var old])];
adamc@1236 1711 decomp {Save = St.stash,
adamc@1236 1712 Restore = St.reinstate,
adamc@1236 1713 Add = fn a => St.assert [a]} p
adamc@1236 1714 (fn () => (St.delete loc;
adamc@1236 1715 St.reinstate saved;
adamc@1236 1716 St.havocReln (Sql tab);
adamc@1236 1717 k (Recd []))
adamc@1236 1718 handle Cc.Contradiction => ())
adamc@1223 1719 end
adamc@1223 1720 | Update (tab, fs, e) =>
adamc@1223 1721 let
adamc@1236 1722 val new = St.nextVar ()
adamc@1236 1723 val old = St.nextVar ()
adamc@1223 1724
adamc@1236 1725 val expIn = expIn (Var o St.nextVar) env
adamc@1236 1726 (fn "T" => Var old
adamc@1236 1727 | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1223 1728
adamc@1236 1729 val fs = map
adamc@1236 1730 (fn (x, e) =>
adamc@1236 1731 (x, case expIn e of
adamc@1236 1732 inl e => e
adamc@1236 1733 | inr _ => raise Fail
adamc@1236 1734 ("Iflow.evalExp: Selecting "
adamc@1236 1735 ^ "boolean expression")))
adamc@1236 1736 fs
adamc@1223 1737
adamc@1226 1738 val fs' = case SM.find (!tabs, tab) of
adamc@1224 1739 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
adamc@1226 1740 | SOME (fs', _) => fs'
adamc@1224 1741
adamc@1224 1742 val fs = foldl (fn (f, fs) =>
adamc@1224 1743 if List.exists (fn (f', _) => f' = f) fs then
adamc@1224 1744 fs
adamc@1224 1745 else
adamc@1224 1746 (f, Proj (Var old, f)) :: fs) fs fs'
adamc@1224 1747
adamc@1236 1748 val p = case expIn e of
adamc@1236 1749 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
adamc@1236 1750 | inr p => p
adamc@1236 1751 val saved = St.stash ()
adamc@1223 1752 in
adamc@1236 1753 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
adamc@1246 1754 AReln (Sql (tab ^ "$Old"), [Var old]),
adamc@1246 1755 AReln (Sql tab, [Var old])];
adamc@1236 1756 decomp {Save = St.stash,
adamc@1236 1757 Restore = St.reinstate,
adamc@1236 1758 Add = fn a => St.assert [a]} p
adamc@1236 1759 (fn () => (St.update loc;
adamc@1236 1760 St.reinstate saved;
adamc@1236 1761 St.havocReln (Sql tab);
adamc@1236 1762 k (Recd []))
adamc@1236 1763 handle Cc.Contradiction => ())
adamc@1220 1764 end)
adamc@1220 1765
adamc@1229 1766 | ENextval (EPrim (Prim.String seq), _) =>
adamc@1229 1767 let
adamc@1236 1768 val nv = St.nextVar ()
adamc@1229 1769 in
adamc@1236 1770 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
adamc@1236 1771 k (Var nv)
adamc@1229 1772 end
adamc@1200 1773 | ENextval _ => default ()
adamc@1200 1774 | ESetval _ => default ()
adamc@1200 1775
adam@1663 1776 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String cname), _), _)]), _), _, _) =>
adamc@1217 1777 let
adamc@1238 1778 val e = Var (St.nextVar ())
adamc@1245 1779 val e' = Func (Other ("cookie/" ^ cname), [])
adamc@1217 1780 in
adamc@1245 1781 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
adamc@1238 1782 k e
adamc@1217 1783 end
adamc@1213 1784
adamc@1200 1785 | EUnurlify _ => default ()
adamc@1200 1786 | EJavaScript _ => default ()
adamc@1200 1787 | ESignalReturn _ => default ()
adamc@1200 1788 | ESignalBind _ => default ()
adamc@1200 1789 | ESignalSource _ => default ()
adamc@1200 1790 | EServerCall _ => default ()
adamc@1200 1791 | ERecv _ => default ()
adamc@1200 1792 | ESleep _ => default ()
adamc@1200 1793 | ESpawn _ => default ()
adamc@1200 1794 end
adamc@1200 1795
adamc@1251 1796 datatype var_source = Input of int | SubInput of int | Unknown
adamc@1251 1797
adamc@1200 1798 fun check file =
adamc@1200 1799 let
adamc@1251 1800 val () = (St.reset ();
adamc@1251 1801 rfuns := IM.empty)
adamc@1236 1802
adamc@1213 1803 val file = MonoReduce.reduce file
adamc@1213 1804 val file = MonoOpt.optimize file
adamc@1213 1805 val file = Fuse.fuse file
adamc@1213 1806 val file = MonoOpt.optimize file
adamc@1216 1807 val file = MonoShake.shake file
adamc@1213 1808 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 1809
adamc@1207 1810 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 1811 case d of
adamc@1207 1812 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 1813 | _ => exptd) IS.empty file
adamc@1207 1814
adamc@1249 1815 fun decl (d, loc) =
adamc@1200 1816 case d of
adamc@1226 1817 DTable (tab, fs, pk, _) =>
adamc@1226 1818 let
adamc@1226 1819 val ks =
adamc@1226 1820 case #1 pk of
adamc@1226 1821 EPrim (Prim.String s) =>
adamc@1226 1822 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
adamc@1226 1823 [] => []
adamc@1226 1824 | pk => [pk])
adamc@1226 1825 | _ => []
adamc@1226 1826 in
adamc@1226 1827 if size tab >= 3 then
adamc@1236 1828 tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
adamc@1236 1829 (map #1 fs,
adamc@1236 1830 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
adamc@1236 1831 ^ String.extract (s, 4, NONE))) ks))
adamc@1226 1832 else
adamc@1226 1833 raise Fail "Table name does not begin with uw_"
adamc@1226 1834 end
adamc@1238 1835 | DVal (x, n, _, e, _) =>
adamc@1200 1836 let
adamc@1238 1837 (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
adamc@1238 1838
adamc@1207 1839 val isExptd = IS.member (exptd, n)
adamc@1207 1840
adamc@1236 1841 val saved = St.stash ()
adamc@1236 1842
adamc@1236 1843 fun deAbs (e, env, ps) =
adamc@1200 1844 case #1 e of
adamc@1236 1845 EAbs (_, _, _, e) =>
adamc@1236 1846 let
adamc@1236 1847 val nv = Var (St.nextVar ())
adamc@1236 1848 in
adamc@1236 1849 deAbs (e, nv :: env,
adamc@1236 1850 if isExptd then
adamc@1236 1851 AReln (Known, [nv]) :: ps
adamc@1236 1852 else
adamc@1236 1853 ps)
adamc@1236 1854 end
adamc@1236 1855 | _ => (e, env, ps)
adamc@1200 1856
adamc@1236 1857 val (e, env, ps) = deAbs (e, [], [])
adamc@1200 1858 in
adamc@1236 1859 St.assert ps;
adamc@1236 1860 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
adamc@1236 1861 St.reinstate saved
adamc@1200 1862 end
adamc@1202 1863
adamc@1251 1864 | DValRec [(x, n, _, e, _)] =>
adamc@1251 1865 let
adamc@1251 1866 val tables = ref SS.empty
adamc@1251 1867 val cookies = ref SS.empty
adamc@1251 1868
adamc@1251 1869 fun deAbs (e, env, modes) =
adamc@1251 1870 case #1 e of
adamc@1251 1871 EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
adamc@1251 1872 | _ => (e, env, rev modes)
adamc@1251 1873
adamc@1251 1874 val (e, env, modes) = deAbs (e, [], [])
adamc@1251 1875
adamc@1251 1876 fun doExp env (e as (_, loc)) =
adamc@1251 1877 case #1 e of
adamc@1251 1878 EPrim _ => e
adamc@1251 1879 | ERel _ => e
adamc@1251 1880 | ENamed _ => e
adamc@1251 1881 | ECon (_, _, NONE) => e
adamc@1251 1882 | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
adamc@1251 1883 | ENone _ => e
adamc@1251 1884 | ESome (t, e) => (ESome (t, doExp env e), loc)
adamc@1251 1885 | EFfi _ => e
adamc@1251 1886 | EFfiApp (m, f, es) =>
adamc@1251 1887 (case (m, f, es) of
adam@1663 1888 ("Basis", "set_cookie", [_, ((EPrim (Prim.String cname), _), _), _, _, _]) =>
adamc@1251 1889 cookies := SS.add (!cookies, cname)
adamc@1251 1890 | _ => ();
adam@1663 1891 (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc))
adamc@1251 1892
adamc@1251 1893 | EApp (e1, e2) =>
adamc@1251 1894 let
adamc@1251 1895 fun default () = (EApp (doExp env e1, doExp env e2), loc)
adamc@1251 1896
adamc@1251 1897 fun explore (e, args) =
adamc@1251 1898 case #1 e of
adamc@1251 1899 EApp (e1, e2) => explore (e1, e2 :: args)
adamc@1251 1900 | ENamed n' =>
adamc@1251 1901 if n' = n then
adamc@1251 1902 let
adamc@1251 1903 fun doArgs (pos, args, modes) =
adamc@1251 1904 case (args, modes) of
adamc@1251 1905 ((e1, _) :: args, m1 :: modes) =>
adamc@1251 1906 (case e1 of
adamc@1251 1907 ERel n =>
adamc@1251 1908 (case List.nth (env, n) of
adamc@1251 1909 Input pos' =>
adamc@1251 1910 if pos' = pos then
adamc@1251 1911 ()
adamc@1251 1912 else
adamc@1251 1913 m1 := Arbitrary
adamc@1251 1914 | SubInput pos' =>
adamc@1251 1915 if pos' = pos then
adamc@1251 1916 if !m1 = Arbitrary then
adamc@1251 1917 ()
adamc@1251 1918 else
adamc@1251 1919 m1 := Decreasing
adamc@1251 1920 else
adamc@1251 1921 m1 := Arbitrary
adamc@1251 1922 | Unknown => m1 := Arbitrary)
adamc@1251 1923 | _ => m1 := Arbitrary;
adamc@1251 1924 doArgs (pos + 1, args, modes))
adamc@1251 1925 | (_ :: _, []) => ()
adamc@1251 1926 | ([], ms) => app (fn m => m := Arbitrary) ms
adamc@1251 1927 in
adamc@1251 1928 doArgs (0, args, modes);
adamc@1251 1929 (EFfi ("Basis", "?"), loc)
adamc@1251 1930 end
adamc@1251 1931 else
adamc@1251 1932 default ()
adamc@1251 1933 | _ => default ()
adamc@1251 1934 in
adamc@1251 1935 explore (e, [])
adamc@1251 1936 end
adamc@1251 1937 | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
adamc@1251 1938 | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
adam@1360 1939 | EBinop (bi, bo, e1, e2) => (EBinop (bi, bo, doExp env e1, doExp env e2), loc)
adamc@1251 1940 | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
adamc@1251 1941 | EField (e1, f) => (EField (doExp env e1, f), loc)
adamc@1251 1942 | ECase (e, pes, ts) =>
adamc@1251 1943 let
adamc@1251 1944 val source =
adamc@1251 1945 case #1 e of
adamc@1251 1946 ERel n =>
adamc@1251 1947 (case List.nth (env, n) of
adamc@1251 1948 Input n => SOME n
adamc@1251 1949 | SubInput n => SOME n
adamc@1251 1950 | Unknown => NONE)
adamc@1251 1951 | _ => NONE
adamc@1251 1952
adamc@1251 1953 fun doV v =
adamc@1251 1954 let
adamc@1251 1955 fun doPat (p, env) =
adamc@1251 1956 case #1 p of
adamc@1251 1957 PWild => env
adamc@1251 1958 | PVar _ => v :: env
adamc@1251 1959 | PPrim _ => env
adamc@1251 1960 | PCon (_, _, NONE) => env
adamc@1251 1961 | PCon (_, _, SOME p) => doPat (p, env)
adamc@1251 1962 | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
adamc@1251 1963 | PNone _ => env
adamc@1251 1964 | PSome (_, p) => doPat (p, env)
adamc@1251 1965 in
adamc@1251 1966 (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
adamc@1251 1967 end
adamc@1251 1968 in
adamc@1251 1969 case source of
adamc@1251 1970 NONE => doV Unknown
adamc@1251 1971 | SOME inp => doV (SubInput inp)
adamc@1251 1972 end
adamc@1251 1973 | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
adamc@1251 1974 | EError (e1, t) => (EError (doExp env e1, t), loc)
adamc@1251 1975 | EReturnBlob {blob = b, mimeType = m, t} =>
adamc@1251 1976 (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
adamc@1251 1977 | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
adamc@1251 1978 | EWrite e1 => (EWrite (doExp env e1), loc)
adamc@1251 1979 | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
adamc@1251 1980 | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
adamc@1251 1981 | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
adamc@1251 1982 | EQuery {exps, tables, state, query, body, initial} =>
adamc@1251 1983 (EQuery {exps = exps, tables = tables, state = state,
adamc@1251 1984 query = doExp env query,
adamc@1251 1985 body = doExp (Unknown :: Unknown :: env) body,
adamc@1251 1986 initial = doExp env initial}, loc)
adam@1293 1987 | EDml (e1, mode) =>
adamc@1251 1988 (case parse dml e1 of
adamc@1251 1989 NONE => ()
adamc@1251 1990 | SOME c =>
adamc@1251 1991 case c of
adamc@1251 1992 Insert _ => ()
adamc@1251 1993 | Delete (tab, _) =>
adamc@1251 1994 tables := SS.add (!tables, tab)
adamc@1251 1995 | Update (tab, _, _) =>
adamc@1251 1996 tables := SS.add (!tables, tab);
adam@1293 1997 (EDml (doExp env e1, mode), loc))
adamc@1251 1998 | ENextval e1 => (ENextval (doExp env e1), loc)
adamc@1251 1999 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
adamc@1251 2000 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
adamc@1251 2001 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
adamc@1251 2002 | ESignalReturn _ => e
adamc@1251 2003 | ESignalBind _ => e
adamc@1251 2004 | ESignalSource _ => e
adamc@1251 2005 | EServerCall _ => e
adamc@1251 2006 | ERecv _ => e
adamc@1251 2007 | ESleep _ => e
adamc@1251 2008 | ESpawn _ => e
adamc@1251 2009
adamc@1251 2010 val e = doExp env e
adamc@1251 2011 in
adamc@1251 2012 rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
adamc@1251 2013 args = map (fn r => !r) modes, body = e})
adamc@1251 2014 end
adamc@1251 2015
adamc@1251 2016 | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
adamc@1249 2017
adamc@1220 2018 | DPolicy pol =>
adamc@1218 2019 let
adamc@1236 2020 val rvN = ref 0
adamc@1236 2021 fun rv () =
adamc@1236 2022 let
adamc@1236 2023 val n = !rvN
adamc@1236 2024 in
adamc@1236 2025 rvN := n + 1;
adamc@1236 2026 Lvar n
adamc@1236 2027 end
adamc@1236 2028
adamc@1236 2029 val atoms = ref ([] : atom list)
adamc@1236 2030 fun doQ k = doQuery {Env = [],
adamc@1236 2031 NextVar = rv,
adamc@1236 2032 Add = fn a => atoms := a :: !atoms,
adamc@1236 2033 Save = fn () => !atoms,
adamc@1236 2034 Restore = fn ls => atoms := ls,
adamc@1238 2035 Cont = SomeCol (fn r => k (rev (!atoms), r))}
adamc@1238 2036
adamc@1247 2037 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
adamc@1247 2038 tab' <> tab
adamc@1247 2039 orelse List.all (fn Lvar lv' => lv' <> lv
adamc@1247 2040 | _ => false) nams
adamc@1247 2041 | _ => true)
adamc@1218 2042 in
adamc@1220 2043 case pol of
adamc@1220 2044 PolClient e =>
adamc@1238 2045 doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
adamc@1220 2046 | PolInsert e =>
adamc@1238 2047 doQ (fn (ats, {New = SOME (tab, new), ...}) =>
adamc@1247 2048 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
adamc@1238 2049 | _ => raise Fail "Iflow: No New in mayInsert policy") e
adamc@1221 2050 | PolDelete e =>
adamc@1238 2051 doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
adamc@1247 2052 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
adamc@1238 2053 | _ => raise Fail "Iflow: No Old in mayDelete policy") e
adamc@1223 2054 | PolUpdate e =>
adamc@1238 2055 doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
adamc@1238 2056 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
adamc@1238 2057 :: AReln (Sql (tab ^ "$New"), [new])
adamc@1247 2058 :: untab (tab, [new, old]) ats)
adamc@1238 2059 | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
adamc@1229 2060 | PolSequence e =>
adamc@1229 2061 (case #1 e of
adamc@1229 2062 EPrim (Prim.String seq) =>
adamc@1229 2063 let
adamc@1236 2064 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
adamc@1229 2065 val outs = [Lvar 0]
adamc@1229 2066 in
adamc@1236 2067 St.allowSend ([p], outs)
adamc@1229 2068 end
adamc@1236 2069 | _ => ())
adamc@1218 2070 end
adamc@1214 2071
adamc@1236 2072 | _ => ()
adamc@1200 2073 in
adamc@1236 2074 app decl file
adamc@1200 2075 end
adamc@1200 2076
adamc@1213 2077 val check = fn file =>
adamc@1213 2078 let
adamc@1213 2079 val oldInline = Settings.getMonoInline ()
adamc@1213 2080 in
adamc@1213 2081 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 2082 NONE => 1000000
adamc@1213 2083 | SOME n => n);
adamc@1213 2084 check file;
adamc@1213 2085 Settings.setMonoInline oldInline)
adamc@1213 2086 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 2087 raise ex)
adamc@1213 2088 end
adamc@1213 2089
adamc@1200 2090 end