From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 17 May 2016 15:37:56 +0200 Subject: Introduce register pairs to describe calling conventions more precisely This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations. In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves. Summary of changes: - AST: introduce the type "rpair A" of register pairs - Conventions1, Conventions: use it when describing calling conventions - LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls - Events: suppress external_call', no longer useful - All passes from Allocation to Asmgen: adapt accordingly. --- arm/Asm.v | 51 +++++--- arm/Asmgenproof.v | 6 +- arm/Conventions1.v | 262 +++++++++++++++++-------------------- backend/Allocation.v | 77 +++++------ backend/Allocproof.v | 302 ++++++++++++++++++++----------------------- backend/Asmgenproof0.v | 60 +++++---- backend/CleanupLabelsproof.v | 4 +- backend/Conventions.v | 48 ++++--- backend/Debugvarproof.v | 4 +- backend/LTL.v | 11 +- backend/Linear.v | 11 +- backend/Linearizeproof.v | 4 +- backend/Lineartyping.v | 22 ++-- backend/Locations.v | 34 +++-- backend/Mach.v | 31 +++-- backend/RTLtyping.v | 6 +- backend/Regalloc.ml | 74 +++++++---- backend/Stackingproof.v | 119 +++++++++-------- backend/Tunnelingproof.v | 4 +- backend/XTL.ml | 5 + backend/XTL.mli | 1 + cfrontend/PrintClight.ml | 2 +- cfrontend/PrintCsyntax.ml | 4 +- common/AST.v | 57 +++++++- common/Events.v | 187 --------------------------- configure | 2 +- ia32/Asm.v | 52 +++++--- ia32/Asmgenproof.v | 6 +- ia32/Conventions1.v | 123 +++++++++++------- powerpc/Asm.v | 51 +++++--- powerpc/Asmgenproof.v | 6 +- powerpc/Conventions1.v | 156 ++++++++++++---------- 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. -- cgit From 4e2fb826bd95e3f32459f1845948f37add3cbdb9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 24 May 2016 10:10:00 +0200 Subject: configure: regression on Menhir's minimal version --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure b/configure index 6b0b4da8..2dc60d28 100755 --- a/configure +++ b/configure @@ -314,7 +314,7 @@ else ocaml_opt_comp=false fi -MENHIR_REQUIRED=20151112 +MENHIR_REQUIRED=20160303 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 -- cgit From 8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 24 May 2016 10:10:14 +0200 Subject: ia32/Conventions1: remove commented-out proof attempt --- ia32/Conventions1.v | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v index 672b4219..08a86815 100644 --- a/ia32/Conventions1.v +++ b/ia32/Conventions1.v @@ -213,23 +213,6 @@ 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) (regs_of_rpairs (loc_arguments s)) -> -- cgit