Summary:
Polymorphic models, and type environment refinements, need mutual
references between general types and struct types.
Reviewed By: cristianoc
Differential Revision: D4620076
fbshipit-source-id: f9d01e6
Summary:
1. That information isn't used anywhere so far
2. It will simplify my future workr
3. It can be put back later when we realize we need it
Reviewed By: jvillard
Differential Revision: D4620475
fbshipit-source-id: 2c21ac1
Summary: Rather than having three separate annotations related to checking/assuming thread-safety, let's just have one annotation instead.
Reviewed By: peterogithub
Differential Revision: D4605258
fbshipit-source-id: 17c935b
Summary:
Required in a follow-up into interpret ThreadSafe(enableChecks = false).
Just translating the bool as a string for simplicity, since we already support string parameters.
Reviewed By: jeremydubreil
Differential Revision: D4605222
fbshipit-source-id: 8608bdd
Summary: The summary was stored to disk at the end of the on-demand analysis, unless an exception was raised in which case it was only updated in the in-memory cache.
Reviewed By: sblackshear
Differential Revision: D4612369
fbshipit-source-id: 1c8d75b
Summary:
Given #524 was required to do the last manual update, perhaps the Dockerfile could be updated as part of the release process instead of catching it after the fact?
Cheers!
Closes https://github.com/facebook/infer/pull/585
Reviewed By: akotulski
Differential Revision: D4620311
Pulled By: jvillard
fbshipit-source-id: fa74d95
Summary:
Fixes this error in the Docker image build (mentioned in https://github.com/facebook/infer/issues/570#issuecomment-282191663):
```
#=== ERROR while installing ctypes.0.11.3 =====================================#
# opam-version 1.2.2
# os linux
# command make XEN=disable ctypes-foreign
# path /root/.opam/infer-4.02.3/build/ctypes.0.11.3
# compiler 4.02.3
# exit-code 2
# env-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.env
# stdout-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.out
# stderr-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.err
### stdout ###
# [...]
# The following required C libraries are missing: libffi.
# Please install them and retry. If they are installed in a non-standard location
# or need special flags, set the environment variables <LIB>_CFLAGS and <LIB>_LIBS
# accordingly and retry.
#
# For e
Closes https://github.com/facebook/infer/pull/587
Reviewed By: mbouaziz
Differential Revision: D4605385
Pulled By: jvillard
fbshipit-source-id: 689cd4e
Summary:
Fixes this error in the Docker image build (mentioned in https://github.com/facebook/infer/issues/570#issuecomment-282191663):
```
#=== ERROR while installing ctypes.0.11.3 =====================================#
# opam-version 1.2.2
# os linux
# command make XEN=disable ctypes-foreign
# path /root/.opam/infer-4.02.3/build/ctypes.0.11.3
# compiler 4.02.3
# exit-code 2
# env-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.env
# stdout-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.out
# stderr-file /root/.opam/infer-4.02.3/build/ctypes.0.11.3/ctypes-5557-6ff7fe.err
### stdout ###
# [...]
# The following required C libraries are missing: libffi.
# Please install them and retry. If they are installed in a non-standard location
# or need special flags, set the environment variables <LIB>_CFLAGS and <LIB>_LIBS
# accordingly and retry.
#
# For e
Closes https://github.com/facebook/infer/pull/587
Differential Revision: D4620091
Pulled By: jvillard
fbshipit-source-id: 14c95f4
Summary:
Running Buck can be very expensive depending on your installation of Buck (eg,
no watchman). Hardcoded paths seem good enough for now as `make test` will
catch if they go out of date.
Reviewed By: jeremydubreil
Differential Revision: D4597629
fbshipit-source-id: da9b704
Summary:
As noticed by technion in https://github.com/facebook/infer/issues/570,
failures in the Docker test do not result in failures of the test. Lol.
Reviewed By: mbouaziz
Differential Revision: D4605364
fbshipit-source-id: de9f84c
Summary: distinguish writes via method calls (e.g., add) from writes via assignment in the error messages
Reviewed By: sblackshear
Differential Revision: D4611748
fbshipit-source-id: 7594d3b
Summary: It seems that we need to store the summary to disk in `Summary.write_summary`. The previous code was just saving it to the in-memory cache of summaries.
Reviewed By: sblackshear
Differential Revision: D4611090
fbshipit-source-id: 9973679
Summary: The function `Checkers.ST.store_summary` was only used in one place. This revision moves the functionality to the only place where this function was used, except the part swallowing `Sys_error` which may have the bad side-effect of making issues like race-conditions silent.
Reviewed By: cristianoc
Differential Revision: D4608790
fbshipit-source-id: b84c8ce
Summary: This check is redundant and already happens in `Ondemand`.
Reviewed By: sblackshear
Differential Revision: D4605613
fbshipit-source-id: d249212
Summary:
Instead of translating all structs/c++ classes and putting them into type environment, translate ones that are used. It now follows similar mechanism to ondemand function translation. This change should significantly decrease disk space/memory usage to store type environments
+ small change to fix build
Reviewed By: dulmarod
Differential Revision: D4597723
fbshipit-source-id: c8b0365
Summary: Report at most one read/write race or unprotected write per access path per method
Reviewed By: sblackshear, jvillard
Differential Revision: D4590815
fbshipit-source-id: 3c3a9d9
Summary:
To address a common source of false positives observed in D4494901.
We don't do anything with `release` yet, but can model it as releasing ownership in the future if we want to enforce correct usage of `SynchronizedPool`'s.
Reviewed By: peterogithub
Differential Revision: D4593635
fbshipit-source-id: 621e937
Summary: Reports on reads that have one or more conflicting writes. When you report, say which other methods race with it.
Reviewed By: sblackshear
Differential Revision: D4538793
fbshipit-source-id: 47ce700
Summary:
It seems that what `Checkers.ST.store_summary` was called witin on-demand was actually redundant with what `Ondemand` is doing before storing the summaries.
This also makes the `Ondemand` module no longer depend on `Checkers` as the dependency is expected to be the other way around.
Reviewed By: sblackshear
Differential Revision: D4595006
fbshipit-source-id: d62187e
Summary: Thread-local variables can't be shared between threads, so it's safe to mutate them outside of synchronization
Reviewed By: jeremydubreil
Differential Revision: D4568316
fbshipit-source-id: 0634cad
Summary:
Enrich the domain of SIOF to contain, as well as the globals needed by a
procedure, the globals that the procedure initializes. Also add the possibility
to model some procedures as initializing some variables. Use that mechanism to
teach the checker about `std::ios_base::Init`.
Reviewed By: mbouaziz
Differential Revision: D4588284
fbshipit-source-id: d72fc87
Summary:
Reimplement whitelists as a match against a single regexp. This allows one to
precompile the whitelist regexp to make fast check against a whitelist of fuzzy
qualifiers, instead of checks linear in the number of items in the whitelist.
Reviewed By: akotulski
Differential Revision: D4588278
fbshipit-source-id: 3bac614
Summary:
This is useful to make sure `./build-infer.sh clang` and `./build-infer.sh
java` work correctly.
I had to move one unit test inside a new unit/clang/ directory used only if clang is enabled, and create a stub for it in unit/clang_stubs/ for when clang is disabled.
Renamed `OCAML_SOURCES` to the more consistent and descriptive `OCAML_CONFIG_SOURCES`.
Reviewed By: jeremydubreil
Differential Revision: D4571997
fbshipit-source-id: 9502114
Summary:
It's annoying that changing the Makefile or running `./configure` with
different options does not always retrigger compilation of some targets, eg
infer.
Reviewed By: akotulski
Differential Revision: D4571988
fbshipit-source-id: dda080f
Summary:
This gives a way for users to flag safe methods regarding SIOF, for instance if
the problematic paths in the method cannot happen before `main()` has started.
Reviewed By: akotulski
Differential Revision: D4578700
fbshipit-source-id: 6542dcf
Summary: Shorter is better. `--compilation-database` was taken, renaming it to `--buck-compilation-database`.
Reviewed By: dulmarod
Differential Revision: D4567028
fbshipit-source-id: 011cd6f
Summary:
Two options to do the same thing, one for Java and and one for clang, become
one option to do the same thing.
Reviewed By: akotulski
Differential Revision: D4578472
fbshipit-source-id: fb0f21b
Summary:
Before: `make clean` followed by running `infer -- make`. If infer fails, it is
rerun automatically (by the `silent_on_success` Makefile function) to show the
output to the user, but by then there is nothing to build and `make` does
nothing.
Now: run directly `infer -- make clean all`. If infer fails, the command is
rerun and rebuilds all the source files, so there is a higher chance that the
same error will be displayed to the user than the one that originally caused
the command to fail.
Reviewed By: dulmarod
Differential Revision: D4578477
fbshipit-source-id: 774f45c
Summary:
A good first step in order to run multiple checkers together is to prevent the analysis the analysis to side effect on the summaries of the method being analyzed from disk, or the shared specs summary. The idea is that `Ondemand` creates a summary for the procedure being analyzed and only saves the summary once all the checkers have been run. The summary for the caller (i.e. the procedure being analyzed) should never be looked up from disk during the analysis. In other words, the analysis should only ever lookup the summaries of the callees and the proposed solution to enforce this is to have `Ondemand.analyze_proc_name` be the only way to lookup the summary of a procedure.
Another objective is to make sure that the summaries are never saved to disk more than once.
Reviewed By: sblackshear
Differential Revision: D4549764
fbshipit-source-id: f0a6e21
Summary:
We waste a lot of space storing the types of field accesses and comparing them sets/maps with access paths.
Yet almost none of the code ever looks at these types (only a tiny piece of code in thread-safety).
If we know the base type, we have enough information to recover the type of the field.
Let's do that instead.
Reviewed By: jeremydubreil
Differential Revision: D4567996
fbshipit-source-id: e7fd2da
Dulma Churchill
Josh Berdine
Andrzej Kotulski
Sam Blackshear
Jeremy Dubreil
Matthew Haughton
Cristiano Calcagno
Jules Villard
Peter O'Hearn
Ryan Rhee