Summary:
The introduction of inferbo intervals as pulse attributes creates the
first relational attributes. To make sense of inferbo intervals
appearing in summaries when in a caller context, we need to substitute
the abstract values they contain in the callee with the abstract values
they correspond to in the caller.
This has a significant consequence: we have to delay the check that
arithmetic constraints in the callee are satisfiable at the call-site
until *after* we have discovered all the relationships between callee
values and caller values from the heap. To solve this, we now run an
arithmetic constraints check *after* having materialised all the
addresses.
We also need to translate the abstract values in the attributes in the
post before recording them in the caller, for the same reasons.
Quite some code in this diff is concerned with substituting pulse values
inside inferbo intervals. There is a complication there too: even after
having discovered relationships between caller and callee abstract
values induced by the heap shapes, there could be abstract values in the
callee's attributes that we haven't seen yet. We need to make up new
values for these in the caller, so this substitution has to return a
potentially extended substitution.
Reviewed By: skcho
Differential Revision: D18745695
fbshipit-source-id: 077ae7670
Summary: This extends semantics of binary operator for BoItv. If there is no known interval value for a pulse value, it returns a symbolic value of the pulse value.
Reviewed By: jvillard
Differential Revision: D18726768
fbshipit-source-id: ed8ecf78b
Summary:
This diff adds inferbo's interval values to pulse's attributes. The added values will be used to
filter out infeasible passes in the following diffs.
Reviewed By: jvillard
Differential Revision: D18726667
fbshipit-source-id: c1125ac6e
Summary:
When reporting null dereference it is useful to know where the null came
from.
Reviewed By: skcho
Differential Revision: D18206459
fbshipit-source-id: 0c8e6781b
Summary:
This simplifies the code overall. It also makes accessing the action of
a "trace" (which is now stored alongside it instead of deep inside it)
constant time instead of linear in the number of nested calls.
Reviewed By: skcho
Differential Revision: D18206460
fbshipit-source-id: 9546ff36f
Summary:
This adds a more interesting value domain to pulse: concrete intervals.
There are still two main limitations:
1. arithmetic operations are all over-approximated: any assignment involving arithmetic operations is replaced by non-determinism
2. abstract values that are discovered to be equal are not merged into one
Reviewed By: skcho
Differential Revision: D18058972
fbshipit-source-id: 0492a590f
Summary:
This does several things because it was hard to split it more:
1. Split most of the arithmetic reasoning to PulseArithmetic.ml. This
doesn't need to be reviewed thoroughly because an upcoming diff
changes the domain from just `EqualTo of Const.t` to an interval domain!
2. When going through a prune node intra-procedurally, abduce arithmetic
facts to the pre (instead of just propagating them). This is the "assume
as assert" trick used by biabduction 1.0 too and allows to propagate
arithmetic constraints to callers.
3. Use 2 when applying summaries by pruning specs whose preconditions
have un-satisfiable arithmetic constraints.
This changes one of the tests! Pulse now does a bit more work to find
the false positive, as can be seen in the longer trace.
Reviewed By: skcho
Differential Revision: D18117160
fbshipit-source-id: af3b2c8c0
Summary:
Instead of checking that each address in the pre that must be valid is
not invalid in the caller (and error out if it turns out it is invalid)
as we discover them, save these checks for after we are sure that the
precondition can be applied. It is in fact a bug that we can report an
error when trying to apply a precondition that is actually not
satisfiable in the current state for other reasons than lifetime issues.
We still want to skip calls in case of weird issues like mismatch in
number of formals vs actuals.
This will have more obvious effects later when we also check that
arithmetic facts in preconditions are satisfied at the call site: if a
pre mandates "x=1" and "y must be valid" and we have "x=0" and "y
invalid" then we shouldn't report an error.
Reviewed By: skcho
Differential Revision: D18115229
fbshipit-source-id: ad4ce72ff
Summary:
If a precondition cannot be applied, it means that this program path
somehow doesn't make sense for the caller and so should be pruned. Right
now we just treat this as skipping over the call instead.
This will become more important when specs start mentioning arithmetic
facts that must be satisfied at the call site. As it is we will only
stop if we discover aliasing in the pre not present at the call site or
vice versa.
Reviewed By: dulmarod
Differential Revision: D18115230
fbshipit-source-id: 4f1c7a583
Summary: The way `<=` is used in `AbstractDomain` prevents infix use and forces bracketing it everywhere. Replace with simple `leq`.
Reviewed By: jvillard
Differential Revision: D18201854
fbshipit-source-id: 8175224e4
Summary:
That module's interface was repeated twice to avoid exposing its
internals to PulseDomain itself. It's also quite long so it makes sense
to move it to its own file.
Reviewed By: ezgicicek
Differential Revision: D17977209
fbshipit-source-id: 56a2dac24
Summary:
Another poorman's library, this time about Pulse Domains. Also renames
`PulseDomain` to `PulseBaseDomain`.
Reviewed By: ezgicicek
Differential Revision: D17955287
fbshipit-source-id: 9c947cf98
Summary:
See explanations in D17955104.
This renames `AbstractAddress` to `AbstractValue` since they are not
necessarily addresses.
Reviewed By: ezgicicek
Differential Revision: D17955290
fbshipit-source-id: 8bb4c61f2
Summary:
See explanations in D17955104. I put Attributes inside PulseAttribute
instead of creating a new file to avoid exposing more internals about
ranks.
Reviewed By: ezgicicek
Differential Revision: D17955284
fbshipit-source-id: a8719a58f
Summary:
bigmacro_bender
There are 3 ways pulse tracks history. This is at least one too many. So
far, we have:
1. "histories": a humble list of "events" like "assigned here", "returned from call", ...
2. "interproc actions": a structured nesting of calls with a final "action", eg "f calls g calls h which does blah"
3. "traces", which combine one history with one interproc action
This diff gets rid of interproc actions and makes histories include
"nested" callee histories too. This allows pulse to track and display
how a value got assigned across function calls.
Traces are now more powerful and interleave histories and interproc
actions. This allows pulse to track how a value is fed into an action,
for instance performed in callee, which itself creates some more
(potentially now interprocedural) history before going to the next step
of the action (either another call or the action itself).
This gives much better traces, and some examples are added to showcase
this.
There are a lot of changes when applying summaries to keep track of
histories more accurately than was done before, but also a few
simplifications that give additional evidence that this is the right
concept.
Reviewed By: skcho
Differential Revision: D17908942
fbshipit-source-id: 3b62eaf78
Summary:
I dunno, seemed wrong before. About to introduce another attribute with
similar arguments so making them consistent in advance.
Reviewed By: skcho
Differential Revision: D17930349
fbshipit-source-id: 944b58bac
Summary:
- add the variable being declared so we can report it back in the trace in addition to its location
- distinguish between local vars and formals
Reviewed By: skcho
Differential Revision: D17930348
fbshipit-source-id: a5b863e64
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:
First step in having a value domain: record concrete values. We record
them as equalities to abstract values using a new attribute `Constant`.
In a way, attributes are already our "pure" part in the "formulas" that
are pulse abstract domains, so this is reminiscent of existing
separation logic implementations. Trying to add values directly in the
"heap" part proved very cumbersome whereas this approach is very simple,
allowing us to ignore values most of the time except when we actually
care.
Reviewed By: skcho
Differential Revision: D17665473
fbshipit-source-id: b8033ad9c
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: Like we removed empty edges from the `pre_heap` in D16419183, let's do the same to `post_heap`.
Reviewed By: skcho
Differential Revision: D17111336
fbshipit-source-id: c35fcbabb
Summary:
Before this diff we would record when some values came from the "address
of" logical variables. This makes no sense and also was incorrectly
marking these addresses as "written to" when they appeared in the post
of a procedure, because their attributes weren't empty (they had the
"address of stack variable" attribute).
Reviewed By: ngorogiannis
Differential Revision: D17131210
fbshipit-source-id: 6cc3c465a
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:
Be more flexible in what type of function calls are allowed in `ViaCall ...` actions to be able to include models.
Also get rid of `here here` in traces /o\
As a side-effect, get more precise (=qualified) procedure names in
traces (but not in messages so as not to be too verbose).
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D16121092
fbshipit-source-id: fb51b02f8
Summary:
Sometimes the post of a function call has attributes on addresses that
were mentioned in the pre but are no longer reachable in the post. We
don't want to forget these, see added test.
Reviewed By: mbouaziz
Differential Revision: D16050050
fbshipit-source-id: 1ce522b97
Summary:
Previously we would union them with the previous attributes. I don't
think that makes sense.
Also change the interface a bit in preparation for the next commit.
Reviewed By: mbouaziz
Differential Revision: D16050051
fbshipit-source-id: 2e8f88f4e
Summary:
Noticed that:
- some option was always `Some _`
- recording the post never raises `Aliasing` (only exploring the pre does)
- a mutual recursion was unused
Reviewed By: mbouaziz
Differential Revision: D16050052
fbshipit-source-id: 7f77aae08
Summary: We know how to do interprocedural calls so let's use that!
Reviewed By: mbouaziz
Differential Revision: D16008164
fbshipit-source-id: 4c34bf704
Summary:
Printing `Exp.Const (Cfun proc_name)` adds `_fun_` in front of the
procedure name, eg `_fun_foo` instead of `foo`. This showed up in pulse
traces.
Reviewed By: mbouaziz
Differential Revision: D16004606
fbshipit-source-id: 72ac6866f
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:
Make it possible to re-use the graph visitor to compute all sorts of
things with a flexible API where you can pass a function that folds over
all addresses reachable from certain stack variables (specified with a
filter) and gets passed the access path that leads to each address.
This is used in later commits.
Reviewed By: mbouaziz
Differential Revision: D15824960
fbshipit-source-id: c424a71cb
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
Jules Villard
Sungkeun Cho
Josh Berdine
Nikos Gorogiannis
Ezgi Çiçek