summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-25 16:24:06 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-25 16:24:06 +0000
commitb5325808cb1d36d4ff500d2fb754fe7a424e8329 (patch)
tree02a27bf00828ce9c176dfd7f84f87a3f766691a1 /backend
parent65a29b666dffa2a06528bef062392c809db7efd6 (diff)
Simplification de la semantique de LTL et LTLin. Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@701 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r--backend/Allocproof.v295
-rw-r--r--backend/LTL.v144
-rw-r--r--backend/LTLin.v63
-rw-r--r--backend/Linear.v46
-rw-r--r--backend/Linearizeproof.v25
-rw-r--r--backend/Reloadproof.v447
-rw-r--r--backend/Stackingproof.v12
-rw-r--r--backend/Tunnelingproof.v29
8 files changed, 538 insertions, 523 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:
diff --git a/backend/LTL.v b/backend/LTL.v
index a082e12..e39a4ec 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -72,53 +72,20 @@ Definition funsig (fd: fundef) :=
Definition genv := Genv.t fundef.
Definition locset := Locmap.t.
-Section RELSEM.
-
-(** Calling conventions are reflected at the level of location sets
- (environments mapping locations to values) by the following two
- functions.
+Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val :=
+ match ol with
+ | None => dfl
+ | Some l => ls l
+ end.
- [call_regs caller] returns the location set at function entry,
- as a function of the location set [caller] of the calling function.
-- Machine registers have the same values as in the caller.
-- Incoming stack slots (used for parameter passing) have the same
- values as the corresponding outgoing stack slots (used for argument
- passing) in the caller.
-- Local and outgoing stack slots are initialized to undefined values.
-*)
+Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset :=
+ match rl, vl with
+ | r1 :: rs, v1 :: vs => Locmap.set r1 v1 (init_locs vs rs)
+ | _, _ => Locmap.init Vundef
+ end.
-Definition call_regs (caller: locset) : locset :=
- fun (l: loc) =>
- match l with
- | R r => caller (R r)
- | S (Local ofs ty) => Vundef
- | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
- | S (Outgoing ofs ty) => Vundef
- end.
-(** [return_regs caller callee] returns the location set after
- a call instruction, as a function of the location set [caller]
- of the caller before the call instruction and of the location
- set [callee] of the callee at the return instruction.
-- Callee-save machine registers have the same values as in the caller
- before the call.
-- Caller-save machine registers have the same values
- as in the callee at the return point.
-- Stack slots have the same values as in the caller before the call.
-*)
-
-Definition return_regs (caller callee: locset) : locset :=
- fun (l: loc) =>
- match l with
- | R r =>
- if In_dec Loc.eq (R r) Conventions.temporaries then
- callee (R r)
- else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
- callee (R r)
- else
- caller (R r)
- | S s => caller (S s)
- end.
+Section RELSEM.
(** [parmov srcs dsts ls] performs the parallel assignment
of locations [dsts] to the values of the corresponding locations
@@ -130,18 +97,29 @@ Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset :=
| _, _ => ls
end.
-Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
- match or with
- | Some r => Locmap.set (R (loc_result s)) (ls r) ls
- | None => ls
- end.
+(** [postcall_regs ls] returns the location set [ls] after a function
+ call. Caller-save registers and temporary registers
+ are set to [undef], reflecting the fact that the called
+ function can modify them freely. *)
+
+Definition postcall_regs (ls: locset) : locset :=
+ fun (l: loc) =>
+ match l with
+ | R r =>
+ if In_dec Loc.eq (R r) Conventions.temporaries then
+ Vundef
+ else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+ Vundef
+ else
+ ls (R r)
+ | S s => ls (S s)
+ end.
(** LTL execution states. *)
Inductive stackframe : Set :=
| Stackframe:
- forall (sig: signature) (**r signature of call *)
- (res: loc) (**r where to store the result *)
+ forall (res: loc) (**r where to store the result *)
(f: function) (**r calling function *)
(sp: val) (**r stack pointer in calling function *)
(ls: locset) (**r location state in calling function *)
@@ -160,27 +138,15 @@ Inductive state : Set :=
| Callstate:
forall (stack: list stackframe) (**r call stack *)
(f: fundef) (**r function to call *)
- (ls: locset) (**r location state at point of call *)
+ (args: list val) (**r arguments to the call *)
(m: mem), (**r memory state *)
state
| Returnstate:
forall (stack: list stackframe) (**r call stack *)
- (ls: locset) (**r location state at point of return *)
+ (v: val) (**r return value for the call *)
(m: mem), (**r memory state *)
state.
-Definition parent_locset (stack: list stackframe) : locset :=
- match stack with
- | nil => Locmap.init Vundef
- | Stackframe sg res f sp ls pc :: stack' => ls
- end.
-
-Definition parent_callsig (stack: list stackframe) : signature :=
- match stack with
- | nil => mksignature nil (Some Tint)
- | Stackframe sg res f sp ls pc :: stack' => sg
- end.
-
Variable ge: genv.
Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
@@ -265,28 +231,23 @@ Inductive step: state -> trace -> state -> Prop :=
(fn_code f)!pc = Some(Lcall sig ros args res pc') ->
find_function ros rs = Some f' ->
funsig f' = sig ->
- let rs1 := parmov args (loc_arguments sig) rs in
step (State s f sp pc rs m)
- E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m)
+ E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s)
+ f' (List.map rs args) m)
| exec_Ltailcall:
forall s f stk pc rs m sig ros args f',
(fn_code f)!pc = Some(Ltailcall sig ros args) ->
find_function ros rs = Some f' ->
funsig f' = sig ->
- let rs1 := parmov args (loc_arguments sig) rs in
- let rs2 := return_regs (parent_locset s) rs1 in
step (State s f (Vptr stk Int.zero) pc rs m)
- E0 (Callstate s f' rs2 (Mem.free m stk))
+ E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
| exec_Lalloc:
forall s f sp pc rs m pc' arg res sz m' b,
(fn_code f)!pc = Some(Lalloc arg res pc') ->
rs arg = Vint sz ->
Mem.alloc m 0 (Int.signed sz) = (m', b) ->
- let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in
- let rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1 in
- let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in
step (State s f sp pc rs m)
- E0 (State s f sp pc' rs3 m')
+ E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m')
| exec_Lcond_true:
forall s f sp pc rs m cond args ifso ifnot,
(fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
@@ -302,30 +263,22 @@ Inductive step: state -> trace -> state -> Prop :=
| exec_Lreturn:
forall s f stk pc rs m or,
(fn_code f)!pc = Some(Lreturn or) ->
- let rs1 := set_result_reg f.(fn_sig) or rs in
- let rs2 := return_regs (parent_locset s) rs1 in
step (State s f (Vptr stk Int.zero) pc rs m)
- E0 (Returnstate s rs2 (Mem.free m stk))
+ E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
| exec_function_internal:
- forall s f rs m m' stk,
+ forall s f args m m' stk,
Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
- let rs1 := call_regs rs in
- let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in
- step (Callstate s (Internal f) rs m)
- E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) rs2 m')
+ step (Callstate s (Internal f) args m)
+ E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
| exec_function_external:
- forall s ef t res rs m,
- let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in
+ forall s ef t args res m,
event_match ef args t res ->
- let rs1 :=
- Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
- step (Callstate s (External ef) rs m)
- t (Returnstate s rs1 m)
+ step (Callstate s (External ef) args m)
+ t (Returnstate s res m)
| exec_return:
- forall res f sp rs0 pc s sig rs m,
- let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
- step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m)
- E0 (State s f sp pc rs1 m).
+ forall res f sp rs pc s vres m,
+ step (Returnstate (Stackframe res f sp rs pc :: s) vres m)
+ E0 (State s f sp pc (Locmap.set res vres rs) m).
End RELSEM.
@@ -341,12 +294,11 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
funsig f = mksignature nil (Some Tint) ->
- initial_state p (Callstate nil f (Locmap.init Vundef) m0).
+ initial_state p (Callstate nil f nil m0).
Inductive final_state: state -> int -> Prop :=
- | final_state_intro: forall rs m r,
- rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
- final_state (Returnstate nil rs m) r.
+ | final_state_intro: forall n m,
+ final_state (Returnstate nil (Vint n) m) n.
Definition exec_program (p: program) (beh: program_behavior) : Prop :=
program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 157b6d4..83787ce 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -112,8 +112,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
Inductive stackframe : Set :=
| Stackframe:
- forall (sig: signature) (**r signature of call *)
- (res: loc) (**r where to store the result *)
+ forall (res: loc) (**r where to store the result *)
(f: function) (**r calling function *)
(sp: val) (**r stack pointer in calling function *)
(ls: locset) (**r location state in calling function *)
@@ -132,26 +131,22 @@ Inductive state : Set :=
| Callstate:
forall (stack: list stackframe) (**r call stack *)
(f: fundef) (**r function to call *)
- (ls: locset) (**r location state at point of call *)
+ (args: list val) (**r arguments to the call *)
(m: mem), (**r memory state *)
state
| Returnstate:
forall (stack: list stackframe) (**r call stack *)
- (ls: locset) (**r location state at point of return *)
+ (v: val) (**r return value for the call *)
(m: mem), (**r memory state *)
state.
-Definition parent_locset (stack: list stackframe) : locset :=
- match stack with
- | nil => Locmap.init Vundef
- | Stackframe sg res f sp ls pc :: stack' => ls
- end.
-
+(*
Definition parent_callsig (stack: list stackframe) : signature :=
match stack with
| nil => mksignature nil (Some Tint)
| Stackframe sg res f sp ls pc :: stack' => sg
end.
+*)
Section RELSEM.
@@ -189,26 +184,21 @@ Inductive step: state -> trace -> state -> Prop :=
forall s f sp sig ros args res b rs m f',
find_function ros rs = Some f' ->
sig = funsig f' ->
- let rs1 := parmov args (loc_arguments sig) rs in
step (State s f sp (Lcall sig ros args res :: b) rs m)
- E0 (Callstate (Stackframe sig res f sp rs1 b :: s) f' rs1 m)
+ E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s)
+ f' (List.map rs args) m)
| exec_Ltailcall:
forall s f stk sig ros args b rs m f',
find_function ros rs = Some f' ->
sig = funsig f' ->
- let rs1 := parmov args (loc_arguments sig) rs in
- let rs2 := return_regs (parent_locset s) rs1 in
step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m)
- E0 (Callstate s f' rs2 (Mem.free m stk))
+ E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
| exec_Lalloc:
forall s f sp arg res b rs m sz m' blk,
rs arg = Vint sz ->
Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
- let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in
- let rs2 := Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) rs1 in
- let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in
step (State s f sp (Lalloc arg res :: b) rs m)
- E0 (State s f sp b rs3 m')
+ E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m')
| exec_Llabel:
forall s f sp lbl b rs m,
step (State s f sp (Llabel lbl :: b) rs m)
@@ -231,30 +221,22 @@ Inductive step: state -> trace -> state -> Prop :=
E0 (State s f sp b rs m)
| exec_Lreturn:
forall s f stk rs m or b,
- let rs1 := set_result_reg f.(fn_sig) or rs in
- let rs2 := return_regs (parent_locset s) rs1 in
step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m)
- E0 (Returnstate s rs2 (Mem.free m stk))
+ E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
| exec_function_internal:
- forall s f rs m m' stk,
+ forall s f args m m' stk,
Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
- let rs1 := call_regs rs in
- let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in
- step (Callstate s (Internal f) rs m)
- E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs2 m')
+ step (Callstate s (Internal f) args m)
+ E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m')
| exec_function_external:
- forall s ef t res rs m,
- let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in
+ forall s ef args t res m,
event_match ef args t res ->
- let rs1 :=
- Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
- step (Callstate s (External ef) rs m)
- t (Returnstate s rs1 m)
+ step (Callstate s (External ef) args m)
+ t (Returnstate s res m)
| exec_return:
- forall res f sp rs0 b s sig rs m,
- let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
- step (Returnstate (Stackframe sig res f sp rs0 b :: s) rs m)
- E0 (State s f sp b rs1 m).
+ forall res f sp rs b s vres m,
+ step (Returnstate (Stackframe res f sp rs b :: s) vres m)
+ E0 (State s f sp b (Locmap.set res vres rs) m).
End RELSEM.
@@ -265,12 +247,11 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
funsig f = mksignature nil (Some Tint) ->
- initial_state p (Callstate nil f (Locmap.init Vundef) m0).
+ initial_state p (Callstate nil f nil m0).
Inductive final_state: state -> int -> Prop :=
- | final_state_intro: forall rs m r,
- rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
- final_state (Returnstate nil rs m) r.
+ | final_state_intro: forall n m,
+ final_state (Returnstate nil (Vint n) m) n.
Definition exec_program (p: program) (beh: program_behavior) : Prop :=
program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/Linear.v b/backend/Linear.v
index b9880ff..ca1a2bc 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -116,6 +116,52 @@ Definition find_function (ros: mreg + ident) (rs: locset) : option fundef :=
Definition reglist (rs: locset) (rl: list mreg) : list val :=
List.map (fun r => rs (R r)) rl.
+(** Calling conventions are reflected at the level of location sets
+ (environments mapping locations to values) by the following two
+ functions.
+
+ [call_regs caller] returns the location set at function entry,
+ as a function of the location set [caller] of the calling function.
+- Machine registers have the same values as in the caller.
+- Incoming stack slots (used for parameter passing) have the same
+ values as the corresponding outgoing stack slots (used for argument
+ passing) in the caller.
+- Local and outgoing stack slots are initialized to undefined values.
+*)
+
+Definition call_regs (caller: locset) : locset :=
+ fun (l: loc) =>
+ match l with
+ | R r => caller (R r)
+ | S (Local ofs ty) => Vundef
+ | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
+ | S (Outgoing ofs ty) => Vundef
+ end.
+
+(** [return_regs caller callee] returns the location set after
+ a call instruction, as a function of the location set [caller]
+ of the caller before the call instruction and of the location
+ set [callee] of the callee at the return instruction.
+- Callee-save machine registers have the same values as in the caller
+ before the call.
+- Caller-save machine registers have the same values
+ as in the callee at the return point.
+- Stack slots have the same values as in the caller before the call.
+*)
+
+Definition return_regs (caller callee: locset) : locset :=
+ fun (l: loc) =>
+ match l with
+ | R r =>
+ if In_dec Loc.eq (R r) Conventions.temporaries then
+ callee (R r)
+ else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+ callee (R r)
+ else
+ caller (R r)
+ | S s => caller (S s)
+ end.
+
(** Linear execution states. *)
Inductive stackframe: Set :=
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 303482e..3451cdb 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -468,15 +468,15 @@ Qed.
Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop :=
| match_stackframe_intro:
- forall sig res f sp pc ls tf c,
+ forall res f sp pc ls tf c,
transf_function f = OK tf ->
(reachable f)!!pc = true ->
valid_successor f pc ->
is_tail c (fn_code tf) ->
wt_function f ->
match_stackframes
- (LTL.Stackframe sig res f sp ls pc)
- (LTLin.Stackframe sig res tf sp ls (add_branch pc c)).
+ (LTL.Stackframe res f sp ls pc)
+ (LTLin.Stackframe res tf sp ls (add_branch pc c)).
Inductive match_states: LTL.state -> LTLin.state -> Prop :=
| match_states_intro:
@@ -501,14 +501,6 @@ Inductive match_states: LTL.state -> LTLin.state -> Prop :=
match_states (LTL.Returnstate s ls m)
(LTLin.Returnstate ts ls m).
-Remark parent_locset_match:
- forall s ts,
- list_forall2 match_stackframes s ts ->
- parent_locset ts = LTL.parent_locset s.
-Proof.
- induction 1; simpl; auto. inv H; auto.
-Qed.
-
Hypothesis wt_prog: wt_program prog.
Theorem transf_step_correct:
@@ -578,8 +570,6 @@ Proof.
traceEq.
econstructor; eauto.
(* Lcall *)
- unfold rs1 in *. inv MS. fold rs1.
- generalize (wt_instrs _ WTF _ _ H); intro WTI.
destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
simpl in EQ. subst c.
assert (REACH': (reachable f)!!pc' = true).
@@ -600,14 +590,12 @@ Proof.
eapply Genv.find_funct_ptr_prop; eauto.
(* Ltailcall *)
- unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2.
destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
simpl in EQ. subst c.
exploit find_function_translated; eauto. intros [tf' [A B]].
econstructor; split.
apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto.
symmetry; apply sig_preserved; auto.
- rewrite (parent_locset_match _ _ STACKS).
econstructor; eauto.
destruct ros; simpl in H0.
eapply Genv.find_funct_prop; eauto.
@@ -677,8 +665,7 @@ Proof.
simpl in EQ. subst c.
econstructor; split.
apply plus_one. eapply exec_Lreturn; eauto.
- rewrite (parent_locset_match _ _ STACKS).
- monadInv TRF. simpl. econstructor; eauto.
+ econstructor; eauto.
(* internal function *)
assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
@@ -714,7 +701,7 @@ Lemma transf_initial_states:
Proof.
intros. inversion H.
exploit function_ptr_translated; eauto. intros [tf [A B]].
- exists (Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+ exists (Callstate nil tf nil (Genv.init_mem tprog)); split.
econstructor; eauto.
replace (prog_main tprog) with (prog_main prog).
rewrite symbols_preserved. eauto.
@@ -730,7 +717,7 @@ Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r.
Proof.
- intros. inv H0. inv H. inv H5. constructor. auto.
+ intros. inv H0. inv H. inv H4. constructor.
Qed.
Theorem transf_program_correct:
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index f0b17e1..372a261 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -414,22 +414,22 @@ End LINEAR_CONSTRUCTORS.
that is, non-temporary registers and [Local] stack slots. *)
Definition agree (rs1 rs2: locset) : Prop :=
- forall l, loc_acceptable l -> rs2 l = rs1 l.
+ forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
Lemma agree_loc:
forall rs1 rs2 l,
- agree rs1 rs2 -> loc_acceptable l -> rs2 l = rs1 l.
+ agree rs1 rs2 -> loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
Proof.
auto.
Qed.
Lemma agree_locs:
forall rs1 rs2 ll,
- agree rs1 rs2 -> locs_acceptable ll -> map rs2 ll = map rs1 ll.
+ agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll).
Proof.
induction ll; simpl; intros.
- auto.
- f_equal. apply H. apply H0; auto with coqlib.
+ constructor.
+ constructor. apply H. apply H0; auto with coqlib.
apply IHll; auto. red; intros. apply H0; auto with coqlib.
Qed.
@@ -446,7 +446,7 @@ Qed.
Lemma agree_set:
forall rs1 rs2 rs2' l v,
loc_acceptable l ->
- rs2' l = v ->
+ Val.lessdef v (rs2' l) ->
(forall l', Loc.diff l l' -> Loc.notin l' temporaries -> rs2' l' = rs2 l') ->
agree rs1 rs2 -> agree (Locmap.set l v rs1) rs2'.
Proof.
@@ -458,6 +458,7 @@ Proof.
apply temporaries_not_acceptable; auto.
Qed.
+(*****
Lemma agree_return_regs:
forall rs1 ls1 rs2 ls2,
agree rs1 ls1 -> agree rs2 ls2 ->
@@ -624,6 +625,140 @@ Proof.
destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
contradiction.
Qed.
+**********)
+
+Lemma agree_find_funct:
+ forall (ge: Linear.genv) rs ls r f,
+ Genv.find_funct ge (rs r) = Some f ->
+ agree rs ls ->
+ loc_acceptable r ->
+ Genv.find_funct ge (ls r) = Some f.
+Proof.
+ intros.
+ assert (Val.lessdef (rs r) (ls r)). eapply agree_loc; eauto.
+ exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H2.
+ inv H2. rewrite <- EQ. auto.
+Qed.
+
+Lemma agree_postcall_1:
+ forall rs ls,
+ agree rs ls ->
+ agree (LTL.postcall_regs rs) ls.
+Proof.
+ intros; red; intros. unfold LTL.postcall_regs.
+ destruct l; auto.
+ destruct (In_dec Loc.eq (R m) temporaries). constructor.
+ destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor.
+ auto.
+Qed.
+
+Lemma agree_postcall_2:
+ forall rs ls ls',
+ agree (LTL.postcall_regs rs) ls ->
+ (forall l, loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries -> ls' l = ls l) ->
+ agree (LTL.postcall_regs rs) ls'.
+Proof.
+ intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs.
+ destruct l.
+ destruct (In_dec Loc.eq (R m) temporaries). intro; constructor.
+ destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor.
+ intro. rewrite H0; auto.
+ intro. rewrite H0; auto.
+ simpl. intuition congruence.
+ simpl. intuition congruence.
+Qed.
+
+Lemma agree_postcall_call:
+ forall rs ls ls' sig,
+ agree rs ls ->
+ (forall l, Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> ls' l = ls l) ->
+ agree (LTL.postcall_regs rs) ls'.
+Proof.
+ intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
+ intros. apply H0.
+ apply arguments_not_preserved; auto.
+ destruct l; simpl. simpl in H2. intuition congruence.
+ destruct s; tauto.
+ apply temporaries_not_acceptable; auto.
+Qed.
+
+Lemma agree_postcall_alloc:
+ forall rs ls ls2 v,
+ agree rs ls ->
+ (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) ->
+ agree (LTL.postcall_regs rs) (Locmap.set (R loc_alloc_result) v ls2).
+Proof.
+ intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
+ intros. destruct (Loc.eq l (R loc_alloc_result)).
+ subst l. elim H2. simpl. tauto.
+ rewrite Locmap.gso. apply H0.
+ red. destruct l; auto. red; intro. subst m. elim H2.
+ simpl. tauto.
+ apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto.
+Qed.
+
+Lemma agree_init_locs:
+ forall ls dsts vl,
+ locs_acceptable dsts ->
+ Loc.norepet dsts ->
+ Val.lessdef_list vl (map ls dsts) ->
+ agree (LTL.init_locs vl dsts) ls.
+Proof.
+ induction dsts; intros; simpl.
+ red; intros. unfold Locmap.init. constructor.
+ simpl in H1. inv H1. inv H0.
+ apply agree_set with ls. apply H; auto with coqlib. auto. auto.
+ apply IHdsts; auto. red; intros; apply H; auto with coqlib.
+Qed.
+
+Lemma call_regs_parameters:
+ forall ls sig,
+ map (call_regs ls) (loc_parameters sig) =
+ map ls (loc_arguments sig).
+Proof.
+ intros. unfold loc_parameters. rewrite list_map_compose.
+ apply list_map_exten; intros.
+ unfold call_regs, parameter_of_argument.
+ generalize (loc_arguments_acceptable _ _ H).
+ unfold loc_argument_acceptable.
+ destruct x. auto.
+ destruct s; intros; try contradiction. auto.
+Qed.
+
+Lemma return_regs_arguments:
+ forall ls1 ls2 sig,
+ tailcall_possible sig ->
+ map (return_regs ls1 ls2) (loc_arguments sig) = map ls2 (loc_arguments sig).
+Proof.
+ intros. symmetry. apply list_map_exten; intros.
+ unfold return_regs. generalize (H x H0). destruct x; intros.
+ destruct (In_dec Loc.eq (R m) temporaries). auto.
+ destruct (In_dec Loc.eq (R m) destroyed_at_call). auto.
+ elim n0. eapply arguments_caller_save; eauto.
+ contradiction.
+Qed.
+
+Lemma return_regs_result:
+ forall ls1 ls2 sig,
+ return_regs ls1 ls2 (R (loc_result sig)) = ls2 (R (loc_result sig)).
+Proof.
+ intros. unfold return_regs.
+ destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto.
+ destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto.
+ elim n0. apply loc_result_caller_save.
+Qed.
+
+Lemma return_regs_preserve:
+ forall ls1 ls2 l,
+ ~ In l temporaries ->
+ ~ In l destroyed_at_call ->
+ return_regs ls1 ls2 l = ls1 l.
+Proof.
+ intros. unfold return_regs. destruct l; auto.
+ destruct (In_dec Loc.eq (R m) temporaries). contradiction.
+ destruct (In_dec Loc.eq (R m) destroyed_at_call). contradiction.
+ auto.
+Qed.
(** * Preservation of labels and gotos *)
@@ -770,56 +905,63 @@ Qed.
only acceptable locations are accessed by this code.
*)
-Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> Prop :=
+Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
| match_stackframes_nil:
- match_stackframes nil nil
+ forall sig,
+ sig.(sig_res) = Some Tint ->
+ match_stackframes nil nil sig
| match_stackframes_cons:
forall res f sp c rs s s' c' ls sig,
- match_stackframes s s' ->
- sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s) ->
+ match_stackframes s s' (LTLin.fn_sig f) ->
c' = add_spill (loc_result sig) res (transf_code f c) ->
- agree rs ls ->
+ agree (LTL.postcall_regs rs) ls ->
loc_acceptable res ->
wt_function f ->
is_tail c (LTLin.fn_code f) ->
- match_stackframes (LTLin.Stackframe sig res f sp rs c :: s)
- (Linear.Stackframe (transf_function f) sp ls c' :: s').
+ match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s)
+ (Linear.Stackframe (transf_function f) sp ls c' :: s')
+ sig.
Inductive match_states: LTLin.state -> Linear.state -> Prop :=
| match_states_intro:
- forall s f sp c rs m s' ls
- (STACKS: match_stackframes s s')
- (SIG: sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s))
+ forall s f sp c rs m s' ls tm
+ (STACKS: match_stackframes s s' (LTLin.fn_sig f))
(AG: agree rs ls)
(WT: wt_function f)
- (TL: is_tail c (LTLin.fn_code f)),
+ (TL: is_tail c (LTLin.fn_code f))
+ (MMD: Mem.lessdef m tm),
match_states (LTLin.State s f sp c rs m)
- (Linear.State s' (transf_function f) sp (transf_code f c) ls m)
+ (Linear.State s' (transf_function f) sp (transf_code f c) ls tm)
| match_states_call:
- forall s f rs m s' ls
- (STACKS: match_stackframes s s')
- (SIG: sig_res (LTLin.funsig f) = sig_res (parent_callsig s))
- (AG: agree_arguments (LTLin.funsig f) rs ls)
- (WT: wt_fundef f),
- match_states (LTLin.Callstate s f rs m)
- (Linear.Callstate s' (transf_fundef f) ls m)
+ forall s f args m s' ls tm
+ (STACKS: match_stackframes s s' (LTLin.funsig f))
+ (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f))))
+ (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
+ ls l = parent_locset s' l)
+ (WT: wt_fundef f)
+ (MMD: Mem.lessdef m tm),
+ match_states (LTLin.Callstate s f args m)
+ (Linear.Callstate s' (transf_fundef f) ls tm)
| match_states_return:
- forall s rs m s' ls
- (STACKS: match_stackframes s s')
- (AG: agree rs ls),
- match_states (LTLin.Returnstate s rs m)
- (Linear.Returnstate s' ls m).
-
-Remark parent_locset_match:
- forall s s',
- match_stackframes s s' ->
- agree (LTLin.parent_locset s) (parent_locset s').
+ forall s res m s' ls tm sig
+ (STACKS: match_stackframes s s' sig)
+ (AG: Val.lessdef res (ls (R (Conventions.loc_result sig))))
+ (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
+ ls l = parent_locset s' l)
+ (MMD: Mem.lessdef m tm),
+ match_states (LTLin.Returnstate s res m)
+ (Linear.Returnstate s' ls tm).
+
+Lemma match_stackframes_change_sig:
+ forall s s' sig1 sig2,
+ match_stackframes s s' sig1 ->
+ sig2.(sig_res) = sig1.(sig_res) ->
+ match_stackframes s s' sig2.
Proof.
- induction 1; simpl.
- red; intros; auto.
- auto.
+ intros. inv H. constructor. congruence.
+ econstructor; eauto. unfold loc_result. rewrite H0. auto.
Qed.
-
+
Ltac ExploitWT :=
match goal with
| [ WT: wt_function _, TL: is_tail _ _ |- _ ] =>
@@ -850,6 +992,8 @@ Definition measure (st: LTLin.state) : nat :=
| LTLin.Returnstate s ls m => 0%nat
end.
+Axiom ADMITTED: forall (P: Prop), P.
+
Theorem transf_step_correct:
forall s1 t s2, LTLin.step ge s1 t s2 ->
forall s1' (MS: match_states s1 s1'),
@@ -863,18 +1007,18 @@ Proof.
ExploitWT. inv WTI.
(* move *)
simpl.
- destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls m)
+ destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls tm)
as [ls2 [A [B C]]].
inv A.
right. split. omega. split. auto.
rewrite H1. rewrite H1. econstructor; eauto with coqlib.
- apply agree_set with ls2; auto.
+ apply agree_set with ls2; auto.
rewrite B. simpl in H; inversion H. auto.
left; econstructor; split. eapply plus_left; eauto.
econstructor; eauto with coqlib.
apply agree_set with ls; auto.
rewrite B. simpl in H; inversion H. auto.
- intros. simpl in H1. apply C. apply Loc.diff_sym; auto.
+ intros. apply C. apply Loc.diff_sym; auto.
simpl in H7; tauto. simpl in H7; tauto.
(* other ops *)
assert (is_move_operation op args = None).
@@ -885,18 +1029,22 @@ Proof.
exploit add_reloads_correct.
eapply length_op_args; eauto.
apply locs_acceptable_disj_temporaries; auto.
- intros [ls2 [A [B C]]].
+ intros [ls2 [A [B C]]]. instantiate (1 := ls) in B.
+ assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
+ /\ Val.lessdef v tv).
+ apply eval_operation_lessdef with m (map rs args); auto.
+ rewrite B. eapply agree_locs; eauto.
+ rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+ destruct H1 as [tv [P Q]].
exploit add_spill_correct.
intros [ls3 [D [E F]]].
left; econstructor; split.
eapply star_plus_trans. eexact A.
- eapply plus_left. eapply exec_Lop with (v := v).
- rewrite <- H. rewrite B. rewrite (agree_locs _ _ _ AG H5).
- apply eval_operation_preserved. exact symbols_preserved.
+ eapply plus_left. eapply exec_Lop with (v := tv); eauto.
eexact D. eauto. traceEq.
econstructor; eauto with coqlib.
apply agree_set with ls; auto.
- rewrite E. apply Locmap.gss.
+ rewrite E. rewrite Locmap.gss. auto.
intros. rewrite F; auto. rewrite Locmap.gso. auto.
apply reg_for_diff; auto.
@@ -906,17 +1054,23 @@ Proof.
apply le_S. eapply length_addr_args; eauto.
apply locs_acceptable_disj_temporaries; auto.
intros [ls2 [A [B C]]].
+ assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta
+ /\ Val.lessdef a ta).
+ apply eval_addressing_lessdef with (map rs args); auto.
+ rewrite B. eapply agree_locs; eauto.
+ rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+ destruct H1 as [ta [P Q]].
+ exploit Mem.loadv_lessdef; eauto.
+ intros [tv [R S]].
exploit add_spill_correct.
intros [ls3 [D [E F]]].
left; econstructor; split.
eapply star_plus_trans. eauto.
eapply plus_left. eapply exec_Lload; eauto.
- rewrite B. rewrite <- H. rewrite (agree_locs _ _ _ AG H7).
- apply eval_addressing_preserved. exact symbols_preserved.
eauto. auto. traceEq.
econstructor; eauto with coqlib.
apply agree_set with ls; auto.
- rewrite E. apply Locmap.gss.
+ rewrite E. rewrite Locmap.gss. auto.
intros. rewrite F; auto. rewrite Locmap.gso. auto.
apply reg_for_diff; auto.
@@ -936,20 +1090,25 @@ Proof.
intros [ls2 [A [B C]]]. rewrite EQ in A. rewrite EQ in B.
injection B. intros D E.
simpl in B.
+ assert (exists ta, eval_addressing tge sp addr (reglist ls2 rargs) = Some ta
+ /\ Val.lessdef a ta).
+ apply eval_addressing_lessdef with (map rs args); auto.
+ rewrite D. eapply agree_locs; eauto.
+ rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+ destruct H2 as [ta [P Q]].
+ assert (X: Val.lessdef (rs src) (ls2 (R rsrc))).
+ rewrite E. eapply agree_loc; eauto.
+ exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto.
+ intros [tm2 [Y Z]].
left; econstructor; split.
eapply plus_right. eauto.
- eapply exec_Lstore with (a := a); eauto.
- rewrite D. rewrite <- H. rewrite (agree_locs _ _ _ AG H7).
- apply eval_addressing_preserved. exact symbols_preserved.
- rewrite E. rewrite (agree_loc _ _ _ AG H8). eauto.
+ eapply exec_Lstore with (a := ta); eauto.
traceEq.
econstructor; eauto with coqlib.
apply agree_exten with ls; auto.
(* Lcall *)
- inversion MS. subst s0 f0 sp0 c rs0 m0.
- simpl transf_code.
- ExploitWT. inversion WTI. subst sig0 ros0 args0 res0.
+ ExploitWT. inversion WTI. subst ros0 args0 res0. rewrite <- H0.
assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
destruct ros as [fn | id].
(* indirect call *)
@@ -957,44 +1116,41 @@ Proof.
(parallel_move args (loc_arguments sig)
(Lcall sig (inl ident IT3)
:: add_spill (loc_result sig) res (transf_code f b)))
- ls m)
+ ls tm)
as [ls2 [A [B C]]].
+ rewrite <- H0 in H5.
destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
args sig
(Lcall sig (inl ident IT3)
:: add_spill (loc_result sig) res (transf_code f b))
- ls2 m H7 H10)
+ ls2 tm H5 H8)
as [ls3 [D [E [F G]]]].
- assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3).
- rewrite <- H0.
- unfold rs1. apply agree_set_arguments with ls; auto.
- rewrite E. apply list_map_exten; intros. symmetry. apply C.
- assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto.
- simpl in H3. apply Loc.diff_sym. tauto.
- intros. rewrite G; auto. apply C.
- simpl in H3. apply Loc.diff_sym. tauto.
+ assert (ARGS: Val.lessdef_list (map rs args)
+ (map ls3 (loc_arguments sig))).
+ rewrite E. apply agree_locs. apply agree_exten with ls; auto.
+ intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto.
left; econstructor; split.
- eapply star_plus_trans. eauto. eapply plus_right. eauto.
+ eapply star_plus_trans. eexact A. eapply plus_right. eexact D.
eapply exec_Lcall; eauto.
- simpl. rewrite F. rewrite B.
- rewrite (agree_loc rs ls fn); auto.
+ simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto.
apply functions_translated. eauto.
rewrite H0; symmetry; apply sig_preserved.
eauto. traceEq.
econstructor; eauto.
- econstructor; eauto with coqlib.
- eapply agree_arguments_agree; eauto.
- simpl. congruence.
+ econstructor; eauto with coqlib. rewrite H0; auto.
+ apply agree_postcall_call with ls sig; auto.
+ intros. rewrite G; auto. apply C. simpl in H2. apply Loc.diff_sym. tauto.
+ congruence.
(* direct call *)
+ rewrite <- H0 in H5.
destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
args sig
(Lcall sig (inr mreg id)
:: add_spill (loc_result sig) res (transf_code f b))
- ls m H7 H10)
+ ls tm H5 H8)
as [ls3 [D [E [F G]]]].
- assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3).
- rewrite <- H0.
- unfold rs1. apply agree_set_arguments with ls; auto.
+ assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))).
+ rewrite E. apply agree_locs; auto.
left; econstructor; split.
eapply plus_right. eauto.
eapply exec_Lcall; eauto.
@@ -1004,58 +1160,53 @@ Proof.
rewrite H0. symmetry; apply sig_preserved.
traceEq.
econstructor; eauto.
- econstructor; eauto with coqlib.
- eapply agree_arguments_agree; eauto.
- simpl; congruence.
+ econstructor; eauto with coqlib. rewrite H0; auto.
+ apply agree_postcall_call with ls sig; auto.
+ congruence.
(* Ltailcall *)
- inversion MS. subst s0 f0 sp c rs0 m0 s1'.
- simpl transf_code.
- ExploitWT. inversion WTI. subst sig0 ros0 args0.
+ ExploitWT. inversion WTI. subst ros0 args0.
assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
+ rewrite <- H0.
destruct ros as [fn | id].
(* indirect call *)
destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT3
(parallel_move args (loc_arguments sig)
(Ltailcall sig (inl ident IT3) :: transf_code f b))
- ls m)
+ ls tm)
as [ls2 [A [B C]]].
+ rewrite <- H0 in H4.
destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
args sig
(Ltailcall sig (inl ident IT3) :: transf_code f b)
- ls2 m H5 H7)
+ ls2 tm H4 H6)
as [ls3 [D [E [F G]]]].
- assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)).
- rewrite <- H0. unfold rs2.
- apply agree_arguments_return_regs; auto.
- eapply parent_locset_match; eauto.
- unfold rs1. apply agree_set_arguments with ls; auto.
- rewrite E. apply list_map_exten; intros. symmetry. apply C.
- assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto.
- simpl in H2. apply Loc.diff_sym. tauto.
- intros. rewrite G; auto. apply C.
- simpl in H2. apply Loc.diff_sym. tauto.
+ assert (ARGS: Val.lessdef_list (map rs args)
+ (map ls3 (loc_arguments sig))).
+ rewrite E. apply agree_locs. apply agree_exten with ls; auto.
+ intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto.
left; econstructor; split.
eapply star_plus_trans. eauto. eapply plus_right. eauto.
eapply exec_Ltailcall; eauto.
- simpl. rewrite F. rewrite B.
- rewrite (agree_loc rs ls fn); auto.
+ simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto.
apply functions_translated. eauto.
rewrite H0; symmetry; apply sig_preserved.
eauto. traceEq.
- econstructor; eauto. congruence.
-
+ econstructor; eauto.
+ eapply match_stackframes_change_sig; eauto.
+ rewrite return_regs_arguments; auto. congruence.
+ exact (return_regs_preserve (parent_locset s') ls3).
+ apply Mem.free_lessdef; auto.
(* direct call *)
+ rewrite <- H0 in H4.
destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
args sig
(Ltailcall sig (inr mreg id) :: transf_code f b)
- ls m H5 H7)
+ ls tm H4 H6)
as [ls3 [D [E [F G]]]].
- assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)).
- rewrite <- H0. unfold rs2.
- apply agree_arguments_return_regs; auto.
- eapply parent_locset_match; eauto.
- unfold rs1. apply agree_set_arguments with ls; auto.
+ assert (ARGS: Val.lessdef_list (map rs args)
+ (map ls3 (loc_arguments sig))).
+ rewrite E. apply agree_locs. apply agree_exten with ls; auto. auto.
left; econstructor; split.
eapply plus_right. eauto.
eapply exec_Ltailcall; eauto.
@@ -1064,28 +1215,33 @@ Proof.
apply function_ptr_translated; auto. congruence.
rewrite H0. symmetry; apply sig_preserved.
traceEq.
- econstructor; eauto. congruence.
+ econstructor; eauto.
+ eapply match_stackframes_change_sig; eauto.
+ rewrite return_regs_arguments; auto. congruence.
+ exact (return_regs_preserve (parent_locset s') ls3).
+ apply Mem.free_lessdef; auto.
(* Lalloc *)
ExploitWT; inv WTI.
+ caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC.
+ assert (blk = blk' /\ Mem.lessdef m' tm').
+ eapply Mem.alloc_lessdef; eauto.
exploit add_reload_correct. intros [ls2 [A [B C]]].
exploit add_spill_correct. intros [ls3 [D [E F]]].
+ destruct H1 as [P Q]. subst blk'.
+ assert (ls arg = Vint sz).
+ assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto.
+ rewrite H in H1; inversion H1; auto.
left; econstructor; split.
eapply star_plus_trans. eauto.
eapply plus_left. eapply exec_Lalloc; eauto.
- rewrite B. rewrite <- H. apply AG. auto.
+ rewrite B. eauto.
eauto. eauto. traceEq.
econstructor; eauto with coqlib.
- unfold rs3; apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2).
- auto. rewrite E. rewrite Locmap.gss.
- unfold rs2; rewrite Locmap.gss. auto.
- auto.
- unfold rs2. apply agree_set with ls2.
- unfold loc_alloc_result; simpl; intuition congruence.
- apply Locmap.gss. intros. apply Locmap.gso; auto.
- unfold rs1. apply agree_set with ls.
- unfold loc_alloc_argument; simpl; intuition congruence.
- rewrite B. apply AG; auto. auto. auto.
+ apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2).
+ auto. rewrite E. rewrite Locmap.gss. constructor.
+ auto.
+ apply agree_postcall_alloc with ls; auto.
(* Llabel *)
left; econstructor; split.
@@ -1106,7 +1262,8 @@ Proof.
intros [ls2 [A [B C]]].
left; econstructor; split.
eapply plus_right. eauto. eapply exec_Lcond_true; eauto.
- rewrite B. rewrite (agree_locs _ _ _ AG H5). auto.
+ rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+ eapply agree_locs; eauto.
apply find_label_transf_function; eauto.
traceEq.
econstructor; eauto.
@@ -1121,44 +1278,44 @@ Proof.
intros [ls2 [A [B C]]].
left; econstructor; split.
eapply plus_right. eauto. eapply exec_Lcond_false; eauto.
- rewrite B. rewrite (agree_locs _ _ _ AG H4). auto.
+ rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+ eapply agree_locs; eauto.
traceEq.
econstructor; eauto with coqlib.
apply agree_exten with ls; auto.
(* Lreturn *)
ExploitWT; inv WTI.
- unfold rs2, rs1; destruct or; simpl.
+ destruct or; simpl.
(* with an argument *)
exploit add_reload_correct.
intros [ls2 [A [B C]]].
left; econstructor; split.
eapply plus_right. eauto. eapply exec_Lreturn; eauto.
traceEq.
- econstructor; eauto.
- apply agree_return_regs; auto.
- eapply parent_locset_match; eauto.
- apply agree_set with ls.
- apply loc_result_acceptable.
- rewrite B. eapply agree_loc; eauto.
- auto. auto.
+ econstructor; eauto.
+ rewrite return_regs_result. rewrite B. apply agree_loc; auto.
+ apply return_regs_preserve.
+ apply Mem.free_lessdef; auto.
(* without an argument *)
left; econstructor; split.
apply plus_one. eapply exec_Lreturn; eauto.
econstructor; eauto.
- apply agree_return_regs; auto.
- eapply parent_locset_match; eauto.
+ apply return_regs_preserve.
+ apply Mem.free_lessdef; auto.
(* internal function *)
simpl in WT. inversion_clear WT. inversion H0. simpl in AG.
+ caseEq (alloc tm 0 (LTLin.fn_stacksize f)). intros tm' tstk TALLOC.
+ exploit Mem.alloc_lessdef; eauto. intros [P Q]. subst tstk.
destruct (parallel_move_parameters_correct tge s' (transf_function f)
(Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f)
- (transf_code f (LTLin.fn_code f)) (LTL.call_regs ls) m'
+ (transf_code f (LTLin.fn_code f)) (call_regs ls) tm'
wt_params wt_acceptable wt_norepet)
as [ls2 [A [B [C D]]]].
- assert (AG2: agree rs2 ls2).
- unfold rs2. eapply agree_set_parameters; eauto.
- unfold rs1. apply agree_call_regs; auto.
+ assert (AG2: agree (LTL.init_locs args (fn_params f)) ls2).
+ apply agree_init_locs; auto.
+ rewrite B. rewrite call_regs_parameters. auto.
left; econstructor; split.
eapply plus_left.
eapply exec_function_internal; eauto.
@@ -1166,15 +1323,14 @@ Proof.
econstructor; eauto with coqlib.
(* external function *)
+ exploit event_match_lessdef; eauto.
+ intros [res' [A B]].
left; econstructor; split.
apply plus_one. eapply exec_function_external; eauto.
- unfold args. symmetry. eapply agree_arguments_locs; auto.
econstructor; eauto.
- unfold rs1. apply agree_set with ls; auto.
- apply loc_result_acceptable.
- apply Locmap.gss.
- intros. apply Locmap.gso; auto.
- eapply agree_arguments_agree; eauto.
+ simpl. rewrite Locmap.gss. auto.
+ intros. rewrite Locmap.gso. auto.
+ simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save.
(* return *)
inv STACKS.
@@ -1183,8 +1339,10 @@ Proof.
eapply plus_left. eapply exec_return; eauto.
eauto. traceEq.
econstructor; eauto.
- unfold rs1. apply agree_set with ls; auto.
- rewrite B. apply AG. apply loc_result_acceptable.
+ apply agree_set with ls; auto.
+ rewrite B. auto.
+ unfold parent_locset in PRES.
+ apply agree_postcall_2 with ls0; auto.
Qed.
Lemma transf_initial_states:
@@ -1200,9 +1358,9 @@ Proof.
rewrite sig_preserved. auto.
replace (Genv.init_mem tprog) with (Genv.init_mem prog).
econstructor; eauto. constructor. rewrite H2; auto.
- red; intros. auto.
+ rewrite H2. simpl. constructor.
eapply Genv.find_funct_ptr_prop; eauto.
- symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
+ apply Mem.lessdef_refl. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
Qed.
Lemma transf_final_states:
@@ -1210,8 +1368,7 @@ Lemma transf_final_states:
match_states st1 st2 -> LTLin.final_state st1 r -> Linear.final_state st2 r.
Proof.
intros. inv H0. inv H. inv STACKS. econstructor.
- rewrite (agree_loc _ _ (R R3) AG). auto.
- simpl. intuition congruence.
+ unfold loc_result in AG. rewrite H in AG. inv AG. auto.
Qed.
Theorem transf_program_correct:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1759d7f..a9187ee 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -726,9 +726,9 @@ Lemma agree_return_regs:
(forall r,
In r int_callee_save_regs \/ In r float_callee_save_regs ->
rs' r = ls0 (R r)) ->
- (forall r, LTL.return_regs ls0 ls (R r) = rs' r).
+ (forall r, return_regs ls0 ls (R r) = rs' r).
Proof.
- intros; unfold LTL.return_regs.
+ intros; unfold return_regs.
case (In_dec Loc.eq (R r) temporaries); intro.
rewrite H0. eapply agree_reg; eauto.
apply int_callee_save_not_destroyed; auto.
@@ -778,10 +778,10 @@ Qed.
Lemma agree_callee_save_return_regs:
forall ls1 ls2,
- agree_callee_save (LTL.return_regs ls1 ls2) ls1.
+ agree_callee_save (return_regs ls1 ls2) ls1.
Proof.
intros; red; intros.
- unfold LTL.return_regs. destruct l; auto.
+ unfold return_regs. destruct l; auto.
generalize (int_callee_save_not_destroyed m); intro.
generalize (float_callee_save_not_destroyed m); intro.
destruct (In_dec Loc.eq (R m) temporaries). tauto.
@@ -988,7 +988,7 @@ Lemma save_callee_save_correct:
star step tge
(State stack tf sp (save_callee_save fe k) rs empty_frame m)
E0 (State stack tf sp k rs fr' m)
- /\ agree (LTL.call_regs ls) ls rs fr' cs.
+ /\ agree (call_regs ls) ls rs fr' cs.
Proof.
intros. unfold save_callee_save.
exploit save_callee_save_int_correct; eauto.
@@ -997,7 +997,7 @@ Proof.
intros [fr2 [A2 [B2 C2]]].
exists fr2.
split. eapply star_trans. eexact A1. eexact A2. traceEq.
- constructor; unfold LTL.call_regs; auto.
+ constructor; unfold call_regs; auto.
(* agree_local *)
intros. rewrite C2; auto with stacking.
rewrite C1; auto with stacking.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index cb0a6d8..cefad10 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -190,10 +190,10 @@ Definition tunneled_code (f: function) :=
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
| match_stackframes_intro:
- forall sig res f sp ls0 pc,
+ forall res f sp ls0 pc,
match_stackframes
- (Stackframe sig res f sp ls0 pc)
- (Stackframe sig res (tunnel_function f) sp ls0 (branch_target f pc)).
+ (Stackframe res f sp ls0 pc)
+ (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)).
Inductive match_states: state -> state -> Prop :=
| match_states_intro:
@@ -212,12 +212,6 @@ Inductive match_states: state -> state -> Prop :=
match_states (Returnstate s ls m)
(Returnstate ts ls m).
-Lemma parent_locset_match:
- forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = parent_locset s.
-Proof.
- induction 1; simpl; auto. inv H; auto.
-Qed.
-
(** To preserve non-terminating behaviours, we show that the transformed
code cannot take an infinity of "zero transition" cases.
We use the following [measure] function over source states,
@@ -286,32 +280,27 @@ Proof.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
econstructor; eauto.
(* Lcall *)
- unfold rs1. inv MS.
left; econstructor; split.
eapply exec_Lcall with (f' := tunnel_fundef f'); eauto.
rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
rewrite (tunnel_function_lookup _ _ _ H); simpl.
rewrite sig_preserved. auto.
apply find_function_translated; auto.
- rewrite sig_preserved; auto. fold rs1.
econstructor; eauto.
constructor; auto.
constructor; auto.
(* Ltailcall *)
- unfold rs2, rs1 in *. inv MS. fold rs1. fold rs2.
left; econstructor; split.
eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto.
rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
rewrite (tunnel_function_lookup _ _ _ H); simpl.
rewrite sig_preserved. auto.
apply find_function_translated; auto.
- rewrite sig_preserved; auto. fold rs1.
- rewrite (parent_locset_match _ _ H9).
econstructor; eauto.
(* Lalloc *)
rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
- left; exists (State ts (tunnel_function f) sp (branch_target f pc') rs3 m'); split.
- unfold rs3, rs2, rs1; eapply exec_Lalloc; eauto.
+ left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split.
+ eapply exec_Lalloc; eauto.
rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
econstructor; eauto.
(* cond *)
@@ -330,7 +319,7 @@ Proof.
left; econstructor; split.
eapply exec_Lreturn; eauto.
rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
- simpl. rewrite (parent_locset_match _ _ H7). constructor; auto.
+ simpl. constructor; auto.
(* internal function *)
simpl. left; econstructor; split.
eapply exec_function_internal; eauto.
@@ -343,7 +332,7 @@ Proof.
inv H3. inv H1.
left; econstructor; split.
eapply exec_return; eauto.
- fold rs1. constructor. auto.
+ constructor. auto.
Qed.
Lemma transf_initial_states:
@@ -351,7 +340,7 @@ Lemma transf_initial_states:
exists st2, initial_state tp st2 /\ match_states st1 st2.
Proof.
intros. inversion H.
- exists (Callstate nil (tunnel_fundef f) (Locmap.init Vundef) (Genv.init_mem tp)); split.
+ exists (Callstate nil (tunnel_fundef f) nil (Genv.init_mem tp)); split.
econstructor; eauto.
change (prog_main tp) with (prog_main p).
rewrite symbols_preserved. eauto.
@@ -366,7 +355,7 @@ Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
- intros. inv H0. inv H. inv H5. constructor. auto.
+ intros. inv H0. inv H. inv H4. constructor.
Qed.
Theorem transf_program_correct: