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:
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:
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:
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:
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
Dulma Churchill
Jules Villard
Ezgi Çiçek
Josh Berdine
Qianyi Shu
Nikos Gorogiannis
David Pichardie
Sungkeun Cho
Daiva Naudziuniene