Summary: To avoid NULLPTR_DEREFERENCE false positives we want to treat some functions as `abort`. A new flag `--pulse-model-abort` allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D21962555
fbshipit-source-id: d46b93c99
Summary: The new memory leaks analysis is now ready to be enabled by default and turned on in production. This also replaces the biabduction one which is now disabled.
Reviewed By: jvillard
Differential Revision: D21998666
fbshipit-source-id: 9cd95e894
Summary:
Turns out it was useful, so it is now reborn in OCaml.
Fixes https://github.com/facebook/infer/issues/1262.
Reviewed By: skcho
Differential Revision: D22016185
fbshipit-source-id: 31ccb7540
Summary:
This models ARC implementation of dealloc, see https://clang.llvm.org/docs/AutomaticReferenceCounting.html#dealloc. Dealloc methods can be added to ObjC classes to free C memory for example, but the deallocation of the ObjC instance variables of the object is done automatically. So here we add this explicitly to Infer:
1. First, we add an empty dealloc method when it is not written explicitly.
2. For each dealloc method (including the implicitly added ones) we add calls to dealloc of the ObjC instance variables.
Reviewed By: jvillard
Differential Revision: D21883546
fbshipit-source-id: f5d4930f2
Summary:
This diff avoids `infer report`s run parallel. If they do, there may be race for writing
`infer-out/.infer_runstate.json`, which result in `make test` failure in the next time.
Reviewed By: jvillard
Differential Revision: D21999073
fbshipit-source-id: 64df79cb6
Summary: We don't rely on `external-java-packages` in the inferconfig anymore. Let's remove it altogether.
Reviewed By: jvillard
Differential Revision: D21997962
fbshipit-source-id: 7a2e13cfe
Summary:
Finish implementing the CLI of the `help` command with these two
functions that can provide more information about checkers.
Reviewed By: ngorogiannis
Differential Revision: D21937175
fbshipit-source-id: da6b3ecee
Summary:
Write documentation for all documented issue types and all user-facing
checkers in the "next" version of the documentation. Next diff shows the
new website.
Reviewed By: dulmarod
Differential Revision: D21934370
fbshipit-source-id: 53315d2b4
Summary:
Similarly as for issue types, we want to generate the website
documentation from infer itself so we can easily cross-reference
checkers and the issue types they report.
This imports the website documentation written for some (very few) of
the checkers. I wrote some cursory one-liners for the rest.
Reviewed By: dulmarod
Differential Revision: D21934375
fbshipit-source-id: 8c9dc2b08
Summary:
Take all the issue type documentation in the website and add it to infer
itself so it can generate the website (see further diffs).
I mostly generated this diff by writing a script to call from `utop`
with various file lists to do most of the heavy lifting for me and make
sure I didn't forget any issue types: P132800781
Reviewed By: ngorogiannis
Differential Revision: D21934372
fbshipit-source-id: f3ea8c566
Summary:
This provides some of the infrastructure needed for documentation issue
types within infer itself so we can generate the website and keep it up
to date when introducing new issue types.
Basically each issue type has documentation in its datatype in OCaml
now. But, documentation strings can be several pages of text! To avoid
making IssueType.ml even more unreadable, add the option to write
documentation in long form in files in infer/documentation/issues/.
This implements `infer help --help-issue-type` and show-cases how
documentation works for a couple of issue types. Next diff bulk-imports
the current website documentation in this form.
allow-large-files
Reviewed By: skcho
Differential Revision: D21934374
fbshipit-source-id: 2705bf424
Summary:
```
$ infer help --list-issue-types
Format:
Issue type unique identifier:Human-readable version:Visibility:Default severity:Enabled:Checker:Documentation URL (AL only):Linters definition file (AL only)
ARRAY_OUT_OF_BOUNDS_L1:Array Out Of Bounds L1:Developer:ERROR:false:biabduction::
ARRAY_OUT_OF_BOUNDS_L2:Array Out Of Bounds L2:Developer:WARNING:false:biabduction::
ARRAY_OUT_OF_BOUNDS_L3:Array Out Of Bounds L3:Developer:WARNING:false:biabduction::
Abduction_case_not_implemented:Abduction Case Not Implemented:Developer:ERROR:true:biabduction::
...
```
Reviewed By: skcho
Differential Revision: D21934371
fbshipit-source-id: 77df2a40f
Summary:
`infer help` will be used to display information about issue types and
checkers, and to generate the corresponding website documentation. We
can add more things in it over time. The goal is to avoid having to go
read the source code of infer to figure things out that are user-facing.
Reviewed By: ezgicicek
Differential Revision: D21934376
fbshipit-source-id: 2788c5af1
Summary:
The checker names are only used in debug information but I need them to
be more useful so users can do queries about each checker. Turn them
into an "id" instead of a "name", with some constraints to avoid crazy
IDs. In the next diff these IDs will be used on the command lin.
Reviewed By: dulmarod
Differential Revision: D21934373
fbshipit-source-id: 847a4958d
Summary:
This diff gives an order on running `test1`, `test2`, and `test3`. If they run parallel, they may
have a data race on writing `infer-out/.infer_runstate.json`.
Another minor fix is the object file path to remove.
Reviewed By: jvillard
Differential Revision: D21995671
fbshipit-source-id: eb9950cae
Summary:
The past issue with ppx_compare on nonrec types has (at some point) been fixed.
Greped for `let compare = compare` and removed the workaround for `nonrec`.
Reviewed By: jberdine
Differential Revision: D21973087
fbshipit-source-id: 5e2043e20
Summary:
The past issue with ppx_compare on nonrec types has (at some point)
been fixed. Cf. https://github.com/janestreet/ppx_compare/issues/2
Reviewed By: ngorogiannis
Differential Revision: D21961645
fbshipit-source-id: de03a60a4
Summary:
It has no dependencies on the rest of the sledge codebase and might be
more generally useful.
Reviewed By: jvillard
Differential Revision: D21720980
fbshipit-source-id: b4f061e73
Summary: Cost analysis has an additional mode that checks whether the function occurs on a UI (main) thread. If so, it warns the user. This check is only supported for Java and C++ but not for ObjC, so the diff suppresses this check for ObjC, and set ```is_on_ui_thread``` to ```false``` by default.
Reviewed By: ezgicicek
Differential Revision: D21952470
fbshipit-source-id: 838dd5639
Summary:
Due to:
1. Additional dependency on kotlin-annotations,
2. nullsafe annotation being annotated as TypeQualifierDefault and
UnderMigration(status = STRICT) [which can have breaking effect on
Kotlin code],
let's bump the minor version of the artifact.
Pull Request resolved: https://github.com/facebook/infer/pull/1281
Reviewed By: jvillard
Differential Revision: D21952759
Pulled By: artempyanykh
fbshipit-source-id: 58aea14c3
Summary:
There was an issue on `make build_ant_test` that newly generated `issues.exp.test` is empty. When
infer runs with `-- ant`, if there is already built objects in `ant_out`, infer analyzes nothing,
which result in the empty `issues.exp.test`. For example,
```
~/infer/infer/tests/build_systems/ant$ make test
[11:26:49][36924] Testing ant integration...
[ 2s][36924] SUCCESS Testing ant integration
~/infer/infer/tests/build_systems/ant$ touch `which infer`
```
The makefile tries to reanalyze ant targets because `infer` binary has been changed. However, there
is nothing to build/analyze, since `ant_out` still exists as the same.
```
~/infer/infer/tests/build_systems/ant$ make test
[11:26:57][37078] Testing ant integration...
[ 1s][37078] SUCCESS Testing ant integration
diff --git a/Users/scho/infer/infer/tests/build_systems/ant/issues.exp b/Users/scho/infer/infer/tests/build_systems/ant/issues.exp.test
index 376146b5f..e69de29bb 100644
--- a/Users/scho/infer/infer/tests/build_systems/ant/issues.exp
+++ b/Users/scho/infer/infer/tests/build_systems/ant/issues.exp.test
@@ -1 +0,0 @@
[-build_systems/ant/src/Hello.java, Hello.test():int, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure test()]-]
Test output (build_systems/ant/issues.exp.test) differs from expected test output build_systems/ant/issues.exp
Run the following command to replace the expected test output with the new output:
make -C build_systems/ant replace
make: *** [test] Error 1
```
To handle this issue, this cleans `ant_out` before running infer.
Reviewed By: jvillard
Differential Revision: D21950916
fbshipit-source-id: f57056f6e
Summary:
Before: to report an issue type, wrap it in an exception type then pass
that around and translate it back to an issue type at some point.
After: no. Except biabduction, which was built like this and uses
raising of exceptions to stop the analysis too.
Reviewed By: dulmarod
Differential Revision: D21904589
fbshipit-source-id: cb8446f38
Summary:
See previous diff: issues are always reported with the same severity so
recognise that and just use their default severity in "modern" checkers.
Reviewed By: ngorogiannis
Differential Revision: D21904591
fbshipit-source-id: fb5387e35
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
Summary:
The Java frontend translates java field accesses on an object reference as field (`.`) followed by dereference (`*`) exactly like the arrow operator in C. However, when the field is static, it generates just a field access `.`. This is a bug.
This diff mitigates its effects for printing locks in starvation.
Reviewed By: skcho
Differential Revision: D21882875
fbshipit-source-id: 79846d826
Summary:
This diff implements part of the memory management for Objective-C classes in ARC, namely that `dealloc` is called when the objects become unreachable. In reality the semantics of ARC says that this happens when their reference count becomes 0, but we are not modelling this yet in Pulse. However, we could in the future.
This fixes false positives memory leaks when the memory is freed in dealloc.
`dealloc` is often implicit in Objective-C, it also calls the dealloc of instance variables and superclass. None of this is implemented yet, and will be done in a future diff. This will be added in the frontend probably, similarly to how it's done for C++ destructors.
This is an important part of modelling Objective-C semantics in Infer, I looked at whether this should be a preanalysis to be used by all analyses but this needs Pulse. So the idea is that any analysis that needs to understand Objective-C memory model well, should have Pulse as a preanalysis.
Reviewed By: jvillard
Differential Revision: D21762292
fbshipit-source-id: ced014324
Summary:
Adding a new attribute for dynamic type. It is set in the models of constructors, currently only in `alloc` in Objective-C. We use it in the following diff to figure out which `dealloc` method to call. However it could be useful for other things, such as dynamic dispatch.
#skipdeadcode
Reviewed By: jvillard
Differential Revision: D21739928
fbshipit-source-id: 9276c0a4d
Summary:
Since Java8, interfaces mays contain implementations
(default methods). We modify the resolve algorith in the Java frontend
to take care of that.
Reviewed By: jvillard
Differential Revision: D21785182
fbshipit-source-id: ffab8124c
Summary:
We stopped relying on an arbitrary threshold. Hence,
- we don't need all the machinery for reporting at a specific node for a threshold
- we can remove
- the issue type `EXPENSIVE_EXECUTION_TIME`
- the config option `--use-cost-threshold`.
Reviewed By: skcho
Differential Revision: D21859815
fbshipit-source-id: b73a2372d
Summary: We do not use an arbitrary threshold to test cost results anymore but instead rely on `cost-issues` which do not have any trace attached. This diff adds traces to `costs-report.json` so that we can test cost issues with traces.
Reviewed By: skcho
Differential Revision: D21858846
fbshipit-source-id: e73321a92
Summary:
Now that we have a way to write cost issues, let's not rely on some arbitrary threshold (and also get rid of `EXPENSIVE_EXECUTION_TIME` issues in tests).
One consequence of this is that we will loose the cost traces in tests since `costs-report.json` doesn't have any traces. Next diff fixes that.
Reviewed By: skcho
Differential Revision: D21837574
fbshipit-source-id: 86b4d028d
Summary:
The model returns an array the length of which is the same to that of enum entries.
It takes the length of enum entries from the summary of `Enum.values` because it is not written in `tenv`. In order to do that, the model semantics should be able to request the summary of the function with `get_summary`, so I extended `model_env` to include the functionality.
Reviewed By: ezgicicek
Differential Revision: D21843319
fbshipit-source-id: d6f10eb91
Summary:
The model returns an array the length of which is the number of known
fields in `tenv`.
Reviewed By: ezgicicek
Differential Revision: D21840375
fbshipit-source-id: 891517c6e
Summary: D21816312 forgot to add the new cost testing mechanism to `fb-performance` and `performance-exlusive` directories. This diff fixes that.
Reviewed By: skcho
Differential Revision: D21837912
fbshipit-source-id: 407dafcd3
Summary: The models were too naive before since they invalidated the underlying array completely (copying C++'s push_back model), causing spurious vector invalidation issues in Java. This diff adds more reasonable models.
Reviewed By: skcho
Differential Revision: D21787543
fbshipit-source-id: a5a59ff69
Summary:
In order to test cost analysis results, currently we rely on having an arbitrary cost threshold (200) and report issues that exceed this cost. For instance, a cost of 201 is considered expensive and reported as `EXPENSIVE_EXECUTION_TIME` issue in cost tests.
This means, if we change the cost analysis in a slight way that results in some constant cost increase under 200, we wouldn't able to detect it. I find this unsatisfactory and somewhat hacky.
This diff adds the ability to write the result of `costs-report.json` into a separate `cost-issues.exp` and then compare the actual costs (not only than relying on this arbitrary threshold reporting mechanism).
Reviewed By: skcho
Differential Revision: D21816312
fbshipit-source-id: 93b531928
Summary: Add models for `View` methods that schedule on the UI thread.
Reviewed By: skcho
Differential Revision: D21767954
fbshipit-source-id: 015441ea7
Summary:
There were two problems: (1) `Signal.Expert.handle` does not call exit by itself; (2) it calls `flush` inside, which introduced deadlock, result in zombie processes.
This diff changes overall processes of the signal handler.
1. It uses `Caml.Sys.set_signal` instead of `Signal.Expert.handle`.
2. Inside the signal handler it raises an exception, then which is catched in `uncaught_exception_handler` of `Config.ml`. Epilogues are executed there.
Reviewed By: jvillard
Differential Revision: D21769246
fbshipit-source-id: cecd998c6
Summary:
IR/ should contain modules pertaining to the core IR of infer, i.e. how
CFGs are represented (including SIL).
These categories of modules were moved:
- Access paths and HIL are an abstraction on top of SIL used by certain
analyses. Moving the corresponding modules to IR/ makes this clearer
as they are not really part of the IR (they are less fundamental than
SIL).
- Error reporting is also something for other analyses, not part of IR.
Moved a bunch of modules related to that to absint/.
- Same for ProcnameDispatcher
- biabduction-speficic modules: Objc_models, BiabductionModels
- test-determinator-specific modules: JProcname
Reviewed By: ezgicicek
Differential Revision: D21722368
fbshipit-source-id: b28e9bdac
Summary:
Android OS calls certain overridden class methods always on the UI thread. The function changed here attempted to build a list of all these methods, one by one. It's much more complete to simply consider a method as callable on the UI thread if it's an override of an Android library method, and it starts with "on". Only a single instance is known not to obey this pattern, so it's easier to blacklist than to whitelist.
Also clarify the name to `is_android_lifecycle_method`.
Reviewed By: ezgicicek
Differential Revision: D21703365
fbshipit-source-id: 41ca3e998
Summary:
In inferbo's domain, `Loc.t` and `Symb.SymbolPath.partial` are defined with the same *field abstraction*. The depth of appended fields were limited in both of them exactly in the same way, e.g. `x.*.field`. Problem is that the implementation related
to the field abstraction are duplicated in their code, which had been synchronized manually. This diff avoids the duplication by adding a `BufferOverrunField.t`.
Reviewed By: ezgicicek
Differential Revision: D21743728
fbshipit-source-id: 4b01d027c
Summary: This is more idiomatic in OCaml and hopefully a bit easier to read. Internally `lazy` will do pretty much the same thing but it also ensures the callback is called at most once.
Reviewed By: artempyanykh
Differential Revision: D21722522
fbshipit-source-id: 00897aaf1
Summary:
This is the same as Exceptions.Checkers. Eventual goal is to stop having
all issues going through the Exceptions layer.
Reviewed By: dulmarod
Differential Revision: D21686937
fbshipit-source-id: bd92fd0ff
Summary:
It seems these were put there even though there is no inter-dependency
with any of the other options.
Reviewed By: skcho
Differential Revision: D21686739
fbshipit-source-id: 6578f55c2
Summary:
I think `Analysis_stops` ought to achieve roughly the same thing (except
that weird filtering logic which I removed).
Reviewed By: dulmarod
Differential Revision: D21686562
fbshipit-source-id: 53d40729f
Summary:
The option was misleading as it only concerns the biabduction analysis.
Moreover, this is a developer option, and one can already see it by
removing filtering altogether. I think this option was added as the
result of a user request, let's see if anyone notices.
Reviewed By: ezgicicek
Differential Revision: D21686526
fbshipit-source-id: ff383a0ca
Summary:
Don't assign different visibilities to the same issue type dynamically,
use different issue types with always static visibility instead. This is
to be able to document the visibility of each issue type.
Reviewed By: dulmarod
Differential Revision: D21686458
fbshipit-source-id: 876ab4157
Summary:
We allow some fields of issues to be defined dynamically, more precisely
when loading AL files. We don't want this to be abused and in particular
we don't want to miss an issue being declared once for a checker and
another time for another as this would be hard to debug.
Also, only register unknown issue types as coming from AL if they
haven't been registered already.
Reviewed By: skcho
Differential Revision: D21685879
fbshipit-source-id: 9e9438a75
Summary: Assigning `nullptr` to `std::function` was causing `NULLPTR_DEREFERENCE` as our model was expecting to get an object in the right hand side of the assignment (`std::function::operator=`) and was dereferencing that object. Assigning `nullptr` to `std::function` removes callable object from it. We model this special case by creating a fresh value.
Reviewed By: skcho
Differential Revision: D21685318
fbshipit-source-id: 2d4af1933
Summary:
- fix compilation errors due to bitrot
- ensure they don't happen again by adding dune files
- make a quick pass through the README
Reviewed By: skcho
Differential Revision: D21684760
fbshipit-source-id: c541f9376
Summary:
It was unused except one place in JsonReports where we disabled
filtering for the Linters category. But, it seems the behaviour is the
same without that since the only filtering this does is for bucketting
for certain bug types, which doesn't include any linters bug types.
Reviewed By: ngorogiannis
Differential Revision: D21683723
fbshipit-source-id: d0555531b
Summary:
That was an interesting way to do things. But let's not. Also the logic
to fill in the CIssue.t should probably do something to check that each
field was provided instead of just filling them with default values but
that's a separate concern.
Reviewed By: ngorogiannis
Differential Revision: D21664619
fbshipit-source-id: d49b74458
Summary:
Problem: issue types can be reported by several checkers. The current
solution is to change the name of the issue, eg `BIABD_USE_AFTER_FREE`.
This doesn't look great for the user.
We already store a "human readable" name for each issue. These need not
be unique. Use this instead in textual output. In order to keep the link
between the text output and the true "issue type", eg to pass to
`--disable-issue-type`, also print the `unique_id` part of the issue in
the summary:
```
examples/hello.c:12: error: Null Dereference
pointer `s` last assigned on line 11 could be null and is dereferenced at line 12, column 3.
10. void test() {
11. int* s = NULL;
12. *s = 42;
^
13. }
Found 1 issue
Issue Type(ISSUED_TYPE_ID): #
Null Dereference(NULL_DEREFERENCE): 1
```
We could also print the issue id in each report but that looks worse.
Other tools use numbers for issue ids, but these are not descriptive at
all, eg `--disable-issue-type 86` is not very telling.
Reviewed By: skcho
Differential Revision: D21663957
fbshipit-source-id: 506b0fda9
Summary:
- avoid creating issues just to look up their `unique_id` in the set
- avoid `let _ =` since it can hide partial applications
- delete outdated comment
Reviewed By: skcho
Differential Revision: D21663959
fbshipit-source-id: e50d02447
Summary:
Introduce BIABD_ prefixes for a few issue types that were duplicated
between analyses, and also prefix the lab exercise issue type to avoid
sharing with biabduction.
Reviewed By: ngorogiannis
Differential Revision: D21660226
fbshipit-source-id: 3435916e6
Summary:
Consider the below program,
```
const int gvar = 0;
enum {
cvar = gvar + 1,
};
bool dangling_cvar(int x) {
for (int i = 0; i < cvar; i++){
}
}
```
In the prune node, we don't have `cvar` but its inlined version, i.e. we have ` i < n$2 + 1` and the variable `n$2` is defined not in predecessor nodes to the prune node (as normally one would expect) but in a separate dangling node (see the {F236910156})
:
```
6: BinaryOperatorStmt:Add n$2=*&#GB<test.cpp|ice>$gvar:int [line 38, column 10]
```
When computing the control var of this loop, previously we gave up and simply raised an error.
With this diff, let's handle this case by looking inside this dangling node.
Reviewed By: skcho
Differential Revision: D21525569
fbshipit-source-id: bd4371493
Summary: Argument `filter_kind` is only ever set to `Auto` by the clang integration.
Reviewed By: jvillard
Differential Revision: D21685943
fbshipit-source-id: ebeb04409
Summary:
`Buck.parse_command_and_targets` is never called with a `filter_kind:No` argument.
Open variants are not great for detecting dead code.
Reviewed By: jvillard
Differential Revision: D21685076
fbshipit-source-id: 68a89ef65
Summary:
`partition` always constructs two new maps, which is expensive when
there are a lot of entries. Let's avoid it if possible.
Reviewed By: jvillard
Differential Revision: D21684298
fbshipit-source-id: a8674d358
Summary: The list of source files is only needed in the scheduler process, not in the children workers.
Reviewed By: ngorogiannis
Differential Revision: D21662486
fbshipit-source-id: 9c5be13b5
Summary: Without having the added jar files in the classpath, Tenv cannot pick up the type/inheritence info.
Reviewed By: jvillard
Differential Revision: D21662402
fbshipit-source-id: c149356c9
Summary:
## Problem
In method specialization, we don't translate the loads of specialized blocks (e.g. `n$0 = block:_fn_`) and only add them to the id map. Later on, when the block is called with arguments (`n$0(arg1,..argn))` we lookup the id and use the substitution for the block. However, this means, if the program uses the id loading the block (n$0) anywhere else in the program, we have no declaration for it.
## When does this happen?
For blocks that return a nullable result, objC programs usually do a null check as in the following example:
```
typedef id _Nullable (^BlockType)(id object);
+ (void)useBlock:(int) x
myBlock:(BlockType)myBlock{
if (myBlock){
myBlock(x);
}
}
+ (void)callUseBlock{
[X useBlock 1 myBlock:^id(id object) {
return nil;
}];
}
```
Here, method specialization currently ignores the loads of this block (`n$0=*&myBlock:_fn_(*)`) which results in having variables in prune nodes that are not defined anywhere in the CFG (like `n$0`).
This confuses control variable analysis when the conditional is wrapped in a loop because it cannot lookup where `n$0` is coming from.
## Fix
This diff fixes the issue by translating the loading of the blocks.
Reviewed By: dulmarod
Differential Revision: D21642924
fbshipit-source-id: 2bc0442ff
Summary: In the previous code, `old_from_new_` was not used in the result.
Reviewed By: jvillard
Differential Revision: D21641385
fbshipit-source-id: 09e12e106
Summary:
Add an extra argument everywhere we report about the identity of the
checker doing the reporting. This isn't type safe in any way, i.e. a
checker can masquerade as another. But, hopefully it's enough to ensure
checker writers (and diff reviewers) have a chance to reflect on what
issue type they are reporting.
Reviewed By: ngorogiannis
Differential Revision: D21638823
fbshipit-source-id: b4a4b0c0a
Summary:
Before: `RegisterCheckers` activates each checker based on a boolean
condition about which other checkers can enable it, eg for pulse:
```
(* registerCheckers.ml *)
active= Config.(is_checker_enabled Pulse || is_checker_enabled Impurity)
```
After: `Checker` declares for each checker the list of its dependencies,
eg for impurity:
```
(* Checker.ml *)
name= "impurity";
activates= [Pulse]
```
Now `Config` computes for each checker whether it was transitively
activated by other checkers or not. It saves us from having to encode
the logic from before everywhere we want to know "is checker X
running?"; this was prone to errors.
It will also allow us to display which checkers actually run to the user
more easily.
Reviewed By: ezgicicek
Differential Revision: D21622198
fbshipit-source-id: 004931192
Summary:
A buck integration for capturing simultaneously clang and java targets.
Just like the java-specific `JavaGenruleCapture` integration, it relies on
dummy targets that depend on the flavoured clang versions.
For example, a `cxx_library` target named `//clang:hello` will have an associated target
called `//clang:hello_infer` that depends on `//clang:hello#infer-capture-all`,
and whose output is a text file containing the output path of the dependency.
Reviewed By: jvillard
Differential Revision: D21620458
fbshipit-source-id: 23919387b
Summary:
`ocamlc` didn't tell us but there are a bunch of dead exceptions in
`Exceptions.ml` that translate into dead issue types.
Found with:
```
for ex in $(grep -o -e '^exception [^ ]*' infer/src/IR/Exceptions.mli | cut -d ' ' -f 2); do git grep -q -e '\braise .*'$ex || git grep -q -e 'Exceptions\.'$ex || echo $ex; done
```
Reviewed By: skcho
Differential Revision: D21618645
fbshipit-source-id: f60a3f445
Summary:
The eventual goal is to document issue types and checkers better, in
particular which issue types "belong" to which checkers. (note:
Currently some issue types are reported by several checkers.)
The plan is to associate a list of "allowed" checkers to each issue type
and (not in this diff) raise a runtime exception if a checker not in
that list tries to report that issue. Hopefully tests cover all the use
cases and there are no surprises. I've filled in the lists by
`git grep`ing which checkers used which issue types in their code.
Reviewed By: ngorogiannis
Differential Revision: D21617622
fbshipit-source-id: 159ab171f
Summary:
This seems to make sense as it's a separate analysis (that depends on
biabduction). This introduces unpleasant `|| is_checker_enabled TOPL`
whenever we try to figure out if biabduction will run. I think this is a
more general problem that deserves a more general solution to express
the fact that checkers can depend on others, so that, eg,
`is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will
address in another diff.
Reviewed By: ngorogiannis
Differential Revision: D21618460
fbshipit-source-id: 8b0c9a015
Summary: Later on, this can be changed again or made customizable.
Reviewed By: artempyanykh
Differential Revision: D21618730
fbshipit-source-id: fe517c766
Summary: Filenames can contain spaces, so we need to split on the first ' '
Reviewed By: jvillard
Differential Revision: D21618408
fbshipit-source-id: b1e472d18
Summary: A few misformattings have slipped through in to the repo.
Reviewed By: jvillard
Differential Revision: D21583050
fbshipit-source-id: ded0c5dde
Summary:
We stopped relying on an external perf data file to determine which functions are on the cold start. Let's remove this issue now.
NB: Keeping the `--perf-profiler-data-file` as deprecated to prevent issues on the CI and prod.
Reviewed By: skcho
Differential Revision: D21594150
fbshipit-source-id: faa58782d
Summary:
This is to be able to run the Java source file parser (that detects the position of class definitions and other things) on individual .java files for debugging.
Use with `infer --java-debug-source-file-info SomeFile.java`.
Reviewed By: ngorogiannis
Differential Revision: D21594327
fbshipit-source-id: 2f6d747b7
Summary:
Start with tests about dynamic dispatch to test the upcoming
pre-analysis.
Reviewed By: ezgicicek
Differential Revision: D21594496
fbshipit-source-id: 1771ea968
Summary:
Pulse is disabled by default anyway so it's safe to enabled it for Java
too.
Also noticed that OCaml is smart enough not to need `Language.` in
frontend of `Clang`/`Java` in all of registerCheckers.ml so delete
these.
Reviewed By: ezgicicek
Differential Revision: D21594364
fbshipit-source-id: 4b561c9a0
Summary:
- Move code out of Buck that is specific to infer flavors.
- Move capture function and sundry from Driver to the new module.
Reviewed By: jvillard
Differential Revision: D21592276
fbshipit-source-id: 9bef89e8f
Summary:
Welp, that was an *old* file. Originally to emit odoc for the Java
frontend.
Reviewed By: dulmarod
Differential Revision: D21594244
fbshipit-source-id: b9ba078c0
Summary:
This function had been computing the name for ObjC methods wrong, with only the class name. This was causing wrong error messages in Pulse.
The main issue was that `Procname.to_simplified_string` was writing `Classname::methodname` for ObjC methods, which is not the convention. This confused the `hashable_name` funtion. So changing the method name to `Classname.methodname` which is more standard, and this also fixes `hashable_name`.
Reviewed By: ngorogiannis, jvillard
Differential Revision: D21570880
fbshipit-source-id: 13ed62cf8
Summary: In an intra-procedural analysis, we assume that parameters passed by reference to a function will be initialized inside that function. To do that we use the type information of a formal parameter to initialize the fields of the struct. This was causing false positives if the formal parameter in function signature had type `void*`. To solve this, we used type information from local variables instead. However, we also get false positives for any kind of pointer if we use cast. We fix this by using type information of local variables as in `void*` case.
Reviewed By: jvillard
Differential Revision: D21522979
fbshipit-source-id: 4222ff134
Summary:
The documentation had gone out of sync with the new library names. Add
or copy some short documentation for the main libraries, i.e. all of
them except individual analyses (and scripts, third party, ..).
The idea is that each library has some toplevel documentation
`infer/src/<library_dir>/<LibraryName>.mld` that is linked to from the
main entry point of the document infer/infer.mld. We can link to some
important modules for each library from within their toplevel
documentation, then the actual documentation should live inside the
.mli's of the modules of the library as appropriate.
Hopefully this leads to better documentation over time. At least now we
can write some docs and they'll end up somewhere nice. Lots can be
improved still at this point.
Reviewed By: ngorogiannis
Differential Revision: D21551955
fbshipit-source-id: 69a0cfa44
Summary:
Previous translation of enum constants were wrong since they assumed that the enum constant didn't include any global variable (hence they just looked up the enum exp from the map, forgetting to tie the respective instructions into the cfg).
```
const int gvar = 0;
enum {
evar = gvar,
};
int dangling() {
return evar;
}
```
as a result, the CFG was missing the instruction for the load of the `gvar`.
{F237004587}
This diff fixes this issue by hooking up the instructions that load the enum constant in to the CFG. Note that in this example, it is only a load instruction but there could be more instructions (e.g. if we had `gvar > 1`, we would have prune +join).
{F237004493}
Reviewed By: ezgicicek
Differential Revision: D21549781
fbshipit-source-id: 525534fb2
Summary:
Just like `CFBridgingRelease` we want to be able to model functions that are specific to a given codebase that make a transfer of memory ownership so that developers don't need to worry about releasing that memory anymore, and hence, we don't want to report leaks on that memory.
Things get a little more complicated, because some of the functions we want to model are in a specific namespace, so with this flag we take both cases into account, when we are dealing with namespaces or not.
Reviewed By: jvillard
Differential Revision: D21404409
fbshipit-source-id: c36bd7afc
Summary:
Ever since deadcode/dune stopped being a dune.in file that created the
dune file on the fly, `make check` stopped working because it now tried
to build the "deadcode" executable but usually all_infer_in_one_file.ml
isn't around and so it fails. Only create deadcode/dune when needed to
avoid dune taking deadcode/ into account on most operations.
Reviewed By: ezgicicek
Differential Revision: D21528811
fbshipit-source-id: 040e4c138
Summary:
Before total dune-ification we could tell if a dune file was in OCaml or
lisp syntax by looking at its filename only: all OCaml files ended in
".in". But now this isn't the case anymore so we should read the first
line to figure it out instead.
Reviewed By: skcho
Differential Revision: D21544434
fbshipit-source-id: 19296676a
Summary: Currently we get false positive if we apply `operator--` to the `end()` iterator. To solve this, we model iterator `operator--` not to raise an error for the `EndIterator` invalidation, but to create a fresh element in the underlying array.
Reviewed By: ezgicicek
Differential Revision: D21476353
fbshipit-source-id: 5c722372e
Summary:
It is undefined behavior to dereference end iterator.
To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself.
Reviewed By: ezgicicek
Differential Revision: D21178441
fbshipit-source-id: fd6a94b0b
Summary: We mistakenly invalidated the set element which causes spurious vector invalidation errors. Instead, we should modify it without any invalidation.
Reviewed By: jvillard
Differential Revision: D21521943
fbshipit-source-id: 67963967e
Summary:
This will is useful for understanding and debugging file level analysis
flow.
Reviewed By: jvillard
Differential Revision: D21449240
fbshipit-source-id: 7c259674b
Summary:
This diff adds semantics of assume null, heuristics. When `assume(x == null)`, it removes the
methods called on the builder `*x` from the abstract state.
```
x -> {p}
p -> {method1 called}
assume(x == null)
x -> {p}
```
This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder
object, which cannot imply that the object `p` does not exist in the concrete semantics. The
unsoundness may appear when there is an alias (see the FP test added).
Reviewed By: ezgicicek
Differential Revision: D21502923
fbshipit-source-id: 2e392bd89
Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array.
Reviewed By: skcho
Differential Revision: D21448322
fbshipit-source-id: 7d44354b5
Summary:
These 2 methods are automatically supplied for all enums, with
predefined behavior and nullability: https://www.geeksforgeeks.org/enum-in-java/
(Note that they are not part of java.lang.Enum class).
This will allow using them in unvetted third part and under strict mode.
Reviewed By: artempyanykh
Differential Revision: D21501716
fbshipit-source-id: 104082d15
Summary:
The only thing keeping this module alive were unit tests, proving once
and for all that unit tests are bad.
Reviewed By: ngorogiannis
Differential Revision: D21451855
fbshipit-source-id: e63995732
Summary:
- move unit/clang/ to clang/unit/ and make it a dune library
- move unit/nullsafe/ to nullsafe/unit/ and make it a dune library
- make unit/ a dune library
- inline most of dune.common.in into dune.in and make more explicit
rules for each binary as they don't depend on the same libraries
- move inferunit from unit/ to ./ like the other toplevel binaries
Reviewed By: skcho
Differential Revision: D21440822
fbshipit-source-id: 075c693e0
Summary:
Using the same trick as for the java frontend: define a dune library
that takes either all the modules in the directory (except possibly
stubs) or none of the modules (except possible stubs).
In order to break the circular dependency between al/ and clang/,
introduce a dirty callback in clang/.
Reviewed By: dulmarod
Differential Revision: D21440823
fbshipit-source-id: ac6b40b4e
Summary:
Kill java_stubs/ with this one easy trick:
- java/dune contains either the "normal" modules or just the
JavaFrontendStubs module
- libraries that depend on java need to open JavaFrontendStubs if java
is disabled to bring the expected modules from java/ into their
namespace
Also needed to move biabduction/Prover.Subtyping_check to
absint/SubtypingCheck because the Java frontend was using it.
Reviewed By: ngorogiannis
Differential Revision: D21435937
fbshipit-source-id: af957253a
Summary:
Because in the real semantics CFRelease can be used more than once, and also the variables can be used after CFRelease in general, modelling this as `free` causes many `USE_AFTER_FREE` errors. Now we change the model to not add the `Invalid CFree` attribute, but to just remove the `Allocated` attribute. So we can model memory leaks in the simple case of `Create` and not `CFRelease` before going out of scope, but we avoid the `USE_AFTER_FREE`.
Since the model for CFRelease now diverges from free, changed the command line option for modelling to `pulse-model-release-pattern`.
Reviewed By: jvillard
Differential Revision: D21324895
fbshipit-source-id: ab323d981
Summary:
This diff suppresses the internal error on mismatched signedness. It happens usually when inferbo
has incomplete type information. Since it does not seem to fix in the near future, let's suppress
them, not to hide other internal errors.
Reviewed By: jvillard
Differential Revision: D21455062
fbshipit-source-id: 4562bb177
Summary:
OSX filesystem gets confused by its case-insensitivity and the library
trick of having TOPL.ml (vs the existing Topl.ml).
Reviewed By: skcho
Differential Revision: D21456696
fbshipit-source-id: 2f6ffc2fb
Summary:
Needed to move some "Differential" files out of the way. This makes
sense I think: backend/ is only about orchestrating the various
checkers.
Reviewed By: ngorogiannis
Differential Revision: D21431968
fbshipit-source-id: 14fad8b88
Summary:
Last checker for good. Updated the README of the lab to reflect changes.
Delete now-defunct SummaryPayload: all checkers now behave in a
functional manner as far as summary payloads are concerned.
Reviewed By: ngorogiannis
Differential Revision: D21426550
fbshipit-source-id: 2b52b9f5b
Summary:
The global analysis is doing funky stuff directly with `Summary.OnDisk`.
In order to make starvation/ its own dune library this part needs to
either use ondemand or moved elsewhere. Let's do the latter for now to
avoid changing the behaviour in the middle of the refactoring.
Reviewed By: ngorogiannis
Differential Revision: D21425699
fbshipit-source-id: ab9e2f429
Summary:
It started with wondering which function the "O(1)" comment was about
but I ended up deleting `is_singleton` because it's unused and it can be
easily re-implemented.
Reviewed By: ngorogiannis
Differential Revision: D21425225
fbshipit-source-id: 5ee3e189c
Summary:
Also ondemand doesn't need to call Topl itself after an analysis.
Inline last call site of SummaryReporting (ondemand.ml) and delete the
file.
Reviewed By: ngorogiannis
Differential Revision: D21424386
fbshipit-source-id: 064f4e261
Summary:
- make quandary an `interprocedural`
- move quandary traces to absint/ since they are also used at least by
SIOF
- no more `Summary.OnDisk.dummy` :')
Reviewed By: ngorogiannis
Differential Revision: D21408391
fbshipit-source-id: cc53d2c6c
Summary:
There is a case where the class name is "A$1$B$2".
In this case, we would correctly say it is an anonymous class, and
return A$1$B as user defined, which is bad: now we can get the outer
class which will be A$1 that will be anonymous again.
This was leading to tricky bugs.
Now, get_user_defined_class name will return something that is indeeed
contains only user defined names.
There is one tricky pathological case left: when the outermost class is
anonymous, which can in theory occur. This might lead to other tricky
bugs, so the follow up will be to rewrite API of JavaClassName.t so that
this case is made clear for the client.
But lets unbreak nullsafe fore now first.
Reviewed By: ngorogiannis
Differential Revision: D21449686
fbshipit-source-id: b0ba4702e
Summary: This will allow us to track cases when this assert fires
Reviewed By: ngorogiannis
Differential Revision: D21427776
fbshipit-source-id: 96b6d7c3b
Summary: This diff gets only one disjunct from blacklisted callee, in order to avoid OOMing in specific cases.
Reviewed By: jvillard
Differential Revision: D21406023
fbshipit-source-id: f9214c9c6
Summary:
Needed to move a bunch of files around to make this happen. Notably,
moving "preanal.ml" outside of checkers/ into backend/ since it needs to
modify the proc desc in the summary. Also hoisting goes to cost/.
Reviewed By: skcho
Differential Revision: D21407069
fbshipit-source-id: ebb9b78ec
Summary:
An easy one. One subtlety: I needed to name the library "pulselib"
instead of "pulse" because dune got confused by the Pulse.ml module.
Reviewed By: skcho
Differential Revision: D21401815
fbshipit-source-id: 05e75b1fa
Summary:
Main change: needed to cut the dependency of inferbo on pulse, since
pulse will need to depend on inferbo. Achieved by changing the ad-hoc
"PulseValue" into a little less ad-hoc "ForeignVariable" variant.
Reviewed By: skcho
Differential Revision: D21401816
fbshipit-source-id: bb341b9ff
Summary:
Changing inferbo required changing all the analyses that depend on it
too. This introduces a new feature of the the new framework: the ability
for the checkers to read other analyses' payloads in a more functional
way.
Reviewed By: ezgicicek, skcho
Differential Revision: D21401819
fbshipit-source-id: f9b99e344
Summary:
An easy one. Will be needed eventually to make checkers/ its own dune
library.
Reviewed By: ngorogiannis
Differential Revision: D21401818
fbshipit-source-id: 64e8a4bf4
Summary:
`RegisterCheckers` is now doing a bunch of work to convert the new-style
checkers to the good old Callbacks datatypes. Extract the conversion
code into another module before more is added. A good opportunity to
document them.
Reviewed By: ezgicicek
Differential Revision: D21401817
fbshipit-source-id: 4cba3aa7b
Summary:
This module needs to be above all checkers since it knows about all the
checkers; put it at the same level of ondemand and callbacks.
Reviewed By: ezgicicek
Differential Revision: D21401821
fbshipit-source-id: f40dba6dd
Summary: Build tool wrappers sometimes have issues when their output streams are redirected to those of infer's while one of those streams is read and used in infer. This diff side-steps this problem by always redirecting the stream of interest to a file (which also helps in debugging), while logging the other stream through `Logging.progress`.
Reviewed By: jvillard
Differential Revision: D21404736
fbshipit-source-id: 04c92799c
Summary:
- move a few files from checkers/ so that nullsafe can depend on them
- nullsafe depends on a few files in biabduction/ via Errdesc (not the
biabduction analysis itself but some datatypes and functionality):
- when possible, I've moved the individual functions elsewhere, in absint/Decompile.ml
- nullsafe still depends on a function in Errdesc that unfortunately
depends on a bunch of biabduction datatypes like Prop(!) and some
other functionality that for now is embedded in biabduction
(substitution in SIL instructions).
Reviewed By: mityal
Differential Revision: D21351906
fbshipit-source-id: 757528120
Summary: So it can be used by dune libraries without depending on backend/.
Reviewed By: dulmarod
Differential Revision: D21351908
fbshipit-source-id: d288f9179
Summary:
Easy cleanup. The tenv is now part of the analysis_data that is in the
closure passed to the Dataflow framework.
Reviewed By: dulmarod
Differential Revision: D21351907
fbshipit-source-id: 592542c06
Summary:
This turned into a pretty big refactoring: the
`IntraproceduralAnalysis.t` needs to be passed around through quite a
few functions. These functions usually depended on
tenv/proc_desc/proc_name that are already in the `analysis_data` so
refactored that too (checking that these were indeed the same as in the
`analysis_data` record (using my own eyeballs). Interestingly there is
one place where we actually turn the analysis to other proc descs than
the original one in eradicate.ml so I've added a small comment there.
Reviewed By: mityal
Differential Revision: D21351909
fbshipit-source-id: 6e6330e5b
Summary: The contract for reporting races in C++ is to flag races between writes under lock with reads without a lock. This diff restores that contract which had been violated by recent changes.
Reviewed By: jberdine
Differential Revision: D21383876
fbshipit-source-id: 6a84e1506
Summary: As per title. Also, hide most deduplication functionality inside a module.
Reviewed By: skcho
Differential Revision: D21382377
fbshipit-source-id: d979f5b54
Summary:
This diff changes way we treat classes w.r.t. to Nullsafe modes when
issuing meta-issues.
Previously, we considered nested class independently of the outer one.
This was leading to a tricky case: when the class is clean but nested
class needs fixing, meta-info told that class can be Nullsafe.
This is counter-intutive and lead to problems when users tried to follow
wrong nullsafe suggestions for this case.
After this diff we:
1. Start calculating meta-issues only on the outermost level. This will simplify
reasoning about nullsafe stats.
2. Aggregate all nested issues counters to corresponding outer-level class.
Among others, CLASS_CAN_BE_NULLSAFE Advice will finally become
actionable in all known cases.
Reviewed By: artempyanykh
Differential Revision: D21353607
fbshipit-source-id: a17c6958a
Summary:
That function was testing if a proc is defined (ok) and if so if it also
had no summary. The second check is wrong because it could be that the
function hasn't been analysed yet. We should call "Ondemand" instead.
But, it seems like a weird check so I just deleted it and replaced is
with just the "is defined" check.
Renamed the "is_library" field in typeOrigin to "is_defined" to better
reflect the expectations. While I was at it, inlined record type
definitions in `TypeOrigin.t`. They were already inlined except for 2!
Reviewed By: dulmarod
Differential Revision: D21351453
fbshipit-source-id: 1acc7ff90
Summary:
This is to eventually remove eradicate's dependency on Ondemand and
other modules in backend/.
Reviewed By: mityal
Differential Revision: D21351456
fbshipit-source-id: 1c4723cbc
Summary: Improve determinism by sorting the order of capture databases before merging.
Reviewed By: jvillard
Differential Revision: D21378208
fbshipit-source-id: 9c82d9d56
Summary:
These exceptions were caught earlier before but D21257474 made absint
log an error every time before reraising them.
The exception type had to move to IR/ or absint/, so I moved
"SchedulerTypes" to "absint/TaskSchedulerTypes" and added the restart
scheduler's exception there. There is already a "Scheduler.ml" file in
absint/ so to address the ambiguity I added "Task" in front of that one.
Reviewed By: ngorogiannis
Differential Revision: D21348593
fbshipit-source-id: 58055c9b7
Summary: Factor out common behaviour and error handling in executing buck commands, while protecting from `SIGQUIT` which results in thread dumps appearing in standard output.
Reviewed By: jvillard
Differential Revision: D21331696
fbshipit-source-id: d3b6abe2d
Summary:
List of things happening in this unreviewable diff:
- moved PulsePathCondition to PulseSledge
- renamed --pulse-path-conditions to --pudge
- PulsePathCondition now contains all the arithmetic of pulse
(inferbo+concrete intervals+pudge). In particular, moved arithmetic
attributes into PulsePathCondition.t. PulsePathCondition plays the
role of PulseArithmetic (combining all domains).
- added tests for a false positive involving free()
- PulseArithmetic is now just a thin wrapper around PulsePathCondition
to operate on states directly (instead of on path conditions).
- The rest is mostly moving code into PulsePathCondition (eg, from
PulseInterproc) and adjusting it.
Reviewed By: jberdine
Differential Revision: D21332073
fbshipit-source-id: 184c8e0a9
Summary:
We have a common entry point where we skip analysis in nullsafe.
This logic is copied from `Reporting.log_issue_from_summary`.
I believe this should not exist in Reporting: it is not the right place
to decide whether to suppress issues: we should not try to report it in
first place.
Because of that we falsely report "needs improvement" meta-issue while
we don't issue any (they were suppressed but participated in needs
improvement count calculations).
Now this change will make meta-issue to be synced with what the user
actually sees.
Down the line we should have a more reliable fix for that.
So far I reviewed suppressing code and looks like we should not suppress
anything else (unless explicitly SuppressLint-ed, which is fine).
Reviewed By: artempyanykh
Differential Revision: D21328634
fbshipit-source-id: 120ce06d1
Summary:
Add a new data structure and use it for the map of memory accesses to
limit the number of destinations reachable from a given address. This
avoids remembering details of each index in large arrays, or even each
field in large structs.
Reviewed By: skcho
Differential Revision: D18246091
fbshipit-source-id: 5d3974d9c
Summary:
Kotlin has an experimental support for [JSR-305 custom nullability
qualifiers](https://github.com/Kotlin/KEEP/blob/master/proposals/jsr-305-custom-nullability-qualifiers.md).
Annotating Nullsafe in a special way makes kotlinc recognize it as
such custom nullability qualifier and therefore treat types coming
from Nullsafe Java classes **not** as platform types, but rather
proper nonnull/nullable, which affects:
1. Generated bytecode (more thorough null-checks).
2. Type inference in the IDE.
NOTE re: p.1: one might expect that with properly annotated Java code
Kotlin would avoid inserting runtime checks. This is not how
Kotlin-Java interop works - in reality Kotlin does even more runtime
checking for Java code annotated as Nonull, which IMO is a good
thing, since you can't trust Java anyway.
Reviewed By: mityal
Differential Revision: D21278440
fbshipit-source-id: d0598738a
Summary:
The idea was to keep track of why we know certain facts but actually
these traces are never read. Other arithmetic facts (BoItv and the path
condition) don't have histories so remove them from concrete intervals
too.
Reviewed By: dulmarod
Differential Revision: D21303353
fbshipit-source-id: eecf07b05
Summary:
It suppresses cost reports of access methods, anonymous class methods, and auto-generated methods.
For those methods, this diff blocks reporting both expensive
issue (`EXPENSIVE_COLD_START/_UI_THREAD`) and complexity increase issue (`COMPLEXITY_INCREASE`).
Reviewed By: jvillard
Differential Revision: D21303068
fbshipit-source-id: 1c9533956
Summary:
The C++ tests were a bit of a mess. This diff tries to enforce the following principles:
- mark every function with `_ok` or `_bad` so that when a function appears in `issues.exp` it's easy to figure out the intention;
- mark every false negative and positive with `FP_` and `FN_` to document expectations;
- make every function access one field and participate in at most one issue report so that it's easier to assess changes.
Reviewed By: jvillard
Differential Revision: D21278627
fbshipit-source-id: 9698f716f
Summary:
We were invalidating "*(vec.__infer_backing_array)" instead of the
address of the field itself.
Reviewed By: ezgicicek
Differential Revision: D21280357
fbshipit-source-id: 48b984800
Summary:
The directory was created to have several sets of nullsafe tests but
there is only one in the end. Remove the redundant "-default".
Reviewed By: mityal
Differential Revision: D21300205
fbshipit-source-id: 46ed8b032
Summary:
The directory names had some interesting variety due to historical
reasons.
- {c,cpp,objc,objcpp}/errors/ date from the time when infer was only
biabduction
- java/infer/ dates from the time when we had an "--analyzer" option and
"infer" was one of them (sic), and eg another was "eradicate".
- c/biabduction/ dates from the time when the biabduction analysis was
being migrated to the "checkers" (AI) framework. For some reasons the
tests there are not a subset of c/infer/ but seem to be entirely new
tests.
The convention now dictates that we should name all of these
*/biabduction/. This diff moves the existing tests from c/biabduction/
into c/biabduction/misc/.
Reviewed By: mityal
Differential Revision: D21300147
fbshipit-source-id: 516d1cb15
Summary:
The test for the ant integration used to import all of biabduction tests
via a symlink. This is extremely annoying: whenever the biabduction
tests change, so do the ant tests.
Replace the ant tests with a simple single file project.
Reviewed By: ngorogiannis
Differential Revision: D21301450
fbshipit-source-id: 0d67d71d7
Summary:
Based on a shrewd observation by mityal, we can copy a little bit of
code from nullsafe and cut the dependency between biabduction and
nullsafe. The trick was to notice that biabduction doesn't use the full
power of the functions it was calling.
Reviewed By: mityal
Differential Revision: D21282656
fbshipit-source-id: 906847c26
Summary:
By far the most annoying thing to migrate. There will be a bunch of
these diffs.
Reviewed By: dulmarod
Differential Revision: D21261635
fbshipit-source-id: 0f290dd96
Summary:
This shows how the strategy for making each analysis its own library
looks like. Starting with biabduction since it's one of the worst ones.
A checker cannot depend on ProcData (in its current form) as it contains
a Summary.t. We don't want to change all the analyzers at once so let's
make up a new type. The new type also contains callbacks for Ondemand
since a checker that is its own dune library cannot call Ondemand
directly either (because Ondemand needs Summary.OnDisk).
Once all checkers are migrated we should be able to reclaim the
callbacks set up by callbacks.ml in exchange for these new callbacks,
therefore achieving a neutral callback karma.
Reviewed By: dulmarod, skcho
Differential Revision: D21261638
fbshipit-source-id: fa91ca50f
Summary:
Looks like this one was already causing circular dependency issues!
Saves threading the callback through *many* functions.
Reviewed By: ngorogiannis
Differential Revision: D21261636
fbshipit-source-id: 2b23aa07d
Summary:
- needed to make biabduction/ its own library as it shouldn't depend on
backend/Printer as a result
- it's a higher level of abstraction
Changed NodePrinter to not swallow biabduction timeouts, thereby
removing its footgunness.
Reviewed By: ngorogiannis
Differential Revision: D21261645
fbshipit-source-id: 592526d85
Summary:
absint/ is its own dune library. There was one last obstacle: we need
callbacks to `NodePrinter`. We'll add more to `AnalysisCallbacks` in future
diffs.
Reviewed By: ngorogiannis
Differential Revision: D21257476
fbshipit-source-id: 3a2ddef14
Summary:
`State` is used by the AI framework, which isn't supposed to know about
biabduction/. Split the biabduction-specific parts into
biabduction/State.ml and keep the rest in absint/AnalysisState.ml.
Reviewed By: ngorogiannis
Differential Revision: D21257470
fbshipit-source-id: e01d1fed3
Summary:
`ProcData.t` contains a `Summary.t`. Eventually we want to fix this too
so that checkers don't depend on backend/, i.e. on all the other
checkers via Summary.ml. But in order to migrate progressively we can
first migrate absint/ and one step on the way is for it to not know what
kind of analysis data it is passing around.
This extra flexibility only costs us passing an extra `Procdesc.t` in a
couple more functions so it's actually not a bad change in itself.
Reviewed By: ngorogiannis
Differential Revision: D21257466
fbshipit-source-id: a91f7b191
Summary:
This is needed to make absint/ its own dune library. Modules in absint/
cannot depend on modules in backend/. This is because backend/Summary.ml
depends on *all* the (inteprocedural) analyses since its stores elements
of their domains. But analyses are supposed to depend on absint/ to
use the AI framework and others. Thus absint/ cannot depend on backend/
otherwise it creates a dependency cycle.
Right now infer builds with this cycle because we consider all these
directories to be one library and there is no dependency cycle between
the individual modules, but making absint/ a library makes the situation
coarser.
One actual change in there: one function in PatternMatch was specific to
nullsafe and was moved there.
Reviewed By: ngorogiannis
Differential Revision: D21257467
fbshipit-source-id: 42af43315
Summary:
This is a step in disentangling the various analyses: that file used to
make every checker on biabduction because of a few of its functions that
use biabduction datatypes.
Split reporting.ml into:
- Reporting.ml: the functions all checkers need to report errors. This
is put in absint/ with the other files that are needed by all
checkers.
- SummaryReporting.ml: functions that need to depend on Summary.ml
(useful for later). This is put in backend/ where Summary.ml lives.
- BiabductionReporting.ml: for the biabduction analysis
The rest of the changes are renames to use the appropriate module
amongst the above.
Reviewed By: ngorogiannis
Differential Revision: D21257468
fbshipit-source-id: fa28cefbc
Summary:
This doesn't depend on the java frontend, as we can see from the fact
that it was symlinked from java/ into java_stubs/. So instead of having
these fake stubs (double negation!) put that file in IR/.
Reviewed By: ngorogiannis
Differential Revision: D21257469
fbshipit-source-id: 1c9e88bcc
Summary:
We re-raise all exceptions a few lines below already so this is not
needed. In fact it prevents us from writing the html cleanly before
hitting the exception, which was bad.
Reviewed By: ngorogiannis
Differential Revision: D21257474
fbshipit-source-id: 0b7e2b8d3
Summary:
This fixes a long-standing TODO. I re-ordered the lines by:
- first putting each entry on a single line (replacing "^J " -> " "
in emacs)
- then using emacs' M-x reverse-region
- then auto-formatting again
Reviewed By: skcho
Differential Revision: D21257475
fbshipit-source-id: 91b780a5d
Summary:
The are already ignored by git and can be useful to 1) debug when the
deadcode Makefile has a bug, and 2) help incremental analysis.
Reviewed By: ngorogiannis
Differential Revision: D21277538
fbshipit-source-id: dc6394ed7
Summary: We currently don't support abducing the spec that we need to delete an attribute, that makes the model for `CFBridgingRelease` work les well when it is, for instance, wrapped in a method. We show examples of how this doesn't work at the moment.
Reviewed By: jvillard
Differential Revision: D21176108
fbshipit-source-id: 79aed7a5d
Summary:
We model `malloc` in Objective-C as `malloc_not_fail` I think because the null case is not normally handled in iOS apps because the OS will just killed the app after giving some memory warnings.
So adding `malloc_not_fail` model to Pulse.
Reviewed By: jvillard
Differential Revision: D21278527
fbshipit-source-id: 17a5008fe
Summary:
This translates the construct `ObjCBridgedCastExpr` when the cast_kind is `OBC_BridgeTransfer`, or in syntax, the cast (`__bridge_transfer`).
This cast means that the object is passed from manual memory management to ARC, so one doesn't need to call `release` manually. It is important to model this to avoid false positives.
It translates it as a builtin that we then model in Pulse, the same way we modelled `CFBridgingRelease` which does the same thing.
The name of the builtin is `__free_cf` which is not ideal but I left it like that for compatibility with biabduction. We can change it once we remove this check from biabduction.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D21176337
fbshipit-source-id: 736ceeb9b
Summary:
Good night, sweet prince. This was never used and hasn't seen progress
in a while.
Reviewed By: jberdine
Differential Revision: D21201932
fbshipit-source-id: e6f537b30
Summary:
In the previous diffs, nullsafe behavior was changed to the following:
nested class mode is inherited from the outer class mode.
Though it is possible to e.g. make nested class Nullsafe and outer not,
or make nested class STRICT and outer just LOCAL, this is an edge case
and we don't want to recommend annotating nested classes by default. The
right way is to make outer class Nullsafe instead.
In this decision, we take into account user experience and codebase
readability.
Reviewed By: ngorogiannis
Differential Revision: D21255806
fbshipit-source-id: 0200cb555
Summary:
With this change, set of possibilities will be more actionable. Most
importantly, this will also educate users and make them realize how
Nullsafe trust works.
NOTE: yes, parenthesis are bit clumsy, but it was the easiest way to
make this change and let the phrase remain grammatically correct.
Reviewed By: artempyanykh
Differential Revision: D21231468
fbshipit-source-id: 4b5349fb5
Summary:
As artempyanykh pointed out, exposing trust list might encourage clients to
start writing business logic manipulating with trust lists outside of
NullsafeMode module, which we don't like to happen.
Reviewed By: artempyanykh
Differential Revision: D21230973
fbshipit-source-id: 39bd0b0d8
Summary:
In the previous diff we changed the semantics of nested classes w.r.t.
to Nullsafe.
Let's make it clear if users will attempt to misuse it.
Reviewed By: artempyanykh
Differential Revision: D21230717
fbshipit-source-id: 0ecc0dd06
Summary:
The order of model list is important to understand which model will be dispatched. Previously, the
models were shuffled with no pattern or rule. This diff sorts them and collects them as groups, so
making it easier to anticipate the dispatch.
Reviewed By: jvillard
Differential Revision: D21227541
fbshipit-source-id: 80be46d86
Summary: Similarly to Enum.name, we model Class.getCanonicalName as returning an arbitrary non-empty string.
Reviewed By: ngorogiannis
Differential Revision: D21207120
fbshipit-source-id: 1e2dbd1fd
Summary:
From the user perspective, the current behavior is confusing.
The users intutitively expect the inner class to inherit Nullsafe mode
from the outer one.
Having a class that is Nullsafe but the inner is not is hence dangerous
and misleading.
For the sake of completeness and to support gradual strictification, we
allow the nested class to improse additional strictness. Particularly,
the inner class can be Nullsafe but the outer can be not.
A follow up to this diff will include warnings telling about redundant and wrong usages of nested annotations.
Reviewed By: artempyanykh
Differential Revision: D21228055
fbshipit-source-id: 75755ad1d
Summary:
1. Most of trust list operations are abstract anyway, we don't actually
rely on the fact that this is list
2. Inside NullsafeMode.ml, we effectively need set operations, which is both more
idiomatic to express and Ocaml and faster
3. This will simplify implementation of the next diff which introduces
mode intersect operation
Reviewed By: artempyanykh
Differential Revision: D21207207
fbshipit-source-id: 0c1fc4426
Summary: Iterator invalidation traces were based on vector rather than iterator itself.
Reviewed By: ezgicicek
Differential Revision: D21202047
fbshipit-source-id: 62ce8a488
Summary: The transition function was using a complicated-looking and possibly-inefficient pattern of options for everything, when simple pattern matching with guards is sufficient.
Reviewed By: skcho
Differential Revision: D21179606
fbshipit-source-id: a37f97594
Summary:
Lets move the logic dealing with non-java classes outside of this module
so we can modify it easier in the next diff.
Reviewed By: artempyanykh
Differential Revision: D21204822
fbshipit-source-id: 67b5937bc
Summary:
Because of this bug, we evaluated anonymous class constructors in
Default mode, even if the underlying class was Nullsafe
Reviewed By: artempyanykh
Differential Revision: D21202986
fbshipit-source-id: a31318901
Summary: Specialise the above option to `true` and remove resulting dead code.
Reviewed By: dulmarod
Differential Revision: D21177041
fbshipit-source-id: 4a1c65850
Summary: This option makes RacerD angelic wrt the ownership of returned objects from procedures without summary. This will now be made the default and the option deprecated up the diff stack.
Reviewed By: dulmarod
Differential Revision: D21174676
fbshipit-source-id: 9c48d3d7d
Summary:
We model Enum.name as returing a constant name, rather than getting real field names. We did this
because we couldn't think of any big gains, in terms of analysis precision/performance, from getting
the real names.
Reviewed By: ezgicicek
Differential Revision: D21201730
fbshipit-source-id: a2dc01a44
Summary: This diff revises the models of Collection.set and get to handle its elements.
Reviewed By: ezgicicek
Differential Revision: D21201242
fbshipit-source-id: 9c248453d
Summary:
We ignored allocator models for vectors, and were not able to initialize vectors properly. This diff fixes this issue.
It also adds a test which was a FN before.
Reviewed By: skcho, jvillard
Differential Revision: D21089492
fbshipit-source-id: 6906cd1d1
Summary: D21155014 replaced `skip` call with a Load but this was not right. Instead, let's add a new builtin function (rather than skip) so that other analyses can freely model it as they want.
Reviewed By: jvillard
Differential Revision: D21178286
fbshipit-source-id: c214ccfb0
Summary: Java has this pattern of wrapping non-thread-safe containers in factory methods producing identically-typed results, but wrapped in a synchronised shell. This diff teaches RacerD about some common factory methods and uses the attribute domain to track the dynamic type of their results.
Reviewed By: ezgicicek
Differential Revision: D21155538
fbshipit-source-id: 42ebe6251
Summary: Complete the set of models for java containers that Infer should not report thread safety violations.
Reviewed By: ezgicicek
Differential Revision: D21138280
fbshipit-source-id: 01e1944b6
Summary: Models were partial and/or simply missing (`Map` writes!). Now the modelled containers use inheritance for conciseness (`List` reads are only those not caught by the `Collection` matcher, etc). Also, add URLs to documentation sources.
Reviewed By: ezgicicek
Differential Revision: D21132069
fbshipit-source-id: fefb360f0
Summary: `CFBridgingRelease` and `__bridge_transfer` which I'll model later, transfer the memory model from manual memory ref count to ARC (automatic ref count), so to avoid false positives this needs to be modelled. We can simply remove the Allocated attribute from the state, which means we won't try to track that memory anymore.
Reviewed By: skcho
Differential Revision: D21088218
fbshipit-source-id: 3520a0d59
Summary: This diff suppresses cost issues on lambda and auto-generated procedures, since they were too noisy.
Reviewed By: ezgicicek
Differential Revision: D21153619
fbshipit-source-id: 65ad6dcc3
Summary:
Replace horrible hack with ok hack.
The main difficulty in implementing the disjunctive domain is to avoid
the quadratic time complexity of executing the same disjuncts over and
over again when going around loops:
First time around a loop, assuming for example a single disjunct `d`:
```
[d]
loop body
[d1' \/ d2']
```
Second time around the same loop: the new pre will be the join of the
posts of predecessor nodes, so `old_pre \/ post(loop,old_pre)`, i.e.
`d \/ d1' \/ d2'`. Now we need to execute `loop body` again
*without running the symbolic execution of `d` again* (and the time after
that we'll want to not execute `d`, `d1'`, or `d2'`).
Horrible hack (before): Disjuncts have a boolean "visited" attached
that does its best to keep track of whether a given disjunct is old or
new. When executing a single *instruction* look at the flag and skip the
state if it's old. Of course we have no way to know for sure so it turns
out it was often wrongly re-executing old disjuncts. This was also
producing the wrong results over even simple loops: only the last
iteration would make it outside the loop for some reason. Overall, the
semantics were pretty untractable and shady at best.
New hack (this diff): only run instructions of a given *node* on
disjuncts that are not physically equal to the "pre" ones already in the
invariant map for the current node.
This gives the correct result over simple loops and a nice performance
improvement in general (probably the old heuristic was hitting the
quadratic bad case more often).
Reviewed By: skcho
Differential Revision: D21154063
fbshipit-source-id: 5ee38c68c
Summary:
This is a preparatory diff to make the actual change more readable. This
just moves the code around, trying to change it as little as possible.
Reviewed By: skcho
Differential Revision: D21154065
fbshipit-source-id: e086318c1
Summary:
This makes the API of [instrs] easier to work with at the price of some
duplication in the GADT.
This allows us to construct `[skip]` in `AbstractInterpreter` without
imposing a particular direction. This will make it the next diffs about
a disjunctive domain easier.
Reviewed By: skcho
Differential Revision: D21153694
fbshipit-source-id: f86c180fa
Summary:
We translated the expression `CXXStdInitializerListExpr` naively in D3058895 as a call to
a skip function, with the hope that it would be translated better in the future. However, the naive means that we lose access to the initialized list/array because we are simply skipping it. So, even if we want to model the initializer properly, we have to deal with the skip specially.
This diff tries to solve this problem by removing the skip call whenever
possible. Instead, we translate the underlying array/list as a Load, so
that when it is passed to the constructor, we can pick it up.
For the following initialization:
``` std::vector<int*> vec = {nullptr};
```
Before, we translated it as
```
*&0$?%__sil_tmpSIL_materialize_temp__n$7[0]:int* const =null
n$8=_fun___infer_skip_function(&0$?%__sil_tmpSIL_materialize_temp__n$7:int* const [1*8] const )
n$9=_fun_std::vector<int*,std::allocator<int*>>::vector(&vec:std::vector<int*,std::allocator<int*>>*,n$8:std::initializer_list<int*>)
```
However, this means, `n$8` would be result of something skipped which we can't reason about. Instead, we just pass the underlying initialized array now, so we get the following translation:
```
*&0$?%__sil_tmpSIL_materialize_temp__n$7[0]:int* const =null
n$8=*&0$?%__sil_tmpSIL_materialize_temp__n$7:int* const [1*8] const
n$9=_fun_std::vector<int*,std::allocator<int*>>::vector(&vec:std::vector<int*,std::allocator<int*>>*,n$8:std::initializer_list<int*>)
```
Reviewed By: jvillard
Differential Revision: D21155014
fbshipit-source-id: 75850b1e6
Summary:
It is true that `Info` issues are normally not intended for the end user
and in general should be hidden by default.
However, the current behavior - show them only if `--no-filtering` is
true - is super non-intuitive and complicates already complex reporting
logic.
Lets use the general "enable/disable" mechanism for controlling this.
Reviewed By: jvillard
Differential Revision: D21154140
fbshipit-source-id: 69e4c88e4
Summary:
Computing sledge's equality relation and normalising terms is costly. We
can avoid doing that most of the time by keeping the sledge path
condition lazily evaluated and only forcing it down to a value at two
critical points in the analysis:
1. Summary creation, to avoid storing unsatisfiable pre/posts that will have
to be needlessly executed by callers. This also saves us from having
to serialise the closures involved in the uncomputed form of lazy
values inside the pulse summaries.
2. Before reporting errors we check in the state is in fact satisfiable.
If not we just prune it away at that point.
This yields ~4x speedup on some targets.
Reviewed By: ezgicicek
Differential Revision: D21129759
fbshipit-source-id: a75fdd3bc
Summary:
This is mostly just a type change for now, more changes to come. This
doesn't make thing much faster yet because we force computations pretty
often to check for unsatisfiability (each function call and PRUNE node).
Next diff will build on that.
Reviewed By: skcho
Differential Revision: D21129758
fbshipit-source-id: 72200e2b1
Summary:
When encountering a constant, pulse creates an abstract value (a
variable) to represent it, and remembers that it's equal to it. The
problem is that pulse doesn't yet know how to deal with the fact that
some variables are going to be equal to each other.
This hacks around this issue in the case of constants, within the same
procedure, by remembering which constants have been assigned to which
place-holder variables, and serving those variables again when the same
constant is translated again.
Limitation: this doesn't work across procedure calls as the "constant
maps" are not saved in summaries.
Something to look out for: we don't want to make `if (p == NULL)` create
a path where `p` is invalid (we only make null invalid when we see an
assignment from 0, i.e. `p = NULL;`).
Reviewed By: ezgicicek
Differential Revision: D21089961
fbshipit-source-id: 5ebb85d0a
Summary:
1. Package will make the error too verbose.
2. We don't even need to say it is "class" because we say it in the error
description ("Class has 0 issues and can be marked Nullsafe").
Reviewed By: artempyanykh
Differential Revision: D21131998
fbshipit-source-id: 6ccca7615
Summary:
One source of false positives on container races is when the container member field is initialised to a concurrent version in a constructor, but the static type of the field doesn't reflect the thread safety of it.
This solution
- tracks flows from constructors of safe data structures to abstract addresses;
- initialises the initial attribute state when analysing a non-constructor method to that achieved by all constructors/class-initializers.
- checks for that attribute when recording container accesses.
Reviewed By: jvillard
Differential Revision: D21089428
fbshipit-source-id: 02a88f6e8
Summary:
As artempyanykh pointed out, `nullable` works much better for required fields
than `optional` in terms of x-plat.
Reviewed By: artempyanykh
Differential Revision: D21129614
fbshipit-source-id: b03c91b78
Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array.
Reviewed By: ezgicicek
Differential Revision: D21043304
fbshipit-source-id: db3be49ce
Summary:
The java source file parser should refuse to run on non
.java file. Also, as we expect some autogenerated source files to
break Java official syntax, we catch parsing error silently and
cancel location recording for them.
Reviewed By: jvillard
Differential Revision: D21089587
fbshipit-source-id: 35f1a1e28
Summary:
Now that only races rooted at formals or globals are reported, there is no point using the ownership domain to exclude accesses to locals, so remove the code that initialises the ownership of those.
Also, remove an accidentally quadratic use of `Map.bindings |> List.find` in `FormalMap` and simplify the analysis driver.
Reviewed By: skcho
Differential Revision: D21066855
fbshipit-source-id: 126080778
Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.
This is gated behind a flag for now as there are performance issues with the new arithmetic.
Reviewed By: jberdine
Differential Revision: D20393947
fbshipit-source-id: b780de22a
Summary: Move state to summary conversion into the domain file, move a model matcher into the models file and simplify.
Reviewed By: skcho
Differential Revision: D21064351
fbshipit-source-id: bb5b07b6b
Summary:
There are two types of anonymous classes (not user defined classes):
- classic anonymous classes (defined as $<int> suffixes)
- lambda classes (corresponding to lambda expressions). Experimentally,
they all have form `$Lambda$_<int>_<int>`, but the code just uses
`$Lambda$` as a heuristic so it is potentially more robust.
# Problem this diff solves
When generate meta-issues for nullsafe, we are interested only in
user-defined classes, so we merge all nested anonymous stuff to
corresponding user-defined classes and hence aggregate the issues.
Without this diff, for each lambda in the code, we would report this as
a separate meta-issue, which would both screw up stats and be confusing
for the user (when we start reporting mode promo suggestions!).
Reviewed By: artempyanykh
Differential Revision: D21042928
fbshipit-source-id: a7be266af
Summary: In `PowLoc`, we focus on making every constructors of `PowLoc.t` return nomalized value. Thus, it is unnecessary to nomalize any `PowLoc.t` inputs.
Reviewed By: ezgicicek
Differential Revision: D21064893
fbshipit-source-id: d00a7f06b
Summary:
This diff revises how to handle the unknown location in inferbo in two ways:
* stop appending field to the `Unknown` location, e.g. `Unknown.x.a` is evaluated to `Unknown`
* redesign the abstract of multiple locations, like `Bottom` < `Unknown` < `Known` locations
I am doing them in one diff since applying only one of them showed bad results.
Background: `Unknown` was adopted for abstracting all unknown concrete locations, so we could avoid missing semantics of assignments to unknown locations. We tried to keep soundness. However, it brought some other problems related to precision and performance.
1. Sometimes especially when Inferbo failed to reason precise pointer values, `Unknown` may point to many other abstract locations.
2. At that time, value assignments to `*Unknown` makes the situation worse: many abstract locations are updated with imprecise values.
This problem harmed not only its precision, but also its performance since it introduced more location entries in the abstract memory.
Reviewed By: jvillard
Differential Revision: D21017789
fbshipit-source-id: 0bb6bd8b5
Summary: The flags `--biabduction-fallback-model-alloc-pattern` and `--biabduction-fallback-model-free-pattern` were unused because we removed the models from .inferconfig a while ago because of too many false positives. We are implementing a better memory leak check based on Pulse, and are adding the similar flags `--pulse-model-alloc-pattern` and `--pulse-model-free-pattern`.
Reviewed By: jvillard
Differential Revision: D21061511
fbshipit-source-id: 1b3476c22
Summary:
Instead of having to remember to update both the inferbo and the concrete
intervals domains of pulse, hide these details under a unified API. This
should help the transition to adding a third(!) numerical domain later
on (pudge!).
Reviewed By: ezgicicek
Differential Revision: D21022920
fbshipit-source-id: 783157464
Summary:
Now that the shape of the record type of AbductiveDomain.t is known, we
don't need this getter anymore. Keep `get_pre` and `get_post` as they
perform useful casting to `BaseDomain.t`.
Reviewed By: ezgicicek
Differential Revision: D21022924
fbshipit-source-id: 340f4edf8
Summary:
The "interface" modules define short forms for the internals of pulse
and also serve as a guide of which modules you are supposed to use at
which "level" in the pulse domains (base domain vs abductive domain vs
higher-level PulseOperations.ml). Make sure they are used.
Reviewed By: skcho
Differential Revision: D21022927
fbshipit-source-id: f890df245
Summary:
PulseAbductiveDomain.ml can be split into two distinct parts:
1. The definition of the "abductive domain" itself. This remains in that
file.
2. How to apply a given pre/post pair to the current state (during a
function call). This is about the same size as 1. in terms of lines
of code(!) and is now in PulseInterproc.ml.
Reviewed By: ezgicicek
Differential Revision: D21022921
fbshipit-source-id: 431fe061e
Summary:
I'm moving this code in the next diff and need this refactor. It should
be the same as before.
Reviewed By: ezgicicek
Differential Revision: D21022926
fbshipit-source-id: ebe644ef9
Summary:
See the code comment re: why don't we also recommend "strict" at this
stage. We can always change it later when we think users are happy with
strict.
Reviewed By: artempyanykh
Differential Revision: D21039553
fbshipit-source-id: 758ccf32c
Summary:
Having copypaste is painful to support. Lets make .mli the source of
truth.
Improved docs a bit, while I was here.
Reviewed By: artempyanykh
Differential Revision: D20948916
fbshipit-source-id: 1668dbc9c
Summary:
This diff is a step forward to the state when the list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes a case when we incorrectly defined possible promo mode (see
the test payload)
Reviewed By: artempyanykh
Differential Revision: D20948897
fbshipit-source-id: 616b96f96
Summary:
See the comments in the code why it makes logical sense.
This diff is a step forward the state when list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes majority of cases in ModePromotions.java
Reviewed By: artempyanykh
Differential Revision: D20948656
fbshipit-source-id: 82c0d530b
Summary:
Currently we exlude only if the method is based on deprecated config
packages.
Lets use the proper method, which covers both cases (config +
user-defined third party repo).
Reviewed By: artempyanykh
Differential Revision: D20946506
fbshipit-source-id: c3332667f
Summary:
Previously, we learned to detect if Default mode class can be made
Nullsafe(LOCAL).
Lets generalize it and calculate the precise mode.
NOTE 1: We don't distinct shades of "Trust some". We also don't
recommend trust some and recommend "Trust all" instead.
NOTE 2: As you can see from the test payload (see ModePromotions.java),
the precise calculation is not working as expected. This is due to a bug
in nullsafe implementation/design. See follow up diffs that will fix
this test.
Reviewed By: artempyanykh
Differential Revision: D20941345
fbshipit-source-id: 2255359ba
Summary:
The full inventory of everything in infer-out/. The main change is
around "issues directories": instead of registering them dynamically
they are now all declared statically (well, they kind of were already in
Config.ml).
Reviewed By: ngorogiannis
Differential Revision: D20894305
fbshipit-source-id: 1a06ec09d
Summary:
This is another entry in infer-out/, we want these to be predictable,
not user-defined.
Reviewed By: dulmarod
Differential Revision: D20894302
fbshipit-source-id: ee60ddbcf
Summary:
This is an entry in infer-out/, we want these to be predictable, not
user-defined.
Reviewed By: ngorogiannis
Differential Revision: D20894307
fbshipit-source-id: 332f85969
Summary:
This option allowed one to customise the name of the log file, but the
log file lives in infer-out/ so that flexibility is not needed and even
undesirable: we want entries in infer-out/ to be predictable.
Reviewed By: skcho
Differential Revision: D20894304
fbshipit-source-id: 760d91df3
Summary: Another entry to practice adding entries to ResultsDirEntryName.
Reviewed By: skcho
Differential Revision: D20894299
fbshipit-source-id: 9c387e0f3
Summary:
First real step to keep an inventory of all the entries in infer-out/ in
a single place, and associate meta-data to each entry. In particular, we
want to avoid adding things in infer-out/ without a clear idea of
whether they should be cleaned up before going into a cache, or before
an incremental analysis.
Migrate infer-out/tmp/ first just as an example and an excuse to write
the scaffolding code needed for all the other entries.
Reviewed By: skcho
Differential Revision: D20894300
fbshipit-source-id: f796fca55
Summary:
The only accurate entry it contains is the number of files analysed and
we can already get that information from the log file (and console
output).
Reviewed By: dulmarod
Differential Revision: D20894303
fbshipit-source-id: bc180015a
Summary: Needed for later: RunState needs to run files in ResultsDir.
Reviewed By: skcho
Differential Revision: D20894306
fbshipit-source-id: 259b7da69
Summary:
I wanted to change the order in which we try loading them but it changes
analysis results too much for the cost analysis.
Reviewed By: skcho
Differential Revision: D20891172
fbshipit-source-id: f972f314e
Summary:
Simplifies the models story. The model jar is still needed to look up
fields in modelled classes (we save the .class of each model!). This is
sad as we should be able to get these from the models' tenv, which
should be more compact, but that's a bigger change.
Reviewed By: skcho
Differential Revision: D20891117
fbshipit-source-id: fcb5104ae
Summary:
Parsing the standard output of buck is brittle. Instead, use the `--build-report` option, which generates a json file, with a mapping from target name to output path. This already contains all the information required.
This diff adapts the buck-java integration.
Reviewed By: artempyanykh
Differential Revision: D20942858
fbshipit-source-id: faf3f2078
Summary: Unify the models of malloc and for the Create and Copy functions for Core Graphics. This add the null case from the malloc model to the Core Graphics models.
Reviewed By: jvillard
Differential Revision: D20890956
fbshipit-source-id: 278ac9d2f
Summary:
- Open-source stubs are in a library with no dependencies
- That library is included in InferBase, but in facebook builds it
contains no modules
Reviewed By: ezgicicek
Differential Revision: D20922574
fbshipit-source-id: af918a687
Summary:
As soon as pulse detects an error, it completely stops the analysis and loses the state where the error occurred. This makes it difficult to debug and understand the state the program failed. Moreover, other analyses that might build on pulse (e.g. impurity), cannot access the error state.
This diff aims to restore and display the state at the time of the error in `PulseExecutionState` along with the diagnostic by extending it as follows:
```
type exec_state =
| represents the state at the program point that caused an error *)
```
As a result, since we don't immediately stop the analysis as soon as we find an error, we detect both errors in conditional branches simultaneously (see test result changes for examples).
NOTE: We need to extend `PulseOperations.access_result` to keep track of the failed state as follows:
```
type 'a access_result = ('a, Diagnostic.t * t [denoting the exit state] ) result
```
Reviewed By: jvillard
Differential Revision: D20918920
fbshipit-source-id: 432ac68d6
Summary: Consider functions that simply exit as impure by extending the impurity domain with `AbstractDomain.BooleanOr` that signifies whether the program exited.
Reviewed By: skcho
Differential Revision: D20941628
fbshipit-source-id: 19bc90e66
Summary: The pruning location of array size was dummy. This diff gives a right location to traces in the pruning.
Reviewed By: ezgicicek
Differential Revision: D20915167
fbshipit-source-id: 55cc583df
Summary:
Instead of looking up each proc name in models/, pre-compute the list of
models and do lookups there instead of in the filesystem.
Reviewed By: ngorogiannis
Differential Revision: D16603148
fbshipit-source-id: 5eb534a14
Summary:
Java bytecode format does not record the declarations location
for classes and fields. We set up a first infrastructure to recover this
information. Currently we only track location for classes and only gives
the first line of the corresponding source file. We will enhance this location
with source file (baby) parsing in a next diff.
Reviewed By: mityal
Differential Revision: D20868187
fbshipit-source-id: d355475e9
Summary:
This information can be useful for tooling responsible for further
processing (e.g. metric calculation and logging)
Reviewed By: artempyanykh
Differential Revision: D20914583
fbshipit-source-id: 61804d88f
Summary: The heuristics is to find a method in non-abstract sub-classes. See D20647101.
Reviewed By: jvillard
Differential Revision: D20491461
fbshipit-source-id: 759713ef4
Summary:
This diff distinguishes array declaration and size-setting in trace. For example, when there is an
assume statement on an array size, the array size can be pruned to another value. In which case, we
want to see "Set array size" in the trace, instead of "Array declaration".
Reviewed By: jvillard
Differential Revision: D20914930
fbshipit-source-id: 0253fb69e
Summary:
This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`):
```
type exec_state =
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t
(** represents the state originating at exit/divergence. *)
```
Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state.
The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit.
TODO:
- Impurity analysis needs to be improved to consider functions that simply exit as impure.
- The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?).
Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely.
Reviewed By: jvillard
Differential Revision: D20791747
fbshipit-source-id: df9e5445a
Summary:
Malloc returns either an allocated object or a null pointer if there is no memory available. Modelling that.
This has always been a bit contentious because this leads to NPEs that people often ignores because they don't care. But if we don't model this, then we have FPs when people do take this into account when freeing the memory.
Reviewed By: jvillard
Differential Revision: D20791692
fbshipit-source-id: 6fd259f12
Summary:
infer-out/tmp/ should be deleted before sending infer-out/ to any cache.
Also separate the list of directories to delete in `delete_capture_and_results_data` and in `scrub_for_caching` as it was only confusing to try to share them.
Reviewed By: ngorogiannis
Differential Revision: D20772512
fbshipit-source-id: b1e4e252c
Summary: This makes it similar to the other dir names in infer-out/.
Reviewed By: ngorogiannis
Differential Revision: D20795359
fbshipit-source-id: 88729d26d
Summary:
This diff limits the depth of abstract location by a constant.
problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.
(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)
Reviewed By: jvillard
Differential Revision: D20818471
fbshipit-source-id: f8af27e5c
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary:
It's easy to create large arrays in code, eg `int x[1UL << 16];`, but
these can generate huge nodes in SIL because zero-initialization is
translated by zero-ing structures element by element. Introduce a
builtin to use instead. Keep the naive method for small structures (with
a configurable limit on "small").
Reviewed By: dulmarod
Differential Revision: D20836836
fbshipit-source-id: 6bf5410f8
Summary: Modelling `CG.*Release ` and `CFRelease` as `free`. This is what we were doing in biabduction.
Reviewed By: skcho
Differential Revision: D20767174
fbshipit-source-id: c77c1cdc6
Summary:
This models all the Create and Copy functions from CoreGraphics, examples in the tests.
These functions all allocate memory that needs to be manually released.
The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests.
This check is currently in biabduction, and we aim to move it to Pulse.
Reviewed By: jvillard
Differential Revision: D20626395
fbshipit-source-id: b39eae2d9
Summary: Sometimes buck hangs with the new integration and using pipes. Use a temp file for standard output and redirect stderr.
Reviewed By: jvillard
Differential Revision: D20856346
fbshipit-source-id: 13a5f90d5
Summary:
Fix all the docstrings that `odoc` or `ocamlformat` is not happy about.
Delete all `[@@ocamlformat "parse-docstring = false"]` pragmas as a
result.
Reviewed By: jberdine, ngorogiannis
Differential Revision: D20798913
fbshipit-source-id: 728d9e45c
Summary:
All dune libraries in infer/src/ were declared with their own public
names, each one needing its own .opam file. There's no need for that:
they can all be part of the `infer` library by calling them `infer.Foo`.
One wrinkle: now we need to explicitly point at their .mld files in the
generated documentation.
Reviewed By: jberdine
Differential Revision: D20798914
fbshipit-source-id: 64b64261c
Summary:
This avoids dune scanning 2000+ directories (according to its logs),
mostly due to scanning infer/tests/ I think.
Reviewed By: artempyanykh
Differential Revision: D20798915
fbshipit-source-id: 3764cd3fb
Summary:
- Add `no_return` models for Java's `exit(...)` methods (can be extended further later on)
- handle throw-catch better by short-cutting throw nodes to not exit node but to all **catch nodes** that are reachable by the node. If there is no catch node, we short-cut to the exit node as before.
This removes a FP from deadstore tests because before we simply were not able to handle CF from throw-> catch nodes at all.
Reviewed By: skcho
Differential Revision: D20769039
fbshipit-source-id: e978f6cdb
Summary:
To find a method in non-abstract sub-classes, this diff applies the
same heuristics of inferbo.
* If the class is an interface: Find its unique sub-class and apply the heuristics recursively.
* If the class is an abstract class: Find/use its own summary if possible. If not found, find
one (arbitrary but deterministic) summary from its sub-classes.
* Otherwise: Find its own summary.
Reviewed By: ezgicicek
Differential Revision: D20647101
fbshipit-source-id: 2f8f3ff81
Summary: When looking at some reports I realised that adding the place where the memory becomes unreachable to the trace makes it more readable.
Reviewed By: skcho
Differential Revision: D20790277
fbshipit-source-id: d5df69e68
Summary:
`IssueLog` is used by the file-level analysis callbacks to store reports outside error logs so as to avoid racing on spec files. Each file should generate a single issue log which is then written to an appropriate file. The starvation checker was breaking that contract because it ostensibly needs to write out multiple issue files when analysing a single source file.
This is unnecessary, because the existing mechanisms for deduplication ensure only one issue file needs to be written out.
The whole-program mode still needs that capability, but this is implemented outside the file-analysis callback.
Reviewed By: mityal
Differential Revision: D20736135
fbshipit-source-id: 620e5484d
Summary:
Sometimes buck emits a timestamp, leading to a crash
> External Error: Failed to parse `buck targets --show-output ...` line of output:
> 2020-03-30 20:03:51
Reviewed By: dulmarod
Differential Revision: D20766438
fbshipit-source-id: 47cc00150
Summary:
OCaml 4.10.0 flagged that the `Extension` functor argument was unused.
Delete it and remove one layer of module in the file too now that it
doesn't need to be a functor.
Reviewed By: mityal
Differential Revision: D20669652
fbshipit-source-id: 089043d7d
Summary:
1. The return value is annotated as Nullable in codebase
2. The second parameter can be null as well.
Reviewed By: artempyanykh
Differential Revision: D20766243
fbshipit-source-id: 9aad37a8c
Summary:
This was needed countless of times. We log current signature, but not
callees.
Reviewed By: dulmarod
Differential Revision: D20765107
fbshipit-source-id: 399926c65
Summary:
This declaration is heavily used in Guava library.
Quick inspection shows that majority of methods are annotated correctly.
This will hide previosly hidden unsoundness issues in the codebase.
Reviewed By: artempyanykh
Differential Revision: D20737104
fbshipit-source-id: aa048bfc1
Summary:
The attribute `[no_return]` signifies that a function doesn't return. Previously, pre-analysis had cut the links to successor nodes of such no-return function nodes. This was intended to help with suppressing reporting on unreachable paths for some analyses. However, this results in having these nodes as dangling, with no connection to exit nodes.
This diff additionally shortcuts these no-return function nodes to exit node. This would allow us to enhance inter-procedural analyses like pulse to kepp track of paths that do not return since we will be keeping their connections at exit node rather than completely cutting them of as before. It would also allow us to assume that all paths start at the one start node and end at the one exit node (at least syntactically in the CFG).
Reviewed By: skcho
Differential Revision: D20736043
fbshipit-source-id: 0eace1bdb
Summary:
D20416859 introduced a new utility
`Process.create_process_and_wait_with_output` that:
1. executes the process to completion
2. reads stdout in full
3. reads stderr in full
Unfortunately, writing to stdout/stderr can be a blocking operation for
the callee process in that situation. Double unfortunately, reading both
stdout and stderr in a way that avoids starvation requires sophisticated
Unix-fu. Fortunately, callers of this utility only ever need to read
*one* of stdout or stderr.
Fix the starvation by:
1. reading *one* channel only (either stdout or stderr)
2. doing the reading *before* `wait`ing on the process to finish
3. redirecting the other channel to the console
Reviewed By: skcho, ngorogiannis
Differential Revision: D20737388
fbshipit-source-id: 2988ac865
Summary:
Knowing the number associated with each issue is useful to pass to
`infer explore --select XXX`.
Reviewed By: skcho
Differential Revision: D20696724
fbshipit-source-id: f6f368aa1
Summary:
Used `2to3` but had to (poorly, sorry!) fix byte -> string output of processes.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D20672767
fbshipit-source-id: 852c7e973
Summary:
infer/lib/python/'s not pinin'! It's passed on! This library is no more!
It has ceased to be! It's expired and gone to meet its maker! It's a
stiff! Bereft of life, it rests in peace! If you hadn't nailed it to the
perch it'd be pushing up the daisies! 'ts metabolic processes are now
'istory! It's off the twig! It's kicked the bucket, it's shuffled off
its mortal coil, run down the curtain and joined the bleedin' choir
invisible!! THIS IS AN EX-PYTHON!!
Reviewed By: ngorogiannis
Differential Revision: D20672771
fbshipit-source-id: 7808c0ece
Summary:
Re-implement the generation of an HTML report (with bug traces) in
OCaml.
Kills the --only-show as a side-effect, it is of dubious use since there
is already infer-out/report.txt to get the report list as text. A
follow-up diff adds numbers to the list in infer-out/report.txt for easy
cross-referencing with `infer explore --select 123`.
Reviewed By: skcho
Differential Revision: D20672769
fbshipit-source-id: 39b3a299d
Summary:
When executing unit tests, don't parse the arguments as they will be
parsed by OUnit.
Reviewed By: skcho
Differential Revision: D20669675
fbshipit-source-id: 897ec10ee
Summary:
The text is ambiguous because it sounds as if it recommends annotating the current class as `ThreadSafe`, not the interface invoked.
Also, remove the not useful part "or using an interface known to be thread-safe" because developers don't know in general what interfaces Infer thinks are thread-safe.
Reviewed By: skcho
Differential Revision: D20675729
fbshipit-source-id: 9da438621
Summary:
Morally, INTERFACE_NOT_THREAD_SAFE is issued when an interface method is invoked from `ThreadSafe`-annotated code on an interface that is not known to be thread-safe or annotated so.
However, the ultimate purpose is to prevent races. Thus it should never be issued on an owned object or on objects we would not report races on for any reason (local variables, non-source variables, etc).
This diff equips interface call records with the abstract address they are invoked on, and uses the same rules for maintaining those records or not.
Reviewed By: skcho
Differential Revision: D20669259
fbshipit-source-id: 6c7841e6a
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff improves the domain interface and consolidates all the various validity invariant checking for accesses inside their constructors.
Reviewed By: skcho
Differential Revision: D20668611
fbshipit-source-id: 45806d40d
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff inverts 2 and 1.
Reviewed By: skcho
Differential Revision: D20644100
fbshipit-source-id: 89d810b68
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. `Access`, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff introduces functions in (1) that mask calls to (2), making the flip easier.
Reviewed By: skcho
Differential Revision: D20619614
fbshipit-source-id: 19fda0916
Summary: In an intra-procedural analysis we assume that parameters passed by reference to a function will be initialized inside that function. We use the type information of an actual parameter to initialize the fields of the struct. This does not work if a function has a parameter of type void* as the actual parameters also has type void*. To solve this issue, we use type information from local variables.
Reviewed By: jvillard
Differential Revision: D20670253
fbshipit-source-id: dc9f051ef
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:
Introducing a generalization of map_changed that can now
use a context on each instruction. The context is computed with
the previous instructions in the collection.
Reviewed By: skcho, jvillard
Differential Revision: D20669993
fbshipit-source-id: 58fdee1d9
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:
Seems like a more sensible name. Most tooling should read report.json so
won't notice.
Still output a bugs.txt file with a message to point to report.txt while
people migrate.
Reviewed By: mityal, artempyanykh
Differential Revision: D20626111
fbshipit-source-id: efb84d098
Summary:
The documentation of `--quiet` dates back from when it applied only to
`InferPrint.ml`. Make it more general and more in line with
expectations one might have about a `--quiet` option:
- change the doc
- make it disable the progress bar
Reviewed By: ngorogiannis
Differential Revision: D20626110
fbshipit-source-id: db096fd31
Summary:
This is a fairly popular class that have bunch of nullable methods.
Providing an alternative will make an error message actionable.
Note that this involves some duplication, and the whole API could be
improved. But let's leave it for future improvements.
Reviewed By: jvillard
Differential Revision: D20649099
fbshipit-source-id: bfcc7fd95
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: Use the an LRUCache in Ondemand.LocalCache to avoid clearing it after every toplevel analysis.
Reviewed By: ngorogiannis
Differential Revision: D20281932
fbshipit-source-id: 752c8e1ea
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:
This function is used to adapt the callee summary at a call site. It did two things for every domain element in the callee summary:
- A linear search through the list of actuals.
- For each such actual, it would (repeatedly) compute its ownership (!).
For large summaries this can be substantial. The right way is to precompute the ownership for all actuals once and then simply retrieve it (via an array).
Reviewed By: jberdine
Differential Revision: D20564447
fbshipit-source-id: 1ca3121c2
Summary: The attribute types present are exclusive, so sets are not needed for the attribute map domain. This changes `Attribute` to a flat domain and removes the set on top of that.
Reviewed By: jberdine
Differential Revision: D20560240
fbshipit-source-id: 83e59d73e
Summary:
Both modules define properties the analysis maps to addresses, there is no reason to have two modules for this.
Also remove an instance of `Caml.Not_found` usage.
Reviewed By: jberdine
Differential Revision: D20558683
fbshipit-source-id: eacafd780
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:
# Problem
Yes, nullsafe is not null-safe, such an irony.
ErrorRenderingUtils overuses `option` and `let+` constructions. Most of
internal functions can return `None` when "something is wrong".
On top of this, "default" pattern match is overused either.
Because of this, `ErrorRenderingUtils.mk_nullsafe_special_issue` returns
optional type. In practice, this result can be None for many unclear
reasons, and it is super tricky to even understand them all.
This in turn forced AssignmentRule and DereferenceRule to process this
None is defensive way. The rules have some theory why None was returned,
and have assertions along the way.
Turns out those theories might be wrong. This diff will make triaging wrong assumptions easier.
Reviewed By: artempyanykh
Differential Revision: D20535720
fbshipit-source-id: 2b81e25b7
Summary: When we have clashing args to bug (for instance -j and -Xbuck --num-threads) CLI passed -Xbuck args should win.
Reviewed By: jvillard
Differential Revision: D20557060
fbshipit-source-id: 726fc501a
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:
`to_reportable_violation` is responsible for identifying if the
violation is reportable in this mode or not.
This logic is higly coupled with other functions in
`ReportableViolation`, such as `get_description`: You can not have
sensible description on the violation that is NOT reportable in a given
mode.
So from logical perpsective, creation of `ReportableViolation.t` should
belong to this module itself, not to the parent `Rule` module.
This change will make design clearer.
Reviewed By: artempyanykh
Differential Revision: D20511756
fbshipit-source-id: ef27b5057
Summary:
This diff finishes work in D20491716.
We removed dependency on nullsafe mode for field initialization in
D20491716, so this diff just formalizes it.
Reviewed By: jvillard
Differential Revision: D20493164
fbshipit-source-id: 6ac612e78
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:
`make deadcode` is failing on master but our CI jobs didn't catch it :(
Let's fix existing deadcode for now.
Reviewed By: martintrojer
Differential Revision: D20510062
fbshipit-source-id: 4a5e5f849
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:
Make all arguments named and move function from `Procname.Java` to `Procname`, and making it return a `Procname.t` as opposed to `Procname.Java.t` (all callers want a `Procname` eventually).
Various other small fixes in the callers.
Reviewed By: skcho
Differential Revision: D20492305
fbshipit-source-id: e646cc799
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:
As ngorogiannis pointed out, we never expect whitespaces in classname, so
stripping makes no sense here in best case, and hides a bug under rug in
worst case.
Reviewed By: jvillard
Differential Revision: D20417033
fbshipit-source-id: bc7449171
Summary: Let's also print skipped calls in `pp` to ease debugging both for summary and intermediate steps.
Reviewed By: jvillard
Differential Revision: D20417852
fbshipit-source-id: 7da03ae81
Summary:
There is a module and a module type in the file PulseAbductiveDomain.ml
with the same name. This is confusing and it's better to keep separate names.
Reviewed By: jvillard
Differential Revision: D20388769
fbshipit-source-id: bcfed436e
Summary:
Be a bit more careful about the difference between PrePost.t and
AbductiveDomain.t. It's needed in another diff where the types will be
different.
Reviewed By: ezgicicek
Differential Revision: D20393927
fbshipit-source-id: beaf80c90
Summary: In preparation for PulseArithmetic to be something else.
Reviewed By: ezgicicek
Differential Revision: D20393928
fbshipit-source-id: d93131e12
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:
We will use it in follow up diffs.
From many perspectives, if the function belongs to an anonymous class,
it is useful to know the original user-defined class.
This function makes this distinction clear.
Thanks to ngorogiannis, whos work on refactoring `Typ.name` made this module
easy enough so we can introduce unit tests!
Reviewed By: ngorogiannis
Differential Revision: D20389311
fbshipit-source-id: 408d95660
Summary: `Procname.Java.get_return_typ` is buggy because whenever faced with an array of objects, it returns a type that implies the object is stored by value in the array (this is correct behaviour only when the element type is primitive, not when it's an object type).
Reviewed By: ezgicicek
Differential Revision: D20384403
fbshipit-source-id: d91322d3a
Summary:
We try to consolidate Java-specific stuff in JavaClassName.
Let's introduce the function in JavaClassName and make it clear that
its analog in Typ.Name.Java one throws if called on a wrong type.
Reviewed By: ngorogiannis
Differential Revision: D20386357
fbshipit-source-id: a1577ef8b
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: No need to load the contents of the whole file(s) as a string first.
Reviewed By: ngorogiannis
Differential Revision: D20362602
fbshipit-source-id: 46fbc3693
Summary:
Next step in moving logic from make to dune. Since dune understands
build rules with multiple targets we don't need to introduce
artificial pipelining as in make. Rules are pretty straightforward,
albeit somewhat verbose.
The tricky part here was adjusting deadcode detection.
Reviewed By: jvillard
Differential Revision: D20322605
fbshipit-source-id: 688e5f96f
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 the introduction of environments and profiles we no longer need
to generate most dune files in libraries via make. Also, those dune
builds don't need to be in OCaml.
In addition to converting build files to plain sexp definitions, this
patch also:
- Adjusts copyrightCheck to work correctly with sexp-based dune files.
- Adds auto-formatting for sexp-based dune files.
Reviewed By: jvillard
Differential Revision: D20250208
fbshipit-source-id: 495aeaa99
Summary: With plain/sexp dune files we need to support lisp style comments in checkCopyright
Reviewed By: jvillard
Differential Revision: D20366314
fbshipit-source-id: 04db9e3c1
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:
What was happening in that case is that a .inferconfig file containing `{ "myflag":
false }` used to be translated by CommandLineOption as `--no-` (`--no-<long>`),
because it picked the *non-deprecated* form of the option (here `myflag` would
have to be a deprecated form of the option since its non-deprecated form is
empty `""`). Instead, pick a non-empty form of the option.
Reviewed By: jberdine
Differential Revision: D20368784
fbshipit-source-id: 8e761e684
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: Just for fun, and because killing InferPrint.ml is just so satisfying.
Reviewed By: ngorogiannis
Differential Revision: D20362643
fbshipit-source-id: 039cfec61
Summary:
Now that this module only prints report.json and costs_report.json, we
can dis-entangle the whole callback spaghetti.
Reviewed By: ngorogiannis
Differential Revision: D20362640
fbshipit-source-id: 56ffa4e08
Daiva Naudziuniene
Nikos Gorogiannis
Dulma Churchill
Jules Villard
Qianyi Shu
Sungkeun Cho
Ezgi Çiçek
Josh Berdine
Artem Pyanykh
David Pichardie
Mitya Lyubarskiy
Martin Trojer
Artem Pianykh
Fernando Gasperi Jabalera