| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
This prevents the existence of a few naked pointers to C heap from the OCaml
heap. VM bytecode is represented as any block of size at least 1 whose first
field points to a C-allocated string.
This representation is compatible with the Coq VM representation of
(potentially recursive) closures, which are already specifically tailored
in the OCaml GC to be able to contain out-of-heap data.
|
| |
|
|
|
|
| |
The previous code was mimicking what the C implementation was doing, which
was a quadratic algorithm. We simply use the good old exponential reallocation
strategy that is amortized O(1).
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ |
|
| |
|
|
|
|
| |
This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.
|
|
|
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.
|
Maxime Dénès
Pierre-Marie Pédrot
Théo Zimmermann