Mercurial > urweb

annotate src/iflow.sml @ 1207:ae3036773768

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