Summary:
A previous change made pulse look into value histories for causes of
invalidation in case the access trace of a value already contained the
reason why that value is invalid, in order to save printing the
invalidation trace in addition to the access trace. It also made
reporting more accurate for null dereference as the source of null was
often better identified (in cases where several values are null or
zero).
But, the history is also relevant to the bug type and the error message.
Make these take histories into account too.
Also fix a bug where we didn't look inside the sub-histories contained
within function calls when looking for an invalidation along the
history.
Reviewed By: da319
Differential Revision: D28254334
fbshipit-source-id: 5ca00ee54
Summary:
When garbage-collecting addresses we would also remove their attributes.
But even though the addresses are no longer allocated in the heap, they
might show up in the formula and so we need to remember facts about
them.
This forces us to detect leaks closer to the point where addresses are
deleted from the heap, in AbductiveDomain.ml. This is a nice refactoring
in itself: doing so fixes some other FNs where we sometimes missed leak
detection on dead addresses.
This also makes it unecessary to simplify InstanceOf eagerly when
variables get out of scope.
Some new {folly,std}::optionals false positives that either are similar to existing ones or involve unmodelled smart pointers.
Reviewed By: da319
Differential Revision: D28126103
fbshipit-source-id: e3a903282
Summary:
Building on the infra in the previous commits, "fix" all the call sites
that introduce invalidations to make sure they also update the
corresponding histories. This is only possible to do when the access
leading to the invalidation can be recorded. Right now the only place
that's untraceable is the model of `free`/`delete`, because it happens
to be the only place where we invalidate an address without knowing
where it comes from (`free(v)`: what was v's access path? we could track
this in the future).
Reviewed By: skcho
Differential Revision: D28118764
fbshipit-source-id: de67f449e
Summary:
As explained in the previous diff: when the access trace goes through
the invalidation step there is no need to print the invalidation trace
at all.
Note: only a few sources of invalidation are handled at the moment. The
following diffs gradually fix the other sources of invalidation.
Reviewed By: skcho
Differential Revision: D28098335
fbshipit-source-id: 5a5e6481e
Summary:
The eventual goal is to stop having separate sections of the trace
("invalidation part" + "access part") when the "access part" already
goes through the invalidation step. For this, it needs to record when a
value is made invalid along the path.
This is also important for assignements to NULL/0/nullptr/nil: right now
the way we record that 0 is not a valid address is via an attribute
attached to the abstract value that corresponds to 0. This makes traces
inconsistent sometimes: 0 can appear in many places in the same function
and we won't necessarily pick the correct one. In other words, attaching
traces to *values* is fragile, as the same value can be produced in many
ways. On the other hand, histories are stored at the point of access, eg
x->f, so have a much better chance of being correct. See added test:
right now its traces is completely wrong and makes the 0 in `if
(utf16StringLen == 0)` the source of the NULL value instead of the
return of `malloc()`!
This diff makes the traces slightly more verbose for now but this is
fixed in a following diff as the traces that got longer are those that
don't actually need an "invalidation" trace.
Reviewed By: skcho
Differential Revision: D28098337
fbshipit-source-id: e17929259
Summary:
This diff avoids dereference of C struct, in its frontend and its semantics of Pulse. In SIL, C
struct is not first-class value, thus dereferencing on it does not make sense.
Reviewed By: ezgicicek
Differential Revision: D27953258
fbshipit-source-id: 348d56338
Summary:
Whenever an equality "t = v" (t an arbitrary term, v a variable) is
added (or "v = t"), remember the "t -> v" mapping after canonicalising t
and v. Use this to detect when two variables are equal to the same term:
`t = v` and `t = v'` now yields `v = v'` to be added to the equality
relation of variables. This increases the precision of the arithmetic
engine.
Interestingly, the impact on most code I've tried is:
1. mostly same perfs as before, if a bit slower (could be within noise)
2. slightly more (latent) bugs reported in absolute numbers
I would have expected it to be more expensive and yield fewer bugs (as
fewer false positives), but there could be second-order effects at play
here where we get more coverage. We definitely get more latent issues
due to dereferencing pointers after testing nullness, as can be seen in
the unit tests as well, which may alone explain (2).
There's some complexity when adding term equalities where the term
is linear, as we also need to add it to `linear_eqs` but `term_eqs` and
`linear_eqs` are interested in slightly different normal forms.
Reviewed By: skcho
Differential Revision: D27331336
fbshipit-source-id: 7314e127a
Summary:
On some pathological examples of crypto primitives like libsodium, later
diffs make pulse grind to a halt due to an explosion in the size of
literals. This is at least partly due to the fact the arithmetic doesn't
operate modulo 2^64.
Due to the fact the arithmetic is confused in any case when we reach
such large numbers, cap them, currently at 2^128. This removes pathological
cases for now, even now on libsodium Pulse is ~5 times faster than before!
Take this opportunity to put the modified Q/Z modules in the own files.
Reviewed By: jberdine
Differential Revision: D27463933
fbshipit-source-id: 342d941e2
Summary:
See updated tests and code comments: this changes many arithmetic
operations to detect when a contradiction "p|->- * p=0" is about to be
detected, and generate a latent issue instead. It's hacky but it does
what we want. Many APIs change because of this so there's some code
churn but the overall end result is not much worse thanks to monadic
operators.
Reviewed By: skcho
Differential Revision: D26918553
fbshipit-source-id: da2abc652
Summary:
Adapting error messages in Pulse so that they become more intuitive for
developers.
Reviewed By: jvillard
Differential Revision: D26887140
fbshipit-source-id: 896970ba2
Summary:
This resolves a few instances of false negatives; typically:
```
if (x == y) {
// HERE
*x = 10;
*y = 44;
// THERE
}
```
We used to get
```
HERE: &x->v * &y ->v' * v == v'
THERE: &x->v * &y ->v' * v == v' * v |-> 10 * v' |-> 44
```
The state at THERE was thus inconsistent and detected as such (v` and
`v'` are allocated separately in the heap hence cannot be equal).
Now we normalize the state more eagerly and so we get:
```
HERE: &x->v * &y->v
THERE: &x->v * &y->v * v |-> 44
```
Reviewed By: skcho
Differential Revision: D26488377
fbshipit-source-id: 568e685f0
Summary:
These were present for `std::optional` but not `folly::Optional` for
some reason.
Reviewed By: da319
Differential Revision: D26450400
fbshipit-source-id: 45051e828
Summary:
Having different behaviours inter-procedurally and intra-procedurally
sounds like a bad design in retrospect. The model of free() should not
depend on whether we currently know the value is not null as that means
some specs are missing from the summary.
Reviewed By: skcho
Differential Revision: D26019712
fbshipit-source-id: 1ac4316a5
Summary:
When a single field struct is initialized with "type x{v}" form, the translated result is not straightforward. For example,
```
struct t {
int val_;
};
void foo(t x) {
t y{x};
}
```
calls the copy constructor with `x`. This is good.
```
void foo(int n) {
t y{n};
}
```
assigns the integer `n` to `y.val_`. This is good.
```
t get_v();
void foo() {
t y{get_v()};
}
```
assigns return value of `get_v` to `y.val_`, rather than calling the copy constructor. This is not
good, but doesn't matter for actual running; `&y.val_` is the same to `&y` and `t` value is the same
to `int` value.
Reviewed By: jvillard
Differential Revision: D26146578
fbshipit-source-id: 8a81bb1db
Summary: This diff fixes incorrect order of statements on `*p = !b;`.
Reviewed By: jvillard
Differential Revision: D26125069
fbshipit-source-id: 9dcefbd34
Summary:
This diff fixes incorrect order of statements on assignments.
In the translation of `LHS=RHS;`, if `RHS` is a complicated expression that introduced new nodes, eg a conditional expression, some load statements for `LHS` came after its usage. To avoid the issue, this diff forces it to introduce new nodes for `LHS`.
Reviewed By: jvillard
Differential Revision: D26099782
fbshipit-source-id: 27417cd99
Summary:
This was left as a TODO before: where to place calls to destructors for
C++ temporaries that are only conditionally creating when evaluating an
expression. This can happen inside the branches of a conditional
operation `b?e:f` or in potentially-short-circuited conditions on the
righ-hand side of `&&` and `||` operators.
Following the compilation scheme of clang (observed by looking at the
generated LLVM bitcode), we instrument the program with "marker"
variables, so that for instance `X x = true?X():y;` becomes (following
the execution on the true branch):
```
marker1 = 0; // initialize all markers to 0
PRUNE(true) // entering true branch
X::X(&temporary); // create temporary...
marker1 = 1; // ...triggers setting its marker to 1
X::X(&x, &temporary); // finish expression
if (marker1) {
X::~X(&temporary); // conditionally destroy the temporary
}
```
In this diff, you'll find code for:
- associating markers to temporaries that need them
- code to initialize markers to 0 before full-expressions
- code to conditionally destroy temporaries based on the values of the
markers once the full-expression has finished evaluating
Reviewed By: da319
Differential Revision: D24954070
fbshipit-source-id: cf15df7f7
Summary: Model `folly::Optional::get_pointer` which returns an address to a value if exists or `nullptr` if empty.
Reviewed By: jvillard
Differential Revision: D24935677
fbshipit-source-id: 9d990fe07
Summary:
We deliberately stopped as soon as an error was detected when applying a
function call. This is not good as other pre/posts of the function may
apply cleanly, which would allow us to cover more behaviours of the
code.
Went on a bit of a refactoring tangeant while fixing this, to clarify
the `Ok None`/`Ok Some _`/`Error _` datatype returned by PulseInterproc.
Now we report errors as soon as we find them during function calls but
continue accumulating specs afterwards.
Reviewed By: da319
Differential Revision: D24888768
fbshipit-source-id: d5f2c29d7
Summary:
Communicate new facts from the arithmetic domain to the memory domain to
detect contradictions between the two.
Reviewed By: jberdine
Differential Revision: D24832079
fbshipit-source-id: 2caf8e9af
Summary:
This is several inter-connected changes together to keep the tests
happy.
The ConditionalOperator `b?t:e` is translated by first creating a
placeholder variable to temporarily store the result of the evaluation
in each branch, then the real thing we want to assign to reads that
variable. But, there are situations where that changes the semantics of
the expression, namely when the value created is a struct on the stack
(eg, a C++ temporary). This is because in SIL we cannot assign the
*address* of a program variable, only its contents, so by the time we're
out of the conditional operator we cannot set the struct value
correctly anymore: we can only set its content, which we did, but that
results in a "shifted" struct value that is one dereference away from
where it should be.
So a batch of changes concern `conditionalOperator_trans`:
- instead of systematically creating a temporary for the conditional,
use the `trans_state.var_exp_typ` provided from above if available
when translating `ConditionalOperator`
- don't even set anything if that variable was already initialized by
merely translating the branch expression, eg when it's a constructor
- fix long-standing TODO to propagate these initialization facts
accurately for ConditionalOperator (used by `init_expr_trans` to also
figure out if it should insert a store to the variable being
initialised or not)
The rest of the changes adapt some relevant other constructs to deal
with conditionalOperator properly now that it can set the current
variable itself, instead of storing stuff inside a temp variable. This
change was a problem because some constructs, eg a variable declaration,
will insert nodes that set up the variable before calling its
initialization, and now the initialization happens *before* that setup,
in the translation of the inner conditional operator, which naturally
creates nodes above the current one.
- add a generic helper to force a sequential order between two
translation results, forcing node creation if necessary
- use that in `init_expr_trans` and `cxxNewExpr_trans`
- adjust many places where `var_exp_typ` was incorrectly not reset when translating sub-expressions
The sequentiality business creates more nodes when used, and the
conditionalOperator business uses fewer temporary variables, so the
frontend results change quite a bit.
Note that biabduction tests were invaluable in debugging this. There
could be other constructs to adjust similarly to cxxNewExpr that were
not covered by the tests though.
Added tests in pulse that exercises the previous bug.
Reviewed By: da319
Differential Revision: D24796282
fbshipit-source-id: 0790c8d17
Summary: We recently introduced a more precise model for constructing an optional from a value by making a shallow copy. However, this introduced Use After Delete false positives. For now, we go back to a less precise model by creating a fresh value. A proper model would be to either make a deep copy or call the copy constructor for a value. We will address this in the following diff.
Reviewed By: jvillard
Differential Revision: D24826749
fbshipit-source-id: 3e5e4edeb
Summary: Refactor `folly::Optional` models to make them easier to reuse for `std::optional`
Reviewed By: jvillard
Differential Revision: D24760053
fbshipit-source-id: f665e84c8
Summary: `folly::Optional::value()` returns a reference, hence an error was shown when the actual value was being accessed. Since `value()` throws an exception in case of `folly::none`, we want to show the error message at the call site of `value()`. We do this by dereferencing the result of `value()` in the model.
Reviewed By: jvillard
Differential Revision: D24702875
fbshipit-source-id: ca9f30349
Summary:
Before we were creating a fresh internal value when we were constructing `folly::Optional`. This diff models `folly::Optional` constructor more precisely by copying the given value.
There was also a missing dereference in the model of `value_or`
Reviewed By: jvillard
Differential Revision: D24621016
fbshipit-source-id: c86d3c157
Summary:
Take another page from the Incorrectness Logic book and refrain from reporting issues on paths unless we know for sure that this path will be taken.
Previously, we would report on paths that are merely *not impossible*. This goes very far in the other direction, so it's possible we'll want to go back to some sort of middle ground. Or maybe not. See the changes in the tests to get a sense of what we're missing.
Reviewed By: ezgicicek
Differential Revision: D24014719
fbshipit-source-id: d451faf02
Summary: Structs captured both by reference or by value should have reference in their type. Struct captured by value should first call copy constructor. In this diff we fix the type of the captured variable to include reference. Copy constructor injection is left for the future.
Reviewed By: jvillard
Differential Revision: D23688713
fbshipit-source-id: d13748b5d
Summary: Variables captured without initialization do not have correct type inside lambda's body. This diff sets the correct type of captured reference variables inside procdesc and makes sure the translation of captured variables is correct. The translation of lambda's body will then take into account the type of captured var from procdesc.
Reviewed By: jvillard
Differential Revision: D23678371
fbshipit-source-id: ed16dc978
Summary: Add missing reference to the type of variable captured by reference without initialization.
Reviewed By: jvillard
Differential Revision: D23567685
fbshipit-source-id: b4e2ac0b6
Summary:
We were missing assignment to captured variables with initializers.
Consider the following example:
```
S* update_inside_lambda_capture_and_init(S* s) {
S* object = nullptr;
auto f = [& o = object](S* s) { o = s; };
f(s);
return object;
}
```
which was translated to
```
VARIABLE_DECLARED(o:S*&);
*&o:S*&=&object
*&f =(_fun...lambda..._operator(),([by ref]&o &o:S*&))
```
However, we want to capture `o` (which is an address of `object`), rather `&o` in closure.
After the diff
```
VARIABLE_DECLARED(o:S*&);
*&o:S*&=&object
n$7=*&o:S*&
*&f =(_fun...lambda..._operator(),([by ref]n$7 &o:S*&))
```
Reviewed By: jvillard
Differential Revision: D23567346
fbshipit-source-id: 20f77acc2
Summary: Added a model for copy constructor for `std::function`. In most cases, the SIL instruction `std::function::function(&dest, &src)` gives us pointers to `dest` and `src`, hence, we model the copy constructor as a shallow copy. However, in some cases, e.g. `std::function f = lambda_literal`, SIL instruction contains the closure itself `std::function::function(&dest, (operator(), captured_vars)`, hence, we need to make sure we copy the right value.
Reviewed By: ezgicicek
Differential Revision: D23396568
fbshipit-source-id: 0acb8f6bc
Summary: There was a mismatch between formals and actuals in `std::function::operator()` because we were not passing the first argument corresponding to the closure.
Reviewed By: ezgicicek
Differential Revision: D23372104
fbshipit-source-id: d0f9b27d6
Summary: When we evaluate lambdas in pulse, we create a closure object with `fake` fields to store captured variables. However, during the function call we were not linking the captured values from the closure object. We address this missing part here.
Reviewed By: jvillard
Differential Revision: D23316750
fbshipit-source-id: 14751aa58
Summary: Before we were modelling `vector.end()` as returning a fresh pointer every time is was called. It is common to check if an iterator is not the `end()` iterator and proceed to dereference the iterator in that case. In such code pattern `vector.end()` is called twice and returns different fresh values which causes false positives. To fix this, we add a special internal field `__infer_model_backing_array_pointer_to_last_element` to a vector to denote its end. Now, every time we call `vector.end()` we return the value of this field. We introduce a new attribute `EndOfCollection` to mark `end` iterator as the existing `EndIterator` invalidation is not suitable when we need to read the same value multiple times.
Reviewed By: jvillard
Differential Revision: D23101185
fbshipit-source-id: fa8a33b58
Summary:
This time it's personal.
Roll out pulse's own arithmetic domain to be fast and be able to add
precision as needed. Formulas are precise representations of the path
condition to allow for good inter-procedural precision. Reasoning on
these is somewhat ad-hoc (except for equalities, but even these aren't
quite properly saturated in general), so expect lots of holes.
Skipping dead code in the interest of readability as this (at least
temporarily) doesn't use pudge anymore. This may make a come-back as
pudge has/will have better precision: the proposed implementation of
`PulseFormula` is very cheap so can be used any time we could want to
prune paths (see following commits), but this comes at the price of some
precision. Calling into pudge at reporting time still sounds like a good
idea to reduce false positives due to infeasible paths.
#skipdeadcode
Reviewed By: skcho
Differential Revision: D22576004
fbshipit-source-id: c91793256
Summary: We model internal builtin `__new` function to return a non-null value. This fixes nullptr_dereference false positives where we explicitly check the result of a function call for nullptr when the function returns a newly created object.
Reviewed By: jvillard
Differential Revision: D22772217
fbshipit-source-id: 37d209697
Summary:
When applying function summaries, we are careful not to violate the
summary's assumptions about non-aliasing. For example, the summary we
generate for `foo(x,y) { *x = *y; }` will have `x` and `y` be allocated
to two different `AbstractValue.t` in the heap, representing
disjointness.
However, the current logic is too coarse and also rejects passing the
same pure value to functions that made no assumption about them being
equal or different, eg `goo(int x,int y) { int z = x + y; }`. This is
because the corresponding `AbstractValue.t` are different in the
callee's summary, but are represented by only one same value in callers
such as `goo(i,i)`.
This diff restricts the "don't violate aliasing" condition to only
consider heap-allocated values. This is consistent with separation logic
by the way: we use the implication `x|->- * y|->- |- x≠y`, which is
valid only when both `x` and `y` are both allocated in the heap as in
the left-hand-side of `|-`.
Reviewed By: skcho
Differential Revision: D22574297
fbshipit-source-id: 206a18499
Summary:
We need to check if `folly::Optional` is not `folly::none` if we want to retrieve the value, otherwise a runtime exception is thrown:
```
folly::Optional<int> foo{folly::none};
return foo.value(); // bad
```
```
folly::Optional<int> foo{folly::none};
if (foo) {
return foo.value(); // ok
}
```
This diff adds a new issue type that reports if we try to access `folly::Optional` value when it is known to be `folly::none`.
Reviewed By: ezgicicek
Differential Revision: D22053352
fbshipit-source-id: 32cb00a99
Summary: Currently we get false positive if we apply `operator--` to the `end()` iterator. To solve this, we model iterator `operator--` not to raise an error for the `EndIterator` invalidation, but to create a fresh element in the underlying array.
Reviewed By: ezgicicek
Differential Revision: D21476353
fbshipit-source-id: 5c722372e
Summary:
It is undefined behavior to dereference end iterator.
To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself.
Reviewed By: ezgicicek
Differential Revision: D21178441
fbshipit-source-id: fd6a94b0b
Summary:
List of things happening in this unreviewable diff:
- moved PulsePathCondition to PulseSledge
- renamed --pulse-path-conditions to --pudge
- PulsePathCondition now contains all the arithmetic of pulse
(inferbo+concrete intervals+pudge). In particular, moved arithmetic
attributes into PulsePathCondition.t. PulsePathCondition plays the
role of PulseArithmetic (combining all domains).
- added tests for a false positive involving free()
- PulseArithmetic is now just a thin wrapper around PulsePathCondition
to operate on states directly (instead of on path conditions).
- The rest is mostly moving code into PulsePathCondition (eg, from
PulseInterproc) and adjusting it.
Reviewed By: jberdine
Differential Revision: D21332073
fbshipit-source-id: 184c8e0a9
Summary:
We were invalidating "*(vec.__infer_backing_array)" instead of the
address of the field itself.
Reviewed By: ezgicicek
Differential Revision: D21280357
fbshipit-source-id: 48b984800
Summary: Iterator invalidation traces were based on vector rather than iterator itself.
Reviewed By: ezgicicek
Differential Revision: D21202047
fbshipit-source-id: 62ce8a488
Summary:
We ignored allocator models for vectors, and were not able to initialize vectors properly. This diff fixes this issue.
It also adds a test which was a FN before.
Reviewed By: skcho, jvillard
Differential Revision: D21089492
fbshipit-source-id: 6906cd1d1
Jules Villard
Sungkeun Cho
Gabriela Cunha Sampaio
Daiva Naudziuniene
Ezgi Çiçek