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

1 files changed, 211 insertions, 187 deletions

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index c76d9b9..ffe08bf 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.