Summary:
On big analyses, we routinely observe analyses nesting levels of the
order of ~5k (i.e. 5342> on the interactive taskar). This call depth
is meaningless given the size of the codebase we analyze.
Instead, I believe this is due to the fact that Ondemand does not
properly snapshot/restore the nesting level when starting an analysis,
and more importantly when abandoning parts of it. This commit
fixes that oversight.
Pull Request resolved: https://github.com/facebook/infer/pull/1431
Reviewed By: ngorogiannis
Differential Revision: D28118297
Pulled By: jvillard
fbshipit-source-id: 0faf28f84
Summary:
Just moving stuff around.
This is possibly useful for making Pvar depend on ProcAttributes for
other things, eg checking if a pvar is captured by a procedure (which
would be awkward to have in the API of ProcAttributes and not Pvar).
Overall it forced me to move a few other things around in a way that I
feel makes more sense anyway.
Reviewed By: skcho
Differential Revision: D28091497
fbshipit-source-id: 367a1f17c
Summary:
In order to use Inferbo's analysis result, a checker should know current instruction index.
However, for the checkers using `ProcCfg.Normal` CFG, it was impossible to get the instruction
index. To solve the issue, this diff changes the AbsInt framework to give the index together to
`exec_instr`.
Reviewed By: ezgicicek
Differential Revision: D27680894
fbshipit-source-id: 1dc8ff0fb
Summary:
In D27430485 (a6ab4d38cf), we used the static cost of the callee to determine whether it was cheap/expensive. This diff improves on that by taking the whole instantiated cost of the function call (not just the callee's cost).
Also, if the callee is an unmodeled call, we consider it to be expensive as before.
Note: cost instantiation was used by hoisting. I refactored bunch of code there to reuse as much as code possible.
Reviewed By: skcho
Differential Revision: D27649302
fbshipit-source-id: 07d11f3dd
Summary: We have been referring to the arguments of a function call as "params". This has been bothering me. Let's fix it!
Reviewed By: ngorogiannis
Differential Revision: D27649158
fbshipit-source-id: 10e0b28cb
Summary:
Reporting all ungated (un configed?) function calls causes many FPs. Instead, we rely on complexity analysis to determine whether a function is cheap/expensive: if the callee's complexity is not symbolic (e.g. constant), we consider it as cheap and don't keep track of it.
Note that we don't take the instantiated/modeled cost into account yet. So, if we have `foo(int n)` with complexity `O(n)`, and call it as `foo(3)`, we would still keep track of it. Similarly, if `foo` is a modeled function with constant time complexity, we would have no summary for it hence would keep track of it.
These will be improved later.
Reviewed By: skcho
Differential Revision: D27430485
fbshipit-source-id: d5f66320d
Summary:
Copied the documentation from a document created by rgrig
(thanks!!).
Reviewed By: rgrig
Differential Revision: D27325829
fbshipit-source-id: 118e1a2be
Summary:
Before this diff, TOPL had 3 implementations:
1. a post-processing of biabduction summaries
2. a post-processing of pulse summaries
3. a deep embedding in pulse
1 and 2 additionally require instrumenting SIL to generate monitors for
the TOPL properties. 3 is faster than both 1 and 2, by a good lot, and
doesn't require instrumenting the SIL code. Thus, delete 1 and 2!
Also harmonise the CLI so that TOPL is activated by --topl, which
actives it as a checker, like other analyses.
Reviewed By: rgrig
Differential Revision: D27270178
fbshipit-source-id: e86cf972b
Summary:
This diff handles live variables in catch blocks. To do that, this diff adds another metadata,
`CatchEntry`.
Domain change: The domain is changed to
```
(normal:variables) x (exn:try_id->variables)
```
`exn` is a map from try-catch-id to a set of live variables that are live at the corresponding entry
of catch blocks.
Semantics change: It is a backward analysis.
* on `CatchEntry`: It updates `exn` with `try_id` and current `normal`.
* on `Call`: As of now, we assume all function calls can raise an exception. Therefore, it copies
all live variables in `exn` to `normal`.
* on `TryEntry`: It removes corresponding `try_id` from `exn`.
Reviewed By: jvillard
Differential Revision: D26952755
fbshipit-source-id: 1da854a89
Summary: This diff adds TryEntry and TryExit statements to the entry and exit of C++ `try` block, in order to handle exceptional control flow better in analyses.
Reviewed By: da319, jvillard
Differential Revision: D26946188
fbshipit-source-id: 33f4ae9e7
Summary:
The config impact checker prints ungated callees in a separate file config-impact-report.json,
because its results should be compared before actual reporting as the cost checker does.
Reviewed By: ezgicicek
Differential Revision: D26665097
fbshipit-source-id: 0c6e13403
Summary:
Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks.
This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer:
> Data races in `Nullsafe` classes may still cause NPEs.
This only happens if the race is directly on a non-primitively-typed member field of the class.
It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting.
Reviewed By: ezgicicek
Differential Revision: D26403274
fbshipit-source-id: 3cd6ca082
Summary: As there are no dependencies between procedure and file analyses in RacerD, split them into separate modules.
Reviewed By: ezgicicek
Differential Revision: D26198874
fbshipit-source-id: 032aad9d8
Summary:
Dear Infer team,
To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.
Please help to review, discuss and consider to merge this feature.
Thanks,
Xiaoyu
Pull Request resolved: https://github.com/facebook/infer/pull/1361
Reviewed By: skcho
Differential Revision: D25928458
Pulled By: jvillard
fbshipit-source-id: 7726150b8
Summary: In `ClosureSubstSpecializedMethod`, it duplicates a procedure with specialized closure parameters. Since it introduces a new procedure name, its local variables in the procedure body must be replaced to use the new procedure name. (Note that local variable type includes procedure name.) However, in the previous implementation, it missed the translations in some cases: compound expressions and metadata.
Reviewed By: ezgicicek
Differential Revision: D26075490
fbshipit-source-id: 2a5a30cd8
Summary:
D20769039 (cec8cbeff2) added a preanalysis step that creates edges from throw nodes to all reachable catch nodes. It intended to fix some deadstore FPs however it caused more damage than the fix itself. In particular, throws were connected irrespective of
- the type of the exception
- whether the try was surrounded by a catch
This in turn caused weird CFGs with dangling and impossible to understand nodes:(
This diff reverts this change for now.
Instead, the fix should probably be done in the frontend where we have more information about try/catch blocks.
Reviewed By: da319
Differential Revision: D25997475
fbshipit-source-id: bbeabfbef
Summary:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What the previous and this diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then this diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562303
fbshipit-source-id: 4cbc6d234
Summary:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What this and the next diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First this diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then the next diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562297
fbshipit-source-id: b96622336
Summary: As per summary. Note that biabduction will make the results imprecise due to async exceptions from the timeout signal handler, so we warn when both are enabled (https://github.com/janestreet/memtrace/issues/2).
Reviewed By: jvillard
Differential Revision: D25219737
fbshipit-source-id: bdef228fc
Summary: The Ondemand entry point `analyze_proc_desc` exists purely to support specialisation under biabduction. After fixing the storing of specialised `proc_desc`s for java it suffices to use `analyze_proc_name` which will work just fine in its place.
Reviewed By: jvillard
Differential Revision: D25421763
fbshipit-source-id: b162feec3
Summary: Whenever the interface functions are called, there is always an execution environment present, so it is safer and better to get rid of the setter/getter reference thing.
Reviewed By: jvillard
Differential Revision: D25421335
fbshipit-source-id: 7110c932b
Summary:
Since D20736043 (d84fea52ae) is adding edges from the noreturn function node to exit node, analyzers should
handle the state differently to normal states.
Reviewed By: ezgicicek
Differential Revision: D25402576
fbshipit-source-id: a98e41b0c
Summary: When using the restart scheduler incrementing the analyzed count before the analysis itself gives wrong results.
Reviewed By: jvillard
Differential Revision: D25367787
fbshipit-source-id: aed22cc68
Summary:
Put hooks into Pulse for a faster Topl:
- done: PulseAbductiveDomain now tracks a Topl state
- todo: PulseTopl needs some transfer function (now they're dummies)
Reviewed By: jvillard
Differential Revision: D23815497
fbshipit-source-id: f3f0cf9ef
Summary:
Existing closure substitution only supported direct block calls to formals.
The following didn't work since the domain was only keeping track of loads/calls from formals, but didn't support stores.
```
void foo(dispatch_block_t block1){
dispatch_block_t local_block = block1;
local_block(); // we don't substitute the call here
}
```
This diff adds support for assigning a block to a local variable so that we can specialize the above example.
We now have a pair domain
- existing mapping from ids to block vars
- a new mapping from mangled to block specializations
the latter allows us to update the mapping in local block assignment (via store).
Reviewed By: skcho
Differential Revision: D25030234
fbshipit-source-id: 3f172341c
Summary:
Specialized closure substitution was broken for conditionals:
```
void foo(dispatch_block_t block1){
if (x){
block1(); // not replaced with specialized implementation
}
}
```
The problem was that when substituting function calls, it only used memory state at the exit node, rather than at each program point.
We could solve this by
- reverting the domain change in D24418560 (c47911359a), i.e. collecting all possible mappings conservatively (e.g. switch the domain back to `Map`)
- pass the `invariant_map` for substitutions at each program point.
We go with the second option here.
The closure substitution is still somewhat broken as exemplified by the following example:
```
void foo(dispatch_block_t block1){
dispatch_block_t local_block = block1;
local_block(); // we don't substitute the call here
}
```
Reviewed By: skcho
Differential Revision: D24993962
fbshipit-source-id: ebadddb58
Summary: Cleanup `Typ` by moving all constant types to `StdTyp`. Also remove `Typ.typ` as it's just `Typ.t` now.
Reviewed By: jberdine
Differential Revision: D24620397
fbshipit-source-id: 4764f87ef
Summary:
This diff replaces overridden method calls in ObjC when possible, ie the first parameter of the
method has a sub-class type of the method's class. For example,
when `MyEnumerator` is a sub-class of `NSEnumerator` and there is overridden `nextObject`,
```
[my_enumerator nextObject]
```
in Sil, it was translated to like
```
NSEnumerator.nextObject(my_enumerator : MyEnumerator*)
```
and the analyzer missed the overridden method. This diff replaces the function call to
```
MyEnumerator.nextObject(my_enumerator : MyEnumerator*)
```
Reviewed By: ezgicicek
Differential Revision: D24477290
fbshipit-source-id: 6842a76f8
Summary: Can be useful, especially to dump all the summaries as json.
Reviewed By: skcho
Differential Revision: D24504253
fbshipit-source-id: 845e7d657
Summary:
Emit the crucial parts of Pulse summaries as json to enable
post-processing by external tools. Stop somewhat arbitrarily at some
datatypes that are just emitted as "opaque" values.
For example:
```
$ infer debug --procedures --procedures-summary-json --select 0
[[["pulse",[["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v7",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v7","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}],["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v8",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v8","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}]]]]]
```
Reviewed By: ezgicicek
Differential Revision: D24503387
fbshipit-source-id: 9bd08e93b
Summary:
Output summaries in json format, so that other tools can exploit the
results of infer without having to be written inside infer itself.
For now the json for a summary is just one line saying "opaque" :)
Set up the infra to generate (yo)json automatically using
ppx_yojson_conv. See it in action in the next diff.
Reviewed By: ezgicicek
Differential Revision: D24503343
fbshipit-source-id: e24a2fff3
Summary:
- output the "menu" of the interactive mode on stderr instead of stdout
so that we can pipe the results, eg
`infer debug --procedures --procedures-summary | cat`
This will be more useful when we add an option to output json, as
otherwise the menu pollutes the json.
- Allow "--select" to work for infer-debug too:
`infer debug --procedures --procedures-summary --select 0`
Reviewed By: da319
Differential Revision: D24503301
fbshipit-source-id: d7fb4b713
Summary:
Don't wait until pre-analysis has completed before updating the task
bar with the current procedure being analysed.
Reviewed By: skcho
Differential Revision: D24418609
fbshipit-source-id: afedaf687
Summary:
Move from Map to SafeInvertedMap:
- joining two branches where only one branch had the variable set to a
given closure or type should *not* keep that information around: now
we correctly get Top instead
- the "Safe" part is an optimisation that doesn't store Top values in
the map, which is important as most values are not closures so we
don't care about storing the fact that we don't know anything about
them
Reviewed By: ngorogiannis
Differential Revision: D24418560
fbshipit-source-id: 0ac701502
Summary:
Another step in the refactoring of the starvation domain:
- Main purpose is to mediate access to the set of critical pairs in a summary through a fold function (`fold_critical_pairs_of_summary`) and not through direct field access to that set. This will allow eliding storage of critical pairs entirely and dynamically generating those when folding.
- Remove optional arguments as much as possible, as this led to unused arguments not being caught.
- Helper functions distributed more logically among modules.
Reviewed By: skcho
Differential Revision: D24275399
fbshipit-source-id: d23123a48
Summary:
In ObjC, `NSObject.copy` returns the object returned by `copyWithZone:` on the given class. This method must be implemented if the class complies with `NSCopying` protocol. Since we don't have access to `NSObject`'s code, to follow calls into `copyWithZone:`, we replace such `copy` calls with calls to `copyWithZone:` when a) such a method exists in the class and b) the class conforms to `NSCopying` protocol.
This is done in the preanalysis because
- we need to know if there is a `copyWithZone:` method in the class.
- so that other analyses also benefit (as opposed to doing this in cost and inferbo models).
Note that `NSObject` doesn't itself conform to `NSCopying` but all its subclasses must confrom to the protocol and support the same behavior as above.
https://developer.apple.com/documentation/objectivec/nsobject/1418807-copy
Similarly for `mutableCopy` -> `mutableCopyWithZone:` for classes implementing `NSMutableCopying` protocol.
Reviewed By: skcho
Differential Revision: D24218102
fbshipit-source-id: 42900760e
Summary: Subsequent diff will push information down into `Event.t` so as preparation, turn all variant values into records.
Reviewed By: jvillard
Differential Revision: D24115201
fbshipit-source-id: d2126dd49
Summary:
`std::lock(x,y,z)` simultaneously acquires locks `x,y,z` in a deadlock free manner (essentially an unspecified fixed order).
Starvation currently deals with it by exploiting properties of the state domain. It's a map from locks to number of times the lock is held, so the count of many locks can be increased at the same time without recording any particular lock order.
In upcoming diffs the domain will be refactored into a tree of nested lock acquisitions (for other reasons) and that domain necessarily records lock order. The obvious way of doing this correctly is to allow `std::lock` as an atomic even (ie, without trying to break it into multiple acquisitions).
This diff does exactly that, by changing the `Event.LockAcquire` variant to take a list of locks.
Reviewed By: ezgicicek
Differential Revision: D24052304
fbshipit-source-id: 410c812d7
Summary: Gradle produces a number of compilation units which are currently captured sequentially. This diff parallelizes this step.
Reviewed By: jvillard
Differential Revision: D23930978
fbshipit-source-id: d71c22ba3
Summary: Subtle false positives and negatives in Hil make Sil preferable. This diff gets rid of the CFG-emulation of Hil, while still using Hil expressions.
Reviewed By: da319
Differential Revision: D23815026
fbshipit-source-id: 731a6d299
Summary:
This diff substitutes closure parameter when it is given via variable. For example,
```
x = ^{ ... }
foo(x)
```
this diff substitutes the closure variable `x`,
```
x = ^{ ... }
foo(^{ ... })
```
so that the specialization of `foo` can be done by `CCallSpecializaedWithClosures.process`.
Reviewed By: jvillard
Differential Revision: D23814595
fbshipit-source-id: a89f1530f
Summary:
Nullifying these leads to observable side-effects, like in the added
test.
Reviewed By: da319
Differential Revision: D23759756
fbshipit-source-id: 559a6486b
Summary: So that it can be meaningfully used for diffing across infer versions, say.
Reviewed By: martintrojer
Differential Revision: D23648560
fbshipit-source-id: 98d634e37
Summary:
Eliminate the need to serialise procnames when sending work from the restart scheduler to the workers, by sending the proc_uid instead. This is (much) shorter than the byte representation of the proc_name and it's the primary DB key of the procedures table, so it can be used by the worker to obtain the full procname.
Also, reduce GC churn by using folds in the scheduler startup instead of copying lists over and over.
Reviewed By: jberdine
Differential Revision: D23566131
fbshipit-source-id: 1472aa990
Summary:
- freshen up /docs/next/absint-framework to give sensible advice, and
delete outdated bits that are now in the API docs so they remain fresh
- delete SimpleChecker.ml as it's just a source of bitrot
- delete the "adding checkers" page as it's completely outdated and
subsumed by the "AI framework" page + the labs.
Reviewed By: jberdine
Differential Revision: D23597271
fbshipit-source-id: 78b541746
Boris Yakobowski
Jules Villard
Sungkeun Cho
Ezgi Çiçek
Nikos Gorogiannis
Xiaoyu Liu
Radu Grigore