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
---
 arm/Asmgenproof1.v | 44 ++++++++++++++++++++++++++++++++++++++------
 1 file changed, 38 insertions(+), 6 deletions(-)

(limited to 'arm/Asmgenproof1.v')

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 9312f309..d6ad203a 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -337,14 +337,14 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machsem.extcall_args ms m sp ll vl ->
-  exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
+  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
+  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
-  induction 3.
-  exists (@nil val); split; constructor.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
   exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  exploit IHextcall_args; eauto. intros [vl' [C D]].
-  exists(v1' :: vl'); split. constructor; auto. constructor; auto.
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
 Lemma extcall_arguments_match:
@@ -358,6 +358,38 @@ Proof.
   eapply extcall_args_match; eauto.
 Qed.
 
+(** Translation of arguments to annotations. *)
+
+Lemma annot_arg_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Machsem.annot_arg ms m sp p v ->
+  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1; simpl.
+(* reg *)
+  exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto.
+(* stack *)
+  exploit Mem.load_extends; eauto. intros [v' [A B]].
+  exists v'; split; auto. 
+  inv H. econstructor; eauto. 
+Qed.
+
+Lemma annot_arguments_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall pl vl,
+  Machsem.annot_arguments ms m sp pl vl ->
+  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
+           /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros. 
+  exists (@nil val); split. constructor. constructor.
+  exploit annot_arg_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
 (** * Execution of straight-line code *)
 
 Section STRAIGHTLINE.
-- 
cgit