Mercurial > urweb

annotate src/iflow.sml @ 1213:e791d93d4616

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
secret logon
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 16:14:19 -0400
parents fc33072c4d33
children 648e6b087dfb
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@1208 415 end = struct
adamc@1208 416
adamc@1211 417 fun eq (e1, e2) = eeq (simplify e1, simplify e2)
adamc@1208 418
adamc@1208 419 type t = (exp * exp) list
adamc@1208 420
adamc@1208 421 val empty = []
adamc@1208 422
adamc@1208 423 fun lookup (t, e) =
adamc@1208 424 case List.find (fn (e', _) => eq (e', e)) t of
adamc@1208 425 NONE => e
adamc@1208 426 | SOME (_, e2) => lookup (t, e2)
adamc@1208 427
adamc@1208 428 fun allPeers (t, e) =
adamc@1208 429 let
adamc@1208 430 val r = lookup (t, e)
adamc@1208 431 in
adamc@1208 432 r :: List.mapPartial (fn (e1, e2) =>
adamc@1208 433 let
adamc@1208 434 val r' = lookup (t, e2)
adamc@1208 435 in
adamc@1208 436 if eq (r, r') then
adamc@1208 437 SOME e1
adamc@1208 438 else
adamc@1208 439 NONE
adamc@1208 440 end) t
adamc@1208 441 end
adamc@1208 442
adamc@1212 443 fun assert (t, e1, e2) =
adamc@1212 444 let
adamc@1212 445 val r1 = lookup (t, e1)
adamc@1212 446 val r2 = lookup (t, e2)
adamc@1212 447
adamc@1213 448 fun doUn k (t', e1, e2) =
adamc@1212 449 case e2 of
adamc@1212 450 Func (f, [e]) =>
adamc@1212 451 if String.isPrefix "un" f then
adamc@1212 452 let
adamc@1212 453 val f' = String.extract (f, 2, NONE)
adamc@1212 454 in
adamc@1212 455 foldl (fn (e', t') =>
adamc@1212 456 case e' of
adamc@1212 457 Func (f'', [e'']) =>
adamc@1212 458 if f'' = f' then
adamc@1213 459 (lookup (t', e1), k e'') :: t'
adamc@1212 460 else
adamc@1212 461 t'
adamc@1212 462 | _ => t') t' (allPeers (t, e))
adamc@1212 463 end
adamc@1212 464 else
adamc@1212 465 t'
adamc@1213 466 | Proj (e2, f) => doUn (fn e' => k (Proj (e', f))) (t', e1, e2)
adamc@1212 467 | _ => t'
adamc@1212 468 in
adamc@1212 469 if eq (r1, r2) then
adamc@1212 470 t
adamc@1212 471 else
adamc@1213 472 doUn (fn x => x) (doUn (fn x => x) ((r1, r2) :: t, e1, e2), e2, e1)
adamc@1212 473 end
adamc@1212 474
adamc@1212 475 open Print
adamc@1212 476
adamc@1212 477 fun query (t, e1, e2) =
adamc@1212 478 ((*prefaces "CC query" [("e1", p_exp (simplify e1)),
adamc@1212 479 ("e2", p_exp (simplify e2)),
adamc@1212 480 ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
adamc@1212 481 space,
adamc@1212 482 PD.string "->",
adamc@1212 483 space,
adamc@1212 484 p_exp (simplify e2)]) t)];*)
adamc@1212 485 eq (lookup (t, e1), lookup (t, e2)))
adamc@1212 486
adamc@1208 487 end
adamc@1208 488
adamc@1208 489 fun rimp cc ((r1, es1), (r2, es2)) =
adamc@1202 490 case (r1, r2) of
adamc@1202 491 (Sql r1', Sql r2') =>
adamc@1202 492 r1' = r2' andalso
adamc@1202 493 (case (es1, es2) of
adamc@1202 494 ([Recd xes1], [Recd xes2]) =>
adamc@1202 495 let
adamc@1203 496 val saved = save ()
adamc@1202 497 in
adamc@1202 498 if List.all (fn (f, e2) =>
adamc@1203 499 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
adamc@1203 500 NONE => true
adamc@1203 501 | SOME e1 => eq (e1, e2)) xes2 then
adamc@1202 502 true
adamc@1202 503 else
adamc@1203 504 (restore saved;
adamc@1202 505 false)
adamc@1202 506 end
adamc@1202 507 | _ => false)
adamc@1202 508 | (Eq, Eq) =>
adamc@1202 509 (case (es1, es2) of
adamc@1202 510 ([x1, y1], [x2, y2]) =>
adamc@1202 511 let
adamc@1203 512 val saved = save ()
adamc@1202 513 in
adamc@1202 514 if eq (x1, x2) andalso eq (y1, y2) then
adamc@1202 515 true
adamc@1202 516 else
adamc@1203 517 (restore saved;
adamc@1208 518 if eq (x1, y2) andalso eq (y1, x2) then
adamc@1208 519 true
adamc@1208 520 else
adamc@1208 521 (restore saved;
adamc@1208 522 false))
adamc@1202 523 end
adamc@1202 524 | _ => false)
adamc@1207 525 | (Known, Known) =>
adamc@1207 526 (case (es1, es2) of
adamc@1208 527 ([Var v], [e2]) =>
adamc@1207 528 let
adamc@1208 529 fun matches e =
adamc@1208 530 case e of
adamc@1208 531 Var v' => v' = v
adamc@1208 532 | Proj (e, _) => matches e
adamc@1211 533 | Func (f, [e]) => String.isPrefix "un" f andalso matches e
adamc@1207 534 | _ => false
adamc@1207 535 in
adamc@1208 536 List.exists matches (Cc.allPeers (cc, e2))
adamc@1207 537 end
adamc@1207 538 | _ => false)
adamc@1202 539 | _ => false
adamc@1202 540
adamc@1202 541 fun imply (p1, p2) =
adamc@1208 542 let
adamc@1208 543 fun doOne doKnown =
adamc@1208 544 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1208 545 (fn hyps =>
adamc@1208 546 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1208 547 (fn goals =>
adamc@1208 548 let
adamc@1208 549 val cc = foldl (fn (p, cc) =>
adamc@1208 550 case p of
adamc@1212 551 AReln (Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
adamc@1208 552 | _ => cc) Cc.empty hyps
adamc@1202 553
adamc@1208 554 fun gls goals onFail =
adamc@1208 555 case goals of
adamc@1208 556 [] => true
adamc@1212 557 | ACond _ :: _ => false
adamc@1212 558 | AReln g :: goals =>
adamc@1208 559 case (doKnown, g) of
adamc@1208 560 (false, (Known, _)) => gls goals onFail
adamc@1208 561 | _ =>
adamc@1208 562 let
adamc@1208 563 fun hps hyps =
adamc@1208 564 case hyps of
adamc@1213 565 [] => ((*Print.preface ("Fail", p_prop (Reln g));*)
adamc@1213 566 onFail ())
adamc@1212 567 | ACond _ :: hyps => hps hyps
adamc@1212 568 | AReln h :: hyps =>
adamc@1208 569 let
adamc@1208 570 val saved = save ()
adamc@1208 571 in
adamc@1208 572 if rimp cc (h, g) then
adamc@1208 573 let
adamc@1208 574 val changed = IM.numItems (!unif)
adamc@1208 575 <> IM.numItems saved
adamc@1208 576 in
adamc@1208 577 gls goals (fn () => (restore saved;
adamc@1213 578 changed (*andalso
adamc@1213 579 (Print.preface ("Retry",
adamc@1213 580 p_prop
adamc@1213 581 (Reln g)
adamc@1213 582 ); true)*)
adamc@1213 583 andalso hps hyps))
adamc@1208 584 end
adamc@1208 585 else
adamc@1208 586 hps hyps
adamc@1208 587 end
adamc@1208 588 in
adamc@1208 589 (case g of
adamc@1208 590 (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
adamc@1208 591 | _ => false)
adamc@1208 592 orelse hps hyps
adamc@1208 593 end
adamc@1208 594 in
adamc@1212 595 if List.exists (fn AReln (DtCon c1, [e]) =>
adamc@1212 596 List.exists (fn AReln (DtCon c2, [e']) =>
adamc@1211 597 c1 <> c2 andalso
adamc@1211 598 Cc.query (cc, e, e')
adamc@1211 599 | _ => false) hyps
adamc@1211 600 orelse List.exists (fn Func (c2, []) => c1 <> c2
adamc@1211 601 | Finish => true
adamc@1211 602 | _ => false)
adamc@1211 603 (Cc.allPeers (cc, e))
adamc@1211 604 | _ => false) hyps
adamc@1211 605 orelse gls goals (fn () => false) then
adamc@1211 606 true
adamc@1211 607 else
adamc@1212 608 ((*Print.prefaces "Can't prove"
adamc@1212 609 [("hyps", Print.p_list p_atom hyps),
adamc@1212 610 ("goals", Print.p_list p_atom goals)];*)
adamc@1211 611 false)
adamc@1208 612 end))
adamc@1208 613 in
adamc@1208 614 reset ();
adamc@1208 615 doOne false;
adamc@1208 616 doOne true
adamc@1208 617 end
adamc@1200 618
adamc@1200 619 fun patCon pc =
adamc@1200 620 case pc of
adamc@1200 621 PConVar n => "C" ^ Int.toString n
adamc@1200 622 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 623
adamc@1200 624 datatype chunk =
adamc@1200 625 String of string
adamc@1200 626 | Exp of Mono.exp
adamc@1200 627
adamc@1200 628 fun chunkify e =
adamc@1200 629 case #1 e of
adamc@1200 630 EPrim (Prim.String s) => [String s]
adamc@1207 631 | EStrcat (e1, e2) =>
adamc@1207 632 let
adamc@1207 633 val chs1 = chunkify e1
adamc@1207 634 val chs2 = chunkify e2
adamc@1207 635 in
adamc@1207 636 case chs2 of
adamc@1207 637 String s2 :: chs2' =>
adamc@1207 638 (case List.last chs1 of
adamc@1207 639 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207 640 | _ => chs1 @ chs2)
adamc@1207 641 | _ => chs1 @ chs2
adamc@1207 642 end
adamc@1200 643 | _ => [Exp e]
adamc@1200 644
adamc@1201 645 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 646
adamc@1201 647 fun always v chs = SOME (v, chs)
adamc@1201 648
adamc@1202 649 fun parse p s =
adamc@1202 650 case p (chunkify s) of
adamc@1201 651 SOME (v, []) => SOME v
adamc@1201 652 | _ => NONE
adamc@1201 653
adamc@1201 654 fun const s chs =
adamc@1201 655 case chs of
adamc@1201 656 String s' :: chs => if String.isPrefix s s' then
adamc@1201 657 SOME ((), if size s = size s' then
adamc@1201 658 chs
adamc@1201 659 else
adamc@1201 660 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 661 else
adamc@1201 662 NONE
adamc@1201 663 | _ => NONE
adamc@1201 664
adamc@1201 665 fun follow p1 p2 chs =
adamc@1201 666 case p1 chs of
adamc@1201 667 NONE => NONE
adamc@1201 668 | SOME (v1, chs) =>
adamc@1201 669 case p2 chs of
adamc@1201 670 NONE => NONE
adamc@1201 671 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 672
adamc@1201 673 fun wrap p f chs =
adamc@1201 674 case p chs of
adamc@1201 675 NONE => NONE
adamc@1201 676 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 677
adamc@1209 678 fun wrapP p f chs =
adamc@1209 679 case p chs of
adamc@1209 680 NONE => NONE
adamc@1209 681 | SOME (v, chs) =>
adamc@1209 682 case f v of
adamc@1209 683 NONE => NONE
adamc@1209 684 | SOME r => SOME (r, chs)
adamc@1209 685
adamc@1201 686 fun alt p1 p2 chs =
adamc@1201 687 case p1 chs of
adamc@1201 688 NONE => p2 chs
adamc@1201 689 | v => v
adamc@1201 690
adamc@1207 691 fun altL ps =
adamc@1207 692 case rev ps of
adamc@1207 693 [] => (fn _ => NONE)
adamc@1207 694 | p :: ps =>
adamc@1207 695 foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207 696
adamc@1204 697 fun opt p chs =
adamc@1204 698 case p chs of
adamc@1204 699 NONE => SOME (NONE, chs)
adamc@1204 700 | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204 701
adamc@1201 702 fun skip cp chs =
adamc@1201 703 case chs of
adamc@1201 704 String "" :: chs => skip cp chs
adamc@1201 705 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 706 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 707 else
adamc@1201 708 SOME ((), chs)
adamc@1201 709 | _ => SOME ((), chs)
adamc@1201 710
adamc@1201 711 fun keep cp chs =
adamc@1201 712 case chs of
adamc@1201 713 String "" :: chs => keep cp chs
adamc@1201 714 | String s :: chs' =>
adamc@1201 715 let
adamc@1201 716 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 717 in
adamc@1201 718 if Substring.isEmpty befor then
adamc@1201 719 NONE
adamc@1201 720 else
adamc@1201 721 SOME (Substring.string befor,
adamc@1201 722 if Substring.isEmpty after then
adamc@1201 723 chs'
adamc@1201 724 else
adamc@1201 725 String (Substring.string after) :: chs')
adamc@1201 726 end
adamc@1201 727 | _ => NONE
adamc@1201 728
adamc@1204 729 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204 730 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204 731
adamc@1204 732 fun log name p chs =
adamc@1206 733 (if !debug then
adamc@1206 734 case chs of
adamc@1207 735 String s :: _ => print (name ^ ": " ^ s ^ "\n")
adamc@1206 736 | _ => print (name ^ ": blocked!\n")
adamc@1206 737 else
adamc@1206 738 ();
adamc@1204 739 p chs)
adamc@1201 740
adamc@1201 741 fun list p chs =
adamc@1207 742 altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207 743 (fn (v, ((), ls)) => v :: ls),
adamc@1207 744 wrap (ws p) (fn v => [v]),
adamc@1207 745 always []] chs
adamc@1201 746
adamc@1201 747 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 748
adamc@1211 749 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211 750 SOME (String.extract (s, 2, NONE))
adamc@1201 751 else
adamc@1211 752 NONE)
adamc@1211 753 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211 754 SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211 755 ^ String.extract (s, 4, NONE))
adamc@1211 756 else
adamc@1211 757 NONE)
adamc@1201 758
adamc@1211 759 val field = wrap (follow t_ident
adamc@1201 760 (follow (const ".")
adamc@1201 761 uw_ident))
adamc@1201 762 (fn (t, ((), f)) => (t, f))
adamc@1201 763
adamc@1206 764 datatype Rel =
adamc@1206 765 Exps of exp * exp -> prop
adamc@1206 766 | Props of prop * prop -> prop
adamc@1206 767
adamc@1204 768 datatype sqexp =
adamc@1206 769 SqConst of Prim.t
adamc@1206 770 | Field of string * string
adamc@1206 771 | Binop of Rel * sqexp * sqexp
adamc@1207 772 | SqKnown of sqexp
adamc@1207 773 | Inj of Mono.exp
adamc@1211 774 | SqFunc of string * sqexp
adamc@1211 775 | Count
adamc@1204 776
adamc@1210 777 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210 778
adamc@1210 779 val sqbrel = altL [cmp "=" Eq,
adamc@1210 780 cmp "<>" Ne,
adamc@1210 781 cmp "<=" Le,
adamc@1210 782 cmp "<" Lt,
adamc@1210 783 cmp ">=" Ge,
adamc@1210 784 cmp ">" Gt,
adamc@1207 785 wrap (const "AND") (fn () => Props And),
adamc@1207 786 wrap (const "OR") (fn () => Props Or)]
adamc@1204 787
adamc@1204 788 datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204 789
adamc@1209 790 fun string chs =
adamc@1206 791 case chs of
adamc@1209 792 String s :: chs =>
adamc@1209 793 if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209 794 let
adamc@1209 795 fun loop (cs, acc) =
adamc@1209 796 case cs of
adamc@1209 797 [] => NONE
adamc@1209 798 | c :: cs =>
adamc@1209 799 if c = #"'" then
adamc@1209 800 SOME (String.implode (rev acc), cs)
adamc@1209 801 else if c = #"\\" then
adamc@1209 802 case cs of
adamc@1209 803 c :: cs => loop (cs, c :: acc)
adamc@1209 804 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209 805 else
adamc@1209 806 loop (cs, c :: acc)
adamc@1209 807 in
adamc@1209 808 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209 809 NONE => NONE
adamc@1209 810 | SOME (s, []) => SOME (s, chs)
adamc@1209 811 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209 812 end
adamc@1209 813 else
adamc@1209 814 NONE
adamc@1209 815 | _ => NONE
adamc@1206 816
adamc@1209 817 val prim =
adamc@1209 818 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209 819 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209 820 (opt (const "::float8"))) #1,
adamc@1209 821 wrap (follow (wrapP (keep Char.isDigit)
adamc@1209 822 (Option.map Prim.Int o Int64.fromString))
adamc@1209 823 (opt (const "::int8"))) #1,
adamc@1209 824 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209 825 (Prim.String o #1 o #2)]
adamc@1206 826
adamc@1207 827 fun known' chs =
adamc@1207 828 case chs of
adamc@1207 829 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207 830 | _ => NONE
adamc@1207 831
adamc@1207 832 fun sqlify chs =
adamc@1207 833 case chs of
adamc@1207 834 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207 835 if String.isPrefix "sqlify" f then
adamc@1207 836 SOME (e, chs)
adamc@1207 837 else
adamc@1207 838 NONE
adamc@1207 839 | _ => NONE
adamc@1207 840
adamc@1211 841 fun constK s = wrap (const s) (fn () => s)
adamc@1211 842
adamc@1211 843 val funcName = altL [constK "COUNT",
adamc@1211 844 constK "MIN",
adamc@1211 845 constK "MAX",
adamc@1211 846 constK "SUM",
adamc@1211 847 constK "AVG"]
adamc@1211 848
adamc@1204 849 fun sqexp chs =
adamc@1206 850 log "sqexp"
adamc@1207 851 (altL [wrap prim SqConst,
adamc@1211 852 wrap field Field,
adamc@1207 853 wrap known SqKnown,
adamc@1211 854 wrap func SqFunc,
adamc@1211 855 wrap (const "COUNT(*)") (fn () => Count),
adamc@1207 856 wrap sqlify Inj,
adamc@1211 857 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211 858 (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211 859 (fn ((), (e, _)) => e),
adamc@1207 860 wrap (follow (ws (const "("))
adamc@1207 861 (follow (wrap
adamc@1207 862 (follow sqexp
adamc@1207 863 (alt
adamc@1207 864 (wrap
adamc@1207 865 (follow (ws sqbrel)
adamc@1207 866 (ws sqexp))
adamc@1207 867 inl)
adamc@1207 868 (always (inr ()))))
adamc@1207 869 (fn (e1, sm) =>
adamc@1207 870 case sm of
adamc@1207 871 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207 872 | inr () => e1))
adamc@1207 873 (const ")")))
adamc@1207 874 (fn ((), (e, ())) => e)])
adamc@1207 875 chs
adamc@1206 876
adamc@1207 877 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 878 (fn ((), ((), (e, ()))) => e) chs
adamc@1211 879
adamc@1211 880 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 881 (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211 882
adamc@1211 883 datatype sitem =
adamc@1211 884 SqField of string * string
adamc@1211 885 | SqExp of sqexp * string
adamc@1211 886
adamc@1211 887 val sitem = alt (wrap field SqField)
adamc@1211 888 (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211 889 (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207 890
adamc@1207 891 val select = log "select"
adamc@1207 892 (wrap (follow (const "SELECT ") (list sitem))
adamc@1207 893 (fn ((), ls) => ls))
adamc@1201 894
adamc@1201 895 val fitem = wrap (follow uw_ident
adamc@1201 896 (follow (const " AS ")
adamc@1201 897 t_ident))
adamc@1201 898 (fn (t, ((), f)) => (t, f))
adamc@1201 899
adamc@1207 900 val from = log "from"
adamc@1207 901 (wrap (follow (const "FROM ") (list fitem))
adamc@1207 902 (fn ((), ls) => ls))
adamc@1201 903
adamc@1204 904 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204 905 (fn ((), ls) => ls)
adamc@1204 906
adamc@1207 907 val query = log "query"
adamc@1207 908 (wrap (follow (follow select from) (opt wher))
adamc@1207 909 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201 910
adamc@1211 911 fun removeDups ls =
adamc@1211 912 case ls of
adamc@1211 913 [] => []
adamc@1211 914 | x :: ls =>
adamc@1211 915 let
adamc@1211 916 val ls = removeDups ls
adamc@1211 917 in
adamc@1211 918 if List.exists (fn x' => x' = x) ls then
adamc@1211 919 ls
adamc@1211 920 else
adamc@1211 921 x :: ls
adamc@1211 922 end
adamc@1211 923
adamc@1212 924 datatype queryMode =
adamc@1212 925 SomeCol of exp
adamc@1212 926 | AllCols of exp
adamc@1212 927
adamc@1207 928 fun queryProp env rv oe e =
adamc@1202 929 case parse query e of
adamc@1207 930 NONE => (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1207 931 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1210 932 (Unknown, []))
adamc@1201 933 | SOME r =>
adamc@1202 934 let
adamc@1211 935 fun usedFields e =
adamc@1211 936 case e of
adamc@1211 937 SqConst _ => []
adamc@1211 938 | Field (v, f) => [(v, f)]
adamc@1211 939 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1211 940 | SqKnown _ => []
adamc@1211 941 | Inj _ => []
adamc@1211 942 | SqFunc (_, e) => usedFields e
adamc@1211 943 | Count => []
adamc@1211 944
adamc@1211 945 val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r)
adamc@1211 946 @ (case #Where r of
adamc@1211 947 NONE => []
adamc@1211 948 | SOME e => usedFields e))
adamc@1211 949
adamc@1202 950 val p =
adamc@1202 951 foldl (fn ((t, v), p) =>
adamc@1202 952 And (p,
adamc@1202 953 Reln (Sql t,
adamc@1202 954 [Recd (foldl (fn ((v', f), fs) =>
adamc@1202 955 if v' = v then
adamc@1212 956 (f, Proj (Proj (rv, v), f)) :: fs
adamc@1202 957 else
adamc@1211 958 fs) [] allUsed)])))
adamc@1202 959 True (#From r)
adamc@1205 960
adamc@1205 961 fun expIn e =
adamc@1205 962 case e of
adamc@1206 963 SqConst p => inl (Const p)
adamc@1212 964 | Field (v, f) => inl (Proj (Proj (rv, v), f))
adamc@1205 965 | Binop (bo, e1, e2) =>
adamc@1206 966 inr (case (bo, expIn e1, expIn e2) of
adamc@1206 967 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1206 968 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1206 969 | _ => Unknown)
adamc@1207 970 | SqKnown e =>
adamc@1207 971 inr (case expIn e of
adamc@1207 972 inl e => Reln (Known, [e])
adamc@1207 973 | _ => Unknown)
adamc@1207 974 | Inj e =>
adamc@1207 975 let
adamc@1207 976 fun deinj (e, _) =
adamc@1207 977 case e of
adamc@1207 978 ERel n => List.nth (env, n)
adamc@1207 979 | EField (e, f) => Proj (deinj e, f)
adamc@1207 980 | _ => raise Fail "Iflow: non-variable injected into query"
adamc@1207 981 in
adamc@1207 982 inl (deinj e)
adamc@1207 983 end
adamc@1211 984 | SqFunc (f, e) =>
adamc@1211 985 inl (case expIn e of
adamc@1211 986 inl e => Func (f, [e])
adamc@1211 987 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
adamc@1212 988 | Count => inl (Proj (rv, "$COUNT"))
adamc@1210 989
adamc@1205 990 val p = case #Where r of
adamc@1205 991 NONE => p
adamc@1205 992 | SOME e =>
adamc@1205 993 case expIn e of
adamc@1205 994 inr p' => And (p, p')
adamc@1205 995 | _ => p
adamc@1202 996 in
adamc@1212 997 (And (p, case oe of
adamc@1212 998 SomeCol oe =>
adamc@1212 999 foldl (fn (si, p) =>
adamc@1211 1000 let
adamc@1211 1001 val p' = case si of
adamc@1212 1002 SqField (v, f) => Reln (Eq, [oe, Proj (Proj (rv, v), f)])
adamc@1211 1003 | SqExp (e, f) =>
adamc@1211 1004 case expIn e of
adamc@1211 1005 inr _ => Unknown
adamc@1211 1006 | inl e => Reln (Eq, [oe, e])
adamc@1211 1007 in
adamc@1211 1008 Or (p, p')
adamc@1211 1009 end)
adamc@1212 1010 False (#Select r)
adamc@1212 1011 | AllCols oe =>
adamc@1212 1012 foldl (fn (si, p) =>
adamc@1212 1013 let
adamc@1212 1014 val p' = case si of
adamc@1212 1015 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
adamc@1212 1016 Proj (Proj (rv, v), f)])
adamc@1212 1017 | SqExp (e, f) =>
adamc@1212 1018 case expIn e of
adamc@1212 1019 inr p => Cond (Proj (oe, f), p)
adamc@1212 1020 | inl e => Reln (Eq, [Proj (oe, f), e])
adamc@1212 1021 in
adamc@1212 1022 And (p, p')
adamc@1212 1023 end)
adamc@1212 1024 True (#Select r)),
adamc@1210 1025
adamc@1210 1026 case #Where r of
adamc@1210 1027 NONE => []
adamc@1212 1028 | SOME e => map (fn (v, f) => Proj (Proj (rv, v), f)) (usedFields e))
adamc@1202 1029 end
adamc@1200 1030
adamc@1211 1031 fun evalPat env e (pt, _) =
adamc@1211 1032 case pt of
adamc@1211 1033 PWild => (env, True)
adamc@1211 1034 | PVar _ => (e :: env, True)
adamc@1211 1035 | PPrim _ => (env, True)
adamc@1211 1036 | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e]))
adamc@1211 1037 | PCon (_, pc, SOME pt) =>
adamc@1211 1038 let
adamc@1211 1039 val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt
adamc@1211 1040 in
adamc@1211 1041 (env, And (p, Reln (DtCon (patCon pc), [e])))
adamc@1211 1042 end
adamc@1211 1043 | PRecord xpts =>
adamc@1211 1044 foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211 1045 let
adamc@1211 1046 val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211 1047 in
adamc@1211 1048 (env, And (p', p))
adamc@1211 1049 end) (env, True) xpts
adamc@1211 1050 | PNone _ => (env, Reln (DtCon "None", [e]))
adamc@1211 1051 | PSome (_, pt) =>
adamc@1211 1052 let
adamc@1211 1053 val (env, p) = evalPat env (Func ("unSome", [e])) pt
adamc@1211 1054 in
adamc@1211 1055 (env, And (p, Reln (DtCon "Some", [e])))
adamc@1211 1056 end
adamc@1211 1057
adamc@1211 1058 fun peq (p1, p2) =
adamc@1211 1059 case (p1, p2) of
adamc@1211 1060 (True, True) => true
adamc@1211 1061 | (False, False) => true
adamc@1211 1062 | (Unknown, Unknown) => true
adamc@1211 1063 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1064 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1065 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212 1066 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211 1067 | _ => false
adamc@1211 1068
adamc@1211 1069 fun removeRedundant p1 =
adamc@1211 1070 let
adamc@1211 1071 fun rr p2 =
adamc@1211 1072 if peq (p1, p2) then
adamc@1211 1073 True
adamc@1211 1074 else
adamc@1211 1075 case p2 of
adamc@1211 1076 And (x, y) => And (rr x, rr y)
adamc@1211 1077 | Or (x, y) => Or (rr x, rr y)
adamc@1211 1078 | _ => p2
adamc@1211 1079 in
adamc@1211 1080 rr
adamc@1211 1081 end
adamc@1211 1082
adamc@1202 1083 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
adamc@1200 1084 let
adamc@1200 1085 fun default () =
adamc@1213 1086 ((*Print.preface ("Default" ^ Int.toString nv,
adamc@1213 1087 MonoPrint.p_exp MonoEnv.empty e);*)
adamc@1213 1088 (Var nv, (nv+1, p, sent)))
adamc@1200 1089
adamc@1200 1090 fun addSent (p, e, sent) =
adamc@1200 1091 if isKnown e then
adamc@1200 1092 sent
adamc@1200 1093 else
adamc@1202 1094 (loc, e, p) :: sent
adamc@1200 1095 in
adamc@1200 1096 case #1 e of
adamc@1200 1097 EPrim p => (Const p, st)
adamc@1200 1098 | ERel n => (List.nth (env, n), st)
adamc@1200 1099 | ENamed _ => default ()
adamc@1200 1100 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200 1101 | ECon (_, pc, SOME e) =>
adamc@1200 1102 let
adamc@1200 1103 val (e, st) = evalExp env (e, st)
adamc@1200 1104 in
adamc@1200 1105 (Func (patCon pc, [e]), st)
adamc@1200 1106 end
adamc@1200 1107 | ENone _ => (Func ("None", []), st)
adamc@1200 1108 | ESome (_, e) =>
adamc@1200 1109 let
adamc@1200 1110 val (e, st) = evalExp env (e, st)
adamc@1200 1111 in
adamc@1200 1112 (Func ("Some", [e]), st)
adamc@1200 1113 end
adamc@1200 1114 | EFfi _ => default ()
adamc@1213 1115
adamc@1200 1116 | EFfiApp (m, s, es) =>
adamc@1200 1117 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 1118 let
adamc@1200 1119 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1120 in
adamc@1200 1121 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200 1122 end
adamc@1200 1123 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 1124 default ()
adamc@1200 1125 else
adamc@1200 1126 let
adamc@1200 1127 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1128 in
adamc@1200 1129 (Func (m ^ "." ^ s, es), st)
adamc@1200 1130 end
adamc@1213 1131
adamc@1213 1132 | EApp (e1, e2) =>
adamc@1213 1133 let
adamc@1213 1134 val (e1, st) = evalExp env (e1, st)
adamc@1213 1135 in
adamc@1213 1136 case e1 of
adamc@1213 1137 Finish => (Finish, st)
adamc@1213 1138 | _ => default ()
adamc@1213 1139 end
adamc@1213 1140
adamc@1200 1141 | EAbs _ => default ()
adamc@1200 1142 | EUnop (s, e1) =>
adamc@1200 1143 let
adamc@1200 1144 val (e1, st) = evalExp env (e1, st)
adamc@1200 1145 in
adamc@1200 1146 (Func (s, [e1]), st)
adamc@1200 1147 end
adamc@1200 1148 | EBinop (s, e1, e2) =>
adamc@1200 1149 let
adamc@1200 1150 val (e1, st) = evalExp env (e1, st)
adamc@1200 1151 val (e2, st) = evalExp env (e2, st)
adamc@1200 1152 in
adamc@1200 1153 (Func (s, [e1, e2]), st)
adamc@1200 1154 end
adamc@1200 1155 | ERecord xets =>
adamc@1200 1156 let
adamc@1200 1157 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 1158 let
adamc@1200 1159 val (e, st) = evalExp env (e, st)
adamc@1200 1160 in
adamc@1200 1161 ((x, e), st)
adamc@1200 1162 end) st xets
adamc@1200 1163 in
adamc@1200 1164 (Recd xes, st)
adamc@1200 1165 end
adamc@1200 1166 | EField (e, s) =>
adamc@1200 1167 let
adamc@1200 1168 val (e, st) = evalExp env (e, st)
adamc@1200 1169 in
adamc@1200 1170 (Proj (e, s), st)
adamc@1200 1171 end
adamc@1211 1172 | ECase (e, pes, _) =>
adamc@1211 1173 let
adamc@1211 1174 val (e, st) = evalExp env (e, st)
adamc@1211 1175 val r = #1 st
adamc@1211 1176 val st = (r + 1, #2 st, #3 st)
adamc@1211 1177 val orig = #2 st
adamc@1211 1178
adamc@1211 1179 val st = foldl (fn ((pt, pe), st) =>
adamc@1211 1180 let
adamc@1211 1181 val (env, pp) = evalPat env e pt
adamc@1211 1182 val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st))
adamc@1211 1183
adamc@1211 1184 val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe]))
adamc@1211 1185 in
adamc@1211 1186 (#1 st', Or (#2 st, this), #3 st')
adamc@1211 1187 end) (#1 st, False, #3 st) pes
adamc@1211 1188 in
adamc@1211 1189 (Var r, (#1 st, And (orig, #2 st), #3 st))
adamc@1211 1190 end
adamc@1200 1191 | EStrcat (e1, e2) =>
adamc@1200 1192 let
adamc@1200 1193 val (e1, st) = evalExp env (e1, st)
adamc@1200 1194 val (e2, st) = evalExp env (e2, st)
adamc@1200 1195 in
adamc@1200 1196 (Func ("cat", [e1, e2]), st)
adamc@1200 1197 end
adamc@1200 1198 | EError _ => (Finish, st)
adamc@1200 1199 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 1200 let
adamc@1200 1201 val (b, st) = evalExp env (b, st)
adamc@1200 1202 val (m, st) = evalExp env (m, st)
adamc@1200 1203 in
adamc@1200 1204 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200 1205 end
adamc@1200 1206 | ERedirect (e, _) =>
adamc@1200 1207 let
adamc@1200 1208 val (e, st) = evalExp env (e, st)
adamc@1200 1209 in
adamc@1200 1210 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 1211 end
adamc@1200 1212 | EWrite e =>
adamc@1200 1213 let
adamc@1200 1214 val (e, st) = evalExp env (e, st)
adamc@1200 1215 in
adamc@1200 1216 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 1217 end
adamc@1200 1218 | ESeq (e1, e2) =>
adamc@1200 1219 let
adamc@1200 1220 val (_, st) = evalExp env (e1, st)
adamc@1200 1221 in
adamc@1200 1222 evalExp env (e2, st)
adamc@1200 1223 end
adamc@1200 1224 | ELet (_, _, e1, e2) =>
adamc@1200 1225 let
adamc@1200 1226 val (e1, st) = evalExp env (e1, st)
adamc@1200 1227 in
adamc@1200 1228 evalExp (e1 :: env) (e2, st)
adamc@1200 1229 end
adamc@1200 1230 | EClosure (n, es) =>
adamc@1200 1231 let
adamc@1200 1232 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1233 in
adamc@1200 1234 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200 1235 end
adamc@1200 1236
adamc@1200 1237 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 1238 let
adamc@1200 1239 val (_, st) = evalExp env (q, st)
adamc@1200 1240 val (i, st) = evalExp env (i, st)
adamc@1200 1241
adamc@1200 1242 val r = #1 st
adamc@1212 1243 val rv = #1 st + 1
adamc@1212 1244 val acc = #1 st + 2
adamc@1212 1245 val st' = (#1 st + 3, #2 st, #3 st)
adamc@1200 1246
adamc@1200 1247 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 1248
adamc@1212 1249 val (qp, used) = queryProp env (Var rv) (AllCols (Var r)) q
adamc@1200 1250
adamc@1212 1251 val p' = And (qp, #2 st')
adamc@1200 1252
adamc@1212 1253 val (nvs, p, res) = if varInP acc (#2 st') then
adamc@1212 1254 (#1 st + 1, #2 st, Var r)
adamc@1212 1255 else
adamc@1212 1256 let
adamc@1212 1257 val out = #1 st'
adamc@1210 1258
adamc@1212 1259 val p = Or (Reln (Eq, [Var out, i]),
adamc@1212 1260 And (Reln (Eq, [Var out, b]),
adamc@1212 1261 And (Reln (Gt, [Proj (Var rv, "$COUNT"),
adamc@1212 1262 Const (Prim.Int 0)]),
adamc@1212 1263 p')))
adamc@1212 1264 in
adamc@1212 1265 (out + 1, p, Var out)
adamc@1212 1266 end
adamc@1212 1267
adamc@1212 1268 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (#3 st')
adamc@1210 1269 val sent = map (fn e => (loc, e, p')) used @ sent
adamc@1200 1270 in
adamc@1212 1271 (res, (nvs, p, sent))
adamc@1200 1272 end
adamc@1200 1273 | EDml _ => default ()
adamc@1200 1274 | ENextval _ => default ()
adamc@1200 1275 | ESetval _ => default ()
adamc@1200 1276
adamc@1213 1277 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1213 1278 (Var nv, (nv + 1, And (p, Reln (Known, [Var nv])), sent))
adamc@1213 1279
adamc@1200 1280 | EUnurlify _ => default ()
adamc@1200 1281 | EJavaScript _ => default ()
adamc@1200 1282 | ESignalReturn _ => default ()
adamc@1200 1283 | ESignalBind _ => default ()
adamc@1200 1284 | ESignalSource _ => default ()
adamc@1200 1285 | EServerCall _ => default ()
adamc@1200 1286 | ERecv _ => default ()
adamc@1200 1287 | ESleep _ => default ()
adamc@1200 1288 | ESpawn _ => default ()
adamc@1200 1289 end
adamc@1200 1290
adamc@1200 1291 fun check file =
adamc@1200 1292 let
adamc@1213 1293 val file = MonoReduce.reduce file
adamc@1213 1294 val file = MonoOpt.optimize file
adamc@1213 1295 val file = Fuse.fuse file
adamc@1213 1296 val file = MonoOpt.optimize file
adamc@1213 1297 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 1298
adamc@1207 1299 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 1300 case d of
adamc@1207 1301 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 1302 | _ => exptd) IS.empty file
adamc@1207 1303
adamc@1202 1304 fun decl ((d, _), (vals, pols)) =
adamc@1200 1305 case d of
adamc@1207 1306 DVal (_, n, _, e, _) =>
adamc@1200 1307 let
adamc@1207 1308 val isExptd = IS.member (exptd, n)
adamc@1207 1309
adamc@1207 1310 fun deAbs (e, env, nv, p) =
adamc@1200 1311 case #1 e of
adamc@1207 1312 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207 1313 if isExptd then
adamc@1207 1314 And (p, Reln (Known, [Var nv]))
adamc@1207 1315 else
adamc@1207 1316 p)
adamc@1207 1317 | _ => (e, env, nv, p)
adamc@1200 1318
adamc@1207 1319 val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200 1320
adamc@1207 1321 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
adamc@1200 1322 in
adamc@1207 1323 (sent @ vals, pols)
adamc@1200 1324 end
adamc@1202 1325
adamc@1212 1326 | DPolicy (PolQuery e) => (vals, #1 (queryProp [] (Lvar 0) (SomeCol (Var 0)) e) :: pols)
adamc@1202 1327
adamc@1202 1328 | _ => (vals, pols)
adamc@1202 1329
adamc@1203 1330 val () = reset ()
adamc@1202 1331
adamc@1202 1332 val (vals, pols) = foldl decl ([], []) file
adamc@1200 1333 in
adamc@1207 1334 app (fn (loc, e, p) =>
adamc@1207 1335 let
adamc@1213 1336 fun doOne e =
adamc@1213 1337 let
adamc@1213 1338 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213 1339 in
adamc@1213 1340 if List.exists (fn pol => if imply (p, pol) then
adamc@1213 1341 (if !debug then
adamc@1213 1342 Print.prefaces "Match"
adamc@1213 1343 [("Hyp", p_prop p),
adamc@1213 1344 ("Goal", p_prop pol)]
adamc@1213 1345 else
adamc@1213 1346 ();
adamc@1213 1347 true)
adamc@1213 1348 else
adamc@1213 1349 false) pols then
adamc@1213 1350 ()
adamc@1213 1351 else
adamc@1213 1352 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1213 1353 Print.preface ("The state satisifes this predicate:", p_prop p))
adamc@1213 1354 end
adamc@1213 1355
adamc@1213 1356 fun doAll e =
adamc@1213 1357 case e of
adamc@1213 1358 Const _ => ()
adamc@1213 1359 | Var _ => doOne e
adamc@1213 1360 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1213 1361 | Func (f, es) => if String.isPrefix "un" f then
adamc@1213 1362 doOne e
adamc@1213 1363 else
adamc@1213 1364 app doAll es
adamc@1213 1365 | Recd xes => app (doAll o #2) xes
adamc@1213 1366 | Proj _ => doOne e
adamc@1213 1367 | Finish => ()
adamc@1207 1368 in
adamc@1213 1369 doAll e
adamc@1207 1370 end) vals
adamc@1200 1371 end
adamc@1200 1372
adamc@1213 1373 val check = fn file =>
adamc@1213 1374 let
adamc@1213 1375 val oldInline = Settings.getMonoInline ()
adamc@1213 1376 in
adamc@1213 1377 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 1378 NONE => 1000000
adamc@1213 1379 | SOME n => n);
adamc@1213 1380 check file;
adamc@1213 1381 Settings.setMonoInline oldInline)
adamc@1213 1382 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 1383 raise ex)
adamc@1213 1384 end
adamc@1213 1385
adamc@1200 1386 end
adamc@1213 1387