| Age | Commit message (Collapse) | Author |
|---|
|
catching `Not_found`
`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
|
|
This removes the need for the remote counter.
|
|
This seems the official name, the byterun name is just an artifact
from the very preliminary dune build.
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
PArray.set has arity 4, but due to the polymorphic universe, its actual
arity is 5. As a consequence, Kshort_apply cannot be used to invoke it
(or rather its accumulating version).
Using Kapply does not quite work here, because Kpush_retaddr would have to
be invoked before the arguments, that is, before we even know whether the
arguments are accumulators. So, to use Kapply, one would need to push the
return address, push duplicates of the already computed arguments, call
the accumulator, and then pop the original arguments.
This commit follows a simpler approach, but more restrictive, as it is
still limited to arity 4, but this time independently from universes. To
do so, the call is performed in two steps. First, a closure containing the
universes is created. Second, the actual application to the original
arguments is performed, for which Kshort_apply is sufficient.
So, this is inefficient, because a closure is created just so that it can
be immediately fully applied. But since this is the accumulator slow path,
this does not matter.
|
|
Despite their names, APPLY1 to APPLY4 are completely different from
APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return
address was already pushed on the stack, before the arguments were. On the
other hand, APPLY1 to APPLY4 insert the return address in the middle of
the already pushed arguments.
|
|
|
|
This avoids having to drop the last element of the signature in the
common case.
|
|
|
|
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.
|
|
constant expected
Reviewed-by: ppedrot
|
|
Fix #13987
|
|
stack.
Reviewed-by: ppedrot
|
|
Reviewed-by: silene
|
|
transitively closed
Reviewed-by: ppedrot
|
|
|
|
This makes it possible to skip the check when scanning the stack for the
garbage collector.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
Fix #13903
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
caml_something_to_do.
Reviewed-by: gasche
Ack-by: ppedrot
Reviewed-by: xavierleroy
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
called (fix #13849).
The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.
This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
|
|
|
|
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
|
|
Since the compiler initializes the arities to zero, coq_tcode_of_code
wrongly believes that the word following a primitive operation contains
an opcode, while it is the global index of the primitive operation. So,
the function will try to translate it and thus corrupt it. But as long as
the evaluated term fully reduces (which is always the case for
CoqInterval), the corrupted word will never be read.
At this point, it all depends on the arity of the global index (seen as
an opcode). If it is zero, then coq_tcode_of_code will recover and
correctly translate the following opcodes. If it is nonzero, then the
function starts translating random words, possibly corrupting the memory
past the end of the translation buffer. Independently of this memory
corruption, coq_interprete will execute random code once it gets to the
opcode following the primitive operation, since it has not been
translated.
The reason CoqInterval is not always crashing due to this bug is just
plain luck. Indeed, the arity of the pseudo opcode only depends on the
global index of the primitive operations. So, as long as this arity is
zero, the memory corruption is fully contained. This happens in the vast
majority of cases, since coq_tcode_of_code translates any unrecognized
opcode to STOP, which has arity zero.
This bug is exploitable.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Also works for simpl.
|
|
MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
|
|
The generated bytecode almost never needs to modify the field of an OCaml
object. The only exception is the laziness mechanism of coinductive types.
But it modifies field 2, and thus uses the generic opcode SETFIELD anyway.
|
|
The PUSHFIELDS opcode is a costly one, yet lots of constructors have at
most one usable argument (e.g., option, nat, positive, Z, Acc). For those
constructors, PUSHFIELDS(1) is replaced by GETFIELD(0);PUSH, assuming
the accu register is no longer used afterwards.
Replacing one single opcode by two opcodes might seem like a
pessimization, but it is not. Indeed, pattern-matching branches usually
start by filling the accu register with a constructor argument or the
value of a free variable or a constant. All of those offer peephole
optimizations for PUSH, which means that the number of opcodes actually
stay constant.
Note that, for the same reason, the assumption above holds in practice:
the accu register is no longer used after PUSHFIELDS.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
Instead we export a representation function that gives a high-level view
of the data structure in terms of constraints.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
We need this file for the upcoming kernel representation change there.
|
|
Reviewed-by: SkySkimmer
|
|
|
