summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/iflow.sml110
1 files changed, 102 insertions, 8 deletions
diff --git a/src/iflow.sml b/src/iflow.sml
index dffb0875..3ff3d100 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -310,6 +310,66 @@ fun varInP lv =
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)
@@ -2390,16 +2450,50 @@ fun check file =
in
if decompH p
(fn hyps =>
- (fl <> Control Where
- andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
- orelse List.exists (fn (p', outs) =>
- decompG p'
- (fn goals => imply (hyps, goals, SOME outs)))
- client) then
+ let
+ val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab)
+ | (_, avail) => avail) SS.empty hyps
+
+ fun tryCombos (maxLv, pols, g, outs) =
+ case pols of
+ [] =>
+ decompG g
+ (fn goals => imply (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
+ if decompG g1
+ (List.all (fn AReln (Sql tab, _) =>
+ SS.member (avail, tab)
+ | _ => true)) then
+ skip ()
+ orelse tryCombos (Int.max (maxLv,
+ maxLvarP g1),
+ pols,
+ And (g1, g),
+ outs1 @ outs)
+ else
+ skip ()
+ end
+ in
+ (fl <> Control Where
+ andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
+ orelse List.exists (fn (p', outs) =>
+ decompG p'
+ (fn goals => imply (hyps, goals, SOME outs)))
+ client
+ orelse tryCombos (0, client, True, [])
+ orelse (reset ();
+ Print.preface ("Untenable hypotheses",
+ Print.p_list p_atom hyps);
+ false)
+ end) then
()
else
- (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
- Print.preface ("The state satisifies this predicate:", p_prop p))
+ ErrorMsg.errorAt loc "The information flow policy may be violated here."
end
fun doAll e =