From 57d3627c69a812a037d2d4161941ce25d15082d1 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 15 Mar 2015 17:07:36 +0100
Subject: Revised semantics of comparisons between a pointer and 0.

It used to be that a pointer value (Vptr) always compare unequal to the
null pointer (Vint Int.zero).  However, this may not be true in the
final machine code when pointer addition overflows and wraps around
to the bit pattern 0.  This patch checks the validity of the pointer
being compared with 0, and makes the comparison undefined if the
pointer is out of bounds.

Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
---
 backend/Selectionproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/Selectionproof.v')

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index bb9bd592..20b6cf93 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -135,7 +135,7 @@ Proof.
   inv H. econstructor; eauto.
 (* default *)
   econstructor. constructor. eauto. constructor. 
-  simpl. inv H0. auto. auto. 
+  simpl. inv H0. auto. 
 Qed.
 
 Lemma eval_load:
-- 
cgit 


From 4622f49fd089ae47d0c853343cb0a05f986c962a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 27 Mar 2015 08:55:05 +0100
Subject: 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.
---
 backend/Selectionproof.v | 52 ++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 50 insertions(+), 2 deletions(-)

(limited to 'backend/Selectionproof.v')

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.
-- 
cgit 


From 33b742bb41725e47bd88dc12f2a4f40173023f83 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 27 Mar 2015 14:24:03 +0100
Subject: Updated the Caml part.  Added some more tests in annot1.c.

---
 backend/Selectionproof.v | 31 ++++++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 5 deletions(-)

(limited to 'backend/Selectionproof.v')

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d755d46d..392959d4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -598,6 +598,29 @@ Proof.
   exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
+Lemma sel_annot_arg_correct:
+  forall sp e e' m m',
+  env_lessdef e e' -> Mem.extends m m' ->
+  forall a v,
+  Cminor.eval_expr ge sp e m a v ->
+  exists v',
+     CminorSel.eval_annot_arg tge sp e' m' (sel_annot_arg a) v'
+  /\ Val.lessdef v v'.
+Proof.
+  intros until v. functional induction (sel_annot_arg a); intros EV.
+- inv EV. simpl in H2; inv H2. econstructor; split. constructor. 
+  unfold Genv.symbol_address. rewrite symbols_preserved. auto.
+- inv EV. simpl in H2; inv H2. econstructor; split. constructor. auto.
+- inv EV. inv H3. exploit Mem.loadv_extends; eauto. intros (v' & A & B). 
+  exists v'; split; auto. constructor. 
+  replace (Genv.symbol_address tge id ofs) with vaddr; auto.
+  simpl in H2; inv H2. unfold Genv.symbol_address. rewrite symbols_preserved. auto.
+- inv EV. inv H3. simpl in H2; inv H2. exploit Mem.loadv_extends; eauto. intros (v' & A & B). 
+  exists v'; split; auto. constructor; auto.
+- exploit sel_expr_correct; eauto. intros (v1 & A & B).
+  exists v1; split; auto. eapply eval_annot_arg; eauto.
+Qed.
+
 Lemma sel_annot_args_correct:
   forall sp e e' m m',
   env_lessdef e e' -> Mem.extends m m' ->
@@ -605,16 +628,15 @@ Lemma sel_annot_args_correct:
   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)
+                  (List.map sel_annot_arg 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).
+- exploit sel_annot_arg_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. 
+  exists (v1' :: vl'); split; auto. constructor; auto.
 Qed.
 
 (** Semantic preservation for functions and statements. *)
@@ -813,7 +835,6 @@ Proof.
   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]]]]].
-- 
cgit