Summary:
This diff refactors Sil.Int, which represents integer literals, into a
separate module IntLit. There are no dependencies forcing Sil.Int to
be a submodule of Sil, and it is also no simpler as a submodule.
Reviewed By: cristianoc
Differential Revision: D3422910
fbshipit-source-id: 63013f2
Summary:
Change int_compare to avoid overflow, without generating a call to a C
function or any branch instructions.
Reviewed By: cristianoc
Differential Revision: D3417671
fbshipit-source-id: e4c5d7b
Summary:
Reuse data fields of model's superclass (which is actual implementation).
Not very pretty, but makes sizeof shared_ptr same as in actual libraries
Reviewed By: jvillard
Differential Revision: D3398628
fbshipit-source-id: bdb9418
Summary:
Array types where the length is not statically known were represented
using fresh variables. This diff:
- Makes array type length optional, reducing the amount of work needed
for renaming, substitution, and normalization.
- Revises uses of array length so that the length component of a
Tarray type represents only the statically determined constant
length of an array type, and the length component of a Sizeof
expression represents the dynamically determined length of an array
value.
- Restricts the type of static lengths from a general expression
(Sil.exp) to an integer (Sil.Int.t), enforcing that static types are
constant. This in particular ensures that types contain no
variables, and so are invariant under operations such as renaming
and substitution.
- Removes the type substitution and renaming functions typ_sub,
typ_normalize, and typ_captured_ren. Now that array type lengths
are constant integers, all of these functions are the identity.
Reviewed By: cristianoc
Differential Revision: D3387343
fbshipit-source-id: b5db768
Summary:
The extra dereference in stmtexpr was wrong. When a dereference is needed, we have a cast.
This was causing one dereference too many, and creating wrong results.
Reviewed By: akotulski
Differential Revision: D3393294
fbshipit-source-id: 7a1ec8e
Summary:
Use the output of `clang -###` to drive which commands to run. Attach the plugin to all commands starting with `-cc1`.
Benefits:
- support for compiling multiple files in one clang command, eg `infer -- clang -c file1.c file2.c`
- support for compile commands that do not target a `.o` file, eg `infer -- clang -S hello.c`
- support for `-cc1` compile commands
- more generally, run all commands that clang would run, and attach plugin in all compilation cases
Reviewed By: martinoluca
Differential Revision: D3366912
fbshipit-source-id: 98d5e3b
Summary:
buck #infer flavor doesn't rely on .o files so we don't need to generate them.
It will save memory/IO and possibly time
Reviewed By: jvillard, martinoluca
Differential Revision: D3379463
fbshipit-source-id: 1d48f7a
Summary:
This diff extends Sizeof expressions with an optional expression for the
length of the final extensible array, if any. For example, sizeof a
simple array `sizeof(t[n])` is represented by (modulo subtyping info)
`Sizeof t (Some n)`, and sizeof a struct whose final member is an array
`sizeof(struct s {... t[n] f})` is represented by `Sizeof (struct s
{... t[n] f}) (Some n)`.
This is an intermediate step toward eliminating expressions from types,
the redundancy between the length in the types and in the sizeof
expressions will be eliminated later.
Reviewed By: cristianoc
Differential Revision: D3358763
fbshipit-source-id: 2239bca
Summary:
This removes some boilerplate and duplicated code and makes it easier to add
more tests.
Reviewed By: martinoluca, jeremydubreil
Differential Revision: D3365807
fbshipit-source-id: 9a2e0e5
Summary:
Run `InferStatsAggregator` at the end of the execution of `infer` top-level, and store
results on `infer-out/(frontend|backend|reporting)_stats/aggregated_stats.json`
Not ready yet for buck targets analyzed without the use of an `#infer*` flavor.
Reviewed By: jvillard
Differential Revision: D3365504
fbshipit-source-id: 98b2eb3
Summary: It is preferable to always create error reports as a proof of succesful termination, even when the Buck target contains no source file to analyze
Reviewed By: sblackshear, jvillard
Differential Revision: D3362581
fbshipit-source-id: 4f27666
Summary:
Specs files can become stale and cause crashes if the serialized format
changes. It is unclear how to add the right dependencies to the
existing targets, so this patch just removes them. Perhaps when the
specs are built we should drop an empty file to time-stamp them, and add
a target that depends on e.g. InferAnalyze and produces that file, and
then add dependencies on it.
Reviewed By: jvillard
Differential Revision: D3358460
fbshipit-source-id: d8aee48
Summary:
Hardcoding `variable@` in Makefiles is Bad™ because it prevents the users from
overwriting them easily with `make variable="my custom value"`. The right way
to do it is thus:
```
variable = variable@
# then use $(variable) everywhere
```
This diff puts all the `variable = variable@` lines in Makefile.config.in, and
changes every occurrence of a `variable@` to `$(variable)` everywhere else.
I mostly automated generating this diff. Here are the steps I did:
- find out which `variable@`s we use:
find . -name 'Makefile*' -exec grep -e '@[^@ []\+@' -o -h \{\} \+ | sort | uniq > config_variables
- write this `replace.sh` script to replace every `variable@` with `$(variable)`:
```
#!/bin/sh
config_vars_file=$1
shift
for line in $(cat $config_vars_file); do
var=$(echo $line | tr -d @)
sed -i -e "s/$line/\$($var)/g" $@ > /dev/null
done
```
- run the script as such:
find . -name 'Makefile.*in' \( -not -wholename './Makefile.config.in' \) -exec ./replace.sh config_variables \{\} \+
- put all the `VARIABLE = VARIABLE@` lines in Makefile.config.in
- move all `Makefile.in` to `Makefile`, since they don't need to be generated by `./configure` anymore:
```
for i in $(find . -name 'Makefile.*in' \( -not -wholename './Makefile.config.in' \)); do \
rm $(dirname $i)/$(basename $i .in) && git mv $i $(dirname $i)/$(basename $i .in) ; \
done
```
- delete all Makefile except Makefile.config from configure.ac
- manually inspect and remove remaining instances of `VAR = $(VAR)` in makefiles, looking at the output of `git grep '^\(\w\+\) = $(\1)'`
Reviewed By: jberdine
Differential Revision: D3358379
fbshipit-source-id: 5d37f02
Summary:
Now all code in tests is reachable by the analyzer which increases
test quality.
Reviewed By: dulmarod
Differential Revision: D3358591
fbshipit-source-id: d54877e
Summary:
Recent changes in the makefile seem to have made this dependency disappear and
now nothing builds it!
Reviewed By: akotulski
Differential Revision: D3352670
fbshipit-source-id: 8657e89
Summary:
When syntax highlighting the source excerpts that Infer prints on stdout, we
would crash if `pygments.lexers` did not find a suitable class given the name
of the source file. Instead, do not colorize when that's the case.
Reviewed By: martinoluca
Differential Revision: D3358115
fbshipit-source-id: ccb9b41
Summary:
This change introduces a new binary, called `InferStatsAggregator`, that once invoked, aggregates
together all the stats generated by the single invocations of frontend/backend/reporting, that can
be used for performance measurements.
Reviewed By: jvillard
Differential Revision: D3317000
fbshipit-source-id: 61ec615
Summary:
We stopped including the directories for java/clang/llvm with the change in the
makefile. `ocamlbuild` seems to be mostly happy still.
Reviewed By: jberdine
Differential Revision: D3352703
fbshipit-source-id: 5b4e763
Summary:
Pass object by reference every time struct object is passed by value
in C++. Do it only for C++/objC++ where we have guarantee that the
object which is passed will be temporary one (created by copy constructor).
Reviewed By: jberdine
Differential Revision: D3346271
fbshipit-source-id: d3e5daa
Summary: I missed that codepath and it lead to NULL_DEREFERENCE errors when in fact they should be EMPTY_VECTOR_ACCESS
Reviewed By: jvillard
Differential Revision: D3340627
fbshipit-source-id: 52ae85f
Summary:
Make analyzer find out when null dereference comes from std::vector method.
If it does, it means that it's really empty vector access (due to the
way infer models std::vector)
Reviewed By: sblackshear
Differential Revision: D3327933
fbshipit-source-id: b9e11d6
Summary:
Optimize retries in deserialization by opening the file only once
instead of once per retry. Also ensure that the file is closed on
failure. This reduces memory leaked for unclosed channels.
Reviewed By: jvillard, cristianoc
Differential Revision: D3321132
fbshipit-source-id: 05e6ff0
Summary:
Turns out, analyzer was getting confused with complicated
model and it was reporting empty access in places it
shouldn't. Fixing backend is not trivial (tracing mode is the answer),
but the model can be simplified.
It introduces the problem that get() method doesn't return fresh value
every time, but we should be able to change backend later to deal with it.
Reviewed By: sblackshear
Differential Revision: D3328228
fbshipit-source-id: dddbaf8
Summary: Fix apparent bug in sym_eval, where struct fields could be reversed.
Reviewed By: cristianoc
Differential Revision: D3333035
fbshipit-source-id: 4ccc859
Summary:
The typ_iter_types, exp_iter_types, and instr_iter_types functions of
Sil are unused.
Reviewed By: cristianoc
Differential Revision: D3332878
fbshipit-source-id: e8d8f71
Summary:
Optimize attribute loading by caching all attributes read from file in
memory. This reduces io and allocation rate and raises memory usage.
Reviewed By: cristianoc
Differential Revision: D3321156
fbshipit-source-id: 37bc6bc
Summary:
End of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
Reviewed By: jberdine
Differential Revision: D3304798
fbshipit-source-id: 14f6833
Summary:
Part of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
This changes the behaviour of Infer in that we now create matchers eagerly
instead of lazily. I think it's ok because I suspect what's really important is
not laziness but memoisation, and thus laziness was just an implementation
detail. If I'm wrong please yell, it should be easy to revert to a lazy
behaviour if really needed.
Reviewed By: jberdine
Differential Revision: D3304792
fbshipit-source-id: 1ddde6d
Summary:
Part of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
Reviewed By: jberdine
Differential Revision: D3304785
fbshipit-source-id: e0204e9
Summary:
Part of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
Reviewed By: jberdine
Differential Revision: D3322508
fbshipit-source-id: 1820a9d
Summary:
Part of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
Reviewed By: jberdine
Differential Revision: D3304784
fbshipit-source-id: 0c39b39
Summary:
- `test_build` now also test that the OSS build works if we're inside the internal repo
- remove some "if java/clang" in the test targets, since tests work under the
assumption that all the analyzers are to be tested.
Reviewed By: jberdine
Differential Revision: D3305088
fbshipit-source-id: 142fc49
Summary: This is basically not used and removing it makes the Makefiles slightly less convoluted.
Reviewed By: jberdine
Differential Revision: D3322376
fbshipit-source-id: 2d7c1f8
Summary:
`make clean all test` worked, but not `make clean test` because `test` only
builds stuff in infer/src/ (no models, no infer/bin/infer). For now, fix the
workflow by building both `infer` and `test_build` in different directories (so
they can be parallelized).
Reviewed By: jberdine
Differential Revision: D3322797
fbshipit-source-id: 71d146d
Summary:
Part of the migration of .inferconfig-specific options into options accepted
both by .inferconfig and the CLI.
Reviewed By: jberdine
Differential Revision: D3304783
fbshipit-source-id: 4a7ee6f
Summary:
Any option accepted by infer/InferAnalyze/... can now appear in
.inferconfig and will be interpreted accordingly. Options in .inferconfig
are overriden by both env vars parameters and command line
arguments.
To achieve this, we do a first round of parsing that only acts on the
flags necessary to find out where .inferconfig lives. Then we serialise
the contents of the json file into the format expected by command-line
arguments, and use a trick similar to the way we handle env variables to
interpret the json arguments.
Reviewed By: jberdine
Differential Revision: D3298379
fbshipit-source-id: 12b7d57
Summary:
Build everything at once all the time. This removes the need for multiple
directories, which were a hassle to begin with.
This removes the `java`, `clang`, and `llvm` targets in various Makefiles as
well.
Reviewed By: jberdine
Differential Revision: D3317230
fbshipit-source-id: 8e86140
Summary:
Now we can add to inferconfig an option
skip-translation-file to skip completely the translation
and analysis of some file.
Reviewed By: jberdine
Differential Revision: D3311129
fbshipit-source-id: 58fd179
Summary:
Add a Makefile to convert files to reason, to help with rebasing over
the conversion.
Reviewed By: jvillard
Differential Revision: D3316674
fbshipit-source-id: 8abcbe0
Summary: This way we don't need to make the file be valid json later on.
Reviewed By: jeremydubreil
Differential Revision: D3304998
fbshipit-source-id: 25deb5c
Summary:
If we see a read of a field f annotated with GuardedBy("mLock"), we spring into action.
What we do is look for some hpred `A.mLock |-> B` and return `B` as the "guarded-by object".
Once we have models for montitorenter/exit in place, `B.__inferIsLocked = true` will mean "lock held", and `B.__inferIsLocked = false` will mean "lock not held".
Reviewed By: jvillard
Differential Revision: D3316288
fbshipit-source-id: 8625e04
Josh Berdine
Sam Blackshear
Andrzej Kotulski
Peter O'Hearn
Daiva Naudziuniene
Dulma Churchill
Cristiano Calcagno
Jules Villard
Jeremy Dubreil
Martino Luca
Dino Distefano