summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 16:30:46 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-04-13 16:30:46 -0400
commit27a53b9cda6c4e3e1732659fe44a7fb6bad03655 (patch)
tree4161156186558a96b0a98dfd068d7491bb518d83
parent8f4b1358953635df5066b83c250a64f28caf8190 (diff)
Completely redid main Iflow logic; so far, policy and policy2 work
Diffstat
-rw-r--r--src/compiler.sml2
-rw-r--r--src/iflow.sml1816
-rw-r--r--tests/policy.ur4
-rw-r--r--tests/policy2.ur22
-rw-r--r--tests/policy2.urp1
-rw-r--r--tests/policy2.urs1
6 files changed, 629 insertions, 1217 deletions
diff --git a/src/compiler.sml b/src/compiler.sml
index def0e6c3..ba10ed74 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -75,7 +75,7 @@ type ('src, 'dst) transform = {
}
val debug = ref false
-val doIflow = ref false
+val doIflow = ref true
fun transform (ph : ('src, 'dst) phase) name = {
func = fn input => let
diff --git a/src/iflow.sml b/src/iflow.sml
index 24d9d4a6..c8a8df89 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -72,7 +72,6 @@ datatype exp =
| Func of func * exp list
| Recd of (string * exp) list
| Proj of exp * string
- | Finish
datatype reln =
Known
@@ -95,12 +94,6 @@ datatype prop =
| Reln of reln * exp list
| Cond of exp * prop
-val unif = ref (IM.empty : exp IM.map)
-
-fun reset () = unif := IM.empty
-fun save () = !unif
-fun restore x = unif := x
-
local
open Print
val string = PD.string
@@ -117,10 +110,7 @@ fun p_exp e =
case e of
Const p => Prim.p_t p
| Var n => string ("x" ^ Int.toString n)
- | Lvar n =>
- (case IM.find (!unif, n) of
- NONE => string ("X" ^ Int.toString n)
- | SOME e => p_exp e)
+ | Lvar n => string ("X" ^ Int.toString n)
| Func (f, es) => box [p_func f,
string "(",
p_list p_exp es,
@@ -134,7 +124,6 @@ fun p_exp e =
string "}"]
| Proj (e, x) => box [p_exp e,
string ("." ^ x)]
- | Finish => string "FINISH"
fun p_bop s es =
case es of
@@ -203,18 +192,6 @@ fun p_prop p =
end
-local
- val count = ref 1
-in
-fun newLvar () =
- let
- val n = !count
- in
- count := n + 1;
- n
- end
-end
-
fun isKnown e =
case e of
Const _ => true
@@ -223,23 +200,22 @@ fun isKnown e =
| Proj (e, _) => isKnown e
| _ => false
-fun isFinish e =
- case e of
- Finish => true
- | _ => false
-
-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)
- | Finish => Finish
+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
@@ -250,192 +226,7 @@ fun p_atom a =
AReln x => Reln x
| ACond x => Cond x)
-fun lvarIn lv =
- let
- fun lvi e =
- case e of
- Const _ => false
- | Var _ => false
- | Lvar lv' => lv' = lv
- | Func (_, es) => List.exists lvi es
- | Recd xes => List.exists (lvi o #2) xes
- | Proj (e, _) => lvi e
- | Finish => false
- in
- lvi
- end
-
-fun lvarInP lv =
- let
- fun lvi p =
- case p of
- True => false
- | False => false
- | Unknown => true
- | And (p1, p2) => lvi p1 orelse lvi p2
- | Or (p1, p2) => lvi p1 orelse lvi p2
- | Reln (_, es) => List.exists (lvarIn lv) es
- | Cond (e, p) => lvarIn lv e orelse lvi p
- in
- lvi
- end
-
-fun varIn lv =
- let
- fun lvi e =
- case e of
- Const _ => false
- | Lvar _ => false
- | Var lv' => lv' = lv
- | Func (_, es) => List.exists lvi es
- | Recd xes => List.exists (lvi o #2) xes
- | Proj (e, _) => lvi e
- | Finish => false
- in
- lvi
- end
-
-fun varInP lv =
- let
- fun lvi p =
- case p of
- True => false
- | False => false
- | Unknown => false
- | And (p1, p2) => lvi p1 orelse lvi p2
- | Or (p1, p2) => lvi p1 orelse lvi p2
- | Reln (_, es) => List.exists (varIn lv) es
- | Cond (e, p) => varIn lv e orelse lvi p
- in
- lvi
- end
-
-fun bumpLvars by =
- let
- fun lvi e =
- case e of
- Const _ => e
- | Var _ => e
- | Lvar lv => Lvar (lv + by)
- | Func (f, es) => Func (f, map lvi es)
- | Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes)
- | Proj (e, f) => Proj (lvi e, f)
- | Finish => e
- in
- lvi
- end
-
-fun bumpLvarsP by =
- let
- fun lvi p =
- case p of
- True => p
- | False => p
- | Unknown => p
- | And (p1, p2) => And (lvi p1, lvi p2)
- | Or (p1, p2) => And (lvi p1, lvi p2)
- | Reln (r, es) => Reln (r, map (bumpLvars by) es)
- | Cond (e, p) => Cond (bumpLvars by e, lvi p)
- in
- lvi
- end
-
-fun maxLvar e =
- let
- fun lvi e =
- case e of
- Const _ => 0
- | Var _ => 0
- | Lvar lv => lv
- | Func (f, es) => foldl Int.max 0 (map lvi es)
- | Recd xes => foldl Int.max 0 (map (lvi o #2) xes)
- | Proj (e, f) => lvi e
- | Finish => 0
- in
- lvi e
- end
-
-fun maxLvarP p =
- let
- fun lvi p =
- case p of
- True => 0
- | False => 0
- | Unknown => 0
- | And (p1, p2) => Int.max (lvi p1, lvi p2)
- | Or (p1, p2) => Int.max (lvi p1, lvi p2)
- | Reln (r, es) => foldl Int.max 0 (map maxLvar es)
- | Cond (e, p) => Int.max (maxLvar e, lvi p)
- in
- lvi p
- end
-
-fun eq' (e1, e2) =
- case (e1, e2) of
- (Const p1, Const p2) => Prim.equal (p1, p2)
- | (Var n1, Var n2) => n1 = n2
-
- | (Lvar n1, _) =>
- (case IM.find (!unif, n1) of
- SOME e1 => eq' (e1, e2)
- | NONE =>
- case e2 of
- Lvar n2 =>
- (case IM.find (!unif, n2) of
- SOME e2 => eq' (e1, e2)
- | NONE => n1 = n2
- orelse (unif := IM.insert (!unif, n2, e1);
- true))
- | _ =>
- if lvarIn n1 e2 then
- false
- else
- (unif := IM.insert (!unif, n1, e2);
- true))
-
- | (_, Lvar n2) =>
- (case IM.find (!unif, n2) of
- SOME e2 => eq' (e1, e2)
- | NONE =>
- if lvarIn n2 e1 then
- false
- else
- ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
- ("e1", p_exp e1)];*)
- unif := IM.insert (!unif, n2, e1);
- true))
-
- | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
- | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
- | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
- | (Finish, Finish) => true
- | _ => false
-
-fun eq (e1, e2) =
- let
- val saved = save ()
- in
- if eq' (simplify e1, simplify e2) then
- true
- else
- (restore saved;
- false)
- end
-
val debug = ref false
-
-fun eeq (e1, e2) =
- case (e1, e2) of
- (Const p1, Const p2) => Prim.equal (p1, p2)
- | (Var n1, Var n2) => n1 = n2
- | (Lvar n1, Lvar n2) => n1 = n2
- | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
- | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
- List.all (fn (x2, e2) =>
- List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
- | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
- | (Finish, Finish) => true
- | _ => false
(* Congruence closure *)
structure Cc :> sig
@@ -445,6 +236,7 @@ structure Cc :> sig
exception Undetermined
val database : unit -> database
+ val clear : database -> unit
val assert : database * atom -> unit
val check : database * atom -> bool
@@ -490,6 +282,12 @@ fun database () = {Vars = ref IM.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
@@ -594,10 +392,7 @@ fun representative (db : database, e) =
#Vars db := IM.insert (!(#Vars db), n, r);
r
end)
- | Lvar n =>
- (case IM.find (!unif, n) of
- NONE => raise Undetermined
- | SOME e => rep e)
+ | Lvar _ => raise Undetermined
| Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
SOME r => repOf r
| NONE =>
@@ -735,7 +530,6 @@ fun representative (db : database, e) =
end
| _ => raise Contradiction
end
- | Finish => raise Contradiction
in
rep e
end
@@ -938,25 +732,6 @@ fun builtFrom (db, {Base = bs, Derived = d}) =
end
-fun decomp fals or =
- let
- fun decomp p k =
- case p of
- True => k []
- | False => fals
- | Unknown => k []
- | And (p1, p2) =>
- decomp p1 (fn ps1 =>
- decomp p2 (fn ps2 =>
- k (ps1 @ ps2)))
- | Or (p1, p2) =>
- or (decomp p1 k, fn () => decomp p2 k)
- | Reln x => k [AReln x]
- | Cond x => k [ACond x]
- in
- decomp
- end
-
val tabs = ref (SM.empty : (string list * string list list) SM.map)
fun ccOf hyps =
@@ -1018,65 +793,6 @@ fun ccOf hyps =
cc
end
-fun imply (cc, hyps, goals, outs) =
- let
- fun gls goals onFail acc =
- case goals of
- [] =>
- ((List.all (fn a =>
- if Cc.check (cc, a) then
- true
- else
- ((*Print.prefaces "Can't prove"
- [("a", p_atom a),
- ("hyps", Print.p_list p_atom hyps),
- ("db", Cc.p_database cc)];*)
- false)) acc
- andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
- andalso (case outs of
- NONE => true
- | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
- Base = outs})))
- handle Cc.Contradiction => false
- | Cc.Undetermined => false)
- orelse onFail ()
- | (g as AReln (Sql gf, [ge])) :: goals =>
- let
- fun hps hyps =
- case hyps of
- [] => gls goals onFail (g :: acc)
- | (h as AReln (Sql hf, [he])) :: hyps =>
- if gf = hf then
- let
- val saved = save ()
- in
- if eq (ge, he) then
- let
- val changed = IM.numItems (!unif)
- <> IM.numItems saved
- in
- gls goals (fn () => (restore saved;
- changed
- andalso hps hyps))
- acc
- end
- else
- hps hyps
- end
- else
- hps hyps
- | _ :: hyps => hps hyps
- in
- hps hyps
- end
- | g :: goals => gls goals onFail (g :: acc)
- in
- reset ();
- (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
- ("goals", Print.p_list p_atom goals)];*)
- gls goals (fn () => false) []
- end
-
fun patCon pc =
case pc of
PConVar n => "C" ^ Int.toString n
@@ -1430,6 +1146,211 @@ val dml = log "dml"
wrap delete Delete,
wrap update Update])
+type check = exp * ErrorMsg.span
+
+structure St :> sig
+ val reset : unit -> unit
+
+ type stashed
+ val stash : unit -> stashed
+ val reinstate : stashed -> 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
+end = struct
+
+val hnames = ref 1
+
+type hyps = int * atom list
+
+val db = Cc.database ()
+val path = ref ([] : (hyps * check) option ref list)
+val hyps = ref (0, [] : atom list)
+val nvar = ref 0
+
+fun reset () = (Cc.clear db;
+ path := [];
+ hyps := (0, []);
+ nvar := 0)
+
+fun setHyps (h as (n', hs)) =
+ let
+ val (n, _) = !hyps
+ in
+ if n' = n then
+ ()
+ else
+ (hyps := h;
+ Cc.clear db;
+ app (fn a => Cc.assert (db, a)) hs)
+ end
+
+type stashed = int * (hyps * check) option ref list * (int * atom list)
+fun stash () = (!nvar, !path, !hyps)
+fun reinstate (nv, p, h) =
+ (nvar := nv;
+ path := p;
+ setHyps h)
+
+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);
+ app (fn a => Cc.assert (db, a)) ats
+ end
+
+fun addPath c = path := ref (SOME (!hyps, c)) :: !path
+
+val sendable = ref ([] : (atom list * exp list) list)
+
+fun checkGoals goals unifs succ fail =
+ case goals of
+ [] => succ (unifs, [])
+ | AReln (Sql tab, [Lvar lv]) :: goals =>
+ let
+ val saved = stash ()
+ val (_, hyps) = !hyps
+
+ fun tryAll unifs hyps =
+ case hyps of
+ [] => fail ()
+ | AReln (Sql tab', [e]) :: hyps =>
+ if tab' = tab then
+ checkGoals goals (IM.insert (unifs, lv, e)) succ
+ (fn () => tryAll unifs hyps)
+ else
+ tryAll unifs hyps
+ | _ :: hyps => tryAll unifs hyps
+ in
+ tryAll unifs hyps
+ end
+ | AReln (r, es) :: goals => checkGoals goals unifs
+ (fn (unifs, ls) => succ (unifs, AReln (r, map (simplify unifs) es) :: ls))
+ fail
+ | ACond _ :: _ => fail ()
+
+fun buildable (e, loc) =
+ let
+ fun doPols pols acc fail =
+ case pols of
+ [] => ((*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
+ ("Derived", p_exp e),
+ ("Hyps", Print.p_list p_atom (#2 (!hyps)))];*)
+ if Cc.builtFrom (db, {Base = acc, Derived = e}) then
+ ()
+ else
+ fail ())
+ | (goals, es) :: pols =>
+ checkGoals goals IM.empty
+ (fn (unifs, goals) =>
+ if List.all (fn a => Cc.check (db, a)) goals then
+ doPols pols (map (simplify unifs) es @ acc) fail
+ else
+ doPols pols acc fail)
+ (fn () => doPols pols acc fail)
+ in
+ doPols (!sendable) []
+ (fn () => let
+ val (_, hs) = !hyps
+ in
+ ErrorMsg.errorAt loc "The information flow policy may be violated here.";
+ Print.preface ("Hypotheses", Print.p_list p_atom hs)
+ end)
+ end
+
+fun checkPaths () =
+ let
+ val hs = !hyps
+ in
+ app (fn r =>
+ case !r of
+ NONE => ()
+ | SOME (hs, e) =>
+ (r := NONE;
+ setHyps hs;
+ buildable e)) (!path);
+ setHyps hs
+ end
+
+fun allowSend v = sendable := v :: !sendable
+
+fun send (e, loc) = ((*Print.preface ("Send", p_exp e);*)
+ checkPaths ();
+ if isKnown e then
+ ()
+ else
+ buildable (e, loc))
+
+fun doable pols (loc : ErrorMsg.span) =
+ let
+ val pols = !pols
+ in
+ if List.exists (fn goals =>
+ checkGoals goals IM.empty
+ (fn (_, goals) => List.all (fn a => Cc.check (db, a)) goals)
+ (fn () => false)) pols then
+ ()
+ else
+ let
+ val (_, hs) = !hyps
+ in
+ ErrorMsg.errorAt loc "The database update policy may be violated here.";
+ Print.preface ("Hypotheses", Print.p_list p_atom hs)
+ 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 havocReln r =
+ let
+ val n = !hnames
+ val (_, hs) = !hyps
+ in
+ hnames := n + 1;
+ hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs)
+ end
+
+end
+
+
fun removeDups (ls : (string * string) list) =
case ls of
[] => []
@@ -1443,63 +1364,42 @@ fun removeDups (ls : (string * string) list) =
x :: ls
end
-datatype queryMode =
- SomeCol
- | AllCols of exp
-
fun expIn rv env rvOf =
let
- fun expIn (e, rvN) =
+ fun expIn e =
let
- fun default () =
- let
- val (rvN, e') = rv rvN
- in
- (inl e', rvN)
- end
+ fun default () = inl (rv ())
in
case e of
- SqConst p => (inl (Const p), rvN)
- | Field (v, f) => (inl (Proj (rvOf v, f)), rvN)
+ SqConst p => inl (Const p)
+ | Field (v, f) => inl (Proj (rvOf v, f))
| Binop (bo, e1, e2) =>
let
- val (e1, rvN) = expIn (e1, rvN)
- val (e2, rvN) = expIn (e2, rvN)
+ val e1 = expIn e1
+ val e2 = expIn e2
in
- (inr (case (bo, e1, e2) of
- (Exps f, inl e1, inl e2) => f (e1, e2)
- | (Props f, inr p1, inr p2) => f (p1, p2)
- | _ => Unknown), rvN)
+ inr (case (bo, e1, e2) of
+ (Exps f, inl e1, inl e2) => f (e1, e2)
+ | (Props f, inr p1, inr p2) => f (p1, p2)
+ | _ => Unknown)
end
| SqKnown e =>
- (case expIn (e, rvN) of
- (inl e, rvN) => (inr (Reln (Known, [e])), rvN)
- | _ => (inr Unknown, rvN))
+ (case expIn e of
+ inl e => inr (Reln (Known, [e]))
+ | _ => inr Unknown)
| Inj e =>
let
fun deinj e =
case #1 e of
- ERel n => (List.nth (env, n), rvN)
- | EField (e, f) =>
- let
- val (e, rvN) = deinj e
- in
- (Proj (e, f), rvN)
- end
- | _ =>
- let
- val (rvN, e) = rv rvN
- in
- (e, rvN)
- end
-
- val (e, rvN) = deinj e
+ ERel n => List.nth (env, n)
+ | EField (e, f) => Proj (deinj e, f)
+ | _ => rv ()
in
- (inl e, rvN)
+ inl (deinj e)
end
| SqFunc (f, e) =>
- (case expIn (e, rvN) of
- (inl e, rvN) => (inl (Func (Other f, [e])), rvN)
+ (case expIn e of
+ inl e => inl (Func (Other f, [e]))
| _ => default ())
| Count => default ()
@@ -1508,32 +1408,67 @@ fun expIn rv env rvOf =
expIn
end
-fun queryProp env rvN rv oe e =
+fun decomp {Save = save, Restore = restore, Add = add} =
+ let
+ fun go p k =
+ case p of
+ True => k ()
+ | False => ()
+ | Unknown => ()
+ | And (p1, p2) => go p1 (fn () => go p2 k)
+ | 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 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,
+ UsedExp : exp -> unit,
+ Cont : queryMode
+}
+
+fun doQuery (arg : 'a doQuery) e =
let
- fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
- ^ ErrorMsg.spanToString (#2 e) ^ "\n");
- (rvN, Unknown, [], []))
+ fun default () = print ("Warning: Information flow checker can't parse SQL query at "
+ ^ ErrorMsg.spanToString (#2 e) ^ "\n")
in
case parse query e of
NONE => default ()
| SOME q =>
let
- fun doQuery (q, rvN) =
+ fun doQuery q =
case q of
Query1 r =>
let
- val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
- let
- val (rvN, e) = rv rvN
- in
- ((v, e), rvN)
- end) rvN (#From r)
+ val rvs = map (fn (_, v) => (v, #NextVar arg ())) (#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 (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
+
fun usedFields e =
case e of
SqConst _ => []
@@ -1544,695 +1479,276 @@ fun queryProp env rvN rv oe e =
| SqFunc (_, e) => usedFields e
| Count => []
- val p =
- foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
-
- val expIn = expIn rv env rvOf
-
- val (p, rvN) = case #Where r of
- NONE => (p, rvN)
- | SOME e =>
- case expIn (e, rvN) of
- (inr p', rvN) => (And (p, p'), rvN)
- | _ => (p, rvN)
-
- fun normal () =
- case oe of
- SomeCol =>
+ fun doUsed () = case #Where r of
+ NONE => ()
+ | SOME e =>
+ #UsedExp arg (Recd (ListUtil.mapi
+ (fn (n, (v, f)) => (Int.toString n,
+ Proj (rvOf v, f)))
+ (usedFields e)))
+
+ fun normal' () =
+ case #Cont arg of
+ SomeCol k =>
let
- val (sis, rvN) =
- ListUtil.foldlMap
- (fn (si, rvN) =>
- case si of
- SqField (v, f) => (Proj (rvOf v, f), rvN)
- | SqExp (e, f) =>
- case expIn (e, rvN) of
- (inr _, _) =>
- let
- val (rvN, e) = rv rvN
- in
- (e, rvN)
- end
- | (inl e, rvN) => (e, rvN)) rvN (#Select r)
+ 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
- (rvN, p, True, sis)
+ k sis
end
- | AllCols oe =>
+ | AllCols k =>
let
- val (ts, es, rvN) =
- foldl (fn (si, (ts, es, rvN)) =>
+ 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, rvN)
+ (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
end
| SqExp (e, f) =>
let
- val (e, rvN) =
- case expIn (e, rvN) of
- (inr _, rvN) =>
- let
- val (rvN, e) = rv rvN
- in
- (e, rvN)
- end
- | (inl e, rvN) => (e, rvN)
+ val e =
+ case expIn e of
+ inr _ => #NextVar arg ()
+ | inl e => e
in
- (ts, SM.insert (es, f, e), rvN)
+ (ts, SM.insert (es, f, e))
end)
- (SM.empty, SM.empty, rvN) (#Select r)
-
- val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
- (SM.listItemsi ts)
- @ SM.listItemsi es)])
+ (SM.empty, SM.empty) (#Select r)
in
- (rvN, And (p, p'), True, [])
+ k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
+ (SM.listItemsi ts)
+ @ SM.listItemsi es))
end
- val (rvN, p, wp, outs) =
- case #Select r of
- [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
- (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
- Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
- (case oe of
- SomeCol =>
- let
- val (rvN, oe) = rv rvN
- in
- (rvN,
- Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
- And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
- p)),
- Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
- [oe])
- end
- | AllCols oe =>
- let
- fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
- in
- (rvN,
- Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
- And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
- p)),
- oeEq (Func (DtCon0 "Basis.bool.True", [])),
- [])
- end)
- | _ => normal ())
- | _ => normal ()
+ fun doWhere final =
+ (addFrom ();
+ case #Where r of
+ NONE => (doUsed (); final ())
+ | SOME e =>
+ case expIn e of
+ inl _ => (doUsed (); final ())
+ | inr p =>
+ let
+ val saved = #Save arg ()
+ in
+ decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
+ p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
+ #Restore arg saved
+ end)
+ handle Cc.Contradiction => ()
+
+ fun normal () = doWhere normal'
in
- (rvN, p, map (fn x => (wp, x))
- (case #Where r of
- NONE => []
- | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)), outs)
+ (case #Select r of
+ [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
+ (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
+ Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
+ (case #Cont arg of
+ SomeCol _ => ()
+ | AllCols k =>
+ let
+ fun answer e = k (Recd [(f, e)])
+
+ val () = answer (Func (DtCon0 "Basis.bool.False", []))
+ val saved = #Save arg ()
+ in
+ doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
+ #Restore arg saved
+ end)
+ | _ => normal ())
+ | _ => normal ())
+ before #Restore arg saved
end
| Union (q1, q2) =>
let
- val (rvN, p1, used1, outs1) = doQuery (q1, rvN)
- val (rvN, p2, used2, outs2) = doQuery (q2, rvN)
+ val saved = #Save arg ()
in
- case (outs1, outs2) of
- ([], []) => (rvN, Or (p1, p2),
- map (fn (p, e) => (And (p1, p), e)) used1
- @ map (fn (p, e) => (And (p2, p), e)) used2, [])
- | _ => default ()
+ doQuery q1;
+ #Restore arg saved;
+ doQuery q2;
+ #Restore arg saved
end
in
- doQuery (q, rvN)
- end
- end
-
-fun insertProp rvN rv e =
- let
- fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
- ^ ErrorMsg.spanToString (#2 e) ^ "\n");
- Unknown)
- in
- case parse query e of
- SOME (Query1 r) =>
- let
- val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
- let
- val (rvN, e) = rv rvN
- in
- ((v, e), rvN)
- end) rvN (#From r)
-
- fun rvOf v =
- case List.find (fn (v', _) => v' = v) rvs of
- NONE => raise Fail "Iflow.insertProp: Bad table variable"
- | SOME (_, e) => e
-
- val p =
- foldl (fn ((t, v), p) =>
- let
- val t =
- case v of
- "New" => t ^ "$New"
- | _ => t
- in
- And (p, Reln (Sql t, [rvOf v]))
- end) True (#From r)
-
- val expIn = expIn rv [] rvOf
- in
- case #Where r of
- NONE => p
- | SOME e =>
- case expIn (e, rvN) of
- (inr p', _) => And (p, p')
- | _ => p
- end
- | _ => default ()
- end
-
-fun deleteProp rvN rv e =
- let
- fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
- ^ ErrorMsg.spanToString (#2 e) ^ "\n");
- Unknown)
- in
- case parse query e of
- SOME (Query1 r) =>
- let
- val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
- let
- val (rvN, e) = rv rvN
- in
- ((v, e), rvN)
- end) rvN (#From r)
-
- fun rvOf v =
- case List.find (fn (v', _) => v' = v) rvs of
- NONE => raise Fail "Iflow.deleteProp: Bad table variable"
- | SOME (_, e) => e
-
- val p =
- foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
-
- val expIn = expIn rv [] rvOf
- in
- And (Reln (Sql "$Old", [rvOf "Old"]),
- case #Where r of
- NONE => p
- | SOME e =>
- case expIn (e, rvN) of
- (inr p', _) => And (p, p')
- | _ => p)
- end
- | _ => default ()
- end
-
-fun updateProp rvN rv e =
- let
- fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
- ^ ErrorMsg.spanToString (#2 e) ^ "\n");
- Unknown)
- in
- case parse query e of
- SOME (Query1 r) =>
- let
- val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
- let
- val (rvN, e) = rv rvN
- in
- ((v, e), rvN)
- end) rvN (#From r)
-
- fun rvOf v =
- case List.find (fn (v', _) => v' = v) rvs of
- NONE => raise Fail "Iflow.insertProp: Bad table variable"
- | SOME (_, e) => e
-
- val p =
- foldl (fn ((t, v), p) =>
- let
- val t =
- case v of
- "New" => t ^ "$New"
- | _ => t
- in
- And (p, Reln (Sql t, [rvOf v]))
- end) True (#From r)
-
- val expIn = expIn rv [] rvOf
- in
- And (Reln (Sql "$Old", [rvOf "Old"]),
- case #Where r of
- NONE => p
- | SOME e =>
- case expIn (e, rvN) of
- (inr p', _) => And (p, p')
- | _ => p)
+ doQuery q
end
- | _ => default ()
end
fun evalPat env e (pt, _) =
case pt of
- PWild => (env, True)
- | PVar _ => (e :: env, True)
- | PPrim _ => (env, True)
- | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
+ PWild => env
+ | PVar _ => e :: env
+ | PPrim _ => env
+ | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
| PCon (_, pc, SOME pt) =>
let
- val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
+ val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
in
- (env, And (p, Reln (PCon1 (patCon pc), [e])))
+ St.assert [AReln (PCon1 (patCon pc), [e])];
+ env
end
| PRecord xpts =>
- foldl (fn ((x, pt, _), (env, p)) =>
- let
- val (env, p') = evalPat env (Proj (e, x)) pt
- in
- (env, And (p', p))
- end) (env, True) xpts
- | PNone _ => (env, Reln (PCon0 "None", [e]))
+ 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, p) = evalPat env (Func (UnCon "Some", [e])) pt
+ val env = evalPat env (Func (UnCon "Some", [e])) pt
in
- (env, And (p, Reln (PCon1 "Some", [e])))
+ St.assert [AReln (PCon1 "Some", [e])];
+ env
end
-fun peq (p1, p2) =
- case (p1, p2) of
- (True, True) => true
- | (False, False) => true
- | (Unknown, Unknown) => true
- | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
- | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
- | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
- | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
- | _ => false
-
-fun removeRedundant p1 =
+fun evalExp env (e as (_, loc)) k =
let
- fun rr p2 =
- if peq (p1, p2) then
- True
- else
- case p2 of
- And (x, y) => And (rr x, rr y)
- | Or (x, y) => Or (rr x, rr y)
- | _ => p2
- in
- rr
- end
-
-datatype cflow = Case | Where
-datatype flow = Data | Control of cflow
-type check = ErrorMsg.span * exp * prop
-type dml = ErrorMsg.span * prop
-
-structure St :> sig
- type t
- val create : {Var : int,
- Ambient : prop} -> t
-
- val curVar : t -> int
- val nextVar : t -> t * int
-
- val ambient : t -> prop
- val setAmbient : t * prop -> t
-
- val paths : t -> (check * cflow) list
- val addPath : t * (check * cflow) -> t
- val addPaths : t * (check * cflow) list -> t
- val clearPaths : t -> t
- val setPaths : t * (check * cflow) list -> t
+ (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
- val sent : t -> (check * flow) list
- val addSent : t * (check * flow) -> t
- val setSent : t * (check * flow) list -> t
-
- val inserted : t -> dml list
- val addInsert : t * dml -> t
-
- val deleted : t -> dml list
- val addDelete : t * dml -> t
-
- val updated : t -> dml list
- val addUpdate : t * dml -> t
-end = struct
-
-type t = {Var : int,
- Ambient : prop,
- Path : (check * cflow) list,
- Sent : (check * flow) list,
- Insert : dml list,
- Delete : dml list,
- Update : dml list}
-
-fun create {Var = v, Ambient = p} = {Var = v,
- Ambient = p,
- Path = [],
- Sent = [],
- Insert = [],
- Delete = [],
- Update = []}
-
-fun curVar (t : t) = #Var t
-fun nextVar (t : t) = ({Var = #Var t + 1,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}, #Var t)
-
-fun ambient (t : t) = #Ambient t
-fun setAmbient (t : t, p) = {Var = #Var t,
- Ambient = p,
- Path = #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-
-fun paths (t : t) = #Path t
-fun addPath (t : t, c) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = c :: #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-fun addPaths (t : t, cs) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = cs @ #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-fun clearPaths (t : t) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = [],
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-fun setPaths (t : t, cs) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = cs,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-
-fun sent (t : t) = #Sent t
-fun addSent (t : t, c) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = c :: #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-fun setSent (t : t, cs) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = cs,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-
-fun inserted (t : t) = #Insert t
-fun addInsert (t : t, c) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = #Sent t,
- Insert = c :: #Insert t,
- Delete = #Delete t,
- Update = #Update t}
-
-fun deleted (t : t) = #Delete t
-fun addDelete (t : t, c) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = c :: #Delete t,
- Update = #Update t}
-
-fun updated (t : t) = #Update t
-fun addUpdate (t : t, c) = {Var = #Var t,
- Ambient = #Ambient t,
- Path = #Path t,
- Sent = #Sent t,
- Insert = #Insert t,
- Delete = #Delete t,
- Update = c :: #Update t}
-
-end
-
-fun havocReln r =
- let
- fun hr p =
- case p of
- True => p
- | False => p
- | Unknown => p
- | And (p1, p2) => And (hr p1, hr p2)
- | Or (p1, p2) => Or (hr p1, hr p2)
- | Reln (r', _) => if r' = r then True else p
- | Cond (e, p) => Cond (e, hr p)
- in
- hr
- end
-
-fun evalExp env (e as (_, loc), st) =
- let
- fun default () =
- let
- val (st, nv) = St.nextVar st
- in
- (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
- ("nv", p_exp (Var nv))];*)
- (Var nv, st)
- end
-
- fun addSent (p, e, st) =
- let
- val st = if isKnown e then
- st
- else
- St.addSent (st, ((loc, e, p), Data))
-
- val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
- in
- St.clearPaths st
- end
+ fun default () = k (Var (St.nextVar ()))
fun doFfi (m, s, es) =
if m = "Basis" andalso SS.member (writers, s) then
let
- val (es, st) = ListUtil.foldlMap (evalExp env) st es
+ fun doArgs es =
+ case es of
+ [] => k (Recd [])
+ | e :: es =>
+ evalExp env e (fn e => (St.send (e, loc); doArgs es))
in
- (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
+ doArgs es
end
else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
default ()
else
let
- val (es, st) = ListUtil.foldlMap (evalExp env) st es
+ 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
- (Func (Other (m ^ "." ^ s), es), st)
+ doArgs (es, [])
end
in
case #1 e of
- EPrim p => (Const p, st)
- | ERel n => (List.nth (env, n), st)
+ EPrim p => k (Const p)
+ | ERel n => k (List.nth (env, n))
| ENamed _ => default ()
- | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
- | ECon (_, pc, SOME e) =>
- let
- val (e, st) = evalExp env (e, st)
- in
- (Func (DtCon1 (patCon pc), [e]), st)
- end
- | ENone _ => (Func (DtCon0 "None", []), st)
- | ESome (_, e) =>
- let
- val (e, st) = evalExp env (e, st)
- in
- (Func (DtCon1 "Some", [e]), st)
- end
+ | 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 x => doFfi x
| EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
- | EApp (e1, e2) =>
- let
- val (e1, st) = evalExp env (e1, st)
- in
- case e1 of
- Finish => (Finish, st)
- | _ => default ()
- end
+ | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
| EAbs _ => default ()
- | EUnop (s, e1) =>
- let
- val (e1, st) = evalExp env (e1, st)
- in
- (Func (Other s, [e1]), st)
- end
- | EBinop (s, e1, e2) =>
- let
- val (e1, st) = evalExp env (e1, st)
- val (e2, st) = evalExp env (e2, st)
- in
- (Func (Other s, [e1, e2]), st)
- end
+ | 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
- val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
- let
- val (e, st) = evalExp env (e, st)
- in
- ((x, e), st)
- end) st xets
+ 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
- (Recd xes, st)
- end
- | EField (e, s) =>
- let
- val (e, st) = evalExp env (e, st)
- in
- (Proj (e, s), st)
+ doFields (xets, [])
end
+ | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
| ECase (e, pes, {result = res, ...}) =>
- let
- val (e, st) = evalExp env (e, st)
- val (st, r) = St.nextVar st
- val orig = St.ambient st
- val origPaths = St.paths st
-
- val st = St.addPath (st, ((loc, e, orig), Case))
-
- (*val () = Print.prefaces "Case" [("loc", Print.PD.string (ErrorMsg.spanToString loc)),
- ("e", Print.p_list (MonoPrint.p_exp MonoEnv.empty o #2) pes),
- ("orig", p_prop orig)]*)
-
- val (st, ambients, paths) =
- foldl (fn ((pt, pe), (st, ambients, paths)) =>
+ evalExp env e (fn e =>
let
- val (env, pp) = evalPat env e pt
- val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
-
- val this = And (removeRedundant orig (St.ambient st'),
- Reln (Eq, [Var r, pe]))
+ val () = St.addPath (e, loc)
in
- (St.setPaths (st', origPaths),
- Or (ambients, this),
- St.paths st' @ paths)
- end) (st, False, []) pes
-
- val st = case #1 res of
- TRecord [] => St.setPaths (st, origPaths)
- | _ => St.setPaths (st, paths)
- in
- (Var r, St.setAmbient (st, And (orig, ambients)))
- end
+ app (fn (p, pe) =>
+ let
+ val saved = St.stash ()
+
+ val env = evalPat env e p
+ in
+ evalExp env pe k;
+ St.reinstate saved
+ end) pes
+ end handle Cc.Contradiction => ())
| EStrcat (e1, e2) =>
- let
- val (e1, st) = evalExp env (e1, st)
- val (e2, st) = evalExp env (e2, st)
- in
- (Func (Other "cat", [e1, e2]), st)
- end
- | EError _ => (Finish, st)
+ 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 = b, mimeType = m, ...} =>
- let
- val (b, st) = evalExp env (b, st)
- val (m, st) = evalExp env (m, st)
- in
- (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
- end
+ evalExp env b (fn b =>
+ (St.send (b, loc);
+ evalExp env m
+ (fn m => St.send (m, loc))))
| ERedirect (e, _) =>
- let
- val (e, st) = evalExp env (e, st)
- in
- (Finish, addSent (St.ambient st, e, st))
- end
+ evalExp env e (fn e => St.send (e, loc))
| EWrite e =>
- let
- val (e, st) = evalExp env (e, st)
- in
- (Recd [], addSent (St.ambient st, e, st))
- end
+ evalExp env e (fn e => (St.send (e, loc);
+ k (Recd [])))
| ESeq (e1, e2) =>
- let
- val (_, st) = evalExp env (e1, st)
- in
- evalExp env (e2, st)
- end
+ evalExp env e1 (fn _ => evalExp env e2 k)
| ELet (_, _, e1, e2) =>
- let
- val (e1, st) = evalExp env (e1, st)
- in
- evalExp (e1 :: env) (e2, st)
- end
+ evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
| EClosure (n, es) =>
let
- val (es, st) = ListUtil.foldlMap (evalExp env) st es
+ 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
- (Func (Other ("Cl" ^ Int.toString n), es), st)
+ doArgs (es, [])
end
| EQuery {query = q, body = b, initial = i, state = state, ...} =>
- let
- val (_, st) = evalExp env (q, st)
- val (i, st) = evalExp env (i, st)
-
- val (st', r) = St.nextVar st
- val (st', acc) = St.nextVar st'
-
- val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
- val amb = removeRedundant (St.ambient st) (St.ambient st')
-
- val (st', qp, used, _) =
- queryProp env
- st' (fn st' =>
- let
- val (st', rv) = St.nextVar st'
- in
- (st', Var rv)
- end)
- (AllCols (Var r)) q
-
- val (st, res) =
- case #1 state of
- TRecord [] =>
- (st, Func (DtCon0 "unit", []))
- | _ =>
- if varInP acc (St.ambient st') then
- let
- val (st, r) = St.nextVar st
- in
- (st, Var r)
- end
- else
- let
- val (st', out) = St.nextVar st'
-
- val p = And (St.ambient st,
- Or (Reln (Eq, [Var out, i]),
- And (Reln (Eq, [Var out, b]),
- And (qp, amb))))
- in
- (St.setAmbient (st', p), Var out)
- end
-
- val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
+ evalExp env q (fn _ =>
+ evalExp env i (fn i =>
+ let
+ val saved = St.stash ()
- val p' = And (qp, St.ambient st')
- val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
- in
- (res, St.addPaths (St.setSent (st, sent), paths))
- end
+ val r = Var (St.nextVar ())
+ val acc = Var (St.nextVar ())
+ in
+ if MonoUtil.Exp.existsB {typ = fn _ => false,
+ exp = fn (n, e) =>
+ case e of
+ ERel n' => n' = n
+ | _ => false,
+ bind = fn (n, b) =>
+ case b of
+ MonoUtil.Exp.RelE _ => n + 1
+ | _ => n}
+ 0 b then
+ doQuery {Env = env,
+ NextVar = Var o St.nextVar,
+ Add = fn a => St.assert [a],
+ Save = St.stash,
+ Restore = St.reinstate,
+ UsedExp = fn e => St.send (e, loc),
+ Cont = AllCols (fn _ => (St.reinstate saved;
+ evalExp
+ (acc :: r :: env)
+ b (fn _ => default ())))} q
+ else
+ doQuery {Env = env,
+ NextVar = Var o St.nextVar,
+ Add = fn a => St.assert [a],
+ Save = St.stash,
+ Restore = St.reinstate,
+ UsedExp = fn e => St.send (e, loc),
+ Cont = AllCols (fn x =>
+ (St.assert [AReln (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 "
@@ -2242,86 +1758,66 @@ fun evalExp env (e as (_, loc), st) =
case d of
Insert (tab, es) =>
let
- val (st, new) = St.nextVar st
+ val new = St.nextVar ()
- fun rv st =
- let
- val (st, n) = St.nextVar st
- in
- (st, Var n)
- end
+ val expIn = expIn (Var o St.nextVar) env
+ (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
- val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT")
+ 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 (es, st) = ListUtil.foldlMap
- (fn ((x, e), st) =>
- let
- val (e, st) = case expIn (e, st) of
- (inl e, st) => (e, st)
- | (inr _, _) => raise Fail
- ("Iflow.evalExp: Selecting "
- ^ "boolean expression")
- in
- ((x, e), st)
- end)
- st es
+ val saved = St.stash ()
in
- (Recd [], St.addInsert (st, (loc, And (St.ambient st,
- Reln (Sql (tab ^ "$New"), [Recd es])))))
+ St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
+ St.insert loc;
+ St.reinstate saved;
+ k (Recd [])
end
| Delete (tab, e) =>
let
- val (st, old) = St.nextVar st
-
- fun rv st =
- let
- val (st, n) = St.nextVar st
- in
- (st, Var n)
- end
-
- val expIn = expIn rv env (fn "T" => Var old
- | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
-
- val (p, st) = case expIn (e, st) of
- (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean"
- | (inr p, st) => (p, st)
-
- val p = And (p,
- And (Reln (Sql "$Old", [Var old]),
- Reln (Sql tab, [Var old])))
-
- val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
+ 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
- (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
+ St.assert [AReln (Sql "$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 (st, new) = St.nextVar st
- val (st, old) = St.nextVar st
-
- fun rv st =
- let
- val (st, n) = St.nextVar st
- in
- (st, Var n)
- end
-
- val expIn = expIn rv env (fn "T" => Var old
- | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
-
- val (fs, st) = ListUtil.foldlMap
- (fn ((x, e), st) =>
- let
- val (e, st) = case expIn (e, st) of
- (inl e, st) => (e, st)
- | (inr _, _) => raise Fail
- ("Iflow.evalExp: Selecting "
- ^ "boolean expression")
- in
- ((x, e), st)
- end)
- st fs
+ 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"
@@ -2333,34 +1829,40 @@ fun evalExp env (e as (_, loc), st) =
else
(f, Proj (Var old, f)) :: fs) fs fs'
- val (p, st) = case expIn (e, st) of
- (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
- | (inr p, st) => (p, st)
-
- val p = And (p,
- And (Reln (Sql (tab ^ "$New"), [Recd fs]),
- And (Reln (Sql "$Old", [Var old]),
- Reln (Sql tab, [Var old]))))
-
- val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
+ val p = case expIn e of
+ inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
+ | inr p => p
+ val saved = St.stash ()
in
- (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
+ St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
+ AReln (Sql "$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 (st, nv) = St.nextVar st
+ val nv = St.nextVar ()
in
- (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv]))))
+ St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
+ k (Var nv)
end
| ENextval _ => default ()
| ESetval _ => default ()
| EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
let
- val (st, nv) = St.nextVar st
+ val nv = St.nextVar ()
in
- (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
+ St.assert [AReln (Known, [Var nv])];
+ k (Var nv)
end
| EUnurlify _ => default ()
@@ -2376,6 +1878,8 @@ fun evalExp env (e as (_, loc), st) =
fun check file =
let
+ val () = St.reset ()
+
val file = MonoReduce.reduce file
val file = MonoOpt.optimize file
val file = Fuse.fuse file
@@ -2388,7 +1892,7 @@ fun check file =
DExport (_, _, n, _, _, _) => IS.add (exptd, n)
| _ => exptd) IS.empty file
- fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
+ fun decl (d, _) =
case d of
DTable (tab, fs, pk, _) =>
let
@@ -2401,11 +1905,10 @@ fun check file =
| _ => []
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));
- (vals, inserts, deletes, updates, client, insert, delete, update))
+ 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
@@ -2413,186 +1916,73 @@ fun check file =
let
val isExptd = IS.member (exptd, n)
- fun deAbs (e, env, nv, p) =
- case #1 e of
- EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
- if isExptd then
- And (p, Reln (Known, [Var nv]))
- else
- p)
- | _ => (e, env, nv, p)
+ val saved = St.stash ()
- val (e, env, nv, p) = deAbs (e, [], 1, True)
+ 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 (_, st) = evalExp env (e, St.create {Var = nv,
- Ambient = p})
+ val (e, env, ps) = deAbs (e, [], [])
in
- (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates,
- client, insert, delete, update)
+ St.assert ps;
+ (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
+ St.reinstate saved
end
| DPolicy pol =>
let
- fun rv rvN = (rvN + 1, Lvar rvN)
- in
- case pol of
- PolClient e =>
+ val rvN = ref 0
+ fun rv () =
let
- val (_, p, _, outs) = queryProp [] 0 rv SomeCol e
+ val n = !rvN
in
- (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
+ 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,
+ UsedExp = fn _ => (),
+ Cont = SomeCol (fn es => k (!atoms, es))}
+ in
+ case pol of
+ PolClient e =>
+ doQ (fn (ats, es) => St.allowSend (ats, es)) e
| PolInsert e =>
- let
- val p = insertProp 0 rv e
- in
- (vals, inserts, deletes, updates, client, p :: insert, delete, update)
- end
+ doQ (fn (ats, _) => St.allowInsert ats) e
| PolDelete e =>
- let
- val p = deleteProp 0 rv e
- in
- (vals, inserts, deletes, updates, client, insert, p :: delete, update)
- end
+ doQ (fn (ats, _) => St.allowDelete ats) e
| PolUpdate e =>
- let
- val p = updateProp 0 rv e
- in
- (vals, inserts, deletes, updates, client, insert, delete, p :: update)
- end
+ doQ (fn (ats, _) => St.allowUpdate ats) e
| PolSequence e =>
(case #1 e of
EPrim (Prim.String seq) =>
let
- val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
+ val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
val outs = [Lvar 0]
in
- (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
+ St.allowSend ([p], outs)
end
- | _ => (vals, inserts, deletes, updates, client, insert, delete, update))
+ | _ => ())
end
- | _ => (vals, inserts, deletes, updates, client, insert, delete, update)
-
- val () = reset ()
-
- val (vals, inserts, deletes, updates, client, insert, delete, update) =
- foldl decl ([], [], [], [], [], [], [], []) file
-
-
- val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
- val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
-
- fun doDml (cmds, pols) =
- app (fn (loc, p) =>
- if decompH p
- (fn hyps =>
- let
- val cc = ccOf hyps
- in
- List.exists (fn p' =>
- if decompG p'
- (fn goals => imply (cc, hyps, goals, NONE)) then
- ((*reset ();
- Print.prefaces "Match" [("hyp", p_prop p),
- ("goal", p_prop p')];*)
- true)
- else
- false)
- pols
- end handle Cc.Contradiction => true) then
- ()
- else
- (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
- Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
+ | _ => ()
in
- app (fn ((loc, e, p), fl) =>
- let
- fun doOne e =
- let
- val p = And (p, Reln (Eq, [Var 0, e]))
- in
- if decompH p
- (fn hyps =>
- let
- val cc = ccOf hyps
-
- fun relevant () =
- let
- val avail = foldl (fn (AReln (Sql tab, _), avail) =>
- SS.add (avail, tab)
- | (_, avail) => avail) SS.empty hyps
-
- val ls = List.filter
- (fn (g1, _) =>
- decompG g1
- (List.all (fn AReln (Sql tab, _) =>
- SS.member (avail, tab)
- | _ => true))) client
- in
- (*print ("Max: " ^ Int.toString (length ls) ^ "\n");*)
- ls
- end
-
- fun tryCombos (maxLv, pols, g, outs) =
- case pols of
- [] =>
- decompG g
- (fn goals => imply (cc, hyps, goals, SOME outs))
- | (g1, outs1) :: pols =>
- let
- val g1 = bumpLvarsP (maxLv + 1) g1
- val outs1 = map (bumpLvars (maxLv + 1)) outs1
- fun skip () = tryCombos (maxLv, pols, g, outs)
- in
- skip ()
- orelse tryCombos (Int.max (maxLv,
- maxLvarP g1),
- pols,
- And (g1, g),
- outs1 @ outs)
- end
- in
- (fl <> Control Where
- andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
- orelse List.exists (fn (p', outs) =>
- decompG p'
- (fn goals => imply (cc, hyps, goals,
- SOME outs)))
- client
- orelse tryCombos (0, relevant (), True, [])
- orelse (reset ();
- Print.preface ("Untenable hypotheses"
- ^ (case fl of
- Control Where => " (WHERE clause)"
- | Control Case => " (case discriminee)"
- | Data => " (returned data value)"),
- Print.p_list p_atom hyps);
- (*Print.preface ("DB", Cc.p_database cc);*)
- false)
- end handle Cc.Contradiction => true) then
- ()
- else
- ErrorMsg.errorAt loc "The information flow policy may be violated here."
- end
-
- fun doAll e =
- case e of
- Const _ => ()
- | Var _ => doOne e
- | Lvar _ => raise Fail "Iflow.doAll: Lvar"
- | Func (UnCon _, [_]) => doOne e
- | Func (_, es) => app doAll es
- | Recd xes => app (doAll o #2) xes
- | Proj _ => doOne e
- | Finish => ()
- in
- doAll e
- end) vals;
-
- doDml (inserts, insert);
- doDml (deletes, delete);
- doDml (updates, update)
+ app decl file
end
val check = fn file =>
diff --git a/tests/policy.ur b/tests/policy.ur
index 69455cd7..fedc3fcb 100644
--- a/tests/policy.ur
+++ b/tests/policy.ur
@@ -9,9 +9,7 @@ table order : { Id : order, Fruit : fruit, Qty : int, Code : int }
CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id)
(* Everyone may knows IDs and names. *)
-policy sendClient (SELECT fruit.Id
- FROM fruit)
-policy sendClient (SELECT fruit.Nam
+policy sendClient (SELECT fruit.Id, fruit.Nam
FROM fruit)
(* The weight is sensitive information; you must know the secret. *)
diff --git a/tests/policy2.ur b/tests/policy2.ur
new file mode 100644
index 00000000..b8480c0c
--- /dev/null
+++ b/tests/policy2.ur
@@ -0,0 +1,22 @@
+type fruit = int
+table fruit : { Id : fruit, Nam : string, Weight : float, Secret : string }
+ PRIMARY KEY Id,
+ CONSTRAINT Nam UNIQUE Nam
+
+(* Everyone may knows IDs and names. *)
+policy sendClient (SELECT fruit.Id, fruit.Nam
+ FROM fruit)
+
+(* The weight is sensitive information; you must know the secret. *)
+policy sendClient (SELECT fruit.Weight, fruit.Secret
+ FROM fruit
+ WHERE known(fruit.Secret))
+
+fun main () =
+ x1 <- queryX (SELECT fruit.Id, fruit.Nam
+ FROM fruit
+ WHERE fruit.Nam = "apple")
+ (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}</li></xml>);
+ return <xml><body>
+ <ul>{x1}</ul>
+ </body></xml>
diff --git a/tests/policy2.urp b/tests/policy2.urp
new file mode 100644
index 00000000..46509756
--- /dev/null
+++ b/tests/policy2.urp
@@ -0,0 +1 @@
+policy2
diff --git a/tests/policy2.urs b/tests/policy2.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/policy2.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 02:38:47 +0000