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
Ryan Rhee
Dulma Churchill
Andrzej Kotulski
Jules Villard
Cristiano Calcagno
Sam Blackshear
Dino Distefano
Josh Berdine
Martino Luca