From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 398 ++++++++++++++++++++++++++++------------------------ 1 file changed, 211 insertions(+), 187 deletions(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c76d9b95..ffe08bfa 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -30,7 +30,8 @@ Require Import AST. 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. *) + 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 @@ -39,7 +40,8 @@ Inductive signedness : Type := Inductive intsize : Type := | I8: intsize | I16: intsize - | I32: intsize. + | I32: intsize + | IBool: intsize. (** Float types come in two sizes: 32 bits (single precision) and 64-bit (double precision). *) @@ -48,6 +50,15 @@ 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. @@ -84,15 +95,15 @@ Inductive floatsize : Type := *) Inductive type : Type := - | Tvoid: type (**r the [void] type *) - | Tint: intsize -> signedness -> type (**r integer types *) - | Tfloat: floatsize -> type (**r floating-point types *) - | Tpointer: type -> type (**r pointer types ([*ty]) *) - | Tarray: type -> Z -> type (**r array types ([ty[len]]) *) - | Tfunction: typelist -> type -> type (**r function types *) - | Tstruct: ident -> fieldlist -> type (**r struct types *) - | Tunion: ident -> fieldlist -> type (**r union types *) - | Tcomp_ptr: ident -> type (**r pointer to named struct or union *) + | 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 @@ -102,16 +113,51 @@ 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 _ _ => Tint I32 Signed - | Tarray t sz => Tpointer t - | Tfunction _ _ => Tpointer ty - | _ => ty + | Tint I32 Unsigned _ => ty + | Tint _ _ a => Tint I32 Signed a + | Tarray t sz a => Tpointer t a + | Tfunction _ _ => Tpointer ty noattr + | _ => ty end. (** ** Expressions *) @@ -207,33 +253,31 @@ as [*(r1 + r2)]. *) Definition Eindex (r1 r2: expr) (ty: type) := - Ederef (Ebinop Oadd r1 r2 (Tpointer ty)) ty. + Ederef (Ebinop Oadd r1 r2 (Tpointer ty noattr)) ty. (** Pre-increment [++l] and pre-decrement [--l] are expressed as [l += 1] and [l -= 1], respectively. *) Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Eassignop (match id with Incr => Oadd | Decr => Osub end) - l (Eval (Vint Int.one) (Tint I32 Signed)) (typeconv ty) ty. + l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty. -(** Sequential ``and'' [r1 && r2] is viewed as two conditionals - [r1 ? (r2 ? 1 : 0) : 0]. *) +(** Sequential ``and'' [r1 && r2] is viewed as a conditional and a cast: + [r1 ? (_Bool) r2 : 0]. *) Definition Eseqand (r1 r2: expr) (ty: type) := Econdition r1 - (Econdition r2 (Eval (Vint Int.one) (Tint I32 Signed)) - (Eval (Vint Int.zero) (Tint I32 Signed)) ty) - (Eval (Vint Int.zero) (Tint I32 Signed)) + (Ecast r2 type_bool) + (Eval (Vint Int.zero) type_int32s) ty. -(** Sequential ``or'' [r1 || r2] is viewed as two conditionals - [r1 ? 1 : (r2 ? 1 : 0)]. *) +(** Sequential ``or'' [r1 || r2] is viewed as a conditional and a cast: + [r1 ? 1 : (_Bool) r2]. *) Definition Eseqor (r1 r2: expr) (ty: type) := Econdition r1 - (Eval (Vint Int.one) (Tint I32 Signed)) - (Econdition r2 (Eval (Vint Int.one) (Tint I32 Signed)) - (Eval (Vint Int.zero) (Tint I32 Signed)) ty) + (Eval (Vint Int.one) type_int32s) + (Ecast r2 type_bool) ty. (** Extract the type part of a type-annotated expression. *) @@ -353,17 +397,18 @@ Definition type_of_fundef (f: fundef) : type := Fixpoint alignof (t: type) : Z := match t with | Tvoid => 1 - | Tint I8 _ => 1 - | Tint I16 _ => 2 - | Tint I32 _ => 4 - | Tfloat F32 => 4 - | Tfloat F64 => 8 - | Tpointer _ => 4 - | Tarray t' n => alignof t' + | 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 + | Tstruct _ fld _ => alignof_fields fld + | Tunion _ fld _ => alignof_fields fld + | Tcomp_ptr _ _ => 4 end with alignof_fields (f: fieldlist) : Z := @@ -375,90 +420,47 @@ with alignof_fields (f: fieldlist) : Z := Scheme type_ind2 := Induction for type Sort Prop with fieldlist_ind2 := Induction for fieldlist Sort Prop. -Lemma alignof_power_of_2: - forall t, exists n, alignof t = two_power_nat n -with alignof_fields_power_of_2: - forall f, exists n, alignof_fields f = two_power_nat n. +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. - exists 0%nat; auto. - destruct i. exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto. - destruct f. exists 2%nat; auto. exists 3%nat; auto. - exists 2%nat; auto. - auto. - exists 0%nat; auto. - apply alignof_fields_power_of_2. - apply alignof_fields_power_of_2. - exists 2%nat; auto. - induction f; simpl. - exists 0%nat; auto. + 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. destruct (alignof_power_of_2 t) as [p EQ]. rewrite EQ. apply two_power_nat_pos. + intros. generalize (alignof_1248 t). omega. Qed. Lemma alignof_fields_pos: forall f, alignof_fields f > 0. Proof. - intros. destruct (alignof_fields_power_of_2 f) as [p EQ]. rewrite EQ. apply two_power_nat_pos. -Qed. - -(* -Fixpoint In_fieldlist (id: ident) (ty: type) (f: fieldlist) : Prop := - match f with - | Fnil => False - | Fcons id1 ty1 f1 => (id1 = id /\ ty1 = ty) \/ In_fieldlist id ty f1 - end. - -Remark divides_max_pow_two: - forall a b, - (two_power_nat b | Zmax (two_power_nat a) (two_power_nat b)). -Proof. - intros. - rewrite Zmax_spec. destruct (zlt (two_power_nat b) (two_power_nat a)). - repeat rewrite two_power_nat_two_p in *. - destruct (zle (Z_of_nat a) (Z_of_nat b)). - assert (two_p (Z_of_nat a) <= two_p (Z_of_nat b)). apply two_p_monotone; omega. - omegaContradiction. - exists (two_p (Z_of_nat a - Z_of_nat b)). - rewrite <- two_p_is_exp. decEq. omega. omega. omega. - apply Zdivide_refl. + intros. generalize (alignof_fields_1248 f). omega. Qed. -Lemma alignof_each_field: - forall f id t, In_fieldlist id t f -> (alignof t | alignof_fields f). -Proof. - induction f; simpl; intros. - contradiction. - destruct (alignof_power_of_2 t) as [k1 EQ1]. - destruct (alignof_fields_power_of_2 f) as [k2 EQ2]. - destruct H as [[A B] | A]; subst; rewrite EQ1; rewrite EQ2. - rewrite Zmax_comm. apply divides_max_pow_two. - eapply Zdivide_trans. eapply IHf; eauto. - rewrite EQ2. apply divides_max_pow_two. -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 - | Tfloat F32 => 4 - | Tfloat F64 => 8 - | Tpointer _ => 4 - | Tarray t' n => sizeof t' * Zmax 1 n + | 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 + | 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 := @@ -557,9 +559,9 @@ Proof. Qed. Lemma field_offset_in_range: - forall sid fld fid ofs ty, + 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). + 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. @@ -638,33 +640,47 @@ 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; + 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 - | Tfloat F32 => By_value Mfloat32 - | Tfloat F64 => By_value Mfloat64 + | 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 + | Tpointer _ _ => By_value Mint32 + | Tarray _ _ _ => By_reference | Tfunction _ _ => By_reference - | Tstruct _ fList => By_nothing - | Tunion _ fList => By_nothing - | Tcomp_ptr _ => By_nothing + | 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. *) @@ -676,14 +692,14 @@ Variable comp: type. Fixpoint unroll_composite (ty: type) : type := match ty with | Tvoid => ty - | Tint _ _ => ty - | Tfloat _ => ty - | Tpointer t1 => Tpointer (unroll_composite t1) - | Tarray t1 sz => Tarray (unroll_composite t1) sz + | 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 => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) - | Tunion id fld => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) - | Tcomp_ptr id => if ident_eq id cid then Tpointer comp else ty + | 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 := @@ -721,9 +737,9 @@ Opaque alignof. sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); simpl; intros; auto. congruence. - destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f)). + 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)). + 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. @@ -750,9 +766,9 @@ Inductive classify_neg_cases : Type := 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 + | Tint I32 Unsigned _ => neg_case_i Unsigned + | Tint _ _ _ => neg_case_i Signed + | Tfloat _ _ => neg_case_f | _ => neg_default end. @@ -762,8 +778,8 @@ Inductive classify_notint_cases : Type := Definition classify_notint (ty: type) : classify_notint_cases := match ty with - | Tint I32 Unsigned => notint_case_i Unsigned - | Tint _ _ => notint_case_i Signed + | Tint I32 Unsigned _ => notint_case_i Unsigned + | Tint _ _ _ => notint_case_i Signed | _ => notint_default end. @@ -778,9 +794,9 @@ Inductive classify_bool_cases : Type := Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with - | Tint _ _ => bool_case_ip - | Tpointer _ => bool_case_ip - | Tfloat _ => bool_case_f + | Tint _ _ _ => bool_case_ip + | Tpointer _ _ => bool_case_ip + | Tfloat _ _ => bool_case_f | _ => bool_default end. @@ -789,20 +805,20 @@ Inductive classify_add_cases : Type := | 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) (**r pointer, int *) - | add_case_ip(ty: type) (**r int, pointer *) + | 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, Tint _ _ => add_case_pi ty - | Tint _ _, Tpointer ty => add_case_ip ty + | 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. @@ -817,14 +833,14 @@ Inductive classify_sub_cases : Type := 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 + | 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. @@ -837,12 +853,12 @@ Inductive classify_mul_cases : Type:= 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 + | 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. @@ -855,12 +871,12 @@ Inductive classify_div_cases : Type:= 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 + | 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. @@ -873,9 +889,9 @@ Inductive classify_binint_cases : Type:= 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 + | 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. @@ -887,8 +903,8 @@ Inductive classify_shift_cases : Type:= 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 + | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed | _,_ => shift_default end. @@ -902,15 +918,15 @@ Inductive classify_cmp_cases : Type:= 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 + | 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. @@ -921,7 +937,7 @@ Inductive classify_fun_cases : Type:= 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 + | Tpointer (Tfunction args res) _ => fun_case_f args res | _ => fun_default end. @@ -931,17 +947,25 @@ Inductive classify_cast_cases : Type := | 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_ip2bool (**r int|pointer -> bool *) + | cast_case_f2bool (**r float -> 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 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 + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tint IBool _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_ip2bool + | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool + | 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. @@ -951,14 +975,14 @@ Function classify_cast (tfrom tto: type) : classify_cast_cases := Definition typ_of_type (t: type) : AST.typ := match t with - | Tfloat _ => AST.Tfloat + | Tfloat _ _ => AST.Tfloat | _ => AST.Tint end. Definition opttyp_of_type (t: type) : option AST.typ := match t with | Tvoid => None - | Tfloat _ => Some AST.Tfloat + | Tfloat _ _ => Some AST.Tfloat | _ => Some AST.Tint end. -- cgit