Mercurial > urweb

annotate src/iflow.sml @ 1211:1d4d65245dd3

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