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: This diff changes pp of binary operation condition in order to avoid a `make test` failure. For the same `uint64_t` type, it is translated to `unsigned long long` in 64bit mac, but `unsigned long` in 64bit linux, which made a `make test` failure.
Reviewed By: mbouaziz
Differential Revision: D10459466
fbshipit-source-id: 449ab548e
Summary:
Fix the logic for computing duplicate symbols. It was broken at some point and some duplicate symbols creeped into our tests. Fix these, and add a test to avoid duplicate symbols detection to regress again.
Also, this removes one use of `Cfg.load`, on the way to removing file-wide CFGs from the database.
Reviewed By: ngorogiannis
Differential Revision: D10173349
fbshipit-source-id: a0d2365b3
Summary:
Goal of the stack: deprecate the `--analyzer` option in favour of turning
individual features on and off. This option is a mess: some of the options are
now subcommands (compile, capture), others are aliases (infer and checkers),
and they can all be replicated using some straightforward combination of other
options.
This diff: stop using `--analyzer` in tests. It's mostly `checkers` everywhere,
which is already the default. `linters` becomes `--no-capture --linters-only`.
`infer` is supposed to be `checkers` already. `crashcontext` is
`--crashcontext-only`.
Reviewed By: mbouaziz
Differential Revision: D9942689
fbshipit-source-id: 048281761
Summary:
I realized that control variable analysis was broken when we had multiple back-edges for the same loop. This is often the case when we have a switch statement combined with continue in a loop (see `test_switch` in `switch_continue.c`) or when we have disjunctive guards in do-while loops.
This diff fixes that by
- defining a loop by its loophead (the target of its backedges) rather than its back-edges. Then it converts back-edge list to a map from loop_head to sources of the loop's back-edges.
- collecting multiple guard nodes that come from potentially multiple exit nodes per loop head
In addition, it also removes the wrong assumption that an exit node belongs to a single loop head.
Reviewed By: mbouaziz
Differential Revision: D8398061
fbshipit-source-id: abaf288
Summary:
It's useful to test that the bucket a given error is classified as doesn't
change over time without notice.
This records the bucket for *all* the tests, even though some never produce a
bucket. This is to be on the safe size instead of risking to forget adding the
bucket information when the test changes, or when copy/pasting from a test that
doesn't have buckets to one that does.
The implementation is pretty crude: it greps the beginning of the qualifier
string for a `[bucket]`.
Reviewed By: mbouaziz
Differential Revision: D8236393
fbshipit-source-id: b3b1eb9
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s
Reviewed By: mbouaziz
Differential Revision: D8038941
fbshipit-source-id: 61b10cb
Summary:
Before we were computing the size of an abstract state (`range`) using the `NonNegativeBound` domain but it wasn't able to express product of symbolic values.
This diff introduces a domain for that.
The range of an interval is still computed in `NonNegativeBound` but then the product is done in `TopLiftedPolynomial` so all costs end up being of that type.
The //symbols// of a polynomial are `NonNegativeBound` (so the polynomial only represent non-negative values, perfect for a cost), which handles substitution correctly, i.e. it gives zero instead of negative values.
Reviewed By: ddino
Differential Revision: D7397229
fbshipit-source-id: 6868bb7
Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation
Reviewed By: ddino
Differential Revision: D7844267
fbshipit-source-id: c9d9247
Summary:
We want instr-granular invariant maps so let's use the OneInstrPerNode CFG in the AI analyzers.
This requires specializing the TransferFunctions.
Keep using the normal CFG where we only need node-granular informations.
Depends on D7587241
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618320
fbshipit-source-id: 73918f0
Mehdi Bouaziz
Sungkeun Cho
Jules Villard
Dino Distefano
Martino Luca
Ezgi Çiçek