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. --- backend/RTL.v | 40 +++++++++++++--------------------------- 1 file changed, 13 insertions(+), 27 deletions(-) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index 83761c42..56a5efeb 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -70,13 +70,10 @@ Inductive instruction: Type := | Itailcall: signature -> reg + ident -> list reg -> instruction (** [Itailcall sig fn args] performs a function invocation in tail-call position. *) - | Ibuiltin: external_function -> list reg -> reg -> node -> instruction + | Ibuiltin: external_function -> list (builtin_arg reg) -> builtin_res reg -> node -> instruction (** [Ibuiltin ef args dest succ] calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) - | Iannot: external_function -> list (annot_arg reg) -> node -> instruction - (** [Iannot ef args succ] is similar to [Ibuiltin] but specialized - to annotations. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -253,19 +250,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s fd rs##args m') | exec_Ibuiltin: - forall s f sp pc rs m ef args res pc' t v m', + forall s f sp pc rs m ef args res pc' vargs t vres m', (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> - external_call ef ge rs##args m t v m' -> - step (State s f sp pc rs m) - t (State s f sp pc' (rs#res <- v) m') - | exec_Iannot: - forall s f sp pc rs m ef args pc' vargs vres t m', - (fn_code f)!pc = Some(Iannot ef args pc') -> - match ef with EF_annot _ _ => True | _ => False end -> - eval_annot_args ge (fun r => rs#r) sp m args vargs -> + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> step (State s f sp pc rs m) - t (State s f sp pc' rs m') + t (State s f sp pc' (regmap_setres res vres rs) m') | exec_Icond: forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -367,16 +357,13 @@ Proof. intros. subst. inv H0. exists s1; auto. inversion H; subst; auto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. - exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto. - exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. - exists (State s0 f sp pc' rs m2). eapply exec_Iannot; eauto. + exists (State s0 f sp pc' (regmap_setres res vres2 rs) m2). eapply exec_Ibuiltin; eauto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) red; intros; inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. Qed. (** * Operations on RTL abstract syntax *) @@ -411,7 +398,6 @@ Definition successors_instr (i: instruction) : list node := | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil | Ibuiltin ef args res s => s :: nil - | Iannot ef args s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil @@ -432,8 +418,7 @@ Definition instr_uses (i: instruction) : list reg := | Icall sig (inr id) args res s => args | Itailcall sig (inl r) args => r :: args | Itailcall sig (inr id) args => args - | Ibuiltin ef args res s => args - | Iannot ef args s => params_of_annot_args args + | Ibuiltin ef args res s => params_of_builtin_args args | Icond cond args ifso ifnot => args | Ijumptable arg tbl => arg :: nil | Ireturn None => nil @@ -450,8 +435,8 @@ Definition instr_defs (i: instruction) : option reg := | Istore chunk addr args src s => None | Icall sig ros args res s => Some res | Itailcall sig ros args => None - | Ibuiltin ef args res s => Some res - | Iannot ef args s => None + | Ibuiltin ef args res s => + match res with BR r => Some r | _ => None end | Icond cond args ifso ifnot => None | Ijumptable arg tbl => None | Ireturn optarg => None @@ -492,8 +477,9 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m) | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) | Itailcall sig (inr id) args => fold_left Pmax args m - | Ibuiltin ef args res s => fold_left Pmax args (Pmax res m) - | Iannot ef args s => fold_left Pmax (params_of_annot_args args) m + | Ibuiltin ef args res s => + fold_left Pmax (params_of_builtin_args args) + (fold_left Pmax (params_of_builtin_res res) m) | Icond cond args ifso ifnot => fold_left Pmax args m | Ijumptable arg tbl => Pmax arg m | Ireturn None => m @@ -513,7 +499,7 @@ Proof. { induction l; simpl; intros. auto. apply IHl. xomega. } - destruct i; simpl; try (destruct s0); try (apply X); try xomega. + destruct i; simpl; try (destruct s0); repeat (apply X); try xomega. destruct o; xomega. Qed. @@ -527,7 +513,7 @@ Proof. - apply X. xomega. - apply X. xomega. - destruct s0; apply X; xomega. -- apply X. xomega. +- destruct b; inv H1. apply X. simpl. xomega. Qed. Remark max_reg_instr_uses: -- cgit