Summary:
The specialization of the methods based on the type of the arguments should only be performed when the type is an object type. This should in theory be always the case according to the Java semantics but the previous version of the code was relying on Infer to be correct all the way down the the method call:
Before this diff, the analysis on examples like this:
String foo(Object object) {
object.toString();
}
String bar() {
int[] array = {1, 2, 3};
foo(array);
}
This is a legit code that Infer is getting wrong because Java objects are translated as C objects instead of objects containing a C-style object. There may be other issues like this so it is safer to filter out the types when performing the substitution.
Reviewed By: jberdine
Differential Revision: D4345760
fbshipit-source-id: 1c74593
Summary:
We currently can only model the return values of functions as sources.
In order to model inputs of endpoints as sources, we need the capability to treat the formals of certain functions as sources too.
This diff adds that capability by adding a function for getting the tainted sources to the source module, then using that info in the analysis.
Reviewed By: jeremydubreil
Differential Revision: D4314738
fbshipit-source-id: dd7d423
Summary: Different analyses need different preanalyses to run. It doesn't make sense for all of the pre-analyses to be bundled together into one package.
Reviewed By: jvillard
Differential Revision: D4348243
fbshipit-source-id: 46a8ebd
Summary:
Adding #infer-capture-all et al. by hand is annoying and I always forget to do
it. Let infer figure that out.
Reviewed By: dulmarod
Differential Revision: D4339799
fbshipit-source-id: 55e52dc
Summary:
Seems like we cannot run 2 instances of Buck in parallel even when one uses
buck-out/ and the other buck-out/foo/.
Reviewed By: sblackshear
Differential Revision: D4347090
fbshipit-source-id: 7e65d2f
Summary: reactive capture spawns clang from within analysis. Time it takes to compile source code shouldn't be counted towards timout
Reviewed By: jvillard, cristianoc
Differential Revision: D4334037
fbshipit-source-id: 64f417d
Summary: Access to std::vector shouldn't be treated as SKIP. Implementation is simple enough to use one from std:: headers
Reviewed By: jvillard
Differential Revision: D4339577
fbshipit-source-id: d1fbbee
Summary: pattern matching we had before allowed many unintended functions to pass (such as `max_element`). Make matching much more strict
Reviewed By: jvillard
Differential Revision: D4313428
fbshipit-source-id: 189c522
Summary:
Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces.
This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary.
One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible.
Under the old summary system, we would do it at most once for each "function" in the summary list.
Now, we'll do it at most once for each node in the access tree summary.
This will be a smaller number of calls, since each node can summarize many input/output relationships.
Reviewed By: jeremydubreil
Differential Revision: D4271579
fbshipit-source-id: 34e407a
Summary:
This commit avoids using the join operator for the widening
of the Map functor in ```abstractDomain.ml```
and ensures termination when ```ValueDomain``` is infinite
by using ```ValueDomain.widen```.
Closes https://github.com/facebook/infer/pull/535
Differential Revision: D4319797
Pulled By: sblackshear
fbshipit-source-id: 16f15e4
Summary: Don't warn on NotThreadSafe class, particularly when super is ThreadSafe
Reviewed By: sblackshear
Differential Revision: D4334417
fbshipit-source-id: 0df3b9d
Summary:
Most of the time code outside of project root is not interesting to the user - it's either system library or infer C++ model. Skip all of them.
Previous logic was doing something similar, but in more selective way.
I also need this change for D4313428
Reviewed By: jvillard
Differential Revision: D4339298
fbshipit-source-id: c7b5544
Summary:
This will simplify the InferPrint logic of checking what should/should-not be reported.
I will remove the issue names in Localise in a next diff.
Reviewed By: ddino
Differential Revision: D4334327
fbshipit-source-id: ebcfd6c
Summary:
This diff parses the build command args to directly handle the -version
option passed to java and javac, to make the integration with buck more
robust by ensuring that the version and no additional debug logging is
generated for `infer --debug -- javac -version`.
Reviewed By: jeremydubreil
Differential Revision: D4158011
fbshipit-source-id: e7d6b4d
Summary:
SuppressWarnings annotations are hardly used and add considerable
complexity due to requiring recompilation with an annotation processor.
Reviewed By: jvillard
Differential Revision: D4312193
fbshipit-source-id: c4fc07e
Summary:
This option is only useful if you want to treat casts angelically, but nothing else.
Since angelic is on by default and this option is off by default, it's basically useless.
Reviewed By: jeremydubreil
Differential Revision: D4334030
fbshipit-source-id: 3c0b0ed
Summary:
Most of the diff adds a way to run an existing test with different infer
options.
Also, do not run the Python script when capturing "analyze".
fixes https://github.com/facebook/infer/issues/518
Reviewed By: jberdine
Differential Revision: D4333762
fbshipit-source-id: 642acff
Summary:
Change the domain of SIOF to be based on sets of pvar * location instead of
single pvars. This allows us to group several accesses together. However, we
still get different trace elems for different instructions in a proc. We do two
things to get around this limitation and get a trace where all accesses within
the same proc are grouped together, instead of one trace for each access:
1. A post-processing phase at the end of the analysis of one proc collects all
the globals directly accessed in the proc into a single trace elem.
2. When creating the error trace, unpack this set into several trace elements
to see each access (at its correct location) separately in the trace.
This is a bit hacky and another way would be to extend the API of traces to
handle in-procedure accesses natively instead of shoe-horning them. However
since SIOF is the only one to use this, it introduces less boilerplate to do it
that way for now.
Also, a few .mlis for good measure.
Reviewed By: sblackshear
Differential Revision: D4299070
fbshipit-source-id: 3bbb5c2
Summary: These direct tests were still mostly relying on PHONY targets.
Reviewed By: jberdine
Differential Revision: D4326469
fbshipit-source-id: 37b2d0a
Summary:
Turns out that swapping stdout and stderr using a temporary fd 3 was screwing
up with make's jobserver, who also uses fd 3!
Also, infer is partly to blame as it also calls `make`. Unsetting `MAKEFLAGS`
in infer tells `make` that the way infer calls `make` is independent from
parent `make` invocations.
Also, simplify the rules for direct tests and build system tests.
Reviewed By: jberdine
Differential Revision: D4328979
fbshipit-source-id: 96818e8
Summary:
The list of argument specs is a global ref inside `CommandLineOptions`, which
need to be reset to the empty list every time `parse` is called. Otherwise, we
get duplicated sections:
```
$ infer --help
Infer version v0.9.4-84d61cb
Copyright 2009 - present Facebook. All Rights Reserved.
Toplevel options
--inferconfig-home <dir> Path to the .inferconfig file
--project-root | -pr <dir> Specify the root directory of the project (default: /home/jul/infer)
Analysis (backend) options
Clang frontend options
Java frontend options
Toplevel options
[... the rest of the options -- without --inferconfig-home or --project-root,
with all the section headers again ...]
```
Reviewed By: jberdine
Differential Revision: D4333448
fbshipit-source-id: f91ea66
Summary:
The javac -classes_out option is used to set the results directory for
the buck build system integration.
Reviewed By: jeremydubreil
Differential Revision: D4162907
fbshipit-source-id: 75d0a6d
Summary:
We don't need to have separate `--` integration for compilation database. Instead use:
infer --compilation-db-files db.json <other_infer_options> // no -- anywhere!
Reviewed By: jberdine
Differential Revision: D4327570
fbshipit-source-id: caf0dc9
Summary:
This change is to support the development of CTL's DSL, where issues can be specified directly from the language, in the form of strings.
Severity is specified locally to the place where the check is defined
Reviewed By: ddino
Differential Revision: D4326594
fbshipit-source-id: 7b146ac
Summary:
If these collections don't encapsulate their state properly, there are bigger problems than thread safety issues :).
Plus, these warnings are less-than-actionable for non-Guava maintainers.
Reviewed By: peterogithub
Differential Revision: D4324277
fbshipit-source-id: cacfbf0
Summary:
Maintain an "ownership" set of access paths that hold locally allocated memory that has not escaped.
This memory is owned by the current procedure, so modifying it outside of synchronization is safe.
If an owned access path does escape to another procedure, we remove it from the ownership set.
Reviewed By: peterogithub
Differential Revision: D4320034
fbshipit-source-id: 64f9169
Summary: Turns out I forgot to close the fd returned by dup(2) so we were leaking a lot.
Reviewed By: jeremydubreil
Differential Revision: D4327389
fbshipit-source-id: 74574ac
Summary: This is required to maintain a set of owned access paths in a subsequent diff.
Reviewed By: jberdine
Differential Revision: D4318859
fbshipit-source-id: bd1a9fa
Summary:
This diff introduces place-holders strings in error messages and evaluates them
when an error needs to be reported.
Place-holders strings are of the form %name_of_helper_function%. They will be evaluated
using and helper function that gives a value.
For example if we need to display the name of a variable in the error message we will have:
".... %var_name%...."
then %var_name% will be evaluated in the ast node calling the appropriate
helper function and the results will replace %var_name% in the message.
Reviewed By: dulmarod
Differential Revision: D4313133
fbshipit-source-id: bf521ca
Summary:
We've had some issues with names like `arr$` appearing in error reports.
Any identifier name that contains $ cannot have come from source code because it is not a legal Java identifier.
This change should stop these reports because Errdesc.ml refuses to use temporary var names in error reports.
Reviewed By: jeremydubreil
Differential Revision: D4322305
fbshipit-source-id: 16237fe
Summary:
These checks were useful when developing Quandary, but do not fire anymore.
`AccessPath.raw_equal` is implicated as one of the top time-consuming functions in Quandary, so gating the assertion that calls it needlessly might save us some time.
Also minor cleanup: made the error messages a bit clearer and added an mli.
Reviewed By: jeremydubreil
Differential Revision: D4323653
fbshipit-source-id: 2a723b5
Summary:
The debug script wants to run InferClang on the file at hand, but that often
involves running a -cc1 command with InferClang, which is no longer supported.
This removes this functionality. The debug script now only dumps the AST to
biniou and its text representation.
Reviewed By: dulmarod
Differential Revision: D4319431
fbshipit-source-id: ef64912
Summary:
C stubs were causing issues with building:
- need OCaml stubs of the C stubs for byte compilation!
- brittle (to remain polite) support in ocamlbuild
Ctypes is awesome, use it instead.
Slight wrinkle on the previous statement:
- ioctl(2) is variable arguments, which is not officially supported by Ctypes but should work in our use-case
- I'm hardcoding the value of a C macro found in system headers
Reviewed By: jberdine
Differential Revision: D4319507
fbshipit-source-id: 352804a
Summary:
<ugly shameful hack>
Temporarily redirect stderr to /dev/null before calling `Javalib.get_class` so
as to avoid getting spammed with "Warning: unexpected attribute: Code" messages
when parsing Java files.
</ugly shameful hack>
I suspect that now that Javalib handles Java 8 this issue is more prevalent. An
issue/PR should be sent to Javalib too so that it's fixed upstream and we can
eventually remove the hack (t15039096).
Reviewed By: jberdine
Differential Revision: D4319466
fbshipit-source-id: af855ba
Summary:
This removes support for developing infer using Eclipse. If you use Eclipse,
consider using Atom/Emacs/vim instead, which have good OCaml/Reason support.
This allows us to get rid of a couple quirks:
- do not generated ocaml annots (this is very slow)
- move OCaml _build directory to infer/src/ where it makes more sense
Reviewed By: jberdine
Differential Revision: D4319480
fbshipit-source-id: 6f063fc
Summary: Allow backend to trigger compilation of extra files when it needs them. This will allow infer to capture less files initally and possibly speed up compilation
Reviewed By: cristianoc, jberdine
Differential Revision: D4231581
fbshipit-source-id: 181abea
Summary:
Before, the Interprocedural functor was a bit inflexible. You couldn't do custom postprocessing like normalizing the post state or coverting the post from an astate type to a summary type.
Now, you can do whatever you want by passing a custom `~compute_post` function.
Since `AbstractInterpreter.compute_post` can be used by clients who don't care to do anything custom, this doesn't create too much boilerplate.
Reviewed By: jvillard
Differential Revision: D4309877
fbshipit-source-id: 8d1d85d
Summary:
In particular, the method for retrieving an element from the array, this should never be nil. Also added a model for count
similar to the one for NSString length.
Reviewed By: ddino
Differential Revision: D4306655
fbshipit-source-id: 0ecb25a
Summary: Our C++ model magic didn't work when instantiating smart pointers with volatile types. Fix it
Reviewed By: jvillard
Differential Revision: D4313271
fbshipit-source-id: 55ffb98
Summary:
This is to prevent clang from changing AST to make it more performant and less readable.
Reported in https://github.com/facebook/infer/issues/522
+ unrelated `refmt` fix
Reviewed By: jvillard
Differential Revision: D4319731
fbshipit-source-id: 176dfcf
Summary: Rename the intermediate .exp.test files to .exp.test.noreplace so that they don't match the regexp used by `make test-replace`. Otherwise they can accidentally become .exp files that will show up in `git status`.
Reviewed By: cristianoc
Differential Revision: D4319436
fbshipit-source-id: df2ef21
Summary: lines end in '\n' so the last item in `lines.split('\n')` is always empty.
Reviewed By: jeremydubreil
Differential Revision: D4299036
fbshipit-source-id: b3cacbf
Summary:
Before the diff, the code was considering as Nullable any annotation ending with `...Nullable`, including `SuppressParameterNotNullable`.
Closes#533
Reviewed By: jberdine
Differential Revision: D4317356
fbshipit-source-id: 6091c0f
Summary: We're about to add another element to the abstract domain, and a 4-tuple is a bit too cumbersome to work with.
Reviewed By: jberdine
Differential Revision: D4315292
fbshipit-source-id: d04699f
Summary:
Substituting modules into Core.Std breaks the linking behavior of
module aliases, and so does including the module type of Core.Std in a
signature. So, for now, this diff exposes the broken functions in
Core's Gc, Signal, and Sys modules.
Reviewed By: cristianoc
Differential Revision: D4313140
fbshipit-source-id: d8fea00
Summary:
In checkers we use "let" clause to define formulas abbreviation.
This diff expands the use of such formula id when used.
This allows to evaluate the formula.
For example.
let f = f_def
let g = g_def
let h = f or g
will expand the use of f and g with their definition.
Reviewed By: martinoluca
Differential Revision: D4299542
fbshipit-source-id: 9d37dd0
Summary:
This diff adds basic support for parsing the arguments passed to the
build command directly from Config.
Reviewed By: dulmarod
Differential Revision: D4201480
fbshipit-source-id: bba6056
Summary:
Several Core functions silently wrap argument functions with catch-all
exception handlers that exit. This diff protects against these from
ever being used by deprecating them, which causes compilation failure if
they are used.
Reviewed By: jvillard
Differential Revision: D4271781
fbshipit-source-id: a096171
Summary:
Use In_channel and Out_channel operations instead of those in Pervasives. Don't
use physical equality on values that aren't heap-allocated since it doesn't help
the compiler generate faster code and the semantics is unspecified. Also use
phys_equal for physical equality.
Reviewed By: sblackshear
Differential Revision: D4232459
fbshipit-source-id: 36fcfa8
Summary:
Utils contains definitions intended to be in the global namespace for
all of the infer code-base, as well as pretty-printing functions, and
assorted utility functions mostly for dealing with files and processes.
This diff changes the module opened into the global namespace to
IStd (Std conflict with extlib), and moves the pretty-printing
definitions from Utils to Pp.
Reviewed By: jvillard
Differential Revision: D4232457
fbshipit-source-id: 1e070e0
Summary: Adding Buck `DEFS` macros for generating Infer genrules. The generated genrules can be used to run the analysis on any existing `java_library` targets.
Reviewed By: sblackshear
Differential Revision: D4291234
fbshipit-source-id: 6430e2e
Summary: Using multicore introduces some flakiness when building the models. This leads to summries for the models that are not always the same after rebuidling from scratch.
Reviewed By: jberdine
Differential Revision: D4306468
fbshipit-source-id: 96933d6
Summary:
Make sl_file field strongly typed in the AST - store SourceFile.t instead of string. This will make it harder
to access raw string which shouldn't really be accessed before going through `SourceFile` module
Reviewed By: jvillard
Differential Revision: D4299468
fbshipit-source-id: e8ff87e
Summary:
The Java frontend translates exceptions by assigning them to the return value.
This leads to weird behavior when the return type of the function is void.
Already handled one case of this in Quandary (ignoring assignments of exceptions to return value), but was missing the case where null is assigned to the return value.
The frontend does this to "clear" the value of previously assigned exceptions.
Reviewed By: jeremydubreil
Differential Revision: D4294060
fbshipit-source-id: 6bef5ef
Summary:
We previously used `Procname.java_get_parameters` to compute the indices of parameters to taint, but this doesn't always work.
`java_get_parameters` omits the `this` param, which we may sometimes want to taint.
Use the actuals (already passed to `Sink.get`) instead
Reviewed By: jvillard
Differential Revision: D4285164
fbshipit-source-id: d462a0b
Summary: Globals that are constexpr-initializable do not participate in SIOF.
Reviewed By: sblackshear
Differential Revision: D4277216
fbshipit-source-id: fd601c8
Summary:
Functions related to source files were already namespaced by `source_file_` prefix. Make separate module for them.
In high level it replaces all `source_file_` with `SourceFile.` and then fixes all remaining compilation errors
Reviewed By: jvillard
Differential Revision: D4299053
fbshipit-source-id: 20b1d39
Summary: This is very useful to debug issues that have to do with types, for example the cast errors
Reviewed By: sblackshear
Differential Revision: D4289790
fbshipit-source-id: ef5a8bf
Summary: Enabling `--cxx` flag makes C++ analysis much better. It's time to turn it on by default
Reviewed By: dulmarod, jvillard
Differential Revision: D4285327
fbshipit-source-id: 261359a
Summary:
This is legacy code that dates back from when we needed the fields in the models to match exactly the fields in the classes being modeled. We no longer need to this. Besides, it seems that this `android.jar` stopped being part of the release for a while. So this change will not affect the results in prod
I check in details the difference on the code of Guava and it seems to remove (weird) false positives only.
Reviewed By: sblackshear
Differential Revision: D4242444
fbshipit-source-id: 84dd782
Summary:
Although the Builder pattern is not actually thread-safe, Builder's are not expected to be shared between threads.
Handle this by ignoring all unprotected accesses in classes the end with "Builder".
We might be able to soften this heuristic in the future by ensuring rather than assuming that Builder are not shared between methods (or, ideally, between threads).
Reviewed By: peterogithub
Differential Revision: D4280761
fbshipit-source-id: a4e6738
Summary:
Now that the terminal output is truncated to max 10 issues, it's useful to have
some place where all bugs with source excerpts can be found. Since bugs.txt is
already unstructured (to the extend that it's just text), hopefully no one was
relying on it having a particular format so it's safe to change it to add
source excerpts.
Anyone wanting the old behaviour should consider parsing report.json instead,
which is intended to be more stable.
Closes https://github.com/facebook/infer/issues/520
Reviewed By: akotulski
Differential Revision: D4284175
fbshipit-source-id: 764f291
Summary:
When calling function g_realloc(gpointer mem,gsize n_bytes) one of the spec considers the case
whereby n_bytes is zero. In that case g_realloc would return null.
If we call with sizeof(int), infer would compare sizeof(int) with zero. But the prover would fail to
understand that sizeof(int) != 0.
This diff fix this. We try to convert expression to constant when they can be converted (eg in case of sizeof).
The method currently make a partial set of conversion. This could be extended.
Reviewed By: jberdine
Differential Revision: D4166944
fbshipit-source-id: 3ec4fd7
Summary:
Remember which globals are static locals.
It's useful to distinguish those from global variables in objc and in the SIOF
checker. Previously in ObjC we would accomplish that by looking at the name of
the variable, but that wouldn't work reliably in C++. Keep the old method around for
now as the way we deal with static locals in ObjC needs some fixing.
Reviewed By: akotulski
Differential Revision: D4198993
fbshipit-source-id: 357dd11
Summary:
Whenever header file is in changed-files-index, it should be captured and analyzed on demand.
It was already being captured, but ondemand analysis wasn't triggered for code in header file. This diff does it.
Use hacky header->source mapping to go from header to source (cluster) and then analyze everything in that cluster (inlucing code coming from header)
Reviewed By: jberdine
Differential Revision: D4265495
fbshipit-source-id: 61606f4
Summary: When infer runs on preprocessed source, original files may not be around anymore. Don't crash infer when that happens.
Reviewed By: jvillard, jberdine
Differential Revision: D4258285
fbshipit-source-id: a19569c
Summary: This should no work even when Infer is not setup in the PATH
Reviewed By: jvillard
Differential Revision: D4262356
fbshipit-source-id: e3fa779
Summary: `ReentrantReadWriteLock.ReadLock` and `ReentrantReadWriteLock.WriteLock` are commonly used lock types that were not previously modeled.
Reviewed By: peterogithub
Differential Revision: D4262032
fbshipit-source-id: 4ff81a7
Summary:
`o.<init>` cannot be called in parallel with other methods of `o` from outside, so it's less likely to have thread safety violations in `o.<init>`.
This diff suppresses reporting of thread safety violations for fields touched (transitively) by a constructor.
We can do better than this in the future (t14842325).
Reviewed By: peterogithub
Differential Revision: D4259719
fbshipit-source-id: 20db71f
Summary:
Trying to stop other users of the trace domain from making the mistake that Quandary made before D4234766.
This should also improve the performance of Quandary, since the filtering of FP's is now done before building up the full interprocedural trace (which requires disk reads).
Reviewed By: jeremydubreil
Differential Revision: D4234770
fbshipit-source-id: e7e9291
Summary:
source_file_[to|from]_string were dangerous. While removing source_file_to_string is hard/impossible, source file should never be created from string.
Also include many random changes related to `source_file`:
- improve comments in DB.mli
- define behavior of changed-files-index and improve its description
- move some of the "dangerous" code inline to discourage its reuse
This mostly concludes cleanup of DB.source_file, the last bit is to unify filtering by filename (we have duplicated logic in `InferConfig`, `CLocation` and `JMain`)
Reviewed By: jvillard
Differential Revision: D4258795
fbshipit-source-id: 36735a8
Summary:
`DB.source_file_to_string` is very easy to misuse and it shouldn't even exist.
In preparation for that day, replace most of `source_file_to_string` with `source_file_pp`
Reviewed By: jvillard
Differential Revision: D4258390
fbshipit-source-id: 447cf5a
Summary: Originially, there was a missing package declaration meaning that the generated class was ending in a different place. I also added a test for equality of Integer to complement the test of no equality, which could be always true.
Reviewed By: sblackshear
Differential Revision: D4263676
fbshipit-source-id: 86ab0d3
Summary:
We only ought to report a source-sink flow at the call site where the sink is introduced.
Otherwise, we will report silly false positives.
Reviewed By: jeremydubreil
Differential Revision: D4234766
fbshipit-source-id: 118051f
Summary: This should make it easier to understand complex error reports.
Reviewed By: peterogithub
Differential Revision: D4254341
fbshipit-source-id: fb32d73
Summary: We'll eventually want fancy interprocedural traces. This diff adds the required boilerplate for this and adds the line number of each access to the error message. Real traces will come in a follow-up
Reviewed By: peterogithub
Differential Revision: D4251985
fbshipit-source-id: c9d9823
Summary: we no longer use buck for tests and the script has no reason to exist
Reviewed By: dulmarod
Differential Revision: D4212713
fbshipit-source-id: 7bd1cca
Summary: Noticed this when I was writing the documentation for the abstract interpretation framework and was curious about why `Ondemand.analyze_proc` needs the type environment. It turns out that the type environment is only used to transform/normalize Infer bi-abduction specs before storing them to disk, but this can be done elsewhere. Doing this normalization elsewhere simplifies the on-demand API, which is a win for all of its clients.
Reviewed By: cristianoc
Differential Revision: D4241279
fbshipit-source-id: 957b243
Summary: Adding this so we can test interprocedural trace-based reporting in a subsequent diff.
Reviewed By: peterogithub
Differential Revision: D4243046
fbshipit-source-id: 7d07f20
Summary: We're at risk for some silly false positives without these models.
Reviewed By: peterogithub
Differential Revision: D4244795
fbshipit-source-id: b0367e6
Jeremy Dubreil
Sam Blackshear
Jules Villard
Josh Berdine
Andrzej Kotulski
Peter O'Hearn
Kihong Heo
Dulma Churchill
Martino Luca
Cristiano Calcagno
Dino Distefano