From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jun 2010 08:27:14 +0000 Subject: 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 --- common/AST.v | 18 +++++++- common/Events.v | 6 +-- common/Memdata.v | 13 ------ common/Memory.v | 130 +++++++++++++++++++++++++++---------------------------- 4 files changed, 84 insertions(+), 83 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 861795c..bca0535 100644 --- a/common/AST.v +++ b/common/AST.v @@ -82,6 +82,19 @@ Inductive memory_chunk : Type := | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) | Mfloat64 : memory_chunk. (**r 64-bit double-precision float *) +(** The type (integer/pointer or float) of a chunk. *) + +Definition type_of_chunk (c: memory_chunk) : typ := + match c with + | Mint8signed => Tint + | Mint8unsigned => Tint + | Mint16signed => Tint + | Mint16unsigned => Tint + | Mint32 => Tint + | Mfloat32 => Tfloat + | Mfloat64 => Tfloat + end. + (** Initialization data for global variables. *) Inductive init_data: Type := @@ -390,9 +403,12 @@ Qed. Record external_function : Type := mkextfun { ef_id: ident; - ef_sig: signature + ef_sig: signature; + ef_inline: bool }. +(** Function definitions are the union of internal and external functions. *) + Inductive fundef (F: Type): Type := | Internal: F -> fundef F | External: external_function -> fundef F. diff --git a/common/Events.v b/common/Events.v index 329f31c..a5c82d0 100644 --- a/common/Events.v +++ b/common/Events.v @@ -400,7 +400,7 @@ End EVENTVAL_INV. (** Each external function is of one of the following kinds: *) Inductive extfun_kind: signature -> Type := - | EF_syscall (sg: signature) (name: ident): extfun_kind sg + | EF_syscall (name: ident) (sg: signature): extfun_kind sg (** A system call. Takes integer-or-float arguments, produces a result that is an integer or a float, does not modify the memory, and produces an [Event_syscall] event in the trace. *) @@ -985,7 +985,7 @@ This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := match classify_external_function ef with - | EF_syscall sg name => extcall_io_sem name sg + | EF_syscall name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem @@ -994,7 +994,7 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef.(ef_sig)). + extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call. destruct (classify_external_function ef). apply extcall_io_ok. diff --git a/common/Memdata.v b/common/Memdata.v index 94a9917..20c0b10 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -103,19 +103,6 @@ Proof. destruct chunk1; destruct chunk2; simpl; congruence. Qed. -(** The type (integer/pointer or float) of a chunk. *) - -Definition type_of_chunk (c: memory_chunk) : typ := - match c with - | Mint8signed => Tint - | Mint8unsigned => Tint - | Mint16signed => Tint - | Mint16unsigned => Tint - | Mint32 => Tint - | Mfloat32 => Tfloat - | Mfloat64 => Tfloat - end. - (** * Memory values *) (** A ``memory value'' is a byte-sized quantity that describes the current diff --git a/common/Memory.v b/common/Memory.v index 4d65c5c..1fb7816 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -80,9 +80,7 @@ Lemma mkmem_ext: mkmem cont1 acc1 bound1 next1 a1 b1 c1 d1 = mkmem cont2 acc2 bound2 next2 a2 b2 c2 d2. Proof. -intros. -subst. -f_equal; apply proof_irr. + intros. subst. f_equal; apply proof_irr. Qed. (** * Validity of blocks and accesses *) @@ -1699,78 +1697,78 @@ Hint Local Resolve valid_block_free_1 valid_block_free_2 Lemma mem_access_ext: forall m1 m2, perm m1 = perm m2 -> mem_access m1 = mem_access m2. Proof. -intros. -apply extensionality; intro b. -apply extensionality; intro ofs. -case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition). -unfold perm, perm_order' in H2,H3. -rewrite H0 in H2,H3; rewrite H1 in H2,H3. -f_equal. -assert (perm_order p p0 -> perm_order p0 p -> p0=p) by - (clear; intros; inv H; inv H0; auto). -intuition. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. -assert (perm_order p p) by auto with mem. -intuition. -assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). -unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. -assert (perm_order p p) by auto with mem. -intuition. + intros. + apply extensionality; intro b. + apply extensionality; intro ofs. + case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition). + unfold perm, perm_order' in H2,H3. + rewrite H0 in H2,H3; rewrite H1 in H2,H3. + f_equal. + assert (perm_order p p0 -> perm_order p0 p -> p0=p) by + (clear; intros; inv H; inv H0; auto). + intuition. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. + assert (perm_order p p) by auto with mem. + intuition. + assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). + unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. + assert (perm_order p p) by auto with mem. + intuition. Qed. Lemma mem_ext': forall m1 m2, - mem_access m1 = mem_access m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> - mem_contents m1 b ofs = mem_contents m2 b ofs) -> - m1 = m2. + mem_access m1 = mem_access m2 -> + nextblock m1 = nextblock m2 -> + (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> + (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> + mem_contents m1 b ofs = mem_contents m2 b ofs) -> + m1 = m2. Proof. -intros. -destruct m1; destruct m2; simpl in *. -destruct H; subst. -apply mkmem_ext; auto. -apply extensionality; intro b. -apply extensionality; intro ofs. -destruct (perm_order'_dec (mem_access0 b ofs) Readable). -auto. -destruct (noread_undef0 b ofs); try contradiction. -destruct (noread_undef1 b ofs); try contradiction. -congruence. -apply extensionality; intro b. -destruct (nextblock_noaccess0 b); auto. -destruct (nextblock_noaccess1 b); auto. -congruence. + intros. + destruct m1; destruct m2; simpl in *. + destruct H; subst. + apply mkmem_ext; auto. + apply extensionality; intro b. + apply extensionality; intro ofs. + destruct (perm_order'_dec (mem_access0 b ofs) Readable). + auto. + destruct (noread_undef0 b ofs); try contradiction. + destruct (noread_undef1 b ofs); try contradiction. + congruence. + apply extensionality; intro b. + destruct (nextblock_noaccess0 b); auto. + destruct (nextblock_noaccess1 b); auto. + congruence. Qed. Theorem mem_ext: - forall m1 m2, - perm m1 = perm m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) -> - m1 = m2. + forall m1 m2, + perm m1 = perm m2 -> + nextblock m1 = nextblock m2 -> + (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> + (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) -> + m1 = m2. Proof. -intros. -generalize (mem_access_ext _ _ H); clear H; intro. -apply mem_ext'; auto. -intros. -specialize (H2 b ofs). -unfold loadbytes in H2; simpl in H2. -destruct (range_perm_dec m1 b ofs (ofs+1)). -destruct (range_perm_dec m2 b ofs (ofs+1)). -inv H2; auto. -contradict n. -intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. -unfold perm, perm_order'. - rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition. -contradict n. -intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. -unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition. + intros. + generalize (mem_access_ext _ _ H); clear H; intro. + apply mem_ext'; auto. + intros. + specialize (H2 b ofs). + unfold loadbytes in H2; simpl in H2. + destruct (range_perm_dec m1 b ofs (ofs+1)). + destruct (range_perm_dec m2 b ofs (ofs+1)). + inv H2; auto. + contradict n. + intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. + unfold perm, perm_order'. + rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition. + contradict n. + intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. + unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition. Qed. (** * Generic injections *) -- cgit v1.2.3