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, 31 insertions, 45 deletions

diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 993e0b34..c7cc8d8a 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -400,25 +400,25 @@ Proof.
   eapply function_ptr_translated; eauto.
 Qed.
 
-(** Translation of annotation arguments. *)
+(** Translation of builtin arguments. *)
 
-Lemma tr_annot_arg:
+Lemma tr_builtin_arg:
   forall F bound ctx rs rs' sp sp' m m',
   match_globalenvs F bound ->
   agree_regs F ctx rs rs' ->
   F sp = Some(sp', ctx.(dstk)) ->
   Mem.inject F m m' ->
   forall a v,
-  eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
-  exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v'
+  eval_builtin_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
+  exists v', eval_builtin_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sbuiltinarg ctx a) v'
           /\ Val.inject F v v'.
 Proof.
   intros until m'; intros MG AG SP MI. induction 1; simpl.
 - exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto.
-- econstructor; eauto with aarg.
-- econstructor; eauto with aarg.
-- econstructor; eauto with aarg.
-- econstructor; eauto with aarg.
+- econstructor; eauto with barg.
+- econstructor; eauto with barg.
+- econstructor; eauto with barg.
+- econstructor; eauto with barg.
 - exploit Mem.loadv_inject; eauto. 
   instantiate (1 := Vptr sp' (Int.add ofs (Int.repr (dstk ctx)))). 
   simpl. econstructor; eauto. rewrite Int.add_zero_l; auto.
@@ -429,30 +429,30 @@ Proof.
     rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
     inv MG. econstructor. eauto. rewrite Int.add_zero; auto. }
   exploit Mem.loadv_inject; eauto. intros (v' & A & B).
-  exists v'; eauto with aarg. 
+  exists v'; eauto with barg. 
 - econstructor; split. constructor. 
   unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
   rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
   inv MG. econstructor. eauto. rewrite Int.add_zero; auto.
-- destruct IHeval_annot_arg1 as (v1 & A1 & B1).
-  destruct IHeval_annot_arg2 as (v2 & A2 & B2).
-  econstructor; split. eauto with aarg. apply Val.longofwords_inject; auto. 
+- destruct IHeval_builtin_arg1 as (v1 & A1 & B1).
+  destruct IHeval_builtin_arg2 as (v2 & A2 & B2).
+  econstructor; split. eauto with barg. apply Val.longofwords_inject; auto. 
 Qed.
 
-Lemma tr_annot_args:
+Lemma tr_builtin_args:
   forall F bound ctx rs rs' sp sp' m m',
   match_globalenvs F bound ->
   agree_regs F ctx rs rs' ->
   F sp = Some(sp', ctx.(dstk)) ->
   Mem.inject F m m' ->
   forall al vl,
-  eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
-  exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl'
+  eval_builtin_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
+  exists vl', eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sbuiltinarg ctx) al) vl'
           /\ Val.inject_list F vl vl'.
 Proof.
   induction 5; simpl.
 - exists (@nil val); split; constructor.
-- exploit tr_annot_arg; eauto. intros (v1' & A & B).
+- exploit tr_builtin_arg; eauto. intros (v1' & A & B).
   destruct IHlist_forall2 as (vl' & C & D).
   exists (v1' :: vl'); split; constructor; auto.
 Qed.
@@ -663,6 +663,15 @@ Proof.
   intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega.
 Qed.
 
+Lemma match_stacks_inside_set_res:
+  forall F m m' stk stk' f' ctx sp' rs' res v, 
+  match_stacks_inside F m m' stk stk' f' ctx sp' rs' ->
+  match_stacks_inside F m m' stk stk' f' ctx sp' (regmap_setres (sbuiltinres ctx res) v rs').
+Proof.
+  intros. destruct res; simpl; auto. 
+  apply match_stacks_inside_set_reg; auto.
+Qed.
+
 (** Preservation by a memory store *)
 
 Lemma match_stacks_inside_store:
@@ -1064,46 +1073,23 @@ Proof.
 
 (* builtin *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
-  exploit external_call_mem_inject; eauto. 
-    eapply match_stacks_inside_globals; eauto.
-    instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. 
-  intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
-  left; econstructor; split.
-  eapply plus_one. eapply exec_Ibuiltin; eauto. 
-    eapply external_call_symbols_preserved; eauto. 
-    exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  econstructor.
-    eapply match_stacks_inside_set_reg. 
-    eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
-    intros; eapply external_call_max_perm; eauto. 
-    intros; eapply external_call_max_perm; eauto. 
-  auto. 
-  eapply agree_set_reg. eapply agree_regs_incr; eauto. auto. auto. 
-  apply J; auto.
-  auto. 
-  eapply external_call_valid_block; eauto. 
-  eapply range_private_extcall; eauto. 
-    intros; eapply external_call_max_perm; eauto. 
-  auto. 
-  intros. apply SSZ2. eapply external_call_max_perm; eauto. 
-
-(* annot *)
-  exploit tr_funbody_inv; eauto. intros TR; inv TR.
   exploit match_stacks_inside_globalenvs; eauto. intros [bound MG]. 
-  exploit tr_annot_args; eauto. intros (vargs' & P & Q).
+  exploit tr_builtin_args; eauto. intros (vargs' & P & Q).
   exploit external_call_mem_inject; eauto. 
     eapply match_stacks_inside_globals; eauto.
   intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
   left; econstructor; split.
-  eapply plus_one. eapply exec_Iannot; eauto.
+  eapply plus_one. eapply exec_Ibuiltin; eauto. 
     eapply external_call_symbols_preserved; eauto. 
     exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor.
+    eapply match_stacks_inside_set_res. 
     eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
     intros; eapply external_call_max_perm; eauto. 
     intros; eapply external_call_max_perm; eauto. 
-  auto. 
-  eapply agree_regs_incr; eauto. auto. auto. 
+  auto.
+  destruct res; simpl; [apply agree_set_reg;auto|idtac|idtac]; eapply agree_regs_incr; eauto.
+  auto. auto.
   eapply external_call_valid_block; eauto. 
   eapply range_private_extcall; eauto. 
     intros; eapply external_call_max_perm; eauto.