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
Sam Blackshear
Martino Luca
Jules Villard
Kyriakos Nikolaos Gkorogiannis
Josh Berdine
Don Stewart
Jeremy Dubreil
Jia Chen
Andrzej Kotulski
Dulma Churchill
Daiva Naudziuniene
Dino Distefano
Peter O'Hearn
Mehdi Bouaziz
Kihong Heo