From 353b3cee4d08b5820bf62b7228afb67be69f10e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Mar 2013 15:28:28 +0000 Subject: Finished backtracking (cf previous commit) for ARM and PowerPC. ARM: slightly shorter code generated for indirect memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof1.v | 183 +++++++++++++++++++---------------------------------- 1 file changed, 65 insertions(+), 118 deletions(-) (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 8fc8a7ee..9d90d1f0 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -12,7 +12,6 @@ (** Correctness proof for ARM code generation: auxiliary results. *) -(*Require Import Axioms.*) Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -363,6 +362,35 @@ Qed. (** Indexed memory loads. *) +Lemma indexed_memory_access_correct: + forall (P: regset -> Prop) (mk_instr: ireg -> int -> instruction) + (mk_immed: int -> int) (base: ireg) n k (rs: regset) m m', + (forall (r1: ireg) (rs1: regset) n1 k, + Val.add rs1#r1 (Vint n1) = Val.add rs#base (Vint n) -> + (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> + exists rs', + exec_straight ge fn (mk_instr r1 n1 :: k) rs1 m k rs' m' /\ P rs') -> + exists rs', + exec_straight ge fn + (indexed_memory_access mk_instr mk_immed base n k) rs m + k rs' m' + /\ P rs'. +Proof. + intros until m'; intros SEM. + unfold indexed_memory_access. + destruct (Int.eq n (mk_immed n)). +- apply SEM; auto. +- destruct (addimm_correct IR14 base (Int.sub n (mk_immed n)) (mk_instr IR14 (mk_immed n) :: k) rs m) + as (rs1 & A & B & C). + destruct (SEM IR14 rs1 (mk_immed n) k) as (rs2 & D & E). + rewrite B. rewrite Val.add_assoc. f_equal. simpl. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg (mk_immed n))). + rewrite Int.add_neg_zero. rewrite Int.add_zero. auto. + auto with asmgen. + exists rs2; split; auto. eapply exec_straight_trans; eauto. +Qed. + Lemma loadind_int_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> @@ -371,18 +399,10 @@ Lemma loadind_int_correct: /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. - intros; unfold loadind_int. destruct (is_immed_mem_word ofs). - exists (nextinstr (rs#dst <- v)). - split. apply exec_straight_one. simpl. - unfold exec_load. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#dst <- v)). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_load. rewrite B. - rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. auto. - intuition Simpl. + intros; unfold loadind_int. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma loadind_float_correct: @@ -393,18 +413,10 @@ Lemma loadind_float_correct: /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. - intros; unfold loadind_float. destruct (is_immed_mem_float ofs). - exists (nextinstr (rs#dst <- v)). - split. apply exec_straight_one. simpl. - unfold exec_load. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#dst <- v)). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_load. rewrite B. - rewrite Val.add_assoc. simpl. - rewrite Int.add_zero. rewrite H. auto. auto. - intuition Simpl. + intros; unfold loadind_float. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma loadind_correct: @@ -432,19 +444,11 @@ Lemma storeind_int_correct: exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. - intros; unfold storeind_int. destruct (is_immed_mem_word ofs). - exists (nextinstr rs). - split. apply exec_straight_one. simpl. - unfold exec_store. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. - rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. - congruence. auto with asmgen. auto. - intuition Simpl. + intros; unfold storeind_int. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H1. rewrite H2; auto with asmgen. rewrite H; eauto. auto. + intros; Simpl. Qed. Lemma storeind_float_correct: @@ -454,20 +458,11 @@ Lemma storeind_float_correct: exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. - intros; unfold storeind_float. destruct (is_immed_mem_float ofs). - exists (nextinstr rs). - split. apply exec_straight_one. simpl. - unfold exec_store. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. - rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. - congruence. congruence. - auto with asmgen. - intuition Simpl. + intros; unfold storeind_float. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H0. rewrite H1; auto with asmgen. rewrite H; eauto. auto. + intros; Simpl. Qed. Lemma storeind_correct: @@ -541,8 +536,6 @@ Proof. unfold compare_float. Simpl. Qed. -Definition lock {A: Type} (x: A) := x. - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -552,12 +545,8 @@ Ltac ArgsInv := end); subst; repeat (match goal with - | [ H: ireg_of ?x = OK ?y |- _ ] => - simpl in *; rewrite (ireg_of_eq _ _ H) in * -(*; change H with (lock (ireg_of x) = OK y)*) - | [ H: freg_of ?x = OK ?y |- _ ] => - simpl in *; rewrite (freg_of_eq _ _ H) in * -(*; change H with (lock (freg_of x) = OK y)*) + | [ H: ireg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * end). Lemma transl_cond_correct: @@ -833,6 +822,8 @@ Proof. unfold rs2. Simpl. Qed. +(** Translation of loads and stores. *) + Remark val_add_add_zero: forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero). Proof. @@ -842,9 +833,9 @@ Qed. Lemma transl_memory_access_correct: forall (P: regset -> Prop) (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) - (is_immed: int -> bool) + (mk_immed: int -> int) addr args k c (rs: regset) a m m', - transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> + transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> (forall (r1: ireg) (rs1: regset) n k, Val.add rs1#r1 (Vint n) = a -> @@ -854,11 +845,10 @@ Lemma transl_memory_access_correct: match mk_instr_gen with | None => True | Some mk => - (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, - Val.add rs1#r1 (eval_shift_addr sa rs1) = a -> - (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> - exists rs', - exec_straight ge fn (mk r1 sa :: k) rs1 m k rs' m' /\ P rs') + (forall (r1: ireg) (sa: shift_addr) k, + Val.add rs#r1 (eval_shift_addr sa rs) = a -> + exists rs', + exec_straight ge fn (mk r1 sa :: k) rs m k rs' m' /\ P rs') end -> exists rs', exec_straight ge fn c rs m k rs' m' /\ P rs'. @@ -866,56 +856,15 @@ Proof. intros until m'; intros TR EA MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA. (* Aindexed *) - case (is_immed i). - (* Aindexed, small displacement *) - apply MK1; auto. - (* Aindexed, large displacement *) - destruct (addimm_correct IR14 x i (mk_instr_imm IR14 Int.zero :: k) rs m) - as [rs' [A [B C]]]. - exploit (MK1 IR14 rs' Int.zero); eauto. - rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. - intros [rs'' [D E]]. - exists rs''; split. - eapply exec_straight_trans. eexact A. eexact D. auto. + apply indexed_memory_access_correct. exact MK1. (* Aindexed2 *) - destruct mk_instr_gen as [mk | ]. - (* binary form available *) - apply MK2; auto. - (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (rs x0)))). - exploit (MK1 IR14 rs' Int.zero); eauto. - unfold rs'. Simpl. symmetry. apply val_add_add_zero. - intros. unfold rs'. Simpl. - intros [rs'' [A B]]. - exists rs''; split. - eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. auto. auto. + destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. + simpl. erewrite ! ireg_of_eq; eauto. (* Aindexed2shift *) - destruct mk_instr_gen as [mk | ]. - (* binary form available *) - apply MK2; auto. rewrite transl_shift_addr_correct. auto. - (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (eval_shift s (rs x0))))). - exploit (MK1 IR14 rs' Int.zero); eauto. - unfold rs'. Simpl. symmetry. apply val_add_add_zero. - intros; unfold rs'; Simpl. - intros [rs'' [A B]]. - exists rs''; split. - eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. rewrite transl_shift_correct. auto. - auto. + destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. + erewrite ! ireg_of_eq; eauto. rewrite transl_shift_addr_correct. auto. (* Ainstack *) - destruct (is_immed i); inv TR. - (* Ainstack, short displacement *) - apply MK1; auto. - (* Ainstack, large displacement *) - destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m) - as [rs' [A [B C]]]. - exploit (MK1 IR14 rs' Int.zero); eauto. - rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.add_zero; auto. - intros [rs'' [D E]]. - exists rs''; split. - eapply exec_straight_trans. eexact A. eexact D. auto. + inv TR. apply indexed_memory_access_correct. exact MK1. Qed. Lemma transl_load_int_correct: @@ -983,8 +932,7 @@ Proof. intros; Simpl. simpl; intros. econstructor; split. apply exec_straight_one. - rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. - rewrite H1. eauto. auto. + rewrite H2. unfold exec_store. rewrite H. rewrite H1. eauto. auto. intros; Simpl. Qed. @@ -1003,8 +951,7 @@ Proof. intros. monadInv H. erewrite freg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. intros; simpl. econstructor; split. apply exec_straight_one. - rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. - rewrite H1. eauto. auto. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto. intros; Simpl. simpl; auto. Qed. -- cgit