| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
When a union is initialized with an initializer without designator the
first named member should be initialized. This commit skips members
without names during the elaboration of union initializers.
Note that anonymous members (unnamed members of struct or union type)
should not be skipped, and are not skipped since elaboration give names
to these members.
Bug 31982
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.
The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.
The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".
All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.
The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.
Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.
The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).
Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.
This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.
Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.
|
| |
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Extend check for incomplete type.
Extended the check to also include a check for variables with
incomplete object type that are not arrays, that have an
initializer. Furthermore the warning includes the type and variable
name.
* Warning for incomplete type in compound literals.
Incomplete types are not allowed for compound literals, except for
array types.
* Extend type printing function.
The type of a typedeof of an anonymous type should not be printed.
Furthermore added '<anonymous>' to the printing of anonymous types.
* Unify incomplete type errors message.
The incomplete type error messages should all look the same including
name of the variable, parameter, etc. and then the incomplete type.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not use `Pervasives.xxx` qualified names
Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
and uses of `Pervasives` cause fatal warnings.
This commit uses unqualified names instead, as no ambiguity occurs.
* Clarify "open" statements
OCaml 4.08.0 has stricter warnings concerning open statements that
shadow module names.
Closes: #300
|
| |
|
|
|
| |
The function determines whether the given type is an array type
or not.
|
| |
|
|
|
|
| |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds a check to reject type definitions such as
```
typedef __attribute((section "foo")) int fooint;
```
GCC and Clang also reject this as an error.
Without the check, the behavior is somewhat surprising:
```
fooint x; // placed in section "foo"
fooint * x; // placed in default section, attribute "foo" is ignored
```
Note that the following must be accepted:
```
typedef struct { ... } __attribute((packed)) t;
```
The "packed" attribute is correctly attached to the struct type and should not be checked. This is achieved by using `attribute_of_type_no_expand` to get the attributes of the typedef-ed type, excluding the attributes carried by a struct/union or another typedef.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a second step towards mimicking GCC/Clang's handling of attributes.
This commit introduces a distinction between
- Object-related attributes, such as "section", which apply to the object (function, variable) being defined;
- Name-related attributes, such as "aligned", which apply to the name (object, struct/union member, struct/union/enum tag) being defined.
In particular, "aligned" is now attached to "struct" and "union" definitions, while it used to be "floated up" before.
The C11 _Alignas modifier is treated like an object-related attribute, so that
```
struct s { ... };
_Alignas(64) struct s x;
```
correctly associates the alignment with "x" and not with "struct s", where it would be ignored because it was not part of the original definition of s.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
During elaboration of type declarators, non-type-related attributes such as "aligned" or "section" are "floated up" so that they apply to the thing being declared. For example, consider:
```
__attribute((aligned(16))) int * p;
```
The attribute is first attached to type `int`, then floated up to type `int *`, so that it finally applies to `p`, giving a 16-aligned pointer to int, and not a naturally-aligned pointer to 16-aligned int.
What happens when the non-type-related attribute comes from a typedef?
```
typedef __attribute((aligned(16))) int i16;
i16 * p;
```
CompCert used to expand the typedef then float up the attribute, resulting in `p` being a 16-aligned pointer to int.
GCC and Clang produce a naturally-aligned pointer, so they do not expand the typedef before floating.
The old CompCert behavior is somewhat surprising, and potentially less useful than the GCC/Clang behavior.
This commit changes the floating up of non-type-related attributes so that typedefs and struct/union/enum definitions are not expanded when determining which attributes to float up. This is a first step towards mimicking the GCC/Clang behavior.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Refactor common code of alignas.
Instead of working on attributes the function now works directly
on the type since the check always performed an extraction of
attributes from a type.
Bug 23393
* Attach _Alignas to the name.
Bug 23393
* Attach "aligned" attributes to names
So that __attribute((aligned(N))) remains consistent with _Alignas(N).
gcc and clang apply "aligned" attributes to names, with a special case
for typedefs:
typedef __attribute((aligned(16))) int int_al_16;
int_al_16 * p;
__attribute((aligned(16))) int * q;
For gcc, p is naturally-aligned pointer to 16-aligned int and
q is 16-aligned pointer to naturally-aligned int.
For CompCert with this commit, both p and q are 16-aligned pointers
to naturally-aligned int.
* Resurrect the alignment test involving typedef
The test was removed because it involved an _Alignas in a typedef,
which is no longer supported. However the same effect can be achieved
with an "aligned" attribute, which is still supported in typedef.
|
| |
|
|
|
|
| |
The check tests whether the standard _Alignas is contained within
a given attribute list.
Bug 23391
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Since commit 5963ac4, "aligned" attributes and _Alignas qualifiers
are represented differently, causing them to be treated differently
by the previous implementation of Cutil.attr_array_applicable.
This is incorrect and inconsistent with what happens during elaboration
of array types in Elab.
This PR reimplements attr_array_applicable in terms of class_of_attribute.
Just like during elaboration, attributes of the Attr_type class
are applied to the type of array elements, other attributes stay
attached to the array type.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N)
during elaboration.
However, we want to restrict the places where _Alignas can occur, as
standardized in ISO C11, while leaving more freedom for the placement
of the "aligned" attribute.
As a first step in this direction, this commit keeps the "aligned"
attribute unchanged in the AST, and distinct from _Alignas attributes.
Both attributes are honored when it comes to determining the actual
alignment of a type.
|
| |
|
|
|
|
| |
Restrict is only allowed for pointers whose referenced type is an
object type or incomplete type, but not a function type.
Bug 23397
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Add diagnostic for type qualified arrays that occur in the wrong place
Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as
function parameters and for them
only the outermost array type derivation.
Bug 23400
* Keep attributes from array for argument conversion
Type qualifiers of arrays in function parameters are just syntactic sugar
to allow adding them to the resulting pointer type. Hence, when a
qualified array type such as `int t[const 5]` decays into a pointer type
during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Error for structs with only flex array member
Flexible array members are only allowed if another member exists.
Bug 23324
* Added checks for nesting of structs with flex array members
Warn if a struct with a flex array member is used as array element
or member of another struct. Such usage is dubious.
Bug 23324
Don't warn if the struct-with-flex-array is a member of an union.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field):
- the reference implementation, in Coq, from cfrontend/Ctypes.v
- the implementation used during elaboration, in OCaml, from cparser/Cutil.ml
The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used.
This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example:
```
struct __packed__(1) s { char c; short s; int i; };
assert (__builtin_offsetof(struct s, i) == 3);
assert (sizeof(struct s) = sizeof(char[sizeof(struct s)]));
```
The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs.
This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout.
Related changes:
* cparser/Cutil: add `packing_parameters` function to extract packing info from attributes
* cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout
* cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.)
* cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)).
* cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab
* cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/.
* test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Allow strings literals as lvalues.
Strings and WStrings literals are lvalues, thus it is allowed to take their
addresses.
Bug 23356.
* String literals have types "array of (wide) char", not "pointer to (wide) char"
The pointer types were a leftover from the early, CIL-based C frontend.
* Remove special case for sizeof("string literal") during elaboration
No longer needed now that literals have array types.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In rare cases we can end up querying the attributes of a struct, union
or enum type that is no longer in scope and therefore not bound
in the current environment.
Instead of raising an Env.Error_ exception in this case,
this commit treats such structs / unions / enums as having no
attributes attached to their definitions: only the attributes
carried by the type expression are returned.
One example where this occurs is the following, made possible by
the previous commit ("Revised elaboration of function definitions"):
int f(struct s { int a; } * p) { return p-> a; }
int g(void) { return f(NULL); }
"struct s" is scoped within the definition of f. When we get to
checking the call to f from g, checking that the NULL argument
is compatible with the "struct s *" parameters, we're outside
the scope of "struct s" and its definition is not found in the
current environment.
|
| |
|
|
|
|
|
|
|
|
|
| |
The ISO C99 standard allows cast only if the type name involved
is either a void type or a scalar type.
For compatibility with GCC and Clang we used to support casting
a struct or union to exactly the same struct or union type.
That does not seem useful in practice and complicates conformance
testing. This commit gets rid of this exception to the C99 rule.
Bug 23310
|
| |
|
|
|
|
|
| |
Sizeof and _Alignof are not allowed on bit-fields
Sizeof and _Alignof are not allowed to be applied to a expression
that designates a bit-field member.
Bug 23311
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Check recursively for const for modifiable lvalues
According to 6.3.2.1 a modifiable lvalue is an lvalue that does
have a const-qualified type, and if it is a union or structure it
does not have any member, including any member of all contained
strutures or union, with a const-qualified type.
The new check for modifiable lvalue additionally checks this now
instead of only testing for toplevel const.
Bug 22420
|
| |
|
|
|
|
|
| |
The check tests whether the size calculation of an array overflows
or the array covers half of the available address space and reports
an error in this case.
Bug 21034
|
| |
|
|
|
|
|
|
|
|
| |
The C11 standard declares exit,abort,_Exit,quick_exit and
thrd_exit as _Noreturn however this is not included in older C
libs and leads to false negatives in reporting _Noreturn and
return type warnings. This can be avoided by enhancing the
noreturn check of the Cflow analysis to also test if one of the
above functions is called.
Bug 21009
|
| |
|
|
|
|
| |
Instead of changing the definition of sizeof we now ignore errors
raise in the Cflow module.
Bug 21005
|
| |
|
|
|
|
|
|
| |
Since the function environment does not necessary contain structs
and unions defined in sizeof expressions the evaluation should be
not constant and the Environment excpetions should be catched.
Fix 21005
|
| |\
| |
| |
| | |
Improved warnings related to function returns
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to
- warn for non-void functions that can return by falling through the body
- warn more precisely for _Noreturn functions that can return
- introduce the "return 0" in "main" functions less often (cosmetic).
For the control-flow analysis, the following conservative approximations are made:
- any "goto" label is reachable
- all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case)
- the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.
|
| |/
|
|
|
|
| |
The optional hex parameter only worked if the intconstant was also
of unsigned kind. Hence it is better to have one function in
Bitfields for this.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Introduce Cutil.class_of_attribute to return the class of the given attribute: one among
Attr_type attribute related to types (e.g. "aligned")
Attr_struct attribute related to struct/union/enum types (e.g. "packed")
Attr_function attribute related to function types (e.g. "noreturn")
Attr_name attribute related to variable and function declarations (e.g. "section")
Attr_unknown attribute was not declared
Cutil.declare_attribute is used to associate a class to a custom attribute.
Standard attributes (const, volatile, _Alignas, etc) are Attr_type.
cfronted/C2C.ml: declare the few attributes that CompCert honors currently.
cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The treatment of attributes in the current CompCert is often surprising. For example,
attribute(xxx) char * x;
is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char".
CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e.
const char * x;
is really "x is a pointer to a const char", not "x is a const pointer to char".
This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above,
attribute(xxx) char * x; // "attribute(xxx)" applies to "x"
const char * x; // "const" applies to "char"
This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
|
| | |
| |
| |
| |
| | |
The intconst function comes with an optional parameter to add an
hex string for later printing.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The c standard allows member designators for offsetof. The current
implementation works by recursively combining the offset of each
of the member designators. For array access the size of the
subtypes is multiplied by the index and for members the offset of
the member is calculated.
Bug 20765
|
| | |
| |
| |
| |
| |
| |
| |
| | |
The problem was that sub structs are were not correctly aligned.
The new version is much simpler and uses the sizeof_struct to
calculate the individual offsets and add them up to get correct
offest.
Bug 20765
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
| |
Instead of using idents the anonymous fileds get names of the
for <anon>_c where c is a counter of all anonymous members.
Bug 20003
|
| |
|
|
|
|
| |
The warning missing declarations is now also triggered for
declarations without name in field lists of composite types if
the declaration is not an anonymous composite or a bitfield member.
|
| |
|
|
|
|
| |
Now the same warning is triggered for both cases, int to ptr and
ptr to int.
Bug 18004
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Since some incomplete types are allowed in initialization just
test whether the default initilization exists.
Bug 19601
|
| |/
|
|
|
|
|
|
|
|
| |
Now each warning either has a name and can be turned on/off, made
into an error,etc. or is a warning that always will be triggered.
The message of the warnings are similar to the ones emited by
gcc/clang and all fit into one line.
Furthermore the diagnostics are now colored if colored output is
available.
Bug 18004
|
| |
|
|
|
|
|
|
| |
CompCert now recognizes the C11 _Noreturn function specifier and
emits a simple warning for functions declared _Noreturn containing
a return statement. Also the stdnoreturn header and additionally
the stdalign header are added.
Bug 18541
|
| |
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
