Summary:
At least when installation of the conf-llvm package uses a non-system
llvm, additional compilation flags are needed. These can be queries by
asking opam for the location of the llvm-config binary, and asking
that for the compilation flags.
Reviewed By: ngorogiannis
Differential Revision: D28907810
fbshipit-source-id: 6806c78a8
Summary:
Generating the help file runs sledge, which refers to the
SLEDGE_CONFIG environment variable. This dependency was missing from
the build rule.
Reviewed By: ngorogiannis
Differential Revision: D28907804
fbshipit-source-id: e20178c6e
Summary:
Broken html could be generated if there were multiple status entries
for a single test.
Reviewed By: ngorogiannis
Differential Revision: D28907807
fbshipit-source-id: 5fcb30b5f
Summary:
It is possible for normalization to change a term from an
uninterpreted application to e.g. an interpreted atom. For instance,
the conversion `(u1)-1` evaluates to `1`. Context.canon_extend was not
taking this into account, and as a result could violate the
representation invariant of Context.t.
Reviewed By: ngorogiannis
Differential Revision: D28907806
fbshipit-source-id: 9b5171e15
Summary:
Allow joining relations with distinct entry states, since the
destinations will be the same, there is no loss of context
sensitivity. As a result, check that the call stack of the
destinations of edges are equal before joining, as it is no longer
implicitly ensured by the equal entry state check.
This change leads to joining a state with itself often, as the entry
states are often idential, so this diff also adds an optimization of
join with a fast path for joining identical states.
Reviewed By: ngorogiannis
Differential Revision: D28907809
fbshipit-source-id: 2c66223ff
Summary:
The control scheduler treats functions as if they were syntactically
inlined, by including a call stack in each control flow edge,
implicitly copying each function's control-flow graph for each calling
context. A "depth" is maintained for each retreating edge,
representing the number of times the edge has been crossed. The depths
are used to explore executions with fewer loop iterations before those
with more iterations.
The current implementation is incorrect in some situations involving
mutually recursive functions where the cycle detection algorithm
determines that calls to one of the mutually recursive functions need
not be considered retreating. Currently return frames of recursive
calls are filtered out of call stacks for the purposes of tracking
edge depths. This is insufficient in such mutual recursive
situations. This diff fixes this by explicity ignoring the entire
stack of recursive call edges.
Reviewed By: ngorogiannis
Differential Revision: D28907813
fbshipit-source-id: e04849ca8
Summary:
The formatting of sugared list syntax regressed with
https://github.com/ocaml-ppx/ocamlformat/pull/1567.
Reviewed By: ngorogiannis
Differential Revision: D28907812
fbshipit-source-id: 16ad68218
Summary: The llvm code to avoid formatting is now under `vendor` not `llvm`.
Reviewed By: da319
Differential Revision: D28907808
fbshipit-source-id: ae9444f49
Summary:
Add a mode which executes randomly-chosen paths depth-first, without
duplicating the work of executing shared prefixes. This mode is to be
used when hoping to get lucky and quickly choose a path that exhibits
a bug, but is slower to achieve coverage than the default.
Differential Revision: D27996963
fbshipit-source-id: 20a7a32c5
Summary:
The configuration options for the analysis are used only/principally
in Control, they do not belong in the interface of domains. Also, the
definition of the used_globals type for the results of the used
globals pre-analysis belongs to the Domain_used_globals module.
Reviewed By: jvillard
Differential Revision: D27828752
fbshipit-source-id: e42de74e0
Summary:
Just reorder definitions to clarify that as_inlined_location is not
used in the rest of Stack.
Reviewed By: jvillard
Differential Revision: D27828755
fbshipit-source-id: 1436f1e6d
Summary: Preparation for allowing a choice among several scheduler strategies.
Reviewed By: jvillard
Differential Revision: D27828759
fbshipit-source-id: 63d6ec203
Summary:
The priority queue does not crucially depend on the type of
elements. This diff makes it parametric.
Reviewed By: jvillard
Differential Revision: D27828756
fbshipit-source-id: a7bfc4ee5
Summary:
When domain join operations are total, the control scheduler does not
need to handle the case where joining states is undefined. This leads
to some simplification, and in particular removed the need to expose a
remove operation for the scheduling queue.
Reviewed By: jvillard
Differential Revision: D27828761
fbshipit-source-id: b8cdd2eb6
Summary:
The only domain with a partial join is the lifting of a predicate
domain to a relation one, where the entry states are required to be
equal. This situation now indicates a programming error in the
analysis, rather than something that the domain should be responsible
for. Therefore this diff changes that check to an assertion and
simplifies the remaining join operations which are all total.
Reviewed By: jvillard
Differential Revision: D27828763
fbshipit-source-id: ec52ff741
Summary:
llvm-config can return the lib dir without manual manipulation using
an assumed relative path from llvm-config to the lib dir. Also fix
missing semicolon to appease shell variable semantics.
Reviewed By: jvillard
Differential Revision: D27828757
fbshipit-source-id: 5080c8671
Summary:
Mainly code cleanup. The only potential functional change is to
eliminate the test that a function returning with an empty stack is an
entry point, which should always hold anyhow.
Reviewed By: jvillard
Differential Revision: D27828749
fbshipit-source-id: 25124a568
Summary:
Mainly code simplification. The only functional change is to move the
test that a candidate entry-point function has no formals earlier,
with the result of avoiding failure if a function with an entry-point
name but with formals is encountered before an entry-point function
with no formals.
Reviewed By: jvillard
Differential Revision: D27828751
fbshipit-source-id: d5a832952
Summary:
There used to be a bug where recursive calls were not correctly
bounded. This is no longer needed, and this diff removes the
workaround that was added in D15577134 (881a4d10af) / 4cd3b62.
Reviewed By: jvillard
Differential Revision: D27828764
fbshipit-source-id: 80265a588
Summary:
Specifying that sledge should stop execution when the first report is
made via e.g. `sledge l a -t Stop` currently only works when debug
tracing is enabled. This diff fixes this so that `-t Stop` also works
for the release build.
Reviewed By: jvillard
Differential Revision: D27828753
fbshipit-source-id: dd7511ff1
Summary:
Currently all alarms are reported as "Invalid memory access", which is
not accurate for `abort` and hence assertion violations. This diff
adds an explicit type for alarms which distinguishes these two
cases. Further refinement is left for later.
Reviewed By: jvillard
Differential Revision: D27828754
fbshipit-source-id: 9c33f3c86
Summary:
The computation of common prefixes and suffixes was wrong. In
particular, the computation of the common suffix did not correctly
consider the common prefix. This manifested in case one entire
sequence is a suffix of the other.
Reviewed By: ngorogiannis
Differential Revision: D27564874
fbshipit-source-id: 267a75102
Summary:
If either all or no tracing is enabled, it is not necessary to compute
the module and function names for each Trace operation to determine
whether or not it is enabled. This diff optimizes this case.
Reviewed By: ngorogiannis
Differential Revision: D27564869
fbshipit-source-id: bf766eb2f
Summary:
Switch to a stronger but more expensive operation to check if a
symbolic heap is unsatisfiable.
Reviewed By: ngorogiannis
Differential Revision: D27564872
fbshipit-source-id: c8e306408
Summary:
By default compiling with `-O0` adds `optnone` annotations, which
prevents the transformations sledge explicitly performs. This diff
adds a flag to disable this uncooperative behavior.
Reviewed By: ngorogiannis
Differential Revision: D27564879
fbshipit-source-id: 061397e3f
Summary:
`Typ.equivalent` relates types that denote the same sets of values in
the semantic model, such as pointers and integers of the appropriate
size. This diff strengthens the treatment of casts between such types
in the first-order solver by translating `(s)(t)e` to `e` for
equivalent types `s` and `t`.
These casts are usually simplified out of the bitcode produced by
clang. However, code using `_Atomic(...)` leads to `load atomic` llvm
instructions that, for some reason, cast pointers to i64 and back.
Reviewed By: ngorogiannis
Differential Revision: D27564881
fbshipit-source-id: 6138eb4f1
Summary:
When solving equations such as `α[o,l) = β`, the memory theory solver
computes a term to represent the length of α. This fails if α is a
variable (which might itself be equal to a sized term elsewhere in the
formula). This diff fixes such failures by generating a fresh variable
for the length in such situations.
Reviewed By: ngorogiannis
Differential Revision: D27564871
fbshipit-source-id: e5e066b77
Summary:
It is desirable to programmatically enable backtrace printing in debug
mode, but in other modes it should not forcably disabled. For example,
after this diff, executing
```
$ OCAMLRUNPARAM=b sledge.trc ...
```
now prints a backtrace if an unhandled exception is raised.
Reviewed By: ngorogiannis
Differential Revision: D27564883
fbshipit-source-id: 66ea5efe2
Summary:
This diff `#define`s the functions to which `assert` compiles to
`abort`. This enables the analyzer to report assertion violations, and
is independent of platform.
Also add a simple test to check that it is detected correctly.
Reviewed By: ngorogiannis
Differential Revision: D27564870
fbshipit-source-id: 5517ca910
Summary:
The removal of CAMLprim left the code in need of an application of
clang-format. There are various other changes made by clang-format
which it seems ought to be rolled together into this diff.
Upstream Differential Revision: https://reviews.llvm.org/D99477
Reviewed By: ngorogiannis
Differential Revision: D27564876
fbshipit-source-id: 8e22eb099
Summary:
The CAMLprim macro has not been needed since OCaml 3.11, and is
defined to the empty string. This diff removes all instances of it.
Upstream Differential Revision: https://reviews.llvm.org/D99476
Reviewed By: ngorogiannis
Differential Revision: D27564877
fbshipit-source-id: 14745646b
Summary:
The current code does not follow the simple interface to the OCaml GC,
where GC roots are registered conservatively, only initializing
allocations are performed, etc. This is intentional, as stated in the
opening file comments. On the other hand, the current code does
register GC roots in many situations where it is not strictly
necessary. This diff omits many of them.
Upstream Differential Revision: https://reviews.llvm.org/D99475
Reviewed By: ngorogiannis
Differential Revision: D27564873
fbshipit-source-id: f9e5b183f
Summary:
Using the `cstr_to_string` function that allocates and initializes an
OCaml `string` value enables simplifications in several cases. This
change also has the effect of avoiding calling `memcpy` on NULL
pointers even if only 0 bytes are to be copied.
Upstream Differential Revision: https://reviews.llvm.org/D99474
Reviewed By: ngorogiannis
Differential Revision: D27564875
fbshipit-source-id: b316adfe1
Summary:
Using the `caml_alloc_some` and `ptr_to_option` functions that
allocate OCaml `option` values enables simplifications in many
cases. These simplifications also result in avoiding unnecessary
double initialization in many cases, so yield a minor optimization as
well.
Also, change to avoid using the old unprefixed functions such as
`alloc_small` and instead use the current `caml_alloc_small`.
A few of the changed functions were slightly rewritten in the
early-return style.
Upstream Differential Revision: https://reviews.llvm.org/D99473
Reviewed By: ngorogiannis
Differential Revision: D27564884
fbshipit-source-id: 17883785c
Summary:
In several functions an OCaml block is allocated and no further OCaml
allocation functions (or other functions that might trigger allocation
or collection) are performed before the block is fully initialized. In
these cases, it is safe and slightly more efficient to allocate an
uninitialized block.
Also, the code does not become more complex after the non-initializing
allocation, since in the case that a non-small allocation is made, the
initial values stored are definitely not pointers to OCaml young
blocks, and so initializing via direct assignment is still safe. That
is, in general if `caml_alloc_small` is called, initializing it with
direct assignments is safe, but if `caml_alloc_shr` is
called (e.g. for a block larger than `Max_young_wosize`), then
`caml_initialize` should be called to inform the GC of a potential
major to minor pointer. But if the initial value is definitely not a
young OCaml block, direct assignment is safe.
Upstream Differential Revision: https://reviews.llvm.org/D99472
Reviewed By: ngorogiannis
Differential Revision: D27564878
fbshipit-source-id: 20cd69e92
Summary:
Using `Store_field` to initialize fields of blocks allocated with
`caml_alloc_small` is unsafe. The fields of blocks allocated by
`caml_alloc_small` are not initialized, and `Store_field` calls the
OCaml GC write barrier. If the uninitialized value of a field happens
to point into the OCaml heap, then it will e.g. be added to a conflict
set or followed and have what the GC thinks are color bits
changed. This leads to crashes or memory corruption.
This diff fixes a few (I think all) instances of this problem. Some of
these are creating option values. OCaml 4.12 has a dedicated
`caml_alloc_some` function for this, so this diff adds a compatible
function with a version check to avoid conflict. With that, macros for
accessing option values are also added.
Upstream Differential Revision: https://reviews.llvm.org/D99471
Reviewed By: ngorogiannis
Differential Revision: D27564868
fbshipit-source-id: 1dfdd0530
Summary:
This diff pulls in upstream changes to the LLVM OCaml
bindings. Includes upstream commits:
> Add (get/set)_module_identifer functions
> Fix documentation for verify_function and const_of_int64
> DebugInfo support for OCaml bindings
> llvmbuildectomy - compatibility with ocaml bindings
> Remove ConstantPropagation
> Remove and move tests to SCCP.
Also includes updates to llvm-dune to adapt the build to the added
header file.
Reviewed By: ngorogiannis
Differential Revision: D27564717
fbshipit-source-id: af63e2aba
Summary:
There are not too many cases where the function name is not enough to
disambiguate a trace message, but it is still perhaps more
approachable to include the module names as well.
Reviewed By: jvillard
Differential Revision: D27396914
fbshipit-source-id: ea4c8b44f
Josh Berdine
Roman Manevich