From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001 From: xleroy 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 --- powerpc/Asmgenproof.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 3846a6c..0efe646 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -447,6 +447,7 @@ Proof. destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args); try reflexivity; autorewrite with labels; try reflexivity. case (mreg_type m); reflexivity. + case (symbol_is_small_data i i0); reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. Qed. @@ -1126,6 +1127,35 @@ Proof. intros. repeat rewrite Pregmap.gso; auto. Qed. +Lemma exec_Mannot_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list Mach.annot_param) (b : list Mach.instruction) + (vargs: list val) (t : trace) (v : val) (m' : mem), + Machsem.annot_arguments ms m sp args vargs -> + external_call ef ge vargs m t v m' -> + exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t + (Machsem.State s f sp b ms m'). +Proof. + intros; red; intros; inv MS. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + left. econstructor; split. apply plus_one. + eapply exec_step_annot. eauto. eauto. + eapply find_instr_tail; eauto. eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. + rewrite <- H1; simpl. econstructor; auto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr. auto. +Qed. + Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1458,6 +1488,7 @@ Proof exec_Mcall_prop exec_Mtailcall_prop exec_Mbuiltin_prop + exec_Mannot_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop -- cgit v1.2.3