| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
|
|
|
|
|
|
|
| |
If ocamlopt is not available, use ocamlc instead of ocamlopt to build
auxiliary tools (tools/modorder, tools/ndfun).
This is a follow-up to commit 9af28924.
|
|
|
|
|
|
|
| |
This is a follow-up to commit 3b1f3dd5, which was wrong in that
errors in a shell pipeline were not correctly detected.
Fixes: #363
|
| |
|
| |
|
|
|
|
| |
This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
|
|
|
|
|
|
| |
The version string dumped in the file should be the same as the version
string printed by `-version`. The option is also not printed by `-help`
since it is for internal use only.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
If ocamlopt (the native-code OCaml compiler) is not available,
fall back to building with ocamlc (the bytecode OCaml compiler).
Fixes: #359
|
|
|
|
|
| |
Use `ocamlfind query menhirLib` in preference to `menhir --suggest-menhirLib`.
Fixes: #363
|
| |
|
| |
|
| |
|
|
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
|
|
|
|
| |
The function is in fact just a call to the
function`is_callee_save_register` from `Conventions1.v`.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
In particular __builtin_sel.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Follow-up to commit 070babef.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Updated configure script to also allow coq version 8.11.2
|
|
|
|
| |
__builtin_ais_annot is not supported for macOS nor for Cygwin.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
Closes: #358
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(#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
|
|
|
|
|
|
| |
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/
|
|
|
|
| |
Closes: #351
|
|
|
|
|
|
| |
The corresponding files in all other ports are dual-licensed
(GPL + non-commercial), there is no reason it should be different for
aarch64.
|
|
|
|
|
| |
So as not to depend on an implicit import from module Program.
(See PR #352.)
|
|
|
|
|
|
| |
On some versions of Coq, "nil" is of type "Rlist"...
This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
|
|
|
|
|
| |
The rest of the code base uses `nil`, so let's be consistent.
Also, this avoids depending on `Import ListNotations`.
|
| |
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
compile.pl is a build artefact.
|
|
|
|
| |
Don't use sed, just echo the contents of the file.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Update configure script.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|