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:
This simplifies a bit the code to run the analysis on all the prcedures in the cluster. Before, the functions procedure_should_be_analyzed, which loads the attributes, and get_proc_desc were called twice for the analysis of every procedure.
The objective is to remove the calls to procedure_should_be_analyzed and hide it from the ondemand API since it is already called before the analysis of every procedure.
Reviewed By: sblackshear
Differential Revision: D4553397
fbshipit-source-id: 02cffaf
Summary:
One gets very obscure errors when trying to run infer for clang when it was
compiled for Java, or vice-versa. This diff makes sure we crash early with the
appropriate error message. For instance:
```
$ ./build-infer java
$ infer -- clang -c hello.c
Uncaught exception:
(Failure
"Unsupported build mode: make/cc\
\nInfer was built with clang analyzers disabled.\
\nPlease rebuild infer with clang enabled.\
\n")
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "backend/infer.ml", line 398, characters 6-48
Called from file "backend/infer.ml", line 449, characters 20-38
$ infer --clang-compilation-db-files foo.json
Uncaught exception:
(Failure
"Unsupported build mode: clang compilation database\
\nInfer was built with clang analyzers disabled.\
\nPlease rebuild infer with clang enabled.\
\n")
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "backend/infer.ml", line 392, characters 8-65
Called from file "backend/infer.ml", line 449, characters 20-38
```
Reviewed By: sblackshear
Differential Revision: D4566641
fbshipit-source-id: d9a118f
Summary:
- inferbo introduced a dependency to extlib. When building Java analyzers, this
is implicitly pulled in by javalib, but it's missing when building only the
clang analyzers. Add `extlib` to the packages we build against.
- infer.ml and Javac.ml depend on Javalib, but it's easy to push down the code
that needs it to `jMain.ml` so that we can build without javalib for the
clang-only case.
- jMain.mli had 2 copies: one in java/ and one in java_stubs/. Make one a symlink to the other.
Reviewed By: jeremydubreil
Differential Revision: D4566581
fbshipit-source-id: 214a4eb
Summary:
Sevel auxiliary files made it to the output directory of the analysis of individual targets when analyzing Java projects build with Buck. However, these files are then taken into account= to compute the target rule key and then to decide whether to analyze the dependent targets. Since these auxiliary files were containing time sentive information, every cach miss on a given target would then invalitate the cache entries for all the dependent targets.
This diff cleans up the output directory to only keep the specs files, the `global.tenv` and the `report.json` files which are the only artifacts needed to analyze the dependent targets
This diff makes a minimal number of changes to see how it behaves in prod, but I intend to refoctor this more when continuing to add support for running Infer with genrules
Reviewed By: sblackshear
Differential Revision: D4562615
fbshipit-source-id: 4628420
Summary:
Xcode's compilation databases follows a different convention than cmake's and
escape the `"file"` and `"dir"` fields of each unit to make them shell-ready.
We need to treat them differently when reading them.
This adds a new `--clang-compilation-db-files-escaped` option and makes the
code related to reading compilation databases deal correctly with both
conventions.
Reviewed By: akotulski
Differential Revision: D4559239
fbshipit-source-id: 51120ae
Summary:
At one point I thought we'd want to have lots of different schedulers for things like exploring loops in different orders, but that hasn't materialized.
Let's make the common use-case simpler by hiding the `Scheduler` parameter inside the `AbstractInterpreter` module.
We can always expose `MakeWithScheduler` later if we want to.
Reviewed By: jberdine
Differential Revision: D4508095
fbshipit-source-id: 726e051
Summary:
Clients should use `Config.parse_action` instead to figure in what mode they
are operating.
In particular, the biggest change is in logging. Take the `parse_action` into
account instead of the exe, and change the log/ subdirectories to be "capture",
"driver", "analyze", and "print", corresponding to the various phases of an
infer run.
Reviewed By: jberdine
Differential Revision: D4474943
fbshipit-source-id: 6d33ad3
Summary:
Infer used to report null dereference when field was accessed later:
```
vector<int> v;
int& a = v[0]; // should be EMPTY_VECTOR_ACCESS here, but it wasn't reported
int b = a; // was NULL_DEREFERENCE here
```
To avoid this problem, model all accesses to vector as dereference of its internal `beginPtr` field.
Reviewed By: jberdine
Differential Revision: D4481942
fbshipit-source-id: 2142894
Summary:
One of the things that confuses me about the current annotations API is that there's a lot of ways to do the same thing.
Some of the concepts like `annotated_signature` are only really needed by Eradicate.
This diff removes usages of `annotated_signature` outside of Eradicate (everyone else was just using `get_annotated_signature` as a roundabout way to get the return annotation of a procedure).
In the future, I'll move `get_annotated_signature` and other Eradicate-specific functionality into its own module inside the Eradicate directory.
Reviewed By: jberdine
Differential Revision: D4472058
fbshipit-source-id: 5bb0846
Summary:
`pdesc_has_annot` checks the annotations of both the return values and the parameters, which seems like a bad idea in general.
The client should have to specify which annotations they actually care about.
Converting existing uses of `pdesc_has_annot` to what I read as the intended behavior (checking the return annotation).
Will make better use of the other new functions in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D4469885
fbshipit-source-id: de5531e
Summary:
Remove the remaining uses of polymorphic equality `=`.
In case of basic types, this is replaced by String.equal or Int.equal.
In case of `= []`, this is replaced by `List.is_empty`.
In case of `= None`, this is replaced by `is_none`.
In case of a datatype definition such as `type a = A | B`,
a `compare_a` function is defined by adding `type a = A | B [@deriving compare]`
and a `equal_a` function is defined as `let equal_a = [%compare.equal : a]`.
In case of comparison with a polymorphic variant `= `Yes`, the equality
defined in `PVariant.(=)` is used. Typically, `open! Pvariant` is added
at the beginning of the file to cover all the uses.
Reviewed By: jberdine
Differential Revision: D4456129
fbshipit-source-id: f31c433
Summary:
Epilogue tasks such as closing logs or putting files back were we found them
run automatically at the end of our executables by registering them with
`at_exit`. They do not run if the program is interrupted by a signal. This diff
makes sure they are run when the user stops infer with Ctrl-C (SIGINT).
Reviewed By: cristianoc
Differential Revision: D4435575
fbshipit-source-id: c3ab702
Summary:
This replaces the previous integration written in Python, which consisted in 1)
run the mvn command and parse its output to locate "directories containing
source files", 2) run on files named "*.java" in these directories. This meant
we had to run javac twice on each source file, and more importantly this
mechanism of finding source files was very fragile. In fact, I could not make
it work on several mvn projects I tried.
The new integration is based on parsing "pom.xml" to add an "infer-capture"
profile which instructs mvn to run `/path/to/infer` instead of `javac`. We also
add this profile to each maven submodule.
Users can specify an "infer-capture" profile themselves if the default one
doesn't work; in that case we don't inject our own "infer-capture" profile.
Reviewed By: jeremydubreil
Differential Revision: D4409613
fbshipit-source-id: d664274
Summary:
Also make sure we don't introduce deprecated options in our repo, eg when
calling infer from infer.
Reviewed By: jeremydubreil
Differential Revision: D4430379
fbshipit-source-id: 77ea7fd
Summary:
Make the html output available to checkers when -g is used on the command-line.
A checker needs to call a function to start and finish the processing of each node,
and add prints during the processing.
This diff illustrates the case for Eradicate, by adding printing of the pre-state
and post-states.
Reviewed By: sblackshear
Differential Revision: D4421379
fbshipit-source-id: 67501ba
Summary:
Previously, we would first compute which build command is at hand, based on the
first argument after "infer --", then do everything depending on that piece of
information. However, the build command alone is not enough to know in which
"build mode" we are operating. For instance, there are several build modes
corresponding to "buck" build commands.
This led to duplication of the logic (to retrieve which build mode we are in in
the various phases of an infer run), and some invariants that had to be
re-asserted at various points in the code, eg that the arguments are not empty.
This diff adds a `build_mode` type (renaming the previous `build_mode` to
`build_system`) that identifies the various integrations we support. We compute
the build mode at the start of infer, then pass the build mode around.
Also, move `run_javac` to a new `integration/Javac.ml` file given that it's a
bit large.
Reviewed By: jberdine
Differential Revision: D4415074
fbshipit-source-id: db854a0
Summary:
Currently, if we don't find `-d` or `-classes_out` on the command line then we
tell javac to redirect the compiled classes in some other directory, by default
the initial working directory. But we don't detect when these arguments are
hidden inside files (`foo` arguments on the javac command line) so the
heuristic was incomplete. Look inside these files to better tell whether we need
to make up an output directory or not.
Reviewed By: jeremydubreil
Differential Revision: D4397716
fbshipit-source-id: 30c5e4f
Summary:
Sometimes we don't want to analyze but a message gets printed that there was
nothing to analyze and we exit with error, which is confusing.
Reviewed By: jberdine
Differential Revision: D4398120
fbshipit-source-id: 43ce3ab
Summary:
Add more debug output to be able to trace the calls to javac more easily
when --stats or --debug is passed to infer.
Reviewed By: sblackshear
Differential Revision: D4398100
fbshipit-source-id: 3012900
Summary:
This would fail before and works as expected now:
```
$ infer -- clang -c hello.c
$ cd infer-out/ && ln -s ../foo && cd ..
$ infer -- clang -c hello.c # crashes because it fails to delete infer-out/foo
```
Reviewed By: jberdine
Differential Revision: D4398763
fbshipit-source-id: 38465f8
Summary:
One of the tests was failing without `make clean` because infer-out didn't get
deleted when rerunning the clang db test. This was because infer thinks it's in
`Analyze` mode when capturing clang db files.
Reviewed By: akotulski
Differential Revision: D4397731
fbshipit-source-id: 26f423a
Summary:
This error message is confusing when the user is not actually running
InferPrint, eg `infer foo`: `Load Error: file foo: arguments must be .specs
files`.
With this diff, we don't get any error for `infer foo`, which is not great
either and will need to be addressed (do we support all the python arguments in
OCaml now too and are able to turn on argument parsing errors in OCaml land?).
Reviewed By: jberdine
Differential Revision: D4397765
fbshipit-source-id: e7ca48f
Summary:
A domain should not definite its initial state, since distinct users of the domain may want to choose different initial values.
For example, one user might want to bind all of the formals to some special values, and one user might want the initial domain to be an empty map
This diff makes this distinction clear in the types by (a) requiring the initial state to be passed to the abstract interpreter and (b) lifting the requirement that abstract domains define `initial`.
Reviewed By: jberdine
Differential Revision: D4359629
fbshipit-source-id: cbcee28
Summary:
Force clients to specify the path relative to which relative paths
should be made absolute.
Reviewed By: akotulski
Differential Revision: D4370262
fbshipit-source-id: 36a2807
Summary:
There is not much to redirect except for an uninformative line before proper
logging files are set up. This is from before the current logging system, which
has builtin support for logging into custom files.
Reviewed By: jberdine
Differential Revision: D4365988
fbshipit-source-id: 044290a
Summary:
Instead of opening new log files each time with non-deterministic names, keep
appending to the same log files. This only removes the randomized part of the
names in the files. In particular, it keeps the name prefixes for, eg, clang
source files.
Also changed most "<executable>/<executable>-out.log" to simply "<executable>/out.log".
Reviewed By: jberdine
Differential Revision: D4365983
fbshipit-source-id: 46792dc
Summary: This more easily allow to switch between the different modes for handeling dynamic dispatch
Reviewed By: sblackshear
Differential Revision: D4367556
fbshipit-source-id: 795d2c4
Summary: 957b243 removed the last use of `Exe_env.get_tenv ~create:true`
Reviewed By: jeremydubreil
Differential Revision: D4364521
fbshipit-source-id: 819efee
Summary: Use the lazy dynamic dispatch by default in prod for the Java analysis
Reviewed By: sblackshear
Differential Revision: D4356872
fbshipit-source-id: 491e92e
Summary: Adding the information that a procedure has been modelled as part of the attributes, during the translation, instead of getting this information from where is the summary loaded from. This is more consistent with the use of the attributes in other parts of the analysis, but is also useful in the context of the lazy dynamic dispatch algorithm where the procedures, including the models, are cloned and reanalyzed with more specialized parameters. The information about whether a procedure is a model must persist when cloning the procedures.
Reviewed By: sblackshear
Differential Revision: D4356892
fbshipit-source-id: 40ff5ca
Summary:
When you try to log an error on a procedure P and a summary for P doesn't exist, the error gets quietly dropped on the floor.
But we should fail loudly instead, because this should only happen in the case of a user error.
Got burned by this today; I was trying to log an error on the *caller* of `Integer.parseInt`, but was accidentally logging it to `Integer.parseInt` itself instead.
Since no summary for that method exists, my error wasn't appearing.
Reviewed By: jvillard, jeremydubreil
Differential Revision: D4355546
fbshipit-source-id: db2a0e6
Summary:
The two concepts are not negation of each other. The type environment created by the different frontends is not guaranteed to contain a full view of the type hierarchy. In this case, there can be holes preventing Infer to prove that `t <: t'` if the type definition between `t` and `t'` is missing. There are now two functions:
# `is_known_subtype` when the subtyping relation can be proven
# `is_known_not_subtype` when it can be proven that there is no subtyping relation between two types
This diff is intended to make no functional changes but to add functionality to detect cast error angelically, i.e. assuming that the program is probably fine where there is not enough information to prove the cast error.
Reviewed By: jberdine
Differential Revision: D4345803
fbshipit-source-id: 39b79bc
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: 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:
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:
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:
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:
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 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: 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:
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:
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:
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:
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: 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:
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: 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:
Currently cfg nodes are written into dot files in whatever order they
appear in a hash table. This seems unnecessarily sensitive, so this
diff sorts the nodes.
Reviewed By: dulmarod
Differential Revision: D4232377
fbshipit-source-id: a907cc6
Summary: Add some basic command line API to run Infer using Buck genrules. Remains to fix issues with absolute vs relative paths and to see how to create these genrules on the fly for a given java or android library.
Reviewed By: sblackshear
Differential Revision: D4245622
fbshipit-source-id: 1cda4ee
Summary:
Clean up code related to --changed-files-index option:
1. Store DB.SourceFileSet.t in DB.changed_source_files_set
2. Refactor rest of the code to use it
3. Bunch of minor changes to make code more consise
Reviewed By: jberdine
Differential Revision: D4238736
fbshipit-source-id: 51e5684
Summary:
Dealing with symbolic links in project root is tricky. To avoid it, always normalize all paths to sources with `realpath`.
Changes to tests are expected - infer started to resolve symbolic links which screws up with our testing mechanism.
Reviewed By: jberdine
Differential Revision: D4237587
fbshipit-source-id: fe1cb01
Summary: Make backend know filenames of compilation database. It will allow it to compile extra files when needed
Reviewed By: cristianoc
Differential Revision: D4231521
fbshipit-source-id: c462448
Summary: Pure refactoring simplifying the code doing the case analysis for execturing the cast instruction.
Reviewed By: dulmarod
Differential Revision: D4215238
fbshipit-source-id: 9f0f163
Summary:
1. Always store cpp model source_file with relative path. This will make them cache friendly independent of infer location
2. Distinguish between "relative to project root" and "relative to infer models src"
3. Unify `source_file_from_path` used by java and C frontends into one function. There are no improvements to that logic yet
4. Move `is_cpp_model_file` to use `source_file` instead of `filename`
Reviewed By: jberdine
Differential Revision: D4204548
fbshipit-source-id: 6e21771
Summary: This option is unused and it's making DB.source_file_* API harder to simplify
Reviewed By: cristianoc
Differential Revision: D4219803
fbshipit-source-id: 23ce697
Summary:
Using DB.source_file_to_string may return relative path which may or may not be relative to current location.
I went through all calls to `DB.source_file_to_string` and fixed ones that used that output to open files
Reviewed By: jeremydubreil
Differential Revision: D4205407
fbshipit-source-id: b285b7e
Summary:
Developers will sometimes write GuardedBy("T.f") with the intended semantics: "guarded by the field f of the object with type T in the current state".
We want to support this to avoid false positives.
Reviewed By: peterogithub
Differential Revision: D4197476
fbshipit-source-id: acd00d9
Summary:
- fix python calling function with wrong number of arguments (sic)
- print legend of analysis output, this was lost in translation ('F', '.', ...)
- add "Capturing in <mode> mode..." message before capture
- remove version from "Analyzing..." message (users don't even paste the full output, so this is not as useful as initially hoped)
Reviewed By: akotulski
Differential Revision: D4205072
fbshipit-source-id: 2b6505c
Summary: These are dangerous if you are trying to compare a type to a string, and they're also unsightly.
Reviewed By: jvillard
Differential Revision: D4189956
fbshipit-source-id: 14ce127
Summary:
This diff implements enough of the functionality in the python code in
the OCaml toplevel driver that executing `infer -- analyze` is done
with direct procedure calls instead of forking the python interpreter.
Except for some reporting code that remains in report.py.
Reviewed By: jvillard
Differential Revision: D4074718
fbshipit-source-id: 56a794d
Summary:
Record an abstraction of the bug traces in the tests. The abstraction of a
trace is the sequence of descriptions. In practice, descriptions are either
empty, or of the form "start/end/return from/call to procedure X". They seem
pretty stable.
Motivation: there is nothing testing the traces reported by Infer right now,
even though they are surfaced to developers. For instance, Quandary uses
--issues-txt instead of --issues-tests to make sure the traces do not regress.
This change would make this approach more widespread.
Reviewed By: sblackshear
Differential Revision: D4159597
fbshipit-source-id: 9c83952
Summary: clang has very complicated logic what to translate based on `project_root` and filename. Add tests for different situations in regard of symbolic links in path/project_root
Reviewed By: jvillard
Differential Revision: D4168551
fbshipit-source-id: 586b364
Summary: Refactoring to make thread safety checker interpocedural. This should not change funcitonality, and will only set things up for making the interprocedural part more serious.
Reviewed By: sblackshear
Differential Revision: D4124316
fbshipit-source-id: 6721953
Summary:
When loading results from a json file, sort them. This prints results in some
sane order for both --issues-test and --issues-txt, removing the need for
post-processing of the result.
Reviewed By: cristianoc
Differential Revision: D4167029
fbshipit-source-id: 37e9f1c
Summary: The thread safety checker is run independently of other analyses, using the command "infer -a threadsafety -- <build-command>".
Reviewed By: sblackshear
Differential Revision: D4148553
fbshipit-source-id: bc7b3f9
Summary: When searching for cast errors, types that were not Java objects, e.g. arrays of primitive types were not taken into account, leading to incorrect class cast excpetion reports.
Reviewed By: sblackshear
Differential Revision: D4166184
fbshipit-source-id: 7157c95
Summary:
It was defined in two places and I'm about to add a third, so let's share
instead.
Reviewed By: sblackshear
Differential Revision: D4153420
fbshipit-source-id: 3d2c519
Summary:
Move code that initializes the InferAnalyze executable from
InferAnalyze.main to InferAnalyzeExe. This enables InferAnalyze.main to
be called from other executables without conflicts due to
initialization.
Reviewed By: jvillard
Differential Revision: D4137280
fbshipit-source-id: 3dd76db
Summary: Also use the executable as a default name prefix.
Reviewed By: akotulski, jvillard
Differential Revision: D4135539
fbshipit-source-id: 84ba011
Summary:
Location.nLOC was introducing a lot of complexity for little benefit (and edge cases were wrong anyway).
We can restore it in some simplified way if we find that we need it
Reviewed By: jeremydubreil
Differential Revision: D4139868
fbshipit-source-id: 4f8e033
Summary:
Summaries are modified before saving from disk, for example the attributes of the postcondition can change.
I have observed flaky reports of the internal error NULL_TEST_AFTER_DEREFERENCE. Some attributes (e.g. assigned) are changed before saving, but the spec table in memory is not changed.
So in case:
1) the procedure is analyzed on-demand, then subsequent uses in the same process use the summary in memory with the unchanged attribute, and the issue is not reported.
2) the procedure is already on disk and loaded, then the loaded summary has the changed attributes, and the issue is reported.
Flakiness happens as because of parallelism, whether a procedure is analyzed already or whether it is analyzed on-demand, can change.
The normalization function can change the instrumentation of a symbolic heap because it uses the existing comparison functions, which ignore instrumentations.
So normalization can replace part of a symbolic heap with an identical one but where the instrumentation is different — this is what I have observed.
The diff uses a different comparison function where instrumentations are taken into account.
Reviewed By: jberdine
Differential Revision: D4140031
fbshipit-source-id: f4f119a
Summary:
Instead of the custom filtering done by `InferPrint --issues-tests`, use the
filtering done by `infer` and run without filtering for our e2e tests. We still
test the filtering for our build systems integration tests, and this diff
restores that behaviour for the ant test (hence the bugs removed from
ant/issues.exp).
Also add internal exceptions to most tests to get more signal out of them (eg,
knowing when we add assertion failures and the like).
Retire the old `--issues-tests` to limit the number of ways we do filtering.
Reviewed By: jeremydubreil
Differential Revision: D4131308
fbshipit-source-id: 35805cc
Summary:
This will be useful to migrate the existing tests to using report.json to
output the list of bugs found by Infer. This will make the tests reflect what
happens in prod more faithfully: right now running with --issues-tests does its
own filtering starting from the specs.
Moreover, this will allow --issues-tests to support the Buck integration, where
the specs/ directory is not populated after a run (although I suppose we could
also copy them from buck-out/ for InferPrint's benefit).
Reviewed By: jeremydubreil
Differential Revision: D4130851
fbshipit-source-id: 0457fba
Summary:
This makes our python code work (instead of crashing) when the source file
should be found not from the current directory (or absolute path), eg with
`infer --project-root .. -- clang -c hello.c`.
Reviewed By: jeremydubreil
Differential Revision: D4130802
fbshipit-source-id: 001f72d
Summary:
If the project root contains ".." then it doesn't work as expected, eg
infer --project-root .. -- clang hello.c
doesn't report at all. Now it works.
Reviewed By: jeremydubreil
Differential Revision: D4125489
fbshipit-source-id: 06b10ad
Summary: These functions are also called when the summary is guaranteed to exist. Enforcing this within the API
Reviewed By: cristianoc
Differential Revision: D4126839
fbshipit-source-id: 305b484
Summary: For some reason, `Specs.is_active` was re-loading from the specs table the summary that should already be in scope.
Reviewed By: cristianoc
Differential Revision: D4124693
fbshipit-source-id: c0e9113
Summary: Right now there is no test for compilation database integration. Add one
Reviewed By: jvillard
Differential Revision: D4118769
fbshipit-source-id: 5591de7
Summary:
This diff adds a skeleton implementation of the capture and analysis
driver to infer.ml, and removes some unnecessary code from infer.py.
With this, individual capture and analysis modules can be added, or
moved from python.
Reviewed By: jvillard
Differential Revision: D4109547
fbshipit-source-id: 0dce2bf
Summary: Don't use a hardcoded string, and enable reports in --issues-tests.
Reviewed By: jvillard
Differential Revision: D4110731
fbshipit-source-id: 9922557
Summary:
ClusterMakefile need not depend on Sys.executable_name referring to
InferAnalyze, use Config.bin_dir instead.
Reviewed By: jvillard
Differential Revision: D4110730
fbshipit-source-id: c330bb3
Summary:
Child processes invoked in multicore mode get arguments using the usual
INFER_ARGS mechanism already, no need for a special case.
Reviewed By: jvillard
Differential Revision: D4110728
fbshipit-source-id: 0987216
Summary: We want to skip readwrite locks for now, maybe report on their misuses later.
Reviewed By: sblackshear
Differential Revision: D4110998
fbshipit-source-id: 986f77e
Summary:
this makes frontends no longer depend on SymExec.ml. `ModelBuiltins` was split into two modules:
- `BuiltinDecl` with procnames for builtins (used to determine whether some function is a builtin)
- `BuiltinDefn` with implementations used by `SymExec`
- they both have similar type defined in `BUILTINS.S` which makes sure that new builtin gets added into both modules.
During the refactor I ran some scripts:
`BuiltinDecl.ml`:
let X = create_procname "X"
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,$4,"\42"$2"\42"} '
then manually confirm string match. Exceptions:
"__exit" -> "_exit"
"objc_cpp_throw" -> "__infer_objc_cpp_throw"
__objc_dictionary_literal
nsArray_arrayWithObjects
nsArray_arrayWithObjectsCount
`BuiltinDefn.ml`:
let X = Builtin.register BuiltinDecl.X execute_X
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,"Builtin.register BuiltinDecl."$2,"execute_"$2} '
then, fix all compilation problems
Reviewed By: jberdine
Differential Revision: D3951035
fbshipit-source-id: f059602
Summary: Doing `sychronized(A.class)` where `A` is an inner class was not previously recognized by the `GuardedBy` checker.
Reviewed By: peterogithub
Differential Revision: D4095094
fbshipit-source-id: c832f9e
Summary:
Now that it's possible to run clang wrapper as a function from another process,
Logging module cannot rely on `Config.current_exe` to determine which directory
it should write to.
Reviewed By: jeremydubreil
Differential Revision: D4095455
fbshipit-source-id: d989b06
Summary:
Change command line options for dynamic dispatch to capture that the
alternatives are mutually exclusive.
Reviewed By: jeremydubreil
Differential Revision: D4074540
fbshipit-source-id: c329717
Summary: The lazy dynamic dispatch algorithm works by re-analyzing the generic methods with the more specialized types encountered during the symbolic execution. In order to do that, the analysis must access the procedure description of the method to reanalyze in order to run the analysis of the specialized procedure description on demand. This diff adds the procedure description on the summary as the summary are stored in the Buck cache and can easily be retrieved by procname.
Reviewed By: sblackshear
Differential Revision: D4077415
fbshipit-source-id: c2f1cc8
Summary:
- do a semantic analysis of each variable initializer to figure out if they need initialization
- add a flag to globals that is true when they are `constexpr`. In that case, no analysis is needed as the user + compile guarantee that it is a compile-time constant.
Reviewed By: sblackshear
Differential Revision: D4081273
fbshipit-source-id: 44dbe29
Summary:
Merging the results directories of targets on buck projects involved creating symbolic links into buck-out.
The bulk of files are .attr files: one per procedure. Creating these links can be a bottleneck, and the merge phase can be slower than the analysis phases on projects with many procedures.
This diff introduces multilinks to speed up merge.
A multilink is a file `multilink.txt` containing a sequence of paths
```
path/to/file1.ext
path/to/file2.ext
...
```
A multilink file is a compact way to represent a link for each entry.
This diff creates a multilink file for each `attributes/dir` directory, instead of one symbolic link for each file.
Reviewed By: jberdine
Differential Revision: D4067428
fbshipit-source-id: 911f8a9
Summary:
Config.analyze_models, set by the INFER_ANALYZE_MODELS environment
variable, is redundant with Config.models_mode.
Reviewed By: jvillard
Differential Revision: D4047338
fbshipit-source-id: 4522d65
Summary: Some arguments passed from infer.ml to infer.py were only used to pass further to infer.ml invocations. Those args should be passed by env variable anyway (???)
Reviewed By: jberdine
Differential Revision: D4048003
fbshipit-source-id: 6f5fbeb
Summary:
Python isn't needed anymore to pass options between `infer` and `InferClang`.
However, it is still needed to set up `PATH` so that we pick up compilation
commands.
Reviewed By: jberdine
Differential Revision: D4008469
fbshipit-source-id: 05c5716
Summary:
Checker for the Static Initialization Order Fiasco pattern:
https://isocpp.org/wiki/faq/ctors#static-init-order
1. Collect all globals (transitively) accessed in any given procedure.
2. Once the interprocedural analysis has finished, look at globals accessed in
initializers that do not belong to the current translation unit.
Reviewed By: sblackshear
Differential Revision: D3780266
fbshipit-source-id: 1d07161
Summary:
There's no reason for infer to be in lib/ anymore, move it to the same place as
the other binaries. Thus all binaries are in the same directory and Config.ml
can better know where things are.
Reviewed By: jberdine
Differential Revision: D4015958
fbshipit-source-id: c5e851f
Summary:
This fixes a perf issue on large files, where a copy of the type environment and control flow graph were loaded for each procedure analyzed in the file.
If the type environment or the control flow graph are big, and the file contains many procedures, this can cause a big memory overhead.
Reviewed By: jvillard
Differential Revision: D4008655
fbshipit-source-id: 11d07c1
Summary:
This changes executions of the former InferClang into a function call. In
particular, it can be called several times per execution.
The new InferClang must be called as if it was clang, and knows how to run
clang with our plugin to get the AST of the source file.
Reviewed By: akotulski
Differential Revision: D3981017
fbshipit-source-id: 7af6490
Summary:
This diff removes the unused support for reporting props, which enables
refactoring so that the 'base' directory has no dependencies, and the
'IR' directory depends only on 'base'.
Reviewed By: jvillard
Differential Revision: D3981352
fbshipit-source-id: 3700a23
Summary:
This changes the algorithm for pure join to keep the constraints that,
after normalization, occur in both arguments. Previously pure join
would normalize, filter, and then union the constraints of the
arguments.
Reviewed By: sblackshear
Differential Revision: D3970394
fbshipit-source-id: 3dc1672
Summary:
This is needed for later: InferClang will no longer be started once for each
source file to be analysed. Instead, it will be called to analyse several files
at once, and will analyse them one by one. Thus, `clang_lang` and `source_file`
are moved to `cFrontend_config` as references.
The biggest change this entailed was the new logging infrastructure, which was
depending on `Config.source_file`. This diff moves the logic entirely to
`Logging`, and changes the API so that executables wishing to log into files
have to set it up using `Logging.set_log_file_identifier`. This can be called
several times during the execution, allowing to dynamically change the log file
(eg, when analysing several source files one by one!).
Reviewed By: jberdine
Differential Revision: D3944148
fbshipit-source-id: 6129090
Summary:
Let's start migrating some of our bash script to OCaml to make them easier to
maintain and extend.
For now replace just one script and put it in lib/clang_wrappers/ at compile
time, where the former script used to be. Further simplifications will come
later.
Reviewed By: jberdine
Differential Revision: D3929988
fbshipit-source-id: b2d8b37
Summary: The code has not much to do with IR and should be part of backend/ directory.
Reviewed By: sblackshear
Differential Revision: D3950834
fbshipit-source-id: 315ea19
Summary:
Move most of common dependencies out of backend/ into base/
Diff doesn't change any code and hence files in base/ may still depend on
code outside of base/. There will be followup diff cleaning those up.
There are also files that maybe should be in common/ but haven't been moved there yet.
Reviewed By: jberdine
Differential Revision: D3950695
fbshipit-source-id: 00612b1
Summary:
Just adds a language agnostic option to skip the analysis of some files based on the path name. Can be used from the command line with:
infer infer --skip-analysis-in-path "some/path/" ...
or via the `.inferconfig` file:
{
"skip-analysis-in-path": [
"infer/demo/Resource.java"
]
}
Reviewed By: jberdine
Differential Revision: D3954809
fbshipit-source-id: d0d2b9f
Summary:
It's nice to be able to know how well the process we started did, although this
diff ignores it for now.
Reviewed By: dulmarod
Differential Revision: D3937902
fbshipit-source-id: 80bf20f
Summary:
In order to have only InferJava depend on JBasics, do not use
JBasics.java_lang_object in the IR or backend. Note that this implies
that the Java frontend should ideally translate JBasics.java_lang_object
to Typename.Java.java_lang_Object.
Reviewed By: jeremydubreil
Differential Revision: D3956468
fbshipit-source-id: def64dd
Summary:
Change implementation of NSArray and NSDictionary model builtins to use
the method return type instead of magicking up types from strings.
Reviewed By: jvillard
Differential Revision: D3919815
fbshipit-source-id: f07a993
Summary:
Change Sil.Call instruction to have only a single optional return
identifier, insted of a list. Essentially none of the code handled
multiple return identifiers. Also, add the type of the return
identitifier to Call instructions.
Reviewed By: sblackshear
Differential Revision: D3919358
fbshipit-source-id: d2d4f72
Summary:
Refactor Sil.struct_typ and associated operations into a separate
StructTyp module. This is possible now that Typ.Tstruct only carries a
type name instead of the definition directly, and is helpful to simplify
module dependencies.
Reviewed By: cristianoc
Differential Revision: D3919357
fbshipit-source-id: a37a656
Summary:
It is no longer necessary to keep the name of a struct within the
struct, as the name will just have been used to look it up.
Reviewed By: cristianoc
Differential Revision: D3919355
fbshipit-source-id: ab65168
Summary:
Pass the exe_env to checker cluster callbacks, and add it to the domain
extras for BoundedCallTree, and use the Exe_env instead of
AttributesTable to obtain the tenv.
Reviewed By: sblackshear
Differential Revision: D3921850
fbshipit-source-id: 9edf324
Summary: The Infer builtins can be used in the e2e tests, but those tests should not depend on the Infer models to avoid cyclic dependencies. This diff separates the models and the Infer builtins in two directories so that the test can depend on the builtins without depending on the models
Reviewed By: sblackshear
Differential Revision: D3929478
fbshipit-source-id: 7d0ab79
Summary:
The global reference `DB.current_source` is used internally in the module DB, by all the front-ends, and directly and indirectly by the back-end, including saving and restoring the state in case of on-demand procedure calls. In particular, it is heavily used in printing functions.
This diff cleans up the flow of information about what the current file is, making it explicit, and removes the reference.
Reviewed By: jberdine
Differential Revision: D3901247
fbshipit-source-id: ef596bd
Summary:
Create the log directory even if the parent results directory does not
exist. In particular, the python buck module will delete the results
directory after it is created the first time, so it needs to be
re-created or else there is nowhere for the log files.
Reviewed By: sblackshear
Differential Revision: D3896546
fbshipit-source-id: 834cf79
Summary:
Rename symbols in test files so they are not duplicated and files can be analyzed together without affecting analysis results.
Fix some compilation errors, where files could be analyzed but would fail direct compilation.
Add Makefile mimicking the same analysis parameters used for the existing tests.
Reviewed By: dulmarod
Differential Revision: D3869993
fbshipit-source-id: 6db1baf
Summary:
This diff removes the redundancy in the representation of types where
struct types could be represented either directly using Tstruct or
indirectly using Tvar to refer to the type environment. A consequence
is that it is much harder to construct large type values.
Reviewed By: sblackshear, cristianoc
Differential Revision: D3839753
fbshipit-source-id: cf04ea5
Summary:
Rename Typ.mk_struct to internal_mk_struct, and add Tenv.mk_struct that
ensures types are added to the environment under the right name.
Reviewed By: cristianoc
Differential Revision: D3791865
fbshipit-source-id: fd4b667
Summary:
The Typ.struct_typ.csu field is now redundant with the Csu.t in the
name: Typename.t field.
Reviewed By: cristianoc
Differential Revision: D3791861
fbshipit-source-id: 5370885
Summary: Replace the struct_name: Mangled.t option field of Typ.struct_typ with name: Typename.t
Reviewed By: sblackshear
Differential Revision: D3791860
fbshipit-source-id: 3ee1d00
Summary:
This diff fixes two issues in the backend that were causing Bad_footprint
errors when abducing pointsto facts for expressions that start in an array
access and follow up with another structured access, eg `x[0].some_field`:
1. array accesses were assumed to come last in these expressions
2. the type of the root exp passed to the function that walks down the list of
offsets to apply to it was wrong in the case of arrays: it was always the
type of the whole expression instead of the root expr (eg the type of
`x[0].some_field` instead of the type of `x`).
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D3800566
fbshipit-source-id: 0511604
Summary:
This simplifies the determination of whether the current process is the
originator of all the infer sub-processes.
Reviewed By: jvillard
Differential Revision: D3751324
fbshipit-source-id: 5e6dc6b
Summary: Make it possible to run infer code from within `ocaml`/`utop`. Integration is really basic, but we can extend it if we find it useful.
Reviewed By: jberdine
Differential Revision: D3736029
fbshipit-source-id: 4cebb7c
Summary: Python needs to know about the value of -l if the user passes it at the top level.
Reviewed By: martinoluca
Differential Revision: D3757614
fbshipit-source-id: fbd3c0f
Summary:
Infer doesn't go looking into field values when looking for unsigned
expressions, which could cause some unintended reports.
Reviewed By: sblackshear
Differential Revision: D3724232
fbshipit-source-id: 9c4cd97
Summary:
This was causing headaches as catching error code 2 may hide real issues.
While there, move crashcontext finalizer code to crashcontext.ml, and create a
.mli file for that module.
Reviewed By: jberdine
Differential Revision: D3742785
fbshipit-source-id: 3032451
Summary:
Make `infer -h` behave the same as `--help`, document it, and finally align the
`--help` and `--help-full` options with the other options in the help output
(they are added separately from the other options so this wasn't the case
before).
Reviewed By: jberdine
Differential Revision: D3741778
fbshipit-source-id: a0c81ba
Summary:
The error code was always 1, and was only enabled in crashcontext mode due to a
typo.
Reviewed By: sblackshear, lazaroclapp
Differential Revision: D3735661
fbshipit-source-id: c0bb0f5
Summary:
On wrong arguments (or on no arguments at all), `infer` would spew the error
message of `infer.py`, which makes no sense. Make the python code swallow error
messages and exit with a special code on errors coming from command line
parsing so that the OCaml side is in charge of printing usage messages.
Reviewed By: cristianoc
Differential Revision: D3731594
fbshipit-source-id: fe49cda
Summary:
This helps avoid some unintended reports where the actual is known to point to
a specific object before a call to a skipped function. This requires a change
in the plugin to export more info about const types.
Reviewed By: dulmarod
Differential Revision: D3711901
fbshipit-source-id: f5c903e
Summary:
Adding a new mode linters. Now if the analyzer is linters, we do the linters and don't translate,
then, if the analyzer is Infer, we do the translation and the backend and not the linters checks, and the
default is that we do capture, backend and lint checks.
Made the tests separated, which saves time and also shows that the linters mode works.
Reviewed By: jvillard
Differential Revision: D3723472
fbshipit-source-id: 9d828d8
Summary:
So far infer had very fragile mechanism to detect smart pointers. It was looking for "std" and "(shared|unique)_ptr" inside name string.
This is easy to trick (like mystd::shared_ptr) and not something we want.
Instead, inside models create models inside infer_std_model namespace. Then just "export" that model into std namespace
via `using shared_ptr = infer_std_model<T>;`
Reviewed By: jvillard
Differential Revision: D3703827
fbshipit-source-id: 9640fc2
Summary:
- make sure former options of `./infer/lib/python/infer.py --help`, `./infer/lib/python/infer.py --help -- make`, ... all appear in `infer --help`
- add some options to config.ml and infer.ml to fix missing options
- have `infer --help` output help info for Toplevel + Backend + Clang + Java
- wrap help lines at 80 characters
Reviewed By: jberdine
Differential Revision: D3669865
fbshipit-source-id: 1ceff2d
Summary:
Refactor module Prop disentangling the various normalization functions, and moving them inside a new module Normalize.
There is quite a reshuffling of functions, including some dead code removal, but there should be no computational difference.
Reviewed By: jvillard
Differential Revision: D3696491
fbshipit-source-id: 68dd719
Summary:
Clean up the API to access component of propositions.
Use uniform naming for getting and setting components.
Reviewed By: jberdine
Differential Revision: D3696180
fbshipit-source-id: a8aedb0
Summary:
Add module `Core` in Prop to contain the implementation of a prop as a record. The record is private so that pattern matching is unchanged.
Added new function to set individual fields, enforcing that the type becomes exposed when constructing explicitly.
Added function unsafe_cast_to_normal to mark all the cases where a coercion to a normalized type is used.
This is purely a refactoring diff that only affects types, it should have no runtime consequence.
Reviewed By: jberdine
Differential Revision: D3691342
fbshipit-source-id: fa06e29
Summary:
Attribute.remove was performing an ad hoc form of normalization on
atoms, replace with the standard normalization from Prop.
Reviewed By: cristianoc
Differential Revision: D3686041
fbshipit-source-id: b89e59e
Summary:
This diff lifts the Prop.Attribute module out of Prop. This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches. Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.
Reviewed By: cristianoc
Differential Revision: D3684523
fbshipit-source-id: f37af8b
Summary:
Move the Sil.attribute type and associated types and operations to a new
PredSymb module.
Reviewed By: cristianoc
Differential Revision: D3683834
fbshipit-source-id: d3606a8
Summary:
Change the Aobjc_null attribute from a family of unary predicates, one
for each Pvar.t * Ident.fieldname list, to a single binary predicate.
This diff should not change behavior except for printing of Aobjc_null
attributes. Also, operations such as free variables, etc. should now
behave correctly with respect to variables occurring in the arguments of
Aobjc_null.
Reviewed By: cristianoc
Differential Revision: D3669392
fbshipit-source-id: fe4434a
Summary:
Add support for nary predicates, not just unary ones. Many operations
don't make much sense for nullary predicates, and are generally treated
as no-ops. The first argument is treated specially, as the "anchor" of
the predicate application. For example, adding or removing an attribute
uses the anchor to identify the atom to operate on. Also, abstraction
and normalization operations treat the anchor specially.
Reviewed By: cristianoc
Differential Revision: D3669391
fbshipit-source-id: 3d142ea
Summary:
There is no need to call exp_normalize on the sub-expressions of
arguments to atom_normalize, as it calls exp_normalize on its
sub-expressions.
Reviewed By: cristianoc
Differential Revision: D3669390
fbshipit-source-id: 468b6b1
Summary:
Simplify the (implementation and) interface of Prop by using the atom
type directly instead of a tuple type that duplicates the fields.
This change does not weaken the type guarantees, while reducing
redundancy between types thereby making future changes easier.
Reviewed By: cristianoc
Differential Revision: D3669388
fbshipit-source-id: 65f7493
Summary:
Change representation of pure predicate applications to distinguish
between positive and negative literals using the Apred and Anpred
constructors instead of a boolean field.
This representation is more compact, and is uniform with the treatment
of equalities and disequalities. Some code is simpler, but there isn't
much in it.
Reviewed By: cristianoc
Differential Revision: D3669387
fbshipit-source-id: 07cdea6
Summary:
Treat attributes as unary predicates in classical first-order logic.
This diff extends predicates with a polarity and uses classical 2-valued
semantics. This potentially changes the behavior of negating
attributes, which was not previously relied on.
Reviewed By: sblackshear
Differential Revision: D3669365
fbshipit-source-id: 2f26776
Summary:
Replace disequalities to Attribute expressions with predicate symbol
application pure atomic formulas.
This diff should preserve existing behavior, up to the comparison order
of attribute disequalities versus predicate applications.
Reviewed By: sblackshear
Differential Revision: D3647049
fbshipit-source-id: c39a901
Summary:
Cosmetic changes to comments to improve the results of the Reason
comment attachment logic.
These were found using `git grep -nH -e 'in[ ]*(\*'` although the
attachment logic seems ok if the associated `let` is on the same line.
Some others were found with `git grep -nH -e ')[ ]*(\*'` although the
attachment logic seems ok if the associated `(` is on the same line.
Reviewed By: jvillard
Differential Revision: D3654027
fbshipit-source-id: 122aa3b
Summary: Follow up D3579581. We forget about memory acquired in resources with assumption that developers use raii and free memory in destructors.
Reviewed By: jvillard
Differential Revision: D3614056
fbshipit-source-id: 08fa112
Summary:
This is needed on osx, where one of {`Sys.executable_name`, `Unix.readlink`}
does not behave the same as Linux.
Reviewed By: jberdine
Differential Revision: D3614254
fbshipit-source-id: a376636
Summary:
Previously, we would translate `throw` with `return`. However, `throw` in
ObjC/C++ is often used to mean "abort". We now translate `throw` the same as
`exit` to prune these paths.
Reviewed By: akotulski
Differential Revision: D3594156
fbshipit-source-id: 81083bb
Summary:
Python needs to know about these because it does different things depending on
whether these flags are passed or not.
Reviewed By: cristianoc
Differential Revision: D3593381
fbshipit-source-id: fe3194d
Summary:
Store more information inside Procname.objc_cpp type: replace mangling info
with "kind" info, which also contains mangling info when appropriate.
Reviewed By: akotulski
Differential Revision: D3580283
fbshipit-source-id: b1197ed
Summary:
Generation of the module dependency graph was broken (all IR modules
were omitted) by the reason conversion.
Reviewed By: cristianoc
Differential Revision: D3541395
fbshipit-source-id: e5af125
Summary: Move Sil.dexp type and operations into separate DecompExp module.
Reviewed By: dulmarod
Differential Revision: D3548095
fbshipit-source-id: 5ab4360
Summary:
Move Sil.call_flags type and operations into separate CallFlags
module.
Reviewed By: dulmarod
Differential Revision: D3548086
fbshipit-source-id: 6d264e9
Summary: Move Sil.binop type and operations into separate Binop module.
Reviewed By: dulmarod
Differential Revision: D3548082
fbshipit-source-id: 356bee3
Summary: Move Sil.unop type and operations into separate Unop module.
Reviewed By: dulmarod
Differential Revision: D3548077
fbshipit-source-id: 49d3d83
Summary: Move Sil.const type and operations into separate Const module.
Reviewed By: dulmarod
Differential Revision: D3548073
fbshipit-source-id: 388d03e
Summary:
Move attribute values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: cristianoc
Differential Revision: D3548055
fbshipit-source-id: 31a9121
Summary: Use Prop.atom_negate in Rearrange instead of almost reimplementing it.
Reviewed By: sblackshear
Differential Revision: D3554171
fbshipit-source-id: 9baabc9
Summary:
The Aobjc_null attribute does not need a fully general exp. This diff
refines this to a possibly-empty path of fields starting from a pvar,
which reduces interdependence between Sil types.
Reviewed By: dulmarod
Differential Revision: D3548043
fbshipit-source-id: 49d16ab
Summary:
Move closure values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: sblackshear
Differential Revision: D3541364
fbshipit-source-id: 1a2f998
Summary:
Move exception values from const to exp. They are not constants, and
this reduces interdependence between Sil types.
Reviewed By: sblackshear
Differential Revision: D3541355
fbshipit-source-id: f22e0ba
Summary:
Move analyzer type and ops from Utils to Config, and simplify by
reducing interface. There are very few uses so no need to pollute
global namespace.
Reviewed By: sblackshear
Differential Revision: D3541047
fbshipit-source-id: 2be56af
Summary: Change length of Dsizeof from an exp to a dexp. This make a little progress toward reducing the types that must be mutually recursive with exp.
Reviewed By: sblackshear
Differential Revision: D3541337
fbshipit-source-id: 95d1f70
Summary:
Simplify config implementation to make it easier to define new
executables.
Reviewed By: martinoluca
Differential Revision: D3529213
fbshipit-source-id: 71324a2
Summary:
Document how to define new command line and config file options, and
slight cleanup.
Reviewed By: jvillard
Differential Revision: D3528952
fbshipit-source-id: 6bd7601
Summary:
Call infer with `--unsafe-malloc` or set `unsafe-malloc: true,` in .inferconfig to
have infer assume that `malloc()` never returns null.
closes#389
Reviewed By: jberdine
Differential Revision: D3522169
fbshipit-source-id: 6b88a16
Summary: `Config.abs_val` was always set to 2 instead of taking its value from the option.
Reviewed By: jberdine
Differential Revision: D3515024
fbshipit-source-id: fa27396
Summary:
Simplify DB initialization by removing some unit functions, since
Config values are now already initialized at module load time.
Reviewed By: akotulski
Differential Revision: D3522728
fbshipit-source-id: ac93d30
Summary:
Use resolve instead of filename_to_absolute, to resolve relative paths
in command line arguments with respect to the working directory infer
is initially invoked from, rather than the possibly-changed current
working directory of the child processes.
Also use initial instead of current working dir for default
project_root and results_dir
Reviewed By: martinoluca
Differential Revision: D3467571
fbshipit-source-id: fbb0f3f
Summary:
In InferPrint, ignore non-existent dirs when looking for specs. This
allows InferPrint to work when the results dir does not exist.
Reviewed By: sblackshear
Differential Revision: D3522757
fbshipit-source-id: 5ef905d
Summary:
Create log dir only if results_dir exists, otherwise, log to standard
output and error even in developer mode.
Reviewed By: sblackshear
Differential Revision: D3522737
fbshipit-source-id: e00571b
Summary:
There is nice hook inside glog/logging.h for all CHECK_(GT|LT|GE|...) macros.
This simplifies AST significantly which makes infer way more happy:
cda16b3443/src/glog/logging.h.in (L722-L724)
Reviewed By: jberdine
Differential Revision: D3522110
fbshipit-source-id: 70c94cb
Summary:
InferPrint used to:
1. always print specs to stdout
2. not require --results-dir to be present
3. if invoked with .spec file, print just that file (that broke long time ago I think)
This diff fixes only (1) as this is most annoying and easiest part, but the rest should be fixed as well
Reviewed By: sblackshear
Differential Revision: D3504015
fbshipit-source-id: 469b46f
Summary: in text mode (`pp_stats`), we print it and so we probably should to the same for html
Reviewed By: jvillard, sblackshear
Differential Revision: D3497678
fbshipit-source-id: 3d47d2a
Summary: Those functions have simple enough implementations for infer to understand them
Reviewed By: jvillard
Differential Revision: D3463084
fbshipit-source-id: f84160f
Summary:
This diff changes the toplevel 'infer' executable from the current
python script to an OCaml binary. Currently this executable only parses
command line arguments, sets up environment variables, and invokes the
existing python script. This improves infer's command-line and
configuration interface, since passing arguments to the frontends or
backend no longer requires manually setting environment variables, and
arguments for the toplevel can now also be specified in .inferconfig.
Simplification and migration of functionality from the python script is
left for the future.
Reviewed By: martinoluca, jvillard
Differential Revision: D3450662
fbshipit-source-id: 1b52302
Summary: Move the initialization code for Logging into the Logging module.
Reviewed By: sblackshear
Differential Revision: D3466751
fbshipit-source-id: 9e79c5b
Summary:
Deabbreviate CommandLineOption.exe type constructors, which correspond
to the various infer executables.
Reviewed By: cristianoc
Differential Revision: D3455942
fbshipit-source-id: f25ed77
Summary:
The code to set the minor heap size confused bytes and words, and so was
off by a factor 8. Fortunately it attempted to set the minor heap to
1MB and got the better value of 8MB instead.
Reviewed By: cristianoc
Differential Revision: D3455937
fbshipit-source-id: 48d0e23
Summary:
Two phase parsing of command line options, part of unifying command
line options and .inferconfig, broke the --help and --help-full usage
messages. This diff fixes them.
Reviewed By: jvillard
Differential Revision: D3435521
fbshipit-source-id: d4ecbb1
Jeremy Dubreil
Dulma Churchill
Jules Villard
Cristiano Calcagno
Sam Blackshear
Andrzej Kotulski
Kihong Heo
Josh Berdine
Peter O'Hearn
Martino Luca
Dino Distefano
Ryan Rhee
Lázaro Clapp Jiménez Labora
Daiva Naudziuniene