aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' into dev/michalisdev/michalisYann Herklotz2021-09-17337-8490/+12887
|\
| * Fix compilation of verilog back endYann Herklotz2021-09-172-102/+77
| |
| * Replace omega by liaYann Herklotz2021-09-177-52/+57
| |
| * Merge remote-tracking branch 'upstream/master'Yann Herklotz2021-09-17328-8336/+12753
| |\
| | * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-158-5/+13
| | | | | | | | | | | | | | | | | | 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
| | * clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-152-16/+28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 `_`.
| | * Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-132-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * Share code for memory access for PowerPCBernhard Schommer2021-09-064-166/+159
| | | | | | | | | | | | | | | | | | 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`.
| | * Protect against overflows in `leaq` (all forms)Bernhard Schommer2021-08-271-22/+27
| | | | | | | | | | | | | | | | | | | | | | | | leaq's offsets can overflow (not fit in 32 bits) in other cases than those fixed in 4daebb7a0, 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.
| | * Protect against overflows in `leaq N(src), dst` (#407)Xavier Leroy2021-08-271-12/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * Merge branch 'bitfields' (#400)Xavier Leroy2021-08-2245-2305/+4004
| | |\
| | | * Native support for bit fields (#400)Xavier Leroy2021-08-2242-2299/+3866
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-223-6/+6
| | | | | | | | | | | | | | | | | | | | | | | | Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
| | | * Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
| | | |
| | | * More lemmas about `align`Xavier Leroy2021-07-261-0/+17
| | | |
| | | * More lemmas about list appendXavier Leroy2021-07-261-0/+26
| | | |
| | * | 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.
| | * | x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * | Support `# 0 ...` preprocessed line directiveXavier Leroy2021-06-011-1/+1
| | |/ | | | | | | | | | | | | | | | | | | Before, the line number had to start with a nonzero digit. However, the GCC 11 preprocessor was observed to produce `# 0 ...` directives. Fixes: #398
| | * Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-132-3/+5
| | | | | | | | | | | | E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
| | * Update for release 3.9v3.9Xavier Leroy2021-05-101-1/+1
| | |
| | * Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
| | |
| | * Update for release 3.9Xavier Leroy2021-05-091-4/+5
| | | | | | | | | | | | Also: limit the max width of the page, to avoid very long lines.
| | * Update ChangelogXavier Leroy2021-05-081-1/+11
| | |
| | * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-08149-860/+1171
| | | | | | | | | | | | | | | | | | 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.
| | * Fix evaluation order in emulation of bitfield assignmentXavier Leroy2021-05-021-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bitfield assignment `x.b = f()` is expanded into a read-modify-write on `x.carrier`. Wrong results can occur if `x.carrier` is read before the call to `f()`, and `f` itself modifies a bitfield with the same carrier `x.carrier`. In this temporary fix, we play on the evaluation order implemented by the SimplExpr pass of CompCert (left-to-right for side-effecting subexpression) to make sure the read part of the read-modify-write sequence occurs after the evaluation of the right-hand side. More substantial fixes will be considered later. Fixes: #395
| | * 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-028-2/+32
| | | | | | | | | | | | Not yet used for optimizations.
| | * Fix spurious error on initialization of struct with flexible array memberXavier Leroy2021-05-021-0/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The following is correct but was causing a "wrong type for array initializer" fatal error. ``` struct s { int n; int d[]; }; void f(void) { struct s x = {0}; } ``` Co-authored-by: Michael Schmidt <github@mschmidt.me>
| | * Update ChangelogXavier Leroy2021-04-291-0/+53
| | |
| | * Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| | | | | | | | | | | | | | | | | | | | | Variables without init do not generated any assembly code so no entry in the json AST should be generated. They correspond to extern variables without initializer that are defined in another compilation unit. Bug 30112
| | * MacOS: add a #define __DARWIN_OS_INLINEXavier Leroy2021-04-271-2/+2
| | | | | | | | | | | | | | | Seems necessary for the standard headers of a recent version of XCode. The actual definition in the standard headers is only for GNUC.
| | * Support Coq 8.13.2Xavier Leroy2021-04-271-2/+2
| | |
| | * More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
| | | | | | | | | | | | | | | | | | | | | Volatile load and store are expanded later and also use the ld/std instructions, therefore the same fixes that are applied as well for them. Bug 30983
| | * Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The offsets immediates used in the ld and std instructions must be a multiple of the word size. This commit changes the two functions which are used when generating load/stores in Asmgen, accessind and transl_memory_access. For accessind one only needs an additional check that the offset is a multiple of the word size for the case that the high part of the offset is zero, since otherwise the immediate is loaded into a register anyway. The transl_memory_access function needs some slightly more complex adoption. For all variants that do not construct the address in a register before hand we must check that the offsets are multiples of the word size and additionally if a symbol is used that the alignment of the symbol is also a multiple of the word size. Therefore a new parameter is introduced that allows checking the alignment. In order to reduce the code duplication for the proofs these two functions get an additional parameter in order to indicate wether the offset needs to be a multiple of the word size or not. Bug 30983
| | * Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| | | | | | | | | | | | Follow-up to bb5dab848
| | * Remove `-version-file` option from option summaryXavier Leroy2021-04-231-1/+0
| | | | | | | | | | | | | | | The `-version-file` option was removed in commit 600803cae, but remained in the option summary, as reported in #386.
| | * Move `$` notation in submodule `ClightNotations` and scope `clight_scope`Xavier Leroy2021-04-231-11/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This avoids a nasty conflict with Ltac2 notations as reported in #392. The old `$` notation in scope `string_scope` was not used yet, AFAIK. The new submodule and the new scope are the right places to add future notations to facilitate working with the output of clightgen. Fixes: #392
| | * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-194-36/+16
| | |
| | * Bump minimal Coq version to 8.9.0Xavier Leroy2021-04-191-2/+2
| | | | | | | | | | | | This is required to have List.repeat in the standard library (next commit).
| | * Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-194-2/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When desugaring a bitfield, allow any integral type that is 32 bits or smaller. Previously this was checking the rank of the type rather than the size. This rank check caused issues with standard headers that declare `uint32_t` to be an `unsigned long` rather than an `unsigned int`. Here, any bitfields declared as `uint32_t` were failing to compile even though they are still actually 32 bits. Co-authored-by: Amos Robinson <amos@gh.st>
| | * Refactor cparser/Parse.mlXavier Leroy2021-04-191-31/+29
| | | | | | | | | | | | | | | | | | | | | | | | | | | - Use pipeline notation `|>` for legibility and better GC behavior (in bytecode at least). - Introduce auxiliary functions. - Remove useless function parameters. - Fix the timing of the "Emulations" pass (because of an extra parameter, what was timed took zero time).
| | * Ensure compatibility with future versions of MenhirLibXavier Leroy2021-04-191-6/+7
| | | | | | | | | | | | | | | | | | | | | | | | After Menhir version 20210310, the `Fail_pr` constructor of the `parse_result` type becomes `Fail_pr_full` with two extra arguments. This PR enables CompCert to handle both versions of the `parse_result` type in MenhirLib.
| | * Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
| | | | | | | | | | | | | | | | | | coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters. There was one place in CompCert where one of these automatically-generated names was used. This commit avoids using this name.
| | * Coq 8.13.1 is supportedXavier Leroy2021-03-091-2/+2
| | | | | | | | | | | | Closes: #389
| | * Fix regression on PowerPC / DiabXavier Leroy2021-02-232-4/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On PowerPC/Diab, common declarations must not be used for small data sections. Add a `~common` option to `PrintAsmaux.variable_section` to control the use of common declarations. The default is whatever is specified on the command line using the `-fcommon` and `-fno-common` options. Use `~common:false` for `Section_small_data` on PowerPC / Diab. Note that on PowerPC/Linux, GCC uses common declarations for uninitialized variables in small data section, so we keep doing this in CompCert as well.
| | * Section handling: finer control of variable initializationXavier Leroy2021-02-239-42/+90
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-236-35/+34
| | | | | | | | | | | | | | | | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
| | * Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| | | | | | | | | | | | | | | | | | | | | | | | Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile.
generated by cgit (git 2.34.1) at 2024-05-17 09:27:33 +0000