Mercurial > urweb

annotate src/iflow.sml @ 1227:1d8fba74e7f5

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