summaryrefslogtreecommitdiff
path: root/src/iflow.sml
diff options
context:
space:
mode:
authorBenjamin Barenblat <bbaren@mit.edu>2017-07-23 09:50:04 -0400
committerBenjamin Barenblat <bbaren@mit.edu>2017-07-23 09:50:04 -0400
commit0cccdb0ae595cd7e3e136e984ac7b95b99f71a53 (patch)
tree491d3b13813610943c60460d3e178d3a73916346 /src/iflow.sml
Import urweb_20170720+dfsg.orig.tar.gz
[dgit import orig urweb_20170720+dfsg.orig.tar.gz]
Diffstat (limited to 'src/iflow.sml')
-rw-r--r--src/iflow.sml2184
1 files changed, 2184 insertions, 0 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
new file mode 100644
index 0000000..5e8d697
--- /dev/null
+++ b/src/iflow.sml
@@ -0,0 +1,2184 @@
+(* Copyright (c) 2010, 2013, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Iflow :> IFLOW = struct
+
+open Mono
+open Sql
+
+structure IS = IntBinarySet
+structure IM = IntBinaryMap
+
+structure SK = struct
+type ord_key = string
+val compare = String.compare
+end
+
+structure SS = BinarySetFn(SK)
+structure SM = BinaryMapFn(SK)
+
+val writers = ["htmlifyInt_w",
+ "htmlifyFloat_w",
+ "htmlifyString_w",
+ "htmlifyBool_w",
+ "htmlifyTime_w",
+ "attrifyInt_w",
+ "attrifyFloat_w",
+ "attrifyString_w",
+ "attrifyChar_w",
+ "urlifyInt_w",
+ "urlifyFloat_w",
+ "urlifyString_w",
+ "urlifyBool_w",
+ "set_cookie"]
+
+val writers = SS.addList (SS.empty, writers)
+
+local
+ open Print
+ val string = PD.string
+in
+
+fun p_func f =
+ string (case f of
+ DtCon0 s => s
+ | DtCon1 s => s
+ | UnCon s => "un" ^ s
+ | Other s => s)
+
+fun p_exp e =
+ case e of
+ Const p => Prim.p_t p
+ | Var n => string ("x" ^ Int.toString n)
+ | Lvar n => string ("X" ^ Int.toString n)
+ | Func (f, es) => box [p_func f,
+ string "(",
+ p_list p_exp es,
+ string ")"]
+ | Recd xes => box [string "{",
+ p_list (fn (x, e) => box [string x,
+ space,
+ string "=",
+ space,
+ p_exp e]) xes,
+ string "}"]
+ | Proj (e, x) => box [p_exp e,
+ string ("." ^ x)]
+
+fun p_bop s es =
+ case es of
+ [e1, e2] => box [p_exp e1,
+ space,
+ string s,
+ space,
+ p_exp e2]
+ | _ => raise Fail "Iflow.p_bop"
+
+fun p_reln r es =
+ case r of
+ Known =>
+ (case es of
+ [e] => box [string "known(",
+ p_exp e,
+ string ")"]
+ | _ => raise Fail "Iflow.p_reln: Known")
+ | Sql s => box [string (s ^ "("),
+ p_list p_exp es,
+ string ")"]
+ | PCon0 s => box [string (s ^ "("),
+ p_list p_exp es,
+ string ")"]
+ | PCon1 s => box [string (s ^ "("),
+ p_list p_exp es,
+ string ")"]
+ | Cmp Eq => p_bop "=" es
+ | Cmp Ne => p_bop "<>" es
+ | Cmp Lt => p_bop "<" es
+ | Cmp Le => p_bop "<=" es
+ | Cmp Gt => p_bop ">" es
+ | Cmp Ge => p_bop ">=" es
+
+fun p_prop p =
+ case p of
+ True => string "True"
+ | False => string "False"
+ | Unknown => string "??"
+ | Lop (And, p1, p2) => box [string "(",
+ p_prop p1,
+ string ")",
+ space,
+ string "&&",
+ space,
+ string "(",
+ p_prop p2,
+ string ")"]
+ | Lop (Or, p1, p2) => box [string "(",
+ p_prop p1,
+ string ")",
+ space,
+ string "||",
+ space,
+ string "(",
+ p_prop p2,
+ string ")"]
+ | Reln (r, es) => p_reln r es
+ | Cond (e, p) => box [string "(",
+ p_exp e,
+ space,
+ string "==",
+ space,
+ p_prop p,
+ string ")"]
+
+end
+
+fun isKnown e =
+ case e of
+ Const _ => true
+ | Func (_, es) => List.all isKnown es
+ | Recd xes => List.all (isKnown o #2) xes
+ | Proj (e, _) => isKnown e
+ | _ => false
+
+fun simplify unif =
+ let
+ fun simplify e =
+ case e of
+ Const _ => e
+ | Var _ => e
+ | Lvar n =>
+ (case IM.find (unif, n) of
+ NONE => e
+ | SOME e => simplify e)
+ | Func (f, es) => Func (f, map simplify es)
+ | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
+ | Proj (e, s) => Proj (simplify e, s)
+ in
+ simplify
+ end
+
+datatype atom =
+ AReln of reln * exp list
+ | ACond of exp * prop
+
+fun p_atom a =
+ p_prop (case a of
+ AReln x => Reln x
+ | ACond x => Cond x)
+
+(* Congruence closure *)
+structure Cc :> sig
+ type database
+
+ exception Contradiction
+
+ val database : unit -> database
+ val clear : database -> unit
+
+ val assert : database * atom -> unit
+ val check : database * atom -> bool
+
+ val p_database : database Print.printer
+
+ val builtFrom : database * {Base : exp list, Derived : exp} -> bool
+
+ val p_repOf : database -> exp Print.printer
+end = struct
+
+local
+ val count = ref 0
+in
+fun nodeId () =
+ let
+ val n = !count
+ in
+ count := n + 1;
+ n
+ end
+end
+
+exception Contradiction
+exception Undetermined
+
+structure CM = BinaryMapFn(struct
+ type ord_key = Prim.t
+ val compare = Prim.compare
+ end)
+
+datatype node = Node of {Id : int,
+ Rep : node ref option ref,
+ Cons : node ref SM.map ref,
+ Variety : variety,
+ Known : bool ref,
+ Ge : Int64.int option ref}
+
+ and variety =
+ Dt0 of string
+ | Dt1 of string * node ref
+ | Prim of Prim.t
+ | Recrd of node ref SM.map ref * bool
+ | Nothing
+
+type representative = node ref
+
+type database = {Vars : representative IM.map ref,
+ Consts : representative CM.map ref,
+ Con0s : representative SM.map ref,
+ Records : (representative SM.map * representative) list ref,
+ Funcs : ((string * representative list) * representative) list ref}
+
+fun database () = {Vars = ref IM.empty,
+ Consts = ref CM.empty,
+ Con0s = ref SM.empty,
+ Records = ref [],
+ Funcs = ref []}
+
+fun clear (t : database) = (#Vars t := IM.empty;
+ #Consts t := CM.empty;
+ #Con0s t := SM.empty;
+ #Records t := [];
+ #Funcs t := [])
+
+fun unNode n =
+ case !n of
+ Node r => r
+
+open Print
+val string = PD.string
+val newline = PD.newline
+
+fun p_rep n =
+ case !(#Rep (unNode n)) of
+ SOME n => p_rep n
+ | NONE =>
+ box [string (Int.toString (#Id (unNode n)) ^ ":"),
+ space,
+ case #Variety (unNode n) of
+ Nothing => string "?"
+ | Dt0 s => string ("Dt0(" ^ s ^ ")")
+ | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
+ space,
+ p_rep n,
+ string ")"]
+ | Prim p => Prim.p_t p
+ | Recrd (ref m, b) => box [string "{",
+ p_list (fn (x, n) => box [string x,
+ space,
+ string "=",
+ space,
+ p_rep n]) (SM.listItemsi m),
+ string "}",
+ if b then
+ box [space,
+ string "(complete)"]
+ else
+ box []],
+ if !(#Known (unNode n)) then
+ string " (known)"
+ else
+ box [],
+ case !(#Ge (unNode n)) of
+ NONE => box []
+ | SOME n => string (" (>= " ^ Int64.toString n ^ ")")]
+
+fun p_database (db : database) =
+ box [string "Vars:",
+ newline,
+ p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
+ space,
+ string "=",
+ space,
+ p_rep n]) (IM.listItemsi (!(#Vars db)))]
+
+fun repOf (n : representative) : representative =
+ case !(#Rep (unNode n)) of
+ NONE => n
+ | SOME r =>
+ let
+ val r = repOf r
+ in
+ #Rep (unNode n) := SOME r;
+ r
+ end
+
+fun markKnown r =
+ let
+ val r = repOf r
+ in
+ (*Print.preface ("markKnown", p_rep r);*)
+ if !(#Known (unNode r)) then
+ ()(*TextIO.print "Already known\n"*)
+ else
+ (#Known (unNode r) := true;
+ SM.app markKnown (!(#Cons (unNode r)));
+ case #Variety (unNode r) of
+ Dt1 (_, r) => markKnown r
+ | Recrd (xes, _) => SM.app markKnown (!xes)
+ | _ => ())
+ end
+
+fun representative (db : database, e) =
+ let
+ fun rep e =
+ case e of
+ Const p => (case CM.find (!(#Consts db), p) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Prim p,
+ Known = ref true,
+ Ge = ref (case p of
+ Prim.Int n => SOME n
+ | _ => NONE)})
+ in
+ #Consts db := CM.insert (!(#Consts db), p, r);
+ r
+ end)
+ | Var n => (case IM.find (!(#Vars db), n) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref false,
+ Ge = ref NONE})
+ in
+ #Vars db := IM.insert (!(#Vars db), n, r);
+ r
+ end)
+ | Lvar _ => raise Undetermined
+ | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt0 f,
+ Known = ref true,
+ Ge = ref NONE})
+ in
+ #Con0s db := SM.insert (!(#Con0s db), f, r);
+ r
+ end)
+ | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
+ | Func (DtCon1 f, [e]) =>
+ let
+ val r = rep e
+ in
+ case SM.find (!(#Cons (unNode r)), f) of
+ SOME r => repOf r
+ | NONE =>
+ let
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt1 (f, r),
+ Known = ref (!(#Known (unNode r))),
+ Ge = ref NONE})
+ in
+ #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
+ r'
+ end
+ end
+ | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
+ | Func (UnCon f, [e]) =>
+ let
+ val r = rep e
+ in
+ case #Variety (unNode r) of
+ Dt1 (f', n) => if f' = f then
+ repOf n
+ else
+ raise Contradiction
+ | Nothing =>
+ let
+ val cons = ref SM.empty
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = cons,
+ Variety = Nothing,
+ Known = ref (!(#Known (unNode r))),
+ Ge = ref NONE})
+
+ val r'' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = #Cons (unNode r),
+ Variety = Dt1 (f, r'),
+ Known = #Known (unNode r),
+ Ge = ref NONE})
+ in
+ cons := SM.insert (!cons, f, r'');
+ #Rep (unNode r) := SOME r'';
+ r'
+ end
+ | _ => raise Contradiction
+ end
+ | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
+ | Func (Other f, es) =>
+ let
+ val rs = map rep es
+ in
+ case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
+ NONE =>
+ let
+ val r = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref (f = "allow"),
+ Ge = ref NONE})
+ in
+ #Funcs db := ((f, rs), r) :: (!(#Funcs db));
+ r
+ end
+ | SOME (_, r) => repOf r
+ end
+ | Recd xes =>
+ let
+ val xes = map (fn (x, e) => (x, rep e)) xes
+ val len = length xes
+ in
+ case List.find (fn (xes', _) =>
+ SM.numItems xes' = len
+ andalso List.all (fn (x, n) =>
+ case SM.find (xes', x) of
+ NONE => false
+ | SOME n' => n = repOf n') xes)
+ (!(#Records db)) of
+ SOME (_, r) => repOf r
+ | NONE =>
+ let
+ val xes = foldl SM.insert' SM.empty xes
+
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Recrd (ref xes, true),
+ Known = ref false,
+ Ge = ref NONE})
+ in
+ #Records db := (xes, r') :: (!(#Records db));
+ r'
+ end
+ end
+ | Proj (e, f) =>
+ let
+ val r = rep e
+ in
+ case #Variety (unNode r) of
+ Recrd (xes, _) =>
+ (case SM.find (!xes, f) of
+ SOME r => repOf r
+ | NONE => let
+ val r = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref (!(#Known (unNode r))),
+ Ge = ref NONE})
+ in
+ xes := SM.insert (!xes, f, r);
+ r
+ end)
+ | Nothing =>
+ let
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Nothing,
+ Known = ref (!(#Known (unNode r))),
+ Ge = ref NONE})
+
+ val r'' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = #Cons (unNode r),
+ Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
+ Known = #Known (unNode r),
+ Ge = ref NONE})
+ in
+ #Rep (unNode r) := SOME r'';
+ r'
+ end
+ | _ => raise Contradiction
+ end
+ in
+ rep e
+ end
+
+fun p_repOf db e = p_rep (representative (db, e))
+
+fun assert (db, a) =
+ let
+ fun markEq (r1, r2) =
+ let
+ val r1 = repOf r1
+ val r2 = repOf r2
+ in
+ if r1 = r2 then
+ ()
+ else case (#Variety (unNode r1), #Variety (unNode r2)) of
+ (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
+ ()
+ else
+ raise Contradiction
+ | (Dt0 f1, Dt0 f2) => if f1 = f2 then
+ ()
+ else
+ raise Contradiction
+ | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
+ markEq (r1, r2)
+ else
+ raise Contradiction
+ | (Recrd (xes1, _), Recrd (xes2, _)) =>
+ let
+ fun unif (xes1, xes2) =
+ SM.appi (fn (x, r1) =>
+ case SM.find (!xes2, x) of
+ NONE => xes2 := SM.insert (!xes2, x, r1)
+ | SOME r2 => markEq (r1, r2)) (!xes1)
+ in
+ unif (xes1, xes2);
+ unif (xes2, xes1)
+ end
+ | (Nothing, _) => mergeNodes (r1, r2)
+ | (_, Nothing) => mergeNodes (r2, r1)
+ | _ => raise Contradiction
+ end
+
+ and mergeNodes (r1, r2) =
+ (#Rep (unNode r1) := SOME r2;
+ if !(#Known (unNode r1)) then
+ markKnown r2
+ else
+ ();
+ if !(#Known (unNode r2)) then
+ markKnown r1
+ else
+ ();
+ #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
+
+ case !(#Ge (unNode r1)) of
+ NONE => ()
+ | SOME n1 =>
+ case !(#Ge (unNode r2)) of
+ NONE => #Ge (unNode r2) := SOME n1
+ | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));
+
+ compactFuncs ())
+
+ and compactFuncs () =
+ let
+ fun loop funcs =
+ case funcs of
+ [] => []
+ | (fr as ((f, rs), r)) :: rest =>
+ let
+ val rest = List.filter (fn ((f' : string, rs'), r') =>
+ if f' = f
+ andalso ListPair.allEq (fn (r1, r2) =>
+ repOf r1 = repOf r2)
+ (rs, rs') then
+ (markEq (r, r');
+ false)
+ else
+ true) rest
+ in
+ fr :: loop rest
+ end
+ in
+ #Funcs db := loop (!(#Funcs db))
+ end
+ in
+ case a of
+ ACond _ => ()
+ | AReln x =>
+ case x of
+ (Known, [e]) =>
+ ((*Print.prefaces "Before" [("e", p_exp e),
+ ("db", p_database db)];*)
+ markKnown (representative (db, e))(*;
+ Print.prefaces "After" [("e", p_exp e),
+ ("db", p_database db)]*))
+ | (PCon0 f, [e]) =>
+ let
+ val r = representative (db, e)
+ in
+ case #Variety (unNode r) of
+ Dt0 f' => if f = f' then
+ ()
+ else
+ raise Contradiction
+ | Nothing =>
+ (case SM.find (!(#Con0s db), f) of
+ SOME r' => markEq (r, r')
+ | NONE =>
+ let
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt0 f,
+ Known = ref false,
+ Ge = ref NONE})
+ in
+ #Rep (unNode r) := SOME r';
+ #Con0s db := SM.insert (!(#Con0s db), f, r')
+ end)
+ | _ => raise Contradiction
+ end
+ | (PCon1 f, [e]) =>
+ let
+ val r = representative (db, e)
+ in
+ case #Variety (unNode r) of
+ Dt1 (f', e') => if f = f' then
+ ()
+ else
+ raise Contradiction
+ | Nothing =>
+ let
+ val cons = ref SM.empty
+
+ val r'' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = cons,
+ Variety = Nothing,
+ Known = ref (!(#Known (unNode r))),
+ Ge = ref NONE})
+
+ val r' = ref (Node {Id = nodeId (),
+ Rep = ref NONE,
+ Cons = ref SM.empty,
+ Variety = Dt1 (f, r''),
+ Known = #Known (unNode r),
+ Ge = ref NONE})
+ in
+ cons := SM.insert (!cons, f, r');
+ #Rep (unNode r) := SOME r'
+ end
+ | _ => raise Contradiction
+ end
+ | (Cmp Eq, [e1, e2]) =>
+ markEq (representative (db, e1), representative (db, e2))
+ | (Cmp Ge, [e1, e2]) =>
+ let
+ val r1 = representative (db, e1)
+ val r2 = representative (db, e2)
+ in
+ case !(#Ge (unNode (repOf r2))) of
+ NONE => ()
+ | SOME n2 =>
+ case !(#Ge (unNode (repOf r1))) of
+ NONE => #Ge (unNode (repOf r1)) := SOME n2
+ | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
+ end
+ | _ => ()
+ end handle Undetermined => ()
+
+fun check (db, a) =
+ (case a of
+ ACond _ => false
+ | AReln x =>
+ case x of
+ (Known, [e]) =>
+ let
+ fun isKnown r =
+ let
+ val r = repOf r
+ in
+ !(#Known (unNode r))
+ orelse case #Variety (unNode r) of
+ Dt1 (_, r) => isKnown r
+ | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
+ | _ => false
+ end
+
+ val r = representative (db, e)
+ in
+ isKnown r
+ end
+ | (PCon0 f, [e]) =>
+ (case #Variety (unNode (representative (db, e))) of
+ Dt0 f' => f' = f
+ | _ => false)
+ | (PCon1 f, [e]) =>
+ (case #Variety (unNode (representative (db, e))) of
+ Dt1 (f', _) => f' = f
+ | _ => false)
+ | (Cmp Eq, [e1, e2]) =>
+ let
+ val r1 = representative (db, e1)
+ val r2 = representative (db, e2)
+ in
+ repOf r1 = repOf r2
+ end
+ | (Cmp Ge, [e1, e2]) =>
+ let
+ val r1 = representative (db, e1)
+ val r2 = representative (db, e2)
+ in
+ case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
+ (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
+ | _ => false
+ end
+ | _ => false)
+ handle Undetermined => false
+
+fun builtFrom (db, {Base = bs, Derived = d}) =
+ let
+ val bs = map (fn b => representative (db, b)) bs
+
+ fun loop d =
+ let
+ val d = repOf d
+ in
+ !(#Known (unNode d))
+ orelse List.exists (fn b => repOf b = d) bs
+ orelse (case #Variety (unNode d) of
+ Dt0 _ => true
+ | Dt1 (_, d) => loop d
+ | Prim _ => true
+ | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
+ | Nothing => false)
+ orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs)
+ (SM.listItems (!(#Cons (unNode d))))
+ end
+
+ fun decomp e =
+ case e of
+ Func (Other _, es) => List.all decomp es
+ | _ => loop (representative (db, e))
+ in
+ decomp d
+ end handle Undetermined => false
+
+end
+
+val tabs = ref (SM.empty : (string list * string list list) SM.map)
+
+fun patCon pc =
+ case pc of
+ PConVar n => "C" ^ Int.toString n
+ | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
+
+type check = exp * ErrorMsg.span
+
+structure St :> sig
+ val reset : unit -> unit
+
+ type stashed
+ val stash : unit -> stashed
+ val reinstate : stashed -> unit
+
+ type stashedPath
+ val stashPath : unit -> stashedPath
+ val reinstatePath : stashedPath -> unit
+
+ val nextVar : unit -> int
+
+ val assert : atom list -> unit
+
+ val addPath : check -> unit
+
+ val allowSend : atom list * exp list -> unit
+ val send : check -> unit
+
+ val allowInsert : atom list -> unit
+ val insert : ErrorMsg.span -> unit
+
+ val allowDelete : atom list -> unit
+ val delete : ErrorMsg.span -> unit
+
+ val allowUpdate : atom list -> unit
+ val update : ErrorMsg.span -> unit
+
+ val havocReln : reln -> unit
+ val havocCookie : string -> unit
+
+ val check : atom -> bool
+
+ val debug : unit -> unit
+end = struct
+
+val hnames = ref 1
+
+type hyps = int * atom list * bool ref
+
+val db = Cc.database ()
+val path = ref ([] : ((int * atom list) * check) option ref list)
+val hyps = ref (0, [] : atom list, ref false)
+val nvar = ref 0
+
+fun setHyps (n', hs) =
+ let
+ val (n, _, _) = !hyps
+ in
+ if n' = n then
+ ()
+ else
+ (hyps := (n', hs, ref false);
+ Cc.clear db;
+ app (fn a => Cc.assert (db, a)) hs)
+ end
+
+fun useKeys () =
+ let
+ val changed = ref false
+
+ fun findKeys (hyps, acc) =
+ case hyps of
+ [] => rev acc
+ | (a as AReln (Sql tab, [r1])) :: hyps =>
+ (case SM.find (!tabs, tab) of
+ NONE => findKeys (hyps, a :: acc)
+ | SOME (_, []) => findKeys (hyps, a :: acc)
+ | SOME (_, ks) =>
+ let
+ fun finder (hyps, acc) =
+ case hyps of
+ [] => rev acc
+ | (a as AReln (Sql tab', [r2])) :: hyps =>
+ if tab' = tab andalso
+ List.exists (List.all (fn f =>
+ let
+ val r =
+ Cc.check (db,
+ AReln (Cmp Eq, [Proj (r1, f),
+ Proj (r2, f)]))
+ in
+ (*Print.prefaces "Fs"
+ [("tab",
+ Print.PD.string tab),
+ ("r1",
+ p_exp (Proj (r1, f))),
+ ("r2",
+ p_exp (Proj (r2, f))),
+ ("r",
+ Print.PD.string
+ (Bool.toString r))];*)
+ r
+ end)) ks then
+ (changed := true;
+ Cc.assert (db, AReln (Cmp Eq, [r1, r2]));
+ finder (hyps, acc))
+ else
+ finder (hyps, a :: acc)
+ | a :: hyps => finder (hyps, a :: acc)
+
+ val hyps = finder (hyps, [])
+ in
+ findKeys (hyps, a :: acc)
+ end)
+ | a :: hyps => findKeys (hyps, a :: acc)
+
+ fun loop hs =
+ let
+ val hs = findKeys (hs, [])
+ in
+ if !changed then
+ (changed := false;
+ loop hs)
+ else
+ ()
+ end
+
+ val (_, hs, _) = !hyps
+ in
+ (*print "useKeys\n";*)
+ loop hs
+ end
+
+fun complete () =
+ let
+ val (_, _, bf) = !hyps
+ in
+ if !bf then
+ ()
+ else
+ (bf := true;
+ useKeys ())
+ end
+
+type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
+fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
+fun reinstate (nv, p, h) =
+ (nvar := nv;
+ path := p;
+ setHyps h)
+
+type stashedPath = ((int * atom list) * check) option ref list
+fun stashPath () = !path
+fun reinstatePath p = path := p
+
+fun nextVar () =
+ let
+ val n = !nvar
+ in
+ nvar := n + 1;
+ n
+ end
+
+fun assert ats =
+ let
+ val n = !hnames
+ val (_, hs, _) = !hyps
+ in
+ hnames := n + 1;
+ hyps := (n, ats @ hs, ref false);
+ app (fn a => Cc.assert (db, a)) ats
+ end
+
+fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
+
+val sendable = ref ([] : (atom list * exp list) list)
+
+fun checkGoals goals k =
+ let
+ fun checkGoals goals unifs =
+ case goals of
+ [] => k unifs
+ | AReln (Sql tab, [Lvar lv]) :: goals =>
+ let
+ val saved = stash ()
+ val (_, hyps, _) = !hyps
+
+ fun tryAll unifs hyps =
+ case hyps of
+ [] => false
+ | AReln (Sql tab', [e]) :: hyps =>
+ (tab' = tab andalso
+ checkGoals goals (IM.insert (unifs, lv, e)))
+ orelse tryAll unifs hyps
+ | _ :: hyps => tryAll unifs hyps
+ in
+ tryAll unifs hyps
+ end
+ | (g as AReln (r, es)) :: goals =>
+ (complete ();
+ (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
+ true
+ else
+ ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
+ false))
+ andalso checkGoals goals unifs)
+ | ACond _ :: _ => false
+ in
+ checkGoals goals IM.empty
+ end
+
+fun buildable (e, loc) =
+ let
+ fun doPols pols acc =
+ case pols of
+ [] =>
+ let
+ val b = Cc.builtFrom (db, {Base = acc, Derived = e})
+ in
+ (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
+ ("Derived", p_exp e),
+ ("Hyps", Print.p_list p_atom (#2 (!hyps))),
+ ("Good", Print.PD.string (Bool.toString b))];*)
+ b
+ end
+ | (goals, es) :: pols =>
+ checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
+ orelse doPols pols acc
+ in
+ if doPols (!sendable) [] then
+ ()
+ else
+ let
+ val (_, hs, _) = !hyps
+ in
+ ErrorMsg.errorAt loc "The information flow policy may be violated here.";
+ Print.prefaces "Situation" [("User learns", p_exp e),
+ ("Hypotheses", Print.p_list p_atom hs),
+ ("E-graph", Cc.p_database db)]
+ end
+ end
+
+fun checkPaths () =
+ let
+ val (n, hs, _) = !hyps
+ val hs = (n, hs)
+ in
+ app (fn r =>
+ case !r of
+ NONE => ()
+ | SOME (hs, e) =>
+ (r := NONE;
+ setHyps hs;
+ buildable e)) (!path);
+ setHyps hs
+ end
+
+fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
+ ("exps", Print.p_list p_exp (#2 v))];*)
+ sendable := v :: !sendable)
+
+fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
+ complete ();
+ checkPaths ();
+ if isKnown e then
+ ()
+ else
+ buildable (e, loc))
+
+fun doable pols (loc : ErrorMsg.span) =
+ let
+ val pols = !pols
+ in
+ complete ();
+ if List.exists (fn goals =>
+ if checkGoals goals (fn _ => true) then
+ ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
+ ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
+ true)
+ else
+ ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
+ ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
+ false)) pols then
+ ()
+ else
+ let
+ val (_, hs, _) = !hyps
+ in
+ ErrorMsg.errorAt loc "The database update policy may be violated here.";
+ Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
+ ("E-graph", Cc.p_database db)*)]
+ end
+ end
+
+val insertable = ref ([] : atom list list)
+fun allowInsert v = insertable := v :: !insertable
+val insert = doable insertable
+
+val updatable = ref ([] : atom list list)
+fun allowUpdate v = updatable := v :: !updatable
+val update = doable updatable
+
+val deletable = ref ([] : atom list list)
+fun allowDelete v = deletable := v :: !deletable
+val delete = doable deletable
+
+fun reset () = (Cc.clear db;
+ path := [];
+ hyps := (0, [], ref false);
+ nvar := 0;
+ sendable := [];
+ insertable := [];
+ updatable := [];
+ deletable := [])
+
+fun havocReln r =
+ let
+ val n = !hnames
+ val (_, hs, _) = !hyps
+ in
+ hnames := n + 1;
+ hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
+ end
+
+fun havocCookie cname =
+ let
+ val cname = "cookie/" ^ cname
+ val n = !hnames
+ val (_, hs, _) = !hyps
+ in
+ hnames := n + 1;
+ hyps := (n, List.filter (fn AReln (Cmp Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
+ end
+
+fun check a = Cc.check (db, a)
+
+fun debug () =
+ let
+ val (_, hs, _) = !hyps
+ in
+ Print.preface ("Hyps", Print.p_list p_atom hs)
+ end
+
+end
+
+
+fun removeDups (ls : (string * string) list) =
+ case ls of
+ [] => []
+ | x :: ls =>
+ let
+ val ls = removeDups ls
+ in
+ if List.exists (fn x' => x' = x) ls then
+ ls
+ else
+ x :: ls
+ end
+
+fun deinj env e =
+ case #1 e of
+ ERel n => SOME (List.nth (env, n))
+ | EField (e, f) =>
+ (case deinj env e of
+ NONE => NONE
+ | SOME e => SOME (Proj (e, f)))
+ | EApp ((EFfi mf, _), e) =>
+ if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
+ NONE
+ else (case deinj env e of
+ NONE => NONE
+ | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
+ | _ => NONE
+
+fun expIn rv env rvOf =
+ let
+ fun expIn e =
+ let
+ fun default () = inl (rv ())
+ in
+ case e of
+ SqConst p => inl (Const p)
+ | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
+ | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
+ | Null => inl (Func (DtCon0 "None", []))
+ | SqNot e =>
+ inr (case expIn e of
+ inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
+ | inr _ => Unknown)
+ | Field (v, f) => inl (Proj (rvOf v, f))
+ | Computed _ => default ()
+ | Binop (bo, e1, e2) =>
+ let
+ val e1 = expIn e1
+ val e2 = expIn e2
+ in
+ inr (case (bo, e1, e2) of
+ (RCmp c, inl e1, inl e2) => Reln (Cmp c, [e1, e2])
+ | (RLop l, v1, v2) =>
+ let
+ fun pin v =
+ case v of
+ inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+ | inr p => p
+ in
+ Lop (l, pin v1, pin v2)
+ end
+ | _ => Unknown)
+ end
+ | SqKnown e =>
+ (case expIn e of
+ inl e => inr (Reln (Known, [e]))
+ | _ => inr Unknown)
+ | Inj e =>
+ inl (case deinj env e of
+ NONE => rv ()
+ | SOME e => e)
+ | SqFunc (f, e) =>
+ (case expIn e of
+ inl e => inl (Func (Other f, [e]))
+ | _ => default ())
+
+ | Unmodeled => inl (Func (Other "allow", [rv ()]))
+ end
+ in
+ expIn
+ end
+
+fun decomp {Save = save, Restore = restore, Add = add} =
+ let
+ fun go p k =
+ case p of
+ True => (k () handle Cc.Contradiction => ())
+ | False => ()
+ | Unknown => ()
+ | Lop (And, p1, p2) => go p1 (fn () => go p2 k)
+ | Lop (Or, p1, p2) =>
+ let
+ val saved = save ()
+ in
+ go p1 k;
+ restore saved;
+ go p2 k
+ end
+ | Reln x => (add (AReln x); k ())
+ | Cond x => (add (ACond x); k ())
+ in
+ go
+ end
+
+datatype queryMode =
+ SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
+ | AllCols of exp -> unit
+
+type 'a doQuery = {
+ Env : exp list,
+ NextVar : unit -> exp,
+ Add : atom -> unit,
+ Save : unit -> 'a,
+ Restore : 'a -> unit,
+ Cont : queryMode
+}
+
+fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
+ let
+ fun default () = (ErrorMsg.errorAt loc "Information flow checker can't parse SQL query";
+ Print.preface ("Query", MonoPrint.p_exp MonoEnv.empty e))
+ in
+ case parse query e of
+ NONE => default ()
+ | SOME q =>
+ let
+ fun doQuery q =
+ case q of
+ Query1 r =>
+ let
+ val new = ref NONE
+ val old = ref NONE
+
+ val rvs = map (fn Table (tab, v) =>
+ let
+ val nv = #NextVar arg ()
+ in
+ case v of
+ "New" => new := SOME (tab, nv)
+ | "Old" => old := SOME (tab, nv)
+ | _ => ();
+ (v, nv)
+ end
+ | _ => raise Fail "Iflow: not ready for joins or nesteds") (#From r)
+
+ fun rvOf v =
+ case List.find (fn (v', _) => v' = v) rvs of
+ NONE => raise Fail "Iflow.queryProp: Bad table variable"
+ | SOME (_, e) => e
+
+ val expIn = expIn (#NextVar arg) (#Env arg) rvOf
+
+ val saved = #Save arg ()
+ fun addFrom () = app (fn Table (t, v) => #Add arg (AReln (Sql t, [rvOf v]))
+ | _ => raise Fail "Iflow: not ready for joins or nesteds") (#From r)
+
+ fun usedFields e =
+ case e of
+ SqConst _ => []
+ | SqTrue => []
+ | SqFalse => []
+ | Null => []
+ | SqNot e => usedFields e
+ | Field (v, f) => [(false, Proj (rvOf v, f))]
+ | Computed _ => []
+ | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
+ | SqKnown _ => []
+ | Inj e =>
+ (case deinj (#Env arg) e of
+ NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
+ [])
+ | SOME e => [(true, e)])
+ | SqFunc (_, e) => usedFields e
+ | Unmodeled => []
+
+ fun normal' () =
+ case #Cont arg of
+ SomeCol k =>
+ let
+ val sis = map (fn si =>
+ case si of
+ SqField (v, f) => Proj (rvOf v, f)
+ | SqExp (e, f) =>
+ case expIn e of
+ inr _ => #NextVar arg ()
+ | inl e => e) (#Select r)
+ in
+ k {New = !new, Old = !old, Outs = sis}
+ end
+ | AllCols k =>
+ let
+ val (ts, es) =
+ foldl (fn (si, (ts, es)) =>
+ case si of
+ SqField (v, f) =>
+ let
+ val fs = getOpt (SM.find (ts, v), SM.empty)
+ in
+ (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
+ end
+ | SqExp (e, f) =>
+ let
+ val e =
+ case expIn e of
+ inr _ => #NextVar arg ()
+ | inl e => e
+ in
+ (ts, SM.insert (es, f, e))
+ end)
+ (SM.empty, SM.empty) (#Select r)
+ in
+ k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
+ (SM.listItemsi ts)
+ @ SM.listItemsi es))
+ end
+
+ fun doWhere final =
+ (addFrom ();
+ case #Where r of
+ NONE => final ()
+ | SOME e =>
+ let
+ val p = case expIn e of
+ inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+ | inr p => p
+
+ val saved = #Save arg ()
+ in
+ decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
+ p (fn () => final () handle Cc.Contradiction => ());
+ #Restore arg saved
+ end)
+ handle Cc.Contradiction => ()
+
+ fun normal () = doWhere normal'
+ in
+ (case #Select r of
+ [SqExp (Binop (RCmp bo, Count, SqConst (Prim.Int 0)), f)] =>
+ (case bo of
+ Gt =>
+ (case #Cont arg of
+ SomeCol _ => ()
+ | AllCols k =>
+ let
+ fun answer e = k (Recd [(f, e)])
+
+ val saved = #Save arg ()
+ val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
+ handle Cc.Contradiction => ()
+ in
+ #Restore arg saved;
+ (*print "True time!\n";*)
+ doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
+ #Restore arg saved
+ end)
+ | _ => normal ())
+ | _ => normal ())
+ before #Restore arg saved
+ end
+ | Union (q1, q2) =>
+ let
+ val saved = #Save arg ()
+ in
+ doQuery q1;
+ #Restore arg saved;
+ doQuery q2;
+ #Restore arg saved
+ end
+ in
+ doQuery q
+ end
+ end
+
+fun evalPat env e (pt, _) =
+ case pt of
+ PVar _ => e :: env
+ | PPrim _ => env
+ | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
+ | PCon (_, pc, SOME pt) =>
+ let
+ val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
+ in
+ St.assert [AReln (PCon1 (patCon pc), [e])];
+ env
+ end
+ | PRecord xpts =>
+ foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
+ | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
+ | PSome (_, pt) =>
+ let
+ val env = evalPat env (Func (UnCon "Some", [e])) pt
+ in
+ St.assert [AReln (PCon1 "Some", [e])];
+ env
+ end
+
+datatype arg_mode = Fixed | Decreasing | Arbitrary
+type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
+val rfuns = ref (IM.empty : rfun IM.map)
+
+fun evalExp env (e as (_, loc)) k =
+ let
+ (*val () = St.debug ()*)
+ (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
+
+ fun default () = k (Var (St.nextVar ()))
+
+ fun doFfi (m, s, es) =
+ if m = "Basis" andalso SS.member (writers, s) then
+ let
+ fun doArgs es =
+ case es of
+ [] =>
+ (if s = "set_cookie" then
+ case es of
+ [_, (cname, _), _, _, _] =>
+ (case #1 cname of
+ EPrim (Prim.String (_, cname)) =>
+ St.havocCookie cname
+ | _ => ())
+ | _ => ()
+ else
+ ();
+ k (Recd []))
+ | (e, _) :: es =>
+ evalExp env e (fn e => (St.send (e, loc); doArgs es))
+ in
+ doArgs es
+ end
+ else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
+ default ()
+ else
+ let
+ fun doArgs (es, acc) =
+ case es of
+ [] => k (Func (Other (m ^ "." ^ s), rev acc))
+ | (e, _) :: es =>
+ evalExp env e (fn e => doArgs (es, e :: acc))
+ in
+ doArgs (es, [])
+ end
+ in
+ case #1 e of
+ EPrim p => k (Const p)
+ | ERel n => k (List.nth (env, n))
+ | ENamed _ => default ()
+ | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
+ | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
+ | ENone _ => k (Func (DtCon0 "None", []))
+ | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
+ | EFfi _ => default ()
+
+ | EFfiApp ("Basis", "rand", []) =>
+ let
+ val e = Var (St.nextVar ())
+ in
+ St.assert [AReln (Known, [e])];
+ k e
+ end
+ | EFfiApp x => doFfi x
+ | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [(e, (TRecord [], loc))])
+
+ | EApp (e1 as (EError _, _), _) => evalExp env e1 k
+
+ | EApp (e1, e2) =>
+ let
+ fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
+ Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
+ default ())
+
+ fun doArgs (e, args) =
+ case #1 e of
+ EApp (e1, e2) => doArgs (e1, e2 :: args)
+ | ENamed n =>
+ (case IM.find (!rfuns, n) of
+ NONE => adefault ()
+ | SOME rf =>
+ if length (#args rf) <> length args then
+ adefault ()
+ else
+ let
+ val () = (SS.app (St.havocReln o Sql) (#tables rf);
+ SS.app St.havocCookie (#cookies rf))
+ val saved = St.stash ()
+
+ fun doArgs (args, modes, env') =
+ case (args, modes) of
+ ([], []) => (evalExp env' (#body rf) (fn _ => ());
+ St.reinstate saved;
+ default ())
+
+ | (arg :: args, mode :: modes) =>
+ evalExp env arg (fn arg =>
+ let
+ val v = case mode of
+ Arbitrary => Var (St.nextVar ())
+ | Fixed => arg
+ | Decreasing =>
+ let
+ val v = Var (St.nextVar ())
+ in
+ if St.check (AReln (Known, [arg])) then
+ St.assert [(AReln (Known, [v]))]
+ else
+ ();
+ v
+ end
+ in
+ doArgs (args, modes, v :: env')
+ end)
+ | _ => raise Fail "Iflow.doArgs: Impossible"
+ in
+ doArgs (args, #args rf, [])
+ end)
+ | _ => adefault ()
+ in
+ doArgs (e, [])
+ end
+
+ | EAbs _ => default ()
+ | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
+ | EBinop (_, s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
+ | ERecord xets =>
+ let
+ fun doFields (xes, acc) =
+ case xes of
+ [] => k (Recd (rev acc))
+ | (x, e, _) :: xes =>
+ evalExp env e (fn e => doFields (xes, (x, e) :: acc))
+ in
+ doFields (xets, [])
+ end
+ | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
+ | ECase (e, pes, {result = res, ...}) =>
+ evalExp env e (fn e =>
+ if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
+ | _ => false) pes then
+ (St.send (e, loc);
+ k (Recd []))
+ else
+ (St.addPath (e, loc);
+ app (fn (p, pe) =>
+ let
+ val saved = St.stash ()
+ in
+ let
+ val env = evalPat env e p
+ in
+ evalExp env pe k;
+ St.reinstate saved
+ end
+ handle Cc.Contradiction => St.reinstate saved
+ end) pes))
+ | EStrcat (e1, e2) =>
+ evalExp env e1 (fn e1 =>
+ evalExp env e2 (fn e2 =>
+ k (Func (Other "cat", [e1, e2]))))
+ | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
+ | EReturnBlob {blob = NONE, ...} => raise Fail "Iflow doesn't support blob optimization"
+ | EReturnBlob {blob = SOME b, mimeType = m, ...} =>
+ evalExp env b (fn b =>
+ (St.send (b, loc);
+ evalExp env m
+ (fn m => St.send (m, loc))))
+ | ERedirect (e, _) =>
+ evalExp env e (fn e => St.send (e, loc))
+ | EWrite e =>
+ evalExp env e (fn e => (St.send (e, loc);
+ k (Recd [])))
+ | ESeq (e1, e2) =>
+ let
+ val path = St.stashPath ()
+ in
+ evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
+ end
+ | ELet (_, _, e1, e2) =>
+ evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
+ | EClosure (n, es) =>
+ let
+ fun doArgs (es, acc) =
+ case es of
+ [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
+ | e :: es =>
+ evalExp env e (fn e => doArgs (es, e :: acc))
+ in
+ doArgs (es, [])
+ end
+
+ | EQuery {query = q, body = b, initial = i, state = state, ...} =>
+ evalExp env i (fn i =>
+ let
+ val r = Var (St.nextVar ())
+ val acc = Var (St.nextVar ())
+
+ val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
+ exp = fn (e, st as (cs, ts)) =>
+ case e of
+ EDml (e, _) =>
+ (case parse dml e of
+ NONE => st
+ | SOME c =>
+ case c of
+ Insert _ => st
+ | Delete (tab, _) =>
+ (cs, SS.add (ts, tab))
+ | Update (tab, _, _) =>
+ (cs, SS.add (ts, tab)))
+ | EFfiApp ("Basis", "set_cookie",
+ [_, ((EPrim (Prim.String (_, cname)), _), _),
+ _, _, _]) =>
+ (SS.add (cs, cname), ts)
+ | _ => st}
+ (SS.empty, SS.empty) b
+ in
+ case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
+ (TRecord [], true, true) => ()
+ | _ =>
+ let
+ val saved = St.stash ()
+ in
+ (k i)
+ handle Cc.Contradiction => ();
+ St.reinstate saved
+ end;
+
+ SS.app (St.havocReln o Sql) ts;
+ SS.app St.havocCookie cs;
+
+ doQuery {Env = env,
+ NextVar = Var o St.nextVar,
+ Add = fn a => St.assert [a],
+ Save = St.stash,
+ Restore = St.reinstate,
+ Cont = AllCols (fn x =>
+ (St.assert [AReln (Cmp Eq, [r, x])];
+ evalExp (acc :: r :: env) b k))} q
+ end)
+ | EDml (e, _) =>
+ (case parse dml e of
+ NONE => (print ("Warning: Information flow checker can't parse DML command at "
+ ^ ErrorMsg.spanToString loc ^ "\n");
+ default ())
+ | SOME d =>
+ case d of
+ Insert (tab, es) =>
+ let
+ val new = St.nextVar ()
+
+ val expIn = expIn (Var o St.nextVar) env
+ (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
+
+ val es = map (fn (x, e) =>
+ case expIn e of
+ inl e => (x, e)
+ | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
+ es
+
+ val saved = St.stash ()
+ in
+ St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
+ St.insert loc;
+ St.reinstate saved;
+ St.assert [AReln (Sql tab, [Recd es])];
+ k (Recd [])
+ end
+ | Delete (tab, e) =>
+ let
+ val old = St.nextVar ()
+
+ val expIn = expIn (Var o St.nextVar) env
+ (fn "T" => Var old
+ | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
+
+ val p = case expIn e of
+ inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
+ | inr p => p
+
+ val saved = St.stash ()
+ in
+ St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
+ AReln (Sql (tab), [Var old])];
+ decomp {Save = St.stash,
+ Restore = St.reinstate,
+ Add = fn a => St.assert [a]} p
+ (fn () => (St.delete loc;
+ St.reinstate saved;
+ St.havocReln (Sql tab);
+ k (Recd []))
+ handle Cc.Contradiction => ())
+ end
+ | Update (tab, fs, e) =>
+ let
+ val new = St.nextVar ()
+ val old = St.nextVar ()
+
+ val expIn = expIn (Var o St.nextVar) env
+ (fn "T" => Var old
+ | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
+
+ val fs = map
+ (fn (x, e) =>
+ (x, case expIn e of
+ inl e => e
+ | inr _ => raise Fail
+ ("Iflow.evalExp: Selecting "
+ ^ "boolean expression")))
+ fs
+
+ val fs' = case SM.find (!tabs, tab) of
+ NONE => raise Fail "Iflow.evalExp: Updating unknown table"
+ | SOME (fs', _) => fs'
+
+ val fs = foldl (fn (f, fs) =>
+ if List.exists (fn (f', _) => f' = f) fs then
+ fs
+ else
+ (f, Proj (Var old, f)) :: fs) fs fs'
+
+ val p = case expIn e of
+ inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
+ | inr p => p
+ val saved = St.stash ()
+ in
+ St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
+ AReln (Sql (tab ^ "$Old"), [Var old]),
+ AReln (Sql tab, [Var old])];
+ decomp {Save = St.stash,
+ Restore = St.reinstate,
+ Add = fn a => St.assert [a]} p
+ (fn () => (St.update loc;
+ St.reinstate saved;
+ St.havocReln (Sql tab);
+ k (Recd []))
+ handle Cc.Contradiction => ())
+ end)
+
+ | ENextval (EPrim (Prim.String (_, seq)), _) =>
+ let
+ val nv = St.nextVar ()
+ in
+ St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
+ k (Var nv)
+ end
+ | ENextval _ => default ()
+ | ESetval _ => default ()
+
+ | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String (_, cname)), _), _)]), _), _, _) =>
+ let
+ val e = Var (St.nextVar ())
+ val e' = Func (Other ("cookie/" ^ cname), [])
+ in
+ St.assert [AReln (Known, [e]), AReln (Cmp Eq, [e, e'])];
+ k e
+ end
+
+ | EUnurlify _ => default ()
+ | EJavaScript _ => default ()
+ | ESignalReturn _ => default ()
+ | ESignalBind _ => default ()
+ | ESignalSource _ => default ()
+ | EServerCall _ => default ()
+ | ERecv _ => default ()
+ | ESleep _ => default ()
+ | ESpawn _ => default ()
+ end
+
+datatype var_source = Input of int | SubInput of int | Unknown
+
+structure U = MonoUtil
+
+fun mliftExpInExp by =
+ U.Exp.mapB {typ = fn t => t,
+ exp = fn bound => fn e =>
+ case e of
+ ERel xn =>
+ if xn < bound then
+ e
+ else
+ ERel (xn + by)
+ | _ => e,
+ bind = fn (bound, U.Exp.RelE _) => bound + 1
+ | (bound, _) => bound}
+
+fun nameSubexps k (e : Mono.exp) =
+ let
+ fun numParams (e : Mono.exp) =
+ case #1 e of
+ EStrcat (e1, e2) => numParams e1 + numParams e2
+ | EPrim (Prim.String _) => 0
+ | _ => 1
+
+ val nps = numParams e
+
+ fun getParams (e : Mono.exp) x =
+ case #1 e of
+ EStrcat (e1, e2) =>
+ let
+ val (ps1, e1') = getParams e1 x
+ val (ps2, e2') = getParams e2 (x - length ps1)
+ in
+ (ps2 @ ps1, (EStrcat (e1', e2'), #2 e))
+ end
+ | EPrim (Prim.String _) => ([], e)
+ | _ =>
+ let
+ val (e', k) =
+ case #1 e of
+ EFfiApp (m, f, [(e', t)]) =>
+ if Settings.isEffectful (m, f) orelse Settings.isBenignEffectful (m, f) then
+ (e, fn x => x)
+ else
+ (e', fn e' => (EFfiApp (m, f, [(e', t)]), #2 e))
+ | ECase (e', ps as
+ [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
+ (EPrim (Prim.String (_, "TRUE")), _)),
+ ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
+ (EPrim (Prim.String (_, "FALSE")), _))], q) =>
+ (e', fn e' => (ECase (e', ps, q), #2 e))
+ | _ => (e, fn x => x)
+ in
+ ([e'], k (ERel x, #2 e))
+ end
+
+ val (ps, e') = getParams e (nps - 1)
+
+ val string = (TFfi ("Basis", "string"), #2 e)
+
+ val (e', _) = foldl (fn (p, (e', liftBy)) =>
+ ((ELet ("p" ^ Int.toString liftBy,
+ string,
+ mliftExpInExp liftBy 0 p,
+ e'), #2 e), liftBy - 1)) (k (nps, e'), nps - 1) ps
+ in
+ #1 e'
+ end
+
+val namer = MonoUtil.File.map {typ = fn t => t,
+ exp = fn e =>
+ case e of
+ EDml (e, fm) =>
+ nameSubexps (fn (_, e') => (EDml (e', fm), #2 e)) e
+ | EQuery {exps, tables, state, query, body, initial} =>
+ nameSubexps (fn (liftBy, e') =>
+ (EQuery {exps = exps,
+ tables = tables,
+ state = state,
+ query = e',
+ body = mliftExpInExp liftBy 2 body,
+ initial = mliftExpInExp liftBy 0 initial},
+ #2 query)) query
+ | _ => e,
+ decl = fn d => d}
+
+fun check (file : file) =
+ let
+ val () = (St.reset ();
+ rfuns := IM.empty)
+
+ (*val () = Print.preface ("FilePre", MonoPrint.p_file MonoEnv.empty file)*)
+ val file = MonoReduce.reduce file
+ val file = MonoOpt.optimize file
+ val file = Fuse.fuse file
+ val file = MonoOpt.optimize file
+ val file = MonoShake.shake file
+ val file = namer file
+ (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
+
+ val exptd = foldl (fn ((d, _), exptd) =>
+ case d of
+ DExport (_, _, n, _, _, _) => IS.add (exptd, n)
+ | _ => exptd) IS.empty (#1 file)
+
+ fun decl (d, loc) =
+ case d of
+ DTable (tab, fs, pk, _) =>
+ let
+ val ks =
+ case #1 pk of
+ EPrim (Prim.String (_, s)) =>
+ (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
+ [] => []
+ | pk => [pk])
+ | _ => []
+ in
+ if size tab >= 3 then
+ tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
+ (map #1 fs,
+ map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
+ ^ String.extract (s, 4, NONE))) ks))
+ else
+ raise Fail "Table name does not begin with uw_"
+ end
+ | DVal (x, n, _, e, _) =>
+ let
+ (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
+
+ val isExptd = IS.member (exptd, n)
+
+ val saved = St.stash ()
+
+ fun deAbs (e, env, ps) =
+ case #1 e of
+ EAbs (_, _, _, e) =>
+ let
+ val nv = Var (St.nextVar ())
+ in
+ deAbs (e, nv :: env,
+ if isExptd then
+ AReln (Known, [nv]) :: ps
+ else
+ ps)
+ end
+ | _ => (e, env, ps)
+
+ val (e, env, ps) = deAbs (e, [], [])
+ in
+ St.assert ps;
+ (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
+ St.reinstate saved
+ end
+
+ | DValRec [(x, n, _, e, _)] =>
+ let
+ val tables = ref SS.empty
+ val cookies = ref SS.empty
+
+ fun deAbs (e, env, modes) =
+ case #1 e of
+ EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
+ | _ => (e, env, rev modes)
+
+ val (e, env, modes) = deAbs (e, [], [])
+
+ fun doExp env (e as (_, loc)) =
+ case #1 e of
+ EPrim _ => e
+ | ERel _ => e
+ | ENamed _ => e
+ | ECon (_, _, NONE) => e
+ | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
+ | ENone _ => e
+ | ESome (t, e) => (ESome (t, doExp env e), loc)
+ | EFfi _ => e
+ | EFfiApp (m, f, es) =>
+ (case (m, f, es) of
+ ("Basis", "set_cookie", [_, ((EPrim (Prim.String (_, cname)), _), _), _, _, _]) =>
+ cookies := SS.add (!cookies, cname)
+ | _ => ();
+ (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc))
+
+ | EApp (e1, e2) =>
+ let
+ fun default () = (EApp (doExp env e1, doExp env e2), loc)
+
+ fun explore (e, args) =
+ case #1 e of
+ EApp (e1, e2) => explore (e1, e2 :: args)
+ | ENamed n' =>
+ if n' = n then
+ let
+ fun doArgs (pos, args, modes) =
+ case (args, modes) of
+ ((e1, _) :: args, m1 :: modes) =>
+ (case e1 of
+ ERel n =>
+ (case List.nth (env, n) of
+ Input pos' =>
+ if pos' = pos then
+ ()
+ else
+ m1 := Arbitrary
+ | SubInput pos' =>
+ if pos' = pos then
+ if !m1 = Arbitrary then
+ ()
+ else
+ m1 := Decreasing
+ else
+ m1 := Arbitrary
+ | Unknown => m1 := Arbitrary)
+ | _ => m1 := Arbitrary;
+ doArgs (pos + 1, args, modes))
+ | (_ :: _, []) => ()
+ | ([], ms) => app (fn m => m := Arbitrary) ms
+ in
+ doArgs (0, args, modes);
+ (EFfi ("Basis", "?"), loc)
+ end
+ else
+ default ()
+ | _ => default ()
+ in
+ explore (e, [])
+ end
+ | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
+ | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
+ | EBinop (bi, bo, e1, e2) => (EBinop (bi, bo, doExp env e1, doExp env e2), loc)
+ | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
+ | EField (e1, f) => (EField (doExp env e1, f), loc)
+ | ECase (e, pes, ts) =>
+ let
+ val source =
+ case #1 e of
+ ERel n =>
+ (case List.nth (env, n) of
+ Input n => SOME n
+ | SubInput n => SOME n
+ | Unknown => NONE)
+ | _ => NONE
+
+ fun doV v =
+ let
+ fun doPat (p, env) =
+ case #1 p of
+ PVar _ => v :: env
+ | PPrim _ => env
+ | PCon (_, _, NONE) => env
+ | PCon (_, _, SOME p) => doPat (p, env)
+ | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
+ | PNone _ => env
+ | PSome (_, p) => doPat (p, env)
+ in
+ (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
+ end
+ in
+ case source of
+ NONE => doV Unknown
+ | SOME inp => doV (SubInput inp)
+ end
+ | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
+ | EError (e1, t) => (EError (doExp env e1, t), loc)
+ | EReturnBlob {blob = NONE, mimeType = m, t} =>
+ (EReturnBlob {blob = NONE, mimeType = doExp env m, t = t}, loc)
+ | EReturnBlob {blob = SOME b, mimeType = m, t} =>
+ (EReturnBlob {blob = SOME (doExp env b), mimeType = doExp env m, t = t}, loc)
+ | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
+ | EWrite e1 => (EWrite (doExp env e1), loc)
+ | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
+ | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
+ | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
+ | EQuery {exps, tables, state, query, body, initial} =>
+ (EQuery {exps = exps, tables = tables, state = state,
+ query = doExp env query,
+ body = doExp (Unknown :: Unknown :: env) body,
+ initial = doExp env initial}, loc)
+ | EDml (e1, mode) =>
+ (case parse dml e1 of
+ NONE => ()
+ | SOME c =>
+ case c of
+ Insert _ => ()
+ | Delete (tab, _) =>
+ tables := SS.add (!tables, tab)
+ | Update (tab, _, _) =>
+ tables := SS.add (!tables, tab);
+ (EDml (doExp env e1, mode), loc))
+ | ENextval e1 => (ENextval (doExp env e1), loc)
+ | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
+ | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
+ | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
+ | ESignalReturn _ => e
+ | ESignalBind _ => e
+ | ESignalSource _ => e
+ | EServerCall _ => e
+ | ERecv _ => e
+ | ESleep _ => e
+ | ESpawn _ => e
+
+ val e = doExp env e
+ in
+ rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
+ args = map (fn r => !r) modes, body = e})
+ end
+
+ | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
+
+ | DPolicy pol =>
+ let
+ val rvN = ref 0
+ fun rv () =
+ let
+ val n = !rvN
+ in
+ rvN := n + 1;
+ Lvar n
+ end
+
+ val atoms = ref ([] : atom list)
+ fun doQ k = doQuery {Env = [],
+ NextVar = rv,
+ Add = fn a => atoms := a :: !atoms,
+ Save = fn () => !atoms,
+ Restore = fn ls => atoms := ls,
+ Cont = SomeCol (fn r => k (rev (!atoms), r))}
+
+ fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
+ tab' <> tab
+ orelse List.all (fn Lvar lv' => lv' <> lv
+ | _ => false) nams
+ | _ => true)
+ in
+ case pol of
+ PolClient e =>
+ doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
+ | PolInsert e =>
+ doQ (fn (ats, {New = SOME (tab, new), ...}) =>
+ St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
+ | _ => raise Fail "Iflow: No New in mayInsert policy") e
+ | PolDelete e =>
+ doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
+ St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
+ | _ => raise Fail "Iflow: No Old in mayDelete policy") e
+ | PolUpdate e =>
+ doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
+ St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
+ :: AReln (Sql (tab ^ "$New"), [new])
+ :: untab (tab, [new, old]) ats)
+ | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
+ | PolSequence e =>
+ (case #1 e of
+ EPrim (Prim.String (_, seq)) =>
+ let
+ val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
+ val outs = [Lvar 0]
+ in
+ St.allowSend ([p], outs)
+ end
+ | _ => ())
+ end
+
+ | _ => ()
+ in
+ app decl (#1 file)
+ end
+
+val check = fn file =>
+ let
+ val oldInline = Settings.getMonoInline ()
+ val oldFull = !MonoReduce.fullMode
+ in
+ (Settings.setMonoInline (case Int.maxInt of
+ NONE => 1000000
+ | SOME n => n);
+ MonoReduce.fullMode := true;
+ check file;
+ Settings.setMonoInline oldInline)
+ handle ex => (Settings.setMonoInline oldInline;
+ MonoReduce.fullMode := oldFull;
+ raise ex)
+ end
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-16 02:51:01 +0000