From e66be6e05b190c51b38d628884ef3e015ebf73fd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 24 Feb 2020 19:59:43 +0100 Subject: Make single arg alignment depend on toolchain. GCC does passes single arguments as singles on the stack but diab and the eabi say single arguments should be passed as double on the stack. This commit changes the alignment of single arguments to 4 for gcc based backends. --- powerpc/Archi.v | 3 +++ powerpc/Conventions1.v | 17 ++++++++++++++--- powerpc/extractionMachdep.v | 3 +++ 3 files changed, 20 insertions(+), 3 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..88fff302 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,9 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** Should singles be passed as single or double *) +Parameter single_passed_as_single : bool. + Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1f048694..5639ff8d 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -208,7 +208,16 @@ Fixpoint loc_arguments_rec | Some ireg => One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs end - | (Tfloat | Tsingle | Tany64) as ty :: tys => + | Tsingle as ty :: tys => + match list_nth_z float_param_regs fr with + | None => + let ty := if Archi.single_passed_as_single then Tsingle else Tfloat in + let ofs := align ofs (typesize ty) in + One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) + | Some freg => + One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs + end + | (Tfloat | Tany64) as ty :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in @@ -295,12 +304,14 @@ Opaque list_nth_z. apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. eapply Y; eauto. omega. - (* single *) + assert (ofs <= align ofs 1) by (apply align_le; omega). 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. omega. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. destruct Archi.single_passed_as_single; simpl; omega. + destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l. + eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega. - (* any32 *) destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 7482435f..a3e945bf 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 => | ""e5500"" -> true | _ -> false end". + +(* Choice of passing of single *) +Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain". -- cgit From 9190ca38b3ae098186421a7cc21a087666a6a677 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Feb 2020 10:10:23 +0100 Subject: In strict PPC ABI mode, pass single FP on stack in double FP format The EABI and the SVR4 ABI state that single-precision FP arguments passed on stack are passed as a 64-bit word, extended to double-precision. This commit implements this behavior by using a stack slot of type Tany64. Not only this ensures that the slot is of size and alignment 8 bytes, but it also ensures that it is accessed by stfd and lfd instructions, using single-extended-to-double format. --- powerpc/Conventions1.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 5639ff8d..5c9cbd4f 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -211,9 +211,9 @@ Fixpoint loc_arguments_rec | Tsingle as ty :: tys => match list_nth_z float_param_regs fr with | None => - let ty := if Archi.single_passed_as_single then Tsingle else Tfloat in + let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in let ofs := align ofs (typesize ty) in - One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) + One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) | Some freg => One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs end -- cgit From 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Feb 2020 10:15:40 +0100 Subject: Documentation comment for single_passed_as_single --- powerpc/Archi.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 88fff302..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,7 +30,8 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. -(** Should singles be passed as single or double *) +(** Should single-precision FP arguments passed on stack be passed + as singles or use double FP format. *) Parameter single_passed_as_single : bool. Definition splitlong := negb ppc64. -- cgit From 63c878610c5ef531731f5d9f83570f19c8c1acbc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 15:08:43 +0100 Subject: CSE2 for powerpc --- powerpc/CSE2deps.v | 20 ++++++++ powerpc/CSE2depsproof.v | 132 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 152 insertions(+) create mode 100644 powerpc/CSE2deps.v create mode 100644 powerpc/CSE2depsproof.v (limited to 'powerpc') diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v new file mode 100644 index 00000000..9db51bbb --- /dev/null +++ b/powerpc/CSE2deps.v @@ -0,0 +1,20 @@ +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (base :: nil), (base' :: nil) => + if peq base base' + then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk) + else true | _, _, _, _ => true + end. diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v new file mode 100644 index 00000000..2112a230 --- /dev/null +++ b/powerpc/CSE2depsproof.v @@ -0,0 +1,132 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = 32%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw valr : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + Hypothesis READ : Mem.loadv chunkr m addrr = Some valr. + + Section INDEXED_AWAY. + Variable ofsw ofsr : int. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr + \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + rewrite ptrofs_modulus in *. + simpl in *. + inv ADDRR. + inv ADDRW. + rewrite <- READ. + destruct base; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: unfold Ptrofs.of_int. + + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' vl rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m a') = Some vl -> + (Mem.loadv chunk' m' a') = Some vl. +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE LOAD. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. -- cgit