[DO NOT MERGE] V3.11 #11
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
As reported in #399, it seems better to use `##` instead of `#` as comment delimiter under macOS. For the time being we keep using `#` for Linux and Cygwin. Closes: #399
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.
Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
A more general version of the link_match_program linking theorem. It supports match_fundef relations parameterized by the source compilation unit.
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.
If N does not fit in signed 32 bits, `leaq` cannot be used and `mov; addq` must be used instead. This was already the case for `leaq` instructions produced by the Asmgen pass, but not for some `leaq` instructions produced by Asmexpand. Normally, assemblers should fail if the `leaq` offset is not representable, but this is not always the case (see issue #406). Fixes: #406
leaq's offsets can overflow (not fit in 32 bits) in other cases than those fixed in 4daebb7, e.g. in the expansion of __builtin_memcpy_aligned. This commit implements full normalization of the `leaq` instructions produced in Asmexpand, following the same method used in Asmgen.
Instead of duplicating the memory access code in `Asmexpand.ml` we move the code for each of the different addressings in `Asmgen.v` into separate functions that then can be reused in `Asmexpand.ml`.
Warning 69 "mutable record field is never mutated": 3 occurrences in backend/IRC.ml removed the "mutable" qualifier on these fields Warning 70 "cannot find interface file" many .ml files have no .mli no strong motivation to add the .mli files turned off the warning in Makefile.extr
In the Clight AST, padding bit fields (such as `int : 6;`) in composite declarations are given an ident that corresponds to the empty string. Previously, clightgen would give name `_` to this ident, but this is not valid Coq. This commit gives name `empty_ident` to the empty ident. This name does not start with an underscore, so it cannot conflict with the names for regular idents, which all start with `_`.
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
The return type is Tint8unsigned (i.e. _Bool), not Tint.
Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
Stack offsets must be multiple of 8 when using ldp/stp instructions and multiple of the transferred size when using other load/store instructions with offsets greater than 256. For simplicity, always require that the offset is multiple of 8. Fixes: #410
In the "small" case, there was an error in the choice of temporary registers to use when one argument is a stack location and the other is a register. The chosen temporary could conflict with the argument that resides in a register. Fixes: #412
For compatibility with the upcoming Coq 8.14.
For compatibility with Coq 8.14. Cherry-picked from upstream commit 2e3c2441
Add support to clightgen for generating Csyntax AST as .v files
E.g. `struct { int; int x; };`. The `int;` declaration provides no name,
is not a bit field, and is not a C11 anonymous struct/union member.
Such declarations are not allowed by the C99 grammar, even though GCC,
Clang and CompCert tolerate them. The C11 grammar allows these
declarations but the standard text gives them no meaning.
CompCert used to warn about such declarations, yet include them in the
struct or union as unnamed members, similar to an unnamed bit field.
This is incorrect and inconsistent with what GCC and Clang do.
With this commit, CompCert still warns, then ignores the declaration
and does not create an unnamed member. This is consistent with GCC
and Clang.
Fixes: #411
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
Follow-up to c34d25e
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.
…ersions For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428
`Kloop1` should have been `Kloop2`.
Otherwise, BinarySingleNaN.Bleb_correct cannot be proved.
Upgrade to Flocq 4.1.
Enum types should only be compatible with the underlying integer type, not all integer types. Bug 33212
The `pp_indication` optional argument that governs formatting boxes in types was not propagated recursively, causing boxes to appear.
Before, in casts, `int (*)()` was parsed like `int (*)(void)`. This caused expressions like `((int (*)()) &f)(42)` to be rejected. Declarations were correctly parsed.
Entirely handled during elaboration. No impact on the verified part of CompCert.
- Emit the warning even for functions without parameters `int f() {...}`
- Show what the type is after prototyping
- Refactor this part of `elab_fundef` slightly
At some places the ".c" was hard coded as suffix for computing the output filenames. This lead to problems if for example `-S`or `-c` is used with preprocessed files. Bug 33196
Since we are sure that all files passed have a valid extension we can use the OCaml function Filename.remove_extension and don't need to pass the suffixes. Bug 33218
- Honor "noreturn" attributes and _Noreturn declarations on calls to function pointers. - Don't crash if a function type is an unknown typedef. (This can happen with local typedefs.) Instead, conservatively assume this function can return.
CompCert doesn't maintain a frame pointer in X29. However, it must treat X29 as callee-save, so that CompCert-generated code can be called from code that uses X29 as frame pointer. This commit makes X29 callee-save. In places where X29 was used as a temporary, X15 or X14 is used instead.
As suggested by Léo Gourdin in #437. The previous expansion as a plain "j" instruction fails when the jump offset is too large to be represented (issue #436). Fixes: #436 Closes: #437
Fixes: #435
Handle constructors with 5, 6 and 7 arguments. Handle lists.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
snu-sf/CompCertM#25 와 짝인 CompCertR 수정입니다.