diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Cabs.v | 1 | ||||
-rw-r--r-- | cparser/Cutil.ml | 19 | ||||
-rw-r--r-- | cparser/Cutil.mli | 6 | ||||
-rw-r--r-- | cparser/Elab.ml | 39 | ||||
-rw-r--r-- | cparser/Lexer.mll | 2 | ||||
-rw-r--r-- | cparser/Parser.vy | 4 | ||||
-rw-r--r-- | cparser/pre_parser.mly | 3 |
7 files changed, 72 insertions, 2 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v index d087e8c7..b3e4ffda 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) -> list initwhat -> 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..20cdc038 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -533,6 +533,25 @@ let sizeof_struct env members = end in sizeof_rec 0 members +(* Compute the offset of a struct member *) +let offsetof env ty field = + let rec sub acc name = function + | [] -> List.rev acc + | m::rem -> if m.fld_name = name then + List.rev acc + else + sub (m::acc) name rem in + match unroll env ty with + | TStruct (id,_) -> + let str = Env.find_struct env id in + let pre = sub [] field.fld_name str.ci_members in + begin match sizeof_struct env pre, alignof env field.fld_typ with + | Some s, Some a -> + align s a + | _ -> assert false end + | TUnion _ -> 0 + | _ -> assert false + (* 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..ee3c7625 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -111,6 +111,12 @@ 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 -> int +(* Compute the offset of a struct member *) +val cautious_mul: int64 -> int -> int option +(* Overflow-avoiding multiplication of an int64 and an int, with + result in type int. *) (* Type classification functions *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1bfc2d11..61f51520 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1642,6 +1642,45 @@ 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 + if Cutil.incomplete_type env ty then + error "offsetof of incomplete type %a" (print_typ env) ty; + let members env ty mem = + match ty with + | TStruct (id,_) -> wrap Env.find_struct_member loc env (id,mem) + | TUnion (id,_) -> wrap Env.find_union_member loc env (id,mem) + | _ -> error "request for member '%s' in something not a structure or union" mem in + let rec offset_of_list acc env ty = function + | [] -> acc,ty + | fld::rest -> let off = Cutil.offsetof env ty fld in + offset_of_list (acc+off) env fld.fld_typ rest in + let offset_of_member (env,off_accu,ty) mem = + match mem,unroll env ty with + | INFIELD_INIT mem,ty -> + let flds = members env ty mem in + let flds = List.rev flds in + let off,ty = offset_of_list 0 env ty flds in + env,off_accu + off,ty + | ATINDEX_INIT e,TArray (sub_ty,_,_) -> + let e,env = elab env e in + let e = match Ceval.integer_expr env e with + | None -> error "array element designator for is not an integer constant expression" + | Some n-> n in + let size = match sizeof env sub_ty with + | None -> assert false (* We expect only complete types *) + | Some s -> s in + let off_accu = match cautious_mul e size with + | None -> error "'offsetof' overflows" + | Some s -> off_accu + s in + env,off_accu,sub_ty + | ATINDEX_INIT _,_ -> error "subscripted value is not an array" in + let env,offset,_ = List.fold_left offset_of_member (env,0,ty) mem in + let size_t = size_t_ikind () in + let offset = Ceval.normalize_int (Int64.of_int offset) size_t in + let offsetof_const = EConst (CInt(offset,size_t,"")) in + { edesc = offsetof_const; etyp = TInt(size_t, []) },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..f6bd6a7e 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 = designator_list RPAREN + { (BUILTIN_OFFSETOF typ (rev 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..dc9c5319 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 designator_list RPAREN | postfix_expression DOT other_identifier | postfix_expression PTR other_identifier | postfix_expression INC |