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, 25 insertions, 17 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index ae9da0a7..2e631ad2 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -34,6 +34,7 @@ Require Import CminorSel.
 Require Import SelectOp.
 Require Import SelectDiv.
 Require Import SelectLong.
+Require Machregs.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope error_monad_scope.
@@ -203,21 +204,27 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind :=
       end
   end.
 
-(** Annotations *)
-
-Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool :=
-  match ef, optid with
-  | EF_annot _ _, None => true
-  | _, _ => false
+(** Builtin arguments and results *)
+
+Definition sel_builtin_arg
+       (e: Cminor.expr) (c: builtin_arg_constraint): AST.builtin_arg expr :=
+  let e' := sel_expr e in
+  let ba := builtin_arg e' in
+  if builtin_arg_ok ba c then ba else BA e'.
+
+Fixpoint sel_builtin_args
+       (el: list Cminor.expr)
+       (cl: list builtin_arg_constraint): list (AST.builtin_arg expr) :=
+  match el with
+  | nil => nil
+  | e :: el =>
+      sel_builtin_arg e (List.hd OK_default cl) :: sel_builtin_args el (List.tl cl)
   end.
 
-Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr :=
-  match e with
-  | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs
-  | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs
-  | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs
-  | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs
-  | _ => annot_arg (sel_expr e)
+Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
+  match optid with
+  | None => BR_none
+  | Some id => BR id
   end.
 
 (** Conversion of Cminor [switch] statements to decision trees. *)
@@ -277,12 +284,13 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt :=
       OK (match classify_call ge fn with
       | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
       | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
-      | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args)
+      | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
+                                    (sel_builtin_args args
+                                       (Machregs.builtin_constraints ef))
       end)
   | Cminor.Sbuiltin optid ef args =>
-      OK (if builtin_is_annot ef optid
-          then Sannot ef (List.map sel_annot_arg args)
-          else Sbuiltin optid ef (sel_exprlist args))
+      OK (Sbuiltin (sel_builtin_res optid) ef
+                   (sel_builtin_args args (Machregs.builtin_constraints ef)))
   | Cminor.Stailcall sg fn args => 
       OK (match classify_call ge fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)