From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Velus Require Import Common.
From Velus Require Import CommonTyping.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import VelusMemory.
From Velus Require Import Obc.ObcSyntax.
From Velus Require Import Obc.ObcSemantics.
From Velus Require Import Obc.ObcInvariants.
From Velus Require Import Obc.ObcTyping.
Module Type OBCDEADCODE
(
Import Ids :
IDS)
(
Import Op :
OPERATORS)
(
Import OpAux :
OPERATORS_AUX Ids Op)
(
Import SynObc:
OBCSYNTAX Ids Op OpAux)
(
Import ComTyp:
COMMONTYPING Ids Op OpAux)
(
Import SemObc:
OBCSEMANTICS Ids Op OpAux SynObc)
(
Import InvObc:
OBCINVARIANTS Ids Op OpAux SynObc SemObc)
(
Import TypObc:
OBCTYPING Ids Op OpAux SynObc ComTyp SemObc).
Dead Updates Elimination
Remove instruction of the form state.x = state.x
Fixpoint deadcode_stmt (
s:
stmt):
stmt :=
match s with
|
AssignSt x (
State y _ _)
_ =>
if x ==
b y then Skip else s
|
Switch e ss sd =>
Switch e (
map (
option_map deadcode_stmt)
ss) (
deadcode_stmt sd)
|
Comp s1 s2 =>
Comp (
deadcode_stmt s1) (
deadcode_stmt s2)
|
_ =>
s
end.
Definition deadcode_method (
m:
method):
method :=
mk_method (
m_name m) (
m_in m) (
m_vars m) (
m_out m)
(
deadcode_stmt (
m_body m))
(
m_nodupvars m) (
m_good m).
Lemma map_m_name_deadcode_methods:
forall methods,
map m_name (
map deadcode_method methods) =
map m_name methods.
Proof.
Program Definition deadcode_class (
c:
class):
class :=
mk_class (
c_name c) (
c_mems c) (
c_objs c)
(
map deadcode_method (
c_methods c))
(
c_nodup c)
_ (
c_good c).
Next Obligation.
Global Program Instance deadcode_class_transform_unit:
TransformUnit class class :=
{
transform_unit :=
deadcode_class }.
Global Program Instance deadcode_class_transform_state_unit:
TransformStateUnit class class.
Definition deadcode_program :
program ->
program :=
transform_units.
Lemma deadcode_find_class:
forall p id c p',
find_class id p =
Some (
c,
p') ->
find_class id (
deadcode_program p) =
Some (
deadcode_class c,
deadcode_program p').
Proof.
Lemma deadcode_find_method:
forall f fm cls,
find_method f cls.(
c_methods) =
Some fm ->
find_method f (
deadcode_class cls).(
c_methods) =
Some (
deadcode_method fm).
Proof.
destruct cls;
simpl.
induction c_methods0 as [|
m ms];
inversion 1.
simpl.
destruct (
ident_eq_dec m.(
m_name)
f)
as [
He|
Hne].
-
rewrite He,
ident_eqb_refl in *.
now injection H1;
intro;
subst.
-
apply ident_eqb_neq in Hne.
rewrite Hne in *.
inv c_nodupm0;
auto.
Qed.
Lemma deadcode_find_method':
forall id c m,
find_method id (
deadcode_class c).(
c_methods) =
Some m ->
exists m',
m =
deadcode_method m'
/\
find_method id c.(
c_methods) =
Some m'.
Proof.
intros *
Find.
destruct c as [? ? ?
meths ?
Nodup];
simpl in *.
induction meths as [|
m'];
simpl in *;
try discriminate.
inv Nodup;
auto.
destruct (
ident_eqb (
m_name m')
id);
auto.
inv Find.
exists m';
auto.
Qed.
Semantic preservation
Lemma deadcode_stmt_eval prog :
forall s menv env menv'
env',
stmt_eval prog menv env s (
menv',
env') ->
stmt_eval prog menv env (
deadcode_stmt s) (
menv',
env').
Proof.
induction s using stmt_ind2';
intros *
Sem;
simpl;
auto.
-
cases_eqn Eq;
auto.
rewrite equiv_decb_equiv in Eq0.
inv Eq0.
inv Sem.
take (
exp_eval _ _ _ _)
and inv it.
unfold add_val.
destruct menv0.
rewrite Env.gsident;
auto.
constructor.
-
inv Sem.
econstructor;
eauto.
+
take (
nth_error _ _ =
_)
and rewrite nth_error_map,
it;
simpl;
eauto.
+
take (
nth_error _ _ =
_)
and apply nth_error_In in it.
simpl_Forall.
destruct s0;
simpl in *;
eauto.
-
inv Sem.
econstructor;
eauto.
Qed.
Lemma deadcode_call:
forall p n me me'
f xss rs,
stmt_call_eval p me n f xss me'
rs ->
stmt_call_eval (
deadcode_program p)
me n f xss me'
rs.
Proof.
Corollary deadcode_loop_call:
forall f c ins outs prog me,
loop_call prog c f ins outs 0
me ->
loop_call (
deadcode_program prog)
c f ins outs 0
me.
Proof.
intros ?????;
generalize 0%
nat.
cofix COINDHYP.
intros n me Hdo.
destruct Hdo.
econstructor;
eauto using deadcode_call.
Qed.
Typing preservation
Lemma wt_exp_deadcode:
forall p Γ
m Γ
v e,
wt_exp p Γ
m Γ
v e ->
wt_exp (
deadcode_program p) Γ
m Γ
v e.
Proof.
induction e;
inversion_clear 1;
eauto using wt_exp.
Qed.
Lemma deadcode_stmt_wt:
forall p insts Γ
m Γ
v s,
wt_stmt p insts Γ
m Γ
v s ->
wt_stmt (
deadcode_program p)
insts Γ
m Γ
v (
deadcode_stmt s).
Proof.
Lemma deadcode_program_wt:
forall p,
wt_program p ->
wt_program (
deadcode_program p).
Proof.
Lemma deadcode_program_wt_memory:
forall me p c,
wt_memory me p c.(
c_mems)
c.(
c_objs) ->
wt_memory me (
deadcode_program p) (
deadcode_class c).(
c_mems) (
deadcode_class c).(
c_objs).
Proof.
intros * WT.
pose proof transform_units_wt_memory' as Spec; simpl in Spec.
apply Spec in WT; auto.
Qed.
Preservation of Can_write_in.
Lemma deadcode_stmt_Can_write_in_var:
forall s x,
Can_write_in_var x s <->
Can_write_in_var x (
deadcode_stmt s).
Proof.
induction s using stmt_ind2';
simpl;
try reflexivity;
intros.
-
cases;
try reflexivity.
split;
intros CwI;
inv CwI.
-
rewrite ?
Can_write_in_var_Switch.
split;
intros Ex;
solve_Exists;
simpl_Forall.
1,2:
take (
option _)
and destruct it; [
apply H|
apply IHs];
auto.
-
rewrite ?
Can_write_in_var_Comp,
IHs1,
IHs2.
reflexivity.
Qed.
Lemma deadcode_program_cannot_write_inputs:
forall p,
Forall_methods (
fun m =>
Forall (
fun x => ~
Can_write_in_var x (
m_body m)) (
map fst (
m_in m)))
p ->
Forall_methods (
fun m =>
Forall (
fun x => ~
Can_write_in_var x (
m_body m)) (
map fst (
m_in m)))
(
deadcode_program p).
Proof.
Preservation of No_Overwrites
Lemma deadcode_stmt_No_Overwrites:
forall s,
No_Overwrites s ->
No_Overwrites (
deadcode_stmt s).
Proof.
induction s using stmt_ind2';
intros *
NO;
auto;
simpl;
inv NO.
-
cases;
constructor.
-
constructor.
simpl_Forall.
take (
option _)
and destruct it;
auto.
-
constructor;
auto.
1,2:
intros *;
rewrite <- ?
deadcode_stmt_Can_write_in_var;
auto.
Qed.
Lemma deadcode_program_No_Overwrites:
forall p,
Forall_methods (
fun m =>
No_Overwrites (
m_body m))
p ->
Forall_methods (
fun m =>
No_Overwrites (
m_body m)) (
deadcode_program p).
Proof.
End OBCDEADCODE.
Module ObcDeadCodeFun
(
Ids :
IDS)
(
Op :
OPERATORS)
(
OpAux :
OPERATORS_AUX Ids Op)
(
SynObc:
OBCSYNTAX Ids Op OpAux)
(
ComTyp:
COMMONTYPING Ids Op OpAux)
(
SemObc:
OBCSEMANTICS Ids Op OpAux SynObc)
(
InvObc:
OBCINVARIANTS Ids Op OpAux SynObc SemObc)
(
TypObc:
OBCTYPING Ids Op OpAux SynObc ComTyp SemObc)
<:
OBCDEADCODE Ids Op OpAux SynObc ComTyp SemObc InvObc TypObc .
Include OBCDEADCODE Ids Op OpAux SynObc ComTyp SemObc InvObc TypObc .
End ObcDeadCodeFun.