Implement offsetof via builtin.

The implementation of offsetof as macro in the form
((size_t) &((ty*) NULL)->member) has the problem that it cannot be
used everywhere were an integer constant expression is allowed,
for example in initiliazers of global variables and there is also
no check for the case that member is of bitifield type.

The new implementation adds a builtin function for this which is
replaced by an integer constant during elaboration.
Bug 20765

8 files changed, 65 insertions, 3 deletions

diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index d087e8c7..355c748e 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -142,6 +142,7 @@ with expression :=
     (* Non-standard *)
   | EXPR_ALIGNOF : expression -> expression
   | TYPE_ALIGNOF : (list spec_elem * decl_type) -> expression
+  | BUILTIN_OFFSETOF : (list spec_elem * decl_type) -> string -> expression
 
 with constant :=
   (* The string is the textual representation of the constant in
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index f5d5c425..66ea19e4 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -533,6 +533,43 @@ let sizeof_struct env members =
       end
   in sizeof_rec 0 members
 
+(* Compute the offset of a struct member *)
+let offsetof env ty fields =
+  let align_field ofs ty =
+    let a =  match alignof env ty with
+      | Some a -> a
+      | None -> assert false in
+    align ofs a in
+  let rec offsetof_rec ofs field rest = function
+    | [] -> ofs
+    | m :: rem as ml ->
+      if m.fld_name = field.fld_name then begin
+        match rest with
+        | [] -> align_field ofs field.fld_typ
+        | _ -> lookup_field ofs field.fld_typ rest
+      end else if m.fld_bitfield = None then begin
+        match alignof env m.fld_typ, sizeof env m.fld_typ with
+        | Some a, Some s -> offsetof_rec (align ofs a + s) field rest rem
+        | _, _ -> assert false (* should never happen *)
+      end else begin
+        let (s, a, ml') = pack_bitfields ml in
+        let ofs = align ofs a + s in
+        offsetof_rec ofs field rest ml'
+      end
+  and lookup_field ofs ty = function
+    | [] -> align_field ofs ty
+    | fld::rest ->
+      begin match unroll env ty with
+        | TStruct (id,_) ->
+          let str = Env.find_struct env id in
+          offsetof_rec ofs fld rest str.ci_members
+        | TUnion (id,_) ->
+          lookup_field ofs fld.fld_typ rest
+        | _ -> assert false
+      end
+  in
+  lookup_field 0  ty (List.rev fields)
+
 (* Simplified version to compute offsets on structs without bitfields *)
 let struct_layout env members =
   let rec struct_layout_rec mem ofs = function
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index edff9ee1..c5a074c5 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -111,6 +111,9 @@ val composite_info_def:
   Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
 val struct_layout:
   Env.t -> field list -> (string * int) list
+val offsetof:
+  Env.t -> typ -> field list -> int
+(* Compute the offset of a struct member *)
 
 (* Type classification functions *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 1bfc2d11..d8d1d7d2 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1642,6 +1642,22 @@ let elab_expr vararg loc env a =
         error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty;
       { edesc = EAlignof ty; etyp =  TInt(size_t_ikind(), []) },env'
 
+  | BUILTIN_OFFSETOF ((spec,dcl), mem) ->
+    let (ty,env) = elab_type loc env spec dcl in
+    let offset =
+      match unroll env ty with
+      | TStruct(id, attrs) ->
+        if  Cutil.incomplete_type env ty then
+          error "offsetof of incomplete type %a" (print_typ env) ty;
+        let fld = (wrap Env.find_struct_member loc env (id,mem)) in
+        if List.exists (fun fld -> fld.fld_bitfield <> None) fld then
+          error "cannot compute the offset of bitfield '%s" mem;
+        Cutil.offsetof env ty fld
+      | _ ->
+        error "request offsetof for member '%s' in something not a structure" mem in
+    let offsetof_const = EConst (CInt(Int64.of_int offset,size_t_ikind (),"")) in
+    { edesc = offsetof_const; etyp = TInt(size_t_ikind(), []) },env
+
   | UNARY(PLUS, a1) ->
       let b1,env = elab env a1 in
       if not (is_arith_type env b1.etyp) then
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 71aad604..efb06b5d 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -36,6 +36,7 @@ let () =
       ("__attribute", fun loc -> ATTRIBUTE loc);
       ("__attribute__", fun loc -> ATTRIBUTE loc);
       ("__builtin_va_arg", fun loc -> BUILTIN_VA_ARG loc);
+      ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
       ("__const", fun loc -> CONST loc);
       ("__const__", fun loc -> CONST loc);
       ("__inline", fun loc -> INLINE loc);
@@ -510,6 +511,7 @@ and singleline_comment = parse
       | UNDERSCORE_BOOL loc -> loop UNDERSCORE_BOOL't loc
       | BREAK loc -> loop BREAK't loc
       | BUILTIN_VA_ARG loc -> loop BUILTIN_VA_ARG't loc
+      | BUILTIN_OFFSETOF loc -> loop BUILTIN_OFFSETOF't loc
       | CASE loc -> loop CASE't loc
       | CHAR loc -> loop CHAR't loc
       | COLON loc -> loop COLON't loc
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index 3e175a37..fb0b7444 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -37,7 +37,7 @@ Require Import List.
   STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM
 
 %token<cabsloc> CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK
-  RETURN BUILTIN_VA_ARG
+  RETURN BUILTIN_VA_ARG BUILTIN_OFFSETOF
 
 %token EOF
 
@@ -145,6 +145,8 @@ postfix_expression:
     { (CAST typ (COMPOUND_INIT (rev' init)), loc) }
 | loc = LPAREN typ = type_name RPAREN LBRACE init = initializer_list COMMA RBRACE
     { (CAST typ (COMPOUND_INIT (rev' init)), loc) }
+| loc = BUILTIN_OFFSETOF LPAREN typ = type_name COMMA mem = OTHER_NAME RPAREN
+    { (BUILTIN_OFFSETOF typ (fst mem), loc) }
 
 (* Semantic value is in reverse order. *)
 argument_expression_list:
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 613ec17f..1c917b23 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -57,7 +57,7 @@
   AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE
   UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE
   SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF
-  ATTRIBUTE ALIGNAS PACKED ASM
+  ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF
 
 %token EOF
 
@@ -254,6 +254,7 @@ postfix_expression:
 | postfix_expression LBRACK expression RBRACK
 | postfix_expression LPAREN argument_expression_list? RPAREN
 | BUILTIN_VA_ARG LPAREN assignment_expression COMMA type_name RPAREN
+| BUILTIN_OFFSETOF LPAREN type_name COMMA other_identifier RPAREN
 | postfix_expression DOT other_identifier
 | postfix_expression PTR other_identifier
 | postfix_expression INC
diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h
index 5bdff564..452497c3 100644
--- a/runtime/include/stddef.h
+++ b/runtime/include/stddef.h
@@ -114,7 +114,7 @@ typedef signed int wchar_t;
 #endif
 
 #if defined(_STDDEF_H) && !defined(offsetof)
-#define offsetof(ty,member) ((size_t) &((ty*) NULL)->member)
+#define offsetof(ty,member) (__builtin_offsetof(ty,member))
 #endif
 
 #endif