From 08efc2a09b850476e39469791650faf99dd06183 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Feb 2020 13:56:07 +0100 Subject: Platform-independent implementation of Conventions.size_arguments (#222) The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions. --- arm/Conventions1.v | 206 ----------------------------------------------------- 1 file changed, 206 deletions(-) (limited to 'arm') diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 7016c1ee..fe49a781 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -269,48 +269,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) := else loc_arguments_hf s.(sig_args) 0 0 0 end. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint|Tany32) :: tys => - if zlt ir 4 - then size_arguments_hf tys (ir + 1) fr ofs - else size_arguments_hf tys ir fr (ofs + 1) - | (Tfloat|Tany64) :: tys => - if zlt fr 8 - then size_arguments_hf tys ir (fr + 1) ofs - else size_arguments_hf tys ir fr (align ofs 2 + 2) - | Tsingle :: tys => - if zlt fr 8 - then size_arguments_hf tys ir (fr + 1) ofs - else size_arguments_hf tys ir fr (ofs + 1) - | Tlong :: tys => - let ir := align ir 2 in - if zlt ir 4 - then size_arguments_hf tys (ir + 2) fr ofs - else size_arguments_hf tys ir fr (align ofs 2 + 2) - end. - -Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z := - match tyl with - | nil => Z.max 0 ofs - | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1) - | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2) - end. - -Definition size_arguments (s: signature) : Z := - match Archi.abi with - | Archi.Softfloat => - size_arguments_sf s.(sig_args) (-4) - | Archi.Hardfloat => - if s.(sig_cc).(cc_vararg) - then size_arguments_sf s.(sig_args) (-4) - else size_arguments_hf s.(sig_args) 0 0 0 - end. - (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -471,170 +429,6 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_hf_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_hf tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a. - destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (zlt fr 8); 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 (zlt ir' 4); 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 (zlt fr 8); eauto. - apply Z.le_trans with (ofs0 + 1); eauto. omega. - destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (zlt fr 8); 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. - -Remark size_arguments_sf_above: - forall tyl ofs0, - Z.max 0 ofs0 <= size_arguments_sf tyl ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a; (eapply Z.le_trans; [idtac|eauto]). - xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. - xomega. - xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - assert (0 <= size_arguments_sf (sig_args s) (-4)). - { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. } - assert (0 <= size_arguments_hf (sig_args s) 0 0 0). - { apply size_arguments_hf_above. } - destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. -Qed. - -Lemma loc_arguments_hf_bounded: - forall ofs ty 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. - elim H. - destruct a. -- (* int *) - destruct (zlt ir 4); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* float *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* long *) - destruct (zlt (align ir 2) 4). - destruct H. discriminate. destruct H. discriminate. eauto. - destruct Archi.big_endian. - destruct H. inv H. - eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. - destruct H. inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. - eauto. - destruct H. inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. - destruct H. inv H. - eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. - eauto. -- (* float *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* any32 *) - destruct (zlt ir 4); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* any64 *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -Qed. - -Lemma loc_arguments_sf_bounded: - forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> - Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. -Proof. - induction tyl; simpl; intros. - elim H. - destruct a. -- (* int *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* float *) - destruct H. - destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above. - eauto. -- (* long *) - destruct H. - destruct Archi.big_endian. - destruct (zlt (align ofs0 2) 0); inv H. - eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. - destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. - destruct H. - destruct Archi.big_endian. - destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. - destruct (zlt (align ofs0 2) 0); inv H. - eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. - eauto. -- (* float *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* any32 *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* any64 *) - destruct H. - destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above. - eauto. -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. - unfold loc_arguments, size_arguments; intros. - 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 Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } - 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. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. -- cgit From 091e00ed16d4189c27a05ad7056eab47bd29f5b7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 14:39:31 +0100 Subject: CSE2 for ARM --- arm/CSE2depsproof.v | 132 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 arm/CSE2depsproof.v (limited to 'arm') diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v new file mode 100644 index 00000000..2112a230 --- /dev/null +++ b/arm/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 From 3b640f041be480b82f1b3a1f695ed8a57193bf28 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 15:28:27 +0100 Subject: CSE2 with alias analysis --- arm/CSE2deps.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 arm/CSE2deps.v (limited to 'arm') diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v new file mode 100644 index 00000000..9db51bbb --- /dev/null +++ b/arm/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. -- cgit From f503e4287bc76150fd3ec5be8c076bf734361493 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 17:56:53 +0100 Subject: ported to arm --- arm/CSE2depsproof.v | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'arm') diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v index 2112a230..61fe5980 100644 --- a/arm/CSE2depsproof.v +++ b/arm/CSE2depsproof.v @@ -34,9 +34,8 @@ Section MEMORY_WRITE. Variable chunkw chunkr : memory_chunk. Variable base : val. - Variable addrw addrr valw valr : val. + Variable addrw addrr valw : 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. @@ -50,7 +49,7 @@ Section MEMORY_WRITE. 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. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intros. @@ -62,7 +61,6 @@ Section MEMORY_WRITE. 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. @@ -83,7 +81,7 @@ Section MEMORY_WRITE. Theorem load_store_away : can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true -> - Mem.loadv chunkr m2 addrr = Some valr. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intro SWAP. unfold can_swap_accesses_ofs in SWAP. @@ -105,16 +103,15 @@ Section SOUNDNESS. Lemma may_overlap_sound: forall m m' : mem, - forall chunk addr args chunk' addr' args' v a a' vl rs, + 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') = Some vl -> - (Mem.loadv chunk' m' a') = Some vl. + (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a'). Proof. intros until rs. - intros ADDR ADDR' OVERLAP STORE LOAD. + intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. { (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. -- cgit From 0ebdbc31c3e992e43d85699a039ebdd23e272df6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 07:49:46 +0100 Subject: DuplicateOpcodeHeuristic for ARM --- arm/DuplicateOpcodeHeuristic.ml | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) (limited to 'arm') diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml index 85505245..9b6a6409 100644 --- a/arm/DuplicateOpcodeHeuristic.ml +++ b/arm/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,22 @@ -exception HeuristicSucceeded - -let opcode_heuristic code cond ifso ifnot preferred = () +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 + | Ccompf c | Ccompfs c -> (match c with + | Ceq -> Some false + | Cne -> Some true + | _ -> None + ) + | Cnotcompf c | Cnotcompfs c -> (match c with + | Ceq -> Some true + | Cne -> Some false + | _ -> None + ) + | _ -> None + -- cgit