Mercurial > urweb

annotate src/iflow.sml @ 1210:c5bd970e77a5

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