summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-27 07:34:38 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-27 07:34:38 +0000
commitcab28a5331400fee1a0dd1c5fa7d0366fa888f5f (patch)
tree907fff89969cd913604b11e134d3b83f6145db5c
parentb5325808cb1d36d4ff500d2fb754fe7a424e8329 (diff)
MAJ documentation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--.depend2
-rw-r--r--backend/Allocproof.v93
-rw-r--r--backend/LTL.v70
-rw-r--r--backend/LTLin.v12
-rw-r--r--backend/Linear.v34
-rw-r--r--backend/Reloadproof.v260
-rw-r--r--backend/Tunnelingproof.v2
7 files changed, 111 insertions, 362 deletions
diff --git a/.depend b/.depend
index cf24f7f..bc2750a 100644
--- a/.depend
+++ b/.depend
@@ -20,7 +20,7 @@ backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/
backend/Op.vo: backend/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo
backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo backend/Cminor.vo backend/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo
backend/Selection.vo: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo
-backend/Selectionproof.vo: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo backend/Selection.vo
+backend/Selectionproof.vo: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo backend/Selection.vo
backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo
backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Registers.vo
backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo backend/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index fd569ad..58ed3b6 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -35,92 +35,6 @@ Require Import Coloring.
Require Import Coloringproof.
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. *)
-
-Lemma call_regs_param_of_arg:
- forall sig ls l,
- In l (loc_arguments sig) ->
- LTL.call_regs ls (parameter_of_argument l) = ls l.
-Proof.
- intros.
- generalize (loc_arguments_acceptable sig l H).
- unfold LTL.call_regs; unfold parameter_of_argument.
- unfold loc_argument_acceptable.
- destruct l. auto. destruct s; tauto.
-Qed.
-
-(** The return value, stored in the conventional return register,
- is correctly passed from the callee back to the caller. *)
-
-Lemma return_regs_result:
- forall sig caller callee,
- LTL.return_regs caller callee (R (loc_result sig)) =
- callee (R (loc_result sig)).
-Proof.
- intros. unfold LTL.return_regs.
- case (In_dec Loc.eq (R (loc_result sig)) temporaries); intro.
- auto.
- case (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call); intro.
- auto.
- elim n0. apply loc_result_caller_save.
-Qed.
-
-(** Function arguments for a tail call are preserved by a
- [return_regs] operation. *)
-
-Lemma return_regs_arguments:
- forall sig caller callee,
- tailcall_possible sig ->
- map (LTL.return_regs caller callee) (loc_arguments sig) =
- map callee (loc_arguments sig).
-Proof.
- intros. apply list_map_exten; intros.
- generalize (H x H0). destruct x; intro.
- unfold LTL.return_regs.
- 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.
-
-(** Acceptable locations that are not destroyed at call keep
- their values across a call. *)
-
-Lemma return_regs_not_destroyed:
- forall caller callee l,
- Loc.notin l destroyed_at_call -> loc_acceptable l ->
- LTL.return_regs caller callee l = caller l.
-Proof.
- unfold loc_acceptable, LTL.return_regs.
- destruct l; auto.
- intros. case (In_dec Loc.eq (R m) temporaries); intro.
- contradiction.
- case (In_dec Loc.eq (R m) destroyed_at_call); intro.
- elim (Loc.notin_not_in _ _ H i).
- auto.
-Qed.
-
-(** Characterization of parallel assignments. *)
-
-Lemma parmov_spec:
- forall ls srcs dsts,
- Loc.norepet dsts -> List.length srcs = List.length dsts ->
- List.map (LTL.parmov srcs dsts ls) dsts = List.map ls srcs /\
- (forall l, Loc.notin l dsts -> LTL.parmov srcs dsts ls l = ls l).
-Proof.
- induction srcs; destruct dsts; simpl; intros; try discriminate.
- auto.
- inv H. inv H0. destruct (IHsrcs _ H4 H1). split.
- f_equal. apply Locmap.gss. rewrite <- H. apply list_map_exten; intros.
- 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 *)
(** We list here various properties of the locations [alloc r],
@@ -256,9 +170,8 @@ Proof.
red; intros. elim (Regset.empty_1 _ H4).
unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
Qed.
-
-(** Some useful special cases of [agree_increasing]. *)
+(** Some useful special cases of [agree_increasing]. *)
Lemma agree_reg_live:
forall r live rs ls,
@@ -423,7 +336,7 @@ Lemma agree_postcall:
(forall r,
Regset.In r live -> r <> res -> assign r <> assign res) ->
agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls ->
- agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)).
+ agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_locs ls)).
Proof.
intros.
assert (agree (reg_dead res live) rs ls).
@@ -433,7 +346,7 @@ Proof.
subst r. rewrite Locmap.gss. auto.
rewrite Locmap.gso. transitivity (ls (assign r)).
apply H2. apply Regset.remove_2; auto.
- unfold postcall_regs.
+ unfold postcall_locs.
assert (~In (assign r) temporaries).
apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto.
assert (~In (assign r) destroyed_at_call).
diff --git a/backend/LTL.v b/backend/LTL.v
index e39a4ec..6ee07f7 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -84,25 +84,12 @@ Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset :=
| _, _ => Locmap.init Vundef
end.
-
-Section RELSEM.
-
-(** [parmov srcs dsts ls] performs the parallel assignment
- of locations [dsts] to the values of the corresponding locations
- [srcs]. *)
-
-Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset :=
- match srcs, dsts with
- | s1 :: sl, d1 :: dl => Locmap.set d1 (ls s1) (parmov sl dl ls)
- | _, _ => ls
- end.
-
-(** [postcall_regs ls] returns the location set [ls] after a function
+(** [postcall_locs 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 :=
+Definition postcall_locs (ls: locset) : locset :=
fun (l: loc) =>
match l with
| R r =>
@@ -147,6 +134,9 @@ Inductive state : Set :=
(m: mem), (**r memory state *)
state.
+
+Section RELSEM.
+
Variable ge: genv.
Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
@@ -159,46 +149,12 @@ Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
end
end.
-(** The main difference between the LTL transition relation
- and the RTL transition relation is the handling of function calls.
- In RTL, arguments and results to calls are transmitted via
- [vargs] and [vres] components of [Callstate] and [Returnstate],
- respectively. The semantics takes care of transferring these values
- between the pseudo-registers of the caller and of the callee.
-
- In lower-level intermediate languages (e.g [Linear], [Mach], [PPC]),
- arguments and results are transmitted implicitly: the generated
- code for the caller arranges for arguments to be left in conventional
- registers and stack locations, as determined by the calling conventions,
- where the function being called will find them. Similarly,
- conventional registers will be used to pass the result value back
- to the caller.
-
- In LTL, we take an hybrid view of argument and result passing.
- The LTL code does not contain (yet) instructions for moving
- arguments and results to the conventional registers. However,
- the dynamic semantics "goes through the motions" of such code:
-- The [exec_Lcall] transition from [State] to [Callstate]
- leaves the values of arguments in the conventional locations
- given by [loc_arguments].
-- The [exec_function_internal] transition from [Callstate] to [State]
- changes the view of stack slots ([Outgoing] slots slide to
- [Incoming] slots as per [call_regs]), then recovers the
- values of parameters from the conventional locations given by
- [loc_parameters].
-- The [exec_Lreturn] transition from [State] to [Returnstate]
- moves the result value to the conventional location [loc_result],
- then restores the values of callee-save locations from
- the location state of the caller, using [return_regs].
-- The [exec_return] transition from [Returnstate] to [State]
- reads the result value from the conventional location [loc_result],
- then stores it in the result location for the [Lcall] instruction.
-
-This complicated protocol will make it much easier to prove
-the correctness of the [Stacking] pass later, which inserts actual
-code that performs all the shuffling of arguments and results
-described above.
-*)
+(** The LTL transition relation is very similar to that of RTL,
+ with locations being used in place of pseudo-registers.
+ The main difference is for the [call] instruction: caller-save
+ registers are set to [Vundef] across the call, using the [postcall_locs]
+ function defined above. This forces the LTL producer to avoid
+ storing values live across the call in a caller-save register. *)
Inductive step: state -> trace -> state -> Prop :=
| exec_Lnop:
@@ -232,7 +188,7 @@ Inductive step: state -> trace -> state -> Prop :=
find_function ros rs = Some f' ->
funsig f' = sig ->
step (State s f sp pc rs m)
- E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s)
+ E0 (Callstate (Stackframe res f sp (postcall_locs rs) pc' :: s)
f' (List.map rs args) m)
| exec_Ltailcall:
forall s f stk pc rs m sig ros args f',
@@ -247,7 +203,7 @@ Inductive step: state -> trace -> state -> Prop :=
rs arg = Vint sz ->
Mem.alloc m 0 (Int.signed sz) = (m', b) ->
step (State s f sp pc rs m)
- E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m')
+ E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs 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) ->
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 83787ce..fae6417 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -140,14 +140,6 @@ Inductive state : Set :=
(m: mem), (**r memory state *)
state.
-(*
-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.
Variable ge: genv.
@@ -185,7 +177,7 @@ Inductive step: state -> trace -> state -> Prop :=
find_function ros rs = Some f' ->
sig = funsig f' ->
step (State s f sp (Lcall sig ros args res :: b) rs m)
- E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s)
+ E0 (Callstate (Stackframe res f sp (postcall_locs rs) b :: s)
f' (List.map rs args) m)
| exec_Ltailcall:
forall s f stk sig ros args b rs m f',
@@ -198,7 +190,7 @@ Inductive step: state -> trace -> state -> Prop :=
rs arg = Vint sz ->
Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
step (State s f sp (Lalloc arg res :: b) rs m)
- E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m')
+ E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m')
| exec_Llabel:
forall s f sp lbl b rs m,
step (State s f sp (Llabel lbl :: b) rs m)
diff --git a/backend/Linear.v b/backend/Linear.v
index ca1a2bc..900b6a5 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -202,6 +202,40 @@ Definition parent_locset (stack: list stackframe) : locset :=
| Stackframe f sp ls c :: stack' => ls
end.
+(** The main difference between the Linear transition relation
+ and the LTL transition relation is the handling of function calls.
+ In LTL, arguments and results to calls are transmitted via
+ [vargs] and [vres] components of [Callstate] and [Returnstate],
+ respectively. The semantics takes care of transferring these values
+ between the locations of the caller and of the callee.
+
+ In Linear and lower-level languages (Mach, PPC), arguments and
+ results are transmitted implicitly: the generated code for the
+ caller arranges for arguments to be left in conventional registers
+ and stack locations, as determined by the calling conventions, where
+ the function being called will find them. Similarly, conventional
+ registers will be used to pass the result value back to the caller.
+ This is reflected in the definition of [Callstate] and [Returnstate]
+ above, where a whole location state [rs] is passed instead of just
+ the values of arguments or returns as in LTL.
+
+ These location states passed across calls are treated in a way that
+ reflects the callee-save/caller-save convention:
+- The [exec_Lcall] transition from [State] to [Callstate]
+ saves the current location state [ls] in the call stack,
+ and passes it to the callee.
+- The [exec_function_internal] transition from [Callstate] to [State]
+ changes the view of stack slots ([Outgoing] slots slide to
+ [Incoming] slots as per [call_regs]).
+- The [exec_Lreturn] transition from [State] to [Returnstate]
+ restores the values of callee-save locations from
+ the location state of the caller, using [return_regs].
+
+This protocol makes it much easier to later prove the correctness of
+the [Stacking] pass, which inserts actual code that performs the
+saving and restoring of callee-save registers described above.
+*)
+
Inductive step: state -> trace -> state -> Prop :=
| exec_Lgetstack:
forall s f sp sl r b rs m,
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 372a261..3177eaf 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -410,8 +410,19 @@ End LINEAR_CONSTRUCTORS.
(** * Agreement between values of locations *)
(** The predicate [agree] states that two location maps
- give the same values to all acceptable locations,
- that is, non-temporary registers and [Local] stack slots. *)
+ give compatible values to all acceptable locations,
+ that is, non-temporary registers and [Local] stack slots.
+ The notion of compatibility used is the [Val.lessdef] ordering,
+ which enables a [Vundef] value in the original program to be refined
+ into any value in the transformed program.
+
+ A typical situation where this refinement of values occurs is at
+ function entry point. In LTLin, all registers except those
+ belonging to the function parameters are set to [Vundef]. In
+ Linear, these registers have whatever value they had in the caller
+ function. This difference is harmless: if the original LTLin code
+ does not get stuck, we know that it does not use any of these
+ [Vundef] values. *)
Definition agree (rs1 rs2: locset) : Prop :=
forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
@@ -425,7 +436,8 @@ Qed.
Lemma agree_locs:
forall rs1 rs2 ll,
- agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll).
+ agree rs1 rs2 -> locs_acceptable ll ->
+ Val.lessdef_list (map rs1 ll) (map rs2 ll).
Proof.
induction ll; simpl; intros.
constructor.
@@ -458,175 +470,6 @@ Proof.
apply temporaries_not_acceptable; auto.
Qed.
-(*****
-Lemma agree_return_regs:
- forall rs1 ls1 rs2 ls2,
- agree rs1 ls1 -> agree rs2 ls2 ->
- agree (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2).
-Proof.
- intros; red; intros. unfold LTL.return_regs.
- assert (~In l temporaries).
- apply Loc.notin_not_in. apply temporaries_not_acceptable; auto.
- destruct l.
- destruct (In_dec Loc.eq (R m) temporaries). contradiction.
- destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
- auto.
-Qed.
-
-Lemma agree_set_result:
- forall rs1 ls1 rs2 ls2 sig res ls3,
- loc_acceptable res -> agree rs1 ls1 -> agree rs2 ls2 ->
- ls3 res = LTL.return_regs ls1 ls2 (R (loc_result sig)) ->
- (forall l : loc, Loc.diff res l -> ls3 l = LTL.return_regs ls1 ls2 l) ->
- let rs_merge := LTL.return_regs rs1 rs2 in
- agree (Locmap.set res (rs_merge (R (loc_result sig))) rs_merge) ls3.
-Proof.
- intros. apply agree_set with (LTL.return_regs ls1 ls2); auto.
- rewrite H2; unfold rs_merge.
- repeat rewrite return_regs_result. apply H1. apply loc_result_acceptable.
- unfold rs_merge. apply agree_return_regs; auto.
-Qed.
-
-(** [agree_arguments] and [agree_parameters] are two stronger
- variants of the predicate [agree]. They additionally demand
- equality of the values of locations that are arguments or parameters
- (respectively) for a call to a function of signature [sg]. *)
-
-Definition agree_arguments (sg: signature) (rs1 rs2: locset) : Prop :=
- forall l, loc_acceptable l \/ In l (loc_arguments sg) -> rs2 l = rs1 l.
-
-Definition agree_parameters (sg: signature) (rs1 rs2: locset) : Prop :=
- forall l, loc_acceptable l \/ In l (loc_parameters sg) -> rs2 l = rs1 l.
-
-Remark parallel_assignment:
- forall (P: loc -> Prop) (rs1 rs2 ls1 ls2: locset) srcs dsts,
- map rs2 dsts = map rs1 srcs ->
- map ls2 dsts = map ls1 srcs ->
- (forall l, In l srcs -> P l) ->
- (forall l, P l -> ls1 l = rs1 l) ->
- (forall l, In l dsts -> ls2 l = rs2 l).
-Proof.
- induction srcs; destruct dsts; simpl; intros; try congruence.
- contradiction.
- inv H; inv H0. elim H3; intro. subst l0.
- rewrite H5; rewrite H4. auto with coqlib.
- eapply IHsrcs; eauto.
-Qed.
-
-Lemma agree_set_arguments:
- forall rs1 ls1 ls2 args sg,
- agree rs1 ls1 ->
- List.map Loc.type args = sg.(sig_args) ->
- locs_acceptable args ->
- List.map ls2 (loc_arguments sg) = map ls1 args ->
- (forall l : loc,
- Loc.notin l (loc_arguments sg) ->
- Loc.notin l temporaries -> ls2 l = ls1 l) ->
- agree_arguments sg (LTL.parmov args (loc_arguments sg) rs1) ls2.
-Proof.
- intros.
- assert (Loc.norepet (loc_arguments sg)).
- apply loc_arguments_norepet.
- assert (List.length args = List.length (loc_arguments sg)).
- rewrite loc_arguments_length. rewrite <- H0.
- symmetry. apply list_length_map.
- destruct (parmov_spec rs1 _ _ H4 H5) as [A B].
- set (rs2 := LTL.parmov args (loc_arguments sg) rs1) in *.
- assert (forall l, In l (loc_arguments sg) -> ls2 l = rs2 l).
- intros.
- eapply parallel_assignment with (P := loc_acceptable); eauto.
- red; intros.
- destruct (In_dec Loc.eq l (loc_arguments sg)).
- auto.
- assert (loc_acceptable l) by tauto.
- assert (Loc.notin l (loc_arguments sg)).
- eapply loc_acceptable_notin_notin; eauto.
- rewrite H3; auto. rewrite B; auto.
- apply temporaries_not_acceptable; auto.
-Qed.
-
-Lemma agree_arguments_agree:
- forall sg rs ls, agree_arguments sg rs ls -> agree rs ls.
-Proof.
- intros; red; intros; auto.
-Qed.
-
-Lemma agree_arguments_locs:
- forall sg rs1 rs2,
- agree_arguments sg rs1 rs2 ->
- map rs2 (loc_arguments sg) = map rs1 (loc_arguments sg).
-Proof.
- intros.
- assert (forall ll, incl ll (loc_arguments sg) -> map rs2 ll = map rs1 ll).
- induction ll; simpl; intros. auto.
- f_equal. apply H. right. apply H0. auto with coqlib.
- apply IHll. eapply incl_cons_inv; eauto.
- apply H0. apply incl_refl.
-Qed.
-
-Lemma agree_set_parameters:
- forall rs1 ls1 ls2 sg params,
- agree_parameters sg rs1 ls1 ->
- List.map Loc.type params = sg.(sig_args) ->
- locs_acceptable params ->
- Loc.norepet params ->
- List.map ls2 params = List.map ls1 (loc_parameters sg) ->
- (forall l : loc,
- Loc.notin l params ->
- Loc.notin l temporaries -> ls2 l = ls1 l) ->
- agree (LTL.parmov (loc_parameters sg) params rs1) ls2.
-Proof.
- intros.
- assert (List.length (loc_parameters sg) = List.length params).
- unfold loc_parameters. rewrite list_length_map.
- rewrite loc_arguments_length. rewrite <- H0.
- apply list_length_map.
- destruct (parmov_spec rs1 _ _ H2 H5) as [A B].
- set (rs2 := LTL.parmov (loc_parameters sg) params rs1) in *.
- red; intros.
- assert (forall l, In l params -> ls2 l = rs2 l).
- intros.
- eapply parallel_assignment with (P := fun l => In l (loc_parameters sg)); eauto.
- destruct (In_dec Loc.eq l params).
- auto.
- assert (Loc.notin l params).
- eapply loc_acceptable_notin_notin; eauto.
- rewrite B; auto. rewrite H4; auto.
- apply temporaries_not_acceptable; auto.
-Qed.
-
-Lemma agree_call_regs:
- forall sg rs ls,
- agree_arguments sg rs ls ->
- agree_parameters sg (LTL.call_regs rs) (LTL.call_regs ls).
-Proof.
- intros; red; intros. elim H0.
- destruct l; simpl; auto. destruct s; auto.
- unfold loc_parameters. intro.
- destruct (list_in_map_inv _ _ _ H1) as [r [A B]].
- subst l. generalize (loc_arguments_acceptable _ _ B).
- destruct r; simpl; auto. destruct s; simpl; auto.
-Qed.
-
-Lemma agree_arguments_return_regs:
- forall sg rs1 rs2 ls1 ls2,
- tailcall_possible sg ->
- agree rs1 ls1 ->
- agree_arguments sg rs2 ls2 ->
- agree_arguments sg (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2).
-Proof.
- intros; red; intros. generalize (H1 l H2). intro.
- elim H2; intro. generalize (H0 l H4); intro.
- unfold LTL.return_regs. destruct l; auto.
- destruct (In_dec Loc.eq (R m) temporaries); auto.
- destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
- generalize (H l H4). unfold LTL.return_regs; destruct l; intro.
- destruct (In_dec Loc.eq (R m) temporaries); auto.
- 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 ->
@@ -643,9 +486,9 @@ Qed.
Lemma agree_postcall_1:
forall rs ls,
agree rs ls ->
- agree (LTL.postcall_regs rs) ls.
+ agree (LTL.postcall_locs rs) ls.
Proof.
- intros; red; intros. unfold LTL.postcall_regs.
+ intros; red; intros. unfold LTL.postcall_locs.
destruct l; auto.
destruct (In_dec Loc.eq (R m) temporaries). constructor.
destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor.
@@ -654,11 +497,13 @@ 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'.
+ agree (LTL.postcall_locs rs) ls ->
+ (forall l,
+ loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries ->
+ ls' l = ls l) ->
+ agree (LTL.postcall_locs rs) ls'.
Proof.
- intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs.
+ intros; red; intros. generalize (H l H1). unfold LTL.postcall_locs.
destruct l.
destruct (In_dec Loc.eq (R m) temporaries). intro; constructor.
destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor.
@@ -671,8 +516,10 @@ 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'.
+ (forall l,
+ Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries ->
+ ls' l = ls l) ->
+ agree (LTL.postcall_locs rs) ls'.
Proof.
intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
intros. apply H0.
@@ -686,7 +533,7 @@ 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).
+ agree (LTL.postcall_locs 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)).
@@ -713,8 +560,7 @@ Qed.
Lemma call_regs_parameters:
forall ls sig,
- map (call_regs ls) (loc_parameters sig) =
- map ls (loc_arguments 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.
@@ -725,12 +571,24 @@ Proof.
destruct s; intros; try contradiction. auto.
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.
+
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.
+ intros. 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.
@@ -748,18 +606,6 @@ Proof.
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 *)
Lemma find_label_add_spill:
@@ -899,13 +745,22 @@ Qed.
it enforces are:
- Agreement between the values of locations in the two programs,
according to the [agree] or [agree_arguments] predicates.
+- Agreement between the memory states of the two programs,
+ according to the [Mem.lessdef] predicate.
- Lists of LTLin instructions appearing in the source state
are always suffixes of the code for the corresponding functions.
- Well-typedness of the source code, which ensures that
only acceptable locations are accessed by this code.
+- Agreement over return types during calls: the return type of a function
+ is always equal to the return type of the signature of the corresponding
+ call. This invariant is necessary since the conventional location
+ used for passing return values depend on the return type. This invariant
+ is enforced through the third parameter of the [match_stackframes]
+ predicate, which is the signature of the called function.
*)
-Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
+Inductive match_stackframes:
+ list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
| match_stackframes_nil:
forall sig,
sig.(sig_res) = Some Tint ->
@@ -914,13 +769,14 @@ Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe ->
forall res f sp c rs s s' c' ls sig,
match_stackframes s s' (LTLin.fn_sig f) ->
c' = add_spill (loc_result sig) res (transf_code f c) ->
- agree (LTL.postcall_regs rs) ls ->
+ agree (LTL.postcall_locs rs) ls ->
loc_acceptable res ->
wt_function f ->
is_tail c (LTLin.fn_code f) ->
- match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s)
- (Linear.Stackframe (transf_function f) sp ls c' :: s')
- sig.
+ match_stackframes
+ (LTLin.Stackframe res f sp (LTL.postcall_locs rs) c :: s)
+ (Linear.Stackframe (transf_function f) sp ls c' :: s')
+ sig.
Inductive match_states: LTLin.state -> Linear.state -> Prop :=
| match_states_intro:
@@ -992,8 +848,6 @@ 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'),
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index cefad10..7ad75ba 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -299,7 +299,7 @@ Proof.
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') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split.
+ left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split.
eapply exec_Lalloc; eauto.
rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
econstructor; eauto.