| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
Follow-up to bb5dab848
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers. (Issue #319.)
|
|
|
|
|
| |
Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info.
Closes: #226.
|
|
|
|
|
| |
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.
|
|
|
|
| |
Added types for global_definitions in order to avoid problems with
implicit parameters. This should fix issue 215
|
|
|
|
| |
This should fix issue 216 and also allows it to print 64 bit offsets.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
| |
Bug 18768.
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|/
|
|
|
| |
Removed unused code and code generating warnings.
Bug 18394
|
|
|
|
| |
clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.
So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq.
This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
- Revised printing of intermediate RTL code.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
instead, thread a single generator through all functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
Short doc in exportclight/README
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|