aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
Commit message (Collapse)AuthorAgeFilesLines
* Fix a comment in Cstrategy.v (#485)Xuyang Li2023-04-051-2/+2
|
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-101-2/+2
| | | | | | | | | | | | | | | * Define our own `Z_div_mod_eq` lemma The one in the Coq standard library is deprecated since 8.14, but its replacement changed type between 8.13 and 8.14. So the only way to remain compatible from 8.12 to 8.16 is to define our own lemma. Phew. * Do not use `Arith.Max`, deprecated. * Do not use `plus_lt_compat_r`, deprecated. * Do not use `beq_nat_refl` and `beq_nat_true`, deprecated.
* Don't discard argument of `__builtin_va_end`Michael Schmidt2023-01-231-2/+2
| | | | | | Instead, evaluate it for the side effects it may contain. Fixes: #474
* C2C: wrong handling of typedefs to enums in bit fieldsXavier Leroy2023-01-231-1/+1
| | | | Fixes: #472
* Fix incomplete checking of unsolved holes (#465)Gaëtan Gilbert2022-11-281-1/+1
| | | | Adaptation to https://github.com/coq/coq/pull/16743
* Merge pull request #459 from AbsInt/full-switchXavier Leroy2022-11-091-84/+18
|\ | | | | Handle Duff's device and other unstructured `switch` statements
| * Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-291-84/+18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - New elaboration pass: SwitchNorm - recognizes structured 'switch' statements and puts them in a normalized form; - if selected, transforms unstructured 'switch' statements into a structured switch with goto actions + the original switch body with appropriate labels and gotos. - C2C treatment of 'switch' statements is simplified accordingly. - New language support option `-funstructured-switch`. - Some tests were added (test/regression/switch3.c).
* | SimplExpr: revised handling of nested conditional, `||`, `&&` operatorsXavier Leroy2022-10-013-98/+165
|/ | | | | | | | | | | | | | | In a `For_set` destination, a temporary can be reused only if it always used with the same type. Otherwise, typing of Cminor code fails later in the compilation pipeline. This commit implements temporary reuse if and only if the typing constraint is respected. - For `&&` and `||`, it avoids the possibility of wrong reuse (as reported in #453). - For nested conditional expressions, it improves a bit the generated code by reusing the temporary when possible. Fixes: #453
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-191-102/+95
| | | | | | | | | | | | | | | | | * Support C11 Unicode string literals and character constants * Add tests for C11 string literals and character constants * Better error message for ill-formed universal character names E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits. * Add new warning `invalid-utf8` for byte sequences that are not valid UTF8. The warning is activated but not fatal by default. * Warn on uses of C11 Unicode character constants and string literals This uses the `c11-extensions` warning, which is off by default. * Support preprocessing option -finput-charset= for GNU toolchains
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-192-0/+7
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* Rework of struct member offsets for debug info.Bernhard Schommer2022-09-031-12/+45
| | | | | | | | | | | | | The struct member byte and bit offsets are now set based upon the new function `struct_layout` from Ctypes.v, thus using the same code to compute as used to generate the actual struct access. The struct offset member information is addded using the types computed after the translation in C2C. Therefore we need to store the new internal names of the members as well as the composites and use them when adding the offset information. Fixes: #445
* Introduce `struct_layout` functionBernhard Schommer2022-09-031-0/+26
| | | | | The `struct_layout` function computes for each member, that is neither padding nor zero-length, the same result as `field_offset`.
* Support mergeable sections for string literals and wide string literalsXavier Leroy2022-08-291-6/+13
| | | | | Note that strings containing null characters (code 0) cannot be put in a mergeable section, as this will confuse the linker's merging criterion.
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-291-2/+2
| | | | | | | | | | | | On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
* Fix a typo in a comment in Clight.v (#427)Hanzhi Liu2022-04-251-1/+1
| | | | `Kloop1` should have been `Kloop2`.
* 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.
* An improved PTree data structure (#420)Xavier Leroy2021-11-163-8/+2
| | | | | | | | | | | | | | This PR replaces the "PTree" data structure used in lib/Maps.v by the canonical binary tries data structure proposed by A. W. Appel and described in the paper "Efficient Extensional Binary Tries", https://arxiv.org/abs/2110.05063 The new implementation is more memory-efficient and a bit faster, resulting in reduced compilation times (-5% on typical C programs, up to -10% on very large C functions). It also enjoys the extensionality property (two tries mapping equal keys to equal data are equal), which simplifies some proofs.
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-034-7/+7
| | | | This avoids a new warning of Coq 8.14.
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-3/+3
| | | | The change is backward compatible with Coq 8.9 to 8.13 (at least).
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-0/+2
| | | | | | Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403
* Merge branch 'bitfields' (#400)Xavier Leroy2021-08-2219-1604/+3295
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-2219-1604/+3243
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Add Ctypes.link_match_program_genXavier Leroy2021-08-221-0/+52
| | | | | | | | | | A more general version of the link_match_program linking theorem. It supports match_fundef relations parameterized by the source compilation unit.
* | 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-0812-48/+60
| | | | | | 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.
* 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.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-4/+4
| | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
* Support re-normalization of function parameters at function entryXavier Leroy2021-01-162-17/+36
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to pass arguments that are not normalized.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-219/+222
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* Changed cc_varargs to an option typeBernhard Schommer2020-12-254-10/+18
| | | | | | 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.
* 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
|
* Move shared code in new file.Bernhard Schommer2020-06-281-1/+1
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-281-1/+1
| | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
| | | | In particular __builtin_sel.
* SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
| | | | Follow-up to commit 070babef.
* SimplExpr: better translation of casts in a "for effects" contextXavier Leroy2020-06-153-136/+166
| | | | | | | | This is useful for statements such as `(void) expr;` where we would prefer not to explicitly compute intermediate values of type `void` and store them in Clight temporary variables. See issue #361 for a real-world occurrence of this phenomenon.
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-1/+6
| | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* 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.
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-29/+44
| | | | | | | | According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334
* Support re-normalization of values returned by function callsXavier Leroy2020-02-212-33/+137
| | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-216-39/+78
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* 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.
* Take the sign into account for int to ptr cast.Bernhard Schommer2020-02-122-2/+3
| | | | | | | Casting from an integer constant to pointer on 64 bit architectures did not take the signedness into account and always interpreted the integer as unsigned which causes some incompatibility with libc implementations.
* 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.
* -dclight output: use nicer names for temporary variablesXavier Leroy2019-09-161-2/+11
| | | | | | | | | | | | | | | | | | | | | The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names.
generated by cgit (git 2.34.1) at 2024-05-18 05:53:36 +0000