aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asm.v51
-rw-r--r--arm/Asmgenproof.v6
-rw-r--r--arm/Conventions1.v262
-rw-r--r--backend/Allocation.v77
-rw-r--r--backend/Allocproof.v302
-rw-r--r--backend/Asmgenproof0.v60
-rw-r--r--backend/CleanupLabelsproof.v4
-rw-r--r--backend/Conventions.v48
-rw-r--r--backend/Debugvarproof.v4
-rw-r--r--backend/LTL.v11
-rw-r--r--backend/Linear.v11
-rw-r--r--backend/Linearizeproof.v4
-rw-r--r--backend/Lineartyping.v22
-rw-r--r--backend/Locations.v34
-rw-r--r--backend/Mach.v31
-rw-r--r--backend/RTLtyping.v6
-rw-r--r--backend/Regalloc.ml74
-rw-r--r--backend/Stackingproof.v119
-rw-r--r--backend/Tunnelingproof.v4
-rw-r--r--backend/XTL.ml5
-rw-r--r--backend/XTL.mli1
-rw-r--r--cfrontend/PrintClight.ml2
-rw-r--r--cfrontend/PrintCsyntax.ml4
-rw-r--r--common/AST.v57
-rw-r--r--common/Events.v187
-rwxr-xr-xconfigure2
-rw-r--r--ia32/Asm.v52
-rw-r--r--ia32/Asmgenproof.v6
-rw-r--r--ia32/Conventions1.v123
-rw-r--r--powerpc/Asm.v51
-rw-r--r--powerpc/Asmgenproof.v6
-rw-r--r--powerpc/Conventions1.v156
32 files changed, 888 insertions, 894 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index b350b047..010d5d7b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -310,12 +310,12 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
Definition undef_flags (rs: regset) : regset :=
fun r => match r with CR _ => Vundef | _ => rs r end.
-(** Assigning multiple registers *)
+(** Assigning a register pair *)
-Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
- match rl, vl with
- | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
- | _, _ => rs
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+ match p with
+ | One r => rs#r <- v
+ | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
end.
(** Assigning the result of a builtin *)
@@ -813,12 +813,21 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
(Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
extcall_arg rs m (S Outgoing ofs ty) v.
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+ | extcall_arg_one: forall l v,
+ extcall_arg rs m l v ->
+ extcall_arg_pair rs m (One l) v
+ | extcall_arg_twolong: forall hi lo vhi vlo,
+ extcall_arg rs m hi vhi ->
+ extcall_arg rs m lo vlo ->
+ extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
Definition extcall_arguments
(rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
- list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
+ list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
-Definition loc_external_result (sg: signature) : list preg :=
- map preg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : rpair preg :=
+ map_rpair preg_of (loc_result sg).
(** Execution of the instruction at [rs#PC]. *)
@@ -848,9 +857,9 @@ Inductive step: state -> trace -> state -> Prop :=
forall b ef args res rs m t rs' m',
rs PC = Vptr b Int.zero ->
Genv.find_funct_ptr ge b = Some (External ef) ->
- external_call' ef ge args m t res m' ->
+ external_call ef ge args m t res m' ->
extcall_arguments rs m (ef_sig ef) args ->
- rs' = (set_regs (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) ->
+ rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) ->
step (State rs m) t (State rs' m').
End RELSEM.
@@ -884,13 +893,21 @@ Remark extcall_arguments_determ:
extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
intros until m.
- assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 ->
- forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
+ assert (A: forall l v1 v2,
+ extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
+ { intros. inv H; inv H0; congruence. }
+ assert (B: forall p v1 v2,
+ extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
+ { intros. inv H; inv H0.
+ eapply A; eauto.
+ f_equal; eapply A; eauto. }
+ assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
+ forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
+ {
induction 1; intros vl2 EA; inv EA.
auto.
- f_equal; auto.
- inv H; inv H3; congruence.
- intros. red in H0; red in H1. eauto.
+ f_equal; eauto. }
+ intros. eapply C; eauto.
Qed.
Lemma semantics_determinate: forall p, determinate (semantics p).
@@ -911,13 +928,13 @@ Ltac Equalities :=
exploit external_call_determ. eexact H5. eexact H11. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
- exploit external_call_determ'. eexact H3. eexact H8. intros [A B].
+ exploit external_call_determ. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
(* trace length *)
red; intros; inv H; simpl.
omega.
inv H3; eapply external_call_trace_length; eauto.
- inv H2; eapply external_call_trace_length; eauto.
+ eapply external_call_trace_length; eauto.
(* initial states *)
inv H; inv H0. f_equal. congruence.
(* final no step *)
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index eb52d16e..5bd2b54f 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -892,14 +892,14 @@ Opaque loadind.
intros [tf [A B]]. simpl in B. inv B.
exploit extcall_arguments_match; eauto.
intros [args' [C D]].
- exploit external_call_mem_extends'; eauto.
+ exploit external_call_mem_extends; eauto.
intros [res' [m2' [P [Q [R S]]]]].
left; econstructor; split.
apply plus_one. eapply exec_step_external; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto.
apply agree_set_other; auto with asmgen.
- eapply agree_set_mregs; eauto.
+ eapply agree_set_pair; eauto.
- (* return *)
inv STACKS. simpl in *.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index abd28b18..3eae50ef 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -88,33 +88,43 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
so we have code in [arm/PrintAsm.ml] that inserts additional moves
to/from [F0]. *)
-Definition loc_result (s: signature) : list mreg :=
+Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
- | None => R0 :: nil
- | Some (Tint | Tany32) => R0 :: nil
- | Some (Tfloat | Tsingle | Tany64) => F0 :: nil
- | Some Tlong => R1 :: R0 :: nil
+ | None => One R0
+ | Some (Tint | Tany32) => One R0
+ | Some (Tfloat | Tsingle | Tany64) => One F0
+ | Some Tlong => Twolong R1 R0
end.
(** The result registers have types compatible with that given in the signature. *)
Lemma loc_result_type:
forall sig,
- subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true.
+ subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
Qed.
(** The result locations are caller-save registers *)
Lemma loc_result_caller_save:
- forall (s: signature) (r: mreg),
- In r (loc_result s) -> is_callee_save r = false.
+ forall (s: signature),
+ forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- assert (r = R0 \/ r = R1 \/ r = F0).
- unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
- destruct H0 as [A | [A | A]]; subst r; auto.
+ unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+Qed.
+
+(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
+
+Lemma loc_result_pair:
+ forall sg,
+ match loc_result sg with
+ | One _ => True
+ | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+ end.
+Proof.
+ intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence.
Qed.
(** ** Location of function arguments *)
@@ -149,28 +159,28 @@ Definition freg_param (n: Z) : mreg :=
match list_nth_z float_param_regs n with Some r => r | None => F0 end.
Fixpoint loc_arguments_hf
- (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc :=
+ (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| (Tint | Tany32) as ty :: tys =>
if zlt ir 4
- then R (ireg_param ir) :: loc_arguments_hf tys (ir + 1) fr ofs
- else S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 1)
+ then One (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 1) fr ofs
+ else One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 1)
| (Tfloat | Tany64) as ty :: tys =>
if zlt fr 8
- then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs
+ then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs
else let ofs := align ofs 2 in
- S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 2)
+ One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 2)
| Tsingle :: tys =>
if zlt fr 8
- then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs
- else S Outgoing ofs Tsingle :: loc_arguments_hf tys ir fr (ofs + 1)
+ then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs
+ else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1)
| Tlong :: tys =>
let ir := align ir 2 in
if zlt ir 4
- then R (ireg_param (ir + 1)) :: R (ireg_param ir) :: loc_arguments_hf tys (ir + 2) fr ofs
+ then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs
else let ofs := align ofs 2 in
- S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_hf tys ir fr (ofs + 2)
+ Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2)
end.
(** For the "softfloat" configuration, as well as for variable-argument functions
@@ -194,30 +204,30 @@ we insert additional code around function calls and returns that moves
data appropriately. *)
Fixpoint loc_arguments_sf
- (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
+ (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| (Tint|Tany32) as ty :: tys =>
- (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty)
+ One (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty)
:: loc_arguments_sf tys (ofs + 1)
| (Tfloat|Tany64) as ty :: tys =>
let ofs := align ofs 2 in
- (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty)
+ One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty)
:: loc_arguments_sf tys (ofs + 2)
| Tsingle :: tys =>
- (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle)
+ One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle)
:: loc_arguments_sf tys (ofs + 1)
| Tlong :: tys =>
let ofs := align ofs 2 in
- (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint)
- :: (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint)
+ Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint)
+ (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint)
:: loc_arguments_sf tys (ofs + 2)
end.
(** [loc_arguments s] returns the list of locations where to store arguments
when calling a function with signature [s]. *)
-Definition loc_arguments (s: signature) : list loc :=
+Definition loc_arguments (s: signature) : list (rpair loc) :=
match Archi.abi with
| Archi.Softfloat =>
loc_arguments_sf s.(sig_args) (-4)
@@ -279,185 +289,151 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
| _ => False
end.
-Remark ireg_param_in_params: forall n, In (ireg_param n) int_param_regs.
+Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
+ match l with
+ | R r => is_callee_save r = false
+ | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
+ | _ => False
+ end.
+
+Remark ireg_param_caller_save: forall n, is_callee_save (ireg_param n) = false.
Proof.
unfold ireg_param; intros.
+ assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
destruct (list_nth_z int_param_regs n) as [r|] eqn:NTH.
- eapply list_nth_z_in; eauto.
- simpl; auto.
+ apply A. eapply list_nth_z_in; eauto.
+ auto.
Qed.
-Remark freg_param_in_params: forall n, In (freg_param n) float_param_regs.
+Remark freg_param_caller_save: forall n, is_callee_save (freg_param n) = false.
Proof.
unfold freg_param; intros.
+ assert (A: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
destruct (list_nth_z float_param_regs n) as [r|] eqn:NTH.
- eapply list_nth_z_in; eauto.
- simpl; auto.
+ apply A. eapply list_nth_z_in; eauto.
+ auto.
Qed.
Remark loc_arguments_hf_charact:
- forall tyl ir fr ofs l,
- In l (loc_arguments_hf tyl ir fr ofs) ->
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
- | S _ _ _ => False
- end.
+ forall tyl ir fr ofs p,
+ In p (loc_arguments_hf tyl ir fr ofs) -> forall_rpair (loc_argument_charact ofs) p.
Proof.
- assert (INCR: forall l ofs1 ofs2,
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= ofs2 /\ typealign ty = 1
- | S _ _ _ => False
- end ->
- ofs1 <= ofs2 ->
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= ofs1 /\ typealign ty = 1
- | S _ _ _ => False
- end).
- {
- intros. destruct l; auto. destruct sl; auto. intuition omega.
- }
+ assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
+ { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+ assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
+ { destruct p; simpl; intuition eauto. }
induction tyl; simpl loc_arguments_hf; intros.
elim H.
destruct a.
- (* int *)
destruct (zlt ir 4); destruct H.
- subst. left; apply ireg_param_in_params.
+ subst. apply ireg_param_caller_save.
eapply IHtyl; eauto.
subst. split; [omega | auto].
- eapply INCR. eapply IHtyl; eauto. omega.
+ eapply Y; eauto. omega.
- (* float *)
destruct (zlt fr 8); destruct H.
- subst. right; apply freg_param_in_params.
+ subst. apply freg_param_caller_save.
eapply IHtyl; eauto.
subst. split. apply Zle_ge. apply align_le. omega. auto.
- eapply INCR. eapply IHtyl; eauto.
- apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
+ eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
- (* long *)
set (ir' := align ir 2) in *.
assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (zlt ir' 4).
- destruct H. subst l; left; apply ireg_param_in_params.
- destruct H. subst l; left; apply ireg_param_in_params.
+ destruct H. subst p. split; apply ireg_param_caller_save.
eapply IHtyl; eauto.
- destruct H. subst l; split; [ omega | auto ].
- destruct H. subst l; split; [ omega | auto ].
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct H. subst p. split; (split; [ omega | auto ]).
+ eapply Y. eapply IHtyl; eauto. omega.
- (* single *)
destruct (zlt fr 8); destruct H.
- subst. right; apply freg_param_in_params.
+ subst. apply freg_param_caller_save.
eapply IHtyl; eauto.
- subst. split; [omega | auto].
- eapply INCR. eapply IHtyl; eauto. omega.
+ subst. split; [omega|auto].
+ eapply Y; eauto. omega.
- (* any32 *)
destruct (zlt ir 4); destruct H.
- subst. left; apply ireg_param_in_params.
+ subst. apply ireg_param_caller_save.
eapply IHtyl; eauto.
subst. split; [omega | auto].
- eapply INCR. eapply IHtyl; eauto. omega.
+ eapply Y; eauto. omega.
- (* any64 *)
destruct (zlt fr 8); destruct H.
- subst. right; apply freg_param_in_params.
+ subst. apply freg_param_caller_save.
eapply IHtyl; eauto.
subst. split. apply Zle_ge. apply align_le. omega. auto.
- eapply INCR. eapply IHtyl; eauto.
- apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
+ eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
Qed.
Remark loc_arguments_sf_charact:
- forall tyl ofs l,
- In l (loc_arguments_sf tyl ofs) ->
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ typealign ty = 1
- | S _ _ _ => False
- end.
+ forall tyl ofs p,
+ In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p.
Proof.
- assert (INCR: forall l ofs1 ofs2,
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ typealign ty = 1
- | S _ _ _ => False
- end ->
- ofs1 <= ofs2 ->
- match l with
- | R r => In r int_param_regs \/ In r float_param_regs
- | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ typealign ty = 1
- | S _ _ _ => False
- end).
- {
- intros. destruct l; auto. destruct sl; auto. intuition xomega.
- }
+ assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l).
+ { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. }
+ assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p).
+ { destruct p; simpl; intuition eauto. }
induction tyl; simpl loc_arguments_sf; intros.
elim H.
destruct a.
- (* int *)
destruct H.
- destruct (zlt ofs 0); subst l.
- left; apply ireg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs 0); subst p.
+ apply ireg_param_caller_save.
+ split; [xomega|auto].
+ eapply Y; eauto. omega.
- (* float *)
set (ofs' := align ofs 2) in *.
assert (ofs <= ofs') by (apply align_le; omega).
destruct H.
- destruct (zlt ofs' 0); subst l.
- right; apply freg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs' 0); subst p.
+ apply freg_param_caller_save.
+ split; [xomega|auto].
+ eapply Y. eapply IHtyl; eauto. omega.
- (* long *)
set (ofs' := align ofs 2) in *.
assert (ofs <= ofs') by (apply align_le; omega).
destruct H.
- destruct (zlt ofs' 0); subst l.
- left; apply ireg_param_in_params.
- split. xomega. auto.
- destruct H.
- destruct (zlt ofs' 0); subst l.
- left; apply ireg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs' 0); subst p.
+ split; apply ireg_param_caller_save.
+ split; (split; [xomega|auto]).
+ eapply Y. eapply IHtyl; eauto. omega.
- (* single *)
destruct H.
- destruct (zlt ofs 0); subst l.
- right; apply freg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs 0); subst p.
+ apply freg_param_caller_save.
+ split; [xomega|auto].
+ eapply Y; eauto. omega.
- (* any32 *)
destruct H.
- destruct (zlt ofs 0); subst l.
- left; apply ireg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs 0); subst p.
+ apply ireg_param_caller_save.
+ split; [xomega|auto].
+ eapply Y; eauto. omega.
- (* any64 *)
set (ofs' := align ofs 2) in *.
assert (ofs <= ofs') by (apply align_le; omega).
destruct H.
- destruct (zlt ofs' 0); subst l.
- right; apply freg_param_in_params.
- split. xomega. auto.
- eapply INCR. eapply IHtyl; eauto. omega.
+ destruct (zlt ofs' 0); subst p.
+ apply freg_param_caller_save.
+ split; [xomega|auto].
+ eapply Y. eapply IHtyl; eauto. omega.
Qed.
Lemma loc_arguments_acceptable:
- forall (s: signature) (l: loc),
- In l (loc_arguments s) -> loc_argument_acceptable l.
+ forall (s: signature) (p: rpair loc),
+ In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
Proof.
unfold loc_arguments; intros.
- assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
- assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
- assert (C: forall r, In r int_param_regs \/ In r float_param_regs -> is_callee_save r = false).
- { intros. destruct H0; auto. }
- assert (In l (loc_arguments_sf (sig_args s) (-4)) -> loc_argument_acceptable l).
- { intros. red. exploit loc_arguments_sf_charact; eauto.
- destruct l as [r | [] ofs ty]; auto.
- intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. }
- assert (In l (loc_arguments_hf (sig_args s) 0 0 0) -> loc_argument_acceptable l).
- { intros. red. exploit loc_arguments_hf_charact; eauto.
- destruct l as [r | [] ofs ty]; auto.
- intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. }
+ assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
+ { unfold loc_argument_charact, loc_argument_acceptable.
+ destruct l as [r | [] ofs ty]; auto. intros (A & B); split; auto. rewrite B; apply Z.divide_1_l. }
+ assert (Y: forall p, forall_rpair (loc_argument_charact 0) p -> forall_rpair loc_argument_acceptable p).
+ { destruct p0; simpl; intuition auto. }
+ assert (In p (loc_arguments_sf (sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p).
+ { intros. exploit loc_arguments_sf_charact; eauto. }
+ assert (In p (loc_arguments_hf (sig_args s) 0 0 0) -> forall_rpair loc_argument_acceptable p).
+ { intros. exploit loc_arguments_hf_charact; eauto. }
destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
Qed.
@@ -516,7 +492,7 @@ Qed.
Lemma loc_arguments_hf_bounded:
forall ofs ty tyl ir fr ofs0,
- In (S Outgoing ofs ty) (loc_arguments_hf tyl ir fr ofs0) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) ->
ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0.
Proof.
induction tyl; simpl; intros.
@@ -564,7 +540,7 @@ Qed.
Lemma loc_arguments_sf_bounded:
forall ofs ty tyl ofs0,
- In (S Outgoing ofs ty) (loc_arguments_sf tyl ofs0) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) ->
Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0.
Proof.
induction tyl; simpl; intros.
@@ -602,14 +578,14 @@ Qed.
Lemma loc_arguments_bounded:
forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (loc_arguments s) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
ofs + typesize ty <= size_arguments s.
Proof.
unfold loc_arguments, size_arguments; intros.
- assert (In (S Outgoing ofs ty) (loc_arguments_sf (sig_args s) (-4)) ->
+ assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) ->
ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)).
{ intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. }
- assert (In (S Outgoing ofs ty) (loc_arguments_hf (sig_args s) 0 0 0) ->
+ assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) ->
ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0).
{ intros. eapply loc_arguments_hf_bounded; eauto. }
destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto.
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 84606210..0d25d84a 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -616,51 +616,40 @@ Fixpoint add_equations (rl: list reg) (ml: list mreg) (e: eqs) : option eqs :=
of pseudoregisters of type [Tlong] in two locations containing the
two 32-bit halves of the 64-bit integer. *)
-Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list loc) (e: eqs) : option eqs :=
+Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc)) (e: eqs) : option eqs :=
match rl, tyl, ll with
| nil, nil, nil => Some e
- | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
- add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
- | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
+ | r1 :: rl, ty :: tyl, One l1 :: ll =>
add_equations_args rl tyl ll (add_equation (Eq Full r1 l1) e)
+ | r1 :: rl, Tlong :: tyl, Twolong l1 l2 :: ll =>
+ add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
| _, _, _ => None
end.
(** [add_equations_res] is similar but is specialized to the case where
there is only one pseudo-register. *)
-Function add_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
- match oty with
- | Some Tlong =>
- match ll with
- | l1 :: l2 :: nil => Some (add_equation (Eq Low r l2) (add_equation (Eq High r l1) e))
- | _ => None
- end
- | _ =>
- match ll with
- | l1 :: nil => Some (add_equation (Eq Full r l1) e)
- | _ => None
- end
+Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs :=
+ match p, oty with
+ | One mr, _ =>
+ Some (add_equation (Eq Full r (R mr)) e)
+ | Twolong mr1 mr2, Some Tlong =>
+ Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e))
+ | _, _ =>
+ None
end.
(** [remove_equations_res] is similar to [add_equations_res] but removes
equations instead of adding them. *)
-Function remove_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
- match oty with
- | Some Tlong =>
- match ll with
- | l1 :: l2 :: nil =>
- if Loc.diff_dec l2 l1
- then Some (remove_equation (Eq Low r l2) (remove_equation (Eq High r l1) e))
- else None
- | _ => None
- end
- | _ =>
- match ll with
- | l1 :: nil => Some (remove_equation (Eq Full r l1) e)
- | _ => None
- end
+Function remove_equations_res (r: reg) (p: rpair mreg) (e: eqs) : option eqs :=
+ match p with
+ | One mr =>
+ Some (remove_equation (Eq Full r (R mr)) e)
+ | Twolong mr1 mr2 =>
+ if mreg_eq mr2 mr1
+ then None
+ else Some (remove_equation (Eq Low r (R mr2)) (remove_equation (Eq High r (R mr1)) e))
end.
(** [add_equations_ros] adds an equation, if needed, between an optional
@@ -960,10 +949,11 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
track_moves env mv1 e3
| BScall sg ros args res mv1 ros' mv2 s =>
let args' := loc_arguments sg in
- let res' := map R (loc_result sg) in
+ let res' := loc_result sg in
do e1 <- track_moves env mv2 e;
- do e2 <- remove_equations_res res (sig_res sg) res' e1;
- assertion (forallb (fun l => reg_loc_unconstrained res l e2) res');
+ do e2 <- remove_equations_res res res' e1;
+ assertion (forallb (fun l => reg_loc_unconstrained res l e2)
+ (map R (regs_of_rpair res')));
assertion (no_caller_saves e2);
do e3 <- add_equation_ros ros ros' e2;
do e4 <- add_equations_args args (sig_args sg) args' e3;
@@ -1000,7 +990,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
| BSreturn None mv =>
track_moves env mv empty_eqs
| BSreturn (Some arg) mv =>
- let arg' := map R (loc_result (RTL.fn_sig f)) in
+ let arg' := loc_result (RTL.fn_sig f) in
do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
track_moves env mv e1
end.
@@ -1184,15 +1174,15 @@ Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) :=
involving pseudoregs [r'] not in [rparams]: these equations are
automatically satisfied since the initial value of [r'] is [Vundef]. *)
-Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e: eqs)
+Function compat_entry (rparams: list reg) (lparams: list (rpair loc)) (e: eqs)
{struct rparams} : bool :=
- match rparams, tys, lparams with
- | nil, nil, nil => true
- | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
- compat_left2 r1 l1 l2 e && compat_entry rl tyl ll e
- | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
- compat_left r1 l1 e && compat_entry rl tyl ll e
- | _, _, _ => false
+ match rparams, lparams with
+ | nil, nil => true
+ | r1 :: rl, One l1 :: ll =>
+ compat_left r1 l1 e && compat_entry rl ll e
+ | r1 :: rl, Twolong l1 l2 :: ll =>
+ compat_left2 r1 l1 l2 e && compat_entry rl ll e
+ | _, _ => false
end.
(** Checking the satisfiability of equations inferred at function entry
@@ -1204,7 +1194,6 @@ Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function)
do mv <- pair_entrypoints rtl ltl;
do e2 <- track_moves env mv e1;
assertion (compat_entry (RTL.fn_params rtl)
- (sig_args (RTL.fn_sig rtl))
(loc_parameters (RTL.fn_sig rtl)) e2);
assertion (can_undef destroyed_at_function_entry e2);
assertion (zeq (RTL.fn_stacksize rtl) (LTL.fn_stacksize ltl));
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index bf60a57f..154c1e2e 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -415,12 +415,10 @@ Lemma add_equations_args_satisf:
satisf rs ls e' -> satisf rs ls e.
Proof.
intros until e'. functional induction (add_equations_args rl tyl ll e); intros.
- inv H; auto.
- eapply add_equation_satisf. eapply add_equation_satisf. eauto.
- eapply add_equation_satisf. eauto.
- eapply add_equation_satisf. eauto.
- eapply add_equation_satisf. eauto.
- congruence.
+- inv H; auto.
+- eapply add_equation_satisf; eauto.
+- eapply add_equation_satisf. eapply add_equation_satisf. eauto.
+- congruence.
Qed.
Lemma val_longofwords_eq:
@@ -438,22 +436,18 @@ Lemma add_equations_args_lessdef:
add_equations_args rl tyl ll e = Some e' ->
satisf rs ls e' ->
Val.has_type_list (rs##rl) tyl ->
- Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)).
+ Val.lessdef_list (rs##rl) (map (fun p => Locmap.getpair p ls) ll).
Proof.
intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros.
- inv H; auto.
- destruct H1. constructor; auto.
+ eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
+- destruct H1. constructor; auto.
rewrite <- (val_longofwords_eq (rs#r1)); auto. apply Val.longofwords_lessdef.
eapply add_equation_lessdef with (q := Eq High r1 l1).
eapply add_equation_satisf. eapply add_equations_args_satisf; eauto.
eapply add_equation_lessdef with (q := Eq Low r1 l2).
eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
- eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
- eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
- eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
- discriminate.
Qed.
@@ -475,13 +469,13 @@ Proof.
Qed.
Lemma remove_equation_res_satisf:
- forall rs ls r oty ll e e',
- remove_equations_res r oty ll e = Some e' ->
+ forall rs ls r l e e',
+ remove_equations_res r l e = Some e' ->
satisf rs ls e -> satisf rs ls e'.
Proof.
intros. functional inversion H.
- apply remove_equation_satisf. apply remove_equation_satisf; auto.
apply remove_equation_satisf; auto.
+ apply remove_equation_satisf. apply remove_equation_satisf; auto.
Qed.
Remark select_reg_l_monotone:
@@ -668,50 +662,36 @@ Proof.
Qed.
Lemma parallel_assignment_satisf_2:
- forall rs ls res mres' oty e e' v v',
- let res' := map R mres' in
- remove_equations_res res oty res' e = Some e' ->
+ forall rs ls res res' e e' v v',
+ remove_equations_res res res' e = Some e' ->
satisf rs ls e' ->
reg_unconstrained res e' = true ->
- forallb (fun l => loc_unconstrained l e') res' = true ->
+ forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true ->
Val.lessdef v v' ->
- satisf (rs#res <- v) (Locmap.setlist res' (encode_long oty v') ls) e.
+ satisf (rs#res <- v) (Locmap.setpair res' v' ls) e.
Proof.
- intros; red; intros.
- assert (ISREG: forall l, In l res' -> exists mr, l = R mr).
- { unfold res'; intros. exploit list_in_map_inv; eauto. intros [mr [A B]]. exists mr; auto. }
- functional inversion H.
+ intros. functional inversion H.
+- (* One location *)
+ subst. simpl in H2. InvBooleans. simpl.
+ apply parallel_assignment_satisf with Full; auto.
+ unfold reg_loc_unconstrained. rewrite H1, H4. auto.
- (* Two 32-bit halves *)
subst.
- set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |}
- (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *.
- rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl.
- destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
- subst q; simpl. rewrite Regmap.gss.
- destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+ set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |}
+ (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *.
+ simpl in H2. InvBooleans. simpl.
+ red; intros.
+ destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
+ subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss.
apply Val.loword_lessdef; auto.
- destruct (OrderedEquation.eq_dec q (Eq High res l1)).
- subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto.
- destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+ destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
+ subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. rewrite Locmap.gss.
apply Val.hiword_lessdef; auto.
assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
eapply loc_unconstrained_sound; eauto.
eapply loc_unconstrained_sound; eauto.
eapply reg_unconstrained_sound; eauto.
-- (* One location *)
- subst. rewrite <- H5 in H2. simpl in H2. InvBooleans.
- replace (encode_long oty v') with (v' :: nil).
- set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
- destruct (OrderedEquation.eq_dec q (Eq Full res l1)).
- subst q; simpl. rewrite Regmap.gss.
- destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
- auto.
- assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec.
- simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto.
- eapply loc_unconstrained_sound; eauto.
- eapply reg_unconstrained_sound; eauto.
- destruct oty as [[]|]; reflexivity || contradiction.
Qed.
Lemma in_subst_reg:
@@ -1101,21 +1081,20 @@ Proof.
Qed.
Lemma add_equations_res_lessdef:
- forall r oty ll e e' rs ls,
- add_equations_res r oty ll e = Some e' ->
+ forall r oty l e e' rs ls,
+ add_equations_res r oty l e = Some e' ->
satisf rs ls e' ->
- Val.lessdef_list (encode_long oty rs#r) (map ls ll).
-Proof.
- intros. functional inversion H.
-- subst. simpl. constructor.
- eapply add_equation_lessdef with (q := Eq High r l1).
+ Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) ->
+ Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls).
+Proof.
+ intros. functional inversion H; simpl.
+- subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto.
+- subst. rewrite <- (val_longofwords_eq rs#r) by auto.
+ apply Val.longofwords_lessdef.
+ eapply add_equation_lessdef with (q := Eq High r (R mr1)).
eapply add_equation_satisf. eauto.
- constructor.
- eapply add_equation_lessdef with (q := Eq Low r l2). eauto.
- constructor.
-- subst. replace (encode_long oty rs#r) with (rs#r :: nil). simpl. constructor; auto.
- eapply add_equation_lessdef with (q := Eq Full r l1); eauto.
- destruct oty as [[]|]; reflexivity || contradiction.
+ eapply add_equation_lessdef with (q := Eq Low r (R mr2)).
+ eauto.
Qed.
Definition callee_save_loc (l: loc) :=
@@ -1149,47 +1128,60 @@ Proof.
lazy beta. destruct (eloc q). auto. destruct sl; congruence.
Qed.
+Lemma val_hiword_longofwords:
+ forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1.
+Proof.
+ intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword.
+ rewrite Int64.hi_ofwords. auto.
+Qed.
+
+Lemma val_loword_longofwords:
+ forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2.
+Proof.
+ intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword.
+ rewrite Int64.lo_ofwords. auto.
+Qed.
+
Lemma function_return_satisf:
forall rs ls_before ls_after res res' sg e e' v,
- res' = map R (loc_result sg) ->
- remove_equations_res res (sig_res sg) res' e = Some e' ->
+ res' = loc_result sg ->
+ remove_equations_res res res' e = Some e' ->
satisf rs ls_before e' ->
- forallb (fun l => reg_loc_unconstrained res l e') res' = true ->
+ forallb (fun l => reg_loc_unconstrained res l e') (map R (regs_of_rpair res')) = true ->
no_caller_saves e' = true ->
- Val.lessdef_list (encode_long (sig_res sg) v) (map ls_after res') ->
+ Val.lessdef v (Locmap.getpair (map_rpair R res') ls_after) ->
agree_callee_save ls_before ls_after ->
satisf (rs#res <- v) ls_after e.
Proof.
intros; red; intros.
functional inversion H0.
-- subst. rewrite <- H11 in *. unfold encode_long in H4. rewrite <- H7 in H4.
- simpl in H4. inv H4. inv H14.
- set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |}
- (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *.
- simpl in H2. InvBooleans.
- destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
- subst q; simpl. rewrite Regmap.gss. auto.
- destruct (OrderedEquation.eq_dec q (Eq High res l1)).
- subst q; simpl. rewrite Regmap.gss. auto.
- assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
- exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B].
- exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D].
- rewrite Regmap.gso; auto.
- exploit no_caller_saves_sound; eauto. intros.
- red in H5. rewrite <- H5; auto.
-- subst. rewrite <- H11 in *.
- replace (encode_long (sig_res sg) v) with (v :: nil) in H4.
- simpl in H4. inv H4.
- simpl in H2. InvBooleans.
- set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
- destruct (OrderedEquation.eq_dec q (Eq Full res l1)).
+- (* One register *)
+ subst. rewrite <- H8 in *. simpl in *. InvBooleans.
+ set (e' := remove_equation {| ekind := Full; ereg := res; eloc := R mr |} e) in *.
+ destruct (OrderedEquation.eq_dec q (Eq Full res (R mr))).
subst q; simpl. rewrite Regmap.gss; auto.
assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec.
exploit reg_loc_unconstrained_sound; eauto. intros [A B].
rewrite Regmap.gso; auto.
exploit no_caller_saves_sound; eauto. intros.
red in H5. rewrite <- H5; auto.
- destruct (sig_res sg) as [[]|]; reflexivity || contradiction.
+- (* Two 32-bit halves *)
+ subst. rewrite <- H9 in *. simpl in *.
+ set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |}
+ (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *.
+ InvBooleans.
+ destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
+ subst q; simpl. rewrite Regmap.gss.
+ eapply Val.lessdef_trans. apply Val.loword_lessdef. eauto. apply val_loword_longofwords.
+ destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
+ subst q; simpl. rewrite Regmap.gss.
+ eapply Val.lessdef_trans. apply Val.hiword_lessdef. eauto. apply val_hiword_longofwords.
+ assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
+ exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B].
+ exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D].
+ rewrite Regmap.gso; auto.
+ exploit no_caller_saves_sound; eauto. intros.
+ red in H5. rewrite <- H5; auto.
Qed.
Lemma compat_left_sound:
@@ -1225,31 +1217,22 @@ Proof.
exact (select_reg_h_monotone r).
Qed.
-Lemma val_hiword_longofwords:
- forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1.
-Proof.
- intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword.
- rewrite Int64.hi_ofwords. auto.
-Qed.
-
-Lemma val_loword_longofwords:
- forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2.
-Proof.
- intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword.
- rewrite Int64.lo_ofwords. auto.
-Qed.
-
Lemma compat_entry_satisf:
- forall rl tyl ll e,
- compat_entry rl tyl ll e = true ->
+ forall rl ll e,
+ compat_entry rl ll e = true ->
forall vl ls,
- Val.lessdef_list vl (decode_longs tyl (map ls ll)) ->
+ Val.lessdef_list vl (map (fun p => Locmap.getpair p ls) ll) ->
satisf (init_regs vl rl) ls e.
Proof.
- intros until e. functional induction (compat_entry rl tyl ll e); intros.
+ intros until e. functional induction (compat_entry rl ll e); intros.
- (* no params *)
simpl. red; intros. rewrite Regmap.gi. destruct (ekind q); simpl; auto.
-- (* a param of type Tlong *)
+- (* a param in a single location *)
+ InvBooleans. simpl in H0. inv H0. simpl.
+ red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
+ exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
+ eapply IHb; eauto.
+- (* a param split across two locations *)
InvBooleans. simpl in H0. inv H0. simpl.
red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
exploit compat_left2_sound; eauto.
@@ -1259,47 +1242,37 @@ Proof.
apply Val.lessdef_trans with (Val.loword (Val.longofwords (ls l1) (ls l2))).
apply Val.loword_lessdef; auto. apply val_loword_longofwords.
eapply IHb; eauto.
-- (* a param of type Tint *)
- InvBooleans. simpl in H0. inv H0. simpl.
- red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
- exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
- eapply IHb; eauto.
-- (* a param of type Tfloat *)
- InvBooleans. simpl in H0. inv H0. simpl.
- red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
- exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
- eapply IHb; eauto.
-- (* a param of type Tsingle *)
- InvBooleans. simpl in H0. inv H0. simpl.
- red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
- exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
- eapply IHb; eauto.
- (* error case *)
discriminate.
Qed.
Lemma call_regs_param_values:
forall sg ls,
- map (call_regs ls) (loc_parameters sg) = map ls (loc_arguments sg).
+ map (fun p => Locmap.getpair p (call_regs ls)) (loc_parameters sg)
+ = map (fun p => Locmap.getpair p ls) (loc_arguments sg).
Proof.
intros. unfold loc_parameters. rewrite list_map_compose.
- apply list_map_exten; intros. unfold call_regs, parameter_of_argument.
- exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable.
- destruct x; auto. destruct sl; tauto.
+ apply list_map_exten; intros. symmetry.
+ assert (A: forall l, loc_argument_acceptable l -> call_regs ls (parameter_of_argument l) = ls l).
+ { destruct l as [r | [] ofs ty]; simpl; auto; contradiction. }
+ exploit loc_arguments_acceptable; eauto. destruct x; simpl; intros.
+- auto.
+- destruct H0; f_equal; auto.
Qed.
Lemma return_regs_arg_values:
forall sg ls1 ls2,
tailcall_is_possible sg = true ->
- map (return_regs ls1 ls2) (loc_arguments sg) = map ls2 (loc_arguments sg).
-Proof.
- intros. apply list_map_exten; intros.
- exploit loc_arguments_acceptable; eauto.
- exploit tailcall_is_possible_correct; eauto.
- unfold loc_argument_acceptable, return_regs.
- destruct x; intros.
- rewrite H2; auto.
- contradiction.
+ map (fun p => Locmap.getpair p (return_regs ls1 ls2)) (loc_arguments sg)
+ = map (fun p => Locmap.getpair p ls2) (loc_arguments sg).
+Proof.
+ intros.
+ apply tailcall_is_possible_correct in H.
+ apply list_map_exten; intros.
+ apply Locmap.getpair_exten; intros.
+ assert (In l (regs_of_rpairs (loc_arguments sg))) by (eapply in_regs_of_rpairs; eauto).
+ exploit loc_arguments_acceptable_2; eauto. exploit H; eauto.
+ destruct l; simpl; intros; try contradiction. rewrite H4; auto.
Qed.
Lemma find_function_tailcall:
@@ -1542,7 +1515,7 @@ Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop :=
wf_moves mv ->
transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
track_moves env mv e1 = Some e2 ->
- compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true ->
+ compat_entry (RTL.fn_params f) (loc_parameters (fn_sig tf)) e2 = true ->
can_undef destroyed_at_function_entry e2 = true ->
RTL.fn_stacksize f = LTL.fn_stacksize tf ->
RTL.fn_sig f = LTL.fn_sig tf ->
@@ -1702,7 +1675,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
(WTRS: wt_regset env rs)
(WTRES: env res = proj_sig_res sg)
(STEPS: forall v ls1 m,
- Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
+ Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) ->
Val.has_type v (env res) ->
agree_callee_save ls ls1 ->
exists ls2,
@@ -1731,7 +1704,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
forall s f args m ts tf ls m'
(STACKS: match_stackframes s ts (funsig tf))
(FUN: transf_fundef f = OK tf)
- (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf)))))
+ (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf))))
(AG: agree_callee_save (parent_locset ts) ls)
(MEM: Mem.extends m m')
(WTARGS: Val.has_type_list args (sig_args (funsig tf))),
@@ -1740,7 +1713,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
| match_states_return:
forall s res m ts ls m' sg
(STACKS: match_stackframes s ts sg)
- (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
+ (RES: Val.lessdef res (Locmap.getpair (map_rpair R (loc_result sg)) ls))
(AG: agree_callee_save (parent_locset ts) ls)
(MEM: Mem.extends m m')
(WTRES: Val.has_type res (proj_sig_res sg)),
@@ -2089,7 +2062,7 @@ Proof.
(* call *)
- set (sg := RTL.funsig fd) in *.
set (args' := loc_arguments sg) in *.
- set (res' := map R (loc_result sg)) in *.
+ set (res' := loc_result sg) in *.
exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto.
intros [tfd [E F]].
@@ -2203,7 +2176,6 @@ Proof.
eapply star_right. eexact A1.
econstructor. eauto. eauto. traceEq.
simpl. econstructor; eauto.
- unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto.
apply return_regs_agree_callee_save.
constructor.
+ (* with an argument *)
@@ -2213,11 +2185,15 @@ Proof.
eapply star_right. eexact A1.
econstructor. eauto. eauto. traceEq.
simpl. econstructor; eauto. rewrite <- H11.
- replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f))))
- with (map ls1 (map R (loc_result (RTL.fn_sig f)))).
+ replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f)))
+ (return_regs (parent_locset ts) ls1))
+ with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1).
eapply add_equations_res_lessdef; eauto.
- rewrite !list_map_compose. apply list_map_exten; intros.
- unfold return_regs. erewrite loc_result_caller_save by eauto. auto.
+ rewrite H13. apply WTRS.
+ generalize (loc_result_caller_save (RTL.fn_sig f)).
+ destruct (loc_result (RTL.fn_sig f)); simpl.
+ intros A; rewrite A; auto.
+ intros [A B]; rewrite A, B; auto.
apply return_regs_agree_callee_save.
unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS.
@@ -2230,7 +2206,7 @@ Proof.
{ apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. }
exploit (exec_moves mv). eauto. eauto.
eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto.
- rewrite call_regs_param_values. rewrite H9. eexact ARGS.
+ rewrite call_regs_param_values. eexact ARGS.
exact WTRS.
intros [ls1 [A B]].
econstructor; split.
@@ -2246,22 +2222,20 @@ Proof.
simpl in FUN; inv FUN.
econstructor; split.
apply plus_one. econstructor; eauto.
- eapply external_call_symbols_preserved' with (ge1 := ge).
- econstructor; eauto. apply senv_preserved.
- econstructor; eauto. simpl.
- replace (map
- (Locmap.setlist (map R (loc_result (ef_sig ef)))
- (encode_long (sig_res (ef_sig ef)) v') ls)
- (map R (loc_result (ef_sig ef))))
- with (encode_long (sig_res (ef_sig ef)) v').
- apply encode_long_lessdef; auto.
- unfold encode_long, loc_result.
- destruct (sig_res (ef_sig ef)) as [[]|]; simpl; symmetry; f_equal; auto.
- red; intros. rewrite Locmap.gsetlisto. apply AG; auto.
- apply Loc.notin_iff. intros.
- exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'.
- destruct l; simpl; auto. red in H0. apply loc_result_caller_save in B. congruence.
- simpl. eapply external_call_well_typed; eauto.
+ eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved.
+ econstructor; eauto.
+ simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl.
+ rewrite Locmap.gss; auto.
+ generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D).
+ exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
+ rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss.
+ rewrite val_longofwords_eq by auto. auto.
+ red; intros. rewrite (AG l H0).
+ symmetry; apply Locmap.gpo.
+ assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
+ { intros. destruct l; simpl in *. congruence. auto. }
+ generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto.
+ eapply external_call_well_typed; eauto.
(* return *)
- inv STACKS.
@@ -2287,7 +2261,7 @@ Proof.
congruence.
constructor; auto.
constructor. rewrite SIG; rewrite H3; auto.
- rewrite SIG; rewrite H3; simpl; auto.
+ rewrite SIG, H3, loc_arguments_main. auto.
red; auto.
apply Mem.extends_refl.
rewrite SIG, H3. constructor.
@@ -2297,9 +2271,9 @@ Lemma final_states_simulation:
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 STACKS.
- econstructor. simpl; reflexivity.
- unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto.
+ intros. inv H0. inv H. inv STACKS.
+ econstructor.
+ unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. auto.
Qed.
Lemma wt_prog: wt_program prog.
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index cc27bd55..30d6990e 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -145,19 +145,6 @@ Proof.
rewrite preg_notin_charact in H. auto.
Qed.
-Lemma set_pregs_other_2:
- forall r rl vl rs,
- preg_notin r rl ->
- set_regs (map preg_of rl) vl rs r = rs r.
-Proof.
- induction rl; simpl; intros.
- auto.
- destruct vl; auto.
- assert (r <> preg_of a) by (destruct rl; tauto).
- assert (preg_notin r rl) by (destruct rl; simpl; tauto).
- rewrite IHrl by auto. apply Pregmap.gso; auto.
-Qed.
-
(** * Agreement between Mach registers and processor registers *)
Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
@@ -230,6 +217,15 @@ Proof.
red; intros; elim n. eapply preg_of_injective; eauto.
Qed.
+Corollary agree_set_mreg_parallel:
+ forall ms sp rs r v v',
+ agree ms sp rs ->
+ Val.lessdef v v' ->
+ agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
+Proof.
+ intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
+Qed.
+
Lemma agree_set_other:
forall ms sp rs r v,
agree ms sp rs ->
@@ -247,18 +243,16 @@ Proof.
intros. unfold nextinstr. apply agree_set_other. auto. auto.
Qed.
-Lemma agree_set_mregs:
- forall sp rl vl vl' ms rs,
+Lemma agree_set_pair:
+ forall sp p v v' ms rs,
agree ms sp rs ->
- Val.lessdef_list vl vl' ->
- agree (Mach.set_regs rl vl ms) sp (set_regs (map preg_of rl) vl' rs).
+ Val.lessdef v v' ->
+ agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
Proof.
- induction rl; simpl; intros.
- auto.
- inv H0. auto. apply IHrl; auto.
- eapply agree_set_mreg. eexact H.
- rewrite Pregmap.gss. auto.
- intros. apply Pregmap.gso; auto.
+ intros. destruct p; simpl.
+- apply agree_set_mreg_parallel; auto.
+- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+ apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
Qed.
Lemma agree_undef_nondata_regs:
@@ -333,15 +327,29 @@ Proof.
econstructor. eauto. assumption.
Qed.
+Lemma extcall_arg_pair_match:
+ forall ms sp rs m m' p v,
+ agree ms sp rs ->
+ Mem.extends m m' ->
+ Mach.extcall_arg_pair ms m sp p v ->
+ exists v', Asm.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
+Proof.
+ intros. inv H1.
+- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+ exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+ exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
+Qed.
+
Lemma extcall_args_match:
forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
forall ll vl,
- list_forall2 (Mach.extcall_arg ms m sp) ll vl ->
- exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
+ list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
+ exists vl', list_forall2 (Asm.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
Proof.
induction 3; intros.
exists (@nil val); split. constructor. constructor.
- exploit extcall_arg_match; eauto. intros [v1' [A B]].
+ exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
destruct IHlist_forall2 as [vl' [C D]].
exists (v1' :: vl'); split; constructor; auto.
Qed.
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index a498a654..e92be2b4 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -315,7 +315,7 @@ Proof.
econstructor; eauto with coqlib.
(* external function *)
left; econstructor; split.
- econstructor; eauto. eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto with coqlib.
(* return *)
inv H3. inv H1. left; econstructor; split.
@@ -341,7 +341,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 H6. econstructor; eauto.
+ intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.
Theorem transf_program_correct:
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 69cdd07d..64a83a58 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -22,6 +22,18 @@ Require Export Conventions1.
[arch/abi/Conventions1.v]. This file adds various processor-independent
definitions and lemmas. *)
+Lemma loc_arguments_acceptable_2:
+ forall s l,
+ In l (regs_of_rpairs (loc_arguments s)) -> loc_argument_acceptable l.
+Proof.
+ intros until l. generalize (loc_arguments_acceptable s). generalize (loc_arguments s).
+ induction l0 as [ | p pl]; simpl; intros.
+- contradiction.
+- rewrite in_app_iff in H0. destruct H0.
+ exploit H; eauto. destruct p; simpl in *; intuition congruence.
+ apply IHpl; auto.
+Qed.
+
(** ** Location of function parameters *)
(** A function finds the values of its parameter in the same locations
@@ -35,22 +47,25 @@ Definition parameter_of_argument (l: loc) : loc :=
| _ => l
end.
-Definition loc_parameters (s: signature) :=
- List.map parameter_of_argument (loc_arguments s).
+Definition loc_parameters (s: signature) : list (rpair loc) :=
+ List.map (map_rpair parameter_of_argument) (loc_arguments s).
Lemma incoming_slot_in_parameters:
forall ofs ty sg,
- In (S Incoming ofs ty) (loc_parameters sg) ->
- In (S Outgoing ofs ty) (loc_arguments sg).
+ In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters sg)) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)).
Proof.
intros.
- unfold loc_parameters in H.
+ replace (regs_of_rpairs (loc_parameters sg)) with (List.map parameter_of_argument (regs_of_rpairs (loc_arguments sg))) in H.
change (S Incoming ofs ty) with (parameter_of_argument (S Outgoing ofs ty)) in H.
exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
- exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
+ exploit loc_arguments_acceptable_2; eauto. unfold loc_argument_acceptable; intros.
destruct x; simpl in A; try discriminate.
destruct sl; try contradiction.
inv A. auto.
+ unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros.
+ auto.
+ rewrite map_app. f_equal; auto. destruct p; auto.
Qed.
(** * Tail calls *)
@@ -62,34 +77,27 @@ Qed.
arguments are all passed in registers. *)
Definition tailcall_possible (s: signature) : Prop :=
- forall l, In l (loc_arguments s) ->
+ forall l, In l (regs_of_rpairs (loc_arguments s)) ->
match l with R _ => True | S _ _ _ => False end.
(** Decide whether a tailcall is possible. *)
Definition tailcall_is_possible (sg: signature) : bool :=
- let fix tcisp (l: list loc) :=
- match l with
- | nil => true
- | R _ :: l' => tcisp l'
- | S _ _ _ :: l' => false
- end
- in tcisp (loc_arguments sg).
+ List.forallb
+ (fun l => match l with R _ => true | S _ _ _ => false end)
+ (regs_of_rpairs (loc_arguments sg)).
Lemma tailcall_is_possible_correct:
forall s, tailcall_is_possible s = true -> tailcall_possible s.
Proof.
- intro s. unfold tailcall_is_possible, tailcall_possible.
- generalize (loc_arguments s). induction l; simpl; intros.
- elim H0.
- destruct a.
- destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
+ unfold tailcall_is_possible; intros. rewrite forallb_forall in H.
+ red; intros. apply H in H0. destruct l; [auto|discriminate].
Qed.
Lemma zero_size_arguments_tailcall_possible:
forall sg, size_arguments sg = 0 -> tailcall_possible sg.
Proof.
- intros; red; intros. exploit loc_arguments_acceptable; eauto.
+ intros; red; intros. exploit loc_arguments_acceptable_2; eauto.
unfold loc_argument_acceptable.
destruct l; intros. auto. destruct sl; try contradiction. destruct H1.
generalize (loc_arguments_bounded _ _ _ H0).
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index 110c0f26..0b8ff3c7 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -518,7 +518,7 @@ Proof.
- (* external function *)
monadInv H8. econstructor; split.
apply plus_one. econstructor; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
constructor; auto.
- (* return *)
inv H3. inv H1.
@@ -544,7 +544,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 H6. econstructor; eauto.
+ intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.
Theorem transf_program_correct:
diff --git a/backend/LTL.v b/backend/LTL.v
index bb596fa2..5f7116ae 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -266,9 +266,9 @@ Inductive step: state -> trace -> state -> Prop :=
step (Callstate s (Internal f) rs m)
E0 (State s f (Vptr sp Int.zero) f.(fn_entrypoint) rs' m')
| exec_function_external: forall s ef t args res rs m rs' m',
- args = map rs (loc_arguments (ef_sig ef)) ->
- external_call' ef ge args m t res m' ->
- rs' = Locmap.setlist (map R (loc_result (ef_sig ef))) res rs ->
+ args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) ->
+ external_call ef ge args m t res m' ->
+ rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs ->
step (Callstate s (External ef) rs m)
t (Returnstate s rs' m')
| exec_return: forall f sp rs1 bb s rs m,
@@ -292,9 +292,8 @@ Inductive initial_state (p: program): state -> Prop :=
initial_state p (Callstate nil f (Locmap.init Vundef) m0).
Inductive final_state: state -> int -> Prop :=
- | final_state_intro: forall rs m r retcode,
- loc_result signature_main = r :: nil ->
- rs (R r) = Vint retcode ->
+ | final_state_intro: forall rs m retcode,
+ Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
Definition semantics (p: program) :=
diff --git a/backend/Linear.v b/backend/Linear.v
index 8c91a809..da1b4c04 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -246,9 +246,9 @@ Inductive step: state -> trace -> state -> Prop :=
E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs' m')
| exec_function_external:
forall s ef args res rs1 rs2 m t m',
- args = map rs1 (loc_arguments (ef_sig ef)) ->
- external_call' ef ge args m t res m' ->
- rs2 = Locmap.setlist (map R (loc_result (ef_sig ef))) res rs1 ->
+ args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) ->
+ external_call ef ge args m t res m' ->
+ rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 ->
step (Callstate s (External ef) rs1 m)
t (Returnstate s rs2 m')
| exec_return:
@@ -268,9 +268,8 @@ Inductive initial_state (p: program): state -> Prop :=
initial_state p (Callstate nil f (Locmap.init Vundef) m0).
Inductive final_state: state -> int -> Prop :=
- | final_state_intro: forall rs m r retcode,
- loc_result signature_main = r :: nil ->
- rs (R r) = Vint retcode ->
+ | final_state_intro: forall rs m retcode,
+ Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
Definition semantics (p: program) :=
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 16717365..10a3d8b2 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -694,7 +694,7 @@ Proof.
(* external function *)
monadInv H8. left; econstructor; split.
apply plus_one. eapply exec_function_external; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto.
(* return *)
@@ -722,7 +722,7 @@ Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> LTL.final_state st1 r -> Linear.final_state st2 r.
Proof.
- intros. inv H0. inv H. inv H6. econstructor; eauto.
+ intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.
Theorem transf_program_correct:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 50cd16d6..123c6b5a 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -37,7 +37,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
match sl with
| Local => zle 0 ofs
| Outgoing => zle 0 ofs
- | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
+ | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
end
&& Zdivide_dec (typealign ty) ofs (typealign_pos ty).
@@ -155,15 +155,19 @@ Proof.
red; intros. unfold Locmap.init. red; auto.
Qed.
-Lemma wt_setlist:
- forall vl rl rs,
- Val.has_type_list vl (map mreg_type rl) ->
+Lemma wt_setpair:
+ forall sg v rs,
+ Val.has_type v (proj_sig_res sg) ->
wt_locset rs ->
- wt_locset (Locmap.setlist (map R rl) vl rs).
+ wt_locset (Locmap.setpair (loc_result sg) v rs).
Proof.
- induction vl; destruct rl; simpl; intros; try contradiction.
+ intros. generalize (loc_result_pair sg) (loc_result_type sg).
+ destruct (loc_result sg); simpl Locmap.setpair.
+- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+- intros (A & B & C & D) E.
+ apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
+ apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
auto.
- destruct H. apply IHvl; auto. apply wt_setreg; auto.
Qed.
Lemma wt_setres:
@@ -334,8 +338,8 @@ Proof.
econstructor. eauto. eauto. eauto.
apply wt_undef_regs. apply wt_call_regs. auto.
- (* external function *)
- econstructor. auto. apply wt_setlist; auto.
- eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
+ econstructor. auto. apply wt_setpair; auto.
+ eapply external_call_well_typed; eauto.
- (* return *)
inv WTSTK. econstructor; eauto.
Qed.
diff --git a/backend/Locations.v b/backend/Locations.v
index 6ca84ea7..52abfc46 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -386,17 +386,35 @@ Module Locmap.
auto.
Qed.
- Fixpoint setlist (ll: list loc) (vl: list val) (m: t) {struct ll} : t :=
- match ll, vl with
- | l1 :: ls, v1 :: vs => setlist ls vs (set l1 v1 m)
- | _, _ => m
+ Definition getpair (p: rpair loc) (m: t) : val :=
+ match p with
+ | One l => m l
+ | Twolong l1 l2 => Val.longofwords (m l1) (m l2)
end.
- Lemma gsetlisto: forall l ll vl m, Loc.notin l ll -> (setlist ll vl m) l = m l.
+ Definition setpair (p: rpair mreg) (v: val) (m: t) : t :=
+ match p with
+ | One r => set (R r) v m
+ | Twolong hi lo => set (R lo) (Val.loword v) (set (R hi) (Val.hiword v) m)
+ end.
+
+ Lemma getpair_exten:
+ forall p ls1 ls2,
+ (forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) ->
+ getpair p ls2 = getpair p ls1.
Proof.
- induction ll; simpl; intros.
- auto.
- destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto.
+ intros. destruct p; simpl.
+ apply H; simpl; auto.
+ f_equal; apply H; simpl; auto.
+ Qed.
+
+ Lemma gpo:
+ forall p v m l,
+ forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l.
+ Proof.
+ intros; destruct p; simpl in *.
+ - apply gso. apply Loc.diff_sym; auto.
+ - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto.
Qed.
Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t :=
diff --git a/backend/Mach.v b/backend/Mach.v
index 739c8212..3e15c97c 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -156,10 +156,10 @@ Proof.
unfold Regmap.set. destruct (RegEq.eq r a); auto.
Qed.
-Fixpoint set_regs (rl: list mreg) (vl: list val) (rs: regset) : regset :=
- match rl, vl with
- | r1 :: rl', v1 :: vl' => set_regs rl' vl' (Regmap.set r1 v1 rs)
- | _, _ => rs
+Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset :=
+ match p with
+ | One r => rs#r <- v
+ | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
end.
Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
@@ -216,16 +216,25 @@ Definition find_function_ptr
(** Extract the values of the arguments to an external call. *)
-Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
- | extcall_arg_reg: forall rs m sp r,
+Inductive extcall_arg (rs: regset) (m: mem) (sp: val): loc -> val -> Prop :=
+ | extcall_arg_reg: forall r,
extcall_arg rs m sp (R r) (rs r)
- | extcall_arg_stack: forall rs m sp ofs ty v,
+ | extcall_arg_stack: forall ofs ty v,
load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v ->
extcall_arg rs m sp (S Outgoing ofs ty) v.
+Inductive extcall_arg_pair (rs: regset) (m: mem) (sp: val): rpair loc -> val -> Prop :=
+ | extcall_arg_one: forall l v,
+ extcall_arg rs m sp l v ->
+ extcall_arg_pair rs m sp (One l) v
+ | extcall_arg_twolong: forall hi lo vhi vlo,
+ extcall_arg rs m sp hi vhi ->
+ extcall_arg rs m sp lo vlo ->
+ extcall_arg_pair rs m sp (Twolong hi lo) (Val.longofwords vhi vlo).
+
Definition extcall_arguments
(rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
- list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args.
+ list_forall2 (extcall_arg_pair rs m sp) (loc_arguments sg) args.
(** Mach execution states. *)
@@ -391,8 +400,8 @@ Inductive step: state -> trace -> state -> Prop :=
forall s fb rs m t rs' ef args res m',
Genv.find_funct_ptr ge fb = Some (External ef) ->
extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
- external_call' ef ge args m t res m' ->
- rs' = set_regs (loc_result (ef_sig ef)) res rs ->
+ external_call ef ge args m t res m' ->
+ rs' = set_pair (loc_result (ef_sig ef)) res rs ->
step (Callstate s fb rs m)
t (Returnstate s rs' m')
| exec_return:
@@ -411,7 +420,7 @@ Inductive initial_state (p: program): state -> Prop :=
Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall rs m r retcode,
- loc_result signature_main = r :: nil ->
+ loc_result signature_main = One r ->
rs r = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 57fc8b86..dec1b988 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -693,10 +693,8 @@ Proof.
rewrite A; simpl; rewrite C; simpl.
rewrite H2; rewrite dec_eq_true.
replace (tailcall_is_possible sig) with true; auto.
- revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig).
- induction l; simpl; intros. auto.
- exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl.
- intros; apply H3; auto.
+ symmetry. unfold tailcall_is_possible. apply forallb_forall.
+ intros. apply H3 in H4. destruct x; intuition auto.
- (* builtin *)
exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]].
exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]].
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 3432b79d..e6e07339 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -70,13 +70,6 @@ let vreg tyenv r = V(r, tyenv r)
let vregs tyenv rl = List.map (vreg tyenv) rl
-let rec expand_regs tyenv = function
- | [] -> []
- | r :: rl ->
- match tyenv r with
- | Tlong -> V(r, Tint) :: V(twin_reg r, Tint) :: expand_regs tyenv rl
- | ty -> V(r, ty) :: expand_regs tyenv rl
-
let constrain_reg v c =
match c with
| None -> v
@@ -105,12 +98,47 @@ let rec movelist vl1 vl2 k =
| v1 :: vl1, v2 :: vl2 -> move v1 v2 (movelist vl1 vl2 k)
| _, _ -> assert false
-let xparmove srcs dsts k =
+let parmove_regs2locs tyenv srcs dsts k =
assert (List.length srcs = List.length dsts);
- match srcs, dsts with
+ let rec expand srcs' dsts' rl ll =
+ match rl, ll with
+ | [], [] -> (srcs', dsts')
+ | r :: rl, One l :: ll ->
+ let ty = tyenv r in
+ expand (V(r, ty) :: srcs') (L l :: dsts') rl ll
+ | r :: rl, Twolong(l1, l2) :: ll ->
+ assert (tyenv r = Tlong);
+ expand (V(r, Tint) :: V(twin_reg r, Tint) :: srcs')
+ (L l1 :: L l2 :: dsts')
+ rl ll
+ | _, _ ->
+ assert false in
+ let (srcs', dsts') = expand [] [] srcs dsts in
+ match srcs', dsts' with
+ | [], [] -> k
+ | [src], [dst] -> move src dst k
+ | _, _ -> Xparmove(srcs', dsts', new_temp Tint, new_temp Tfloat) :: k
+
+let parmove_locs2regs tyenv srcs dsts k =
+ assert (List.length srcs = List.length dsts);
+ let rec expand srcs' dsts' ll rl =
+ match ll, rl with
+ | [], [] -> (srcs', dsts')
+ | One l :: ll, r :: rl ->
+ let ty = tyenv r in
+ expand (L l :: srcs') (V(r, ty) :: dsts') ll rl
+ | Twolong(l1, l2) :: ll, r :: rl ->
+ assert (tyenv r = Tlong);
+ expand (L l1 :: L l2 :: srcs')
+ (V(r, Tint) :: V(twin_reg r, Tint) :: dsts')
+ ll rl
+ | _, _ ->
+ assert false in
+ let (srcs', dsts') = expand [] [] srcs dsts in
+ match srcs', dsts' with
| [], [] -> k
| [src], [dst] -> move src dst k
- | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k
+ | _, _ -> Xparmove(srcs', dsts', new_temp Tint, new_temp Tfloat) :: k
let rec convert_builtin_arg tyenv = function
| BA r ->
@@ -228,16 +256,17 @@ let block_of_RTL_instr funsig tyenv = function
end else
[Xstore(chunk, addr, vregs tyenv args, vreg tyenv src); Xbranch s]
| RTL.Icall(sg, ros, args, res, s) ->
- let args' = vlocs (loc_arguments sg)
- and res' = vmregs (loc_result sg) in
- xparmove (expand_regs tyenv args) args'
- (Xcall(sg, sum_left_map (vreg tyenv) ros, args', res') ::
- xparmove res' (expand_regs tyenv [res])
+ let args' = loc_arguments sg
+ and res' = [map_rpair (fun r -> R r) (loc_result sg)] in
+ parmove_regs2locs tyenv args args'
+ (Xcall(sg, sum_left_map (vreg tyenv) ros,
+ vlocpairs args', vlocpairs res') ::
+ parmove_locs2regs tyenv res' [res]
[Xbranch s])
| RTL.Itailcall(sg, ros, args) ->
- let args' = vlocs (loc_arguments sg) in
- xparmove (expand_regs tyenv args) args'
- [Xtailcall(sg, sum_left_map (vreg tyenv) ros, args')]
+ let args' = loc_arguments sg in
+ parmove_regs2locs tyenv args args'
+ [Xtailcall(sg, sum_left_map (vreg tyenv) ros, vlocpairs args')]
| RTL.Ibuiltin(ef, args, res, s) ->
let (cargs, cres) = mregs_for_builtin ef in
let args1 = List.map (convert_builtin_arg tyenv) args
@@ -255,8 +284,8 @@ let block_of_RTL_instr funsig tyenv = function
| RTL.Ireturn None ->
[Xreturn []]
| RTL.Ireturn (Some arg) ->
- let args' = vmregs (loc_result funsig) in
- xparmove (expand_regs tyenv [arg]) args' [Xreturn args']
+ let args' = [map_rpair (fun r -> R r) (loc_result funsig)] in
+ parmove_regs2locs tyenv [arg] args' [Xreturn (vlocpairs args')]
(* One above the [pc] nodes of the given RTL function *)
@@ -272,8 +301,9 @@ let function_of_RTL_function f tyenv =
(* Add moves for function parameters *)
let pc_entrypoint = next_pc f in
let b_entrypoint =
- xparmove (vlocs (loc_parameters f.RTL.fn_sig))
- (expand_regs tyenv f.RTL.fn_params)
+ parmove_locs2regs tyenv
+ (loc_parameters f.RTL.fn_sig)
+ f.RTL.fn_params
[Xbranch f.RTL.fn_entrypoint] in
{ fn_sig = f.RTL.fn_sig;
fn_stacksize = f.RTL.fn_stacksize;
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 15953131..da024a25 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -54,9 +54,9 @@ Qed.
Lemma slot_outgoing_argument_valid:
forall f ofs ty sg,
- In (S Outgoing ofs ty) (loc_arguments sg) -> slot_valid f Outgoing ofs ty = true.
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) -> slot_valid f Outgoing ofs ty = true.
Proof.
- intros. exploit loc_arguments_acceptable; eauto. intros [A B].
+ intros. exploit loc_arguments_acceptable_2; eauto. intros [A B].
unfold slot_valid. unfold proj_sumbool.
rewrite zle_true by omega.
rewrite pred_dec_true by auto.
@@ -511,12 +511,14 @@ Local Opaque sepconj.
- apply frame_set_reg; auto.
Qed.
-Corollary frame_set_regs:
- forall j sp ls0 parent retaddr m P rl vl ls,
+Corollary frame_set_regpair:
+ forall j sp ls0 parent retaddr m P p v ls,
m |= frame_contents j sp ls ls0 parent retaddr ** P ->
- m |= frame_contents j sp (Locmap.setlist (map R rl) vl ls) ls0 parent retaddr ** P.
+ m |= frame_contents j sp (Locmap.setpair p v ls) ls0 parent retaddr ** P.
Proof.
- induction rl; destruct vl; simpl; intros; trivial. apply IHrl. apply frame_set_reg; auto.
+ intros. destruct p; simpl.
+ apply frame_set_reg; auto.
+ apply frame_set_reg; apply frame_set_reg; auto.
Qed.
Corollary frame_set_res:
@@ -565,7 +567,7 @@ Record agree_locs (ls ls0: locset) : Prop :=
corresponding Outgoing stack slots in the caller *)
agree_incoming:
forall ofs ty,
- In (S Incoming ofs ty) (loc_parameters f.(Linear.fn_sig)) ->
+ In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters f.(Linear.fn_sig))) ->
ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty)
}.
@@ -614,16 +616,16 @@ Proof.
rewrite Locmap.gso; auto. red. auto.
Qed.
-Lemma agree_regs_set_regs:
- forall j rl vl vl' ls rs,
+Lemma agree_regs_set_pair:
+ forall j p v v' ls rs,
agree_regs j ls rs ->
- Val.inject_list j vl vl' ->
- agree_regs j (Locmap.setlist (map R rl) vl ls) (set_regs rl vl' rs).
+ Val.inject j v v' ->
+ agree_regs j (Locmap.setpair p v ls) (set_pair p v' rs).
Proof.
- induction rl; simpl; intros.
- auto.
- inv H0. auto.
- apply IHrl; auto. apply agree_regs_set_reg; auto.
+ intros. destruct p; simpl.
+- apply agree_regs_set_reg; auto.
+- apply agree_regs_set_reg. apply agree_regs_set_reg; auto.
+ apply Val.hiword_inject; auto. apply Val.loword_inject; auto.
Qed.
Lemma agree_regs_set_res:
@@ -706,14 +708,25 @@ Proof.
rewrite Locmap.gso. auto. red. intuition congruence.
Qed.
-Lemma agree_locs_set_regs:
- forall ls0 rl vl ls,
+Lemma caller_save_reg_within_bounds:
+ forall r,
+ is_callee_save r = false -> mreg_within_bounds b r.
+Proof.
+ intros; red; intros. congruence.
+Qed.
+
+Lemma agree_locs_set_pair:
+ forall ls0 p v ls,
agree_locs ls ls0 ->
- (forall r, In r rl -> mreg_within_bounds b r) ->
- agree_locs (Locmap.setlist (map R rl) vl ls) ls0.
+ forall_rpair (fun r => is_callee_save r = false) p ->
+ agree_locs (Locmap.setpair p v ls) ls0.
Proof.
- induction rl; destruct vl; simpl; intros; auto.
- apply IHrl; auto. apply agree_locs_set_reg; auto.
+ intros.
+ destruct p; simpl in *.
+ apply agree_locs_set_reg; auto. apply caller_save_reg_within_bounds; auto.
+ destruct H0.
+ apply agree_locs_set_reg; auto. apply agree_locs_set_reg; auto.
+ apply caller_save_reg_within_bounds; auto. apply caller_save_reg_within_bounds; auto.
Qed.
Lemma agree_locs_set_res:
@@ -739,13 +752,6 @@ Proof.
apply agree_locs_set_reg; auto.
Qed.
-Lemma caller_save_reg_within_bounds:
- forall r,
- is_callee_save r = false -> mreg_within_bounds b r.
-Proof.
- intros; red; intros. congruence.
-Qed.
-
Lemma agree_locs_undef_locs_1:
forall ls0 regs ls,
agree_locs ls ls0 ->
@@ -819,19 +825,14 @@ Proof.
Qed.
Lemma agree_callee_save_set_result:
- forall sg vl ls1 ls2,
+ forall sg v ls1 ls2,
agree_callee_save ls1 ls2 ->
- agree_callee_save (Locmap.setlist (map R (loc_result sg)) vl ls1) ls2.
+ agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2.
Proof.
- intros sg. generalize (loc_result_caller_save sg).
- generalize (loc_result sg).
- induction l; simpl; intros.
- auto.
- destruct vl; auto.
- apply IHl; auto.
- red; intros. rewrite Locmap.gso. apply H0; auto.
- destruct l0; simpl; auto. red; intros; subst a.
- assert (is_callee_save r = false) by auto. congruence.
+ intros; red; intros. rewrite Locmap.gpo. apply H; auto.
+ assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
+ { intros. destruct l; auto. simpl; congruence. }
+ generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto.
Qed.
(** ** Properties of destroyed registers. *)
@@ -1355,7 +1356,7 @@ Inductive match_stacks (j: meminj):
(TY_RA: Val.has_type ra Tint)
(AGL: agree_locs f ls (parent_locset cs))
(ARGS: forall ofs ty,
- In (S Outgoing ofs ty) (loc_arguments sg) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) ->
slot_within_bounds (function_bounds f) Outgoing ofs ty)
(STK: match_stacks j cs cs' (Linear.fn_sig f)),
match_stacks j
@@ -1617,11 +1618,11 @@ Hypothesis SEP: m' |= stack_contents j cs cs'.
Lemma transl_external_argument:
forall l,
- In l (loc_arguments sg) ->
+ In l (regs_of_rpairs (loc_arguments sg)) ->
exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v.
Proof.
intros.
- assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable with sg; auto).
+ assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable_2 with sg; auto).
destruct l; red in H0.
- exists (rs r); split. constructor. auto.
- destruct sl; try contradiction.
@@ -1637,23 +1638,39 @@ Proof.
constructor. exact A. red in AGCS. rewrite AGCS; auto.
Qed.
+Lemma transl_external_argument_2:
+ forall p,
+ In p (loc_arguments sg) ->
+ exists v, extcall_arg_pair rs m' (parent_sp cs') p v /\ Val.inject j (Locmap.getpair p ls) v.
+Proof.
+ intros. destruct p as [l | l1 l2].
+- destruct (transl_external_argument l) as (v & A & B). eapply in_regs_of_rpairs; eauto; simpl; auto.
+ exists v; split; auto. constructor; auto.
+- destruct (transl_external_argument l1) as (v1 & A1 & B1). eapply in_regs_of_rpairs; eauto; simpl; auto.
+ destruct (transl_external_argument l2) as (v2 & A2 & B2). eapply in_regs_of_rpairs; eauto; simpl; auto.
+ exists (Val.longofwords v1 v2); split.
+ constructor; auto.
+ apply Val.longofwords_inject; auto.
+Qed.
+
Lemma transl_external_arguments_rec:
forall locs,
incl locs (loc_arguments sg) ->
exists vl,
- list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ Val.inject_list j ls##locs vl.
+ list_forall2 (extcall_arg_pair rs m' (parent_sp cs')) locs vl
+ /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) locs) vl.
Proof.
induction locs; simpl; intros.
exists (@nil val); split. constructor. constructor.
- exploit transl_external_argument; eauto with coqlib. intros [v [A B]].
+ exploit transl_external_argument_2; eauto with coqlib. intros [v [A B]].
exploit IHlocs; eauto with coqlib. intros [vl [C D]].
exists (v :: vl); split; constructor; auto.
Qed.
Lemma transl_external_arguments:
exists vl,
- extcall_arguments rs m' (parent_sp cs') sg vl /\
- Val.inject_list j (ls ## (loc_arguments sg)) vl.
+ extcall_arguments rs m' (parent_sp cs') sg vl
+ /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) (loc_arguments sg)) vl.
Proof.
unfold extcall_arguments.
apply transl_external_arguments_rec.
@@ -2079,16 +2096,14 @@ Proof.
simpl in TRANSL. inversion TRANSL; subst tf.
exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]].
rewrite sep_comm, sep_assoc in SEP.
- inv H0.
exploit external_call_parallel_rule; eauto.
- eapply decode_longs_inject; eauto.
intros (j' & res' & m1' & A & B & C & D & E).
econstructor; split.
apply plus_one. eapply exec_function_external; eauto.
- eapply external_call_symbols_preserved'. econstructor; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
eapply match_states_return with (j := j').
eapply match_stacks_change_meminj; eauto.
- apply agree_regs_set_regs. apply agree_regs_inject_incr with j; auto. apply encode_long_inject; auto.
+ apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
apply agree_callee_save_set_result; auto.
apply stack_contents_change_meminj with j; auto.
rewrite sep_comm, sep_assoc; auto.
@@ -2135,7 +2150,9 @@ Lemma transf_final_states:
match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r.
Proof.
intros. inv H0. inv H. inv STACKS.
- generalize (AGREGS r0). rewrite H2. intros A; inv A.
+ assert (R: exists r, loc_result signature_main = One r) by (econstructor; reflexivity).
+ destruct R as [rres EQ]. rewrite EQ in H1. simpl in H1.
+ generalize (AGREGS rres). rewrite H1. intros A; inv A.
econstructor; eauto.
Qed.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 4f1f8143..4f3ba5cb 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -367,7 +367,7 @@ Proof.
(* external function *)
left; simpl; econstructor; split.
eapply exec_function_external; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
simpl. econstructor; eauto.
(* return *)
inv H3. inv H1.
@@ -395,7 +395,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 H6. econstructor; eauto.
+ intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.
Theorem transf_program_correct:
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 2ddbc50a..a1b7f23b 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -64,6 +64,11 @@ let vlocs ll = List.map vloc ll
let vmreg mr = L(R mr)
let vmregs mrl = List.map vmreg mrl
+let rec vlocpairs = function
+ | [] -> []
+ | One l :: ll -> L l :: vlocpairs ll
+ | Twolong(l1, l2) :: ll -> L l1 :: L l2 :: vlocpairs ll
+
(* Tests over variables *)
let is_stack_reg = function
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 6bdcc8c6..54988d4b 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -64,6 +64,7 @@ val vloc: loc -> var
val vlocs: loc list -> var list
val vmreg: mreg -> var
val vmregs: mreg list -> var list
+val vlocpairs: loc rpair list -> var list
(* Tests over variables *)
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index e08411a5..7fa35f16 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -50,7 +50,7 @@ let precedence = function
| Ebinop((Oadd|Osub), _, _, _) -> (12, LtoR)
| Ebinop((Oshl|Oshr), _, _, _) -> (11, LtoR)
| Ebinop((Olt|Ogt|Ole|Oge), _, _, _) -> (10, LtoR)
- | Ebinop((Oeq|One), _, _, _) -> (9, LtoR)
+ | Ebinop((Oeq|Cop.One), _, _, _) -> (9, LtoR)
| Ebinop(Oand, _, _, _) -> (8, LtoR)
| Ebinop(Oxor, _, _, _) -> (7, LtoR)
| Ebinop(Oor, _, _, _) -> (6, LtoR)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 4287f7f9..9a6107ff 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -41,7 +41,7 @@ let name_binop = function
| Oshl -> "<<"
| Oshr -> ">>"
| Oeq -> "=="
- | One -> "!="
+ | Cop.One -> "!="
| Olt -> "<"
| Ogt -> ">"
| Ole -> "<="
@@ -154,7 +154,7 @@ let rec precedence = function
| Ebinop((Oadd|Osub), _, _, _) -> (12, LtoR)
| Ebinop((Oshl|Oshr), _, _, _) -> (11, LtoR)
| Ebinop((Olt|Ogt|Ole|Oge), _, _, _) -> (10, LtoR)
- | Ebinop((Oeq|One), _, _, _) -> (9, LtoR)
+ | Ebinop((Oeq|Cop.One), _, _, _) -> (9, LtoR)
| Ebinop(Oand, _, _, _) -> (8, LtoR)
| Ebinop(Oxor, _, _, _) -> (7, LtoR)
| Ebinop(Oor, _, _, _) -> (6, LtoR)
diff --git a/common/AST.v b/common/AST.v
index 415e90e2..0b524eb8 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -544,10 +544,65 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
End TRANSF_PARTIAL_FUNDEF.
-(** * Arguments and results to builtin functions *)
+(** * Register pairs *)
Set Contextual Implicit.
+(** In some intermediate languages (LTL, Mach), 64-bit integers can be
+ split into two 32-bit halves and held in a pair of registers.
+ Syntactically, this is captured by the type [rpair] below. *)
+
+Inductive rpair (A: Type) : Type :=
+ | One (r: A)
+ | Twolong (rhi rlo: A).
+
+Definition typ_rpair (A: Type) (typ_of: A -> typ) (p: rpair A): typ :=
+ match p with
+ | One r => typ_of r
+ | Twolong rhi rlo => Tlong
+ end.
+
+Definition map_rpair (A B: Type) (f: A -> B) (p: rpair A): rpair B :=
+ match p with
+ | One r => One (f r)
+ | Twolong rhi rlo => Twolong (f rhi) (f rlo)
+ end.
+
+Definition regs_of_rpair (A: Type) (p: rpair A): list A :=
+ match p with
+ | One r => r :: nil
+ | Twolong rhi rlo => rhi :: rlo :: nil
+ end.
+
+Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A :=
+ match l with
+ | nil => nil
+ | p :: l => regs_of_rpair p ++ regs_of_rpairs l
+ end.
+
+Lemma in_regs_of_rpairs:
+ forall (A: Type) (x: A) p, In x (regs_of_rpair p) -> forall l, In p l -> In x (regs_of_rpairs l).
+Proof.
+ induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto.
+Qed.
+
+Lemma in_regs_of_rpairs_inv:
+ forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p).
+Proof.
+ induction l; simpl; intros. contradiction.
+ rewrite in_app_iff in H; destruct H.
+ exists a; auto.
+ apply IHl in H. firstorder auto.
+Qed.
+
+Definition forall_rpair (A: Type) (P: A -> Prop) (p: rpair A): Prop :=
+ match p with
+ | One r => P r
+ | Twolong rhi rlo => P rhi /\ P rlo
+ end.
+
+(** * Arguments and results to builtin functions *)
+
Inductive builtin_arg (A: Type) : Type :=
| BA (x: A)
| BA_int (n: int)
diff --git a/common/Events.v b/common/Events.v
index 040029fb..c94d6d35 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1487,193 +1487,6 @@ Proof.
intros. exploit external_call_determ. eexact H. eexact H0. intuition.
Qed.
-(** Late in the back-end, calling conventions for external calls change:
- arguments and results of type [Tlong] are passed as two integers.
- We now wrap [external_call] to adapt to this convention. *)
-
-Fixpoint decode_longs (tyl: list typ) (vl: list val) : list val :=
- match tyl with
- | nil => nil
- | Tlong :: tys =>
- match vl with
- | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs
- | _ => nil
- end
- | ty :: tys =>
- match vl with
- | v1 :: vs => v1 :: decode_longs tys vs
- | _ => nil
- end
- end.
-
-Definition encode_long (oty: option typ) (v: val) : list val :=
- match oty with
- | Some Tlong => Val.hiword v :: Val.loword v :: nil
- | _ => v :: nil
- end.
-
-Definition proj_sig_res' (s: signature) : list typ :=
- match s.(sig_res) with
- | Some Tlong => Tint :: Tint :: nil
- | Some ty => ty :: nil
- | None => Tint :: nil
- end.
-
-Inductive external_call'
- (ef: external_function) (ge: Senv.t)
- (vargs: list val) (m1: mem) (t: trace) (vres: list val) (m2: mem) : Prop :=
- external_call'_intro: forall v,
- external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 ->
- vres = encode_long (sig_res (ef_sig ef)) v ->
- external_call' ef ge vargs m1 t vres m2.
-
-Lemma decode_longs_lessdef:
- forall tyl vl1 vl2, Val.lessdef_list vl1 vl2 -> Val.lessdef_list (decode_longs tyl vl1) (decode_longs tyl vl2).
-Proof.
- induction tyl; simpl; intros.
- auto.
- destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_lessdef; auto.
-Qed.
-
-Lemma decode_longs_inject:
- forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list f (decode_longs tyl vl1) (decode_longs tyl vl2).
-Proof.
- induction tyl; simpl; intros.
- auto.
- destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed.
-
-Lemma encode_long_lessdef:
- forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2).
-Proof.
- intros. destruct oty as [[]|]; simpl; auto.
- constructor. apply Val.hiword_lessdef; auto. constructor. apply Val.loword_lessdef; auto. auto.
-Qed.
-
-Lemma encode_long_inject:
- forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list f (encode_long oty v1) (encode_long oty v2).
-Proof.
- intros. destruct oty as [[]|]; simpl; auto.
- constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto.
-Qed.
-
-Lemma encode_long_has_type:
- forall v sg,
- Val.has_type v (proj_sig_res sg) ->
- Val.has_type_list (encode_long (sig_res sg) v) (proj_sig_res' sg).
-Proof.
- unfold proj_sig_res, proj_sig_res', encode_long; intros.
- destruct (sig_res sg) as [[] | ]; simpl; auto.
- destruct v; simpl; auto.
-Qed.
-
-Lemma external_call_well_typed':
- forall ef ge vargs m1 t vres m2,
- external_call' ef ge vargs m1 t vres m2 ->
- Val.has_type_list vres (proj_sig_res' (ef_sig ef)).
-Proof.
- intros. inv H. apply encode_long_has_type.
- eapply external_call_well_typed; eauto.
-Qed.
-
-Lemma external_call_symbols_preserved':
- forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
- external_call' ef ge1 vargs m1 t vres m2 ->
- Senv.equiv ge1 ge2 ->
- external_call' ef ge2 vargs m1 t vres m2.
-Proof.
- intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto.
-Qed.
-
-Lemma external_call_valid_block':
- forall ef ge vargs m1 t vres m2 b,
- external_call' ef ge vargs m1 t vres m2 ->
- Mem.valid_block m1 b -> Mem.valid_block m2 b.
-Proof.
- intros. inv H. eapply external_call_valid_block; eauto.
-Qed.
-
-Lemma external_call_nextblock':
- forall ef ge vargs m1 t vres m2,
- external_call' ef ge vargs m1 t vres m2 ->
- Ple (Mem.nextblock m1) (Mem.nextblock m2).
-Proof.
- intros. inv H. eapply external_call_nextblock; eauto.
-Qed.
-
-Lemma external_call_mem_extends':
- forall ef ge vargs m1 t vres m2 m1' vargs',
- external_call' ef ge vargs m1 t vres m2 ->
- Mem.extends m1 m1' ->
- Val.lessdef_list vargs vargs' ->
- exists vres' m2',
- external_call' ef ge vargs' m1' t vres' m2'
- /\ Val.lessdef_list vres vres'
- /\ Mem.extends m2 m2'
- /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'.
-Proof.
- intros. inv H.
- exploit external_call_mem_extends; eauto.
- eapply decode_longs_lessdef; eauto.
- intros (v' & m2' & A & B & C & D).
- exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
- econstructor; eauto.
- eapply encode_long_lessdef; eauto.
-Qed.
-
-Lemma external_call_mem_inject':
- forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs',
- meminj_preserves_globals ge f ->
- external_call' ef ge vargs m1 t vres m2 ->
- Mem.inject f m1 m1' ->
- Val.inject_list f vargs vargs' ->
- exists f' vres' m2',
- external_call' ef ge vargs' m1' t vres' m2'
- /\ Val.inject_list f' vres vres'
- /\ Mem.inject f' m2 m2'
- /\ Mem.unchanged_on (loc_unmapped f) m1 m2
- /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
- /\ inject_incr f f'
- /\ inject_separated f f' m1 m1'.
-Proof.
- intros. inv H0.
- exploit external_call_mem_inject; eauto.
- eapply decode_longs_inject; eauto.
- intros (f' & v' & m2' & A & B & C & D & E & P & Q).
- exists f'; exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
- econstructor; eauto.
- apply encode_long_inject; auto.
-Qed.
-
-Lemma external_call_determ':
- forall ef ge vargs m t1 vres1 m1 t2 vres2 m2,
- external_call' ef ge vargs m t1 vres1 m1 ->
- external_call' ef ge vargs m t2 vres2 m2 ->
- match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2).
-Proof.
- intros. inv H; inv H0. exploit external_call_determ. eexact H1. eexact H.
- intros [A B]. split. auto. intros. destruct B as [C D]; auto. subst. auto.
-Qed.
-
-Lemma external_call_match_traces':
- forall ef ge vargs m t1 vres1 m1 t2 vres2 m2,
- external_call' ef ge vargs m t1 vres1 m1 ->
- external_call' ef ge vargs m t2 vres2 m2 ->
- match_traces ge t1 t2.
-Proof.
- intros. inv H; inv H0. eapply external_call_match_traces; eauto.
-Qed.
-
-Lemma external_call_deterministic':
- forall ef ge vargs m t vres1 m1 vres2 m2,
- external_call' ef ge vargs m t vres1 m1 ->
- external_call' ef ge vargs m t vres2 m2 ->
- vres1 = vres2 /\ m1 = m2.
-Proof.
- intros. inv H; inv H0.
- exploit external_call_deterministic. eexact H1. eexact H. intros [A B].
- split; congruence.
-Qed.
-
(** * Evaluation of builtin arguments *)
Section EVAL_BUILTIN_ARG.
diff --git a/configure b/configure
index 2dc60d28..6b0b4da8 100755
--- a/configure
+++ b/configure
@@ -314,7 +314,7 @@ else
ocaml_opt_comp=false
fi
-MENHIR_REQUIRED=20160303
+MENHIR_REQUIRED=20151112
echo "Testing Menhir... " | tr -d '\n'
menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
case "$menhir_ver" in
diff --git a/ia32/Asm.v b/ia32/Asm.v
index f3ec3703..12d164a6 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -279,12 +279,12 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
| r :: l' => undef_regs l' (rs#r <- Vundef)
end.
-(** Assigning multiple registers *)
+(** Assigning a register pair *)
-Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
- match rl, vl with
- | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
- | _, _ => rs
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+ match p with
+ | One r => rs#r <- v
+ | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
end.
(** Assigning the result of a builtin *)
@@ -864,12 +864,21 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
(Val.add (rs (IR ESP)) (Vint (Int.repr bofs))) = Some v ->
extcall_arg rs m (S Outgoing ofs ty) v.
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+ | extcall_arg_one: forall l v,
+ extcall_arg rs m l v ->
+ extcall_arg_pair rs m (One l) v
+ | extcall_arg_twolong: forall hi lo vhi vlo,
+ extcall_arg rs m hi vhi ->
+ extcall_arg rs m lo vlo ->
+ extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
Definition extcall_arguments
(rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
- list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
+ list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
-Definition loc_external_result (sg: signature) : list preg :=
- map preg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : rpair preg :=
+ map_rpair preg_of (loc_result sg).
(** Execution of the instruction at [rs#PC]. *)
@@ -900,8 +909,8 @@ Inductive step: state -> trace -> state -> Prop :=
rs PC = Vptr b Int.zero ->
Genv.find_funct_ptr ge b = Some (External ef) ->
extcall_arguments rs m (ef_sig ef) args ->
- external_call' ef ge args m t res m' ->
- rs' = (set_regs (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) ->
+ external_call ef ge args m t res m' ->
+ rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) ->
step (State rs m) t (State rs' m').
End RELSEM.
@@ -935,13 +944,21 @@ Remark extcall_arguments_determ:
extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
intros until m.
- assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 ->
- forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
+ assert (A: forall l v1 v2,
+ extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
+ { intros. inv H; inv H0; congruence. }
+ assert (B: forall p v1 v2,
+ extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
+ { intros. inv H; inv H0.
+ eapply A; eauto.
+ f_equal; eapply A; eauto. }
+ assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
+ forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
+ {
induction 1; intros vl2 EA; inv EA.
auto.
- f_equal; auto.
- inv H; inv H3; congruence.
- intros. red in H0; red in H1. eauto.
+ f_equal; eauto. }
+ intros. eapply C; eauto.
Qed.
Lemma semantics_determinate: forall p, determinate (semantics p).
@@ -962,14 +979,13 @@ Ltac Equalities :=
exploit external_call_determ. eexact H5. eexact H11. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
+ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
- exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
+ exploit external_call_determ. eexact H4. eexact H9. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros; inv H; simpl.
omega.
- inv H3. eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- inv H3. eapply external_call_trace_length; eauto.
+ eapply external_call_trace_length; eauto.
- (* initial states *)
inv H; inv H0. f_equal. congruence.
- (* final no step *)
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 28237237..c498b601 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -840,14 +840,14 @@ Transparent destroyed_at_function_entry.
intros [tf [A B]]. simpl in B. inv B.
exploit extcall_arguments_match; eauto.
intros [args' [C D]].
- exploit external_call_mem_extends'; eauto.
+ exploit external_call_mem_extends; eauto.
intros [res' [m2' [P [Q [R S]]]]].
left; econstructor; split.
apply plus_one. eapply exec_step_external; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto.
unfold loc_external_result.
- apply agree_set_other; auto. apply agree_set_mregs; auto.
+ apply agree_set_other; auto. apply agree_set_pair; auto.
- (* return *)
inv STACKS. simpl in *.
diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v
index e9969ab8..672b4219 100644
--- a/ia32/Conventions1.v
+++ b/ia32/Conventions1.v
@@ -73,37 +73,47 @@ Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *)
(** ** Location of function result *)
(** The result value of a function is passed back to the caller in
- registers [AX] or [FP0], depending on the type of the returned value.
+ registers [AX] or [DX:AX] or [FP0], depending on the type of the returned value.
We treat a function without result as a function with one integer result. *)
-Definition loc_result (s: signature) : list mreg :=
+Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
- | None => AX :: nil
- | Some (Tint | Tany32) => AX :: nil
- | Some (Tfloat | Tsingle) => FP0 :: nil
- | Some Tany64 => X0 :: nil
- | Some Tlong => DX :: AX :: nil
+ | None => One AX
+ | Some (Tint | Tany32) => One AX
+ | Some (Tfloat | Tsingle) => One FP0
+ | Some Tany64 => One X0
+ | Some Tlong => Twolong DX AX
end.
(** The result registers have types compatible with that given in the signature. *)
Lemma loc_result_type:
forall sig,
- subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true.
+ subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
Qed.
(** The result locations are caller-save registers *)
Lemma loc_result_caller_save:
- forall (s: signature) (r: mreg),
- In r (loc_result s) -> is_callee_save r = false.
+ forall (s: signature),
+ forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- assert (r = AX \/ r = DX \/ r = FP0 \/ r = X0).
- unfold loc_result in H. destruct (sig_res s) as [[]|]; simpl in H; intuition.
- destruct H0 as [A | [A | [A | A]]]; subst r; reflexivity.
+ unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+Qed.
+
+(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
+
+Lemma loc_result_pair:
+ forall sg,
+ match loc_result sg with
+ | One _ => True
+ | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+ end.
+Proof.
+ intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence.
Qed.
(** ** Location of function arguments *)
@@ -111,21 +121,21 @@ Qed.
(** All arguments are passed on stack. (Snif.) *)
Fixpoint loc_arguments_rec
- (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
+ (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
- | Tint :: tys => S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 1)
- | Tfloat :: tys => S Outgoing ofs Tfloat :: loc_arguments_rec tys (ofs + 2)
- | Tsingle :: tys => S Outgoing ofs Tsingle :: loc_arguments_rec tys (ofs + 1)
- | Tlong :: tys => S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 2)
- | Tany32 :: tys => S Outgoing ofs Tany32 :: loc_arguments_rec tys (ofs + 1)
- | Tany64 :: tys => S Outgoing ofs Tany64 :: loc_arguments_rec tys (ofs + 2)
+ | ty :: tys =>
+ match ty with
+ | Tlong => Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint)
+ | _ => One (S Outgoing ofs ty)
+ end
+ :: loc_arguments_rec tys (ofs + typesize ty)
end.
(** [loc_arguments s] returns the list of locations where to store arguments
when calling a function with signature [s]. *)
-Definition loc_arguments (s: signature) : list loc :=
+Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_args) 0.
(** [size_arguments s] returns the number of [Outgoing] slots used
@@ -151,37 +161,36 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
| _ => False
end.
-Remark loc_arguments_rec_charact:
- forall tyl ofs l,
- In l (loc_arguments_rec tyl ofs) ->
+Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
match l with
| S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
| _ => False
end.
+
+Remark loc_arguments_rec_charact:
+ forall tyl ofs p,
+ In p (loc_arguments_rec tyl ofs) -> forall_rpair (loc_argument_charact ofs) p.
Proof.
- induction tyl; simpl loc_arguments_rec; intros.
+ assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
+ { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+ induction tyl as [ | ty tyl]; simpl loc_arguments_rec; intros.
+- contradiction.
- destruct H.
-- assert (REC: forall ofs1, In l (loc_arguments_rec tyl ofs1) -> ofs1 > ofs ->
- match l with
- | R _ => False
- | S Local _ _ => False
- | S Incoming _ _ => False
- | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
- end).
- { intros. exploit IHtyl; eauto. destruct l; auto. destruct sl; intuition omega
-. }
- destruct a; simpl in H; repeat (destruct H);
- ((eapply REC; eauto; omega) || (split; [omega|reflexivity])).
++ destruct ty; subst p; simpl; omega.
++ apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *.
+* eapply X; eauto; omega.
+* destruct H; split; eapply X; eauto; omega.
Qed.
Lemma loc_arguments_acceptable:
- forall (s: signature) (l: loc),
- In l (loc_arguments s) -> loc_argument_acceptable l.
+ forall (s: signature) (p: rpair loc),
+ In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
Proof.
unfold loc_arguments; intros.
exploit loc_arguments_rec_charact; eauto.
- unfold loc_argument_acceptable.
- destruct l as [r | [] ofs ty]; intuition auto. rewrite H2; apply Z.divide_1_l.
+ assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
+ { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. }
+ destruct p; simpl; intuition auto.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
@@ -204,23 +213,41 @@ Proof.
apply size_arguments_rec_above.
Qed.
+(*
+Lemma loc_arguments_bounded:
+ forall (s: signature) (p: rpair loc),
+ In p (loc_arguments s) ->
+ forall_rpair
+ (fun l => match l with S Outgoing ofs ty => ofs + typesize ty <= size_arguments s | _ => True end)
+ p.
+Proof.
+ intros until p. unfold loc_arguments, size_arguments. generalize (sig_args s) 0.
+ induction l as [ | ty l]; simpl; intros x IN.
+- contradiction.
+- destruct IN as [EQ|IN].
++ generalize (size_arguments_rec_above l (x + typesize ty)); intros A.
+ subst p. destruct ty; simpl in *; omega.
++ apply IHl; auto.
+Qed.
+*)
Lemma loc_arguments_bounded:
forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (loc_arguments s) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
ofs + typesize ty <= size_arguments s.
Proof.
intros until ty. unfold loc_arguments, size_arguments. generalize (sig_args s) 0.
- induction l; simpl; intros.
+ induction l as [ | t l]; simpl; intros x IN.
- contradiction.
-- Ltac decomp :=
+- rewrite in_app_iff in IN; destruct IN as [IN|IN].
++ apply Zle_trans with (x + typesize t); [|apply size_arguments_rec_above].
+ Ltac decomp :=
match goal with
| [ H: _ \/ _ |- _ ] => destruct H; decomp
| [ H: S _ _ _ = S _ _ _ |- _ ] => inv H
- | _ => idtac
+ | [ H: False |- _ ] => contradiction
end.
- destruct a; simpl in H; decomp; auto; try apply size_arguments_rec_above.
- simpl typesize. replace (z + 1 + 1) with (z + 2) by omega. apply size_arguments_rec_above.
- simpl typesize. apply Zle_trans with (ofs + 2). omega. apply size_arguments_rec_above.
+ destruct t; simpl in IN; decomp; simpl; omega.
++ apply IHl; auto.
Qed.
Lemma loc_arguments_main:
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index a9b60fbd..9f8231e0 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -396,12 +396,12 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
| r :: l' => undef_regs l' (rs#r <- Vundef)
end.
-(** Assigning multiple registers *)
+(** Assigning a register pair *)
-Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
- match rl, vl with
- | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
- | _, _ => rs
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+ match p with
+ | One r => rs#r <- v
+ | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
end.
(** Assigning the result of a builtin *)
@@ -980,12 +980,21 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
(Val.add (rs (IR GPR1)) (Vint (Int.repr bofs))) = Some v ->
extcall_arg rs m (S Outgoing ofs ty) v.
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+ | extcall_arg_one: forall l v,
+ extcall_arg rs m l v ->
+ extcall_arg_pair rs m (One l) v
+ | extcall_arg_twolong: forall hi lo vhi vlo,
+ extcall_arg rs m hi vhi ->
+ extcall_arg rs m lo vlo ->
+ extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
Definition extcall_arguments
(rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
- list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
+ list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
-Definition loc_external_result (sg: signature) : list preg :=
- map preg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : rpair preg :=
+ map_rpair preg_of (loc_result sg).
(** Execution of the instruction at [rs#PC]. *)
@@ -1015,9 +1024,9 @@ Inductive step: state -> trace -> state -> Prop :=
forall b ef args res rs m t rs' m',
rs PC = Vptr b Int.zero ->
Genv.find_funct_ptr ge b = Some (External ef) ->
- external_call' ef ge args m t res m' ->
+ external_call ef ge args m t res m' ->
extcall_arguments rs m (ef_sig ef) args ->
- rs' = (set_regs (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) ->
+ rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) ->
step (State rs m) t (State rs' m').
End RELSEM.
@@ -1051,13 +1060,21 @@ Remark extcall_arguments_determ:
extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
Proof.
intros until m.
- assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 ->
- forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
+ assert (A: forall l v1 v2,
+ extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
+ { intros. inv H; inv H0; congruence. }
+ assert (B: forall p v1 v2,
+ extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
+ { intros. inv H; inv H0.
+ eapply A; eauto.
+ f_equal; eapply A; eauto. }
+ assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
+ forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
+ {
induction 1; intros vl2 EA; inv EA.
auto.
- f_equal; auto.
- inv H; inv H3; congruence.
- intros. red in H0; red in H1. eauto.
+ f_equal; eauto. }
+ intros. eapply C; eauto.
Qed.
Lemma semantics_determinate: forall p, determinate (semantics p).
@@ -1078,13 +1095,13 @@ Ltac Equalities :=
exploit external_call_determ. eexact H5. eexact H11. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
- exploit external_call_determ'. eexact H3. eexact H8. intros [A B].
+ exploit external_call_determ. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
(* trace length *)
red; intros. inv H; simpl.
omega.
eapply external_call_trace_length; eauto.
- inv H2; eapply external_call_trace_length; eauto.
+ eapply external_call_trace_length; eauto.
(* initial states *)
inv H; inv H0. f_equal. congruence.
(* final no step *)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 31db77ca..44c81735 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -926,14 +926,14 @@ Local Transparent destroyed_by_jumptable.
intros [tf [A B]]. simpl in B. inv B.
exploit extcall_arguments_match; eauto.
intros [args' [C D]].
- exploit external_call_mem_extends'; eauto.
+ exploit external_call_mem_extends; eauto.
intros [res' [m2' [P [Q [R S]]]]].
left; econstructor; split.
apply plus_one. eapply exec_step_external; eauto.
- eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto.
unfold loc_external_result.
- apply agree_set_other; auto. apply agree_set_mregs; auto.
+ apply agree_set_other; auto. apply agree_set_pair; auto.
- (* return *)
inv STACKS. simpl in *.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index e78395bf..1605de73 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -86,33 +86,43 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
registers [R3] or [F1] or [R3, R4], depending on the type of the returned value.
We treat a function without result as a function with one integer result. *)
-Definition loc_result (s: signature) : list mreg :=
+Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
- | None => R3 :: nil
- | Some (Tint | Tany32) => R3 :: nil
- | Some (Tfloat | Tsingle | Tany64) => F1 :: nil
- | Some Tlong => R3 :: R4 :: nil
+ | None => One R3
+ | Some (Tint | Tany32) => One R3
+ | Some (Tfloat | Tsingle | Tany64) => One F1
+ | Some Tlong => Twolong R3 R4
end.
-(** The result registers have types compatible with that given in the signature. *)
-
Lemma loc_result_type:
forall sig,
- subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true.
+ subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold proj_sig_res, loc_result.
+ destruct (sig_res sig) as [[]|]; simpl; destruct Archi.ppc64; auto.
Qed.
(** The result locations are caller-save registers *)
Lemma loc_result_caller_save:
- forall (s: signature) (r: mreg),
- In r (loc_result s) -> is_callee_save r = false.
+ forall (s: signature),
+ forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- assert (r = R3 \/ r = R4 \/ r = F1).
- unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
- destruct H0 as [A | [A | A]]; subst r; reflexivity.
+ unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+Qed.
+
+(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
+
+Lemma loc_result_pair:
+ forall sg,
+ match loc_result sg with
+ | One _ => True
+ | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+ end.
+Proof.
+ intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto.
+ simpl; destruct Archi.ppc64; intuition congruence.
Qed.
(** ** Location of function arguments *)
@@ -134,39 +144,39 @@ Definition float_param_regs :=
F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: nil.
Fixpoint loc_arguments_rec
- (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc :=
+ (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| (Tint | Tany32) as ty :: tys =>
match list_nth_z int_param_regs ir with
| None =>
- S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 1)
+ One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 1)
| Some ireg =>
- R ireg :: loc_arguments_rec tys (ir + 1) fr ofs
+ One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs
end
| (Tfloat | Tsingle | Tany64) as ty :: tys =>
match list_nth_z float_param_regs fr with
| None =>
let ofs := align ofs 2 in
- S Outgoing ofs ty :: loc_arguments_rec tys ir fr (ofs + 2)
+ One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 2)
| Some freg =>
- R freg :: loc_arguments_rec tys ir (fr + 1) ofs
+ One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
end
| Tlong :: tys =>
let ir := align ir 2 in
match list_nth_z int_param_regs ir, list_nth_z int_param_regs (ir + 1) with
| Some r1, Some r2 =>
- R r1 :: R r2 :: loc_arguments_rec tys (ir + 2) fr ofs
+ Twolong (R r1) (R r2) :: loc_arguments_rec tys (ir + 2) fr ofs
| _, _ =>
let ofs := align ofs 2 in
- S Outgoing ofs Tint :: S Outgoing (ofs + 1) Tint :: loc_arguments_rec tys ir fr (ofs + 2)
+ Twolong (S Outgoing ofs Tint) (S Outgoing (ofs + 1) Tint) :: loc_arguments_rec tys ir fr (ofs + 2)
end
end.
(** [loc_arguments s] returns the list of locations where to store arguments
when calling a function with signature [s]. *)
-Definition loc_arguments (s: signature) : list loc :=
+Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_args) 0 0 0.
(** [size_arguments s] returns the number of [Outgoing] slots used
@@ -206,15 +216,22 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
| _ => False
end.
-Remark loc_arguments_rec_charact:
- forall tyl ir fr ofs l,
- In l (loc_arguments_rec tyl ir fr ofs) ->
+Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
match l with
| R r => In r int_param_regs \/ In r float_param_regs
| S Outgoing ofs' ty => ofs' >= ofs /\ (typealign ty | ofs')
- | S _ _ _ => False
+ | _ => False
end.
+
+Remark loc_arguments_rec_charact:
+ forall tyl ir fr ofs p,
+ In p (loc_arguments_rec tyl ir fr ofs) ->
+ forall_rpair (loc_argument_charact ofs) p.
Proof.
+ assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
+ { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+ assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
+ { destruct p; simpl; intuition eauto. }
Opaque list_nth_z.
induction tyl; simpl loc_arguments_rec; intros.
elim H.
@@ -224,66 +241,63 @@ Opaque list_nth_z.
subst. left. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
subst. split. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+ eapply Y; eauto. omega.
- (* float *)
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
- assert (ofs <= align ofs 2) by (apply align_le; omega).
- intuition omega.
+ subst. split. omega. apply Z.divide_1_l.
+ eapply Y; eauto. omega.
- (* long *)
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
set (ir' := align ir 2) in *.
destruct (list_nth_z int_param_regs ir') as [r1|] eqn:E1.
destruct (list_nth_z int_param_regs (ir' + 1)) as [r2|] eqn:E2.
- destruct H. subst; left; eapply list_nth_z_in; eauto.
- destruct H. subst; left; eapply list_nth_z_in; eauto.
+ destruct H. subst; split; left; eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- assert (ofs <= align ofs 2) by (apply align_le; omega).
- destruct H. subst. split. omega. apply Z.divide_1_l.
- destruct H. subst. split. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
- assert (ofs <= align ofs 2) by (apply align_le; omega).
- destruct H. subst. split. omega. apply Z.divide_1_l.
- destruct H. subst. split. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+ destruct H.
+ subst. split; (split; [omega|apply Z.divide_1_l]).
+ eapply Y; eauto. omega.
+ destruct H.
+ subst. split; (split; [omega|apply Z.divide_1_l]).
+ eapply Y; eauto. omega.
- (* single *)
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
- assert (ofs <= align ofs 2) by (apply align_le; omega).
- intuition omega.
+ subst. split. omega. apply Z.divide_1_l.
+ eapply Y; eauto. omega.
- (* any32 *)
destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
subst. left. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
subst. split. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
-- (* any64 *)
+ eapply Y; eauto. omega.
+- (* float *)
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
- assert (ofs <= align ofs 2) by (apply align_le; omega).
- intuition omega.
+ subst. split. omega. apply Z.divide_1_l.
+ eapply Y; eauto. omega.
Qed.
Lemma loc_arguments_acceptable:
- forall (s: signature) (l: loc),
- In l (loc_arguments s) -> loc_argument_acceptable l.
+ forall (s: signature) (p: rpair loc),
+ In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
Proof.
unfold loc_arguments; intros.
+ exploit loc_arguments_rec_charact; eauto.
assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
- generalize (loc_arguments_rec_charact _ _ _ _ _ H).
- destruct l.
- intros [C|C]; simpl; auto.
- destruct sl; try contradiction. simpl; auto.
+ assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
+ { unfold loc_argument_charact, loc_argument_acceptable.
+ destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. }
+ unfold forall_rpair; destruct p; intuition auto.
Qed.
+
Hint Resolve loc_arguments_acceptable: locs.
(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
@@ -324,12 +338,12 @@ Qed.
Lemma loc_arguments_bounded:
forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (loc_arguments s) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
ofs + typesize ty <= size_arguments s.
Proof.
intros.
assert (forall tyl ir fr ofs0,
- In (S Outgoing ofs ty) (loc_arguments_rec tyl ir fr ofs0) ->
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) ->
ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0).
{
induction tyl; simpl; intros.
@@ -348,19 +362,19 @@ Proof.
inv H0. apply size_arguments_rec_above. eauto.
- (* long *)
set (ir' := align ir 2) in *.
- destruct (list_nth_z int_param_regs ir').
- destruct (list_nth_z int_param_regs (ir' + 1)).
+ assert (DFL:
+ In (S Outgoing ofs ty) (regs_of_rpairs
+ (Twolong (S Outgoing (align ofs0 2) Tint)
+ (S Outgoing (align ofs0 2 + 1) Tint)
+ :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) ->
+ ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)).
+ { intros IN. destruct IN. inv H1.
+ transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
+ destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
+ auto. }
+ destruct (list_nth_z int_param_regs ir'); auto.
+ destruct (list_nth_z int_param_regs (ir' + 1)); auto.
destruct H0. congruence. destruct H0. congruence. eauto.
- destruct H0. inv H0.
- transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
- destruct H0. inv H0.
- transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
- eauto.
- destruct H0. inv H0.
- transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
- destruct H0. inv H0.
- transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
- eauto.
- (* single *)
destruct (list_nth_z float_param_regs fr); destruct H0.
congruence.
generated by cgit (git 2.34.1) at 2024-06-02 15:36:16 +0000