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 ezyang@1697: open Sql 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: 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@1236: | Lvar n => string ("X" ^ Int.toString n) 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: 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@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@1236: fun simplify unif = adamc@1236: let adamc@1236: fun simplify e = adamc@1236: case e of adamc@1236: Const _ => e adamc@1236: | Var _ => e adamc@1236: | Lvar n => adamc@1236: (case IM.find (unif, n) of adamc@1236: NONE => e adamc@1236: | SOME e => simplify e) adamc@1236: | Func (f, es) => Func (f, map simplify es) adamc@1236: | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes) adamc@1236: | Proj (e, s) => Proj (simplify e, s) adamc@1236: in adamc@1236: simplify adamc@1236: end 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@1208: (* Congruence closure *) adamc@1208: structure Cc :> sig adamc@1215: type database adamc@1215: adamc@1215: exception Contradiction adamc@1215: adamc@1215: val database : unit -> database adamc@1236: val clear : database -> unit 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@1253: 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@1244: local adamc@1244: val count = ref 0 adamc@1244: in adamc@1244: fun nodeId () = adamc@1244: let adamc@1244: val n = !count adamc@1244: in adamc@1244: count := n + 1; adamc@1244: n adamc@1244: end adamc@1244: end adamc@1244: 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@1244: datatype node = Node of {Id : int, adamc@1244: Rep : node ref option ref, adamc@1215: Cons : node ref SM.map ref, adamc@1215: Variety : variety, adamc@1245: Known : bool ref, adamc@1245: Ge : Int64.int option 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@1229: 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@1236: fun clear (t : database) = (#Vars t := IM.empty; adamc@1236: #Consts t := CM.empty; adamc@1236: #Con0s t := SM.empty; adamc@1236: #Records t := []; adamc@1236: #Funcs t := []) adamc@1236: 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@1244: box [string (Int.toString (#Id (unNode n)) ^ ":"), adamc@1244: 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@1245: box []], adamc@1245: if !(#Known (unNode n)) then adamc@1245: string " (known)" adamc@1245: else adamc@1245: box [], adamc@1245: case !(#Ge (unNode n)) of adamc@1245: NONE => box [] adamc@1245: | SOME n => string (" (>= " ^ Int64.toString n ^ ")")] 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@1245: p_rep n]) (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@1244: val r = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Prim p, adamc@1245: Known = ref true, adamc@1245: Ge = ref (case p of adamc@1245: Prim.Int n => SOME n adamc@1245: | _ => NONE)}) 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@1244: val r = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1245: Known = ref false, adamc@1245: Ge = ref NONE}) adamc@1215: in adamc@1215: #Vars db := IM.insert (!(#Vars db), n, r); adamc@1215: r adamc@1215: end) adamc@1236: | Lvar _ => raise Undetermined 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@1244: val r = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt0 f, adamc@1245: Known = ref true, adamc@1245: Ge = ref NONE}) 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@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Dt1 (f, r), adamc@1245: Known = ref (!(#Known (unNode r))), adamc@1245: Ge = ref NONE}) 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@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = cons, adamc@1215: Variety = Nothing, adamc@1245: Known = ref (!(#Known (unNode r))), adamc@1245: Ge = ref NONE}) adamc@1215: adamc@1244: val r'' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = #Cons (unNode r), adamc@1215: Variety = Dt1 (f, r'), adamc@1245: Known = #Known (unNode r), adamc@1245: Ge = ref NONE}) 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@1244: val r = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1252: Known = ref (f = "allow"), adamc@1245: Ge = ref NONE}) 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@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1221: Variety = Recrd (ref xes, true), adamc@1245: Known = ref false, adamc@1245: Ge = ref NONE}) 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@1244: val r = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1245: Known = ref (!(#Known (unNode r))), adamc@1245: Ge = ref NONE}) adamc@1215: in adamc@1215: xes := SM.insert (!xes, f, r); adamc@1215: r adamc@1215: end) adamc@1215: | Nothing => adamc@1215: let adamc@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = ref SM.empty, adamc@1215: Variety = Nothing, adamc@1245: Known = ref (!(#Known (unNode r))), adamc@1245: Ge = ref NONE}) adamc@1215: adamc@1244: val r'' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1215: Cons = #Cons (unNode r), adamc@1221: Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false), adamc@1245: Known = #Known (unNode r), adamc@1245: Ge = ref NONE}) adamc@1215: in adamc@1215: #Rep (unNode r) := SOME r''; adamc@1215: r' adamc@1215: end adamc@1215: | _ => raise Contradiction adamc@1215: end 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@1243: let adamc@1243: fun markEq (r1, r2) = adamc@1215: let adamc@1243: val r1 = repOf r1 adamc@1243: val r2 = repOf r2 adamc@1215: in adamc@1243: if r1 = r2 then adamc@1243: () adamc@1243: else case (#Variety (unNode r1), #Variety (unNode r2)) of adamc@1243: (Prim p1, Prim p2) => if Prim.equal (p1, p2) then adamc@1243: () adamc@1243: else adamc@1243: raise Contradiction adamc@1243: | (Dt0 f1, Dt0 f2) => if f1 = f2 then adamc@1243: () adamc@1243: else adamc@1243: raise Contradiction adamc@1243: | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then adamc@1243: markEq (r1, r2) adamc@1243: else adamc@1243: raise Contradiction adamc@1243: | (Recrd (xes1, _), Recrd (xes2, _)) => adamc@1243: let adamc@1243: fun unif (xes1, xes2) = adamc@1243: SM.appi (fn (x, r1) => adamc@1243: case SM.find (!xes2, x) of adamc@1243: NONE => xes2 := SM.insert (!xes2, x, r1) adamc@1243: | SOME r2 => markEq (r1, r2)) (!xes1) adamc@1243: in adamc@1243: unif (xes1, xes2); adamc@1243: unif (xes2, xes1) adamc@1243: end adamc@1243: | (Nothing, _) => mergeNodes (r1, r2) adamc@1243: | (_, Nothing) => mergeNodes (r2, r1) adamc@1243: | _ => raise Contradiction adamc@1215: end adamc@1243: adamc@1243: and mergeNodes (r1, r2) = adamc@1243: (#Rep (unNode r1) := SOME r2; adamc@1243: if !(#Known (unNode r1)) then adamc@1243: markKnown r2 adamc@1243: else adamc@1243: (); adamc@1243: if !(#Known (unNode r2)) then adamc@1243: markKnown r1 adamc@1243: else adamc@1243: (); adamc@1243: #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1))); adamc@1243: adamc@1245: case !(#Ge (unNode r1)) of adamc@1245: NONE => () adamc@1245: | SOME n1 => adamc@1245: case !(#Ge (unNode r2)) of adamc@1245: NONE => #Ge (unNode r2) := SOME n1 adamc@1245: | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2)); adamc@1245: adamc@1243: compactFuncs ()) adamc@1243: adamc@1243: and compactFuncs () = adamc@1215: let adamc@1243: fun loop funcs = adamc@1243: case funcs of adamc@1243: [] => [] adamc@1243: | (fr as ((f, rs), r)) :: rest => adamc@1243: let adamc@1243: val rest = List.filter (fn ((f' : string, rs'), r') => adamc@1243: if f' = f adamc@1243: andalso ListPair.allEq (fn (r1, r2) => adamc@1243: repOf r1 = repOf r2) adamc@1243: (rs, rs') then adamc@1243: (markEq (r, r'); adamc@1243: false) adamc@1243: else adamc@1243: true) rest adamc@1243: in adamc@1243: fr :: loop rest adamc@1243: end adamc@1215: in adamc@1243: #Funcs db := loop (!(#Funcs db)) adamc@1243: end adamc@1243: in adamc@1243: case a of adamc@1243: ACond _ => () adamc@1243: | AReln x => adamc@1243: case x of adamc@1243: (Known, [e]) => adamc@1243: ((*Print.prefaces "Before" [("e", p_exp e), adamc@1243: ("db", p_database db)];*) adamc@1243: markKnown (representative (db, e))(*; adamc@1243: Print.prefaces "After" [("e", p_exp e), adamc@1243: ("db", p_database db)]*)) adamc@1243: | (PCon0 f, [e]) => adamc@1243: let adamc@1243: val r = representative (db, e) adamc@1243: in adamc@1243: case #Variety (unNode r) of adamc@1243: Dt0 f' => if f = f' then adamc@1243: () adamc@1243: else adamc@1243: raise Contradiction adamc@1243: | Nothing => adamc@1243: (case SM.find (!(#Con0s db), f) of adamc@1243: SOME r' => markEq (r, r') adamc@1243: | NONE => adamc@1243: let adamc@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1243: Cons = ref SM.empty, adamc@1243: Variety = Dt0 f, adamc@1245: Known = ref false, adamc@1245: Ge = ref NONE}) adamc@1243: in adamc@1243: #Rep (unNode r) := SOME r'; adamc@1243: #Con0s db := SM.insert (!(#Con0s db), f, r') adamc@1243: end) adamc@1243: | _ => raise Contradiction adamc@1243: end adamc@1243: | (PCon1 f, [e]) => adamc@1243: let adamc@1243: val r = representative (db, e) adamc@1243: in adamc@1243: case #Variety (unNode r) of adamc@1243: Dt1 (f', e') => if f = f' then adamc@1243: () adamc@1243: else adamc@1243: raise Contradiction adamc@1243: | Nothing => adamc@1243: let adamc@1253: val cons = ref SM.empty adamc@1253: adamc@1244: val r'' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1253: Cons = cons, adamc@1243: Variety = Nothing, adamc@1245: Known = ref (!(#Known (unNode r))), adamc@1245: Ge = ref NONE}) adamc@1214: adamc@1244: val r' = ref (Node {Id = nodeId (), adamc@1244: Rep = ref NONE, adamc@1243: Cons = ref SM.empty, adamc@1243: Variety = Dt1 (f, r''), adamc@1245: Known = #Known (unNode r), adamc@1245: Ge = ref NONE}) adamc@1243: in adamc@1253: cons := SM.insert (!cons, f, r'); adamc@1243: #Rep (unNode r) := SOME r' adamc@1243: end adamc@1243: | _ => raise Contradiction adamc@1243: end adamc@1243: | (Eq, [e1, e2]) => adamc@1215: markEq (representative (db, e1), representative (db, e2)) adamc@1245: | (Ge, [e1, e2]) => adamc@1245: let adamc@1245: val r1 = representative (db, e1) adamc@1245: val r2 = representative (db, e2) adamc@1245: in adamc@1245: case !(#Ge (unNode (repOf r2))) of adamc@1245: NONE => () adamc@1245: | SOME n2 => adamc@1245: case !(#Ge (unNode (repOf r1))) of adamc@1245: NONE => #Ge (unNode (repOf r1)) := SOME n2 adamc@1245: | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2)) adamc@1245: end adamc@1243: | _ => () adamc@1247: end handle Undetermined => () adamc@1214: adamc@1215: fun check (db, a) = adamc@1247: (case a of adamc@1247: ACond _ => false adamc@1247: | AReln x => adamc@1247: case x of adamc@1247: (Known, [e]) => adamc@1247: let adamc@1247: fun isKnown r = adamc@1247: let adamc@1247: val r = repOf r adamc@1247: in adamc@1247: !(#Known (unNode r)) adamc@1247: orelse case #Variety (unNode r) of adamc@1247: Dt1 (_, r) => isKnown r adamc@1247: | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes)) adamc@1247: | _ => false adamc@1247: end adamc@1221: adamc@1247: val r = representative (db, e) adamc@1247: in adamc@1247: isKnown r adamc@1247: end adamc@1247: | (PCon0 f, [e]) => adamc@1247: (case #Variety (unNode (representative (db, e))) of adamc@1247: Dt0 f' => f' = f adamc@1247: | _ => false) adamc@1247: | (PCon1 f, [e]) => adamc@1247: (case #Variety (unNode (representative (db, e))) of adamc@1247: Dt1 (f', _) => f' = f adamc@1247: | _ => false) adamc@1247: | (Eq, [e1, e2]) => adamc@1247: let adamc@1247: val r1 = representative (db, e1) adamc@1247: val r2 = representative (db, e2) adamc@1247: in adamc@1247: repOf r1 = repOf r2 adamc@1247: end adamc@1247: | (Ge, [e1, e2]) => adamc@1247: let adamc@1247: val r1 = representative (db, e1) adamc@1247: val r2 = representative (db, e2) adamc@1247: in adamc@1247: case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of adamc@1247: (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2) adamc@1247: | _ => false adamc@1247: end adamc@1247: | _ => false) adamc@1247: handle Undetermined => false adamc@1212: adamc@1253: 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@1253: !(#Known (unNode d)) adamc@1238: orelse List.exists (fn b => repOf b = d) bs adamc@1246: orelse (case #Variety (unNode d) of adamc@1246: Dt0 _ => true adamc@1246: | Dt1 (_, d) => loop d adamc@1246: | Prim _ => true adamc@1246: | Recrd (xes, _) => List.all loop (SM.listItems (!xes)) adamc@1246: | Nothing => false) adamc@1253: orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs) adamc@1253: (SM.listItems (!(#Cons (unNode d)))) adamc@1218: end adamc@1238: adamc@1238: fun decomp e = adamc@1238: case e of adamc@1238: Func (Other _, es) => List.all decomp es adamc@1238: | _ => loop (representative (db, e)) adamc@1218: in adamc@1238: decomp d adamc@1247: end handle Undetermined => false adamc@1218: adamc@1208: end adamc@1208: adamc@1226: val tabs = ref (SM.empty : (string list * string list list) SM.map) adamc@1226: 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@1236: type check = exp * ErrorMsg.span adamc@1236: adamc@1236: structure St :> sig adamc@1236: val reset : unit -> unit adamc@1236: adamc@1236: type stashed adamc@1236: val stash : unit -> stashed adamc@1236: val reinstate : stashed -> unit adamc@1236: adamc@1249: type stashedPath adamc@1249: val stashPath : unit -> stashedPath adamc@1249: val reinstatePath : stashedPath -> unit adamc@1249: adamc@1236: val nextVar : unit -> int adamc@1236: adamc@1236: val assert : atom list -> unit adamc@1236: adamc@1236: val addPath : check -> unit adamc@1236: adamc@1236: val allowSend : atom list * exp list -> unit adamc@1253: val send : check -> unit adamc@1236: adamc@1236: val allowInsert : atom list -> unit adamc@1236: val insert : ErrorMsg.span -> unit adamc@1236: adamc@1236: val allowDelete : atom list -> unit adamc@1236: val delete : ErrorMsg.span -> unit adamc@1236: adamc@1236: val allowUpdate : atom list -> unit adamc@1236: val update : ErrorMsg.span -> unit adamc@1236: adamc@1236: val havocReln : reln -> unit adamc@1245: val havocCookie : string -> unit adamc@1238: adamc@1251: val check : atom -> bool adamc@1251: adamc@1238: val debug : unit -> unit adamc@1236: end = struct adamc@1236: adamc@1236: val hnames = ref 1 adamc@1236: adamc@1244: type hyps = int * atom list * bool ref adamc@1236: adamc@1236: val db = Cc.database () adamc@1244: val path = ref ([] : ((int * atom list) * check) option ref list) adamc@1244: val hyps = ref (0, [] : atom list, ref false) adamc@1236: val nvar = ref 0 adamc@1236: adamc@1244: fun setHyps (n', hs) = adamc@1236: let adamc@1244: val (n, _, _) = !hyps adamc@1236: in adamc@1236: if n' = n then adamc@1236: () adamc@1236: else adamc@1244: (hyps := (n', hs, ref false); adamc@1236: Cc.clear db; adamc@1236: app (fn a => Cc.assert (db, a)) hs) adamc@1236: end adamc@1236: adamc@1244: fun useKeys () = adamc@1244: let adamc@1244: val changed = ref false adamc@1244: adamc@1244: fun findKeys (hyps, acc) = adamc@1244: case hyps of adamc@1247: [] => rev acc adamc@1244: | (a as AReln (Sql tab, [r1])) :: hyps => adamc@1244: (case SM.find (!tabs, tab) of adamc@1244: NONE => findKeys (hyps, a :: acc) adamc@1244: | SOME (_, []) => findKeys (hyps, a :: acc) adamc@1244: | SOME (_, ks) => adamc@1244: let adamc@1244: fun finder (hyps, acc) = adamc@1244: case hyps of adamc@1247: [] => rev acc adamc@1244: | (a as AReln (Sql tab', [r2])) :: hyps => adamc@1244: if tab' = tab andalso adamc@1244: List.exists (List.all (fn f => adamc@1244: let adamc@1244: val r = adamc@1244: Cc.check (db, adamc@1244: AReln (Eq, [Proj (r1, f), adamc@1244: Proj (r2, f)])) adamc@1244: in adamc@1244: (*Print.prefaces "Fs" adamc@1244: [("tab", adamc@1244: Print.PD.string tab), adamc@1244: ("r1", adamc@1244: p_exp (Proj (r1, f))), adamc@1244: ("r2", adamc@1244: p_exp (Proj (r2, f))), adamc@1244: ("r", adamc@1244: Print.PD.string adamc@1244: (Bool.toString r))];*) adamc@1244: r adamc@1244: end)) ks then adamc@1244: (changed := true; adamc@1244: Cc.assert (db, AReln (Eq, [r1, r2])); adamc@1244: finder (hyps, acc)) adamc@1244: else adamc@1244: finder (hyps, a :: acc) adamc@1244: | a :: hyps => finder (hyps, a :: acc) adamc@1244: adamc@1244: val hyps = finder (hyps, []) adamc@1244: in adamc@1246: findKeys (hyps, a :: acc) adamc@1244: end) adamc@1244: | a :: hyps => findKeys (hyps, a :: acc) adamc@1244: adamc@1244: fun loop hs = adamc@1244: let adamc@1244: val hs = findKeys (hs, []) adamc@1244: in adamc@1244: if !changed then adamc@1244: (changed := false; adamc@1244: loop hs) adamc@1244: else adamc@1244: () adamc@1244: end adamc@1244: adamc@1244: val (_, hs, _) = !hyps adamc@1244: in adamc@1246: (*print "useKeys\n";*) adamc@1244: loop hs adamc@1244: end adamc@1244: adamc@1244: fun complete () = adamc@1244: let adamc@1244: val (_, _, bf) = !hyps adamc@1244: in adamc@1244: if !bf then adamc@1244: () adamc@1244: else adamc@1244: (bf := true; adamc@1244: useKeys ()) adamc@1244: end adamc@1244: adamc@1244: type stashed = int * ((int * atom list) * check) option ref list * (int * atom list) adamc@1244: fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps))) adamc@1236: fun reinstate (nv, p, h) = adamc@1236: (nvar := nv; adamc@1236: path := p; adamc@1236: setHyps h) adamc@1236: adamc@1249: type stashedPath = ((int * atom list) * check) option ref list adamc@1249: fun stashPath () = !path adamc@1249: fun reinstatePath p = path := p adamc@1249: adamc@1236: fun nextVar () = adamc@1236: let adamc@1236: val n = !nvar adamc@1236: in adamc@1236: nvar := n + 1; adamc@1236: n adamc@1236: end adamc@1236: adamc@1236: fun assert ats = adamc@1236: let adamc@1236: val n = !hnames adamc@1244: val (_, hs, _) = !hyps adamc@1236: in adamc@1236: hnames := n + 1; adamc@1244: hyps := (n, ats @ hs, ref false); adamc@1236: app (fn a => Cc.assert (db, a)) ats adamc@1236: end adamc@1236: adamc@1244: fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path adamc@1236: adamc@1236: val sendable = ref ([] : (atom list * exp list) list) adamc@1236: adamc@1238: fun checkGoals goals k = adamc@1238: let adamc@1238: fun checkGoals goals unifs = adamc@1238: case goals of adamc@1238: [] => k unifs adamc@1238: | AReln (Sql tab, [Lvar lv]) :: goals => adamc@1238: let adamc@1238: val saved = stash () adamc@1244: val (_, hyps, _) = !hyps adamc@1236: adamc@1238: fun tryAll unifs hyps = adamc@1238: case hyps of adamc@1238: [] => false adamc@1238: | AReln (Sql tab', [e]) :: hyps => adamc@1238: (tab' = tab andalso adamc@1238: checkGoals goals (IM.insert (unifs, lv, e))) adamc@1238: orelse tryAll unifs hyps adamc@1238: | _ :: hyps => tryAll unifs hyps adamc@1238: in adamc@1238: tryAll unifs hyps adamc@1238: end adamc@1243: | (g as AReln (r, es)) :: goals => adamc@1244: (complete (); adamc@1245: (if Cc.check (db, AReln (r, map (simplify unifs) es)) then adamc@1245: true adamc@1245: else adamc@1245: ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*) adamc@1245: false)) adamc@1244: andalso checkGoals goals unifs) adamc@1238: | ACond _ :: _ => false adamc@1238: in adamc@1238: checkGoals goals IM.empty adamc@1238: end adamc@1236: adamc@1253: fun buildable (e, loc) = adamc@1238: let adamc@1238: fun doPols pols acc = adamc@1236: case pols of adamc@1253: [] => adamc@1253: let adamc@1253: val b = Cc.builtFrom (db, {Base = acc, Derived = e}) adamc@1253: in adamc@1253: (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc), adamc@1253: ("Derived", p_exp e), adamc@1253: ("Hyps", Print.p_list p_atom (#2 (!hyps))), adamc@1253: ("Good", Print.PD.string (Bool.toString b))];*) adamc@1253: b adamc@1253: end adamc@1236: | (goals, es) :: pols => adamc@1238: checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc)) adamc@1238: orelse doPols pols acc adamc@1236: in adamc@1238: if doPols (!sendable) [] then adamc@1238: () adamc@1238: else adamc@1238: let adamc@1244: val (_, hs, _) = !hyps adamc@1238: in adamc@1238: ErrorMsg.errorAt loc "The information flow policy may be violated here."; adamc@1245: Print.prefaces "Situation" [("User learns", p_exp e), adamc@1253: ("Hypotheses", Print.p_list p_atom hs), adamc@1253: ("E-graph", Cc.p_database db)] adamc@1238: end adamc@1246: end adamc@1236: adamc@1236: fun checkPaths () = adamc@1236: let adamc@1244: val (n, hs, _) = !hyps adamc@1244: val hs = (n, hs) adamc@1236: in adamc@1236: app (fn r => adamc@1236: case !r of adamc@1236: NONE => () adamc@1236: | SOME (hs, e) => adamc@1236: (r := NONE; adamc@1236: setHyps hs; adamc@1253: buildable e)) (!path); adamc@1236: setHyps hs adamc@1236: end adamc@1236: adamc@1238: fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)), adamc@1243: ("exps", Print.p_list p_exp (#2 v))];*) adamc@1238: sendable := v :: !sendable) adamc@1236: adamc@1253: fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*) adamc@1253: complete (); adamc@1253: checkPaths (); adamc@1253: if isKnown e then adamc@1253: () adamc@1253: else adamc@1253: buildable (e, loc)) adamc@1236: adamc@1236: fun doable pols (loc : ErrorMsg.span) = adamc@1236: let adamc@1236: val pols = !pols adamc@1236: in adamc@1244: complete (); adamc@1236: if List.exists (fn goals => adamc@1238: if checkGoals goals (fn _ => true) then adamc@1238: ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals), adamc@1238: ("hyps", Print.p_list p_atom (#2 (!hyps)))];*) adamc@1238: true) adamc@1238: else adamc@1246: ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*, adamc@1246: ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*) adamc@1238: false)) pols then adamc@1236: () adamc@1236: else adamc@1236: let adamc@1244: val (_, hs, _) = !hyps adamc@1236: in adamc@1236: ErrorMsg.errorAt loc "The database update policy may be violated here."; adamc@1250: Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*, adamc@1250: ("E-graph", Cc.p_database db)*)] adamc@1236: end adamc@1236: end adamc@1236: adamc@1236: val insertable = ref ([] : atom list list) adamc@1236: fun allowInsert v = insertable := v :: !insertable adamc@1236: val insert = doable insertable adamc@1236: adamc@1236: val updatable = ref ([] : atom list list) adamc@1236: fun allowUpdate v = updatable := v :: !updatable adamc@1236: val update = doable updatable adamc@1236: adamc@1236: val deletable = ref ([] : atom list list) adamc@1236: fun allowDelete v = deletable := v :: !deletable adamc@1236: val delete = doable deletable adamc@1236: adamc@1238: fun reset () = (Cc.clear db; adamc@1238: path := []; adamc@1244: hyps := (0, [], ref false); adamc@1238: nvar := 0; adamc@1238: sendable := []; adamc@1238: insertable := []; adamc@1238: updatable := []; adamc@1238: deletable := []) adamc@1238: adamc@1236: fun havocReln r = adamc@1236: let adamc@1236: val n = !hnames adamc@1244: val (_, hs, _) = !hyps adamc@1236: in adamc@1236: hnames := n + 1; adamc@1244: hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false) adamc@1236: end adamc@1236: adamc@1245: fun havocCookie cname = adamc@1245: let adamc@1245: val cname = "cookie/" ^ cname adamc@1245: val n = !hnames adamc@1245: val (_, hs, _) = !hyps adamc@1245: in adamc@1245: hnames := n + 1; adamc@1245: hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false) adamc@1245: end adamc@1245: adamc@1251: fun check a = Cc.check (db, a) adamc@1251: adamc@1238: fun debug () = adamc@1238: let adamc@1244: val (_, hs, _) = !hyps adamc@1238: in adamc@1238: Print.preface ("Hyps", Print.p_list p_atom hs) adamc@1238: end adamc@1238: adamc@1236: end adamc@1236: adamc@1236: 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@1241: fun deinj env e = adamc@1241: case #1 e of adamc@1241: ERel n => SOME (List.nth (env, n)) adamc@1241: | EField (e, f) => adamc@1241: (case deinj env e of adamc@1241: NONE => NONE adamc@1241: | SOME e => SOME (Proj (e, f))) adamc@1251: | EApp ((EFfi mf, _), e) => adamc@1251: if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then adamc@1251: NONE adamc@1251: else (case deinj env e of adamc@1251: NONE => NONE adamc@1251: | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e]))) adamc@1241: | _ => NONE adamc@1241: adamc@1220: fun expIn rv env rvOf = adamc@1220: let adamc@1236: fun expIn e = adamc@1220: let adamc@1236: fun default () = inl (rv ()) adamc@1220: in adamc@1220: case e of adamc@1236: SqConst p => inl (Const p) adamc@1243: | SqTrue => inl (Func (DtCon0 "Basis.bool.True", [])) adamc@1243: | SqFalse => inl (Func (DtCon0 "Basis.bool.False", [])) adamc@1253: | Null => inl (Func (DtCon0 "None", [])) adamc@1250: | SqNot e => adamc@1250: inr (case expIn e of adamc@1250: inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])]) adamc@1250: | inr _ => Unknown) adamc@1236: | Field (v, f) => inl (Proj (rvOf v, f)) adamc@1239: | Computed _ => default () adamc@1220: | Binop (bo, e1, e2) => adamc@1220: let adamc@1236: val e1 = expIn e1 adamc@1236: val e2 = expIn e2 adamc@1220: in adamc@1236: inr (case (bo, e1, e2) of adamc@1236: (Exps f, inl e1, inl e2) => f (e1, e2) adamc@1243: | (Props f, v1, v2) => adamc@1243: let adamc@1243: fun pin v = adamc@1243: case v of adamc@1243: inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) adamc@1243: | inr p => p adamc@1243: in adamc@1243: f (pin v1, pin v2) adamc@1243: end adamc@1236: | _ => Unknown) adamc@1220: end adamc@1220: | SqKnown e => adamc@1236: (case expIn e of adamc@1236: inl e => inr (Reln (Known, [e])) adamc@1236: | _ => inr Unknown) adamc@1220: | Inj e => adamc@1241: inl (case deinj env e of adamc@1241: NONE => rv () adamc@1241: | SOME e => e) adamc@1220: | SqFunc (f, e) => adamc@1236: (case expIn e of adamc@1236: inl e => inl (Func (Other f, [e])) adamc@1220: | _ => default ()) adamc@1220: adamc@1252: | Unmodeled => inl (Func (Other "allow", [rv ()])) adamc@1220: end adamc@1220: in adamc@1220: expIn adamc@1220: end adamc@1216: adamc@1236: fun decomp {Save = save, Restore = restore, Add = add} = adamc@1216: let adamc@1236: fun go p k = adamc@1236: case p of adamc@1238: True => (k () handle Cc.Contradiction => ()) adamc@1236: | False => () adamc@1236: | Unknown => () adamc@1236: | And (p1, p2) => go p1 (fn () => go p2 k) adamc@1236: | Or (p1, p2) => adamc@1236: let adamc@1236: val saved = save () adamc@1236: in adamc@1236: go p1 k; adamc@1236: restore saved; adamc@1236: go p2 k adamc@1236: end adamc@1236: | Reln x => (add (AReln x); k ()) adamc@1236: | Cond x => (add (ACond x); k ()) adamc@1236: in adamc@1236: go adamc@1236: end adamc@1236: adamc@1236: datatype queryMode = adamc@1238: SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit adamc@1236: | AllCols of exp -> unit adamc@1236: adamc@1236: type 'a doQuery = { adamc@1236: Env : exp list, adamc@1236: NextVar : unit -> exp, adamc@1236: Add : atom -> unit, adamc@1236: Save : unit -> 'a, adamc@1236: Restore : 'a -> unit, adam@1282: Cont : queryMode adamc@1236: } adamc@1236: adamc@1241: fun doQuery (arg : 'a doQuery) (e as (_, loc)) = adamc@1236: let adamc@1241: fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query" adamc@1216: in adamc@1216: case parse query e of adamc@1216: NONE => default () adamc@1227: | SOME q => adamc@1216: let adamc@1236: fun doQuery q = adamc@1227: case q of adamc@1227: Query1 r => adamc@1227: let adamc@1238: val new = ref NONE adamc@1238: val old = ref NONE adamc@1238: adamc@1238: val rvs = map (fn (tab, v) => adamc@1238: let adamc@1238: val nv = #NextVar arg () adamc@1238: in adamc@1238: case v of adamc@1238: "New" => new := SOME (tab, nv) adamc@1238: | "Old" => old := SOME (tab, nv) adamc@1238: | _ => (); adamc@1238: (v, nv) adamc@1238: end) (#From r) adamc@1214: adamc@1227: fun rvOf v = adamc@1227: case List.find (fn (v', _) => v' = v) rvs of adamc@1227: NONE => raise Fail "Iflow.queryProp: Bad table variable" adamc@1227: | SOME (_, e) => e adamc@1214: adamc@1236: val expIn = expIn (#NextVar arg) (#Env arg) rvOf adamc@1236: adamc@1236: val saved = #Save arg () adamc@1236: fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r) adamc@1236: adam@1282: fun usedFields e = adamc@1227: case e of adam@1282: SqConst _ => [] adam@1282: | SqTrue => [] adam@1282: | SqFalse => [] adam@1282: | Null => [] adam@1282: | SqNot e => usedFields e adam@1282: | Field (v, f) => [(false, Proj (rvOf v, f))] adam@1282: | Computed _ => [] adam@1282: | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 adam@1282: | SqKnown _ => [] adam@1282: | Inj e => adam@1282: (case deinj (#Env arg) e of adam@1282: NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated"; adam@1282: []) adam@1282: | SOME e => [(true, e)]) adam@1282: | SqFunc (_, e) => usedFields e adam@1282: | Unmodeled => [] adamc@1214: adamc@1236: fun normal' () = adamc@1236: case #Cont arg of adamc@1236: SomeCol k => adamc@1227: let adamc@1236: val sis = map (fn si => adamc@1236: case si of adamc@1236: SqField (v, f) => Proj (rvOf v, f) adamc@1236: | SqExp (e, f) => adamc@1236: case expIn e of adamc@1236: inr _ => #NextVar arg () adamc@1236: | inl e => e) (#Select r) adamc@1227: in adamc@1238: k {New = !new, Old = !old, Outs = sis} adamc@1227: end adamc@1236: | AllCols k => adamc@1227: let adamc@1236: val (ts, es) = adamc@1236: foldl (fn (si, (ts, es)) => adamc@1227: case si of adamc@1227: SqField (v, f) => adamc@1227: let adamc@1227: val fs = getOpt (SM.find (ts, v), SM.empty) adamc@1227: in adamc@1236: (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es) adamc@1227: end adamc@1227: | SqExp (e, f) => adamc@1227: let adamc@1236: val e = adamc@1236: case expIn e of adamc@1236: inr _ => #NextVar arg () adamc@1236: | inl e => e adamc@1227: in adamc@1236: (ts, SM.insert (es, f, e)) adamc@1227: end) adamc@1236: (SM.empty, SM.empty) (#Select r) adamc@1227: in adamc@1236: k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs))) adamc@1236: (SM.listItemsi ts) adamc@1236: @ SM.listItemsi es)) adamc@1227: end adamc@1227: adamc@1236: fun doWhere final = adamc@1236: (addFrom (); adamc@1236: case #Where r of adamc@1253: NONE => final () adamc@1236: | SOME e => adamc@1243: let adamc@1243: val p = case expIn e of adamc@1243: inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])]) adamc@1243: | inr p => p adamc@1243: adamc@1243: val saved = #Save arg () adamc@1243: in adamc@1243: decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg} adamc@1253: p (fn () => final () handle Cc.Contradiction => ()); adamc@1243: #Restore arg saved adamc@1243: end) adamc@1236: handle Cc.Contradiction => () adamc@1236: adamc@1236: fun normal () = doWhere normal' adamc@1227: in adamc@1236: (case #Select r of adamc@1236: [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => adamc@1236: (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of adamc@1236: Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => adamc@1236: (case #Cont arg of adamc@1236: SomeCol _ => () adamc@1236: | AllCols k => adamc@1236: let adamc@1236: fun answer e = k (Recd [(f, e)]) adamc@1236: adamc@1236: val saved = #Save arg () adamc@1238: val () = (answer (Func (DtCon0 "Basis.bool.False", []))) adamc@1238: handle Cc.Contradiction => () adamc@1236: in adamc@1238: #Restore arg saved; adamc@1238: (*print "True time!\n";*) adamc@1236: doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", []))); adamc@1236: #Restore arg saved adamc@1236: end) adamc@1236: | _ => normal ()) adamc@1236: | _ => normal ()) adamc@1236: before #Restore arg saved adamc@1227: end adamc@1227: | Union (q1, q2) => adamc@1220: let adamc@1236: val saved = #Save arg () adamc@1220: in adamc@1236: doQuery q1; adamc@1236: #Restore arg saved; adamc@1236: doQuery q2; adamc@1236: #Restore arg saved adamc@1220: end adamc@1216: in adamc@1236: doQuery q adamc@1216: end adamc@1220: end adamc@1220: adamc@1211: fun evalPat env e (pt, _) = adamc@1211: case pt of adamc@1236: PWild => env adamc@1236: | PVar _ => e :: env adamc@1236: | PPrim _ => env adamc@1236: | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env) adamc@1211: | PCon (_, pc, SOME pt) => adamc@1211: let adamc@1236: val env = evalPat env (Func (UnCon (patCon pc), [e])) pt adamc@1211: in adamc@1236: St.assert [AReln (PCon1 (patCon pc), [e])]; adamc@1236: env adamc@1211: end adamc@1211: | PRecord xpts => adamc@1236: foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts adamc@1236: | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env) adamc@1211: | PSome (_, pt) => adamc@1211: let adamc@1236: val env = evalPat env (Func (UnCon "Some", [e])) pt adamc@1211: in adamc@1236: St.assert [AReln (PCon1 "Some", [e])]; adamc@1236: env adamc@1211: end adamc@1211: adamc@1251: datatype arg_mode = Fixed | Decreasing | Arbitrary adamc@1251: type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp} adamc@1251: val rfuns = ref (IM.empty : rfun IM.map) adamc@1251: adamc@1236: fun evalExp env (e as (_, loc)) k = adamc@1236: let adamc@1238: (*val () = St.debug ()*) adamc@1236: (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*) adamc@1211: adamc@1236: fun default () = k (Var (St.nextVar ())) adamc@1234: adamc@1234: fun doFfi (m, s, es) = adamc@1234: if m = "Basis" andalso SS.member (writers, s) then adamc@1234: let adamc@1236: fun doArgs es = adamc@1236: case es of adamc@1245: [] => adamc@1245: (if s = "set_cookie" then adamc@1245: case es of adam@1663: [_, (cname, _), _, _, _] => adamc@1245: (case #1 cname of adamc@1245: EPrim (Prim.String cname) => adamc@1245: St.havocCookie cname adamc@1245: | _ => ()) adamc@1245: | _ => () adamc@1245: else adamc@1245: (); adamc@1245: k (Recd [])) adam@1663: | (e, _) :: es => adamc@1253: evalExp env e (fn e => (St.send (e, loc); doArgs es)) adamc@1234: in adamc@1236: doArgs es adamc@1234: end adamc@1234: else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then adamc@1234: default () adamc@1234: else adamc@1234: let adamc@1236: fun doArgs (es, acc) = adamc@1236: case es of adamc@1236: [] => k (Func (Other (m ^ "." ^ s), rev acc)) adam@1663: | (e, _) :: es => adamc@1236: evalExp env e (fn e => doArgs (es, e :: acc)) adamc@1234: in adamc@1236: doArgs (es, []) adamc@1234: end adamc@1200: in adamc@1200: case #1 e of adamc@1236: EPrim p => k (Const p) adamc@1236: | ERel n => k (List.nth (env, n)) adamc@1200: | ENamed _ => default () adamc@1236: | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), [])) adamc@1236: | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e]))) adamc@1236: | ENone _ => k (Func (DtCon0 "None", [])) adamc@1236: | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e]))) adamc@1200: | EFfi _ => default () adamc@1213: adamc@1250: | EFfiApp ("Basis", "rand", []) => adamc@1250: let adamc@1250: val e = Var (St.nextVar ()) adamc@1250: in adamc@1250: St.assert [AReln (Known, [e])]; adamc@1250: k e adamc@1250: end adamc@1234: | EFfiApp x => doFfi x adam@1663: | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [(e, (TRecord [], loc))]) adamc@1213: adamc@1251: | EApp (e1 as (EError _, _), _) => evalExp env e1 k adamc@1251: adamc@1251: | EApp (e1, e2) => adamc@1251: let adamc@1251: fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call"; adamc@1251: Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e); adamc@1251: default ()) adamc@1251: adamc@1251: fun doArgs (e, args) = adamc@1251: case #1 e of adamc@1251: EApp (e1, e2) => doArgs (e1, e2 :: args) adamc@1251: | ENamed n => adamc@1251: (case IM.find (!rfuns, n) of adamc@1251: NONE => adefault () adamc@1251: | SOME rf => adamc@1251: if length (#args rf) <> length args then adamc@1251: adefault () adamc@1251: else adamc@1251: let adamc@1251: val () = (SS.app (St.havocReln o Sql) (#tables rf); adamc@1251: SS.app St.havocCookie (#cookies rf)) adamc@1251: val saved = St.stash () adamc@1251: adamc@1251: fun doArgs (args, modes, env') = adamc@1251: case (args, modes) of adamc@1251: ([], []) => (evalExp env' (#body rf) (fn _ => ()); adamc@1251: St.reinstate saved; adamc@1251: default ()) adamc@1251: adamc@1251: | (arg :: args, mode :: modes) => adamc@1251: evalExp env arg (fn arg => adamc@1251: let adamc@1251: val v = case mode of adamc@1251: Arbitrary => Var (St.nextVar ()) adamc@1251: | Fixed => arg adamc@1251: | Decreasing => adamc@1251: let adamc@1251: val v = Var (St.nextVar ()) adamc@1251: in adamc@1251: if St.check (AReln (Known, [arg])) then adamc@1251: St.assert [(AReln (Known, [v]))] adamc@1251: else adamc@1251: (); adamc@1251: v adamc@1251: end adamc@1251: in adamc@1251: doArgs (args, modes, v :: env') adamc@1251: end) adamc@1251: | _ => raise Fail "Iflow.doArgs: Impossible" adamc@1251: in adamc@1251: doArgs (args, #args rf, []) adamc@1251: end) adamc@1251: | _ => adefault () adamc@1251: in adamc@1251: doArgs (e, []) adamc@1251: end adamc@1213: adamc@1200: | EAbs _ => default () adamc@1236: | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1]))) adam@1360: | EBinop (_, s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2])))) adamc@1200: | ERecord xets => adamc@1200: let adamc@1236: fun doFields (xes, acc) = adamc@1236: case xes of adamc@1236: [] => k (Recd (rev acc)) adamc@1236: | (x, e, _) :: xes => adamc@1236: evalExp env e (fn e => doFields (xes, (x, e) :: acc)) adamc@1200: in adamc@1236: doFields (xets, []) adamc@1200: end adamc@1236: | EField (e, s) => evalExp env e (fn e => k (Proj (e, s))) adamc@1218: | ECase (e, pes, {result = res, ...}) => adamc@1236: evalExp env e (fn e => adamc@1248: if List.all (fn (_, (EWrite (EPrim _, _), _)) => true adamc@1248: | _ => false) pes then adamc@1253: (St.send (e, loc); adamc@1248: k (Recd [])) adamc@1248: else adamc@1248: (St.addPath (e, loc); adamc@1248: app (fn (p, pe) => adamc@1248: let adamc@1248: val saved = St.stash () adamc@1248: in adamc@1248: let adamc@1248: val env = evalPat env e p adamc@1248: in adamc@1248: evalExp env pe k; adamc@1248: St.reinstate saved adamc@1248: end adamc@1248: handle Cc.Contradiction => St.reinstate saved adamc@1248: end) pes)) adamc@1200: | EStrcat (e1, e2) => adamc@1236: evalExp env e1 (fn e1 => adamc@1236: evalExp env e2 (fn e2 => adamc@1236: k (Func (Other "cat", [e1, e2])))) adamc@1253: | EError (e, _) => evalExp env e (fn e => St.send (e, loc)) adamc@1200: | EReturnBlob {blob = b, mimeType = m, ...} => adamc@1236: evalExp env b (fn b => adamc@1253: (St.send (b, loc); adamc@1236: evalExp env m adamc@1253: (fn m => St.send (m, loc)))) adamc@1200: | ERedirect (e, _) => adamc@1253: evalExp env e (fn e => St.send (e, loc)) adamc@1200: | EWrite e => adamc@1253: evalExp env e (fn e => (St.send (e, loc); adamc@1236: k (Recd []))) adamc@1200: | ESeq (e1, e2) => adamc@1249: let adamc@1249: val path = St.stashPath () adamc@1249: in adamc@1249: evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k)) adamc@1249: end adamc@1200: | ELet (_, _, e1, e2) => adamc@1236: evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k) adamc@1200: | EClosure (n, es) => adamc@1200: let adamc@1236: fun doArgs (es, acc) = adamc@1236: case es of adamc@1236: [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc)) adamc@1236: | e :: es => adamc@1236: evalExp env e (fn e => doArgs (es, e :: acc)) adamc@1200: in adamc@1236: doArgs (es, []) adamc@1200: end adamc@1200: adamc@1235: | EQuery {query = q, body = b, initial = i, state = state, ...} => adamc@1238: evalExp env i (fn i => adamc@1238: let adamc@1238: val r = Var (St.nextVar ()) adamc@1238: val acc = Var (St.nextVar ()) adamc@1242: adamc@1249: val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st, adamc@1249: exp = fn (e, st as (cs, ts)) => adamc@1242: case e of adam@1293: EDml (e, _) => adamc@1242: (case parse dml e of adamc@1249: NONE => st adamc@1242: | SOME c => adamc@1242: case c of adamc@1249: Insert _ => st adamc@1242: | Delete (tab, _) => adamc@1249: (cs, SS.add (ts, tab)) adamc@1242: | Update (tab, _, _) => adamc@1249: (cs, SS.add (ts, tab))) adamc@1249: | EFfiApp ("Basis", "set_cookie", adam@1663: [_, ((EPrim (Prim.String cname), _), _), adamc@1249: _, _, _]) => adamc@1249: (SS.add (cs, cname), ts) adamc@1249: | _ => st} adamc@1249: (SS.empty, SS.empty) b adamc@1238: in adamc@1249: case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of adamc@1249: (TRecord [], true, true) => () adamc@1249: | _ => adamc@1249: let adamc@1249: val saved = St.stash () adamc@1249: in adamc@1249: (k i) adamc@1249: handle Cc.Contradiction => (); adamc@1249: St.reinstate saved adamc@1249: end; adamc@1249: adamc@1249: SS.app (St.havocReln o Sql) ts; adamc@1249: SS.app St.havocCookie cs; adamc@1242: adamc@1242: doQuery {Env = env, adamc@1242: NextVar = Var o St.nextVar, adamc@1242: Add = fn a => St.assert [a], adamc@1242: Save = St.stash, adamc@1242: Restore = St.reinstate, adamc@1242: Cont = AllCols (fn x => adamc@1242: (St.assert [AReln (Eq, [r, x])]; adamc@1242: evalExp (acc :: r :: env) b k))} q adamc@1238: end) adam@1293: | 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@1236: val new = St.nextVar () adamc@1220: adamc@1236: val expIn = expIn (Var o St.nextVar) env adamc@1236: (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]") adamc@1220: adamc@1236: val es = map (fn (x, e) => adamc@1236: case expIn e of adamc@1236: inl e => (x, e) adamc@1236: | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]") adamc@1236: es adamc@1220: adamc@1236: val saved = St.stash () adamc@1220: in adamc@1236: St.assert [AReln (Sql (tab ^ "$New"), [Recd es])]; adamc@1236: St.insert loc; adamc@1236: St.reinstate saved; adamc@1251: St.assert [AReln (Sql tab, [Recd es])]; adamc@1236: k (Recd []) adamc@1221: end adamc@1221: | Delete (tab, e) => adamc@1221: let adamc@1236: val old = St.nextVar () adamc@1236: adamc@1236: val expIn = expIn (Var o St.nextVar) env adamc@1236: (fn "T" => Var old adamc@1236: | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE") adamc@1221: adamc@1236: val p = case expIn e of adamc@1236: inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" adamc@1236: | inr p => p adamc@1236: adamc@1236: val saved = St.stash () adamc@1221: in adamc@1246: St.assert [AReln (Sql (tab ^ "$Old"), [Var old]), adamc@1246: AReln (Sql (tab), [Var old])]; adamc@1236: decomp {Save = St.stash, adamc@1236: Restore = St.reinstate, adamc@1236: Add = fn a => St.assert [a]} p adamc@1236: (fn () => (St.delete loc; adamc@1236: St.reinstate saved; adamc@1236: St.havocReln (Sql tab); adamc@1236: k (Recd [])) adamc@1236: handle Cc.Contradiction => ()) adamc@1223: end adamc@1223: | Update (tab, fs, e) => adamc@1223: let adamc@1236: val new = St.nextVar () adamc@1236: val old = St.nextVar () adamc@1223: adamc@1236: val expIn = expIn (Var o St.nextVar) env adamc@1236: (fn "T" => Var old adamc@1236: | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE") adamc@1223: adamc@1236: val fs = map adamc@1236: (fn (x, e) => adamc@1236: (x, case expIn e of adamc@1236: inl e => e adamc@1236: | inr _ => raise Fail adamc@1236: ("Iflow.evalExp: Selecting " adamc@1236: ^ "boolean expression"))) adamc@1236: 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@1236: val p = case expIn e of adamc@1236: inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" adamc@1236: | inr p => p adamc@1236: val saved = St.stash () adamc@1223: in adamc@1236: St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]), adamc@1246: AReln (Sql (tab ^ "$Old"), [Var old]), adamc@1246: AReln (Sql tab, [Var old])]; adamc@1236: decomp {Save = St.stash, adamc@1236: Restore = St.reinstate, adamc@1236: Add = fn a => St.assert [a]} p adamc@1236: (fn () => (St.update loc; adamc@1236: St.reinstate saved; adamc@1236: St.havocReln (Sql tab); adamc@1236: k (Recd [])) adamc@1236: handle Cc.Contradiction => ()) adamc@1220: end) adamc@1220: adamc@1229: | ENextval (EPrim (Prim.String seq), _) => adamc@1229: let adamc@1236: val nv = St.nextVar () adamc@1229: in adamc@1236: St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])]; adamc@1236: k (Var nv) adamc@1229: end adamc@1200: | ENextval _ => default () adamc@1200: | ESetval _ => default () adamc@1200: adam@1663: | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String cname), _), _)]), _), _, _) => adamc@1217: let adamc@1238: val e = Var (St.nextVar ()) adamc@1245: val e' = Func (Other ("cookie/" ^ cname), []) adamc@1217: in adamc@1245: St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])]; adamc@1238: k e 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@1251: datatype var_source = Input of int | SubInput of int | Unknown adamc@1251: adamc@1200: fun check file = adamc@1200: let adamc@1251: val () = (St.reset (); adamc@1251: rfuns := IM.empty) adamc@1236: 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@1249: fun decl (d, loc) = 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@1236: tabs := SM.insert (!tabs, String.extract (tab, 3, NONE), adamc@1236: (map #1 fs, adamc@1236: map (map (fn s => str (Char.toUpper (String.sub (s, 3))) adamc@1236: ^ String.extract (s, 4, NONE))) ks)) adamc@1226: else adamc@1226: raise Fail "Table name does not begin with uw_" adamc@1226: end adamc@1238: | DVal (x, n, _, e, _) => adamc@1200: let adamc@1238: (*val () = print ("\n=== " ^ x ^ " ===\n\n");*) adamc@1238: adamc@1207: val isExptd = IS.member (exptd, n) adamc@1207: adamc@1236: val saved = St.stash () adamc@1236: adamc@1236: fun deAbs (e, env, ps) = adamc@1200: case #1 e of adamc@1236: EAbs (_, _, _, e) => adamc@1236: let adamc@1236: val nv = Var (St.nextVar ()) adamc@1236: in adamc@1236: deAbs (e, nv :: env, adamc@1236: if isExptd then adamc@1236: AReln (Known, [nv]) :: ps adamc@1236: else adamc@1236: ps) adamc@1236: end adamc@1236: | _ => (e, env, ps) adamc@1200: adamc@1236: val (e, env, ps) = deAbs (e, [], []) adamc@1200: in adamc@1236: St.assert ps; adamc@1236: (evalExp env e (fn _ => ()) handle Cc.Contradiction => ()); adamc@1236: St.reinstate saved adamc@1200: end adamc@1202: adamc@1251: | DValRec [(x, n, _, e, _)] => adamc@1251: let adamc@1251: val tables = ref SS.empty adamc@1251: val cookies = ref SS.empty adamc@1251: adamc@1251: fun deAbs (e, env, modes) = adamc@1251: case #1 e of adamc@1251: EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes) adamc@1251: | _ => (e, env, rev modes) adamc@1251: adamc@1251: val (e, env, modes) = deAbs (e, [], []) adamc@1251: adamc@1251: fun doExp env (e as (_, loc)) = adamc@1251: case #1 e of adamc@1251: EPrim _ => e adamc@1251: | ERel _ => e adamc@1251: | ENamed _ => e adamc@1251: | ECon (_, _, NONE) => e adamc@1251: | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc) adamc@1251: | ENone _ => e adamc@1251: | ESome (t, e) => (ESome (t, doExp env e), loc) adamc@1251: | EFfi _ => e adamc@1251: | EFfiApp (m, f, es) => adamc@1251: (case (m, f, es) of adam@1663: ("Basis", "set_cookie", [_, ((EPrim (Prim.String cname), _), _), _, _, _]) => adamc@1251: cookies := SS.add (!cookies, cname) adamc@1251: | _ => (); adam@1663: (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc)) adamc@1251: adamc@1251: | EApp (e1, e2) => adamc@1251: let adamc@1251: fun default () = (EApp (doExp env e1, doExp env e2), loc) adamc@1251: adamc@1251: fun explore (e, args) = adamc@1251: case #1 e of adamc@1251: EApp (e1, e2) => explore (e1, e2 :: args) adamc@1251: | ENamed n' => adamc@1251: if n' = n then adamc@1251: let adamc@1251: fun doArgs (pos, args, modes) = adamc@1251: case (args, modes) of adamc@1251: ((e1, _) :: args, m1 :: modes) => adamc@1251: (case e1 of adamc@1251: ERel n => adamc@1251: (case List.nth (env, n) of adamc@1251: Input pos' => adamc@1251: if pos' = pos then adamc@1251: () adamc@1251: else adamc@1251: m1 := Arbitrary adamc@1251: | SubInput pos' => adamc@1251: if pos' = pos then adamc@1251: if !m1 = Arbitrary then adamc@1251: () adamc@1251: else adamc@1251: m1 := Decreasing adamc@1251: else adamc@1251: m1 := Arbitrary adamc@1251: | Unknown => m1 := Arbitrary) adamc@1251: | _ => m1 := Arbitrary; adamc@1251: doArgs (pos + 1, args, modes)) adamc@1251: | (_ :: _, []) => () adamc@1251: | ([], ms) => app (fn m => m := Arbitrary) ms adamc@1251: in adamc@1251: doArgs (0, args, modes); adamc@1251: (EFfi ("Basis", "?"), loc) adamc@1251: end adamc@1251: else adamc@1251: default () adamc@1251: | _ => default () adamc@1251: in adamc@1251: explore (e, []) adamc@1251: end adamc@1251: | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc) adamc@1251: | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc) adam@1360: | EBinop (bi, bo, e1, e2) => (EBinop (bi, bo, doExp env e1, doExp env e2), loc) adamc@1251: | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc) adamc@1251: | EField (e1, f) => (EField (doExp env e1, f), loc) adamc@1251: | ECase (e, pes, ts) => adamc@1251: let adamc@1251: val source = adamc@1251: case #1 e of adamc@1251: ERel n => adamc@1251: (case List.nth (env, n) of adamc@1251: Input n => SOME n adamc@1251: | SubInput n => SOME n adamc@1251: | Unknown => NONE) adamc@1251: | _ => NONE adamc@1251: adamc@1251: fun doV v = adamc@1251: let adamc@1251: fun doPat (p, env) = adamc@1251: case #1 p of adamc@1251: PWild => env adamc@1251: | PVar _ => v :: env adamc@1251: | PPrim _ => env adamc@1251: | PCon (_, _, NONE) => env adamc@1251: | PCon (_, _, SOME p) => doPat (p, env) adamc@1251: | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts adamc@1251: | PNone _ => env adamc@1251: | PSome (_, p) => doPat (p, env) adamc@1251: in adamc@1251: (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc) adamc@1251: end adamc@1251: in adamc@1251: case source of adamc@1251: NONE => doV Unknown adamc@1251: | SOME inp => doV (SubInput inp) adamc@1251: end adamc@1251: | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc) adamc@1251: | EError (e1, t) => (EError (doExp env e1, t), loc) adamc@1251: | EReturnBlob {blob = b, mimeType = m, t} => adamc@1251: (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc) adamc@1251: | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc) adamc@1251: | EWrite e1 => (EWrite (doExp env e1), loc) adamc@1251: | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc) adamc@1251: | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc) adamc@1251: | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc) adamc@1251: | EQuery {exps, tables, state, query, body, initial} => adamc@1251: (EQuery {exps = exps, tables = tables, state = state, adamc@1251: query = doExp env query, adamc@1251: body = doExp (Unknown :: Unknown :: env) body, adamc@1251: initial = doExp env initial}, loc) adam@1293: | EDml (e1, mode) => adamc@1251: (case parse dml e1 of adamc@1251: NONE => () adamc@1251: | SOME c => adamc@1251: case c of adamc@1251: Insert _ => () adamc@1251: | Delete (tab, _) => adamc@1251: tables := SS.add (!tables, tab) adamc@1251: | Update (tab, _, _) => adamc@1251: tables := SS.add (!tables, tab); adam@1293: (EDml (doExp env e1, mode), loc)) adamc@1251: | ENextval e1 => (ENextval (doExp env e1), loc) adamc@1251: | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc) adamc@1251: | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc) adamc@1251: | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc) adamc@1251: | ESignalReturn _ => e adamc@1251: | ESignalBind _ => e adamc@1251: | ESignalSource _ => e adamc@1251: | EServerCall _ => e adamc@1251: | ERecv _ => e adamc@1251: | ESleep _ => e adamc@1251: | ESpawn _ => e adamc@1251: adamc@1251: val e = doExp env e adamc@1251: in adamc@1251: rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies, adamc@1251: args = map (fn r => !r) modes, body = e}) adamc@1251: end adamc@1251: adamc@1251: | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet." adamc@1249: adamc@1220: | DPolicy pol => adamc@1218: let adamc@1236: val rvN = ref 0 adamc@1236: fun rv () = adamc@1236: let adamc@1236: val n = !rvN adamc@1236: in adamc@1236: rvN := n + 1; adamc@1236: Lvar n adamc@1236: end adamc@1236: adamc@1236: val atoms = ref ([] : atom list) adamc@1236: fun doQ k = doQuery {Env = [], adamc@1236: NextVar = rv, adamc@1236: Add = fn a => atoms := a :: !atoms, adamc@1236: Save = fn () => !atoms, adamc@1236: Restore = fn ls => atoms := ls, adamc@1238: Cont = SomeCol (fn r => k (rev (!atoms), r))} adamc@1238: adamc@1247: fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) => adamc@1247: tab' <> tab adamc@1247: orelse List.all (fn Lvar lv' => lv' <> lv adamc@1247: | _ => false) nams adamc@1247: | _ => true) adamc@1218: in adamc@1220: case pol of adamc@1220: PolClient e => adamc@1238: doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e adamc@1220: | PolInsert e => adamc@1238: doQ (fn (ats, {New = SOME (tab, new), ...}) => adamc@1247: St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats) adamc@1238: | _ => raise Fail "Iflow: No New in mayInsert policy") e adamc@1221: | PolDelete e => adamc@1238: doQ (fn (ats, {Old = SOME (tab, old), ...}) => adamc@1247: St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats) adamc@1238: | _ => raise Fail "Iflow: No Old in mayDelete policy") e adamc@1223: | PolUpdate e => adamc@1238: doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) => adamc@1238: St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old]) adamc@1238: :: AReln (Sql (tab ^ "$New"), [new]) adamc@1247: :: untab (tab, [new, old]) ats) adamc@1238: | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e adamc@1229: | PolSequence e => adamc@1229: (case #1 e of adamc@1229: EPrim (Prim.String seq) => adamc@1229: let adamc@1236: val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0]) adamc@1229: val outs = [Lvar 0] adamc@1229: in adamc@1236: St.allowSend ([p], outs) adamc@1229: end adamc@1236: | _ => ()) adamc@1218: end adamc@1214: adamc@1236: | _ => () adamc@1200: in adamc@1236: app decl file 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