aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-03-011-13/+16
|\
| * Check for arguments of struct/union type passed to a vararg functionXavier Leroy2022-02-111-13/+16
| | | | | | | | | | | | | | If any are found, make sure that `-fstruct-passing` was given. Previously, we used to check the fixed arguments (as part of a call to `checkFunctionType`) but not the variable arguments.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-24/+118
|\|
| * Merge branch 'bitfields' (#400)Xavier Leroy2021-08-221-5/+34
| |\
| | * Native support for bit fields (#400)Xavier Leroy2021-08-221-5/+34
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Revise the declaration of __compcert_* helper functionsXavier Leroy2021-06-301-82/+79
| |/ | | | | | | | | | | Don't put them in the C environment used for elaboration. Instead, add them directly to the generated CompCert C at the end of the C2C translation.
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | | | | | | | 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.
| * Support __builtin_expectXavier Leroy2021-05-021-0/+5
| | | | | | | | | | | | | | Not yet used for optimizations. Actually, __builtin_expect is removed during C2C conversion, otherwise the conversion to type "long" produces inefficient code on 64-bit platforms.
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+3
| | | | | | | | Not yet used for optimizations.
* | Commenting out __builtin_expect from AbsIntCyril SIX2021-06-011-2/+2
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+13
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-6/+18
|\| | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+12
| | | | | | | | | | | | Instead of being a simple boolean we now use an option type to record the number of fixed (non-vararg) arguments. Hence, `None` means not vararg, and `Some n` means `n` fixed arguments followed with varargs.
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+17
|\|
| * Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-301-1/+1
| | | | | | | | | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+2
| | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| * Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-0/+12
| | | | | | | | These functions are now available on all targets.
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+2
| |
* | Merge remote-tracking branch 'origin/mppa-expect3' into mppa-workDavid Monniaux2020-04-091-2/+11
|\ \
| * | expect operationDavid Monniaux2020-04-071-0/+8
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-expectDavid Monniaux2020-04-061-5/+22
| |\ \
| * | | __builtin_expect defined as its first argumentDavid Monniaux2019-09-251-2/+3
| | | |
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-081-2/+2
|\ \ \ \ | | |/ / | |/| |
| * | | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-2/+2
| |\ \ \ | | | |/ | | |/|
| | * | Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-291-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-031-4/+36
| |\ \ \ | | |/ / | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-251-3/+15
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-241-3/+15
| |\| | | | | |/ / | |/| | | | | | mppa-work-upstream-merge
| | * | More precise determination of small data accesses (#220)Bernhard Schommer2020-02-201-3/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | thread local declarations now workDavid Monniaux2020-02-241-1/+5
| | | |
* | | | it now works, no more ugly hack to access thread local dataDavid Monniaux2020-02-241-0/+9
| | | |
* | | | seems to process _Thread_local but not till backendDavid Monniaux2020-02-241-7/+14
|/ / /
* | / Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-12-091-0/+5
|\| | | |/ |/| | | mppa-work-upstream-merge
| * Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-281-0/+5
| | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-08-281-1/+3
|\| | | | | | | mppa-work-upstream-merge
| * bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | * 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.
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-25/+45
|\| | | | | | | mppa-work-upstream-merge
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+9
| | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| * Remove the cparser/Builtins moduleXavier Leroy2019-07-171-7/+10
| | | | | | | | | | | | | | | | | | 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()`.
| * Change the expected types for arguments to __builtin_annot, and extended asmXavier Leroy2019-06-191-5/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-5/+5
|\| | | | | | | mppa-if-conversion
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
| | | | | | | | | | | | 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.
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | 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).
* | ternary ops for float/doubleDavid Monniaux2019-04-031-0/+4
| |
* | problem in ValueAOpDavid Monniaux2019-04-031-0/+1
| |
* | attempts at generating builtins, startDavid Monniaux2019-04-031-1/+8
| |
* | la division flottante fonctionneDavid Monniaux2019-03-201-2/+16
| |
* | ça semble passerDavid Monniaux2019-03-201-2/+4
| |
* | added helper functions but strangeDavid Monniaux2019-03-191-1/+17
|/ | | | idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
generated by cgit (git 2.34.1) at 2024-05-20 00:55:40 +0000