| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
Introduce an error message for section attributes with non string
arguments,and another for multiple, ambiguous section attributes.
This is more consistent with the handling of other
attributes, like packed, than the old behavior of silently
ignoring them.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We can get linker errors for addresses of the form "symbol + offset"
where "symbol" is in the small data area and "offset" is large enough
to overflow the relative displacement from the SDA base register.
To avoid this, this commit enriches `C2C.atom_is_small_data`,
which is the implementation of `Asm.symbol_is_small_data` in the PPC port,
with a check that the offset is within the bounds of the symbol.
If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces
an absolute addressing instead of a SDA-relative addressing.
To implement the check, we record the sizes of symbols in the atom table,
just like we already record their alignments.
|
| |
|
|
|
|
|
|
|
| |
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
* Added semantic for byte swap builtins
The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics.
The semantics is given in terms of the decode/encode functions used for the memory model.
* Added bswap64 expansion to PowerPC 32 bits.
* Added bswap64 expansion for ARM.
|
| |
|
|
|
| |
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
|
| |
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the arguments to __builtin_annot, __builtin_ais_annot,
__builtin_debug, and extended asm statements are treated like
arguments to an unprototyped or vararg function call. In particular,
arguments of type "float" are converted to "double", generating useless
code.
To avoid this extra, useless conversion, this commit changes the types
expected for the arguments to these built-ins and to extended asm
statements. Now they are the types of the arguments themselves, after
performing the usual unary conversions (e.g. char -> int), but without
the problematic float -> double conversion. This ensures that no code
is generated to change the representation of the arguments.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Main changes to CompCert outside of Flocq are as follows:
- Minimal supported version of Coq is now 8.7, due to Flocq requirements.
- Most modifications are due to Z2R being dropped in favor of IZR and to
the way Flocq now handles NaNs.
- CompCert now correctly handles NaNs for the Risc-V architecture
(hopefully).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* bug 24268: avoid assertion after reporting error for invalid call to builtin_debug
* bug 24268, remove duplicated warning tag in lexer messages
* bug 24268, fix spelling in array element designator message
* bug 24268, unify 'consider adding option ...' messages
* bug 24268, add spacing for icbi operands
* bug 24268, uniform use of Ignored_attributes class for identical warnings
* bug 24268, unify message for 'assignment to const type' to error from error/fatal error
* bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
This is a follow-up to commit 6e1a5ce.
Another `open! Floats` is needed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Adds a warning when a volatile struct is assigned to another
struct, that the volatile qualifier is ignored in this context.
Example:
```
volatile struct S s;
struct S t;
t = s; // did not warn before; now it warns
s = t; // did warn already
```
Bug 23489
|
| |
|
|
|
|
|
|
| |
The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST. However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32. This is not correct, esp. on a 64-bit target.
This commit refactors C2C around three integer conversion functions:
convertInt32 producing a Coq "int" (32 bit)
convertInt64 producing a Coq "int64" (64 bit)
convertIntZ producing a Coq "Z" (arbitrary precision)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single
C2C.atom_inline function that returns one of the three possible values
stored in the the a_inline field.
|
| |
|
|
|
|
|
| |
In order to correctly support the noinline attribute we must store
whether the function was specified with an inline specifer, had
a noinline attribute or nothing.
Bug 22642
|
| | |
|
| |
|
|
|
|
| |
The file and line information are now stored as comment string at
the start of each annotation.
Bug 22462
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
|
| | |
|
| |
|
|
|
|
|
| |
The runtime functions are prefixed with compcert in order to
avoid potential clashes with runtime/builtin functions of other
compilers.
Bug 22062
|
| |
|
|
|
|
|
|
|
| |
ISO C99 states that "inline defintions", functions with inline
specifier that are not extern, does not provide an external
definition and another compilation unit can contain an external
definition. Thus in the case of non-static inline functions no
code should be generated.
Bug 21343
|
| |
|
|
| |
The noinline attribute prevents functions from inlining.
|
| |
|
|
|
|
|
|
|
| |
The attribute unused can be used to indicate if a variable or
parameter is unused and no warning should be emitted for it.
Furthermore this commit simplifies the check by adding a generic
function to traverse the program.
Bug 19872
|
| |
|
|
| |
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
|
| |\ |
|
| | |
| |
| |
| |
| | |
- Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type.
- Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/ |
|
| |
|
|
|
|
|
| |
Instead of just accepting a string the function is changed to
accept a format string. This removes a lot of artificial sprintfs
in calls to the functions.
Bug 19872
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This fixes two issues:
1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform.
2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer.
(Reported by Michael Schmidt.)
The fix:
1- Evaluate the 3rd and 4th arguments at type size_t
2- Support both Vint and Vlong as results of this evaluation
3- Declare these arguments with type 'unsigned long'.
Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations.
Concerning part 3 of the fix, type size_t would be better for future
platforms where size_t is bigger than unsigned long, but some more
work is needed to delay the evaluation of C2C.builtins_generic to
after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate
the cparser/ machine configuration before C2C initializes.
|
| |
|
|
|
|
|
| |
is 64 bits
It was wrongly assumed that 'long' is 32 bits.
(Reported by Michael Schmidt.)
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| | |
| |
| |
| |
| |
| | |
This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case.
For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.
|
| | | |
|
