diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Archi.v | 4 | ||||
| -rw-r--r-- | arm/Asm.v | 9 | ||||
| -rw-r--r-- | arm/AsmToJSON.ml | 2 | ||||
| -rw-r--r-- | arm/AsmToJSON.mli | 2 | ||||
| -rw-r--r-- | arm/Asmexpand.ml | 62 | ||||
| -rw-r--r-- | arm/Asmgen.v | 32 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 69 | ||||
| -rw-r--r-- | arm/Asmgenproof1.v | 39 | ||||
| -rw-r--r-- | arm/CBuiltins.ml | 9 | ||||
| -rw-r--r-- | arm/ConstpropOp.vp | 29 | ||||
| -rw-r--r-- | arm/ConstpropOpproof.v | 73 | ||||
| -rw-r--r-- | arm/Conventions1.v | 62 | ||||
| -rw-r--r-- | arm/Machregs.v | 2 | ||||
| -rw-r--r-- | arm/Op.v | 4 | ||||
| -rw-r--r-- | arm/Stacklayout.v | 73 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 58 | ||||
| -rw-r--r-- | arm/extractionMachdep.v | 4 |
17 files changed, 367 insertions, 166 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index 64afb3ec..353731e0 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -65,3 +65,7 @@ Global Opaque ptr64 big_endian splitlong Inductive abi_kind := Softfloat | Hardfloat. Parameter abi: abi_kind. + +(** Whether instructions added with Thumb2 are supported. True for ARMv6T2 + and above. *) +Parameter thumb2_support: bool. @@ -199,15 +199,16 @@ Inductive instruction : Type := | Pfsts: freg -> ireg -> int -> instruction (**r float32 store *) (* Pseudo-instructions *) - | 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 *) + | 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 -> 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) *) | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) + | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset debug directive *) | Pclz: ireg -> ireg -> instruction (**r count leading zeros. *) | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) | Prev: ireg -> ireg -> instruction (**r reverse bytes and reverse bits. *) @@ -757,6 +758,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | _ => Stuck end + | Pcfi_rel_offset ofs => + Next (nextinstr rs) m | Pbuiltin ef args res => Stuck (**r treated specially below *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 73706d3b..74c64180 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -16,3 +16,5 @@ let pp_program pp prog = Format.fprintf pp "null" + +let pp_mnemonics pp = () diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli index e4d9c39a..058a4e83 100644 --- a/arm/AsmToJSON.mli +++ b/arm/AsmToJSON.mli @@ -11,3 +11,5 @@ (* *********************************************************************) val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit + +val pp_mnemonics: Format.formatter -> unit diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index a32b0e8b..b65007df 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -46,18 +46,22 @@ let expand_movimm dst n = (fun n -> emit (Porr (dst,dst, SOimm n))) tl let expand_subimm dst src n = - match Asmgen.decompose_int n with - | [] -> assert false - | hd::tl -> - emit (Psub(dst,src,SOimm hd)); - List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl + if dst <> src || n <> _0 then begin + match Asmgen.decompose_int n with + | [] -> assert false + | hd::tl -> + emit (Psub(dst,src,SOimm hd)); + List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl + end let expand_addimm dst src n = - match Asmgen.decompose_int n with - | [] -> assert false - | hd::tl -> - emit (Padd (dst,src,SOimm hd)); - List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl + if dst <> src || n <> _0 then begin + match Asmgen.decompose_int n with + | [] -> assert false + | hd::tl -> + emit (Padd (dst,src,SOimm hd)); + List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl + end let expand_int64_arith conflict rl fn = if conflict then @@ -77,8 +81,8 @@ let expand_int64_arith conflict rl fn = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmov (dst,SOreg src)) @@ -410,12 +414,22 @@ let expand_instruction instr = | Pallocframe (sz, ofs) -> emit (Pmov (IR12,SOreg IR13)); if (is_current_function_variadic ()) then begin - emit (Ppush [IR0;IR1;IR2;IR3]); - emit (Pcfi_adjust _16); - end; - expand_subimm IR13 IR13 sz; - emit (Pcfi_adjust sz); - emit (Pstr (IR12,IR13,SOimm ofs)); + emit (Ppush [IR0;IR1;IR2;IR3]); + emit (Pcfi_adjust _16); + end; + let sz' = camlint_of_coqint sz in + let ofs' = camlint_of_coqint ofs in + if ofs' >= 4096l && sz' >= ofs' then begin + expand_subimm IR13 IR13 (coqint_of_camlint (Int32.sub sz' (Int32.add ofs' 4l))); + emit (Ppush [IR12]); + expand_subimm IR13 IR13 ofs; + emit (Pcfi_adjust sz); + end else begin + assert (ofs' < 4096l); + expand_subimm IR13 IR13 sz; + emit (Pcfi_adjust sz); + emit (Pstr (IR12,IR13,SOimm ofs)); + end; PrintAsmaux.current_function_stacksize := camlint_of_coqint sz | Pfreeframe (sz, ofs) -> let sz = @@ -424,7 +438,13 @@ let expand_instruction instr = else sz in if Asmgen.is_immed_arith sz then emit (Padd (IR13,IR13,SOimm sz)) - else emit (Pldr (IR13,IR13,SOimm ofs)) + else begin + if camlint_of_coqint ofs >= 4096l then begin + expand_addimm IR13 IR13 ofs; + emit (Pldr (IR13,IR13,SOimm _0)) + end else + emit (Pldr (IR13,IR13,SOimm ofs)); + end | Pbuiltin (ef,args,res) -> begin match ef with | EF_builtin (name,sg) -> @@ -433,8 +453,8 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_annot_val (txt,targ) -> - expand_annot_val txt targ args res + | EF_annot_val (kind,txt,targ) -> + expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args diff --git a/arm/Asmgen.v b/arm/Asmgen.v index e7a3b4fa..ed64e2f0 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -162,7 +162,7 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) (** Smart constructors for integer immediate arguments. *) -Definition loadimm_thumb (r: ireg) (n: int) (k: code) := +Definition loadimm_word (r: ireg) (n: int) (k: code) := let hi := Int.shru n (Int.repr 16) in if Int.eq hi Int.zero then Pmovw r n :: k @@ -177,8 +177,8 @@ Definition loadimm (r: ireg) (n: int) (k: code) := Pmov r (SOimm n) :: k else if Nat.leb l2 1%nat then Pmvn r (SOimm (Int.not n)) :: k - else if thumb tt then - loadimm_thumb r n k + else if Archi.thumb2_support then + loadimm_word r n k else if Nat.leb l1 l2 then iterate_op (Pmov r) (Porr r r) d1 k else @@ -365,14 +365,14 @@ Definition transl_op 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 + OK (if Archi.thumb2_support then Psbfx r r1 Int.zero (Int.repr 8) :: k else Pmov r (SOlsl r1 (Int.repr 24)) :: Pmov r (SOasr r (Int.repr 24)) :: k) | Ocast16signed, a1 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; - OK (if thumb tt then + OK (if Archi.thumb2_support then Psbfx r r1 Int.zero (Int.repr 16) :: k else Pmov r (SOlsl r1 (Int.repr 16)) :: @@ -602,6 +602,22 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : Error (msg "Asmgen.storeind") end. +(** This is a variant of [storeind] that is used to save the return address + at the beginning of a function. It uses [R12] instead of [R14] as + temporary register. *) + +Definition save_lr (ofs: ptrofs) (k: code) := + let n := Ptrofs.to_int ofs in + let n1 := mk_immed_mem_word n in + if Int.eq n n1 + then Pstr IR14 IR13 (SOimm n) :: k + else addimm IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k). + +Definition save_lr_preserves_R12 (ofs: ptrofs) : bool := + let n := Ptrofs.to_int ofs in + let n1 := mk_immed_mem_word n in + Int.eq n n1. + (** Translation of memory accesses *) Definition transl_memory_access @@ -787,10 +803,12 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - do c <- transl_code f f.(Mach.fn_code) true; + do c <- transl_code f f.(Mach.fn_code) + (save_lr_preserves_R12 f.(fn_retaddr_ofs)); OK (mkfunction f.(Mach.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SOimm (Ptrofs.to_int f.(fn_retaddr_ofs))) :: c)). + save_lr f.(fn_retaddr_ofs) + (Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)):: c))). Definition transf_function (f: Mach.function) : res Asm.function := do tf <- transl_function f; diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 09c20d5c..9e6b2c98 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -170,7 +170,7 @@ Proof. set (l2 := length (decompose_int (Int.not n))). destruct (Nat.leb l1 1%nat). TailNoLabel. destruct (Nat.leb l2 1%nat). TailNoLabel. - destruct (thumb tt). unfold loadimm_thumb. + destruct Archi.thumb2_support. unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. destruct (Nat.leb l1 l2); auto with labels. Qed. @@ -241,6 +241,15 @@ Proof. destruct ty, (preg_of src); inv H; TailNoLabel. Qed. +Remark save_lr_label: + forall ofs k, tail_nolabel k (save_lr ofs k). +Proof. + unfold save_lr; intros. + destruct (Int.eq (Ptrofs.to_int ofs) (mk_immed_mem_word (Ptrofs.to_int ofs))). + TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. +Qed. + Remark transl_cond_label: forall cond args k c, transl_cond cond args k = OK c -> tail_nolabel k c. Proof. @@ -255,8 +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 (thumb tt); TailNoLabel. - destruct (thumb tt); TailNoLabel. + destruct Archi.thumb2_support; TailNoLabel. + destruct Archi.thumb2_support; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. Qed. @@ -338,7 +347,7 @@ Lemma transl_find_label: end. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. - monadInv EQ. simpl. + monadInv EQ. simpl. erewrite tail_nolabel_find_label by (apply save_lr_label). simpl. eapply transl_code_label; eauto. Qed. @@ -382,7 +391,8 @@ Proof. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. - exists x; exists true; split; auto. repeat constructor. + exists x; exists (save_lr_preserves_R12 (fn_retaddr_ofs f0)); split; auto. + constructor. eapply is_tail_trans. 2: apply tail_nolabel_is_tail; apply save_lr_label. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -854,10 +864,13 @@ Opaque loadind. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. subst x0. monadInv EQ0. - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x0) in *. + set (ra_ofs := fn_retaddr_ofs f) in *. + set (ra_ofs' := Ptrofs.to_int ra_ofs) in *. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: + save_lr ra_ofs (Pcfi_rel_offset ra_ofs' :: x0)) in *. set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. @@ -865,32 +878,40 @@ Opaque loadind. intros [m3' [P Q]]. (* Execution of function prologue *) set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))). - set (rs3 := nextinstr rs2). + edestruct (save_lr_correct tge tf ra_ofs (Pcfi_rel_offset ra_ofs' :: x0) rs2) as (rs3 & X & Y & Z). + change (rs2 IR13) with sp. change (rs2 IR14) with (rs0 IR14). rewrite ATLR. eexact P. + set (rs4 := nextinstr rs3). assert (EXEC_PROLOGUE: exec_straight tge tf (fn_code tf) rs0 m' - x0 rs3 m3'). + x0 rs4 m3'). + { change (fn_code tf) with tfbody; unfold tfbody. - apply exec_straight_two with rs2 m2'. + eapply exec_straight_trans with (rs2 := rs2) (m2 := m2'). + apply exec_straight_one. unfold exec_instr. rewrite C. fold sp. 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 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. + auto. + eapply exec_straight_trans with (rs2 := rs3) (m2 := m3'). + eexact X. + apply exec_straight_one. + simpl; reflexivity. reflexivity. + } + (* After the function prologue is the code for the function body *) + exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + intros (ofsbody & U & V). + (* Conclusions *) + left; exists (State rs4 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. - econstructor; eauto. - change (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one). - rewrite ATPC. simpl. constructor; eauto. - eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. constructor. - unfold rs3, rs2. - apply agree_nextinstr. apply agree_nextinstr. + econstructor; eauto. rewrite U. econstructor; eauto. + apply agree_nextinstr. + apply agree_undef_regs2 with rs2. + apply agree_nextinstr. eapply agree_change_sp. apply agree_undef_regs with rs0; eauto. - intros. Simpl. congruence. + intros; Simpl. + congruence. + intros; apply Y; eauto with asmgen. - (* external function *) exploit functions_translated; eauto. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index eec531dc..c1015a8c 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -344,9 +344,9 @@ Proof. econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. split; intros; Simpl. } - destruct (thumb tt). + destruct Archi.thumb2_support. { (* movw / movt *) - unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero). + unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero). econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. econstructor; split. @@ -616,6 +616,37 @@ Proof. intros; Simpl. Qed. +(** Saving the link register *) + +Lemma save_lr_correct: + forall ofs k (rs: regset) m m', + Mem.storev Mint32 m (Val.offset_ptr rs#IR13 ofs) (rs#IR14) = Some m' -> + exists rs', + exec_straight ge fn (save_lr ofs k) rs m k rs' m' + /\ (forall r, if_preg r = true -> r <> IR12 -> rs'#r = rs#r) + /\ (save_lr_preserves_R12 ofs = true -> rs'#IR12 = rs#IR12). +Proof. + intros; unfold save_lr, save_lr_preserves_R12. + set (n := Ptrofs.to_int ofs). set (n1 := mk_immed_mem_word n). + assert (EQ: Val.offset_ptr rs#IR13 ofs = Val.add rs#IR13 (Vint n)). + { destruct rs#IR13; try discriminate. simpl. f_equal; f_equal. unfold n; symmetry; auto with ptrofs. } + destruct (Int.eq n n1). +- econstructor; split. apply exec_straight_one. simpl; unfold exec_store. rewrite <- EQ, H; reflexivity. auto. + split. intros; Simpl. intros; Simpl. +- destruct (addimm_correct IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k) rs m) + as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl; unfold exec_store. + rewrite B. rewrite Val.add_assoc. simpl. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg n1)). + rewrite Int.add_neg_zero. rewrite Int.add_zero. + rewrite <- EQ. rewrite C by eauto with asmgen. rewrite H. reflexivity. + auto. + split. intros; Simpl. congruence. +Qed. + (** Translation of shift immediates *) Lemma transl_shift_correct: @@ -1162,7 +1193,7 @@ Proof. (* Oaddrstack *) contradiction. (* Ocast8signed *) - destruct (thumb tt). + destruct Archi.thumb2_support. econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity. set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))). @@ -1175,7 +1206,7 @@ Proof. f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto. intros. unfold rs2, rs1; Simpl. (* Ocast16signed *) - destruct (thumb tt). + destruct Archi.thumb2_support. econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity. set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))). diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index 2015607a..ec4f4aaa 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -23,12 +23,6 @@ let builtins = { ]; Builtins.functions = [ (* Integer arithmetic *) - "__builtin_bswap", - (TInt(IUInt, []), [TInt(IUInt, [])], false); - "__builtin_bswap32", - (TInt(IUInt, []), [TInt(IUInt, [])], false); - "__builtin_bswap16", - (TInt(IUShort, []), [TInt(IUShort, [])], false); "__builtin_clz", (TInt(IInt, []), [TInt(IUInt, [])], false); "__builtin_clzl", @@ -41,9 +35,6 @@ let builtins = { (TInt(IInt, []), [TInt(IULong, [])], false); "__builtin_ctzll", (TInt(IInt, []), [TInt(IULongLong, [])], false); - (* Float arithmetic *) - "__builtin_fsqrt", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Memory accesses *) "__builtin_read16_reversed", (TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false); diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index cb7a73eb..f94606b0 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -206,6 +206,30 @@ Definition make_cast8signed (r: reg) (a: aval) := Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). +Definition make_mla_mulimm (n1: int) (r1 r2 r3: reg) := + if Int.eq n1 Int.zero then + (Omove, r3 :: nil) + else if Int.eq n1 Int.one then + (Oadd, r2 :: r3 :: nil) + else + (Omla, r1 :: r2 :: r3 :: nil). + +Definition make_mla_addimm (n3: int) (r1 r2 r3: reg) := + if Int.eq n3 Int.zero then + (Omul, r1 :: r2 :: nil) + else + (Omla, r1 :: r2 :: r3 :: nil). + +Definition make_mla_bothimm (n1 n3: int) (r1 r2 r3: reg) := + if Int.eq n1 Int.zero then + (Ointconst n3, nil) + else if Int.eq n1 Int.one then + make_addimm n3 r2 + else if Int.eq n3 Int.zero then + make_mulimm n1 r2 r1 + else + (Omla, r1 :: r2 :: r3 :: nil). + Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with @@ -220,6 +244,11 @@ Nondetfunction op_strength_reduction | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil) | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1 | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2 + | Omla, r1 :: r2 :: r3 :: nil, I n1 :: v2 :: I n3 :: nil => make_mla_bothimm n1 n3 r1 r2 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: I n2 :: I n3 :: nil => make_mla_bothimm n2 n3 r2 r1 r3 + | Omla, r1 :: r2 :: r3 :: nil, I n1 :: v2 :: v3 :: nil => make_mla_mulimm n1 r1 r2 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: I n2 :: v3 :: nil => make_mla_mulimm n2 r2 r1 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: v2 :: I n3 :: nil => make_mla_addimm n3 r1 r2 r3 | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2 diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index c9f97aa8..93ef2475 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -285,6 +285,69 @@ Proof. econstructor; split; eauto. simpl. congruence. Qed. +Lemma make_mla_mulimm_correct: + forall n1 r1 r2 r3, + rs#r1 = Vint n1 -> + let (op, args) := make_mla_mulimm n1 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul (Vint n1) rs#r2) rs#r3) v. +Proof. + intros; unfold make_mla_mulimm. + predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst. + exists (rs#r3); split; auto. destruct (rs#r2); simpl; auto. + destruct (rs#r3); simpl; auto. + rewrite Int.mul_commut, Int.mul_zero, Int.add_zero_l; auto. + rewrite Int.mul_commut, Int.mul_zero, Ptrofs.add_zero; auto. + predSpec Int.eq Int.eq_spec n1 Int.one; intros. subst. + exists (Val.add rs#r2 rs#r3); split; auto. destruct (rs#r2); simpl; auto. + destruct (rs#r3); simpl; auto. + rewrite Int.mul_commut, Int.mul_one; auto. + rewrite Int.mul_commut, Int.mul_one; auto. + eexists. simpl; split; eauto. + fold (Val.mul (Vint n1) (rs#r2)). rewrite H; auto. +Qed. + +Lemma make_mla_addimm_correct: + forall n3 r1 r2 r3, + rs#r3 = Vint n3 -> + let (op, args) := make_mla_addimm n3 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul rs#r1 rs#r2) (Vint n3)) v. +Proof. + intros; unfold make_mla_addimm. + predSpec Int.eq Int.eq_spec n3 Int.zero; intros. subst. + exists (Val.mul rs#r1 rs#r2); split; auto. + destruct (rs#r1), (rs#r2); simpl; auto. + rewrite Int.add_zero; auto. + eexists. simpl; split; eauto. rewrite H; auto. +Qed. + +Lemma make_mla_bothimm_correct: + forall n1 n3 r1 r2 r3, + rs#r1 = Vint n1 -> + rs#r3 = Vint n3 -> + let (op, args) := make_mla_bothimm n1 n3 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul (Vint n1) rs#r2) (Vint n3)) v. +Proof. + intros; unfold make_mla_bothimm. + predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst. + exists (Vint n3); split; auto. + destruct (rs#r2); simpl; auto. + rewrite Int.mul_commut, Int.mul_zero, Int.add_zero_l; auto. + predSpec Int.eq Int.eq_spec n1 Int.one; intros. subst. + generalize (make_addimm_correct n3 r2); intro ADDIMM. + destruct (make_addimm n3 r2) as [op args]. destruct ADDIMM as [v [OP LESSDEF]]. + exists v; split; auto. + destruct (rs#r2); simpl; auto. + simpl in LESSDEF. rewrite Int.mul_commut, Int.mul_one; auto. + predSpec Int.eq Int.eq_spec n3 Int.zero; intros. subst. + generalize (make_mulimm_correct n1 r2 r1 H); eauto; intro MULIMM. + destruct (make_mulimm n1 r2 r1) as [op args]. destruct MULIMM as [v [OP LESSDEF]]. + exists v; split; auto. + destruct (rs#r2); simpl; auto. + simpl in LESSDEF. rewrite Int.add_zero, Int.mul_commut; auto. + eexists. simpl; split; eauto. + fold (Val.mul (Vint n1) (rs#r2)). rewrite H, H0; auto. +Qed. + Lemma make_divimm_correct: forall n r1 r2 v, Val.divs rs#r1 rs#r2 = Some v -> @@ -480,6 +543,16 @@ Proof. InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). rewrite Val.mul_commut. apply make_mulimm_correct; auto. InvApproxRegs; SimplVM. inv H0. apply make_mulimm_correct; auto. +(* mla *) + InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). + apply make_mla_bothimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. + rewrite Val.mul_commut. apply make_mla_bothimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). + apply make_mla_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. + rewrite Val.mul_commut. apply make_mla_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_mla_addimm_correct; auto. (* divs *) assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divimm_correct; auto. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 86be8c95..c5277e8d 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -298,7 +298,7 @@ Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with - | nil => Zmax 0 ofs + | nil => Z.max 0 ofs | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1) | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2) end. @@ -369,8 +369,8 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). @@ -395,17 +395,17 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. Qed. Remark loc_arguments_sf_charact: forall tyl ofs p, - In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p. + In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Z.max 0 ofs)) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l). + assert (X: forall ofs1 ofs2 l, loc_argument_charact (Z.max 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Z.max 0 ofs1) l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p). + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Z.max 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Z.max 0 ofs1)) p). { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_sf; intros. elim H. @@ -482,29 +482,29 @@ Proof. induction tyl; simpl; intros. omega. destruct a. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. set (ir' := align ir 2). destruct (zlt ir' 4); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (ofs0 + 1); eauto. omega. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + apply Z.le_trans with (ofs0 + 1); eauto. omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. Qed. Remark size_arguments_sf_above: forall tyl ofs0, - Zmax 0 ofs0 <= size_arguments_sf tyl ofs0. + Z.max 0 ofs0 <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. omega. - destruct a; (eapply Zle_trans; [idtac|eauto]). + destruct a; (eapply Z.le_trans; [idtac|eauto]). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. @@ -516,9 +516,9 @@ Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Z.le_ge. assert (0 <= size_arguments_sf (sig_args s) (-4)). - { change 0 with (Zmax 0 (-4)). apply size_arguments_sf_above. } + { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. } assert (0 <= size_arguments_hf (sig_args s) 0 0 0). { apply size_arguments_hf_above. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. @@ -549,14 +549,14 @@ Proof. destruct H. discriminate. destruct H. discriminate. eauto. destruct Archi.big_endian. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. eauto. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. eauto. - (* float *) destruct (zlt fr 8); destruct H. @@ -581,7 +581,7 @@ Qed. Lemma loc_arguments_sf_bounded: forall ofs ty tyl ofs0, In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> - Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. + Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. elim H. @@ -598,15 +598,15 @@ Proof. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. eauto. - (* float *) destruct H. @@ -630,7 +630,7 @@ Proof. unfold loc_arguments, size_arguments; intros. assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) -> ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)). - { intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } + { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) -> ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0). { intros. eapply loc_arguments_hf_bounded; eauto. } diff --git a/arm/Machregs.v b/arm/Machregs.v index ba3bda7c..ae0ff6bf 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -200,7 +200,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. @@ -522,7 +522,7 @@ End SOUNDNESS. Program Definition mk_shift_amount (n: int) : shift_amount := {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}. Next Obligation. - assert (0 <= Zmod (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. + assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. rewrite Int.unsigned_repr. apply zlt_true. omega. assert (32 < Int.max_unsigned). compute; auto. omega. @@ -983,7 +983,7 @@ Remark weak_valid_pointer_no_overflow_extends: 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 Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index c867ba59..462d83ad 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -19,11 +19,10 @@ 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. -- Saved values of integer callee-save registers used by the function. -- Saved values of float callee-save registers used by the function. -- Saved return address into caller. - Pointer to activation record of the caller. +- Saved return address into caller. +- Local stack slots. +- Saved values of callee-save registers used by the function. - Space for the stack-allocated data declared in Cminor. The [frame_env] compilation environment records the positions of @@ -36,11 +35,11 @@ Definition fe_ofs_arg := 0. function. *) Definition make_env (b: bounds) := - let ol := align (4 * b.(bound_outgoing)) 8 in (* locals *) + let olink := 4 * b.(bound_outgoing) in (* back link*) + let ora := olink + 4 in (* return address *) + let ol := align (ora + 4) 8 in (* locals *) let ocs := ol + 4 * b.(bound_local) in (* callee-saves *) - let ora := align (size_callee_save_area b ocs) 4 in (* retaddr *) - let olink := ora + 4 in (* back link *) - let ostkdata := align (olink + 4) 8 in (* stack data *) + let ostkdata := align (size_callee_save_area b ocs) 8 in (* retaddr *) let sz := align (ostkdata + b.(bound_stack_data)) 8 in {| fe_size := sz; fe_ofs_link := olink; @@ -67,33 +66,32 @@ Lemma frame_env_separated: Proof. Local Opaque Z.add Z.mul sepconj range. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). + set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (0 <= olink) by (unfold olink; omega). + assert (olink <= ora) by (unfold ora; omega). + assert (ora + 4 <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ora) by (apply align_le; omega). - assert (ora <= olink) by (unfold olink; omega). - assert (olink + 4 <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). (* Reorder as: outgoing - local - callee-save + back link retaddr - back link *) + local + callee-save *) rewrite sep_swap12. - rewrite sep_swap45. + rewrite sep_swap23. rewrite sep_swap34. - rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold ol; omega. omega. apply range_split. omega. - apply range_split_2. fold ora; omega. omega. + apply range_split. omega. + apply range_split_2. fold ol; omega. omega. apply range_split. omega. apply range_drop_right with ostkdata. omega. eapply sep_drop2. eexact H. @@ -105,18 +103,18 @@ Lemma frame_env_range: 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). + set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (0 <= olink) by (unfold olink; omega). + assert (olink <= ora) by (unfold ora; omega). + assert (ora + 4 <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ora) by (apply align_le; omega). - assert (ora <= olink) by (unfold olink; omega). - assert (olink + 4 <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). split. omega. apply align_le; omega. Qed. @@ -130,14 +128,13 @@ Lemma frame_env_aligned: /\ (4 | fe_ofs_retaddr fe). Proof. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). - split. apply Zdivide_0. + set (ostkdata := align (size_callee_save_area b ocs) 8). + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. - split. apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. - apply align_divides; omega. + unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl. Qed. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 6f1cb6c1..67bc5d8b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -81,6 +81,11 @@ struct | FR r -> freg oc r | _ -> assert false + let preg_annot = function + | IR r -> int_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + let condition_name = function | TCeq -> "eq" | TCne -> "ne" @@ -154,6 +159,7 @@ struct | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",%%note" let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -534,23 +540,13 @@ struct | Psbc (r1,r2,sa) -> fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1 | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> - fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; - begin match r1, r2, sa with - | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) - | _ -> () - end; - 1 + fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrb(r1, r2, sa) -> fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pstr_p(r1, r2, sa) -> - fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; - begin match r1, r2, sa with - | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) - | _ -> () - end; - 1 + fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrb_p(r1, r2, sa) -> fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 | Pstrh_p(r1, r2, sa) -> @@ -710,15 +706,13 @@ struct (neg_condition_name cond) ireg r1 shift_op ifnot; 2 | Pbtbl(r, tbl) -> if !Clflags.option_mthumb then begin - let lbl = new_label() in - fprintf oc " adr r14, .L%d\n" lbl; - fprintf oc " add r14, r14, %a, lsl #2\n" ireg r; - fprintf oc " mov pc, r14\n"; - fprintf oc ".L%d:\n" lbl; + fprintf oc " lsl r14, %a, #2\n" ireg r; + fprintf oc " add pc, r14\n"; (* 16-bit encoding *) + fprintf oc " nop\n"; (* 16-bit encoding *) List.iter (fun l -> fprintf oc " b.w %a\n" print_label l) tbl; - 3 + List.length tbl + 2 + List.length tbl end else begin fprintf oc " add pc, pc, %a, lsl #2\n" ireg r; fprintf oc " nop\n"; @@ -729,12 +723,19 @@ struct end | Pbuiltin(ef, args, res) -> begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " elf_label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot; 0 | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "sp" oc + print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args; 0 | EF_inline_asm(txt, sg, clob) -> @@ -746,6 +747,7 @@ struct assert false end | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 + | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs); 0 let no_fallthrough = function | Pb _ -> true @@ -762,6 +764,9 @@ struct 2 in (len + add) * 4 | Pbuiltin (EF_inline_asm _,_,_) -> 1024 (* Better be safe than sorry *) + | Pbreg _ + | Pblsymb _ + | Pblreg _ -> 72 (* 4 for branch, 4 for fixup result 4 * 16 for fixup args *) | _ -> 12 @@ -857,10 +862,11 @@ struct fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" (match Configuration.model with - | "armv6" -> "armv6" - | "armv7a" -> "armv7-a" - | "armv7r" -> "armv7-r" - | "armv7m" -> "armv7-m" + | "armv6" -> "armv6" + | "armv6t2" -> "armv6t2" + | "armv7a" -> "armv7-a" + | "armv7r" -> "armv7-r" + | "armv7m" -> "armv7-m" | _ -> "armv7"); fprintf oc " .fpu %s\n" (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2"); diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index fb75435f..9d243413 100644 --- a/arm/extractionMachdep.v +++ b/arm/extractionMachdep.v @@ -28,3 +28,7 @@ Extract Constant Archi.abi => (* Choice of endianness *) Extract Constant Archi.big_endian => "Configuration.is_big_endian". + +(* Whether the model is ARMv6T2 or above and hence supports Thumb2. *) +Extract Constant Archi.thumb2_support => + "(Configuration.model = ""armv6t2"" || Configuration.model >= ""armv7"")". |