Extend annotations so that they can keep track of global variables and local variables whose address is taken.

- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.

Implementation is not complete yet.

1 files changed, 50 insertions, 2 deletions

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index bb9bd592..d755d46d 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -520,6 +520,14 @@ Proof.
   auto.
 Qed.
 
+Lemma set_optvar_lessdef:
+  forall e1 e2 optid v1 v2,
+  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
+  env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2).
+Proof.
+  unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto.
+Qed.
+
 Lemma set_params_lessdef:
   forall il vl1 vl2, 
   Val.lessdef_list vl1 vl2 ->
@@ -590,6 +598,25 @@ Proof.
   exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
+Lemma sel_annot_args_correct:
+  forall sp e e' m m',
+  env_lessdef e e' -> Mem.extends m m' ->
+  forall al vl,
+  Cminor.eval_exprlist ge sp e m al vl ->
+  exists vl',
+     list_forall2 (CminorSel.eval_annot_arg tge sp e' m')
+                  (List.map (fun a => annot_arg (sel_expr a)) al)
+                  vl'
+  /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; simpl.
+- exists (@nil val); split; constructor. 
+- exploit sel_expr_correct; eauto. intros (v1' & A & B).
+  destruct IHeval_exprlist as (vl' & C & D).
+  exists (v1' :: vl'); split; auto.
+  constructor; auto. eapply eval_annot_arg; eauto. 
+Qed.
+
 (** Semantic preservation for functions and statements. *)
 
 Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
@@ -675,6 +702,8 @@ Proof.
   destruct (classify_call ge e); simpl; auto.
 (* tailcall *)
   destruct (classify_call ge e); simpl; auto.
+(* builtin *)
+  destruct (builtin_is_annot e); simpl; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.  
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -776,14 +805,33 @@ Proof.
   econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
   constructor; auto. apply call_cont_commut; auto.
 - (* Sbuiltin *)
+  destruct (builtin_is_annot ef optid) eqn:ISANNOT.
++ (* annotation *)
+  assert (X: exists text targs, ef = EF_annot text targs). 
+  { destruct ef; try discriminate. econstructor; econstructor; eauto. }
+  destruct X as (text & targs & EQ). 
+  assert (Y: optid = None).
+  { destruct ef; try discriminate. destruct optid; try discriminate. auto. }
+  exploit sel_annot_args_correct; eauto. 
+  set (bl' := map (fun e => annot_arg (sel_expr e)) bl).
+  intros (vargs' & P & Q).
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2 [A [B [C D]]]]].
+  left; econstructor; split.
+  econstructor.
+  rewrite EQ; auto.
+  eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  rewrite Y. constructor; auto.
++ (* other builtin *)
   exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
   exploit external_call_mem_extends; eauto. 
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eauto. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  constructor; auto.
-  destruct optid; simpl; auto. apply set_var_lessdef; auto.
+  constructor; auto. apply set_optvar_lessdef; auto. 
 - (* Seq *)
   left; econstructor; split.
   constructor. constructor; auto. constructor; auto.