Summary:
The purpose of DefinitelyNotNullable currently is bit unclear; let's
rename it so that the intention is obvious.
Reviewed By: artempyanykh
Differential Revision: D16984529
fbshipit-source-id: 696d58315
Summary:
`nullsafe` currently allows the following:
```
public void Nonnull Object willBeOK() { return null; }
```
But disallows the following:
```
public void Object willBeAnIssue() { return null; }
```
This was a deliberate choice made back in 2014.
The motivation was to provide a way to tell the checker "I know it can not be null, trust me".
A huge problem with that approach is that it is extremely non-intuitive and surprising, and contradicts with pretty much everything when Nonnull or similar annotations are used in external world.
This is not the way how checkers should be supressed.
We do provide 2 options to express this intention, namely `assertNotNull` and `assumeNotNull` would do the thing.
This is a much better approach for additional reason: assertNotNull is
granular and applies only to the exact expression that is under
question. In contrast, suppressing the check on the whole function level
make any modifications of a function dangerous.
Reviewed By: artempyanykh
Differential Revision: D16984213
fbshipit-source-id: 0ba0f623b
Summary:
This diff revises some models of Java String.
They had been implemented by C's string models such as models of
`strlen` or `strcat`, however, Java's String is different to C's,
rather is similar to C++'s String object.
Reviewed By: ezgicicek
Differential Revision: D17093136
fbshipit-source-id: b4f2cb4d0
Summary: Numeric attribute ranks are getting confused with addresses. Add an option (false by default) to MakePPUniqRankSet which prevents printing of the ranks.
Reviewed By: jvillard
Differential Revision: D17094269
fbshipit-source-id: 353c52fca
Summary:
`from_string` is too benign in constrast with what this method is really
doing (and oh my what it is really doing).
There are a lot of potential follow ups to clean this up even more, but
this is beyond the scope of this diff
Reviewed By: jvillard
Differential Revision: D17070826
fbshipit-source-id: 3d190039e
Summary:
`__inferbo_empty`, `__inferbo_min`, and `__inferbo_set_size` were in the
"include-based" cpp model.
Reviewed By: jvillard
Differential Revision: D17072034
fbshipit-source-id: dd840331f
Summary:
This diff uses the models of vector for modelling string in Cpp.
Depends on D16963153
Reviewed By: ezgicicek
Differential Revision: D16963166
fbshipit-source-id: 5effe2d72
Summary:
This is more powerful than `"symbols"` for more advanced use-cases. Keep
`"symbols"` unchanged to make migrating easier.
Differential Revision: D16985756
fbshipit-source-id: dfbb09393
Summary: Adding new predicate for checking whether a variable is defined as extern. May be useful in AL rules.
Reviewed By: jvillard
Differential Revision: D16961690
fbshipit-source-id: 0677077dc
Summary:
The clang frontend has bugs. When a bug we know about happens some
exception is raised and, most of the time, logged away so as not to
crash the whole process. This catching of exceptions wasn't done from
testDeterminator so it could crash where capture didn't. This diff wraps
the crashy function in test determinator to avoid that.
Reviewed By: ngorogiannis
Differential Revision: D16963178
fbshipit-source-id: 87a4ff70b
Summary:
This isn't really a "config" part of the frontend and this change is
needed later to catch these errors more robustly.
Reviewed By: ngorogiannis
Differential Revision: D16963177
fbshipit-source-id: 293b23acf
Summary: This diff prunes array sizes in Java by adding the size alias on the `get_array_length` function calls.
Reviewed By: ezgicicek
Differential Revision: D16983501
fbshipit-source-id: a924af09d
Summary:
Rename some AL source files so they mention AL explicitly instead of
"cFrontend" which could be confused with the clang frontend itself.
Reviewed By: ezgicicek
Differential Revision: D16962539
fbshipit-source-id: 29237cd1c
Summary: AL makes for close to a third of the source files in clang/. Put the code in its own folder for clarity.
Reviewed By: ezgicicek
Differential Revision: D16962438
fbshipit-source-id: 3373e69b9
Summary:
This diff avoids that an integer value is pruned to the bottom by
comparing to a pointer.
For example, before this diff,
assume((int*)x == p);
assume((int*)x != p);
where x is an integer, x is pruned to the bottom in both of the assume
cases. So, there were some, unintentional and false, unreachable
code.
Depends on D16960199
Reviewed By: ezgicicek
Differential Revision: D16964735
fbshipit-source-id: 90a3c8c80
Summary:
It changes the order of StdBasicString and StdVector for easier
reviewing of the following diff.
Reviewed By: ezgicicek
Differential Revision: D16963153
fbshipit-source-id: 50325e4e1
Summary:
The access path format forced some weird patterns on this code, simplify
using the access expression structure.
Reviewed By: ezgicicek
Differential Revision: D16960660
fbshipit-source-id: e8faf619e
Summary:
It prunes the size of collections when the size function is called in the condition expression. The diff extended the alias domain to understand temporary variables of SIL from Java.
Depends on D16761461
Reviewed By: ezgicicek
Differential Revision: D16761611
fbshipit-source-id: 849c5c71c
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: Ideally, we should be able to handle them like pruning if statements but for now, let's add the test.
Reviewed By: skcho
Differential Revision: D16938842
fbshipit-source-id: 04fae9559
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: Functions with empty body have unit cost, not zero. The unit cost comes from the start node.
Reviewed By: skcho
Differential Revision: D16855642
fbshipit-source-id: 6b5181faf
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
Mitya Lyubarskiy
Sungkeun Cho
Ezgi Çiçek
Jules Villard
Dulma Churchill
Nikos Gorogiannis
Phoebe Nichols
Martin Trojer