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 --- backend/Locations.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'backend/Locations.v') diff --git a/backend/Locations.v b/backend/Locations.v index 295df28..c2fda9c 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -173,6 +173,18 @@ Module Loc. destruct s; destruct s0; intuition auto. Qed. + Lemma diff_reg_right: + forall l r, l <> R r -> diff (R r) l. + Proof. + intros. simpl. destruct l. congruence. auto. + Qed. + + Lemma diff_reg_left: + forall l r, l <> R r -> diff l (R r). + Proof. + intros. apply diff_sym. apply diff_reg_right. auto. + Qed. + (** [Loc.overlap l1 l2] returns [false] if [l1] and [l2] are different and non-overlapping, and [true] otherwise: either [l1 = l2] or they partially overlap. *) @@ -290,6 +302,14 @@ Module Loc. auto. Qed. + Lemma reg_notin: + forall r ll, ~(In (R r) ll) -> notin (R r) ll. + Proof. + induction ll; simpl; intros. auto. + split. destruct a; auto. intuition congruence. + apply IHll. intuition. + Qed. + (** [Loc.disjoint l1 l2] is true if the locations in list [l1] are different from all locations in list [l2]. *) @@ -352,6 +372,9 @@ Module Loc. | norepet_cons: forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl). +(** [Loc.no_overlap l1 l2] holds if elements of [l1] never overlap partially + with elements of [l2]. *) + Definition no_overlap (l1 l2 : list loc) := forall r, In r l1 -> forall s, In s l2 -> r = s \/ Loc.diff r s. -- cgit v1.2.3