From 8c94ad72e7479cb3d6ec36fddc7a70c56b1caf3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 3 Mar 2020 18:05:43 +0100
Subject: [PATCH] [Kernel] Cabs2cil: inlines the C offsetof macro before the
analyses.
In order to avoid an undefined behavior in the C code generated for this macro
(conversion from an absolute integer to a pointer).
---
src/kernel_internals/parsing/cparser.mly | 9 +++++++-
src/kernel_internals/typing/cabs2cil.ml | 22 +++++++++++++++++++
.../ast_printing/cil_printer.ml | 17 ++++++++++++++
src/kernel_services/ast_queries/cil.ml | 13 -----------
tests/misc/oracle/pragma-pack.0.res.oracle | 2 ++
tests/misc/oracle/pragma-pack.1.res.oracle | 2 ++
tests/misc/oracle/pragma-pack.2.res.oracle | 2 ++
.../misc/oracle/pragma_pack_zero.0.res.oracle | 2 ++
.../misc/oracle/pragma_pack_zero.1.res.oracle | 2 ++
tests/syntax/oracle/offsetof.res.oracle | 7 +++---
.../value/oracle/attribute-aligned.res.oracle | 2 ++
11 files changed, 62 insertions(+), 18 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 666053a2830..fadfd5c5949 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -566,7 +566,14 @@ postfix_expression: /*(* 6.5.2 *)*/
{ expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
}
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN
- { transformOffsetOf $3 $5 }
+ {
+ let loc_f = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
+ let arg = transformOffsetOf $3 $5 in
+ let builtin = { expr_loc = loc_f;
+ expr_node = VARIABLE "__builtin_offsetof" }
+ in
+ make_expr (CALL (builtin, [ arg ], []))
+ }
| postfix_expression DOT id_or_typename { make_expr (MEMBEROF ($1, $3))}
| postfix_expression ARROW id_or_typename { make_expr (MEMBEROFPTR ($1, $3)) }
| postfix_expression PLUS_PLUS { make_expr (UNARY (POSINCR, $1)) }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 42b88e95e86..39a07c2eb0e 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7026,6 +7026,28 @@ and doExp local_env
Kernel.warning ~current:true
"Invalid call to builtin_constant_p")
end
+ | "__builtin_offsetof" ->
+ begin
+ match !pargs with
+ | [{ enode = CastE (_, {enode = AddrOf (host, offset)}) } as e] ->
+ begin
+ piscall := false;
+ prestype := Cil.theMachine.Cil.typeOfSizeOf;
+ try
+ let typ = Cil.typeOfLhost host in
+ let start, _width = Cil.bitsOffset typ offset in
+ if start mod 8 <> 0 then
+ Kernel.error ~current:true "Using offset of bitfield";
+ let kind = Cil.theMachine.kindOfSizeOf in
+ pres := Cil.kinteger ~loc:e.eloc kind (start / 8);
+ with SizeOfError _ ->
+ pres := e;
+ Kernel.warning ~once:true ~current:true
+ "Invalid call to builtin_offsetof";
+ end
+ | _ ->
+ Kernel.abort ~current:true "Invalid call to builtin_offsetof";
+ end
| "__builtin_types_compatible_p" ->
begin
(* Constant-fold the argument and see if it is a constant *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index aef50199843..8bb7a5f20ef 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1047,6 +1047,23 @@ class cil_printer () = object (self)
"__builtin_types_compatible_p: cabs2cil should have added sizeof to \
the arguments."
+ | Call(dest, {enode = Lval (Var vi, NoOffset)}, [ arg ], (l, _))
+ when vi.vname = "__builtin_offsetof"
+ && not state.print_cil_as_is ->
+ begin
+ match arg.enode with
+ | CastE (_, { enode = AddrOf (host, offset) }) ->
+ (* Print the destination *)
+ Extlib.may (fprintf fmt "%a = " self#lval) dest;
+ (* Now the call itself *)
+ fprintf fmt "%a(%a, %a)%s"
+ self#varname vi.vname
+ (self#typ None) (Cil.typeOfLhost host)
+ self#offset offset
+ instr_terminator
+ | _ -> Kernel.fatal ~source:l "__builtin_offsetof: invalid argument."
+ end
+
| Call(dest,e,args,_) -> pp_call dest e fmt args
| Asm(attrs, tmpls, ext_asm, l) ->
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 459570e1be6..91afc7abef7 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4509,19 +4509,6 @@ and constFold (machdep: bool) (e: exp) : exp =
| AlignOfE _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | SizeOf _ ->
e (* Depends on machdep. Do not evaluate in this case*)
- (* Special case to handle the C macro 'offsetof' *)
- | CastE(it,
- { enode = AddrOf (Mem ({enode = CastE(TPtr(bt, _), z)}), off)})
- when machdep && isZero z -> begin
- try
- let start, _width = bitsOffset bt off in
- if start mod 8 <> 0 then
- Kernel.error ~current:true "Using offset of bitfield" ;
- constFold machdep
- (new_exp ~loc (CastE(it, (integer ~loc (start / 8)))))
- with SizeOfError _ -> e
- end
-
| CastE (t, e) -> begin
Kernel.debug ~dkey "ConstFold CAST to %a@." !pp_typ_ref t ;
let e = constFold machdep e in
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index 8688b345c3b..f3f41b911f7 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -87,6 +87,8 @@
adding aligned(1) attribute to field 'PACKOVERPOP.j' due to packing pragma
[kernel:typing:pragma] tests/misc/pragma-pack.c:88:
adding aligned(1) attribute to comp 'PACKOVERPOP' due to packing pragma
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[kernel:typing:pragma] tests/misc/pragma-pack.c:133:
packing pragma: restoring alignment to default (16)
[kernel:typing:pragma] tests/misc/pragma-pack.c:135:
diff --git a/tests/misc/oracle/pragma-pack.1.res.oracle b/tests/misc/oracle/pragma-pack.1.res.oracle
index 559d8cfaacb..59c543748f2 100644
--- a/tests/misc/oracle/pragma-pack.1.res.oracle
+++ b/tests/misc/oracle/pragma-pack.1.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma-pack.c (with preprocessing)
[kernel] tests/misc/pragma-pack.c:87: Warning:
ignoring #pragma pack(pop) with empty stack
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma-pack.2.res.oracle b/tests/misc/oracle/pragma-pack.2.res.oracle
index ae56a3d1f1a..c2534c76f82 100644
--- a/tests/misc/oracle/pragma-pack.2.res.oracle
+++ b/tests/misc/oracle/pragma-pack.2.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma-pack.c (with preprocessing)
[kernel] tests/misc/pragma-pack.c:87: Warning:
ignoring #pragma pack(pop) with empty stack
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma_pack_zero.0.res.oracle b/tests/misc/oracle/pragma_pack_zero.0.res.oracle
index 6c491d9c591..0137611438a 100644
--- a/tests/misc/oracle/pragma_pack_zero.0.res.oracle
+++ b/tests/misc/oracle/pragma_pack_zero.0.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma_pack_zero.c (with preprocessing)
[kernel] tests/misc/pragma_pack_zero.c:35: Warning:
GCC accepts pack(0) but does not specify its behavior; considering it equivalent to pack()
+[kernel:typing:implicit-function-declaration] tests/misc/pragma_pack_zero.c:47: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma_pack_zero.1.res.oracle b/tests/misc/oracle/pragma_pack_zero.1.res.oracle
index 69b3a971800..672ee382233 100644
--- a/tests/misc/oracle/pragma_pack_zero.1.res.oracle
+++ b/tests/misc/oracle/pragma_pack_zero.1.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma_pack_zero.c (with preprocessing)
[kernel] tests/misc/pragma_pack_zero.c:35: Warning:
ignoring invalid packing alignment (0)
+[kernel:typing:implicit-function-declaration] tests/misc/pragma_pack_zero.c:47: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/syntax/oracle/offsetof.res.oracle b/tests/syntax/oracle/offsetof.res.oracle
index ac9886f97c2..0829a102008 100644
--- a/tests/syntax/oracle/offsetof.res.oracle
+++ b/tests/syntax/oracle/offsetof.res.oracle
@@ -1,13 +1,12 @@
[kernel] Parsing tests/syntax/offsetof.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/syntax/offsetof.c:6: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
/* Generated by Frama-C */
#include "stddef.h"
-struct c {
- char ca ;
-};
void main(void)
{
size_t S;
- S = (unsigned int)(& ((struct c *)0)->ca);
+ S = 0U;
return;
}
diff --git a/tests/value/oracle/attribute-aligned.res.oracle b/tests/value/oracle/attribute-aligned.res.oracle
index c451f494f10..160214c6a77 100644
--- a/tests/value/oracle/attribute-aligned.res.oracle
+++ b/tests/value/oracle/attribute-aligned.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/value/attribute-aligned.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/value/attribute-aligned.c:17: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
--
GitLab