From c6d2ef0c5c896a82295c1fb8a717ea29ee3c0e4d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Oct 2012 07:12:33 +0000 Subject: Make Clight independent of CompCert C. Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 789 +--------------------------------------------------- 1 file changed, 7 insertions(+), 782 deletions(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 86bba85c..51556897 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -21,174 +21,11 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import AST. - -(** * Abstract syntax *) - -(** ** Types *) - -(** Compcert C types are similar to those of C. They include numeric types, - pointers, arrays, function types, and composite types (struct and - union). Numeric types (integers and floats) fully specify the - bit size of the type. An integer type is a pair of a signed/unsigned - flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size - standing for the C99 [_Bool] type. *) - -Inductive signedness : Type := - | Signed: signedness - | Unsigned: signedness. - -Inductive intsize : Type := - | I8: intsize - | I16: intsize - | I32: intsize - | IBool: intsize. - -(** Float types come in two sizes: 32 bits (single precision) - and 64-bit (double precision). *) - -Inductive floatsize : Type := - | F32: floatsize - | F64: floatsize. - -(** Every type carries a set of attributes. Currently, only one - attribute is modeled: [volatile]. *) - -Record attr : Type := mk_attr { - attr_volatile: bool -}. - -Definition noattr := {| attr_volatile := false |}. - -(** The syntax of type expressions. Some points to note: -- Array types [Tarray n] carry the size [n] of the array. - Arrays with unknown sizes are represented by pointer types. -- Function types [Tfunction targs tres] specify the number and types - of the function arguments (list [targs]), and the type of the - function result ([tres]). Variadic functions and old-style unprototyped - functions are not supported. -- In C, struct and union types are named and compared by name. - This enables the definition of recursive struct types such as -<< - struct s1 { int n; struct * s1 next; }; ->> - Note that recursion within types must go through a pointer type. - For instance, the following is not allowed in C. -<< - struct s2 { int n; struct s2 next; }; ->> - In Compcert C, struct and union types [Tstruct id fields] and - [Tunion id fields] are compared by structure: the [fields] - argument gives the names and types of the members. The identifier - [id] is a local name which can be used in conjuction with the - [Tcomp_ptr] constructor to express recursive types. [Tcomp_ptr id] - stands for a pointer type to the nearest enclosing [Tstruct] - or [Tunion] type named [id]. For instance. the structure [s1] - defined above in C is expressed by -<< - Tstruct "s1" (Fcons "n" (Tint I32 Signed) - (Fcons "next" (Tcomp_ptr "s1") - Fnil)) ->> - Note that the incorrect structure [s2] above cannot be expressed at - all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing - structure or union, but not to the structure or union directly. -*) - -Inductive type : Type := - | Tvoid: type (**r the [void] type *) - | Tint: intsize -> signedness -> attr -> type (**r integer types *) - | Tfloat: floatsize -> attr -> type (**r floating-point types *) - | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) - | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) - | Tfunction: typelist -> type -> type (**r function types *) - | Tstruct: ident -> fieldlist -> attr -> type (**r struct types *) - | Tunion: ident -> fieldlist -> attr -> type (**r union types *) - | Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *) - -with typelist : Type := - | Tnil: typelist - | Tcons: type -> typelist -> typelist - -with fieldlist : Type := - | Fnil: fieldlist - | Fcons: ident -> type -> fieldlist -> fieldlist. - -Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} -with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} -with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. -Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. - assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec. - generalize ident_eq zeq. intros E1 E2. - decide equality. - decide equality. - generalize ident_eq. intros E1. - decide equality. -Defined. - -Opaque type_eq typelist_eq fieldlist_eq. - -(** Extract the attributes of a type. *) - -Definition attr_of_type (ty: type) := - match ty with - | Tvoid => noattr - | Tint sz si a => a - | Tfloat sz a => a - | Tpointer elt a => a - | Tarray elt sz a => a - | Tfunction args res => noattr - | Tstruct id fld a => a - | Tunion id fld a => a - | Tcomp_ptr id a => a - end. - -Definition type_int32s := Tint I32 Signed noattr. -Definition type_bool := Tint IBool Signed noattr. - -(** The usual unary conversion. Promotes small integer types to [signed int32] - and degrades array types and function types to pointer types. *) - -Definition typeconv (ty: type) : type := - match ty with - | Tint I32 Unsigned _ => ty - | Tint _ _ a => Tint I32 Signed a - | Tarray t sz a => Tpointer t a - | Tfunction _ _ => Tpointer ty noattr - | _ => ty - end. +Require Import Ctypes. +Require Import Cop. (** ** Expressions *) -(** Arithmetic and logical operators. *) - -Inductive unary_operation : Type := - | Onotbool : unary_operation (**r boolean negation ([!] in C) *) - | Onotint : unary_operation (**r integer complement ([~] in C) *) - | Oneg : unary_operation. (**r opposite (unary [-]) *) - -Inductive binary_operation : Type := - | Oadd : binary_operation (**r addition (binary [+]) *) - | Osub : binary_operation (**r subtraction (binary [-]) *) - | Omul : binary_operation (**r multiplication (binary [*]) *) - | Odiv : binary_operation (**r division ([/]) *) - | Omod : binary_operation (**r remainder ([%]) *) - | Oand : binary_operation (**r bitwise and ([&]) *) - | Oor : binary_operation (**r bitwise or ([|]) *) - | Oxor : binary_operation (**r bitwise xor ([^]) *) - | Oshl : binary_operation (**r left shift ([<<]) *) - | Oshr : binary_operation (**r right shift ([>>]) *) - | Oeq: binary_operation (**r comparison ([==]) *) - | One: binary_operation (**r comparison ([!=]) *) - | Olt: binary_operation (**r comparison ([<]) *) - | Ogt: binary_operation (**r comparison ([>]) *) - | Ole: binary_operation (**r comparison ([<=]) *) - | Oge: binary_operation. (**r comparison ([>=]) *) - -Inductive incr_or_decr : Type := Incr | Decr. - (** Compcert C expressions are almost identical to those of C. The only omission is string literals. Some operators are treated as derived forms: array indexing, pre-increment, pre-decrement, and @@ -356,24 +193,8 @@ Inductive fundef : Type := | Internal: function -> fundef | External: external_function -> typelist -> type -> fundef. -(** ** Programs *) - -(** A program is a collection of named functions, plus a collection - of named global variables, carrying their types and optional initialization - data. See module [AST] for more details. *) - -Definition program : Type := AST.program fundef type. - -(** * Operations over types *) - (** The type of a function definition. *) -Fixpoint type_of_params (params: list (ident * type)) : typelist := - match params with - | nil => Tnil - | (id, ty) :: rem => Tcons ty (type_of_params rem) - end. - Definition type_of_function (f: function) : type := Tfunction (type_of_params (fn_params f)) (fn_return f). @@ -383,606 +204,10 @@ Definition type_of_fundef (f: fundef) : type := | External id args res => Tfunction args res end. -(** Natural alignment of a type, in bytes. *) - -Fixpoint alignof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' _ _ => alignof t' - | Tfunction _ _ => 1 - | Tstruct _ fld _ => alignof_fields fld - | Tunion _ fld _ => alignof_fields fld - | Tcomp_ptr _ _ => 4 - end - -with alignof_fields (f: fieldlist) : Z := - match f with - | Fnil => 1 - | Fcons id t f' => Zmax (alignof t) (alignof_fields f') - end. - -Scheme type_ind2 := Induction for type Sort Prop - with fieldlist_ind2 := Induction for fieldlist Sort Prop. - -Lemma alignof_1248: - forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8 -with alignof_fields_1248: - forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8. -Proof. - induction t; simpl; auto. - destruct i; auto. - destruct f; auto. - induction f; simpl; auto. - rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto. -Qed. - -Lemma alignof_pos: - forall t, alignof t > 0. -Proof. - intros. generalize (alignof_1248 t). omega. -Qed. - -Lemma alignof_fields_pos: - forall f, alignof_fields f > 0. -Proof. - intros. generalize (alignof_fields_1248 f). omega. -Qed. - -(** Size of a type, in bytes. *) - -Fixpoint sizeof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' n _ => sizeof t' * Zmax 1 n - | Tfunction _ _ => 1 - | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) - | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) - | Tcomp_ptr _ _ => 4 - end - -with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := - match fld with - | Fnil => pos - | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t) - end - -with sizeof_union (fld: fieldlist) : Z := - match fld with - | Fnil => 0 - | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld') - end. - -Lemma sizeof_pos: - forall t, sizeof t > 0. -Proof. - intro t0. - apply (type_ind2 (fun t => sizeof t > 0) - (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0)); - intros; simpl; auto; try omega. - destruct i; omega. - destruct f; omega. - apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. - destruct H. - generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_struct f 0)). omega. - generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_union f)). omega. - split. omega. auto. - destruct H0. split; intros. - generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. - apply H1. - generalize (align_le pos (alignof t) (alignof_pos t)). omega. -Qed. - -Lemma sizeof_struct_incr: - forall fld pos, pos <= sizeof_struct fld pos. -Proof. - induction fld; intros; simpl. omega. - eapply Zle_trans. 2: apply IHfld. - apply Zle_trans with (align pos (alignof t)). - apply align_le. apply alignof_pos. - assert (sizeof t > 0) by apply sizeof_pos. omega. -Qed. - -Lemma sizeof_alignof_compat: - forall t, (alignof t | sizeof t). -Proof. - induction t; simpl; try (apply Zdivide_refl). - apply Zdivide_mult_l. auto. - apply align_divides. apply alignof_fields_pos. - apply align_divides. apply alignof_fields_pos. -Qed. - -(** Byte offset for a field in a struct or union. - Field are laid out consecutively, and padding is inserted - to align each field to the natural alignment for its type. *) - -Open Local Scope string_scope. - -Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) - {struct fld} : res Z := - match fld with - | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) - | Fcons id' t fld' => - if ident_eq id id' - then OK (align pos (alignof t)) - else field_offset_rec id fld' (align pos (alignof t) + sizeof t) - end. - -Definition field_offset (id: ident) (fld: fieldlist) : res Z := - field_offset_rec id fld 0. - -Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type := - match fld with - | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) - | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld' - end. - -(** Some sanity checks about field offsets. First, field offsets are - within the range of acceptable offsets. *) - -Remark field_offset_rec_in_range: - forall id ofs ty fld pos, - field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> - pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos. -Proof. - intros until ty. induction fld; simpl. - congruence. - destruct (ident_eq id i); intros. - inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. - exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)). - apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. -Qed. - -Lemma field_offset_in_range: - forall sid fld a fid ofs ty, - field_offset fid fld = OK ofs -> field_type fid fld = OK ty -> - 0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a). -Proof. - intros. exploit field_offset_rec_in_range; eauto. intros [A B]. - split. auto. simpl. eapply Zle_trans. eauto. - eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_fields_pos. -Qed. - -(** Second, two distinct fields do not overlap *) - -Lemma field_offset_no_overlap: - forall id1 ofs1 ty1 id2 ofs2 ty2 fld, - field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 -> - field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 -> - id1 <> id2 -> - ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1. -Proof. - intros until ty2. intros fld0 A B C D NEQ. - assert (forall fld pos, - field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 -> - field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 -> - ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1). - induction fld; intro pos; simpl. congruence. - destruct (ident_eq id1 i); destruct (ident_eq id2 i). - congruence. - subst i. intros. inv H; inv H0. - exploit field_offset_rec_in_range. eexact H1. eauto. tauto. - subst i. intros. inv H1; inv H2. - exploit field_offset_rec_in_range. eexact H. eauto. tauto. - intros. eapply IHfld; eauto. - - apply H with fld0 0; auto. -Qed. - -(** Third, if a struct is a prefix of another, the offsets of common fields - are the same. *) - -Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist := - match fld1 with - | Fnil => fld2 - | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2) - end. - -Lemma field_offset_prefix: - forall id ofs fld2 fld1, - field_offset id fld1 = OK ofs -> - field_offset id (fieldlist_app fld1 fld2) = OK ofs. -Proof. - intros until fld2. - assert (forall fld1 pos, - field_offset_rec id fld1 pos = OK ofs -> - field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs). - induction fld1; intros pos; simpl. congruence. - destruct (ident_eq id i); auto. - intros. unfold field_offset; auto. -Qed. - -(** Fourth, the position of each field respects its alignment. *) - -Lemma field_offset_aligned: - forall id fld ofs ty, - field_offset id fld = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs). -Proof. - assert (forall id ofs ty fld pos, - field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs)). - induction fld; simpl; intros. - discriminate. - destruct (ident_eq id i). inv H; inv H0. - apply align_divides. apply alignof_pos. - eapply IHfld; eauto. - intros. eapply H with (pos := 0); eauto. -Qed. - -(** The [access_mode] function describes how a l-value of the given -type must be accessed: -- [By_value ch]: access by value, i.e. by loading from the address - of the l-value using the memory chunk [ch]; -- [By_reference]: access by reference, i.e. by just returning - the address of the l-value (used for arrays and functions); -- [By_copy]: access is by reference, assignment is by copy - (used for [struct] and [union] types) -- [By_nothing]: no access is possible, e.g. for the [void] type. -*) - -Inductive mode: Type := - | By_value: memory_chunk -> mode - | By_reference: mode - | By_copy: mode - | By_nothing: mode. - -Definition access_mode (ty: type) : mode := - match ty with - | Tint I8 Signed _ => By_value Mint8signed - | Tint I8 Unsigned _ => By_value Mint8unsigned - | Tint I16 Signed _ => By_value Mint16signed - | Tint I16 Unsigned _ => By_value Mint16unsigned - | Tint I32 _ _ => By_value Mint32 - | Tint IBool _ _ => By_value Mint8unsigned - | Tfloat F32 _ => By_value Mfloat32 - | Tfloat F64 _ => By_value Mfloat64 - | Tvoid => By_nothing - | Tpointer _ _ => By_value Mint32 - | Tarray _ _ _ => By_reference - | Tfunction _ _ => By_reference - | Tstruct _ _ _ => By_copy - | Tunion _ _ _ => By_copy - | Tcomp_ptr _ _ => By_nothing -end. - -(** For the purposes of the semantics and the compiler, a type denotes - a volatile access if it carries the [volatile] attribute and it is - accessed by value. *) - -Definition type_is_volatile (ty: type) : bool := - match access_mode ty with - | By_value _ => attr_volatile (attr_of_type ty) - | _ => false - end. - -(** Unroll the type of a structure or union field, substituting - [Tcomp_ptr] by a pointer to the structure. *) - -Section UNROLL_COMPOSITE. - -Variable cid: ident. -Variable comp: type. - -Fixpoint unroll_composite (ty: type) : type := - match ty with - | Tvoid => ty - | Tint _ _ _ => ty - | Tfloat _ _ => ty - | Tpointer t1 a => Tpointer (unroll_composite t1) a - | Tarray t1 sz a => Tarray (unroll_composite t1) sz a - | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2) - | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a - | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a - | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty - end - -with unroll_composite_list (tl: typelist) : typelist := - match tl with - | Tnil => Tnil - | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl') - end - -with unroll_composite_fields (fld: fieldlist) : fieldlist := - match fld with - | Fnil => Fnil - | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld') - end. - -Lemma alignof_unroll_composite: - forall ty, alignof (unroll_composite ty) = alignof ty. -Proof. - apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty) - (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld)); - simpl; intros; auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - decEq; auto. -Qed. - -Lemma sizeof_unroll_composite: - forall ty, sizeof (unroll_composite ty) = sizeof ty. -Proof. -Opaque alignof. - apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty) - (fun fld => - sizeof_union (unroll_composite_fields fld) = sizeof_union fld - /\ forall pos, - sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); - simpl; intros; auto. - congruence. - destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto. - destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto. - destruct (ident_eq i cid); auto. - destruct H0. split. congruence. - intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto. -Qed. - -End UNROLL_COMPOSITE. - -(** Classification of arithmetic operations and comparisons. - The following [classify_] functions take as arguments the types - of the arguments of an operation. They return enough information - to resolve overloading for this operator applications, such as - ``both arguments are floats'', or ``the first is a pointer - and the second is an integer''. These functions are used to resolve - overloading both in the dynamic semantics (module [Csem]), in the - type system (module [Ctyping]), and in the compiler (module - [Cshmgen]). -*) - -Inductive classify_neg_cases : Type := - | neg_case_i(s: signedness) (**r int *) - | neg_case_f (**r float *) - | neg_default. - -Definition classify_neg (ty: type) : classify_neg_cases := - match ty with - | Tint I32 Unsigned _ => neg_case_i Unsigned - | Tint _ _ _ => neg_case_i Signed - | Tfloat _ _ => neg_case_f - | _ => neg_default - end. - -Inductive classify_notint_cases : Type := - | notint_case_i(s: signedness) (**r int *) - | notint_default. - -Definition classify_notint (ty: type) : classify_notint_cases := - match ty with - | Tint I32 Unsigned _ => notint_case_i Unsigned - | Tint _ _ _ => notint_case_i Signed - | _ => notint_default - end. - -(** The following describes types that can be interpreted as a boolean: - integers, floats, pointers. It is used for the semantics of - the [!] and [?] operators, as well as the [if], [while], [for] statements. *) - -Inductive classify_bool_cases : Type := - | bool_case_i (**r integer *) - | bool_case_f (**r float *) - | bool_case_p (**r pointer *) - | bool_default. - -Definition classify_bool (ty: type) : classify_bool_cases := - match typeconv ty with - | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p - | Tfloat _ _ => bool_case_f - | _ => bool_default - end. - -Inductive classify_add_cases : Type := - | add_case_ii(s: signedness) (**r int, int *) - | add_case_ff (**r float, float *) - | add_case_if(s: signedness) (**r int, float *) - | add_case_fi(s: signedness) (**r float, int *) - | add_case_pi(ty: type)(a: attr) (**r pointer, int *) - | add_case_ip(ty: type)(a: attr) (**r int, pointer *) - | add_default. - -Definition classify_add (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => add_case_ii Signed - | Tfloat _ _, Tfloat _ _ => add_case_ff - | Tint _ sg _, Tfloat _ _ => add_case_if sg - | Tfloat _ _, Tint _ sg _ => add_case_fi sg - | Tpointer ty a, Tint _ _ _ => add_case_pi ty a - | Tint _ _ _, Tpointer ty a => add_case_ip ty a - | _, _ => add_default - end. - -Inductive classify_sub_cases : Type := - | sub_case_ii(s: signedness) (**r int , int *) - | sub_case_ff (**r float , float *) - | sub_case_if(s: signedness) (**r int, float *) - | sub_case_fi(s: signedness) (**r float, int *) - | sub_case_pi(ty: type) (**r pointer, int *) - | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_default. - -Definition classify_sub (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => sub_case_ff - | Tint _ sg _, Tfloat _ _ => sub_case_if sg - | Tfloat _ _, Tint _ sg _ => sub_case_fi sg - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty - | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty - | _ ,_ => sub_default - end. - -Inductive classify_mul_cases : Type:= - | mul_case_ii(s: signedness) (**r int , int *) - | mul_case_ff (**r float , float *) - | mul_case_if(s: signedness) (**r int, float *) - | mul_case_fi(s: signedness) (**r float, int *) - | mul_default. - -Definition classify_mul (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => mul_case_ff - | Tint _ sg _, Tfloat _ _ => mul_case_if sg - | Tfloat _ _, Tint _ sg _ => mul_case_fi sg - | _,_ => mul_default -end. - -Inductive classify_div_cases : Type:= - | div_case_ii(s: signedness) (**r int , int *) - | div_case_ff (**r float , float *) - | div_case_if(s: signedness) (**r int, float *) - | div_case_fi(s: signedness) (**r float, int *) - | div_default. - -Definition classify_div (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => div_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => div_case_ff - | Tint _ sg _, Tfloat _ _ => div_case_if sg - | Tfloat _ _, Tint _ sg _ => div_case_fi sg - | _,_ => div_default -end. - -(** The following is common to binary integer-only operators: - modulus, bitwise "and", "or", and "xor". *) - -Inductive classify_binint_cases : Type:= - | binint_case_ii(s: signedness) (**r int , int *) - | binint_default. - -Definition classify_binint (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed - | _,_ => binint_default -end. - -(** The following is common to shift operators [<<] and [>>]. *) - -Inductive classify_shift_cases : Type:= - | shift_case_ii(s: signedness) (**r int , int *) - | shift_default. - -Definition classify_shift (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed - | _,_ => shift_default -end. - -Inductive classify_cmp_cases : Type:= - | cmp_case_ii(s: signedness) (**r int, int *) - | cmp_case_pp (**r pointer, pointer *) - | cmp_case_ff (**r float , float *) - | cmp_case_if(s: signedness) (**r int, float *) - | cmp_case_fi(s: signedness) (**r float, int *) - | cmp_default. - -Definition classify_cmp (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => cmp_case_ff - | Tint _ sg _, Tfloat _ _ => cmp_case_if sg - | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg - | Tpointer _ _ , Tpointer _ _ => cmp_case_pp - | Tpointer _ _ , Tint _ _ _ => cmp_case_pp - | Tint _ _ _, Tpointer _ _ => cmp_case_pp - | _ , _ => cmp_default - end. - -Inductive classify_fun_cases : Type:= - | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *) - | fun_default. - -Definition classify_fun (ty: type) := - match ty with - | Tfunction args res => fun_case_f args res - | Tpointer (Tfunction args res) _ => fun_case_f args res - | _ => fun_default - end. - -Inductive classify_cast_cases : Type := - | cast_case_neutral (**r int|pointer -> int32|pointer *) - | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) - | cast_case_f2f (sz2:floatsize) (**r float -> float *) - | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) - | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) - | cast_case_f2bool (**r float -> bool *) - | cast_case_p2bool (**r pointer -> bool *) - | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) - | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) - | cast_case_void (**r any -> void *) - | cast_case_default. - -Function classify_cast (tfrom tto: type) : classify_cast_cases := - match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral - | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool - | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 - | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 - | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 - | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral - | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 - | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 - | Tvoid, _ => cast_case_void - | _, _ => cast_case_default - end. - -(** Translating C types to Cminor types, function signatures, - and external functions. *) - -Definition typ_of_type (t: type) : AST.typ := - match t with - | Tfloat _ _ => AST.Tfloat - | _ => AST.Tint - end. - -Definition opttyp_of_type (t: type) : option AST.typ := - match t with - | Tvoid => None - | Tfloat _ _ => Some AST.Tfloat - | _ => Some AST.Tint - end. +(** ** Programs *) -Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := - match tl with - | Tnil => nil - | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl - end. +(** A program is a collection of named functions, plus a collection + of named global variables, carrying their types and optional initialization + data. See module [AST] for more details. *) -Definition signature_of_type (args: typelist) (res: type) : signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res). +Definition program : Type := AST.program fundef type. -- cgit