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@1215: structure SK = struct adamc@1215: type ord_key = string adamc@1215: val compare = String.compare adamc@1215: end adamc@1215: adamc@1215: structure SS = BinarySetFn(SK) adamc@1215: structure SM = BinaryMapFn(SK) 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@1213: "urlifyBool_w", adamc@1213: "set_cookie"] adamc@1200: adamc@1200: val writers = SS.addList (SS.empty, writers) adamc@1200: adamc@1200: type lvar = int adamc@1200: adamc@1215: datatype func = adamc@1215: DtCon0 of string adamc@1215: | DtCon1 of string adamc@1215: | UnCon of string adamc@1215: | Other of string adamc@1215: adamc@1200: datatype exp = adamc@1200: Const of Prim.t adamc@1200: | Var of int adamc@1200: | Lvar of lvar adamc@1215: | Func of func * 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@1215: | PCon0 of string adamc@1215: | PCon1 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@1212: | Cond of exp * prop adamc@1200: adamc@1215: val unif = ref (IM.empty : exp IM.map) adamc@1215: adamc@1215: fun reset () = unif := IM.empty adamc@1215: fun save () = !unif adamc@1215: fun restore x = unif := x adamc@1215: adamc@1200: local adamc@1207: open Print adamc@1207: val string = PD.string adamc@1207: in adamc@1207: adamc@1215: fun p_func f = adamc@1215: string (case f of adamc@1215: DtCon0 s => s adamc@1215: | DtCon1 s => s adamc@1215: | UnCon s => "un" ^ s adamc@1215: | Other s => s) adamc@1215: 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@1215: | Lvar n => adamc@1215: (case IM.find (!unif, n) of adamc@1215: NONE => string ("X" ^ Int.toString n) adamc@1215: | SOME e => p_exp e) adamc@1215: | Func (f, es) => box [p_func f, adamc@1215: string "(", 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@1215: | PCon0 s => box [string (s ^ "("), adamc@1215: p_list p_exp es, adamc@1215: string ")"] adamc@1215: | PCon1 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@1212: | Cond (e, p) => box [string "(", adamc@1212: p_exp e, adamc@1212: space, adamc@1212: string "==", adamc@1212: space, adamc@1212: p_prop p, adamc@1212: 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 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@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@1215: | Func (f, es) => Func (f, map simplify es) adamc@1215: | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes) adamc@1215: | Proj (e, s) => Proj (simplify e, s) adamc@1200: | Finish => Finish adamc@1200: adamc@1212: datatype atom = adamc@1212: AReln of reln * exp list adamc@1212: | ACond of exp * prop adamc@1212: adamc@1212: fun p_atom a = adamc@1212: p_prop (case a of adamc@1212: AReln x => Reln x adamc@1212: | ACond x => Cond x) adamc@1212: 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@1212: fun lvarInP lv = adamc@1212: let adamc@1212: fun lvi p = adamc@1212: case p of adamc@1212: True => false adamc@1212: | False => false adamc@1212: | Unknown => true adamc@1212: | And (p1, p2) => lvi p1 orelse lvi p2 adamc@1212: | Or (p1, p2) => lvi p1 orelse lvi p2 adamc@1212: | Reln (_, es) => List.exists (lvarIn lv) es adamc@1212: | Cond (e, p) => lvarIn lv e orelse lvi p adamc@1212: in adamc@1212: lvi adamc@1212: end adamc@1212: adamc@1212: fun varIn lv = adamc@1212: let adamc@1212: fun lvi e = adamc@1212: case e of adamc@1212: Const _ => false adamc@1212: | Lvar _ => false adamc@1212: | Var lv' => lv' = lv adamc@1212: | Func (_, es) => List.exists lvi es adamc@1212: | Recd xes => List.exists (lvi o #2) xes adamc@1212: | Proj (e, _) => lvi e adamc@1212: | Finish => false adamc@1212: in adamc@1212: lvi adamc@1212: end adamc@1212: adamc@1212: fun varInP lv = adamc@1212: let adamc@1212: fun lvi p = adamc@1212: case p of adamc@1212: True => false adamc@1212: | False => false adamc@1212: | Unknown => false adamc@1212: | And (p1, p2) => lvi p1 orelse lvi p2 adamc@1212: | Or (p1, p2) => lvi p1 orelse lvi p2 adamc@1212: | Reln (_, es) => List.exists (varIn lv) es adamc@1212: | Cond (e, p) => varIn lv e orelse lvi p adamc@1212: in adamc@1212: lvi adamc@1212: end adamc@1212: 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@1213: ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)), adamc@1213: ("e1", p_exp e1)];*) adamc@1213: 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@1215: type database adamc@1215: adamc@1215: exception Contradiction adamc@1215: exception Undetermined adamc@1215: adamc@1215: val database : unit -> database adamc@1215: adamc@1215: val assert : database * atom -> unit adamc@1215: val check : database * atom -> bool adamc@1215: adamc@1215: val p_database : database Print.printer adamc@1218: adamc@1218: val builtFrom : database * {Base : exp list, Derived : exp} -> bool adamc@1226: adamc@1226: val p_repOf : database -> exp Print.printer adamc@1208: end = struct adamc@1208: adamc@1215: exception Contradiction adamc@1215: exception Undetermined adamc@1208: adamc@1215: structure CM = BinaryMapFn(struct adamc@1215: type ord_key = Prim.t adamc@1215: val compare = Prim.compare adamc@1215: end) adamc@1208: adamc@1215: datatype node = Node of {Rep : node ref option ref, adamc@1215: Cons : node ref SM.map ref, adamc@1215: Variety : variety, adamc@1215: Known : bool ref} adamc@1208: adamc@1215: and variety = adamc@1215: Dt0 of string adamc@1215: | Dt1 of string * node ref adamc@1215: | Prim of Prim.t adamc@1221: | Recrd of node ref SM.map ref * bool adamc@1215: | Nothing adamc@1208: adamc@1215: type representative = node ref adamc@1215: adamc@1215: type database = {Vars : representative IM.map ref, adamc@1215: Consts : representative CM.map ref, adamc@1215: Con0s : representative SM.map ref, adamc@1215: Records : (representative SM.map * representative) list ref, adamc@1215: Funcs : ((string * representative list) * representative) list ref } adamc@1215: adamc@1215: fun database () = {Vars = ref IM.empty, adamc@1215: Consts = ref CM.empty, adamc@1215: Con0s = ref SM.empty, adamc@1215: Records = ref [], adamc@1215: Funcs = ref []} adamc@1215: adamc@1215: fun unNode n = adamc@1215: case !n of adamc@1215: Node r => r adamc@1215: adamc@1215: open Print adamc@1215: val string = PD.string adamc@1215: val newline = PD.newline adamc@1215: adamc@1215: fun p_rep n = adamc@1215: case !(#Rep (unNode n)) of adamc@1215: SOME n => p_rep n adamc@1215: | NONE => adamc@1221: box [string (Int.toString (Unsafe.cast n) ^ ":"), adamc@1221: space, adamc@1221: case #Variety (unNode n) of adamc@1221: Nothing => string "?" adamc@1221: | Dt0 s => string ("Dt0(" ^ s ^ ")") adamc@1221: | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), adamc@1221: space, adamc@1221: p_rep n, adamc@1221: string ")"] adamc@1221: | Prim p => Prim.p_t p adamc@1221: | Recrd (ref m, b) => box [string "{", adamc@1221: p_list (fn (x, n) => box [string x, adamc@1221: space, adamc@1221: string "=", adamc@1221: space, adamc@1221: p_rep n]) (SM.listItemsi m), adamc@1221: string "}", adamc@1221: if b then adamc@1221: box [space, adamc@1221: string "(complete)"] adamc@1221: else adamc@1226: box []]] adamc@1215: adamc@1215: fun p_database (db : database) = adamc@1215: box [string "Vars:", adamc@1215: newline, adamc@1215: p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i), adamc@1215: space, adamc@1215: string "=", adamc@1215: space, adamc@1218: p_rep n, adamc@1218: if !(#Known (unNode n)) then adamc@1218: box [space, adamc@1218: string "(known)"] adamc@1218: else adamc@1218: box []]) (IM.listItemsi (!(#Vars db)))] adamc@1215: adamc@1215: fun repOf (n : representative) : representative = adamc@1215: case !(#Rep (unNode n)) of adamc@1215: NONE => n adamc@1215: | SOME r => adamc@1215: let adamc@1215: val r = repOf r adamc@1215: in adamc@1215: #Rep (unNode n) := SOME r; adamc@1215: r adamc@1215: end adamc@1215: adamc@1215: fun markKnown r = adamc@1221: let adamc@1221: val r = repOf r adamc@1221: in adamc@1221: (*Print.preface ("markKnown", p_rep r);*) adamc@1221: if !(#Known (unNode r)) then adamc@1221: ()(*TextIO.print "Already known\n"*) adamc@1221: else adamc@1221: (#Known (unNode r) := true; adamc@1221: SM.app markKnown (!(#Cons (unNode r))); adamc@1221: case #Variety (unNode r) of adamc@1221: Dt1 (_, r) => markKnown r adamc@1221: | Recrd (xes, _) => SM.app markKnown (!xes) adamc@1221: | _ => ()) adamc@1221: end adamc@1215: adamc@1215: fun representative (db : database, e) = adamc@1208: let adamc@1215: fun rep e = adamc@1215: case e of adamc@1215: Const p => (case CM.find (!(#Consts db), p) of adamc@1215: SOME r => repOf r adamc@1215: | NONE => adamc@1215: let adamc@1215: val r = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Prim p, adamc@1219: Known = ref true}) adamc@1215: in adamc@1215: #Consts db := CM.insert (!(#Consts db), p, r); adamc@1215: r adamc@1215: end) adamc@1215: | Var n => (case IM.find (!(#Vars db), n) of adamc@1215: SOME r => repOf r adamc@1215: | NONE => adamc@1215: let adamc@1215: val r = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1215: Known = ref false}) adamc@1215: in adamc@1215: #Vars db := IM.insert (!(#Vars db), n, r); adamc@1215: r adamc@1215: end) adamc@1215: | Lvar n => adamc@1215: (case IM.find (!unif, n) of adamc@1215: NONE => raise Undetermined adamc@1215: | SOME e => rep e) adamc@1215: | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of adamc@1215: SOME r => repOf r adamc@1215: | NONE => adamc@1215: let adamc@1215: val r = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt0 f, adamc@1218: Known = ref true}) adamc@1215: in adamc@1215: #Con0s db := SM.insert (!(#Con0s db), f, r); adamc@1215: r adamc@1215: end) adamc@1215: | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0" adamc@1215: | Func (DtCon1 f, [e]) => adamc@1215: let adamc@1215: val r = rep e adamc@1215: in adamc@1215: case SM.find (!(#Cons (unNode r)), f) of adamc@1215: SOME r => repOf r adamc@1215: | NONE => adamc@1215: let adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt1 (f, r), adamc@1221: Known = ref (!(#Known (unNode r)))}) adamc@1215: in adamc@1215: #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r'); adamc@1215: r' adamc@1215: end adamc@1215: end adamc@1215: | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1" adamc@1215: | Func (UnCon f, [e]) => adamc@1215: let adamc@1215: val r = rep e adamc@1215: in adamc@1215: case #Variety (unNode r) of adamc@1215: Dt1 (f', n) => if f' = f then adamc@1215: repOf n adamc@1215: else adamc@1215: raise Contradiction adamc@1215: | Nothing => adamc@1215: let adamc@1215: val cons = ref SM.empty adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = cons, adamc@1215: Variety = Nothing, adamc@1221: Known = ref (!(#Known (unNode r)))}) adamc@1215: adamc@1215: val r'' = ref (Node {Rep = ref NONE, adamc@1215: Cons = #Cons (unNode r), adamc@1215: Variety = Dt1 (f, r'), adamc@1215: Known = #Known (unNode r)}) adamc@1215: in adamc@1215: cons := SM.insert (!cons, f, r''); adamc@1215: #Rep (unNode r) := SOME r''; adamc@1215: r' adamc@1215: end adamc@1215: | _ => raise Contradiction adamc@1215: end adamc@1215: | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon" adamc@1215: | Func (Other f, es) => adamc@1215: let adamc@1215: val rs = map rep es adamc@1215: in adamc@1215: case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of adamc@1215: NONE => adamc@1215: let adamc@1215: val r = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1215: Known = ref false}) adamc@1215: in adamc@1215: #Funcs db := ((f, rs), r) :: (!(#Funcs db)); adamc@1215: r adamc@1215: end adamc@1215: | SOME (_, r) => repOf r adamc@1215: end adamc@1215: | Recd xes => adamc@1215: let adamc@1215: val xes = map (fn (x, e) => (x, rep e)) xes adamc@1215: val len = length xes adamc@1215: in adamc@1215: case List.find (fn (xes', _) => adamc@1215: SM.numItems xes' = len adamc@1215: andalso List.all (fn (x, n) => adamc@1215: case SM.find (xes', x) of adamc@1215: NONE => false adamc@1215: | SOME n' => n = repOf n') xes) adamc@1215: (!(#Records db)) of adamc@1215: SOME (_, r) => repOf r adamc@1215: | NONE => adamc@1215: let adamc@1215: val xes = foldl SM.insert' SM.empty xes adamc@1215: adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1221: Variety = Recrd (ref xes, true), adamc@1215: Known = ref false}) adamc@1215: in adamc@1215: #Records db := (xes, r') :: (!(#Records db)); adamc@1215: r' adamc@1215: end adamc@1215: end adamc@1215: | Proj (e, f) => adamc@1215: let adamc@1215: val r = rep e adamc@1215: in adamc@1215: case #Variety (unNode r) of adamc@1221: Recrd (xes, _) => adamc@1215: (case SM.find (!xes, f) of adamc@1215: SOME r => repOf r adamc@1216: | NONE => let adamc@1215: val r = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1221: Known = ref (!(#Known (unNode r)))}) adamc@1215: in adamc@1215: xes := SM.insert (!xes, f, r); adamc@1215: r adamc@1215: end) adamc@1215: | Nothing => adamc@1215: let adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1221: Known = ref (!(#Known (unNode r)))}) adamc@1215: adamc@1215: val r'' = ref (Node {Rep = ref NONE, adamc@1215: Cons = #Cons (unNode r), adamc@1221: Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false), adamc@1215: Known = #Known (unNode r)}) adamc@1215: in adamc@1215: #Rep (unNode r) := SOME r''; adamc@1215: r' adamc@1215: end adamc@1215: | _ => raise Contradiction adamc@1215: end adamc@1226: | Finish => raise Contradiction adamc@1208: in adamc@1215: rep e adamc@1208: end adamc@1208: adamc@1226: fun p_repOf db e = p_rep (representative (db, e)) adamc@1226: adamc@1215: fun assert (db, a) = adamc@1215: case a of adamc@1215: ACond _ => () adamc@1215: | AReln x => adamc@1215: case x of adamc@1221: (Known, [e]) => adamc@1221: ((*Print.prefaces "Before" [("e", p_exp e), adamc@1221: ("db", p_database db)];*) adamc@1221: markKnown (representative (db, e))(*; adamc@1221: Print.prefaces "After" [("e", p_exp e), adamc@1221: ("db", p_database db)]*)) adamc@1215: | (PCon0 f, [e]) => adamc@1215: let adamc@1215: val r = representative (db, e) adamc@1215: in adamc@1215: case #Variety (unNode r) of adamc@1215: Dt0 f' => if f = f' then adamc@1215: () adamc@1215: else adamc@1215: raise Contradiction adamc@1215: | Nothing => adamc@1215: let adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt0 f, adamc@1215: Known = ref false}) adamc@1215: in adamc@1215: #Rep (unNode r) := SOME r' adamc@1215: end adamc@1215: | _ => raise Contradiction adamc@1215: end adamc@1215: | (PCon1 f, [e]) => adamc@1215: let adamc@1215: val r = representative (db, e) adamc@1215: in adamc@1215: case #Variety (unNode r) of adamc@1215: Dt1 (f', e') => if f = f' then adamc@1215: () adamc@1215: else adamc@1215: raise Contradiction adamc@1215: | Nothing => adamc@1215: let adamc@1215: val r'' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1215: Known = ref false}) adamc@1214: adamc@1215: val r' = ref (Node {Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt1 (f, r''), adamc@1215: Known = ref false}) adamc@1215: in adamc@1215: #Rep (unNode r) := SOME r' adamc@1215: end adamc@1215: | _ => raise Contradiction adamc@1215: end adamc@1215: | (Eq, [e1, e2]) => adamc@1215: let adamc@1215: fun markEq (r1, r2) = adamc@1226: let adamc@1226: val r1 = repOf r1 adamc@1226: val r2 = repOf r2 adamc@1226: in adamc@1226: if r1 = r2 then adamc@1226: () adamc@1226: else case (#Variety (unNode r1), #Variety (unNode r2)) of adamc@1226: (Prim p1, Prim p2) => if Prim.equal (p1, p2) then adamc@1226: () adamc@1226: else adamc@1226: raise Contradiction adamc@1226: | (Dt0 f1, Dt0 f2) => if f1 = f2 then adamc@1226: () adamc@1226: else adamc@1226: raise Contradiction adamc@1226: | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then adamc@1226: markEq (r1, r2) adamc@1226: else adamc@1226: raise Contradiction adamc@1226: | (Recrd (xes1, _), Recrd (xes2, _)) => adamc@1226: let adamc@1226: fun unif (xes1, xes2) = adamc@1226: SM.appi (fn (x, r1) => adamc@1226: case SM.find (!xes2, x) of adamc@1226: NONE => xes2 := SM.insert (!xes2, x, r1) adamc@1226: | SOME r2 => markEq (r1, r2)) (!xes1) adamc@1226: in adamc@1226: unif (xes1, xes2); adamc@1226: unif (xes2, xes1) adamc@1226: end adamc@1226: | (Nothing, _) => mergeNodes (r1, r2) adamc@1226: | (_, Nothing) => mergeNodes (r2, r1) adamc@1226: | _ => raise Contradiction adamc@1226: end adamc@1214: adamc@1218: and mergeNodes (r1, r2) = adamc@1218: (#Rep (unNode r1) := SOME r2; adamc@1218: if !(#Known (unNode r1)) then adamc@1218: markKnown r2 adamc@1218: else adamc@1218: (); adamc@1218: if !(#Known (unNode r2)) then adamc@1218: markKnown r1 adamc@1218: else adamc@1218: (); adamc@1218: #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1))); adamc@1218: compactFuncs ()) adamc@1218: adamc@1215: and compactFuncs () = adamc@1214: let adamc@1215: fun loop funcs = adamc@1215: case funcs of adamc@1215: [] => [] adamc@1215: | (fr as ((f, rs), r)) :: rest => adamc@1215: let adamc@1215: val rest = List.filter (fn ((f' : string, rs'), r') => adamc@1215: if f' = f adamc@1215: andalso ListPair.allEq (fn (r1, r2) => adamc@1215: repOf r1 = repOf r2) adamc@1215: (rs, rs') then adamc@1215: (markEq (r, r'); adamc@1215: false) adamc@1215: else adamc@1215: true) rest adamc@1215: in adamc@1215: fr :: loop rest adamc@1215: end adamc@1214: in adamc@1215: #Funcs db := loop (!(#Funcs db)) adamc@1214: end adamc@1215: in adamc@1215: markEq (representative (db, e1), representative (db, e2)) adamc@1215: end adamc@1215: | _ => () adamc@1214: adamc@1215: fun check (db, a) = adamc@1215: case a of adamc@1215: ACond _ => false adamc@1215: | AReln x => adamc@1215: case x of adamc@1221: (Known, [e]) => adamc@1221: let adamc@1221: fun isKnown r = adamc@1221: let adamc@1221: val r = repOf r adamc@1221: in adamc@1221: !(#Known (unNode r)) adamc@1221: orelse case #Variety (unNode r) of adamc@1221: Dt1 (_, r) => isKnown r adamc@1221: | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes)) adamc@1221: | _ => false adamc@1221: end adamc@1221: adamc@1221: val r = representative (db, e) adamc@1221: in adamc@1221: isKnown r adamc@1221: end adamc@1215: | (PCon0 f, [e]) => adamc@1215: (case #Variety (unNode (representative (db, e))) of adamc@1215: Dt0 f' => f' = f adamc@1215: | _ => false) adamc@1215: | (PCon1 f, [e]) => adamc@1215: (case #Variety (unNode (representative (db, e))) of adamc@1215: Dt1 (f', _) => f' = f adamc@1215: | _ => false) adamc@1215: | (Eq, [e1, e2]) => adamc@1214: let adamc@1215: val r1 = representative (db, e1) adamc@1215: val r2 = representative (db, e2) adamc@1214: in adamc@1215: repOf r1 = repOf r2 adamc@1214: end adamc@1215: | _ => false adamc@1212: adamc@1218: fun builtFrom (db, {Base = bs, Derived = d}) = adamc@1218: let adamc@1218: val bs = map (fn b => representative (db, b)) bs adamc@1218: adamc@1218: fun loop d = adamc@1218: let adamc@1218: val d = repOf d adamc@1218: in adamc@1218: List.exists (fn b => repOf b = d) bs adamc@1218: orelse case #Variety (unNode d) of adamc@1218: Dt0 _ => true adamc@1218: | Dt1 (_, d) => loop d adamc@1218: | Prim _ => true adamc@1221: | Recrd (xes, _) => List.all loop (SM.listItems (!xes)) adamc@1218: | Nothing => false adamc@1218: end adamc@1218: in adamc@1218: loop (representative (db, d)) adamc@1218: end adamc@1218: adamc@1208: end adamc@1208: adamc@1215: fun decomp fals or = adamc@1215: let adamc@1215: fun decomp p k = adamc@1215: case p of adamc@1215: True => k [] adamc@1215: | False => fals adamc@1215: | Unknown => k [] adamc@1215: | And (p1, p2) => adamc@1215: decomp p1 (fn ps1 => adamc@1215: decomp p2 (fn ps2 => adamc@1215: k (ps1 @ ps2))) adamc@1215: | Or (p1, p2) => adamc@1215: or (decomp p1 k, fn () => decomp p2 k) adamc@1215: | Reln x => k [AReln x] adamc@1215: | Cond x => k [ACond x] adamc@1215: in adamc@1215: decomp adamc@1215: end adamc@1202: adamc@1226: val tabs = ref (SM.empty : (string list * string list list) SM.map) adamc@1226: adamc@1218: fun imply (hyps, goals, outs) = adamc@1218: let adamc@1218: fun gls goals onFail acc = adamc@1218: case goals of adamc@1218: [] => adamc@1218: (let adamc@1218: val cc = Cc.database () adamc@1218: val () = app (fn a => Cc.assert (cc, a)) hyps adamc@1226: adamc@1226: (* Take advantage of table key information *) adamc@1226: fun findKeys hyps = adamc@1226: case hyps of adamc@1226: [] => () adamc@1226: | AReln (Sql tab, [r1]) :: hyps => adamc@1226: (case SM.find (!tabs, tab) of adamc@1226: NONE => findKeys hyps adamc@1226: | SOME (_, []) => findKeys hyps adamc@1226: | SOME (_, ks) => adamc@1226: let adamc@1226: fun finder hyps = adamc@1226: case hyps of adamc@1226: [] => () adamc@1226: | AReln (Sql tab', [r2]) :: hyps => adamc@1226: (if tab' = tab andalso adamc@1226: List.exists (List.all (fn f => adamc@1226: let adamc@1226: val r = adamc@1226: Cc.check (cc, adamc@1226: AReln (Eq, [Proj (r1, f), adamc@1226: Proj (r2, f)])) adamc@1226: in adamc@1226: (*Print.prefaces "Fs" adamc@1226: [("tab", adamc@1226: Print.PD.string tab), adamc@1226: ("r1", adamc@1226: p_exp (Proj (r1, f))), adamc@1226: ("r2", adamc@1226: p_exp (Proj (r2, f))), adamc@1226: ("r", adamc@1226: Print.PD.string adamc@1226: (Bool.toString r))];*) adamc@1226: r adamc@1226: end)) ks then adamc@1226: ((*Print.prefaces "Key match" [("tab", Print.PD.string tab), adamc@1226: ("r1", p_exp r1), adamc@1226: ("r2", p_exp r2), adamc@1226: ("rp1", Cc.p_repOf cc r1), adamc@1226: ("rp2", Cc.p_repOf cc r2)];*) adamc@1226: Cc.assert (cc, AReln (Eq, [r1, r2]))) adamc@1226: else adamc@1226: (); adamc@1226: finder hyps) adamc@1226: | _ :: hyps => finder hyps adamc@1226: in adamc@1226: finder hyps; adamc@1226: findKeys hyps adamc@1226: end) adamc@1226: | _ :: hyps => findKeys hyps adamc@1218: in adamc@1226: findKeys hyps; adamc@1226: adamc@1221: (*Print.preface ("db", Cc.p_database cc);*) adamc@1218: (List.all (fn a => adamc@1218: if Cc.check (cc, a) then adamc@1218: true adamc@1218: else adamc@1218: ((*Print.prefaces "Can't prove" adamc@1218: [("a", p_atom a), adamc@1218: ("hyps", Print.p_list p_atom hyps), adamc@1218: ("db", Cc.p_database cc)];*) adamc@1218: false)) acc adamc@1218: (*andalso (Print.preface ("Finding", Cc.p_database cc); true)*) adamc@1220: andalso (case outs of adamc@1220: NONE => true adamc@1220: | SOME outs => Cc.builtFrom (cc, {Derived = Var 0, adamc@1220: Base = outs}))) adamc@1218: handle Cc.Contradiction => false adamc@1218: end handle Cc.Undetermined => false) adamc@1218: orelse onFail () adamc@1218: | (g as AReln (Sql gf, [ge])) :: goals => adamc@1218: let adamc@1218: fun hps hyps = adamc@1218: case hyps of adamc@1218: [] => gls goals onFail (g :: acc) adamc@1218: | (h as AReln (Sql hf, [he])) :: hyps => adamc@1218: if gf = hf then adamc@1218: let adamc@1218: val saved = save () adamc@1218: in adamc@1218: if eq (ge, he) then adamc@1218: let adamc@1218: val changed = IM.numItems (!unif) adamc@1218: <> IM.numItems saved adamc@1218: in adamc@1218: gls goals (fn () => (restore saved; adamc@1218: changed adamc@1218: andalso hps hyps)) adamc@1218: acc adamc@1218: end adamc@1218: else adamc@1218: hps hyps adamc@1218: end adamc@1218: else adamc@1218: hps hyps adamc@1218: | _ :: hyps => hps hyps adamc@1218: in adamc@1218: hps hyps adamc@1218: end adamc@1218: | g :: goals => gls goals onFail (g :: acc) adamc@1218: in adamc@1218: reset (); adamc@1218: (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps), adamc@1223: ("goals", Print.p_list p_atom goals)];*) adamc@1218: gls goals (fn () => false) [] adamc@1218: end handle Cc.Contradiction => true 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@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@1220: datatype dml = adamc@1220: Insert of string * (string * sqexp) list adamc@1221: | Delete of string * sqexp adamc@1223: | Update of string * (string * sqexp) list * sqexp adamc@1220: adamc@1220: val insert = log "insert" adamc@1220: (wrapP (follow (const "INSERT INTO ") adamc@1220: (follow uw_ident adamc@1220: (follow (const " (") adamc@1220: (follow (list uw_ident) adamc@1220: (follow (const ") VALUES (") adamc@1220: (follow (list sqexp) adamc@1220: (const ")"))))))) adamc@1220: (fn ((), (tab, ((), (fs, ((), (es, ())))))) => adamc@1221: (SOME (tab, ListPair.zipEq (fs, es))) adamc@1220: handle ListPair.UnequalLengths => NONE)) adamc@1220: adamc@1221: val delete = log "delete" adamc@1221: (wrap (follow (const "DELETE FROM ") adamc@1221: (follow uw_ident adamc@1221: (follow (const " AS T_T WHERE ") adamc@1221: sqexp))) adamc@1221: (fn ((), (tab, ((), es))) => (tab, es))) adamc@1221: adamc@1223: val setting = log "setting" adamc@1223: (wrap (follow uw_ident (follow (const " = ") sqexp)) adamc@1223: (fn (f, ((), e)) => (f, e))) adamc@1223: adamc@1223: val update = log "update" adamc@1223: (wrap (follow (const "UPDATE ") adamc@1223: (follow uw_ident adamc@1223: (follow (const " AS T_T SET ") adamc@1223: (follow (list setting) adamc@1223: (follow (ws (const "WHERE ")) adamc@1223: sqexp))))) adamc@1223: (fn ((), (tab, ((), (fs, ((), e))))) => adamc@1223: (tab, fs, e))) adamc@1223: adamc@1220: val dml = log "dml" adamc@1221: (altL [wrap insert Insert, adamc@1223: wrap delete Delete, adamc@1223: wrap update Update]) adamc@1220: adamc@1215: fun removeDups (ls : (string * string) list) = 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@1212: datatype queryMode = adamc@1218: SomeCol adamc@1212: | AllCols of exp adamc@1212: adamc@1220: fun expIn rv env rvOf = adamc@1220: let adamc@1220: fun expIn (e, rvN) = adamc@1220: let adamc@1220: fun default () = adamc@1220: let adamc@1220: val (rvN, e) = rv rvN adamc@1220: in adamc@1220: (inl e, rvN) adamc@1220: end adamc@1220: in adamc@1220: case e of adamc@1220: SqConst p => (inl (Const p), rvN) adamc@1220: | Field (v, f) => (inl (Proj (rvOf v, f)), rvN) adamc@1220: | Binop (bo, e1, e2) => adamc@1220: let adamc@1220: val (e1, rvN) = expIn (e1, rvN) adamc@1220: val (e2, rvN) = expIn (e2, rvN) adamc@1220: in adamc@1220: (inr (case (bo, e1, e2) of adamc@1220: (Exps f, inl e1, inl e2) => f (e1, e2) adamc@1220: | (Props f, inr p1, inr p2) => f (p1, p2) adamc@1220: | _ => Unknown), rvN) adamc@1220: end adamc@1220: | SqKnown e => adamc@1220: (case expIn (e, rvN) of adamc@1220: (inl e, rvN) => (inr (Reln (Known, [e])), rvN) adamc@1220: | _ => (inr Unknown, rvN)) adamc@1220: | Inj e => adamc@1220: let adamc@1220: fun deinj e = adamc@1220: case #1 e of adamc@1220: ERel n => (List.nth (env, n), rvN) adamc@1220: | EField (e, f) => adamc@1220: let adamc@1220: val (e, rvN) = deinj e adamc@1220: in adamc@1220: (Proj (e, f), rvN) adamc@1220: end adamc@1220: | _ => adamc@1220: let adamc@1220: val (rvN, e) = rv rvN adamc@1220: in adamc@1220: (e, rvN) adamc@1220: end adamc@1220: adamc@1220: val (e, rvN) = deinj e adamc@1220: in adamc@1220: (inl e, rvN) adamc@1220: end adamc@1220: | SqFunc (f, e) => adamc@1220: (case expIn (e, rvN) of adamc@1220: (inl e, rvN) => (inl (Func (Other f, [e])), rvN) adamc@1220: | _ => default ()) adamc@1220: adamc@1220: | Count => default () adamc@1220: end adamc@1220: in adamc@1220: expIn adamc@1220: end adamc@1216: adamc@1214: fun queryProp env rvN rv oe e = adamc@1216: let adamc@1216: fun default () = (print ("Warning: Information flow checker can't parse SQL query at " adamc@1216: ^ ErrorMsg.spanToString (#2 e) ^ "\n"); adamc@1218: (rvN, Unknown, Unknown, [], [])) adamc@1216: in adamc@1216: case parse query e of adamc@1216: NONE => default () adamc@1216: | SOME r => adamc@1216: let adamc@1216: val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => adamc@1216: let adamc@1216: val (rvN, e) = rv rvN adamc@1216: in adamc@1216: ((v, e), rvN) adamc@1216: end) rvN (#From r) adamc@1214: adamc@1216: fun rvOf v = adamc@1216: case List.find (fn (v', _) => v' = v) rvs of adamc@1216: NONE => raise Fail "Iflow.queryProp: Bad table variable" adamc@1216: | SOME (_, e) => e adamc@1214: adamc@1216: fun usedFields e = adamc@1216: case e of adamc@1216: SqConst _ => [] adamc@1216: | Field (v, f) => [(v, f)] adamc@1216: | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2) adamc@1216: | SqKnown _ => [] adamc@1216: | Inj _ => [] adamc@1216: | SqFunc (_, e) => usedFields e adamc@1216: | Count => [] adamc@1214: adamc@1216: val p = adamc@1216: foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r) adamc@1211: adamc@1220: val expIn = expIn rv env rvOf adamc@1205: adamc@1220: val (p, rvN) = case #Where r of adamc@1220: NONE => (p, rvN) adamc@1220: | SOME e => adamc@1220: case expIn (e, rvN) of adamc@1220: (inr p', rvN) => (And (p, p'), rvN) adamc@1220: | _ => (p, rvN) adamc@1210: adamc@1216: fun normal () = adamc@1218: case oe of adamc@1218: SomeCol => adamc@1220: let adamc@1220: val (sis, rvN) = adamc@1220: ListUtil.foldlMap adamc@1220: (fn (si, rvN) => adamc@1220: case si of adamc@1220: SqField (v, f) => (Proj (rvOf v, f), rvN) adamc@1220: | SqExp (e, f) => adamc@1220: case expIn (e, rvN) of adamc@1220: (inr _, _) => adamc@1220: let adamc@1220: val (rvN, e) = rv rvN adamc@1220: in adamc@1220: (e, rvN) adamc@1220: end adamc@1220: | (inl e, rvN) => (e, rvN)) rvN (#Select r) adamc@1220: in adamc@1220: (rvN, p, True, sis) adamc@1220: end adamc@1218: | AllCols oe => adamc@1220: let adamc@1222: val (ts, es, rvN) = adamc@1222: foldl (fn (si, (ts, es, rvN)) => adamc@1222: case si of adamc@1222: SqField (v, f) => adamc@1222: let adamc@1222: val fs = getOpt (SM.find (ts, v), SM.empty) adamc@1222: in adamc@1222: (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN) adamc@1222: end adamc@1222: | SqExp (e, f) => adamc@1222: let adamc@1222: val (e, rvN) = adamc@1220: case expIn (e, rvN) of adamc@1222: (inr _, rvN) => adamc@1222: let adamc@1222: val (rvN, e) = rv rvN adamc@1222: in adamc@1222: (e, rvN) adamc@1222: end adamc@1222: | (inl e, rvN) => (e, rvN) adamc@1222: in adamc@1222: (ts, SM.insert (es, f, e), rvN) adamc@1222: end) adamc@1222: (SM.empty, SM.empty, rvN) (#Select r) adamc@1222: adamc@1222: val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs))) adamc@1222: (SM.listItemsi ts) adamc@1222: @ SM.listItemsi es)]) adamc@1220: in adamc@1220: (rvN, And (p, p'), True, []) adamc@1220: end adamc@1217: adamc@1218: val (rvN, p, wp, outs) = adamc@1217: case #Select r of adamc@1217: [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => adamc@1217: (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of adamc@1217: Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => adamc@1218: (case oe of adamc@1218: SomeCol => adamc@1218: let adamc@1218: val (rvN, oe) = rv rvN adamc@1218: in adamc@1218: (rvN, adamc@1218: Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]), adamc@1218: And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), adamc@1218: p)), adamc@1218: Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), adamc@1218: [oe]) adamc@1218: end adamc@1218: | AllCols oe => adamc@1218: let adamc@1221: fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]]) adamc@1218: in adamc@1218: (rvN, adamc@1221: Or (oeEq (Func (DtCon0 "Basis.bool.False", [])), adamc@1221: And (oeEq (Func (DtCon0 "Basis.bool.True", [])), adamc@1218: p)), adamc@1221: oeEq (Func (DtCon0 "Basis.bool.True", [])), adamc@1218: []) adamc@1218: end) adamc@1217: | _ => normal ()) adamc@1217: | _ => normal () adamc@1216: in adamc@1217: (rvN, p, wp, case #Where r of adamc@1217: NONE => [] adamc@1218: | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e), outs) adamc@1216: end adamc@1220: end adamc@1220: adamc@1220: fun insertProp rvN rv e = adamc@1220: let adamc@1220: fun default () = (print ("Warning: Information flow checker can't parse SQL query at " adamc@1220: ^ ErrorMsg.spanToString (#2 e) ^ "\n"); adamc@1220: Unknown) adamc@1220: in adamc@1220: case parse query e of adamc@1220: NONE => default () adamc@1220: | SOME r => adamc@1220: let adamc@1220: val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => adamc@1220: let adamc@1220: val (rvN, e) = rv rvN adamc@1220: in adamc@1220: ((v, e), rvN) adamc@1220: end) rvN (#From r) adamc@1220: adamc@1220: fun rvOf v = adamc@1220: case List.find (fn (v', _) => v' = v) rvs of adamc@1220: NONE => raise Fail "Iflow.insertProp: Bad table variable" adamc@1220: | SOME (_, e) => e adamc@1220: adamc@1220: val p = adamc@1220: foldl (fn ((t, v), p) => adamc@1220: let adamc@1220: val t = adamc@1220: case v of adamc@1220: "New" => "$New" adamc@1220: | _ => t adamc@1220: in adamc@1220: And (p, Reln (Sql t, [rvOf v])) adamc@1220: end) True (#From r) adamc@1220: adamc@1220: val expIn = expIn rv [] rvOf adamc@1220: in adamc@1220: case #Where r of adamc@1220: NONE => p adamc@1220: | SOME e => adamc@1220: case expIn (e, rvN) of adamc@1220: (inr p', _) => And (p, p') adamc@1220: | _ => p adamc@1220: end adamc@1216: end adamc@1200: adamc@1221: fun deleteProp rvN rv e = adamc@1221: let adamc@1221: fun default () = (print ("Warning: Information flow checker can't parse SQL query at " adamc@1221: ^ ErrorMsg.spanToString (#2 e) ^ "\n"); adamc@1221: Unknown) adamc@1221: in adamc@1221: case parse query e of adamc@1221: NONE => default () adamc@1221: | SOME r => adamc@1221: let adamc@1221: val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => adamc@1221: let adamc@1221: val (rvN, e) = rv rvN adamc@1221: in adamc@1221: ((v, e), rvN) adamc@1221: end) rvN (#From r) adamc@1221: adamc@1221: fun rvOf v = adamc@1221: case List.find (fn (v', _) => v' = v) rvs of adamc@1221: NONE => raise Fail "Iflow.deleteProp: Bad table variable" adamc@1221: | SOME (_, e) => e adamc@1221: adamc@1221: val p = adamc@1221: foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r) adamc@1221: adamc@1221: val expIn = expIn rv [] rvOf adamc@1221: in adamc@1221: And (Reln (Sql "$Old", [rvOf "Old"]), adamc@1221: case #Where r of adamc@1221: NONE => p adamc@1221: | SOME e => adamc@1221: case expIn (e, rvN) of adamc@1221: (inr p', _) => And (p, p') adamc@1221: | _ => p) adamc@1221: end adamc@1221: end adamc@1221: adamc@1223: fun updateProp rvN rv e = adamc@1223: let adamc@1223: fun default () = (print ("Warning: Information flow checker can't parse SQL query at " adamc@1223: ^ ErrorMsg.spanToString (#2 e) ^ "\n"); adamc@1223: Unknown) adamc@1223: in adamc@1223: case parse query e of adamc@1223: NONE => default () adamc@1223: | SOME r => adamc@1223: let adamc@1223: val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => adamc@1223: let adamc@1223: val (rvN, e) = rv rvN adamc@1223: in adamc@1223: ((v, e), rvN) adamc@1223: end) rvN (#From r) adamc@1223: adamc@1223: fun rvOf v = adamc@1223: case List.find (fn (v', _) => v' = v) rvs of adamc@1223: NONE => raise Fail "Iflow.insertProp: Bad table variable" adamc@1223: | SOME (_, e) => e adamc@1223: adamc@1223: val p = adamc@1223: foldl (fn ((t, v), p) => adamc@1223: let adamc@1223: val t = adamc@1223: case v of adamc@1223: "New" => "$New" adamc@1223: | _ => t adamc@1223: in adamc@1223: And (p, Reln (Sql t, [rvOf v])) adamc@1223: end) True (#From r) adamc@1223: adamc@1223: val expIn = expIn rv [] rvOf adamc@1223: in adamc@1223: And (Reln (Sql "$Old", [rvOf "Old"]), adamc@1223: case #Where r of adamc@1223: NONE => p adamc@1223: | SOME e => adamc@1223: case expIn (e, rvN) of adamc@1223: (inr p', _) => And (p, p') adamc@1223: | _ => p) adamc@1223: end adamc@1223: end adamc@1223: 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@1215: | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e])) adamc@1211: | PCon (_, pc, SOME pt) => adamc@1211: let adamc@1215: val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt adamc@1211: in adamc@1215: (env, And (p, Reln (PCon1 (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@1215: | PNone _ => (env, Reln (PCon0 "None", [e])) adamc@1211: | PSome (_, pt) => adamc@1211: let adamc@1215: val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt adamc@1211: in adamc@1215: (env, And (p, Reln (PCon1 "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@1212: | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2) 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: | _ => p2 adamc@1211: in adamc@1211: rr adamc@1211: end adamc@1211: adamc@1218: datatype cflow = Case | Where adamc@1218: datatype flow = Data | Control of cflow adamc@1218: type check = ErrorMsg.span * exp * prop adamc@1221: type dml = ErrorMsg.span * prop adamc@1218: adamc@1217: structure St :> sig adamc@1217: type t adamc@1217: val create : {Var : int, adamc@1217: Ambient : prop} -> t adamc@1217: adamc@1217: val curVar : t -> int adamc@1217: val nextVar : t -> t * int adamc@1217: adamc@1217: val ambient : t -> prop adamc@1217: val setAmbient : t * prop -> t adamc@1217: adamc@1218: val paths : t -> (check * cflow) list adamc@1218: val addPath : t * (check * cflow) -> t adamc@1218: val addPaths : t * (check * cflow) list -> t adamc@1218: val clearPaths : t -> t adamc@1218: val setPaths : t * (check * cflow) list -> t adamc@1217: adamc@1218: val sent : t -> (check * flow) list adamc@1218: val addSent : t * (check * flow) -> t adamc@1218: val setSent : t * (check * flow) list -> t adamc@1220: adamc@1221: val inserted : t -> dml list adamc@1221: val addInsert : t * dml -> t adamc@1221: adamc@1221: val deleted : t -> dml list adamc@1221: val addDelete : t * dml -> t adamc@1223: adamc@1223: val updated : t -> dml list adamc@1223: val addUpdate : t * dml -> t adamc@1217: end = struct adamc@1217: adamc@1217: type t = {Var : int, adamc@1217: Ambient : prop, adamc@1218: Path : (check * cflow) list, adamc@1220: Sent : (check * flow) list, adamc@1221: Insert : dml list, adamc@1223: Delete : dml list, adamc@1223: Update : dml list} adamc@1217: adamc@1217: fun create {Var = v, Ambient = p} = {Var = v, adamc@1217: Ambient = p, adamc@1217: Path = [], adamc@1220: Sent = [], adamc@1221: Insert = [], adamc@1223: Delete = [], adamc@1223: Update = []} adamc@1217: adamc@1217: fun curVar (t : t) = #Var t adamc@1217: fun nextVar (t : t) = ({Var = #Var t + 1, adamc@1217: Ambient = #Ambient t, adamc@1217: Path = #Path t, adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t}, #Var t) adamc@1217: adamc@1217: fun ambient (t : t) = #Ambient t adamc@1217: fun setAmbient (t : t, p) = {Var = #Var t, adamc@1217: Ambient = p, adamc@1217: Path = #Path t, adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1217: adamc@1218: fun paths (t : t) = #Path t adamc@1217: fun addPath (t : t, c) = {Var = #Var t, adamc@1217: Ambient = #Ambient t, adamc@1217: Path = c :: #Path t, adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1218: fun addPaths (t : t, cs) = {Var = #Var t, adamc@1218: Ambient = #Ambient t, adamc@1218: Path = cs @ #Path t, adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1218: fun clearPaths (t : t) = {Var = #Var t, adamc@1218: Ambient = #Ambient t, adamc@1218: Path = [], adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1218: fun setPaths (t : t, cs) = {Var = #Var t, adamc@1218: Ambient = #Ambient t, adamc@1218: Path = cs, adamc@1220: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1217: adamc@1217: fun sent (t : t) = #Sent t adamc@1217: fun addSent (t : t, c) = {Var = #Var t, adamc@1217: Ambient = #Ambient t, adamc@1217: Path = #Path t, adamc@1220: Sent = c :: #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1217: fun setSent (t : t, cs) = {Var = #Var t, adamc@1217: Ambient = #Ambient t, adamc@1217: Path = #Path t, adamc@1220: Sent = cs, adamc@1221: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1220: adamc@1220: fun inserted (t : t) = #Insert t adamc@1220: fun addInsert (t : t, c) = {Var = #Var t, adamc@1220: Ambient = #Ambient t, adamc@1220: Path = #Path t, adamc@1220: Sent = #Sent t, adamc@1221: Insert = c :: #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = #Update t} adamc@1221: adamc@1221: fun deleted (t : t) = #Delete t adamc@1221: fun addDelete (t : t, c) = {Var = #Var t, adamc@1221: Ambient = #Ambient t, adamc@1221: Path = #Path t, adamc@1221: Sent = #Sent t, adamc@1221: Insert = #Insert t, adamc@1223: Delete = c :: #Delete t, adamc@1223: Update = #Update t} adamc@1223: adamc@1223: fun updated (t : t) = #Update t adamc@1223: fun addUpdate (t : t, c) = {Var = #Var t, adamc@1223: Ambient = #Ambient t, adamc@1223: Path = #Path t, adamc@1223: Sent = #Sent t, adamc@1223: Insert = #Insert t, adamc@1223: Delete = #Delete t, adamc@1223: Update = c :: #Update t} adamc@1217: adamc@1217: end adamc@1217: adamc@1217: fun evalExp env (e as (_, loc), st) = adamc@1200: let adamc@1200: fun default () = adamc@1217: let adamc@1217: val (st, nv) = St.nextVar st adamc@1217: in adamc@1217: (Var nv, st) adamc@1217: end adamc@1200: adamc@1217: fun addSent (p, e, st) = adamc@1218: let adamc@1218: val st = if isKnown e then adamc@1218: st adamc@1218: else adamc@1218: St.addSent (st, ((loc, e, p), Data)) adamc@1218: adamc@1218: val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st) adamc@1218: in adamc@1218: St.clearPaths st adamc@1218: end 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@1215: | ECon (_, pc, NONE) => (Func (DtCon0 (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@1215: (Func (DtCon1 (patCon pc), [e]), st) adamc@1200: end adamc@1215: | ENone _ => (Func (DtCon0 "None", []), st) adamc@1200: | ESome (_, e) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1215: (Func (DtCon1 "Some", [e]), st) adamc@1200: end adamc@1200: | EFfi _ => default () adamc@1213: 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@1217: (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st 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@1215: (Func (Other (m ^ "." ^ s), es), st) adamc@1200: end adamc@1213: adamc@1213: | EApp (e1, e2) => adamc@1213: let adamc@1213: val (e1, st) = evalExp env (e1, st) adamc@1213: in adamc@1213: case e1 of adamc@1213: Finish => (Finish, st) adamc@1213: | _ => default () adamc@1213: end adamc@1213: 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@1215: (Func (Other 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@1215: (Func (Other 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@1218: | ECase (e, pes, {result = res, ...}) => adamc@1211: let adamc@1211: val (e, st) = evalExp env (e, st) adamc@1217: val (st, r) = St.nextVar st adamc@1217: val orig = St.ambient st adamc@1218: val origPaths = St.paths st adamc@1211: adamc@1218: val st = St.addPath (st, ((loc, e, orig), Case)) adamc@1218: adamc@1218: val (st, paths) = adamc@1218: foldl (fn ((pt, pe), (st, paths)) => adamc@1218: let adamc@1218: val (env, pp) = evalPat env e pt adamc@1218: val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp))) adamc@1218: adamc@1218: val this = And (removeRedundant orig (St.ambient st'), adamc@1218: Reln (Eq, [Var r, pe])) adamc@1218: in adamc@1218: (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths), adamc@1218: St.paths st' @ paths) adamc@1218: end) (St.setAmbient (st, False), []) pes adamc@1218: adamc@1218: val st = case #1 res of adamc@1218: TRecord [] => St.setPaths (st, origPaths) adamc@1218: | _ => St.setPaths (st, paths) adamc@1211: in adamc@1217: (Var r, St.setAmbient (st, And (orig, St.ambient 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@1215: (Func (Other "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@1217: (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st))) adamc@1200: end adamc@1200: | ERedirect (e, _) => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1217: (Finish, addSent (St.ambient st, e, st)) adamc@1200: end adamc@1200: | EWrite e => adamc@1200: let adamc@1200: val (e, st) = evalExp env (e, st) adamc@1200: in adamc@1217: (Recd [], addSent (St.ambient st, e, st)) 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@1215: (Func (Other ("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@1217: val (st', r) = St.nextVar st adamc@1217: val (st', acc) = St.nextVar st' adamc@1200: adamc@1200: val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') adamc@1200: adamc@1218: val (st', qp, qwp, used, _) = adamc@1214: queryProp env adamc@1217: st' (fn st' => adamc@1217: let adamc@1217: val (st', rv) = St.nextVar st' adamc@1217: in adamc@1217: (st', Var rv) adamc@1217: end) adamc@1214: (AllCols (Var r)) q adamc@1200: adamc@1217: val p' = And (qp, St.ambient st') adamc@1200: adamc@1217: val (st, res) = if varInP acc (St.ambient st') then adamc@1217: let adamc@1217: val (st, r) = St.nextVar st adamc@1217: in adamc@1217: (st, Var r) adamc@1217: end adamc@1217: else adamc@1217: let adamc@1217: val (st, out) = St.nextVar st' adamc@1217: adamc@1217: val p = Or (Reln (Eq, [Var out, i]), adamc@1217: And (Reln (Eq, [Var out, b]), adamc@1217: p')) adamc@1217: in adamc@1217: (St.setAmbient (st, p), Var out) adamc@1217: end adamc@1210: adamc@1218: val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st') adamc@1212: adamc@1217: val p' = And (p', qwp) adamc@1218: val paths = map (fn e => ((loc, e, p'), Where)) used adamc@1200: in adamc@1218: (res, St.addPaths (St.setSent (st, sent), paths)) adamc@1200: end adamc@1220: | EDml e => adamc@1220: (case parse dml e of adamc@1220: NONE => (print ("Warning: Information flow checker can't parse DML command at " adamc@1220: ^ ErrorMsg.spanToString loc ^ "\n"); adamc@1220: default ()) adamc@1220: | SOME d => adamc@1220: case d of adamc@1220: Insert (tab, es) => adamc@1220: let adamc@1220: val (st, new) = St.nextVar st adamc@1220: adamc@1220: fun rv st = adamc@1220: let adamc@1220: val (st, n) = St.nextVar st adamc@1220: in adamc@1220: (st, Var n) adamc@1220: end adamc@1220: adamc@1223: val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT") adamc@1220: adamc@1220: val (es, st) = ListUtil.foldlMap adamc@1220: (fn ((x, e), st) => adamc@1220: let adamc@1220: val (e, st) = case expIn (e, st) of adamc@1220: (inl e, st) => (e, st) adamc@1220: | (inr _, _) => raise Fail adamc@1220: ("Iflow.evalExp: Selecting " adamc@1220: ^ "boolean expression") adamc@1220: in adamc@1220: ((x, e), st) adamc@1220: end) adamc@1220: st es adamc@1220: in adamc@1220: (Recd [], St.addInsert (st, (loc, And (St.ambient st, adamc@1220: Reln (Sql "$New", [Recd es]))))) adamc@1221: end adamc@1221: | Delete (tab, e) => adamc@1221: let adamc@1221: val (st, old) = St.nextVar st adamc@1221: adamc@1221: fun rv st = adamc@1221: let adamc@1221: val (st, n) = St.nextVar st adamc@1221: in adamc@1221: (st, Var n) adamc@1221: end adamc@1221: adamc@1221: val expIn = expIn rv env (fn "T" => Var old adamc@1221: | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE") adamc@1221: adamc@1221: val (p, st) = case expIn (e, st) of adamc@1221: (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean" adamc@1221: | (inr p, st) => (p, st) adamc@1221: adamc@1221: val p = And (p, adamc@1221: And (Reln (Sql "$Old", [Var old]), adamc@1221: Reln (Sql tab, [Var old]))) adamc@1221: in adamc@1221: (Recd [], St.addDelete (st, (loc, And (St.ambient st, p)))) adamc@1223: end adamc@1223: | Update (tab, fs, e) => adamc@1223: let adamc@1223: val (st, new) = St.nextVar st adamc@1223: val (st, old) = St.nextVar st adamc@1223: adamc@1223: fun rv st = adamc@1223: let adamc@1223: val (st, n) = St.nextVar st adamc@1223: in adamc@1223: (st, Var n) adamc@1223: end adamc@1223: adamc@1223: val expIn = expIn rv env (fn "T" => Var old adamc@1223: | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE") adamc@1223: adamc@1223: val (fs, st) = ListUtil.foldlMap adamc@1223: (fn ((x, e), st) => adamc@1223: let adamc@1223: val (e, st) = case expIn (e, st) of adamc@1223: (inl e, st) => (e, st) adamc@1223: | (inr _, _) => raise Fail adamc@1223: ("Iflow.evalExp: Selecting " adamc@1223: ^ "boolean expression") adamc@1223: in adamc@1223: ((x, e), st) adamc@1223: end) adamc@1223: st fs adamc@1223: adamc@1226: val fs' = case SM.find (!tabs, tab) of adamc@1224: NONE => raise Fail "Iflow.evalExp: Updating unknown table" adamc@1226: | SOME (fs', _) => fs' adamc@1224: adamc@1224: val fs = foldl (fn (f, fs) => adamc@1224: if List.exists (fn (f', _) => f' = f) fs then adamc@1224: fs adamc@1224: else adamc@1224: (f, Proj (Var old, f)) :: fs) fs fs' adamc@1224: adamc@1223: val (p, st) = case expIn (e, st) of adamc@1223: (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean" adamc@1223: | (inr p, st) => (p, st) adamc@1223: adamc@1223: val p = And (p, adamc@1223: And (Reln (Sql "$New", [Recd fs]), adamc@1223: And (Reln (Sql "$Old", [Var old]), adamc@1223: Reln (Sql tab, [Var old])))) adamc@1223: in adamc@1223: (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p)))) adamc@1220: end) adamc@1220: adamc@1200: | ENextval _ => default () adamc@1200: | ESetval _ => default () adamc@1200: adamc@1213: | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) => adamc@1217: let adamc@1217: val (st, nv) = St.nextVar st adamc@1217: in adamc@1217: (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv])))) adamc@1217: end adamc@1213: 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@1213: val file = MonoReduce.reduce file adamc@1213: val file = MonoOpt.optimize file adamc@1213: val file = Fuse.fuse file adamc@1213: val file = MonoOpt.optimize file adamc@1216: val file = MonoShake.shake file adamc@1213: (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*) adamc@1213: 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@1223: fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) = adamc@1200: case d of adamc@1226: DTable (tab, fs, pk, _) => adamc@1226: let adamc@1226: val ks = adamc@1226: case #1 pk of adamc@1226: EPrim (Prim.String s) => adamc@1226: (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of adamc@1226: [] => [] adamc@1226: | pk => [pk]) adamc@1226: | _ => [] adamc@1226: in adamc@1226: if size tab >= 3 then adamc@1226: (tabs := SM.insert (!tabs, String.extract (tab, 3, NONE), adamc@1226: (map #1 fs, adamc@1226: map (map (fn s => str (Char.toUpper (String.sub (s, 3))) adamc@1226: ^ String.extract (s, 4, NONE))) ks)); adamc@1226: (vals, inserts, deletes, updates, client, insert, delete, update)) adamc@1226: else adamc@1226: raise Fail "Table name does not begin with uw_" adamc@1226: end adamc@1224: | 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@1217: val (_, st) = evalExp env (e, St.create {Var = nv, adamc@1217: Ambient = p}) adamc@1200: in adamc@1223: (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates, adamc@1223: client, insert, delete, update) adamc@1200: end adamc@1202: adamc@1220: | DPolicy pol => adamc@1218: let adamc@1220: fun rv rvN = (rvN + 1, Lvar rvN) adamc@1218: in adamc@1220: case pol of adamc@1220: PolClient e => adamc@1220: let adamc@1220: val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e adamc@1220: in adamc@1223: (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update) adamc@1220: end adamc@1220: | PolInsert e => adamc@1220: let adamc@1220: val p = insertProp 0 rv e adamc@1220: in adamc@1223: (vals, inserts, deletes, updates, client, p :: insert, delete, update) adamc@1221: end adamc@1221: | PolDelete e => adamc@1221: let adamc@1221: val p = deleteProp 0 rv e adamc@1221: in adamc@1223: (vals, inserts, deletes, updates, client, insert, p :: delete, update) adamc@1223: end adamc@1223: | PolUpdate e => adamc@1223: let adamc@1223: val p = updateProp 0 rv e adamc@1223: in adamc@1223: (vals, inserts, deletes, updates, client, insert, delete, p :: update) adamc@1220: end adamc@1218: end adamc@1214: adamc@1223: | _ => (vals, inserts, deletes, updates, client, insert, delete, update) adamc@1202: adamc@1203: val () = reset () adamc@1202: adamc@1223: val (vals, inserts, deletes, updates, client, insert, delete, update) = adamc@1223: foldl decl ([], [], [], [], [], [], [], []) file adamc@1220: adamc@1224: adamc@1220: val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ()) adamc@1220: val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ()) adamc@1221: adamc@1221: fun doDml (cmds, pols) = adamc@1221: app (fn (loc, p) => adamc@1221: if decompH p adamc@1221: (fn hyps => adamc@1221: List.exists (fn p' => adamc@1221: decompG p' adamc@1221: (fn goals => imply (hyps, goals, NONE))) adamc@1221: pols) then adamc@1221: () adamc@1221: else adamc@1221: (ErrorMsg.errorAt loc "The information flow policy may be violated here."; adamc@1221: Print.preface ("The state satisifies this predicate:", p_prop p))) cmds adamc@1200: in adamc@1218: app (fn ((loc, e, p), fl) => adamc@1207: let adamc@1213: fun doOne e = adamc@1213: let adamc@1213: val p = And (p, Reln (Eq, [Var 0, e])) adamc@1213: in adamc@1220: if decompH p adamc@1220: (fn hyps => adamc@1220: (fl <> Control Where adamc@1220: andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) adamc@1220: orelse List.exists (fn (p', outs) => adamc@1220: decompG p' adamc@1220: (fn goals => imply (hyps, goals, SOME outs))) adamc@1220: client) then adamc@1213: () adamc@1213: else adamc@1213: (ErrorMsg.errorAt loc "The information flow policy may be violated here."; adamc@1216: Print.preface ("The state satisifies this predicate:", p_prop p)) adamc@1213: end adamc@1213: adamc@1213: fun doAll e = adamc@1213: case e of adamc@1213: Const _ => () adamc@1213: | Var _ => doOne e adamc@1213: | Lvar _ => raise Fail "Iflow.doAll: Lvar" adamc@1216: | Func (UnCon _, [_]) => doOne e adamc@1215: | Func (_, es) => app doAll es adamc@1213: | Recd xes => app (doAll o #2) xes adamc@1213: | Proj _ => doOne e adamc@1213: | Finish => () adamc@1207: in adamc@1213: doAll e adamc@1220: end) vals; adamc@1220: adamc@1221: doDml (inserts, insert); adamc@1223: doDml (deletes, delete); adamc@1223: doDml (updates, update) adamc@1200: end adamc@1200: adamc@1213: val check = fn file => adamc@1213: let adamc@1213: val oldInline = Settings.getMonoInline () adamc@1213: in adamc@1213: (Settings.setMonoInline (case Int.maxInt of adamc@1213: NONE => 1000000 adamc@1213: | SOME n => n); adamc@1213: check file; adamc@1213: Settings.setMonoInline oldInline) adamc@1213: handle ex => (Settings.setMonoInline oldInline; adamc@1213: raise ex) adamc@1213: end adamc@1213: adamc@1200: end adamc@1213: