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:
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:
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:
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:
It terminates narrowing when new and old states are not comparable.
Since current narrowing does not use meet operations guaranteeing
termination of narrowing, it tries to terminate narrowing more
conservatively.
Reviewed By: mbouaziz
Differential Revision: D12815419
fbshipit-source-id: e8b45199e
Summary: It tries division on minmax value approximately, rather than just returning infinities. For example, `[0,2+min(6,s)] / 2` returns `[0,4]`.
Reviewed By: mbouaziz
Differential Revision: D10867091
fbshipit-source-id: d3f49987b
Summary:
This diff preserves values of offset and index separately, rather than
one value of their addition, because premature addition results in
imprecise FPs by the limited expressiveness of the domain.
Reviewed By: mbouaziz
Differential Revision: D10851393
fbshipit-source-id: 1685ead36
Summary:
It avoids checking integer overflow when it definitely cannot happen.
For example, it does not check integer overflow of addition when one
of parameters is a negative number, or underflow of subtraction when
its first parameter is a positive number.
Reviewed By: mbouaziz
Differential Revision: D10446161
fbshipit-source-id: b8c86e1b2
Summary: We assume multiplication of 1 is safe. It happens sometimes by multiplying `sizeof(char)`.
Reviewed By: mbouaziz
Differential Revision: D10444680
fbshipit-source-id: 2f33be280
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: It uses big int, instead of 63bits int of OCaml, in the interval domain in order to get preciser numeric values in the future.
Reviewed By: jvillard
Differential Revision: D10123364
fbshipit-source-id: c217f4366
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:
The model for `getcwd` assumes the first argument should be non-null when in fact a NULL pointer is legitimate and results in allocation:
> As an extension to the POSIX.1-2001 standard, glibc's getcwd() allocates the buffer dynamically using mal‐
> loc(3) if buf is NULL. In this case, the allocated buffer has the length size unless size is zero, when buf
> is allocated as big as necessary. The caller should free(3) the returned buffer.
I suggest this glibc extension be used for the getcwd model to reduce false positives.
Pull Request resolved: https://github.com/facebook/infer/pull/925
Reviewed By: mbouaziz
Differential Revision: D9830450
Pulled By: jvillard
fbshipit-source-id: 95c4862b1
Summary:
It simplifies abstract memory instantiations of function calls. Now it instantiates callee memories by directly evaluating symbol paths, rather than constructing `subst_map`.
main changes are:
- no construction of `subst_map` and `trace_map`
- no symbol table in Inferbo's summary
- no `Symbol_not_found` exception (for when a required symbol was unavailable in `subst_map`)
Reviewed By: mbouaziz
Differential Revision: D9495597
fbshipit-source-id: 18cdcd6f7
Summary: When a typedef-ed structure is defined in another source file, `tenv` returns a structure with empty fields.
Reviewed By: mbouaziz
Differential Revision: D9629200
fbshipit-source-id: 8859803f9
Summary:
It returns unknown values on non-const function calls like on unknown
function calls.
Reviewed By: mbouaziz
Differential Revision: D9478862
fbshipit-source-id: 4b795ec55
Summary: `CONDITION_ALWAYS_**` can be introduced by global constants.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D9478528
fbshipit-source-id: 7b1a46e7a
Summary:
When we see `pthread_create(..., ..., foo, ...)`, we want to call the function
`foo` to check that its precondition is met. The initial goal was to get rid
of the uncouth call to `Summary.get` when what we really want is to analyse
`foo` instead of just betting on the fact that it has been analysed already.
Besides switching to `Ondemand.analyze_proc_name`, this also changes the
matching of the function pointer in the arguments of `pthread_create()` to
detect the common case of a constant function name. I also added tests.
Reviewed By: jeremydubreil
Differential Revision: D9195159
fbshipit-source-id: dfec79f14
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each Mem domain value includes one relational value containing relations among symbols. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: jvillard
Differential Revision: D8874102
fbshipit-source-id: 08e5883cb
Summary:
Infer does the right thing now, make sure it doesn't regress.
https://github.com/facebook/infer/issues/86
Reviewed By: mbouaziz, dulmarod
Differential Revision: D8442855
fbshipit-source-id: 3df29b88c
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each `Mem` domain value includes one relational value containing relations among *symbols*. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three *symbols*, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default, so this diff should not make any differences in CI.
Use `--bo-relational-domain {oct, poly}` for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8478542
fbshipit-source-id: 510ff53
Summary: The frontend got better and now `assert` is correctly translated.
Reviewed By: dulmarod
Differential Revision: D8731877
fbshipit-source-id: ba11b0c
Summary: Record that it is not supported: https://github.com/facebook/infer/issues/8
Reviewed By: mbouaziz, dulmarod
Differential Revision: D8442762
fbshipit-source-id: fa271cb
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: There is a number of dangling pointer dereference false positives coming from our treatment of union in c/cpp. For now, do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8279802
fbshipit-source-id: a339b0e
Sungkeun Cho
Mehdi Bouaziz
Martino Luca
Jules Villard
Ezgi Çiçek
Dino Distefano
Thomas M. DuBuisson
Julian Sutherland
Daiva Naudziuniene