Summary: Pulse doesn't care about exceptions yet. With Exceptional CFG, java analysis takes a lot of time due to having many disjuncts. Let's use Normal CFG for now.
Reviewed By: jvillard
Differential Revision: D19194479
fbshipit-source-id: f94bb6078
Summary:
In order to improve the impurity analysis, this diff adds models for
- `hasNext()` and - `Object.equals()` modeled as returning a non-deterministic value (havoc_id)
- `next()` modeled as `StdVector.get` with a fresh index
- `iterator` modeled as just returning the underlying list
Reviewed By: jvillard
Differential Revision: D19177392
fbshipit-source-id: 0babb037a
Summary:
Remove Clang and Java submodules of Typ.Fieldname. They are unnecessary and they reflect a fake dichotomy: there is only one fieldname type. To distinguish between fields of Java classes and other C constructs, there is a helper function provided, but the idea is simple: obtain the class type the field belongs to, and check if it's a Java class.
This diff still preserves behaviour, but removes as many functions as possible from the interface, to leave a small surface.
Reviewed By: mityal
Differential Revision: D18962423
fbshipit-source-id: ffe6933ee
Summary:
That class does some complicated accounting of memory that depends on
whether the string is "small", "medium" or "large". In the latter case
it does its own ref-counting and copy-on-write to save memory, and that
trips up pulse. Pretending all strings are small avoids that issue.
Reviewed By: skcho
Differential Revision: D18909030
fbshipit-source-id: 1c14d909b
Summary:
Including the current call state is useful because the contradiction
sometimes refers to abstract values that have been materialised since
the last call state so we cannot make sense of them unless we print the
current call state.
Reviewed By: skcho
Differential Revision: D18908424
fbshipit-source-id: 297f397a6
Summary:
- Do most of the work of `solve_arithmetic_constraints` inside `subst_attribute` instead, since we need to re-use the latter function for post-conditions where the first function is not appropriate.
- When substituting arithmetic constraints, we refine arithmetic information (both concrete intervals and inferbo), which can lead to inconsistent states. Instead of recording the new arithmetic facts by returning a new current state, just act as a map on attributes. This is to enable doing the point above.
- All this lead to a somewhat messy refactoring...
- Rename `CannotApplyPre` to `Contradiction` since it's used for post-conditions as well now
Reviewed By: skcho
Differential Revision: D18889120
fbshipit-source-id: d81647143
Summary:
After passing a `PRUNE` instruction we can refine the current inferbo
intervals for the values involved.
Reviewed By: ezgicicek
Differential Revision: D18889103
fbshipit-source-id: b521046aa
Summary:
Every time we add an arithmetic information, add the corresponding
inferbo one.
Reviewed By: skcho
Differential Revision: D18888863
fbshipit-source-id: ab4afd372
Summary:
Finally use information from the inferbo intervals in pulse's domain to
make decisions about whether conditionals are feasible or not.
Reviewed By: skcho
Differential Revision: D18811193
fbshipit-source-id: d80a28657
Summary:
Refine the type of inferbo intervals attributes to "pure" (non-bottom)
ones. This is because were we to get a Bottom value from inferbo we
should stop the abstract execution instead of recording it in the state.
Reviewed By: ezgicicek
Differential Revision: D18811165
fbshipit-source-id: fff8664b7
Summary:
Similarly to binops, let inferbo evaluate unary operations and record
the results.
Reviewed By: ezgicicek
Differential Revision: D18811146
fbshipit-source-id: 8f9e16bbd
Summary:
This diff enables parsing and auto-formatting documentation
comments (aka docstrings).
I have looked at this entire diff and manually made some changes to
improve the formatting. In some cases it looked like it would take too
much time, or benefit from someone more familiar with the code doing
it, and I instead disabled auto-formatting docstrings in those files.
Also, there are some source files where the docstrings are invalid,
and some where the structure detected by the parser appears not to
match what was intended. Auto-formatting has been disabled for these
files.
Reviewed By: ezgicicek
Differential Revision: D18755888
fbshipit-source-id: 68d72465d
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 gets rid of false positives when something invalid (eg null) is
passed by reference to an initialisation function. Havoc'ing what the
contents of the pointer to results in being optimistic about said
contents in the future.
Also surprisingly gets rid of some FNs (which means it can also
introduce FPs) in the `std::atomic` tests because a path condition
becomes feasible with havoc'ing.
There's a slight refinement possible where we don't havoc pointers to
const but that's more involved and left as future work.
Reviewed By: skcho
Differential Revision: D18726203
fbshipit-source-id: 264b5daeb
Summary:
It's a well-known fact that pulse should know too. To avoid splitting
the abstract state systematically, only act if we know the pointer is
exactly 0 to avoid reporting a nullptr dereference on `free(x)`.
Reviewed By: ezgicicek
Differential Revision: D18708575
fbshipit-source-id: 1cc3f6908
Summary:
Turns out code uses atomics in important places, modelling it removes
FPs.
The tests are copied from biabduction and adapted and extended a bit. I
didn't implement compare_exchange primitives for now (plus, giving them
a sequential semantics like in biabduction is probably a bit cheeky).
Reviewed By: skcho
Differential Revision: D18708576
fbshipit-source-id: a3581b8a4
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: Rather than repeatedly matching actuals, let's use `ProcnameDispatcher.ModeledCall` to pick up the actual arguments with their corresponding values. This simplifies the models.
Reviewed By: jvillard
Differential Revision: D18685855
fbshipit-source-id: 7788bd8bb
Summary:
This was never set to true except in a wrong way in the Java frontend
(see previous diff).
Reviewed By: dulmarod
Differential Revision: D18573927
fbshipit-source-id: 4c9d1a855
Summary:
Note: Disabled by default.
Having some support for values, we can report when a null or constant
value is being dereferenced. The particularity here is that we don't
report when 0 is a possible value for the address, or even if we know
that the value of the address can only be 0 in that branch! Instead, we
allow ourselves to report only when we the address has been *set* to
NULL (or any constant).
This is in line with how pulse deals with other issues: only report when
1. we see an address become invalid, and
2. we see the same address be used later on
Reviewed By: skcho
Differential Revision: D17665468
fbshipit-source-id: f1ccf94cf
Summary:
This was causing loads of false positives later in the stack.
Invalidating the address of the object seems to be enough here as it
doesn't break any tests.
Reviewed By: ezgicicek
Differential Revision: D18246090
fbshipit-source-id: 2ef9a6a5c
Summary:
We consider Java collections to be like c++ std::vectors and add models for
- `Collections.get(..)`
- `__cast`
Reviewed By: skcho
Differential Revision: D18449607
fbshipit-source-id: 448206c84
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: This will be more useful later when adding another one.
Reviewed By: ezgicicek, jberdine
Differential Revision: D18115231
fbshipit-source-id: a0a01901a
Summary:
The business of translating `Top/True/False` to `true/false` can be
hidden more.
Reviewed By: skcho
Differential Revision: D18115228
fbshipit-source-id: 071fcbddf
Summary:
Warning 33 (unused open) is enabled but the module open is not really
unused, it's just also opened at the top of the file...
Reviewed By: skcho
Differential Revision: D18114385
fbshipit-source-id: 2a8f9512a
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:
The name had rotten: it should be `AddrHistPair`. There is little value
of exposing the type of the pair `AbstractValue.t * ValueHistory.t`,
just inline its definition everywhere.
Reviewed By: ezgicicek
Differential Revision: D17955283
fbshipit-source-id: d145251e0
Ezgi Çiçek
Nikos Gorogiannis
Sungkeun Cho
Jules Villard
Josh Berdine