Summary:
This adds logging of the number of nodes in the reverse analysis call graph, and the number of these nodes that are invalidated by incremental analysis.
This data will show the precision of incremental analysis.
Reviewed By: ngorogiannis
Differential Revision: D16939101
fbshipit-source-id: 1e465f1a6
Summary:
It revises Java's cast model to keep type in the location when it has a field.
The type information is useful especially when generating ondemand values of Collection elements.
Depends on D16807299
Reviewed By: ezgicicek
Differential Revision: D16807378
fbshipit-source-id: 636e54429
Summary:
It doesn't make sense to use incremental analysis without specifying changed files. This is a possible source of future bugs.
This commit causes infer to die if incremental analysis is used without changed files.
---
Previously:
I think this code is currently a bit brittle because the CI shadow builds sometimes use `--incremental-analysis` because they are called with the same command as the diff analysis.
I am worried that in the future the shadow builds could be broken by this, although everything looks like it works right now. This diff would prevent breaking smoke builds in future because the shadow builds don't set changed-files (afaik).
However, possibly this is not the right place to fix the problem. It might be better to change the CI, I'm not sure.
Reviewed By: mityal
Differential Revision: D16829192
fbshipit-source-id: 5ee1ce9d0
Summary:
Use whatever information we can to decide whether to use C or Java
syntax when outputting an access expression, now that we store them as
such.
Also, make cluster callbacks explicitly set the language, as this was not done before and led to some confusion (Clang being set when analysing a Java file).
Reviewed By: skcho
Differential Revision: D16884160
fbshipit-source-id: 40adf9f35
Summary:
Access paths are too coarse to properly address C/C++ instructions, and lead to false positives and negatives. Begin the process of porting the underlying domains to access expressions, in a results-preserving way. This roughly consists in:
- Adding missing functions in `AccessExpression` to mirror those in `AccessPath`.
- Replacing `AccessExpression` for `AccessPath` and removing conversions from the former to the latter except in:
- Printing functions, to ensure formatting issues won't change tests/CI.
- Reporting/deduplication still happens through access path conversion, as we need an analogue of `ModuloThis` for `AccessExpression`.
- In selected places, ignore any access type not present in `AccessPath` (ie. dereference/take address of).
Reviewed By: jberdine
Differential Revision: D16856721
fbshipit-source-id: 5e3a88b75
Summary:
It uses inline record for Loc.Field
Depends on D16807279
Reviewed By: ezgicicek
Differential Revision: D16807299
fbshipit-source-id: 45eab34a4
Summary: Checker configs were defined as tuples which are amenable to problems with wrong ordering. Let's make convert them to a record type to prevent such issues.
Reviewed By: jvillard
Differential Revision: D16936737
fbshipit-source-id: 32aad6e97
Summary: Javalib is not happy about some class signature, let's try to silence it temporarily.
Reviewed By: ngorogiannis
Differential Revision: D16917273
fbshipit-source-id: 39ce4adee
Summary:
Change the logic of the annotation reachability checker in the following
ways:
1. Sanitizers take priority over sinks, i.e. a procedure that is both a
sink and a sanitizer is not a sink. This changes the existing tests
that seemed to assume the opposite. However I think that way is more
useful and goes better with the fact that sanitizers are specified as
"overrides".
2. When applying a summary, check again that we are not in a sanitizer
for the corresponding sink.
Without (2) this there was a subtle bug when several rules were
specified. For example, if `sink_wrapper()` wraps `sink()` for a rule
`R` then the summary of `sink_wrapper()` will be: `R-sink : call to sink()`.
Then, suppose `sanitizer()` calls `sink_wrapper()` and `sanitizer()` is
a sanitizer for `R` but not for another rule `R'`. The previous code
would add the call to `sink()` to the summary of `sanitizer()` because
it's not a sanitizer for `R'`, even though `sink()` is not a sink for
`R'`!
The current code will re-apply the rules correctly so that sinks are
matched only against the right sanitizers.
Reviewed By: skcho
Differential Revision: D16895577
fbshipit-source-id: 266cc4940
Summary:
- run the tests! they weren't hooked up to the main Makefile :/
- add some html debug messages
- formatting
Reviewed By: skcho
Differential Revision: D16895578
fbshipit-source-id: e96d737cc
Summary:
I added this logging in D16730426, to try and debug incremental analysis.
I don't need the logging anymore, so I'm taking it out. I don't this it's very useful for users.
Reviewed By: ezgicicek
Differential Revision: D16904498
fbshipit-source-id: 88b0f1cb5
Summary:
Since it is non-sense to get ranges of boolean values, this diff
ignores control values that only contain boolean symbols.
Depends on D16804802
Reviewed By: ezgicicek
Differential Revision: D16804808
fbshipit-source-id: ccb25db4d
Summary: The pattern "check if an access has already been reported, otherwise see if it is a violation, report it, then add it to the set of reported accesses" is too much copy pasta. Push that into the reporting functions.
Reviewed By: ezgicicek
Differential Revision: D16859208
fbshipit-source-id: 5370efd41
Summary: I'm not entirely sure why this function was written in such a horrendous way :)
Reviewed By: skcho
Differential Revision: D16858396
fbshipit-source-id: d998e17f3
Summary:
Before this diff it returned `[0,size-1]`, but which became bottom
when size was given by 0. As a result, it made the both branches of
`if(iterator.hasNext())` unreachable. Similarly, if the size was 1,
it only visited the false branch of the if condition because the
condition value was `[0,0]` at that time.
This diff changes it to return `[0,size]`, so that
* the false branch is reachable when the size is 0
* the both branches are reachable when the size is 1
Reviewed By: ezgicicek
Differential Revision: D16803000
fbshipit-source-id: f8772be27
Summary: We want to keep big O notation as simple as possible in cost analysis reports (especially in diff time). Therefore, let's not show constants/min/max in big O notations even though the resulting asymptotic bound might be inaccurate. Developers can click on the trace and see the actual cost.
Reviewed By: skcho
Differential Revision: D16731351
fbshipit-source-id: 2e16f7eca
Summary: In order to test changes to bigO notation, let's record them in test results.
Reviewed By: skcho
Differential Revision: D16763972
fbshipit-source-id: c1376909b
Summary:
It renames a function to make it clear what it does.
Depends on D16761451
Reviewed By: ezgicicek
Differential Revision: D16761461
fbshipit-source-id: b989cc274
Summary: We do not need to keep the elements type of vector in the field.
Reviewed By: ezgicicek
Differential Revision: D16761451
fbshipit-source-id: 6d5384662
Summary: Add a sanity check that looks up the `INFERVERSION` environment variable and, if set, checks that the current binary matches that version.
Reviewed By: skcho
Differential Revision: D16761575
fbshipit-source-id: 9d5c32220
Summary:
Incremental analysis isn't behaving as expected in production, and I think the deletion and re-creation of the results directory is why
Adding logging to test this theory
Reviewed By: ngorogiannis
Differential Revision: D16730426
fbshipit-source-id: 0a670cabf
Summary:
Correct the models of ArrayList initialization. Basically, there are two ways to initialize:
- by setting an initial capacity, which creates an empty list
- by passing another collection as an argument
Before, we had only modeled the second case which was resulting in wrong memory model for the first case. This diff fixes that.
Reviewed By: skcho
Differential Revision: D16711055
fbshipit-source-id: e82faf191
Summary: Remove duplicate `s` when printing the time taken by the analysis
Reviewed By: ngorogiannis
Differential Revision: D16710277
fbshipit-source-id: 3ba7f6693
Summary:
It adds a vector model of `data` method.
Depends on D16687280
Reviewed By: ezgicicek
Differential Revision: D16689400
fbshipit-source-id: 156016b3c
Summary:
It adds a model of vector::push_back
Depends on D16687225
Reviewed By: ezgicicek
Differential Revision: D16687269
fbshipit-source-id: 9d2a73fca
Summary:
It enables pruning of vector's size when the return value of the function call of `vector::size` is pruned.
Depends on D16687167
Reviewed By: ezgicicek
Differential Revision: D16687225
fbshipit-source-id: 793a21b3a
Summary:
Add logging for the number of procedures whose summaries are invalidated by incremental analysis
This will help verify that incremental analysis is working as expected in production
Reviewed By: ngorogiannis
Differential Revision: D16686911
fbshipit-source-id: 53c89c3bb
Summary:
It generates vector value ondemand when it is given as a parameter.
Depends on D16645589
Reviewed By: ezgicicek
Differential Revision: D16645624
fbshipit-source-id: 7498c8ab2
Summary:
This diff makes it sure that Inferbo does nothing on relational domain
at function calls when the command line option for them is not given.
Reviewed By: ezgicicek
Differential Revision: D16647903
fbshipit-source-id: 74ef251fe
Summary:
The models are only for biabduction so try to make that clearer in the
code and documentation.
Reviewed By: skcho
Differential Revision: D16603147
fbshipit-source-id: 4a2be53de
Summary:
It's not being worked on and is not in a state where it works.
It would probably better to write this as a script of some kind or else
resurrect this subcommand in a form where it behaves more like a script,
ie fork/execs infer analyses instead of having them be function calls
(but then it might as well *be* a script as it would likely be more
flexible).
In any case...
youarealreadydead
Reviewed By: ezgicicek
Differential Revision: D16602417
fbshipit-source-id: d0d129539
Summary:
These have proved to be too fragile to maintain as they would often break
compilation of user code. They have been off by default for more than a year
now (D7350715).
Removing the include models shows a more accurate picture of what infer results
look like in production. As such, lots of tests have changed, mostly
biabduction but also in inferbo. SIOF was using include-based models too but
now libc++ is better and iostreams are implemented in a way that SIOF
understands (instead of being magical creatures) so nothing changed there.
Reviewed By: skcho
Differential Revision: D16602171
fbshipit-source-id: ce38f045b
Summary: Models of Java's Collection mistakenly assumed that there was an argument for empty set whereas `Collections.emptySet()` doesn't have any actuals. This diff fixes that an also removes the type argument from the corresponding model definition.
Reviewed By: skcho
Differential Revision: D16582314
fbshipit-source-id: d4304dc60
Summary: Sometimes programmers use integer underflow to get a maximum number of that type. This diff assumes that integer underflows from the syntactical form `(unsigned 0) - constant` is intended by the programmer, and suppresses the alarms of which.
Reviewed By: ezgicicek
Differential Revision: D16560639
fbshipit-source-id: 206f30dbc
Summary:
Count the following:
- how many procedures were *actually* analyzed (i.e. some checkers ran
on them)
- how many times an analysis result was retrieved from the local cache
and how many times it was missed
Reviewed By: skcho
Differential Revision: D16561867
fbshipit-source-id: 8c43ce13c
Summary:
Instead of `let incr_foo () = global_stats.foo <- global_stats.foo + 1` where you have to
check that you copy/pasted the right stuff and substituted `foo`
everywhere, write `let incr_foo () = incr Fiels.summary_foo` where
there's less room for errors.
Reviewed By: artempyanykh
Differential Revision: D16561868
fbshipit-source-id: 77ea09bef
Summary:
Before this diff, it gave up pruning of linear bound by minmax bound.
For example, `overapprox_min (x+c1, c2+min(d1,y))` was `x+c1`.
However, we can get a bit more preciser value as follows.
```
overapprox_min (x+c1, c2+min(d1,y))
<= min (x+c1, c2+d1)
= c1+min(c2+d1-c1, x)
```
Reviewed By: ezgicicek
Differential Revision: D16543837
fbshipit-source-id: 8fdbce097
Summary:
- make most behaviours independent of the java version so that either works fine without user intervention
- modify regexp used to parse `javac` output to work for all versions
- no need to be sure we are in Java 11 to match java 11-only method name in quandary
- for the rest, provide a command-line flag to specify the java version manually in case it differs from the version that infer was built against
- this only affects the Maven integration for now
To do all that, also change the configure script to record the version of java instead of just a boolean for whether it's >= 10.
Reviewed By: ezgicicek
Differential Revision: D16493988
fbshipit-source-id: 622e91b25
Phoebe Nichols
Sungkeun Cho
Nikos Gorogiannis
Ezgi Çiçek
Jules Villard
Martin Trojer