Summary: We should be able to run this processing ast steps without running linters or capture. This also adds a new module ProcessAST to do the processing, Capture.ml should not know anything else than calling the respective modules for capture, linting or processing.
Reviewed By: ngorogiannis
Differential Revision: D17501453
fbshipit-source-id: 30adba5b1
Summary:
`ModeledRange` represents how many times the interval value can be updated by modeled functions. This
domain is to support the case where there are mismatches between value of a control variable and
actual number of loop iterations. For example,
```
while((c = file_channel.read(buf)) != -1) { ... }
```
the loop will iterates as the file size, but the control variable `c` does not have that value. In
these cases, it assigns a symbolic value of the file size to the modeled range of `c`, then which
is used when calculating the overall cost.
Reviewed By: jvillard
Differential Revision: D17476621
fbshipit-source-id: 9a81376e8
Summary:
Fixes a bug where are all calls are treated as intrinsics in used
globals analysis, since exec_intrinsic is invoked at _all_ calls
to determine which are intrinsic, not only at call sites known to
target intrinsics.
Reviewed By: jberdine
Differential Revision: D17499406
fbshipit-source-id: 41f7621f2
Summary:
While the symbolic heap analysis ends its search upon hitting the
bound on recursion depth, the used-globals analysis should instead
simply skip recursive calls beyond the depth. Note that this is
unsound for arbitrary abstract domains, however, and the flag
controlling this feature should be used with caution.
Note that procedure calls are still not handled correctly, since
Used_globals.exec_intrinsic does not properly check whether callees
are intrinsic. A forthcoming commit will fix that, as well.
Reviewed By: jberdine
Differential Revision: D17479753
fbshipit-source-id: aa92e0ef3
Summary:
Include global variables used in function callees in used globals
analysis. Also adds support for arbitrary changes to symbolic
state while resolving callees in other analyses.
Reviewed By: jberdine
Differential Revision: D17479352
fbshipit-source-id: e3cd9f179
Summary:
1/ Nikos Gorogiannis pointed out that
- for highly reused public types, records (especially when >= 3 params) are generally more readable than tuples.
- Records simplify code modifications, especially adding new fields. And we are going to add some, namely param flags, in the future.
2/ Let's make the fact that annotated signature is deprecated more
visible; it will also simplify searching for usages when we will be
getting rid of them.
Reviewed By: ngorogiannis
Differential Revision: D17475033
fbshipit-source-id: 7740c979b
Summary:
- Instead of merging one target DB into the main DB at a time, merge all target DBs into an in-memory DB (thus, no writing) and then dump it into the main DB at the end. This makes merging faster.
- When using the sqlite write daemon, there is no reason to drive the merge process from the master, sending each individual target to merge down the socket and doing one DB merge at a time. Here we move all the DB merging logic in the daemon, and expose a single function that does it all.
- Refactor some common functionality (notably the `iter_infer_deps` function is now in `Utils`) and remove dead files.
This can be also done using a temporary DB (which is not limited to memory) but this showed worse perf in tests than the in-memory solution as well as the current state of things (! possibly Sqlite-version related?).
Reviewed By: skcho
Differential Revision: D17182862
fbshipit-source-id: a6f81937d
Summary:
Replace custom version reporting support using a shell script with
code using dune's Build_info API.
Note that after this diff, the executables under _build/<context> are
not version-stamped, but those under _build/_install are. The symlinks
in bin point to the latter, stamped, exes.
Reviewed By: bennostein
Differential Revision: D16985446
fbshipit-source-id: 7afac87be
Summary:
`get_field_annotation` is (together with
`get_modelled_annotated_signature`) an entry point when Nullsafe fetches
annotation information.
In follow up diffs we are going to utilize added information; see also
TODO in the code
Reviewed By: ngorogiannis
Differential Revision: D17475034
fbshipit-source-id: dab77bc7b
Summary:
"Unannotated" is misleading and ambiguous concept, it can have different
meanings depending on agreements.
The current logic treats them as Nonnull, which is exactly what we want
to preserve.
(If we need to partially model some functions where we don't have
opinion on some of types in the signature, we can explicitly model
unknown nullability later on).
Note that I am not aiming for substantial refactoring of
modelsTables.ml; the scope of this diff is merely to clarify things.
Reviewed By: ngorogiannis
Differential Revision: D17449347
fbshipit-source-id: 43c798ce7
Summary:
This function is the main entry point for getting annotated signature
for nullsafe.
We will modify it and its callees in follow up diffs to migrate other
features of Annot.items to specialized types.
Reviewed By: ngorogiannis
Differential Revision: D17448082
fbshipit-source-id: be00b4737
Summary:
Adds an abstract domain to track global variable usages, as well as supporting
changes to the frontend, IR and CLI. This analysis will support optimizations
to the main symbolic-heap analysis, but for now can be invoked independently
through the `-domain` flag on `analyze` targets of the Sledge executable.
Reviewed By: jberdine
Differential Revision: D17422212
fbshipit-source-id: 74bed0a76
Summary:
This is a central abstraction for coming future unknown nullability support.
# Context
Annot.ml is a low-level module:
- it contains lists of raw (string) annotations
- no algebraic datatypes for annotations
- it mixes annotations that Nullsafe should be aware of with all sorts of other annotations
- some annotations make sense for return values, some make sense for params, and some make sense for methods.
But, most importantly, it does not contain information about source of an annotation, making it hard to distinct things like "Nonnull as default" vs "Nonnull as explicitly annotated" vs "Nonnull as modelled". Ditto for nullable.
Because of this, it is tricky to introduce unknown nullability in an elegant way.
Let's get rid of using Annot.Item.t in nullsafe code in the following way:
- Move nullability information associated with the Java type to a dedicated algebraic DT.
- Split other annotations that are important for nullsafe into param flags, ret value flags, and method flags, and introduce corresponding datatypes.
# This diff
This diff introduces NullsafeType and adds this to AnnotatedSignature.
It is not used yet, hence the diff is a no-op.
In future diffs, we are going to (see also TODOs in the code):
- actually use this information instead of accessing Annot.item
- add more information to AnnotatedSignature
- remove Annot.item from AnnnotatedSignature
- when this is done, introduce notion of unknown nullability.
Reviewed By: ngorogiannis
Differential Revision: D17420595
fbshipit-source-id: b30706d9b
Summary:
This diff extends the `Simple` alias domain to address Java's
temporary variables better. It now has an additional field to denote
an alias temporary variable.
Reviewed By: jvillard
Differential Revision: D17421907
fbshipit-source-id: 8b8b47461
Summary:
We historically had Model.Inference, which was an attempt to enhance
models with additional abilities to get the annotation.
This feature got removed in D9805110, including removing of the key
condition Models.Inference.field_is_marked.
This code also is not executed: `Config.eradicate` condition
was an old artefact of migrating Eradicate to callback infrastructure:
D1508451. We run eradicate only as a callback as of now, so this flag is
always true.
In follow up diffs we refactor AnnotationSignature module, and this
cleanup simplifies the refactoring.
Reviewed By: ngorogiannis
Differential Revision: D17419173
fbshipit-source-id: 1b30555de
Summary:
CONDITION_REDUNDANT_NONNULL was an attempt to reduce number of false
positives for condition redundant. (It is the most popular check as of
now).
The root case for most of false positives is that a lot of code is
simply not annotated (but should have been), so blaming developers for defense programming is
not actionable.
In attempt to solve the problem, a special issue type (for case when the
code is explicitly annotated with Nonnull) was introduced.
In follow up diffs we are going to introduce a generic way of doing the
same, not limited to this particular check only.
Namely, we will introduce notion of unknown nullability, so it will be
possible to distinguish not annotated yet (hence no warnings) and already
annotated (hence warnings) parts of code.
This piece of logic is incompatible with the aforementioned work, hence
we need to remove it.
Reviewed By: jvillard
Differential Revision: D17398768
fbshipit-source-id: 8bddf10e5
Summary:
D17397144 adds dedicated tests for condition redundant.
We also have tests for overannotated methods.
This makes these test cases redundant. Let's not pollute the results.
Reviewed By: jberdine
Differential Revision: D17398757
fbshipit-source-id: 10f6beeca
Summary:
This will simplify modifying functionality around this type of error.
Also rename the file for clarity.
Reviewed By: jvillard
Differential Revision: D17397144
fbshipit-source-id: 552215243
Summary:
This diff simplifies two similar alias targets: AliasTarget.Simple and
AliasTarget.SimplePlusA. Since the latter is simply extended version
of the former, they are better to have a common constructor.
Reviewed By: jvillard
Differential Revision: D17421416
fbshipit-source-id: e0946a73b
Summary:
This diff revises widening functions of bounds that have a linear form and a min/max form.
For example, for lower bounds,
* 3 ▽ (1+min(2, x)) = (1+min(2, x))
* 3+x ▽ (3+min(2, x)) = (3+min(2, x))
Reviewed By: jvillard
Differential Revision: D17420786
fbshipit-source-id: ff9eebed3
Summary: This diff ignores field's type in their comparisons. They should be distinguished by their names and struct types.
Reviewed By: dulmarod
Differential Revision: D17284621
fbshipit-source-id: ae8a33083
Summary:
This diff addresses collection adds in loop. For example,
```
ArrayList<...> a = new ArrayList<>();
for (int i = 0; i < size; i++) {
a.add(...);
}
// we want to know the size of `a` here!
```
This is a common pattern on initializing a collection in Java.
How we did: Instead of adopting general (but complicated) solutions such as relational domain, we
extended the current alias domain of inferbo, to be able to handle this specific case:
* An array `a` should have size 0, at the entry of the loop.
* The iterating variable `i` should start with 0.
* `add` should be called once inside the loop.
Reviewed By: jvillard
Differential Revision: D17319350
fbshipit-source-id: 99b6acae1
Summary:
In D17156724, we forked nullsafe tests, which was a strategy to
introduce nullsafe-gradual mode back then.
The reason was "gradual" mode is a pretty big change in a way Infer
handles annotations, so we wanted to tests both scenarios: gradual and
non-gradual mode.
The plan was to deprecate "non-gradual" tests at some point, hence we
decided to go with duplication.
Now we have a better approach to ensure "gradual" features are well
covered. The approach is the following.
1. [Mostly finished] Improve existings tests so that they cover negative and positive
cases. With this, we can safely add something like
--non-annotated-default UNKNOWN_NULLABILITY to the test config and be sure tests still make
sense (i.e. don't pass simply because annotations don't make sense
anymore)
2. [In progress]. Refactor nullsafe code so that instead of using of Annot.ml everywhere we use a special abstraction telling if the class is annotated with Nullable, Nonnull, or not annotated. With this change, we essenstially have a single place we need to test, which removes the need to have 2 pair of tests for each feature.
3. [To be done]. Introduce Uknown nullability and add small number of tests specifically
for that feature (together with existing tests).
NOTE: I did not rename `nullsafe-default` back to `nullsafe` to not
pollute blame without need.
Reviewed By: artempyanykh
Differential Revision: D17395743
fbshipit-source-id: 3d3e062f6
Summary:
Sqlite versions set their own default page and cache size. Old versions use crazy-non-optimal settings.
Allow setting both from command line and set up reasonable defaults. See, e.g.,
https://wiki.mozilla.org/Performance/Avoid_SQLite_In_Your_Next_Firefox_Feature
for page size notes.
The defaults will cost a maximum of 64Mb in cache per Infer process. These improve merging times significantly.
Reviewed By: jvillard
Differential Revision: D17364643
fbshipit-source-id: b9abab10f
Summary:
At some point, there was a custom equality function that deliberately ignored some fields in err_instance. It was deleted in D4232422, so having a custom hash function does not serve any purpose anymore.
Since 2016 there was no known problems with the change in D4232422.
If we decide that we need similar behavior that was before D4232422, it will be easier to reimplement the functionality again.
Reviewed By: jberdine
Differential Revision: D17313660
fbshipit-source-id: 5c6c29a0b
Summary:
We want to allow following declaration
```
CK::UIContext t(foo);
```
In this case t is only part of the scope and we don't want to check that is never mutated.
Reviewed By: kfirapps
Differential Revision: D17367040
fbshipit-source-id: 5312a1249
Summary: Adding a test to the top level makefile that I forgot to add (ooops)
Reviewed By: jvillard
Differential Revision: D17366065
fbshipit-source-id: 8111ccf7a
Summary: This calls the method `delete_capture_and_analysis_data` introduced in D17184424 once the appropriate specs files for incremental analysis have been deleted. This fixes two bugs that I observed in incremental analysis that were arising because of stale state left in the results directory.
Reviewed By: ngorogiannis
Differential Revision: D17184424
fbshipit-source-id: d63f59db9
Summary:
I observed a bug in incremental analysis for thread safety analysis, where a thread safety violation was not being reported because the folder `racerd` was not being cleaned. This meant that the violation was determined to be a preexisting issue when it was actually an introduced issue.
This method can be used to fix this problem by cleaning the `racerd` folder. It also cleans the `captured` folder, I've done this following the original version of the method (see D16602417).
I'm not sure if the `captured` folder is used; it wasn't used in the tests I did. Thoughts about this?
Reviewed By: ngorogiannis
Differential Revision: D17261504
fbshipit-source-id: 8fea23e98
Summary:
There is currently a bug in incremental analysis because the capture data is not reset once the specs files have been invalidated. This has caused a problem where cost issues that should be reported are not spotted. I'm introducing this method so I can use it to fix incremental analysis.
This method is resurrected from D16602417
Reviewed By: ngorogiannis
Differential Revision: D17184401
fbshipit-source-id: e84925324
Summary:
Get rid of helper class `C`, normal Object serves the same goal well
Don't return values from a function, focus only on nullable
dereferences.
Reviewed By: jberdine
Differential Revision: D17314569
fbshipit-source-id: d70e66b5f
Summary:
Generalize the lifting from State_domain (i.e. symbolic heaps) to Sh_domain (i.e. relations over symbolic heaps).
Also, extract abstract-domain-related code into its own module/directory.
Reviewed By: jberdine
Differential Revision: D17319007
fbshipit-source-id: cefbd1393
Summary: Add support for future development of new abstract domains by eliminating hard-wired dependencies from the worklist into the symbolic heap domain. Also includes an implementation of a trivial unit domain and a CLI flag to enable its use, for debugging purposes.
Reviewed By: jberdine
Differential Revision: D17281681
fbshipit-source-id: 5858fd420
Summary:
1. Split into 3 subclasses for 3 major set of features we test
2. Document a known FP
3. More clear names
Reviewed By: jberdine
Differential Revision: D17285902
fbshipit-source-id: 66e3b5668
Summary:
Let's consolidate "positive" and "negative" cased together by adding an example
of not annotated class as a source of "negative" cases.
Also join the case with modelled methods to the same class.
Reviewed By: jberdine
Differential Revision: D17284101
fbshipit-source-id: e15e60691
Summary: It prints debug information when top values is generated.
Reviewed By: ngorogiannis
Differential Revision: D17285448
fbshipit-source-id: 0621fd36d
Summary:
This check was an incomplete attempt to make nullsafe check nutritious
annotations for fields that get modified.
This was never fully productionized, and this check is turned off by
default.
In near future, we don't anticipate supporting this feature, so let's
remove it to simplify the code.
Reviewed By: artempyanykh
Differential Revision: D17282015
fbshipit-source-id: d63a2f1f7
Summary:
There are currently plenty of ways to suppress the warning, including Inject, Initializer, and SuppressFieldNotInitialized annotations.
This one (annotating field with Nonnull) is counter-intuitive and does not align with gradual nullsafe
semantics we are working on.
Reviewed By: artempyanykh
Differential Revision: D17281702
fbshipit-source-id: 132e1b687
Summary:
This diff ignores character symbols in the cost results, in order to
avoid FPs from parser code.
Reviewed By: ezgicicek
Differential Revision: D17132053
fbshipit-source-id: d9cf8bd26
Summary: let's always have positive and negative case for each feature we test
Reviewed By: ngorogiannis
Differential Revision: D17206785
fbshipit-source-id: 5791ace48
Dulma Churchill
Sungkeun Cho
Taras Tsugrii
Benno Stein
Mitya Lyubarskiy
Nikos Gorogiannis
Josh Berdine
Fabio Milano
Phoebe Nichols