Summary:
Now the domain can reason about `&` and `*` too. When recording `&`
between two locations also record a back-edge `*`, and vice-versa.
Reviewed By: mbouaziz
Differential Revision: D10509335
fbshipit-source-id: 8091b6ec0
Summary: This is more flexible and allows us to give more details when reporting.
Reviewed By: mbouaziz
Differential Revision: D10509336
fbshipit-source-id: 79c3ac1c8
Summary:
Invalidating addresses for destructors to catch use after destructor errors.
To pass ownership tests for use after destructor errors, we still need to:
(1) fix pointer arithmetic false positives
(2) add model for placement new to fix false positives
(3) add model for operator= to fix false positives
(4) support inter-procedural analysis for destructor_order_bad test
Reviewed By: jvillard
Differential Revision: D10450912
fbshipit-source-id: 2d9b1ee68
Summary:
Instead of the non-sensical piecewise join we had until now write
a proper one. Hopefully the comments explain what it does. Main one:
```
(* high-level idea: maintain some union-find data structure to identify locations in one heap
with locations in the other heap. Build the initial join state as follows:
- equate all locations that correspond to identical variables in both stacks, eg joining
stacks {x=1} and {x=2} adds "1=2" to the unification.
- add all addresses reachable from stack variables to the join state heap
This gives us an abstract state that is the union of both abstract states, but more states
can still be made equal. For instance, if 1 points to 3 in the first heap and 2 points to 4
in the second heap and we deduced "1 = 2" from the stacks already (as in the example just
above) then we can deduce "3 = 4". Proceed in this fashion until no more equalities are
discovered, and return the abstract state where a canonical representative has been chosen
consistently for each equivalence class (this is what the union-find data structure gives
us). *)
```
Reviewed By: mbouaziz
Differential Revision: D10483978
fbshipit-source-id: f6ffd7528
Summary:
`Location` was clashing with the `Location` module, so use `Address`
instead.
When invalidating an address, remember the "actor" of its invalidation,
i.e. the access expression leading to the address and the source
location of the corresponding instruction.
When checking accesses, also pass the actor responsible for the access,
so that when we raise an error we know:
1. when and why a location was invalidated
2. when and why we tried to read it after that
Reviewed By: mbouaziz
Differential Revision: D10446282
fbshipit-source-id: 3ca4fb3d4
Summary:
Model `x[y]` and `x.push_back(i)` to catch the classic bug of "take
reference inside vector, invalidate, then use again".
Reviewed By: da319
Differential Revision: D10445824
fbshipit-source-id: 21ffd9677
Summary:
Do the intersection of the heap and stack domains, and the union of the
invalid location sets. This forgets invalid locations that appear only
in one heap, unfortunately. We can start with this and improve later.
Reviewed By: mbouaziz
Differential Revision: D10445825
fbshipit-source-id: cc24460af
Summary:
New analysis in foetal form to detect invalid use of C++ objects after their
lifetime has ended. For now it has:
- A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended)
- The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid.
- A simple transfer function reads and updates the stack and heap in a rudimentary way for now
- C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations
- Also, the domain has a really crappy join and widening for now (see comments in the code)
With this we already pass most of the "use after delete" tests from the
Ownership checker. The ones we don't pass are only because we are missing
models.
Reviewed By: mbouaziz
Differential Revision: D10383249
fbshipit-source-id: f414664cb
Jules Villard
Daiva Naudziuniene