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
Summary:
OCaml 4.12 added
```
val __FUNCTION__ : string
__FUNCTION__ returns the name of the current function or method,
including any enclosing modules or classes.
```
This diff simplifies ppx_trace using `__FUNCTION__` to obtain the name
of the function containing each call to a `Trace` function. Before
this diff this is done by maintaining a stack of function names
obtained by parsing value binding patterns during preprocessing. This
technique is not entirely robust and does not deal with some cases (if
calls to `Trace` functions appear in some places, preprocessing fails
with an exception).
Reviewed By: jvillard
Differential Revision: D27396915
fbshipit-source-id: da7aa2945
Summary:
This diff renames and moves the opam package definition files to
`<package>.opam` in an `opam` directory at the root of the
repository. This enables opam pinning the different packages contained
in the repo. It is necessary for these files to be either at the root
of the repo or in a directory named `opam` at the root of the repo, or
else opam cannot find them.
Reviewed By: skcho
Differential Revision: D27326495
fbshipit-source-id: 4c95c6955
Summary:
The implementation of `llvm_struct_name` before this diff calls
`caml_copy_string`, which allocates, while the `result` local variable
points to a block allocated by `caml_alloc_small` that has not yet
been initialized. If the allocation in `caml_copy_string` triggers a
garbage collection, then the GC root `result` contains a pointer to
uninitialized data, which may crash the GC or lead to a memory
corruption.
This diff fixes this by allocating and initializing the string first
and then allocating and initializing the option, thereby leaving no
dangling pointers when allocations are made.
The conversion from a C string to an OCaml string option is refactored
into a function, `cstr_to_string_option`. This function is also used
to simplify the definitions of `llvm_get_mdstring` and
`llvm_string_of_const`.
Upstream Differential Revision: https://reviews.llvm.org/D99393
Reviewed By: ngorogiannis
Differential Revision: D27360848
fbshipit-source-id: f2daa7561
Summary:
There are a number of compilation warnings regarding disregarding
const qualifiers, and casting between pointers to integer types with
different sign.
The incompatible sign warnings are due to treating the result of
`LLVMGetModuleIdentifier` as `const unsigned char *`, but it is
declared as `const char *`.
The dropped const qualifiers are due to the code pattern
`memcpy(String_val(_),_,_)` which ought to be (following the
implementation of the OCaml runtime)
`memcpy((char *)String_val(_),_,_)`. The issue is that `String_val` is
usually used to get the value of an immutable string. But in the
context of the `memcpy` calls, the string is in the process of being
initialized, so is not yet constant.
Upstream Differential Revision: https://reviews.llvm.org/D99392
Reviewed By: ngorogiannis
Differential Revision: D27360846
fbshipit-source-id: d045ad7c0
Summary:
This diff uses ptr_to_option to convert a nullable C pointer to an
OCaml option instead of the redundant implementation in
llvm_global_initializer.
Upstream Differential Revision: https://reviews.llvm.org/D99391
Reviewed By: ngorogiannis
Differential Revision: D27360847
fbshipit-source-id: b5bfcadf7
Summary:
The names of the compiled sledge executables are long, which is
inconvenient. Also, all build modes produce an executable named
`sledge`, so it is not possible to add them to PATH and still be able
to run the desired executable. This diff adds a directory of symbolic
links with different names that refer to the executables built in the
different build modes. The intent is for people to add .../sledge/bin
to their PATH.
Reviewed By: jvillard
Differential Revision: D27315805
fbshipit-source-id: 7e84e43a7
Summary:
These no-cmx-file warnings on libraries in dependencies do not seem to
be resolvable, and there is no smaller scope I can find to suppress
them.
Reviewed By: jvillard
Differential Revision: D27280739
fbshipit-source-id: 6e8886f7f
Summary:
This is a form of call only used with inline asm, so currently not
supported.
Reviewed By: jvillard
Differential Revision: D27280742
fbshipit-source-id: f286e7886
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 patch exposes the predicate API of internalize pass to OCaml.
Reviewed By: jvillard
Differential Revision: D27188305
fbshipit-source-id: d53bf5871
Summary:
LLVMGetInitializer returns nullptr in case there is no
initializer. There is not much that can be done with nullptr in OCaml,
not even test if it is null. Also, there does not seem to be a C or
OCaml API to test if there is an initializer. So this diff changes
Llvm.global_initializer to return an option.
Reviewed By: jvillard
Differential Revision: D27188302
fbshipit-source-id: 3474ec840
Summary:
There are several enum values that have been added to LLVM-C that are
missing from the OCaml bindings.
Reviewed By: jvillard
Differential Revision: D27188299
fbshipit-source-id: 215f15469
Summary:
Add thin shims to OCaml interfaces to provide access to DebugLoc info
for Instructions, GlobalVariables and Functions.
Reviewed By: jvillard
Differential Revision: D27188296
fbshipit-source-id: 52129f957
Summary:
Add a vendored copy of llvm-dune, a dune-based build system for the
LLVM OCaml bindings.
Source: https://github.com/kit-ty-kate/llvm-dune
Reviewed By: jvillard
Differential Revision: D27188306
fbshipit-source-id: 89e9265e0
Summary:
Add a vendored copy of the LLVM cxxabi project.
The sledge models compile llvm's libcxxabi to bitcode, so that the
analyzer knows the real definitions of the e.g. exception handling
primitives. Before this diff, the sledge build relied on having a
clone of a fork of llvm in the sledge working tree. This diff is part
of enabling using the upstream llvm 11 library instead of the fork.
Source: https://github.com/llvm/llvm-project/tree/main/libcxxabi
Reviewed By: jvillard
Differential Revision: D27188298
fbshipit-source-id: dc76b0714
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:
They only attach debug info to labels, and have no execution
behavior. At some later point it would be good to scan for these and
gather the attached debug info.
Reviewed By: jvillard
Differential Revision: D27262516
fbshipit-source-id: 2eb91a475
Summary:
Llair.Func.mk makes two passes over the CFG to resolve block parents,
jump destinations, and eliminate jumps to jumps. This is not
economical, but more importantly the current code mistakenly uses the
`retreating` metadata before it is set correctly. This diff combines
these passes into a single one, which also incorporates setting the
retreating field from Llair.Program.mk.
This avoids nontermination on code that contains immediate self-jumps
such as `L: goto L;` that LLVM 11 can now generate.
Reviewed By: jvillard
Differential Revision: D27262512
fbshipit-source-id: 0543ba669
Roman Manevich
Josh Berdine