summaryrefslogtreecommitdiff
path: root/backend/Allocproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Allocproof.v')
-rw-r--r--backend/Allocproof.v295
1 files changed, 99 insertions, 196 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 051be1e..fd569ad 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -37,6 +37,7 @@ Require Import Allocation.
(** * Semantic properties of calling conventions *)
+(*************
(** The value of a parameter in the called function is the same
as the value of the corresponding argument in the caller function. *)
@@ -118,6 +119,7 @@ Proof.
symmetry. apply Locmap.gso. eapply Loc.in_notin_diff; eauto.
intros x [A B]. rewrite Locmap.gso; auto. apply Loc.diff_sym; auto.
Qed.
+****************)
(** * Properties of allocated locations *)
@@ -220,7 +222,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign.
of [assign r] can be arbitrary. *)
Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop :=
- forall (r: reg), Regset.In r live -> Val.lessdef (rs#r) (ls (assign r)).
+ forall (r: reg), Regset.In r live -> rs#r = ls (assign r).
(** What follows is a long list of lemmas expressing properties
of the [agree_live_regs] predicate that are useful for the
@@ -289,7 +291,7 @@ Qed.
Lemma agree_eval_reg:
forall r live rs ls,
- agree (reg_live r live) rs ls -> Val.lessdef (rs#r) (ls (assign r)).
+ agree (reg_live r live) rs ls -> rs#r = ls (assign r).
Proof.
intros. apply H. apply Regset.add_1. auto.
Qed.
@@ -299,11 +301,11 @@ Qed.
Lemma agree_eval_regs:
forall rl live rs ls,
agree (reg_list_live rl live) rs ls ->
- Val.lessdef_list (rs##rl) (List.map ls (List.map assign rl)).
+ rs##rl = List.map ls (List.map assign rl).
Proof.
induction rl; simpl; intros.
- constructor.
- constructor.
+ auto.
+ f_equal.
apply agree_eval_reg with live.
apply agree_reg_list_live with rl. auto.
eapply IHrl. eexact H.
@@ -345,17 +347,16 @@ Qed.
are mapped to locations other than that of [r]. *)
Lemma agree_assign_live:
- forall live r rs ls v v',
+ forall live r rs ls v,
(forall s,
Regset.In s live -> s <> r -> assign s <> assign r) ->
- Val.lessdef v v' ->
agree (reg_dead r live) rs ls ->
- agree live (rs#r <- v) (Locmap.set (assign r) v' ls).
+ agree live (rs#r <- v) (Locmap.set (assign r) v ls).
Proof.
unfold agree; intros. rewrite Regmap.gsspec.
destruct (peq r0 r).
subst r0. rewrite Locmap.gss. auto.
- rewrite Locmap.gso. apply H1. apply Regset.remove_2; auto.
+ rewrite Locmap.gso. apply H0. apply Regset.remove_2; auto.
eapply regalloc_noteq_diff. eauto. apply sym_not_equal. apply H. auto. auto.
Qed.
@@ -414,66 +415,70 @@ Qed.
a function call, provided that the states before the call agree
and that calling conventions are respected. *)
-Lemma agree_call:
- forall live args ros res rs v (ls ls': locset),
+Lemma agree_postcall:
+ forall live args ros res rs v (ls: locset),
(forall r,
Regset.In r live -> r <> res ->
~(In (assign r) Conventions.destroyed_at_call)) ->
(forall r,
Regset.In r live -> r <> res -> assign r <> assign res) ->
- Val.lessdef v (ls' (assign res)) ->
- (forall l,
- Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) ->
- ls' l = ls l) ->
agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls ->
- agree live (rs#res <- v) ls'.
+ agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)).
Proof.
intros.
assert (agree (reg_dead res live) rs ls).
apply agree_reg_sum_live with ros.
apply agree_reg_list_live with args. assumption.
- red; intros.
- case (Reg.eq r res); intro.
- subst r. rewrite Regmap.gss. assumption.
- rewrite Regmap.gso; auto. rewrite H2. apply H4.
- apply Regset.remove_2; auto.
- eapply regalloc_notin_notin; eauto.
- eapply regalloc_acceptable; eauto.
- eapply regalloc_noteq_diff; eauto.
+ red; intros. rewrite Regmap.gsspec. destruct (peq r res).
+ subst r. rewrite Locmap.gss. auto.
+ rewrite Locmap.gso. transitivity (ls (assign r)).
+ apply H2. apply Regset.remove_2; auto.
+ unfold postcall_regs.
+ assert (~In (assign r) temporaries).
+ apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto.
+ assert (~In (assign r) destroyed_at_call).
+ apply H. auto. auto.
+ caseEq (assign r); auto. intros m ASG. rewrite <- ASG.
+ destruct (In_dec Loc.eq (assign r) temporaries). contradiction.
+ destruct (In_dec Loc.eq (assign r) destroyed_at_call). contradiction.
+ auto.
+ eapply regalloc_noteq_diff; eauto. apply sym_not_eq. auto.
Qed.
(** Agreement between the initial register set at RTL function entry
and the location set at LTL function entry. *)
Lemma agree_init_regs:
- forall rl vl ls live,
+ forall live rl vl,
(forall r1 r2,
In r1 rl -> Regset.In r2 live -> r1 <> r2 ->
assign r1 <> assign r2) ->
- Val.lessdef_list vl (List.map ls (List.map assign rl)) ->
- agree live (init_regs vl rl) ls.
+ agree live (RTL.init_regs vl rl)
+ (LTL.init_locs vl (List.map assign rl)).
Proof.
+ intro live.
+ assert (agree live (Regmap.init Vundef) (Locmap.init Vundef)).
+ red; intros. rewrite Regmap.gi. auto.
induction rl; simpl; intros.
- red; intros. rewrite Regmap.gi. auto.
- inv H0.
- assert (agree live (init_regs vl1 rl) ls).
- apply IHrl. intros. apply H. tauto. auto. auto. auto.
- red; intros. case (Reg.eq a r); intro.
- subst r. rewrite Regmap.gss. auto.
- rewrite Regmap.gso; auto.
+ auto.
+ destruct vl. auto.
+ assert (agree live (init_regs vl rl) (init_locs vl (map assign rl))).
+ apply IHrl. intros. apply H0. tauto. auto. auto.
+ red; intros. rewrite Regmap.gsspec. destruct (peq r a).
+ subst r. rewrite Locmap.gss. auto.
+ rewrite Locmap.gso. apply H1; auto.
+ eapply regalloc_noteq_diff; eauto.
Qed.
Lemma agree_parameters:
- forall vl ls,
+ forall vl,
let params := f.(RTL.fn_params) in
- Val.lessdef_list vl (List.map ls (List.map assign params)) ->
agree (live0 f flive)
- (init_regs vl params)
- ls.
+ (RTL.init_regs vl params)
+ (LTL.init_locs vl (List.map assign params)).
Proof.
intros. apply agree_init_regs.
intros. eapply regalloc_correct_3; eauto.
- auto.
Qed.
End AGREE.
@@ -556,52 +561,40 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop
| match_stackframes_nil:
match_stackframes nil nil
| match_stackframes_cons:
- forall s ts sig res f sp pc rs ls env live assign,
+ forall s ts res f sp pc rs ls env live assign,
match_stackframes s ts ->
- sig_res (RTL.fn_sig f) = sig_res (parent_callsig ts) ->
wt_function f env ->
analyze f = Some live ->
regalloc f live (live0 f live) env = Some assign ->
- (forall rv ls1,
- (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls1 l = ls l) ->
- Val.lessdef rv (ls1 (R (loc_result sig))) ->
+ (forall rv,
agree assign (transfer f pc live!!pc)
(rs#res <- rv)
- (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) ->
+ (Locmap.set (assign res) rv ls)) ->
match_stackframes
(RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s)
- (LTL.Stackframe sig (assign res) (transf_fun f live assign) sp ls pc :: ts).
+ (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts).
Inductive match_states: RTL.state -> LTL.state -> Prop :=
| match_states_intro:
- forall s f sp pc rs m ts ls tm live assign env
+ forall s f sp pc rs m ts ls live assign env
(STACKS: match_stackframes s ts)
- (SIG: sig_res(RTL.fn_sig f) = sig_res(parent_callsig ts))
(WT: wt_function f env)
(ANL: analyze f = Some live)
(ASG: regalloc f live (live0 f live) env = Some assign)
- (AG: agree assign (transfer f pc live!!pc) rs ls)
- (MMD: Mem.lessdef m tm),
+ (AG: agree assign (transfer f pc live!!pc) rs ls),
match_states (RTL.State s (RTL.fn_code f) sp pc rs m)
- (LTL.State ts (transf_fun f live assign) sp pc ls tm)
+ (LTL.State ts (transf_fun f live assign) sp pc ls m)
| match_states_call:
- forall s f args m ts tf ls tm,
+ forall s f args m ts tf,
match_stackframes s ts ->
- sig_res(RTL.funsig f) = sig_res(parent_callsig ts) ->
transf_fundef f = OK tf ->
- Val.lessdef_list args (List.map ls (loc_arguments (funsig tf))) ->
- Mem.lessdef m tm ->
- (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
match_states (RTL.Callstate s f args m)
- (LTL.Callstate ts tf ls tm)
+ (LTL.Callstate ts tf args m)
| match_states_return:
- forall s v m ts ls tm,
+ forall s v m ts,
match_stackframes s ts ->
- Val.lessdef v (ls (R (loc_result (parent_callsig ts)))) ->
- Mem.lessdef m tm ->
- (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
match_states (RTL.Returnstate s v m)
- (LTL.Returnstate ts ls tm).
+ (LTL.Returnstate ts v m).
(** The simulation proof is by case analysis over the RTL transition
taken in the source program. *)
@@ -652,10 +645,9 @@ Lemma transl_find_function:
transf_fundef f = OK tf.
Proof.
intros; destruct ros; simpl in *.
- assert (Val.lessdef (rs#r) (ls (alloc r))).
+ assert (rs#r = ls (alloc r)).
eapply agree_eval_reg. eapply agree_reg_list_live; eauto.
- inv H1. apply functions_translated. auto.
- exploit Genv.find_funct_inv; eauto. intros [b EQ]. congruence.
+ rewrite <- H1. apply functions_translated. auto.
rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
apply function_ptr_translated. auto. discriminate.
Qed.
@@ -696,15 +688,11 @@ Proof.
rewrite <- H1. eapply agree_move_live; eauto.
(* Not a move *)
intros INMO CORR CODE.
- assert (exists v1,
- eval_operation tge sp op (map ls (map assign args)) tm = Some v1
- /\ Val.lessdef v v1).
- apply eval_operation_lessdef with m (rs##args); auto.
+ assert (eval_operation tge sp op (map ls (map assign args)) m = Some v).
+ replace (map ls (map assign args)) with (rs##args).
+ rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
eapply agree_eval_regs; eauto.
- rewrite (eval_operation_preserved symbols_preserved). assumption.
- destruct H1 as [v1 [EV VMD]].
- econstructor; split. eapply exec_Lop; eauto.
- MatchStates.
+ econstructor; split. eapply exec_Lop; eauto. MatchStates.
apply agree_assign_live with f env live; auto.
eapply agree_reg_list_live; eauto.
(* Result is not live, instruction turned into a nop *)
@@ -717,15 +705,10 @@ Proof.
rewrite LV in AG.
(* dst is live *)
exploit Regset.mem_2; eauto. intro LV'.
- assert (exists a',
- eval_addressing tge sp addr (map ls (map assign args)) = Some a'
- /\ Val.lessdef a a').
- apply eval_addressing_lessdef with (rs##args).
- eapply agree_eval_regs; eauto.
+ assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a).
+ replace (map ls (map assign args)) with (rs##args).
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
- destruct H2 as [a' [EVAL VMD]].
- exploit Mem.loadv_lessdef; eauto.
- intros [v' [LOADV VMD2]].
+ eapply agree_eval_regs; eauto.
econstructor; split.
eapply exec_Lload; eauto. TranslInstr. rewrite LV; auto.
generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
@@ -740,106 +723,61 @@ Proof.
red; intro; exploit Regset.mem_1; eauto. congruence.
(* Istore *)
- assert (exists a',
- eval_addressing tge sp addr (map ls (map assign args)) = Some a'
- /\ Val.lessdef a a').
- apply eval_addressing_lessdef with (rs##args).
- eapply agree_eval_regs; eauto.
+ assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a).
+ replace (map ls (map assign args)) with (rs##args).
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
- destruct H2 as [a' [EVAL VMD]].
- assert (ESRC: Val.lessdef rs#src (ls (assign src))).
+ eapply agree_eval_regs; eauto.
+ assert (ESRC: rs#src = ls (assign src)).
eapply agree_eval_reg. eapply agree_reg_list_live. eauto.
- assert (exists tm', storev chunk tm a' (ls (assign src)) = Some tm'
- /\ Mem.lessdef m' tm').
- eapply Mem.storev_lessdef; eauto.
- destruct H2 as [m1' [STORE MMD']].
econstructor; split.
eapply exec_Lstore; eauto. TranslInstr.
+ rewrite <- ESRC. eauto.
MatchStates. eapply agree_reg_live. eapply agree_reg_list_live. eauto.
(* Icall *)
exploit transl_find_function; eauto. intros [tf [TFIND TF]].
generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H). unfold correct_alloc_instr. intros [CORR1 CORR2].
- exploit (parmov_spec ls (map assign args)
- (loc_arguments (RTL.funsig f))).
- apply loc_arguments_norepet.
- rewrite loc_arguments_length. inv WTI.
- rewrite <- H7. repeat rewrite list_length_map. auto.
- intros [PM1 PM2].
+ assert (rs##args = map ls (map assign args)).
+ eapply agree_eval_regs; eauto.
econstructor; split.
eapply exec_Lcall; eauto. TranslInstr.
rewrite (sig_function_translated _ _ TF). eauto.
- rewrite (sig_function_translated _ _ TF).
+ rewrite H1.
econstructor; eauto.
econstructor; eauto.
intros. eapply agree_succ with (n := pc); eauto.
unfold RTL.successors; rewrite H; auto with coqlib.
- eapply agree_call with (ls := ls); eauto.
- rewrite Locmap.gss. auto.
- intros. rewrite Locmap.gso. rewrite H1; auto. apply PM2; auto.
- eapply arguments_not_preserved; eauto. apply Loc.diff_sym; auto.
- rewrite (sig_function_translated _ _ TF).
- change Regset.elt with reg in PM1.
- rewrite PM1. eapply agree_eval_regs; eauto.
+ eapply agree_postcall; eauto.
(* Itailcall *)
exploit transl_find_function; eauto. intros [tf [TFIND TF]].
- exploit (parmov_spec ls (map assign args)
- (loc_arguments (RTL.funsig f))).
- apply loc_arguments_norepet.
- rewrite loc_arguments_length. inv WTI.
- rewrite <- H6. repeat rewrite list_length_map. auto.
- intros [PM1 PM2].
+ assert (rs##args = map ls (map assign args)).
+ eapply agree_eval_regs; eauto.
econstructor; split.
eapply exec_Ltailcall; eauto. TranslInstr.
rewrite (sig_function_translated _ _ TF). eauto.
- rewrite (sig_function_translated _ _ TF).
- econstructor; eauto.
- inv WTI. congruence.
- rewrite (sig_function_translated _ _ TF).
- rewrite return_regs_arguments.
- change Regset.elt with reg in PM1.
- rewrite PM1. eapply agree_eval_regs; eauto.
- inv WTI; auto.
- apply free_lessdef; auto.
- intros. rewrite return_regs_not_destroyed; auto.
+ rewrite H1. econstructor; eauto.
(* Ialloc *)
- assert (Val.lessdef (Vint sz) (ls (assign arg))).
- rewrite <- H0. eapply agree_eval_reg. eauto.
- inversion H2. subst v.
- pose (ls1 := Locmap.set (R loc_alloc_argument) (ls (assign arg)) ls).
- pose (ls2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) ls1).
- pose (ls3 := Locmap.set (assign res) (ls2 (R loc_alloc_result)) ls2).
- caseEq (alloc tm 0 (Int.signed sz)). intros tm' b1 ALLOC1.
- exploit Mem.alloc_lessdef; eauto. intros [EQ MMD1]. subst b1.
- exists (State ts (transf_fun f live assign) sp pc' ls3 tm'); split.
- unfold ls3, ls2, ls1. eapply exec_Lalloc; eauto. TranslInstr.
+ assert (ls (assign arg) = Vint sz).
+ rewrite <- H0. symmetry. eapply agree_eval_reg; eauto.
+ econstructor; split.
+ eapply exec_Lalloc; eauto. TranslInstr.
generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 CORR2].
MatchStates.
- eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls); eauto.
- unfold ls3; rewrite Locmap.gss.
- unfold ls2; rewrite Locmap.gss. auto.
- intros. unfold ls3; rewrite Locmap.gso.
- unfold ls2; rewrite Locmap.gso.
- unfold ls1; apply Locmap.gso.
- apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
- unfold loc_alloc_argument, destroyed_at_call; simpl; tauto.
- apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
- unfold loc_alloc_result, destroyed_at_call; simpl; tauto.
- apply Loc.diff_sym; auto.
+ eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto.
(* Icond, true *)
- assert (COND: eval_condition cond (map ls (map assign args)) tm = Some true).
- eapply eval_condition_lessdef; eauto.
+ assert (COND: eval_condition cond (map ls (map assign args)) m = Some true).
+ replace (map ls (map assign args)) with (rs##args). auto.
eapply agree_eval_regs; eauto.
econstructor; split.
eapply exec_Lcond_true; eauto. TranslInstr.
MatchStates. eapply agree_reg_list_live. eauto.
(* Icond, false *)
- assert (COND: eval_condition cond (map ls (map assign args)) tm = Some false).
- eapply eval_condition_lessdef; eauto.
+ assert (COND: eval_condition cond (map ls (map assign args)) m = Some false).
+ replace (map ls (map assign args)) with (rs##args). auto.
eapply agree_eval_regs; eauto.
econstructor; split.
eapply exec_Lcond_false; eauto. TranslInstr.
@@ -848,16 +786,12 @@ Proof.
(* Ireturn *)
econstructor; split.
eapply exec_Lreturn; eauto. TranslInstr; eauto.
+ replace (regmap_optget or Vundef rs)
+ with (locmap_optget (option_map assign or) Vundef ls).
econstructor; eauto.
- rewrite return_regs_result.
- inv WTI. destruct or; simpl in *.
- replace (loc_result (parent_callsig ts))
- with (loc_result (RTL.fn_sig f)).
- rewrite Locmap.gss. eapply agree_eval_reg; eauto.
- unfold loc_result. rewrite SIG. auto.
- constructor.
- apply free_lessdef; auto.
- intros. apply return_regs_not_destroyed; auto.
+ inv WTI. destruct or; simpl in *.
+ symmetry; eapply agree_eval_reg; eauto.
+ auto.
(* internal function *)
generalize H7. simpl. unfold transf_function.
@@ -866,46 +800,21 @@ Proof.
caseEq (analyze f); simpl; try congruence. intros live ANL.
caseEq (regalloc f live (live0 f live) env); simpl; try congruence.
intros alloc ALLOC EQ. inv EQ. simpl in *.
- caseEq (Mem.alloc tm 0 (RTL.fn_stacksize f)). intros tm' stk' MEMALLOC.
- exploit alloc_lessdef; eauto. intros [EQ LDM]. subst stk'.
econstructor; split.
eapply exec_function_internal; simpl; eauto.
simpl. econstructor; eauto.
- apply agree_init_regs. intros; eapply regalloc_correct_3; eauto.
- inv WTF.
- exploit (parmov_spec (call_regs ls)
- (loc_parameters (RTL.fn_sig f))
- (map alloc (RTL.fn_params f))).
- eapply regalloc_norepet_norepet; eauto.
- eapply regalloc_correct_2; eauto.
- rewrite loc_parameters_length. symmetry.
- transitivity (length (map env (RTL.fn_params f))).
- repeat rewrite list_length_map. auto.
- rewrite wt_params; auto.
- intros [PM1 PM2].
- change Regset.elt with reg in PM1. rewrite PM1.
- replace (map (call_regs ls) (loc_parameters (RTL.fn_sig f)))
- with (map ls (loc_arguments (RTL.fn_sig f))).
- auto.
- symmetry. unfold loc_parameters. rewrite list_map_compose.
- apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto.
+ change (transfer f (RTL.fn_entrypoint f) live !! (RTL.fn_entrypoint f))
+ with (live0 f live).
+ eapply agree_parameters; eauto.
(* external function *)
injection H7; intro EQ; inv EQ.
- exploit event_match_lessdef; eauto. intros [tres [A B]].
econstructor; split.
eapply exec_function_external; eauto.
eapply match_states_return; eauto.
- replace (loc_result (parent_callsig ts))
- with (loc_result (ef_sig ef)).
- rewrite Locmap.gss. auto.
- unfold loc_result. rewrite <- H6. auto.
- intros. rewrite <- H11; auto. apply Locmap.gso.
- apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
- apply loc_result_caller_save.
(* return *)
- inv H3.
+ inv H4.
econstructor; split.
eapply exec_return; eauto.
econstructor; eauto.
@@ -920,27 +829,21 @@ Lemma transf_initial_states:
Proof.
intros. inversion H.
exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
- assert (SIG2: funsig tf = mksignature nil (Some Tint)).
- rewrite <- H2. apply sig_function_translated; auto.
- assert (VPARAMS: Val.lessdef_list nil (map (Locmap.init Vundef) (loc_arguments (funsig tf)))).
- rewrite SIG2. simpl. constructor.
- assert (GENV: (Genv.init_mem tprog) = (Genv.init_mem prog)).
+ assert (MEM: (Genv.init_mem tprog) = (Genv.init_mem prog)).
exact (Genv.init_mem_transf_partial _ _ TRANSF).
- assert (MMD: Mem.lessdef (Genv.init_mem prog) (Genv.init_mem tprog)).
- rewrite GENV. apply Mem.lessdef_refl.
- exists (LTL.Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+ exists (LTL.Callstate nil tf nil (Genv.init_mem tprog)); split.
econstructor; eauto.
rewrite symbols_preserved.
rewrite (transform_partial_program_main _ _ TRANSF). auto.
- constructor; auto. constructor. rewrite H2; auto.
+ rewrite <- H2. apply sig_function_translated; auto.
+ rewrite MEM. constructor; auto. constructor.
Qed.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.
Proof.
- intros. inv H0. inv H. inv H3. econstructor.
- simpl in H4. inv H4. auto.
+ intros. inv H0. inv H. inv H4. econstructor.
Qed.
Theorem transf_program_correct: