Summary: Delete function that would get a linter warning or not depending on the version of Xcode.
Reviewed By: martintrojer
Differential Revision: D13215750
fbshipit-source-id: 886ce397d
Summary: It is not used yet and still manages to cause false positives.
Reviewed By: mbouaziz
Differential Revision: D13102948
fbshipit-source-id: 2122666c2
Summary:
It's useful for checkers to know when variables go out of scope to
perform garbage collection in their domains, especially for complex
domains with non-trivial joins. This makes the analyses more precise at
little cost.
This could have been added as a custom function call to a builtin, but I
decided against it because this instruction doesn't have the semantics
of any function call. It's better for each checker to explicitly not
deal with the custom instruction instead.
Reviewed By: jberdine
Differential Revision: D13102951
fbshipit-source-id: 33be22fab
Summary:
Before, the liveness pre-analysis would place extra instructions in the
CFG for either:
1. marking an `Ident.t` as dead, or
2. marking a `Pvar.t` as `= 0`
But we have no way of marking pvars dead without setting them to 0. This
is bad because setting pvars to 0 is not possible everywhere they are
dead. Indeed, we only do it when we haven't seen their address being
taken anyway. This prevents the following situation, recorded in our tests:
```
int address_taken() {
int** x;
int* y;
int i = 7;
y = &i;
x = &y;
// if we don't reason about taken addresses while adding nullify instructions,
// we'll add
// `nullify(y)` here and report a false NPE on the next line
return **x;
}
```
So we want to mark pvars as dead without nullifying them. This diff
extends the `Remove_temps` SIL instruction to accept pvars as well, and
so renames it to `ExitScope`.
Reviewed By: da319
Differential Revision: D13102953
fbshipit-source-id: aa7f03a52
Summary:
Switches from opam 1 to opam 2.
Opam2 has some cool new features that simplify some of the scripting.
Notable changes:
1. Use the new `opam lock` *plugin* from https://github.com/AltGr/opam-lock/ instead of https://github.com/rgrinberg/opam-lock. This has a simpler interface for our purposes.
2. Change the way `./build-infer.sh` can be called to use an already existing switch: simply pass `--user-opam-switch` to the script and it won't attempt to create/set the current switch. This can be used to build infer in a local switch for instance.
3. Take advantage of automatic pinning where possible, eg to install infer deps without using opam.locked.
Reviewed By: ngorogiannis
Differential Revision: D13167863
fbshipit-source-id: 1a667c270
Summary:
It removes the `represents_multiple_values` parameters when we can know them from `path` values.
Depends on D12939124
Reviewed By: skcho
Differential Revision: D12939130
fbshipit-source-id: 30ff768b2
Summary:
It modifies sizes and offsets of array values on pointer castings.
Currently, it supports only simple castings of pointer-to-integers.
Reviewed By: mbouaziz
Differential Revision: D12920589
fbshipit-source-id: a5ba831b8
Summary: In this diff, it passes the parameter of integer type widths to evaluation functions. The parameter which will be used for casting in the following diff.
Reviewed By: mbouaziz
Differential Revision: D12920581
fbshipit-source-id: 48bbc802b
Summary:
It enables the translation of casting expression. As of now, it
translates only the castings of pointers to integer types, in order to
avoid too much of change, which may mess the checkers up.
Reviewed By: jvillard
Differential Revision: D12920568
fbshipit-source-id: a5489df24
Summary:
Useful to understand the changes in the pre-analysis, or to inspect the
CFG that checkers actually get.
This means that the pre-analysis always runs when we output the dotty,
but I don't really see a reason why not. In fact, we could probably
*always* store the CFGs as pre-analysed.
Reviewed By: mbouaziz
Differential Revision: D13102952
fbshipit-source-id: 89f3102ec
Summary: It fixes the conditions of the `check` function to address `is_collection_add` cases correctly.
Reviewed By: mbouaziz
Differential Revision: D13081281
fbshipit-source-id: 39ae5ef03
Summary: Experimental feature: Use memcached for summaries as a look-aside cache during analysis.
Reviewed By: jvillard
Differential Revision: D12939311
fbshipit-source-id: 9f78994e2
Summary:
Currently, if there are several reports on the same line, the most important one is reported together with a message containing how many reports were suppressed.
This is sometimes causing the bug hash we use believe that a report is introduced (eg if the number of suppressed reports changes).
Reviewed By: mbouaziz
Differential Revision: D13067306
fbshipit-source-id: 1cc0c6d3a
Summary:
Messages emitted by cost-analysis now look like the following:
Complexity of this function has **increased** from `O(1)` to `O(n)`.
Reviewed By: mbouaziz
Differential Revision: D13058008
fbshipit-source-id: 119037703
Summary:
Update clang plugin which now gives names to variables captured by lambdas that were empty before.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D12979015
fbshipit-source-id: 0b092fb24
Summary:
It turns out keeping attributes (such as invalidation facts) separate
from the memory is a bad idea and leads to loss of precision and false
positives, as seen in the new test (which previously generated a
report).
Allow me to illustrate on this example, which is a stylised version of
the issue in the added test: previously we'd have:
```
state1 = { x = 1; invalids={} }
state2 = { x = 2; invalids ={1} }
join(state1, state2) = { x = {1, 2}; invalids={{1, 2}} }
```
So even though none of the states said that `x` pointed to an invalid
location, the join state says it does because `1` and `2` have been
glommed together. The fact `x=1` from `state1` and the fact "1 is
invalid" from `state2` conspire together and `x` is now invalid even
though it shouldn't.
Instead, if we record attributes as part of the memory we get that `x`
is still valid after the join:
```
state1 = { x = (1, {}) }
state2 = { x = (2, {}) }
join(state1, state2) = { x = ({1, 2}, {}) }
```
Reviewed By: mbouaziz
Differential Revision: D12958130
fbshipit-source-id: 53dc81cc7
Summary:
I hear that this scheduler is better. I want the best scheduler
possible. Also pulse's join is a bit complex so it might matter one day.
whydididothis
Reviewed By: mbouaziz
Differential Revision: D12958131
fbshipit-source-id: 3bd77ccba
Summary: There is a bug on the instantiation of function parameters.
Reviewed By: mbouaziz
Differential Revision: D12973691
fbshipit-source-id: ca7fbc4e6
Summary: The aligned width of bool should be 1-byte, while the range of bool [0,1].
Reviewed By: jvillard
Differential Revision: D12932394
fbshipit-source-id: be1a5d6d1
Summary: For a general case of `operator=` we want to create a fresh location for the first parameter as `operator=` behaves as copy assignment.
Reviewed By: jvillard
Differential Revision: D12940635
fbshipit-source-id: 89c6e530d
Summary:
Whenever `vec.reserve(n)` is called, remember that the vector is
"reserved". When doing `vec.push_back(x)` on a reserved vector, assume
enough size has been reserved in advance and do not invalidate the
underlying array.
This gets rid of false positives.
Reviewed By: mbouaziz
Differential Revision: D12939837
fbshipit-source-id: ce6354fc5
Summary:
Instead of keeping at most one invalidation fact for each address, keep
a set of them and call them "attributes". Keeping a set of invalidation
facts is redundant since we always only want the smallest one, but
makes the implementation simpler, especially once we add more kinds of
attributes (used for modelling, see next diffs).
Reviewed By: mbouaziz
Differential Revision: D12939839
fbshipit-source-id: 4a54c2132
Summary:
Copied on the ownership checker logic: return the initial value of the
domain as return. This can probably be improved.
Reviewed By: mbouaziz
Differential Revision: D12888102
fbshipit-source-id: 9e2dac7fc
Summary:
When initialising a variable via semi-exotic means, the frontend loses
the information that the variable was initialised. For instance, it
translates:
```
struct Foo { int i; };
...
Foo s = {42};
```
as:
```
s.i := 42
```
This can be confusing for backends that need to know that `s` actually
got initialised, eg pulse.
The solution implemented here is to insert of dummy call to
`__variable_initiazition`:
```
__variable_initialization(&s);
s.i := 42;
```
Then checkers can recognise that this builtin function does what its
name says.
Reviewed By: mbouaziz
Differential Revision: D12887122
fbshipit-source-id: 6e7214438
Summary:
Now that arrays are dealt with separately (see previous diff), we can
turn the join back into an over-approximation as far as invalid
locations are concerned.
Reviewed By: skcho
Differential Revision: D12881989
fbshipit-source-id: fd85e49c0
Summary:
Arrays are the main source of false positives that prevent us from
having a better (less under-approximate) join in general. The next diff
improves join and I split this off to make it easier to review.
Reviewed By: mbouaziz
Differential Revision: D12881986
fbshipit-source-id: 5f52dea27
Summary:
This prevents the join from wrongly assuming that we haven't seen a
variable on one side of the join.
Reviewed By: skcho
Differential Revision: D12881987
fbshipit-source-id: 42a776adb
Summary:
Smaller numbers are easier to read and abstract addresses should never
be shared across functions anyway.
Reviewed By: da319
Differential Revision: D12881988
fbshipit-source-id: f9bcfa343
Summary:
As explained in the added comment, clang started adding `-faddrsig` at the end
of every `-cc1` command, which trumps our heuristic for finding the file name
(thus we would write debug scripts to `-faddrsig.ast.sh`, do filename-based
filtering on `-faddrsig` instead of the source path, and more...). We rely on
the file name being the last argument in `-cc1` commands because so far that's
always been the case, and we don't want to parse the clang command line and
have to know about all the clang options...
Thanks martinoluca for the trick of simply passing `-fno-addrsig`!
Reviewed By: martinoluca
Differential Revision: D12921987
fbshipit-source-id: 28bebe647
Summary:
The upcoming ocamlformat has the ability to parse and format
docstrings. This requires that the docstrings conform to the ocamldoc
spec a bit more strongly. If a docstring does not parse, it is left
alone, but if it is morally ill-formed but parses by chance, it can be
reformatted incorrectly. This patch fixes the existing instances of
this problem.
Reviewed By: mbouaziz
Differential Revision: D12911937
fbshipit-source-id: 1c2eb590b
Summary:
For more deduplications of issues, this diff loosens the condition of
similar bounds. The previous condition of similar bounds was too
strict, so [0,0] and [0,+oo] were not similar.
Depends on D10851762
Reviewed By: mbouaziz
Differential Revision: D10866127
fbshipit-source-id: 4ba912a88
Summary: For `operator=(lhs, rhs)` we want to model it as an assignment if rhs is materialized temporary created in the constructor.
Reviewed By: jvillard
Differential Revision: D10462510
fbshipit-source-id: 998341e69
Summary: Do not create a new location for placement new argument if it already exists.
Reviewed By: jvillard
Differential Revision: D12839942
fbshipit-source-id: 758b67a82
Summary:
In order to know whether a global variable is an integral constant
expression in C, this diff adds a field for the results of isInitICE.
The controller you requested could not be found.: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D12838521
fbshipit-source-id: 388bff1f3
Summary:
This may help running the id map bookkeeping on its own in the future
and makes the code slightly more readable in my opinion.
Reviewed By: mbouaziz
Differential Revision: D12858066
fbshipit-source-id: fea4aea63
Summary:
HIL wanted to do its own HTML printing, causing code duplication and hacks to
avoid double opening/closing files. Instead, pass a hook to print SIL
instructions or not.
This also makes the debug HTML be printed even in case of raised exceptions,
which is invaluable to debug crashes or even just reports in the case of
checkers that can raise `Stop_analysis` (pulse only for now).
This also print intermediate abstract states between instructions instead of
only at the start and end of nodes, for moar debugging.
Reviewed By: mbouaziz
Differential Revision: D12857425
fbshipit-source-id: 4ee6c88d6
Ezgi Çiçek
Jules Villard
Nikos Gorogiannis
Sungkeun Cho
Mehdi Bouaziz
Ted Reed
Daiva Naudziuniene
Dino Distefano
Martino Luca
Martin Trojer
Josh Berdine