| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
It seems necessary that the mulitplication for the high part of
split registers is put into brackets.
Bug 23169
|
| |
|
|
|
| |
The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199
|
| |
|
|
|
|
| |
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
|
| | |
|
| |
|
|
|
| |
struct/union arguments to annotations should not be transformed at top level,
but the regular function calls contained within must be transformed recursively.
|
| |
|
|
|
|
|
| |
In order to ensure that no transformation for arguments to
builtin annotations are used, the original unchanged arguments are
used.
Bug 23179
|
| |
|
|
|
|
|
| |
This should help with parallel builds, which currently fail sometimes
owing to a lack of a dependency on pre_parser_aux.cmi.
Also: move documentation comments from the .ml to the .mli
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Make sure struct/union arguments to __builtin_annot and related
builtins are always passed by reference using the default passing mode,
regardless of the ABI for passing struct/unions to "real" functions.
This ensures portability of annotations across ABIs, and avoids mismatches
between the annotation text and the actual number of arguments
(when a struct/union argument is passed as N integer arguments).
A similar special case already existed for __builtin_va_arg.
|
| |
|
|
|
|
| |
Printing variable names with the default expression printer
results in newlines in the outputed error message.
Bug 23169
|
| |
|
|
|
|
| |
The strings for json need quoting of special characters such as
\" and \\.
Bug 22438
|
| |
|
|
|
|
| |
x2 is the stack pointer of the riscV, both sp and x2 are supported
but to be safe use x2 in annotations.
Bug 23176
|
| | |
|
| |
|
|
|
|
| |
This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
|
| |
|
|
|
|
| |
It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and
'sp' for riscV.
Bug 23176.
|
| |
|
|
|
| |
Registers should not contain the % prefix for ais annotations.
Bug 23176
|
| |
|
|
|
|
|
|
| |
Include the format specifier in error message when available in
order to make it easier to spot the broken ais parameter.
Futhermore introduce a new warning for unused ais parameters.
Bug 22464
|
| | |
|
| | |
|
| |
|
|
|
| |
Mention that it is a global memory cell.
Fix 22464
|
| |
|
|
|
|
| |
This should avoid problems when newlines are used in string
constants etc.
Bug 23172
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |\
| |
| | |
Move the struct-return / struct-passing platform aspects from compcert.ini to cparser/Machine.ml
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Since the used configuration for passing and returning values
struct values is pretty much static it can be hardwired into the
machine settings.
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When x is known to be either 0 or 1, comparisons such as
x == 0 x != 0 x == 1 x != 1
can be optimized away. This optimization was already performed
for signed comparisons. This commit extends the optimization to
unsigned comparisons as well.
Additionally, for PowerPC only, some unsigned (dis)equality comparisons are
turned into signed comparisons when we know it makes no difference,
i.e. when both arguments are guaranteed not to be pointers. The
reason is that Asmgen can produce shorter instruction sequences for
some signed equality comparisons than for the corresponding unsigned
comparisons.
It's important to optimize unsigned integer comparisons because casts
to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons.
In particular, cascades of casts to _Bool are now reduced to a single
cast much more often than before.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
In 32-bit mode, a symbolic reference "symbol + ofs" (address of "symbol" plus "ofs" bytes) can always be resolved by the linker into a 32-bit quantity that fits the 32-bit displacement field of x86 addressing modes.
Not so in 64-bit mode: first, the displacement field is still 32 bits but the full address is 64 bits; second, the displacement is relative to the RIP instruction pointer. In the "small code model" that CompCert uses for x86-64, excessively large offsets lead to link-time overflows of this 32-bit displacement field.
This commit addresses the issue by limiting the "ofs" part of "symbol + ofs" global addressing models to the range [-2^24, 2^24 - 1]. As explained in the AMD64 ELF ABI document, this is a safe range in the small code model, under the assumption that no global symbol is bigger than 2^24 bytes. GCC seems to be using a wider range [-2^31, 2^24 - 1] but I'd rather be safe.
The limitation of the "ofs" offset is achieved by extending the mechanisms already present to ensure that "ofs" in "reg + ofs" indexed addressing modes fits in 32-bit signed:
- Op.addressing_valid checks that the "ofs" part of "symbol + ofs" addressing modes is in the correct interval;
- SelectOp.addressing turns invalid addressings into lea's + indexed addressings;
- Asmgen.normalize_addrmode_64 turns lea's with invalid addressings into simpler lea's + addq of the large offset.
|
| | |
|
| | |
|
| |
|
|
|
| |
When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'. (Relying on the error code is not enough.)
|
| |
|
|
|
|
|
|
| |
addressing
In the original code, the addressing_valid check is skipped if we are in 32 bits, because we know the check is always true. This is correct but not obvious nor future-proof. (In the future we may want to make addressing_valid more strict.)
This commit restructures ConstpropOp.addr_strength_reduction so that the addressing_valid check is always performed.
|
| |
|
|
|
|
|
|
|
|
| |
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)
|
| |
|
|
|
|
| |
This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs.
Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| | |
|
| |
|
|
|
|
| |
In order to avoid more divergence between the command line options of
clightgen and ccomp the code for the common options, the language support
options, the version string and the general options.
|
| |
|
|
|
| |
This change is backwards compatible, and makes flocq compatible with
https://github.com/coq/coq/pull/6596. Was applied to the Flocq master sources
https://gitlab.inria.fr/flocq/flocq/commit/db356aa5ea0fd0234e3872f70e8972086055cd57
|
| |\ |
|
| | |
| |
| |
| | |
Added types for global_definitions in order to avoid problems with
implicit parameters. This should fix issue 215
|
| | |
| |
| |
| | |
This should fix issue 216 and also allows it to print 64 bit offsets.
|
| |/
|
|
|
| |
Clightgen also now has command line flags to control warnings as
well as some other general options.
|
| | |
|
