From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 13 Jun 2011 18:11:19 +0000
Subject: Revised handling of annotation statements, and more generally
 built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Bounds.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'backend/Bounds.v')

diff --git a/backend/Bounds.v b/backend/Bounds.v
index 04156707..23fa3b56 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -75,6 +75,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lload chunk addr args dst => mreg_within_bounds dst
   | Lcall sig ros => size_arguments sig <= bound_outgoing b
   | Lbuiltin ef args res => mreg_within_bounds res
+  | Lannot ef args => forall s, In (S s) args -> slot_within_bounds s
   | _ => True
   end.
 
@@ -107,6 +108,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
   | Lbuiltin ef args res => res :: nil
+  | Lannot ef args => nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil
@@ -114,10 +116,18 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lreturn => nil
   end.
 
+Fixpoint slots_of_locs (l: list loc) : list slot :=
+  match l with
+  | nil => nil
+  | S s :: l' => s :: slots_of_locs l'
+  | R r :: l' => slots_of_locs l'
+  end.
+
 Definition slots_of_instr (i: instruction) : list slot :=
   match i with
   | Lgetstack s r => s :: nil
   | Lsetstack r s => s :: nil
+  | Lannot ef args => slots_of_locs args
   | _ => nil
   end.
 
@@ -343,6 +353,14 @@ Proof.
   split. simpl in H1. exact H1. eapply outgoing_slot_bound; eauto.
 Qed.
 
+Lemma slots_of_locs_charact:
+  forall s l, In s (slots_of_locs l) <-> In (S s) l.
+Proof.
+  induction l; simpl; intros. 
+  tauto.
+  destruct a; simpl; intuition congruence.
+Qed.
+
 (** It follows that every instruction in the function is within bounds, 
     in the sense of the [instr_within_bounds] predicate. *)
 
@@ -356,9 +374,16 @@ Proof.
   destruct i;
   generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); 
   simpl; intros; auto.
+(* getstack *)
   inv H0. split; auto.
+(* setstack *)
   inv H0; auto.
+(* call *)
   eapply size_arguments_bound; eauto.
+(* annot *)
+  inv H0. apply H1. rewrite slots_of_locs_charact; auto. 
+  generalize (H8 _ H3). unfold loc_acceptable, slot_valid. 
+  destruct s; (contradiction || omega).
 Qed.
 
 Lemma function_is_within_bounds:
-- 
cgit