Summary: Unknown locations in the alias domain resulted in unexpected unreachable code.
Reviewed By: mbouaziz
Differential Revision: D14339412
fbshipit-source-id: a5dca6489
Summary:
The disjunctive domain shouldn't really be a set in the first place as
comparing abstract states for equality is expensive to do naively
(walking the whole maps representing the abstract heap). Moreover in
practice these sets have a small max size (currently 50 for pulse, the
only client), so switching them to plain lists makes sense.
Reviewed By: mbouaziz
Differential Revision: D14258489
fbshipit-source-id: c512169eb
Summary:
It's useful to keep the size of states down, especially when humans are
trying to read it. It will also help keep the size of summaries down in
the inter-procedural pulse.
Reviewed By: mbouaziz
Differential Revision: D14258486
fbshipit-source-id: 45ebcac67
Summary: After a redeclaration of a global constant, it is not parsed as ICE(integral constant expression), which results in FN.
Reviewed By: ezgicicek
Differential Revision: D14299288
fbshipit-source-id: 394afd595
Summary:
It assigns symbolic values for global variables in the load commands. However, it does not instantiate the symbols for the global variables yet, which will be addressed in another diff.
Depends on D14208643
Reviewed By: ezgicicek
Differential Revision: D14257619
fbshipit-source-id: f9113c8a3
Summary:
the predicate to check that a decl is const was not working for VarDecl.
This diff fixes this
Reviewed By: jvillard
Differential Revision: D14106798
fbshipit-source-id: 1f6c24113
Summary:
This diff differentiates proof obligations by allocsites. Sizes and
offsets of arrays were joined when making proof obligations.
Reviewed By: mbouaziz
Differential Revision: D14163149
fbshipit-source-id: cb6608c16
Summary:
The Eradicate backend is reporting nullable type errors, that are not always necessarily leading to null pointer exceptions.
For example, the analysis is designed to be consistent with the Java type system and report on the following code:
String foo(boolean test) {
Object object = test ? new Object() : null;
if (test) {
return object.toString(); // the analysis reports here
}
}
even though the code will not crash.
In order to make this aspect clear, this diff renames the warnings `Null Method Call` and `Null Field Access` into `Nullable Dereference`
Reviewed By: ngorogiannis
Differential Revision: D14001979
fbshipit-source-id: ff1285283
Summary:
This diff adds a constant to the set of widening thresholds if the
constant is compared to an abstract value in condition expressions.
Each abstract value has its own set of thresholds.
Reviewed By: mbouaziz
Differential Revision: D14147150
fbshipit-source-id: ca0db34d4
Summary:
In this diff, it avoids a precision-losing pruning, which was needed
to keep effects of assume commands.
```
unsigned int c = a + b; // (1)
if (c > 0) { // (2)
char result[c];
result[c - 1] = 0; // (4)
}
```
For example, in the example, `c` is assigned by `[a+b,a+b]` at (1),
then it tried to prune the lower bound of `c` to 1 at (2) while losing
precision, in order to say `c - 1` at (4) is safe in terms of integer
underflow. Instead, it could not say that `c - 1` is smaller than `c`
in the buffer access, because the former is analyzed to `[0,a+b-1]` and
the latter `[1,a+b]` at (4).
Now, the situation has changed. By adopting conditional proof
obligation (D13749914), the FP of integer overflow can be suppressed
without the precision-losing pruning.
Reviewed By: mbouaziz
Differential Revision: D14122770
fbshipit-source-id: 634744e99
Summary: Since Inferbo's current min/max domain can keep only a single symbol, e.g. min(constant, symbol) , it loses precision when trying to prune a value including multiple symbols.
Reviewed By: ezgicicek
Differential Revision: D14099399
fbshipit-source-id: 71d677b75
Summary: Record where each symbol in a polynomial is coming from: either a loop, function call or a modeled call.
Reviewed By: mbouaziz
Differential Revision: D14047420
fbshipit-source-id: 56d0bd926
Summary: It keeps alias of simple plus/minus arithmetic in order to pruning the value of "++i" expression.
Reviewed By: mbouaziz
Differential Revision: D14080230
fbshipit-source-id: d3af32a32
Summary: In SIL, Java's array member is a pointer to an array, while C++'s is the array itself. This diff differentiate them in evaluating abstract locations.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D14021451
fbshipit-source-id: 00f14fe3b
Summary:
- There is no need to use AI to compute a dot product: let's just fold over all nodes, but still do it in order (using the WTO) to report at the right place
- The previous version was computing a dot product on nodes for each node, which was quadratic, the new version is linear
- Report only once, the first time the threshold is reached (if in a loop, report at the loop head)
Reviewed By: ddino
Differential Revision: D14028171
fbshipit-source-id: b4a840c6e
Summary:
Add an option to specify some classes that we really want to warn about
with the liveness checker, even when they appear used because of the
implicit destructor call inserted by the compiler.
Reviewed By: mbouaziz
Differential Revision: D13991129
fbshipit-source-id: 7fafdba84
Summary:
Get rid of false positive as in the test by modelling `Double`. Longer term we
should probably prevent biabduction from blocking the angelic analysis on
`Nullable` fields but that seems harder.
Reviewed By: jeremydubreil
Differential Revision: D14005228
fbshipit-source-id: 59ef2ed66
Summary:
The purpose these serve is unclear to me. From the comment I *think*
they were used to hint to the biabduction backend that smart pointers
are just pointers. That said, The tests still mostly pass even without
that (just a few `weak_ptr` tests changed from `NULL_DEREFERENCE` to
`Bad_footprint`).
Moreover, this extra dereference was added unreliably. For instance,
this piece of code:
```
auto x = std::make_unique<X>(some_X);
```
would either get the extra dereference or not depending on which headers
were picked for the C++ stdlib.
The extra dereference was tripping up the liveness checker (see later in
the stack), and probably most checkers too.
Reviewed By: mbouaziz
Differential Revision: D13991130
fbshipit-source-id: 462923595
Summary: When a `VarDecl` has the attribute `unused` then do not assign its initialisation result to the corresponding variable.
Reviewed By: ngorogiannis
Differential Revision: D13974497
fbshipit-source-id: 28029f995
Summary: The Makefile was missing that target and making `make test-replace` at the root of the repo fail.
Reviewed By: ngorogiannis
Differential Revision: D13990483
fbshipit-source-id: 805b5d2a9
Summary:
If the result of `fgets` is not-null, the length of `s` should be
bigger than or equal to 1.
Reviewed By: mbouaziz
Differential Revision: D13939994
fbshipit-source-id: 298fe33f4
Summary:
This diff updates the reachability conditions of proof obligations at every function calls.
Depends on D13781124
Reviewed By: mbouaziz
Differential Revision: D13781147
fbshipit-source-id: 3c8768bd9
Summary:
It adds a semantics for evaluation of abstract location of literal
string, which was missing.
Reviewed By: mbouaziz
Differential Revision: D13915265
fbshipit-source-id: 741df843b
Sungkeun Cho
Dino Distefano
Jeremy Dubreil
Jules Villard
Mehdi Bouaziz
Ezgi Çiçek
Nikos Gorogiannis
Boris Valkov
David Lively
Nikos Gorogiannis