From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 86 ++++++------ arm/Asmgen.v | 32 +++-- arm/Asmgenproof.v | 79 ++++++----- arm/Asmgenproof1.v | 44 ++++--- arm/ConstpropOp.vp | 4 + arm/ConstpropOpproof.v | 5 +- arm/Machregs.v | 105 +++++++++++---- arm/Machregsaux.ml | 9 +- arm/Op.v | 45 +++++++ arm/PrintAsm.ml | 161 ++++++++++++---------- arm/PrintOp.ml | 4 + arm/SelectOp.vp | 6 + arm/SelectOpproof.v | 22 +++- arm/linux/Conventions1.v | 337 ++++++++++++++++------------------------------- arm/linux/Stacklayout.v | 83 +++++------- 15 files changed, 540 insertions(+), 482 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index cad71884..60dae473 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -141,6 +141,7 @@ Inductive instruction : Type := | Pldrh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) | Pldrsb: ireg -> ireg -> shift_addr -> instruction (**r signed int8 load *) | Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) + | Pmla: ireg -> ireg -> ireg -> ireg -> instruction (**r integer multiply-add *) | Pmov: ireg -> shift_op -> instruction (**r integer move *) | Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *) | Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *) @@ -180,7 +181,7 @@ Inductive instruction : Type := | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) - | Pbuiltin: external_function -> list preg -> preg -> instruction (**r built-in function *) + | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *) | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *) with annot_param : Type := @@ -261,6 +262,14 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset := | r :: l' => undef_regs l' (rs#r <- Vundef) end. +(** Assigning multiple registers *) + +Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := + match rl, vl with + | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1) + | _, _ => rs + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -461,6 +470,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out exec_load Mint8signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pldrsh r1 r2 sa => exec_load Mint16signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pmla r1 r2 r3 r4 => + Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m | Pmov r1 so => Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m | Pmovc bit r1 so => @@ -522,9 +533,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfuitod r1 r2 => Next (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofintu rs#r2)))) m | Pftosizd r1 r2 => - Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m + Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m | Pftouizd r1 r2 => - Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m + Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m | Pfcvtsd r1 r2 => Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m | Pfldd r1 r2 n => @@ -535,7 +546,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with - | Next rs' m' => Next (rs'#FR7 <- Vundef) m' + | Next rs' m' => Next (rs'#FR6 <- Vundef) m' | Stuck => Stuck end (* Pseudo-instructions *) @@ -544,7 +555,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out let sp := (Vptr stk Int.zero) in match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with | None => Stuck - | Some m2 => Next (nextinstr (rs #IR10 <- (rs#IR13) #IR13 <- sp)) m2 + | 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 @@ -585,37 +596,36 @@ Definition preg_of (r: mreg) : preg := match r with | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 - | R8 => IR8 | R9 => IR9 | R11 => IR11 - | IT1 => IR10 | IT2 => IR12 + | R8 => IR8 | R9 => IR9 | R10 => IR10 | R11 => IR11 + | R12 => IR12 | F0 => FR0 | F1 => FR1 | F2 => FR2 | F3 => FR3 - | F4 => FR4 | F5 => FR5 + | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7 | F8 => FR8 | F9 => FR9 | F10 => FR10 | F11 => FR11 | F12 => FR12 | F13 => FR13 | F14 => FR14 | F15 => FR15 - | FT1 => FR6 | FT2 => FR7 end. (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use ARM registers instead of locations. *) +Definition chunk_of_type (ty: typ) := + match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end. + Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := | extcall_arg_reg: forall r, extcall_arg rs m (R r) (rs (preg_of r)) - | extcall_arg_int_stack: forall ofs bofs v, - bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> - Mem.loadv Mint32 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> - extcall_arg rs m (S (Outgoing ofs Tint)) v - | extcall_arg_float_stack: forall ofs bofs v, + | extcall_arg_stack: forall ofs ty bofs v, bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> - Mem.loadv Mfloat64al32 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> - extcall_arg rs m (S (Outgoing ofs Tfloat)) v. + Mem.loadv (chunk_of_type ty) m + (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> + extcall_arg rs m (S Outgoing ofs ty) v. Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := list_forall2 (extcall_arg rs m) (loc_arguments sg) args. -Definition loc_external_result (sg: signature) : preg := - preg_of (loc_result sg). +Definition loc_external_result (sg: signature) : list preg := + map preg_of (loc_result sg). (** Extract the values of the arguments of an annotation. *) @@ -645,28 +655,30 @@ Inductive step: state -> trace -> state -> Prop := 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 t v m', + forall b ofs f ef args res rs m t vl 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 (Pbuiltin ef args res) -> - external_call ef ge (map rs args) m t v m' -> - step (State rs m) t (State (nextinstr(rs # res <- v)) m') + external_call' ef ge (map rs args) m t vl m' -> + rs' = nextinstr + (set_regs res vl + (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + step (State rs m) t (State rs' m') | exec_step_annot: forall b ofs f ef args rs m vargs t v m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) (fn_code f) = Some (Pannot ef args) -> annot_arguments rs m args vargs -> - external_call ef ge vargs m t v m' -> + external_call' ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - external_call ef ge args m t res m' -> + external_call' ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (rs#(loc_external_result (ef_sig ef)) <- res - #PC <- (rs IR14)) -> + rs' = (set_regs (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) -> step (State rs m) t (State rs' m'). End RELSEM. @@ -734,21 +746,21 @@ Ltac Equalities := discriminate. discriminate. inv H11. - exploit external_call_determ. eexact H4. eexact H11. intros [A B]. + exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. - exploit external_call_determ. eexact H3. eexact H8. intros [A B]. + exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. (* trace length *) red; intros; inv H; simpl. omega. - eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. + inv H3; eapply external_call_trace_length; eauto. + inv H4; eapply external_call_trace_length; eauto. + inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. (* final no step *) @@ -768,15 +780,3 @@ Definition data_preg (r: preg) : bool := | PC => false end. -Definition nontemp_preg (r: preg) : bool := - match r with - | IR IR14 => false - | IR IR10 => false - | IR IR12 => false - | IR _ => true - | FR FR6 => false - | FR FR7 => false - | FR _ => true - | CR _ => false - | PC => false - end. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index d158c77b..1ff28d94 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -290,9 +290,15 @@ Definition transl_op OK (rsubimm r r1 n k) | Omul, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (if ireg_eq r r1 || ireg_eq r r2 - then Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k - else Pmul r r1 r2 :: k) + OK (if negb (ireg_eq r r1) then Pmul r r1 r2 :: k + else if negb (ireg_eq r r2) then Pmul r r2 r1 :: k + else Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k) + | Omla, a1 :: a2 :: a3 :: nil => + do r <- ireg_of res; do r1 <- ireg_of a1; + do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (if negb (ireg_eq r r1) then Pmla r r1 r2 r3 :: k + else if negb (ireg_eq r r2) then Pmla r r2 r1 r3 :: k + else Pmla IR14 r1 r2 r3 :: Pmov r (SOreg IR14) :: k) | Odiv, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Psdiv r r1 r2 :: k) @@ -420,6 +426,7 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := match ty with | Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k) | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k) + | Tlong => Error (msg "Asmgen.loadind") end. Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := @@ -432,6 +439,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := match ty with | Tint => do r <- ireg_of src; OK (storeind_int r base ofs k) | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k) + | Tlong => Error (msg "Asmgen.storeind") end. (** Translation of memory accesses *) @@ -512,6 +520,8 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pflds mk_immed_mem_float dst addr args k | Mfloat64 | Mfloat64al32 => transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k + | Mint64 => + Error (msg "Asmgen.transl_load") end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -531,6 +541,8 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pfsts mk_immed_mem_float src addr args k | Mfloat64 | Mfloat64al32 => transl_memory_access_float Pfstd mk_immed_mem_float src addr args k + | Mint64 => + Error (msg "Asmgen.transl_store") end. (** Translation of arguments to annotations *) @@ -544,17 +556,17 @@ Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) - (r10_is_parent: bool) (k: code) := + (r12_is_parent: bool) (k: code) := match i with | Mgetstack ofs ty dst => loadind IR13 ofs ty dst k | Msetstack src ofs ty => storeind src IR13 ofs ty k | Mgetparam ofs ty dst => - do c <- loadind IR10 ofs ty dst k; - OK (if r10_is_parent + do c <- loadind IR12 ofs ty dst k; + OK (if r12_is_parent then c - else loadind_int IR13 f.(fn_link_ofs) IR10 c) + else loadind_int IR13 f.(fn_link_ofs) IR12 c) | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -573,7 +585,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14 (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k)) | Mbuiltin ef args res => - OK (Pbuiltin ef (map preg_of args) (preg_of res) :: k) + OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => OK (Pannot ef (map transl_annot_param args) :: k) | Mlabel lbl => @@ -596,8 +608,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before - | Mgetparam ofs ty dst => negb (mreg_eq dst IT1) - | Mop Omove args res => before && negb (mreg_eq res IT1) + | Mgetparam ofs ty dst => negb (mreg_eq dst R12) + | Mop Omove args res => before && negb (mreg_eq res R12) | _ => false end. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 986d4746..aede0da4 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -264,7 +264,8 @@ Proof. Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. - destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel. + destruct (negb (ireg_eq x x0)). TailNoLabel. destruct (negb (ireg_eq x x1)); TailNoLabel. + destruct (negb (ireg_eq x x0)). TailNoLabel. destruct (negb (ireg_eq x x1)); TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. Qed. @@ -420,7 +421,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop := (MEXT: Mem.extends m m') (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) (AG: agree ms sp rs) - (DXP: ep = true -> rs#IR10 = parent_sp s), + (DXP: ep = true -> rs#IR12 = parent_sp s), match_states (Mach.State s fb sp c ms m) (Asm.State rs m') | match_states_call: @@ -451,7 +452,7 @@ Lemma exec_straight_steps: exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (it1_is_parent ep i = true -> rs2#IR10 = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#IR12 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. @@ -515,9 +516,9 @@ Definition measure (s: Mach.state) : nat := | Mach.Returnstate _ _ _ => 1%nat end. -Remark preg_of_not_R10: forall r, negb (mreg_eq r IT1) = true -> IR IR10 <> preg_of r. +Remark preg_of_not_R12: forall r, negb (mreg_eq r R12) = true -> IR IR12 <> preg_of r. Proof. - intros. change (IR IR10) with (preg_of IT1). red; intros. + intros. change (IR IR12) with (preg_of R12). red; intros. exploit preg_of_injective; eauto. intros; subst r. unfold proj_sumbool in H; rewrite dec_eq_true in H; discriminate. Qed. @@ -555,7 +556,7 @@ Proof. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. exists rs'; split. eauto. - split. change (undef_setstack rs) with rs. apply agree_exten with rs0; auto with asmgen. + split. change (Mach.undef_regs (destroyed_by_op Omove) rs) with rs. apply agree_exten with rs0; auto with asmgen. simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) @@ -569,24 +570,24 @@ Proof. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. destruct ep; monadInv TR. -(* R10 contains parent *) +(* R12 contains parent *) exploit loadind_correct. eexact EQ. instantiate (2 := rs0). rewrite DXP; eauto. intros [rs1 [P [Q R]]]. exists rs1; split. eauto. split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. simpl; intros. rewrite R; auto with asmgen. - apply preg_of_not_R10; auto. + apply preg_of_not_R12; auto. (* GPR11 does not contain parent *) - exploit loadind_int_correct. eexact A. instantiate (1 := IR10). intros [rs1 [P [Q R]]]. + exploit loadind_int_correct. eexact A. instantiate (1 := IR12). intros [rs1 [P [Q R]]]. exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]]. exists rs2; split. eapply exec_straight_trans; eauto. split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. - instantiate (1 := rs1#IR10 <- (rs2#IR10)). intros. + instantiate (1 := rs1#IR12 <- (rs2#IR12)). intros. rewrite Pregmap.gso; auto with asmgen. - congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR10). congruence. auto with asmgen. + congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen. simpl; intros. rewrite U; auto with asmgen. - apply preg_of_not_R10; auto. + apply preg_of_not_R12; auto. - (* Mop *) assert (eval_operation tge sp op rs##args m = Some v). @@ -597,12 +598,9 @@ Opaque loadind. exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto). exists rs2; split. eauto. split. - assert (agree (Regmap.set res v (undef_temps rs)) sp rs2). - eapply agree_set_undef_mreg; eauto with asmgen. - unfold undef_op; destruct op; auto. - change (undef_move rs) with rs. eapply agree_set_mreg; eauto. + eapply agree_set_undef_mreg; eauto with asmgen. simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. - rewrite R; auto. apply preg_of_not_R10; auto. + rewrite R; auto. apply preg_of_not_R12; auto. exact I. - (* Mload *) assert (eval_addressing tge sp addr rs##args = Some a). @@ -627,7 +625,7 @@ Opaque loadind. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. - split. eapply agree_exten_temps; eauto. + split. eapply agree_undef_regs; eauto. simpl; congruence. - (* Mcall *) @@ -695,7 +693,7 @@ 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. rewrite A. + simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. @@ -741,19 +739,21 @@ Opaque loadind. inv AT. monadInv H3. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H2); intro NOOV. - exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. + eauto. econstructor; eauto. - Simpl. rewrite <- H0. simpl. econstructor; eauto. + Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - rewrite Pregmap.gss. auto. - intros. Simpl. + apply preg_notin_charact. auto with asmgen. + apply preg_notin_charact. auto with asmgen. + apply agree_nextinstr. eapply agree_set_mregs; auto. + eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. - (* Mannot *) @@ -761,12 +761,12 @@ Opaque loadind. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends'; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. @@ -796,7 +796,7 @@ Opaque loadind. destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. rewrite EC in B. econstructor; econstructor; econstructor; split. eexact A. - split. eapply agree_exten_temps; eauto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. simpl. rewrite B. reflexivity. - (* Mcond false *) @@ -807,7 +807,7 @@ Opaque loadind. econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite B. reflexivity. auto. - split. eapply agree_exten_temps; eauto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. intros; Simpl. simpl. congruence. @@ -827,7 +827,7 @@ Opaque loadind. eapply find_instr_tail; eauto. simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. - eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. + eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl. congruence. - (* Mreturn *) @@ -887,7 +887,7 @@ Opaque loadind. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. (* Execution of function prologue *) - set (rs2 := nextinstr (rs0#IR10 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). + set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). set (rs3 := nextinstr rs2). assert (EXEC_PROLOGUE: exec_straight tge x @@ -896,7 +896,7 @@ Opaque loadind. rewrite <- H5 at 2; unfold fn_code. 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 Mach.chunk_of_type 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. @@ -911,7 +911,7 @@ Opaque loadind. unfold rs3, rs2. apply agree_nextinstr. apply agree_nextinstr. eapply agree_change_sp. - apply agree_exten_temps with rs0; eauto. + apply agree_undef_regs with rs0; eauto. intros. Simpl. congruence. - (* external function *) @@ -919,16 +919,15 @@ Opaque loadind. intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. intros [args' [C D]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends'; eauto. intros [res' [m2' [P [Q [R S]]]]]. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - eapply agree_set_mreg; eauto. - rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. - intros; Simpl. + apply agree_set_other; auto with asmgen. + eapply agree_set_mregs; eauto. - (* return *) inv STACKS. simpl in *. @@ -962,8 +961,8 @@ Lemma transf_final_states: Proof. intros. inv H0. inv H. inv STACKS. constructor. auto. - compute in H1. - generalize (preg_val _ _ _ R0 AG). rewrite H1. intros LD; inv LD. auto. + compute in H1. inv H1. + generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. Qed. Theorem transf_program_correct: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 06d6d179..e27ee80a 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -541,7 +541,8 @@ Ltac ArgsInv := | [ H: Error _ = OK _ |- _ ] => discriminate | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args | [ H: bind _ _ = OK _ |- _ ] => monadInv H - | [ H: assertion _ = OK _ |- _ ] => monadInv H + | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H + | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H end); subst; repeat (match goal with @@ -685,7 +686,7 @@ Lemma transl_op_correct_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 -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r. Proof. intros until v; intros TR EV NOCMP. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail). @@ -713,11 +714,21 @@ Proof. intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Omul *) - destruct (ireg_eq x x0 || ireg_eq x x1). + destruct (negb (ireg_eq x x0)). + TranslOpSimpl. + destruct (negb (ireg_eq x x1)). + rewrite Val.mul_commut. TranslOpSimpl. econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. intuition Simpl. + (* Omla *) + destruct (negb (ireg_eq x x0)). TranslOpSimpl. + destruct (negb (ireg_eq x x1)). + rewrite Val.mul_commut. TranslOpSimpl. + econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + intuition Simpl. (* divs *) econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. intuition Simpl. @@ -767,10 +778,11 @@ Proof. intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. - intuition Simpl. +Transparent destroyed_by_op. + simpl. intuition Simpl. (* intuoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. - intuition Simpl. + simpl. intuition Simpl. (* floatofint *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. intuition Simpl. @@ -788,7 +800,7 @@ Lemma transl_op_correct: 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 -> rs'#r = rs#r. + /\ 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). @@ -878,7 +890,7 @@ Lemma transl_load_int_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros. monadInv H. erewrite ireg_of_eq by eauto. eapply transl_memory_access_correct; eauto. @@ -902,7 +914,7 @@ Lemma transl_load_float_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros. monadInv H. erewrite freg_of_eq by eauto. eapply transl_memory_access_correct; eauto. @@ -913,7 +925,7 @@ Proof. Qed. Lemma transl_store_int_correct: - forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m', transl_memory_access_int mk_instr is_immed src addr args k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.storev chunk m a rs#(preg_of src) = Some m' -> @@ -922,7 +934,7 @@ Lemma transl_store_int_correct: exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r. Proof. intros. monadInv H. erewrite ireg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. @@ -937,7 +949,7 @@ Proof. Qed. Lemma transl_store_float_correct: - forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m', transl_memory_access_float mk_instr is_immed src addr args k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.storev chunk m a rs#(preg_of src) = Some m' -> @@ -946,7 +958,7 @@ Lemma transl_store_float_correct: exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r. Proof. intros. monadInv H. erewrite freg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. @@ -964,7 +976,7 @@ Lemma transl_load_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros. destruct chunk; simpl in H. eapply transl_load_int_correct; eauto. @@ -972,6 +984,7 @@ Proof. eapply transl_load_int_correct; eauto. eapply transl_load_int_correct; eauto. eapply transl_load_int_correct; eauto. + discriminate. eapply transl_load_float_correct; eauto. apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto. eapply transl_load_float_correct; eauto. @@ -984,7 +997,7 @@ Lemma transl_store_correct: Mem.storev chunk m a rs#(preg_of src) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r. Proof. intros. destruct chunk; simpl in H. - assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m'). @@ -996,11 +1009,12 @@ Proof. clear H1. eapply transl_store_int_correct; eauto. - eapply transl_store_int_correct; eauto. - eapply transl_store_int_correct; eauto. +- discriminate. - unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *. eapply transl_memory_access_correct; eauto. intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen. - rewrite H1. eauto. auto. intros. Simpl. + rewrite H1. eauto. auto. intros. Simpl. simpl; auto. - apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto. - eapply transl_store_float_correct; eauto. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 7e3217ee..9bf066b2 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -31,6 +31,7 @@ Inductive approx : Type := no compile-time information is available. *) | I: int -> approx (** A known integer value. *) | F: float -> approx (** A known floating-point value. *) + | L: int64 -> approx (** A know 64-bit integer value. *) | G: ident -> int -> approx (** The value is the address of the given global symbol plus the given integer offset. *) @@ -145,6 +146,9 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1 | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown | Ofloatofintu, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofintu n1) else Unknown + | Omakelong, I n1 :: I n2 :: nil => L(Int64.ofwords n1 n2) + | Olowlong, L n :: nil => I(Int64.loword n) + | Ohighlong, L n :: nil => I(Int64.hiword n) | Ocmp c, vl => eval_static_condition_val c vl | _, _ => Unknown end. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index c7de86d9..687e08f0 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -45,9 +45,10 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | Unknown => True | I p => v = Vint p | F p => v = Vfloat p + | L p => v = Vlong p | G symb ofs => v = symbol_address ge symb ofs | S ofs => v = Val.add sp (Vint ofs) - | _ => False + | Novalue => False end. Inductive val_list_match_approx: list approx -> list val -> Prop := @@ -65,6 +66,8 @@ Ltac SimplVMA := simpl in H; (try subst v); SimplVMA | H: (val_match_approx (F _) ?v) |- _ => simpl in H; (try subst v); SimplVMA + | H: (val_match_approx (L _) ?v) |- _ => + simpl in H; (try subst v); SimplVMA | H: (val_match_approx (G _ _) ?v) |- _ => simpl in H; (try subst v); SimplVMA | H: (val_match_approx (S _) ?v) |- _ => diff --git a/arm/Machregs.v b/arm/Machregs.v index 317515c3..4906eb0b 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -13,6 +13,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Op. (** ** Machine registers *) @@ -21,43 +22,36 @@ Require Import AST. - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]). - Floating-point registers that can be allocated to RTL pseudo-registers ([Fxx]). -- Two integer registers, not allocatable, reserved as temporaries for - spilling and reloading ([ITx]). -- Two float registers, not allocatable, reserved as temporaries for - spilling and reloading ([FTx]). - The type [mreg] does not include special-purpose machine registers - such as the stack pointer and the condition codes. *) + The type [mreg] does not include reserved machine registers + such as the stack pointer, the link register, and the condition codes. *) Inductive mreg: Type := (** Allocatable integer regs *) | R0: mreg | R1: mreg | R2: mreg | R3: mreg | R4: mreg | R5: mreg | R6: mreg | R7: mreg - | R8: mreg | R9: mreg | R11: mreg + | R8: mreg | R9: mreg | R10: mreg | R11: mreg + | R12: mreg (** Allocatable double-precision float regs *) | F0: mreg | F1: mreg | F2: mreg | F3: mreg - | F4: mreg | F5: mreg + | F4: mreg | F5: mreg | F6: mreg | F7: mreg | F8: mreg | F9: mreg | F10: mreg | F11: mreg - | F12: mreg | F13: mreg | F14: mreg | F15: mreg - (** Integer temporaries *) - | IT1: mreg (* R10 *) | IT2: mreg (* R12 *) - (** Float temporaries *) - | FT1: mreg (* F6 *) | FT2: mreg (* F7 *). + | F12: mreg | F13: mreg | F14: mreg | F15: mreg. Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. +Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with | R0 => Tint | R1 => Tint | R2 => Tint | R3 => Tint | R4 => Tint | R5 => Tint | R6 => Tint | R7 => Tint - | R8 => Tint | R9 => Tint | R11 => Tint + | R8 => Tint | R9 => Tint | R10 => Tint | R11 => Tint + | R12 => Tint | F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat - | F4 => Tfloat| F5 => Tfloat + | F4 => Tfloat| F5 => Tfloat | F6 => Tfloat | F7 => Tfloat | F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat | F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat - | IT1 => Tint | IT2 => Tint - | FT1 => Tfloat | FT2 => Tfloat end. Open Scope positive_scope. @@ -69,13 +63,12 @@ Module IndexedMreg <: INDEXED_TYPE. match r with | R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 | R5 => 6 | R6 => 7 | R7 => 8 - | R8 => 9 | R9 => 10 | R11 => 11 - | F0 => 12 | F1 => 13 | F2 => 14 | F3 => 15 - | F4 => 16 | F5 => 17 - | F8 => 18 | F9 => 19 | F10 => 20 | F11 => 21 - | F12 => 22 | F13 => 23 | F14 => 24 | F15 => 25 - | IT1 => 26 | IT2 => 27 - | FT1 => 28 | FT2 => 29 + | R8 => 9 | R9 => 10 | R10 => 11 | R11 => 12 + | R12 => 13 + | F0 => 14 | F1 => 15 | F2 => 16 | F3 => 17 + | F4 => 18 | F5 => 19 | F6 => 20 | F7 => 21 + | F8 => 22 | F9 => 23 | F10 => 24 | F11 => 25 + | F12 => 26 | F13 => 27 | F14 => 28 | F15 => 29 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -84,3 +77,67 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. +(** ** Destroyed registers, preferred registers *) + +Definition destroyed_by_op (op: operation): list mreg := + match op with + | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil + | Ointoffloat | Ointuoffloat => F6 :: nil + | _ => nil + end. + +Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg := + nil. + +Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := + match chunk with + | Mfloat32 => F6 :: nil + | _ => nil + end. + +Definition destroyed_by_cond (cond: condition): list mreg := + nil. + +Definition destroyed_by_jumptable: list mreg := + nil. + +Definition destroyed_by_builtin (ef: external_function): list mreg := + match ef with + | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil + | _ => R12 :: F6 :: nil + end. + +Definition destroyed_at_function_entry: list mreg := + R12 :: nil. + +Definition temp_for_parent_frame: mreg := + R12. + +Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := + match op with + | Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0) + | _ => (nil, None) + end. + +Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) := + match ef with + | EF_memcpy sz al => + if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil) + | _ => (nil, nil) + end. + +Global Opaque + destroyed_by_op destroyed_by_load destroyed_by_store + destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_function_entry temp_for_parent_frame + mregs_for_operation mregs_for_builtin. + +(** Two-address operations. Return [true] if the first argument and + the result must be in the same location *and* are unconstrained + by [mregs_for_operation]. There are none for ARM. *) + +Definition two_address_op (op: operation) : bool := + false. + +Global Opaque two_address_op. + diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml index 642437eb..5486c4b4 100644 --- a/arm/Machregsaux.ml +++ b/arm/Machregsaux.ml @@ -17,13 +17,12 @@ open Machregs let register_names = [ ("R0", R0); ("R1", R1); ("R2", R2); ("R3", R3); ("R4", R4); ("R5", R5); ("R6", R6); ("R7", R7); - ("R8", R8); ("R9", R9); ("R11", R11); + ("R8", R8); ("R9", R9); ("R10", R10); ("R11", R11); + ("R12", R12); ("F0", F0); ("F1", F1); ("F2", F2); ("F3", F3); - ("F4", F4); ("F5", F5); + ("F4", F4); ("F5", F5); ("F6", F6); ("F7", F7); ("F8", F8); ("F9", F9); ("F10", F10); ("F11", F11); - ("F12", F12);("F13", F13);("F14", F14); ("F15", F15); - ("R10", IT1); ("R12", IT2); - ("F6", FT1); ("F7", FT2) + ("F12", F12);("F13", F13);("F14", F14); ("F15", F15) ] let name_of_register r = diff --git a/arm/Op.v b/arm/Op.v index 06d07051..3dfea774 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -81,6 +81,7 @@ Inductive operation : Type := | Orsubshift: shift -> operation (**r [rd = shifted r2 - r1] *) | Orsubimm: int -> operation (**r [rd = n - r1] *) | Omul: operation (**r [rd = r1 * r2] *) + | Omla: operation (**r [rd = r1 * r2 + r3] *) | Odiv: operation (**r [rd = r1 / r2] (signed) *) | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) | Oand: operation (**r [rd = r1 & r2] *) @@ -114,6 +115,10 @@ Inductive operation : Type := | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) +(*c Manipulating 64-bit integers: *) + | Omakelong: operation (**r [rd = r1 << 32 | r2] *) + | Olowlong: operation (**r [rd = low-word(r1)] *) + | Ohighlong: operation (**r [rd = high-word(r1)] *) (*c Boolean tests: *) | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) @@ -213,6 +218,7 @@ Definition eval_operation | Orsubshift s, v1 :: v2 :: nil => Some (Val.sub (eval_shift s v2) v1) | Orsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) + | Omla, v1 :: v2 :: v3 :: nil => Some (Val.add (Val.mul v1 v2) v3) | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 | Odivu, v1 :: v2 :: nil => Val.divu v1 v2 | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2) @@ -244,6 +250,9 @@ Definition eval_operation | Ointuoffloat, v1::nil => Val.intuoffloat v1 | Ofloatofint, v1::nil => Val.floatofint v1 | Ofloatofintu, v1::nil => Val.floatofintu v1 + | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) + | Olowlong, v1::nil => Some(Val.loword v1) + | Ohighlong, v1::nil => Some(Val.hiword v1) | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m)) | _, _ => None end. @@ -302,6 +311,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Orsubshift _ => (Tint :: Tint :: nil, Tint) | Orsubimm _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) + | Omla => (Tint :: Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) | Odivu => (Tint :: Tint :: nil, Tint) | Oand => (Tint :: Tint :: nil, Tint) @@ -333,6 +343,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ointuoffloat => (Tfloat :: nil, Tint) | Ofloatofint => (Tint :: nil, Tfloat) | Ofloatofintu => (Tint :: nil, Tfloat) + | Omakelong => (Tint :: Tint :: nil, Tlong) + | Olowlong => (Tlong :: nil, Tint) + | Ohighlong => (Tlong :: nil, Tint) | Ocmp c => (type_of_condition c, Tint) end. @@ -374,6 +387,7 @@ Proof with (try exact I). generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b0 b)... destruct v0... destruct v0; destruct v1... + destruct v0... destruct v1... destruct v2... destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2... @@ -406,6 +420,9 @@ Proof with (try exact I). destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2... destruct v0; simpl in H0; inv H0... destruct v0; simpl in H0; inv H0... + destruct v0; destruct v1... + destruct v0... + destruct v0... destruct (eval_condition c vl m)... destruct b... Qed. @@ -544,6 +561,29 @@ Proof. rewrite Val.add_assoc. simpl. 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 := + match addr with + | Aindexed n => Some(Aindexed (Int.add n delta)) + | Aindexed2 => None + | Aindexed2shift s => None + | Ainstack n => Some(Ainstack (Int.add n 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)). +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 @@ -787,6 +827,7 @@ Proof. apply (@Values.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. inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists. inv H4; inv H3; simpl in H1; inv H1. simpl. @@ -828,6 +869,10 @@ Proof. inv H4; simpl in *; inv H1. TrivialExists. inv H4; simpl in *; inv H1. TrivialExists. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + subst v1. destruct (eval_condition c vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 57782866..1bac7159 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -181,47 +181,11 @@ let emit_constants oc = symbol_labels; reset_constants () -(* Simulate instructions by calling helper functions *) - -let print_list_ireg oc l = - match l with - | [] -> assert false - | r1 :: rs -> ireg oc r1; List.iter (fun r -> fprintf oc ", %a" ireg r) rs - -let rec remove l r = - match l with - | [] -> [] - | hd :: tl -> if hd = r then remove tl r else hd :: remove tl r - -let call_helper oc fn dst arg1 arg2 = - (* Preserve caller-save registers r0...r3 except dst *) - let tosave = remove [IR0; IR1; IR2; IR3] dst in - fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave; - (* Copy arg1 to R0 and arg2 to R1 *) - let moves = - Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in - List.iter - (fun (s, d) -> - fprintf oc " mov %a, %a\n" ireg d ireg s) - moves; - (* Call the helper function *) - fprintf oc " bl %s\n" fn; - (* Move result to dst *) - begin match dst with - | IR0 -> () - | _ -> fprintf oc " mov %a, r0\n" ireg dst - end; - (* Restore the other caller-save registers *) - fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; - (* ... for a total of at most 7 instructions *) - 7 - (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers the temporaries - (IR10, IR12, IR14, FP2, FP4) + registers; preserve all registers except IR2, IR3, IR12 and FP6. *) (* Handling of annotations *) @@ -234,9 +198,9 @@ let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_val preg oc txt args; match args, res with - | IR src :: _, IR dst -> + | [IR src], [IR dst] -> if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) - | FR src :: _, FR dst -> + | [FR src], [FR dst] -> if dst = src then 0 else (fprintf oc " fcpy %a, %a\n" freg dst freg src; 1) | _, _ -> assert false @@ -265,16 +229,12 @@ let print_builtin_memcpy_small oc sz al src dst = let print_builtin_memcpy_big oc sz al src dst = assert (sz >= al); assert (sz mod al = 0); + assert (src = IR2); + assert (dst = IR3); let (load, store, chunksize) = if al >= 4 then ("ldr", "str", 4) else if al = 2 then ("ldrh", "strh", 2) else ("ldrb", "strb", 1) in - let tmp = - if src <> IR0 && dst <> IR0 then IR0 - else if src <> IR1 && dst <> IR1 then IR1 - else IR2 in - let tosave = List.sort compare [tmp;src;dst] in - fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave; begin match Asmgen.decompose_int (coqint_of_camlint (Int32.of_int (sz / chunksize))) with | [] -> assert false @@ -286,12 +246,11 @@ let print_builtin_memcpy_big oc sz al src dst = tl end; let lbl = new_label() in - fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg tmp ireg src chunksize; + fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize; fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14; - fprintf oc " %s %a, [%a], #%d\n" store ireg tmp ireg dst chunksize; + fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize; fprintf oc " bne .L%d\n" lbl; - fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; - 9 + 8 let print_builtin_memcpy oc sz al args = let (dst, src) = @@ -308,20 +267,28 @@ let print_builtin_memcpy oc sz al args = let print_builtin_vload_common oc chunk args res = match chunk, args, res with - | Mint8unsigned, [IR addr], IR res -> + | Mint8unsigned, [IR addr], [IR res] -> fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint8signed, [IR addr], IR res -> + | Mint8signed, [IR addr], [IR res] -> fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16unsigned, [IR addr], IR res -> + | Mint16unsigned, [IR addr], [IR res] -> fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16signed, [IR addr], IR res -> + | Mint16signed, [IR addr], [IR res] -> fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint32, [IR addr], IR res -> + | Mint32, [IR addr], [IR res] -> fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mfloat32, [IR addr], FR res -> + | Mint64, [IR addr], [IR res1; IR res2] -> + if addr <> res2 then begin + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr; + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr + end else begin + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr; + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr + end; 2 + | Mfloat32, [IR addr], [FR res] -> fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 - | (Mfloat64 | Mfloat64al32), [IR addr], FR res -> + | (Mfloat64 | Mfloat64al32), [IR addr], [FR res] -> fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 | _ -> assert false @@ -346,6 +313,9 @@ let print_builtin_vstore_common oc chunk args = fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 | Mint32, [IR addr; IR src] -> fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint64, [IR addr; IR src1; IR src2] -> + fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr; + fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2 | Mfloat32, [IR addr; FR src] -> fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 @@ -386,22 +356,57 @@ let print_builtin_inline oc name args res = fprintf oc "%s begin %s\n" comment name; let n = match name, args, res with (* Integer arithmetic *) - | "__builtin_bswap", [IR a1], IR res -> + | "__builtin_bswap", [IR a1], [IR res] -> print_bswap oc a1 IR14 res; 4 - | "__builtin_cntlz", [IR a1], IR res -> + | "__builtin_cntlz", [IR a1], [IR res] -> fprintf oc " clz %a, %a\n" ireg res ireg a1; 1 (* Float arithmetic *) - | "__builtin_fabs", [FR a1], FR res -> + | "__builtin_fabs", [FR a1], [FR res] -> fprintf oc " fabsd %a, %a\n" freg res freg a1; 1 - | "__builtin_fsqrt", [FR a1], FR res -> + | "__builtin_fsqrt", [FR a1], [FR res] -> fprintf oc " fsqrtd %a, %a\n" freg res freg a1; 1 + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + if rl = ah then begin + fprintf oc " rsbs %a, %a, #0\n" ireg IR14 ireg al; + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2 + end + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + if rl = ah || rl = bh then begin + fprintf oc " adds %a, %a, %a\n" ireg IR14 ireg al ireg bl; + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 + end + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + if rl = ah || rl = bh then begin + fprintf oc " subs %a, %a, %a\n" ireg IR14 ireg al ireg bl; + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 + end + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + if rl = a || rh = a then begin + fprintf oc " mov %a, %a\n" ireg IR14 ireg a; + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg IR14 ireg b; 2 + end else begin + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 + end (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], IR res -> + | "__builtin_read16_reversed", [IR a1], [IR res] -> fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; fprintf oc " mov %a, %a, lsl #8\n" ireg IR14 ireg res; fprintf oc " and %a, %a, #0xFF00\n" ireg IR14 ireg IR14; fprintf oc " orr %a, %a, %a, lsr #8\n" ireg res ireg IR14 ireg res; 4 - | "__builtin_read32_reversed", [IR a1], IR res -> + | "__builtin_read32_reversed", [IR a1], [IR res] -> fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; print_bswap oc res IR14 res; 5 | "__builtin_write16_reversed", [IR a1; IR a2], _ -> @@ -410,9 +415,19 @@ let print_builtin_inline oc name args res = fprintf oc " orr %a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2; fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 4 | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = IR10 then IR12 else IR10 in - print_bswap oc a2 IR14 tmp; - fprintf oc " str %a, [%a, #0]\n" ireg tmp ireg a1; 5 + if a1 <> IR12 then begin + print_bswap oc a2 IR14 IR12; + fprintf oc " str %a, [%a, #0]\n" ireg IR12 ireg a1; 5 + end else begin + fprintf oc " mov %a, %a, lsr #24\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; + fprintf oc " mov %a, %a, lsr #16\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #1]\n" ireg IR14 ireg a1; + fprintf oc " mov %a, %a, lsr #8\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #2]\n" ireg IR14 ireg a1; + fprintf oc " str %a, [%a, #3]\n" ireg IR14 ireg a1; + 7 + end (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -516,6 +531,8 @@ let print_instruction oc = function fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Pldrsh(r1, r2, sa) -> fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pmla(r1, r2, r3, r4) -> + fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 | Pmov(r1, so) -> fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 1 | Pmovc(bit, r1, so) -> @@ -535,11 +552,13 @@ let print_instruction oc = function | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Psdiv(r1, r2, r3) -> - call_helper oc "__aeabi_idiv" r1 r2 r3 + assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + fprintf oc " bl __aeabi_idiv\n"; 1 | Psub(r1, r2, so) -> fprintf oc " sub %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 | Pudiv(r1, r2, r3) -> - call_helper oc "__aeabi_uidiv" r1 r2 r3 + assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + fprintf oc " bl __aeabi_uidiv\n"; 1 (* Floating-point coprocessor instructions *) | Pfcpyd(r1, r2) -> fprintf oc " fcpyd %a, %a\n" freg r1 freg r2; 1 @@ -593,14 +612,14 @@ let print_instruction oc = function fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> - fprintf oc " mov r10, sp\n"; + fprintf oc " mov r12, sp\n"; let ninstr = ref 0 in List.iter (fun n -> fprintf oc " sub sp, sp, #%a\n" coqint n; incr ninstr) (Asmgen.decompose_int sz); - fprintf oc " str r10, [sp, #%a]\n" coqint ofs; + fprintf oc " str r12, [sp, #%a]\n" coqint ofs; 2 + !ninstr | Pfreeframe(sz, ofs) -> if Asmgen.is_immed_arith sz @@ -620,7 +639,7 @@ let print_instruction oc = function List.iter (fun l -> fprintf oc " .word %a\n" print_label l) tbl; - 2 + List.length tbl + 3 + List.length tbl | Pbuiltin(ef, args, res) -> begin match ef with | EF_builtin(name, sg) -> @@ -713,6 +732,8 @@ let print_init oc = function fprintf oc " .short %ld\n" (camlint_of_coqint n) | Init_int32 n -> fprintf oc " .word %ld\n" (camlint_of_coqint n) + | Init_int64 n -> + fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) | Init_float32 n -> fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float.bits_of_single n)) comment (camlfloat_of_coqfloat n) diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index b5a8d754..eff39591 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -71,6 +71,7 @@ let print_operation reg pp = function | 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 + | Omla, [r1;r2;r3] -> fprintf pp "%a * %a + %a" reg r1 reg r2 reg r3 | Odiv, [r1;r2] -> fprintf pp "%a /s %a" reg r1 reg r2 | Odivu, [r1;r2] -> fprintf pp "%a /u %a" reg r1 reg r2 | Oand, [r1;r2] -> fprintf pp "%a & %a" reg r1 reg r2 @@ -100,6 +101,9 @@ let print_operation reg pp = function | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 + | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 + | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 + | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) | _ -> fprintf pp "" diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 22ef88d2..d81328b0 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -85,6 +85,8 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) + | Eop Omul (t1:::t2:::Enil), t3 => Eop Omla (t1:::t2:::t3:::Enil) + | t1, Eop Omul (t2:::t3:::Enil) => Eop Omla (t2:::t3:::t1:::Enil) | _, _ => Eop Oadd (e1:::e2:::Enil) end. @@ -185,6 +187,7 @@ Nondetfunction mul (e1: expr) (e2: expr) := Nondetfunction andimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else + if Int.eq n1 Int.mone then e2 else match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil @@ -215,6 +218,7 @@ Definition same_expr_pure (e1 e2: expr) := Nondetfunction orimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then e2 else + if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) @@ -407,6 +411,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool := | Mint16signed => true | Mint16unsigned => true | Mint32 => true + | Mint64 => false | Mfloat32 => false | Mfloat64 => false | Mfloat64al32 => false @@ -419,6 +424,7 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := | Mint16signed => false | Mint16unsigned => false | Mint32 => true + | Mint64 => false | Mfloat32 => false | Mfloat64 => false | Mfloat64al32 => false diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index ecc758fe..a71ead78 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -27,13 +27,6 @@ Require Import SelectOp. Open Local Scope cminorsel_scope. -Section CMCONSTR. - -Variable ge: genv. -Variable sp: val. -Variable e: env. -Variable m: mem. - (** * Useful lemmas and tactics *) (** The following are trivial lemmas and custom tactics that help @@ -81,6 +74,13 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) +Section CMCONSTR. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + (** We now show that the code generated by "smart constructor" functions such as [Selection.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] @@ -172,6 +172,8 @@ Proof. subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. subst. rewrite Val.add_commut. TrivialExists. subst. TrivialExists. + subst. TrivialExists. + subst. rewrite Val.add_commut. TrivialExists. TrivialExists. Qed. @@ -325,6 +327,9 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. exists (Vint Int.zero); split. EvalOp. destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto. + predSpec Int.eq Int.eq_spec n Int.mone. + intros. exists x; split; auto. + subst. destruct x; simpl; auto. rewrite Int.and_mone; auto. case (andimm_match a); intros. InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. @@ -352,6 +357,9 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.or_zero; auto. + predSpec Int.eq Int.eq_spec n Int.mone. + intros. exists (Vint Int.mone); split. EvalOp. + destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto. destruct (orimm_match a); intros; InvEval. TrivialExists. simpl. rewrite Int.or_commut; auto. subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v index f1ddc23a..1731eba2 100644 --- a/arm/linux/Conventions1.v +++ b/arm/linux/Conventions1.v @@ -32,34 +32,19 @@ Require Import Locations. *) Definition int_caller_save_regs := - R0 :: R1 :: R2 :: R3 :: nil. + R0 :: R1 :: R2 :: R3 :: R12 :: nil. Definition float_caller_save_regs := - F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: nil. + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. Definition int_callee_save_regs := - R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R11 :: nil. + R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil. Definition float_callee_save_regs := F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil. -Definition destroyed_at_call_regs := - int_caller_save_regs ++ float_caller_save_regs. - Definition destroyed_at_call := - List.map R destroyed_at_call_regs. - -Definition int_temporaries := IT1 :: IT2 :: nil. - -Definition float_temporaries := FT1 :: FT2 :: nil. - -Definition temporary_regs := int_temporaries ++ float_temporaries. - -Definition temporaries := List.map R temporary_regs. - -Definition destroyed_at_move_regs: list mreg := nil. - -Definition destroyed_at_move := List.map R destroyed_at_move_regs. + int_caller_save_regs ++ float_caller_save_regs. Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) @@ -72,7 +57,7 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) Definition index_int_callee_save (r: mreg) := match r with | R4 => 0 | R5 => 1 | R6 => 2 | R7 => 3 - | R8 => 4 | R9 => 5 | R11 => 6 + | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 | _ => -1 end. @@ -169,34 +154,27 @@ Qed. Lemma register_classification: forall r, - (In (R r) temporaries \/ In (R r) destroyed_at_call) \/ - (In r int_callee_save_regs \/ In r float_callee_save_regs). + In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs. Proof. destruct r; - try (left; left; simpl; OrEq); - try (left; right; simpl; OrEq); + try (left; simpl; OrEq); try (right; left; simpl; OrEq); try (right; right; simpl; OrEq). Qed. + Lemma int_callee_save_not_destroyed: forall r, - In (R r) temporaries \/ In (R r) destroyed_at_call -> - ~(In r int_callee_save_regs). + In r destroyed_at_call -> In r int_callee_save_regs -> False. Proof. - intros; red; intros. elim H. - generalize H0. simpl; ElimOrEq; NotOrEq. - generalize H0. simpl; ElimOrEq; NotOrEq. + intros. revert H0 H. simpl. ElimOrEq; NotOrEq. Qed. Lemma float_callee_save_not_destroyed: forall r, - In (R r) temporaries \/ In (R r) destroyed_at_call -> - ~(In r float_callee_save_regs). + In r destroyed_at_call -> In r float_callee_save_regs -> False. Proof. - intros; red; intros. elim H. - generalize H0. simpl; ElimOrEq; NotOrEq. - generalize H0. simpl; ElimOrEq; NotOrEq. + intros. revert H0 H. simpl. ElimOrEq; NotOrEq. Qed. Lemma int_callee_save_type: @@ -245,51 +223,33 @@ Qed. Calling conventions are largely arbitrary: they must respect the properties proved in this section (such as no overlapping between the locations of function arguments), but this leaves much liberty in choosing actual - locations. To ensure binary interoperability of code generated by our - compiler with libraries compiled by another ARM EABI compiler, we - implement *almost* the standard conventions defined in the ARM EABI application - binary interface, with two exceptions: -- Double-precision arguments and results are passed in VFP double registers - instead of pairs of integer registers. -- Single-precision arguments and results are passed as double-precision floats. -*) + locations. *) (** ** Location of function result *) (** The result value of a function is passed back to the caller in - registers [R0] or [F0], depending on the type of the returned value. - We treat a function without result as a function with one integer result. *) + registers [R0] or [F0] or [R0,R1], depending on the type of the + returned value. We treat a function without result as a function + with one integer result. *) -Definition loc_result (s: signature) : mreg := +Definition loc_result (s: signature) : list mreg := match s.(sig_res) with - | None => R0 - | Some Tint => R0 - | Some Tfloat => F0 + | None => R0 :: nil + | Some Tint => R0 :: nil + | Some Tfloat => F0 :: nil + | Some Tlong => R1 :: R0 :: nil end. -(** The result location has the type stated in the signature. *) - -Lemma loc_result_type: - forall sig, - mreg_type (loc_result sig) = - match sig.(sig_res) with None => Tint | Some ty => ty end. -Proof. - intros; unfold loc_result. - destruct (sig_res sig). - destruct t; reflexivity. - reflexivity. -Qed. - (** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), - In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. + forall (s: signature) (r: mreg), + In r (loc_result s) -> In r destroyed_at_call. Proof. - intros; unfold loc_result. left; - destruct (sig_res s). - destruct t; simpl; OrEq. - simpl; OrEq. + intros. + assert (r = R0 \/ r = R1 \/ r = F0). + unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition. + destruct H0 as [A | [A | A]]; subst r; simpl; OrEq. Qed. (** ** Location of function arguments *) @@ -299,34 +259,37 @@ Qed. - The first 2 float arguments are passed in registers [F0] and [F1]. - Each float argument passed in a float register ``consumes'' an aligned pair of two integer registers. +- Each long integer argument is passed in an aligned pair of two integer + registers. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively - assigned (1 word for an integer argument, 2 words for a float), + assigned (1 word for an integer argument, 2 words for a float or a long), starting at word offset 0. *) -Function ireg_param (n: Z) : mreg := +Definition ireg_param (n: Z) : mreg := if zeq n (-4) then R0 else if zeq n (-3) then R1 else if zeq n (-2) then R2 - else if zeq n (-1) then R3 - else R4. (**r should not happen *) - -Function freg_param (n: Z) : mreg := - if zeq n (-4) then F0 - else if zeq n (-3) then F1 - else if zeq n (-2) then F1 - else F2. (**r should not happen *) + else R3. +Definition freg_param (n: Z) : mreg := + if zeq n (-4) then F0 else F1. Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil | Tint :: tys => - (if zle 0 ofs then S (Outgoing ofs Tint) else R (ireg_param ofs)) + (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs)) :: loc_arguments_rec tys (ofs + 1) | Tfloat :: tys => - (if zle (-1) ofs then S (Outgoing (align ofs 2) Tfloat) else R (freg_param ofs)) - :: loc_arguments_rec tys (align ofs 2 + 2) + let ofs := align ofs 2 in + (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs)) + :: loc_arguments_rec tys (ofs + 2) + | Tlong :: tys => + let ofs := align ofs 2 in + (if zle 0 ofs then S Outgoing (ofs + 1) Tint else R (ireg_param (ofs + 1))) + :: (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs)) + :: loc_arguments_rec tys (ofs + 2) end. (** [loc_arguments s] returns the list of locations where to store arguments @@ -342,7 +305,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs | Tint :: tys => size_arguments_rec tys (ofs + 1) - | Tfloat :: tys => size_arguments_rec tys (align ofs 2 + 2) + | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2) end. Definition size_arguments (s: signature) : Z := @@ -353,109 +316,85 @@ Definition size_arguments (s: signature) : Z := Definition loc_argument_acceptable (l: loc) : Prop := match l with - | R r => ~(In l temporaries) - | S (Outgoing ofs ty) => ofs >= 0 + | R r => In r destroyed_at_call + | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong | _ => False end. +(* Lemma align_monotone: forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y. Proof. intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le. omega. omega. omega. Qed. +*) + +Remark ireg_param_caller_save: + forall n, In (ireg_param n) destroyed_at_call. +Proof. + unfold ireg_param; intros. + destruct (zeq n (-4)). simpl; auto. + destruct (zeq n (-3)). simpl; auto. + destruct (zeq n (-2)); simpl; auto. +Qed. + +Remark freg_param_caller_save: + forall n, In (freg_param n) destroyed_at_call. +Proof. + unfold freg_param; intros. destruct (zeq n (-4)); simpl; OrEq. +Qed. Remark loc_arguments_rec_charact: forall tyl ofs l, In l (loc_arguments_rec tyl ofs) -> match l with - | R r => - (exists n, ofs <= n < 0 /\ r = ireg_param n) - \/ (exists n, ofs <= n < -1 /\ r = freg_param n) - | S (Outgoing ofs' ty) => ofs' >= 0 /\ ofs' >= ofs - | S _ => False + | R r => In r destroyed_at_call + | S Outgoing ofs' ty => ofs' >= 0 /\ ofs <= ofs' /\ ty <> Tlong + | S _ _ _ => False end. Proof. induction tyl; simpl loc_arguments_rec; intros. elim H. - destruct a; elim H; intro. - subst l. destruct (zle 0 ofs). omega. - left. exists ofs; split; auto; omega. - generalize (IHtyl _ _ H0). - destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. - destruct s; auto; omega. - subst l. destruct (zle (-1) ofs). - split. apply Zle_ge. change 0 with (align (-1) 2). apply align_monotone; omega. - apply Zle_ge. apply align_le. omega. - right. exists ofs. intuition. + destruct a. +- (* Tint *) + destruct H. + subst l. destruct (zle 0 ofs). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tfloat *) assert (ofs <= align ofs 2) by (apply align_le; omega). - generalize (IHtyl _ _ H0). - destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. - destruct s; auto; omega. -Qed. - -Lemma loc_notin_in_diff: - forall l ll, - Loc.notin l ll <-> (forall l', In l' ll -> Loc.diff l l'). -Proof. - induction ll; simpl; intuition. subst l'. auto. -Qed. - -Remark loc_arguments_rec_notin_local: - forall tyl ofs ofs0 ty0, - Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs). -Proof. - intros. rewrite loc_notin_in_diff. intros. - exploit loc_arguments_rec_charact; eauto. - destruct l'; intros; simpl; auto. destruct s; auto; contradiction. + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. auto. congruence. + apply freg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tlong *) + assert (ofs <= align ofs 2) by (apply align_le; omega). + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. Qed. Lemma loc_arguments_acceptable: forall (s: signature) (r: loc), In r (loc_arguments s) -> loc_argument_acceptable r. Proof. - unfold loc_arguments; intros. + unfold loc_arguments, loc_argument_acceptable; intros. generalize (loc_arguments_rec_charact _ _ _ H). - destruct r; simpl. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (ireg_param n); intuition congruence. - functional induction (freg_param n); intuition congruence. - destruct s0; tauto. + destruct r; auto. + destruct sl; auto. + tauto. Qed. Hint Resolve loc_arguments_acceptable: locs. -(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *) - -Lemma loc_arguments_norepet: - forall (s: signature), Loc.norepet (loc_arguments s). -Proof. - unfold loc_arguments; intros. - assert (forall tyl ofs, -4 <= ofs -> Loc.norepet (loc_arguments_rec tyl ofs)). - induction tyl; simpl; intros. - constructor. - destruct a; constructor. - rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. - destruct (zle 0 ofs); destruct l'; simpl; auto. - destruct s0; intuition. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (ireg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. - functional induction (ireg_param ofs); functional induction (freg_param n); congruence || omegaContradiction. - apply IHtyl. omega. - rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. - destruct (zle (-1) ofs); destruct l'; simpl; auto. - destruct s0; intuition. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (freg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. - functional induction (freg_param ofs); functional induction (freg_param n); try (congruence || omegaContradiction). - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - apply IHtyl. assert (ofs <= align ofs 2) by (apply align_le; omega). omega. - apply H. omega. -Qed. - (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) Remark size_arguments_rec_above: @@ -468,6 +407,8 @@ Proof. apply Zle_trans with (ofs + 1); auto; omega. assert (ofs <= align ofs 2) by (apply align_le; omega). apply Zle_trans with (align ofs 2 + 2); auto; omega. + assert (ofs <= align ofs 2) by (apply align_le; omega). + apply Zle_trans with (align ofs 2 + 2); auto; omega. Qed. Lemma size_arguments_above: @@ -478,79 +419,35 @@ Qed. Lemma loc_arguments_bounded: forall (s: signature) (ofs: Z) (ty: typ), - In (S (Outgoing ofs ty)) (loc_arguments s) -> + In (S Outgoing ofs ty) (loc_arguments s) -> ofs + typesize ty <= size_arguments s. Proof. intros. assert (forall tyl ofs0, 0 <= ofs0 -> ofs0 <= Zmax 0 (size_arguments_rec tyl ofs0)). + { intros. generalize (size_arguments_rec_above tyl ofs0). intros. - rewrite Zmax_spec. rewrite zlt_false. auto. omega. + rewrite Zmax_spec. rewrite zlt_false. auto. omega. + } assert (forall tyl ofs0, - In (S (Outgoing ofs ty)) (loc_arguments_rec tyl ofs0) -> + In (S Outgoing ofs ty) (loc_arguments_rec tyl ofs0) -> ofs + typesize ty <= Zmax 0 (size_arguments_rec tyl ofs0)). - induction tyl; simpl; intros. - elim H1. - destruct a; elim H1; intros. - destruct (zle 0 ofs0); inv H2. apply H0. omega. auto. - destruct (zle (-1) ofs0); inv H2. apply H0. - assert (align (-1) 2 <= align ofs0 2). apply align_monotone. omega. auto. - change (align (-1) 2) with 0 in H2. omega. - auto. - + { + induction tyl; simpl; intros. + elim H1. + destruct a. + - (* Tint *) + destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. + - (* Tfloat *) + destruct H1; auto. destruct (zle 0 (align ofs0 2)); inv H1. apply H0. omega. + - (* Tlong *) + destruct H1. + destruct (zle 0 (align ofs0 2)); inv H1. + eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. + destruct H1; auto. + destruct (zle 0 (align ofs0 2)); inv H1. + eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. + } unfold size_arguments. apply H1. auto. Qed. - -(** Temporary registers do not overlap with argument locations. *) - -Lemma loc_arguments_not_temporaries: - forall sig, Loc.disjoint (loc_arguments sig) temporaries. -Proof. - intros; red; intros x1 x2 A B. - exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable. - destruct x1; intros. simpl. destruct x2; auto. intuition congruence. - destruct s; try contradiction. revert B. simpl. ElimOrEq; auto. -Qed. -Hint Resolve loc_arguments_not_temporaries: locs. - -(** Argument registers are caller-save. *) - -Lemma arguments_caller_save: - forall sig r, - In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call. -Proof. - unfold loc_arguments; intros. - destruct (loc_arguments_rec_charact _ _ _ H) as [[n [A B]] | [n [A B]]]; subst r. - functional induction (ireg_param n); simpl; auto. omegaContradiction. - functional induction (freg_param n); simpl; auto 10. -Qed. - -(** Argument locations agree in number with the function signature. *) - -Lemma loc_arguments_length: - forall sig, - List.length (loc_arguments sig) = List.length sig.(sig_args). -Proof. - assert (forall tyl ofs, List.length (loc_arguments_rec tyl ofs) = List.length tyl). - induction tyl; simpl; intros. - auto. - destruct a; simpl; decEq; auto. - - intros. unfold loc_arguments. auto. -Qed. - -(** Argument locations agree in types with the function signature. *) - -Lemma loc_arguments_type: - forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args). -Proof. - assert (forall tyl ofs, List.map Loc.type (loc_arguments_rec tyl ofs) = tyl). - induction tyl; simpl; intros. - auto. - destruct a; simpl; decEq; auto. - destruct (zle 0 ofs). auto. functional induction (ireg_param ofs); auto. - destruct (zle (-1) ofs). auto. functional induction (freg_param ofs); auto. - - intros. unfold loc_arguments. apply H. -Qed. diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v index d84da6ba..7694dcfe 100644 --- a/arm/linux/Stacklayout.v +++ b/arm/linux/Stacklayout.v @@ -18,11 +18,8 @@ Require Import Bounds. (** The general shape of activation records is as follows, from bottom (lowest offsets) to top: - Space for outgoing arguments to function calls. -- Local stack slots of integer type. +- Local stack slots. - Saved values of integer callee-save registers used by the function. -- One word of padding, if necessary to align the following data - on a 8-byte boundary. -- Local stack slots of float type. - Saved values of float callee-save registers used by the function. - Saved return address into caller. - Pointer to activation record of the caller. @@ -38,10 +35,9 @@ Record frame_env : Type := mk_frame_env { fe_size: Z; fe_ofs_link: Z; fe_ofs_retaddr: Z; - fe_ofs_int_local: Z; + fe_ofs_local: Z; fe_ofs_int_callee_save: Z; fe_num_int_callee_save: Z; - fe_ofs_float_local: Z; fe_ofs_float_callee_save: Z; fe_num_float_callee_save: Z; fe_stack_data: Z @@ -51,18 +47,17 @@ Record frame_env : Type := mk_frame_env { function. *) Definition make_env (b: bounds) := - let oil := 4 * b.(bound_outgoing) in (* integer locals *) - let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) + let ol := align (4 * b.(bound_outgoing)) 8 in (* locals *) + let oics := ol + 4 * b.(bound_local) in (* integer callee-saves *) let oendi := oics + 4 * b.(bound_int_callee_save) in - let ofl := align oendi 8 in (* float locals *) - let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) + let ofcs := align oendi 8 in (* float callee-saves *) let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *) let olink := ora + 4 in (* back link *) let ostkdata := olink + 4 in (* stack data *) let sz := align (ostkdata + b.(bound_stack_data)) 8 in - mk_frame_env sz olink ora - oil oics b.(bound_int_callee_save) - ofl ofcs b.(bound_float_callee_save) + mk_frame_env sz olink ora ol + oics b.(bound_int_callee_save) + ofcs b.(bound_float_callee_save) ostkdata. (** Separation property *) @@ -71,26 +66,24 @@ Remark frame_env_separated: forall b, let fe := make_env b in 0 <= fe_ofs_arg - /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local) - /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save) - /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local) - /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save) + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_local) + /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_ofs_int_callee_save) + /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_callee_save) /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_retaddr) /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_link) /\ fe.(fe_ofs_link) + 4 <= fe.(fe_stack_data) /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). Proof. intros. - generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). - generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 8 (refl_equal _)). + generalize (align_le (4 * bound_outgoing b) 8 (refl_equal)). + generalize (align_le (fe_ofs_int_callee_save fe + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). + generalize (align_le (fe_stack_data fe + b.(bound_stack_data)) 8 (refl_equal)). unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_int_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save, + fe_ofs_float_callee_save, fe_num_float_callee_save, fe_stack_data, fe_ofs_arg. intros. - generalize (bound_int_local_pos b); intro; - generalize (bound_float_local_pos b); intro; + generalize (bound_local_pos b); intro; generalize (bound_int_callee_save_pos b); intro; generalize (bound_float_callee_save_pos b); intro; generalize (bound_outgoing_pos b); intro; @@ -104,9 +97,8 @@ Remark frame_env_aligned: forall b, let fe := make_env b in (4 | fe.(fe_ofs_link)) - /\ (4 | fe.(fe_ofs_int_local)) + /\ (8 | fe.(fe_ofs_local)) /\ (4 | fe.(fe_ofs_int_callee_save)) - /\ (8 | fe.(fe_ofs_float_local)) /\ (8 | fe.(fe_ofs_float_callee_save)) /\ (4 | fe.(fe_ofs_retaddr)) /\ (8 | fe.(fe_stack_data)) @@ -114,30 +106,27 @@ Remark frame_env_aligned: Proof. intros. unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_int_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save, + fe_ofs_float_callee_save, fe_num_float_callee_save, fe_stack_data. set (x1 := 4 * bound_outgoing b). assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. - set (x2 := x1 + 4 * bound_int_local b). - assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. - set (x3 := x2 + 4 * bound_int_callee_save b). - set (x4 := align x3 8). - assert (8 | x4). unfold x4. apply align_divides. omega. - set (x5 := x4 + 8 * bound_float_local b). - assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. - set (x6 := x5 + 8 * bound_float_callee_save b). - assert (8 | x6). - unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. - assert (4 | x6). - apply Zdivides_trans with 8. exists 2; auto. auto. + set (x2 := align x1 8). + assert (8 | x2). apply align_divides. omega. + set (x3 := x2 + 4 * bound_local b). + assert (4 | x3). apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. + exists (bound_local b); ring. + set (x4 := align (x3 + 4 * bound_int_callee_save b) 8). + assert (8 | x4). apply align_divides. omega. + set (x5 := x4 + 8 * bound_float_callee_save b). + assert (8 | x5). apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + assert (4 | x5). apply Zdivides_trans with 8; auto. exists 2; auto. + set (x6 := x5 + 4). + assert (4 | x6). apply Zdivide_plus_r; auto. exists 1; auto. set (x7 := x6 + 4). - assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto. - set (x8 := x7 + 4). - assert (8 | x8). unfold x8, x7. replace (x6 + 4 + 4) with (x6 + 8) by omega. - apply Zdivide_plus_r; auto. exists 1; auto. - set (x9 := align (x8 + bound_stack_data b) 8). - assert (8 | x9). unfold x9; apply align_divides. omega. + assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega. + apply Zdivide_plus_r; auto. exists 1; auto. + set (x8 := align (x7 + bound_stack_data b) 8). + assert (8 | x8). apply align_divides. omega. tauto. Qed. -- cgit