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, 4 insertions, 5 deletions

diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index f7e6c317..161e2a6e 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -313,12 +313,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop :=
       context_stack_tailcall ctx f ctx' ->
       tr_instr ctx pc (Itailcall sg (inr _ id) args) c
   | tr_builtin: forall ctx pc c ef args res s,
-      Ple res ctx.(mreg) ->
-      c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+      match res with BR r => Ple r ctx.(mreg) | _ => True end ->
+      c!(spc ctx pc) = Some (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s)) ->
       tr_instr ctx pc (Ibuiltin ef args res s) c
-  | tr_annot: forall ctx pc c ef args s,
-      c!(spc ctx pc) = Some (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) ->
-      tr_instr ctx pc (Iannot ef args s) c
   | tr_cond: forall ctx pc cond args s1 s2 c,
       c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) ->
       tr_instr ctx pc (Icond cond args s1 s2) c
@@ -554,6 +551,8 @@ Proof.
   red; simpl. 
 subst s2; simpl in *; xomega.
   red; auto.
+(* builtin *)
+  eapply tr_builtin; eauto. destruct b; eauto. 
 (* return *)
   destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. 
   (* inlined *)