diff options
author | 2010-06-29 08:27:14 +0000 | |
---|---|---|
committer | 2010-06-29 08:27:14 +0000 | |
commit | 9c7c84cc40eaacc1e2c13091165785cddecba5ad (patch) | |
tree | 65eafe51ad284d88fd5a949e1b2a54cd272f9f91 /powerpc/Asmgenproof.v | |
parent | f4b416882955d9d91bca60f3eb35b95f4124a5be (diff) |
Support for inlined built-ins.
AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
and a machine-dependent part (ARCH/SYS/Conventions1).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenproof.v')
-rw-r--r-- | powerpc/Asmgenproof.v | 35 |
1 files changed, 34 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index fcbbbd7..ee2867e 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -25,6 +25,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. +Require Import Conventions. Require Import Mach. Require Import Machconcr. Require Import Machtyping. @@ -1063,6 +1064,37 @@ Proof. unfold rs5; auto with ppcgen. Qed. +Lemma exec_Mbuiltin_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list mreg) (res : mreg) (b : list Mach.instruction) + (t : trace) (v : val) (m' : mem), + external_call ef ge ms ## args m t v m' -> + exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t + (Machconcr.State s f sp b (Regmap.set res v ms) m'). +Proof. + intros; red; intros; inv MS. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + replace (rs##(preg_of##args)) with (ms##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + rewrite list_map_compose. apply list_map_exten. intros. + symmetry. eapply preg_val; eauto. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + rewrite <- H0. simpl. constructor; auto. + eapply code_tail_next_int; eauto. + apply sym_not_equal. auto with ppcgen. + auto with ppcgen. +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) @@ -1345,7 +1377,7 @@ Lemma exec_function_external_prop: Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> + ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof. @@ -1387,6 +1419,7 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop + exec_Mbuiltin_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop |