aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'upstream/master'Yann Herklotz2021-09-1748-873/+327
|\
| * Merge branch 'bitfields' (#400)Xavier Leroy2021-08-225-654/+46
| |\
| | * Native support for bit fields (#400)Xavier Leroy2021-08-225-654/+46
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | 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
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0848-192/+240
| | | | | | | | | | | | 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_unreachableXavier Leroy2021-05-021-1/+5
| | | | | | | | 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>
| * Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-191-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * "macosx" is now called "macos"Xavier Leroy2021-01-182-3/+3
| | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
| * Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | | | | | | | | | | | | | Follow-up to 35e2b11db. Put the warning "pragmas are ignored inside functions" inside the Unnamed category, so that it is displayed by default and cannot be disabled.
| * Ignore and warn about pragmas inside functionsXavier Leroy2021-01-071-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Pragmas can occur either outside external declarations, at the top level of a compilation unit, or within a compound statement, inside a function definition. The parse tree in cparse/C.mli cannot represent pragmas occuring within a compound statement. In this case, the elaborator used to silently move the pragma to top level, just before the function definition where the pragma occurs. It looks safer to just ignore pragmas occurring inside a function definition, and emit a specific warning.
| * AArch64: macOS portXavier Leroy2020-12-262-0/+4
| | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
| * C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | | | | | | | | | All the built-in types declared in $ARCH/CBuiltins.ml are now recognized as type names initially.
* | Ignore unnecessary foldersYann Herklotz2020-11-271-1/+0
|/
* Check ptr arithmetic for ++ and --Bernhard Schommer2020-09-201-10/+16
| | | | | Also: improve check for ptr - integer. (Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
* Add new static-assert token for deLexer utility; bug 29273Michael Schmidt2020-08-041-0/+1
|
* Add comments we missed to sync to GitHubChristoph Cullmann2020-07-301-0/+2
|
* Allow string_literals_list in _Static_assert.Bernhard Schommer2020-07-272-24/+25
| | | | | | Not all pre-processors concatenate string literal lists, however they are allowed in _Static_assert. This is similar to the rules for inline assembly etc.
* More checks for __builtin_va_start (#250)Bernhard Schommer2020-07-211-6/+10
| | | | We check that this builtin function is only called from within a variadic function and has the correct number of arguments.
* cparser/handcrafted.messages: missing blank lineXavier Leroy2020-07-211-0/+1
|
* Updated handcrafted.messages.Bernhard Schommer2020-07-211-0/+108
| | | | | Added error descriptions for the new syntax errors introduced by '_Static_assert'.
* Support _Static_assert from C11Xavier Leroy2020-07-217-1060/+1116
|
* Support __builtin_constant_p as in GCC and Clang (#367)Xavier Leroy2020-07-211-0/+10
| | | | | Returns 1 if the argument is a constant expression, 0 otherwise. Closes: #366
* Use the correct location for Slabaled in transform.Bernhard Schommer2020-07-211-2/+2
|
* Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
| | | | | | We check in the initial environment if a function is already defined to avoid redefinition of functions that are part of the builtin environment.
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-5/+5
|
* 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.
* Use library function.Bernhard Schommer2020-06-281-4/+1
| | | | | | | The function String.uppercase was deprecated and the replacement function String.upercase_ascii was only available from OCaml 4.03.0. Since the minimal OCaml version is now 4.05.0 we can use the function String.upercase_ascii.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-2/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
|
* Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
|
* Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
|
* Include typedef name in error message (#228)Bernhard Schommer2020-03-041-2/+2
| | | In case of redefinition of a typedef name with a different type.
* The type of a wide char constant is wchar_t. (#223)Bernhard Schommer2020-02-241-1/+2
| | | | See ISO C2011 standard, section 6.4.4.4 para 11.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
* Support vertical tabs and treat them as whitespace (#218)Bernhard Schommer2020-02-181-1/+1
| | | | Some preprocessors don't remove the vertical tab from the input so we should be able to handle them in the lexer.
* Added error for unknown builtin functions. (#208)Bernhard Schommer2019-12-211-1/+6
| | | | | | | | | Previously, using an unknown builtin function was treated like any other call to an undeclared function: a warning was emitted, and an error occurred at link-time. With this commit, using an unknown builtin function is an error, like in Clang.
* Added back unused_ais_parameter warning.Bernhard Schommer2019-11-261-0/+1
|
* Simplified diagnostics module.Bernhard Schommer2019-11-251-118/+41
| | | | | | | Instead of constructing four different lists for maintaining the state of the warnings only one list is now used. This list contains the name of the warning and a boolean indicating whether this option should be active by default. The rest is computed from this list.
* Remove duplicated ticks.Bernhard Schommer2019-10-011-2/+2
|
* Use pointer type for evaluated constants.Bernhard Schommer2019-10-011-1/+1
|
* Various improvements for diagnostics.Bernhard Schommer2019-09-303-10/+34
| | | | | | | | | | | | | | | | | | | | | | | | * Extend check for incomplete type. Extended the check to also include a check for variables with incomplete object type that are not arrays, that have an initializer. Furthermore the warning includes the type and variable name. * Warning for incomplete type in compound literals. Incomplete types are not allowed for compound literals, except for array types. * Extend type printing function. The type of a typedeof of an anonymous type should not be printed. Furthermore added '<anonymous>' to the printing of anonymous types. * Unify incomplete type errors message. The incomplete type error messages should all look the same including name of the variable, parameter, etc. and then the incomplete type.
* Functions that are extern should stay extern (#201)Bernhard Schommer2019-09-251-1/+1
| | | | | | In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier). Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
* AArch64 portXavier Leroy2019-08-082-0/+6
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Make __builtin_sel available from C source codeXavier Leroy2019-07-171-0/+36
| | | | | 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-1712-87/+62
| | | | | | | | | 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 condition for warning of conditional exprBernhard Schommer2019-07-101-1/+1
| | | | | | The warning should only be active if the optimization is active, so the check is only performed when the warning is active and additionally the command line flag -Obranchless is specified.
generated by cgit (git 2.34.1) at 2024-06-28 02:46:49 +0000