aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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.
* Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
| | | | Updated configure script to also allow coq version 8.11.2
* Improve portability of the test for annotations inclightgenXavier Leroy2020-06-052-0/+4
| | | | __builtin_ais_annot is not supported for macOS nor for Cygwin.
* clightgen: fix the printing of annotationsXavier Leroy2020-06-052-59/+14
| | | | | | | | | | | | 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-194-20/+204
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#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
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+0
| | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/
* Update the list of dual-licensed filesXavier Leroy2020-05-051-2/+2
| | | | Closes: #351
* Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
| | | | | | The corresponding files in all other ports are dual-licensed (GPL + non-commercial), there is no reason it should be different for aarch64.
* Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | | | | So as not to depend on an implicit import from module Program. (See PR #352.)
* Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | | | | | On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
* Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | | | | The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`.
* Do not use "Declare Scope", introduced in Coq 8.10 onlyXavier Leroy2020-05-041-1/+0
|
* Coq-MenhirLib: explicit import ListNotations (#354)Jacques-Henri Jourdan2020-05-047-4/+12
| | | | | import ListNotations wherever it is necessary so that we do not rely on it being exported by Program. (See #352.) This is a backport from upstream: https://gitlab.inria.fr/fpottier/menhir/-/commit/53f94fa42c80ab1728383e9d2b19006180b14a78
* Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-292-1/+19
| | | | | | | | The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script.
* Updated .gitignoreBernhard Schommer2020-04-271-0/+1
| | | | compile.pl is a build artefact.
* Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
| | | | Don't use sed, just echo the contents of the file.
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-204-8/+8
| | | | | | | 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.
* Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
| | | | Update configure script.
* 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
|
* Updates for release 3.7v3.7Xavier Leroy2020-03-311-1/+1
|
* Updates for release 3.7Xavier Leroy2020-03-312-1/+6
|
* Update ChangelogXavier Leroy2020-03-311-3/+34
|
* Double rounding error in int64->float32 conversions on PowerPC and ARMXavier Leroy2020-03-304-24/+22
| | | | | | | | | The "stof" and "utof" runtime functions contain a round-to-odd step that avoids double rounding. However, this step was incorrectly coded on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making round-to-odd ineffective and causing double rounding. Closes: #343
* Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
| | | | | This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32.
* Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-293-12/+25
| | | | | | | | 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.
* 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.
* Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
| | | | | | | | Double FP arguments passed on stack were incorrectly aligned: they must be 8-aligned but were 4-aligned only. This was due to the use of `Location.typealign`, which is the minimal hardware-supported alignment for a given type, namely 1 word for type Tfloat. To get the correct alignments, `Location.typesize` must be used instead.
* Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | | | | The proof script for Events.excall_free_ok was incomplete if Archi.ptr64 is unknown (as in the RISC-V case).
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-022-43/+74
| | | | | | | | 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
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-022-18/+35
| | | | | | | | Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals.
* Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
|
* In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
| | | | | | | | | | The EABI and the SVR4 ABI state that single-precision FP arguments passed on stack are passed as a 64-bit word, extended to double-precision. This commit implements this behavior by using a stack slot of type Tany64. Not only this ensures that the slot is of size and alignment 8 bytes, but it also ensures that it is accessed by stfd and lfd instructions, using single-extended-to-double format.
* Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
| | | | | | | | | | | | Until now the types Tany32 and Tany64 were not used prior to register allocation, so IRC.class_of_type did not need to be defined for those types. However, there are possible uses of stack slots of type Tany32 and Tany64 to specify calling conventions. For this purpose, we need to define class_of_type for Tany32 and Tany64. We follow the informal convention that Tany32 goes in integer registers and Tany64 goes into integer registers if 64-bit wide, or FP registers otherwise.
* Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
| | | | | | | | | GCC does passes single arguments as singles on the stack but diab and the eabi say single arguments should be passed as double on the stack. This commit changes the alignment of single arguments to 4 for gcc based backends.
* Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
| | | | | | | | | | | | We were implementing the ABI described in the RISC-V Instruction Set Manual, version 2.1. However, this ABI was superseded by the RISC-V ELF psABI specification. This commit changes the calling conventions to better match the ELF psABI specification. This should greatly improve interoperability with code compiled by other RISC-V compilers. One incompatibility remains: when all 8 FP argument registers have been used, further FP arguments should be passed in integer argument registers if available, while this PR passes them on stack.
* 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.
* Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-247-649/+68
| | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions.
* AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
| | | | | | | According to AAPCS64 (the AArch64 ABI specification), the top bits of the register containing the function result have unspecified value, so we need to sign- or zero-extend the function result before using it, as in the x86 port.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-215-6/+6
| | | | | | "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.
* Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
|
* Support re-normalization of values returned by function callsXavier Leroy2020-02-217-33/+174
| | | | | | | | | | | | | | | | | | | | | | | | | 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-2143-286/+445
| | | | | | | | | | 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.
* 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.
* 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.
* Added base address if needed.Bernhard Schommer2020-02-063-33/+53
| | | | | | | | Ranges of locations are relative to some base address. Most times this is just the same as the compilation unit. However if the compilation unit contains functions in multiple sections we need to add a base address of the section that the locations are contained.
generated by cgit (git 2.34.1) at 2024-07-01 06:04:40 +0000