Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1208:b5a4c5407ae0

Checking known() correctly, according to a pair of examples

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 06 Apr 2010 10:39:15 -0400
parents	ae3036773768
children	775357041e48

comparison

equal deleted inserted replaced

-:ae3036773768
+:b5a4c5407ae0
 fun isFinish e =
 case e of
 Finish => true
 | _ => false
+val unif = ref (IM.empty : exp IM.map)
+fun reset () = unif := IM.empty
+fun save () = !unif
+fun restore x = unif := x
 fun simplify e =
 case e of
 Const _ => e
 | Var _ => e
-| Lvar _ => e
+| Lvar n =>
+(case IM.find (!unif, n) of
+NONE => e
+| SOME e => simplify e)
 | Func (f, es) =>
 let
 val es = map simplify es
 in
 if List.exists isFinish es then
 | Select _ => k []
 in
 decomp
 end
-val unif = ref (IM.empty : exp IM.map)
-fun reset () = unif := IM.empty
-fun save () = !unif
-fun restore x = unif := x
 fun lvarIn lv =
 let
 fun lvi e =
 case e of
 Const _ => false
 case e2 of
 Lvar n2 =>
 (case IM.find (!unif, n2) of
 SOME e2 => eq' (e1, e2)
 | NONE => n1 = n2
-orelse (unif := IM.insert (!unif, n1, e2);
+orelse (unif := IM.insert (!unif, n2, e1);
 true))
 | _ =>
 if lvarIn n1 e2 then
 false
 else
 false)
 end
 exception Imply of prop * prop
-fun rimp ((r1, es1), (r2, es2)) =
+val debug = ref false
+(* Congruence closure *)
+structure Cc :> sig
+type t
+val empty : t
+val assert : t * exp * exp -> t
+val query : t * exp * exp -> bool
+val allPeers : t * exp -> exp list
+end = struct
+fun eq' (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 eq' (es1, es2)
+| (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
+List.all (fn (x2, e2) =>
+List.exists (fn (x1, e1) => x1 = x2 andalso eq' (e1, e2)) xes2) xes1
+| (Proj (e1, x1), Proj (e2, x2)) => eq' (e1, e2) andalso x1 = x2
+| (Finish, Finish) => true
+| _ => false
+fun eq (e1, e2) = eq' (simplify e1, simplify e2)
+type t = (exp * exp) list
+val empty = []
+fun lookup (t, e) =
+case List.find (fn (e', _) => eq (e', e)) t of
+NONE => e
+| SOME (_, e2) => lookup (t, e2)
+fun assert (t, e1, e2) =
+let
+val r1 = lookup (t, e1)
+val r2 = lookup (t, e2)
+in
+if eq (r1, r2) then
+t
+else
+(r1, r2) :: t
+end
+open Print
+fun query (t, e1, e2) =
+(if !debug then
+prefaces "CC query" [("e1", p_exp (simplify e1)),
+("e2", p_exp (simplify e2)),
+("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
+space,
+PD.string "->",
+space,
+p_exp (simplify e2)]) t)]
+else
+();
+eq (lookup (t, e1), lookup (t, e2)))
+fun allPeers (t, e) =
+let
+val r = lookup (t, e)
+in
+r :: List.mapPartial (fn (e1, e2) =>
+let
+val r' = lookup (t, e2)
+in
+if eq (r, r') then
+SOME e1
+else
+NONE
+end) t
+end
+end
+fun rimp cc ((r1, es1), (r2, es2)) =
 case (r1, r2) of
 (Sql r1', Sql r2') =>
 r1' = r2' andalso
 (case (es1, es2) of
 ([Recd xes1], [Recd xes2]) =>
 in
 if eq (x1, x2) andalso eq (y1, y2) then
 true
 else
 (restore saved;
-(*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
+if eq (x1, y2) andalso eq (y1, x2) then
-eq (x1, y2) andalso eq (y1, x2))
+true
+else
+(restore saved;
+false))
 end
 | _ => false)
 | (Known, Known) =>
 (case (es1, es2) of
-([e1], [e2]) =>
+([Var v], [e2]) =>
 let
-fun walk e2 =
+fun matches e =
-eq (e1, e2) orelse
+case e of
-case e2 of
+Var v' => v' = v
-Proj (e2, _) => walk e2
+| Proj (e, _) => matches e
 | _ => false
 in
-walk e2
+List.exists matches (Cc.allPeers (cc, e2))
 end
 | _ => false)
 | _ => false
 fun imply (p1, p2) =
-(reset ();
+let
-(*raise (Imply (p1, p2));*)
+fun doOne doKnown =
 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
 (fn hyps =>
 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
 (fn goals =>
 let
-fun gls goals onFail =
+val cc = foldl (fn (p, cc) =>
-case goals of
+case p of
-[] => true
+(Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
-| g :: goals =>
+| _ => cc) Cc.empty hyps
-let
-fun hps hyps =
+fun gls goals onFail =
-case hyps of
+case goals of
-[] => onFail ()
+[] => true
-| h :: hyps =>
+| g :: goals =>
-let
+case (doKnown, g) of
-val saved = save ()
+(false, (Known, _)) => gls goals onFail
-in
+| _ =>
-if rimp (h, g) then
+let
-let
+fun hps hyps =
-val changed = IM.numItems (!unif) <> IM.numItems saved
+case hyps of
-in
+[] => onFail ()
-gls goals (fn () => (restore saved;
+| h :: hyps =>
-changed andalso hps hyps))
+let
-end
+val saved = save ()
-else
+in
-hps hyps
+if rimp cc (h, g) then
-end
+let
-in
+val changed = IM.numItems (!unif)
-hps hyps
+<> IM.numItems saved
-end
+in
-in
+gls goals (fn () => (restore saved;
-gls goals (fn () => false)
+changed andalso hps hyps))
-end)))
+end
+else
+hps hyps
+end
+in
+(case g of
+(Eq, [e1, e2]) => Cc.query (cc, e1, e2)
+| _ => false)
+orelse hps hyps
+end
+in
+gls goals (fn () => false)
+end))
+in
+reset ();
+doOne false;
+doOne true
+end
 fun patCon pc =
 case pc of
 PConVar n => "C" ^ Int.toString n
 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
 end
 | _ => NONE
 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
-val debug = ref false
 fun log name p chs =
 (if !debug then
 case chs of
 String s :: _ => print (name ^ ": " ^ s ^ "\n")
 in
 app (fn (loc, e, p) =>
 let
 val p = And (p, Reln (Eq, [Var 0, e]))
 in
-if List.exists (fn pol => imply (p, pol)) pols then
+if List.exists (fn pol => if imply (p, pol) then
+(if !debug then
+Print.prefaces "Match"
+[("Hyp", p_prop p),
+("Goal", p_prop pol)]
+else
+();
+true)
+else
+false) pols then
 ()
 else
 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
 Print.preface ("The state satisifes this predicate:", p_prop p))
 end) vals

Mercurial > urweb

comparison src/iflow.sml @ 1208:b5a4c5407ae0