Lvc.UnreachableCode
Require Import AllInRel List Map Env DecSolve.
Require Import IL Annotation AutoIndTac Exp SetOperations.
Require Export Filter LabelsDefined OUnion.
Set Implicit Arguments.
Local Hint Resolve incl_empty minus_incl incl_right incl_left.
Require Import IL Annotation AutoIndTac Exp SetOperations.
Require Export Filter LabelsDefined OUnion.
Set Implicit Arguments.
Local Hint Resolve incl_empty minus_incl incl_right incl_left.
Rechability Specification
The reachability predicate is parameterized by a value of type sc, which indicates whether soundness, completeness, or both are desired.Inductive sc := Sound | Complete | SoundAndComplete.
Definition isComplete (s:sc) :=
match s with
| SoundAndComplete => true
| Complete => true
| _ => false
end.
Definition isSound (s:sc) :=
match s with
| SoundAndComplete => true
| Sound => true
| _ => false
end.
Depending on whether soundness, completeness or both are desiered,
the relation uceq is instantiated differently.
Definition uceq (i:sc) (a b:bool) :=
match i with
| Sound => impb a b
| Complete => impb b a
| SoundAndComplete => a = b
end.
Hint Extern 0 (uceq _ _ _) => simpl.
Lemma uceq_refl i a
: uceq i a a.
Proof.
destruct i; simpl; eauto.
Qed.
Lemma eq_uceq i (a b:bool)
: a = b -> uceq i a b.
Proof.
intros; subst. eauto using uceq_refl.
Qed.
Lemma eq_uceq_sym i (a b:bool)
: b = a -> uceq i a b.
Proof.
intros; subst. eauto using uceq_refl.
Qed.
Hint Resolve uceq_refl eq_uceq eq_uceq_sym.
Inductive unreachable_code (i:sc)
: list bool -> stmt -> ann bool -> Prop :=
| UCPOpr BL x s b e al
: unreachable_code i BL s al
-> uceq i b (getAnn al)
-> unreachable_code i BL (stmtLet x e s) (ann1 b al)
| UCPIf BL e b1 b2 b al1 al2
: (op2bool e <> Some false -> uceq i b (getAnn al1))
-> (op2bool e <> Some true -> uceq i b (getAnn al2))
-> unreachable_code i BL b1 al1
-> unreachable_code i BL b2 al2
-> (if isComplete i then op2bool e = ⎣ false ⎦ -> getAnn al1 = false else True)
-> (if isComplete i then op2bool e = ⎣ true ⎦ -> getAnn al2 = false else True)
-> unreachable_code i BL (stmtIf e b1 b2) (ann2 b al1 al2)
| UCPGoto BL l Y b a
: get BL (counted l) b
-> (if isSound i then impb a b else True)
-> unreachable_code i BL (stmtApp l Y) (ann0 a)
| UCReturn BL e b
: unreachable_code i BL (stmtReturn e) (ann0 b)
| UCLet BL F t b als alt
: unreachable_code i (getAnn ⊝ als ++ BL) t alt
-> length F = length als
-> uceq i b (getAnn alt)
-> (forall n Zs a, get F n Zs ->
get als n a ->
unreachable_code i (getAnn ⊝ als ++ BL) (snd Zs) a)
-> (if isComplete i then (forall n a,
get als n a ->
getAnn a ->
isCalledFrom trueIsCalled F t (LabI n)) else True)
-> (if isComplete i then forall n a, get als n a -> impb (getAnn a) b else True)
-> unreachable_code i BL (stmtFun F t) (annF b als alt).
Local Hint Extern 0 =>
match goal with
| [ H : op2bool ?e <> Some ?t , H' : op2bool ?e <> Some ?t -> _ |- _ ] =>
specialize (H' H); subst
end.
Lemma unreachable_code_SC_S Lv s slv
: unreachable_code SoundAndComplete Lv s slv
-> unreachable_code Sound Lv s slv.
Proof.
intros UC.
general induction UC; simpl in *; subst; eauto 20 using unreachable_code, uceq_refl.
- econstructor; simpl; eauto using uceq_refl.
- econstructor; simpl; eauto using uceq_refl.
Qed.
Hint Resolve unreachable_code_SC_S.
Lemma ucc_sound_and_complete BL s a
: unreachable_code Complete BL s a
-> unreachable_code Sound BL s a
-> unreachable_code SoundAndComplete BL s a.
Proof.
intros UCC UCS.
general induction UCS; inv UCC; simpl in *; eauto 20 using unreachable_code, impb_eq.
Qed.
Lemma unreachable_code_trueIsCalled Lv s slv l
: unreachable_code Sound Lv s slv
-> trueIsCalled s l
-> exists b, get Lv (counted l) b /\ impb (getAnn slv) b.
Proof.
destruct l; simpl.
revert Lv slv n.
sind s; destruct s; intros Lv slv n UC IC; inv UC; inv IC;
simpl in *; subst; simpl in *; eauto 20.
- edestruct (IH s); dcr; eauto.
- edestruct (IH s1); dcr; eauto.
- edestruct (IH s2); dcr; eauto.
- destruct l'.
exploit (IH s); eauto; dcr.
setoid_rewrite H3. setoid_rewrite H10.
clear H3 H10 UC H9 H1 alt.
general induction H5.
+ inv_get. eexists; split; eauto.
+ inv_get.
exploit H4; eauto.
eapply IH in H3; eauto.
dcr. inv_get.
edestruct IHcallChain; try eapply H8; eauto; dcr.
eexists x1; split; eauto.
Qed.