Summary:
It is undefined behavior to dereference end iterator.
To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself.
Reviewed By: ezgicicek
Differential Revision: D21178441
fbshipit-source-id: fd6a94b0b
Summary: We mistakenly invalidated the set element which causes spurious vector invalidation errors. Instead, we should modify it without any invalidation.
Reviewed By: jvillard
Differential Revision: D21521943
fbshipit-source-id: 67963967e
Summary:
This will is useful for understanding and debugging file level analysis
flow.
Reviewed By: jvillard
Differential Revision: D21449240
fbshipit-source-id: 7c259674b
Summary:
This diff adds semantics of assume null, heuristics. When `assume(x == null)`, it removes the
methods called on the builder `*x` from the abstract state.
```
x -> {p}
p -> {method1 called}
assume(x == null)
x -> {p}
```
This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder
object, which cannot imply that the object `p` does not exist in the concrete semantics. The
unsoundness may appear when there is an alias (see the FP test added).
Reviewed By: ezgicicek
Differential Revision: D21502923
fbshipit-source-id: 2e392bd89
Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array.
Reviewed By: skcho
Differential Revision: D21448322
fbshipit-source-id: 7d44354b5
Summary:
These 2 methods are automatically supplied for all enums, with
predefined behavior and nullability: https://www.geeksforgeeks.org/enum-in-java/
(Note that they are not part of java.lang.Enum class).
This will allow using them in unvetted third part and under strict mode.
Reviewed By: artempyanykh
Differential Revision: D21501716
fbshipit-source-id: 104082d15
Summary:
The only thing keeping this module alive were unit tests, proving once
and for all that unit tests are bad.
Reviewed By: ngorogiannis
Differential Revision: D21451855
fbshipit-source-id: e63995732
Summary:
- move unit/clang/ to clang/unit/ and make it a dune library
- move unit/nullsafe/ to nullsafe/unit/ and make it a dune library
- make unit/ a dune library
- inline most of dune.common.in into dune.in and make more explicit
rules for each binary as they don't depend on the same libraries
- move inferunit from unit/ to ./ like the other toplevel binaries
Reviewed By: skcho
Differential Revision: D21440822
fbshipit-source-id: 075c693e0
Summary:
Using the same trick as for the java frontend: define a dune library
that takes either all the modules in the directory (except possibly
stubs) or none of the modules (except possible stubs).
In order to break the circular dependency between al/ and clang/,
introduce a dirty callback in clang/.
Reviewed By: dulmarod
Differential Revision: D21440823
fbshipit-source-id: ac6b40b4e
Summary:
Kill java_stubs/ with this one easy trick:
- java/dune contains either the "normal" modules or just the
JavaFrontendStubs module
- libraries that depend on java need to open JavaFrontendStubs if java
is disabled to bring the expected modules from java/ into their
namespace
Also needed to move biabduction/Prover.Subtyping_check to
absint/SubtypingCheck because the Java frontend was using it.
Reviewed By: ngorogiannis
Differential Revision: D21435937
fbshipit-source-id: af957253a
Summary:
Because in the real semantics CFRelease can be used more than once, and also the variables can be used after CFRelease in general, modelling this as `free` causes many `USE_AFTER_FREE` errors. Now we change the model to not add the `Invalid CFree` attribute, but to just remove the `Allocated` attribute. So we can model memory leaks in the simple case of `Create` and not `CFRelease` before going out of scope, but we avoid the `USE_AFTER_FREE`.
Since the model for CFRelease now diverges from free, changed the command line option for modelling to `pulse-model-release-pattern`.
Reviewed By: jvillard
Differential Revision: D21324895
fbshipit-source-id: ab323d981
Summary:
This diff suppresses the internal error on mismatched signedness. It happens usually when inferbo
has incomplete type information. Since it does not seem to fix in the near future, let's suppress
them, not to hide other internal errors.
Reviewed By: jvillard
Differential Revision: D21455062
fbshipit-source-id: 4562bb177
Summary:
OSX filesystem gets confused by its case-insensitivity and the library
trick of having TOPL.ml (vs the existing Topl.ml).
Reviewed By: skcho
Differential Revision: D21456696
fbshipit-source-id: 2f6ffc2fb
Summary:
Needed to move some "Differential" files out of the way. This makes
sense I think: backend/ is only about orchestrating the various
checkers.
Reviewed By: ngorogiannis
Differential Revision: D21431968
fbshipit-source-id: 14fad8b88
Summary:
Last checker for good. Updated the README of the lab to reflect changes.
Delete now-defunct SummaryPayload: all checkers now behave in a
functional manner as far as summary payloads are concerned.
Reviewed By: ngorogiannis
Differential Revision: D21426550
fbshipit-source-id: 2b52b9f5b
Summary:
The global analysis is doing funky stuff directly with `Summary.OnDisk`.
In order to make starvation/ its own dune library this part needs to
either use ondemand or moved elsewhere. Let's do the latter for now to
avoid changing the behaviour in the middle of the refactoring.
Reviewed By: ngorogiannis
Differential Revision: D21425699
fbshipit-source-id: ab9e2f429
Summary:
It started with wondering which function the "O(1)" comment was about
but I ended up deleting `is_singleton` because it's unused and it can be
easily re-implemented.
Reviewed By: ngorogiannis
Differential Revision: D21425225
fbshipit-source-id: 5ee3e189c
Summary:
Also ondemand doesn't need to call Topl itself after an analysis.
Inline last call site of SummaryReporting (ondemand.ml) and delete the
file.
Reviewed By: ngorogiannis
Differential Revision: D21424386
fbshipit-source-id: 064f4e261
Summary:
- make quandary an `interprocedural`
- move quandary traces to absint/ since they are also used at least by
SIOF
- no more `Summary.OnDisk.dummy` :')
Reviewed By: ngorogiannis
Differential Revision: D21408391
fbshipit-source-id: cc53d2c6c
Summary:
There is a case where the class name is "A$1$B$2".
In this case, we would correctly say it is an anonymous class, and
return A$1$B as user defined, which is bad: now we can get the outer
class which will be A$1 that will be anonymous again.
This was leading to tricky bugs.
Now, get_user_defined_class name will return something that is indeeed
contains only user defined names.
There is one tricky pathological case left: when the outermost class is
anonymous, which can in theory occur. This might lead to other tricky
bugs, so the follow up will be to rewrite API of JavaClassName.t so that
this case is made clear for the client.
But lets unbreak nullsafe fore now first.
Reviewed By: ngorogiannis
Differential Revision: D21449686
fbshipit-source-id: b0ba4702e
Summary: This will allow us to track cases when this assert fires
Reviewed By: ngorogiannis
Differential Revision: D21427776
fbshipit-source-id: 96b6d7c3b
Summary: This diff gets only one disjunct from blacklisted callee, in order to avoid OOMing in specific cases.
Reviewed By: jvillard
Differential Revision: D21406023
fbshipit-source-id: f9214c9c6
Summary:
Needed to move a bunch of files around to make this happen. Notably,
moving "preanal.ml" outside of checkers/ into backend/ since it needs to
modify the proc desc in the summary. Also hoisting goes to cost/.
Reviewed By: skcho
Differential Revision: D21407069
fbshipit-source-id: ebb9b78ec
Summary:
An easy one. One subtlety: I needed to name the library "pulselib"
instead of "pulse" because dune got confused by the Pulse.ml module.
Reviewed By: skcho
Differential Revision: D21401815
fbshipit-source-id: 05e75b1fa
Summary:
Main change: needed to cut the dependency of inferbo on pulse, since
pulse will need to depend on inferbo. Achieved by changing the ad-hoc
"PulseValue" into a little less ad-hoc "ForeignVariable" variant.
Reviewed By: skcho
Differential Revision: D21401816
fbshipit-source-id: bb341b9ff
Summary:
Changing inferbo required changing all the analyses that depend on it
too. This introduces a new feature of the the new framework: the ability
for the checkers to read other analyses' payloads in a more functional
way.
Reviewed By: ezgicicek, skcho
Differential Revision: D21401819
fbshipit-source-id: f9b99e344
Summary:
An easy one. Will be needed eventually to make checkers/ its own dune
library.
Reviewed By: ngorogiannis
Differential Revision: D21401818
fbshipit-source-id: 64e8a4bf4
Summary:
`RegisterCheckers` is now doing a bunch of work to convert the new-style
checkers to the good old Callbacks datatypes. Extract the conversion
code into another module before more is added. A good opportunity to
document them.
Reviewed By: ezgicicek
Differential Revision: D21401817
fbshipit-source-id: 4cba3aa7b
Summary:
This module needs to be above all checkers since it knows about all the
checkers; put it at the same level of ondemand and callbacks.
Reviewed By: ezgicicek
Differential Revision: D21401821
fbshipit-source-id: f40dba6dd
Summary: Build tool wrappers sometimes have issues when their output streams are redirected to those of infer's while one of those streams is read and used in infer. This diff side-steps this problem by always redirecting the stream of interest to a file (which also helps in debugging), while logging the other stream through `Logging.progress`.
Reviewed By: jvillard
Differential Revision: D21404736
fbshipit-source-id: 04c92799c
Summary:
- move a few files from checkers/ so that nullsafe can depend on them
- nullsafe depends on a few files in biabduction/ via Errdesc (not the
biabduction analysis itself but some datatypes and functionality):
- when possible, I've moved the individual functions elsewhere, in absint/Decompile.ml
- nullsafe still depends on a function in Errdesc that unfortunately
depends on a bunch of biabduction datatypes like Prop(!) and some
other functionality that for now is embedded in biabduction
(substitution in SIL instructions).
Reviewed By: mityal
Differential Revision: D21351906
fbshipit-source-id: 757528120
Summary: So it can be used by dune libraries without depending on backend/.
Reviewed By: dulmarod
Differential Revision: D21351908
fbshipit-source-id: d288f9179
Summary:
Easy cleanup. The tenv is now part of the analysis_data that is in the
closure passed to the Dataflow framework.
Reviewed By: dulmarod
Differential Revision: D21351907
fbshipit-source-id: 592542c06
Summary:
This turned into a pretty big refactoring: the
`IntraproceduralAnalysis.t` needs to be passed around through quite a
few functions. These functions usually depended on
tenv/proc_desc/proc_name that are already in the `analysis_data` so
refactored that too (checking that these were indeed the same as in the
`analysis_data` record (using my own eyeballs). Interestingly there is
one place where we actually turn the analysis to other proc descs than
the original one in eradicate.ml so I've added a small comment there.
Reviewed By: mityal
Differential Revision: D21351909
fbshipit-source-id: 6e6330e5b
Summary: The contract for reporting races in C++ is to flag races between writes under lock with reads without a lock. This diff restores that contract which had been violated by recent changes.
Reviewed By: jberdine
Differential Revision: D21383876
fbshipit-source-id: 6a84e1506
Summary: As per title. Also, hide most deduplication functionality inside a module.
Reviewed By: skcho
Differential Revision: D21382377
fbshipit-source-id: d979f5b54
Summary:
This diff changes way we treat classes w.r.t. to Nullsafe modes when
issuing meta-issues.
Previously, we considered nested class independently of the outer one.
This was leading to a tricky case: when the class is clean but nested
class needs fixing, meta-info told that class can be Nullsafe.
This is counter-intutive and lead to problems when users tried to follow
wrong nullsafe suggestions for this case.
After this diff we:
1. Start calculating meta-issues only on the outermost level. This will simplify
reasoning about nullsafe stats.
2. Aggregate all nested issues counters to corresponding outer-level class.
Among others, CLASS_CAN_BE_NULLSAFE Advice will finally become
actionable in all known cases.
Reviewed By: artempyanykh
Differential Revision: D21353607
fbshipit-source-id: a17c6958a
Summary:
That function was testing if a proc is defined (ok) and if so if it also
had no summary. The second check is wrong because it could be that the
function hasn't been analysed yet. We should call "Ondemand" instead.
But, it seems like a weird check so I just deleted it and replaced is
with just the "is defined" check.
Renamed the "is_library" field in typeOrigin to "is_defined" to better
reflect the expectations. While I was at it, inlined record type
definitions in `TypeOrigin.t`. They were already inlined except for 2!
Reviewed By: dulmarod
Differential Revision: D21351453
fbshipit-source-id: 1acc7ff90
Summary:
This is to eventually remove eradicate's dependency on Ondemand and
other modules in backend/.
Reviewed By: mityal
Differential Revision: D21351456
fbshipit-source-id: 1c4723cbc
Summary: Improve determinism by sorting the order of capture databases before merging.
Reviewed By: jvillard
Differential Revision: D21378208
fbshipit-source-id: 9c82d9d56
Summary:
These exceptions were caught earlier before but D21257474 made absint
log an error every time before reraising them.
The exception type had to move to IR/ or absint/, so I moved
"SchedulerTypes" to "absint/TaskSchedulerTypes" and added the restart
scheduler's exception there. There is already a "Scheduler.ml" file in
absint/ so to address the ambiguity I added "Task" in front of that one.
Reviewed By: ngorogiannis
Differential Revision: D21348593
fbshipit-source-id: 58055c9b7
Summary: Factor out common behaviour and error handling in executing buck commands, while protecting from `SIGQUIT` which results in thread dumps appearing in standard output.
Reviewed By: jvillard
Differential Revision: D21331696
fbshipit-source-id: d3b6abe2d
Summary:
List of things happening in this unreviewable diff:
- moved PulsePathCondition to PulseSledge
- renamed --pulse-path-conditions to --pudge
- PulsePathCondition now contains all the arithmetic of pulse
(inferbo+concrete intervals+pudge). In particular, moved arithmetic
attributes into PulsePathCondition.t. PulsePathCondition plays the
role of PulseArithmetic (combining all domains).
- added tests for a false positive involving free()
- PulseArithmetic is now just a thin wrapper around PulsePathCondition
to operate on states directly (instead of on path conditions).
- The rest is mostly moving code into PulsePathCondition (eg, from
PulseInterproc) and adjusting it.
Reviewed By: jberdine
Differential Revision: D21332073
fbshipit-source-id: 184c8e0a9
Summary:
We have a common entry point where we skip analysis in nullsafe.
This logic is copied from `Reporting.log_issue_from_summary`.
I believe this should not exist in Reporting: it is not the right place
to decide whether to suppress issues: we should not try to report it in
first place.
Because of that we falsely report "needs improvement" meta-issue while
we don't issue any (they were suppressed but participated in needs
improvement count calculations).
Now this change will make meta-issue to be synced with what the user
actually sees.
Down the line we should have a more reliable fix for that.
So far I reviewed suppressing code and looks like we should not suppress
anything else (unless explicitly SuppressLint-ed, which is fine).
Reviewed By: artempyanykh
Differential Revision: D21328634
fbshipit-source-id: 120ce06d1
Summary:
Add a new data structure and use it for the map of memory accesses to
limit the number of destinations reachable from a given address. This
avoids remembering details of each index in large arrays, or even each
field in large structs.
Reviewed By: skcho
Differential Revision: D18246091
fbshipit-source-id: 5d3974d9c
Summary:
Kotlin has an experimental support for [JSR-305 custom nullability
qualifiers](https://github.com/Kotlin/KEEP/blob/master/proposals/jsr-305-custom-nullability-qualifiers.md).
Annotating Nullsafe in a special way makes kotlinc recognize it as
such custom nullability qualifier and therefore treat types coming
from Nullsafe Java classes **not** as platform types, but rather
proper nonnull/nullable, which affects:
1. Generated bytecode (more thorough null-checks).
2. Type inference in the IDE.
NOTE re: p.1: one might expect that with properly annotated Java code
Kotlin would avoid inserting runtime checks. This is not how
Kotlin-Java interop works - in reality Kotlin does even more runtime
checking for Java code annotated as Nonull, which IMO is a good
thing, since you can't trust Java anyway.
Reviewed By: mityal
Differential Revision: D21278440
fbshipit-source-id: d0598738a
Summary:
The idea was to keep track of why we know certain facts but actually
these traces are never read. Other arithmetic facts (BoItv and the path
condition) don't have histories so remove them from concrete intervals
too.
Reviewed By: dulmarod
Differential Revision: D21303353
fbshipit-source-id: eecf07b05
Summary:
It suppresses cost reports of access methods, anonymous class methods, and auto-generated methods.
For those methods, this diff blocks reporting both expensive
issue (`EXPENSIVE_COLD_START/_UI_THREAD`) and complexity increase issue (`COMPLEXITY_INCREASE`).
Reviewed By: jvillard
Differential Revision: D21303068
fbshipit-source-id: 1c9533956
Summary:
The C++ tests were a bit of a mess. This diff tries to enforce the following principles:
- mark every function with `_ok` or `_bad` so that when a function appears in `issues.exp` it's easy to figure out the intention;
- mark every false negative and positive with `FP_` and `FN_` to document expectations;
- make every function access one field and participate in at most one issue report so that it's easier to assess changes.
Reviewed By: jvillard
Differential Revision: D21278627
fbshipit-source-id: 9698f716f
Summary:
We were invalidating "*(vec.__infer_backing_array)" instead of the
address of the field itself.
Reviewed By: ezgicicek
Differential Revision: D21280357
fbshipit-source-id: 48b984800
Summary:
The directory was created to have several sets of nullsafe tests but
there is only one in the end. Remove the redundant "-default".
Reviewed By: mityal
Differential Revision: D21300205
fbshipit-source-id: 46ed8b032
Summary:
The directory names had some interesting variety due to historical
reasons.
- {c,cpp,objc,objcpp}/errors/ date from the time when infer was only
biabduction
- java/infer/ dates from the time when we had an "--analyzer" option and
"infer" was one of them (sic), and eg another was "eradicate".
- c/biabduction/ dates from the time when the biabduction analysis was
being migrated to the "checkers" (AI) framework. For some reasons the
tests there are not a subset of c/infer/ but seem to be entirely new
tests.
The convention now dictates that we should name all of these
*/biabduction/. This diff moves the existing tests from c/biabduction/
into c/biabduction/misc/.
Reviewed By: mityal
Differential Revision: D21300147
fbshipit-source-id: 516d1cb15
Summary:
The test for the ant integration used to import all of biabduction tests
via a symlink. This is extremely annoying: whenever the biabduction
tests change, so do the ant tests.
Replace the ant tests with a simple single file project.
Reviewed By: ngorogiannis
Differential Revision: D21301450
fbshipit-source-id: 0d67d71d7
Summary:
Based on a shrewd observation by mityal, we can copy a little bit of
code from nullsafe and cut the dependency between biabduction and
nullsafe. The trick was to notice that biabduction doesn't use the full
power of the functions it was calling.
Reviewed By: mityal
Differential Revision: D21282656
fbshipit-source-id: 906847c26
Summary:
By far the most annoying thing to migrate. There will be a bunch of
these diffs.
Reviewed By: dulmarod
Differential Revision: D21261635
fbshipit-source-id: 0f290dd96
Summary:
This shows how the strategy for making each analysis its own library
looks like. Starting with biabduction since it's one of the worst ones.
A checker cannot depend on ProcData (in its current form) as it contains
a Summary.t. We don't want to change all the analyzers at once so let's
make up a new type. The new type also contains callbacks for Ondemand
since a checker that is its own dune library cannot call Ondemand
directly either (because Ondemand needs Summary.OnDisk).
Once all checkers are migrated we should be able to reclaim the
callbacks set up by callbacks.ml in exchange for these new callbacks,
therefore achieving a neutral callback karma.
Reviewed By: dulmarod, skcho
Differential Revision: D21261638
fbshipit-source-id: fa91ca50f
Summary:
Looks like this one was already causing circular dependency issues!
Saves threading the callback through *many* functions.
Reviewed By: ngorogiannis
Differential Revision: D21261636
fbshipit-source-id: 2b23aa07d
Summary:
- needed to make biabduction/ its own library as it shouldn't depend on
backend/Printer as a result
- it's a higher level of abstraction
Changed NodePrinter to not swallow biabduction timeouts, thereby
removing its footgunness.
Reviewed By: ngorogiannis
Differential Revision: D21261645
fbshipit-source-id: 592526d85
Summary:
absint/ is its own dune library. There was one last obstacle: we need
callbacks to `NodePrinter`. We'll add more to `AnalysisCallbacks` in future
diffs.
Reviewed By: ngorogiannis
Differential Revision: D21257476
fbshipit-source-id: 3a2ddef14
Summary:
`State` is used by the AI framework, which isn't supposed to know about
biabduction/. Split the biabduction-specific parts into
biabduction/State.ml and keep the rest in absint/AnalysisState.ml.
Reviewed By: ngorogiannis
Differential Revision: D21257470
fbshipit-source-id: e01d1fed3
Summary:
`ProcData.t` contains a `Summary.t`. Eventually we want to fix this too
so that checkers don't depend on backend/, i.e. on all the other
checkers via Summary.ml. But in order to migrate progressively we can
first migrate absint/ and one step on the way is for it to not know what
kind of analysis data it is passing around.
This extra flexibility only costs us passing an extra `Procdesc.t` in a
couple more functions so it's actually not a bad change in itself.
Reviewed By: ngorogiannis
Differential Revision: D21257466
fbshipit-source-id: a91f7b191
Summary:
This is needed to make absint/ its own dune library. Modules in absint/
cannot depend on modules in backend/. This is because backend/Summary.ml
depends on *all* the (inteprocedural) analyses since its stores elements
of their domains. But analyses are supposed to depend on absint/ to
use the AI framework and others. Thus absint/ cannot depend on backend/
otherwise it creates a dependency cycle.
Right now infer builds with this cycle because we consider all these
directories to be one library and there is no dependency cycle between
the individual modules, but making absint/ a library makes the situation
coarser.
One actual change in there: one function in PatternMatch was specific to
nullsafe and was moved there.
Reviewed By: ngorogiannis
Differential Revision: D21257467
fbshipit-source-id: 42af43315
Daiva Naudziuniene
Ezgi Çiçek
Mitya Lyubarskiy
Sungkeun Cho
Nikos Gorogiannis
Jules Villard
Dulma Churchill
Artem Pianykh