adamc@1200: (* Copyright (c) 2010, Adam Chlipala adamc@1200: * All rights reserved. adamc@1200: * adamc@1200: * Redistribution and use in source and binary forms, with or without adamc@1200: * modification, are permitted provided that the following conditions are met: adamc@1200: * adamc@1200: * - Redistributions of source code must retain the above copyright notice, adamc@1200: * this list of conditions and the following disclaimer. adamc@1200: * - Redistributions in binary form must reproduce the above copyright notice, adamc@1200: * this list of conditions and the following disclaimer in the documentation adamc@1200: * and/or other materials provided with the distribution. adamc@1200: * - The names of contributors may not be used to endorse or promote products adamc@1200: * derived from this software without specific prior written permission. adamc@1200: * adamc@1200: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@1200: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@1200: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@1200: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@1200: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@1200: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@1200: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@1200: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@1200: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@1200: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@1200: * POSSIBILITY OF SUCH DAMAGE. adamc@1200: *) adamc@1200: adamc@1200: structure Iflow :> IFLOW = struct adamc@1200: adamc@1200: open Mono adamc@1200: adamc@1207: structure IS = IntBinarySet adamc@1202: structure IM = IntBinaryMap adamc@1202: adamc@1200: structure SS = BinarySetFn(struct adamc@1200: type ord_key = string adamc@1200: val compare = String.compare adamc@1200: end) adamc@1200: adamc@1200: val writers = ["htmlifyInt_w", adamc@1200: "htmlifyFloat_w", adamc@1200: "htmlifyString_w", adamc@1200: "htmlifyBool_w", adamc@1200: "htmlifyTime_w", adamc@1200: "attrifyInt_w", adamc@1200: "attrifyFloat_w", adamc@1200: "attrifyString_w", adamc@1200: "attrifyChar_w", adamc@1200: "urlifyInt_w", adamc@1200: "urlifyFloat_w", adamc@1200: "urlifyString_w", adamc@1200: "urlifyBool_w"] adamc@1200: adamc@1200: val writers = SS.addList (SS.empty, writers) adamc@1200: adamc@1200: type lvar = int adamc@1200: adamc@1200: datatype exp = adamc@1200: Const of Prim.t adamc@1200: | Var of int adamc@1200: | Lvar of lvar adamc@1200: | Func of string * exp list adamc@1200: | Recd of (string * exp) list adamc@1200: | Proj of exp * string adamc@1200: | Finish adamc@1200: adamc@1200: datatype reln = adamc@1207: Known adamc@1207: | Sql of string adamc@1211: | DtCon of string adamc@1200: | Eq adamc@1210: | Ne adamc@1210: | Lt adamc@1210: | Le adamc@1210: | Gt adamc@1210: | Ge adamc@1200: adamc@1200: datatype prop = adamc@1200: True adamc@1200: | False adamc@1200: | Unknown adamc@1200: | And of prop * prop adamc@1200: | Or of prop * prop adamc@1200: | Reln of reln * exp list adamc@1200: | Select of int * lvar * lvar * prop * exp adamc@1200: adamc@1200: local adamc@1207: open Print adamc@1207: val string = PD.string adamc@1207: in adamc@1207: adamc@1207: fun p_exp e = adamc@1207: case e of adamc@1207: Const p => Prim.p_t p adamc@1207: | Var n => string ("x" ^ Int.toString n) adamc@1207: | Lvar n => string ("X" ^ Int.toString n) adamc@1207: | Func (f, es) => box [string (f ^ "("), adamc@1207: p_list p_exp es, adamc@1207: string ")"] adamc@1207: | Recd xes => box [string "{", adamc@1210: p_list (fn (x, e) => box [string x, adamc@1207: space, adamc@1207: string "=", adamc@1207: space, adamc@1207: p_exp e]) xes, adamc@1207: string "}"] adamc@1207: | Proj (e, x) => box [p_exp e, adamc@1207: string ("." ^ x)] adamc@1207: | Finish => string "FINISH" adamc@1207: adamc@1210: fun p_bop s es = adamc@1210: case es of adamc@1210: [e1, e2] => box [p_exp e1, adamc@1210: space, adamc@1210: string s, adamc@1210: space, adamc@1210: p_exp e2] adamc@1210: | _ => raise Fail "Iflow.p_bop" adamc@1210: adamc@1207: fun p_reln r es = adamc@1207: case r of adamc@1207: Known => adamc@1207: (case es of adamc@1207: [e] => box [string "known(", adamc@1207: p_exp e, adamc@1207: string ")"] adamc@1207: | _ => raise Fail "Iflow.p_reln: Known") adamc@1207: | Sql s => box [string (s ^ "("), adamc@1207: p_list p_exp es, adamc@1207: string ")"] adamc@1211: | DtCon s => box [string (s ^ "("), adamc@1211: p_list p_exp es, adamc@1211: string ")"] adamc@1210: | Eq => p_bop "=" es adamc@1210: | Ne => p_bop "<>" es adamc@1210: | Lt => p_bop "<" es adamc@1210: | Le => p_bop "<=" es adamc@1210: | Gt => p_bop ">" es adamc@1210: | Ge => p_bop ">=" es adamc@1207: adamc@1207: fun p_prop p = adamc@1207: case p of adamc@1207: True => string "True" adamc@1207: | False => string "False" adamc@1207: | Unknown => string "??" adamc@1207: | And (p1, p2) => box [string "(", adamc@1207: p_prop p1, adamc@1207: string ")", adamc@1207: space, adamc@1207: string "&&", adamc@1207: space, adamc@1207: string "(", adamc@1207: p_prop p2, adamc@1207: string ")"] adamc@1207: | Or (p1, p2) => box [string "(", adamc@1207: p_prop p1, adamc@1207: string ")", adamc@1207: space, adamc@1207: string "||", adamc@1207: space, adamc@1207: string "(", adamc@1207: p_prop p2, adamc@1207: string ")"] adamc@1207: | Reln (r, es) => p_reln r es adamc@1207: | Select (n1, n2, n3, p, e) => box [string ("select(x" ^ Int.toString n1 adamc@1207: ^ ",X" ^ Int.toString n2 adamc@1207: ^ ",X" ^ Int.toString n3 adamc@1207: ^ "){"), adamc@1207: p_prop p, adamc@1207: string "}{", adamc@1207: p_exp e, adamc@1207: string "}"] adamc@1207: adamc@1207: end adamc@1207: adamc@1207: local adamc@1202: val count = ref 1 adamc@1200: in adamc@1200: fun newLvar () = adamc@1200: let adamc@1200: val n = !count adamc@1200: in adamc@1200: count := n + 1; adamc@1200: n adamc@1200: end adamc@1200: end adamc@1200: adamc@1200: fun subExp (v, lv) = adamc@1200: let adamc@1200: fun sub e = adamc@1200: case e of adamc@1200: Const _ => e adamc@1200: | Var v' => if v' = v then Lvar lv else e adamc@1200: | Lvar _ => e adamc@1200: | Func (f, es) => Func (f, map sub es) adamc@1200: | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes) adamc@1200: | Proj (e, s) => Proj (sub e, s) adamc@1200: | Finish => Finish adamc@1200: in adamc@1200: sub adamc@1200: end adamc@1200: adamc@1200: fun subProp (v, lv) = adamc@1200: let adamc@1200: fun sub p = adamc@1200: case p of adamc@1200: True => p adamc@1200: | False => p adamc@1200: | Unknown => p adamc@1200: | And (p1, p2) => And (sub p1, sub p2) adamc@1200: | Or (p1, p2) => Or (sub p1, sub p2) adamc@1200: | Reln (r, es) => Reln (r, map (subExp (v, lv)) es) adamc@1200: | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e) adamc@1200: in adamc@1200: sub adamc@1200: end adamc@1200: adamc@1200: fun isKnown e = adamc@1200: case e of adamc@1200: Const _ => true adamc@1200: | Func (_, es) => List.all isKnown es adamc@1200: | Recd xes => List.all (isKnown o #2) xes adamc@1200: | Proj (e, _) => isKnown e adamc@1200: | _ => false adamc@1200: adamc@1200: fun isFinish e = adamc@1200: case e of adamc@1200: Finish => true adamc@1200: | _ => false adamc@1200: adamc@1208: val unif = ref (IM.empty : exp IM.map) adamc@1208: adamc@1208: fun reset () = unif := IM.empty adamc@1208: fun save () = !unif adamc@1208: fun restore x = unif := x adamc@1208: adamc@1200: fun simplify e = adamc@1200: case e of adamc@1200: Const _ => e adamc@1200: | Var _ => e adamc@1208: | Lvar n => adamc@1208: (case IM.find (!unif, n) of adamc@1208: NONE => e adamc@1208: | SOME e => simplify e) adamc@1200: | Func (f, es) => adamc@1200: let adamc@1200: val es = map simplify es adamc@1211: adamc@1211: fun default () = Func (f, es) adamc@1200: in adamc@1200: if List.exists isFinish es then adamc@1200: Finish adamc@1211: else if String.isPrefix "un" f then adamc@1211: case es of adamc@1211: [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then adamc@1211: e adamc@1211: else adamc@1211: default () adamc@1211: | _ => default () adamc@1200: else adamc@1211: default () adamc@1200: end adamc@1200: | Recd xes => adamc@1200: let adamc@1200: val xes = map (fn (x, e) => (x, simplify e)) xes adamc@1200: in adamc@1200: if List.exists (isFinish o #2) xes then adamc@1200: Finish adamc@1200: else adamc@1200: Recd xes adamc@1200: end adamc@1200: | Proj (e, s) => adamc@1200: (case simplify e of adamc@1200: Recd xes => adamc@1200: getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes) adamc@1200: | e' => adamc@1200: if isFinish e' then adamc@1200: Finish adamc@1200: else adamc@1200: Proj (e', s)) adamc@1200: | Finish => Finish adamc@1200: adamc@1202: fun decomp fals or = adamc@1200: let adamc@1200: fun decomp p k = adamc@1200: case p of adamc@1200: True => k [] adamc@1202: | False => fals adamc@1200: | Unknown => k [] adamc@1200: | And (p1, p2) => adamc@1200: decomp p1 (fn ps1 => adamc@1200: decomp p2 (fn ps2 => adamc@1200: k (ps1 @ ps2))) adamc@1200: | Or (p1, p2) => adamc@1200: or (decomp p1 k, fn () => decomp p2 k) adamc@1200: | Reln x => k [x] adamc@1200: | Select _ => k [] adamc@1200: in adamc@1200: decomp adamc@1200: end adamc@1200: adamc@1202: fun lvarIn lv = adamc@1202: let adamc@1202: fun lvi e = adamc@1202: case e of adamc@1202: Const _ => false adamc@1202: | Var _ => false adamc@1202: | Lvar lv' => lv' = lv adamc@1202: | Func (_, es) => List.exists lvi es adamc@1202: | Recd xes => List.exists (lvi o #2) xes adamc@1202: | Proj (e, _) => lvi e adamc@1202: | Finish => false adamc@1202: in adamc@1202: lvi adamc@1202: end adamc@1202: adamc@1202: fun eq' (e1, e2) = adamc@1202: case (e1, e2) of adamc@1202: (Const p1, Const p2) => Prim.equal (p1, p2) adamc@1202: | (Var n1, Var n2) => n1 = n2 adamc@1202: adamc@1202: | (Lvar n1, _) => adamc@1202: (case IM.find (!unif, n1) of adamc@1202: SOME e1 => eq' (e1, e2) adamc@1202: | NONE => adamc@1202: case e2 of adamc@1202: Lvar n2 => adamc@1202: (case IM.find (!unif, n2) of adamc@1202: SOME e2 => eq' (e1, e2) adamc@1202: | NONE => n1 = n2 adamc@1208: orelse (unif := IM.insert (!unif, n2, e1); adamc@1202: true)) adamc@1202: | _ => adamc@1202: if lvarIn n1 e2 then adamc@1202: false adamc@1202: else adamc@1202: (unif := IM.insert (!unif, n1, e2); adamc@1202: true)) adamc@1202: adamc@1202: | (_, Lvar n2) => adamc@1202: (case IM.find (!unif, n2) of adamc@1202: SOME e2 => eq' (e1, e2) adamc@1202: | NONE => adamc@1202: if lvarIn n2 e1 then adamc@1202: false adamc@1202: else adamc@1202: (unif := IM.insert (!unif, n2, e1); adamc@1202: true)) adamc@1202: adamc@1202: | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2) adamc@1202: | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2) adamc@1202: | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2 adamc@1202: | (Finish, Finish) => true adamc@1202: | _ => false adamc@1202: adamc@1202: fun eq (e1, e2) = adamc@1202: let adamc@1203: val saved = save () adamc@1202: in adamc@1202: if eq' (simplify e1, simplify e2) then adamc@1202: true adamc@1202: else adamc@1203: (restore saved; adamc@1202: false) adamc@1202: end adamc@1202: adamc@1208: val debug = ref false adamc@1208: adamc@1211: fun eeq (e1, e2) = adamc@1211: case (e1, e2) of adamc@1211: (Const p1, Const p2) => Prim.equal (p1, p2) adamc@1211: | (Var n1, Var n2) => n1 = n2 adamc@1211: | (Lvar n1, Lvar n2) => n1 = n2 adamc@1211: | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2) adamc@1211: | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso adamc@1211: List.all (fn (x2, e2) => adamc@1211: List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1 adamc@1211: | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2 adamc@1211: | (Finish, Finish) => true adamc@1211: | _ => false adamc@1211: adamc@1208: (* Congruence closure *) adamc@1208: structure Cc :> sig adamc@1208: type t adamc@1208: val empty : t adamc@1208: val assert : t * exp * exp -> t adamc@1208: val query : t * exp * exp -> bool adamc@1208: val allPeers : t * exp -> exp list adamc@1208: end = struct adamc@1208: adamc@1211: fun eq (e1, e2) = eeq (simplify e1, simplify e2) adamc@1208: adamc@1208: type t = (exp * exp) list adamc@1208: adamc@1208: val empty = [] adamc@1208: adamc@1208: fun lookup (t, e) = adamc@1208: case List.find (fn (e', _) => eq (e', e)) t of adamc@1208: NONE => e adamc@1208: | SOME (_, e2) => lookup (t, e2) adamc@1208: adamc@1208: fun assert (t, e1, e2) = adamc@1208: let adamc@1208: val r1 = lookup (t, e1) adamc@1208: val r2 = lookup (t, e2) adamc@1208: in adamc@1208: if eq (r1, r2) then adamc@1208: t adamc@1208: else adamc@1208: (r1, r2) :: t adamc@1208: end adamc@1208: adamc@1208: open Print adamc@1208: adamc@1208: fun query (t, e1, e2) = adamc@1208: (if !debug then adamc@1208: prefaces "CC query" [("e1", p_exp (simplify e1)), adamc@1208: ("e2", p_exp (simplify e2)), adamc@1208: ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1), adamc@1208: space, adamc@1208: PD.string "->", adamc@1208: space, adamc@1208: p_exp (simplify e2)]) t)] adamc@1208: else adamc@1208: (); adamc@1208: eq (lookup (t, e1), lookup (t, e2))) adamc@1208: adamc@1208: fun allPeers (t, e) = adamc@1208: let adamc@1208: val r = lookup (t, e) adamc@1208: in adamc@1208: r :: List.mapPartial (fn (e1, e2) => adamc@1208: let adamc@1208: val r' = lookup (t, e2) adamc@1208: in adamc@1208: if eq (r, r') then adamc@1208: SOME e1 adamc@1208: else adamc@1208: NONE adamc@1208: end) t adamc@1208: end adamc@1208: adamc@1208: end adamc@1208: adamc@1208: fun rimp cc ((r1, es1), (r2, es2)) = adamc@1202: case (r1, r2) of adamc@1202: (Sql r1', Sql r2') => adamc@1202: r1' = r2' andalso adamc@1202: (case (es1, es2) of adamc@1202: ([Recd xes1], [Recd xes2]) => adamc@1202: let adamc@1203: val saved = save () adamc@1202: in adamc@1202: if List.all (fn (f, e2) => adamc@1203: case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of adamc@1203: NONE => true adamc@1203: | SOME e1 => eq (e1, e2)) xes2 then adamc@1202: true adamc@1202: else adamc@1203: (restore saved; adamc@1202: false) adamc@1202: end adamc@1202: | _ => false) adamc@1202: | (Eq, Eq) => adamc@1202: (case (es1, es2) of adamc@1202: ([x1, y1], [x2, y2]) => adamc@1202: let adamc@1203: val saved = save () adamc@1202: in adamc@1202: if eq (x1, x2) andalso eq (y1, y2) then adamc@1202: true adamc@1202: else adamc@1203: (restore saved; adamc@1208: if eq (x1, y2) andalso eq (y1, x2) then adamc@1208: true adamc@1208: else adamc@1208: (restore saved; adamc@1208: false)) adamc@1202: end adamc@1202: | _ => false) adamc@1207: | (Known, Known) => adamc@1207: (case (es1, es2) of adamc@1208: ([Var v], [e2]) => adamc@1207: let adamc@1208: fun matches e = adamc@1208: case e of adamc@1208: Var v' => v' = v adamc@1208: | Proj (e, _) => matches e adamc@1211: | Func (f, [e]) => String.isPrefix "un" f andalso matches e adamc@1207: | _ => false adamc@1207: in adamc@1208: List.exists matches (Cc.allPeers (cc, e2)) adamc@1207: end adamc@1207: | _ => false) adamc@1202: | _ => false adamc@1202: adamc@1202: fun imply (p1, p2) = adamc@1208: let adamc@1208: fun doOne doKnown = adamc@1208: decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 adamc@1208: (fn hyps => adamc@1208: decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 adamc@1208: (fn goals => adamc@1208: let adamc@1208: val cc = foldl (fn (p, cc) => adamc@1208: case p of adamc@1208: (Eq, [e1, e2]) => Cc.assert (cc, e1, e2) adamc@1208: | _ => cc) Cc.empty hyps adamc@1202: adamc@1208: fun gls goals onFail = adamc@1208: case goals of adamc@1208: [] => true adamc@1208: | g :: goals => adamc@1208: case (doKnown, g) of adamc@1208: (false, (Known, _)) => gls goals onFail adamc@1208: | _ => adamc@1208: let adamc@1208: fun hps hyps = adamc@1208: case hyps of adamc@1208: [] => onFail () adamc@1208: | h :: hyps => adamc@1208: let adamc@1208: val saved = save () adamc@1208: in adamc@1208: if rimp cc (h, g) then adamc@1208: let adamc@1208: val changed = IM.numItems (!unif) adamc@1208: <> IM.numItems saved adamc@1208: in adamc@1208: gls goals (fn () => (restore saved; adamc@1208: changed andalso hps hyps)) adamc@1208: end adamc@1208: else adamc@1208: hps hyps adamc@1208: end adamc@1208: in adamc@1208: (case g of adamc@1208: (Eq, [e1, e2]) => Cc.query (cc, e1, e2) adamc@1208: | _ => false) adamc@1208: orelse hps hyps adamc@1208: end adamc@1208: in adamc@1211: if List.exists (fn (DtCon c1, [e]) => adamc@1211: List.exists (fn (DtCon c2, [e']) => adamc@1211: c1 <> c2 andalso adamc@1211: Cc.query (cc, e, e') adamc@1211: | _ => false) hyps adamc@1211: orelse List.exists (fn Func (c2, []) => c1 <> c2 adamc@1211: | Finish => true adamc@1211: | _ => false) adamc@1211: (Cc.allPeers (cc, e)) adamc@1211: | _ => false) hyps adamc@1211: orelse gls goals (fn () => false) then adamc@1211: true adamc@1211: else adamc@1211: (Print.prefaces "Can't prove" adamc@1211: [("hyps", Print.p_list (fn x => p_prop (Reln x)) hyps), adamc@1211: ("goals", Print.p_list (fn x => p_prop (Reln x)) goals)]; adamc@1211: false) adamc@1208: end)) adamc@1208: in adamc@1208: reset (); adamc@1208: doOne false; adamc@1208: doOne true adamc@1208: end adamc@1200: adamc@1200: fun patCon pc = adamc@1200: case pc of adamc@1200: PConVar n => "C" ^ Int.toString n adamc@1200: | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c adamc@1200: adamc@1202: adamc@1200: adamc@1200: datatype chunk = adamc@1200: String of string adamc@1200: | Exp of Mono.exp adamc@1200: adamc@1200: fun chunkify e = adamc@1200: case #1 e of adamc@1200: EPrim (Prim.String s) => [String s] adamc@1207: | EStrcat (e1, e2) => adamc@1207: let adamc@1207: val chs1 = chunkify e1 adamc@1207: val chs2 = chunkify e2 adamc@1207: in adamc@1207: case chs2 of adamc@1207: String s2 :: chs2' => adamc@1207: (case List.last chs1 of adamc@1207: String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2' adamc@1207: | _ => chs1 @ chs2) adamc@1207: | _ => chs1 @ chs2 adamc@1207: end adamc@1200: | _ => [Exp e] adamc@1200: adamc@1201: type 'a parser = chunk list -> ('a * chunk list) option adamc@1201: adamc@1201: fun always v chs = SOME (v, chs) adamc@1201: adamc@1202: fun parse p s = adamc@1202: case p (chunkify s) of adamc@1201: SOME (v, []) => SOME v adamc@1201: | _ => NONE adamc@1201: adamc@1201: fun const s chs = adamc@1201: case chs of adamc@1201: String s' :: chs => if String.isPrefix s s' then adamc@1201: SOME ((), if size s = size s' then adamc@1201: chs adamc@1201: else adamc@1201: String (String.extract (s', size s, NONE)) :: chs) adamc@1201: else adamc@1201: NONE adamc@1201: | _ => NONE adamc@1201: adamc@1201: fun follow p1 p2 chs = adamc@1201: case p1 chs of adamc@1201: NONE => NONE adamc@1201: | SOME (v1, chs) => adamc@1201: case p2 chs of adamc@1201: NONE => NONE adamc@1201: | SOME (v2, chs) => SOME ((v1, v2), chs) adamc@1201: adamc@1201: fun wrap p f chs = adamc@1201: case p chs of adamc@1201: NONE => NONE adamc@1201: | SOME (v, chs) => SOME (f v, chs) adamc@1201: adamc@1209: fun wrapP p f chs = adamc@1209: case p chs of adamc@1209: NONE => NONE adamc@1209: | SOME (v, chs) => adamc@1209: case f v of adamc@1209: NONE => NONE adamc@1209: | SOME r => SOME (r, chs) adamc@1209: adamc@1201: fun alt p1 p2 chs = adamc@1201: case p1 chs of adamc@1201: NONE => p2 chs adamc@1201: | v => v adamc@1201: adamc@1207: fun altL ps = adamc@1207: case rev ps of adamc@1207: [] => (fn _ => NONE) adamc@1207: | p :: ps => adamc@1207: foldl (fn (p1, p2) => alt p1 p2) p ps adamc@1207: adamc@1204: fun opt p chs = adamc@1204: case p chs of adamc@1204: NONE => SOME (NONE, chs) adamc@1204: | SOME (v, chs) => SOME (SOME v, chs) adamc@1204: adamc@1201: fun skip cp chs = adamc@1201: case chs of adamc@1201: String "" :: chs => skip cp chs adamc@1201: | String s :: chs' => if cp (String.sub (s, 0)) then adamc@1201: skip cp (String (String.extract (s, 1, NONE)) :: chs') adamc@1201: else adamc@1201: SOME ((), chs) adamc@1201: | _ => SOME ((), chs) adamc@1201: adamc@1201: fun keep cp chs = adamc@1201: case chs of adamc@1201: String "" :: chs => keep cp chs adamc@1201: | String s :: chs' => adamc@1201: let adamc@1201: val (befor, after) = Substring.splitl cp (Substring.full s) adamc@1201: in adamc@1201: if Substring.isEmpty befor then adamc@1201: NONE adamc@1201: else adamc@1201: SOME (Substring.string befor, adamc@1201: if Substring.isEmpty after then adamc@1201: chs' adamc@1201: else adamc@1201: String (Substring.string after) :: chs') adamc@1201: end adamc@1201: | _ => NONE adamc@1201: adamc@1204: fun ws p = wrap (follow (skip (fn ch => ch = #" ")) adamc@1204: (follow p (skip (fn ch => ch = #" ")))) (#1 o #2) adamc@1204: adamc@1204: fun log name p chs = adamc@1206: (if !debug then adamc@1206: case chs of adamc@1207: String s :: _ => print (name ^ ": " ^ s ^ "\n") adamc@1206: | _ => print (name ^ ": blocked!\n") adamc@1206: else adamc@1206: (); adamc@1204: p chs) adamc@1201: adamc@1201: fun list p chs = adamc@1207: altL [wrap (follow p (follow (ws (const ",")) (list p))) adamc@1207: (fn (v, ((), ls)) => v :: ls), adamc@1207: wrap (ws p) (fn v => [v]), adamc@1207: always []] chs adamc@1201: adamc@1201: val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_") adamc@1201: adamc@1211: val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then adamc@1211: SOME (String.extract (s, 2, NONE)) adamc@1201: else adamc@1211: NONE) adamc@1211: val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then adamc@1211: SOME (str (Char.toUpper (String.sub (s, 3))) adamc@1211: ^ String.extract (s, 4, NONE)) adamc@1211: else adamc@1211: NONE) adamc@1201: adamc@1211: val field = wrap (follow t_ident adamc@1201: (follow (const ".") adamc@1201: uw_ident)) adamc@1201: (fn (t, ((), f)) => (t, f)) adamc@1201: adamc@1206: datatype Rel = adamc@1206: Exps of exp * exp -> prop adamc@1206: | Props of prop * prop -> prop adamc@1206: adamc@1204: datatype sqexp = adamc@1206: SqConst of Prim.t adamc@1206: | Field of string * string adamc@1206: | Binop of Rel * sqexp * sqexp adamc@1207: | SqKnown of sqexp adamc@1207: | Inj of Mono.exp adamc@1211: | SqFunc of string * sqexp adamc@1211: | Count adamc@1204: adamc@1210: fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2]))) adamc@1210: adamc@1210: val sqbrel = altL [cmp "=" Eq, adamc@1210: cmp "<>" Ne, adamc@1210: cmp "<=" Le, adamc@1210: cmp "<" Lt, adamc@1210: cmp ">=" Ge, adamc@1210: cmp ">" Gt, adamc@1207: wrap (const "AND") (fn () => Props And), adamc@1207: wrap (const "OR") (fn () => Props Or)] adamc@1204: adamc@1204: datatype ('a, 'b) sum = inl of 'a | inr of 'b adamc@1204: adamc@1209: fun string chs = adamc@1206: case chs of adamc@1209: String s :: chs => adamc@1209: if size s >= 2 andalso String.sub (s, 0) = #"'" then adamc@1209: let adamc@1209: fun loop (cs, acc) = adamc@1209: case cs of adamc@1209: [] => NONE adamc@1209: | c :: cs => adamc@1209: if c = #"'" then adamc@1209: SOME (String.implode (rev acc), cs) adamc@1209: else if c = #"\\" then adamc@1209: case cs of adamc@1209: c :: cs => loop (cs, c :: acc) adamc@1209: | _ => raise Fail "Iflow.string: Unmatched backslash escape" adamc@1209: else adamc@1209: loop (cs, c :: acc) adamc@1209: in adamc@1209: case loop (String.explode (String.extract (s, 1, NONE)), []) of adamc@1209: NONE => NONE adamc@1209: | SOME (s, []) => SOME (s, chs) adamc@1209: | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs) adamc@1209: end adamc@1209: else adamc@1209: NONE adamc@1209: | _ => NONE adamc@1206: adamc@1209: val prim = adamc@1209: altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit))) adamc@1209: (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y)))) adamc@1209: (opt (const "::float8"))) #1, adamc@1209: wrap (follow (wrapP (keep Char.isDigit) adamc@1209: (Option.map Prim.Int o Int64.fromString)) adamc@1209: (opt (const "::int8"))) #1, adamc@1209: wrap (follow (opt (const "E")) (follow string (opt (const "::text")))) adamc@1209: (Prim.String o #1 o #2)] adamc@1206: adamc@1207: fun known' chs = adamc@1207: case chs of adamc@1207: Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs) adamc@1207: | _ => NONE adamc@1207: adamc@1207: fun sqlify chs = adamc@1207: case chs of adamc@1207: Exp (EFfiApp ("Basis", f, [e]), _) :: chs => adamc@1207: if String.isPrefix "sqlify" f then adamc@1207: SOME (e, chs) adamc@1207: else adamc@1207: NONE adamc@1207: | _ => NONE adamc@1207: adamc@1211: fun constK s = wrap (const s) (fn () => s) adamc@1211: adamc@1211: val funcName = altL [constK "COUNT", adamc@1211: constK "MIN", adamc@1211: constK "MAX", adamc@1211: constK "SUM", adamc@1211: constK "AVG"] adamc@1211: adamc@1204: fun sqexp chs = adamc@1206: log "sqexp" adamc@1207: (altL [wrap prim SqConst, adamc@1211: wrap field Field, adamc@1207: wrap known SqKnown, adamc@1211: wrap func SqFunc, adamc@1211: wrap (const "COUNT(*)") (fn () => Count), adamc@1207: wrap sqlify Inj, adamc@1211: wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",") adamc@1211: (follow (keep (fn ch => ch <> #")")) (const ")"))))) adamc@1211: (fn ((), (e, _)) => e), adamc@1207: wrap (follow (ws (const "(")) adamc@1207: (follow (wrap adamc@1207: (follow sqexp adamc@1207: (alt adamc@1207: (wrap adamc@1207: (follow (ws sqbrel) adamc@1207: (ws sqexp)) adamc@1207: inl) adamc@1207: (always (inr ())))) adamc@1207: (fn (e1, sm) => adamc@1207: case sm of adamc@1207: inl (bo, e2) => Binop (bo, e1, e2) adamc@1207: | inr () => e1)) adamc@1207: (const ")"))) adamc@1207: (fn ((), (e, ())) => e)]) adamc@1207: chs adamc@1206: adamc@1207: and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")")))) adamc@1211: (fn ((), ((), (e, ()))) => e) chs adamc@1211: adamc@1211: and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")")))) adamc@1211: (fn (f, ((), (e, ()))) => (f, e)) chs adamc@1211: adamc@1211: datatype sitem = adamc@1211: SqField of string * string adamc@1211: | SqExp of sqexp * string adamc@1211: adamc@1211: val sitem = alt (wrap field SqField) adamc@1211: (wrap (follow sqexp (follow (const " AS ") uw_ident)) adamc@1211: (fn (e, ((), s)) => SqExp (e, s))) adamc@1207: adamc@1207: val select = log "select" adamc@1207: (wrap (follow (const "SELECT ") (list sitem)) adamc@1207: (fn ((), ls) => ls)) adamc@1201: adamc@1201: val fitem = wrap (follow uw_ident adamc@1201: (follow (const " AS ") adamc@1201: t_ident)) adamc@1201: (fn (t, ((), f)) => (t, f)) adamc@1201: adamc@1207: val from = log "from" adamc@1207: (wrap (follow (const "FROM ") (list fitem)) adamc@1207: (fn ((), ls) => ls)) adamc@1201: adamc@1204: val wher = wrap (follow (ws (const "WHERE ")) sqexp) adamc@1204: (fn ((), ls) => ls) adamc@1204: adamc@1207: val query = log "query" adamc@1207: (wrap (follow (follow select from) (opt wher)) adamc@1207: (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) adamc@1201: adamc@1211: fun removeDups ls = adamc@1211: case ls of adamc@1211: [] => [] adamc@1211: | x :: ls => adamc@1211: let adamc@1211: val ls = removeDups ls adamc@1211: in adamc@1211: if List.exists (fn x' => x' = x) ls then adamc@1211: ls adamc@1211: else adamc@1211: x :: ls adamc@1211: end adamc@1211: adamc@1207: fun queryProp env rv oe e = adamc@1202: case parse query e of adamc@1207: NONE => (print ("Warning: Information flow checker can't parse SQL query at " adamc@1207: ^ ErrorMsg.spanToString (#2 e) ^ "\n"); adamc@1210: (Unknown, [])) adamc@1201: | SOME r => adamc@1202: let adamc@1211: fun usedFields e = adamc@1211: case e of adamc@1211: SqConst _ => [] adamc@1211: | Field (v, f) => [(v, f)] adamc@1211: | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2) adamc@1211: | SqKnown _ => [] adamc@1211: | Inj _ => [] adamc@1211: | SqFunc (_, e) => usedFields e adamc@1211: | Count => [] adamc@1211: adamc@1211: val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r) adamc@1211: @ (case #Where r of adamc@1211: NONE => [] adamc@1211: | SOME e => usedFields e)) adamc@1211: adamc@1202: val p = adamc@1202: foldl (fn ((t, v), p) => adamc@1202: And (p, adamc@1202: Reln (Sql t, adamc@1202: [Recd (foldl (fn ((v', f), fs) => adamc@1202: if v' = v then adamc@1202: (f, Proj (Proj (Lvar rv, v), f)) :: fs adamc@1202: else adamc@1211: fs) [] allUsed)]))) adamc@1202: True (#From r) adamc@1205: adamc@1205: fun expIn e = adamc@1205: case e of adamc@1206: SqConst p => inl (Const p) adamc@1206: | Field (v, f) => inl (Proj (Proj (Lvar rv, v), f)) adamc@1205: | Binop (bo, e1, e2) => adamc@1206: inr (case (bo, expIn e1, expIn e2) of adamc@1206: (Exps f, inl e1, inl e2) => f (e1, e2) adamc@1206: | (Props f, inr p1, inr p2) => f (p1, p2) adamc@1206: | _ => Unknown) adamc@1207: | SqKnown e => adamc@1207: inr (case expIn e of adamc@1207: inl e => Reln (Known, [e]) adamc@1207: | _ => Unknown) adamc@1207: | Inj e => adamc@1207: let adamc@1207: fun deinj (e, _) = adamc@1207: case e of adamc@1207: ERel n => List.nth (env, n) adamc@1207: | EField (e, f) => Proj (deinj e, f) adamc@1207: | _ => raise Fail "Iflow: non-variable injected into query" adamc@1207: in adamc@1207: inl (deinj e) adamc@1207: end adamc@1211: | SqFunc (f, e) => adamc@1211: inl (case expIn e of adamc@1211: inl e => Func (f, [e]) adamc@1211: | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f)) adamc@1211: | Count => inl (Func ("COUNT", [])) adamc@1210: adamc@1205: val p = case #Where r of adamc@1205: NONE => p adamc@1205: | SOME e => adamc@1205: case expIn e of adamc@1205: inr p' => And (p, p') adamc@1205: | _ => p adamc@1202: in adamc@1210: (case oe of adamc@1210: NONE => p adamc@1210: | SOME oe => adamc@1211: And (p, foldl (fn (si, p) => adamc@1211: let adamc@1211: val p' = case si of adamc@1211: SqField (v, f) => Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]) adamc@1211: | SqExp (e, f) => adamc@1211: case expIn e of adamc@1211: inr _ => Unknown adamc@1211: | inl e => Reln (Eq, [oe, e]) adamc@1211: in adamc@1211: Or (p, p') adamc@1211: end) adamc@1210: False (#Select r)), adamc@1210: adamc@1210: case #Where r of adamc@1210: NONE => [] adamc@1211: | SOME e => map (fn (v, f) => Proj (Proj (Lvar rv, v), f)) (usedFields e)) adamc@1202: end adamc@1200: adamc@1211: fun evalPat env e (pt, _) = adamc@1211: case pt of adamc@1211: PWild => (env, True) adamc@1211: | PVar _ => (e :: env, True) adamc@1211: | PPrim _ => (env, True) adamc@1211: | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e])) adamc@1211: | PCon (_, pc, SOME pt) => adamc@1211: let adamc@1211: val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt adamc@1211: in adamc@1211: (env, And (p, Reln (DtCon (patCon pc), [e]))) adamc@1211: end adamc@1211: | PRecord xpts => adamc@1211: foldl (fn ((x, pt, _), (env, p)) => adamc@1211: let adamc@1211: val (env, p') = evalPat env (Proj (e, x)) pt adamc@1211: in adamc@1211: (env, And (p', p)) adamc@1211: end) (env, True) xpts adamc@1211: | PNone _ => (env, Reln (DtCon "None", [e])) adamc@1211: | PSome (_, pt) => adamc@1211: let adamc@1211: val (env, p) = evalPat env (Func ("unSome", [e])) pt adamc@1211: in adamc@1211: (env, And (p, Reln (DtCon "Some", [e]))) adamc@1211: end adamc@1211: adamc@1211: fun peq (p1, p2) = adamc@1211: case (p1, p2) of adamc@1211: (True, True) => true adamc@1211: | (False, False) => true adamc@1211: | (Unknown, Unknown) => true adamc@1211: | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2) adamc@1211: | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2) adamc@1211: | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2) adamc@1211: | (Select (n1, n2, n3, p1, e1), Select (n1', n2', n3', p2, e2)) => adamc@1211: n1 = n1' andalso n2 = n2' andalso n3 = n3' adamc@1211: andalso peq (p1, p2) andalso eeq (e1, e2) adamc@1211: | _ => false adamc@1211: adamc@1211: fun removeRedundant p1 = adamc@1211: let adamc@1211: fun rr p2 = adamc@1211: if peq (p1, p2) then adamc@1211: True adamc@1211: else adamc@1211: case p2 of adamc@1211: And (x, y) => And (rr x, rr y) adamc@1211: | Or (x, y) => Or (rr x, rr y) adamc@1211: | Select (n1, n2, n3, p, e) => Select (n1, n2, n3, rr p, e) adamc@1211: | _ => p2 adamc@1211: in adamc@1211: rr adamc@1211: end adamc@1211: adamc@1202: fun evalExp env (e as (_, loc), st as (nv, p, sent)) = adamc@1200: let adamc@1200: fun default () = adamc@1200: (Var nv, (nv+1, p, sent)) adamc@1200: adamc@1200: fun addSent (p, e, sent) = adamc@1200: if isKnown e then adamc@1200: sent adamc@1200: else adamc@1202: (loc, e, p) :: sent adamc@1200: in adamc@1200: case #1 e of adamc@1200: EPrim p => (Const p, st) adamc@1200: | ERel n => (List.nth (env, n), st) adamc@1200: | ENamed _ => default () adamc@1200: | ECon (_, pc, NONE) => (Func (patCon pc, []), st) adamc@1200: | ECon (_, pc, SOME e) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: (Func (patCon pc, [e]), st) adamc@1200: end adamc@1200: | ENone _ => (Func ("None", []), st) adamc@1200: | ESome (_, e) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: (Func ("Some", [e]), st) adamc@1200: end adamc@1200: | EFfi _ => default () adamc@1200: | EFfiApp (m, s, es) => adamc@1200: if m = "Basis" andalso SS.member (writers, s) then adamc@1200: let adamc@1200: val (es, st) = ListUtil.foldlMap (evalExp env) st es adamc@1200: in adamc@1200: (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es)) adamc@1200: end adamc@1200: else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then adamc@1200: default () adamc@1200: else adamc@1200: let adamc@1200: val (es, st) = ListUtil.foldlMap (evalExp env) st es adamc@1200: in adamc@1200: (Func (m ^ "." ^ s, es), st) adamc@1200: end adamc@1200: | EApp _ => default () adamc@1200: | EAbs _ => default () adamc@1200: | EUnop (s, e1) => adamc@1200: let adamc@1200: val (e1, st) = evalExp env (e1, st) adamc@1200: in adamc@1200: (Func (s, [e1]), st) adamc@1200: end adamc@1200: | EBinop (s, e1, e2) => adamc@1200: let adamc@1200: val (e1, st) = evalExp env (e1, st) adamc@1200: val (e2, st) = evalExp env (e2, st) adamc@1200: in adamc@1200: (Func (s, [e1, e2]), st) adamc@1200: end adamc@1200: | ERecord xets => adamc@1200: let adamc@1200: val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: ((x, e), st) adamc@1200: end) st xets adamc@1200: in adamc@1200: (Recd xes, st) adamc@1200: end adamc@1200: | EField (e, s) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: (Proj (e, s), st) adamc@1200: end adamc@1211: | ECase (e, pes, _) => adamc@1211: let adamc@1211: val (e, st) = evalExp env (e, st) adamc@1211: val r = #1 st adamc@1211: val st = (r + 1, #2 st, #3 st) adamc@1211: val orig = #2 st adamc@1211: adamc@1211: val st = foldl (fn ((pt, pe), st) => adamc@1211: let adamc@1211: val (env, pp) = evalPat env e pt adamc@1211: val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st)) adamc@1211: adamc@1211: val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe])) adamc@1211: in adamc@1211: (#1 st', Or (#2 st, this), #3 st') adamc@1211: end) (#1 st, False, #3 st) pes adamc@1211: in adamc@1211: (Var r, (#1 st, And (orig, #2 st), #3 st)) adamc@1211: end adamc@1200: | EStrcat (e1, e2) => adamc@1200: let adamc@1200: val (e1, st) = evalExp env (e1, st) adamc@1200: val (e2, st) = evalExp env (e2, st) adamc@1200: in adamc@1200: (Func ("cat", [e1, e2]), st) adamc@1200: end adamc@1200: | EError _ => (Finish, st) adamc@1200: | EReturnBlob {blob = b, mimeType = m, ...} => adamc@1200: let adamc@1200: val (b, st) = evalExp env (b, st) adamc@1200: val (m, st) = evalExp env (m, st) adamc@1200: in adamc@1200: (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent)))) adamc@1200: end adamc@1200: | ERedirect (e, _) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: (Finish, (#1 st, p, addSent (#2 st, e, sent))) adamc@1200: end adamc@1200: | EWrite e => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1200: (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent))) adamc@1200: end adamc@1200: | ESeq (e1, e2) => adamc@1200: let adamc@1200: val (_, st) = evalExp env (e1, st) adamc@1200: in adamc@1200: evalExp env (e2, st) adamc@1200: end adamc@1200: | ELet (_, _, e1, e2) => adamc@1200: let adamc@1200: val (e1, st) = evalExp env (e1, st) adamc@1200: in adamc@1200: evalExp (e1 :: env) (e2, st) adamc@1200: end adamc@1200: | EClosure (n, es) => adamc@1200: let adamc@1200: val (es, st) = ListUtil.foldlMap (evalExp env) st es adamc@1200: in adamc@1200: (Func ("Cl" ^ Int.toString n, es), st) adamc@1200: end adamc@1200: adamc@1200: | EQuery {query = q, body = b, initial = i, ...} => adamc@1200: let adamc@1200: val (_, st) = evalExp env (q, st) adamc@1200: val (i, st) = evalExp env (i, st) adamc@1200: adamc@1200: val r = #1 st adamc@1200: val acc = #1 st + 1 adamc@1200: val st' = (#1 st + 2, #2 st, #3 st) adamc@1200: adamc@1200: val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') adamc@1200: adamc@1200: val r' = newLvar () adamc@1200: val acc' = newLvar () adamc@1210: val (qp, used) = queryProp env r' NONE q adamc@1200: adamc@1200: val doSubExp = subExp (r, r') o subExp (acc, acc') adamc@1200: val doSubProp = subProp (r, r') o subProp (acc, acc') adamc@1200: adamc@1200: val p = doSubProp (#2 st') adamc@1210: val p' = And (p, qp) adamc@1210: val p = Select (r, r', acc', p', doSubExp b) adamc@1210: adamc@1210: val sent = map (fn (loc, e, p) => (loc, adamc@1210: doSubExp e, adamc@1210: And (qp, doSubProp p))) (#3 st') adamc@1210: val sent = map (fn e => (loc, e, p')) used @ sent adamc@1200: in adamc@1210: (Var r, (#1 st + 1, And (#2 st, p), sent)) adamc@1200: end adamc@1200: | EDml _ => default () adamc@1200: | ENextval _ => default () adamc@1200: | ESetval _ => default () adamc@1200: adamc@1200: | EUnurlify _ => default () adamc@1200: | EJavaScript _ => default () adamc@1200: | ESignalReturn _ => default () adamc@1200: | ESignalBind _ => default () adamc@1200: | ESignalSource _ => default () adamc@1200: | EServerCall _ => default () adamc@1200: | ERecv _ => default () adamc@1200: | ESleep _ => default () adamc@1200: | ESpawn _ => default () adamc@1200: end adamc@1200: adamc@1200: fun check file = adamc@1200: let adamc@1207: val exptd = foldl (fn ((d, _), exptd) => adamc@1207: case d of adamc@1207: DExport (_, _, n, _, _, _) => IS.add (exptd, n) adamc@1207: | _ => exptd) IS.empty file adamc@1207: adamc@1202: fun decl ((d, _), (vals, pols)) = adamc@1200: case d of adamc@1207: DVal (_, n, _, e, _) => adamc@1200: let adamc@1207: val isExptd = IS.member (exptd, n) adamc@1207: adamc@1207: fun deAbs (e, env, nv, p) = adamc@1200: case #1 e of adamc@1207: EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1, adamc@1207: if isExptd then adamc@1207: And (p, Reln (Known, [Var nv])) adamc@1207: else adamc@1207: p) adamc@1207: | _ => (e, env, nv, p) adamc@1200: adamc@1207: val (e, env, nv, p) = deAbs (e, [], 1, True) adamc@1200: adamc@1207: val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) adamc@1200: in adamc@1207: (sent @ vals, pols) adamc@1200: end adamc@1202: adamc@1210: | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols) adamc@1202: adamc@1202: | _ => (vals, pols) adamc@1202: adamc@1203: val () = reset () adamc@1202: adamc@1202: val (vals, pols) = foldl decl ([], []) file adamc@1200: in adamc@1207: app (fn (loc, e, p) => adamc@1207: let adamc@1207: val p = And (p, Reln (Eq, [Var 0, e])) adamc@1207: in adamc@1208: if List.exists (fn pol => if imply (p, pol) then adamc@1208: (if !debug then adamc@1208: Print.prefaces "Match" adamc@1208: [("Hyp", p_prop p), adamc@1208: ("Goal", p_prop pol)] adamc@1208: else adamc@1208: (); adamc@1208: true) adamc@1208: else adamc@1208: false) pols then adamc@1207: () adamc@1207: else adamc@1207: (ErrorMsg.errorAt loc "The information flow policy may be violated here."; adamc@1207: Print.preface ("The state satisifes this predicate:", p_prop p)) adamc@1207: end) vals adamc@1200: end adamc@1200: adamc@1200: end