From 3324ece265091490d5380caf753d76aeee059d3f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Aug 2015 18:19:58 +0200 Subject: Upgrade the ARM port to the new builtins. --- arm/Asm.v | 47 ++++---- arm/Asmexpand.ml | 290 ++++++++++++++++++++++++++++++------------------ arm/Asmgen.v | 4 +- arm/Asmgenproof.v | 44 +++----- arm/Machregs.v | 20 +++- arm/SelectOp.vp | 20 ++-- arm/SelectOpproof.v | 8 +- arm/TargetPrinter.ml | 32 ++---- backend/Debugvarproof.v | 6 +- 9 files changed, 260 insertions(+), 211 deletions(-) diff --git a/arm/Asm.v b/arm/Asm.v index 4e8a411a..1fd792b8 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -205,14 +205,13 @@ Inductive instruction : Type := | Ploadsymbol: ireg -> ident -> int -> 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 preg -> list preg -> instruction (**r built-in function *) - | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *) + | 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 *) - | Pclz: preg -> preg -> instruction (**r count leading zeros. *) + | Pclz: ireg -> ireg -> instruction (**r count leading zeros. *) | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) - | Prev: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) - | Prev16: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) + | Prev: ireg -> ireg -> instruction (**r reverse bytes and reverse bits. *) + | Prev16: ireg -> ireg -> instruction (**r reverse bytes and reverse bits. *) | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *) | Psbc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) (* Add, sub, rsb versions with s suffix *) @@ -319,6 +318,15 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := | _, _ => rs end. +(** Assigning the result of a builtin *) + +Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := + match res with + | BR r => rs#r <- v + | BR_none => rs + | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -748,7 +756,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pannot ef args => Stuck (**r treated specially below *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) | Ppush _ @@ -827,23 +834,16 @@ 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 vl rs' m', + forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) (fn_code f) = Some (Pbuiltin ef args res) -> - external_call' ef ge (map rs args) m t vl m' -> - rs' = nextinstr - (set_regs res vl + find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> + eval_builtin_args ge rs (rs SP) m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = nextinstr + (set_res res vres (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) -> - eval_annot_args ge rs (rs SP) m args vargs -> - 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 -> @@ -907,12 +907,8 @@ Ltac Equalities := split. constructor. auto. discriminate. discriminate. - inv H11. - 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 eval_annot_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H11. 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]. @@ -921,7 +917,6 @@ Ltac Equalities := red; intros; inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index ca30924c..d13015ff 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -21,6 +21,8 @@ open AST open Camlcoq open Integers +exception Error of string + (* Useful constants and helper functions *) let _0 = Integers.Int.zero @@ -74,51 +76,83 @@ let expand_int64_arith conflict rl fn = (* Handling of annotations *) let expand_annot_val txt targ args res = - emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args)); + emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); match args, res with - | [IR src], [IR dst] -> + | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmov (dst,SOreg src)) - | [FR src], [FR dst] -> + | [BA(FR src)], BR(FR dst) -> if dst <> src then emit (Pfcpyd (dst,src)) - | _, _ -> assert false - + | _, _ -> + raise (Error "ill-formed __builtin_annot_val") (* Handling of memcpy *) (* The ARM has strict alignment constraints for 2 and 4 byte accesses. 8-byte accesses must be 4-aligned. *) +let offset_in_range ofs = + let n = camlint_of_coqint ofs in n <= 128l && n >= -128l + +let memcpy_small_arg sz arg tmp = + match arg with + | BA (IR r) -> + (r, _0) + | BA_addrstack ofs -> + if offset_in_range ofs + && offset_in_range (Int.add ofs (Int.repr (Z.of_uint sz))) + then (IR13, ofs) + else begin expand_addimm tmp IR13 ofs; (tmp, _0) end + | _ -> + assert false + let expand_builtin_memcpy_small sz al src dst = - let rec copy ofs sz = + let (tsrc, tdst) = + if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in + let (rsrc, osrc) = memcpy_small_arg sz src tsrc in + let (rdst, odst) = memcpy_small_arg sz dst tdst in + let rec copy osrc odst sz = if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin - emit (Pfldd (FR7,src,ofs)); - emit (Pfstd (FR7,dst,ofs)); - copy (Int.add ofs _8) (sz - 8) + emit (Pfldd (FR7,rsrc,osrc)); + emit (Pfstd (FR7,rdst,odst)); + copy (Int.add osrc _8) (Int.add odst _8) (sz - 8) end else if sz >= 4 && al >= 4 then begin - emit (Pldr (IR14,src,SOimm ofs)); - emit (Pstr (IR14,dst,SOimm ofs)); - copy (Int.add ofs _4) (sz - 4) + emit (Pldr (IR14,rsrc,SOimm osrc)); + emit (Pstr (IR14,rdst,SOimm odst)); + copy (Int.add osrc _4) (Int.add odst _4) (sz - 4) end else if sz >= 2 && al >= 2 then begin - emit (Pldrh (IR14,src,SOimm ofs)); - emit (Pstrh (IR14,dst,SOimm ofs)); - copy (Int.add ofs _2) (sz - 2) + emit (Pldrh (IR14,rsrc,SOimm osrc)); + emit (Pstrh (IR14,rdst,SOimm odst)); + copy (Int.add osrc _2) (Int.add odst _2) (sz - 2) end else if sz >= 1 then begin - emit (Pldrb (IR14,src,SOimm ofs)); - emit (Pstrb (IR14,dst,SOimm ofs)); - copy (Int.add ofs _1) (sz - 1) - end else - () in - copy _0 sz + emit (Pldrb (IR14,rsrc,SOimm osrc)); + emit (Pstrb (IR14,rdst,SOimm odst)); + copy (Int.add osrc _1) (Int.add odst _1) (sz - 1) + end in + copy osrc odst sz + +let memcpy_big_arg arg tmp = + match arg with + | BA (IR r) -> + if r <> tmp then emit (Pmov(tmp, SOreg r)) + | BA_addrstack ofs -> + expand_addimm tmp IR13 ofs + | _ -> + assert false let expand_builtin_memcpy_big sz al src dst = assert (sz >= al); assert (sz mod al = 0); - assert (src = IR2); - assert (dst = IR3); + let (s, d) = + if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in + memcpy_big_arg src s; + memcpy_big_arg dst d; let (load, store, chunksize) = - if al >= 4 then (Pldr_p (IR12,src,SOimm _4), Pstr_p (IR12,dst,SOimm _4) , 4) - else if al = 2 then (Pldrh_p (IR12,src,SOimm _2), Pstrh_p (IR12,dst,SOimm _2), 2) - else (Pldrb_p (IR12,src,SOimm _1), Pstrb_p (IR12,dst,SOimm _1), 1) in + if al >= 4 then + (Pldr_p (IR12,s,SOimm _4), Pstr_p (IR12,d,SOimm _4) , 4) + else if al = 2 then + (Pldrh_p (IR12,s,SOimm _2), Pstrh_p (IR12,d,SOimm _2), 2) + else + (Pldrb_p (IR12,s,SOimm _1), Pstrb_p (IR12,d,SOimm _1), 1) in expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize))); let lbl = new_label () in emit (Plabel lbl); @@ -129,71 +163,93 @@ let expand_builtin_memcpy_big sz al src dst = let expand_builtin_memcpy sz al args = let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in + match args with [d; s] -> (d, s) | _ -> assert false in if sz <= 32 then expand_builtin_memcpy_small sz al src dst else expand_builtin_memcpy_big sz al src dst (* Handling of volatile reads and writes *) -let expand_builtin_vload_common chunk args res = - match chunk, args, res with - | Mint8unsigned, [IR addr], [IR res] -> - emit (Pldrb (res, addr,SOimm _0)) - | Mint8signed, [IR addr], [IR res] -> - emit (Pldrsb (res, addr,SOimm _0)) - | Mint16unsigned, [IR addr], [IR res] -> - emit (Pldrh (res, addr, SOimm _0)) - | Mint16signed, [IR addr], [IR res] -> - emit (Pldrsh (res, addr, SOimm _0)) - | Mint32, [IR addr], [IR res] -> - emit (Pldr (res,addr, SOimm _0)) - | Mint64, [IR addr], [IR res1; IR res2] -> - if addr <> res2 then begin - emit (Pldr (res2, addr, SOimm _0)); - emit (Pldr (res1, addr, SOimm _4)) +let expand_builtin_vload_common chunk base ofs res = + match chunk, res with + | Mint8unsigned, BR(IR res) -> + emit (Pldrb (res, base, SOimm ofs)) + | Mint8signed, BR(IR res) -> + emit (Pldrsb (res, base, SOimm ofs)) + | Mint16unsigned, BR(IR res) -> + emit (Pldrh (res, base, SOimm ofs)) + | Mint16signed, BR(IR res) -> + emit (Pldrsh (res, base, SOimm ofs)) + | Mint32, BR(IR res) -> + emit (Pldr (res, base, SOimm ofs)) + | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> + let ofs' = Int.add ofs _4 in + if base <> res2 then begin + emit (Pldr (res2, base, SOimm ofs)); + emit (Pldr (res1, base, SOimm ofs')) end else begin - emit (Pldr (res1,addr, SOimm _4)); - emit (Pldr (res2,addr, SOimm _0)) + emit (Pldr (res1, base, SOimm ofs')); + emit (Pldr (res2, base, SOimm ofs)) end - | Mfloat32, [IR addr], [FR res] -> - emit (Pflds (res, addr, _0)) - | Mfloat64, [IR addr], [FR res] -> - emit (Pfldd (res,addr, _0)) + | Mfloat32, BR(FR res) -> + emit (Pflds (res, base, ofs)) + | Mfloat64, BR(FR res) -> + emit (Pfldd (res, base, ofs)) | _ -> assert false let expand_builtin_vload chunk args res = - expand_builtin_vload_common chunk args res - -let expand_builtin_vload_global chunk id ofs args res = - emit (Ploadsymbol (IR14,id,ofs)); - expand_builtin_vload_common chunk (IR IR14 :: args) res - -let expand_builtin_vstore_common chunk args = - match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> - emit (Pstrb (src,addr, SOimm _0)) - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> - emit (Pstrh (src,addr, SOimm _0)) - | Mint32, [IR addr; IR src] -> - emit (Pstr (src,addr, SOimm _0)) - | Mint64, [IR addr; IR src1; IR src2] -> - emit (Pstr (src2,addr,SOimm _0)); - emit (Pstr (src1,addr,SOimm _4)) - | Mfloat32, [IR addr; FR src] -> - emit (Pfsts (src,addr,_0)) - | Mfloat64, [IR addr; FR src] -> - emit (Pfstd (src,addr,_0)); + match args with + | [BA(IR addr)] -> + expand_builtin_vload_common chunk addr _0 res + | [BA_addrstack ofs] -> + if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vload_common chunk IR13 ofs res + else begin + expand_addimm IR14 IR13 ofs; + expand_builtin_vload_common chunk IR14 _0 res + end + | [BA_addrglobal(id, ofs)] -> + emit (Ploadsymbol (IR14,id,ofs)); + expand_builtin_vload_common chunk IR14 _0 res + | _ -> + assert false + +let expand_builtin_vstore_common chunk base ofs src = + match chunk, src with + | (Mint8signed | Mint8unsigned), BA(IR src) -> + emit (Pstrb (src, base, SOimm ofs)) + | (Mint16signed | Mint16unsigned), BA(IR src) -> + emit (Pstrh (src, base, SOimm ofs)) + | Mint32, BA(IR src) -> + emit (Pstr (src, base, SOimm ofs)) + | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) -> + let ofs' = Int.add ofs _4 in + emit (Pstr (src2, base, SOimm ofs)); + emit (Pstr (src1, base, SOimm ofs')) + | Mfloat32, BA(FR src) -> + emit (Pfsts (src, base, ofs)) + | Mfloat64, BA(FR src) -> + emit (Pfstd (src, base, ofs)) | _ -> assert false let expand_builtin_vstore chunk args = - expand_builtin_vstore_common chunk args - -let expand_builtin_vstore_global chunk id ofs args = - emit (Ploadsymbol (IR14,id,ofs)); - expand_builtin_vstore_common chunk (IR IR14 :: args) + match args with + | [BA(IR addr); src] -> + expand_builtin_vstore_common chunk addr _0 src + | [BA_addrstack ofs; src] -> + if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then + expand_builtin_vstore_common chunk IR13 ofs src + else begin + expand_addimm IR14 IR13 ofs; + expand_builtin_vstore_common chunk IR14 _0 src + end + | [BA_addrglobal(id, ofs); src] -> + emit (Ploadsymbol (IR14,id,ofs)); + expand_builtin_vstore_common chunk IR14 _0 src + | _ -> + assert false (* Handling of varargs *) @@ -223,22 +279,24 @@ let expand_builtin_va_start r = (* Handling of compiler-inlined builtins *) + let expand_builtin_inline name args res = match name, args, res with (* Integer arithmetic *) - | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> - emit (Prev (IR res,IR a1)) - | "__builtin_bswap16", [IR a1], [IR res] -> - emit (Prev16 (IR res,IR a1)) - | "__builtin_clz", [IR a1], [IR res] -> - emit (Pclz (IR res, IR a1)) + | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> + emit (Prev (res, a1)) + | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> + emit (Prev16 (res, a1)) + | "__builtin_clz", [BA(IR a1)], BR(IR res) -> + emit (Pclz (res, a1)) (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> + | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> emit (Pfabsd (res,a1)) - | "__builtin_fsqrt", [FR a1], [FR res] -> + | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Pfsqrt (res,a1)) (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] -> + | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah ) rl (fun rl -> emit (Prsbs (rl,al,SOimm _0)); (* No "rsc" instruction in Thumb2. Emulate based on @@ -250,30 +308,35 @@ let expand_builtin_inline name args res = end else begin emit (Prsc (rh,ah,SOimm _0)) end) - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); + BA_splitlong(BA(IR bh), BA(IR bl))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Padds (rl,al,SOreg bl)); emit (Padc (rh,ah,SOreg bh))) - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); + BA_splitlong(BA(IR bh), BA(IR bl))], + BR_splitlong(BR(IR rh), BR(IR rl)) -> expand_int64_arith (rl = ah || rl = bh) rl (fun rl -> emit (Psubs (rl,al,SOreg bl)); emit (Psbc (rh,ah,SOreg bh))) - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + | "__builtin_mull", [BA(IR a); BA(IR b)], + BR_splitlong(BR(IR rh), BR(IR rl)) -> emit (Pumull (rl,rh,a,b)) (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> + | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) -> emit (Pldrh (res,a1,SOimm _0)); - emit (Prev16 (IR res,IR res)); - | "__builtin_read32_reversed", [IR a1], [IR res] -> + emit (Prev16 (res, res)); + | "__builtin_read32_reversed", [BA(IR a1)], BR(IR res) -> emit (Pldr (res,a1,SOimm _0)); - emit (Prev (IR res,IR res)); - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - emit (Prev16 (IR IR14, IR a2)); + emit (Prev (res, res)); + | "__builtin_write16_reversed", [BA(IR a1); BA(IR a2)], _ -> + emit (Prev16 (IR14, a2)); emit (Pstrh (IR14, a1, SOimm _0)) - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - emit (Prev (IR IR14, IR a2)); + | "__builtin_write32_reversed", [BA(IR a1); BA(IR a2)], _ -> + emit (Prev (IR14, a2)); emit (Pstr (IR14, a1, SOimm _0)) (* Synchronization *) | "__builtin_membar",[], _ -> @@ -285,11 +348,11 @@ let expand_builtin_inline name args res = | "__builtin_isb", [], _ -> emit Pisb (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> + | "__builtin_va_start", [BA(IR a)], _ -> expand_builtin_va_start a (* Catch-all *) | _ -> - invalid_arg ("unrecognized builtin " ^ name) + raise (Error ("unrecognized builtin " ^ name)) let expand_instruction instr = match instr with @@ -319,30 +382,35 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_vload_global(chunk, id, ofs) -> - expand_builtin_vload_global chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - expand_builtin_vstore_global chunk id ofs args | EF_annot_val (txt,targ) -> expand_annot_val 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 - | EF_inline_asm(txt, sg, clob) -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr - | _ -> assert false + | _ -> + assert false end | _ -> emit instr let expand_function fn = - set_current_function fn; - List.iter expand_instruction fn.fn_code; - get_current_function () + try + set_current_function fn; + List.iter expand_instruction fn.fn_code; + Errors.OK (get_current_function ()) + with Error s -> + Errors.Error (Errors.msg (coqstring_of_camlstring s)) let expand_fundef = function - | Internal f -> Internal (expand_function f) - | External ef -> External ef - -let expand_program (p: Asm.program) : Asm.program = - AST.transform_program expand_fundef p + | Internal f -> + begin match expand_function f with + | Errors.OK tf -> Errors.OK (Internal tf) + | Errors.Error msg -> Errors.Error msg + end + | External ef -> + Errors.OK (External ef) + +let expand_program (p: Asm.program) : Asm.program Errors.res = + AST.transform_partial_program expand_fundef p diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 5a3a48e1..2365d1d2 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -727,9 +727,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) (map preg_of res) :: k) - | Mannot ef args => - OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) + OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 6d9b134f..93c50bfb 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -747,48 +747,32 @@ Opaque loadind. intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - (* Mbuiltin *) - inv AT. monadInv H3. + inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H2); intro NOOV. - exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; 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. + erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. - Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. + instantiate (2 := tf); instantiate (1 := x). + unfold nextinstr. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. - apply preg_notin_charact. auto with asmgen. - apply preg_notin_charact. auto with asmgen. - apply agree_nextinstr. eapply agree_set_mregs; auto. + rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. + apply agree_nextinstr. eapply agree_set_res; auto. eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. -- (* Mannot *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_args_match; eauto. intros [vargs' [P Q]]. - 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. - erewrite <- sp_val by eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. - exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_states_intro with (ep := false); eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. - rewrite <- H1; simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - apply agree_nextinstr. auto. - congruence. - - (* Mgoto *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H4. diff --git a/arm/Machregs.v b/arm/Machregs.v index f46f2904..f4bd4613 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -130,7 +130,7 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with - | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil + | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. @@ -150,11 +150,7 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg 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. + (nil, nil). Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store @@ -171,3 +167,15 @@ Definition two_address_op (op: operation) : bool := Global Opaque two_address_op. +(* Constraints on constant propagation for builtins *) + +Definition builtin_constraints (ef: external_function) : + list builtin_arg_constraint := + match ef with + | EF_vload _ => OK_addrany :: nil + | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil + | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_debug kind txt targs => map (fun _ => OK_all) targs + | _ => nil + end. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index fea99ef5..aec737ad 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -489,16 +489,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. -(** ** Arguments of annotations *) +(** ** Arguments of builtins *) -Nondetfunction annot_arg (e: expr) := +Nondetfunction builtin_arg (e: expr) := match e with - | Eop (Ointconst n) Enil => AA_int n - | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs - | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop (Ointconst n) Enil => BA_int n + | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - AA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) - | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs - | _ => AA_base e + BA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) + | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) => + BA_loadglobal chunk id (Int.add ofs ofs1) + | _ => BA e end. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index d3c3239a..5f41e754 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -864,18 +864,20 @@ Proof. exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto. Qed. -Theorem eval_annot_arg: +Theorem eval_builtin_arg: forall a v, eval_expr ge sp e m nil a v -> - CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. + CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v. Proof. - intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. + intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. - constructor. - constructor. - constructor. - simpl in H5. inv H5. constructor. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address in H6. + inv H6. constructor; auto. - constructor; auto. Qed. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index f8d72836..f7f0d313 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -305,17 +305,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) -(* Handling of annotations *) - - let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - print_annot_stmt preg "sp" oc txt targs args - end - (* Auxiliary for 64-bit integer arithmetic built-ins. They expand to two instructions, one computing the low 32 bits of the result, followed by another computing the high 32 bits. In cases where @@ -521,7 +510,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " bic%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 | Pclz (r1,r2) -> - fprintf oc " clz %a, %a\n" preg r1 preg r2; 1 + fprintf oc " clz %a, %a\n" ireg r1 ireg r2; 1 | Pcmp(r1, so) -> fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 | Pdmb -> @@ -571,9 +560,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " orr%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 | Prev (r1,r2) -> - fprintf oc " rev %a, %a\n" preg r1 preg r2; 1 + fprintf oc " rev %a, %a\n" ireg r1 ireg r2; 1 | Prev16 (r1,r2) -> - fprintf oc " rev16 %a, %a\n" preg r1 preg r2; 1 + fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2; 1 | Prsb(r1, r2, so) -> fprintf oc " rsb%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 @@ -782,6 +771,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | Pbuiltin(ef, args, res) -> begin match ef with + | EF_annot(txt, targs) -> + fprintf oc "%s annotation: " comment; + print_annot_text preg "sp" oc (extern_atom txt) args; + 0 + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg "sp" oc + (P.to_int kind) (extern_atom txt) args; + 0 | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; @@ -790,13 +787,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | _ -> assert false end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args; 0 - | _ -> - assert false - end | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 let no_fallthrough = function diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index 35fbe226..6f0b8cda 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -455,15 +455,17 @@ Proof. - (* load *) econstructor; split. eapply plus_left. - econstructor; eauto. + eapply exec_Lload with (a := a). rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. apply eval_add_delta_ranges. traceEq. constructor; auto. - (* store *) econstructor; split. eapply plus_left. - econstructor; eauto. + eapply exec_Lstore with (a := a). rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. apply eval_add_delta_ranges. traceEq. constructor; auto. - (* call *) -- cgit