Summary: Before we were modelling `vector.end()` as returning a fresh pointer every time is was called. It is common to check if an iterator is not the `end()` iterator and proceed to dereference the iterator in that case. In such code pattern `vector.end()` is called twice and returns different fresh values which causes false positives. To fix this, we add a special internal field `__infer_model_backing_array_pointer_to_last_element` to a vector to denote its end. Now, every time we call `vector.end()` we return the value of this field. We introduce a new attribute `EndOfCollection` to mark `end` iterator as the existing `EndIterator` invalidation is not suitable when we need to read the same value multiple times.
Reviewed By: jvillard
Differential Revision: D23101185
fbshipit-source-id: fa8a33b58
Summary:
Constructing the report is done by reading all the summaries, and using certain parts thereof. However, the payloads, which typically account for the greatest size, are not used (with the exception of costs).
This diff splits the storage of summaries into analysis and report summaries, and only reads and deserialises the latter for the report phase. This makes a big difference for runs with a large number of procedures.
Reviewed By: jvillard
Differential Revision: D23105072
fbshipit-source-id: 359067a0f
Summary:
As preparation for splitting summaries into some of their components, and then iterating over only those when reporting (thus gaining performance) we need procnames in the table.
Also, this fixes the now-broken use case of `infer report` with spec files, by using `--procedures-filter` to restrict printing of summaries accordingly.
Reviewed By: skcho
Differential Revision: D23101853
fbshipit-source-id: 1ae878d8e
Summary: Implement specs storage in DB, apart from biabduction models which are still left in specs files.
Reviewed By: skcho
Differential Revision: D22795638
fbshipit-source-id: 140801d3f
Summary: Extra info helps in debugging frontend issues and such.
Reviewed By: ngorogiannis
Differential Revision: D23101854
fbshipit-source-id: 27024675d
Summary:
At the end of analysing a procedure we call `simplify
~keep:vars_live_in_pre_post`. Any variable not in
`vars_live_in_pre_post` is not mentioned anywhere else in the state and
therefore is not going to contribute constraints in callers of the
procedure (in other words: they're dead). We want to also forget
arithmetic facts about these variables as this is a good opportunity to
make the path condition smaller, sometimes by a lot!
The main issue is that dead variables may be useful intermediate terms
in the formula, eg trying to keep only facts about `x` in `y = x + 1 &&
y = 0` is going to lose a lot of precision. But, if a variable not in
`keep` is only mentioned in a simple atom `z = 42` atom, for example,
it's safe to forget about it, eg it's safe to remember only `x=0` in
`x=0 && z=42` (if only `x` is live).
In other words, we can get rid of all atoms containing variables not
transitively involved in other atoms that eventually involve live
variables. A graph problem! This is guaranteed not to forget anything
important and can still trim a lot of atoms in certain situations.
Reviewed By: skcho
Differential Revision: D22921313
fbshipit-source-id: 6d5db7cbe
Summary:
Perhaps a bit overkill to introduce all this extra complexity but it
makes the unit tests much more readable. In fact, this uncovered a bug
in the dead variable elimination!
Reviewed By: dulmarod
Differential Revision: D22925548
fbshipit-source-id: d1f411683
Summary:
Do not always add parens around sub-terms, and add more parens around
terms in atoms and normal forms when they can be confused with the atom
or normal form structure.
Reviewed By: skcho
Differential Revision: D22925549
fbshipit-source-id: 8646e96a5
Summary: These will change to more interesting outputs in the next diff.
Reviewed By: dulmarod
Differential Revision: D22921349
fbshipit-source-id: c58c6240a
Summary:
Add unit tests to pulse in order to write tests for the arithmetic
solver, because it is a pain to write programs to do that end to end.
Reviewed By: ezgicicek
Differential Revision: D22864607
fbshipit-source-id: 0a20a3593
Summary:
This is needed to make dune auto-updating of unit tests introduced in
the next diff cohabit peacefully with our tests to make sure code stays
correctly formatted wrt ocamlformat.
Also, more auto-formatting = better.
Reviewed By: da319
Differential Revision: D22865004
fbshipit-source-id: 91c47ab08
Summary:
Normalization is potentially expensive and its result should be
remembered if the formula keeps being used. In the future we might use
this to make normalization more incremental.
Also rename PathCondition.satisfiable -> is_unsat to match
PulseFormula.is_unsat.
Reviewed By: skcho
Differential Revision: D22728264
fbshipit-source-id: 7759b33ac
Summary:
Now that this is a cheap operation, use it whenever we are checking the
satisfiability of the path condition.
Reviewed By: skcho
Differential Revision: D22724373
fbshipit-source-id: df31c6010
Summary:
Pausing the experiment in favour of new PulseFormula. Can be resurrected
later.
Reviewed By: skcho
Differential Revision: D22576274
fbshipit-source-id: 76529d767
Summary:
This time it's personal.
Roll out pulse's own arithmetic domain to be fast and be able to add
precision as needed. Formulas are precise representations of the path
condition to allow for good inter-procedural precision. Reasoning on
these is somewhat ad-hoc (except for equalities, but even these aren't
quite properly saturated in general), so expect lots of holes.
Skipping dead code in the interest of readability as this (at least
temporarily) doesn't use pudge anymore. This may make a come-back as
pudge has/will have better precision: the proposed implementation of
`PulseFormula` is very cheap so can be used any time we could want to
prune paths (see following commits), but this comes at the price of some
precision. Calling into pudge at reporting time still sounds like a good
idea to reduce false positives due to infeasible paths.
#skipdeadcode
Reviewed By: skcho
Differential Revision: D22576004
fbshipit-source-id: c91793256
Summary:
Current handling of lambdas is quite rudimentary. Looking at test
results we can see that errors are all over the place: False Positives,
False Negatives and just plain wrong results.
These tests can be grouped in 2 sets:
1. Basic support which implies:
- understanding method signatures,
- providing comprehensible error messages.
2. Extended support with implies:
- understanding scoping of values captures in lambdas (needs proper aliasing analysis).
- understanding parametric nullability in generics (needs "some"
support for Generics in our Java frontend).
With follow-up patches I'll attempt to implement "Basic" support for
Lambdas. "Extended" support will be out of scope unless there's
significant demand.
Reviewed By: mityal
Differential Revision: D23058673
fbshipit-source-id: 621551cca
Summary:
Absence of kotlin-annotations led to warnings messages during tests compilation:
```
$ make
warning: unknown enum constant MigrationStatus.STRICT
reason: class file for kotlin.annotations.jvm.MigrationStatus not found
```
This doesn't affect test results but is annoying, hence the fix.
Reviewed By: mityal
Differential Revision: D23051769
fbshipit-source-id: e45fbe7be
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
As usual, in this diff we don't convert everything and take some
shorthands.
Reviewed By: ngorogiannis
Differential Revision: D23054169
fbshipit-source-id: 70913ddfd
Summary:
Note that the current implementation lists classes and methods (not
<class:method> pairs.
This is bit clowny, but works for now (given the list of classes is small).
So I'll leave it out of the scope of this diff.
Reviewed By: ngorogiannis
Differential Revision: D23076671
fbshipit-source-id: 71c94ebd9
Summary: This diff separates purity analysis and its reporting, since sometimes we want to use the purity analysis results in other checkers, but don't want to report purity issues.
Reviewed By: ezgicicek, jvillard
Differential Revision: D23054913
fbshipit-source-id: 12cc1fc42
Summary: Since there is no discernible downside in using the write daemon unless in single-thread mode or in buck, make it only depend on these circumstances, not a command line flag.
Reviewed By: skcho
Differential Revision: D23004451
fbshipit-source-id: 5c1d06ed1
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: artempyanykh
Differential Revision: D23052773
fbshipit-source-id: aacd07f27
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: artempyanykh
Differential Revision: D23052339
fbshipit-source-id: 665126957
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
This diff:
1/ migrates AssignmentRule
2/ passes Procname.Java.t around from the start of analysis.
For now we have places where we have both procname and java procname.
This is fine as we can get rid of it in follow up diffs.
Reviewed By: artempyanykh
Differential Revision: D23052226
fbshipit-source-id: 0125de297
Summary:
This is part of work aimed to reduce number of language-agnostic methods
used in Nullsafe codebase.
Reviewed By: artempyanykh
Differential Revision: D23052328
fbshipit-source-id: 2b69f5f7a
Summary:
This diff adds a false positive test that is introduced imprecise loop
invariant detection.
In the example, `i` and a temp variable `$irvar = get_size(arr)` are
all included in the control variables, so the complexity becomes
quadratic. The problem is that `$irvar` is not addressed as a loop
invariant:
* `is.read` is analyzed as modifying a global
* all return variables, including `$irvar`, of unmodeled functions are invalidated
Reviewed By: ezgicicek
Differential Revision: D23051414
fbshipit-source-id: 011fd086b
Summary: To avoid dead store false positives we skip initialization of a variable that has an `unused` attribute. However, this causes uninitialized value false positives when the variable is later used in macros. To fix this, instead of skipping initialization we record the information about `unused` attribute in local variable data that we can later use for filtering out dead store issues.
Reviewed By: jvillard
Differential Revision: D22868050
fbshipit-source-id: 4a2d0e680
Summary:
In the current implementation, we record 3 states: modelled internally,
modelled intenally, not modelled.
The follow up diffs will need to distinct first- and third- party, given
annotated signature. This diff makes it possible.
Reviewed By: artempyanykh
Differential Revision: D22977962
fbshipit-source-id: b8f3616b5
Summary:
We get duplicated variable declaration instruction for primitive type variable initialized using list initializer, e.g.
```
int* p{nullptr};
```
This happens because we add variable declaration instruction when we translate both `DeclStmt` and `InitListExpr`. To fix this, we do not add the duplicated variable declaration when we translate `InitListExpr`.
Reviewed By: jvillard
Differential Revision: D22844726
fbshipit-source-id: 422806924
Summary:
Synthetic/autogenerated methods/fields usually contain `$` in their names.
Reporting nullability violations on such code doesn't make much sense
since the violations are not actionable for users and likely need to be
resolved on another level.
This diff contributes:
1. Several test cases that involve synthetic code of different
complexity.
2. Code that handles some particular types of errors (but not all!).
Reviewed By: mityal
Differential Revision: D22984578
fbshipit-source-id: d25806209
Summary:
Use `Typ.t` for parameter types in procnames, instead of `JavaSplitName.t`. This allows more precise and usable types stored in procnames, as well as not using the string-based representation of `JavaSplitName` which meant parsing strings whenever one needed a `Typ.t`.
This also makes `JavaSplitName` dead code, so it is removed.
Reviewed By: skcho
Differential Revision: D20500423
fbshipit-source-id: a72728e3f
Summary: Since types from the java frontend are a subtype of `Typ.t` provide the means to check and enforce that for return types in procnames.
Reviewed By: ezgicicek
Differential Revision: D20495527
fbshipit-source-id: b99c784af
Summary:
`java_type` aka `JavaSplitName.t` is a pair of strings. It's used in a procname to store the return type. Replace that with `Typ.t`.
This is step one of deleting `JavaSplitName`. Step two will be to replace parameters with `Typ.t`.
Reviewed By: skcho
Differential Revision: D20323748
fbshipit-source-id: f0029c3ca
Summary:
This diff adds an option `max-jobs` that restrict the number of jobs
running simultaneously.
Reviewed By: ngorogiannis
Differential Revision: D22978328
fbshipit-source-id: 544153c1c
Summary:
Currently, the notion of a third party method signature (corresponding to
a single record in a .sig file) is scattered between unique_repr and
nullability.
Logically, ThirdPartyMethod.t should not "know" about unique_repr
because this is a detail needed only for searching for a method
definition in `.sig` storage.
This diff:
1. Introduces ThirdPartyMethod.t which exposes exactly information
stored in .sig file. We are going to use this abstraction more in follow
up diffs.
2. Moves functionality operating with `unique_repr` to the module
responsible for searching in the repository.
3. Deletes `ThirdPartyMethod.nullability` abstraction - we don't need it as we can just store ThirdPartyMethod.t where was previously `nullability` stored.
4. Introduces `to_canonical_string` method that prints back third party
method in a format needed for `.sig` file, and a test ensuring that
parsing works back and forth consistently. We are going to use this
method in follow up diffs as well.
Reviewed By: artempyanykh
Differential Revision: D22950706
fbshipit-source-id: a0e72ccdb
Summary: As per title. Eases next diffs by making Summary the only source of truth for how spec files are accessed/stored.
Reviewed By: ezgicicek
Differential Revision: D22794742
fbshipit-source-id: 0ee20ec1c
Summary: New, experimental for now, integration with buck on Java using the `#infer-java-capture` flavor.
Reviewed By: artempyanykh
Differential Revision: D22187748
fbshipit-source-id: 62cdafe6b
Summary:
This diff removes a dead field `Struct.subs`, which was used in
heuristics finding methods from sub-classes.
Reviewed By: ezgicicek
Differential Revision: D22945346
fbshipit-source-id: 4b3bf0093
Summary: This diff is on par with this change, with the same motivation
Reviewed By: artempyanykh
Differential Revision: D22924891
fbshipit-source-id: 578ca5869
Summary:
This change will simplify the further refactoring I am doing in follow
up diffs.
Logically, AssignmentRule is about passing actual value to the declared
one, and the proper abstactions for this is exactly AnnotatedNullability
and InferredNullability.
This will also make the client less error prone (no way to call if you
don't have a declaration and actual value to compare).
In the next diff, we will do the same in DereferenceRule.
Reviewed By: artempyanykh
Differential Revision: D22923779
fbshipit-source-id: 5f8f0931c
Summary: Before, `NSCollection` are modelled like array, but this will have issue when we want to say add object to array. This diff changes `NSCollection`'s model to use Java's Collection model.
Reviewed By: ezgicicek
Differential Revision: D22840079
fbshipit-source-id: b944b743b
Summary:
In Cost/Inferbo checkers, it tried to find a subclass with heuristics when a method of interface or
abstract class is called. While it makes preciser analysis results in general, sometimes introduced
tricky FPs since the behavior of the heuristics depends on targets. This diff revert the heuristics
to suppress the FPs.
Reviewed By: ngorogiannis
Differential Revision: D22924485
fbshipit-source-id: 9f151231f
Summary: Implement `alloc` and implement initialisation method that uses the return value of `alloc`, i.e. `NSString.init`.
Reviewed By: ezgicicek
Differential Revision: D22840080
fbshipit-source-id: 47a7523e3
Summary:
This diff translates for-in block in objc as a simple for-loop. For example,
`for (item_type item in items) { body }` is translated to
```
NSEnumerator *enumerator = [items objectEnumerator];
item_type item;
while (item = [enumerator nextObject]) { body }
```
Reviewed By: ezgicicek
Differential Revision: D22841524
fbshipit-source-id: 296ee84df
Summary:
Capture of certain Kotlin files fails at the javalib level (probably,
some unanticipated bytecode pattern). We however can't just completely
skip Kotlin class-files during capture as those have NotNull/Nullable
annotations on methods/params that are important for Java <- Kotlin
interop (using Kt classes from Java).
Instead we can skip translation of concrete methods from Kotlin classes
while retaining method signatures with annots in the TEnv.
Reviewed By: ngorogiannis
Differential Revision: D22897638
fbshipit-source-id: 67909aa43
Summary:
There are two ways to suppress it.
1. Field level suppression annotation (was already tested). This will
apply to all constructors.
2. Constructor level annotation (this is what this test does). Sometimes
there are "fake" constructors that are not intended to be called in
prod, they might leave some fields not initialized.
Note that there are two ways to add a suppression; one has a known
problem that is documented here.
Reviewed By: artempyanykh
Differential Revision: D22864869
fbshipit-source-id: f95aaa26a
Summary: `alloc` actually allocates the array, not the `init`. Let's reflect that in our models.
Reviewed By: roro47
Differential Revision: D22864198
fbshipit-source-id: 687f9f247
Summary:
It's typically used inside another ~fold argument and it gets too
verbose.
Reviewed By: da319
Differential Revision: D22846501
fbshipit-source-id: 2fdd4271f
Summary: `Array.copyOf` model has nothing to do with Collections. Refactor it to the appropriate place
Reviewed By: roro47
Differential Revision: D22844638
fbshipit-source-id: 48dde4d53
Summary:
When expressions use generics or typecasts, CFG contains intermediate `_fun_cast` nodes which break some nullsafe heuristics and lead to false positives.
This affects different types of checks (null-check on assignment expressions, `map.containsKey` checks in assignment expressions, regular typecasts, etc.
See added tests for examples.
Reviewed By: mityal
Differential Revision: D22815631
fbshipit-source-id: 80d444b1c
Summary:
We check for supertypes in Java. Why not ObjC?
Would be good to get dulmarod's input here.
Reviewed By: roro47
Differential Revision: D22817126
fbshipit-source-id: 52c1c3f3c
Summary: This diff adds an option to shard spec files in `infer-out/specs`. For some big analysis targets, there can be too many of spec files in the one directory, which slows down IO speed for reading the spec files.
Reviewed By: jvillard
Differential Revision: D20002128
fbshipit-source-id: bd7722883
Summary: There used to be `JoinAfter n` mode where we would try to join `n` states instead of always making disjunctions. It got deleted in D14258485 and Pulse's underlying (pre-disjuncts) domain doesn't even have a join operation. `NeverJoin` mode is not useful in Pulse anymore: pulse will diverge or OOM if we don't limit the number of disjuncts. It is also not used by any other analyzer. Let's remove it.
Reviewed By: jvillard
Differential Revision: D22817425
fbshipit-source-id: 1e658f11d
Summary: This diff refactors Java specific `PatternMatch` functions into its own module. When `PatternMatch.ml` was originally created, it was mainly for Java but now it also supports ObjC. Let's refactor it to reflect the Java/ObjC separation: move all functions that operate on Java procnames into Java submodule.
Reviewed By: jvillard
Differential Revision: D22816504
fbshipit-source-id: ff6b64b29
Summary:
This avoids wasting potentially large amount of work in some
pathological situations. Suppose `foo()` has D specs/disjuncts in its
Pulse summary, and consider a node that calls `foo()` N times, starting
with just one disjunct:
```
[x]
foo()
[x1, ..., xD]
foo()
[y1, ..., yD^2]
foo()
...
```
At the end we get `D^N` disjuncts. Except, currently (before this diff),
we prune the number of disjuncts to the limit L at each step, so really
what happens is that we (very) quickly reach the L limit, then perform
`L*D` work at each step (where we take "apply one pre/post pair to the
current state" to be one unit of work), thus doing `O(L*D*n)` amount of
work.
Instead, this diff counts how many disjuncts we get after each
instruction is executed, and we already reched the limit L then doesn't
bother accumulating more disjuncts (as they'd get discarded any way),
and crucially also doesn't bother executing the current instruction on
these extra disjuncts. This means we only do `O(L*n)` work now, which is
exactly how we expect pulse to scale: execute each instruction (in
loop-free code) at most L times.
This helps with new arithmetic domains that are more expensive and
exhibit huge slowdowns without this diff but no slowdown with this diff
(at least on a few examples).
Reviewed By: skcho
Differential Revision: D22815241
fbshipit-source-id: ce9928e7c
Summary:
The old --topl-only is now --topl-biabd-only, and there's also
--topl-pulse-only. This is WIP: the latter runs pulse, but it doesn't yet
extract Topl errors from pulse summaries. (The citv part of pulse path
conditions appears to have the necessary information.)
Reviewed By: jvillard
Differential Revision: D22815250
fbshipit-source-id: a01792945
Summary:
This diff:
1. Adds general capability to model any field as nullable /
non-nullable.
2. Uses it for Boolean.TRUE and Boolean.FALSE
Reviewed By: artempyanykh
Differential Revision: D22794226
fbshipit-source-id: 95f586592
Summary: D17500386 had added the ability to give symbolic values on functions returning exceptions. However, this might cause FPs or cryptic complexity reports (especially with subclass heuristics). This diff aims to revert it back.
Reviewed By: skcho
Differential Revision: D22764266
fbshipit-source-id: 1615544d8
Summary: We model internal builtin `__new` function to return a non-null value. This fixes nullptr_dereference false positives where we explicitly check the result of a function call for nullptr when the function returns a newly created object.
Reviewed By: jvillard
Differential Revision: D22772217
fbshipit-source-id: 37d209697
Summary:
This stopped compiling on my Debian and it seems hard to fix. It was
already having compilation issues between osx and Linux but here I don't
know how to detect which type it wants since the OS is Linux too.
Reviewed By: ezgicicek
Differential Revision: D22728282
fbshipit-source-id: 818ae87e6
Summary:
This step does extra normalization so it's useful to see what's going on
when debugging. Log stuff in the html debug of the exit node.
Reviewed By: da319
Differential Revision: D22596248
fbshipit-source-id: cde3bbb6c
Summary:
Pulse has models for iterators that make them use a fake field to
remember the element of the collection they point to. But, not all
methods are modelled, and some of them look at the real field, eg
`operator==`. Since we don't update the real field in the model, this
causes imprecision.
The imprecision was visible in pudge.
Reviewed By: skcho
Differential Revision: D22576003
fbshipit-source-id: 2af6be646
Summary:
The java frontend used an unsound flow insensitive class analysis to devirtualize
some virtual calls. We remove it and let the recent devirtualizer preanalysis do the job.
This unsoudness in the Java frontend may have been here for a long time. Removing it may
modify several analysis results (specially Nullsafe) where virtual calls may look different
now.
Reviewed By: jvillard
Differential Revision: D22662739
fbshipit-source-id: c45296dce
Summary:
Changing the order of the superclasses of a struct exposes a bug in both biabduction and the devirtualiser where a method would be resolved into a still virtual method (an interface method).
The reason is that we don't check whether a super class is an interface before exploring it, and seemingly we assume that there is only one (first) superclass worth exploring. This also ignores multiple inheritance in C++.
To fix this, refactor the resolution to a complete search (not just the first super class!) which ignores Java interface methods. Also moved it to `Tenv` so that both biabduction and the devirtualiser can use it.
Reviewed By: jvillard
Differential Revision: D22357488
fbshipit-source-id: 54b96c1f4
Summary: We recently changed the translation of NSArray literals in a way that we pass a different type of argument to `arrayWithObjects:count`, such that the biabduction model doesn't work anymore. So we remove the model for now.
Reviewed By: skcho
Differential Revision: D22691611
fbshipit-source-id: 03cd940ed
Summary:
Merging global type environments for Java needs some form of non-trivial type definition merging because:
- The frontend is likely non-deterministic, so it can capture the same type differently.
- There are classes that appear with two distinct definitions (usually ordered by inclusion) when one is produced by an ABI-like compilation process (so only public fields/methods would appear for example), and one full version.
- The frontend produces dummy versions (empty definitions), and full ones.
- The location information is variously missing/present.
This diff tries to strike a balance between a full semantic merge (which depends on the frontend/buck integration) and the current code which "merges" by clobbering old definitions with new ones.
One side-effect of this diff is that code cannot expect a special order for supers.
Reviewed By: jvillard
Differential Revision: D22630286
fbshipit-source-id: fc66c7000
Summary:
This diff adds translation of `arrayWithObjects:count:`. In the previous implementation it was
translated as if it was `arrayWithObjects:`, but their function parameters are different.
In this diff, it translates an array literal `NSArray* a = @ [ 2, 3 ];` to
```
n$1=NSNumber.numberWithInt:(2:int)
n$2=NSNumber.numberWithInt:(3:int)
temp[0]:objc_object*=n$1
temp[1]:objc_object*=n$2
n$3=NSArray.arrayWithObjects:count:(temp:objc_object* const [2*8],2:int)
a:NSArray*=n$3
```
where `temp` is an additional local variable declared as array.
See,
https://developer.apple.com/documentation/foundation/nsarray/1460145-arraywithobjectshttps://developer.apple.com/documentation/foundation/nsarray/1460096-arraywithobjects?language=objc
Reviewed By: jvillard
Differential Revision: D22631305
fbshipit-source-id: 5be0a55d4
Summary:
Add a test to the repo to try and detect perf regressions in pulse.
Currently analyzed in ~0.1s. With `--pudge`, takes ~10s.
Sledge does eager normalization and canonicalization when incorporating new facts into formula contexts and the algorithm is polynomial in the number of equalities. This example generates one equality per location in the array => boom. This bypasses the recency model of arrays because the formula needs to be constructed before it can be simplified to get rid of dead variables.
The new arithmetic is not as complete as sledge's algorithm but linear in time. We could use it to simplify the formula *before* passing it to sledge. In fact, that was the original motivation.
Reviewed By: skcho
Differential Revision: D22574366
fbshipit-source-id: e9044ae09
Summary:
When applying function summaries, we are careful not to violate the
summary's assumptions about non-aliasing. For example, the summary we
generate for `foo(x,y) { *x = *y; }` will have `x` and `y` be allocated
to two different `AbstractValue.t` in the heap, representing
disjointness.
However, the current logic is too coarse and also rejects passing the
same pure value to functions that made no assumption about them being
equal or different, eg `goo(int x,int y) { int z = x + y; }`. This is
because the corresponding `AbstractValue.t` are different in the
callee's summary, but are represented by only one same value in callers
such as `goo(i,i)`.
This diff restricts the "don't violate aliasing" condition to only
consider heap-allocated values. This is consistent with separation logic
by the way: we use the implication `x|->- * y|->- |- x≠y`, which is
valid only when both `x` and `y` are both allocated in the heap as in
the left-hand-side of `|-`.
Reviewed By: skcho
Differential Revision: D22574297
fbshipit-source-id: 206a18499
Summary:
This will allow all the analyses to be able to call closures without any special treatment: we transform the call to variables that point to closures into normal function calls. We treat only ObjC blocks at the moment, with C++ lambdas to be done as a next step.
We aimed to achieve certain results in Pulse (see tests: avoid memory leaks and NPEs FPs) while also keeping the biabduction analysis working as before.
We also checked that for the examples analyzed Pulse behaves like the correct semantics of ObjC programs with blocks.
Reviewed By: jvillard
Differential Revision: D22547333
fbshipit-source-id: efe56ed51
Summary: Lambda is called using `operator()`. We need to know the information of captured variables when `operator()` procedure is being analysed. This diff records lambda captured variables in `operator()` procdesc. The complication arises from the fact that procdesc for `operator()` is created before translating lambda expression or during the translation of lambda expression where captured variables are translated. To solve this issue, we update existing `operator()` procdesc attributes with captured variable information when we translate lambda expression.
Reviewed By: jvillard
Differential Revision: D22374495
fbshipit-source-id: 44909adea
Summary:
This diff fixes a bug that eval_arr misses the case when a stack
variable points to an array.
Reviewed By: ezgicicek, roro47
Differential Revision: D22596999
fbshipit-source-id: 7c4a13d01
Summary: Add cost model for most common `NSString` functions in cost analysis
Reviewed By: skcho
Differential Revision: D22433005
fbshipit-source-id: 2f57bbda9
Summary: If a node is unreachable and the cost of the node is Top, we were giving Top cost :( Let's fix it.
Reviewed By: skcho
Differential Revision: D22548269
fbshipit-source-id: d79743669
Summary:
We update the type of captured variables to include information about capture mode (`ByReference` or `ByValue`) both for procdesc attributes and the closure expression.
For lambda: closure expression now contains correct capture mode for capture variables. Procdesc still does not contain information about captured variables which we will address in the next diff.
For objc blocks: at the moment all captured variables have mode `ByReference`. Added TODOs to fix this.
Reviewed By: jvillard
Differential Revision: D22572054
fbshipit-source-id: 4c88678ee
Summary: This diff prints where the cost becomes top by calling `html_debug_new_node_session`. This will print them in the start node of the procedure in html. There are already printing functions in `get_instr_node_cost_record`.
Reviewed By: ezgicicek
Differential Revision: D22547578
fbshipit-source-id: 257e957c0
Summary:
The frontend was hackily adding protocols as superclasses in the tenv, with the implicit encoding that the first element in the list was the actual superclass. This was clearly very fragile.
Protocols are not used in the backend at the moment, so for now we will remove them from the list of superclasses to have more consistency in the tenv.
Reviewed By: ngorogiannis
Differential Revision: D22525078
fbshipit-source-id: 2aef1fab1
Summary: This diff extends the value domain to express multiple markers.
Reviewed By: ngorogiannis
Differential Revision: D22524864
fbshipit-source-id: b8e4af2eb
Summary:
As title
Model `NSString` as `JavaString`.
Since `NSArray` does not contain information about its type of element, we do not use associate string with collection as in Java and C++. In Java, String model is implemented using java collection, and for C++, string model is implemented using vector.
So instead, we use existing `JavaString` model.
Reviewed By: skcho
Differential Revision: D22431949
fbshipit-source-id: 7cdde1ad7
Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.
The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.
Reviewed By: jvillard
Differential Revision: D22170506
fbshipit-source-id: a014ee7d7
Summary: To avoid NULLPTR_DEREFERENCE false positives we want to model some functions as returning non-null. A new flag --pulse-model-return-nonnull allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D22431564
fbshipit-source-id: 9944c7382
Summary: Make the module interface safe wrt closing the classpath channel when done, plus reducing the exposed API.
Reviewed By: skcho
Differential Revision: D22411685
fbshipit-source-id: 11316c577
Summary: `addAll` adds elements one by one and hence takes linear time. We didn't have a model for this and considered it O(1).
Reviewed By: skcho
Differential Revision: D22375157
fbshipit-source-id: 65b82bfae
Summary: This diff prevents printing line numbers of loop in the trace description, which helps to keep the same descriptions even when the line number of a function is changed in tests.
Reviewed By: ezgicicek
Differential Revision: D22375584
fbshipit-source-id: 676d1a7cc
Summary:
This one is observed to be more memory efficient. Intuitively, maps need
to be re-allocated more often than lists for balancing. In pulse, we'll
often only ever add new values, in increasing order (when they are fresh
variables created as we symbolically execute the program), which pushes
maps into their worst-case allocation pattern. At least I suspect that's
what happens. With lists, this case is handled much better as lists are
not re-allocated when adding elements.
This is somewhat confirmed by benchmarking and observing GC stats.
Reviewed By: skcho
Differential Revision: D22140908
fbshipit-source-id: 29815112f
Summary:
Messed up the aggregation of GC stats in the previous commit.
It's cleaner to have GC stats (and analysis time) outside of
BackendStats as the rules for computing them is different than the rest,
eg notice how "analysis time" needed to be corrected at the end of the
run, and similarly for GC stats. Thus, refactor this part.
Also output different aggregations of GC stats: +/max/average.
Reviewed By: skcho
Differential Revision: D22332496
fbshipit-source-id: eefd9dd72
Summary:
Keyword `thread_local` in cpp allows us to create a variable with thread storage duration, meaning that the object's lifetime begins when the thread begins and ends when the thread ends.
We get `NULLPTR_DEREFERENCE` false positive for `thread_local` variable since we reallocate it in the `VariableLifetimeBegins` metadata instruction and we do not see further updates to the variable. To solve the issue we special case `VariableLifetimeBegins` instruction for global variables.
Reviewed By: jvillard
Differential Revision: D22284135
fbshipit-source-id: 13c14ef90
Summary: Create test for the most common unmodeled function in inferbo that acts as control variable.
Reviewed By: skcho
Differential Revision: D22331168
fbshipit-source-id: 1913682db
Summary: Add objc test for customized class and blocks. Mostly sanity test.
Reviewed By: ezgicicek
Differential Revision: D22043918
fbshipit-source-id: 917deeea7
Summary:
This diff adds a model of `File.listFiles` as returning an array with
a symbolic length.
Reviewed By: ezgicicek
Differential Revision: D22332258
fbshipit-source-id: 6ca593b8b
Summary: This diff adds support for `com.facebook.litho.sections.Section` which mimics the behavior for `com.facebook.litho.Component`.
Reviewed By: skcho
Differential Revision: D22309039
fbshipit-source-id: 3510441a8
Summary:
Following from previous diff.
**Idea** - 80% of functions with Top cost are caused by calling top-costed callees, i.e. callee's Top cost is simply propagated to its transitive callers, so the aim is to investigate such root callees along with the number of their transitive callers.
Consider the following code
```
void bar1() {
// top cost function
}
void bar2() {
// another top cost function
}
void baz(){
// baz have top cost because of bar
bar1();
}
void foo() {
// goo have top cost because of baz
baz();
bar2()
}
```
Clearly, the root cause of the foo being top cost is `bar1` and `bar2`.
1. When we are analyzing `baz`, we know that it calls `bar1`, which is top cost, so we record that `baz = { T, bar1 } `.
2. Now, say we are analyzing foo.
When we analyze the call to `baz`, we found out that the top cost of `baz` is caused by `bar1`, so we record `foo = { T, bar1 }`.
When we analyze the call to `bar2`, we know that `bar2` is top cost, but since at this stage we only want to deal with the first top cost function we met, so we ignore it.
Since we are keeping track of top cost function by examining the `Call` instruction, we would expect to see two log of `bar1` in the result. The test plan confirms it.
Reviewed By: ezgicicek
Differential Revision: D22231457
fbshipit-source-id: 45d48e4a7
Summary:
New `debug` command takes over from `explore` the `--procedures`, `--source-files` functionality and adds `--global-tenv` for printing the global type environment.
Also, uncrustify printing of type environments.
Reviewed By: jvillard
Differential Revision: D22284807
fbshipit-source-id: 9c6fb0c7a
Summary:
Log stats obtained via `Gc.stat ()` for various phases:
- capture (doesn't include child infer processes created by the build
system)
- analysis
- worker processes of the analysis, aggregated
- reporting phase
- total GC stats for the main infer process
Reviewed By: jberdine
Differential Revision: D22140131
fbshipit-source-id: b0ee39559
Summary:
We already had a heuristic to deal with assignment expressions, but it
relied on the very previous CFG node to have a non-empty list of instrs.
In some cases, however, this previous node is a Join_node with no instrs,
so we need to take one more step back to find what we're looking for.
I've also added a bit more logging around this functionality, so it's
easier to debug/tune in future.
Reviewed By: ngorogiannis
Differential Revision: D22282930
fbshipit-source-id: 024eec145
Summary:
This model is very important in the analysis of ObjC classes because the pattern
```
- (instancetype)init {
if (self = [super init]) {
...
}
return self;
}
```
is very common, so we need to know that if the super class is `NSObject`, the implementation of `init` is returning `self`, otherwise it's a skip function and we don't get the correct spec for the function. We fix some memory leak FP with this model, see test.
Reviewed By: ezgicicek
Differential Revision: D22259281
fbshipit-source-id: 3ee48c827
Summary:
We need to check if `folly::Optional` is not `folly::none` if we want to retrieve the value, otherwise a runtime exception is thrown:
```
folly::Optional<int> foo{folly::none};
return foo.value(); // bad
```
```
folly::Optional<int> foo{folly::none};
if (foo) {
return foo.value(); // ok
}
```
This diff adds a new issue type that reports if we try to access `folly::Optional` value when it is known to be `folly::none`.
Reviewed By: ezgicicek
Differential Revision: D22053352
fbshipit-source-id: 32cb00a99
Summary: This linters were not used much anymore, so we can delete them.
Reviewed By: ngorogiannis
Differential Revision: D22233895
fbshipit-source-id: f31180a05
Summary: There is now a compilation check for UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK so this check is less useful. Also the check REGISTERED_OBSERVER_BEING_DEALLOCATED is useful only in an old version of iOS.
Reviewed By: ngorogiannis
Differential Revision: D22231851
fbshipit-source-id: 72151fef5
Summary:
Extend BasicCost to BasicCostWithReason which contains a record of the form
```{cost: BasicCost.t; proc_name_list: Procname.t list}```
This is done so that we can keep track of top cost function.
So the idea is that 80% of functions with Top cost are caused by calling top-costed callees, i.e. callee's Top cost is simply propagated to its transitive callers, so the aim is to investigate such root callees along with the number of their transitive callers.
Therefore, we create an extension that match `cost` to the root cause function.
This diff only handles the extension. Details about how we update the root cause function is in the next diff.
Reviewed By: skcho
Differential Revision: D22158717
fbshipit-source-id: 6498d904f
Summary:
This diff tries to support a specific form of linked list iteration in Java.
```
while (p != null) {
p = p.getNext();
}
```
This example was a constant cost before because the cost checker could not detect that it is an iteration on a linked list.
The heuristic this diff implemented is:
(1) `p = p.getNext()`: It tries to find this specific form of assignment. Then, it increments `p.linked_list_index` by 1. Note that `linked_list_index` is a virtual field for keeping an index in the linked list. Its initial value is always 0.
(2) At `p != null`, it tries to prune the value of `p.linked_list_index`: the upper-bound of `p.linked_list_index` is pruned by `<= p.linked_list_length`. Here again, `p.linked_list_length` is also a virtual field to denote the length of the linked list.
Reviewed By: ezgicicek
Differential Revision: D22234892
fbshipit-source-id: 2fee176bb
Summary: Log unmodeled function in cost analysis and send result to scuba.
Reviewed By: ezgicicek
Differential Revision: D22158510
fbshipit-source-id: c6eade67e
Summary: This continues on the previous diff by removing the model for `__bridge_transfer` in biabduction. This also had the name __free_cf which we kept for compatibility with biabduction until now but that we can now change.
Reviewed By: ezgicicek
Differential Revision: D22207396
fbshipit-source-id: 7a175eca6
Summary: These models for Memory Leaks have been ported to Pulse, so we can remove the models in biabduction and corresponding tests.
Reviewed By: skcho
Differential Revision: D22206287
fbshipit-source-id: e17499ad3
Summary:
Move the implementation of implicit getters and setters from the biabduction to the clang frontend so these methods are accessible to all the checkers.
*Background*: In Objective-C when properties are created in the interface of a class, the compiler creates automatically the instance variable for it and also the getter and setter in the implementation of the class. In the frontend we collect the information about which method is the implicit getter and setter of which instance variable (we get the method declaration but not the implementation), and here we add the implicit implementation.
Reviewed By: skcho
Differential Revision: D22187238
fbshipit-source-id: 76e0508ed
Summary: Let's make package name match the directory name to follow Java's file lookup conventions
Reviewed By: skcho
Differential Revision: D22183964
fbshipit-source-id: b9958b975
Summary:
Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain. The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`).
Reported by Andreea Costea.
Reviewed By: ezgicicek
Differential Revision: D22186240
fbshipit-source-id: 84e5e72b1
Summary:
There is a lot of subtlety in our parsing of buck targets on the command line, that is then just thrown away. Push this one level up, getting rid of the special case where in Clang mode if we only have "normal" targets we don't resolve them.
Also introduce a proper variant for buck target types.
Reviewed By: skcho
Differential Revision: D22160490
fbshipit-source-id: 500c1b12c
Summary:
This diff revises assignment semantics, so it can store/load from the
heap location.
Reviewed By: ezgicicek
Differential Revision: D22042823
fbshipit-source-id: 20d91bfc5
Summary:
Nullability of the assignment result is not refined in code snippets
like:
```
while ((a = foo.getA()) != null) {
nonNullableVal = a;
}
```
Let's add a test for this.
Reviewed By: jvillard
Differential Revision: D22136218
fbshipit-source-id: 206c368d6
Summary:
Better API for creating issue types:
- distinguish hidden/normal/dynamic issue types
- normal issue types should always be documented
- add "TODO" to missing documentation
- dynamic issue types are the only ones that can be created outside of
IssueType.ml
I had to document the new CCBM and the resource leak lab exercise to
keep Help.ml happy, did `make doc-publish`.
Reviewed By: ngorogiannis
Differential Revision: D22118766
fbshipit-source-id: 3d0194518
Summary:
A bug in docusaurus makes relative URLs fail depending on how the page
was accessed, because the URL of a page in docs/ will end in / if
accessed directly or via hyperlink, but that / will be omitted when
clicking on the sidebar. The final / makes all the difference when
interpreting relative URLs so relative URLs are essentially broken.
See https://github.com/facebook/docusaurus/issues/2832 for more details.
This changes URL generation to generate URLs /docs/next/..., and
manually substitute relative URLs that had been written by hand.
Also fix a few other things about outdated links/comments.
Finally, `make doc-publish`.
Reviewed By: dulmarod
Differential Revision: D22117187
fbshipit-source-id: 32e2ba7e1
Summary: Buck uses its own estimate for how many workers to spawn, there is no need to pass our own estimate for capture.
Reviewed By: ezgicicek
Differential Revision: D22065565
fbshipit-source-id: 4c062a9aa
Summary:
Needed to remove user_documentation for the new
CONFIG_CHECK_BETWEEN_MARKERS issue type otherwise it violated the
invariant that the corresponding checker should be documented too but
its development has just started.
Reviewed By: skcho
Differential Revision: D22065820
fbshipit-source-id: 4b3a58850
Summary:
Add objc test for ```NSArray``` and ```NSMutableArray```.
```NSMutableArray``` is a subclass of ```NSArray```.
For documentation of ```NSArray```, https://developer.apple.com/documentation/foundation/nsarray?language=objc
For documentation of ```NSMutableArray```, https://developer.apple.com/documentation/foundation/nsmutablearray?language=objc
The underlying mechanism for ```NSMutableArray``` is quite complicated. It changes the underlying data structure during runtime, so it is possible to have say O(log n) complexity for accessing element in array. (See here https://opensource.apple.com/source/CF/CF-855.11/CFArray.h) However, this is unlikely to happen if the engineer does not abuse the usage of the class ```NSMutableArray``` according to at least two ios engineers. So here the complexity is set to match the normal expectation of the complexity.
Reviewed By: ezgicicek
Differential Revision: D22041277
fbshipit-source-id: c27f43167
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21998170
fbshipit-source-id: e7759f62f
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21998150
fbshipit-source-id: 337a8938a
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21935546
fbshipit-source-id: 092abb92c
Summary: Most of them had some form of documentation in source comments.
Reviewed By: ngorogiannis
Differential Revision: D22020016
fbshipit-source-id: 468f86658
Summary: Pulse has now a better version of this check, so let's delete it.
Reviewed By: ngorogiannis
Differential Revision: D22019247
fbshipit-source-id: 344678225
Summary: Remove unsafe invocations of `String.rsplit2_exn` as this code may run on C++.
Reviewed By: dulmarod, jvillard
Differential Revision: D22042750
fbshipit-source-id: b2879e17b
Summary:
This issue type was not giving good results and can be replaced by
Pulse's version.
Reviewed By: ngorogiannis
Differential Revision: D22019551
fbshipit-source-id: 5cf3db46d
Summary:
Add objc test case for ```NSInteger``` and ```NSString```.
The test cases are adapted from java test case: ```IntTest.java```, ```StringBuilder.java```, and ```StringTest.java```.
Inspection of the record will be done later.
Reviewed By: ezgicicek
Differential Revision: D21994620
fbshipit-source-id: 0c1d7b34e
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
Daiva Naudziuniene
Nikos Gorogiannis
Artem Pianykh
Jules Villard
Mitya Lyubarskiy
Sungkeun Cho
Ezgi Çiçek
Qianyi Shu
Radu Grigore
David Pichardie
Dulma Churchill
Josh Berdine
GaloisNeko
Andrew V. Jones
Artem Pyanykh