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, 34 insertions, 34 deletions

diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 668eb808..ad1cbd14 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -78,8 +78,7 @@ Inductive stmt : Type :=
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
   | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt
   | Stailcall: signature -> expr + ident -> exprlist -> stmt
-  | Sbuiltin : option ident -> external_function -> exprlist -> stmt
-  | Sannot : external_function -> list (annot_arg expr) -> stmt
+  | Sbuiltin : builtin_res ident -> external_function -> list (builtin_arg expr) -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -249,34 +248,42 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
       Genv.find_symbol ge id = Some b ->
       eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero).
 
-Inductive eval_annot_arg: annot_arg expr -> val -> Prop :=
-  | eval_AA_base: forall a v,
+Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop :=
+  | eval_BA: forall a v,
       eval_expr nil a v ->
-      eval_annot_arg (AA_base a) v
-  | eval_AA_int: forall n,
-      eval_annot_arg (AA_int n) (Vint n)
-  | eval_AA_long: forall n,
-      eval_annot_arg (AA_long n) (Vlong n)
-  | eval_AA_float: forall n,
-      eval_annot_arg (AA_float n) (Vfloat n)
-  | eval_AA_single: forall n,
-      eval_annot_arg (AA_single n) (Vsingle n)
-  | eval_AA_loadstack: forall chunk ofs v,
+      eval_builtin_arg (BA a) v
+  | eval_BA_int: forall n,
+      eval_builtin_arg (BA_int n) (Vint n)
+  | eval_BA_long: forall n,
+      eval_builtin_arg (BA_long n) (Vlong n)
+  | eval_BA_float: forall n,
+      eval_builtin_arg (BA_float n) (Vfloat n)
+  | eval_BA_single: forall n,
+      eval_builtin_arg (BA_single n) (Vsingle n)
+  | eval_BA_loadstack: forall chunk ofs v,
       Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v ->
-      eval_annot_arg (AA_loadstack chunk ofs) v
-  | eval_AA_addrstack: forall ofs,
-      eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs))
-  | eval_AA_loadglobal: forall chunk id ofs v,
+      eval_builtin_arg (BA_loadstack chunk ofs) v
+  | eval_BA_addrstack: forall ofs,
+      eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs))
+  | eval_BA_loadglobal: forall chunk id ofs v,
       Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v ->
-      eval_annot_arg (AA_loadglobal chunk id ofs) v
-  | eval_AA_addrglobal: forall id ofs,
-      eval_annot_arg (AA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
-  | eval_AA_longofwords: forall a1 a2 v1 v2,
+      eval_builtin_arg (BA_loadglobal chunk id ofs) v
+  | eval_BA_addrglobal: forall id ofs,
+      eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
+  | eval_BA_longofwords: forall a1 a2 v1 v2,
       eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
-      eval_annot_arg (AA_longofwords (AA_base a1) (AA_base a2)) (Val.longofwords v1 v2).
+      eval_builtin_arg (BA_longofwords (BA a1) (BA a2)) (Val.longofwords v1 v2).
 
 End EVAL_EXPR.
 
+(** Update local environment with the result of a builtin. *)
+
+Definition set_builtin_res (res: builtin_res ident) (v: val) (e: env) : env :=
+  match res with
+  | BR id => PTree.set id v e
+  | _ => e
+  end.
+
 (** Pop continuation until a call or stop *)
 
 Fixpoint call_cont (k: cont) : cont :=
@@ -364,18 +371,11 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
         E0 (Callstate fd vargs (call_cont k) m')
 
-  | step_builtin: forall f optid ef al k sp e m vl t v m',
-      eval_exprlist sp e m nil al vl ->
-      external_call ef ge vl m t v m' ->
-      step (State f (Sbuiltin optid ef al) k sp e m)
-         t (State f Sskip k sp (set_optvar optid v e) m')
-
-  | step_annot: forall f ef al k sp e m vl t v m',
-      match ef with EF_annot _ _ => True | _ => False end ->
-      list_forall2 (eval_annot_arg sp e m) al vl ->
+  | step_builtin: forall f res ef al k sp e m vl t v m',
+      list_forall2 (eval_builtin_arg sp e m) al vl ->
       external_call ef ge vl m t v m' ->
-      step (State f (Sannot ef al) k sp e m)
-         t (State f Sskip k sp e m')
+      step (State f (Sbuiltin res ef al) k sp e m)
+         t (State f Sskip k sp (set_builtin_res res v e) m')
 
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)