From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 13 +- arm/Asmgen.v | 4 - arm/Asmgenproof.v | 402 ++++++++++------- arm/Asmgenproof1.v | 1077 ++++++++++++++++++++++------------------------ arm/ConstpropOp.v | 7 - arm/Op.v | 88 +++- arm/PrintAsm.ml | 29 +- arm/PrintOp.ml | 8 +- arm/SelectOp.v | 168 ++------ arm/SelectOpproof.v | 143 +++--- arm/linux/Conventions1.v | 4 +- 11 files changed, 966 insertions(+), 977 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index d160be7..7ea1a8a 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -152,9 +152,7 @@ Inductive instruction : Type := | Pcmf: freg -> freg -> instruction (**r float comparison *) | Pdvfd: freg -> freg -> freg -> instruction (**r float division *) | Pfixz: ireg -> freg -> instruction (**r float to signed int *) - | Pfixzu: ireg -> freg -> instruction (**r float to unsigned int *) | Pfltd: freg -> ireg -> instruction (**r signed int to float *) - | Pfltud: freg -> ireg -> instruction (**r unsigned int to float *) | Pldfd: freg -> ireg -> int -> instruction (**r float64 load *) | Pldfs: freg -> ireg -> int -> instruction (**r float32 load *) | Plifd: freg -> float -> instruction (**r load float constant *) @@ -470,12 +468,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m | Pfixz r1 r2 => OK (nextinstr (rs#r1 <- (Val.intoffloat rs#r2))) m - | Pfixzu r1 r2 => - OK (nextinstr (rs#r1 <- (Val.intuoffloat rs#r2))) m | Pfltd r1 r2 => OK (nextinstr (rs#r1 <- (Val.floatofint rs#r2))) m - | Pfltud r1 r2 => - OK (nextinstr (rs#r1 <- (Val.floatofintu rs#r2))) m | Pldfd r1 r2 n => exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pldfs r1 r2 n => @@ -492,8 +486,11 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m | Pstfd r1 r2 n => exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m - | Pstfs r1 r2 n => - exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m + | Pstfs r1 r2 n => + match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with + | OK rs' m' => OK (rs'#FR3 <- Vundef) m' + | Error => Error + end | Psufd r1 r2 r3 => OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m (* Pseudo-instructions *) diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 775bb37..b3412fb 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -300,12 +300,8 @@ Definition transl_op Pmvfs (freg_of r) (freg_of a1) :: k | Ointoffloat, a1 :: nil => Pfixz (ireg_of r) (freg_of a1) :: k - | Ointuoffloat, a1 :: nil => - Pfixzu (ireg_of r) (freg_of a1) :: k | Ofloatofint, a1 :: nil => Pfltd (freg_of r) (ireg_of a1) :: k - | Ofloatofintu, a1 :: nil => - Pfltud (freg_of r) (ireg_of a1) :: k | Ocmp cmp, _ => transl_cond cmp args (Pmov (ireg_of r) (SOimm Int.zero) :: diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index cc4d7ac..d3e082f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -558,56 +558,84 @@ Inductive match_stack: list Machconcr.stackframe -> Prop := wt_function f -> incl c f.(fn_code) -> transl_code_at_pc ra fb f c -> + sp <> Vundef -> + ra <> Vundef -> match_stack s -> match_stack (Stackframe fb sp ra c :: s). Inductive match_states: Machconcr.state -> Asm.state -> Prop := | match_states_intro: - forall s fb sp c ms m rs f + forall s fb sp c ms m rs f m' (STACKS: match_stack s) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (WTF: wt_function f) (INCL: incl c f.(fn_code)) (AT: transl_code_at_pc (rs PC) fb f c) - (AG: agree ms sp rs), + (AG: agree ms sp rs) + (MEXT: Mem.extends m m'), match_states (Machconcr.State s fb sp c ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_call: - forall s fb ms m rs + forall s fb ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs IR14 = parent_ra s), + (ATLR: rs IR14 = parent_ra s) + (MEXT: Mem.extends m m'), match_states (Machconcr.Callstate s fb ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_return: - forall s ms m rs + forall s ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), + (ATPC: rs PC = parent_ra s) + (MEXT: Mem.extends m m'), match_states (Machconcr.Returnstate s ms m) - (Asm.State rs m). + (Asm.State rs m'). Lemma exec_straight_steps: - forall s fb sp m1 f c1 rs1 c2 m2 ms2, + forall s fb sp m1 m1' f c1 rs1 c2 m2 ms2, match_stack s -> Genv.find_funct_ptr ge fb = Some (Internal f) -> wt_function f -> incl c2 f.(fn_code) -> transl_code_at_pc (rs1 PC) fb f c1 -> - (exists rs2, - exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2 + Mem.extends m1 m1' -> + (exists m2', + Mem.extends m2 m2' /\ + exists rs2, + exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2' /\ agree ms2 sp rs2) -> exists st', - plus step tge (State rs1 m1) E0 st' /\ + plus step tge (State rs1 m1') E0 st' /\ match_states (Machconcr.State s fb sp c2 ms2 m2) st'. Proof. - intros. destruct H4 as [rs2 [A B]]. - exists (State rs2 m2); split. + intros. destruct H5 as [m2' [A [rs2 [B C]]]]. + exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. Qed. +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. induction 1; simpl. congruence. auto. Qed. + +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +Qed. + (** We need to show that, in the simulation diagram, we cannot take infinitely many Mach transitions that correspond to zero transitions on the ARM side. Actually, all Mach transitions @@ -642,6 +670,7 @@ Lemma exec_Mlabel_prop: Proof. intros; red; intros; inv MS. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists (nextinstr rs); split. simpl. apply exec_straight_one. reflexivity. reflexivity. apply agree_nextinstr; auto. @@ -658,18 +687,15 @@ Proof. intros; red; intros; inv MS. unfold load_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - generalize (loadind_correct tge (transl_function f) IR13 ofs ty - dst (transl_code f c) rs m v H H1). + intro WTI. inv WTI. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit loadind_correct. eexact A. reflexivity. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. - simpl. exists rs2; split. auto. - apply agree_exten_2 with (rs#(preg_of dst) <- v). - auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + exists m'; split; auto. + simpl. exists rs2; split. eauto. + apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. Qed. Lemma exec_Msetstack_prop: @@ -683,16 +709,16 @@ Proof. intros; red; intros; inv MS. unfold store_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - rewrite (preg_val ms sp rs) in H; auto. - assert (NOTE: IR13 <> IR14) by congruence. - generalize (storeind_correct tge (transl_function f) IR13 ofs ty - src (transl_code f c) rs m m' H H1 NOTE). + intro WTI. inv WTI. + exploit preg_val; eauto. instantiate (1 := src). intros A. + exploit Mem.storev_extends; eauto. intros [m2 [B C]]. + rewrite (sp_val _ _ _ AG) in B. + exploit storeind_correct. eexact B. reflexivity. congruence. intros [rs2 [EX OTH]]. left; eapply exec_straight_steps; eauto with coqlib. - exists rs2; split; auto. - apply agree_exten_2 with rs; auto. + exists m2; split; auto. + exists rs2; split; eauto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mgetparam_prop: @@ -703,29 +729,33 @@ Lemma exec_Mgetparam_prop: load_stack m sp Tint f.(fn_link_ofs) = Some parent -> load_stack m parent ty ofs = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. auto. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. eauto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. eauto. + intros [v' [C D]]. exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14 - rs m parent (loadind IR14 ofs ty dst (transl_code f c))). - rewrite <- (sp_val ms sp rs); auto. + rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))). + auto. intros [rs1 [EX1 [RES1 OTH1]]]. - exploit (loadind_correct tge (transl_function f) IR14 ofs ty dst - (transl_code f c) rs1 m v). - rewrite RES1. auto. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. auto. + exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst + (transl_code f c) rs1 m' v'). + rewrite RES1. auto. auto. intros [rs2 [EX2 [RES2 OTH2]]]. left. eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists rs2; split; simpl. eapply exec_straight_trans; eauto. - apply agree_exten_2 with (rs1#(preg_of dst) <- v). - apply agree_set_mreg. - apply agree_exten_2 with rs; auto. - intros. case (preg_eq r (preg_of dst)); intro. - subst r. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + apply agree_set_mreg with rs1. + apply agree_set_mreg with rs. auto. auto. auto with ppcgen. + congruence. auto with ppcgen. Qed. Lemma exec_Mop_prop: @@ -734,14 +764,27 @@ Lemma exec_Mop_prop: (ms : mreg -> val) (m : mem) (v : val), eval_operation ge sp op ms ## args = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set res v ms) m). + (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. + intros [v' [A B]]. + assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v'). + rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. + rewrite (sp_val _ _ _ AG) in C. + exploit transl_op_correct; eauto. intros [rs' [P [Q R]]]. left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_op_correct; auto. - rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exists m'; split; auto. + exists rs'; split. simpl. eexact P. + assert (agree (Regmap.set res v ms) sp rs'). + apply agree_set_mreg with rs; auto. congruence. + auto with ppcgen. + assert (agree (Regmap.set res v (undef_temps ms)) sp rs'). + apply agree_set_undef_mreg with rs; auto. congruence. + auto with ppcgen. + destruct op; assumption. Qed. Lemma exec_Mload_prop: @@ -752,7 +795,7 @@ Lemma exec_Mload_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.loadv chunk m a = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + E0 (Machconcr.State s fb sp c (Regmap.set dst v (undef_temps ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -760,12 +803,14 @@ Proof. assert (eval_addressing tge sp addr ms##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. destruct chunk; simpl; simpl in H6; (eapply transl_load_int_correct || eapply transl_load_float_correct); eauto; intros; reflexivity. Qed. -Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. +Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. + Lemma exec_Mstore_prop: forall (s : list stackframe) (fb : block) (sp : val) (chunk : memory_chunk) (addr : addressing) (args : list mreg) @@ -774,7 +819,7 @@ Lemma exec_Mstore_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.storev chunk m a (ms src) = Some m' -> exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machconcr.State s fb sp c ms m'). + (Machconcr.State s fb sp c (undef_temps ms) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -788,6 +833,7 @@ Proof. simpl; (eapply transl_store_int_correct || eapply transl_store_float_correct); eauto; intros; simpl; auto. + econstructor; split. rewrite H2. eauto. intros. apply Pregmap.gso; auto. Qed. Lemma exec_Mcall_prop: @@ -817,17 +863,20 @@ Proof. rewrite RA_EQ. change (rs2 IR14) with (Val.add (rs PC) Vone). rewrite <- H2. reflexivity. - assert (AG3: agree ms sp rs2). - unfold rs2; auto 8 with ppcgen. - left; exists (State rs2 m); split. + assert (AG3: agree ms sp rs2). + unfold rs2. apply agree_set_other; auto. apply agree_set_other; auto. + left; exists (State rs2 m'); split. apply plus_one. destruct ros; simpl in H5. econstructor. eauto. apply functions_transl. eexact H0. eapply find_instr_tail. eauto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - simpl in H. destruct (ms m0); try congruence. - generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H7. - auto. + simpl. + assert (rs (ireg_of m0) = Vptr f' Int.zero). + generalize (ireg_val _ _ _ m0 AG H3). intro LD. simpl in H. inv LD. + destruct (ms m0); try congruence. + generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. + rewrite <- H7 in H; congruence. + rewrite H6. auto. econstructor. eauto. apply functions_transl. eexact H0. eapply find_instr_tail. eauto. simpl. unfold symbol_offset. rewrite symbols_preserved. @@ -835,8 +884,19 @@ Proof. econstructor; eauto. econstructor; eauto with coqlib. rewrite RA_EQ. econstructor; eauto. + eapply agree_sp_def; eauto. congruence. Qed. +Lemma agree_change_sp: + forall ms sp rs sp', + agree ms sp rs -> sp' <> Vundef -> + agree ms sp' (rs#IR13 <- sp'). +Proof. + intros. inv H. split. apply Pregmap.gss. auto. + intros. rewrite Pregmap.gso; auto with ppcgen. +Qed. + + Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -848,23 +908,31 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)). unfold call_instr; destruct ros; auto. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H2. auto. + intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. + exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 - rs m (parent_ra s) + rs m'0 (parent_ra s) (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c)) as [rs1 [EXEC1 [RES1 OTH1]]]. rewrite <- (sp_val ms (Vptr stk soff) rs); auto. set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). assert (EXEC2: exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig ros :: c)) rs m - (call_instr :: transl_code f c) rs2 m'). + (transl_code f (Mtailcall sig ros :: c)) rs m'0 + (call_instr :: transl_code f c) rs2 m2'). rewrite TR. eapply exec_straight_trans. eexact EXEC1. apply exec_straight_one. simpl. rewrite OTH1; auto with ppcgen. rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - unfold load_stack in H1. simpl in H1. simpl. rewrite H1. - rewrite H3. auto. auto. + simpl chunk_of_type in A. rewrite A. + rewrite P. auto. auto. set (rs3 := rs2#PC <- (Vptr f' Int.zero)). - left. exists (State rs3 m'); split. + left. exists (State rs3 m2'); split. (* Execution *) eapply plus_right'. eapply exec_straight_exec; eauto. inv AT. exploit exec_straight_steps_2; eauto. @@ -877,24 +945,19 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff replace (rs2 (ireg_of m0)) with (Vptr f' Int.zero). auto. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen. - rewrite <- (ireg_val ms (Vptr stk soff) rs); auto. - destruct (ms m0); try discriminate. - generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H10. - auto. - decEq. auto with ppcgen. decEq. auto with ppcgen. decEq. auto with ppcgen. - replace (symbol_offset tge i Int.zero) with (Vptr f' Int.zero). auto. - unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. + generalize (ireg_val _ _ _ m0 AG H7). intro LD. inv LD. + destruct (ms m0); try congruence. + generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. + rewrite <- H10 in H; congruence. + auto with ppcgen. + unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq. (* Match states *) constructor; auto. - assert (AG1: agree ms (Vptr stk soff) rs1). - eapply agree_exten_2; eauto. - assert (AG2: agree ms (parent_sp s) rs2). - inv AG1. constructor. auto. intros. unfold rs2. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso. auto. auto with ppcgen. - unfold rs3. apply agree_exten_2 with rs2; auto. - intros. rewrite Pregmap.gso; auto. + unfold rs3. apply agree_set_other; auto. + unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). + apply agree_exten with rs; auto with ppcgen. + apply parent_sp_def. auto. Qed. Lemma exec_Mbuiltin_prop: @@ -904,28 +967,29 @@ Lemma exec_Mbuiltin_prop: (t : trace) (v : val) (m' : mem), external_call ef ge ms ## args m t v m' -> exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t - (Machconcr.State s f sp b (Regmap.set res v ms) m'). + (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. + exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + intros [vres' [m2' [A [B [C D]]]]]. inv AT. simpl in H3. generalize (functions_transl _ _ FIND); intro FN. generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - replace (rs##(preg_of##args)) with (ms##args). - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - rewrite list_map_compose. apply list_map_exten. intros. - symmetry. eapply preg_val; eauto. + eapply external_call_symbols_preserved; eauto. + eexact symbols_preserved. eexact varinfo_preserved. econstructor; eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite <- H0. simpl. constructor; auto. eapply code_tail_next_int; eauto. - apply sym_not_equal. auto with ppcgen. - auto with ppcgen. + apply sym_not_equal. auto with ppcgen. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + rewrite Pregmap.gss; auto. + intros. rewrite Pregmap.gso; auto. Qed. Lemma exec_Mgoto_prop: @@ -940,16 +1004,16 @@ Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. inv AT. simpl in H3. - generalize (find_label_goto_label f lbl rs m _ _ _ FIND (sym_equal H1) H0). + generalize (find_label_goto_label f lbl rs m' _ _ _ FIND (sym_equal H1) H0). intros [rs2 [GOTO [AT2 INV]]]. - left; exists (State rs2 m); split. + left; exists (State rs2 m'); split. apply plus_one. econstructor; eauto. apply functions_transl; eauto. eapply find_instr_tail; eauto. simpl; auto. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs; auto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mcond_true_prop: @@ -961,32 +1025,32 @@ Lemma exec_Mcond_true_prop: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c' ms m). + (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. - pose (k1 := Pbc (crbit_for_cond cond) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m true H3 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit transl_cond_correct. eauto. eauto. + intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. exploit exec_straight_steps_2; eauto. intros [ofs' [PC2 CT2]]. - generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H1). + generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H1). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2. eauto. + eapply find_instr_tail. eauto. simpl. rewrite RES. simpl. auto. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto. + apply agree_exten_temps with rs; auto. intros. + rewrite INV3; auto with ppcgen. Qed. Lemma exec_Mcond_false_prop: @@ -995,36 +1059,34 @@ Lemma exec_Mcond_false_prop: (c : list Mach.instruction) (ms : mreg -> val) (m : mem), eval_condition cond ms ## args = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c ms m). + (Machconcr.State s fb sp c (undef_temps ms) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - pose (k1 := Pbc (crbit_for_cond cond) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m false H1 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. + intro WTI. inv WTI. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit transl_cond_correct. eauto. eauto. + intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists (nextinstr rs2); split. simpl. eapply exec_straight_trans. eexact EX. - unfold k1; apply exec_straight_one. - simpl. rewrite RES. reflexivity. - reflexivity. - auto with ppcgen. + apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. + apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. Qed. Lemma exec_Mjumptable_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction) - (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) + (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) (c' : Mach.code), - rs arg = Vint n -> + ms arg = Vint n -> list_nth_z tbl (Int.signed n) = Some lbl -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop - (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0 - (Machconcr.State s fb sp c' rs m). + (Machconcr.State s fb sp (Mjumptable arg tbl :: c) ms m) E0 + (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -1039,19 +1101,21 @@ Proof. omega. inv AT. simpl in H7. set (k1 := Pbtbl IR14 tbl :: transl_code f c). - set (rs1 := nextinstr (rs0 # IR14 <- (Vint (Int.shl n (Int.repr 2))))). + set (rs1 := nextinstr (rs # IR14 <- (Vint (Int.shl n (Int.repr 2))))). generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. + assert (rs (ireg_of arg) = Vint n). + exploit ireg_val; eauto. intros LD. inv LD. auto. congruence. assert (exec_straight tge (transl_function f) - (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs0 m - k1 rs1 m). + (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs m' + k1 rs1 m'). apply exec_straight_one. - simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. + simpl. rewrite H8. reflexivity. reflexivity. exploit exec_straight_steps_2; eauto. intros [ofs' [PC1 CT1]]. - generalize (find_label_goto_label f lbl rs1 m _ _ _ FIND PC1 H2). + generalize (find_label_goto_label f lbl rs1 m' _ _ _ FIND PC1 H2). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. econstructor; eauto. @@ -1064,15 +1128,25 @@ Opaque Zmod. Opaque Zdiv. change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs1; auto. + apply agree_exten with rs1; auto with ppcgen. unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen. + apply agree_undef_temps; auto. Qed. Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 - rs m (parent_ra s) + rs m'0 (parent_ra s) (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)). rewrite <- (sp_val ms (Vptr stk soff) rs); auto. intros [rs1 [EXEC1 [RES1 OTH1]]]. @@ -1080,14 +1154,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : assert (EXEC2: exec_straight tge (transl_function f) (loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c)) - rs m (Pbreg IR14 :: transl_code f c) rs2 m'). + rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2'). eapply exec_straight_trans. eexact EXEC1. apply exec_straight_one. simpl. rewrite OTH1; try congruence. - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - unfold load_stack in H0. simpl in H0; simpl; rewrite H0. rewrite H2. reflexivity. - reflexivity. + rewrite <- (sp_val ms (Vptr stk soff) rs); auto. + simpl chunk_of_type in A. rewrite A. rewrite E. auto. auto. set (rs3 := rs2#PC <- (parent_ra s)). - left; exists (State rs3 m'); split. + left; exists (State rs3 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. inv AT. exploit exec_straight_steps_2; eauto. @@ -1100,15 +1173,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : traceEq. (* match states *) constructor. auto. - assert (AG1: agree ms (Vptr stk soff) rs1). - apply agree_exten_2 with rs; auto. - assert (AG2: agree ms (parent_sp s) rs2). - constructor. reflexivity. intros; unfold rs2. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso; auto with ppcgen. - inv AG1; auto. - unfold rs3. auto with ppcgen. - reflexivity. + apply agree_exten with rs2. + unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). + apply agree_exten with rs; auto with ppcgen. + apply parent_sp_def. auto. + intros. unfold rs3. apply Pregmap.gso; auto with ppcgen. + unfold rs3. apply Pregmap.gss. + auto. Qed. Hypothesis wt_prog: wt_program prog. @@ -1132,21 +1203,26 @@ Proof. generalize (functions_transl_no_overflow _ _ H); intro NOOV. set (rs2 := nextinstr (rs#IR13 <- sp)). set (rs3 := nextinstr rs2). + exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [A B]]. + unfold store_stack in *; simpl chunk_of_type in *. + exploit Mem.storev_extends. eexact B. eauto. auto. auto. + intros [m2' [C D]]. + exploit Mem.storev_extends. eexact D. eauto. auto. auto. + intros [m3' [E F]]. (* Execution of function prologue *) assert (EXEC_PROLOGUE: exec_straight tge (transl_function f) - (transl_function f) rs m - (transl_code f f.(fn_code)) rs3 m3). + (transl_function f) rs m' + (transl_code f f.(fn_code)) rs3 m3'). unfold transl_function at 2. - apply exec_straight_two with rs2 m2. - unfold exec_instr. rewrite H0. fold sp. - rewrite <- (sp_val ms (parent_sp s) rs); auto. - unfold store_stack in H1. change Mint32 with (chunk_of_type Tint). rewrite H1. - auto. + apply exec_straight_two with rs2 m2'. + unfold exec_instr. rewrite A. fold sp. + rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto. unfold exec_instr. unfold eval_shift_addr. unfold exec_store. change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR. - unfold store_stack in H2. change Mint32 with (chunk_of_type Tint). rewrite H2. - auto. auto. auto. + rewrite E. auto. + auto. auto. (* Agreement at end of prologue *) assert (AT3: transl_code_at_pc rs3#PC fb f f.(fn_code)). change (rs3 PC) with (Val.add (Val.add (rs PC) Vone) Vone). @@ -1155,14 +1231,12 @@ Proof. eapply code_tail_next_int; auto. change (Int.unsigned Int.zero) with 0. unfold transl_function. constructor. - assert (AG2: agree ms sp rs2). - split. reflexivity. - intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). elim AG; auto. - auto with ppcgen. auto with ppcgen. assert (AG3: agree ms sp rs3). - unfold rs3; auto with ppcgen. - left; exists (State rs3 m3); split. + unfold rs3. apply agree_nextinstr. + unfold rs2. apply agree_nextinstr. + apply agree_change_sp with (parent_sp s); auto. + unfold sp. congruence. + left; exists (State rs3 m3'); split. (* execution *) eapply exec_straight_steps_1; eauto. change (Int.unsigned Int.zero) with 0. constructor. @@ -1183,15 +1257,21 @@ Lemma exec_function_external_prop: Proof. intros; red; intros; inv MS. exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14)) - m'); split. + intros [tf [A B]]. simpl in B. inv B. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [P [Q [R S]]]]]. + left; exists (State (rs#(loc_external_result (ef_sig ef)) <- vres' #PC <- (rs IR14)) + m2'); split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - eapply extcall_arguments_match; eauto. econstructor; eauto. - unfold loc_external_result. auto with ppcgen. + unfold loc_external_result. + eapply agree_set_mreg; eauto. + rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. Qed. Lemma exec_return_prop: @@ -1241,6 +1321,8 @@ Proof. with (Vptr fb Int.zero). econstructor; eauto. constructor. split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. + intros. unfold Regmap.init. auto. + apply Mem.extends_refl. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. @@ -1251,8 +1333,8 @@ Lemma transf_final_states: match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r. Proof. intros. inv H0. inv H. constructor. auto. - compute in H1. - rewrite (ireg_val _ _ _ R0 AG) in H1. auto. auto. + compute in H1. exploit ireg_val; eauto. instantiate (1 := R0); auto. + simpl. intros LD. inv LD; congruence. Qed. Theorem transf_program_correct: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index fc2ce7f..c10c9df 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -27,7 +27,7 @@ Require Import Machconcr. Require Import Machtyping. Require Import Asm. Require Import Asmgen. -Require Conventions. +Require Import Conventions. (** * Correspondence between Mach registers and PPC registers *) @@ -41,91 +41,86 @@ Proof. destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. Qed. -(** Characterization of PPC registers that correspond to Mach registers. *) - -Definition is_data_reg (r: preg) : Prop := - match r with - | IR IR14 => False - | CR _ => False - | PC => False - | _ => True - end. - -Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). -Proof. - destruct r; exact I. -Qed. - -Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). -Proof. - destruct r; exact I. -Qed. - -Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r). -Proof. - destruct r; exact I. -Qed. - Lemma ireg_of_not_IR13: forall r, ireg_of r <> IR13. Proof. - intro. case r; discriminate. + destruct r; simpl; congruence. Qed. + Lemma ireg_of_not_IR14: forall r, ireg_of r <> IR14. Proof. - intro. case r; discriminate. + destruct r; simpl; congruence. Qed. -Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14: ppcgen. +Lemma preg_of_not_IR13: + forall r, preg_of r <> IR13. +Proof. + unfold preg_of; intros. destruct (mreg_type r). + generalize (ireg_of_not_IR13 r); congruence. + congruence. +Qed. -Lemma preg_of_not: - forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. +Lemma preg_of_not_IR14: + forall r, preg_of r <> IR14. Proof. - intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg. + unfold preg_of; intros. destruct (mreg_type r). + generalize (ireg_of_not_IR14 r); congruence. + congruence. Qed. -Hint Resolve preg_of_not: ppcgen. -Lemma preg_of_not_IR13: - forall r, preg_of r <> IR13. +Lemma preg_of_not_PC: + forall r, preg_of r <> PC. Proof. - intro. case r; discriminate. + intros. unfold preg_of. destruct (mreg_type r); congruence. Qed. -Hint Resolve preg_of_not_IR13: ppcgen. -(** Agreement between Mach register sets and PPC register sets. *) +Lemma ireg_diff: + forall r1 r2, r1 <> r2 -> IR r1 <> IR r2. +Proof. intros; congruence. Qed. + +Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14 + preg_of_not_IR13 preg_of_not_IR14 + preg_of_not_PC ireg_diff: ppcgen. + +(** Agreement between Mach register sets and ARM register sets. *) -Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) := - rs#IR13 = sp /\ forall r: mreg, ms r = rs#(preg_of r). +Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { + agree_sp: rs#IR13 = sp; + agree_sp_def: sp <> Vundef; + agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) +}. Lemma preg_val: forall ms sp rs r, - agree ms sp rs -> ms r = rs#(preg_of r). + agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). +Proof. + intros. destruct H. auto. +Qed. + +Lemma preg_vals: + forall ms sp rs, agree ms sp rs -> + forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). Proof. - intros. elim H. auto. + induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. Qed. - + Lemma ireg_val: forall ms sp rs r, agree ms sp rs -> mreg_type r = Tint -> - ms r = rs#(ireg_of r). + Val.lessdef (ms r) rs#(ireg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto. Qed. Lemma freg_val: forall ms sp rs r, agree ms sp rs -> mreg_type r = Tfloat -> - ms r = rs#(freg_of r). + Val.lessdef (ms r) rs#(freg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto. Qed. Lemma sp_val: @@ -133,76 +128,71 @@ Lemma sp_val: agree ms sp rs -> sp = rs#IR13. Proof. - intros. elim H; auto. + intros. destruct H; auto. Qed. -Lemma agree_exten_1: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r -> rs'#r = rs#r) -> - agree ms sp rs'. +Hint Resolve preg_val ireg_val freg_val sp_val: ppcgen. + +Definition important_preg (r: preg) : bool := + match r with + | IR IR14 => false + | IR _ => true + | FR _ => true + | CR _ => false + | PC => false + end. + +Lemma preg_of_important: + forall r, important_preg (preg_of r) = true. Proof. - unfold agree; intros. elim H; intros. - split. rewrite H0. auto. exact I. - intros. rewrite H0. auto. apply preg_of_is_data_reg. + intros. destruct r; reflexivity. Qed. -Lemma agree_exten_2: +Lemma important_diff: + forall r r', + important_preg r = true -> important_preg r' = false -> r <> r'. +Proof. + congruence. +Qed. +Hint Resolve important_diff: ppcgen. + +Lemma agree_exten: forall ms sp rs rs', agree ms sp rs -> - (forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r) -> + (forall r, important_preg r = true -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - intros. eapply agree_exten_1; eauto. - intros. apply H0; red; intro; subst r; elim H1. + intros. destruct H. split. + rewrite H0; auto. auto. + intros. rewrite H0; auto. apply preg_of_important. Qed. (** Preservation of register agreement under various assignments. *) Lemma agree_set_mreg: - forall ms sp rs r v, + forall ms sp rs r v rs', agree ms sp rs -> - agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v). -Proof. - unfold agree; intros. elim H; intros; clear H. - split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_IR13. - intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso. auto. red; intro. - elim n. apply preg_of_injective; auto. -Qed. -Hint Resolve agree_set_mreg: ppcgen. - -Lemma agree_set_mireg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> - mreg_type r = Tint -> - agree ms sp (rs#(ireg_of r) <- v). -Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. -Qed. -Hint Resolve agree_set_mireg: ppcgen. - -Lemma agree_set_mfreg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> - mreg_type r = Tfloat -> - agree ms sp (rs#(freg_of r) <- v). + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. + intros. destruct H. split. + rewrite H1; auto. apply sym_not_equal. apply preg_of_not_IR13. + auto. + intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. + rewrite H1. auto. apply preg_of_important. + red; intros; elim n. eapply preg_of_injective; eauto. Qed. -Hint Resolve agree_set_mfreg: ppcgen. Lemma agree_set_other: forall ms sp rs r v, agree ms sp rs -> - ~(is_data_reg r) -> + important_preg r = false -> agree ms sp (rs#r <- v). Proof. - intros. apply agree_exten_1 with rs. - auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction. + intros. apply agree_exten with rs. auto. + intros. apply Pregmap.gso. congruence. Qed. -Hint Resolve agree_set_other: ppcgen. Lemma agree_nextinstr: forall ms sp rs, @@ -210,139 +200,159 @@ Lemma agree_nextinstr: Proof. intros. unfold nextinstr. apply agree_set_other. auto. auto. Qed. -Hint Resolve agree_nextinstr: ppcgen. -Lemma agree_set_mireg_twice: - forall ms sp rs r v v', - agree ms sp rs -> - mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v). +Definition nontemp_preg (r: preg) : bool := + match r with + | IR IR14 => false + | IR IR10 => false + | IR IR12 => false + | IR _ => true + | FR FR2 => false + | FR FR3 => false + | FR _ => true + | CR _ => false + | PC => false + end. + +Lemma nontemp_diff: + forall r r', + nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'. Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). - intros. case (mreg_eq r r0); intro. - subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. - assert (preg_of r <> preg_of r0). - red; intro. elim n. apply preg_of_injective. auto. - rewrite Regmap.gso; auto. - repeat (rewrite Pregmap.gso; auto). - unfold preg_of. rewrite H0. auto. + congruence. Qed. -Hint Resolve agree_set_mireg_twice: ppcgen. -Lemma agree_set_twice_mireg: - forall ms sp rs r v v', - agree (Regmap.set r v' ms) sp rs -> - mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v). +Hint Resolve nontemp_diff: ppcgen. + +Lemma nontemp_important: + forall r, nontemp_preg r = true -> important_preg r = true. Proof. - intros. elim H; intros. - split. rewrite Pregmap.gso. auto. - generalize (ireg_of_not_IR13 r); congruence. - intros. generalize (H2 r0). - case (mreg_eq r0 r); intro. - subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0. - rewrite Pregmap.gss. auto. - repeat rewrite Regmap.gso; auto. - rewrite Pregmap.gso. auto. - replace (IR (ireg_of r)) with (preg_of r). - red; intros. elim n. apply preg_of_injective; auto. - unfold preg_of. rewrite H0. auto. + unfold nontemp_preg, important_preg; destruct r; auto. destruct i; auto. Qed. -Hint Resolve agree_set_twice_mireg: ppcgen. -Lemma agree_set_commut: - forall ms sp rs r1 r2 v1 v2, - r1 <> r2 -> - agree ms sp ((rs#r2 <- v2)#r1 <- v1) -> - agree ms sp ((rs#r1 <- v1)#r2 <- v2). +Hint Resolve nontemp_important: ppcgen. + +Remark undef_regs_1: + forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef. Proof. - intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto. - intros. - case (preg_eq r r1); intro. - subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - case (preg_eq r r2); intro. - subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - repeat (rewrite Pregmap.gso; auto). -Qed. -Hint Resolve agree_set_commut: ppcgen. - -Lemma agree_nextinstr_commut: - forall ms sp rs r v, - agree ms sp (rs#r <- v) -> - r <> PC -> - agree ms sp ((nextinstr rs)#r <- v). + induction l; simpl; intros. auto. apply IHl. unfold Regmap.set. + destruct (RegEq.eq r a); congruence. +Qed. + +Remark undef_regs_2: + forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef. +Proof. + induction l; simpl; intros. contradiction. + destruct H. subst. apply undef_regs_1. apply Regmap.gss. + auto. +Qed. + +Remark undef_regs_3: + forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r. Proof. - intros. unfold nextinstr. apply agree_set_commut. auto. - apply agree_set_other. auto. auto. + induction l; simpl; intros. auto. + rewrite IHl. apply Regmap.gso. intuition. intuition. Qed. -Hint Resolve agree_nextinstr_commut: ppcgen. -Lemma agree_set_mireg_exten: - forall ms sp rs r v (rs': regset), +Lemma agree_exten_temps: + forall ms sp rs rs', agree ms sp rs -> - mreg_type r = Tint -> - rs'#(ireg_of r) = v -> - (forall r', r' <> PC -> r' <> ireg_of r -> r' <> IR14 -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. + (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> + agree (undef_temps ms) sp rs'. Proof. - intros. apply agree_exten_2 with (rs#(ireg_of r) <- v). - auto with ppcgen. - intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro. - subst r0. auto. apply H2; auto. + intros. destruct H. split. + rewrite H0; auto. auto. + intros. unfold undef_temps. + destruct (In_dec mreg_eq r (int_temporaries ++ float_temporaries)). + rewrite undef_regs_2; auto. + rewrite undef_regs_3; auto. rewrite H0; auto. + simpl in n. destruct r; auto; intuition. Qed. -(** Useful properties of the PC and GPR0 registers. *) +Lemma agree_set_undef_mreg: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', nontemp_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v (undef_temps ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. + eapply agree_exten_temps; eauto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + congruence. auto. + intros. rewrite Pregmap.gso; auto. +Qed. + +Lemma agree_undef_temps: + forall ms sp rs, + agree ms sp rs -> + agree (undef_temps ms) sp rs. +Proof. + intros. eapply agree_exten_temps; eauto. +Qed. + +(** Useful properties of the PC register. *) Lemma nextinstr_inv: - forall r rs, r <> PC -> (nextinstr rs)#r = rs#r. + forall r rs, + r <> PC -> + (nextinstr rs)#r = rs#r. +Proof. + intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto. +Qed. + +Lemma nextinstr_inv2: + forall r rs, + nontemp_preg r = true -> + (nextinstr rs)#r = rs#r. Proof. - intros. unfold nextinstr. apply Pregmap.gso. auto. + intros. apply nextinstr_inv. red; intro; subst; discriminate. Qed. -Hint Resolve nextinstr_inv: ppcgen. Lemma nextinstr_set_preg: forall rs m v, (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. Proof. intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen. + rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. Qed. -Hint Resolve nextinstr_set_preg: ppcgen. (** Connection between Mach and Asm calling conventions for external functions. *) Lemma extcall_arg_match: - forall ms sp rs m l v, + forall ms sp rs m m' l v, agree ms sp rs -> Machconcr.extcall_arg ms m sp l v -> - Asm.extcall_arg rs m l v. + Mem.extends m m' -> + exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. Proof. - intros. inv H0. - rewrite (preg_val _ _ _ r H). constructor. - rewrite (sp_val _ _ _ H) in H1. - destruct ty; unfold load_stack in H1. - econstructor. reflexivity. assumption. - econstructor. reflexivity. assumption. + intros. inv H0. + exists (rs#(preg_of r)); split. constructor. eauto with ppcgen. + unfold load_stack in H2. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ H) in A. + exists v'; split; auto. destruct ty; econstructor; eauto. Qed. Lemma extcall_args_match: - forall ms sp rs m, agree ms sp rs -> + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall ll vl, Machconcr.extcall_args ms m sp ll vl -> - Asm.extcall_args rs m ll vl. + exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'. Proof. - induction 2; constructor; auto. eapply extcall_arg_match; eauto. + induction 3. + exists (@nil val); split; constructor. + exploit extcall_arg_match; eauto. intros [v1' [A B]]. + exploit IHextcall_args; eauto. intros [vl' [C D]]. + exists(v1' :: vl'); split. constructor; auto. constructor; auto. Qed. Lemma extcall_arguments_match: - forall ms m sp rs sg args, + forall ms m sp rs sg args m', agree ms sp rs -> Machconcr.extcall_arguments ms m sp sg args -> - Asm.extcall_arguments rs m sg args. + Mem.extends m m' -> + exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. Proof. unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros. eapply extcall_args_match; eauto. @@ -564,7 +574,7 @@ Proof. exploit loadimm_correct. intros [rs' [A [B C]]]. exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))). split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. rewrite B. rewrite C; auto with ppcgen. congruence. + simpl. rewrite B. rewrite C; auto with ppcgen. auto. split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. @@ -756,20 +766,6 @@ Qed. (** Translation of conditions *) -Ltac TypeInv := - match goal with - | H: (List.map ?f ?x = nil) |- _ => - destruct x; [clear H | simpl in H; discriminate] - | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => - destruct x; simpl in H; - [ discriminate | - injection H; clear H; let T := fresh "T" in ( - intros H T; TypeInv) ] - | _ => idtac - end. - -(** Translation of conditions. *) - Lemma compare_int_spec: forall rs v1 v2, let rs1 := nextinstr (compare_int rs v1 v2) in @@ -783,11 +779,11 @@ Lemma compare_int_spec: /\ rs1#CRlt = (Val.cmp Clt v1 v2) /\ rs1#CRgt = (Val.cmp Cgt v1 v2) /\ rs1#CRle = (Val.cmp Cle v1 v2) - /\ forall r', is_data_reg r' -> rs1#r' = rs#r'. + /\ forall r', important_preg r' = true -> rs1#r' = rs#r'. Proof. intros. unfold rs1. intuition; try reflexivity. - rewrite nextinstr_inv; [unfold compare_int; repeat rewrite Pregmap.gso; auto | idtac]; - red; intro; subst r'; elim H. + rewrite nextinstr_inv; auto with ppcgen. + unfold compare_int. repeat rewrite Pregmap.gso; auto with ppcgen. Qed. Lemma compare_float_spec: @@ -803,302 +799,237 @@ Lemma compare_float_spec: /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) - /\ forall r', is_data_reg r' -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> rs'#r' = rs#r'. Proof. intros. unfold rs'. intuition; try reflexivity. - rewrite nextinstr_inv; [unfold compare_float; repeat rewrite Pregmap.gso; auto | idtac]; - red; intro; subst r'; elim H. + rewrite nextinstr_inv; auto with ppcgen. + unfold compare_float. repeat rewrite Pregmap.gso; auto with ppcgen. Qed. +Ltac TypeInv1 := + match goal with + | H: (List.map ?f ?x = nil) |- _ => + destruct x; inv H; TypeInv1 + | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => + destruct x; simpl in H; simplify_eq H; clear H; intros; TypeInv1 + | _ => idtac + end. + +Ltac TypeInv2 := + match goal with + | H: (mreg_type _ = Tint) |- _ => try (rewrite H in *); clear H; TypeInv2 + | H: (mreg_type _ = Tfloat) |- _ => try (rewrite H in *); clear H; TypeInv2 + | _ => idtac + end. + +Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2. + Lemma transl_cond_correct: - forall cond args k ms sp rs m b, + forall cond args k rs m b, map mreg_type args = type_of_condition cond -> - agree ms sp rs -> - eval_condition cond (map ms args) = Some b -> + eval_condition cond (map rs (map preg_of args)) = Some b -> exists rs', exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b - /\ agree ms sp rs'. + /\ forall r, important_preg r = true -> rs'#r = rs r. Proof. - intros. - rewrite <- (eval_condition_weaken _ _ H1). clear H1. - destruct cond; simpl in H; TypeInv; simpl. + intros until b; intros TY EV. rewrite <- (eval_condition_weaken _ _ EV). clear EV. + destruct cond; simpl in TY; TypeInv. (* Ccomp *) - generalize (compare_int_spec rs ms#m0 ms#m1). + generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat rewrite <- (ireg_val ms sp rs); trivial. - reflexivity. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; assumption. + auto. (* Ccompu *) - generalize (compare_int_spec rs ms#m0 ms#m1). + generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat rewrite <- (ireg_val ms sp rs); trivial. - reflexivity. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; assumption. + auto. (* Ccompshift *) - generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)). + generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))). - split. apply exec_straight_one. simpl. - rewrite transl_shift_correct. - repeat rewrite <- (ireg_val ms sp rs); trivial. - reflexivity. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. rewrite transl_shift_correct. case c; assumption. + rewrite transl_shift_correct. auto. (* Ccompushift *) - generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)). + generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))). - split. apply exec_straight_one. simpl. - rewrite transl_shift_correct. - repeat rewrite <- (ireg_val ms sp rs); trivial. - reflexivity. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. rewrite transl_shift_correct. case c; assumption. + rewrite transl_shift_correct. auto. (* Ccompimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs ms#m0 (Vint i)). + generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i)). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - rewrite <- (ireg_val ms sp rs); trivial. auto. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; assumption. + auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. - generalize (compare_int_spec rs' ms#m0 (Vint i)). + generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i)). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs' ms#m0 (Vint i))). + econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto. - split. - case c; simpl; auto. - apply agree_exten_1 with rs'; auto. + rewrite Q. rewrite R; eauto with ppcgen. auto. + split. case c; assumption. + intros. rewrite K; auto with ppcgen. (* Ccompuimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs ms#m0 (Vint i)). + generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i)). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - rewrite <- (ireg_val ms sp rs); trivial. auto. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; assumption. + auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. - generalize (compare_int_spec rs' ms#m0 (Vint i)). + generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i)). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_int rs' ms#m0 (Vint i))). + econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto. - split. - case c; simpl; auto. - apply agree_exten_1 with rs'; auto. + rewrite Q. rewrite R; eauto with ppcgen. auto. + split. case c; assumption. + intros. rewrite K; auto with ppcgen. (* Ccompf *) - generalize (compare_float_spec rs ms#m0 ms#m1). + generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_float rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat rewrite <- (freg_val ms sp rs); trivial. auto. - split. - case c; simpl; auto. - apply agree_exten_1 with rs; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; assumption. + auto. (* Cnotcompf *) - generalize (compare_float_spec rs ms#m0 ms#m1). + generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. - exists (nextinstr (compare_float rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat rewrite <- (freg_val ms sp rs); trivial. auto. - split. - case c; simpl; auto. + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. case c; try assumption. rewrite Val.negate_cmpf_ne. auto. rewrite Val.negate_cmpf_eq. auto. - apply agree_exten_1 with rs; auto. + auto. Qed. (** Translation of arithmetic operations. *) -Ltac TranslOpSimpl := +Ltac Simpl := match goal with - | |- exists rs' : regset, - exec_straight ?c ?rs ?m ?k rs' ?m /\ - agree (Regmap.set ?res ?v ?ms) ?sp rs' => - (exists (nextinstr (rs#(ireg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (ireg_val ms sp rs); auto); - simpl; try rewrite transl_shift_correct; reflexivity - | reflexivity ] - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) + | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen] + | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] end. +Ltac TranslOpSimpl := + econstructor; split; + [ apply exec_straight_one; [simpl; eauto | reflexivity ] + | split; [try rewrite transl_shift_correct; repeat Simpl | intros; repeat Simpl] ]. + Lemma transl_op_correct: - forall op args res k ms sp rs m v, + forall op args res k (rs: regset) m v, wt_instr (Mop op args res) -> - agree ms sp rs -> - eval_operation ge sp op (map ms args) = Some v -> + eval_operation ge rs#IR13 op (map rs (map preg_of args)) = Some v -> exists rs', exec_straight (transl_op op args res k) rs m k rs' m - /\ agree (Regmap.set res v ms) sp rs'. + /\ rs'#(preg_of res) = v + /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros. rewrite <- (eval_operation_weaken _ _ _ _ H1). (*clear H1; clear v.*) - inversion H. + intros. rewrite <- (eval_operation_weaken _ _ _ _ H0). inv H. (* Omove *) - simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))). - split. caseEq (mreg_type r1); intro. - apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity. - auto with ppcgen. - apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity. - auto with ppcgen. - auto with ppcgen. + simpl. + exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). + split. unfold preg_of; rewrite <- H2. + destruct (mreg_type r1); apply exec_straight_one; auto. + split. Simpl. Simpl. + intros. Simpl. Simpl. (* Other instructions *) - clear H2 H3 H5. - destruct op; simpl in H6; injection H6; clear H6; intros; - TypeInv; simpl; try (TranslOpSimpl). + destruct op; simpl in H5; inv H5; TypeInv; try (TranslOpSimpl; fail). (* Omove again *) congruence. (* Ointconst *) - generalize (loadimm_correct (ireg_of res) i k rs m). - intros [rs' [A [B C]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. + generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. + exists rs'. split. auto. split. auto. intros. auto with ppcgen. (* Oaddrstack *) generalize (addimm_correct (ireg_of res) IR13 i k rs m). intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (sp_val ms sp rs). auto. auto. + exists rs'. split. auto. split. auto. auto with ppcgen. (* Ocast8signed *) - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 24))))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))))). - exists rs2. split. - apply exec_straight_two with rs1 m; auto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - unfold rs2. - replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))) with (Val.sign_ext 8 (ms m0)). - apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. - apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. - vm_compute; auto. + econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + compute; auto. + intros. repeat Simpl. (* Ocast8unsigned *) - exists (nextinstr (rs#(ireg_of res) <- (Val.and (ms m0) (Vint (Int.repr 255))))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. - replace (Val.zero_ext 8 (ms m0)) - with (Val.and (ms m0) (Vint (Int.repr 255))). - auto with ppcgen. - destruct (ms m0); simpl; auto. rewrite Int.zero_ext_and. reflexivity. - vm_compute; auto. + econstructor; split. + eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. Simpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. reflexivity. + compute; auto. + intros. repeat Simpl. (* Ocast16signed *) - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))))). - exists rs2. split. - apply exec_straight_two with rs1 m; auto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - unfold rs2. - replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.sign_ext 16 (ms m0)). - apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. - apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. - vm_compute; auto. + econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + compute; auto. + intros. repeat Simpl. (* Ocast16unsigned *) - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))))). - exists rs2. split. - apply exec_straight_two with rs1 m; auto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - unfold rs2. - replace (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.zero_ext 16 (ms m0)). - apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. - apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (ms m0); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity. - vm_compute; auto. + econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity. + compute; auto. + intros. repeat Simpl. (* Oaddimm *) generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. + exists rs'. split. auto. split. auto. auto with ppcgen. (* Orsbimm *) exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0)); auto with ppcgen. intros [rs' [A [B C]]]. exists rs'. - split. eauto. - apply agree_set_mireg_exten with rs; auto. rewrite B. - rewrite <- (ireg_val ms sp rs); auto. + split. eauto. split. rewrite B. auto. auto with ppcgen. (* Omul *) destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)). - set (rs1 := nextinstr (rs#IR14 <- (Val.mul (ms m0) (ms m1)))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#IR14))). - exists rs2; split. - apply exec_straight_two with rs1 m; auto. - simpl. repeat rewrite <- (ireg_val ms sp rs); auto. - unfold rs2. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - apply agree_nextinstr. apply agree_nextinstr_commut. - apply agree_set_mireg; auto. apply agree_set_mreg. apply agree_set_other. auto. - simpl; auto. auto with ppcgen. discriminate. + econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. repeat Simpl. + intros. repeat Simpl. TranslOpSimpl. (* Oandimm *) generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m (ireg_of_not_IR14 m0)). intros [rs' [A [B C]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. + exists rs'. split. auto. split. auto. auto with ppcgen. (* Oorimm *) exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0)); auto with ppcgen. - intros [rs' [A [B C]]]. - exists rs'. - split. eauto. - apply agree_set_mireg_exten with rs; auto. rewrite B. - rewrite <- (ireg_val ms sp rs); auto. + intros [rs' [A [B C]]]. + exists rs'. split. eauto. split. auto. auto with ppcgen. (* Oxorimm *) exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0)); auto with ppcgen. - intros [rs' [A [B C]]]. - exists rs'. - split. eauto. - apply agree_set_mireg_exten with rs; auto. rewrite B. - rewrite <- (ireg_val ms sp rs); auto. + intros [rs' [A [B C]]]. + exists rs'. split. eauto. split. auto. auto with ppcgen. (* Oshrximm *) - assert (exists n, ms m0 = Vint n /\ Int.ltu i (Int.repr 31) = true). - simpl in H1. destruct (ms m0); try discriminate. + assert (exists n, rs (ireg_of m0) = Vint n /\ Int.ltu i (Int.repr 31) = true). + destruct (rs (ireg_of m0)); try discriminate. exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto. - destruct H3 as [n [ARG1 LTU]]. + destruct H as [n [ARG1 LTU]]. clear H0. assert (LTU': Int.ltu i Int.iwordsize = true). exploit Int.ltu_inv. eexact LTU. intro. unfold Int.ltu. apply zlt_true. - assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto. + assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). compute; auto. omega. - assert (RSm0: rs (ireg_of m0) = Vint n). - rewrite <- ARG1. symmetry. eapply ireg_val; eauto. set (islt := Int.lt n Int.zero). set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero))). - assert (OTH1: forall r', is_data_reg r' -> rs1#r' = rs#r'). + assert (OTH1: forall r', important_preg r' = true -> rs1#r' = rs#r'). generalize (compare_int_spec rs (Vint n) (Vint Int.zero)). fold rs1. intros [A B]. intuition. exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)). @@ -1107,83 +1038,47 @@ Proof. set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))). exists rs4; split. apply exec_straight_step with rs1 m. - simpl. rewrite RSm0. auto. auto. + simpl. rewrite ARG1. auto. auto. eapply exec_straight_trans. eexact EXEC2. apply exec_straight_two with rs3 m. simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). unfold Val.cmp. change (Int.cmp Cge n Int.zero) with (negb islt). - rewrite OTH2. rewrite OTH1. rewrite RSm0. + rewrite OTH2. rewrite OTH1. rewrite ARG1. unfold rs3. case islt; reflexivity. - apply ireg_of_is_data_reg. decEq; auto with ppcgen. auto with ppcgen. congruence. congruence. + destruct m0; reflexivity. auto with ppcgen. auto with ppcgen. discriminate. discriminate. simpl. auto. auto. unfold rs3. case islt; auto. auto. - (* agreement *) - assert (RES4: rs4#(ireg_of res) = Vint(Int.shrx n i)). - unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gss. - rewrite Int.shrx_shr. fold islt. unfold rs3. - repeat rewrite nextinstr_inv; auto. - case islt. rewrite RES2. rewrite OTH1. rewrite RSm0. - simpl. rewrite LTU'. auto. - apply ireg_of_is_data_reg. - rewrite Pregmap.gss. simpl. rewrite LTU'. auto. congruence. - exact LTU. auto with ppcgen. - assert (OTH4: forall r, is_data_reg r -> r <> ireg_of res -> rs4#r = rs#r). - intros. - assert (r <> PC). red; intro; subst r; elim H3. - assert (r <> IR14). red; intro; subst r; elim H3. - unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs3. rewrite nextinstr_inv; auto. - transitivity (rs2 r). - case islt. auto. apply Pregmap.gso; auto. - rewrite OTH2; auto. - apply agree_exten_1 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))). - auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r (ireg_of res)). - subst r. rewrite ARG1. simpl. rewrite LTU'. auto. - auto. - (* Ointoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)))). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ointuoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)))). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ofloatofint *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)))). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. - (* Ofloatofintu *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)))). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. + split. unfold rs4. repeat Simpl. rewrite ARG1. simpl. rewrite LTU'. rewrite Int.shrx_shr. + fold islt. unfold rs3. rewrite nextinstr_inv; auto with ppcgen. + destruct islt. rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). + rewrite ARG1. simpl. rewrite LTU'. auto. + rewrite Pregmap.gss. simpl. rewrite LTU'. auto. + assumption. + intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. + transitivity (rs2 r). destruct islt; auto. Simpl. + rewrite OTH2; auto with ppcgen. (* Ocmp *) - assert (exists b, eval_condition c ms##args = Some b /\ v = Val.of_bool b). - simpl in H1. destruct (eval_condition c ms##args). - destruct b; inv H1. exists true; auto. exists false; auto. - discriminate. - destruct H5 as [b [EVC EQ]]. - exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. - rewrite (eval_condition_weaken _ _ EVC). - set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))). - set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)). - exists rs2; split. - eapply exec_straight_trans. eauto. - apply exec_straight_two with rs1 m; auto. - simpl. replace (rs1 (crbit_for_cond c)) with (Val.of_bool b). - unfold rs2. destruct b; auto. - unfold rs2. destruct b; auto. - apply agree_set_mireg_exten with rs'; auto. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. - destruct b. apply Pregmap.gss. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. unfold rs2. rewrite nextinstr_inv; auto. - transitivity (rs1 r'). destruct b; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + fold preg_of in *. + assert (exists b, eval_condition c rs ## (preg_of ## args) = Some b /\ v = Val.of_bool b). + fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args)). + exists b; split; auto. destruct b; inv H0; auto. congruence. + clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ EVC). + destruct (transl_cond_correct c args + (Pmov (ireg_of res) (SOimm Int.zero) + :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k) + rs m b H1 EVC) + as [rs1 [A [B C]]]. + set (rs2 := nextinstr (rs1#(ireg_of res) <- (Vint Int.zero))). + set (rs3 := nextinstr (if b then (rs2#(ireg_of res) <- Vtrue) else rs2)). + exists rs3. + split. eapply exec_straight_trans. eauto. + apply exec_straight_two with rs2 m; auto. + simpl. replace (rs2 (crbit_for_cond c)) with (Val.of_bool b). + unfold rs3. destruct b; auto. + unfold rs3. destruct b; auto. + split. unfold rs3. Simpl. destruct b. Simpl. unfold rs2. repeat Simpl. + intros. unfold rs3. Simpl. transitivity (rs2 r). + destruct b; auto; Simpl. unfold rs2. repeat Simpl. Qed. Remark val_add_add_zero: @@ -1191,15 +1086,15 @@ Remark val_add_add_zero: Proof. intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto. Qed. - + Lemma transl_load_store_correct: forall (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) addr args k ms sp rs m ms' m', (forall (r1: ireg) (rs1: regset) n k, - eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (Vint n) -> - agree ms sp rs1 -> + eval_addressing_total sp addr (map rs (map preg_of args)) = Val.add rs1#r1 (Vint n) -> + (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ agree ms' sp rs') -> @@ -1207,8 +1102,8 @@ Lemma transl_load_store_correct: | None => True | Some mk => (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, - eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (eval_shift_addr sa rs1) -> - agree ms sp rs1 -> + eval_addressing_total sp addr (map rs (map preg_of args)) = Val.add rs1#r1 (eval_shift_addr sa rs1) -> + (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\ agree ms' sp rs') @@ -1224,62 +1119,53 @@ Proof. (* Aindexed *) case (is_immed i). (* Aindexed, small displacement *) - apply H; eauto. simpl. rewrite (ireg_val ms sp rs); auto. + apply H; auto. (* Aindexed, large displacement *) - exploit (addimm_correct IR14 (ireg_of t)); eauto with ppcgen. - intros [rs' [A [B C]]]. - exploit (H IR14 rs' Int.zero); eauto. - simpl. rewrite (ireg_val ms sp rs); auto. rewrite B. - rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. - apply agree_exten_2 with rs; auto. + destruct (addimm_correct IR14 (ireg_of m0) i (mk_instr_imm IR14 Int.zero :: k) rs m) + as [rs' [A [B C]]]. + exploit (H 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. (* Aindexed2 *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. + apply H0; auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (ms t0)))). + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (rs (ireg_of m1))))). exploit (H IR14 rs' Int.zero); eauto. - simpl. repeat rewrite (ireg_val ms sp rs); auto. unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. - unfold rs'; auto with ppcgen. + apply val_add_add_zero. + unfold rs'. intros. repeat Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. repeat rewrite <- (ireg_val ms sp rs); auto. - auto. + simpl. auto. auto. (* Aindexed2shift *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. - rewrite transl_shift_addr_correct. auto. + apply H0; auto. rewrite transl_shift_addr_correct. auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (eval_shift_total s (ms t0))))). + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (eval_shift_total s (rs (ireg_of m1)))))). exploit (H IR14 rs' Int.zero); eauto. - simpl. repeat rewrite (ireg_val ms sp rs); auto. unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. - unfold rs'; auto with ppcgen. + apply val_add_add_zero. + unfold rs'; intros; repeat Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. rewrite transl_shift_correct. - repeat rewrite <- (ireg_val ms sp rs); auto. + simpl. rewrite transl_shift_correct. auto. auto. (* Ainstack *) destruct (is_immed i). (* Ainstack, short displacement *) - apply H. simpl. rewrite (sp_val ms sp rs); auto. auto. + apply H; auto. rewrite (sp_val _ _ _ H1). auto. (* Ainstack, large displacement *) - exploit (addimm_correct IR14 IR13); eauto with ppcgen. - intros [rs' [A [B C]]]. + destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m) + as [rs' [A [B C]]]. exploit (H IR14 rs' Int.zero); eauto. - simpl. rewrite (sp_val ms sp rs); auto. rewrite B. - rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. - apply agree_exten_2 with rs; auto. + rewrite (sp_val _ _ _ H1). rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. auto. intros [rs'' [D E]]. exists rs''; split. eapply exec_straight_trans. eexact A. eexact D. auto. @@ -1288,116 +1174,159 @@ Qed. Lemma transl_load_int_correct: forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m chunk a v, + (rd: mreg) addr args k ms sp rs m m' chunk a v, (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m = - exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + exec_instr ge c (mk_instr r1 r2 sa) rs1 m' = + exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m') -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> mreg_type rd = Tint -> eval_addressing ge sp addr (map ms args) = Some a -> Mem.loadv chunk m a = Some v -> + Mem.extends m m' -> exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m - k rs' m - /\ agree (Regmap.set rd v ms) sp rs'. + exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m' + k rs' m' + /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. Proof. intros. unfold transl_load_store_int. - exploit eval_addressing_weaken. eauto. intros. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + exploit eval_addressing_weaken. eexact A. intros E. apply transl_load_store_correct with ms; auto. - intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split. - apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. - unfold exec_load. rewrite H4. auto. auto. - auto with ppcgen. - intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split. - apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. - unfold exec_load. rewrite H4. auto. auto. - auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (Vint n) = a') by congruence. + exists (nextinstr (rs1#(ireg_of rd) <- v')); split. + apply exec_straight_one. rewrite H. unfold exec_load. + simpl. rewrite H8. rewrite C. auto. auto. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. + unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. + exists (nextinstr (rs1#(ireg_of rd) <- v')); split. + apply exec_straight_one. rewrite H. unfold exec_load. + simpl. rewrite H8. rewrite C. auto. auto. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. + unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. Qed. Lemma transl_load_float_correct: forall (mk_instr: freg -> ireg -> int -> instruction) (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m chunk a v, + (rd: mreg) addr args k ms sp rs m m' chunk a v, (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 n) rs1 m = - exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + exec_instr ge c (mk_instr r1 r2 n) rs1 m' = + exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m') -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> mreg_type rd = Tfloat -> eval_addressing ge sp addr (map ms args) = Some a -> Mem.loadv chunk m a = Some v -> + Mem.extends m m' -> exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m - k rs' m - /\ agree (Regmap.set rd v ms) sp rs'. + exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m' + k rs' m' + /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. Proof. - intros. unfold transl_load_store_float. - exploit eval_addressing_weaken. eauto. intros. + intros. unfold transl_load_store_int. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + exploit eval_addressing_weaken. eexact A. intros E. apply transl_load_store_correct with ms; auto. - intros. exists (nextinstr (rs1#(freg_of rd) <- v)); split. - apply exec_straight_one. rewrite H. rewrite <- H6. rewrite H5. - unfold exec_load. rewrite H4. auto. auto. - auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (Vint n) = a') by congruence. + exists (nextinstr (rs1#(freg_of rd) <- v')); split. + apply exec_straight_one. rewrite H. unfold exec_load. + simpl. rewrite H8. rewrite C. auto. auto. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. + unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. Qed. Lemma transl_store_int_correct: forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m chunk a m', + (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m = - exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + exec_instr ge c (mk_instr r1 r2 sa) rs1 m1' = + exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m1') -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> mreg_type rd = Tint -> eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m a (ms rd) = Some m' -> - exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m - k rs' m' - /\ agree ms sp rs'. + Mem.storev chunk m1 a (ms rd) = Some m2 -> + Mem.extends m1 m1' -> + exists m2', + Mem.extends m2 m2' /\ + exists rs', + exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m1' + k rs' m2' + /\ agree (undef_temps ms) sp rs'. Proof. intros. unfold transl_load_store_int. - exploit eval_addressing_weaken. eauto. intros. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + exploit preg_val; eauto. instantiate (1 := rd). intros C. + exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. + exploit eval_addressing_weaken. eexact A. intros F. + exists m2'; split; auto. apply transl_load_store_correct with ms; auto. - intros. exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. - unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto. - rewrite H4. auto. auto. - auto with ppcgen. - intros. exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. - unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto. - rewrite H4. auto. auto. - auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (Vint n) = a') by congruence. + exists (nextinstr rs1); split. + apply exec_straight_one. rewrite H. simpl. rewrite H8. + unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. + apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. + exists (nextinstr rs1); split. + apply exec_straight_one. rewrite H. simpl. rewrite H8. + unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. + apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. Qed. Lemma transl_store_float_correct: forall (mk_instr: freg -> ireg -> int -> instruction) (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m chunk a m', - (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 n) rs1 m = - exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', + (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset) m2', + exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m1' = OK (nextinstr rs1) m2' -> + exists rs2, + exec_instr ge c (mk_instr r1 r2 n) rs1 m1' = OK rs2 m2' + /\ (forall (r: preg), r <> FR3 -> rs2 r = nextinstr rs1 r)) -> agree ms sp rs -> map mreg_type args = type_of_addressing addr -> mreg_type rd = Tfloat -> eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m a (ms rd) = Some m' -> - exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m - k rs' m' - /\ agree ms sp rs'. + Mem.storev chunk m1 a (ms rd) = Some m2 -> + Mem.extends m1 m1' -> + exists m2', + Mem.extends m2 m2' /\ + exists rs', + exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m1' + k rs' m2' + /\ agree (undef_temps ms) sp rs'. Proof. intros. unfold transl_load_store_float. - exploit eval_addressing_weaken. eauto. intros. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. + intros [a' [A B]]. + exploit preg_val; eauto. instantiate (1 := rd). intros C. + exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. + exploit eval_addressing_weaken. eexact A. intros F. + exists m2'; split; auto. apply transl_load_store_correct with ms; auto. - intros. exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. - unfold exec_store. rewrite <- (freg_val ms sp rs1); auto. - rewrite H4. auto. auto. - auto with ppcgen. + intros. + assert (Val.add (rs1 r1) (Vint n) = a') by congruence. + exploit (H fn (freg_of rd) r1 n rs1 m2'). + unfold exec_store. rewrite H8. rewrite H7; auto with ppcgen. rewrite D. auto. + intros [rs2 [P Q]]. + exists rs2; split. apply exec_straight_one. auto. rewrite Q; auto with ppcgen. + apply agree_exten_temps with rs; auto. + intros. rewrite Q; auto with ppcgen. Simpl. apply H7; auto with ppcgen. Qed. End STRAIGHTLINE. diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v index e55c7f9..a56a5ef 100644 --- a/arm/ConstpropOp.v +++ b/arm/ConstpropOp.v @@ -345,9 +345,6 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), | eval_static_operation_case49: forall n1, eval_static_operation_cases (Ofloatofint) (I n1 :: nil) - | eval_static_operation_case50: - forall n1, - eval_static_operation_cases (Ofloatofintu) (I n1 :: nil) | eval_static_operation_case51: forall c vl, eval_static_operation_cases (Ocmp c) (vl) @@ -458,8 +455,6 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) := eval_static_operation_case48 n1 | Ofloatofint, I n1 :: nil => eval_static_operation_case49 n1 - | Ofloatofintu, I n1 :: nil => - eval_static_operation_case50 n1 | Ocmp c, vl => eval_static_operation_case51 c vl | Oshrximm n, I n1 :: nil => @@ -568,8 +563,6 @@ Definition eval_static_operation (op: operation) (vl: list approx) := I(Float.intoffloat n1) | eval_static_operation_case49 n1 => F(Float.floatofint n1) - | eval_static_operation_case50 n1 => - F(Float.floatofintu n1) | eval_static_operation_case51 c vl => match eval_static_condition c vl with | None => Unknown diff --git a/arm/Op.v b/arm/Op.v index 1f26a72..606281d 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -110,10 +110,8 @@ Inductive operation : Type := | Odivf: operation (**r [rd = r1 / r2] *) | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) (*c Conversions between int and float: *) - | Ointoffloat: operation (**r [rd = int_of_float(r1)] *) - | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) + | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) - | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) (*c Boolean tests: *) | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) @@ -282,16 +280,9 @@ Definition eval_operation | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) - | Osingleoffloat, v1 :: nil => - Some (Val.singleoffloat v1) - | Ointoffloat, Vfloat f1 :: nil => - Some (Vint (Float.intoffloat f1)) - | Ointuoffloat, Vfloat f1 :: nil => - Some (Vint (Float.intuoffloat f1)) - | Ofloatofint, Vint n1 :: nil => - Some (Vfloat (Float.floatofint n1)) - | Ofloatofintu, Vint n1 :: nil => - Some (Vfloat (Float.floatofintu n1)) + | Osingleoffloat, v1 :: nil => Some (Val.singleoffloat v1) + | Ointoffloat, Vfloat f1 :: nil => Some (Vint (Float.intoffloat f1)) + | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1)) | Ocmp c, _ => match eval_condition c vl with | None => None @@ -493,9 +484,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) | Osingleoffloat => (Tfloat :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) - | Ointuoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ocmp c => (type_of_condition c, Tint) end. @@ -659,9 +648,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val : | Odivf, v1::v2::nil => Val.divf v1 v2 | Osingleoffloat, v1::nil => Val.singleoffloat v1 | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ocmp c, _ => eval_condition_total c vl | _, _ => Vundef end. @@ -919,3 +906,70 @@ Lemma type_op_for_binary_addressing: Proof. intros. destruct addr; simpl in H; reflexivity || omegaContradiction. Qed. + +(** Two-address operations. There are none in the ARM architecture. *) + +Definition two_address_op (op: operation) : bool := false. + +(** Operations that are so cheap to recompute that CSE should not factor them out. *) + +Definition is_trivial_op (op: operation) : bool := + match op with + | Omove => true + | Ointconst _ => true + | Oaddrsymbol _ _ => true + | Oaddrstack _ => true + | _ => false + end. + +(** Shifting stack-relative references. This is used in [Stacking]. *) + +Definition shift_stack_addressing (delta: int) (addr: addressing) := + match addr with + | Ainstack ofs => Ainstack (Int.add delta ofs) + | _ => addr + end. + +Definition shift_stack_operation (delta: int) (op: operation) := + match op with + | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | _ => op + end. + +Lemma shift_stack_eval_addressing: + forall (F V: Type) (ge: Genv.t F V) sp addr args delta, + eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args = + eval_addressing ge sp addr args. +Proof. + intros. destruct addr; simpl; auto. + destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. + decEq. decEq. rewrite <- Int.add_assoc. decEq. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. apply Int.add_zero. +Qed. + +Lemma shift_stack_eval_operation: + forall (F V: Type) (ge: Genv.t F V) sp op args delta, + eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = + eval_operation ge sp op args. +Proof. + intros. destruct op; simpl; auto. + destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. + decEq. decEq. rewrite <- Int.add_assoc. decEq. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. apply Int.add_zero. +Qed. + +Lemma type_shift_stack_addressing: + forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. +Proof. + intros. destruct addr; auto. +Qed. + +Lemma type_shift_stack_operation: + forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. +Proof. + intros. destruct op; auto. +Qed. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 9e1cae7..4f470ce 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -79,6 +79,11 @@ let float_reg_name = function let ireg oc r = output_string oc (int_reg_name r) let freg oc r = output_string oc (float_reg_name r) +let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + let condition_name = function | CReq -> "eq" | CRne -> "ne" @@ -417,30 +422,8 @@ let print_instruction oc labels = function fprintf oc " dvfd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 | Pfixz(r1, r2) -> fprintf oc " fixz %a, %a\n" ireg r1 freg r2; 1 - | Pfixzu(r1, r2) -> - (* F3 = second float temporary is unused at this point, - but this should be reflected in the proof *) - let lbl = label_float 2147483648.0 in - let lbl2 = new_label() in - fprintf oc " ldfd f3, .L%d\n" lbl; - fprintf oc " cmfe %a, f3\n" freg r2; - fprintf oc " fixltz %a, %a\n" ireg r1 freg r2; - fprintf oc " blt .L%d\n" lbl2; - fprintf oc " sufd f3, %a, f3\n" freg r2; - fprintf oc " fixz %a, f3\n" ireg r1; - fprintf oc " eor %a, %a, #-2147483648\n" ireg r1 ireg r1; - fprintf oc ".L%d\n" lbl2; - 7 | Pfltd(r1, r2) -> fprintf oc " fltd %a, %a\n" freg r1 ireg r2; 1 - | Pfltud(r1, r2) -> - fprintf oc " fltd %a, %a\n" freg r1 ireg r2; - fprintf oc " cmp %a, #0\n" ireg r2; - (* F3 = second float temporary is unused at this point, - but this should be reflected in the proof *) - let lbl = label_float 4294967296.0 in - fprintf oc " ldfltd f3, .L%d\n" lbl; - fprintf oc " adfltd %a, %a, f3\n" freg r1 freg r1; 4 | Pldfd(r1, r2, n) -> fprintf oc " ldfd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 | Pldfs(r1, r2, n) -> @@ -465,8 +448,6 @@ let print_instruction oc labels = function | Pstfd(r1, r2, n) -> fprintf oc " stfd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 | Pstfs(r1, r2, n) -> - (* F3 = second float temporary is unused at this point, - but this should be reflected in the proof *) fprintf oc " mvfs f3, %a\n" freg r1; fprintf oc " stfs f3, [%a, #%a]\n" ireg r2 coqint n; 2 | Psufd(r1, r2, r3) -> diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 75d8593..dff4e4f 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -38,7 +38,7 @@ let print_condition reg pp = function fprintf pp "%a %su %a" reg r1 (comparison_name c) reg r2 | (Ccompshift(c, s), [r1;r2]) -> fprintf pp "%a %ss %a %a" reg r1 (comparison_name c) reg r2 shift s - | (Ccompu(c, s), [r1;r2]) -> + | (Ccompushift(c, s), [r1;r2]) -> fprintf pp "%a %su %a %a" reg r1 (comparison_name c) reg r2 shift s | (Ccompimm(c, n), [r1]) -> fprintf pp "%a %ss %ld" reg r1 (comparison_name c) (camlint_of_coqint n) @@ -68,7 +68,7 @@ let print_operation reg pp = function | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n) | Osub, [r1;r2] -> fprintf pp "%a - %a" reg r1 reg r2 | Osubshift s, [r1;r2] -> fprintf pp "%a - %a %a" reg r1 reg r2 shift s - | Osubrshift s, [r1;r2] -> fprintf pp "%a %a - %a" reg r2 shift s reg r1 + | Orsubshift s, [r1;r2] -> fprintf pp "%a %a - %a" reg r2 shift s reg r1 | Orsubimm n, [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint n) reg r1 | Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2 | Odiv, [r1;r2] -> fprintf pp "%a /s %a" reg r1 reg r2 @@ -99,9 +99,7 @@ let print_operation reg pp = function | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 - | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 - | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) | _ -> fprintf pp "" @@ -111,5 +109,3 @@ let print_addressing reg pp = function | Aindexed2shift s, [r1; r2] -> fprintf pp "%a + %a %a" reg r1 reg r2 shift s | Ainstack ofs, [] -> fprintf pp "stack(%ld)" (camlint_of_coqint ofs) | _ -> fprintf pp "" - - diff --git a/arm/SelectOp.v b/arm/SelectOp.v index 66c1299..df2413a 100644 --- a/arm/SelectOp.v +++ b/arm/SelectOp.v @@ -50,6 +50,14 @@ Require Import CminorSel. Open Local Scope cminorsel_scope. +(** ** Constants **) + +Definition addrsymbol (id: ident) (ofs: int) := + Eop (Oaddrsymbol id ofs) Enil. + +Definition addrstack (ofs: int) := + Eop (Oaddrstack ofs) Enil. + (** ** Integer logical negation *) (** The natural way to write smart constructors is by pattern-matching @@ -788,22 +796,24 @@ Definition same_expr_pure (e1 e2: expr) := Definition or (e1: expr) (e2: expr) := match e1, e2 with | Eop (Oshift (Olsl n1) (t1:::Enil), Eop (Oshift (Olsr n2) (t2:::Enil)) => ... + | Eop (Oshift (Olsr n1) (t1:::Enil), Eop (Oshift (Olsl n2) (t2:::Enil)) => ... | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. *) -(* TODO: symmetric of first case *) - Inductive or_cases: forall (e1: expr) (e2: expr), Type := | or_case1: forall n1 t1 n2 t2, or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil)) | or_case2: + forall n1 t1 n2 t2, + or_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) (Eop (Oshift (Slsl n2)) (t2:::Enil)) + | or_case3: forall s t1 t2, or_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | or_case3: + | or_case4: forall t1 s t2, or_cases (t1) (Eop (Oshift s) (t2:::Enil)) | or_default: @@ -814,10 +824,12 @@ Definition or_match (e1: expr) (e2: expr) := match e1 as z1, e2 as z2 return or_cases z1 z2 with | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => or_case1 n1 t1 n2 t2 + | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => + or_case2 n1 t1 n2 t2 | Eop (Oshift s) (t1:::Enil), t2 => - or_case2 s t1 t2 + or_case3 s t1 t2 | t1, Eop (Oshift s) (t2:::Enil) => - or_case3 t1 s t2 + or_case4 t1 s t2 | e1, e2 => or_default e1 e2 end. @@ -829,9 +841,14 @@ Definition or (e1: expr) (e2: expr) := && same_expr_pure t1 t2 then Eop (Oshift (Sror n2)) (t1:::Enil) else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) - | or_case2 s t1 t2 => + | or_case2 n1 t1 n2 t2 => + if Int.eq (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n1)) (t1:::Enil) + else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil) + | or_case3 s t1 t2 => Eop (Oorshift s) (t2:::t1:::Enil) - | or_case3 t1 s t2 => + | or_case4 t1 s t2 => Eop (Oorshift s) (t1:::t2:::Enil) | or_default e1 e2 => Eop Oor (e1:::e2:::Enil) @@ -919,118 +936,6 @@ Definition shr (e1: expr) (e2: expr) := Eop Oshr (e1:::e2:::Enil) end. -(** ** Truncations and sign extensions *) - -Inductive cast8signed_cases: forall (e1: expr), Type := - | cast8signed_case1: - forall (e2: expr), - cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) - | cast8signed_default: - forall (e1: expr), - cast8signed_cases e1. - -Definition cast8signed_match (e1: expr) := - match e1 as z1 return cast8signed_cases z1 with - | Eop Ocast8signed (e2 ::: Enil) => - cast8signed_case1 e2 - | e1 => - cast8signed_default e1 - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 e1 => e - | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) - end. - -Inductive cast8unsigned_cases: forall (e1: expr), Type := - | cast8unsigned_case1: - forall (e2: expr), - cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) - | cast8unsigned_default: - forall (e1: expr), - cast8unsigned_cases e1. - -Definition cast8unsigned_match (e1: expr) := - match e1 as z1 return cast8unsigned_cases z1 with - | Eop Ocast8unsigned (e2 ::: Enil) => - cast8unsigned_case1 e2 - | e1 => - cast8unsigned_default e1 - end. - -Definition cast8unsigned (e: expr) := - match cast8unsigned_match e with - | cast8unsigned_case1 e1 => e - | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) - end. - -Inductive cast16signed_cases: forall (e1: expr), Type := - | cast16signed_case1: - forall (e2: expr), - cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) - | cast16signed_default: - forall (e1: expr), - cast16signed_cases e1. - -Definition cast16signed_match (e1: expr) := - match e1 as z1 return cast16signed_cases z1 with - | Eop Ocast16signed (e2 ::: Enil) => - cast16signed_case1 e2 - | e1 => - cast16signed_default e1 - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 e1 => e - | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) - end. - -Inductive cast16unsigned_cases: forall (e1: expr), Type := - | cast16unsigned_case1: - forall (e2: expr), - cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) - | cast16unsigned_default: - forall (e1: expr), - cast16unsigned_cases e1. - -Definition cast16unsigned_match (e1: expr) := - match e1 as z1 return cast16unsigned_cases z1 with - | Eop Ocast16unsigned (e2 ::: Enil) => - cast16unsigned_case1 e2 - | e1 => - cast16unsigned_default e1 - end. - -Definition cast16unsigned (e: expr) := - match cast16unsigned_match e with - | cast16unsigned_case1 e1 => e - | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) - end. - -Inductive singleoffloat_cases: forall (e1: expr), Type := - | singleoffloat_case1: - forall (e2: expr), - singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) - | singleoffloat_default: - forall (e1: expr), - singleoffloat_cases e1. - -Definition singleoffloat_match (e1: expr) := - match e1 as z1 return singleoffloat_cases z1 with - | Eop Osingleoffloat (e2 ::: Enil) => - singleoffloat_case1 e2 - | e1 => - singleoffloat_default e1 - end. - -Definition singleoffloat (e: expr) := - match singleoffloat_match e with - | singleoffloat_case1 e1 => e - | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) - end. - (** ** Comparisons *) (* @@ -1106,20 +1011,39 @@ Definition compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -(** ** Other operators, not optimized. *) +(** ** Non-optimized operators. *) +Definition cast8unsigned (e: expr) := Eop Ocast8unsigned (e ::: Enil). +Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). +Definition cast16unsigned (e: expr) := Eop Ocast16unsigned (e ::: Enil). +Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil). +Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). Definition negf (e: expr) := Eop Onegf (e ::: Enil). Definition absf (e: expr) := Eop Oabsf (e ::: Enil). Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). -Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). +(** ** Conversions between unsigned ints and floats *) + +Definition intuoffloat (e: expr) := + let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + Elet e + (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil)) + (intoffloat (Eletvar O)) + (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))). + +Definition floatofintu (e: expr) := + let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + Elet e + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (floatofint (Eletvar O)) + (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). + (** ** Recognition of addressing modes for load and store operations *) (* diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index b260346..c8f177b 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -100,6 +100,24 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2. by the smart constructor. *) +Theorem eval_addrsymbol: + forall le id ofs b, + Genv.find_symbol ge id = Some b -> + eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs). +Proof. + intros. unfold addrsymbol. econstructor. constructor. + simpl. rewrite H. auto. +Qed. + +Theorem eval_addrstack: + forall le ofs b n, + sp = Vptr b n -> + eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)). +Proof. + intros. unfold addrstack. econstructor. constructor. + simpl. unfold offset_sp. rewrite H. auto. +Qed. + Theorem eval_notint: forall le a x, eval_expr ge sp e m le a (Vint x) -> @@ -644,7 +662,18 @@ Proof. destruct n1; auto. destruct n2; auto. auto. EvalOp. econstructor. EvalOp. simpl. reflexivity. econstructor; eauto with evalexpr. - simpl. congruence. + simpl. congruence. + caseEq (Int.eq (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize + && same_expr_pure t1 t2); intro. + destruct (andb_prop _ _ H1). + generalize (Int.eq_spec (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize). + rewrite H4. intro. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. + simpl. EvalOp. simpl. decEq. decEq. rewrite Int.or_commut. apply Int.or_ror. + destruct n2; auto. destruct n1; auto. auto. + EvalOp. econstructor. EvalOp. simpl. reflexivity. + econstructor; eauto with evalexpr. + simpl. congruence. EvalOp. simpl. rewrite Int.or_commut. congruence. EvalOp. simpl. congruence. EvalOp. @@ -702,55 +731,31 @@ Theorem eval_cast8signed: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). -Proof. - intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. +Proof. TrivialOp cast8signed. Qed. Theorem eval_cast8unsigned: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). -Proof. - intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. +Proof. TrivialOp cast8unsigned. Qed. Theorem eval_cast16signed: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). -Proof. - intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. +Proof. TrivialOp cast16signed. Qed. Theorem eval_cast16unsigned: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). -Proof. - intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. +Proof. TrivialOp cast16unsigned. Qed. Theorem eval_singleoffloat: forall le a v, eval_expr ge sp e m le a v -> eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). -Proof. - intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - EvalOp. -Qed. +Proof. TrivialOp singleoffloat. Qed. Theorem eval_comp_int: forall le c a x b y, @@ -894,30 +899,6 @@ Theorem eval_absf: eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). Proof. intros; unfold absf; EvalOp. Qed. -Theorem eval_intoffloat: - forall le a x, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). -Proof. intros; unfold intoffloat; EvalOp. Qed. - -Theorem eval_intuoffloat: - forall le a x, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). -Proof. intros; unfold intuoffloat; EvalOp. Qed. - -Theorem eval_floatofint: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). -Proof. intros; unfold floatofint; EvalOp. Qed. - -Theorem eval_floatofintu: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). -Proof. intros; unfold floatofintu; EvalOp. Qed. - Theorem eval_addf: forall le a x b y, eval_expr ge sp e m le a (Vfloat x) -> @@ -946,6 +927,60 @@ Theorem eval_divf: eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). Proof. intros; unfold divf; EvalOp. Qed. +Theorem eval_intoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). +Proof. TrivialOp intoffloat. Qed. + +Theorem eval_intuoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). +Proof. + intros. unfold intuoffloat. + econstructor. eauto. + set (f := Float.floatofintu Float.ox8000_0000). + assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)). + constructor. auto. + apply eval_Econdition with (v1 := Float.cmp Clt x f). + econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl. auto. + caseEq (Float.cmp Clt x f); intros. + rewrite Float.intuoffloat_intoffloat_1; auto. + EvalOp. + rewrite Float.intuoffloat_intoffloat_2; auto. + apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp. +Qed. + +Theorem eval_floatofint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). +Proof. intros; unfold floatofint; EvalOp. Qed. + +Theorem eval_floatofintu: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). +Proof. + intros. unfold floatofintu. + econstructor. eauto. + set (f := Float.floatofintu Float.ox8000_0000). + assert (eval_expr ge sp e m (Vint x :: le) (Eletvar O) (Vint x)). + constructor. auto. + apply eval_Econdition with (v1 := Int.ltu x Float.ox8000_0000). + econstructor. constructor. eauto. constructor. + simpl. auto. + caseEq (Int.ltu x Float.ox8000_0000); intros. + rewrite Float.floatofintu_floatofint_1; auto. + apply eval_floatofint; auto. + rewrite Float.floatofintu_floatofint_2; auto. + fold f. apply eval_addf. apply eval_floatofint. + rewrite Int.sub_add_opp. apply eval_addimm; auto. + EvalOp. +Qed. + Lemma eval_addressing: forall le chunk a v b ofs, eval_expr ge sp e m le a v -> diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v index 703dc12..fdccf75 100644 --- a/arm/linux/Conventions1.v +++ b/arm/linux/Conventions1.v @@ -56,6 +56,9 @@ Definition float_temporaries := FT1 :: FT2 :: nil. Definition temporaries := R IT1 :: R IT2 :: R FT1 :: R FT2 :: nil. +Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) +Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) + (** The [index_int_callee_save] and [index_float_callee_save] associate a unique positive integer to callee-save registers. This integer is used in [Stacking] to determine where to save these registers in @@ -641,4 +644,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. intro; simpl. ElimOrEq; reflexivity. Qed. - -- cgit v1.2.3