Summary: The docs for this said that it stores the summary to disk, which is no longer true. `compute_summary` is more descriptive of what it actually does now.
Reviewed By: jberdine
Differential Revision: D5245416
fbshipit-source-id: f5138cd
Summary: We had a model for `Pools.SimplePool`, but were missing models for `Pools.Pool`. Since `SimplePool` and `SynchronizedPool` both extend `Pool`, modeling it should cover all of the cases.
Reviewed By: ngorogiannis
Differential Revision: D5236280
fbshipit-source-id: 9bbdb25
Summary:
When dealing with differential's comparisons, SourceFiles in reports may not exist anymore because of changes between revisions.
Disable user visible warnings if desired, through the labeled argument `~warn_on_error`
Reviewed By: jvillard
Differential Revision: D5217097
fbshipit-source-id: 7a1542b
Summary:
The ThreadSafety analysis currently reports on methods only if some
class in the file defining the method is annotated ThreadSafe, or
if it is called by some other such method call. Conflating files and
classes is a bit of a Javaism that seems to be unnecessary.
Reviewed By: sblackshear
Differential Revision: D5182319
fbshipit-source-id: aa77754
Summary: This will make merlin aware of the sources in src/unit/, which are compiled when running tests
Reviewed By: jvillard
Differential Revision: D5217193
fbshipit-source-id: 18bf01a
Summary: This makes it possible to see which tainted parameter can flow to a sink, which is quite useful.
Reviewed By: jeremydubreil
Differential Revision: D5213297
fbshipit-source-id: 1371b5a
Summary:
:
No longer use deprecated reporting function for the suggest nullable checker
Depends on D5205009
Reviewed By: grievejia
Differential Revision: D5205843
fbshipit-source-id: f6dd059
Summary:
Now that we can run several inter-procedural analyses at the same time, we should no longer use the function `Reporting.log_error_deprecated` as it logs the errors in the specs table. This specs table is normally used for caching and will be deprecated in favor of having a cache summaries for the callees in the `Ondemand` module (to avoid deserialising a callee more than once within the same process).
This revision just renames the reporting functions.
Reviewed By: sblackshear
Differential Revision: D5205009
fbshipit-source-id: b066549
Summary:
Read/write race errors should always show one trace for a read and one trace for a write.
We forget to pass the conflicting writes to the reporting function in one case, which prevented us from showing a well-formed trace.
Fixed it by making the `conflicts` parameter non-optional
Reviewed By: jberdine
Differential Revision: D5209332
fbshipit-source-id: 05da01a
Summary: Can be useful in case there is compilation issue with the models
Reviewed By: jvillard
Differential Revision: D5208830
fbshipit-source-id: f31d84f
Summary:
This messes up with the Buck cache: if infer recaptures a file with only trivial changes that shouldn't affect the capture Buck will still believe it has to reanalyze everything that depends on that file if there's non-deterministic data in infer's output.
Re-use the `--buck` flag used by the Java Buck integration for mostly the same purposes. Add a few special cases for the flavours integration (eg: keep capture data).
Change perf stats registration to take `Config.buck_cache_mode` into account instead of relying on each call site to handle that peculiarity correctly. Also, there's no need to create the perf stats directories before calling the registration function since it will do that too.
Reviewed By: jeremydubreil
Differential Revision: D5192311
fbshipit-source-id: 334ea6e
Summary:
It is not used, so one fewer thing to track inside Python.
Note that Python does pass `--buck` to OCaml infer to make it aware that it is
running from within Buck, and the OCaml code uses that flag to trim infer-out
to only what's strictly necessary (and especially to remove non-deterministic
output that would mess with Buck's cache).
Reviewed By: jberdine
Differential Revision: D5200043
fbshipit-source-id: 1c84442
Summary:
Mutating a formatter in `dup_formatter` had unintended consequences of
double-printing newlines. There's actually no need not to make a fresh copy,
which avoids this problem.
Also, don't warn if the log file is still a buffer at the end of execution as
that can happen in some error cases, eg:
```
$ infer -- build
ERROR: (Invalid_argument "Unsupported build command build")
```
Reviewed By: jberdine
Differential Revision: D5199664
fbshipit-source-id: fc2731d
Summary:
We were saving them in infer-out/clang/ but that's bad for Buck's cache as
these files have randomly-generated names.
Reviewed By: dulmarod
Differential Revision: D5191884
fbshipit-source-id: b3a478b
Summary: These can be useful in other checkers that have a notion of footprint.
Reviewed By: jvillard
Differential Revision: D5189193
fbshipit-source-id: c5bd91b
Summary: Also makes the error message for clang commands a bit nicer to the eye.
Reviewed By: mbouaziz
Differential Revision: D5191664
fbshipit-source-id: 801ec72
Summary:
It's easier to distinguish what's checked into infer and what comes from the
plugin this way.
Reviewed By: akotulski
Differential Revision: D5191581
fbshipit-source-id: 579311e
Summary:
This should help prevent new modules being created that do not `open! IStd`.
Documented this in CONTRIBUTING.md.
Reviewed By: jberdine
Differential Revision: D5183552
fbshipit-source-id: 0f0a8ce
Summary:
First step toward addressing bad traces that happen in examples like
```
void sourceMethod() {
Obj source = (Obj) InferTaint.inferSecretSource();
callSameSink(null, source); // index: 1
}
void callSameSink(Obj o1, Obj o2) {
callMySink1(o1); // flows via o1 ~= index 0, don't expand
callMySink2(o2); // flows via o2 ~= index 1, can expand
}
void callMySink1(Obj o) {
... // maybe interesting something happens here that doesn't happen in callMySink2
InferTaint.inferSensitiveSink(o); // flows via o ~= index 0, can expand
}
void callMySink2(Obj o) {
InferTaint.inferSensitiveSink(o); // flows via o ~= index 0, can expand
}
```
The issue is that when we recreate a trace to the sink starting from `sourceMethod`, we don't know which of the calls to `callMySink` to expand/include in the trace.
If we expand the call to `callMySink(o1)`, we'll get a bogus trace.
In this example that's not such a big deal, but imagine the case where the first call to `callMySink` is a different function that transitively calls the sink through some long and confusing path.
Remembering the index at which taint flows into each sink will let us choose which sinks are safe to expand.
This diff just adds indexes to the API; it's not actually propagating the index info or using it during expansion yet.
Reviewed By: jeremydubreil
Differential Revision: D5170563
fbshipit-source-id: ba4b096
Summary:
Change the API of `Logging` wrt to writing to files and to the console (see
changes in logging.mli).
Write only to one log file: infer-out/log. Prefix each line with the kind of
warning and the PID of the process emitting it. Writing with `O_APPEND` is
atomic so the file should not get garbled by concurrent writes. To get the
output of a single process, find out which one interests you by looking at
infer-out/log, then `grep ^[<PID>] infer-out/log`.
Introduce 3 log levels for debug output and command-line options to set them
for various categories individually.
Change tons of `"\n"` to `"@\n"` so the `Format` module is aware of newlines
without us having to look through every character of every logged string for
`\n` characters.
Reviewed By: mbouaziz
Differential Revision: D5165317
fbshipit-source-id: 93c922f
Summary:
This makes it clearer that something went wrong. Most `failwith` did not set
this prefix already, so I opted to append it automatically and remove it from
the few instances that added it manually.
Also add quotes around bad user arguments to lessen possible confusion.
Reviewed By: jberdine
Differential Revision: D5182272
fbshipit-source-id: 20e4769
Summary:
Introduce a new option `--no-report` (conversely `--report`) to stop reporting
after the analysis. This is useful to call sub-`infer-analyze` processes with
as they shouldn't compute "result.json" or report bugs to stderr. This bug
would only manifest itself when per-procedure parallelism disabled, which
explains why it was noticed only on Java.
Reviewed By: jberdine
Differential Revision: D5182110
fbshipit-source-id: a892470
Summary:
This is a refactoring diff to put the info into the abstract domain
to track when we have done steps which would invalidate "I think I have a proof".
Subsequent diffs will start manipulating ThumbsUpDomain
Reviewed By: sblackshear
Differential Revision: D5172181
fbshipit-source-id: 51ceba6
Summary:
The logic is not that simple and this will be needed in a later diff to create
the log file as early as possible.
Reviewed By: jberdine
Differential Revision: D5173128
fbshipit-source-id: 830f105
Summary: This also allows us to better test that the new commands will keep working.
Reviewed By: jeremydubreil
Differential Revision: D5172891
fbshipit-source-id: 169bd6f
Summary:
Spacetime profiling showed that this was allocating a lot more than it needs
to. Switching to a `Hashtbl` makes the memory overhead go away, and halves the
memory consumption of the whole frontend on some pathological files.
This also brings the file "clang_ast_main.ml" into the infer repo, renamed to
"ClangPointers.ml" (and given an mli). It's useful to have something like
"clang_ast_main.ml" checked into the facebook-clang-plugins repo to illustrate
how to use the OCaml AST visitor generated by atdgen, but it can be simplified
to be more pedagogical instead of being the visitor used in infer.
Reviewed By: jberdine
Differential Revision: D4884383
fbshipit-source-id: 88f324a
Summary: We were almost always using `~report_reachable:true`, and in the cases where we weren't it is fine to do so. In general, a sink could read any state from its parameters, so it makes sense to complain if anything reachable from them is tainted.
Reviewed By: mbouaziz
Differential Revision: D5169067
fbshipit-source-id: ea7d659
Summary:
This was a subtle one. The ranking function of `aux` is the cardinality of `m`..
But if `may_alias` is not reflexive, then `k_part` will be empty, `non_k_part` will be the same size, and we'll diverge.
Sneakily, `may_alias` is actually *not* reflexive because `is_subtype t1 t2` doesn't check for the equality of `t1` and `t2`.
That is confusing and should be fixed separately.
For now, just make sure `may_alias` is always reflexive and add an assertion that `k_part` is never empty.
Reviewed By: jeremydubreil
Differential Revision: D5177427
fbshipit-source-id: 0549d6a
Summary: Have found this useful in Quandary for fbcode, where we want to do this for folly due to its use of assembly (details in comments).
Reviewed By: mbouaziz
Differential Revision: D5167564
fbshipit-source-id: bf6d7e0
Summary:
Now `infer analyze` really has the same behaviour as `infer -- analyze`.
Previously it wouldn't create report.json or report.
Reviewed By: jeremydubreil
Differential Revision: D5172875
fbshipit-source-id: 8f9ddd1
Summary: Needed higher-up the stack, useful to have in the API in general.
Reviewed By: jberdine
Differential Revision: D5165153
fbshipit-source-id: 714aeea
Summary:
This will be needed higher up in the stack because the new `ProcessPool` module
will need to call into `Logging` to refresh the logging formatters to get the
right PID when writing to the log file.
+remove dead code `iter_parallel`
Reviewed By: jberdine
Differential Revision: D5165130
fbshipit-source-id: 95c949b
Summary:
I should not push debugging code to the repo
I should not push debugging code to the repo
I should not push debugging code to the repo
I should not push debugging code to the repo
I should not push debugging code to the repo
I should not push debugging code to the repo
...
Reviewed By: martinoluca
Differential Revision: D5164723
fbshipit-source-id: d944916
Summary:
For now, we just support clearing the taint on a return value.
Ideally, we would associate a kind with the sanitizer and only clear taint that matches that kind.
However, it's fairly complicated to make that work properly with footprint sources.
I have some ideas about how to do it with passthroughs instead, but let's just do the simple thing for now.
Reviewed By: jeremydubreil
Differential Revision: D5141906
fbshipit-source-id: a5b8b5e
Summary: Allow type variables in `Typ.desc`. It will be used to store template type arguments.
Reviewed By: jberdine
Differential Revision: D5154757
fbshipit-source-id: 55b8e81
Summary:
- model `exit` as `Bottom`
- model `fgetc` as returning `[-1; 255]` rather than `[-1; +oo]`
- reduced the number of model functions for simple models
Reviewed By: KihongHeo
Differential Revision: D5137485
fbshipit-source-id: 943eeeb
Summary:
1. `noexcept` was missing from `unique_ptr` constructors leading to compilation errors in some edge cases
2. In case `unique_ptr` specified custom deleter with custom `deleter::pointer`, there could be compilation errors due to invalid cast from `deleter::pointer` to `void*`. Add extra overload of `model_set` to prevent this issue
Reviewed By: jberdine
Differential Revision: D5147071
fbshipit-source-id: 2586701
Summary:
This is a minimal change to (poorly) recognize and model std::mutex
lock and unlock methods, and to surface all thread safety issues for
C++ based on the computed summaries with no filtering.
This ignores much of the Java analysis, including everything about the
Threads domain. The S/N is comically low at this point.
Reviewed By: sblackshear
Differential Revision: D5120485
fbshipit-source-id: 0f08caa
Summary:
ThreadSafety.may_alias crashed on C++ code because it assumed Java
field names.
Reviewed By: sblackshear
Differential Revision: D5147284
fbshipit-source-id: d10841f
Summary: The previous error message recommended annotating the method in question with `GuardedBy`, which doesn't actually work.
Reviewed By: jeremydubreil
Differential Revision: D5149661
fbshipit-source-id: d935aec
Summary:
This diff fixes unintentional bottoms in pointer arithmetic of inferbo.
The pointer arithmetic on addresses of variables (not array) just returns
the operand.
Reviewed By: jvillard
Differential Revision: D5060424
fbshipit-source-id: 495d8b8
Summary: Using Conjunction for thread join has known false negatives. Finer grained recording of threading information fixes this.
Reviewed By: sblackshear
Differential Revision: D5111161
fbshipit-source-id: aab483c
Summary:
All files that match the regular-expressions passed via `--skip-analysis-in-path` are just compiled.
With this change, you can also opt for not compiling those files at all, by passing the `--skip-analysis-in-path-skips-compilation` argument
Reviewed By: mbouaziz
Differential Revision: D5121583
fbshipit-source-id: 4e1325a
Summary:
A recent diff tried to replace `L.out "error message"; assert false` with
`failwith "error message"` but infer relies on the type of raised exceptions to
sometimes keep going. A more careful change will be needed but in the meantime
restore the old behaviour.
Reviewed By: jberdine
Differential Revision: D5112969
fbshipit-source-id: 713fe20
Summary:
Recently we changed the binaries we build and use but it wasn't obvious that
some of the old binaries disappeared. For instance, nothing short of `git clean
-xfd` would get rid of "infer/bin/InferPrint", which can lead to frustrating
attempts to make InferPrint not segfault.
Mitigate this in two ways:
- be more strict in the binaries we ignore in .gitignore, so InferPrint would should up in "git status"
- be less strict in the binaries we clean out with `make clean` so that
InferPrint et al. gets deleted by `make clean`
Reviewed By: jberdine
Differential Revision: D5120573
fbshipit-source-id: 44e7954
Summary: There were some leftover uses of the `Tracing` analyzer option. While I was at it, I also rename the `Config` option name.
Reviewed By: jberdine
Differential Revision: D5113489
fbshipit-source-id: 68d5cc8
Summary: The debug HTML for Quandary/thread-safety was still printing the SIL instructions, which is not very helpful. Print the HIL instructions instead.
Reviewed By: jeremydubreil
Differential Revision: D5112696
fbshipit-source-id: a0aa925
Summary:
Try and enforce the following rules:
- stderr is for updating the user about progress or errors
- Introduce Logging.progress that outputs to stderr, but honours --quiet
- Logging.stderr is as before
- Logging.out now prints to stderr (or to log files as before if set up) and
not stdout. If some information should go on stdout then the user should be
able to rely on it (ie, it's not just some progress message). For now only
the summary of the errors is printed on stdout by default.
- Logging.err* functions are gone. If the error is user-visible, it should be
Logging.stderr, or `failwith`. If not, go to the same log file as other
output, which personally I find much more convenient than having to dig through
2 log files every time I'm looking for some output.
Reviewed By: jberdine
Differential Revision: D5095720
fbshipit-source-id: 68999c9
Summary: This fixes a couple of false positives as objects of BufferedReader don't need to be closed if the wrapped reader resource gets closed correctly.
Reviewed By: sblackshear
Differential Revision: D5106596
fbshipit-source-id: 725fb80
Summary:
`infer analyze ...` (and `InferAnalyze` before it) was not actually running the
analysis in parallel, unlike `infer -- analyze`, which we want to deprecate.
Reviewed By: jberdine
Differential Revision: D5095676
fbshipit-source-id: ec28465
Summary: Gflags is a popular library used to create command line arguments. Flags shouldn't flow directly to `exec` etc.
Reviewed By: jvillard, mbouaziz
Differential Revision: D5058393
fbshipit-source-id: ab062f8
Summary: Useful to have Eradicate and Biabduction agree on how to inform that the analysis that some objects are not null.
Reviewed By: sblackshear
Differential Revision: D5075127
fbshipit-source-id: 9e56981
Summary: The Buck cache was not correctly invalidated when switching between the different analysis mode. This was causing the analysis results to be mixed up. This revision should fix this.
Reviewed By: sblackshear
Differential Revision: D5073606
fbshipit-source-id: eb14418
Summary: String are very important for taint analysis, have to make sure that we have the right models/the right behaviors for unknown code.
Reviewed By: jvillard
Differential Revision: D5054832
fbshipit-source-id: 7e7ee07
Summary:
Interestingly, this crashes the build in a vagrant vm:
```
[*ERROR**][2799] findlib: [WARNING] Interface ctl_parser_types.cmi occurs in several directories: ., clang
[*ERROR**][2799] File "clang/ComponentKit.ml", line 1:
[*ERROR**][2799] Error: The files ctl_parser_types.cmi and clang/cFrontend_checkers.cmi
[*ERROR**][2799] make inconsistent assumptions over interface Ctl_parser_types
[*ERROR**][2799] Command exited with code 2.
```
Reviewed By: mbouaziz
Differential Revision: D5070024
fbshipit-source-id: 01f83fc
Summary:
After:
```
$ infer run -- clang -c examples/hello.c
Capturing in make/cc mode...
Found 1 source file to analyze in /home/jul/infer/infer-out
Starting analysis...
legend:
"F" analyzing a file
"." analyzing a procedure
F.
Found 1 issue
examples/hello.c:14: error: NULL_DEREFERENCE
pointer `s` last assigned on line 13 could be null and is dereferenced at line 14, column 3
12. void test() {
13. int* s = NULL;
14. > *s = 42;
15. }
Summary of the reports
NULL_DEREFERENCE: 1
```
Before, legend and analysis run were separated by 2 lines, one is now before
and the other is in the log files only:
```
Capturing in make/cc mode...
Starting analysis...
legend:
"F" analyzing a file
"." analyzing a procedure
Found 1 (out of 1) source files to be analyzed in /home/jul/infer/infer-out
per-procedure parallelism jobs:4
F.
Found 1 issue
examples/hello.c:14: error: NULL_DEREFERENCE
pointer `s` last assigned on line 13 could be null and is dereferenced at line 14, column 3
12. void test() {
13. int* s = NULL;
14. > *s = 42;
15. }
Summary of the reports
NULL_DEREFERENCE: 1
```
Reviewed By: mbouaziz
Differential Revision: D5069590
fbshipit-source-id: 8843422
Summary:
Previously all knowledge of the dynamic length of such arrays was lost to infer:
```
void foo(int len) {
int a[len];
}
```
The translation of this program would make no reference to `len` (except as a
param of `foo`).
Translate this "initialization" using the existing `__set_array_length` infer
builtin, as:
```
# Declare local a[_]
n$0 = len;
__set_array_length(a, len);
```
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4969446
fbshipit-source-id: dff860f
Summary: There was no option to trigger this checker so it was not possible to enable it when not running the default list of checkers
Reviewed By: jberdine
Differential Revision: D5057088
fbshipit-source-id: 7af36f5
Summary:
This commit fixes a problem that the buffer overrun checker incorrectly
stops when a global variable (bottom) is involved in control flow.
In the new version, abstract memories return Top for unanalyzed abstract
variables.
Reviewed By: mbouaziz
Differential Revision: D5016447
fbshipit-source-id: 5132448
Summary: The issues that are not reported by default are all experimental issues from the biabduction analysis. In that case, it is easier to use a blacklist of errors to filter out so that the issues found by the checkers based on the AI framework can be reported by default without having to add them to the whitelist.
Reviewed By: jvillard
Differential Revision: D5051327
fbshipit-source-id: 2a93b11
Summary:
The code was pretty fragile, it's less fragile now. We should probably just
delete that and start outputting proper class/package info directly in the
report.json instead of reverse-engineering them.
Fixes#640
Reviewed By: jeremydubreil
Differential Revision: D4905973
fbshipit-source-id: 1590067
Summary:
An array has a static or dynamic length (number of elements), but it also has a
stride, determined by the type of the element: `sizeof(element_type)`. We don't
have a good `sizeof()` function available on SIL types, so record that stride
in the array type.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4969697
fbshipit-source-id: 98e0670
Summary: In particular, the heuristics for propagating taint via unknown code needs to be aware of the frontend's trick of introducing dummy return variables.
Reviewed By: mbouaziz
Differential Revision: D5046345
fbshipit-source-id: da87665
Summary:
HIL had only been tested in Java, and it made some assumptions about what array expressions look like (the LHS is always resolvable to an access path) and assignments (the LHS is always an access path) that aren't true in C.
Fixed the code so we won't crash in this case.
Thanks to jeremydubreil for catching this.
Reviewed By: jeremydubreil
Differential Revision: D5047649
fbshipit-source-id: e8484f4
Sam Blackshear
Dulma Churchill
Andrzej Kotulski
Kihong Heo
Daiva Naudziuniene
Jia Chen
Martino Luca
Jules Villard
Kyriakos Nikolaos Gkorogiannis
Josh Berdine
Don Stewart
Jeremy Dubreil
Dino Distefano
Peter O'Hearn
Mehdi Bouaziz