Summary:
Since the llvm bindings package has a setup step that is normally done
when pinning the opam package, to build when it is instead vendored
requires adding a setup step to the sledge build.
Reviewed By: martintrojer
Differential Revision: D27188295
fbshipit-source-id: edb0b317c
Summary:
This allows using the upsteam LLVM 11 library unchanged, only
extensions to the OCaml bindings are needed. Therefore this is to
enable building sledge using e.g. `dnf install llvm-11` or `brew
install llvm@11` instead of cloning and building a fork of llvm.
Reviewed By: jvillard
Differential Revision: D27188301
fbshipit-source-id: f441dbecd
Summary:
The ~20% hit in compilation time is dominated by the time saved
running the tests. This also makes the memory allocation numbers more
robust to inconsequential changes. Note that `make check` is still
fast.
Note that normally dune passes `-g` to ocamlopt itself, but not if the
build profile includes an `ocamlopt_flags` entry. So add it explicitly
to ensure that compilation includes debug symbols.
(Also remove `-error-style short` that was missed in 9c4f263.)
Reviewed By: jvillard
Differential Revision: D25756570
fbshipit-source-id: 94d18bac2
Summary:
Currently intrinsics are treated as functions, with Call instructions
to possibly-undefined functions with known names. This diff adds an
Intrinsic instruction form to express these more directly and:
- avoid the overhead of intrinsics needing to end blocks
- avoid the overhead of the function call machiery
- avoid the complexity of doing the string name lookup to find their
specs, repeatedly
This diff only adds the backend support, the added Intrinsic
instructions are not yet generated by the frontend.
Reviewed By: jvillard
Differential Revision: D25146155
fbshipit-source-id: f24024183
Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.
This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.
Reviewed By: ngorogiannis
Differential Revision: D24989070
fbshipit-source-id: c21b275f5
Summary:
Remove `-error-style short` from the compilation flags since it causes
merlin to complain, see https://github.com/ocaml/merlin/issues/1176.
After this diff, developers will need to set `OCAML_ERROR_STYLE=short`
in their environment.
Reviewed By: jvillard
Differential Revision: D24306066
fbshipit-source-id: 9c4f26393
Summary:
Just to avoid confusion over directories named 'bin' being expected to
contain binaries, rather than the sources of executables.
Reviewed By: jvillard
Differential Revision: D23636372
fbshipit-source-id: 8593380e6
Summary:
The `sledge-help.txt` file is under source control, and should not be
removed by `make clean`.
Reviewed By: ngorogiannis
Differential Revision: D23497893
fbshipit-source-id: 2061160a8
Summary:
Add a `sledge-report` executabe to aggregate and report results from
test runs. Results from possibly-many test runs are averaged and
reported in an html file with color-coded indications of performance
improvement or regression.
Reviewed By: ngorogiannis
Differential Revision: D23459521
fbshipit-source-id: 61ca936f4
Summary:
Add a Report.status type to represent the overall status of an
analysis run, and revise handling of backtraces to preserve the trace
of the originally-raised exception in more cases.
Reviewed By: ngorogiannis
Differential Revision: D23459518
fbshipit-source-id: a99fe0d14
Summary:
The SLEdge internal first-order theory solver targets the "word
problem", where a query has the form `C ⊢ L` where `C` is a
conjunction of literals and `L` is a single literal. This can be
abused to implement a naive SMT solver using an expansion to
disjunctive-normal form and checking `C ⊢ false` for each branch `C`
of the DNF. This is not useful as an SMT solver, but can be used for
testing.
Reviewed By: ngorogiannis
Differential Revision: D23459524
fbshipit-source-id: 5483e5a84
Summary:
It is not needed or very meaningful since the addition of type-based
disambiguation.
Reviewed By: jvillard
Differential Revision: D22401035
fbshipit-source-id: 31996f946
Summary:
Refer to Llair modules using `Llair.` qualifier, except for in
`Frontend`, which makes so much use of `Llair` that it is now opened
(`Llair` only contains types and modules, so `open` is safe).
Reviewed By: jvillard
Differential Revision: D21720979
fbshipit-source-id: dd42075d9
Summary:
It is now possible to not spew dune files all over the repo, and opam
files aren't needed either.
Reviewed By: jvillard
Differential Revision: D21720978
fbshipit-source-id: 553e1d154
Summary:
If both the library and binary are named `sledge`, then compilation
works fine and resolves the names correctly, but merlin gets confused
and cannot find the sledge library modules used in the bin sources. So
the binary and library need different names. The name of the library
gets exposed to clients, while the name of the binary only determines
the name of some files in the _build directory, which can be renamed
as desired. Therefore, use the `sledge` name for the library module,
and rename the binary module to `sledge_cli`, but still have dune
install it as `sledge.exe`.
Reviewed By: jvillard
Differential Revision: D20589431
fbshipit-source-id: 14b65907d
Summary:
Move definitions of profiles from `dune-workspace` to `dune` since it
seems to be ok to use profiles in `dune-workspace` that are only
defined in `dune`. Since the `dune` but not `dune-workspace` file is
used when building as a vendored dependency, this seems to be
preferable.
Also, change the `opt` profile into a wildcard, which seems to be
preferable from the vendored-building perspective.
Also, set library public names such that including `sledge` in the
`libraries` phrase of `dune` files works.
Reviewed By: ngorogiannis
Differential Revision: D20376179
fbshipit-source-id: f2b634716
Summary:
Move files, adjust build system, etc.
This also separates out the ppx_trace conditional compilation debug
tracing machinery into an independent package and library.
Reviewed By: jvillard
Differential Revision: D20322876
fbshipit-source-id: a50522462
Summary:
To easily monitor and track changes to the help generated by the
command line interface, generate it in full and add it to the repo.
Reviewed By: kren1
Differential Revision: D16059783
fbshipit-source-id: be15f9943
Summary: Dune now includes support for ocamlformat, so use it to format in parallel.
Reviewed By: mbouaziz
Differential Revision: D10389485
fbshipit-source-id: cb1dfbe38
Josh Berdine