Summary:
There are currently plenty of ways to suppress the warning, including Inject, Initializer, and SuppressFieldNotInitialized annotations.
This one (annotating field with Nonnull) is counter-intuitive and does not align with gradual nullsafe
semantics we are working on.
Reviewed By: artempyanykh
Differential Revision: D17281702
fbshipit-source-id: 132e1b687
Summary:
This diff ignores character symbols in the cost results, in order to
avoid FPs from parser code.
Reviewed By: ezgicicek
Differential Revision: D17132053
fbshipit-source-id: d9cf8bd26
Summary: let's always have positive and negative case for each feature we test
Reviewed By: ngorogiannis
Differential Revision: D17206785
fbshipit-source-id: 5791ace48
Summary:
1. Let's move it to the file dedicated to this particular warning.
2. Make it more general (Activity was just a particular case) and describe in comments what it really does.
Reviewed By: ngorogiannis
Differential Revision: D17205919
fbshipit-source-id: 82bf5e9bd
Summary:
1. Remove boilerplate with builder that uses builder initializer; it
demostates a usecase but it is not really relevant for the test so it
distracts attention.
Instead, describe the usecase in the comment
2. Add good and bad cases so it is obvious what exactly do we test.
Reviewed By: artempyanykh
Differential Revision: D17204969
fbshipit-source-id: 005ea078b
Summary:
Let's combine with the one that tests a very similar thing for known
cleanup methods
Reviewed By: ngorogiannis
Differential Revision: D17204206
fbshipit-source-id: dbdbde903
Summary:
1. Remove manipulations with "shadowed" fields and abstract class, I don't believe they produced high quality signal (and no related warnings in the test output).
2. For each failure case provide corresponding success case and the
reverse
Reviewed By: artempyanykh
Differential Revision: D17203240
fbshipit-source-id: c809857ed
Summary:
1. Let's make the intention of the test more visible, also let's provide an example
when the error does occur.
2. `onDestroy` silence "field not nullable" warnigs not only for `View`, but for any objects, so let's use `String` (as an example of a trivial object) instead.
Original diff that introduced the test: D10024458
Reviewed By: artempyanykh
Differential Revision: D17202839
fbshipit-source-id: 037d937e4
Summary: This diff adds models of Java String. In order to keep the precision of cost checker, I fixed cost models for String in this diff too.
Reviewed By: ngorogiannis
Differential Revision: D17203309
fbshipit-source-id: 8cc2814fc
Summary:
This diff makes the checkers, except biabduction, to use `typ` instead
of `root_typ` of `Load`/`Store` statemetns.
Reviewed By: dulmarod
Differential Revision: D17203105
fbshipit-source-id: 8be9b5158
Summary:
It adds typ field in Sil.Store. The field will be used by the analyzer in the following diffs.
Motivation: Interbo generates a symbolic value when evaluating expressions including parameter symbols. At that time, it is done with depending on their types, e.g., an integer, a pointer to struct or a pointer to array. Without the type, it is hard to generate a correct symbolic value that will be instantiated later in call sites. Thus, evaluating RHS of the store statement, the type of RHS is better to be given.
Reviewed By: dulmarod
Differential Revision: D17185346
fbshipit-source-id: f0945c40f
Summary: This shows that the current Pulse analyzer works fine in the C++ part of the Objc++ files.
Reviewed By: martintrojer
Differential Revision: D17225683
fbshipit-source-id: faf51c5fa
Summary: Use_after_free was used both for biabduction and pulse, and the biabduction version is blacklisted by default. As a result, the Pulse version was also disabled unintentionally. This changes the name of the old use_after_free so that now we can get use_after_free bugs whenever pulse is enabled.
Reviewed By: skcho
Differential Revision: D17182687
fbshipit-source-id: 539ca69de
Summary:
In integrations where the capturing process isn't forked off the main Infer process, but launched, eg, via a script pretending to be a compiler, the reference indicating whether the server is running will always be false, and thus such integrations will never try to connect to the write daemon.
Fix this by
- making `sqlite-write-daemon` authoritative wrt connecting to the daemon.
- launching the daemon earlier in the setup process.
Reviewed By: jberdine
Differential Revision: D17204002
fbshipit-source-id: 23d452fac
Summary:
See motivation below.
This diff is dealing with FieldNotNullable:
- move not relevant subclasses into dedicated classes and files
- modify the tests so they comply with the standards below
--Motivation--
Gradual mode we are going to introduce is an invasive change in how Infer
treats nullability semantics.
In order to make the change in a controllable way, we need the tests to comply with the
following standards and conventions.
1. For each code peace where we expect a bug to happen, the there should be
corresponding (minimally different from above) peace of code where we expect a bug to NOT happen. (This is to ensure bug is happening for exact reason we think it is happening).
2. Conversely: for each peace of code where we expect a bug to be NOT
present, there shuold be a peace of code where the bug IS happening.
(Otherwise there can be too many reasons for a bug NOT to happen).
3. Convention: end corresponding methods IsOK and IsBUG correspondingly.
4. Keep code examples as small as possible.
Reviewed By: ngorogiannis
Differential Revision: D17183222
fbshipit-source-id: 83d03e67f
Summary:
It adds `typ` field in Sil.Load. The field will be used by the analyzer in the following diffs.
Motivation: Interbo generates a symbolic value when evaluating expressions including parameter symbols. At that time, it is done with depending on their types, e.g., an integer, a pointer to struct or a pointer to array. Without the type, it is hard to generate a correct symbolic value that will be instantiated later in call sites. Thus, evaluating RHS of the load statement, the type of RHS is better to be given.
Reviewed By: jvillard
Differential Revision: D17163350
fbshipit-source-id: f7f0f1429
Summary:
It uses inline record for Sil.Load and Sil.Store for preparing the
following extention.
Reviewed By: dulmarod
Differential Revision: D17161288
fbshipit-source-id: 637ea7bfa
Summary: It prints non-verbose program variables in the report.
Reviewed By: ngorogiannis
Differential Revision: D17163943
fbshipit-source-id: c3f3c2887
Summary:
An exception thrown during capture/analysis may leave the daemon
running. Kill it even when one is thrown.
Reviewed By: martintrojer
Differential Revision: D17181090
fbshipit-source-id: a7b002f23
Summary: With this predicate we are able to check for static global variables in AL.
Reviewed By: ddino
Differential Revision: D17164848
fbshipit-source-id: a3d10598c
Summary:
We currently use storage_class only for checking is_static, adding the flag instead in the plugin to improve perf by avoiding string comparisons.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D17156173
fbshipit-source-id: 2b84a0b84
Summary:
In next diff, we are going to introduce a new mode of nullsafe
(gradual). For testing, we are going to employ the strategy used by jvillard
for Pulse.
In this diff we split tests into two subfolders, one for the default and one for the gradual
mode.
We are planning to make the gradual mode default eventually. For that, most
new features will make sense for gradual mode, and we will mostly evolve
tests for that mode.
As for 'default' mode, we need to preserve tests mostly to ensure we don't introduce
regressions.
Occasionally, we might make changes that make sense for both modes, in
this (expected relatively rare) cases we will make changes to both set
of tests.
An alternative strategy would be to have two sets of issues.exp files,
one for gradual and one for default mode. This has an advantage of each
java file to be always tested twice, but disadvantage is that it will be
harder to write meaningful test code so that it makes sense for both
modes simultaneously.
Reviewed By: ngorogiannis
Differential Revision: D17156724
fbshipit-source-id: a92a9208f
Summary:
This abstraction was not always used consistently.
Its usage made more sense when it supported both present annotations and
optional annotation (which got removed in previous diff).
The rought semantic of that was "what is the inferred type for such and
such value (variable or expression) in typestate". So it is not really
_annotation_ in first place, it is more like "what we inferred about
nullability given annotations, known special cases, and current sybmolic
execition state".
Let's explicitly rename `map` to `is_nullable`. If/when we need to
enhance this further (and we likely will), we will do it accordingly.
Reviewed By: jvillard
Differential Revision: D17153434
fbshipit-source-id: 3c85b56df
Summary:
`Present` annotation was an experiment made many years ago that never
got into real usage. The idea was to annotate Optional<> types with
Present, which means that it is safe to call get().
We don't plan to support `Present` annotation for optional types in the
near future.
Support of `Present` annotation requires extra levels of abstraction
that make the changing the behavior and introducing new features harder.
A lot of checks for nullability are written in generic way so they also
check for presense.
Getting rid of that will allow us to simplify our
work for introducing new semantics for nullsafe.
Reviewed By: ngorogiannis
Differential Revision: D17153432
fbshipit-source-id: c5ea9bdf1
Summary:
Implementation of write-serializer for Sqlite. Points of note:
- A Unix socket is used for communication. This avoids buffer-size limitations, as the objects we send for writing may exceed said limits.
- No daemon is used if running under buck or in genrule mode, as this usually means a single-threaded job capturing into the DB.
- When the daemon is running, read-only access is *not* enforced for other processes. This makes starting and stopping the daemon during Infer execution easier and more robust. In WAL mode this should not have any effect on performance.
- This version is not economical with connections, it uses one per query, todo.
Reviewed By: jvillard
Differential Revision: D17077183
fbshipit-source-id: fa9877d6c
Summary: Developing the Sqlite-writer process further, a type `command` is introduced, which will used for sending instructions down a communications channel to the daemon. For now, the commands are interpreted locally.
Reviewed By: skcho
Differential Revision: D16985056
fbshipit-source-id: 2aa20908d
Summary:
Write contention is becoming a problem in parallel capture (eg when make runs with high parallelism) or when analysis writes CFGs to the DB in parallel (eg when analysing blocks in ObC). This is believed to lead to BUSY errors in Sqlite.
This is step 1 of a process where all writes are cordoned-off in one module, and fixing the interface for that module.
Reviewed By: skcho
Differential Revision: D16985034
fbshipit-source-id: 3d7ce381b
Summary:
When running with high parallelism and a large number of insertions in the DB (eg, ObjC analysis with block specialisation), we see MISUSE exceptions thrown by Sqlite **when trying to bind parameters to queries**. It does not always occur, and maybe that's because the check in Sqlite that throws this error is documented as "probabilistic". For the same reason, it is plausible that high parallelism increases the chance of detection.
According to documentation this unequivocally means a bug in our usage of the API (https://www.sqlite.org/rescode.html#misuse), in particular that a parameter is re-bound while the query is running (https://www2.sqlite.org/cvstrac/wiki?p=LibraryRoutineCalledOutOfSequence). I believe this may have to do with `result_fold_rows` (as it's the only one that uses a query that can be continued, and thus misused), but I have not managed to track the bug.
Always resetting the query before using it is a defensive measure that seems to make these errors go away (and turn some of them to BUSY timeouts, which should be addressed by a write serialiser, but in any case it's a more logical state of affairs = higher parallelism means more contention thus possibly timeouts due to lock usage).
Reviewed By: jvillard
Differential Revision: D17147447
fbshipit-source-id: 7ef3cc73f
Summary:
Since it does not make sense to get ranges of non-integer values and
use them as approximate iteration numbers, this diff ignores control
values that only contain non-integer symbols.
Reviewed By: ezgicicek
Differential Revision: D17130967
fbshipit-source-id: f5ba58d52
Summary: This tests the previous commit D17093980, which moves incremental analysis to run before capture
Reviewed By: ngorogiannis
Differential Revision: D17113475
fbshipit-source-id: 702d967b3
Summary:
Currently, the specs directory is cleaned after running capture. This means that the `changed-files` are interpreted in the context of the second set of source files. Therefore if a procedure is deleted from the second set of source files, its specs file will not be deleted.
This moves the cleaning of the specs directory to before capture, to avoid this problem.
Reviewed By: ngorogiannis
Differential Revision: D17093980
fbshipit-source-id: e1a8d8a54
Summary: This diff extends size alias domain for keeping one more alias of a Java temporary variable.
Reviewed By: ezgicicek
Differential Revision: D16984082
fbshipit-source-id: 244bbd0ee
Summary: This diff ignores boundends when getting the value range.
Reviewed By: ezgicicek
Differential Revision: D17114363
fbshipit-source-id: cca8745e3
Summary: Like we removed empty edges from the `pre_heap` in D16419183, let's do the same to `post_heap`.
Reviewed By: skcho
Differential Revision: D17111336
fbshipit-source-id: c35fcbabb
Summary:
Before this diff we would record when some values came from the "address
of" logical variables. This makes no sense and also was incorrectly
marking these addresses as "written to" when they appeared in the post
of a procedure, because their attributes weren't empty (they had the
"address of stack variable" attribute).
Reviewed By: ngorogiannis
Differential Revision: D17131210
fbshipit-source-id: 6cc3c465a
Summary: When a positive bound is expected, min(1,x) can be simplified to 1.
Reviewed By: ezgicicek
Differential Revision: D17091884
fbshipit-source-id: 3a89a44fa
Summary:
This did not work. One can not create a param that depends on another param (dynamic!) value
```
infer --dynamic_dispatch
/Users/mityal/infer/infer/bin/infer: unknown option '--dynamic_dispatch'.
```
No info in the manual:
```
find . -name "*.txt" | xargs grep "dynamic"
```
Reviewed By: jvillard
Differential Revision: D17113568
fbshipit-source-id: 87d0a18ba
Summary:
I found it very confusing that running infer with --debug makes the
report to be different.
Intuitively, I expect (and I think majority of users would expect) that
`--debug` makes things more verbose (and potentially more slow / consuming
more memory and disk space), but does not change anything apart from it.
One pro of preserving existing behavior, pointed by jvillard:
- Suppose some check is experimental or disabled in the config. The
users expect the issue to be found, but it does not show up. They run
`infer --debug` to understand the behavior, and suddenly the issue shows
up.
I, hovewer, find this pro not important enough and potentially confusing
the users even more.
(If they want to investigate seriously, they can always use
--no-filtering, and there are a lot of cases when the issue does not
show up for others, much hard to undertand reasons, than the fact that
it is disabled).
Reviewed By: jvillard
Differential Revision: D17113750
fbshipit-source-id: 46cc93503
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
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: Test that cost analysis works with incremental analysis enabled
Reviewed By: ezgicicek
Differential Revision: D16620101
fbshipit-source-id: b41403954
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:
Write a test for the invalidation of changed procedures
Reverse analysis graph for this test: https://fburl.com/graphviz/ybidpidq
The procedures marked as changed are `a` and `d`, and this causes `a,b,c,d,e,main` to be invalidated as expected
Reviewed By: jvillard
Differential Revision: D16579526
fbshipit-source-id: cbec304ce
Summary:
Add test `incremental_analysis_remove_file` to the toplevel makefile so that it is called by `make test` etc
Also swapped the src_before and src_after files so the test checks file removal instead of addition.
Reviewed By: jvillard
Differential Revision: D16562340
fbshipit-source-id: 79bab5f66
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
Summary:
The default values of config options can sometimes depend on build-time
configuration values. This makes checking that the manuals "remain the same"
trickier as the manuals can be different depending on the platform. This
removes *all* default values from the checked-in manuals. We could be more
fine-grained and scrub only the values that are susceptible to change but for
now this is probably good enough.
This is done by implementing new options `--help-scrubbed` and
`--help-scrubbed-full` and using these in our tests instead of `--help` and
`--help-full` (which remain unaffected).
Also don't wrap the default values in `$(i,...)` anymore because the defaults
can trigger line breaks and then the man page is ill-formatted because that
format is stupid.
Reviewed By: mityal
Differential Revision: D16543779
fbshipit-source-id: bc929ff8c
Summary:
This diff prevents that the latest prune value is overwritten as top
from callees.
Reviewed By: jvillard
Differential Revision: D16540391
fbshipit-source-id: bdd5b42ed
Summary:
This diff improves the precision of the mod operator.
For example, result of x % c (when x>=0 and c>0) is
(before) [0, c-1]
(after) [0, min(c-1,x)]
Reviewed By: ezgicicek
Differential Revision: D16518578
fbshipit-source-id: a68660ee7
Summary: This diff tries to do weak update for the abstract locations by pointer arithmetic, e.g. `p[n]` or `p+n`, even if the type of `p` is declared as a simple pointer, not an array.
Reviewed By: ezgicicek
Differential Revision: D16458367
fbshipit-source-id: 3b4cdd7e4
Summary:
A test that records the expected output of:
- reverse analysis call graph
- introduced/pre-existing/fixed issues
- cost analysis results
Currently only the call graph is non-empty.
Reviewed By: PhoebeMay
Differential Revision: D16495470
fbshipit-source-id: f186d73d2
Summary:
The `represents_multiple_values` flag was adopted to decide whether updating abstract value strongly or weakly. However, the flag was included in the `Val` domain, which is strange, because it is a property of abstract locations, rather than abstract values. This makes the behavior of memory update function depend on the abstract value to update, making its code complicated.
This diff detach the `represents_multiple_values` flag from the `Value` domain, thus the memory update does not depend on the abstract value. Since this is a refactoring, I believe the diff should not make many semantic changes.
Reviewed By: ezgicicek
Differential Revision: D16441734
fbshipit-source-id: 4c10779d7
Summary: The reverse analysis call-graph is logged if `--debug-level-analysis` > 0, so that its value can be inspected for tests
Reviewed By: jvillard
Differential Revision: D16440567
fbshipit-source-id: 1ec6af1f3
Summary:
Pulse didn't treat local variables going out of scope as invalidating the corresponding address in memory. This diff fixes that by
- marking all local variables that exits the scope with the attribute `AddressOfStackVariable`
- before we write the summary for the proc, we make sure to invalidate all such addresses local to the procedure as `Invalid.` If such an address is read, then we would raise a use-after-lifetime issue.
Reviewed By: jvillard
Differential Revision: D16458355
fbshipit-source-id: 3686524cb
Summary: This implements incremental diff analysis by deleting only the summaries that need to be re-analyzed, keeping all summaries corresponding to procedures that have not been changed (or had a callee change).
Reviewed By: jvillard
Differential Revision: D16358474
fbshipit-source-id: 660a704a0
Summary: Incremental analysis relies on analysis results in the results directory, so don't delete this directory if `--incremental-analysis` is used
Reviewed By: jvillard
Differential Revision: D16458113
fbshipit-source-id: bf7c63cb3
Summary:
The same logic for reading the env var and defaulting to the local
results dir was duplicated in a bunch of places.
Reviewed By: artempyanykh
Differential Revision: D16458976
fbshipit-source-id: 41f1a4f9c
Summary:
There was a little bit of code duplication around `analyze_proc` to deal with
the fact that we may be starting from either a proc name or a proc desc. Create
a new `callee` type that represents this more explicitly. This allows not
loading the `proc_desc` eagerly when we don't need it, although that doesn't
seem to impact perf measurably.
Reviewed By: ezgicicek
Differential Revision: D16442221
fbshipit-source-id: 8e8ebbd6b
Summary:
TL;DR: Until this patch, if you ran infer on MacOS Mojave you most
likely would get an error related to missing header files. Now infer
tries to automatically locate current MacOS SDK path thus providing a
better experience for first time users.
Consider helloworld.c
```
#include <stdio.h>
int main()
{
return 0;
}
```
Invoking the analysis `infer -- cc -c helloworld.c` fails with
facebook-clang-plugins/.../include/c++/v1/stdio.h:108:15: fatal error: 'stdio.h' file not found
The reason for this is twofold:
1. infer uses its own clang, not Apple's one (thus custom paths are
not properly setup).
2. Apple stopped copying standard headers from SDK to /usr/include.
Reviewed By: jvillard
Differential Revision: D16377866
fbshipit-source-id: c336ad64f
Summary: This test wasn't building correctly or being called by the toplevel makefile
Reviewed By: jvillard
Differential Revision: D16458386
fbshipit-source-id: 48a0c2f36
Summary:
:
In previous commits we introduced deriving capabilities in Backend stats.
Now we can rewrite the code so that usage of all fields is enforced at compile time.
Reviewed By: jvillard
Differential Revision: D16458130
fbshipit-source-id: aef751440
Summary:
As discussed in D16358474, the options `--reanalyze` and `--incremental-analysis` are not compatible
This diff warns about the compatibility problem in the documentation
Reviewed By: jvillard
Differential Revision: D16440482
fbshipit-source-id: ab841ace6
Summary:
Minor improvements to a bunch of stuff
- mostly, always log backend stats and time spent analysing, regardless of `-j 1`
- output stats more like they appear in the record
- split `InferAnalyze.main` to be more readable (hopefully)
Reviewed By: mityal
Differential Revision: D16440586
fbshipit-source-id: 6f91f53cd
Summary:
It's a bit more annoying to `incr` but is more uniform with the other
`mutable` field.
Reviewed By: ngorogiannis
Differential Revision: D16359027
fbshipit-source-id: 817cd94a0
Summary:
Modify the scheduler to collect results from children at the end of the
parallel execution. Use this to collect backend stats and log their
aggregated sum.
Reviewed By: ezgicicek
Differential Revision: D16358867
fbshipit-source-id: 775792ef7
Summary:
Use it to trace summary stats. It will be used more/better in future
diffs that aggregates stats across parallel workers.
Reviewed By: ezgicicek
Differential Revision: D16358868
fbshipit-source-id: 764614153
Summary:
Summary.ml defines both a bunch of types and how to use them and a
mechanism to save and store summaries on disk while maintaining a
complex in-memory cache of what's on disk. Make the distinction clear.
Reviewed By: ngorogiannis
Differential Revision: D16358869
fbshipit-source-id: 9d4c6cb77
Summary:
It downgrades issues of void pointer to L5, because of its impreciseness. This is not
ideal but Inferbo cannot analyze arrays pointed by void pointers precisely at the moment.
Reviewed By: jvillard
Differential Revision: D16379911
fbshipit-source-id: f2c016aba
Summary:
Fixes#1126
Different checks contain some ad hoc places that look at this param, but there is no systematic way to suppress this.
The centralized place that is filtering results is `reporting.ml`.
Note that this diff does not remove other usages, because they do more than mere filtering results.
Reviewed By: jvillard
Differential Revision: D16339655
fbshipit-source-id: afabdc97a
Summary:
The analysis call graph is the call graph from the perspective of the analyses run in infer
This commit creates the reverse analysis call graph to be used for incremental diff analysis
Reviewed By: ezgicicek
Differential Revision: D16335938
fbshipit-source-id: 0cbab3298
Summary: The reverse call graph will be constructed by adding edges one-by-one, so expose functionality in CallGraph to add a single edge to the graph
Reviewed By: jvillard
Differential Revision: D16285016
fbshipit-source-id: 553fe1ecf
Summary:
Add a function to delete a summary from disk and caches
This is needed so that summaries corresponding to invalidated procedures can be removed (as part of incremental diff analysis)
Reviewed By: ngorogiannis
Differential Revision: D16332752
fbshipit-source-id: 7d3c7a121
Summary:
The genrule-capture integration with Java relies on a buck config flag `infer.infer_bin=<path to infer>` (see test changes in `DEFS` below).
In a CI environment where the infer binary is checked out under a random directory, this means that the buck genrule is keyed by a random string (the path to infer), and this defeats caching.
Switch to the following contract: the genrule target does not expect a config flag at all. Instead it runs whichever `infer` binary is in the path. To make sure the binary is the same one with the originator, the capture integration runs buck under a modified `PATH` where the originator `infer` is sure to be the first matching entry.
NB cache invalidation is still OK because we rely on `infer.version` buck config flag, which will be hashed into the rulekey.
Reviewed By: jvillard
Differential Revision: D16332696
fbshipit-source-id: 2975d5c26
Summary: The method defined in the interface didn't match the implementation. Caught by ulyssesr.
Differential Revision: D16339179
fbshipit-source-id: 9cbb1dc74
Summary:
Write a function to read in the summaries from the `.specs` folder
This is needed so the reverse analysis call graph can be constructed from the summaries
Reviewed By: ngorogiannis
Differential Revision: D16282333
fbshipit-source-id: 101ce2c5b
Summary:
This javalib release gives compatibility with java 9 modules.
It should also remove some Infer warnings (when a class has no superclass)
JFile.sep is now a char
Reviewed By: jvillard
Differential Revision: D16220583
fbshipit-source-id: 5d05afde0
Summary:
When a file is passed to infer through `--changed-files-index` which is
- an absolute path
- the file does not exist
Then the code fails throwing an exception in the function below while trying to relativise the absolute path.
The behaviour on relative paths is to skip missing files, and does not fail because Infer does not attempt to relativise them.
Swallow the exception and skip the file; and so unify the behaviour across relative and absolute paths.
Reviewed By: mityal
Differential Revision: D16279672
fbshipit-source-id: 33b468da7
Summary:
Move the logic that is general to any call graph from SyntacticCallGraph.ml into CallGraph.ml
This will allow the call graph logic to be re-used in a later diff
Reviewed By: ezgicicek
Differential Revision: D16265150
fbshipit-source-id: 10a067f28
Summary:
This sometimes fail in our CI, eg:
```
[*ERROR**][66148] file has vanished: "/data/sandcastle/boxes/trunk-git-infer/infer/tests/build_systems/utf8_in_pwd/../codetoanalyze/make/utf8_in_function_names-617be4bc.o.tmp"
```
The issue seems to be that we are too greedy and try and copy files that may
disappear. This diff makes the list of files to copy over explicit to exclude
such temporary files.
Reviewed By: artempyanykh
Differential Revision: D16261872
fbshipit-source-id: 2b080d27a
Summary:
Add a flag to enable incremental diff analysis, where old summaries are not recomputed unless necessary
The implementation for this flag will follow
Reviewed By: ngorogiannis
Differential Revision: D16222865
fbshipit-source-id: e7e225a87
Summary:
newer is better, right?
All the code changes in infer are because of core being bumped to v0.12.
Reviewed By: jberdine
Differential Revision: D16223183
fbshipit-source-id: f3c339966
Summary:
A common gotcha is the new test. Model the minimum amount of
`std::basic_string` to catch it.
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D16121090
fbshipit-source-id: 66f06cb43
Summary:
Be more flexible in what type of function calls are allowed in `ViaCall ...` actions to be able to include models.
Also get rid of `here here` in traces /o\
As a side-effect, get more precise (=qualified) procedure names in
traces (but not in messages so as not to be too verbose).
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D16121092
fbshipit-source-id: fb51b02f8
Summary:
The domain supported path sensitivity wrt to a specific boolean guard `Branch.unlikely`. This isn't used in actual code, so remove it.
Also
- add an .mli to the domain;
- unabbreviate domain name to match analyser name;
- use Payload.read instead of calling Ondemand directly;
- adjust tests.
Reviewed By: mbouaziz
Differential Revision: D16203953
fbshipit-source-id: 743aa4400
Summary:
`CallGraph.ml` computes a call graph using the explicit procedure calls in the source code (ie computes a syntactic call graph)
I am going to be adding code for an 'analysis call graph' that gives the callees of a procedure from the perspective of the analyses in infer
This diff renames `CallGraph.ml` to avoid confusion with the new analysis call graph logic
Reviewed By: ngorogiannis, jvillard
Differential Revision: D16204436
fbshipit-source-id: 67bed8e28
Summary: This function is suspected to be slow, let's take a look at realtime distribution
Reviewed By: ngorogiannis
Differential Revision: D16221864
fbshipit-source-id: 2698602a9
Summary:
Move annotation reachability tests to their own directory.
Clean up and complete the tests.
Reviewed By: jvillard
Differential Revision: D16201387
fbshipit-source-id: 8a87a25b7
Summary:
Treat `MainThread` and `WorkerThread` annotations.
Fix wrong test (`AnyThread` cannot call a UI-only method, because it can be called by ANY thread ;) ) See https://developer.android.com/reference/android/support/annotation/AnyThread
Clean up the code a bit.
Reviewed By: jvillard
Differential Revision: D16183798
fbshipit-source-id: 6b7e3b27e
Summary:
This probably never matters because what kind of function would get > 1000 specs?
Anyhow, this way we can all sleep better at night.
Reviewed By: mbouaziz
Differential Revision: D16202186
fbshipit-source-id: b3294b712
Summary:
- Change the method `Ondemand.analyze_proc_name` so that `caller_summary` is not optional
- Introduce a new method `analyze_proc_name_no_caller` to replace `analyze_proc_name` when there is no caller
Reviewed By: ngorogiannis
Differential Revision: D16183378
fbshipit-source-id: c0c67f869
Summary: Refactor the methods `analyze_proc_desc` and `analyze_proc_name` in `ondemand.ml` so that they no longer share code
Reviewed By: ngorogiannis
Differential Revision: D16182733
fbshipit-source-id: 5aee03092
Summary: Register the callees of a procedure in the set `Summary.callee_pnames`
Reviewed By: ngorogiannis
Differential Revision: D16165016
fbshipit-source-id: 364aa948c
Summary:
Store a set callee names (`Typ.Procname.Set`) in the summary of a procedure
This will allow a call graph to be constructed showing the dependencies between procedures from the perspective of the analyses
Reviewed By: ngorogiannis
Differential Revision: D16148907
fbshipit-source-id: ab6f5d616
Summary:
The fields `tenv` and `integer_type_widths` can be obtained from the `exe_env` field of `proc_callback_args`
This commit removes the redundant fields
Reviewed By: ngorogiannis
Differential Revision: D16149520
fbshipit-source-id: d37526fd4
Summary:
Supply the caller `Summary.t` to `Ondemand.analyze_proc_name` and `Ondemand.analyze_proc_desc` instead of the caller `Procdesc.t`
This change will enable a later commit to record the procedures that are called by a procedure in its summary
Reviewed By: ngorogiannis
Differential Revision: D16148677
fbshipit-source-id: cf353e89a
Summary:
Cluster checkers call `SummaryPayload.read` but set the `caller_summary` to correspond to the same summary as gives the `callee_pname`
This change introduces a new method `read_toplevel_procedure` that does not require a `caller_summary`, to be used by the cluster checkers
Reviewed By: ngorogiannis
Differential Revision: D16131660
fbshipit-source-id: 12caa1000
Summary: There were FNs caused by only looking for the immediate predecessors when we were checking the pattern. This diff heuristically chases 4 more predecessors to reduce the number of FNs.
Reviewed By: ngorogiannis
Differential Revision: D16149983
fbshipit-source-id: f65c57a0a
Summary: Adding typechecks to prevent potential FPs like the added test
Reviewed By: ngorogiannis
Differential Revision: D16149511
fbshipit-source-id: 6d3fe0ad4
Summary:
Change the datatype `ProcData` to include a field of type `Summary.t` instead of a field of type `Procdesc.t`
This will enable a later commit to supply a summary to `Ondemand.analyze_proc_desc` and `Ondemand.analyze_proc_name`
Reviewed By: ngorogiannis
Differential Revision: D16121405
fbshipit-source-id: 342374121
Summary:
`proc_desc` is an argument to the function `iterate_procedure_callbacks` in `callbacks.ml` but can always be obtained from another argument (`summary`)
This commit removes the redundant argument
Reviewed By: ngorogiannis
Differential Revision: D16107332
fbshipit-source-id: 21c21921e
Summary:
The record `proc_callback_args` (defined in `callbacks.ml`) contains the fields `proc_desc` and `summary`.
The field `proc_desc` is redundant because it can be obtained from `summary`.
This diff removes `proc_desc` and uses the summary to obtain it where needed.
Reviewed By: ngorogiannis
Differential Revision: D16090783
fbshipit-source-id: 5632d1f4a
Summary:
Replaced by pulse. `--ownership` is now a deprecated form of `--pulse`.
The ownership checker is starting to give wrong answers due to changes in the
clang frontend, so it's better to remove it in favour of pulse.
there_goes_my_hero
Reviewed By: ngorogiannis
Differential Revision: D16107650
fbshipit-source-id: bb2446a19
Summary: Refactor `ondemand.ml` so that the function `analyze_proc` does not need to be passed around as a function argument
Reviewed By: ngorogiannis, jvillard
Differential Revision: D16089689
fbshipit-source-id: 97ba07619
Summary:
javalib 3.0 adds more support for lambdas and instance methods in interfaces.
Java constant type has 2 more constructors. We don't handle them when
generating SIL (as before) but at least we are compatible with
javalib 3.0
Reviewed By: jvillard
Differential Revision: D16030479
fbshipit-source-id: 0b1508482
Summary:
So it turns out we need to translate even more cases. Pulse had a FP
before that this fixes.
Reviewed By: ezgicicek
Differential Revision: D16073629
fbshipit-source-id: c03460b5a
Summary:
This is needed to test some functionality in the next diff. Only one
test changes (no longer a FN), which is now documented. Also, stop
including the "header models" meant for biabduction!
Maybe one day we'll need to have several test modes for different C++
versions. Seems overkill for now, so let's wait until we see some actual
issues (eg FPs) that manifest in one version but not the other.
Reviewed By: mbouaziz
Differential Revision: D16073630
fbshipit-source-id: 1cfdfc933
Summary:
Previously it was required to provide SDKROOT during configure on Mojave
hosts to `make` the project which in scripts was messing up local clang
and somewhat error-prone. Instead we could use xcrun to find required SDK
paths automatically.
Reviewed By: jvillard
Differential Revision: D16072354
fbshipit-source-id: 93cbf3980
Summary:
Move control of the number of remaining task from the taskbar [1] to each task generator [2]. This means that the call graph scheduler can count all procedures in mutually-recursive cycles as dealt with when only those procedures are left.
[1] : `infer/src/base/TaskBar.ml`
[2] : type defined in `/infer/src/base/ProcessPool.ml`
Reviewed By: ngorogiannis
Differential Revision: D16071497
fbshipit-source-id: aa9436638
Summary: Could be made better for cycles but not used and not unit tested, let's remove it.
Reviewed By: ngorogiannis
Differential Revision: D16017744
fbshipit-source-id: 6f7ae95c1
Summary: Do not fail on cycles, normalize values issuing from cycles, but do not try to recognize equal cycles like `let rec x = 1 :: x` and `let rec y = 1 :: 1 :: y`. This is unlikely to happen in our code.
Reviewed By: ngorogiannis
Differential Revision: D16017365
fbshipit-source-id: 691bb756c
Summary:
Sometimes the post of a function call has attributes on addresses that
were mentioned in the pre but are no longer reachable in the post. We
don't want to forget these, see added test.
Reviewed By: mbouaziz
Differential Revision: D16050050
fbshipit-source-id: 1ce522b97
Summary:
Previously we would union them with the previous attributes. I don't
think that makes sense.
Also change the interface a bit in preparation for the next commit.
Reviewed By: mbouaziz
Differential Revision: D16050051
fbshipit-source-id: 2e8f88f4e
Summary:
Noticed that:
- some option was always `Some _`
- recording the post never raises `Aliasing` (only exploring the pre does)
- a mutual recursion was unused
Reviewed By: mbouaziz
Differential Revision: D16050052
fbshipit-source-id: 7f77aae08
Summary:
Currently, `Callbacks.analyze_procedures` creates a function to call the method `Callbacks.iterate_procedure_callbacks`. This is supplied as an argument to functions in `ondemand.ml`, so that it can be invoked. This is done to avoid a cyclic dependancy.
This diff moves the functions that `ondemand.ml` needs to call into `ondemand.ml`, avoiding the need to supply them as arguments.
Reviewed By: ngorogiannis
Differential Revision: D16028836
fbshipit-source-id: 16ae27a3e
Summary:
The previous code would call the destructor for the C++ temporary
*before* the prune nodes, which then try to dereference it. Wrong.
Quick fix: don't destroy temporaries in conditionals.
Reviewed By: mbouaziz
Differential Revision: D16030735
fbshipit-source-id: e11abad58
Summary:
Similar to D16005395: `folly::Optional` has a boolean field to know if
it needs to destroy the wrapped object and pulse ignores that
completely, causing false positives each time an `Optional` is created
around something with a non-trivial destructor.
Reviewed By: mbouaziz
Differential Revision: D16030149
fbshipit-source-id: aeed4a0b3
Summary:
We were skipping some instructions before and that was a problem for
pulse. See added pulse test.
Reviewed By: mbouaziz
Differential Revision: D16030150
fbshipit-source-id: 9c62e6213
Summary: Not sure if anyone uses this but there, now it's modelled.
Reviewed By: mbouaziz
Differential Revision: D16008162
fbshipit-source-id: f4795dcba
Summary:
Prevent false positives about variables captured by value gone out of
scope.
Reviewed By: ezgicicek
Differential Revision: D16008165
fbshipit-source-id: d70e47db4
Summary: We know how to do interprocedural calls so let's use that!
Reviewed By: mbouaziz
Differential Revision: D16008164
fbshipit-source-id: 4c34bf704
Summary:
`function::operator=` is called whenever we assign a literal lambda to a
variable, so it's pretty useful to be able to report anything on
lambdas.
Reviewed By: mbouaziz
Differential Revision: D16008163
fbshipit-source-id: a9d07668d
Summary:
The previous version had a potentially exponential behavior on values with already lots of sharing.
This is fixed here at the price of a multiplicative constant factor (cost of `Hashtbl.hash`).
It also prepares for the handling of cycles.
Reviewed By: ngorogiannis
Differential Revision: D16016906
fbshipit-source-id: 611287917
Summary:
In light of Pulse's misadventures with HIL, leave a warning for future
checkers writers. Comment mostly taken from summary of D15824961.
Reviewed By: ngorogiannis
Differential Revision: D16005392
fbshipit-source-id: 805f17584
Summary:
This can take a minute or so during which the user would have no idea
what infer is doing.
Reviewed By: ngorogiannis
Differential Revision: D16005393
fbshipit-source-id: 586812527
Summary:
No need to hide the real reason for the crash behind another crash when
trying to print the error message.
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D16005394
fbshipit-source-id: dc3d9437e
Summary:
The constructor of `folly::SocketAddress` conditionally deletes some
object and then makes that condition false. The destructor then does the
same. Pulse ignores conditionals so will see a double delete.
Just skip that function for now, but it should be easy for pulse to be
more correct here if it knew how to compare constant values.
Reviewed By: mbouaziz
Differential Revision: D16005395
fbshipit-source-id: 036f5091b
Summary:
Printing `Exp.Const (Cfun proc_name)` adds `_fun_` in front of the
procedure name, eg `_fun_foo` instead of `foo`. This showed up in pulse
traces.
Reviewed By: mbouaziz
Differential Revision: D16004606
fbshipit-source-id: 72ac6866f
Summary:
Fixes a false positive where the address of a C++ temporary is bound to
a static const reference variable then returned. The fix doesn't try to
establish that the variable is a const reference so could lead to false
negatives but that can be addressed later.
Reviewed By: ezgicicek
Differential Revision: D16004538
fbshipit-source-id: e403dbefe
Summary:
Replace Hashtbl.clear with Hashtbl.reset
This saves memory because the reset method shrinks the hash-table, whereas the clear method just empties it
Reviewed By: jvillard
Differential Revision: D16004966
fbshipit-source-id: f32b00b0f
Summary:
[apologies for the unreviewable diff...]
Get rid of HIL expressions in pulse. This finishes the HIL -> SIL
migration. The first step made pulse start from SIL instructions but
would translate most accesses to HIL to re-use most of the existing
pulse code. This diff gets rid of the intermediate translation of SIL
expressions to HIL expressions.
Big changes:
1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything.
2. Stop trying to reverse-engineer what addresses mean in terms of
access paths from program variables. Rely on the trace pointing at
the right places in the code to be enough. This is because it wasn't
that useful (and could even be misleading when wrong) but could be
prohibitively expensive in degenerate cases (eg nodes with tens of
thousands of successive array accesses...)
3. `PulseAbductiveDomain.apply_post` now returns the computed return
value instead of recording it itself.
4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event`
5. Function calls arguments are now evaluated prior to doing anything
else, which saves everything else from having to (remember to) do
that. In particular, this changes how models look quite a bit.
Reviewed By: mbouaziz
Differential Revision: D15986373
fbshipit-source-id: 1d79935de
Summary:
Passing an absolute project path as buck config flag makes buck caching almost impossible for infer artefacts, since on every host/run that directory can be different.
Eliminate that and rely on shell commands to find the project root, executed within the genrule.
Reviewed By: jvillard
Differential Revision: D15963807
fbshipit-source-id: b6e590029
Summary:
Some functions exposed in ScubaLogging interface were not
used outside of ScubaLogging and caused deadcode to fail.
Reviewed By: ngorogiannis
Differential Revision: D15964204
fbshipit-source-id: d823dbf8b
Summary:
Reduces the size of the `tenv` by sharing values as most as possible, in an untyped - but supposedly safe - way, by using black magic on objects.
Can be reused for other things later.
Reviewed By: ngorogiannis
Differential Revision: D15855870
fbshipit-source-id: 169a4b86b
Summary:
Using `Marshal.to_string` to create SQLite values used in comparisons is brittle as there is no guarantee that it will return the same value for structurally equal values.
When adding sharing, this will definitely break.
From the SQLite queries I found, only `SourceFile` and `Procname` are used in comparisons.
I haven't tested performance.
It shouldn't change anything for `SourceFile` as there is no possible sharing.
It shouldn't change much for `Procname` as they are pretty small anyway.
Reviewed By: ngorogiannis
Differential Revision: D15923122
fbshipit-source-id: ce4af1fe3
Summary: Inject destructor calls to destroy a temporary when its lifetime ends.
Reviewed By: mbouaziz
Differential Revision: D15674209
fbshipit-source-id: 0f783a906
Summary:
Now that HIL doesn't help us anymore we need to reconstruct its mapping
"SIL logical var -> program access path". We already have everything we
need in pulse: it suffices to walk the current memory graph starting
from program variables until we find the value of the temporary we are
interested in.
This diff also builds some type machinery to make sure all accesses are
explained.
Reviewed By: mbouaziz
Differential Revision: D15824959
fbshipit-source-id: 722c81b39
Summary:
It turns out HIL gets in the way of a precise heap analysis. For
instance, instead of:
```
n$0 = *&x.f
_ = delete(&x)
*&y = n$0
```
HIL tries hard to forget about intermediate variables and shows instead
```
_ = delete(&x)
*&y = *&x.f
```
Oops, that's a use-after-delete, whereas the original code was safe.
While it's easy to write SIL programs that are completely unsound for
HIL, they are not generated very often from the frontends. In fact, the
problem became apparent only when making the clang frontend translate
C++ temporaries destructors, which produces the situation above
routinely.
This diff makes the minimal amount of change to make Pulse build and
produce equivalent results (minus HIL bugs) starting from SIL instead of
HIL. The reporting sucks for now because we need to translate SIL
temporaries back into program access paths. This is done in the next
diff.
Reviewed By: mbouaziz
Differential Revision: D15824961
fbshipit-source-id: 8e4e2a3ed
Summary:
Just moving code around.
This is needed later to make some types in `PulseTrace` depend on
a new that I'll have to define in `PulseDomain`.
Also, this gives better names all around I think
Reviewed By: mbouaziz
Differential Revision: D15881281
fbshipit-source-id: e86c1472e
Summary:
Just moving code around.
This is needed later to make some types in `PulseInvalidation` depend on
a new type that I'll have to define in `PulseDomain`.
Reviewed By: mbouaziz
Differential Revision: D15824962
fbshipit-source-id: 86cba2bfb
Mitya Lyubarskiy
Sungkeun Cho
Dulma Churchill
Nikos Gorogiannis
Phoebe Nichols
Ezgi Çiçek
Jules Villard
Martin Trojer
Artem Pianykh
David Pichardie
Mehdi Bouaziz
Radu Grigore
Dino Distefano