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.

1 files changed, 19 insertions, 21 deletions

diff --git a/backend/Stacking.v b/backend/Stacking.v
index 21cf6b73..caf0ae59 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -128,26 +128,26 @@ Definition transl_op (fe: frame_env) (op: operation) :=
 Definition transl_addr (fe: frame_env) (addr: addressing) :=
   shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr.
 
-(** Translation of an annotation argument. *)
+(** Translation of a builtin argument. *)
 
-Fixpoint transl_annot_arg (fe: frame_env) (a: annot_arg loc) : annot_arg mreg :=
+Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg mreg :=
   match a with
-  | AA_base (R r) => AA_base r
-  | AA_base (S Local ofs ty) =>
-      AA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty)))
-  | AA_base (S _ _ _) => AA_int Int.zero  (**r never happens *)
-  | AA_int n => AA_int n
-  | AA_long n => AA_long n
-  | AA_float n => AA_float n
-  | AA_single n => AA_single n
-  | AA_loadstack chunk ofs =>
-      AA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data)))
-  | AA_addrstack ofs =>
-      AA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data)))
-  | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs
-  | AA_addrglobal id ofs => AA_addrglobal id ofs
-  | AA_longofwords hi lo => 
-      AA_longofwords (transl_annot_arg fe hi) (transl_annot_arg fe lo)
+  | BA (R r) => BA r
+  | BA (S Local ofs ty) =>
+      BA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty)))
+  | BA (S _ _ _) => BA_int Int.zero  (**r never happens *)
+  | BA_int n => BA_int n
+  | BA_long n => BA_long n
+  | BA_float n => BA_float n
+  | BA_single n => BA_single n
+  | BA_loadstack chunk ofs =>
+      BA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data)))
+  | BA_addrstack ofs =>
+      BA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data)))
+  | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
+  | BA_addrglobal id ofs => BA_addrglobal id ofs
+  | BA_longofwords hi lo => 
+      BA_longofwords (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
   end.
 
 (** Translation of a Linear instruction.  Prepends the corresponding
@@ -192,9 +192,7 @@ Definition transl_instr
       restore_callee_save fe
         (Mtailcall sig ros :: k)
   | Lbuiltin ef args dst =>
-      Mbuiltin ef args dst :: k
-  | Lannot ef args =>
-      Mannot ef (map (transl_annot_arg fe) args) :: k
+      Mbuiltin ef (map (transl_builtin_arg fe) args) dst :: k
   | Llabel lbl =>
       Mlabel lbl :: k
   | Lgoto lbl =>