Summary:
This diff extends the abstract domain to keep binary conditions on
prunings, so Inferbo can suppress more proof obligations (i.e., false
positives) that are known to be unreachable according to the binary
conditions.
Depends on D13729600
Reviewed By: mbouaziz
Differential Revision: D13749914
fbshipit-source-id: 314f048f1
Summary:
This will allow disjunctive analyzers to return sets of states as a
result instead of always returning one state. More precisely, this will
be needed for pulse when it becomes inter-procedural, if we take
summaries of functions to be disjunctive too (like, e.g., biabduction
does with several specs per function).
Reviewed By: mbouaziz
Differential Revision: D13537601
fbshipit-source-id: f54caf802
Summary:
Printing "N specs" next to function definitions in the HTML debug is
misleading because there are more checkers than just biabduction.
Reviewed By: mbouaziz
Differential Revision: D13572456
fbshipit-source-id: 209b874df
Summary:
`memcpy` should copy the contents of the source to the destination.
Depends on D13634754
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13668414
fbshipit-source-id: cb0ff2010
Summary: It extends the abstract location for C string length, i.e., the first index of the null character in character array.
Reviewed By: mbouaziz
Differential Revision: D13634241
fbshipit-source-id: d2727d5f5
Summary: Publish solutions to the lab, and a Docker file and image to get started more quickly with infer hacking.
Reviewed By: mbouaziz
Differential Revision: D13648847
fbshipit-source-id: daf48ad03
Summary:
This diff prevents deduplications of issues when they have different
conditions to reach.
Reviewed By: mbouaziz
Differential Revision: D13596220
fbshipit-source-id: 95f802edb
Summary:
In ObjC there are no access modifiers. The strongest alternative is to put methods in the implementation but omit them from the interface declaration.
Put exported ObjC methods in their own field in the class structure and use that in RacerD to decide whether to report on the method.
Reviewed By: mbouaziz
Differential Revision: D13597504
fbshipit-source-id: c4a3d2705
Summary:
It suppresses intended integer overflows that generate hash values or random numbers. For judging that the intention of integer overflow, it applies a heuristics: checking if traces of issues include a whitelisted words, e.g., "rand" or "seed".
While we would be able to suppress all integer overflows of unsigned integers since they have defined behaviors, we don't want to miss unintended integer overflows, e.g., that on unsigned index value.
Depends on D13595958
Reviewed By: mbouaziz
Differential Revision: D13595967
fbshipit-source-id: 8d3aca5a7
Summary:
- `Printer.NodesHtml.start_node` prints the instructions rather than doing it in the callee
- use color class for `<LISTING>` rather than wrapping them in `<span>` (also fixes a wrong nesting between `<LISTING>` and `<span>`)
- `Summary.pp_html` is always `Black`
- New line before `<hr>` and `<LISTING>`
- `Io_infer.Html.create` takes a `SourceFile.t` rather than a `path_kind`
- typo
Reviewed By: jvillard
Differential Revision: D13572247
fbshipit-source-id: 65f57df25
Summary:
Split into:
- `PulseDiagnostic`, formerly `PulseDomain.Diagnostic`
- `PulseOperations`, formerly `PulseDomain.Operations`
This breaks down the now quite large and complex PulseDomain.ml into
more manageable pieces. More importantly, it will allow us to build a
bigger pulse domain later, where elements of the domain are pairs of the
base domain that include a biabductive "footprint".
What's not as nice is that more of the interface of `PulseDomain` is
exposed, in particular `PulseDomain.Memory` and `PulseDomain.Stack`.
We'll have to be careful not to break abstraction barriers and prefer
`PulseOperations` to `PulseDomain` outside of the domain implementation.
OCaml forces us to do that because of the multi-file approach. It could
be solved by introducing pulse domains as a library but who has time for
that...
Sending early because rebasing that diff is painful.
Reviewed By: ngorogiannis
Differential Revision: D13537602
fbshipit-source-id: d211d6e84
Summary:
Record per-location traces. Actually, that doesn't quite make sense as a
location can be accessed in many ways, so associate a trace to each
*edge* in the memory graph. For instance, when doing `x->f = *y`, we
want to take the history of the `<val of y> --*--> ..` edge, add "assigned
at location blah" to it and store this extended history to the edge
`<val of x> --f--> ..`.
Use this machinery to print nicer traces in `infer explore` and better
error messages too (include the last assignment, like biabduction
messages).
Reviewed By: da319
Differential Revision: D13518668
fbshipit-source-id: 0a62fb55f
Summary:
This diff substitutes the conditions of proof obligations strictly, so that the condition of "p!=Null" becomes bottom
when callee's p is Null.
In the non-strict substitution (which is used by default), if p's location is not found it returns the unknown location.
On the other hand, in the strict substitution (which is used only in the substitution of condition of proof obligation),
it returns bottom location.
Depends on D13415366, D13414636
Reviewed By: mbouaziz, jvillard
Differential Revision: D13415377
fbshipit-source-id: 5ae1e888e
Summary: This diff unset powloc and arrayblk values of p when assume(p==Null).
Reviewed By: mbouaziz, jvillard
Differential Revision: D13415366
fbshipit-source-id: a491a957f
Summary:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).
As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.
Reviewed By: skcho
Differential Revision: D13072084
fbshipit-source-id: 9bc0b9881
Summary: In the `operator=` case that assigns from a temporary, we want to assign an object of a temporary not it's address (as a comment already says)
Reviewed By: jvillard
Differential Revision: D13518496
fbshipit-source-id: 72bd23623
Summary: Adding a test case for use after destructor for temporaries. At the moment pulse does not find it as frontend does not inject destructors for temporaries.
Reviewed By: jvillard
Differential Revision: D13506229
fbshipit-source-id: 31b9466f7
Summary:
It weakens canonical path in order to avoid an explosion of locations when a struct type has pointers to struct.
For example:
```
struct Tree {
struct Tree *root;
struct Tree *left;
struct Tree *right;
};
```
It was able to generate lots of abstract locations before this diff:
```
t->root
t->left
t->right
t->root->left
t->root->right
t->left->root
t->left->right
t->right->root
t->right->left
t->root->left->right
t->root->right->left
t->left->root->right
t->left->right->root
t->right->root->left
t->right->left->root
```
By this diff, pointer fields that have the same type are (unsoundly) canonicalized to the same one. For example,
```
t->root
t->root->left
t->root->right
t->root->left->right
t->root->right->left
```
are canonicalized to `t->root`. This is definitely unsound but I believe it is better than the location explosion by which analyses do not terminate in a reasonable time or giving a fixed limit of depth to the field access.
Reviewed By: mbouaziz
Differential Revision: D13503808
fbshipit-source-id: 867018712
Summary:
When a C++ temporary goes out of scope, tag its address in the heap with
a new attribute `AddressOfCppTemporary` so that we can later check that
we don't return it.
Reviewed By: da319
Differential Revision: D13466898
fbshipit-source-id: 8808338b4
Summary:
When assign to the special `return` variable, check that the result is
not the address of a local variable, otherwise report.
Reviewed By: ngorogiannis
Differential Revision: D13466896
fbshipit-source-id: 465da7f13
Summary: Naming it `FP_` was a mistake in the original commit that copied the tests over as pulse has never reported on that method.
Reviewed By: da319
Differential Revision: D13465324
fbshipit-source-id: f8b24ebda
Summary:
In order to avoid FPs due to lack of relational info, we apply a heuristic: proof obligations has a latest pruned values,
then it is instantiated at Call statements. If there is a bottom value in the instantiated pruned values, we can say the
program point where the proof obligation is introduced is unreachable with the given parameters of the function.
Depends on D13414441
Reviewed By: mbouaziz
Differential Revision: D13414483
fbshipit-source-id: 61bd34ebb
Summary:
It's ok to take an address of a field / array access of an invalid object.
This diff calculates the inner most dereference for an access expression starting with `&` and does not report on the dereference even if the address is invalid.
Reviewed By: jvillard
Differential Revision: D13450758
fbshipit-source-id: 18c038701
Summary:
When we create Dereference edge, we also create TakeAddress back edge. This causes false positives for stack variables. When we write to a stack variable and then take its address, the resulting address is the one from the back edge of the written value. See example `push_back_value_ok`. To solve this issue, this diff changes stack to denote a map from address of variables rather than from variables.
We still have issue for fields, see example, FP_push_back_value_field_ok. To solve this, we probably need to remove back edges.
Reviewed By: jvillard
Differential Revision: D13432415
fbshipit-source-id: 9254a1a6d
Summary: Mostly a revert of D13190876 once the disjunctive domain is in place.
Reviewed By: da319
Differential Revision: D13432488
fbshipit-source-id: f1e98ef0d
Summary:
Change join/widen policies to more interesting ones and play around to
find a good tradeoff.
Reviewed By: mbouaziz
Differential Revision: D13432492
fbshipit-source-id: 2c3e498dd
Summary:
Introduce machinery to do disjunctive HIL domains and use it for pulse,
but only in a mode that preserves the existing behaviour.
The disjunctive domain is a functor that turns any (HIL for now)
transfer function module into one operating on sets of elements of the
original domain. The behaviour of joins (and widenings, which are equal
to joins) can be chosen when instantiating the functor among 3
behaviours:
- `` `JoinAfter n`: when the set of disjuncts gets bigger than `n` the
underlying domain's join is called to collapse them into one state
- `` `UnderApproximateAfter n`: when the sest of disjuncts gets bigger
than `n` then just stop adding new states to it, drop any further states
on the floor. This corresponds to an under-approximation/bounded
approach.
- `` `NeverJoin`
The widening is always of the form ``
`UnderApproximateAfterNumIterations max_iter` for now since the only
user is pulse and I'm not sure what else would be useful.
Picking `` `JoinAfter 0` gives the same results as the non-disjunctive
domain since the underlying `join` will always be called. Make pulse use
this mode for now, and tune it in a next diff.
Reviewed By: mbouaziz
Differential Revision: D13431375
fbshipit-source-id: b93aa50e7
Summary:
This will be useful to make the analysis more precise. In particular, it
allows a disjunctive version of pulse to deal will deleting vector
elements in a loop: without this, deleting an array element in one
iteration will make the analysis think that the next array element is
invalid too since they are all the same. By keep track of the index, we
can detect when we are sure that two elements are the same and only
report in that case.
Reviewed By: ngorogiannis
Differential Revision: D13431374
fbshipit-source-id: dae82deeb
Summary:
A lot of functors that take a `Make{SIL,HIL}` can take a `{SIL,HIL}`
directly instead. This makes my head hurt a bit less.
Reviewed By: mbouaziz
Differential Revision: D13416967
fbshipit-source-id: eb0b33bc4
Summary:
When a lambda gets created, record the abstract addresses it captures, then
complain if we see some of them be invalidated before it is called.
Add a notion of "allocator" for reporting better messages. The messages are
still a bit sucky, will need to improve them more generally at some point.
```
jul lambda ~ infer 1 infer -g --pulse-only -- clang -std=c++11 -c infer/tests/codetoanalyze/cpp/pulse/closures.cpp
Logs in /home/jul/infer.fb/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /home/jul/infer.fb/infer-out
Found 2 issues
infer/tests/codetoanalyze/cpp/pulse/closures.cpp:21: error: USE_AFTER_DESTRUCTOR
`&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 20, column 3 past its lifetime (debug: 5).
19. f = [&s] { return s.f; };
20. } // destructor for s called here
21. > return f(); // s used here
22. }
23.
infer/tests/codetoanalyze/cpp/pulse/closures.cpp:30: error: USE_AFTER_DESTRUCTOR
`&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 29, column 3 past its lifetime (debug: 8).
28. f = [&] { return s.f; };
29. }
30. > return f();
31. }
32.
Summary of the reports
USE_AFTER_DESTRUCTOR: 2
```
Reviewed By: da319
Differential Revision: D13400074
fbshipit-source-id: 3c68ff4ea
Summary: Model more `std::vector` functions that can potentially invalidate references to vector's elements (https://en.cppreference.com/w/cpp/container/vector).
Reviewed By: mbouaziz
Differential Revision: D13399161
fbshipit-source-id: 95cf2cae6
Summary:
Some code calls `this->~Obj()` then proceeds to use fields in the current
object, which previously we would report as invalid uses. Assume people know
what they are doing and ignore destructor calls to `this`.
Reviewed By: mbouaziz
Differential Revision: D13401145
fbshipit-source-id: f6b0fb6ec
Sungkeun Cho
Nikos Gorogiannis
Jules Villard
David Lively
Jeremy Dubreil
Mehdi Bouaziz
Ezgi Çiçek
Fabio Milano
Daiva Naudziuniene
Martino Luca