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

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index ba7fa3a6..0533d561 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -356,29 +356,55 @@ Proof.
   eapply extcall_args_match; eauto.
 Qed.
 
-(** Translation of arguments to annotations. *)
+(** Translation of arguments and results to builtins. *)
 
-Remark annot_arg_match:
+Remark builtin_arg_match:
   forall ge (rs: regset) sp m a v,
-  eval_annot_arg ge (fun r => rs (preg_of r)) sp m a v ->
-  eval_annot_arg ge rs sp m (map_annot_arg preg_of a) v.
+  eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v ->
+  eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v.
 Proof.
-  induction 1; simpl; eauto with aarg.
+  induction 1; simpl; eauto with barg.
 Qed.
 
-Lemma annot_args_match:
+Lemma builtin_args_match:
   forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall al vl, eval_annot_args ge ms sp m al vl ->
-  exists vl', eval_annot_args ge rs sp m' (map (map_annot_arg preg_of) al) vl'
+  forall al vl, eval_builtin_args ge ms sp m al vl ->
+  exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl'
            /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3; intros; simpl.
   exists (@nil val); split; constructor.
-  exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. 
+  exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. 
   intros; eapply preg_val; eauto.
   intros (v1' & A & B).
   destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto. apply annot_arg_match; auto. 
+  exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto. 
+Qed.
+
+Lemma agree_set_res:
+  forall res ms sp rs v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_res res v ms) sp (Asm.set_res (map_builtin_res preg_of res) v' rs).
+Proof.
+  induction res; simpl; intros.
+- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
+  intros. apply Pregmap.gso; auto.
+- auto.
+- apply IHres2. apply IHres1. auto. 
+  apply Val.hiword_lessdef; auto.
+  apply Val.loword_lessdef; auto.
+Qed.
+
+Lemma set_res_other:
+  forall r res v rs,
+  data_preg r = false ->
+  set_res (map_builtin_res preg_of res) v rs r = rs r.
+Proof.
+  induction res; simpl; intros.
+- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate.
+- auto.
+- rewrite IHres2, IHres1; auto.
 Qed.
 
 (** * Correspondence between Mach code and Asm code *)