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, 61 insertions, 185 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 02460f67..559ab3a2 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -220,6 +220,22 @@ Proof.
 Qed.
 Hint Resolve match_env_update_dest: rtlg.
 
+(** A variant of [match_env_update_var] corresponding to the assignment
+  of the result of a builtin. *)
+
+Lemma match_env_update_res:
+  forall map res v e le tres tv rs,
+  Val.lessdef v tv ->
+  map_wf map ->
+  tr_builtin_res map res tres ->
+  match_env map e le rs ->
+  match_env map (set_builtin_res res v e) le (regmap_setres tres tv rs).
+Proof.
+  intros. inv H1; simpl.
+- eapply match_env_update_var; eauto.
+- auto.
+Qed.
+
 (** Matching and [let]-bound variables. *)
 
 Lemma match_env_bind_letvar:
@@ -677,6 +693,15 @@ Proof.
   auto.
 Qed.
 
+Remark eval_builtin_args_trivial:
+  forall (ge: RTL.genv) (rs: regset) sp m rl,
+  eval_builtin_args ge (fun r => rs#r) sp m (List.map (@BA reg) rl) rs##rl.
+Proof.
+  induction rl; simpl.
+- constructor.
+- constructor; auto. constructor.
+Qed.
+
 Lemma transl_expr_Ebuiltin_correct:
   forall le ef al vl v,
   eval_exprlist ge sp e m le al vl ->
@@ -691,7 +716,9 @@ Proof.
   exists (rs1#rd <- v'); exists tm2.
 (* Exec *)
   split. eapply star_right. eexact EX1.
+  change (rs1#rd <- v') with (regmap_setres (BR rd) v' rs1).
   eapply exec_Ibuiltin; eauto.
+  eapply eval_builtin_args_trivial.
   eapply external_call_symbols_preserved; eauto. 
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   reflexivity.
@@ -972,7 +999,7 @@ Proof.
   auto.
 Qed.
 
-(** Annotation arguments. *)
+(** Builtin arguments. *)
 
 Lemma eval_exprlist_append:
   forall le al1 vl1 al2 vl2,
@@ -985,54 +1012,54 @@ Proof.
 - simpl. constructor; eauto. 
 Qed.
 
-Lemma invert_eval_annot_arg:
+Lemma invert_eval_builtin_arg:
   forall a v,
-  eval_annot_arg ge sp e m a v ->
+  eval_builtin_arg ge sp e m a v ->
   exists vl, 
-     eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_arg a)) vl
-  /\ Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v
-  /\ (forall vl', convert_annot_arg a (vl ++ vl') = (fst (convert_annot_arg a vl), vl')).
+     eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_builtin_arg a)) vl
+  /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v
+  /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')).
 Proof.
-  induction 1; simpl; econstructor; intuition eauto with evalexpr aarg.
+  induction 1; simpl; econstructor; intuition eauto with evalexpr barg.
   constructor. 
   constructor. 
   repeat constructor.
 Qed.
 
-Lemma invert_eval_annot_args:
+Lemma invert_eval_builtin_args:
   forall al vl,
-  list_forall2 (eval_annot_arg ge sp e m) al vl ->
+  list_forall2 (eval_builtin_arg ge sp e m) al vl ->
   exists vl',
-     eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_args al)) vl'
-  /\ Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl') vl.
+     eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_builtin_args al)) vl'
+  /\ Events.eval_builtin_args ge (fun v => v) sp m (convert_builtin_args al vl') vl.
 Proof.
   induction 1; simpl.
 - exists (@nil val); split; constructor.
-- exploit invert_eval_annot_arg; eauto. intros (vl1 & A & B & C).
+- exploit invert_eval_builtin_arg; eauto. intros (vl1 & A & B & C).
   destruct IHlist_forall2 as (vl2 & D & E).
   exists (vl1 ++ vl2); split.
   apply eval_exprlist_append; auto.
   rewrite C; simpl. constructor; auto. 
 Qed.
 
-Lemma transl_eval_annot_arg:
+Lemma transl_eval_builtin_arg:
   forall rs a vl rl v,
   Val.lessdef_list vl rs##rl ->
-  Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v ->
+  Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v ->
   exists v',
-     Events.eval_annot_arg ge (fun r => rs#r) sp m (fst (convert_annot_arg a rl)) v'
+     Events.eval_builtin_arg ge (fun r => rs#r) sp m (fst (convert_builtin_arg a rl)) v'
   /\ Val.lessdef v v'
-  /\ Val.lessdef_list (snd (convert_annot_arg a vl)) rs##(snd (convert_annot_arg a rl)).
+  /\ Val.lessdef_list (snd (convert_builtin_arg a vl)) rs##(snd (convert_builtin_arg a rl)).
 Proof.
   induction a; simpl; intros until v; intros LD EV;
-  try (now (inv EV; econstructor; eauto with aarg)).
+  try (now (inv EV; econstructor; eauto with barg)).
 - destruct rl; simpl in LD; inv LD; inv EV; simpl.
-  econstructor; eauto with aarg. 
+  econstructor; eauto with barg. 
   exists (rs#p); intuition auto. constructor.
-- destruct (convert_annot_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *.
-  destruct (convert_annot_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *.
-  destruct (convert_annot_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *.
-  destruct (convert_annot_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *.
+- destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *.
+  destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *.
+  destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *.
+  destruct (convert_builtin_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *.
   inv EV. 
   exploit IHa1; eauto. rewrite CV1; simpl; eauto. 
   rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1).
@@ -1042,164 +1069,25 @@ Proof.
   split; auto. apply Val.longofwords_lessdef; auto.
 Qed.
 
-Lemma transl_eval_annot_args:
+Lemma transl_eval_builtin_args:
   forall rs al vl1 rl vl,
   Val.lessdef_list vl1 rs##rl ->
-  Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl1) vl ->
+  Events.eval_builtin_args ge (fun v => v) sp m (convert_builtin_args al vl1) vl ->
   exists vl',
-     Events.eval_annot_args ge (fun r => rs#r) sp m (convert_annot_args al rl) vl'
+     Events.eval_builtin_args ge (fun r => rs#r) sp m (convert_builtin_args al rl) vl'
   /\ Val.lessdef_list vl vl'.
 Proof.
   induction al; simpl; intros until vl; intros LD EV.
 - inv EV. exists (@nil val); split; constructor.
-- destruct (convert_annot_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *.
+- destruct (convert_builtin_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *.
   inv EV. 
-  exploit transl_eval_annot_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. 
+  exploit transl_eval_builtin_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. 
   rewrite CV1; simpl. intros (v1' & A1 & B1 & C1).
   exploit IHal. eexact C1. eauto. intros (vl' & A2 & B2).
-  destruct (convert_annot_arg a rl) as [a1'' rl2]; simpl in *.
+  destruct (convert_builtin_arg a rl) as [a1'' rl2]; simpl in *.
   exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
-
-(*
-Definition transl_annot_arg_prop (a: annot_arg expr) (v: val): Prop :=
-  forall tm cs f map pr ns nd a' rs
-    (MWF: map_wf map)
-    (TR: tr_annot_arg f.(fn_code) map pr a ns nd a')
-    (ME: match_env map e nil rs)
-    (EXT: Mem.extends m tm),
-  exists rs', exists tm', exists v',
-     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
-  /\ match_env map e nil rs'
-  /\ Events.eval_annot_arg tge (fun r => rs'#r) sp tm' a' v'
-  /\ Val.lessdef v v'
-  /\ (forall r, In r pr -> rs'#r = rs#r)
-  /\ Mem.extends m tm'.
-
-Theorem transl_annot_arg_correct:
-  forall a v,
-  eval_annot_arg ge sp e m a v ->
-  transl_annot_arg_prop a v.
-Proof.
-  induction 1; red; intros; inv TR.
-- exploit transl_expr_correct; eauto. intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
-  exists rs1, tm1, rs1#r; intuition eauto. constructor.
-- exists rs, tm, (Vint n); intuition auto using star_refl with aarg.
-- exists rs, tm, (Vlong n); intuition auto using star_refl with aarg.
-- exists rs, tm, (Vfloat n); intuition auto using star_refl with aarg.
-- exists rs, tm, (Vsingle n); intuition auto using star_refl with aarg.
-- exploit Mem.loadv_extends; eauto. intros (v' & P & Q).
-  exists rs, tm, v'; intuition auto using star_refl with aarg.
-- exists rs, tm, (Val.add sp (Vint ofs)); intuition auto using star_refl with aarg.
-- exploit Mem.loadv_extends; eauto. intros (v' & P & Q).
-  replace (Genv.symbol_address ge id ofs) 
-     with (Senv.symbol_address tge id ofs) in P.
-  exists rs, tm, v'; intuition auto using star_refl with aarg.
-  unfold Genv.symbol_address, Senv.symbol_address. simpl.
-  rewrite symbols_preserved; auto.
-- exists rs, tm, (Senv.symbol_address tge id ofs); intuition auto using star_refl with aarg.
-  unfold Genv.symbol_address, Senv.symbol_address. simpl.
-  rewrite symbols_preserved; auto.
-- inv H5. inv H9. simpl in H5. 
-  exploit transl_expr_correct. eexact H. eauto. eauto. eauto. eauto. 
-  intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
-  exploit transl_expr_correct. eexact H0. eauto. eauto. eauto. eauto. 
-  intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2).
-  exists rs2, tm2, (Val.longofwords rs2#r rs2#r0); intuition auto.
-  eapply star_trans; eauto. 
-  constructor. constructor. constructor. 
-  rewrite (D2 r) by auto with coqlib. apply Val.longofwords_lessdef; auto.
-  transitivity rs1#r1; auto with coqlib.
-Qed.
-
-
-Definition transl_annot_args_prop (l: list (annot_arg expr)) (vl: list val): Prop :=
-  forall tm cs f map pr ns nd l' rs
-    (MWF: map_wf map)
-    (TR: tr_annot_args f.(fn_code) map pr l ns nd l')
-    (ME: match_env map e nil rs)
-    (EXT: Mem.extends m tm),
-  exists rs', exists tm', exists vl',
-     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
-  /\ match_env map e nil rs'
-  /\ eval_annot_args tge (fun r => rs'#r) sp tm' l' vl'
-  /\ Val.lessdef_list vl vl'
-  /\ (forall r, In r pr -> rs'#r = rs#r)
-  /\ Mem.extends m tm'.
-
-Theorem transl_annot_args_correct:
-  forall l vl,
-  list_forall2 (eval_annot_arg ge sp e m) l vl ->
-  transl_annot_args_prop l vl.
-Proof.
-  induction 1; red; intros.
-- inv TR. exists rs, tm, (@nil val). 
-  split. constructor.
-  split. auto.
-  split. constructor.
-  split. constructor.
-  split. auto.
-  auto.
-- inv TR. inv H; inv H5. 
-  + exploit transl_expr_correct; eauto.
-    intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
-    exploit (IHlist_forall2 tm1 cs); eauto. 
-    intros (rs2 & tm2 & vl2 & A2 & B2 & C2 & D2 & E2 & F2). simpl in E2.
-    exists rs2, tm2, (rs2#r :: vl2); intuition auto.
-    eapply star_trans; eauto.
-    constructor; auto. constructor.
-    rewrite E2; auto.
-    transitivity rs1#r0; auto.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Vint n :: vl'); simpl; intuition auto. constructor; auto with aarg.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Vlong n :: vl'); simpl; intuition auto. constructor; auto with aarg.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Vfloat n :: vl'); simpl; intuition auto. constructor; auto with aarg.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Vsingle n :: vl'); simpl; intuition auto. constructor; auto with aarg.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exploit Mem.loadv_extends; eauto. intros (v1' & P & Q).
-    exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; eauto with aarg. 
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Val.add sp (Vint ofs) :: vl'); simpl; intuition auto. constructor; auto with aarg.
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exploit Mem.loadv_extends; eauto. intros (v1' & P & Q).
-    replace (Genv.symbol_address ge id ofs) 
-       with (Senv.symbol_address tge id ofs) in P.
-    exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; auto with aarg. 
-    unfold Genv.symbol_address, Senv.symbol_address. simpl.
-    rewrite symbols_preserved; auto. 
-  + exploit (IHlist_forall2 tm cs); eauto.
-    intros (rs' & tm' & vl' & A & B & C & D & E & F).
-    exists rs', tm', (Genv.symbol_address tge id ofs :: vl'); simpl; intuition auto.
-    constructor; auto with aarg. constructor. 
-    unfold Genv.symbol_address. rewrite symbols_preserved; auto.
-  + inv H7. inv H12. 
-    exploit transl_expr_correct. eexact H1. eauto. eauto. eauto. eauto. 
-    intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
-    exploit transl_expr_correct. eexact H2. eauto. eauto. eauto. eexact E1.  
-    intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). simpl in D2.
-    exploit (IHlist_forall2 tm2 cs); eauto. 
-    intros (rs3 & tm3 & vl3 & A3 & B3 & C3 & D3 & E3 & F3). simpl in E3.
-    exists rs3, tm3, (Val.longofwords rs3#r rs3#r0 :: vl3); intuition auto.
-    eapply star_trans; eauto. eapply star_trans; eauto.  auto.
-    constructor; auto with aarg. constructor. constructor. constructor.  
-    constructor; auto. apply Val.longofwords_lessdef. 
-    rewrite E3, D2; auto.
-    rewrite E3; auto. 
-    transitivity rs1#r1; auto. transitivity rs2#r1; auto.
-Qed.
-*)
-
 End CORRECTNESS_EXPR.
 
 (** ** Measure over CminorSel states *)
@@ -1520,36 +1408,24 @@ Proof.
 
   (* builtin *)
   inv TS. 
+  exploit invert_eval_builtin_args; eauto. intros (vparams & P & Q).
   exploit transl_exprlist_correct; eauto.
   intros [rs' [tm' [E [F [G [J K]]]]]].
-  edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto.
-  econstructor; split.
-  left. eapply plus_right. eexact E.
-  eapply exec_Ibuiltin. eauto. 
-  eapply external_call_symbols_preserved. eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  traceEq. 
-  econstructor; eauto. constructor.
-  eapply match_env_update_dest; eauto.
-
-  (* annot *)
-  inv TS. exploit invert_eval_annot_args; eauto. intros (vparams & P & Q).
-  exploit transl_exprlist_correct; eauto.
-  intros [rs' [tm' [E [F [G [J K]]]]]].
-  exploit transl_eval_annot_args; eauto. 
+  exploit transl_eval_builtin_args; eauto. 
   intros (vargs' & U & V).
-  exploit (@eval_annot_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto.
+  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto.
   intros (vargs'' & X & Y).
   assert (Z: Val.lessdef_list vl vargs'') by (eapply Val.lessdef_list_trans; eauto).
   edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto.
   econstructor; split.
   left. eapply plus_right. eexact E.
-  eapply exec_Iannot; eauto. 
-  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. 
+  eapply exec_Ibuiltin. eauto.
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. 
   eapply external_call_symbols_preserved. eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   traceEq. 
   econstructor; eauto. constructor.
+  eapply match_env_update_res; eauto.
  
   (* seq *)
   inv TS.