Summary:
This diff adds a procedure name to the head of the trace in order to distinguish issues in the same line.
"Updated Cost is ..." is changed to "Updated Cost of <proc name> is ..."
Reviewed By: ezgicicek
Differential Revision: D20672214
fbshipit-source-id: 303b4492f
Summary:
- Model `System.exit()` as early_exit and add a test
- Tweak message of methods that are impure due to having no pulse summary (and add a test)
Reviewed By: skcho
Differential Revision: D20668979
fbshipit-source-id: 6b5589aae
Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning.
Reviewed By: ezgicicek
Differential Revision: D20645488
fbshipit-source-id: 6516c75d1
Summary:
Hopefully no one uses this. This is in Python and we'd like to get rid
of it. Easy enough to either re-implement if needed or to be
re-implemented by a third party.
Reviewed By: ngorogiannis
Differential Revision: D20626344
fbshipit-source-id: 484022482
Summary: The current message is recommending to change `View.findViewById()` to `View.requireViewById()`, but the latter method is not supported in all API, so might lead to a crash in runtime.
Differential Revision: D20619361
fbshipit-source-id: 542746c79
Summary:
- the order of call state was wrong when printing contradiction for CItv
- add a test for impurity
Reviewed By: jvillard
Differential Revision: D20646181
fbshipit-source-id: 1c86fd0a4
Summary: There are no plans currently to track which lock protects each access, so reduce to the functional equivalent of having a singleton lock domain.
Reviewed By: skcho
Differential Revision: D20595013
fbshipit-source-id: d5100ac49
Summary:
As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by:
- discovering aliasing in memory
- widening limited number of times in loops and concluding that loop exit conditions are never taken
However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts:
```
Pulse: 1 pre/post(s)
#0: PRE:
{ roots={ };
mem ={ };
attrs={ };}
POST:
{ roots={ };
mem ={ };
attrs={ };}
SKIPPED_CALLS: { }
```
The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure.
Reviewed By: skcho
Differential Revision: D20619504
fbshipit-source-id: 3a8502c90
Summary:
Although try-with-resource is supported by nullsafe this code pattern
throws it off and make nullsafe report on a virtual **b**yte-**c**ode
variable.
Check out debug output from `TryWithResource` (or attached
visualisation of CFG):
0. node14: $bcvar2=null (on entry to try-with-resource).
1. node16: n$14=$bcvar2, but **also** PRUNE(!(n$14 == null), true). Then we go to
2. node18: do something here and in case of exception go to
3. node25->node23->node19->node20: and here we do
$bcvar2->addSuppressed(...).
Because on step 1 we refined nullability of n$14, but didn't refine
nullability of $bcvar20, on step 3 we are sure that $bcvar is null and
therefore issue an error.
Reviewed By: mityal
Differential Revision: D20558343
fbshipit-source-id: 520505039
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary: Add a flag `is-inclusive-cost` (`true` by default) which computes inclusive cost for each function. Setting the flag to `false` computes exclusive cost of the function where the cost of the callees are assumed to be `0`.
Reviewed By: skcho
Differential Revision: D20558275
fbshipit-source-id: 6b5798916
Summary:
# Problem
Consider
```
some_method(Object a) { a.deref(); }
```
What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.
This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.
The best we can capture it is via StrictNonnull nullability.
Reviewed By: artempyanykh
Differential Revision: D20536586
fbshipit-source-id: 5c2ba7f0d
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
- Add more naive pulse models for:
- `System.arraycopy`
- `StringBuilder.setLength`
- `StringBuilder.delete`
- Model the following as pure
- `SparseArrayCompat.valueAt`
- `File.get...`
- Add a nice test
Reviewed By: jvillard
Differential Revision: D20513397
fbshipit-source-id: 6d412d13a
Summary:
This diff continues work in D20491716.
This time for Inheritance Rule.
Reviewed By: jvillard
Differential Revision: D20492889
fbshipit-source-id: c4dfd95c3
Summary:
This diff continues work in D20491716.
This time for Dereference Rule.
Reviewed By: jvillard
Differential Revision: D20492296
fbshipit-source-id: ff7f824f9
Summary:
# Problem
In current design, Rules (assignment rule, dereference rule, inheritance
rule) decide, depending on the mode, wether the issue is legit or not.
If the issue is not actionable for the given mode, it won't be created
and registered.
For meta-issues, we want to be able to do smart things like:
- Identify if we can raise strictness of the mode without
introducing new issues
- Classify classes on "clean" vs "broken", taking into account issues
that are currently invisible.
# Solution
In the new design:
1. Rules are issuing violations independently of mode. This makes sense
semantically. Mode is "level of trust we have for suspicious things",
but the thing does not cease to be suspicious in any mode.
2. Each Rule decides if it is reportable or not in a given mode.
3. `nullsafe_mode` is passed to the function `register_error`, that 1)
adds error so it can be recorded in summary for file-level analysis
phase 2) reports some of them to the user.
# This diff
This diff converts only AssignmentRule, follow up will include
conversion of other rules, so no issue encapsutes the mode.
Reviewed By: jvillard
Differential Revision: D20491716
fbshipit-source-id: af17dd66d
Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.
For instance, for the following functions
```
public static boolean is_null(Byte a) {
return a == null;
}
public static boolean call_is_null(Byte a) {
return is_null(a);
}
```
We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null,
BoItv ([max(0, v2), min(0, v2)]),
WrittenTo-----------WRONG },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1),
WrittenTo-----------WRONG },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1) },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
Reviewed By: skcho
Differential Revision: D20490102
fbshipit-source-id: 253d8ef64
Summary: These tests fail when seemingly unrelated changes are made to infer. In particular, it seems timeout limits have to be increased by 10x or more to make them succeed again. Disabling until we have a more stable replacement.
Reviewed By: ezgicicek
Differential Revision: D20489647
fbshipit-source-id: 9706b0807
Summary:
This diff naively models the following as `StdVector.push_back`:
- `StringBuilder.append`
- `String.replace`
- `Queue.poll`
It also adds a FN test for `Iterator.next`.
Reviewed By: skcho
Differential Revision: D20469786
fbshipit-source-id: 2d8e8d117
Summary:
This diff is doing three things:
1. Finishes work paved in D20115024, and applies it to nullsafe. In that diff, we hardened API for
file level analysis. Here we use this API in nullsafe, so now we can
analyze things on file-level, not only in proc-level like it was before!
2. Introduces a class-level analysis. For Nullsafe purposes, file is not
an interesting granularity, but we want to analyze a lot of things on
file level. Interesting part here is anonymous classes and how we link
them to their corresponding user-defined classes.
3. Introduces a first (yet to be improved) implementation of class-level
analysis. Namely it is "meta-issues" that tell what is going with class
on high level. For now these are two primitive issues, and we will
refine them in follow up diffs. They are disabled by default.
Follow ups include:
1. Refining semantics of meta-issues.
2. Adding other issues that we could not analyze before or analyzed not
user friendly. Most importantly, we will use it to improve reporting for
FIELD NOT INITIALIZED, which is not very user friendly exactly because
of lack of class-level aggregation.
Reviewed By: artempyanykh
Differential Revision: D20417841
fbshipit-source-id: 59ba7d2e3
Summary: The `FN_loop2` was not actually FN because infer analyzes its complexity as degree 1 correctly.
Reviewed By: dulmarod
Differential Revision: D20468367
fbshipit-source-id: 9e4c19415
Summary: The `iterate_over_mycollection_quad_FN` was not actually FN because infer analyzes its complexity as degree 2 correctly. So, this diff removed `_FN` from there.
Reviewed By: ezgicicek
Differential Revision: D20467398
fbshipit-source-id: b10340612
Summary: There has never been a sufficient formal basis for soundness nor completeness of reports on locals. This diff changes the domain to effectively concern only expressions rooted at formals or globals.
Reviewed By: ezgicicek
Differential Revision: D19769201
fbshipit-source-id: 36ae04d8c
Summary: `Object.clone` modeled as pure until the analysis can distinguish returning a fresh object vs. having no side-effects.
Reviewed By: skcho
Differential Revision: D20439998
fbshipit-source-id: 421054cfb
Summary:
`JavaSplitName` is used to represent Java types (in `Procname` in particular). The type itself is a pair of string (an optional package qualifier) and a "type name" (the quotes are there because it may contain array qualifiers).
For example `java.lang.Object[][]` should be represented as
```
{package=Some "java.lang"; typename="Object[][]"}
```
The constructor `make` was misused to construct instead types such as
```
{package=None; typename="java.lang.Object[][]"}`
```
This is evident when we print the return type of a `Procname` non-verbosely (the default), but we still see the package qualifier.
Obviously this is not just a pretty-printing bug, the values were themselves wrong.
The fix is to use the `of_string` constructor which will parse the package and separate it correctly. Another bug (in response to this one) had to be fixed in `Procname.is_vararg` to maintain behaviour in Nullsafe and Quandary.
Reviewed By: mityal
Differential Revision: D20394146
fbshipit-source-id: 4633902eb
Summary:
Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance,
```
void swap_impure(int[] array, int i, int j) {
int tmp = array[i];
array[i] = array[j]; \\ included in the trace
array[j] = tmp; \\ included in the trace
}
```
here we recorded both array accesses.
This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once.
Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing.
Reviewed By: jvillard
Differential Revision: D20385745
fbshipit-source-id: d3647dad3
Summary:
D20362149 missed
- to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`.
- to set `include_value_history=false` for skipped calls.
This diff fixes these issues.
Reviewed By: skcho
Differential Revision: D20385604
fbshipit-source-id: 176e4d010
Summary:
Main changes are:
1. Dune can promote targets into the source tree as a part of build. This
allows us to **remove custom promotion/installation logic in src/Makefile**.
2. Dune promotion only works for path within workspace. This required
**moving dune-workspace one folder up**: from infer/infer/src to infer/infer.
But this is not bad, since it makes it possible to migrate tests under dune at some point.
3. `checkCopyright` now also promoted into `infer/infer/bin` instead of
`infer/scripts` partly for consistency and partly because of the
dune-workspace location.
4. `byte` mode was replaced with `byte_complete`. The latter takes
similar amount of time to build compared to `byte`, but produces
standalone binaries that don't require InferCStubs to be
installed. This allowed to remove `dune_exec_shim` and custom logic
around `dune build InferCStubs.install` when dealing with byte
targets.
All in all, `infer/src/Makefile` is not about 2/3 its previous size
with less custom logic in Makefiles/scripts and more encoded in dune
build files.
Reviewed By: jvillard
Differential Revision: D20303902
fbshipit-source-id: 9e4c65bd0
Summary:
With profiles and `(env ...)` stanza it's possible to consolidate
various ocamlc/ocamlopt/etc setups in a single place.
Where previously we needed to append `dune.common` to every dune file
and specify `flags` and `ocamlopt_flags` now the flags are specified
in `env` and applied accross the board.
This allows to
1. simplify build definitions,
2. avoid the need to generate dune files,
3. use plain sexps instead of OCaml and JBuilder plugin in build
files.
(I'll try to address 2 and 3 in the followup patches).
Existing `make` targets should continue working as before. Also, we
can use dune CLI like so:
```
infer/src$ dune printenv --profile opt # <- very useful for introspection
infer/src$ dune build check
infer/src$ dune build check --profile test
infer/src$ dune build infer.exe --profile dev
infer/src$ dune build infer.exe --profile opt
```
Also, with just 1 context something like `dune runtest` will run unit
tests only once instead of N times, where N is the number of contexts.
Now, there's one difference compared to the previous setup with
contexts:
- Previously, each context had its own build folder, and building infer
in opt context didn't invalidate any of the build artifacts in default
context. Therefore, alternating between `make` and `make opt` had low
overhead at the expense of having N copies of all build artifacts (1
for every context).
- Now, there's just 1 build folder and switching between profiles does
invalidate some artifacts (but not all) and rebuild takes a bit more
time.
So, if you're alternating like crazy between profiles your experience
may get worse (but not necessarily, more on that below). If you want
to trigger an opt build occasionally, you shouldn't notice much
difference.
For those who are concerned about slower build times when alternating
between different build profiles, there's a solution: [dune
cache](https://dune.readthedocs.io/en/stable/caching.html).
You can enable it by creating a file `~/.config/dune/config` with the
following contents:
```
(lang dune 2.0)
(cache enabled)
```
With cache enabled switching between different build profiles (but
also branches and commits) has ~0 overhead.
Dune cache works fine on Linux, but unfortunately there are [certain
problems with
MacOS](https://github.com/ocaml/dune/issues/3233) (hopefully, those
will be fixed soon and then there will be no downsides to using
profiles compared to contexts for our case).
Reviewed By: jvillard
Differential Revision: D20247864
fbshipit-source-id: 5f8afa0db
Summary:
This was never quite finished and inferbo has a new way to do sort of
the same thing.
Reviewed By: skcho, ngorogiannis
Differential Revision: D20362619
fbshipit-source-id: 7c7935d47
Summary:
Make <infer-out>/report.json the default value for this option, as this
is what is used 99% of the time. Clean up test options using this.
Reviewed By: ngorogiannis
Differential Revision: D20362644
fbshipit-source-id: a1bb18757
Summary:
Adding a model for malloc: we add an attribute "Allocated". This can be used for implementing memory leaks: whenever the variables get out of scope, we can check that if the variable has an attribute Allocated, it also has an attribute Invalid CFree.
Possibly we will need more details in the Allocated attribute, to know if it's malloc, or other allocation function, but we can add that later when we know how it should look like.
Reviewed By: jvillard
Differential Revision: D20364541
fbshipit-source-id: 5e667a8c3
Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories.
Reviewed By: skcho
Differential Revision: D20362149
fbshipit-source-id: 8a2a6115e
Summary: Type is not enough to say a function call of `Provider.get` is expensive or not.
Reviewed By: jvillard
Differential Revision: D20366206
fbshipit-source-id: 83d3e8741
Summary:
This diff uses a type parameter of `Provider.get` to decide whether assigning expensive cost to the
function call or not. For example, if the type is small one like `Provider<Integer>`, it be
evaluated to have a unit cost, otherwise a linear cost.
To get the return type of `Provider.get`, I added a simple analyzer that collects "casted" types
backwards. In Sil, while the function call statement loses the return type, e.g,
```
n$5=_fun_Object Provider.get()(n$3:javax.inject.Provider*);
```
the `n$5`'s value is usually casted to a specific type at some point later.
```
*&$irvar0:java.lang.Object*=n$5
n$8=*&$irvar0:java.lang.Object*
n$9=_fun___cast(n$8:java.lang.Object*,sizeof(t=java.lang.Integer;sub_t=( sub )(cast)):void)
```
So, the analyzer starts from the cast statements backward, collecting the types to cast for each
variables.
Reviewed By: ezgicicek
Differential Revision: D20345268
fbshipit-source-id: 704b42ec1
Summary: This diff adds a model for Java's `Object.clone()` method (similar to existing shallow_copy).
Reviewed By: jvillard
Differential Revision: D20341073
fbshipit-source-id: 30ae40fe7
Summary:
Some (all?) of this is already tested in other tests, but this feature
is important enough (and the implementation is scattered accross the
whole code), so I found it useful to have a small test that ensures the
very basic things are working as expected.
See `NestedFieldAccess.java` that tests far more advances things, but
here we focus only very basic things: conditions, local variable
assignments, and explicit assignments.
Reviewed By: jvillard
Differential Revision: D20339056
fbshipit-source-id: a6cfd0043
Summary: We forgot to take skipped calls into account for state comparison. This diff fixes that.
Reviewed By: skcho
Differential Revision: D20282739
fbshipit-source-id: 7b4d84bb0
Summary:
These were not used (and were actually activated byt the same config
param). They both are in experimental stage that never reached maturity.
Since the team does not have immediate plans to work on ObjC nullability
checker; and since "eradicate" (now known as nullsafe) is the main
solution for Java, removing it is sensible.
Reviewed By: jvillard
Differential Revision: D20279866
fbshipit-source-id: 79e64992b
Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.
Reviewed By: ngorogiannis
Differential Revision: D20118863
fbshipit-source-id: b49740d33
Sungkeun Cho
Ezgi Çiçek
Jules Villard
Mitya Lyubarskiy
Nikos Gorogiannis
Artem Pianykh
Dulma Churchill
Radu Grigore