Summary:
`Initializer` is used (mostly by Nullsafe) to signal that a method will only be run from/as a constructor, even if public.
RacerD should recognise this annotation; this diff makes RacerD treat methods annotated as `Initializer` like constructors with regards to the ownership of the receiver object.
Reviewed By: skcho
Differential Revision: D28748068
fbshipit-source-id: 5dd060865
Summary: Sometimes the type definition is missing, especially in not-well supported build systems. When missing, default to true if on Java since you'd have to explicitly select a non-recursive one on purpose, and vice versa for clang.
Reviewed By: jvillard
Differential Revision: D28745172
fbshipit-source-id: 8b0e26e1a
Summary: Litho (https://fblitho.com/) does some operations in the background. Add RacerD messaging specific to Litho.
Reviewed By: ezgicicek
Differential Revision: D28675504
fbshipit-source-id: e76f9f538
Summary:
Each Erlang function now has a Procdesc in `results.db`. The
ProcAttributes record if a function is exported or not by using the
access Public or Private, respectively.
This adds also `ErlangTypeName`. We use a fixed set of "type names" for
the different types of values in Erlang (i.e., for Erlang's "dynamic types").
Reviewed By: jvillard
Differential Revision: D28385954
fbshipit-source-id: f8278505a
Summary:
This PR adds race condition detection support on CIL backed languages, such as .NET platform languages.
We will add unit tests later since we are still fine tunning Infer# translation module.
Pull Request resolved: https://github.com/facebook/infer/pull/1443
Reviewed By: jvillard
Differential Revision: D28505195
Pulled By: ngorogiannis
fbshipit-source-id: f263f6ba6
Summary:
Just moving stuff around.
This is possibly useful for making Pvar depend on ProcAttributes for
other things, eg checking if a pvar is captured by a procedure (which
would be awkward to have in the API of ProcAttributes and not Pvar).
Overall it forced me to move a few other things around in a way that I
feel makes more sense anyway.
Reviewed By: skcho
Differential Revision: D28091497
fbshipit-source-id: 367a1f17c
Summary:
In order to use Inferbo's analysis result, a checker should know current instruction index.
However, for the checkers using `ProcCfg.Normal` CFG, it was impossible to get the instruction
index. To solve the issue, this diff changes the AbsInt framework to give the index together to
`exec_instr`.
Reviewed By: ezgicicek
Differential Revision: D27680894
fbshipit-source-id: 1dc8ff0fb
Summary: Autogenerated methods sometimes lead to false positives. Also, clean up a little the models file.
Reviewed By: da319
Differential Revision: D27393933
fbshipit-source-id: f79b1a6eb
Summary:
RacerD needs to analyse the class initialiser in order to establish field properties in its post, such as that certain static fields are synchronized containers.
There was a bug where class initializers were not analysed at all, from the time where there was no analysis of field properties in the post.
We still don't want to report on the class initialiser since it cannot possibly race with itself (JVM guarantees that) and it cannot race with any of the other methods in its class (because it must finish before any other method can be called).
Reviewed By: da319
Differential Revision: D26887151
fbshipit-source-id: 570aff370
Summary: The `NonBlocking` annotation should zero out all domain elements that represent blocking calls. The current implementation only really removes such elements when they are generated by the current method under analysis, leaving such elements from callees unaffected. This diff fixes that.
Reviewed By: jvillard
Differential Revision: D26874704
fbshipit-source-id: 2d4859b30
Summary: `STARVATION` is currently used as a catch-all for several blocking events. This diff splits out `IPC_ON_UI_THREAD`.
Reviewed By: skcho
Differential Revision: D26691868
fbshipit-source-id: 618423793
Summary: Instead of accumulating all reports for a location in a list and then partitioning that list by issue type, just use a map from issue types to report lists.
Reviewed By: ezgicicek
Differential Revision: D26748929
fbshipit-source-id: 81c35cd4e
Summary: Now that all reports are deduplicated using the same criterion (trace length), use that to simplify deduplication functions.
Reviewed By: skcho
Differential Revision: D26726239
fbshipit-source-id: 77e3b319a
Summary:
A "severity" level was used for keeping the highest severity issue when deduplicating across many issues on the same location. This was used for only one of the issue types reported by the analysis.
It turned out this isn't very useful and it complicates significantly the reporting code.
This diff removes the type and uses trace depth to sort all the issue types in the same way all other issue types than `starvation` used.
Next diff will remove now unnecessary stuff.
Reviewed By: skcho
Differential Revision: D26725569
fbshipit-source-id: f9287dcd1
Summary:
The javax.crypto.Mac classes behaves like a container
and can lead to race conditions when used in a concurrent context.
This adds Mac operations as container writes/reads in RacerD's models.
Pull Request resolved: https://github.com/facebook/infer/pull/1395
Test Plan: CI
Reviewed By: skcho
Differential Revision: D26722737
Pulled By: ngorogiannis
fbshipit-source-id: 74f03e9a5
Summary:
Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks.
This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer:
> Data races in `Nullsafe` classes may still cause NPEs.
This only happens if the race is directly on a non-primitively-typed member field of the class.
It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting.
Reviewed By: ezgicicek
Differential Revision: D26403274
fbshipit-source-id: 3cd6ca082
Summary: As there are no dependencies between procedure and file analyses in RacerD, split them into separate modules.
Reviewed By: ezgicicek
Differential Revision: D26198874
fbshipit-source-id: 032aad9d8
Summary:
`SettableFuture.set` invokes callbacks registered prior to the call, which may also try to acquire extra locks. If the called of `set` already holds a lock this creates lock dependencies which may lead to deadlocks.
Here we warn whenever `set` is called under a lock taken in a different source file. This avoids reporting when a class internally manages locks and calls `set`, reasoning that developers will be aware this is happening.
Reviewed By: jvillard
Differential Revision: D25562190
fbshipit-source-id: d1b5cb69c
Summary:
Dear Infer team,
To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.
Please help to review, discuss and consider to merge this feature.
Thanks,
Xiaoyu
Pull Request resolved: https://github.com/facebook/infer/pull/1361
Reviewed By: skcho
Differential Revision: D25928458
Pulled By: jvillard
fbshipit-source-id: 7726150b8
Summary:
Lambdas are essentially private (but are not marked as such in Infer),
so we should only report on their non-private callers.
Meanwhile, add a test to document that access propagation to those
callers is currently broken.
Reviewed By: da319
Differential Revision: D25944811
fbshipit-source-id: ef8ca6d9c
Summary:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What the previous and this diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then this diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562303
fbshipit-source-id: 4cbc6d234
Summary:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What this and the next diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First this diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then the next diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562297
fbshipit-source-id: b96622336
Summary: The main point here is to ignore owned interfaces when considering whether to warn about non-thread-safe calls.
Reviewed By: ezgicicek
Differential Revision: D25187775
fbshipit-source-id: c2a7ce89c
Summary: At a function call, an access performed by a callee must be processed in various ways before it's added to the accesses of the caller, and several of these steps may throw away the access. Previously, this was done by effectively doing a bit of transformation, creating a new set of accesses, then folding over that to add to the caller's. This is inefficient and somewhat confusing, as this can be done with one fold and a sequence of `Option.map`s.
Reviewed By: skcho
Differential Revision: D24885117
fbshipit-source-id: 4ab61eab9
Summary:
As per title, plus de-quadratic-ify substitution of actuals into formals.
Also, fix a bug in treatment of callee summaries where the caller lock state was updated first and then used to process accesses in the callee (so should only take into account the original caller state).
Reviewed By: jvillard
Differential Revision: D24857922
fbshipit-source-id: 07ce6999c
Summary: As per title, plus minor improvements in interfaces and a couple of FIXMEs.
Reviewed By: skcho
Differential Revision: D24836125
fbshipit-source-id: f7a4dc196
Summary:
The starvation domain keeps a domain element per distinct pair of lock object and source location. This was used to counteract the imprecision of implicit Quandary-style traces. Starvation has used explicit traces for a long time now, so keeping all these elements is expensive (in fact, in some cases exponential) and of no value. Now, lock object identity is the only distinguishing feature of a domain element.
Also, fix some pretty printing for debugging purposes.
Reviewed By: jvillard
Differential Revision: D24829306
fbshipit-source-id: 22e12f9c1
Summary: Cleanup `Typ` by moving all constant types to `StdTyp`. Also remove `Typ.typ` as it's just `Typ.t` now.
Reviewed By: jberdine
Differential Revision: D24620397
fbshipit-source-id: 4764f87ef
Summary:
Another step in the refactoring of the starvation domain:
- Main purpose is to mediate access to the set of critical pairs in a summary through a fold function (`fold_critical_pairs_of_summary`) and not through direct field access to that set. This will allow eliding storage of critical pairs entirely and dynamically generating those when folding.
- Remove optional arguments as much as possible, as this led to unused arguments not being caught.
- Helper functions distributed more logically among modules.
Reviewed By: skcho
Differential Revision: D24275399
fbshipit-source-id: d23123a48
Summary: As part of a refactor, push `thread` from the enclosing type (`CriticalPairElement`) into `Event.t`.
Reviewed By: jvillard
Differential Revision: D24161709
fbshipit-source-id: bd812f3fd
Summary:
`NonBlocking` methods have starvation errors silenced (but not deadlock ones). This is implemented by summarising as usual and then filtering out such events when the summary is finalised, if the method is annotated as such.
It's better to not record the events in the first place.
Reviewed By: ezgicicek
Differential Revision: D24237465
fbshipit-source-id: 1b24a26f0
Summary: Subsequent diff will push information down into `Event.t` so as preparation, turn all variant values into records.
Reviewed By: jvillard
Differential Revision: D24115201
fbshipit-source-id: d2126dd49
Summary:
`std::lock(x,y,z)` simultaneously acquires locks `x,y,z` in a deadlock free manner (essentially an unspecified fixed order).
Starvation currently deals with it by exploiting properties of the state domain. It's a map from locks to number of times the lock is held, so the count of many locks can be increased at the same time without recording any particular lock order.
In upcoming diffs the domain will be refactored into a tree of nested lock acquisitions (for other reasons) and that domain necessarily records lock order. The obvious way of doing this correctly is to allow `std::lock` as an atomic even (ie, without trying to break it into multiple acquisitions).
This diff does exactly that, by changing the `Event.LockAcquire` variant to take a list of locks.
Reviewed By: ezgicicek
Differential Revision: D24052304
fbshipit-source-id: 410c812d7
Summary: Subtle false positives and negatives in Hil make Sil preferable. This diff gets rid of the CFG-emulation of Hil, while still using Hil expressions.
Reviewed By: da319
Differential Revision: D23815026
fbshipit-source-id: 731a6d299
Summary: Most of the time, when the procdesc of a callee is requested, all that is really required is the procedure attributes. However, requesting the procdesc may return `None` when the procedure is undefined (in Java, and soon for Clang too). So, change all callsites to using attributes instead, where possible.
Reviewed By: jvillard
Differential Revision: D23539422
fbshipit-source-id: 3b1a52d48
Summary:
This is needed to make dune auto-updating of unit tests introduced in
the next diff cohabit peacefully with our tests to make sure code stays
correctly formatted wrt ocamlformat.
Also, more auto-formatting = better.
Reviewed By: da319
Differential Revision: D22865004
fbshipit-source-id: 91c47ab08
Summary:
Use `Typ.t` for parameter types in procnames, instead of `JavaSplitName.t`. This allows more precise and usable types stored in procnames, as well as not using the string-based representation of `JavaSplitName` which meant parsing strings whenever one needed a `Typ.t`.
This also makes `JavaSplitName` dead code, so it is removed.
Reviewed By: skcho
Differential Revision: D20500423
fbshipit-source-id: a72728e3f
Summary: This diff refactors Java specific `PatternMatch` functions into its own module. When `PatternMatch.ml` was originally created, it was mainly for Java but now it also supports ObjC. Let's refactor it to reflect the Java/ObjC separation: move all functions that operate on Java procnames into Java submodule.
Reviewed By: jvillard
Differential Revision: D22816504
fbshipit-source-id: ff6b64b29
Summary:
By and large issues of a given type (eg NULL_DEREFERENCE) are always
reported with the same severity (eg ERROR), but that severity is hard to
tease out from the code. This makes it more explicit by favouring the
default in `IssueType.t` in many cases without changing infer's
behaviour. The checkers typically use `Reporting.log_{error,warning}`;
these are taken care of in the next diff.
Reviewed By: skcho
Differential Revision: D21904590
fbshipit-source-id: 47c76cd4c
Summary:
- "visibility" (whether an issue to report is something to show the user
or something that is only used for debugging or for detecting other
issues) is an intrinsic property of an issue type and thus belongs in
`IssueType.t`.
- "severity" (warning/error/...) is something that each issue should
have a default for ("a memory leak is by default an ERROR", a
"condition always true is by default a warning"), but can also be
overriden at run-time. Right now only nullsafe uses that capability:
when in "strict mode", some warnings become errors. We can imagine
extending this to other issue types, or even providing config flags to
turn warnings into errors, like compilers often have.
To guess the default severity (since it's dynamic it can be hard to know
for sure!), I tried to find places where it was reported as the source
of truth, but also later diffs test these defaults against our tests (by
removing most of the dynamic changes in severity).
With this diff there are 3 places where severity is set:
1. The default severity in IssueType.t: this is unused for now.
2. The severity from `Exceptions.recognize_exception`: this is
semi-statically determined and, if set, takes precedence over number 3 (which looks wrong to me!)
3. The severity passed to `Errlog.log_issue` when we actually add an
issue to the error log: this is used only when (2) is unset.
The next diffs will make 1 the default, delete 2, and make 3 optional
but override 1 when passed.
Reviewed By: skcho
Differential Revision: D21904538
fbshipit-source-id: a674b42d8
Nikos Gorogiannis
Radu Grigore
Xiaoyu Liu
Jules Villard
Sungkeun Cho
Daiva Naudziuniene
Daniel Schoepe
Ezgi Çiçek