Module CleanupLabelsproof

From Coq Require Import FSets .
Require Import Coqlib Ordered Integers .
Require Import AST Linking .
Require Import Values Memory Events Globalenvs Smallstep .
Require Import Op Locations Linear .
Require Import CleanupLabels .

Module LabelsetFacts := FSetFacts.Facts (Labelset ).

Definition match_prog (p tp: Linear.program ) :=
match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.

Lemma transf_program_match :
forall p, match_prog p (transf_program p).

Section CLEANUP .

Variables prog tprog : program .
Hypothesis TRANSL : match_prog prog tprog .
Let ge := Genv.globalenv prog .
Let tge := Genv.globalenv tprog .

Lemma symbols_preserved :
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL ).

Lemma senv_preserved :
Senv.equiv ge tge .
Proof (Genv.senv_transf TRANSL ).

Lemma functions_translated :
forall v f,
Genv.find_funct ge v = Some f ->
Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL ).

Lemma function_ptr_translated :
forall v f,
Genv.find_funct_ptr ge v = Some f ->
Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL ).

Lemma sig_function_translated :
forall f,
funsig (transf_fundef f) = funsig f.

Lemma find_function_translated :
forall ros ls f,
find_function ge ros ls = Some f ->
find_function tge ros ls = Some (transf_fundef f).


Definition instr_branches_to (i: instruction ) (lbl: label ) : Prop :=
match i with
| Lgoto lbl' => lbl = lbl'
| Lcond cond args lbl' => lbl = lbl'
| Ljumptable arg tbl => In lbl tbl
| _ => False
end.

Remark add_label_branched_to_incr :
forall ls i, Labelset.Subset ls (add_label_branched_to ls i).

Remark add_label_branched_to_contains :
forall ls i lbl,
instr_branches_to i lbl ->
Labelset.In lbl (add_label_branched_to ls i).

Lemma labels_branched_to_correct :
forall c i lbl,
In i c -> instr_branches_to i lbl -> Labelset.In lbl (labels_branched_to c).


Lemma remove_unused_labels_cons :
forall bto i c,
remove_unused_labels bto (i :: c) =
match i with
| Llabel lbl =>
if Labelset.mem lbl bto then i :: remove_unused_labels bto c else remove_unused_labels bto c
| _ =>
i :: remove_unused_labels bto c
end.


Lemma find_label_commut :
forall lbl bto,
Labelset.In lbl bto ->
forall c c',
find_label lbl c = Some c' ->
find_label lbl (remove_unused_labels bto c) = Some (remove_unused_labels bto c').

Corollary find_label_translated :
forall f i c' lbl c,
incl (i :: c') (fn_code f) ->
find_label lbl (fn_code f) = Some c ->
instr_branches_to i lbl ->
find_label lbl (fn_code (transf_function f)) =
Some (remove_unused_labels (labels_branched_to (fn_code f)) c).

Lemma find_label_incl :
forall lbl c c', find_label lbl c = Some c' -> incl c' c.


Inductive match_stackframes : stackframe -> stackframe -> Prop :=
| match_stackframe_intro :
forall f sp ls c,
incl c f.(fn_code ) ->
match_stackframes
(Stackframe f sp ls c)
(Stackframe (transf_function f) sp ls
(remove_unused_labels (labels_branched_to f.(fn_code )) c)).

Inductive match_states : state -> state -> Prop :=
| match_states_intro :
forall s f sp c ls m ts
(STACKS: list_forall2 match_stackframes s ts)
(INCL: incl c f.(fn_code )),
match_states (State s f sp c ls m)
(State ts (transf_function f) sp (remove_unused_labels (labels_branched_to f.(fn_code )) c) ls m)
| match_states_call :
forall s f ls m ts,
list_forall2 match_stackframes s ts ->
match_states (Callstate s f ls m)
(Callstate ts (transf_fundef f) ls m)
| match_states_return :
forall s ls m ts,
list_forall2 match_stackframes s ts ->
match_states (Returnstate s ls m)
(Returnstate ts ls m).

Definition measure (st: state ) : nat :=
match st with
| State s f sp c ls m => List.length c
| _ => O
end.

Lemma match_parent_locset :
forall s ts,
list_forall2 match_stackframes s ts ->
parent_locset ts = parent_locset s.

Theorem transf_step_correct :
forall s1 t s2, step ge s1 t s2 ->
forall s1' (MS: match_states s1 s1'),
(exists s2', step tge s1' t s2' /\ match_states s2 s2')
\/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.

Lemma transf_initial_states :
forall st1, initial_state prog st1 ->
exists st2, initial_state tprog st2 /\ match_states st1 st2.

Lemma transf_final_states :
forall st1 st2 r,
match_states st1 st2 -> final_state st1 r -> final_state st2 r.

Theorem transf_program_correct :
forward_simulation (Linear.semantics prog ) (Linear.semantics tprog ).

End CLEANUP .

---

Generated by coq2html