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

diff --git a/backend/LTL.v b/backend/LTL.v
index 8c2749a7..67fb0197 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -44,8 +44,7 @@ Inductive instruction: Type :=
   | Lstore (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg)
   | Lcall (sg: signature) (ros: mreg + ident)
   | Ltailcall (sg: signature) (ros: mreg + ident)
-  | Lbuiltin (ef: external_function) (args: list mreg) (res: list mreg)
-  | Lannot (ef: external_function) (args: list (annot_arg loc))
+  | Lbuiltin (ef: external_function) (args: list (builtin_arg loc)) (res: builtin_res mreg)
   | Lbranch (s: node)
   | Lcond (cond: condition) (args: list mreg) (s1 s2: node)
   | Ljumptable (arg: mreg) (tbl: list node)
@@ -239,16 +238,12 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.free m sp 0 f.(fn_stacksize) = Some m' ->
       step (Block s f (Vptr sp Int.zero) (Ltailcall sig ros :: bb) rs m)
         E0 (Callstate s fd rs' m')
-  | exec_Lbuiltin: forall s f sp ef args res bb rs m t vl rs' m',
-      external_call' ef ge (reglist rs args) m t vl m' ->
-      rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) ->
+  | exec_Lbuiltin: forall s f sp ef args res bb rs m vargs t vres rs' m',
+      eval_builtin_args ge rs sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      rs' = Locmap.setres res vres (undef_regs (destroyed_by_builtin ef) rs) ->
       step (Block s f sp (Lbuiltin ef args res :: bb) rs m)
          t (Block s f sp bb rs' m')
-  | exec_Lannot: forall s f sp ef args bb rs vl m t v' m',
-      eval_annot_args ge rs sp m args vl ->
-      external_call ef ge vl m t v' m' ->
-      step (Block s f sp (Lannot ef args :: bb) rs m)
-         t (Block s f sp bb rs m')
   | exec_Lbranch: forall s f sp pc bb rs m,
       step (Block s f sp (Lbranch pc :: bb) rs m)
         E0 (State s f sp pc rs m)