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: A little bit of sed to adjust links (see previous commit for effect).
Reviewed By: skcho
Differential Revision: D27360106
fbshipit-source-id: 2fa32f05f
Summary:
Fixing `IsInstanceOf` term simplification for null case. Before, this
was only being done if value was known to be null at the moment of the
call to `instanceof`. Otherwise, the `IsInstanceOf` term would remain in
the formula unnecessarily.
Reviewed By: jvillard
Differential Revision: D27361025
fbshipit-source-id: 2d958a757
Summary:
Models for Java Map interface.
This consists of `Map.init()`, `Map.put(key, value)`, `Map.get(key)`,
`Map.containsKey(key)` and
`Map.isEmpty()`. With the exception of `Map.get(key)` and `Map.containsKey(key)`, these functions were modelled using the respective similar ones provided by the Java Collection interface.
Reviewed By: jvillard
Differential Revision: D27326716
fbshipit-source-id: e07f0c952
Summary:
This diff add semantics for collecting all object fields that may have config values. The collected information is used to instantiate conditional unchecked callees introduced in the previous diff.
How it works:
* The summary is extended to have `config_fields:Fields.t`. It has all fields that may have config values intra-procedurally.
* Before reporting to `config-impact-report.json`, it unions all `config_fields` from all specs.
* Using `all_config_fields`, it instantiates each summaries and writes results to `config-impact-report.json`.
Reviewed By: ezgicicek
Differential Revision: D27326306
fbshipit-source-id: 42f16ca45
Summary:
This diff extends domain and semantics to understand object fields that may have config values.
Now, `Summary.t` has one more field `unchecked_callees_conditional`, which is a map from a set of object fields to a set of callees. The meaning is that the callees are called depending of the fields, ie
* if one of field of the fields is known to be an actual config value, the callees are safely gated,
* otherwise, the callees are ungated.
For example,
```
void foo() {
if (mField1) {
if (mField2) {
callee1();
}
callee2();
}
}
```
`foo` will have `unchecked_callees_conditional` value of
```
{ {mField1,mField2} -> {callee1},
{mField1} -> {callee2} }
```
Later, if we know that `mField2` has a config value, we can say `callee1` is gated, or if we know that `mField1` has a config value, we can say `callee1` and `callee2` are gated.
The following diff will add an analysis that collects object fields that may have config values.
Reviewed By: ezgicicek
Differential Revision: D27325522
fbshipit-source-id: d4aff58cb
Summary:
A draft version mentioning 1.1.0 was pushed to master by mistake.
It's ready now!
Reviewed By: martintrojer
Differential Revision: D27293733
fbshipit-source-id: b3c97736f
Summary:
The internal links for the "old latest" 1.0.0 version were wrong. The
fix to `make new-website-version` is in the next diff.
Reviewed By: martintrojer
Differential Revision: D27360089
fbshipit-source-id: 8abefbd8f
Summary:
Copied the documentation from a document created by rgrig
(thanks!!).
Reviewed By: rgrig
Differential Revision: D27325829
fbshipit-source-id: 118e1a2be
Summary:
The explicit marker for nondeterministic states was used to speed up the
shallow implementations of Topl, which ar enow removed.
Reviewed By: jvillard
Differential Revision: D27297019
fbshipit-source-id: 0fce93817
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
Summary:
This warning (68) triggers when a function argument pattern depends on
mutable state, which prevents the remaining arguments from being
uncurried, causing additional closure allocations.
Reviewed By: jvillard
Differential Revision: D27188311
fbshipit-source-id: a43354e15
Summary:
Not all types of exceptions allowed by LLVM are currently
supported. The types of Resume args and LandingPad params must be
compatible, and so it only makes sense to check they the same
way.
Reviewed By: jvillard
Differential Revision: D27188307
fbshipit-source-id: c88cc46d0
Summary:
It is possible for the filename of a source location to be the empty
string. Fpath.v asserts when passed an empty string.
Reviewed By: jvillard
Differential Revision: D27188304
fbshipit-source-id: a7d73444b
Summary:
refactoring Java Integer model so that it uses the new
API designed for manipulating fields in Java.
Reviewed By: jvillard
Differential Revision: D27231810
fbshipit-source-id: 0d9e3c951
Josh Berdine
Jules Villard
Gabriela Cunha Sampaio
Sungkeun Cho
Radu Grigore
Loc Le