diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
commit | 54f97d1988f623ba7422e13a504caeb5701ba93c (patch) | |
tree | d8dea46837352979490f4ed4516f9649fef41b98 /ia32/SelectOp.vp | |
parent | b4846ffadfa3fbb73ffa7d9c43e5218adeece8da (diff) | |
download | compcert-54f97d1988f623ba7422e13a504caeb5701ba93c.tar.gz compcert-54f97d1988f623ba7422e13a504caeb5701ba93c.zip |
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.
Diffstat (limited to 'ia32/SelectOp.vp')
-rw-r--r-- | ia32/SelectOp.vp | 22 |
1 files changed, 12 insertions, 10 deletions
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. |