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. --- x86/Asmexpand.ml | 2 +- x86/Conventions1.v | 145 ----------------------------------------------------- 2 files changed, 1 insertion(+), 146 deletions(-) (limited to 'x86') diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index c82d406e..b8353046 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r = invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments + (mul 4l (Z.to_int32 (Conventions.size_arguments (get_current_function_sig ()))))) in emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 01b15e98..fdd94239 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -220,36 +220,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) := then loc_arguments_64 s.(sig_args) 0 0 0 else loc_arguments_32 s.(sig_args) 0. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_32 - (tyl: list typ) (ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | ty :: tys => size_arguments_32 tys (ofs + typesize ty) - end. - -Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint | Tlong | Tany32 | Tany64) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_64 tys ir fr (ofs + 2) - | Some ireg => size_arguments_64 tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_64 tys ir fr (ofs + 2) - | Some freg => size_arguments_64 tys ir (fr + 1) ofs - end - end. - -Definition size_arguments (s: signature) : Z := - if Archi.ptr64 - then size_arguments_64 s.(sig_args) 0 0 0 - else size_arguments_32 s.(sig_args) 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -351,121 +321,6 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_32_above: - forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0. -Proof. - induction tyl; simpl; intros. - omega. - apply Z.le_trans with (ofs0 + typesize a); auto. - generalize (typesize_pos a); omega. -Qed. - -Remark size_arguments_64_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_64 tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - assert (A: ofs0 <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z int_param_regs ir); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - assert (B: ofs0 <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - destruct a; auto. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. -Qed. - -Lemma loc_arguments_32_bounded: - forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) -> - ofs + typesize ty <= size_arguments_32 tyl ofs0. -Proof. - induction tyl as [ | t l]; simpl; intros x IN. -- contradiction. -- rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above]. - Ltac decomp := - match goal with - | [ H: _ \/ _ |- _ ] => destruct H; decomp - | [ H: S _ _ _ = S _ _ _ |- _ ] => inv H - | [ H: False |- _ ] => contradiction - end. - destruct t; simpl in IN; decomp; simpl; omega. -+ apply IHl; auto. -Qed. - -Lemma loc_arguments_64_bounded: - forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - contradiction. - assert (T: forall ty0, typesize ty0 <= 2). - { destruct ty0; simpl; omega. } - assert (A: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z int_param_regs ir with - | Some ireg => - One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - - eapply IHtyl; eauto. } - assert (B: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z float_param_regs fr with - | Some ireg => - One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - - eapply IHtyl; eauto. } - destruct a; 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. - destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. -- cgit From b11cbccf7eb4a6696c5285cb0bcde57dd0c0447e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 10:41:33 +0100 Subject: starting to move x86 stuff to x86 --- x86/CSE2depsproof.v | 215 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 215 insertions(+) create mode 100644 x86/CSE2depsproof.v (limited to 'x86') diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v new file mode 100644 index 00000000..f4eace6f --- /dev/null +++ b/x86/CSE2depsproof.v @@ -0,0 +1,215 @@ +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. +Require Import Lia. + +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. + + Lemma size_chunk_bounded : + forall chunk, 0 <= size_chunk chunk <= max_chunk_size. + Proof. + unfold max_chunk_size. + destruct chunk; simpl; lia. + Qed. + + 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 : Z. + 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 <= ofsw <= Ptrofs.modulus - max_chunk_size, + forall RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size, + forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr + \/ ofsr + size_chunk chunkr <= ofsw, + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + + pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded. + pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded. + unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded. + try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *. + try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *. + destruct addrr ; simpl in * ; try discriminate. + unfold eval_addressing in *. + destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. + rewrite PTR64 in *. + + inv ADDRR. + inv ADDRW. + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + + all: unfold Ptrofs.of_int64. + all: unfold Ptrofs.of_int. + + + all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). + + all: try change Ptrofs.modulus with 4294967296. + all: try change Ptrofs.modulus with 18446744073709551616. + + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs ofsr chunkr 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. + + Section DIFFERENT_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis symw symr : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal symw ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal symr ofsr) nil = Some addrr. + + Lemma load_store_diff_globals : + symw <> symr -> + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + unfold eval_addressing in *. + destruct Archi.ptr64 eqn:PTR64; simpl in *. + rewrite PTR64 in *. + 2: simpl in *; discriminate. + unfold Genv.symbol_address in *. + unfold Genv.find_symbol in *. + destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW. + 2: simpl in STORE; discriminate. + destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR. + 2: simpl in READ; discriminate. + assert (br <> bw). + { + intro EQ. + subst br. + assert (symr = symw). + { + eapply Genv.genv_vars_inj; eauto. + } + congruence. + } + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw). + - exact STORE. + - left. assumption. + Qed. + End DIFFERENT_GLOBALS. + + Section SAME_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis sym : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal sym ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal sym ofsr) nil = Some addrr. + + Lemma load_store_glob_away1 : + forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - max_chunk_size, + forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - max_chunk_size, + forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr) + \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.unsigned ofsw), + Mem.loadv chunkr m2 addrr = Some valr. + Proof. + intros. + + pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded. + pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded. + unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded. + try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *. + try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *. + unfold eval_addressing, eval_addressing32, eval_addressing64 in *. + destruct Archi.ptr64 eqn:PTR64. + + { + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. + } + + { + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + rewrite <- READ. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. + } + Qed. + + Lemma load_store_glob_away : + (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.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_glob_away1. + all: tauto. + Qed. + End SAME_GLOBALS. +End MEMORY_WRITE. +End SOUNDNESS. -- cgit From 577d3dbeb54aaf23db19dddf149c48764e20c58d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 11:30:23 +0100 Subject: moved away x86-dependent parts --- x86/CSE2depsproof.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) (limited to 'x86') diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v index f4eace6f..84b22c69 100644 --- a/x86/CSE2depsproof.v +++ b/x86/CSE2depsproof.v @@ -213,3 +213,49 @@ Section MEMORY_WRITE. End SAME_GLOBALS. 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 z0 chunk' z chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away; eassumption. + } + { (* Aglobal / Aglobal *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + simpl in *. + destruct (peq i i1). + { + subst i1. + rewrite negb_false_iff in OVERLAP. + eapply load_store_glob_away; eassumption. + } + eapply load_store_diff_globals; eassumption. + } +Qed. + +End SOUNDNESS. -- cgit From 4096e8c1b1e3d4fcdb44e81844d65a74f881aa47 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 13:33:54 +0100 Subject: better 32/64-bit handling --- x86/CSE2deps.v | 24 ++++++++++++++++++++++++ x86/CSE2depsproof.v | 53 +++++++++++++++++++++++++++-------------------------- 2 files changed, 51 insertions(+), 26 deletions(-) create mode 100644 x86/CSE2deps.v (limited to 'x86') diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v new file mode 100644 index 00000000..f4d9e254 --- /dev/null +++ b/x86/CSE2deps.v @@ -0,0 +1,24 @@ +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 ofs' chunk' ofs chunk) + else true + | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil => + if peq symb symb' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else false + | _, _, _, _ => true + end. diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v index 84b22c69..37e16dfe 100644 --- a/x86/CSE2depsproof.v +++ b/x86/CSE2depsproof.v @@ -5,7 +5,7 @@ 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. +Require Import CSE2 CSE2deps. Require Import Lia. Section SOUNDNESS. @@ -17,13 +17,6 @@ Section MEMORY_WRITE. Variable m m2 : mem. Variable chunkw chunkr : memory_chunk. Variable base : val. - - Lemma size_chunk_bounded : - forall chunk, 0 <= size_chunk chunk <= max_chunk_size. - Proof. - unfold max_chunk_size. - destruct chunk; simpl; lia. - Qed. Variable addrw addrr valw valr : val. Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. @@ -37,19 +30,18 @@ Section MEMORY_WRITE. (Aindexed ofsr) (base :: nil) = Some addrr. Lemma load_store_away1 : - forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - max_chunk_size, - forall RANGER : 0 <= ofsr <= Ptrofs.modulus - max_chunk_size, + forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk, forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr \/ ofsr + size_chunk chunkr <= ofsw, Mem.loadv chunkr m2 addrr = Some valr. Proof. intros. - pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded. - pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded. - unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded. - try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *. - try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *. + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. destruct addrr ; simpl in * ; try discriminate. unfold eval_addressing in *. destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. @@ -111,16 +103,25 @@ Section MEMORY_WRITE. (Aglobal symw ofsw) nil = Some addrw. Hypothesis ADDRR : eval_addressing genv sp (Aglobal symr ofsr) nil = Some addrr. - + + Lemma ptr64_cases: + forall {T : Type}, + forall b : bool, + forall x y : T, + (if b then (if b then x else y) else (if b then y else x)) = x. + Proof. + destruct b; reflexivity. + Qed. + Lemma load_store_diff_globals : symw <> symr -> Mem.loadv chunkr m2 addrr = Some valr. Proof. intros. unfold eval_addressing in *. - destruct Archi.ptr64 eqn:PTR64; simpl in *. - rewrite PTR64 in *. - 2: simpl in *; discriminate. + simpl in *. + rewrite ptr64_cases in ADDRR. + rewrite ptr64_cases in ADDRW. unfold Genv.symbol_address in *. unfold Genv.find_symbol in *. destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW. @@ -153,19 +154,19 @@ Section MEMORY_WRITE. (Aglobal sym ofsr) nil = Some addrr. Lemma load_store_glob_away1 : - forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - max_chunk_size, - forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - max_chunk_size, + forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - largest_size_chunk, forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr) \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.unsigned ofsw), Mem.loadv chunkr m2 addrr = Some valr. Proof. intros. - pose proof (size_chunk_bounded chunkr) as size_chunkr_bounded. - pose proof (size_chunk_bounded chunkw) as size_chunkw_bounded. - unfold max_chunk_size in size_chunkr_bounded, size_chunkw_bounded. - try change (Ptrofs.modulus - max_chunk_size) with 4294967288 in *. - try change (Ptrofs.modulus - max_chunk_size) with 18446744073709551608 in *. + 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 size_chunkr_bounded, size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. unfold eval_addressing, eval_addressing32, eval_addressing64 in *. destruct Archi.ptr64 eqn:PTR64. -- cgit From d14c78013f654ca586681136ba291f1487f1b586 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 17:23:01 +0100 Subject: adjust for x86 --- x86/CSE2depsproof.v | 79 ++++++++++++++++++++++++----------------------------- 1 file changed, 35 insertions(+), 44 deletions(-) (limited to 'x86') diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v index 37e16dfe..1e913254 100644 --- a/x86/CSE2depsproof.v +++ b/x86/CSE2depsproof.v @@ -18,9 +18,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 : Z. @@ -34,7 +33,7 @@ Section MEMORY_WRITE. forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk, forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr \/ ofsr + size_chunk chunkr <= ofsw, - Mem.loadv chunkr m2 addrr = Some valr. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intros. @@ -42,14 +41,13 @@ Section MEMORY_WRITE. pose proof (max_size_chunk chunkw) as size_chunkw_bounded. try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. - destruct addrr ; simpl in * ; try discriminate. - unfold eval_addressing in *. + destruct addrr ; simpl in * ; trivial. + unfold eval_addressing, eval_addressing32, eval_addressing64 in *. destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. rewrite PTR64 in *. inv ADDRR. inv ADDRW. - rewrite <- READ. eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). exact STORE. right. @@ -84,7 +82,7 @@ Section MEMORY_WRITE. Theorem load_store_away : can_swap_accesses_ofs ofsr chunkr 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. @@ -113,9 +111,20 @@ Section MEMORY_WRITE. destruct b; reflexivity. Qed. + (* not needed + Lemma bool_cases_same: + forall {T : Type}, + forall b : bool, + forall x : T, + (if b then x else x) = x. + Proof. + destruct b; reflexivity. + Qed. + *) + Lemma load_store_diff_globals : symw <> symr -> - Mem.loadv chunkr m2 addrr = Some valr. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intros. unfold eval_addressing in *. @@ -127,7 +136,7 @@ Section MEMORY_WRITE. destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW. 2: simpl in STORE; discriminate. destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR. - 2: simpl in READ; discriminate. + 2: reflexivity. assert (br <> bw). { intro EQ. @@ -138,7 +147,6 @@ Section MEMORY_WRITE. } congruence. } - rewrite <- READ. eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw). - exact STORE. - left. assumption. @@ -158,7 +166,7 @@ Section MEMORY_WRITE. forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - largest_size_chunk, forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr) \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.unsigned ofsw), - Mem.loadv chunkr m2 addrr = Some valr. + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. Proof. intros. @@ -168,40 +176,24 @@ Section MEMORY_WRITE. try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. unfold eval_addressing, eval_addressing32, eval_addressing64 in *. - destruct Archi.ptr64 eqn:PTR64. - - { - unfold Genv.symbol_address in *. - inv ADDRR. - inv ADDRW. - destruct (Genv.find_symbol genv sym). - 2: discriminate. - - rewrite <- READ. - eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). - exact STORE. - right. - tauto. - } - { - unfold Genv.symbol_address in *. - inv ADDRR. - inv ADDRW. - destruct (Genv.find_symbol genv sym). - 2: discriminate. - - rewrite <- READ. - eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). - exact STORE. - right. - tauto. - } + rewrite ptr64_cases in ADDRR. + rewrite ptr64_cases in ADDRW. + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. Qed. Lemma load_store_glob_away : (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.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. @@ -223,16 +215,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 aa2e3d776cb82ce01c4afdbacc52951e60ff2104 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 17 Mar 2020 08:10:26 +0100 Subject: DuplicateOpcodeHeuristic x86 --- x86/DuplicateOpcodeHeuristic.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'x86') diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml index 85505245..2ec314c1 100644 --- a/x86/DuplicateOpcodeHeuristic.ml +++ b/x86/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 | 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