Clean-up pass on C types:

- Ctypes: add useful functions on attributes; remove attrs in typeconv
    (because attributes are meaningless on r-values)
- C2C: fixed missing or redundant Evalof
- Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values);
    add sanity check between typeconv/classify_binarith and the C99 standard.
- cparser: fixed several cases where incorrect type annotations were put
    on expressions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 55 insertions, 44 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 71404b2..14c9314 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -161,6 +161,14 @@ let insertion_mask bf =
   (* Give the mask an hexadecimal string representation, nicer to read *)
   {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
 
+let eshift env op a b =
+  let ty = unary_conversion env a.etyp in
+  { edesc = EBinop(op, a, b, ty); etyp = ty }
+
+let ebinint env op a b =
+  let ty = binary_conversion env a.etyp b.etyp in
+  { edesc = EBinop(op, a, b, ty); etyp = ty }
+
 (* Extract the value of a bitfield *)
 
 (* Reference C code:
@@ -178,15 +186,11 @@ signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
 
 *)
 
-let bitfield_extract bf carrier =
-  let e1 =
-    {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
-     etyp = carrier.etyp} in
+let bitfield_extract env bf carrier =
+  let e1 = eshift env Oshl carrier (left_shift_count bf) in
   let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
   let e2 = ecast ty e1 in
-  let e3 =
-    {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
-     etyp = ty} in
+  let e3 = eshift env Oshr e2 (right_shift_count bf) in
   if bf.bf_signed_res = bf.bf_signed
   then e3
   else ecast (TInt((if bf.bf_signed_res then IInt else IUInt), [])) e3
@@ -203,23 +207,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
 
 *)
 
-let bitfield_assign bf carrier newval =
+let bitfield_assign env bf carrier newval =
   let msk = insertion_mask bf in
   let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
   let newval_casted =
     ecast (TInt(IUInt,[])) newval in
   let newval_shifted =
-    {edesc = EBinop(Oshl, newval_casted, intconst (Int64.of_int bf.bf_pos) IUInt,
-                    TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
-  let newval_masked =
-    {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])}
-  and oldval_masked =
-    {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
-     etyp = TInt(IUInt,[])} in
-  {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
-   etyp =  TInt(IUInt,[])}
+    eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in
+  let newval_masked = ebinint env Oand newval_shifted msk
+  and oldval_masked = ebinint env Oand carrier notmsk in
+  ebinint env Oor oldval_masked newval_masked
 
 (* Check whether a field access (e.f or e->f) is a bitfield access.
    If so, return carrier expression (e and *e, respectively)
@@ -322,7 +319,7 @@ let transf_expr env ctx e =
         {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp}
 
   and transf_read e bf =
-    bitfield_extract bf
+    bitfield_extract env bf
       {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ}
 
   and transf_assign ctx e1 bf e2 =
@@ -330,19 +327,19 @@ let transf_expr env ctx e =
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let asg =
-        eassign carrier (bitfield_assign bf carrier (texp Val e2)) in
-      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)
+        eassign carrier (bitfield_assign env bf carrier (texp Val e2)) in
+      if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg)
 
   and transf_assignop ctx op e1 bf e2 tyres =
     bind_lvalue env (texp Val e1) (fun base ->
       let carrier =
         {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
       let rhs =
-        {edesc = EBinop(op, bitfield_extract bf carrier, texp Val e2, tyres);
+        {edesc = EBinop(op, bitfield_extract env bf carrier, texp Val e2, tyres);
          etyp = tyres} in
       let asg =
-        eassign carrier (bitfield_assign bf carrier rhs) in
-      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)
+        eassign carrier (bitfield_assign env bf carrier rhs) in
+      if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg)
 
   and transf_pre ctx op e1 bf tyfield =
     transf_assignop ctx op e1 bf (intconst 1L IInt)
@@ -357,11 +354,11 @@ let transf_expr env ctx e =
           {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
         let temp = mk_temp env tyfield in
         let tyres = unary_conversion env tyfield in
-        let settemp = eassign temp (bitfield_extract bf carrier) in
+        let settemp = eassign temp (bitfield_extract env bf carrier) in
         let rhs =
           {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in
         let asg =
-          eassign carrier (bitfield_assign bf carrier rhs) in
+          eassign carrier (bitfield_assign env bf carrier rhs) in
         ecomma (ecomma settemp asg) temp)
     end
 
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 22ef187..1169346 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -92,6 +92,13 @@ let attr_array_applicable = function
   | AConst | AVolatile | ARestrict | AAlignas _ -> false
   | Attr _ -> true
 
+(* Is an attribute of a composite type applicable to members of this type
+  when they are accessed? *)
+
+let attr_inherited_by_members = function
+  | AConst | AVolatile | ARestrict -> true
+  | AAlignas _ | Attr _ -> false
+
 (* Adding top-level attributes to a type.  Doesn't need to unroll defns. *)
 (* For array types, standard attrs are pushed to the element type. *)
 
@@ -574,17 +581,20 @@ let unary_conversion env t =
   | TInt(kind, attr) ->
       begin match kind with
       | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
-          TInt(IInt, attr)
+          TInt(IInt, [])
       | IInt | IUInt | ILong | IULong | ILongLong | IULongLong ->
-          TInt(kind, attr)
+          TInt(kind, [])
       end
   (* Enums are like signed ints *)
-  | TEnum(id, attr) -> TInt(enum_ikind, attr)
+  | TEnum(id, attr) -> TInt(enum_ikind, [])
   (* Arrays and functions decay automatically to pointers *)
   | TArray(ty, _, _) -> TPtr(ty, [])
   | TFun _ as ty -> TPtr(ty, [])
-  (* Other types are not changed *)
-  | t -> t
+  (* Float types and pointer types lose their attributes *)
+  | TFloat(kind, attr) -> TFloat(kind, [])
+  | TPtr(ty, attr) -> TPtr(ty, [])
+  (* Other types should not occur, but in doubt... *)
+  | _ -> t
 
 (* The usual binary conversions  (H&S 6.3.4).
    Applies only to arithmetic types.
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 9f59a76..0de0c82 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -54,6 +54,8 @@ val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ
   (* Apply the given function to the top-level attributes of the given type *)
 val attr_is_type_related: attribute -> bool
   (* Is an attribute type-related (true) or variable-related (false)? *)
+val attr_inherited_by_members: attribute -> bool
+  (* Is an attribute of a composite inherited by members of the composite? *)
 
 (* Type compatibility *)
 val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 0d2cb89..ecc97a7 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -805,7 +805,8 @@ let elab_expr loc env a =
             error "left-hand side of '.' is not a struct or union" in
       (* A field of a const/volatile struct or union is itself const/volatile *)
       { edesc = EUnop(Odot fieldname, b1);
-        etyp = add_attributes_type attrs (type_of_member env fld) }
+        etyp = add_attributes_type (List.filter attr_inherited_by_members attrs)
+                                   (type_of_member env fld) }
 
   | MEMBEROFPTR(a1, fieldname) ->
       let b1 = elab a1 in
@@ -823,7 +824,8 @@ let elab_expr loc env a =
         | _ ->
             error "left-hand side of '->' is not a pointer " in
       { edesc = EUnop(Oarrow fieldname, b1);
-        etyp = add_attributes_type attrs (type_of_member env fld) }
+        etyp = add_attributes_type (List.filter attr_inherited_by_members attrs)
+                                   (type_of_member env fld) }
 
 (* Hack to treat vararg.h functions the GCC way.  Helps with testing.
     va_start(ap,n)
@@ -996,14 +998,14 @@ let elab_expr loc env a =
         if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
           binary_conversion env b1.etyp b2.etyp
         else begin
-          let (ty, attr) =
+          let ty =
             match unroll env b1.etyp, unroll env b2.etyp with
-            | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> (ty, a)
-            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a)
+            | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty
+            | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty
             | _, _ -> error "type error in binary '+'" in
           if not (pointer_arithmetic_ok env ty) then
             err "illegal pointer arithmetic in binary '+'";
-          TPtr(ty, attr)
+          TPtr(ty, [])
         end in
       { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres }
 
@@ -1019,11 +1021,11 @@ let elab_expr loc env a =
           | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
-              (TPtr(ty, a), TPtr(ty, a))
+              (TPtr(ty, []), TPtr(ty, []))
           | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) ->
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '-'";
-              (TPtr(ty, a), TPtr(ty, a))
+              (TPtr(ty, []), TPtr(ty, []))
           | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
             (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
               if not (compatible_types ~noattrs:true env ty1 ty2) then
@@ -1084,7 +1086,7 @@ let elab_expr loc env a =
       | TPtr(ty1, a1), TPtr(ty2, a2) ->
           let tyres =
             if is_void_type env ty1 || is_void_type env ty2 then
-              TPtr(TVoid [], add_attributes a1 a2)
+              TPtr(TVoid (add_attributes a1 a2), [])
             else
               match combine_types ~noattrs:true env
                                   (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
@@ -1095,9 +1097,9 @@ let elab_expr loc env a =
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
       | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
-          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) }
+          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) }
       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
-          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
+          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
           match combine_types ~noattrs:true env ty1 ty2 with
           | None ->
@@ -1312,7 +1314,7 @@ let init_char_array_string opt_size s =
     if i < 0L then init else begin
       let c =
         if i < len then Int64.of_int (Char.code s.[Int64.to_int i]) else 0L in
-      add_chars (Int64.pred i) (Init_single (intconst c IChar) :: init)
+      add_chars (Int64.pred i) (Init_single (intconst c IInt) :: init)
     end in
   Init_array (add_chars (Int64.pred size) [])