aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* Bytecode-only build (#243)Xavier Leroy2020-07-072-4/+29
| | | | | | If ocamlopt (the native-code OCaml compiler) is not available, fall back to building with ocamlc (the bytecode OCaml compiler). Fixes: #359
* Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
| | | | | Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`. Fixes: #363
* Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
|
* Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
|
* Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
|
* Move shared code in new file.Bernhard Schommer2020-06-2817-96/+46
| | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-2810-19/+1
| | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
* 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-288-9/+8
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
| | | | | | | | | | | | | | | A typical example is `(void) __builtin_sel(a, b, c)`. It is safe to generate zero code for these uses of builtins because builtins whose semantics are known to the compiler are pure. Other builtins with side effects (e.g. `__builtin_trap`) are not known and will remain in the compiled code. It is useful to generate zero code for these uses of builtins because some of them (e.g. `__builtin_sel`) must be transformed into proper CminorSel expressions during instruction selection. Otherwise, they propagate all the way to ExpandAsm, causing a "not implemented" error there.
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
| | | | In particular __builtin_sel.
* Preliminary support for Coq 8.12Xavier Leroy2020-06-212-4/+4
| | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead.
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-213-3/+3
| | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
| | | | Follow-up to commit 070babef.
* 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.
generated by cgit (git 2.34.1) at 2024-06-18 12:12:46 +0000