Summary:
When we know "x = 3" and we have a condition "x != 3" we know we can
prune the corresponding path.
Reviewed By: skcho
Differential Revision: D17665472
fbshipit-source-id: 988958ea6
Summary:
Turns out `Memory.add_attributes` was only used to add singletons so
deleted that in the process.
Reviewed By: skcho
Differential Revision: D17627725
fbshipit-source-id: 0abe3889d
Summary:
Introduce a new experimental checker (`--impurity`) that detects
impurity information, tracking which parameters and global variables
of a function are modified. The checker relies on Pulse to detect how
the state changes: it traverses the pre and post pairs starting from
the parameter/global variable and finds where the pre and post heaps
diverge. At diversion points, we expect to see WrittenTo/Invalid attributes
containing a trace of how the address was modified. We use these to
construct the trace of impurity.
This checker is a complement to the purity checker that exists mainly
for Java (and used for cost and loop-hoisting analyses). The aim of
this new experimental checker is to rely on Pulse's precise
memory treatment and come up with a more precise im(purity)
analysis. To distinguish the two checkers, we introduce a new issue
type `IMPURE_FUNCTION` that reports when a function is impure, rather
than when it is pure (as in the purity checker).
TODO:
- improve the analysis to rely on impurity information of external
library calls. Currently, all library calls are assumed to be nops,
hence pure.
- de-entangle Pulse reporting from analysis.
Reviewed By: skcho
Differential Revision: D17051567
fbshipit-source-id: 5e10afb4f
Summary:
Pulse didn't treat local variables going out of scope as invalidating the corresponding address in memory. This diff fixes that by
- marking all local variables that exits the scope with the attribute `AddressOfStackVariable`
- before we write the summary for the proc, we make sure to invalidate all such addresses local to the procedure as `Invalid.` If such an address is read, then we would raise a use-after-lifetime issue.
Reviewed By: jvillard
Differential Revision: D16458355
fbshipit-source-id: 3686524cb
Summary: We know how to do interprocedural calls so let's use that!
Reviewed By: mbouaziz
Differential Revision: D16008164
fbshipit-source-id: 4c34bf704
Summary:
Fixes a false positive where the address of a C++ temporary is bound to
a static const reference variable then returned. The fix doesn't try to
establish that the variable is a const reference so could lead to false
negatives but that can be addressed later.
Reviewed By: ezgicicek
Differential Revision: D16004538
fbshipit-source-id: e403dbefe
Summary:
[apologies for the unreviewable diff...]
Get rid of HIL expressions in pulse. This finishes the HIL -> SIL
migration. The first step made pulse start from SIL instructions but
would translate most accesses to HIL to re-use most of the existing
pulse code. This diff gets rid of the intermediate translation of SIL
expressions to HIL expressions.
Big changes:
1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything.
2. Stop trying to reverse-engineer what addresses mean in terms of
access paths from program variables. Rely on the trace pointing at
the right places in the code to be enough. This is because it wasn't
that useful (and could even be misleading when wrong) but could be
prohibitively expensive in degenerate cases (eg nodes with tens of
thousands of successive array accesses...)
3. `PulseAbductiveDomain.apply_post` now returns the computed return
value instead of recording it itself.
4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event`
5. Function calls arguments are now evaluated prior to doing anything
else, which saves everything else from having to (remember to) do
that. In particular, this changes how models look quite a bit.
Reviewed By: mbouaziz
Differential Revision: D15986373
fbshipit-source-id: 1d79935de
Summary:
Now that HIL doesn't help us anymore we need to reconstruct its mapping
"SIL logical var -> program access path". We already have everything we
need in pulse: it suffices to walk the current memory graph starting
from program variables until we find the value of the temporary we are
interested in.
This diff also builds some type machinery to make sure all accesses are
explained.
Reviewed By: mbouaziz
Differential Revision: D15824959
fbshipit-source-id: 722c81b39
Summary:
Just moving code around.
This is needed later to make some types in `PulseTrace` depend on
a new that I'll have to define in `PulseDomain`.
Also, this gives better names all around I think
Reviewed By: mbouaziz
Differential Revision: D15881281
fbshipit-source-id: e86c1472e
Summary:
Just moving code around.
This is needed later to make some types in `PulseInvalidation` depend on
a new type that I'll have to define in `PulseDomain`.
Reviewed By: mbouaziz
Differential Revision: D15824962
fbshipit-source-id: 86cba2bfb
Summary:
Before: the trace would explain how a value was invalidated and
accessed, but not how the value that was invalidated had been
constructed.
Now: `PulseTrace.t` records breadcrumbs of how the value was constructed
in addition to the interproc "action" trace leading to the invalidation
or access action.
Concretely:
```
void bad(X &x) {
X *y = x;
X *z = x;
delete y;
access(z);
}
```
will produce the trace:
Invalidation part:
y = x
delete y
Access part:
z = x
access(z)
access to z->f inside of access(z)
Before this diff the "Access part" would be missing the "z = x" part of
the trace, so it might be confusing why `z` has anything to do with `y`.
However, such "breadcrumbs" are not recorded in the inter-procedural
part, only the sequence of calls is. This is a trade-off for simplicity,
maybe it's enough for developers maybe it isn't, we'll find out later.
Reviewed By: jberdine
Differential Revision: D15354438
fbshipit-source-id: 8d0aed717
Summary:
In preparation for the next diff that re-uses `PulseTrace.t` for a type
that combines breadcrumbs + action.
No change intended.
Reviewed By: mbouaziz, jberdine
Differential Revision: D15354437
fbshipit-source-id: cbb8757b4
Summary:
Feedback from peterogithub:
- mention which access path is being invalidated and accessed in the message
- mention the line at which it was invalidated (the line at which it's accessed is already the line at which we report)
- traces for stack variable/C++ temporary address escapes
- delete double implementation of the same functionality in
`PulseTrace`: `location_of_action_start` is the same as
`outer_location_of_action`...
Reviewed By: jberdine
Differential Revision: D14800294
fbshipit-source-id: 3d9ab9b3d
Summary:
Only throw values to the pre if they can be followed from "abducible"
variables: formals of the current method and globals.
Because figuring out if a `Pvar.t` is a formal of the current procedure
is actually a giant pain, hack something not too bad instead:
pre-register all formals at the start of the analysis of the
procedure. Then the only other variables we care about in the
precondition are globals, which we can detect easily.
This is mostly an optimisation (summaries won't include irrelevant
"abduced" facts about the procedure's local variables anymore), but it
also fixes a bug where we would sometimes overwrite things in the pre. I
think that's why the tests improved.
Reviewed By: ngorogiannis
Differential Revision: D14753493
fbshipit-source-id: 08e73637f
Summary:
This mostly doesn't make sense. The only thing this would have been good
for was to give the most accurate result on access paths such as
`*(&(x.f))`, but these are normalised anyway (into `x.f`) so we actually
never see these. That said there might be some use to some similar logic
in the future, but in the meantime let's delete the current feature as
it wasn't thought through.
Reviewed By: ezgicicek
Differential Revision: D14753492
fbshipit-source-id: 597cec027
Summary:
For each operation on the domain, try to record what it requires of the
precondition of the function. This is akin to what happens in the
biabduction backend, hence the terminology used.
Reviewed By: jberdine
Differential Revision: D14387148
fbshipit-source-id: a61fe30c8
Jules Villard
Ezgi Çiçek
Josh Berdine