aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'towards_2.10' of ../towards_3.10 into kvx-workDavid Monniaux2021-09-304-716/+0
|\
| * Merge remote-tracking branch 'origin/kvx-work' into towards_3.10David Monniaux2021-09-271-0/+559
| |\
| * | Refactor clightgenXavier Leroy2021-09-225-1300/+0
| | | | | | | | | | | | | | | | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
| * | clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-151-16/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 `_`.
| * | Native support for bit fields (#400)Xavier Leroy2021-08-221-1/+30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-084-16/+20
| | | | | | | | | | | | | | | | | | 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.
| * | Update the output of clightgen to pick the `$` notation from its new placeXavier Leroy2021-04-231-1/+3
| | | | | | | | | | | | Follow-up to bb5dab848
| * | 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
* | | better failDavid Monniaux2021-09-271-1/+1
| |/ |/|
* | fix clightgenDavid Monniaux2021-09-271-0/+3
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-014-28/+46
|/ | | | cfrontend/C2C.ml
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-2/+2
| | | | | | 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 `string_of_ident` conversionXavier Leroy2020-10-121-0/+110
| | | | | | This is the left inverse of `ident_to_string`. Closes: #372
* Use exact arithmetic for printing positive numbersXavier Leroy2020-09-221-52/+56
| | | | | | And also for the computations in name_temporary. Overflowing OCaml's integer types is unlikely in actual use but happened in the past owing to another mistake (see issue #370).
* Fix computation of next temporary in -canonical-idents modeXavier Leroy2020-09-221-1/+12
| | | | | | | Variables were confused for temporaries, causing the temporaries introduced by this pass to be very big integers. Fixes: #370
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-0/+1
|
* clightgen: fix the printing of annotationsXavier Leroy2020-06-051-59/+8
| | | | | | | | | | | | The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360
* clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
| | | | Closes: #358
* clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
| | | | | | | | In the original code, collisions could occur: an identifier could be numbered with a number that happens to be equal to its canonical encoding. This was harmless but confusing. Closes: #358
* Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-193-17/+128
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-2/+10
| | | | | | | | | | 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.
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-281-4/+4
| | | | | A "dollar" sign in a function name or a global variable name was producing incorrect Coq identifiers. (Issue #319.)
* clightgen -dclight: print function parameters correctlyXavier Leroy2019-09-161-1/+1
| | | | | | | | | | | | | The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314
* Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
| | | | | | | | The clightgen tracing options did not result in printing of the intermediate files, but were ignored. Added also two new options, `-dprepro` to print the preprocessed file and `-dall` to dump all intermediate files.
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
| | | | In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-202-4/+21
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-15/+18
| | | | | | | | | | | | | | | | | * Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
* Share code for common options.Bernhard Schommer2018-01-291-70/+15
| | | | | | In order to avoid more divergence between the command line options of clightgen and ccomp the code for the common options, the language support options, the version string and the general options.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| | | | | | | | Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
| * Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
| | | | | | | | This should fix issue 216 and also allows it to print 64 bit offsets.
* | Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
|/ | | | | Clightgen also now has command line flags to control warnings as well as some other general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-20/+1
| | | | | The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function. This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
| | | Also allow preprocessed source files as input.
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
|
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
|
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-031-1/+1
| | | | | | | | | Replaced calls to Filename.temp_file by own version Driveraux.tmp_file. The Driveraux.tmp_file function takes care that the temporary files are removed at exit. Consequently there is no need to explicitly remove temp files in Driver.
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
| | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
| | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-152-13/+33
| | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* clightgen: add option -normalize to ensure that memory loads never occur ↵Xavier Leroy2017-06-122-2/+177
| | | | | | | | | | | | | | | | | | | | | "deep" inside expressions For example, with this option, tmp = *(x + 0) + *(x + 1) in the original Clight is rewritten to tmp1 = *(x + 0) tmp2 = *(x + 1) tmp = tmp1 + tmp2 with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads. Squashed commit of the following: commit 3fb69dae567b1305383b74ce1707945f91369a46 commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
|
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+6
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-1/+3
|\
| * Implement support for big endian arm targets.Bernhard Schommer2016-08-051-1/+3
| | | | | | | | | | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* | Additional test for color output.Bernhard Schommer2016-08-051-10/+10
|/ | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
generated by cgit (git 2.34.1) at 2024-05-09 06:52:42 +0000