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
Summary:
Almost all of the information on this page is wrong :)
I moved some documentation on debug mode to the previous commit.
Debug information is present in CONTRIBUTING.md which is a better source
of truth. Anecdotally it's been kept more up to date than this web page
so far!
Reviewed By: skcho
Differential Revision: D27268171
fbshipit-source-id: 25314a823
Summary:
## Issue:
On `master`, it seems that there is a missing newline when Infer prints the `tenv` for a structure type:
```bash
avj@platypus /tmp/infer_bug$ cat test.c
typedef struct {
int a;
} st1;
typedef struct {
int b;
} st2;
avj@platypus /tmp/infer_bug$ infer --version
Infer version v1.0.0-55871dd28
Copyright 2009 - present Facebook. All Rights Reserved.
avj@platypus /tmp/infer_bug$ rm -rf infer-out && infer --debug run -P -- gcc -c test.c
Logs in /tmp/infer_bug/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /tmp/infer_bug/infer-out
No issues found
avj@platypus /tmp/infer_bug$ grep -A1 "dummy" infer-out/captured/*/*.tenv.debug
dummy: falsestruct st1
fields: {
--
dummy: falsestruct st2
fields: {
--
dummy: falsestruct objc_class
fields: {}
```
(notice that `dummy: false` and `struct objc_class` are on the same line, with no spacing)
## Resolution
Their PR adds an explicit newline at the end of pretty-printing a structured value, such that it is formatted correctly in the `tenv`:
```bash
avj@platypus /tmp/infer_bug$ infer --version
Infer version v1.1.0-bb5a33506
Copyright 2009 - present Facebook. All Rights Reserved.
avj@platypus /tmp/infer_bug$ rm -rf infer-out && infer --debug run -P -- gcc -c test.c
Logs in /tmp/infer_bug/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /tmp/infer_bug/infer-out
No issues found
avj@platypus /tmp/infer_bug$ grep -A1 "dummy" infer-out/captured/*/*.tenv.debug
dummy: false
struct st1
--
dummy: false
struct st2
--
dummy: false
struct objc_class
--
dummy: false
```
(*edit*: I forgot to build after committing; now with updated hash)
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
Pull Request resolved: https://github.com/facebook/infer/pull/1416
Reviewed By: skcho
Differential Revision: D27264518
Pulled By: jvillard
fbshipit-source-id: 3b86b4c22
Summary:
Before this diff, TOPL had 3 implementations:
1. a post-processing of biabduction summaries
2. a post-processing of pulse summaries
3. a deep embedding in pulse
1 and 2 additionally require instrumenting SIL to generate monitors for
the TOPL properties. 3 is faster than both 1 and 2, by a good lot, and
doesn't require instrumenting the SIL code. Thus, delete 1 and 2!
Also harmonise the CLI so that TOPL is activated by --topl, which
actives it as a checker, like other analyses.
Reviewed By: rgrig
Differential Revision: D27270178
fbshipit-source-id: e86cf972b
Summary:
Changing model for Java `Collection` interface. Every collection has now two internal fields, initially set to `null`. We also keep an extra field to compute emptiness. This model was implemented based on the [preexisting model for HashMap](https://github.com/facebook/infer/blob/master/infer/models/java/src/java/util/HashMap.java).
Existing models (`add`, `remove`, `set` and `is_empty`) have been updated accordingly and new models are provided: `init` and `clear`.
This model is not yet compatible with the `Map` interface but this change will happen very soon.
Reviewed By: ezgicicek
Differential Revision: D27126815
fbshipit-source-id: 79a5fe306
Gabriela Cunha Sampaio
Sungkeun Cho
Jules Villard
Radu Grigore
Josh Berdine
Loc Le
Andrew V. Jones