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/Constprop.v | 73 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 45 insertions(+), 28 deletions(-) (limited to 'backend/Constprop.v') diff --git a/backend/Constprop.v b/backend/Constprop.v index ce56ff62..3a238b95 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -20,6 +20,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Op. +Require Machregs. Require Import Registers. Require Import RTL. Require Import Lattice. @@ -102,39 +103,58 @@ Definition num_iter := 10%nat. Definition successor (f: function) (ae: AE.t) (pc: node) : node := successor_rec num_iter f ae pc. -Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) := +Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) := match a with - | AA_base r => + | BA r => match areg ae r with - | I n => AA_int n - | L n => AA_long n - | F n => if Compopts.generate_float_constants tt then AA_float n else a - | FS n => if Compopts.generate_float_constants tt then AA_single n else a + | I n => BA_int n + | L n => BA_long n + | F n => if Compopts.generate_float_constants tt then BA_float n else a + | FS n => if Compopts.generate_float_constants tt then BA_single n else a | _ => a end - | AA_longofwords hi lo => - match annot_strength_reduction ae hi, annot_strength_reduction ae lo with - | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo) - | hi', lo' => AA_longofwords hi' lo' + | BA_longofwords hi lo => + match builtin_arg_reduction ae hi, builtin_arg_reduction ae lo with + | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo) + | hi', lo' => BA_longofwords hi' lo' end | _ => a end. -Function builtin_strength_reduction - (ae: AE.t) (ef: external_function) (args: list reg) := - match ef, args with - | EF_vload chunk, r1 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vload_global chunk symb n1, nil) - | _ => (ef, args) - end - | EF_vstore chunk, r1 :: r2 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) - | _ => (ef, args) +Definition builtin_arg_strength_reduction + (ae: AE.t) (a: builtin_arg reg) (c: builtin_arg_constraint) := + let a' := builtin_arg_reduction ae a in + if builtin_arg_ok a' c then a' else a. + +Fixpoint builtin_args_strength_reduction + (ae: AE.t) (al: list (builtin_arg reg)) (cl: list builtin_arg_constraint) := + match al with + | nil => nil + | a :: al => + builtin_arg_strength_reduction ae a (List.hd OK_default cl) + :: builtin_args_strength_reduction ae al (List.tl cl) + end. + +(** For debug annotations, add constant values to the original info + instead of replacing it. *) + +Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := + match al with + | nil => nil + | a :: al => + let a' := builtin_arg_reduction ae a in + let al' := a :: debug_strength_reduction ae al in + match a' with + | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' + | _ => al' end - | _, _ => - (ef, args) + end. + +Definition builtin_strength_reduction + (ae: AE.t) (ef: external_function) (al: list (builtin_arg reg)) := + match ef with + | EF_debug _ _ _ => debug_strength_reduction ae al + | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef) end. Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) @@ -174,10 +194,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Itailcall sig ros args => Itailcall sig (transf_ros ae ros) args | Ibuiltin ef args res s => - let (ef', args') := builtin_strength_reduction ae ef args in - Ibuiltin ef' args' res s - | Iannot ef args s => - Iannot ef (List.map (annot_strength_reduction ae) args) s + Ibuiltin ef (builtin_strength_reduction ae ef args) res s | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with -- cgit