From 54f97d1988f623ba7422e13a504caeb5701ba93c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 11:05:36 +0200 Subject: Refactoring of builtins and annotations in the back-end. Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations. --- ia32/Asm.v | 38 ++++++++++++++++---------------------- 1 file changed, 16 insertions(+), 22 deletions(-) (limited to 'ia32/Asm.v') diff --git a/ia32/Asm.v b/ia32/Asm.v index b423b4fc..6e21ec63 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -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]. -- cgit From 33dfbe7601ad16fcea5377563fa7ceb4053cb85a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 22 Aug 2015 09:46:37 +0200 Subject: Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small. --- ia32/Asm.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ia32/Asm.v') diff --git a/ia32/Asm.v b/ia32/Asm.v index 96a49005..979041ba 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -293,7 +293,7 @@ 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) + | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) end. Section RELSEM. -- cgit