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, 152 insertions, 0 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 8acce510..db55c8e8 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -972,6 +972,145 @@ Proof.
   auto.
 Qed.
 
+(** Annotation arguments. *)
+
+(*
+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 *)
@@ -1304,6 +1443,19 @@ Proof.
   econstructor; eauto. constructor.
   eapply match_env_update_dest; eauto.
 
+  (* annot *)
+  inv TS. 
+  exploit transl_annot_args_correct; eauto. 
+  intros [rs' [tm' [vl' [E [F [G [J [K L]]]]]]]].
+  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 external_call_symbols_preserved. eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  traceEq. 
+  econstructor; eauto. constructor.
+ 
   (* seq *)
   inv TS. 
   econstructor; split.