Mercurial > urweb

annotate src/iflow.sml @ 1214:648e6b087dfb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change query_policy to sendClient; all arguments passed to SQL predicates are variables
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Apr 2010 09:57:37 -0400
parents e791d93d4616
children 360f1ed0a969
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@1200 35 structure SS = BinarySetFn(struct
adamc@1200 36 type ord_key = string
adamc@1200 37 val compare = String.compare
adamc@1200 38 end)
adamc@1200 39
adamc@1200 40 val writers = ["htmlifyInt_w",
adamc@1200 41 "htmlifyFloat_w",
adamc@1200 42 "htmlifyString_w",
adamc@1200 43 "htmlifyBool_w",
adamc@1200 44 "htmlifyTime_w",
adamc@1200 45 "attrifyInt_w",
adamc@1200 46 "attrifyFloat_w",
adamc@1200 47 "attrifyString_w",
adamc@1200 48 "attrifyChar_w",
adamc@1200 49 "urlifyInt_w",
adamc@1200 50 "urlifyFloat_w",
adamc@1200 51 "urlifyString_w",
adamc@1213 52 "urlifyBool_w",
adamc@1213 53 "set_cookie"]
adamc@1200 54
adamc@1200 55 val writers = SS.addList (SS.empty, writers)
adamc@1200 56
adamc@1200 57 type lvar = int
adamc@1200 58
adamc@1200 59 datatype exp =
adamc@1200 60 Const of Prim.t
adamc@1200 61 | Var of int
adamc@1200 62 | Lvar of lvar
adamc@1200 63 | Func of string * exp list
adamc@1200 64 | Recd of (string * exp) list
adamc@1200 65 | Proj of exp * string
adamc@1200 66 | Finish
adamc@1200 67
adamc@1200 68 datatype reln =
adamc@1207 69 Known
adamc@1207 70 | Sql of string
adamc@1211 71 | DtCon of string
adamc@1200 72 | Eq
adamc@1210 73 | Ne
adamc@1210 74 | Lt
adamc@1210 75 | Le
adamc@1210 76 | Gt
adamc@1210 77 | Ge
adamc@1200 78
adamc@1200 79 datatype prop =
adamc@1200 80 True
adamc@1200 81 | False
adamc@1200 82 | Unknown
adamc@1200 83 | And of prop * prop
adamc@1200 84 | Or of prop * prop
adamc@1200 85 | Reln of reln * exp list
adamc@1212 86 | Cond of exp * prop
adamc@1200 87
adamc@1200 88 local
adamc@1207 89 open Print
adamc@1207 90 val string = PD.string
adamc@1207 91 in
adamc@1207 92
adamc@1207 93 fun p_exp e =
adamc@1207 94 case e of
adamc@1207 95 Const p => Prim.p_t p
adamc@1207 96 | Var n => string ("x" ^ Int.toString n)
adamc@1207 97 | Lvar n => string ("X" ^ Int.toString n)
adamc@1207 98 | Func (f, es) => box [string (f ^ "("),
adamc@1207 99 p_list p_exp es,
adamc@1207 100 string ")"]
adamc@1207 101 | Recd xes => box [string "{",
adamc@1210 102 p_list (fn (x, e) => box [string x,
adamc@1207 103 space,
adamc@1207 104 string "=",
adamc@1207 105 space,
adamc@1207 106 p_exp e]) xes,
adamc@1207 107 string "}"]
adamc@1207 108 | Proj (e, x) => box [p_exp e,
adamc@1207 109 string ("." ^ x)]
adamc@1207 110 | Finish => string "FINISH"
adamc@1207 111
adamc@1210 112 fun p_bop s es =
adamc@1210 113 case es of
adamc@1210 114 [e1, e2] => box [p_exp e1,
adamc@1210 115 space,
adamc@1210 116 string s,
adamc@1210 117 space,
adamc@1210 118 p_exp e2]
adamc@1210 119 | _ => raise Fail "Iflow.p_bop"
adamc@1210 120
adamc@1207 121 fun p_reln r es =
adamc@1207 122 case r of
adamc@1207 123 Known =>
adamc@1207 124 (case es of
adamc@1207 125 [e] => box [string "known(",
adamc@1207 126 p_exp e,
adamc@1207 127 string ")"]
adamc@1207 128 | _ => raise Fail "Iflow.p_reln: Known")
adamc@1207 129 | Sql s => box [string (s ^ "("),
adamc@1207 130 p_list p_exp es,
adamc@1207 131 string ")"]
adamc@1211 132 | DtCon s => box [string (s ^ "("),
adamc@1211 133 p_list p_exp es,
adamc@1211 134 string ")"]
adamc@1210 135 | Eq => p_bop "=" es
adamc@1210 136 | Ne => p_bop "<>" es
adamc@1210 137 | Lt => p_bop "<" es
adamc@1210 138 | Le => p_bop "<=" es
adamc@1210 139 | Gt => p_bop ">" es
adamc@1210 140 | Ge => p_bop ">=" es
adamc@1207 141
adamc@1207 142 fun p_prop p =
adamc@1207 143 case p of
adamc@1207 144 True => string "True"
adamc@1207 145 | False => string "False"
adamc@1207 146 | Unknown => string "??"
adamc@1207 147 | And (p1, p2) => box [string "(",
adamc@1207 148 p_prop p1,
adamc@1207 149 string ")",
adamc@1207 150 space,
adamc@1207 151 string "&&",
adamc@1207 152 space,
adamc@1207 153 string "(",
adamc@1207 154 p_prop p2,
adamc@1207 155 string ")"]
adamc@1207 156 | Or (p1, p2) => box [string "(",
adamc@1207 157 p_prop p1,
adamc@1207 158 string ")",
adamc@1207 159 space,
adamc@1207 160 string "||",
adamc@1207 161 space,
adamc@1207 162 string "(",
adamc@1207 163 p_prop p2,
adamc@1207 164 string ")"]
adamc@1207 165 | Reln (r, es) => p_reln r es
adamc@1212 166 | Cond (e, p) => box [string "(",
adamc@1212 167 p_exp e,
adamc@1212 168 space,
adamc@1212 169 string "==",
adamc@1212 170 space,
adamc@1212 171 p_prop p,
adamc@1212 172 string ")"]
adamc@1207 173
adamc@1207 174 end
adamc@1207 175
adamc@1207 176 local
adamc@1202 177 val count = ref 1
adamc@1200 178 in
adamc@1200 179 fun newLvar () =
adamc@1200 180 let
adamc@1200 181 val n = !count
adamc@1200 182 in
adamc@1200 183 count := n + 1;
adamc@1200 184 n
adamc@1200 185 end
adamc@1200 186 end
adamc@1200 187
adamc@1200 188 fun isKnown e =
adamc@1200 189 case e of
adamc@1200 190 Const _ => true
adamc@1200 191 | Func (_, es) => List.all isKnown es
adamc@1200 192 | Recd xes => List.all (isKnown o #2) xes
adamc@1200 193 | Proj (e, _) => isKnown e
adamc@1200 194 | _ => false
adamc@1200 195
adamc@1200 196 fun isFinish e =
adamc@1200 197 case e of
adamc@1200 198 Finish => true
adamc@1200 199 | _ => false
adamc@1200 200
adamc@1208 201 val unif = ref (IM.empty : exp IM.map)
adamc@1208 202
adamc@1208 203 fun reset () = unif := IM.empty
adamc@1208 204 fun save () = !unif
adamc@1208 205 fun restore x = unif := x
adamc@1208 206
adamc@1200 207 fun simplify e =
adamc@1200 208 case e of
adamc@1200 209 Const _ => e
adamc@1200 210 | Var _ => e
adamc@1208 211 | Lvar n =>
adamc@1208 212 (case IM.find (!unif, n) of
adamc@1208 213 NONE => e
adamc@1208 214 | SOME e => simplify e)
adamc@1200 215 | Func (f, es) =>
adamc@1200 216 let
adamc@1200 217 val es = map simplify es
adamc@1211 218
adamc@1211 219 fun default () = Func (f, es)
adamc@1200 220 in
adamc@1200 221 if List.exists isFinish es then
adamc@1200 222 Finish
adamc@1211 223 else if String.isPrefix "un" f then
adamc@1211 224 case es of
adamc@1211 225 [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then
adamc@1211 226 e
adamc@1211 227 else
adamc@1211 228 default ()
adamc@1211 229 | _ => default ()
adamc@1200 230 else
adamc@1211 231 default ()
adamc@1200 232 end
adamc@1200 233 | Recd xes =>
adamc@1200 234 let
adamc@1200 235 val xes = map (fn (x, e) => (x, simplify e)) xes
adamc@1200 236 in
adamc@1200 237 if List.exists (isFinish o #2) xes then
adamc@1200 238 Finish
adamc@1200 239 else
adamc@1200 240 Recd xes
adamc@1200 241 end
adamc@1200 242 | Proj (e, s) =>
adamc@1200 243 (case simplify e of
adamc@1200 244 Recd xes =>
adamc@1200 245 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
adamc@1200 246 | e' =>
adamc@1200 247 if isFinish e' then
adamc@1200 248 Finish
adamc@1200 249 else
adamc@1200 250 Proj (e', s))
adamc@1200 251 | Finish => Finish
adamc@1200 252
adamc@1212 253 datatype atom =
adamc@1212 254 AReln of reln * exp list
adamc@1212 255 | ACond of exp * prop
adamc@1212 256
adamc@1212 257 fun p_atom a =
adamc@1212 258 p_prop (case a of
adamc@1212 259 AReln x => Reln x
adamc@1212 260 | ACond x => Cond x)
adamc@1212 261
adamc@1202 262 fun decomp fals or =
adamc@1200 263 let
adamc@1200 264 fun decomp p k =
adamc@1200 265 case p of
adamc@1200 266 True => k []
adamc@1202 267 | False => fals
adamc@1200 268 | Unknown => k []
adamc@1200 269 | And (p1, p2) =>
adamc@1200 270 decomp p1 (fn ps1 =>
adamc@1200 271 decomp p2 (fn ps2 =>
adamc@1200 272 k (ps1 @ ps2)))
adamc@1200 273 | Or (p1, p2) =>
adamc@1200 274 or (decomp p1 k, fn () => decomp p2 k)
adamc@1212 275 | Reln x => k [AReln x]
adamc@1212 276 | Cond x => k [ACond x]
adamc@1200 277 in
adamc@1200 278 decomp
adamc@1200 279 end
adamc@1200 280
adamc@1202 281 fun lvarIn lv =
adamc@1202 282 let
adamc@1202 283 fun lvi e =
adamc@1202 284 case e of
adamc@1202 285 Const _ => false
adamc@1202 286 | Var _ => false
adamc@1202 287 | Lvar lv' => lv' = lv
adamc@1202 288 | Func (_, es) => List.exists lvi es
adamc@1202 289 | Recd xes => List.exists (lvi o #2) xes
adamc@1202 290 | Proj (e, _) => lvi e
adamc@1202 291 | Finish => false
adamc@1202 292 in
adamc@1202 293 lvi
adamc@1202 294 end
adamc@1202 295
adamc@1212 296 fun lvarInP lv =
adamc@1212 297 let
adamc@1212 298 fun lvi p =
adamc@1212 299 case p of
adamc@1212 300 True => false
adamc@1212 301 | False => false
adamc@1212 302 | Unknown => true
adamc@1212 303 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 304 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 305 | Reln (_, es) => List.exists (lvarIn lv) es
adamc@1212 306 | Cond (e, p) => lvarIn lv e orelse lvi p
adamc@1212 307 in
adamc@1212 308 lvi
adamc@1212 309 end
adamc@1212 310
adamc@1212 311 fun varIn lv =
adamc@1212 312 let
adamc@1212 313 fun lvi e =
adamc@1212 314 case e of
adamc@1212 315 Const _ => false
adamc@1212 316 | Lvar _ => false
adamc@1212 317 | Var lv' => lv' = lv
adamc@1212 318 | Func (_, es) => List.exists lvi es
adamc@1212 319 | Recd xes => List.exists (lvi o #2) xes
adamc@1212 320 | Proj (e, _) => lvi e
adamc@1212 321 | Finish => false
adamc@1212 322 in
adamc@1212 323 lvi
adamc@1212 324 end
adamc@1212 325
adamc@1212 326 fun varInP lv =
adamc@1212 327 let
adamc@1212 328 fun lvi p =
adamc@1212 329 case p of
adamc@1212 330 True => false
adamc@1212 331 | False => false
adamc@1212 332 | Unknown => false
adamc@1212 333 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 334 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 335 | Reln (_, es) => List.exists (varIn lv) es
adamc@1212 336 | Cond (e, p) => varIn lv e orelse lvi p
adamc@1212 337 in
adamc@1212 338 lvi
adamc@1212 339 end
adamc@1212 340
adamc@1202 341 fun eq' (e1, e2) =
adamc@1202 342 case (e1, e2) of
adamc@1202 343 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202 344 | (Var n1, Var n2) => n1 = n2
adamc@1202 345
adamc@1202 346 | (Lvar n1, _) =>
adamc@1202 347 (case IM.find (!unif, n1) of
adamc@1202 348 SOME e1 => eq' (e1, e2)
adamc@1202 349 | NONE =>
adamc@1202 350 case e2 of
adamc@1202 351 Lvar n2 =>
adamc@1202 352 (case IM.find (!unif, n2) of
adamc@1202 353 SOME e2 => eq' (e1, e2)
adamc@1202 354 | NONE => n1 = n2
adamc@1208 355 orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202 356 true))
adamc@1202 357 | _ =>
adamc@1202 358 if lvarIn n1 e2 then
adamc@1202 359 false
adamc@1202 360 else
adamc@1202 361 (unif := IM.insert (!unif, n1, e2);
adamc@1202 362 true))
adamc@1202 363
adamc@1202 364 | (_, Lvar n2) =>
adamc@1202 365 (case IM.find (!unif, n2) of
adamc@1202 366 SOME e2 => eq' (e1, e2)
adamc@1202 367 | NONE =>
adamc@1202 368 if lvarIn n2 e1 then
adamc@1202 369 false
adamc@1202 370 else
adamc@1213 371 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
adamc@1213 372 ("e1", p_exp e1)];*)
adamc@1213 373 unif := IM.insert (!unif, n2, e1);
adamc@1202 374 true))
adamc@1202 375
adamc@1202 376 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202 377 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202 378 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202 379 | (Finish, Finish) => true
adamc@1202 380 | _ => false
adamc@1202 381
adamc@1202 382 fun eq (e1, e2) =
adamc@1202 383 let
adamc@1203 384 val saved = save ()
adamc@1202 385 in
adamc@1202 386 if eq' (simplify e1, simplify e2) then
adamc@1202 387 true
adamc@1202 388 else
adamc@1203 389 (restore saved;
adamc@1202 390 false)
adamc@1202 391 end
adamc@1202 392
adamc@1208 393 val debug = ref false
adamc@1208 394
adamc@1211 395 fun eeq (e1, e2) =
adamc@1211 396 case (e1, e2) of
adamc@1211 397 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211 398 | (Var n1, Var n2) => n1 = n2
adamc@1211 399 | (Lvar n1, Lvar n2) => n1 = n2
adamc@1211 400 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211 401 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211 402 List.all (fn (x2, e2) =>
adamc@1211 403 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211 404 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211 405 | (Finish, Finish) => true
adamc@1211 406 | _ => false
adamc@1211 407
adamc@1208 408 (* Congruence closure *)
adamc@1208 409 structure Cc :> sig
adamc@1208 410 type t
adamc@1208 411 val empty : t
adamc@1208 412 val assert : t * exp * exp -> t
adamc@1208 413 val query : t * exp * exp -> bool
adamc@1208 414 val allPeers : t * exp -> exp list
adamc@1214 415 val p_t : t Print.printer
adamc@1208 416 end = struct
adamc@1208 417
adamc@1211 418 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
adamc@1208 419
adamc@1208 420 type t = (exp * exp) list
adamc@1208 421
adamc@1208 422 val empty = []
adamc@1208 423
adamc@1208 424 fun lookup (t, e) =
adamc@1208 425 case List.find (fn (e', _) => eq (e', e)) t of
adamc@1208 426 NONE => e
adamc@1208 427 | SOME (_, e2) => lookup (t, e2)
adamc@1208 428
adamc@1208 429 fun allPeers (t, e) =
adamc@1208 430 let
adamc@1208 431 val r = lookup (t, e)
adamc@1208 432 in
adamc@1208 433 r :: List.mapPartial (fn (e1, e2) =>
adamc@1208 434 let
adamc@1208 435 val r' = lookup (t, e2)
adamc@1208 436 in
adamc@1208 437 if eq (r, r') then
adamc@1208 438 SOME e1
adamc@1208 439 else
adamc@1208 440 NONE
adamc@1208 441 end) t
adamc@1208 442 end
adamc@1208 443
adamc@1214 444 open Print
adamc@1214 445
adamc@1214 446 val p_t = p_list (fn (e1, e2) => box [p_exp (simplify e1),
adamc@1214 447 space,
adamc@1214 448 PD.string "->",
adamc@1214 449 space,
adamc@1214 450 p_exp (simplify e2)])
adamc@1214 451
adamc@1214 452 fun query (t, e1, e2) =
adamc@1214 453 let
adamc@1214 454 fun doUn e =
adamc@1214 455 case e of
adamc@1214 456 Func (f, [e1]) =>
adamc@1214 457 if String.isPrefix "un" f then
adamc@1214 458 let
adamc@1214 459 val s = String.extract (f, 2, NONE)
adamc@1214 460 in
adamc@1214 461 case ListUtil.search (fn e =>
adamc@1214 462 case e of
adamc@1214 463 Func (f', [e']) =>
adamc@1214 464 if f' = s then
adamc@1214 465 SOME e'
adamc@1214 466 else
adamc@1214 467 NONE
adamc@1214 468 | _ => NONE) (allPeers (t, e1)) of
adamc@1214 469 NONE => e
adamc@1214 470 | SOME e => doUn e
adamc@1214 471 end
adamc@1214 472 else
adamc@1214 473 e
adamc@1214 474 | _ => e
adamc@1214 475
adamc@1214 476 val e1' = doUn (lookup (t, doUn (simplify e1)))
adamc@1214 477 val e2' = doUn (lookup (t, doUn (simplify e2)))
adamc@1214 478 in
adamc@1214 479 (*prefaces "CC query" [("e1", p_exp (simplify e1)),
adamc@1214 480 ("e2", p_exp (simplify e2)),
adamc@1214 481 ("e1'", p_exp (simplify e1')),
adamc@1214 482 ("e2'", p_exp (simplify e2')),
adamc@1214 483 ("t", p_t t)];*)
adamc@1214 484 eq (e1', e2')
adamc@1214 485 end
adamc@1214 486
adamc@1212 487 fun assert (t, e1, e2) =
adamc@1212 488 let
adamc@1212 489 val r1 = lookup (t, e1)
adamc@1212 490 val r2 = lookup (t, e2)
adamc@1212 491 in
adamc@1212 492 if eq (r1, r2) then
adamc@1212 493 t
adamc@1212 494 else
adamc@1214 495 let
adamc@1214 496 fun doUn (t, e1, e2) =
adamc@1214 497 case e1 of
adamc@1214 498 Func (f, [e]) => if String.isPrefix "un" f then
adamc@1214 499 let
adamc@1214 500 val s = String.extract (f, 2, NONE)
adamc@1214 501 in
adamc@1214 502 foldl (fn (e', t) =>
adamc@1214 503 case e' of
adamc@1214 504 Func (f', [e']) =>
adamc@1214 505 if f' = s then
adamc@1214 506 assert (assert (t, e', e1), e', e2)
adamc@1214 507 else
adamc@1214 508 t
adamc@1214 509 | _ => t) t (allPeers (t, e))
adamc@1214 510 end
adamc@1214 511 else
adamc@1214 512 t
adamc@1214 513 | _ => t
adamc@1214 514
adamc@1214 515 fun doProj (t, e1, e2) =
adamc@1214 516 foldl (fn ((e1', e2'), t) =>
adamc@1214 517 let
adamc@1214 518 fun doOne (e, t) =
adamc@1214 519 case e of
adamc@1214 520 Proj (e', f) =>
adamc@1214 521 if query (t, e1, e') then
adamc@1214 522 assert (t, e, Proj (e2, f))
adamc@1214 523 else
adamc@1214 524 t
adamc@1214 525 | _ => t
adamc@1214 526 in
adamc@1214 527 doOne (e1', doOne (e2', t))
adamc@1214 528 end) t t
adamc@1214 529
adamc@1214 530 val t = (r1, r2) :: t
adamc@1214 531 val t = doUn (t, r1, r2)
adamc@1214 532 val t = doUn (t, r2, r1)
adamc@1214 533 val t = doProj (t, r1, r2)
adamc@1214 534 val t = doProj (t, r2, r1)
adamc@1214 535 in
adamc@1214 536 t
adamc@1214 537 end
adamc@1212 538 end
adamc@1212 539
adamc@1208 540 end
adamc@1208 541
adamc@1208 542 fun rimp cc ((r1, es1), (r2, es2)) =
adamc@1202 543 case (r1, r2) of
adamc@1202 544 (Sql r1', Sql r2') =>
adamc@1202 545 r1' = r2' andalso
adamc@1202 546 (case (es1, es2) of
adamc@1214 547 ([e1], [e2]) => eq (e1, e2)
adamc@1202 548 | _ => false)
adamc@1202 549 | (Eq, Eq) =>
adamc@1202 550 (case (es1, es2) of
adamc@1202 551 ([x1, y1], [x2, y2]) =>
adamc@1202 552 let
adamc@1203 553 val saved = save ()
adamc@1202 554 in
adamc@1202 555 if eq (x1, x2) andalso eq (y1, y2) then
adamc@1202 556 true
adamc@1202 557 else
adamc@1203 558 (restore saved;
adamc@1208 559 if eq (x1, y2) andalso eq (y1, x2) then
adamc@1208 560 true
adamc@1208 561 else
adamc@1208 562 (restore saved;
adamc@1208 563 false))
adamc@1202 564 end
adamc@1202 565 | _ => false)
adamc@1207 566 | (Known, Known) =>
adamc@1207 567 (case (es1, es2) of
adamc@1208 568 ([Var v], [e2]) =>
adamc@1207 569 let
adamc@1208 570 fun matches e =
adamc@1208 571 case e of
adamc@1208 572 Var v' => v' = v
adamc@1208 573 | Proj (e, _) => matches e
adamc@1211 574 | Func (f, [e]) => String.isPrefix "un" f andalso matches e
adamc@1207 575 | _ => false
adamc@1207 576 in
adamc@1214 577 (*Print.prefaces "Checking peers" [("e2", p_exp e2),
adamc@1214 578 ("peers", Print.p_list p_exp (Cc.allPeers (cc, e2))),
adamc@1214 579 ("db", Cc.p_t cc)];*)
adamc@1208 580 List.exists matches (Cc.allPeers (cc, e2))
adamc@1207 581 end
adamc@1207 582 | _ => false)
adamc@1202 583 | _ => false
adamc@1202 584
adamc@1202 585 fun imply (p1, p2) =
adamc@1208 586 let
adamc@1208 587 fun doOne doKnown =
adamc@1208 588 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1208 589 (fn hyps =>
adamc@1208 590 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1208 591 (fn goals =>
adamc@1208 592 let
adamc@1208 593 val cc = foldl (fn (p, cc) =>
adamc@1208 594 case p of
adamc@1212 595 AReln (Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
adamc@1208 596 | _ => cc) Cc.empty hyps
adamc@1202 597
adamc@1208 598 fun gls goals onFail =
adamc@1208 599 case goals of
adamc@1208 600 [] => true
adamc@1212 601 | ACond _ :: _ => false
adamc@1212 602 | AReln g :: goals =>
adamc@1208 603 case (doKnown, g) of
adamc@1208 604 (false, (Known, _)) => gls goals onFail
adamc@1208 605 | _ =>
adamc@1208 606 let
adamc@1208 607 fun hps hyps =
adamc@1208 608 case hyps of
adamc@1214 609 [] => ((*Print.prefaces "Fail" [("g", p_prop (Reln g)),
adamc@1214 610 ("db", Cc.p_t cc)];*)
adamc@1213 611 onFail ())
adamc@1212 612 | ACond _ :: hyps => hps hyps
adamc@1212 613 | AReln h :: hyps =>
adamc@1208 614 let
adamc@1208 615 val saved = save ()
adamc@1208 616 in
adamc@1208 617 if rimp cc (h, g) then
adamc@1208 618 let
adamc@1208 619 val changed = IM.numItems (!unif)
adamc@1208 620 <> IM.numItems saved
adamc@1208 621 in
adamc@1208 622 gls goals (fn () => (restore saved;
adamc@1213 623 changed (*andalso
adamc@1213 624 (Print.preface ("Retry",
adamc@1213 625 p_prop
adamc@1213 626 (Reln g)
adamc@1213 627 ); true)*)
adamc@1213 628 andalso hps hyps))
adamc@1208 629 end
adamc@1208 630 else
adamc@1208 631 hps hyps
adamc@1208 632 end
adamc@1208 633 in
adamc@1208 634 (case g of
adamc@1208 635 (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
adamc@1208 636 | _ => false)
adamc@1208 637 orelse hps hyps
adamc@1208 638 end
adamc@1208 639 in
adamc@1212 640 if List.exists (fn AReln (DtCon c1, [e]) =>
adamc@1212 641 List.exists (fn AReln (DtCon c2, [e']) =>
adamc@1211 642 c1 <> c2 andalso
adamc@1211 643 Cc.query (cc, e, e')
adamc@1211 644 | _ => false) hyps
adamc@1211 645 orelse List.exists (fn Func (c2, []) => c1 <> c2
adamc@1211 646 | Finish => true
adamc@1211 647 | _ => false)
adamc@1211 648 (Cc.allPeers (cc, e))
adamc@1211 649 | _ => false) hyps
adamc@1211 650 orelse gls goals (fn () => false) then
adamc@1211 651 true
adamc@1211 652 else
adamc@1212 653 ((*Print.prefaces "Can't prove"
adamc@1212 654 [("hyps", Print.p_list p_atom hyps),
adamc@1212 655 ("goals", Print.p_list p_atom goals)];*)
adamc@1211 656 false)
adamc@1208 657 end))
adamc@1208 658 in
adamc@1208 659 reset ();
adamc@1208 660 doOne false;
adamc@1208 661 doOne true
adamc@1208 662 end
adamc@1200 663
adamc@1200 664 fun patCon pc =
adamc@1200 665 case pc of
adamc@1200 666 PConVar n => "C" ^ Int.toString n
adamc@1200 667 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 668
adamc@1200 669 datatype chunk =
adamc@1200 670 String of string
adamc@1200 671 | Exp of Mono.exp
adamc@1200 672
adamc@1200 673 fun chunkify e =
adamc@1200 674 case #1 e of
adamc@1200 675 EPrim (Prim.String s) => [String s]
adamc@1207 676 | EStrcat (e1, e2) =>
adamc@1207 677 let
adamc@1207 678 val chs1 = chunkify e1
adamc@1207 679 val chs2 = chunkify e2
adamc@1207 680 in
adamc@1207 681 case chs2 of
adamc@1207 682 String s2 :: chs2' =>
adamc@1207 683 (case List.last chs1 of
adamc@1207 684 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207 685 | _ => chs1 @ chs2)
adamc@1207 686 | _ => chs1 @ chs2
adamc@1207 687 end
adamc@1200 688 | _ => [Exp e]
adamc@1200 689
adamc@1201 690 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 691
adamc@1201 692 fun always v chs = SOME (v, chs)
adamc@1201 693
adamc@1202 694 fun parse p s =
adamc@1202 695 case p (chunkify s) of
adamc@1201 696 SOME (v, []) => SOME v
adamc@1201 697 | _ => NONE
adamc@1201 698
adamc@1201 699 fun const s chs =
adamc@1201 700 case chs of
adamc@1201 701 String s' :: chs => if String.isPrefix s s' then
adamc@1201 702 SOME ((), if size s = size s' then
adamc@1201 703 chs
adamc@1201 704 else
adamc@1201 705 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 706 else
adamc@1201 707 NONE
adamc@1201 708 | _ => NONE
adamc@1201 709
adamc@1201 710 fun follow p1 p2 chs =
adamc@1201 711 case p1 chs of
adamc@1201 712 NONE => NONE
adamc@1201 713 | SOME (v1, chs) =>
adamc@1201 714 case p2 chs of
adamc@1201 715 NONE => NONE
adamc@1201 716 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 717
adamc@1201 718 fun wrap p f chs =
adamc@1201 719 case p chs of
adamc@1201 720 NONE => NONE
adamc@1201 721 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 722
adamc@1209 723 fun wrapP p f chs =
adamc@1209 724 case p chs of
adamc@1209 725 NONE => NONE
adamc@1209 726 | SOME (v, chs) =>
adamc@1209 727 case f v of
adamc@1209 728 NONE => NONE
adamc@1209 729 | SOME r => SOME (r, chs)
adamc@1209 730
adamc@1201 731 fun alt p1 p2 chs =
adamc@1201 732 case p1 chs of
adamc@1201 733 NONE => p2 chs
adamc@1201 734 | v => v
adamc@1201 735
adamc@1207 736 fun altL ps =
adamc@1207 737 case rev ps of
adamc@1207 738 [] => (fn _ => NONE)
adamc@1207 739 | p :: ps =>
adamc@1207 740 foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207 741
adamc@1204 742 fun opt p chs =
adamc@1204 743 case p chs of
adamc@1204 744 NONE => SOME (NONE, chs)
adamc@1204 745 | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204 746
adamc@1201 747 fun skip cp chs =
adamc@1201 748 case chs of
adamc@1201 749 String "" :: chs => skip cp chs
adamc@1201 750 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 751 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 752 else
adamc@1201 753 SOME ((), chs)
adamc@1201 754 | _ => SOME ((), chs)
adamc@1201 755
adamc@1201 756 fun keep cp chs =
adamc@1201 757 case chs of
adamc@1201 758 String "" :: chs => keep cp chs
adamc@1201 759 | String s :: chs' =>
adamc@1201 760 let
adamc@1201 761 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 762 in
adamc@1201 763 if Substring.isEmpty befor then
adamc@1201 764 NONE
adamc@1201 765 else
adamc@1201 766 SOME (Substring.string befor,
adamc@1201 767 if Substring.isEmpty after then
adamc@1201 768 chs'
adamc@1201 769 else
adamc@1201 770 String (Substring.string after) :: chs')
adamc@1201 771 end
adamc@1201 772 | _ => NONE
adamc@1201 773
adamc@1204 774 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204 775 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204 776
adamc@1204 777 fun log name p chs =
adamc@1206 778 (if !debug then
adamc@1206 779 case chs of
adamc@1207 780 String s :: _ => print (name ^ ": " ^ s ^ "\n")
adamc@1206 781 | _ => print (name ^ ": blocked!\n")
adamc@1206 782 else
adamc@1206 783 ();
adamc@1204 784 p chs)
adamc@1201 785
adamc@1201 786 fun list p chs =
adamc@1207 787 altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207 788 (fn (v, ((), ls)) => v :: ls),
adamc@1207 789 wrap (ws p) (fn v => [v]),
adamc@1207 790 always []] chs
adamc@1201 791
adamc@1201 792 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 793
adamc@1211 794 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211 795 SOME (String.extract (s, 2, NONE))
adamc@1201 796 else
adamc@1211 797 NONE)
adamc@1211 798 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211 799 SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211 800 ^ String.extract (s, 4, NONE))
adamc@1211 801 else
adamc@1211 802 NONE)
adamc@1201 803
adamc@1211 804 val field = wrap (follow t_ident
adamc@1201 805 (follow (const ".")
adamc@1201 806 uw_ident))
adamc@1201 807 (fn (t, ((), f)) => (t, f))
adamc@1201 808
adamc@1206 809 datatype Rel =
adamc@1206 810 Exps of exp * exp -> prop
adamc@1206 811 | Props of prop * prop -> prop
adamc@1206 812
adamc@1204 813 datatype sqexp =
adamc@1206 814 SqConst of Prim.t
adamc@1206 815 | Field of string * string
adamc@1206 816 | Binop of Rel * sqexp * sqexp
adamc@1207 817 | SqKnown of sqexp
adamc@1207 818 | Inj of Mono.exp
adamc@1211 819 | SqFunc of string * sqexp
adamc@1211 820 | Count
adamc@1204 821
adamc@1210 822 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210 823
adamc@1210 824 val sqbrel = altL [cmp "=" Eq,
adamc@1210 825 cmp "<>" Ne,
adamc@1210 826 cmp "<=" Le,
adamc@1210 827 cmp "<" Lt,
adamc@1210 828 cmp ">=" Ge,
adamc@1210 829 cmp ">" Gt,
adamc@1207 830 wrap (const "AND") (fn () => Props And),
adamc@1207 831 wrap (const "OR") (fn () => Props Or)]
adamc@1204 832
adamc@1204 833 datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204 834
adamc@1209 835 fun string chs =
adamc@1206 836 case chs of
adamc@1209 837 String s :: chs =>
adamc@1209 838 if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209 839 let
adamc@1209 840 fun loop (cs, acc) =
adamc@1209 841 case cs of
adamc@1209 842 [] => NONE
adamc@1209 843 | c :: cs =>
adamc@1209 844 if c = #"'" then
adamc@1209 845 SOME (String.implode (rev acc), cs)
adamc@1209 846 else if c = #"\\" then
adamc@1209 847 case cs of
adamc@1209 848 c :: cs => loop (cs, c :: acc)
adamc@1209 849 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209 850 else
adamc@1209 851 loop (cs, c :: acc)
adamc@1209 852 in
adamc@1209 853 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209 854 NONE => NONE
adamc@1209 855 | SOME (s, []) => SOME (s, chs)
adamc@1209 856 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209 857 end
adamc@1209 858 else
adamc@1209 859 NONE
adamc@1209 860 | _ => NONE
adamc@1206 861
adamc@1209 862 val prim =
adamc@1209 863 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209 864 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209 865 (opt (const "::float8"))) #1,
adamc@1209 866 wrap (follow (wrapP (keep Char.isDigit)
adamc@1209 867 (Option.map Prim.Int o Int64.fromString))
adamc@1209 868 (opt (const "::int8"))) #1,
adamc@1209 869 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209 870 (Prim.String o #1 o #2)]
adamc@1206 871
adamc@1207 872 fun known' chs =
adamc@1207 873 case chs of
adamc@1207 874 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207 875 | _ => NONE
adamc@1207 876
adamc@1207 877 fun sqlify chs =
adamc@1207 878 case chs of
adamc@1207 879 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207 880 if String.isPrefix "sqlify" f then
adamc@1207 881 SOME (e, chs)
adamc@1207 882 else
adamc@1207 883 NONE
adamc@1207 884 | _ => NONE
adamc@1207 885
adamc@1211 886 fun constK s = wrap (const s) (fn () => s)
adamc@1211 887
adamc@1211 888 val funcName = altL [constK "COUNT",
adamc@1211 889 constK "MIN",
adamc@1211 890 constK "MAX",
adamc@1211 891 constK "SUM",
adamc@1211 892 constK "AVG"]
adamc@1211 893
adamc@1204 894 fun sqexp chs =
adamc@1206 895 log "sqexp"
adamc@1207 896 (altL [wrap prim SqConst,
adamc@1211 897 wrap field Field,
adamc@1207 898 wrap known SqKnown,
adamc@1211 899 wrap func SqFunc,
adamc@1211 900 wrap (const "COUNT(*)") (fn () => Count),
adamc@1207 901 wrap sqlify Inj,
adamc@1211 902 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211 903 (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211 904 (fn ((), (e, _)) => e),
adamc@1207 905 wrap (follow (ws (const "("))
adamc@1207 906 (follow (wrap
adamc@1207 907 (follow sqexp
adamc@1207 908 (alt
adamc@1207 909 (wrap
adamc@1207 910 (follow (ws sqbrel)
adamc@1207 911 (ws sqexp))
adamc@1207 912 inl)
adamc@1207 913 (always (inr ()))))
adamc@1207 914 (fn (e1, sm) =>
adamc@1207 915 case sm of
adamc@1207 916 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207 917 | inr () => e1))
adamc@1207 918 (const ")")))
adamc@1207 919 (fn ((), (e, ())) => e)])
adamc@1207 920 chs
adamc@1206 921
adamc@1207 922 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 923 (fn ((), ((), (e, ()))) => e) chs
adamc@1211 924
adamc@1211 925 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 926 (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211 927
adamc@1211 928 datatype sitem =
adamc@1211 929 SqField of string * string
adamc@1211 930 | SqExp of sqexp * string
adamc@1211 931
adamc@1211 932 val sitem = alt (wrap field SqField)
adamc@1211 933 (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211 934 (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207 935
adamc@1207 936 val select = log "select"
adamc@1207 937 (wrap (follow (const "SELECT ") (list sitem))
adamc@1207 938 (fn ((), ls) => ls))
adamc@1201 939
adamc@1201 940 val fitem = wrap (follow uw_ident
adamc@1201 941 (follow (const " AS ")
adamc@1201 942 t_ident))
adamc@1201 943 (fn (t, ((), f)) => (t, f))
adamc@1201 944
adamc@1207 945 val from = log "from"
adamc@1207 946 (wrap (follow (const "FROM ") (list fitem))
adamc@1207 947 (fn ((), ls) => ls))
adamc@1201 948
adamc@1204 949 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204 950 (fn ((), ls) => ls)
adamc@1204 951
adamc@1207 952 val query = log "query"
adamc@1207 953 (wrap (follow (follow select from) (opt wher))
adamc@1207 954 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201 955
adamc@1211 956 fun removeDups ls =
adamc@1211 957 case ls of
adamc@1211 958 [] => []
adamc@1211 959 | x :: ls =>
adamc@1211 960 let
adamc@1211 961 val ls = removeDups ls
adamc@1211 962 in
adamc@1211 963 if List.exists (fn x' => x' = x) ls then
adamc@1211 964 ls
adamc@1211 965 else
adamc@1211 966 x :: ls
adamc@1211 967 end
adamc@1211 968
adamc@1212 969 datatype queryMode =
adamc@1212 970 SomeCol of exp
adamc@1212 971 | AllCols of exp
adamc@1212 972
adamc@1214 973 fun queryProp env rvN rv oe e =
adamc@1202 974 case parse query e of
adamc@1207 975 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1207 976 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1214 977 (rvN, Var 0, Unknown, []))
adamc@1201 978 | SOME r =>
adamc@1202 979 let
adamc@1214 980 val (rvN, count) = rv rvN
adamc@1214 981
adamc@1214 982 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1214 983 let
adamc@1214 984 val (rvN, e) = rv rvN
adamc@1214 985 in
adamc@1214 986 ((v, e), rvN)
adamc@1214 987 end) rvN (#From r)
adamc@1214 988
adamc@1214 989 fun rvOf v =
adamc@1214 990 case List.find (fn (v', _) => v' = v) rvs of
adamc@1214 991 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1214 992 | SOME (_, e) => e
adamc@1214 993
adamc@1211 994 fun usedFields e =
adamc@1211 995 case e of
adamc@1211 996 SqConst _ => []
adamc@1211 997 | Field (v, f) => [(v, f)]
adamc@1211 998 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1211 999 | SqKnown _ => []
adamc@1211 1000 | Inj _ => []
adamc@1211 1001 | SqFunc (_, e) => usedFields e
adamc@1211 1002 | Count => []
adamc@1211 1003
adamc@1202 1004 val p =
adamc@1214 1005 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1205 1006
adamc@1205 1007 fun expIn e =
adamc@1205 1008 case e of
adamc@1206 1009 SqConst p => inl (Const p)
adamc@1214 1010 | Field (v, f) => inl (Proj (rvOf v, f))
adamc@1205 1011 | Binop (bo, e1, e2) =>
adamc@1206 1012 inr (case (bo, expIn e1, expIn e2) of
adamc@1206 1013 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1206 1014 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1206 1015 | _ => Unknown)
adamc@1207 1016 | SqKnown e =>
adamc@1207 1017 inr (case expIn e of
adamc@1207 1018 inl e => Reln (Known, [e])
adamc@1207 1019 | _ => Unknown)
adamc@1207 1020 | Inj e =>
adamc@1207 1021 let
adamc@1207 1022 fun deinj (e, _) =
adamc@1207 1023 case e of
adamc@1207 1024 ERel n => List.nth (env, n)
adamc@1207 1025 | EField (e, f) => Proj (deinj e, f)
adamc@1207 1026 | _ => raise Fail "Iflow: non-variable injected into query"
adamc@1207 1027 in
adamc@1207 1028 inl (deinj e)
adamc@1207 1029 end
adamc@1211 1030 | SqFunc (f, e) =>
adamc@1211 1031 inl (case expIn e of
adamc@1211 1032 inl e => Func (f, [e])
adamc@1211 1033 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
adamc@1214 1034 | Count => inl count
adamc@1210 1035
adamc@1205 1036 val p = case #Where r of
adamc@1205 1037 NONE => p
adamc@1205 1038 | SOME e =>
adamc@1205 1039 case expIn e of
adamc@1205 1040 inr p' => And (p, p')
adamc@1205 1041 | _ => p
adamc@1202 1042 in
adamc@1214 1043 (rvN,
adamc@1214 1044 count,
adamc@1214 1045 And (p, case oe of
adamc@1212 1046 SomeCol oe =>
adamc@1212 1047 foldl (fn (si, p) =>
adamc@1211 1048 let
adamc@1211 1049 val p' = case si of
adamc@1214 1050 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
adamc@1211 1051 | SqExp (e, f) =>
adamc@1211 1052 case expIn e of
adamc@1211 1053 inr _ => Unknown
adamc@1211 1054 | inl e => Reln (Eq, [oe, e])
adamc@1211 1055 in
adamc@1211 1056 Or (p, p')
adamc@1211 1057 end)
adamc@1212 1058 False (#Select r)
adamc@1212 1059 | AllCols oe =>
adamc@1212 1060 foldl (fn (si, p) =>
adamc@1212 1061 let
adamc@1212 1062 val p' = case si of
adamc@1212 1063 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
adamc@1214 1064 Proj (rvOf v, f)])
adamc@1212 1065 | SqExp (e, f) =>
adamc@1212 1066 case expIn e of
adamc@1212 1067 inr p => Cond (Proj (oe, f), p)
adamc@1212 1068 | inl e => Reln (Eq, [Proj (oe, f), e])
adamc@1212 1069 in
adamc@1212 1070 And (p, p')
adamc@1212 1071 end)
adamc@1212 1072 True (#Select r)),
adamc@1210 1073
adamc@1210 1074 case #Where r of
adamc@1210 1075 NONE => []
adamc@1214 1076 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
adamc@1202 1077 end
adamc@1200 1078
adamc@1211 1079 fun evalPat env e (pt, _) =
adamc@1211 1080 case pt of
adamc@1211 1081 PWild => (env, True)
adamc@1211 1082 | PVar _ => (e :: env, True)
adamc@1211 1083 | PPrim _ => (env, True)
adamc@1211 1084 | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e]))
adamc@1211 1085 | PCon (_, pc, SOME pt) =>
adamc@1211 1086 let
adamc@1211 1087 val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt
adamc@1211 1088 in
adamc@1211 1089 (env, And (p, Reln (DtCon (patCon pc), [e])))
adamc@1211 1090 end
adamc@1211 1091 | PRecord xpts =>
adamc@1211 1092 foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211 1093 let
adamc@1211 1094 val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211 1095 in
adamc@1211 1096 (env, And (p', p))
adamc@1211 1097 end) (env, True) xpts
adamc@1211 1098 | PNone _ => (env, Reln (DtCon "None", [e]))
adamc@1211 1099 | PSome (_, pt) =>
adamc@1211 1100 let
adamc@1211 1101 val (env, p) = evalPat env (Func ("unSome", [e])) pt
adamc@1211 1102 in
adamc@1211 1103 (env, And (p, Reln (DtCon "Some", [e])))
adamc@1211 1104 end
adamc@1211 1105
adamc@1211 1106 fun peq (p1, p2) =
adamc@1211 1107 case (p1, p2) of
adamc@1211 1108 (True, True) => true
adamc@1211 1109 | (False, False) => true
adamc@1211 1110 | (Unknown, Unknown) => true
adamc@1211 1111 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1112 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1113 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212 1114 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211 1115 | _ => false
adamc@1211 1116
adamc@1211 1117 fun removeRedundant p1 =
adamc@1211 1118 let
adamc@1211 1119 fun rr p2 =
adamc@1211 1120 if peq (p1, p2) then
adamc@1211 1121 True
adamc@1211 1122 else
adamc@1211 1123 case p2 of
adamc@1211 1124 And (x, y) => And (rr x, rr y)
adamc@1211 1125 | Or (x, y) => Or (rr x, rr y)
adamc@1211 1126 | _ => p2
adamc@1211 1127 in
adamc@1211 1128 rr
adamc@1211 1129 end
adamc@1211 1130
adamc@1202 1131 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
adamc@1200 1132 let
adamc@1200 1133 fun default () =
adamc@1213 1134 ((*Print.preface ("Default" ^ Int.toString nv,
adamc@1213 1135 MonoPrint.p_exp MonoEnv.empty e);*)
adamc@1213 1136 (Var nv, (nv+1, p, sent)))
adamc@1200 1137
adamc@1200 1138 fun addSent (p, e, sent) =
adamc@1200 1139 if isKnown e then
adamc@1200 1140 sent
adamc@1200 1141 else
adamc@1202 1142 (loc, e, p) :: sent
adamc@1200 1143 in
adamc@1200 1144 case #1 e of
adamc@1200 1145 EPrim p => (Const p, st)
adamc@1200 1146 | ERel n => (List.nth (env, n), st)
adamc@1200 1147 | ENamed _ => default ()
adamc@1200 1148 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200 1149 | ECon (_, pc, SOME e) =>
adamc@1200 1150 let
adamc@1200 1151 val (e, st) = evalExp env (e, st)
adamc@1200 1152 in
adamc@1200 1153 (Func (patCon pc, [e]), st)
adamc@1200 1154 end
adamc@1200 1155 | ENone _ => (Func ("None", []), st)
adamc@1200 1156 | ESome (_, e) =>
adamc@1200 1157 let
adamc@1200 1158 val (e, st) = evalExp env (e, st)
adamc@1200 1159 in
adamc@1200 1160 (Func ("Some", [e]), st)
adamc@1200 1161 end
adamc@1200 1162 | EFfi _ => default ()
adamc@1213 1163
adamc@1200 1164 | EFfiApp (m, s, es) =>
adamc@1200 1165 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 1166 let
adamc@1200 1167 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1168 in
adamc@1214 1169 (Recd [], (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200 1170 end
adamc@1200 1171 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 1172 default ()
adamc@1200 1173 else
adamc@1200 1174 let
adamc@1200 1175 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1176 in
adamc@1200 1177 (Func (m ^ "." ^ s, es), st)
adamc@1200 1178 end
adamc@1213 1179
adamc@1213 1180 | EApp (e1, e2) =>
adamc@1213 1181 let
adamc@1213 1182 val (e1, st) = evalExp env (e1, st)
adamc@1213 1183 in
adamc@1213 1184 case e1 of
adamc@1213 1185 Finish => (Finish, st)
adamc@1213 1186 | _ => default ()
adamc@1213 1187 end
adamc@1213 1188
adamc@1200 1189 | EAbs _ => default ()
adamc@1200 1190 | EUnop (s, e1) =>
adamc@1200 1191 let
adamc@1200 1192 val (e1, st) = evalExp env (e1, st)
adamc@1200 1193 in
adamc@1200 1194 (Func (s, [e1]), st)
adamc@1200 1195 end
adamc@1200 1196 | EBinop (s, e1, e2) =>
adamc@1200 1197 let
adamc@1200 1198 val (e1, st) = evalExp env (e1, st)
adamc@1200 1199 val (e2, st) = evalExp env (e2, st)
adamc@1200 1200 in
adamc@1200 1201 (Func (s, [e1, e2]), st)
adamc@1200 1202 end
adamc@1200 1203 | ERecord xets =>
adamc@1200 1204 let
adamc@1200 1205 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 1206 let
adamc@1200 1207 val (e, st) = evalExp env (e, st)
adamc@1200 1208 in
adamc@1200 1209 ((x, e), st)
adamc@1200 1210 end) st xets
adamc@1200 1211 in
adamc@1200 1212 (Recd xes, st)
adamc@1200 1213 end
adamc@1200 1214 | EField (e, s) =>
adamc@1200 1215 let
adamc@1200 1216 val (e, st) = evalExp env (e, st)
adamc@1200 1217 in
adamc@1200 1218 (Proj (e, s), st)
adamc@1200 1219 end
adamc@1211 1220 | ECase (e, pes, _) =>
adamc@1211 1221 let
adamc@1211 1222 val (e, st) = evalExp env (e, st)
adamc@1211 1223 val r = #1 st
adamc@1211 1224 val st = (r + 1, #2 st, #3 st)
adamc@1211 1225 val orig = #2 st
adamc@1211 1226
adamc@1211 1227 val st = foldl (fn ((pt, pe), st) =>
adamc@1211 1228 let
adamc@1211 1229 val (env, pp) = evalPat env e pt
adamc@1211 1230 val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st))
adamc@1211 1231
adamc@1211 1232 val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe]))
adamc@1211 1233 in
adamc@1211 1234 (#1 st', Or (#2 st, this), #3 st')
adamc@1211 1235 end) (#1 st, False, #3 st) pes
adamc@1211 1236 in
adamc@1211 1237 (Var r, (#1 st, And (orig, #2 st), #3 st))
adamc@1211 1238 end
adamc@1200 1239 | EStrcat (e1, e2) =>
adamc@1200 1240 let
adamc@1200 1241 val (e1, st) = evalExp env (e1, st)
adamc@1200 1242 val (e2, st) = evalExp env (e2, st)
adamc@1200 1243 in
adamc@1200 1244 (Func ("cat", [e1, e2]), st)
adamc@1200 1245 end
adamc@1200 1246 | EError _ => (Finish, st)
adamc@1200 1247 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 1248 let
adamc@1200 1249 val (b, st) = evalExp env (b, st)
adamc@1200 1250 val (m, st) = evalExp env (m, st)
adamc@1200 1251 in
adamc@1200 1252 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200 1253 end
adamc@1200 1254 | ERedirect (e, _) =>
adamc@1200 1255 let
adamc@1200 1256 val (e, st) = evalExp env (e, st)
adamc@1200 1257 in
adamc@1200 1258 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 1259 end
adamc@1200 1260 | EWrite e =>
adamc@1200 1261 let
adamc@1200 1262 val (e, st) = evalExp env (e, st)
adamc@1200 1263 in
adamc@1214 1264 (Recd [], (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 1265 end
adamc@1200 1266 | ESeq (e1, e2) =>
adamc@1200 1267 let
adamc@1200 1268 val (_, st) = evalExp env (e1, st)
adamc@1200 1269 in
adamc@1200 1270 evalExp env (e2, st)
adamc@1200 1271 end
adamc@1200 1272 | ELet (_, _, e1, e2) =>
adamc@1200 1273 let
adamc@1200 1274 val (e1, st) = evalExp env (e1, st)
adamc@1200 1275 in
adamc@1200 1276 evalExp (e1 :: env) (e2, st)
adamc@1200 1277 end
adamc@1200 1278 | EClosure (n, es) =>
adamc@1200 1279 let
adamc@1200 1280 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1281 in
adamc@1200 1282 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200 1283 end
adamc@1200 1284
adamc@1200 1285 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 1286 let
adamc@1200 1287 val (_, st) = evalExp env (q, st)
adamc@1200 1288 val (i, st) = evalExp env (i, st)
adamc@1200 1289
adamc@1200 1290 val r = #1 st
adamc@1214 1291 val acc = #1 st + 1
adamc@1214 1292 val st' = (#1 st + 2, #2 st, #3 st)
adamc@1200 1293
adamc@1200 1294 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 1295
adamc@1214 1296 val (rvN, count, qp, used) =
adamc@1214 1297 queryProp env
adamc@1214 1298 (#1 st') (fn rvN => (rvN + 1, Var rvN))
adamc@1214 1299 (AllCols (Var r)) q
adamc@1200 1300
adamc@1212 1301 val p' = And (qp, #2 st')
adamc@1200 1302
adamc@1212 1303 val (nvs, p, res) = if varInP acc (#2 st') then
adamc@1212 1304 (#1 st + 1, #2 st, Var r)
adamc@1212 1305 else
adamc@1212 1306 let
adamc@1214 1307 val out = rvN
adamc@1210 1308
adamc@1212 1309 val p = Or (Reln (Eq, [Var out, i]),
adamc@1212 1310 And (Reln (Eq, [Var out, b]),
adamc@1214 1311 And (Reln (Gt, [count,
adamc@1212 1312 Const (Prim.Int 0)]),
adamc@1212 1313 p')))
adamc@1212 1314 in
adamc@1212 1315 (out + 1, p, Var out)
adamc@1212 1316 end
adamc@1212 1317
adamc@1212 1318 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (#3 st')
adamc@1210 1319 val sent = map (fn e => (loc, e, p')) used @ sent
adamc@1200 1320 in
adamc@1212 1321 (res, (nvs, p, sent))
adamc@1200 1322 end
adamc@1200 1323 | EDml _ => default ()
adamc@1200 1324 | ENextval _ => default ()
adamc@1200 1325 | ESetval _ => default ()
adamc@1200 1326
adamc@1213 1327 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1213 1328 (Var nv, (nv + 1, And (p, Reln (Known, [Var nv])), sent))
adamc@1213 1329
adamc@1200 1330 | EUnurlify _ => default ()
adamc@1200 1331 | EJavaScript _ => default ()
adamc@1200 1332 | ESignalReturn _ => default ()
adamc@1200 1333 | ESignalBind _ => default ()
adamc@1200 1334 | ESignalSource _ => default ()
adamc@1200 1335 | EServerCall _ => default ()
adamc@1200 1336 | ERecv _ => default ()
adamc@1200 1337 | ESleep _ => default ()
adamc@1200 1338 | ESpawn _ => default ()
adamc@1200 1339 end
adamc@1200 1340
adamc@1200 1341 fun check file =
adamc@1200 1342 let
adamc@1213 1343 val file = MonoReduce.reduce file
adamc@1213 1344 val file = MonoOpt.optimize file
adamc@1213 1345 val file = Fuse.fuse file
adamc@1213 1346 val file = MonoOpt.optimize file
adamc@1213 1347 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 1348
adamc@1207 1349 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 1350 case d of
adamc@1207 1351 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 1352 | _ => exptd) IS.empty file
adamc@1207 1353
adamc@1202 1354 fun decl ((d, _), (vals, pols)) =
adamc@1200 1355 case d of
adamc@1207 1356 DVal (_, n, _, e, _) =>
adamc@1200 1357 let
adamc@1207 1358 val isExptd = IS.member (exptd, n)
adamc@1207 1359
adamc@1207 1360 fun deAbs (e, env, nv, p) =
adamc@1200 1361 case #1 e of
adamc@1207 1362 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207 1363 if isExptd then
adamc@1207 1364 And (p, Reln (Known, [Var nv]))
adamc@1207 1365 else
adamc@1207 1366 p)
adamc@1207 1367 | _ => (e, env, nv, p)
adamc@1200 1368
adamc@1207 1369 val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200 1370
adamc@1207 1371 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
adamc@1200 1372 in
adamc@1207 1373 (sent @ vals, pols)
adamc@1200 1374 end
adamc@1202 1375
adamc@1214 1376 | DPolicy (PolClient e) => (vals, #3 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
adamc@1214 1377 (SomeCol (Var 0)) e) :: pols)
adamc@1214 1378
adamc@1202 1379 | _ => (vals, pols)
adamc@1202 1380
adamc@1203 1381 val () = reset ()
adamc@1202 1382
adamc@1202 1383 val (vals, pols) = foldl decl ([], []) file
adamc@1200 1384 in
adamc@1207 1385 app (fn (loc, e, p) =>
adamc@1207 1386 let
adamc@1213 1387 fun doOne e =
adamc@1213 1388 let
adamc@1213 1389 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213 1390 in
adamc@1213 1391 if List.exists (fn pol => if imply (p, pol) then
adamc@1213 1392 (if !debug then
adamc@1213 1393 Print.prefaces "Match"
adamc@1213 1394 [("Hyp", p_prop p),
adamc@1213 1395 ("Goal", p_prop pol)]
adamc@1213 1396 else
adamc@1213 1397 ();
adamc@1213 1398 true)
adamc@1213 1399 else
adamc@1213 1400 false) pols then
adamc@1213 1401 ()
adamc@1213 1402 else
adamc@1213 1403 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1213 1404 Print.preface ("The state satisifes this predicate:", p_prop p))
adamc@1213 1405 end
adamc@1213 1406
adamc@1213 1407 fun doAll e =
adamc@1213 1408 case e of
adamc@1213 1409 Const _ => ()
adamc@1213 1410 | Var _ => doOne e
adamc@1213 1411 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1213 1412 | Func (f, es) => if String.isPrefix "un" f then
adamc@1213 1413 doOne e
adamc@1213 1414 else
adamc@1213 1415 app doAll es
adamc@1213 1416 | Recd xes => app (doAll o #2) xes
adamc@1213 1417 | Proj _ => doOne e
adamc@1213 1418 | Finish => ()
adamc@1207 1419 in
adamc@1213 1420 doAll e
adamc@1207 1421 end) vals
adamc@1200 1422 end
adamc@1200 1423
adamc@1213 1424 val check = fn file =>
adamc@1213 1425 let
adamc@1213 1426 val oldInline = Settings.getMonoInline ()
adamc@1213 1427 in
adamc@1213 1428 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 1429 NONE => 1000000
adamc@1213 1430 | SOME n => n);
adamc@1213 1431 check file;
adamc@1213 1432 Settings.setMonoInline oldInline)
adamc@1213 1433 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 1434 raise ex)
adamc@1213 1435 end
adamc@1213 1436
adamc@1200 1437 end
adamc@1213 1438