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, 47 insertions, 42 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index b1c36513..45ad8e19 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -381,6 +381,47 @@ Definition add_move (rs rd: reg) (nd: node) : mon node :=
   then ret nd
   else add_instr (Iop Omove (rs::nil) rd nd).
 
+(** Translation of arguments and results of builtins. *)
+
+Definition exprlist_of_expr_list (l: list expr) : exprlist :=
+  List.fold_right Econs Enil l.
+
+Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : builtin_arg A * list A :=
+  match a with
+  | BA a =>
+      match rl with
+      | r :: rs => (BA r, rs)
+      | nil     => (BA_int Int.zero, nil)   (**r never happens *)
+      end
+  | BA_int n => (BA_int n, rl)
+  | BA_long n => (BA_long n, rl)
+  | BA_float n => (BA_float n, rl)
+  | BA_single n => (BA_single n, rl)
+  | BA_loadstack chunk ofs => (BA_loadstack chunk ofs, rl)
+  | BA_addrstack ofs => (BA_addrstack ofs, rl)
+  | BA_loadglobal chunk id ofs => (BA_loadglobal chunk id ofs, rl)
+  | BA_addrglobal id ofs => (BA_addrglobal id ofs, rl)
+  | BA_longofwords hi lo =>
+      let (hi', rl1) := convert_builtin_arg hi rl in
+      let (lo', rl2) := convert_builtin_arg lo rl1 in
+      (BA_longofwords hi' lo', rl2)
+  end.
+
+Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) :=
+  match al with
+  | nil => nil
+  | a1 :: al =>
+      let (a1', rl1) := convert_builtin_arg a1 rl in
+      a1' :: convert_builtin_args al rl1
+  end.
+
+Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) :=
+  match r with
+  | BR id => do r <- find_var map id; ret (BR r)
+  | BR_none => ret BR_none
+  | _ => error (Errors.msg "RTLgen: bad builtin_res")
+  end.
+
 (** Translation of an expression.  [transl_expr map a rd nd]
   enriches the current CFG with the RTL instructions necessary
   to compute the value of CminorSel expression [a], leave its result
@@ -413,7 +454,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do r <- find_letvar map n; add_move r rd nd
   | Ebuiltin ef al =>
       do rl <- alloc_regs map al;
-      do no <- add_instr (Ibuiltin ef rl rd nd);
+      do no <- add_instr (Ibuiltin ef (List.map (@BA reg) rl) (BR rd) nd);
       transl_exprlist map al rl no
   | Eexternal id sg al =>
       do rl <- alloc_regs map al;
@@ -455,39 +496,6 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
          transl_expr map b r nc
   end.
 
-(** Translation of arguments to annotations. *)
-
-Definition exprlist_of_expr_list (l: list expr) : exprlist :=
-  List.fold_right Econs Enil l.
-
-Fixpoint convert_annot_arg {A: Type} (a: annot_arg expr) (rl: list A) : annot_arg A * list A :=
-  match a with
-  | AA_base a =>
-      match rl with
-      | r :: rs => (AA_base r, rs)
-      | nil     => (AA_int Int.zero, nil)   (**r never happens *)
-      end
-  | AA_int n => (AA_int n, rl)
-  | AA_long n => (AA_long n, rl)
-  | AA_float n => (AA_float n, rl)
-  | AA_single n => (AA_single n, rl)
-  | AA_loadstack chunk ofs => (AA_loadstack chunk ofs, rl)
-  | AA_addrstack ofs => (AA_addrstack ofs, rl)
-  | AA_loadglobal chunk id ofs => (AA_loadglobal chunk id ofs, rl)
-  | AA_addrglobal id ofs => (AA_addrglobal id ofs, rl)
-  | AA_longofwords hi lo =>
-      let (hi', rl1) := convert_annot_arg hi rl in
-      let (lo', rl2) := convert_annot_arg lo rl1 in
-      (AA_longofwords hi' lo', rl2)
-  end.
-
-Fixpoint convert_annot_args {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) :=
-  match al with
-  | nil => nil
-  | a1 :: al =>
-      let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1
-  end.
-
 (** Auxiliary for translating exit expressions. *)
 
 Definition transl_exit (nexits: list node) (n: nat) : mon node :=
@@ -586,15 +594,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do rargs <- alloc_regs map cl;
       do n1 <- add_instr (Itailcall sig (inr _ id) rargs);
       transl_exprlist map cl rargs n1
-  | Sbuiltin optid ef al =>
-      do rargs <- alloc_regs map al;
-      do r <- alloc_optreg map optid;
-      do n1 <- add_instr (Ibuiltin ef rargs r nd);
-         transl_exprlist map al rargs n1
-  | Sannot ef args =>
-      let al := exprlist_of_expr_list (params_of_annot_args args) in
+  | Sbuiltin res ef args =>
+      let al := exprlist_of_expr_list (params_of_builtin_args args) in
       do rargs <- alloc_regs map al;
-      do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd);
+      let args' := convert_builtin_args args rargs in
+      do res' <- convert_builtin_res map res;
+      do n1 <- add_instr (Ibuiltin ef args' res' nd);
          transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;