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/CminorSel.v | 68 ++++++++++++++++++++++++++--------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'backend/CminorSel.v') diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 668eb808..ad1cbd14 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -78,8 +78,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt | Stailcall: signature -> expr + ident -> exprlist -> stmt - | Sbuiltin : option ident -> external_function -> exprlist -> stmt - | Sannot : external_function -> list (annot_arg expr) -> stmt + | Sbuiltin : builtin_res ident -> external_function -> list (builtin_arg expr) -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -249,34 +248,42 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := Genv.find_symbol ge id = Some b -> eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero). -Inductive eval_annot_arg: annot_arg expr -> val -> Prop := - | eval_AA_base: forall a v, +Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop := + | eval_BA: forall a v, eval_expr nil a v -> - eval_annot_arg (AA_base a) v - | eval_AA_int: forall n, - eval_annot_arg (AA_int n) (Vint n) - | eval_AA_long: forall n, - eval_annot_arg (AA_long n) (Vlong n) - | eval_AA_float: forall n, - eval_annot_arg (AA_float n) (Vfloat n) - | eval_AA_single: forall n, - eval_annot_arg (AA_single n) (Vsingle n) - | eval_AA_loadstack: forall chunk ofs v, + eval_builtin_arg (BA a) v + | eval_BA_int: forall n, + eval_builtin_arg (BA_int n) (Vint n) + | eval_BA_long: forall n, + eval_builtin_arg (BA_long n) (Vlong n) + | eval_BA_float: forall n, + eval_builtin_arg (BA_float n) (Vfloat n) + | eval_BA_single: forall n, + eval_builtin_arg (BA_single n) (Vsingle n) + | eval_BA_loadstack: forall chunk ofs v, Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> - eval_annot_arg (AA_loadstack chunk ofs) v - | eval_AA_addrstack: forall ofs, - eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) - | eval_AA_loadglobal: forall chunk id ofs v, + eval_builtin_arg (BA_loadstack chunk ofs) v + | eval_BA_addrstack: forall ofs, + eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_BA_loadglobal: forall chunk id ofs v, Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v -> - eval_annot_arg (AA_loadglobal chunk id ofs) v - | eval_AA_addrglobal: forall id ofs, - eval_annot_arg (AA_addrglobal id ofs) (Genv.symbol_address ge id ofs) - | eval_AA_longofwords: forall a1 a2 v1 v2, + eval_builtin_arg (BA_loadglobal chunk id ofs) v + | eval_BA_addrglobal: forall id ofs, + eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs) + | eval_BA_longofwords: forall a1 a2 v1 v2, eval_expr nil a1 v1 -> eval_expr nil a2 v2 -> - eval_annot_arg (AA_longofwords (AA_base a1) (AA_base a2)) (Val.longofwords v1 v2). + eval_builtin_arg (BA_longofwords (BA a1) (BA a2)) (Val.longofwords v1 v2). End EVAL_EXPR. +(** Update local environment with the result of a builtin. *) + +Definition set_builtin_res (res: builtin_res ident) (v: val) (e: env) : env := + match res with + | BR id => PTree.set id v e + | _ => e + end. + (** Pop continuation until a call or stop *) Fixpoint call_cont (k: cont) : cont := @@ -364,18 +371,11 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') - | step_builtin: forall f optid ef al k sp e m vl t v m', - eval_exprlist sp e m nil al vl -> - external_call ef ge vl m t v m' -> - step (State f (Sbuiltin optid ef al) k sp e m) - t (State f Sskip k sp (set_optvar optid v e) m') - - | step_annot: forall f ef al k sp e m vl t v m', - match ef with EF_annot _ _ => True | _ => False end -> - list_forall2 (eval_annot_arg sp e m) al vl -> + | step_builtin: forall f res ef al k sp e m vl t v m', + list_forall2 (eval_builtin_arg sp e m) al vl -> external_call ef ge vl m t v m' -> - step (State f (Sannot ef al) k sp e m) - t (State f Sskip k sp e m') + step (State f (Sbuiltin res ef al) k sp e m) + t (State f Sskip k sp (set_builtin_res res v e) m') | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) -- cgit