Summary:
Enabling starvation by default (D15158597) makes infer double report racerd
issues in these tests. The reason seems to be that both racerd and starvation
use `IssueLog` to record issues, so racerd records its issues there (using side
effects), then starvation adds its own (empty) set of issues and reports
whatever is there again. Since nothing cleans up the IssueLog in the middle,
racerd issues get reported twice: once as racerd issues and the other as
starvation issues.
Let's fix this later, for now just unbreak the test itself.
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D15277552
fbshipit-source-id: 3e7be8795
Summary: Previously there was no way of getting that list from the manual.
Reviewed By: jeremydubreil
Differential Revision: D15158598
fbshipit-source-id: 1705ed59d
Summary:
A more dynamic scheduling scheme will potentially run into the situation where no new work packets can be scheduled, but more work will be possible to schedule in the future, perhaps when some dependent work packet finishes being analysed.
The current implementation prevents that, as it expects that if a worker goes idle, it stays idle.
The changes here address this in two parts:
- the `select` call is always given a finite timeout. If given an infinite timeout, we will not be able to poll the task generator for more work, where none were previously possible.
- when the `select` call times out without updates, check if there is an idle child, and if so if the task generator has more work right now.
See also ProcessPool.mli for comments.
Reviewed By: mbouaziz
Differential Revision: D15197749
fbshipit-source-id: babe5da8e
Summary:
Before moving to any kind of non-trivial scheduling, we need to change the Tasks interface.
In particular, it's too restrictive to expect that the tasks to be scheduled are provided as a list before starting execution. For example, dynamic scheduling does not fit the bill here. Also, the list expectation means all scheduling work has to be done up front.
The solution here is to move to a `Sequence`-like interface with one difference:
- The function returning the next task expects a task option argument. That argument is the task that was just finished (if any) by the worker expecting new work. This will be useful for things like task dependencies (for instance, a procedure has been analysed, and can be marked so).
Reviewed By: mbouaziz
Differential Revision: D15181613
fbshipit-source-id: 21f3ba825
Summary:
Adds option `--summary-stats` to `infer report`.
The formatting is not perfect yet but it gives what I want.
Reviewed By: ngorogiannis
Differential Revision: D15064162
fbshipit-source-id: 56c4b4929
Summary: No reason to use custom function name and not implement `Hashable`.
Reviewed By: mbouaziz
Differential Revision: D15097603
fbshipit-source-id: 7303fc15e
Summary: Remove from inferbo summary locations that are unreachable from callers
Reviewed By: ezgicicek
Differential Revision: D15064518
fbshipit-source-id: 734e79b4a
Summary: Using `Fields.to_list` also makes sure we don't forget fields.
Reviewed By: ezgicicek
Differential Revision: D15062353
fbshipit-source-id: aaac9be99
Summary:
TOPL properties are essentially automata, which will be modeled as a set
of procedures. The code-to-analyze makes calls into these procedures,
thereby driving the automaton. In this commit, these calls do not do
anything. The point is to prepare the hook-up mechanism.
Reviewed By: jvillard
Differential Revision: D14819650
fbshipit-source-id: d95ecdb3d
Summary: The name was misleading, the function only forget locs for relations.
Reviewed By: ezgicicek
Differential Revision: D15045933
fbshipit-source-id: 7f41a55e7
Summary:
- `--source-files` was missing.
- The three modes are actually independent, make it clearer and group options by mode.
- Fail if `--procedures` and `--source-files` are used together.
Reviewed By: jeremydubreil
Differential Revision: D15049822
fbshipit-source-id: cc515cb56
Summary:
Replace `$(u,...)` with `$(i,...)` since `$(u,...)` doesn't exist.
Cmdliner was emitting a warning at runtime:
cmdliner error: Unknown cmdliner markup $(u,...) in "Specify classes where the destructor should be ignored when computing liveness. In other words, assignement to variables of these types (or common wrappers around these types such as $(u,unique_ptr<type>)) will count as dead stores when the variables are not read explicitly by the program. (default: $(i,[]))"
Reviewed By: mbouaziz
Differential Revision: D15045004
fbshipit-source-id: e03ece4f7
Summary:
A long-standing easter egg from infer error messages is the "object
`null` could be null and is dereferenced at line ...". I tried to fix
this but the part that generates the first "null" in the message and the
part that generates the second one are very far apart and it's hard to
see how to make the second part aware of the first in a clean way.
Instead, hack around it by detecting if the string representing the
value is literally `null` and in that case chop `could be null ` from
the error messages...
Reviewed By: jeremydubreil
Differential Revision: D14972324
fbshipit-source-id: ccc48ce6b
Summary:
We get messages like " object returned by `getArguments()` at line 101."
instead of " object returned by `getArguments()` could be null and is
dereferenced at line 101.". Tracking it down, it happens for
nullable-looking values, but I don't know why.
It seems that something regressed but I couldn't track it down.
So, just generate the error message in the same way as for non-nullable
objects in this case to fix the non-sensical message.
Reviewed By: jeremydubreil
Differential Revision: D14972325
fbshipit-source-id: 2a97501cc
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 is useful for the model of `exit` that returns 0 disjuncts. All
other models return 1 disjunct for now, but in the future things like
`malloc()` will need to return 2 possible states for instance.
Reviewed By: ngorogiannis
Differential Revision: D14753491
fbshipit-source-id: 3e7387d6d
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 is ~2.5x wall clock faster, ~5x user time faster, and finds 98% of
the bugs. Not very scientific yet but seems better than the previous
non-scientific arbitrary default.
Reviewed By: ngorogiannis
Differential Revision: D14753494
fbshipit-source-id: b72cdd613
Summary:
Useful to know which disjunct is being executed. Reprinting them
wholesale is too spammy so compromise by outputting just enough to be
able to reconstruct the info "which disjunct was executed and which new
disjuncts were produced?".
Reviewed By: ngorogiannis
Differential Revision: D14753495
fbshipit-source-id: f5aa68160
Summary:
This isn't needed now that this information is recorded in
`PulseTrace.action` instead.
Reviewed By: mbouaziz
Differential Revision: D14645089
fbshipit-source-id: 9c3f38722
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:
This provides a way for AI checkers to read the formals of a procedure,
or other things related to its `Procdesc.t`.
Reviewed By: mbouaziz
Differential Revision: D14258483
fbshipit-source-id: a28e28d3c
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
Summary:
This is in preparation of interprocedural pulse. The abstract addresses
generator keeps a reference to create fresh addresses, but that's a
piece of global state that needs to persist across ondemand analyses.
Reviewed By: jberdine
Differential Revision: D14324760
fbshipit-source-id: 5cdb1d3f5
Summary:
Increases precision a bit. I didn't observe speed problems on what I tested. (But, who knows?)
Closes https://github.com/facebook/infer/pull/799
Reviewed By: jvillard
Differential Revision: D6284206
Pulled By: rgrig
fbshipit-source-id: 6f1e8631f
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:
Several tools that use ocamlformat look for the "project root" in
order to find the config for a given file to format. The project root
is inferred by looking in ancestor directories of the input file until
one of .git, .hg, or dune-project is found. Since the .ocamlformat
config file is currently two directories higher than dune-project,
this fails. This diff moves the config file.
Reviewed By: jvillard
Differential Revision: D14694260
fbshipit-source-id: 2fb51bf30
Summary:
This diff propagates LatestPrune on function calls.
Depends on D14321605
Reviewed By: mbouaziz
Differential Revision: D14321618
fbshipit-source-id: cb2e1b547
Summary:
Given a pointer-typed parameter, Inferbo assumes that it is an array
block. However, when a pointer is given as an actual parameter, it
failed the substitution of the array block value of the parameter, thus
which made some return values to bottom unexpectedly.
This diff revises the substitution of array block, so it can
substitute array block values with actual pointers correctly when it
is possible.
Reviewed By: mbouaziz
Differential Revision: D14663475
fbshipit-source-id: 0477de1ba
Summary:
It does more reachability checks on prunings. Before the diff, it checked the reachability only by the condition expression of prune commands, but now also uses PrunePairs.
Depends on D14321575
Reviewed By: mbouaziz
Differential Revision: D14321605
fbshipit-source-id: f630de842
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: It's all grown up now and taking quite some space in src/checkers/.
Reviewed By: skcho
Differential Revision: D14568273
fbshipit-source-id: b843c031e
Summary:
Open fewer sessions by wrapping AI operations together in the same HTML
node session. This allows us to also print more stuff, such as whether
the current loop computation has converged.
Reviewed By: skcho
Differential Revision: D14568274
fbshipit-source-id: d47110cf4
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: This diff substitutes symbolic values for unknown functions in proof obligations to top. The goal of the diff is to avoid generating too many number of proof obligations that cannot be concretized.
Reviewed By: ezgicicek
Differential Revision: D14537542
fbshipit-source-id: 7f8f3bb4b
Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
Summary:
Add support for GuardedBy: we deviate from the spec as follows:
- No warnings issued for any access within a private method, unless that method is called from a public method and the lock isn't held when the access occurs.
- Warnings are suppressed with the general RacerD mechanism, ie `ThreadSafe(enableChecks=false)`
- GuardedBy warnings override thread-safety violation warnings on the same access, because GuardedBy has a clearer and simpler contract.
Also, some simplifications, cleanups and perf improvements (eg avoid unreportable procs at the top level as opposed to on each of their accesses).
Reviewed By: jeremydubreil
Differential Revision: D14506161
fbshipit-source-id: b7d794051
Summary:
While adding a footprint frame during rearrangement, the footprint
variables should be fresh with respect to the current state too, not
only with respect to he footprint, because the frame is added to the
state.
Reviewed By: jberdine
Differential Revision: D14401026
fbshipit-source-id: 20ea4485a
Summary:
Context: "quandary" traces optimise for space by only storing a call site (plus analysis element) in a summary, as opposed to a list of call sites plus the element (i.e., a trace). When forming a report, the trace is expanded to a full one by reading the summary of the called function, and then matching up the current element with one from the summary, iterating until the trace cannot be expanded any more. In the best case, this can give a quadratic saving, as a real trace gets longer the higher one goes in the call stack, and therefore the total cost of saving that trace in each summary is quadratic in the length of the trace. Quandary traces give a linear cost.
HOWEVER, these have been a source of many subtle bugs.
1. The trace expansion strategy is very arbitrary and cannot distinguish between expanded traces that are invalid (i.e., end with a call and not an originating point, such as a field access in RacerD). Plus the strategy does not explore all expansions, just the left-most one, meaning the left most may be invalid in the above sense, but another (not left-most) isn't even though it's not discovered by the expansion. This is fixable with major surgery.
2. All real traces that lead to the same endpoint are conflated -- this is to save space because there may be exponentially many such traces. That's OK, but these traces may have different locking contexts -- one may take the lock along the way, and another may not. The expansion cannot make sure that if we are reporting a trace we have recorded as taking the lock, will actually do so. This has resulted in very confusing race reports that are superficially false positives (even though they point to the existence of a real race).
3. Expansion completely breaks down in the java/buck integration when the trace goes through f -> g -> h and f,g,h are all in distinct buck targets F,G,H and F does not depend directly on H. In that case, the summary of h is simply not available when reporting/expanding in f, so the expanded trace comes out as truncated and invalid. These are filtered out, but the filtering is buggy and kills real races too.
This diff completely replaces quandary traces in RacerD with plain explicit traces.
- This will incur the quadratic space/time cost previously saved. See test plan: there is indeed a 30% increase in summary size, but there is no slowdown. In fact, on openssl there is a 10-20% perf increase.
- For each endpoint, up to a single trace is used, as before, so no exponential explosion. However, because there is no such thing as expansion, we cannot get it wrong and change the locking context of a trace.
- This diff is emulating the previous reporting format as much as possible to allow good signal from the CI. Further diffs up this stack will remove quandary-trace specific things, and simplify further the code.
- 2 is not fully addressed -- it will require pushing the `AccessSnapshot` structure inside `TraceElem`. Further diffs.
Reviewed By: jberdine
Differential Revision: D14405600
fbshipit-source-id: d239117aa
Summary:
This diff changes a LatestPrune to use a return variable instead of another local variable, when the function returns a conditional value. This is a preparation to propagate LatestPrune inter-procedurally in the following diffs.
context: If a function returns a conditional value, e.g. `return x == y`, the LatestPrune value includes a temporary local variable introduced by the SIL translation. This diff is to avoid propagating the temporary local variables to its caller.
Reviewed By: mbouaziz
Differential Revision: D14321534
fbshipit-source-id: d157bfdd0
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
Jules Villard
Nikos Gorogiannis
Dino Distefano
Jeremy Dubreil
Ezgi Çiçek
Mehdi Bouaziz
David Lively
Radu Grigore
Lee Howes
Daniel Mercier
Mitya Lyubarskiy
Martin Trojer
Radu Grigore
Katie Ots
Josh Berdine
Sungkeun Cho
Wenzhe Lu