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: Use_after_free was used both for biabduction and pulse, and the biabduction version is blacklisted by default. As a result, the Pulse version was also disabled unintentionally. This changes the name of the old use_after_free so that now we can get use_after_free bugs whenever pulse is enabled.
Reviewed By: skcho
Differential Revision: D17182687
fbshipit-source-id: 539ca69de
Summary: With this predicate we are able to check for static global variables in AL.
Reviewed By: ddino
Differential Revision: D17164848
fbshipit-source-id: a3d10598c
Summary:
This diff uses the models of vector for modelling string in Cpp.
Depends on D16963153
Reviewed By: ezgicicek
Differential Revision: D16963166
fbshipit-source-id: 5effe2d72
Summary:
This is more powerful than `"symbols"` for more advanced use-cases. Keep
`"symbols"` unchanged to make migrating easier.
Differential Revision: D16985756
fbshipit-source-id: dfbb09393
Summary: Adding new predicate for checking whether a variable is defined as extern. May be useful in AL rules.
Reviewed By: jvillard
Differential Revision: D16961690
fbshipit-source-id: 0677077dc
Summary:
Use whatever information we can to decide whether to use C or Java
syntax when outputting an access expression, now that we store them as
such.
Also, make cluster callbacks explicitly set the language, as this was not done before and led to some confusion (Clang being set when analysing a Java file).
Reviewed By: skcho
Differential Revision: D16884160
fbshipit-source-id: 40adf9f35
Summary:
Change the logic of the annotation reachability checker in the following
ways:
1. Sanitizers take priority over sinks, i.e. a procedure that is both a
sink and a sanitizer is not a sink. This changes the existing tests
that seemed to assume the opposite. However I think that way is more
useful and goes better with the fact that sanitizers are specified as
"overrides".
2. When applying a summary, check again that we are not in a sanitizer
for the corresponding sink.
Without (2) this there was a subtle bug when several rules were
specified. For example, if `sink_wrapper()` wraps `sink()` for a rule
`R` then the summary of `sink_wrapper()` will be: `R-sink : call to sink()`.
Then, suppose `sanitizer()` calls `sink_wrapper()` and `sanitizer()` is
a sanitizer for `R` but not for another rule `R'`. The previous code
would add the call to `sink()` to the summary of `sanitizer()` because
it's not a sanitizer for `R'`, even though `sink()` is not a sink for
`R'`!
The current code will re-apply the rules correctly so that sinks are
matched only against the right sanitizers.
Reviewed By: skcho
Differential Revision: D16895577
fbshipit-source-id: 266cc4940
Summary:
- run the tests! they weren't hooked up to the main Makefile :/
- add some html debug messages
- formatting
Reviewed By: skcho
Differential Revision: D16895578
fbshipit-source-id: e96d737cc
Summary:
It adds a vector model of `data` method.
Depends on D16687280
Reviewed By: ezgicicek
Differential Revision: D16689400
fbshipit-source-id: 156016b3c
Summary:
It adds a model of vector::push_back
Depends on D16687225
Reviewed By: ezgicicek
Differential Revision: D16687269
fbshipit-source-id: 9d2a73fca
Summary:
It enables pruning of vector's size when the return value of the function call of `vector::size` is pruned.
Depends on D16687167
Reviewed By: ezgicicek
Differential Revision: D16687225
fbshipit-source-id: 793a21b3a
Summary:
It generates vector value ondemand when it is given as a parameter.
Depends on D16645589
Reviewed By: ezgicicek
Differential Revision: D16645624
fbshipit-source-id: 7498c8ab2
Summary:
These have proved to be too fragile to maintain as they would often break
compilation of user code. They have been off by default for more than a year
now (D7350715).
Removing the include models shows a more accurate picture of what infer results
look like in production. As such, lots of tests have changed, mostly
biabduction but also in inferbo. SIOF was using include-based models too but
now libc++ is better and iostreams are implemented in a way that SIOF
understands (instead of being magical creatures) so nothing changed there.
Reviewed By: skcho
Differential Revision: D16602171
fbshipit-source-id: ce38f045b
Summary:
This diff prevents that the latest prune value is overwritten as top
from callees.
Reviewed By: jvillard
Differential Revision: D16540391
fbshipit-source-id: bdd5b42ed
Summary:
This diff improves the precision of the mod operator.
For example, result of x % c (when x>=0 and c>0) is
(before) [0, c-1]
(after) [0, min(c-1,x)]
Reviewed By: ezgicicek
Differential Revision: D16518578
fbshipit-source-id: a68660ee7
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:
It downgrades issues of void pointer to L5, because of its impreciseness. This is not
ideal but Inferbo cannot analyze arrays pointed by void pointers precisely at the moment.
Reviewed By: jvillard
Differential Revision: D16379911
fbshipit-source-id: f2c016aba
Summary:
A common gotcha is the new test. Model the minimum amount of
`std::basic_string` to catch it.
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D16121090
fbshipit-source-id: 66f06cb43
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:
Replaced by pulse. `--ownership` is now a deprecated form of `--pulse`.
The ownership checker is starting to give wrong answers due to changes in the
clang frontend, so it's better to remove it in favour of pulse.
there_goes_my_hero
Reviewed By: ngorogiannis
Differential Revision: D16107650
fbshipit-source-id: bb2446a19
Summary:
So it turns out we need to translate even more cases. Pulse had a FP
before that this fixes.
Reviewed By: ezgicicek
Differential Revision: D16073629
fbshipit-source-id: c03460b5a
Summary:
This is needed to test some functionality in the next diff. Only one
test changes (no longer a FN), which is now documented. Also, stop
including the "header models" meant for biabduction!
Maybe one day we'll need to have several test modes for different C++
versions. Seems overkill for now, so let's wait until we see some actual
issues (eg FPs) that manifest in one version but not the other.
Reviewed By: mbouaziz
Differential Revision: D16073630
fbshipit-source-id: 1cfdfc933
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:
The previous code would call the destructor for the C++ temporary
*before* the prune nodes, which then try to dereference it. Wrong.
Quick fix: don't destroy temporaries in conditionals.
Reviewed By: mbouaziz
Differential Revision: D16030735
fbshipit-source-id: e11abad58
Summary:
We were skipping some instructions before and that was a problem for
pulse. See added pulse test.
Reviewed By: mbouaziz
Differential Revision: D16030150
fbshipit-source-id: 9c62e6213
Summary: Not sure if anyone uses this but there, now it's modelled.
Reviewed By: mbouaziz
Differential Revision: D16008162
fbshipit-source-id: f4795dcba
Summary:
Prevent false positives about variables captured by value gone out of
scope.
Reviewed By: ezgicicek
Differential Revision: D16008165
fbshipit-source-id: d70e47db4
Summary: We know how to do interprocedural calls so let's use that!
Reviewed By: mbouaziz
Differential Revision: D16008164
fbshipit-source-id: 4c34bf704
Summary:
`function::operator=` is called whenever we assign a literal lambda to a
variable, so it's pretty useful to be able to report anything on
lambdas.
Reviewed By: mbouaziz
Differential Revision: D16008163
fbshipit-source-id: a9d07668d
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: Inject destructor calls to destroy a temporary when its lifetime ends.
Reviewed By: mbouaziz
Differential Revision: D15674209
fbshipit-source-id: 0f783a906
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:
It turns out HIL gets in the way of a precise heap analysis. For
instance, instead of:
```
n$0 = *&x.f
_ = delete(&x)
*&y = n$0
```
HIL tries hard to forget about intermediate variables and shows instead
```
_ = delete(&x)
*&y = *&x.f
```
Oops, that's a use-after-delete, whereas the original code was safe.
While it's easy to write SIL programs that are completely unsound for
HIL, they are not generated very often from the frontends. In fact, the
problem became apparent only when making the clang frontend translate
C++ temporaries destructors, which produces the situation above
routinely.
This diff makes the minimal amount of change to make Pulse build and
produce equivalent results (minus HIL bugs) starting from SIL instead of
HIL. The reporting sucks for now because we need to translate SIL
temporaries back into program access paths. This is done in the next
diff.
Reviewed By: mbouaziz
Differential Revision: D15824961
fbshipit-source-id: 8e4e2a3ed
Summary:
This one isn't caught because we don't destruct temporaries that are
bound to a const reference. According to the C++ standard these should
get destroyed when the const reference gets destroyed but instead we
just don't destroy them for now.
Reviewed By: mbouaziz
Differential Revision: D15760209
fbshipit-source-id: 32c935ec0
Summary:
In a next diff temporaries will get destructed at the end of their
lifetimes and that naive model would be causing false positives.
The flipside is that we lose all reports on closures for now, will need
to model them separately later.
Reviewed By: mbouaziz
Differential Revision: D15695943
fbshipit-source-id: c2c482c02
Summary:
This started as an attempt to understand how to modify the frontend to
inject destructors for C++ temporaries (see next diffs).
This diff rewrites the existing logic for computing the list of
variables that should be destroyed at the end of each statement, either
because it's the end of their syntactic scope or because control flow
branches outside of their syntactic scope.
The frontend translates a function from the last instructions to the
first, but scope computation needs to be done in the other direction, so
it's done in a separate pass *before* the main translation happens. That
first pass creates a map from statements in the AST to the list of
variables that should be destroyed at the end of these statements. This
is still the case now.
Before, that map would be computed in a bit of a weird way: scopes are
naturally a stack but instead of that the structure maintained was a
flat list + a counter to know where the current scope ended in that
list.
In this diff, redo the computation maintaining a stack of scopes
instead, which is a bit cleaner. Also treat more instructions as
introducing a new scope, eg if, for, ...
Reviewed By: mbouaziz
Differential Revision: D15674208
fbshipit-source-id: c92429e82
Summary:
Somewhat trivial: add a string to "Destruction" nodes to indicate why
they were created. Rename the main `instruction_aux` function into
`instruction_translate` (see next diff for why).
Reviewed By: mbouaziz
Differential Revision: D15674211
fbshipit-source-id: 8a7eda72c
Summary:
I rewrote the test so it doesn't need any C++ headers so that:
- it's easier to see what's going on
- it's easier to debug: the whole AST is now somewhat readable vs before
the headers made it impossibly long
Reviewed By: ezgicicek
Differential Revision: D15674213
fbshipit-source-id: d98941983
Summary:
The synthetic methods from `topl.Property` are now nonempty: they
simulate a nondeterministic automaton.
Reviewed By: jvillard
Differential Revision: D15668471
fbshipit-source-id: 050408283
Summary:
- take advantage more structured attributes in the exported AST
- circumvent new format of `if` and `switch`
- a few new features/nodes but nothing major there
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz, martintrojer
Differential Revision: D15453572
fbshipit-source-id: c0c24345f
Summary:
This messes with the deduplication heuristic when templated function
names show up in the error messages, since the heuristic demands that
the error messages are the same.
Reviewed By: mbouaziz
Differential Revision: D15374333
fbshipit-source-id: 70232d254
Summary:
Improve the error messages, change is more or less documented in the
code.
Reviewed By: mbouaziz
Differential Revision: D15374334
fbshipit-source-id: f1dd54180
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:
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:
Similarly to function parameters (and the return value), we need to
apply the pre/post of a function call to the globals mentioned in its
summary.
- tigthen summaries further to remember only abducible variables in the
post (as well as in the pre)
- take globals into account when applying pre/post pairs
Reviewed By: jberdine
Differential Revision: D14780800
fbshipit-source-id: fc0d180bb
Summary:
The heuristic to detect variables going out of scope was to detect any
access expression passed as argument to an injected destructor call.
However destructor calls are also injected in destructor bodies to
destruct each field of an object, so the heuristic would detect fields
going out of scope, which, erm, doesn't make sense. Limit the heuristic
to local program variables.
Reviewed By: jberdine
Differential Revision: D14771454
fbshipit-source-id: ffa3c9fe3
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:
The previous message formatting had regressed and produced non-sensical messages.
More importantly, remove template parameters from error messages to
trigger the heuristic in `InferPrint` that deduplicates errors that are
on the same line with the same error type and message. Without this we
get hundreds of reports that correspond to as many instantiations of the
same code.
Reviewed By: ngorogiannis
Differential Revision: D14747979
fbshipit-source-id: 3c4aad2b1
Summary:
We see the magic function `__variable_initialization` at the point where
the variable is declared, eg `int x = foo()`. It's safe to reset `&x` at
that point. This circumvents an issue that pops up in some rare cases
where the ternary conditional operator `?:` and variable initialization
conspire to produce weird frontend results.
Some test becomes a FN again, but I think it was being reported for the
wrong reasons; will investigate more later.
Reviewed By: ngorogiannis
Differential Revision: D14747980
fbshipit-source-id: e75d6e30f
Summary:
This ensures that each attribute type can only be present once per
address. Makes ~80x time improvement on pathological cases such as
Duff's device.
This introduces a new kind of Set in `PrettyPrintable`.
Reviewed By: mbouaziz
Differential Revision: D14645091
fbshipit-source-id: c7f9b760c
Summary:
Detect when a variable goes out of scope. When that's the case, mark its
address *and* its contents as invalid.
Give subsequent uses a USE_AFTER_LIFETIME error type instead of
USE_AFTER_DESTRUCTOR.
Reviewed By: jberdine
Differential Revision: D14387147
fbshipit-source-id: a2c530fda
Summary:
Instead of emitting an ad-hoc builtin on variable declaration emit a new
metadata instruction. This allows us to remove the code matching on that
ad-hoc builtin that had to be inserted in several checkers.
Inferbo & pulse used that information meaningfully and had to undergo
some minor changes to cope with the new metada instruction.
Reviewed By: ezgicicek
Differential Revision: D14833100
fbshipit-source-id: 9b3009d22
Summary:
Bundle all non-semantic-bearing instructions into a `Metadata _`
instruction in SIL.
- On a documentation level this makes clearer the distinction between
instructions that encode the semantics of the program and those that are
just hints for the various backend analysis.
- This makes it easier to add more of these auxiliary instructions in
the future. For example, the next diff introduces a new `Skip` auxiliary
instruction to replace the hacky `ExitScope([], Location.dummy)`.
- It also makes it easier to surface all current and future such
auxiliary instructions to HIL as the datatype for these syntactic hints
can be shared between SIL and HIL. This diff brings `Nullify` and
`Abstract` to HIL for free.
Reviewed By: ngorogiannis
Differential Revision: D14827674
fbshipit-source-id: f68fe2110
Summary:
This diff accumulates LatestPrune in sequential prunings. It should be sound since Inferbo invalidates some data of LatestPrune if they are updated.
Depends on D14321534
Reviewed By: mbouaziz
Differential Revision: D14321575
fbshipit-source-id: 233dbae32
Summary:
Some of these tests were wrong, eg `~lambda()` calls `lambda()` then...
takes the bitwise complement or something? The intent was to call the
destructor.
Add interprocedural tests for later.
Reviewed By: jberdine
Differential Revision: D14324762
fbshipit-source-id: 40d2c32f5
Summary:
Previously we would say that `lhs <= rhs` (or `lhs |- rhs`) when a
mapping existed between the abstract addresses of `lhs` and `rhs` such
that `mapping(lhs)` was a supergraph of `rhs`. In particular,
we had that `x |-> x' * x' |-> x'' |- x |-> x'`. This is not entirely
great, in particular once we get pairs of state representing footprint +
current state. I'm not sure I have an extremely compelling argument why
though, except that it's not the usual way we do implication in SL, but
there wasn't a compelling argument for the previous state of affairs
either.
This changes `|-` to be true only when `mapping(lhs) = rhs` (modulo only
considering the addresses reachable from the stack variables).
Reviewed By: jberdine
Differential Revision: D14568272
fbshipit-source-id: 1bb83950e
Summary: This helps convergence when `<=` is based on physical equality for example, and widening is implemented as `widen ~prev ~next = join prev next`.
Reviewed By: skcho
Differential Revision: D14568270
fbshipit-source-id: ded5ed296
Summary:
Re-declarations of global variables sometimes hide constant
initializations in the original declaration, which caused FN before.
In this diff, it translates global variables to point to original
declarations, rather than following re-declarations, if possible.
Reviewed By: mbouaziz, jvillard
Differential Revision: D14596301
fbshipit-source-id: 55c3b5f95
Summary: In SIL, sometimes a return value is assigned to `__return_param`.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D14538590
fbshipit-source-id: dfbb74dc2
Summary:
To meet the pure parts of formulas, the process was to (a) call Rename.extend
with variables occuring in similar places and (b) extract substitutions out of
those. Two matching primed vars would both be replaced by some fresh primed var.
However, equivalence classes of primed variables would *not* be replaced by
one fresh (primed) variable. Now, that should work.
Reviewed By: mbouaziz
Differential Revision: D14150192
fbshipit-source-id: 90ca9216c
Summary:
This will be used in the future to determine what to do with destructors
in pulse.
Reviewed By: mbouaziz
Differential Revision: D14324759
fbshipit-source-id: bc3c34471
Summary:
When joining two lists of disjuncts we try to ensure there isn't a state
that under-approximates another already in the list. This helps reduce
the number of disjuncts that are generated by conditionals and loops.
Before we would always just add more disjuncts unless they were
physically equal but now we do a subgraph computation to assess
under-approximation.
We only do this half-heartedly for now however, only taking into
consideration the "new" disjuncts vs the "old" ones. It probably makes
sense to do a full quadratic search to minimise the number of disjuncts
from time to time but this isn't done here.
Reviewed By: mbouaziz
Differential Revision: D14258482
fbshipit-source-id: c2dad4889
Ezgi Çiçek
Dulma Churchill
Sungkeun Cho
Jules Villard
Nikos Gorogiannis
Josh Berdine
Radu Grigore
Peter O'Hearn
Jeremy Dubreil
David Lively
Lee Howes