diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Archi.v | 4 | ||||
-rw-r--r-- | powerpc/CSE2deps.v | 20 | ||||
-rw-r--r-- | powerpc/CSE2depsproof.v | 135 | ||||
-rw-r--r-- | powerpc/Conventions1.v | 143 | ||||
-rw-r--r-- | powerpc/DuplicateOpcodeHeuristic.ml | 30 | ||||
-rw-r--r-- | powerpc/extractionMachdep.v | 3 |
6 files changed, 203 insertions, 132 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,10 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** 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. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. 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..fdded9b6 --- /dev/null +++ b/powerpc/CSE2depsproof.v @@ -0,0 +1,135 @@ +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 = if Archi.ptr64 then 64%nat else 32%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Lemma ptrofs_max_unsigned : + Ptrofs.max_unsigned = if Archi.ptr64 then 18446744073709551615 else 4294967295. +Proof. + unfold Ptrofs.max_unsigned. + rewrite ptrofs_modulus. + 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 : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + 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 = Mem.loadv chunkr m addrr. + 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. + 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: unfold Ptrofs.of_int. + + all: repeat rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; rewrite ptrofs_modulus; destruct Archi.ptr64; lia). + all: repeat rewrite ptrofs_modulus. + all: destruct Archi.ptr64; 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 = Mem.loadv chunkr m addrr. + 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' 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') = (Mem.loadv chunk' m a'). +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE. + 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. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 25d9c081..5c9cbd4f 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 Tany64 in + let ofs := align ofs (typesize ty) in + 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 + | (Tfloat | Tany64) as ty :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in @@ -236,33 +245,6 @@ Fixpoint loc_arguments_rec 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 - to call a function with signature [s]. *) - -Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint | Tany32) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_rec tys ir fr (ofs + 1) - | Some ireg => size_arguments_rec tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle | Tany64) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_rec tys ir fr (align ofs 2 + 2) - | Some freg => size_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 => size_arguments_rec tys (ir + 2) fr ofs - | _, _ => size_arguments_rec tys ir fr (align ofs 2 + 2) - end - end. - -Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) 0 0 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -322,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. @@ -359,105 +343,6 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_rec_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_rec tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a. - destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - set (ir' := align ir 2). - destruct (list_nth_z int_param_regs ir'); eauto. - destruct (list_nth_z int_param_regs (ir' + 1)); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - apply size_arguments_rec_above. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - 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) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0). -{ - induction tyl; simpl; intros. - elim H0. - destruct a. -- (* int *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* float *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. -- (* long *) - set (ir' := align ir 2) in *. - assert (DFL: - In (S Outgoing ofs ty) (regs_of_rpairs - ((if Archi.ptr64 - then One (S Outgoing (align ofs0 2) Tlong) - else 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)). - { destruct Archi.ptr64; intros IN. - - destruct IN. inv H1. apply size_arguments_rec_above. auto. - - 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. -- (* single *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - eauto. -- (* any32 *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* any64 *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. - } - eauto. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml index 85505245..33be79e8 100644 --- a/powerpc/DuplicateOpcodeHeuristic.ml +++ b/powerpc/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,27 @@ -exception HeuristicSucceeded - -let opcode_heuristic code cond ifso ifnot preferred = () +(* open Camlcoq *) +open Op +open Integers + +let opcode_heuristic code cond ifso ifnot is_loop_header = + match cond with + | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccompf c -> (match c with + | Ceq -> Some false + | Cne -> Some true + | _ -> None + ) + | Cnotcompf c -> (match c with + | Ceq -> Some true + | Cne -> Some false + | _ -> None + ) + | _ -> None 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". |