Summary:
After merging https://github.com/facebook/facebook-clang-plugins/pull/20, we can now use Actions here to download a facebook-clang custom clang Release here and use it to build C Analyzers during CI, as well as Java Analyzers.
1. had to change `matrix.os: macos-latest` to `matrix.os: macOS-latest`. I guess that's what I typed for the fb clang build, and `curl`ing a Release asset is case-sensitive.
2. Add `jq` to installed packages on mac - we need it for parsing GitHub's API responses
3. Add the logic for fetching a release asset (we currently only look for the `"latest"` release) and downloading the properly-named clang based on OS. Then unpack it and update the `opam` files so we build with clang.
Note: I would have used this Action: https://github.com/dsaltares/fetch-gh-release-asset/ for fetching a Release asset, but unfortunately it seems to be in a fairly new state and it's a Docker Action, which means it doesn't support macOS. The logic in the fetch clang step is roughly based off of this action's logic.
Pull Request resolved: https://github.com/facebook/infer/pull/1286
Reviewed By: da319
Differential Revision: D22475973
Pulled By: jvillard
fbshipit-source-id: cb95b51b9
Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.
Reviewed By: jvillard
Differential Revision: D22455725
fbshipit-source-id: 6f0059873
Summary:
In preparation for more smoothly interoperating with ICS's functional
array theory.
Reviewed By: jvillard
Differential Revision: D22401039
fbshipit-source-id: 4de39c38a
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:
The first-order context is induced by the pure part, so no need to
compare it.
Reviewed By: jvillard
Differential Revision: D22381645
fbshipit-source-id: 29fff13a3
Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.
The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.
Reviewed By: jvillard
Differential Revision: D22170506
fbshipit-source-id: a014ee7d7
Summary:
The eventual aim is for the conversion of Llair to Fol to be external
to Fol. Fol should not need to depend on Llair, nor vice versa. This
is not yet possible, but a step forward is to move the conversion
functions into separate modules outside the core Fol modules.
Reviewed By: ngorogiannis
Differential Revision: D22170522
fbshipit-source-id: 4860b4c07
Summary:
The `Subst` module is not used by `Ses`, so move it out of the
Ses-internal APIs.
Reviewed By: ngorogiannis
Differential Revision: D22170513
fbshipit-source-id: a189a1440
Summary:
Change Term and Equality rename functions to accept a partial
application of Var.Subst.apply to the renaming substitution.
Reviewed By: ngorogiannis
Differential Revision: D22170520
fbshipit-source-id: 003d8b27e
Summary:
The convention is for modules that are intended to be `open`ed, that
define syntax and infix operations, are named `Import`. This diff
combines the `Option.Monad_infix` and `Option.Monad_syntax` modules
into `Option.Import` to follow this convention.
Reviewed By: ngorogiannis
Differential Revision: D22170507
fbshipit-source-id: 44378fd56
Summary:
Exponents in polynomials are represented by rationals for code reuse
purposes, but only integral exponents are supported. Strengthen the
invariant check to clarify this.
Reviewed By: ngorogiannis
Differential Revision: D22170517
fbshipit-source-id: 81ae38f4e
Summary: To avoid NULLPTR_DEREFERENCE false positives we want to model some functions as returning non-null. A new flag --pulse-model-return-nonnull allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D22431564
fbshipit-source-id: 9944c7382
Summary: Make the module interface safe wrt closing the classpath channel when done, plus reducing the exposed API.
Reviewed By: skcho
Differential Revision: D22411685
fbshipit-source-id: 11316c577
Summary: `addAll` adds elements one by one and hence takes linear time. We didn't have a model for this and considered it O(1).
Reviewed By: skcho
Differential Revision: D22375157
fbshipit-source-id: 65b82bfae
Summary: This diff prevents printing line numbers of loop in the trace description, which helps to keep the same descriptions even when the line number of a function is changed in tests.
Reviewed By: ezgicicek
Differential Revision: D22375584
fbshipit-source-id: 676d1a7cc
Summary:
This one is observed to be more memory efficient. Intuitively, maps need
to be re-allocated more often than lists for balancing. In pulse, we'll
often only ever add new values, in increasing order (when they are fresh
variables created as we symbolically execute the program), which pushes
maps into their worst-case allocation pattern. At least I suspect that's
what happens. With lists, this case is handled much better as lists are
not re-allocated when adding elements.
This is somewhat confirmed by benchmarking and observing GC stats.
Reviewed By: skcho
Differential Revision: D22140908
fbshipit-source-id: 29815112f
Summary:
Messed up the aggregation of GC stats in the previous commit.
It's cleaner to have GC stats (and analysis time) outside of
BackendStats as the rules for computing them is different than the rest,
eg notice how "analysis time" needed to be corrected at the end of the
run, and similarly for GC stats. Thus, refactor this part.
Also output different aggregations of GC stats: +/max/average.
Reviewed By: skcho
Differential Revision: D22332496
fbshipit-source-id: eefd9dd72
Summary:
## Issue
There are a number of times when users building `facebook-clang-plugins` hit memory limitations, typically due to the OOM killer and when linking.
In https://github.com/facebook/facebook-clang-plugins/pull/21, I implemented support for building `facebook-clang-plugins` using both Ninja and to only use one process when linking.
## Resolution
This PR exposes the optional flags added in https://github.com/facebook/facebook-clang-plugins/pull/21 to `build-infer.sh`, such that you can build `facebook-clang-plugins` with either just `ninja` or `ninja` + only one process for linking.
As part of this, it updates the `facebook-clang-plugins` submodule.
update-submodule: facebook-clang-plugins
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
Pull Request resolved: https://github.com/facebook/infer/pull/1283
Reviewed By: dulmarod
Differential Revision: D22334307
Pulled By: jvillard
fbshipit-source-id: 97fc1c7db
Summary:
Keyword `thread_local` in cpp allows us to create a variable with thread storage duration, meaning that the object's lifetime begins when the thread begins and ends when the thread ends.
We get `NULLPTR_DEREFERENCE` false positive for `thread_local` variable since we reallocate it in the `VariableLifetimeBegins` metadata instruction and we do not see further updates to the variable. To solve the issue we special case `VariableLifetimeBegins` instruction for global variables.
Reviewed By: jvillard
Differential Revision: D22284135
fbshipit-source-id: 13c14ef90
Qianyi Shu
Amar Paul
Sora Morimoto
Josh Berdine
Ezgi Çiçek
Daiva Naudziuniene
Nikos Gorogiannis
Sungkeun Cho
David Pichardie
Jules Villard
Andrew V. Jones