diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asm.v | 38 | ||||
| -rw-r--r-- | ia32/Asmexpand.ml | 168 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 4 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 40 | ||||
| -rw-r--r-- | ia32/Machregs.v | 13 | ||||
| -rw-r--r-- | ia32/SelectOp.vp | 22 | ||||
| -rw-r--r-- | ia32/SelectOpproof.v | 6 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 13 |
8 files changed, 143 insertions, 161 deletions
@@ -211,8 +211,7 @@ Inductive instruction: Type := | Plabel(l: label) | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) - | Pbuiltin(ef: external_function)(args: list preg)(res: list preg) - | Pannot(ef: external_function)(args: list (annot_arg preg)) + | Pbuiltin(ef: external_function)(args: list (builtin_arg preg))(res: builtin_res preg) | Padcl_ir (n: int) (r: ireg) | Padcl_rr (r1: ireg) (r2: ireg) | Paddl (r1: ireg) (r2: ireg) @@ -288,6 +287,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_longofwords 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. *) @@ -782,8 +790,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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. *) | Padcl_ir _ _ @@ -880,24 +886,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) f.(fn_code) = Some (Pbuiltin ef args res) -> - external_call' ef ge (map rs args) m t vl m' -> + eval_builtin_args ge rs (rs ESP) m args vargs -> + external_call ef ge vargs m t vres m' -> rs' = nextinstr_nf - (set_regs res vl + (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) f.(fn_code) = Some (Pannot ef args) -> - eval_annot_args ge rs (rs ESP) 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 -> @@ -961,12 +959,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 H4. eexact H9. intros [A B]. diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index e07672a6..9d8260b7 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -59,77 +59,83 @@ let sp_adjustment sz = (* 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_rr (dst,src)) - | [FR src], [FR dst] -> + | [BA(FR src)], BR(FR dst) -> if dst <> src then emit (Pmovsd_ff (dst,src)) | _, _ -> assert false - +(* Translate a builtin argument into an addressing mode *) + +let addressing_of_builtin_arg = function + | BA (IR r) -> Addrmode(Some r, None, Coq_inl Integers.Int.zero) + | BA_addrstack ofs -> Addrmode(Some ESP, None, Coq_inl ofs) + | BA_addrglobal(id, ofs) -> Addrmode(None, None, Coq_inr(id, ofs)) + | _ -> assert false + +let offset_addressing (Addrmode(base, ofs, cst)) delta = + Addrmode(base, ofs, + match cst with + | Coq_inl n -> Coq_inl(Integers.Int.add n delta) + | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) + (* Handling of memcpy *) (* Unaligned memory accesses are quite fast on IA32, so use large memory accesses regardless of alignment. *) let expand_builtin_memcpy_small sz al src dst = - assert (src = EDX && dst = EAX); - let rec copy ofs sz = + let rec copy src dst sz = if sz >= 8 && !Clflags.option_ffpu then begin - emit (Pmovq_rm (XMM7,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovq_mr (Addrmode (Some src, None, Coq_inl ofs),XMM7)); - copy (Int.add ofs _8) (sz - 8) + emit (Pmovq_rm (XMM7, src)); + emit (Pmovq_mr (dst, XMM7)); + copy (offset_addressing src _8) (offset_addressing dst _8) (sz - 8) end else if sz >= 4 then begin - emit (Pmov_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmov_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _4) (sz - 4) + emit (Pmov_rm (ECX, src)); + emit (Pmov_mr (dst, ECX)); + copy (offset_addressing src _4) (offset_addressing dst _4) (sz - 4) end else if sz >= 2 then begin - emit (Pmovw_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovw_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _2) (sz - 2) + emit (Pmovw_rm (ECX, src)); + emit (Pmovw_mr (dst, ECX)); + copy (offset_addressing src _2) (offset_addressing dst _2) (sz - 2) end else if sz >= 1 then begin - emit (Pmovb_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovb_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _1) (sz - 1) + emit (Pmovb_rm (ECX, src)); + emit (Pmovb_mr (dst, ECX)); + copy (offset_addressing src _1) (offset_addressing dst _1) (sz - 1) end in - copy _0 sz + copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz let expand_builtin_memcpy_big sz al src dst = - assert (src = ESI && dst = EDI); + if src <> BA (IR ESI) then emit (Plea (ESI, addressing_of_builtin_arg src)); + if dst <> BA (IR EDI) then emit (Plea (EDI, addressing_of_builtin_arg dst)); emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; if sz mod 4 >= 2 then emit Pmovsw; if sz mod 2 >= 1 then emit Pmovsb let expand_builtin_memcpy sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in + let (dst, src) = 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 offset_addressing (Addrmode(base, ofs, cst)) delta = - Addrmode(base, ofs, - match cst with - | Coq_inl n -> Coq_inl(Integers.Int.add n delta) - | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) - let expand_builtin_vload_common chunk addr res = match chunk, res with - | Mint8unsigned, [IR res] -> + | Mint8unsigned, BR(IR res) -> emit (Pmovzb_rm (res,addr)) - | Mint8signed, [IR res] -> + | Mint8signed, BR(IR res) -> emit (Pmovsb_rm (res,addr)) - | Mint16unsigned, [IR res] -> + | Mint16unsigned, BR(IR res) -> emit (Pmovzw_rm (res,addr)) - | Mint16signed, [IR res] -> + | Mint16signed, BR(IR res) -> emit (Pmovsw_rm (res,addr)) - | Mint32, [IR res] -> + | Mint32, BR(IR res) -> emit (Pmov_rm (res,addr)) - | Mint64, [IR res1; IR res2] -> + | Mint64, BR_longofwords(BR(IR res1), BR(IR res2)) -> let addr' = offset_addressing addr (coqint_of_camlint 4l) in if not (Asmgen.addressing_mentions addr res2) then begin emit (Pmov_rm (res2,addr)); @@ -138,60 +144,51 @@ let expand_builtin_vload_common chunk addr res = emit (Pmov_rm (res1,addr')); emit (Pmov_rm (res2,addr)) end - | Mfloat32, [FR res] -> + | Mfloat32, BR(FR res) -> emit (Pmovss_fm (res,addr)) - | Mfloat64, [FR res] -> + | Mfloat64, BR(FR res) -> emit (Pmovsd_fm (res,addr)) | _ -> assert false let expand_builtin_vload chunk args res = match args with - | [IR addr] -> - expand_builtin_vload_common chunk (Addrmode (Some addr,None, Coq_inl _0)) res + | [addr] -> + expand_builtin_vload_common chunk (addressing_of_builtin_arg addr) res | _ -> assert false -let expand_builtin_vload_global chunk id ofs args res = - expand_builtin_vload_common chunk (Addrmode(None, None, Coq_inr(id,ofs))) res - let expand_builtin_vstore_common chunk addr src tmp = match chunk, src with - | (Mint8signed | Mint8unsigned), [IR src] -> + | (Mint8signed | Mint8unsigned), BA(IR src) -> if Asmgen.low_ireg src then emit (Pmovb_mr (addr,src)) else begin emit (Pmov_rr (tmp,src)); emit (Pmovb_mr (addr,tmp)) end - | (Mint16signed | Mint16unsigned), [IR src] -> + | (Mint16signed | Mint16unsigned), BA(IR src) -> emit (Pmovw_mr (addr,src)) - | Mint32, [IR src] -> + | Mint32, BA(IR src) -> emit (Pmov_mr (addr,src)) - | Mint64, [IR src1; IR src2] -> + | Mint64, BA_longofwords(BA(IR src1), BA(IR src2)) -> let addr' = offset_addressing addr (coqint_of_camlint 4l) in emit (Pmov_mr (addr,src2)); emit (Pmov_mr (addr',src1)) - | Mfloat32, [FR src] -> + | Mfloat32, BA(FR src) -> emit (Pmovss_mf (addr,src)) - | Mfloat64, [FR src] -> + | Mfloat64, BA(FR src) -> emit (Pmovsd_mf (addr,src)) | _ -> assert false let expand_builtin_vstore chunk args = match args with - | IR addr :: src -> - expand_builtin_vstore_common chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src - (if addr = EAX then ECX else EAX) + | [addr; src] -> + let addr = addressing_of_builtin_arg addr in + expand_builtin_vstore_common chunk addr src + (if Asmgen.addressing_mentions addr EAX then ECX else EAX) | _ -> assert false - - -let expand_builtin_vstore_global chunk id ofs args = - expand_builtin_vstore_common chunk - (Addrmode(None, None, Coq_inr(id,ofs))) args EAX - (* Handling of varargs *) @@ -210,27 +207,27 @@ let expand_builtin_va_start r = let expand_builtin_inline name args res = match name, args, res with (* Integer arithmetic *) - | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> + | ("__builtin_bswap"| "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> if a1 <> res then emit (Pmov_rr (res,a1)); emit (Pbswap res) - | "__builtin_bswap16", [IR a1], [IR res] -> + | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> if a1 <> res then emit (Pmov_rr (res,a1)); emit (Prolw_8 res) - | "__builtin_clz", [IR a1], [IR res] -> + | "__builtin_clz", [BA(IR a1)], BR(IR res) -> emit (Pbslr (a1,res)); emit (Pxor_ri(res,coqint_of_camlint 31l)) - | "__builtin_ctz", [IR a1], [IR res] -> + | "__builtin_ctz", [BA(IR a1)], BR(IR res) -> emit (Pbsfl (a1,res)) (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> + | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> if a1 <> res then emit (Pmovsd_ff (a1,res)); emit (Pabsd res) (* This ensures that need_masks is set to true *) - | "__builtin_fsqrt", [FR a1], [FR res] -> + | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Psqrtsd (a1,res)) - | "__builtin_fmax", [FR a1; FR a2], [FR res] -> + | "__builtin_fmax", [BA(FR a1); BA(FR a2)], BR(FR res) -> if res = a1 then emit (Pmaxsd (a2,res)) else if res = a2 then @@ -239,7 +236,7 @@ let expand_builtin_inline name args res = emit (Pmovsd_ff (a1,res)); emit (Pmaxsd (a2,res)) end - | "__builtin_fmin", [FR a1; FR a2], [FR res] -> + | "__builtin_fmin", [BA(FR a1); BA(FR a2)], BR(FR res) -> if res = a1 then emit (Pminsd (a2,res)) else if res = a2 then @@ -248,7 +245,7 @@ let expand_builtin_inline name args res = emit (Pmovsd_ff (a1,res)); emit (Pminsd (a2,res)) end - | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> if res = a1 then emit (Pfmadd132 (a2,a3,res)) else if res = a2 then @@ -259,7 +256,7 @@ let expand_builtin_inline name args res = emit (Pmovsd_ff (a2,res)); emit (Pfmadd231 (a1,a2,res)) end - |"__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] -> + |"__builtin_fmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> if res = a1 then emit (Pfmsub132 (a2,a3,res)) else if res = a2 then @@ -270,7 +267,7 @@ let expand_builtin_inline name args res = emit (Pmovsd_ff (a2,res)); emit (Pfmsub231 (a1,a2,res)) end - | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] -> + | "__builtin_fnmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> if res = a1 then emit (Pfnmadd132 (a2,a3,res)) else if res = a2 then @@ -281,7 +278,7 @@ let expand_builtin_inline name args res = emit (Pmovsd_ff (a2,res)); emit (Pfnmadd231 (a1,a2,res)) end - |"__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] -> + |"__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> if res = a1 then emit (Pfnmsub132 (a2,a3,res)) else if res = a2 then @@ -293,32 +290,38 @@ let expand_builtin_inline name args res = emit (Pfnmsub231 (a1,a2,res)) end (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); emit (Pneg EAX); emit (Padcl_ir (_0,EDX)); emit (Pneg EDX) - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al)); + BA_longofwords(BA(IR bh), BA(IR bl))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); emit (Paddl (EBX,EAX)); emit (Padcl_rr (ECX,EDX)) - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al)); + BA_longofwords(BA(IR bh), BA(IR bl))], + BR_longofwords(BR(IR rh), BR(IR rl)) -> assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); emit (Psub_rr (EBX,EAX)); emit (Psbbl (ECX,EDX)) - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + | "__builtin_mull", [BA(IR a); BA(IR b)], + BR_longofwords(BR(IR rh), BR(IR rl)) -> assert (a = EAX && b = EDX && rh = EDX && rl = EAX); emit (Pmul_r EDX) (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> + | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) -> let addr = Addrmode(Some a1,None,Coq_inl _0) in emit (Pmovzw_rm (res,addr)); emit (Prolw_8 res) - | "__builtin_read32_reversed", [IR a1], [IR res] -> + | "__builtin_read32_reversed", [BA(IR a1)], BR(IR res) -> let addr = Addrmode(Some a1,None,Coq_inl _0) in emit (Pmov_rm (res,addr)); emit (Pbswap res) - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + | "__builtin_write16_reversed", [BA(IR a1); BA(IR a2)], _ -> let tmp = if a1 = ECX then EDX else ECX in let addr = Addrmode(Some a1,None,Coq_inl _0) in if a2 <> tmp then @@ -326,7 +329,7 @@ let expand_builtin_inline name args res = emit (Pxchg (tmp,tmp)); emit (Pmovw_mr (addr,tmp)) (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> + | "__builtin_va_start", [BA(IR a)], _ -> expand_builtin_va_start a (* Synchronization *) | "__builtin_membar", [], _ -> @@ -335,7 +338,7 @@ let expand_builtin_inline name args res = | _ -> invalid_arg ("unrecognized builtin " ^ name) - +(* Expansion of instructions *) let expand_instruction instr = match instr with @@ -361,18 +364,15 @@ 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_memcpy(sz, al) -> expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> expand_annot_val txt targ args res - | EF_inline_asm(txt, sg, clob) -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr - | _ -> assert false + | _ -> + assert false end | _ -> emit instr diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 2c1afc11..1ccde43b 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -536,9 +536,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: Pret :: k) | Mbuiltin ef args res => - OK (Pbuiltin ef (List.map preg_of args) (List.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) end. (** Translation of a code sequence *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 3570da2e..d91e17a2 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -671,53 +671,33 @@ Opaque loadind. rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* 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. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. - rewrite undef_regs_other. rewrite set_pregs_other_2. rewrite undef_regs_other_2. - rewrite <- H0. simpl. econstructor; eauto. + rewrite undef_regs_other. rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. - rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. simpl; intros. intuition congruence. - apply agree_nextinstr_nf. eapply agree_set_mregs; auto. + apply agree_nextinstr_nf. 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/ia32/Machregs.v b/ia32/Machregs.v index 65e27599..ace193b7 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -137,7 +137,6 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | EF_memcpy sz al => if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil | EF_vstore (Mint8unsigned|Mint8signed) => AX :: CX :: nil - | EF_vstore_global (Mint8unsigned|Mint8signed) _ _ => AX :: nil | EF_builtin id sg => if ident_eq id builtin_write16_reversed || ident_eq id builtin_write32_reversed @@ -267,3 +266,15 @@ Definition two_address_op (op: operation) : bool := | Ocmp c => false end. +(* 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_addrany :: OK_addrany :: 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/ia32/SelectOp.vp b/ia32/SelectOp.vp index 74e3fbd7..bd3a4850 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -507,17 +507,19 @@ 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 (Olea (Aglobal id ofs)) Enil => AA_addrglobal id ofs - | Eop (Olea (Ainstack ofs)) Enil => AA_addrstack ofs + | Eop (Ointconst n) Enil => BA_int n + | Eop (Olea (Aglobal id ofs)) Enil => BA_addrglobal id ofs + | Eop (Olea (Ainstack 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 (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs - | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs - | _ => AA_base e + BA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l) + | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | _ => BA e end. + +Definition builtin_function_const (id: ident) := false. diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 50f0d9b6..d40ec7af 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -898,12 +898,12 @@ Proof. exists (v :: nil); split. constructor; auto. constructor. 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. diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 18aacebf..581c84e2 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -658,20 +658,17 @@ module Target(System: SYSTEM):TARGET = assert false | Pbuiltin(ef, args, res) -> begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args | 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; + print_inline_asm preg oc (extern_atom txt) sg + (params_of_builtin_args args) + (params_of_builtin_res res); fprintf oc "%s end inline assembly\n" comment | _ -> assert false end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end let print_literal64 oc (lbl, n) = fprintf oc "%a: .quad 0x%Lx\n" label lbl n |