From 1f004665758e26e6e48d13f5702fe55af8944448 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 25 Oct 2016 15:11:30 +0200 Subject: Update ARM port. Not tested yet. --- arm/Archi.v | 16 ++++- arm/Asm.v | 30 ++++---- arm/Asmgen.v | 18 ++--- arm/Asmgenproof.v | 59 ++++++++------- arm/Asmgenproof1.v | 126 +++++++++++++++++++-------------- arm/ConstpropOp.vp | 20 ++++-- arm/ConstpropOpproof.v | 98 +++++++++++++++---------- arm/Conventions1.v | 19 ++++- arm/NeedOp.v | 6 +- arm/Op.v | 189 ++++++++++++++++++++++--------------------------- arm/SelectLong.vp | 21 ++++++ arm/SelectLongproof.v | 22 ++++++ arm/SelectOp.vp | 10 +-- arm/SelectOpproof.v | 17 ++--- arm/ValueAOp.v | 8 +-- 15 files changed, 388 insertions(+), 271 deletions(-) create mode 100644 arm/SelectLong.vp create mode 100644 arm/SelectLongproof.v (limited to 'arm') diff --git a/arm/Archi.v b/arm/Archi.v index fedc55f5..64afb3ec 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -20,10 +20,19 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. +Definition ptr64 := false. + Parameter big_endian: bool. -Notation align_int64 := 8%Z (only parsing). -Notation align_float64 := 8%Z (only parsing). +Definition align_int64 := 8%Z. +Definition align_float64 := 8%Z. + +Definition splitlong := true. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong, ptr64; congruence. +Qed. Program Definition default_pl_64 : bool * nan_pl 53 := (false, iter_nat 51 _ xO xH). @@ -45,7 +54,8 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque default_pl_64 choose_binop_pl_64 +Global Opaque ptr64 big_endian splitlong + default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. diff --git a/arm/Asm.v b/arm/Asm.v index 010d5d7b..d211ead0 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -199,10 +199,10 @@ Inductive instruction : Type := | Pfsts: freg -> ireg -> int -> instruction (**r float32 store *) (* Pseudo-instructions *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) - | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) + | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) - | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) + | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *) | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) @@ -376,7 +376,7 @@ Inductive outcome: Type := instruction ([nextinstr]) or branching to a label ([goto_label]). *) Definition nextinstr (rs: regset) := - rs#PC <- (Val.add rs#PC Vone). + rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one). Definition nextinstr_nf (rs: regset) := nextinstr (undef_flags rs). @@ -386,7 +386,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := | None => Stuck | Some pos => match rs#PC with - | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m | _ => Stuck end end. @@ -564,11 +564,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | None => Stuck end | Pbsymb id sg => - Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m | Pbreg r sg => Next (rs#PC <- (rs#r)) m | Pblsymb id sg => - Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m + Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m | Pblreg r sg => Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m | Pbic r1 r2 so => @@ -716,13 +716,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (* Pseudo-instructions *) | Pallocframe sz pos => let (m1, stk) := Mem.alloc m 0 sz in - let sp := (Vptr stk Int.zero) in - match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mint32 m1 (Val.offset_ptr sp pos) rs#IR13 with | None => Stuck | Some m2 => Next (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2 end | Pfreeframe sz pos => - match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with + match Mem.loadv Mint32 m (Val.offset_ptr rs#IR13 pos) with | None => Stuck | Some v => match rs#IR13 with @@ -810,7 +810,7 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := | extcall_arg_stack: forall ofs ty bofs v, bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> Mem.loadv (chunk_of_type ty) m - (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> + (Val.offset_ptr (rs (IR IR13)) (Ptrofs.repr bofs)) = Some v -> extcall_arg rs m (S Outgoing ofs ty) v. Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := @@ -839,14 +839,14 @@ Inductive step: state -> trace -> state -> Prop := forall b ofs f i rs m rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) (fn_code f) = Some i -> + find_instr (Ptrofs.unsigned ofs) (fn_code f) = Some i -> exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> + find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> eval_builtin_args ge rs (rs SP) m args vargs -> external_call ef ge vargs m t vres m' -> rs' = nextinstr @@ -855,7 +855,7 @@ Inductive step: state -> trace -> state -> Prop := step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', - rs PC = Vptr b Int.zero -> + rs PC = Vptr b Ptrofs.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> @@ -871,7 +871,7 @@ Inductive initial_state (p: program): state -> Prop := let ge := Genv.globalenv p in let rs0 := (Pregmap.init Vundef) - # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero) + # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) # IR14 <- Vzero # IR13 <- Vzero in Genv.init_mem p = Some m0 -> diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 90d3b189..bbfad3c9 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -362,7 +362,7 @@ Definition transl_op OK (Ploadsymbol r s ofs :: k) | Oaddrstack n, nil => do r <- ireg_of res; - OK (addimm r IR13 n k) + OK (addimm r IR13 (Ptrofs.to_int n) k) | Ocast8signed, a1 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; OK (if thumb tt then @@ -565,10 +565,11 @@ Definition indexed_memory_access then mk_instr base n :: k else addimm IR14 base (Int.sub n n1) (mk_instr IR14 n1 :: k). -Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := - indexed_memory_access (fun base n => Pldr dst base (SOimm n)) mk_immed_mem_word base ofs k. +Definition loadind_int (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) := + indexed_memory_access (fun base n => Pldr dst base (SOimm n)) mk_immed_mem_word base (Ptrofs.to_int ofs) k. -Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := +Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := + let ofs := Ptrofs.to_int ofs in match ty, preg_of dst with | Tint, IR r => OK (indexed_memory_access (fun base n => Pldr r base (SOimm n)) mk_immed_mem_word base ofs k) @@ -584,7 +585,8 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := Error (msg "Asmgen.loadind") end. -Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := +Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := + let ofs := Ptrofs.to_int ofs in match ty, preg_of src with | Tint, IR r => OK (indexed_memory_access (fun base n => Pstr r base (SOimm n)) mk_immed_mem_word base ofs k) @@ -628,7 +630,7 @@ Definition transl_memory_access Error (msg "Asmgen.Aindexed2shift") end | Ainstack n, nil => - OK (indexed_memory_access mk_instr_imm mk_immed IR13 n k) + OK (indexed_memory_access mk_instr_imm mk_immed IR13 (Ptrofs.to_int n) k) | _, _ => Error(msg "Asmgen.transl_memory_access") end. @@ -788,11 +790,11 @@ Definition transl_function (f: Mach.function) := do c <- transl_code f f.(Mach.fn_code) true; OK (mkfunction f.(Mach.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SOimm f.(fn_retaddr_ofs)) :: c)). + Pstr IR14 IR13 (SOimm (Ptrofs.to_int f.(fn_retaddr_ofs))) :: c)). Definition transf_function (f: Mach.function) : res Asm.function := do tf <- transl_function f; - if zlt Int.max_unsigned (list_length_z tf.(fn_code)) + if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code)) then Error (msg "code size exceeded") else OK tf. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 431743c6..ade121c5 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -18,6 +18,8 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Mach Conventions Asm. Require Import Asmgen Asmgenproof0 Asmgenproof1. +Local Transparent Archi.ptr64. + Definition match_prog (p: Mach.program) (tp: Asm.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -64,9 +66,9 @@ Qed. Lemma transf_function_no_overflow: forall f tf, - transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. + transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega. Qed. Lemma exec_straight_exec: @@ -335,7 +337,7 @@ Lemma transl_find_label: | Some c => exists tc, find_label lbl (fn_code tf) = Some tc /\ transl_code f c false = OK tc end. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. simpl. eapply transl_code_label; eauto. Qed. @@ -360,10 +362,10 @@ Proof. intros [tc [A B]]. exploit label_pos_code_tail; eauto. instantiate (1 := 0). intros [pos' [P [Q R]]]. - exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))). + exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. - rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q. + rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. auto. omega. generalize (transf_function_no_overflow _ _ H0). omega. intros. apply Pregmap.gso; auto. @@ -379,7 +381,7 @@ Proof. - intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. - destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. exists x; exists true; split; auto. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -418,7 +420,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop := (STACKS: match_stack ge s) (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Int.zero) + (ATPC: rs PC = Vptr fb Ptrofs.zero) (ATLR: rs RA = parent_ra s), match_states (Mach.Callstate s fb ms m) (Asm.State rs m') @@ -624,13 +626,13 @@ Opaque loadind. eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) - assert (rs rf = Vptr f' Int.zero). + assert (rs rf = Vptr f' Ptrofs.zero). destruct (rs rf); try discriminate. - revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (rs0 x0 = Vptr f' Int.zero). + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Ptrofs.zero). exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -644,7 +646,7 @@ Opaque loadind. Simpl. rewrite <- H2. auto. + (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -660,7 +662,7 @@ Opaque loadind. - (* Mtailcall *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. - assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). + assert (NOOV: list_length_z (fn_code tf) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. exploit Mem.loadv_extends. eauto. eexact H1. auto. unfold chunk_of_type. rewrite (sp_val _ _ _ AG). intros [parent' [A B]]. @@ -682,16 +684,16 @@ Opaque loadind. exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. + simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A; simpl in A. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. intros. Simpl. } destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) - assert (rs rf = Vptr f' Int.zero). + assert (rs rf = Vptr f' Ptrofs.zero). destruct (rs rf); try discriminate. - revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (rs0 x0 = Vptr f' Int.zero). + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Ptrofs.zero). exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]]. exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. @@ -850,7 +852,7 @@ Opaque loadind. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. + destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. monadInv EQ0. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. @@ -860,24 +862,27 @@ Opaque loadind. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. (* Execution of function prologue *) - set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). + set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))). set (rs3 := nextinstr rs2). assert (EXEC_PROLOGUE: exec_straight tge x (fn_code x) rs0 m' x1 rs3 m3'). - rewrite <- H5 at 2; unfold fn_code. + replace (fn_code x) + with (Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x1) + by (rewrite <- H5; auto). apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. + rewrite <- (sp_val _ _ _ AG). unfold Tptr, chunk_of_type, Archi.ptr64 in F. rewrite F. auto. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). - rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. - rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. + rewrite Ptrofs.add_zero_l. simpl. unfold Tptr, chunk_of_type, Archi.ptr64 in P. simpl in P. + rewrite Ptrofs.add_zero_l in P. rewrite ATLR. rewrite Ptrofs.of_int_to_int by auto. + rewrite P. auto. auto. auto. left; exists (State rs3 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. econstructor; eauto. - change (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone). + change (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. subst x. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. constructor. @@ -915,12 +920,12 @@ Proof. econstructor; split. econstructor. eapply (Genv.init_mem_transf_partial TRANSF); eauto. - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr fb Int.zero). + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) + with (Vptr fb Ptrofs.zero). econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. + split. auto. simpl. unfold Vnullptr; simpl; congruence. intros. rewrite Regmap.gi. auto. unfold Genv.symbol_address. rewrite (match_program_main TRANSF). rewrite symbols_preserved. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 76a7b080..252a294a 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -30,6 +30,8 @@ Require Import Asmgen. Require Import Conventions. Require Import Asmgenproof0. +Local Transparent Archi.ptr64. + (** Useful properties of the R14 registers. *) Lemma ireg_of_not_R14: @@ -49,7 +51,7 @@ Hint Resolve ireg_of_not_R14': asmgen. (** [undef_flags] and [nextinstr_nf] *) Lemma nextinstr_nf_pc: - forall rs, (nextinstr_nf rs)#PC = Val.add rs#PC Vone. + forall rs, (nextinstr_nf rs)#PC = Val.offset_ptr rs#PC Ptrofs.one. Proof. intros. reflexivity. Qed. @@ -520,49 +522,55 @@ Qed. Lemma loadind_int_correct: forall (base: ireg) ofs dst (rs: regset) m v k, - Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> + Mem.loadv Mint32 m (Val.offset_ptr rs#base ofs) = Some v -> exists rs', exec_straight ge fn (loadind_int base ofs dst k) rs m k rs' m /\ rs'#dst = v /\ forall r, if_preg r = true -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. - intros; unfold loadind_int. apply indexed_memory_access_correct; intros. + intros; unfold loadind_int. + assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } + apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. + apply exec_straight_one. simpl. unfold exec_load. rewrite H1, <- H0, H. eauto. auto. split; intros; Simpl. Qed. Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> - Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> + Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v /\ forall r, if_preg r = true -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - unfold loadind; intros. destruct ty; destruct (preg_of dst); inv H; simpl in H0. + unfold loadind; intros. + assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } + destruct ty; destruct (preg_of dst); inv H; simpl in H0. - (* int *) apply loadind_int_correct; auto. - (* float *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto. split; intros; Simpl. - (* single *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto. split; intros; Simpl. - (* any32 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto. split; intros; Simpl. - (* any64 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto. split; intros; Simpl. Qed. @@ -571,43 +579,40 @@ Qed. Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', storeind src base ofs ty k = OK c -> - Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> + Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) (rs#(preg_of src)) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' /\ forall r, if_preg r = true -> r <> IR14 -> rs'#r = rs#r. Proof. unfold storeind; intros. assert (DATA: data_preg (preg_of src) = true) by eauto with asmgen. + assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } destruct ty; destruct (preg_of src); inv H; simpl in H0. - (* int *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* float *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* single *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* any32 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* any64 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. - rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. Qed. @@ -731,32 +736,32 @@ Proof. destruct (Int.ltu i i0); reflexivity. (* int ptr *) destruct (Int.eq i Int.zero && - (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr int *) destruct (Int.eq i0 Int.zero && - (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr ptr *) simpl. - fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. - fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. + fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *. + fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *. destruct (eq_block b0 b1). - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && - Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. + destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) && + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inversion H1. destruct c; simpl; auto. - destruct (Int.eq i i0); reflexivity. - destruct (Int.eq i i0); auto. - destruct (Int.ltu i i0); auto. - rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto. - rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. - destruct (Int.ltu i i0); reflexivity. - destruct (Mem.valid_pointer m b0 (Int.unsigned i) && - Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. + destruct (Ptrofs.eq i i0); reflexivity. + destruct (Ptrofs.eq i i0); auto. + destruct (Ptrofs.ltu i i0); auto. + rewrite (Ptrofs.not_ltu i i0). destruct (Ptrofs.ltu i i0); simpl; destruct (Ptrofs.eq i i0); auto. + rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity. + destruct (Ptrofs.ltu i i0); reflexivity. + destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) && + Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate. destruct c; simpl in *; inv H1; reflexivity. Qed. @@ -785,7 +790,7 @@ Qed. Lemma compare_float_nextpc: forall rs v1 v2, - nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone. + nextinstr (compare_float rs v1 v2) PC = Val.offset_ptr (rs PC) Ptrofs.one. Proof. intros. unfold compare_float. destruct v1; destruct v2; reflexivity. Qed. @@ -891,7 +896,7 @@ Qed. Lemma compare_float32_nextpc: forall rs v1 v2, - nextinstr (compare_float32 rs v1 v2) PC = Val.add (rs PC) Vone. + nextinstr (compare_float32 rs v1 v2) PC = Val.offset_ptr (rs PC) Ptrofs.one. Proof. intros. unfold compare_float32. destruct v1; destruct v2; reflexivity. Qed. @@ -1138,7 +1143,7 @@ Lemma transl_op_correct_same: forall op args res k c (rs: regset) m v, transl_op op args res k = OK c -> eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> - match op with Ocmp _ => False | _ => True end -> + match op with Ocmp _ => False | Oaddrstack _ => False | _ => True end -> exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v @@ -1155,9 +1160,7 @@ Proof. generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oaddrstack *) - generalize (addimm_correct x IR13 i k rs m). - intros [rs' [EX [RES OTH]]]. - exists rs'; auto with asmgen. + contradiction. (* Ocast8signed *) destruct (thumb tt). econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. @@ -1296,19 +1299,29 @@ Lemma transl_op_correct: /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r. Proof. intros. - assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp). - destruct op; auto. right; exists c0; auto. - destruct EITHER as [A | [cmp A]]. - exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]]. - subst v. exists rs'; eauto. - (* Ocmp *) - subst op. simpl in H. monadInv H. simpl in H0. inv H0. + assert (SAME: + (exists rs', exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of res) = v + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r) -> + exists rs', exec_straight ge fn c rs m k rs' m + /\ Val.lessdef v rs'#(preg_of res) + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r). + { intros (rs' & A & B & C). subst v; exists rs'; auto. } + destruct op; try (apply SAME; eapply transl_op_correct_same; eauto; fail). +- (* Oaddrstack *) + clear SAME; simpl in *; ArgsInv. + destruct (addimm_correct x IR13 (Ptrofs.to_int i) k rs m) as [rs' [EX [RES OTH]]]. + exists rs'; split. auto. split. + rewrite RES; inv H0. destruct (rs IR13); simpl; auto. rewrite Ptrofs.of_int_to_int; auto. + intros; apply OTH; eauto with asmgen. +- (* Ocmp *) + clear SAME. simpl in H. monadInv H. simpl in H0. inv H0. rewrite (ireg_of_eq _ _ EQ). exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. - destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto. + destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. destruct B as [B1 B2]; rewrite B1. destruct b; auto. Qed. @@ -1317,7 +1330,10 @@ Qed. Remark val_add_add_zero: forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero). Proof. - intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto. + intros. destruct v1; destruct v2; simpl; auto. + rewrite Int.add_zero; auto. + rewrite Ptrofs.add_zero; auto. + rewrite Ptrofs.add_zero; auto. Qed. Lemma transl_memory_access_correct: @@ -1327,6 +1343,7 @@ Lemma transl_memory_access_correct: addr args k c (rs: regset) a m m', transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + match a with Vptr _ _ => True | _ => False end -> (forall (r1: ireg) (rs1: regset) n k, Val.add rs1#r1 (Vint n) = a -> (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) -> @@ -1343,7 +1360,7 @@ Lemma transl_memory_access_correct: exists rs', exec_straight ge fn c rs m k rs' m' /\ P rs'. Proof. - intros until m'; intros TR EA MK1 MK2. + intros until m'; intros TR EA ADDR MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA. (* Aindexed *) apply indexed_memory_access_correct. exact MK1. @@ -1354,7 +1371,8 @@ Proof. destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto. (* Ainstack *) - inv TR. apply indexed_memory_access_correct. exact MK1. + inv TR. apply indexed_memory_access_correct. intros. eapply MK1; eauto. + rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs. Qed. Lemma transl_load_int_correct: @@ -1372,6 +1390,7 @@ Lemma transl_load_int_correct: Proof. intros. monadInv H. erewrite ireg_of_eq by eauto. eapply transl_memory_access_correct; eauto. + destruct a; discriminate || trivial. intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_load. simpl eval_shift_op. rewrite H. rewrite H1. eauto. auto. split. Simpl. intros; Simpl. @@ -1396,6 +1415,7 @@ Lemma transl_load_float_correct: Proof. intros. monadInv H. erewrite freg_of_eq by eauto. eapply transl_memory_access_correct; eauto. + destruct a; discriminate || trivial. intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. split. Simpl. intros; Simpl. @@ -1417,6 +1437,7 @@ Proof. intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen. monadInv H. erewrite ireg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. + destruct a; discriminate || trivial. intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen. rewrite H1. eauto. auto. @@ -1442,6 +1463,7 @@ Proof. intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen. monadInv H. erewrite freg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. + destruct a; discriminate || trivial. intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto. intros; Simpl. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 872493a6..e0f0889f 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -22,6 +22,18 @@ Require Import Op. Require Import Registers. Require Import ValueDomain. +(** * Converting known values to constants *) + +Definition const_for_result (a: aval) : option operation := + match a with + | I n => Some(Ointconst n) + | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None + | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None + | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs) + | Ptr(Stk ofs) => Some(Oaddrstack ofs) + | _ => None + end. + (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of @@ -237,19 +249,19 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => - (Ainstack (Int.add n1 n2), nil) + (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n2)), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil => - (Ainstack (Int.add n1 n2), nil) + (Ainstack (Ptrofs.add (Ptrofs.of_int n1) n2), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Aindexed n1, r2 :: nil) | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed n2, r1 :: nil) | Aindexed2shift s, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => - (Ainstack (Int.add n1 (eval_static_shift s n2)), nil) + (Ainstack (Ptrofs.add n1 (Ptrofs.of_int (eval_static_shift s n2))), nil) | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed (eval_static_shift s n2), r1 :: nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => - (Ainstack (Int.add n1 n), nil) + (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n)), nil) | _, _, _ => (addr, args) end. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 0b7643c6..e1ae80a2 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -27,6 +27,8 @@ Require Import RTL. Require Import ValueDomain. Require Import ConstpropOp. +Local Transparent Archi.ptr64. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing @@ -95,6 +97,28 @@ Ltac SimplVM := | _ => idtac end. +Lemma const_for_result_correct: + forall a op v, + const_for_result a = Some op -> + vmatch bc v a -> + exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'. +Proof. + unfold const_for_result; intros. + destruct a; inv H; SimplVM. +- (* integer *) + exists (Vint n); auto. +- (* float *) + destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto. +- (* single *) + destruct (generate_float_constants tt); inv H2. exists (Vsingle f); auto. +- (* pointer *) + destruct p; try discriminate; SimplVM. + + (* global *) + inv H2. exists (Genv.symbol_address ge id ofs); auto. + + (* stack *) + inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma eval_static_shift_correct: forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). Proof. @@ -146,7 +170,7 @@ Lemma make_cmp_base_correct: forall c args vl, vl = map (fun r => AE.get r ae) args -> let (op', args') := make_cmp_base c args vl in - exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros. unfold make_cmp_base. @@ -159,7 +183,7 @@ Lemma make_cmp_correct: forall c args vl, vl = map (fun r => AE.get r ae) args -> let (op', args') := make_cmp c args vl in - exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. @@ -191,11 +215,12 @@ Qed. Lemma make_addimm_correct: forall n r, let (op, args) := make_addimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto. + subst. exists (rs#r); split; auto. + destruct (rs#r); simpl; auto. rewrite Int.add_zero; auto. rewrite Ptrofs.add_zero; auto. exists (Val.add rs#r (Vint n)); auto. Qed. @@ -203,7 +228,7 @@ Lemma make_shlimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shlimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. Proof. Opaque mk_shift_amount. intros; unfold make_shlimm. @@ -218,7 +243,7 @@ Lemma make_shrimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shrimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -232,7 +257,7 @@ Lemma make_shruimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shruimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -246,7 +271,7 @@ Lemma make_mulimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_mulimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -265,7 +290,7 @@ Lemma make_divimm_correct: Val.divs rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in - exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. destruct (Int.is_power2 n) eqn:?. @@ -280,7 +305,7 @@ Lemma make_divuimm_correct: Val.divu rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in - exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. destruct (Int.is_power2 n) eqn:?. @@ -295,7 +320,7 @@ Lemma make_andimm_correct: forall n r x, vmatch bc rs#r x -> let (op, args) := make_andimm n r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -320,7 +345,7 @@ Qed. Lemma make_orimm_correct: forall n r, let (op, args) := make_orimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -333,7 +358,7 @@ Qed. Lemma make_xorimm_correct: forall n r, let (op, args) := make_xorimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -348,7 +373,7 @@ Lemma make_mulfimm_correct: forall n r1 r2, rs#r2 = Vfloat n -> let (op, args) := make_mulfimm n r1 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. @@ -361,7 +386,7 @@ Lemma make_mulfimm_correct_2: forall n r1 r2, rs#r1 = Vfloat n -> let (op, args) := make_mulfimm n r2 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. @@ -375,7 +400,7 @@ Lemma make_mulfsimm_correct: forall n r1 r2, rs#r2 = Vsingle n -> let (op, args) := make_mulfsimm n r1 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. @@ -388,7 +413,7 @@ Lemma make_mulfsimm_correct_2: forall n r1 r2, rs#r1 = Vsingle n -> let (op, args) := make_mulfsimm n r2 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. @@ -402,7 +427,7 @@ Lemma make_cast8signed_correct: forall r x, vmatch bc rs#r x -> let (op, args) := make_cast8signed r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. @@ -416,7 +441,7 @@ Lemma make_cast16signed_correct: forall r x, vmatch bc rs#r x -> let (op, args) := make_cast16signed r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. @@ -429,9 +454,9 @@ Qed. Lemma op_strength_reduction_correct: forall op args vl v, vl = map (fun r => AE.get r ae) args -> - eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v -> let (op', args') := op_strength_reduction op args vl in - exists w, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; case (op_strength_reduction_match op args vl); simpl; intros. @@ -440,8 +465,7 @@ Proof. (* cast8signed *) InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto. (* add *) - InvApproxRegs; SimplVM. inv H0. - fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct. + InvApproxRegs; SimplVM. rewrite Val.add_commut in H0. inv H0. apply make_addimm_correct. InvApproxRegs; SimplVM. inv H0. apply make_addimm_correct. (* addshift *) InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_addimm_correct. @@ -504,28 +528,30 @@ Qed. Lemma addr_strength_reduction_correct: forall addr args vl res, vl = map (fun r => AE.get r ae) args -> - eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some res -> + eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some res -> let (addr', args') := addr_strength_reduction addr args vl in - exists res', eval_addressing ge (Vptr sp Int.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. + exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- rewrite Int.add_zero_l. - change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). +- rewrite Ptrofs.add_zero_l. + change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n2))) with (Val.add (Vptr sp n1) (Vint n2)). econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_zero_l. rewrite Int.add_commut. - change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)). - rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). - rewrite Val.add_commut. econstructor; split; eauto. +- rewrite Ptrofs.add_zero_l. econstructor; split; eauto. rewrite Ptrofs.add_commut. + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add (Vptr sp n2) (Vint n1))). + rewrite Val.add_commut; apply Val.add_lessdef; auto. +- econstructor; split; eauto. + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add rs#r2 (Vint n1))). + rewrite Val.add_commut; apply Val.add_lessdef; auto. - econstructor; split; eauto. -- rewrite eval_static_shift_correct. rewrite Int.add_zero_l. - change (Vptr sp (Int.add n1 (eval_static_shift s n2))) +- rewrite eval_static_shift_correct. rewrite Ptrofs.add_zero_l. econstructor; split; eauto. + change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int (eval_static_shift s n2)))) with (Val.add (Vptr sp n1) (Vint (eval_static_shift s n2))). - econstructor; split; eauto. apply Val.add_lessdef; auto. + apply Val.add_lessdef; auto. - rewrite eval_static_shift_correct. econstructor; split; eauto. -- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). +- rewrite Ptrofs.add_zero_l. + change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n))) with (Val.add (Vptr sp n1) (Vint n)). econstructor; split; eauto. apply Val.add_lessdef; auto. - exists res; auto. Qed. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 888861a5..ecf03e1d 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -60,6 +60,15 @@ Definition destroyed_at_call := Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) +Definition is_float_reg (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 + | R4 | R5 | R6 | R7 + | R8 | R9 | R10 | R11 | R12 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => true + end. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -127,7 +136,7 @@ Lemma loc_result_pair: forall sg, match loc_result sg with | One _ => True - | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.splitlong = true end. Proof. intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. @@ -135,6 +144,14 @@ Proof. intuition congruence. Qed. +(** The location of the result depends only on the result part of the signature *) + +Lemma loc_result_exten: + forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. +Proof. + intros. unfold loc_result. rewrite H; auto. +Qed. + (** ** Location of function arguments *) (** For the "hardfloat" configuration, we use the following calling conventions, diff --git a/arm/NeedOp.v b/arm/NeedOp.v index 41b80941..dee7cae1 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -145,11 +145,11 @@ Qed. Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -188,7 +188,7 @@ Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. diff --git a/arm/Op.v b/arm/Op.v index bc717d7b..0d31c2ac 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -35,6 +35,7 @@ Require Import Globalenvs. Require Import Events. Set Implicit Arguments. +Local Transparent Archi.ptr64. Record shift_amount: Type := { s_amount: int; @@ -74,8 +75,8 @@ Inductive operation : Type := | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given 64-bit float constant *) | Osingleconst: float32 -> operation (**r [rd] is set to the given 32-bit float constant *) - | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) - | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) + | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *) + | Oaddrstack: ptrofs -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) @@ -148,7 +149,7 @@ Inductive addressing: Type := | Aindexed: int -> addressing (**r Address is [r1 + offset] *) | Aindexed2: addressing (**r Address is [r1 + r2] *) | Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *) - | Ainstack: int -> addressing. (**r Address is [stack_pointer + offset] *) + | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) (** Comparison functions (used in module [CSE]). *) @@ -173,10 +174,8 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros. + generalize Float.eq_dec Float32.eq_dec; intros. generalize eq_shift; intro. generalize eq_condition; intro. decide equality. @@ -184,7 +183,7 @@ Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. + generalize Int.eq_dec Ptrofs.eq_dec; intro. generalize eq_shift; intro. decide equality. Defined. @@ -235,7 +234,7 @@ Definition eval_operation | Ofloatconst n, nil => Some (Vfloat n) | Osingleconst n, nil => Some (Vsingle n) | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) - | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2) @@ -305,10 +304,24 @@ Definition eval_addressing | Aindexed n, v1 :: nil => Some (Val.add v1 (Vint n)) | Aindexed2, v1 :: v2 :: nil => Some (Val.add v1 v2) | Aindexed2shift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2)) - | Ainstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Ainstack ofs, nil => Some (Val.offset_ptr sp ofs) | _, _ => None end. +Remark eval_addressing_Ainstack: + forall (F V: Type) (genv: Genv.t F V) sp ofs, + eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs). +Proof. + intros. reflexivity. +Qed. + +Remark eval_addressing_Ainstack_inv: + forall (F V: Type) (genv: Genv.t F V) sp ofs vl v, + eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs. +Proof. + unfold eval_addressing; intros; destruct vl; inv H; auto. +Qed. + Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => @@ -430,7 +443,7 @@ Lemma type_of_operation_sound: op <> Omove -> eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). -Proof with (try exact I). +Proof with (try exact I; try reflexivity). assert (S: forall s v, Val.has_type (eval_shift s v) Tint). intros. unfold eval_shift. destruct s; destruct v; simpl; auto; rewrite s_range; exact I. intros. @@ -588,15 +601,15 @@ Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := +Definition shift_stack_addressing (delta: Z) (addr: addressing) := match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) + | Ainstack ofs => Ainstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => addr end. -Definition shift_stack_operation (delta: int) (op: operation) := +Definition shift_stack_operation (delta: Z) (op: operation) := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | Oaddrstack ofs => Oaddrstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => op end. @@ -614,79 +627,43 @@ Qed. Lemma eval_shift_stack_addressing: forall F V (ge: Genv.t F V) sp addr vl delta, - eval_addressing ge sp (shift_stack_addressing delta addr) vl = - eval_addressing ge (Val.add sp (Vint delta)) addr vl. + eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. intros. destruct addr; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_shift_stack_operation: forall F V (ge: Genv.t F V) sp op vl m delta, - eval_operation ge sp (shift_stack_operation delta op) vl m = - eval_operation ge (Val.add sp (Vint delta)) op vl m. + eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = + eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. intros. destruct op; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that it designates the pointer [delta] bytes past the pointer designated by [addr]. May be undefined, in which case [None] is returned. *) -Definition offset_addressing (addr: addressing) (delta: int) : option addressing := +Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := match addr with - | Aindexed n => Some(Aindexed (Int.add n delta)) + | Aindexed n => Some(Aindexed (Int.add n (Int.repr delta))) | Aindexed2 => None | Aindexed2shift s => None - | Ainstack n => Some(Ainstack (Int.add n delta)) + | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta))) end. Lemma eval_offset_addressing: forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v, offset_addressing addr delta = Some addr' -> eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)). + eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))). Proof. intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. rewrite Val.add_assoc; auto. - rewrite Val.add_assoc. auto. -Qed. - -(** Transformation of addressing modes with two operands or more - into an equivalent arithmetic operation. This is used in the [Reload] - pass when a store instruction cannot be reloaded directly because - it runs out of temporary registers. *) - -(** For the ARM, there are only two binary addressing mode: [Aindexed2] - and [Aindexed2shift]. The corresponding operations are [Oadd] - and [Oaddshift]. *) - -Definition op_for_binary_addressing (addr: addressing) : operation := - match addr with - | Aindexed2 => Oadd - | Aindexed2shift s => Oaddshift s - | _ => Ointconst Int.zero (* never happens *) - end. - -Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v m, - (length args >= 2)%nat -> - eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. -Proof. - intros. - unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl. - congruence. - congruence. -Qed. - -Lemma type_op_for_binary_addressing: - forall addr, - (length (type_of_addressing addr) >= 2)%nat -> - type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). -Proof. - intros. destruct addr; simpl in H; reflexivity || omegaContradiction. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs. Qed. (** Two-address operations. There are none in the ARM architecture. *) @@ -781,30 +758,30 @@ Variable m2: mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Ltac InvInject := match goal with @@ -871,20 +848,20 @@ Lemma eval_operation_inj: Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. - apply Values.Val.add_inject; auto. + apply Val.offset_ptr_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. apply eval_shift_inj; auto. + apply Val.add_inject; auto. - apply Values.Val.sub_inject; auto. - apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. - apply (@Values.Val.sub_inject f (Vint i) (Vint i) v v'); auto. + apply Val.sub_inject; auto. + apply Val.sub_inject; auto. apply eval_shift_inj; auto. + apply Val.sub_inject; auto. apply eval_shift_inj; auto. + apply (@Val.sub_inject f (Vint i) (Vint i) v v'); auto. inv H4; inv H2; simpl; auto. - apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto. + apply Val.add_inject; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H3; simpl in H1; inv H1. simpl. @@ -965,10 +942,10 @@ Lemma eval_addressing_inj: exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. apply eval_shift_inj; auto. + apply Val.offset_ptr_inject; auto. Qed. End EVAL_COMPAT. @@ -984,40 +961,40 @@ Remark valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_no_overflow_extends: forall m1 b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. + intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> Some(b1, 0) = Some (b1', delta1) -> Some(b2, 0) = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. inv H2; inv H3. auto. Qed. @@ -1096,7 +1073,7 @@ Remark symbol_address_inject: Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. - econstructor; eauto. rewrite Int.add_zero; auto. + econstructor; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma eval_condition_inject: @@ -1116,34 +1093,36 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, Val.inject_list f vl1 vl2 -> - eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 -> exists v2, - eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_addressing. simpl. - eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - intros; apply symbol_address_inject. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> - eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 -> exists v2, - eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. - eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. + eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. intros; apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. diff --git a/arm/SelectLong.vp b/arm/SelectLong.vp new file mode 100644 index 00000000..cc7a38f6 --- /dev/null +++ b/arm/SelectLong.vp @@ -0,0 +1,21 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import Coqlib. +Require Import Compopts. +Require Import AST Integers Floats. +Require Import Op CminorSel. +Require Import SelectOp SplitLong. + +(** This file is empty because we use the default implementation provided in [SplitLong]. *) diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v new file mode 100644 index 00000000..a82c082c --- /dev/null +++ b/arm/SelectLongproof.v @@ -0,0 +1,22 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import String Coqlib Maps Integers Floats Errors. +Require Archi. +Require Import AST Values Memory Globalenvs Events. +Require Import Cminor Op CminorSel. +Require Import SelectOp SelectOpproof SplitLong SplitLongproof. +Require Import SelectLong. + +(** This file is empty because we use the default implementation provided in [SplitLong]. *) diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index aec737ad..80a5d753 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -48,10 +48,10 @@ Open Local Scope cminorsel_scope. (** ** Constants **) -Definition addrsymbol (id: ident) (ofs: int) := +Definition addrsymbol (id: ident) (ofs: ptrofs) := Eop (Oaddrsymbol id ofs) Enil. -Definition addrstack (ofs: int) := +Definition addrstack (ofs: ptrofs) := Eop (Oaddrstack ofs) Enil. (** ** Integer logical negation *) @@ -72,8 +72,8 @@ Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) | _ => Eop (Oaddimm n) (e ::: Enil) end. @@ -501,6 +501,6 @@ Nondetfunction builtin_arg (e: expr) := | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) => - BA_loadglobal chunk id (Int.add ofs ofs1) + BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1)) | _ => BA e end. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 297e1f64..e520b3cf 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -26,6 +26,7 @@ Require Import CminorSel. Require Import SelectOp. Open Local Scope cminorsel_scope. +Local Transparent Archi.ptr64. (** * Useful lemmas and tactics *) @@ -123,7 +124,7 @@ Qed. Theorem eval_addrstack: forall le ofs, - exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v. + exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v. Proof. intros. unfold addrstack. econstructor; split. EvalOp. simpl; eauto. @@ -147,11 +148,11 @@ Proof. red; unfold addimm; intros until x. predSpec Int.eq Int.eq_spec n Int.zero. subst n. intros. exists x; split; auto. - destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. + destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Ptrofs.add_zero. auto. case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. - rewrite Val.add_assoc. rewrite Int.add_commut. auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Ptrofs.add_commut; auto. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. Qed. @@ -856,12 +857,12 @@ Proof. destruct (can_use_Aindexed2shift chunk); simpl. exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence. exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor. - simpl. rewrite Int.add_zero; auto. + simpl. rewrite Ptrofs.add_zero; auto. destruct (can_use_Aindexed2 chunk); simpl. exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence. exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor. - simpl. rewrite Int.add_zero; auto. - exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto. + simpl. rewrite Ptrofs.add_zero; auto. + exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. Theorem eval_builtin_arg: @@ -876,7 +877,7 @@ Proof. - simpl in H5. inv H5. constructor. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. -- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address in H6. +- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address_32 in H6 by auto. inv H6. constructor; auto. - constructor; auto. Qed. diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index 64a34329..e19ddd6d 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -183,18 +183,18 @@ Ltac InvHyps := Theorem eval_static_addressing_sound: forall addr vargs vres aargs, - eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres -> + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres -> list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_addressing addr aargs). Proof. unfold eval_addressing, eval_static_addressing; intros; destruct addr; InvHyps; eauto with va. - rewrite Int.add_zero_l; auto with va. + rewrite Ptrofs.add_zero_l; auto with va. Qed. Theorem eval_static_operation_sound: forall op vargs m vres aargs, - eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres -> + eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_operation op aargs). Proof. @@ -202,7 +202,7 @@ Proof. destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. destruct (propagate_float_constants tt); constructor. - rewrite Int.add_zero_l; eauto with va. + rewrite Ptrofs.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. Qed. -- cgit