| Age | Commit message (Collapse) | Author |
|---|
|
Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.
There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.
Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
|
|
|
|
The first field of accumulators points out of the OCaml heap, so using
closures instead of tag-0 objects is better for the GC.
Accumulators are distinguished from closures because their code pointer
necessarily is the "accumulate" address, which points to an ACCUMULATE
instruction.
|
|
The second field of a closure can no longer be the value of the first free
variable (or another closure of a mutually recursive block) but must be an
offset to the first free variable.
This commit makes the bytecode compiler and interpreter agnostic to the
actual representation of closures. To do so, the execution environment
(variable coq_env) no longer points to the currently executed closure but
to the last one. This has the following consequences:
- OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block
(counted from last to first);
- ENVACC(n) now always loads the value of the n-th free variable.
These two changes make the bytecode compiler simpler, since it no
longer has to track the relative position of closures and free variables.
The last change makes the interpreter a bit slower, since it has to adjust
coq_env when executing GRABREC. Hopefully, cache locality will make the
overhead negligible.
|
|
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Add headers to a few files which were missing them.
|
|
* This commit add float instructions to the VM, their encoding in bytecode
and the interpretation of primitive float values after the reduction.
* The flag '-std=c99' could be added to the C compiler flags to ensure
that float computation strictly follows the norm (ie. i387 80-bits
format is not used as an optimization).
Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
because the latter would disable GNU asm used in the VM.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
It was actually a hack since those names are never used to represent
values, only to be passed as arguments to bytecode instructions. So
instead of reusing the structured_constant type, we follow the same
pattern as switch annotations.
|
|
|
|
|
|
|
|
|
|
We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.
This grants wish BZ#5659.
|
|
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
|
|
|
|
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
