In -no-flat-float-array mode, instead of always returning
`best_msig` (the most permissive signature), we first compute the
flat-float-array separability signature -- falling back to `best_msig`
if it fails.
This discipline is conservative: it never rejects -no-flat-float-array
programs. At the same time it guarantees that, for any program that is
also accepted in -flat-float-array mode, the same separability will be
inferred in the two modes. In particular, the same .cmi files and
digests will be produced.
Before we introduced this hack, the production of different .cmi files
would break the build system of the compiler itself, when trying to
build a -no-flat-float-array system from a bootstrap compiler itself
using -flat-float-array. See #9291.
We produce exhaustivity counter-example in the order of the
specialized submatrices. Having submatrices in source order gives the
nice behavior that the clause that would naturally been inserted first
in the source is given first as a counter-example.
Consider for example:
function
| true, true -> true
| false, false -> false
The two counter-examples are (true, false) and (false, true).
Before this patch, (false, true) would be shown first.
After this patch, (true, false) is shown first.
This corresponds to the following natural completion order:
function
| true, true -> true
| true, false -> ?
| false, false -> false
| false, true -> ?
On the other hand, the ordering of the default submatrix, with respect
to the specialized submatrices, is not preserved -- it is always
ordered last.
One could intuitively expect the default submatrix to appear in the
position of the first omega row in the source. We tried this, and
it is not a good idea:
- the change is much more invasive as the interface of
`build_specialized_submatrices` has to change
- the behavior of the result is in fact unpleasant; it is not
intuitive to order counter-examples in this way.
For example, consider:
function
| _, None -> false
| true, Some true -> false
The two exhaustivity counter-examples are (true, Some false)
and (false, Some _). The second comes from the default submatrix:
morally it is (_, Some _), with "some other constructor missing from
the column" instead of the first _. There is no reason to suppose that
the user would want to place this (_, Some _) or (false, Some _)
counter-example first in the completed code; indeed, this intuition
would suggest writing an exhaustive covering of patterns of the
form (_, foo), inserted after the first clause, but then the other
clauses below become unnecessary!
When an omega patterns appears high in the column like this, it is
usually because there is a very specific matching condition to the
rest of its row, that justifies some shortcutting behavior. The
program is typically *not* completed by adding more specific matching
conditions.
This solves exponential-blowup issue with the strict traversal and/or
strict witness computation in cases where an exponential number of
counter-examples is generated. This fixes Stack Overflow and
exponential-time issues on examples using or-patterns heavily,
including one that naturally found its way in real-world user
code (see the following testsuite commit).
We now systematically keep only one counter-example, instead of
letting the type-checker decide whether to discard
counter-examples (in Backtrack_or mode) or to preserve
them (in Refine_or mode).
Note: in the exhaustivity warning, there are sub-messages printed to
indicate that:
- the exhaustivity counter-example is related to an extensible type, or
- that a when-guarded clause does match the counter-example
In both cases the warning is there to explain the counter-example(s)
shown (not a property of all counter-examples); keeping at most one
valid counter-example means that they will be printed less often, but
it is the correct/intended behavior in that case.
This loses no information (descriptions contain the tag), but it will
make it easier to obtain the descriptions inside `combine_constructor`
without doing a dynamic check on the patterns. This will in turn help
simplify the interaction with `Parmatch.complete_constrs`.
Note: after this patch we use `Types.equal_tag` instead of `( = )` to
compare tags during pattern-matching compilation. This is better code,
and we believe that it does not change the behavior: `Types.equal_tag`
is mostly similar to a type-specialized version of `( = )`, except
that it calls `Ident.same` that just compares the stamps and ignore
the names, which (assuming well-formedness of idents) is equivalent
and slightly faster.
Instead of using the stdlib logf function for computing logarithms, we
use a faster polynomial-based approximation.
We use the xoshiro PRNG instead of the Mersenne Twister. xoshiro is
simpler and faster.
We generate samples by batches so that compilers can vectorize the
generation loops using SIMD instructions when possible.
- coreboot + opt.opt gives a faster build than bootstrap + opt.opt
- Restore the original bootstrap compilers on exit, so that
other-configs works (it performs several builds in sequence).
The default build procedure is broken in --disable-flat-float-array mode
since PR#2188 was merged. This commit unblocks temporarily the situation
by using a build with bootstrap for --disable-float-float-array-mode.
Clang's thread sanitizer TSAN reports a (false?) alarm on Unix.system
in multithreaded programs now that Unix.system is implemented
on top of posix_spawn.
This commit replaces Unix.system with Sys.command, which might work
better with TSAN, based on preliminary experiments.
Note that this test is about file I/O, not Unix.system, so the replacement
is acceptable. In parallel, we need to understand what's happening
with TSAN and posix_spawn.
On PowerPC 32 bits Linux, recent versions of GCC produce "secure PLT"
relocatable code by default, while ocamlopt still generates "BSS PLT"
relocatable code. This causes a warning at link-time when "BSS PLT"
object files (produced by ocamlopt) are being linked.
This PR makes sure that "-mbss-plt" is added to the OC_LDFLAGS and
MKSHAREDLIB variables on PowerPC 32 bits Linux.
Gabriel Scherer
Etienne Millon
Manuel Hornung
Nicolás Ojeda Bär
Greta Yorsh
David Allsopp
Jacques-Henri Jourdan
Jacques Garrigue
Stephen Dolan
Xavier Leroy
Xavier Leroy