diff options
| -rw-r--r-- | cparser/Cabs.v | 1 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 37 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 3 | ||||
| -rw-r--r-- | cparser/Elab.ml | 16 | ||||
| -rw-r--r-- | cparser/Lexer.mll | 2 | ||||
| -rw-r--r-- | cparser/Parser.vy | 4 | ||||
| -rw-r--r-- | cparser/pre_parser.mly | 3 | ||||
| -rw-r--r-- | runtime/include/stddef.h | 2 |
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 |