Revised type compatibility check w.r.t. handling of attributes.

We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively.
In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary.
Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do.
Net result is fewer warnings and type-checking that is closer to GCC/Clang.

4 files changed, 93 insertions, 49 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 7d1c2e4b..9093b230 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -79,6 +79,12 @@ let rec remove_custom_attributes (names: string list)  (al: attributes) =
   | a :: tl ->
       a :: remove_custom_attributes names tl
 
+(* Is an attribute a ISO C standard attribute? *)
+
+let attr_is_standard = function
+  | AConst | AVolatile | ARestrict -> true
+  | AAlignas _ | Attr _ -> false
+
 (* Is an attribute type-related (true) or variable-related (false)? *)
 
 let attr_is_type_related = function
@@ -184,12 +190,28 @@ let alignas_attribute al =
 
 exception Incompat
 
-let combine_types ?(noattrs = false) env t1 t2 =
-
-  let comp_attr a1 a2 =
-    if a1 = a2 then a2
-    else if noattrs then add_attributes a1 a2
-    else raise Incompat
+type attr_handling =
+  | AttrCompat
+  | AttrIgnoreTop
+  | AttrIgnoreAll
+
+(* Check that [t1] and [t2] are compatible and produce a type that
+   combines the information in [t1] and [t2].  For example,
+   if [t1] is a prototyped function type and [t2] an unprototyped
+   function type, the combined type takes the prototype from [t1]. *)
+
+let combine_types mode env t1 t2 =
+
+  let comp_attr m a1 a2 =
+    if a1 = a2 then a2 else match m with
+    | AttrCompat ->
+        let (a1std, a1other) = List.partition attr_is_standard a1
+        and (a2std, a2other) = List.partition attr_is_standard a2 in
+        if a1std = a2std
+        then add_attributes a1std (add_attributes a1other a2other)
+        else raise Incompat
+    | AttrIgnoreTop | AttrIgnoreAll ->
+        add_attributes a1 a2
   and comp_base x1 x2 =
     if x1 = x2 then x2 else raise Incompat
   and comp_array_size sz1 sz2 =
@@ -211,18 +233,19 @@ let combine_types ?(noattrs = false) env t1 t2 =
         end
     | _ -> () in
 
-  let rec comp t1 t2 =
+  let rec comp m t1 t2 =
     match t1, t2 with
     | TVoid a1, TVoid a2 ->
-        TVoid(comp_attr a1 a2)
+        TVoid(comp_attr m a1 a2)
     | TInt(ik1, a1), TInt(ik2, a2) ->
-        TInt(comp_base ik1 ik2, comp_attr a1 a2)
+        TInt(comp_base ik1 ik2, comp_attr m a1 a2)
     | TFloat(fk1, a1), TFloat(fk2, a2) ->
-        TFloat(comp_base fk1 fk2, comp_attr a1 a2)
+        TFloat(comp_base fk1 fk2, comp_attr m a1 a2)
     | TPtr(ty1, a1), TPtr(ty2, a2) ->
-        TPtr(comp ty1 ty2, comp_attr a1 a2)
+        let m' = if m = AttrIgnoreTop then AttrCompat else m in
+        TPtr(comp m' ty1 ty2, comp_attr m a1 a2)
     | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
-        TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
+        TArray(comp m ty1 ty2, comp_array_size sz1 sz2, comp_attr m a1 a2)
     | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
         let (params, vararg) =
           match params1, params2 with
@@ -231,26 +254,29 @@ let combine_types ?(noattrs = false) env t1 t2 =
           | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
           | Some l1, Some l2 ->
               if List.length l1 <> List.length l2 then raise Incompat;
-              (Some(List.map2 (fun (id1, ty1) (id2, ty2) -> (id2, comp ty1 ty2))
-                              l1 l2),
-               comp_base vararg1 vararg2)
+              let comp_param (id1, ty1) (id2, ty2) =
+                (id2, comp AttrIgnoreTop ty1 ty2) in
+              (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2)
         in
-          TFun(comp ty1 ty2, params, vararg, comp_attr a1 a2)
-    | TNamed _, _ -> comp (unroll env t1) t2
-    | _, TNamed _ -> comp t1 (unroll env t2)
+        let m' = if m = AttrIgnoreTop then AttrCompat else m in
+        TFun(comp m' ty1 ty2, params, vararg, comp_attr m a1 a2)
+    | TNamed _, _ -> comp m (unroll env t1) t2
+    | _, TNamed _ -> comp m t1 (unroll env t2)
     | TStruct(s1, a1), TStruct(s2, a2) ->
-        TStruct(comp_base s1 s2, comp_attr a1 a2)
+        TStruct(comp_base s1 s2, comp_attr m a1 a2)
     | TUnion(s1, a1), TUnion(s2, a2) -> 
-        TUnion(comp_base s1 s2, comp_attr a1 a2)
+        TUnion(comp_base s1 s2, comp_attr m a1 a2)
     | TEnum(s1, a1), TEnum(s2, a2) -> 
-        TEnum(comp_base s1 s2, comp_attr a1 a2)
+        TEnum(comp_base s1 s2, comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
 
-  in try Some(comp t1 t2) with Incompat -> None
+  in try Some(comp mode t1 t2) with Incompat -> None
+
+(** Check whether two types are compatible. *)
 
-let compatible_types  ?noattrs env t1 t2 =
-  match combine_types ?noattrs env t1 t2 with Some _ -> true | None -> false
+let compatible_types mode env t1 t2 =
+  match combine_types mode env t1 t2 with Some _ -> true | None -> false
 
 (* Naive placement algorithm for bit fields, might not match that
    of the compiler. *)
@@ -756,10 +782,9 @@ let is_literal_0 e =
    Custom attributes can safely be dropped but must not be added. *)
 
 let valid_assignment_attr afrom ato =
-  let is_covariant = function Attr _ -> false | _ -> true in
-  let (afrom1, afrom2) = List.partition is_covariant afrom
-  and (ato1, ato2) = List.partition is_covariant ato in
-  incl_attributes afrom1 ato1 && incl_attributes ato2 afrom2
+  let (afromstd, afromcustom) = List.partition attr_is_standard afrom
+  and (atostd, atocustom) = List.partition attr_is_standard ato in
+  incl_attributes afromstd atostd && incl_attributes atocustom afromcustom
 
 (* Check that an assignment is allowed *)
 
@@ -771,9 +796,7 @@ let valid_assignment env from tto =
       valid_assignment_attr (attributes_of_type env ty)
                             (attributes_of_type env ty')
       && (is_void_type env ty || is_void_type env ty'
-          || compatible_types env
-               (erase_attributes_type env ty)
-               (erase_attributes_type env ty'))
+          || compatible_types AttrIgnoreTop env ty ty')
   | TStruct(s, _), TStruct(s', _) -> s = s'
   | TUnion(s, _), TUnion(s', _) -> s = s'
   | _, _ -> false
@@ -781,16 +804,19 @@ let valid_assignment env from tto =
 (* Check that a cast is allowed *)
 
 let valid_cast env tfrom tto =
-  compatible_types ~noattrs:true env tfrom tto ||
-  begin match unroll env tfrom, unroll env tto with
+  match unroll env tfrom, unroll env tto with
+  (* from any type to void *)
   | _, TVoid _ -> true
   (* from any int-or-pointer (with array and functions decaying to pointers)
      to any int-or-pointer *)
-  | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _), (TInt _ | TPtr _ | TEnum _) -> true
+  | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _),
+    (TInt _ | TPtr _ | TEnum _) -> true
   (* between int and float types *)
   | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> true
+  (* between identical composites *)
+  | TStruct(s1, _), TStruct(s2, _) -> s1 = s2
+  | TUnion(s1, _), TUnion(s2, _) -> s1 = s2
   | _, _ -> false
-  end
 
 (* Construct an integer constant *)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 309981be..53bcfcea 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -58,12 +58,28 @@ 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
+
+type attr_handling =
+  | AttrCompat
+  | AttrIgnoreTop
+  | AttrIgnoreAll
+
+val compatible_types : attr_handling -> Env.t -> typ -> typ -> bool
   (* Check that the two given types are compatible.  
-     If [noattrs], ignore attributes (recursively). *)
-val combine_types : ?noattrs: bool -> Env.t -> typ -> typ -> typ option
+     The attributes in the types are compared according to the first argument:
+- [AttrCompat]: the types must have the same standard attributes
+    ([const], [volatile], [restrict]) but may differ on custom attributes.
+- [AttrIgnoreTop]: the top-level attributes of the two types are ignored,
+    but attributes of e.g. types of pointed objects (for pointer types)
+    are compared as per [AttrCompat].
+- [AttrIgnoreAll]: recursively ignore the attributes in the two types. *)
+val combine_types : attr_handling -> Env.t -> typ -> typ -> typ option
   (* Like [compatible_types], but if the two types are compatible,
-     return the most precise type compatible with both. *)
+     return the most precise type compatible with both.
+     The attributes are compared according to the first argument,
+     with the same meaning as for [compatible_types].
+     When two sets of attributes are compatible, the result of
+     [combine_types] carries the union of these two sets of attributes. *)
 
 (* Size and alignment *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 615ddd97..ac82532b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1121,7 +1121,7 @@ and elab_single zi a il =
       (* This is a scalar: do direct initialization and continue *)
       check_init_type loc env a ty;
       elab_list (I.set zi (Init_single a)) il false
-  | TStruct _ | TUnion _ when compatible_types ~noattrs:true env ty a.etyp ->
+  | TStruct _ | TUnion _ when compatible_types AttrIgnoreTop env ty a.etyp ->
       (* This is a composite that can be initialized directly
          from the expression: do as above *)
       elab_list (I.set zi (Init_single a)) il false
@@ -1267,7 +1267,7 @@ let elab_expr loc env a =
       let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in
       let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
       let ty' = default_argument_conversion env ty in
-      if not (compatible_types env ty ty') then
+      if not (compatible_types AttrIgnoreTop env ty ty') then
         warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'"
                 Cprint.typ ty Cprint.typ ty'
                 Cprint.typ ty' Cprint.typ ty;
@@ -1459,7 +1459,7 @@ let elab_expr loc env 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
+              if not (compatible_types AttrIgnoreAll env ty1 ty2) then
                 err "mismatch between pointer types in binary '-'";
               if not (pointer_arithmetic_ok env ty1) then
                 err "illegal pointer arithmetic in binary '-'";
@@ -1519,11 +1519,13 @@ let elab_expr loc env a =
             if is_void_type env ty1 || is_void_type env ty2 then
               TPtr(TVoid (add_attributes a1 a2), [])
             else
-              match combine_types ~noattrs:true env
+              match combine_types AttrIgnoreAll env
                                   (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
               | None ->
-                  error "the second and third arguments of '? :' \
-                         have incompatible pointer types"
+                  warning "the second and third arguments of '? :' \
+                           have incompatible pointer types";
+                  (* tolerance *)
+                  TPtr(TVoid (add_attributes a1 a2), [])
               | Some ty -> ty
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
@@ -1532,7 +1534,7 @@ let elab_expr loc env a =
       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
-          match combine_types ~noattrs:true env ty1 ty2 with
+          match combine_types AttrIgnoreAll env ty1 ty2 with
           | None ->
               error ("the second and third arguments of '? :' have incompatible types")
           | Some tyres ->
@@ -1660,7 +1662,7 @@ let elab_expr loc env a =
           when is_void_type env ty2 ->
             EBinop(op, b1, b2, TPtr(ty1, []))
         | TPtr(ty1, _), TPtr(ty2, _) ->
-            if not (compatible_types ~noattrs:true env ty1 ty2) then
+            if not (compatible_types AttrIgnoreAll env ty1 ty2) then
               warning "comparison between incompatible pointer types";
             EBinop(op, b1, b2, TPtr(ty1, []))
         | TPtr _, (TInt _ | TEnum _)
@@ -1749,7 +1751,7 @@ let enter_or_refine_ident local loc env s sto ty =
       if local && Env.in_current_scope env id then
         error loc "redefinition of local variable '%s'" s;
       let new_ty =
-        match combine_types env old_ty ty with
+        match combine_types AttrCompat env old_ty ty with
         | Some new_ty ->
             new_ty
         | None ->
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 3064e78d..686a7d39 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -147,7 +147,7 @@ let accessor_type loc env ty =
 let ecast ty e = {edesc = ECast(ty, e); etyp = ty}
 
 let ecast_opt env ty e =
-  if compatible_types ~noattrs:true env ty e.etyp then e else ecast ty e
+  if compatible_types AttrCompat env ty e.etyp then e else ecast ty e
 
 (*  (ty) __builtin_readNN_reversed(&lval)
  or (ty) __builtin_bswapNN(lval) *)