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: pattern matching we had before allowed many unintended functions to pass (such as `max_element`). Make matching much more strict
Reviewed By: jvillard
Differential Revision: D4313428
fbshipit-source-id: 189c522
Summary:
This will simplify the InferPrint logic of checking what should/should-not be reported.
I will remove the issue names in Localise in a next diff.
Reviewed By: ddino
Differential Revision: D4334327
fbshipit-source-id: ebcfd6c
Summary:
This change is to support the development of CTL's DSL, where issues can be specified directly from the language, in the form of strings.
Severity is specified locally to the place where the check is defined
Reviewed By: ddino
Differential Revision: D4326594
fbshipit-source-id: 7b146ac
Summary:
This diff introduces place-holders strings in error messages and evaluates them
when an error needs to be reported.
Place-holders strings are of the form %name_of_helper_function%. They will be evaluated
using and helper function that gives a value.
For example if we need to display the name of a variable in the error message we will have:
".... %var_name%...."
then %var_name% will be evaluated in the ast node calling the appropriate
helper function and the results will replace %var_name% in the message.
Reviewed By: dulmarod
Differential Revision: D4313133
fbshipit-source-id: bf521ca
Summary:
The debug script wants to run InferClang on the file at hand, but that often
involves running a -cc1 command with InferClang, which is no longer supported.
This removes this functionality. The debug script now only dumps the AST to
biniou and its text representation.
Reviewed By: dulmarod
Differential Revision: D4319431
fbshipit-source-id: ef64912
Summary: 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:
In particular, the method for retrieving an element from the array, this should never be nil. Also added a model for count
similar to the one for NSString length.
Reviewed By: ddino
Differential Revision: D4306655
fbshipit-source-id: 0ecb25a
Summary:
This is to prevent clang from changing AST to make it more performant and less readable.
Reported in https://github.com/facebook/infer/issues/522
+ unrelated `refmt` fix
Reviewed By: jvillard
Differential Revision: D4319731
fbshipit-source-id: 176dfcf
Summary:
In checkers we use "let" clause to define formulas abbreviation.
This diff expands the use of such formula id when used.
This allows to evaluate the formula.
For example.
let f = f_def
let g = g_def
let h = f or g
will expand the use of f and g with their definition.
Reviewed By: martinoluca
Differential Revision: D4299542
fbshipit-source-id: 9d37dd0
Summary:
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:
Make sl_file field strongly typed in the AST - store SourceFile.t instead of string. This will make it harder
to access raw string which shouldn't really be accessed before going through `SourceFile` module
Reviewed By: jvillard
Differential Revision: D4299468
fbshipit-source-id: e8ff87e
Summary: Globals that are constexpr-initializable do not participate in SIOF.
Reviewed By: sblackshear
Differential Revision: D4277216
fbshipit-source-id: fd601c8
Summary:
Functions related to source files were already namespaced by `source_file_` prefix. Make separate module for them.
In high level it replaces all `source_file_` with `SourceFile.` and then fixes all remaining compilation errors
Reviewed By: jvillard
Differential Revision: D4299053
fbshipit-source-id: 20b1d39
Summary:
Remember which globals are static locals.
It's useful to distinguish those from global variables in objc and in the SIOF
checker. Previously in ObjC we would accomplish that by looking at the name of
the variable, but that wouldn't work reliably in C++. Keep the old method around for
now as the way we deal with static locals in ObjC needs some fixing.
Reviewed By: akotulski
Differential Revision: D4198993
fbshipit-source-id: 357dd11
Summary:
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:
Implement heuristic to capture more of the user code:
In C++ there is a lot of interesting code in header files. On the other hand,
that code gets included in multiple places and we don't want to capture it by default (for performance reasons).
Right now we capture everything from source file + all symbols from headers that source file needs.
New heuristic will extend "capturing everything" to matching header files (ie. capture everything in X.h if source file is X.cpp)
Reviewed By: jberdine
Differential Revision: D4238008
fbshipit-source-id: 0528250
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:
This will help during the creation of new checkers, and will prevent errors like misspelling of AST node names.
It will also make it possible to fail immediately during the parsing of CTL inputs.
Reviewed By: ddino
Differential Revision: D4205434
fbshipit-source-id: ed8631a
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 will help during the creation of new checkers, and will prevent errors like misspelling of operators' kinds.
It will also make it possible to fail immediately during the parsing of CTL inputs.
Reviewed By: ddino
Differential Revision: D4212956
fbshipit-source-id: c3c7fe7
Summary:
SIOF is only for interactions between objects of non-POD types. Previously the
checker was also reporting for POD types.
Reviewed By: akotulski
Differential Revision: D4197620
fbshipit-source-id: 7c56571
Summary:
clang errors would get diverted to log files instead of being printed on the
console. Also log other types of clang errors and warnings more often.
Before:
$ infer -- clang -c nosuchfile.c
$ # nothing gets printed, exit code set to 1
After:
$ infer -- clang -c nosuchfile.c
clang-4.0: error: no such file or directory: 'nosuchfile.c'
Also print more messages in case of compilation errors:
$ echo ')' >> a.c
$ infer -- clang -c a.c
a.c:1:1: error: expected identifier or '('
)
^
1 error generated.
Error: the following clang command did not run successfully:
'/home/jul/infer/facebook-clang-plugins/clang/install/bin/clang-4.0' "@/home/jul/infer/examples/infer-out/clang/clang_command_2a0a84.txt"
(only the last 2 lines are new)
Reviewed By: akotulski
Differential Revision: D4183039
fbshipit-source-id: b9a9065
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: Speed up capture on MacOS by caching results of realpath. Improvements to lint speed on MacOS will be sent later
Reviewed By: jvillard
Differential Revision: D4166902
fbshipit-source-id: 4d065bc
Summary:
- set SHELL to bash explicitly in Makefiles (Debian uses dash)
- avoid using system headers when using our own clang's headers in tests
- do not rely on the name of the object file to write the frontend debugging scripts. It turns out that `-o` is *not* always present in the arguments of `-cc1` functions so the `Option.get` could crash. Since we don't actually need to get the object file name, just a nice enough name, don't try to be smarter at guessing what object will be created and pick a different name built from the source name instead.
Reviewed By: akotulski
Differential Revision: D4159516
fbshipit-source-id: c7bc2b9
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:
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: This fixes the build when `./configure --disable-c-analyzers` is used.
Reviewed By: jberdine
Differential Revision: D4146818
fbshipit-source-id: bec4b48
Summary:
Fix potential performance problems in `CLocation` module
1. Don't call `Unix.stat` to compare files if it's enough to compare paths
2. Use C implementation of `realpath` and call it only when it's really necessary
This diff breaks `Location.nLOC` information for whole clang frontend, but it's going away soon anyway
Reviewed By: jvillard, jberdine
Differential Revision: D4132526
fbshipit-source-id: f01afe8
Summary:
curr_file is remnant of the past when we didn't have good location information
coming from Clang_ast_t location. But it was fixed ~1 year ago.
Reviewed By: jvillard
Differential Revision: D4139750
fbshipit-source-id: 4ce7235
Summary: Don't ignore errors coming from clang when there are exceptions raised by the frontend
Reviewed By: jvillard
Differential Revision: D4117375
fbshipit-source-id: f31d6cf
Summary:
New version of clang plugin exports `-x` arg information as a part of
TranslationUnitDecl. Get it from there instead of reading it from
clang argv
Reviewed By: jvillard
Differential Revision: D4112652
fbshipit-source-id: 5c3af1f
Summary:
The build system may expect the assembly commands to run. The only issue with
assembly commands is that we shouldn't attach the plugin to them.
This diff also moves the logic of what to capture to the `Capture.capture`
function to be able to reuse code from Capture. This makes sense because the
Capture module is the one with the knowledge of what to actually capture or
not.
Reviewed By: akotulski
Differential Revision: D4096019
fbshipit-source-id: 7fc99e1
Summary: This is assumed everywhere, and so set it in `ClangWrapper` instead of `InferClang`
Reviewed By: jberdine
Differential Revision: D4095766
fbshipit-source-id: f77625e
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:
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:
InferClang knows what to do if its name ends in ++. So it is not
necessary to pass whether or not the original clang executable ended in
++ to InferClang using the the INFER_XX environment variable. Instead,
create an InferClang++ symbolic link and make the clang wrapper call
either InferClang or InferClang++ as needed.
Reviewed By: jvillard
Differential Revision: D4078416
fbshipit-source-id: 3b5d5d0
Summary: Now that InferClang is in ocaml there is nothing stopping us from exposing functionality of `InferClang` as a function in addition to binary
Reviewed By: jvillard
Differential Revision: D4081026
fbshipit-source-id: 86d500b
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: The frontend replaces global variables that are constant with their values as a quick hack to improve the precision of the analysis. This should apply to `constexpr` too.
Reviewed By: dulmarod
Differential Revision: D4058097
fbshipit-source-id: be4fea6
Summary:
Also be more careful when escaping arguments and create a module for shared
functionality between the clang frontend and the buck compilation database.
Reviewed By: jberdine
Differential Revision: D4036627
fbshipit-source-id: c981184
Summary:
Fix an issue where, when `-reactive` mode is used, files captured in the first second are not considered modified, and are not analyzed. This happens because file timestamps are used, and the resolution is one second.
Change the front-ends to change the timestamp of the directory where artifacts are created, so that the timestamps are 1 second in the future.
Small reactive commands such as the following now analyze correctly:
rm -rf infer-out && infer --reactive -- clang -c test.c
Reviewed By: jberdine
Differential Revision: D4050689
fbshipit-source-id: 6271860
Summary:
Move compilation database into separate module which loads said database from json file.
It will allow to load database from json file without calling buck.
Reviewed By: dulmarod
Differential Revision: D4049255
fbshipit-source-id: b2fa29f
Summary: This avoids issues where the command-line may get too large.
Reviewed By: jberdine
Differential Revision: D4008328
fbshipit-source-id: c1558b9
Summary:
This also adds `-a compile` support to `InferClang`. This is needed for the
`xcodebuild` integration, which is hard to fold into the same binary as the
rest.
Reviewed By: jberdine
Differential Revision: D4008262
fbshipit-source-id: 0bbd53f
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:
Create dummy functions representing the initializers of global variables. This
is so we can implement checks in the backend that can look at the initializer
expressions of global variables. We try not to create these dummy functions
when the initializer is not present, although for some reason we sometimes end
up with empty initializers.
Also add source file info to global variables in the backend (Pvar.re).
Reviewed By: sblackshear
Differential Revision: D3780238
fbshipit-source-id: 2dca87e
Summary:
During the development/debugging of AST checks, it will be possible to emit dotty graphs with a representation of the evaluation of formulas.
The formulas, expressed using the notation of CTL (https://en.wikipedia.org/wiki/Computation_tree_logic) are represented in a graph alongside the current ast-node and their final evaluation result (green for true, red for false)
To get the dotty graph, run infer with the `--debug` flag
Reviewed By: ddino
Differential Revision: D3937787
fbshipit-source-id: 163e17d
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: it seems to have no effect on analysis. As such it should be ok to add cg nodes for builtin model calls
Reviewed By: jberdine
Differential Revision: D3967399
fbshipit-source-id: 06c32e5
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: That data was never used and removing it can simplify frontends quite a bit.
Reviewed By: jberdine
Differential Revision: D3967389
fbshipit-source-id: d65c3da
Summary:
- Use the module types in cModule_types.ml instead of redefining them.
- A few occurrences of \n in formatted output replaced by @\n to let the
formatter know of line breaks (by no means complete, these were just a few I
came across while doing something else)
Reviewed By: jberdine
Differential Revision: D3944081
fbshipit-source-id: 4460427
Summary:
This diff introduces a first version of a front-end checkers specification
language. The language is based on the CTL temporal logic that is interpreted
on trees. In this case the model for a formula is the AST of the program produced
by clang.
This diff introduce the language and translate most of the existing checks on
this new language. In other diff I will translate all the other checks.
Then I will generalize the framework to allow the developer to specify only
the CTL formula.
Reviewed By: martinoluca
Differential Revision: D3819211
fbshipit-source-id: f8e01eb
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:
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:
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
Ryan Rhee
Jeremy Dubreil
Andrzej Kotulski
Dulma Churchill
Martino Luca
Dino Distefano
Jules Villard
Josh Berdine
Cristiano Calcagno
Sam Blackshear