Merge pull request #159 from AbsInt/builtin_offsetof

Implement offsetof via builtin

8 files changed, 73 insertions, 3 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
diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h
index 5bdff564..958720a1 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