Summary: Our annotation parameter parsing is too primitive to identify `resType` and before we only assumed that all Prop's can be set by any of the two suffixes: `Attr` and `Res`. After talking to Litho team, there is 3 more additions to these suffixes: `Dip`, `Sip`, and `Px`.
Reviewed By: ngorogiannis
Differential Revision: D17528482
fbshipit-source-id: 8d7f49130
Summary: Before, we were mistakenly checking any annotation that ends with Prop such as TreeProp. This was wrong. Instead, we should only check Prop as adviced by the Litho team.
Reviewed By: ngorogiannis
Differential Revision: D17527769
fbshipit-source-id: b753dd87a
Summary:
Introduce a new experimental checker (`--impurity`) that detects
impurity information, tracking which parameters and global variables
of a function are modified. The checker relies on Pulse to detect how
the state changes: it traverses the pre and post pairs starting from
the parameter/global variable and finds where the pre and post heaps
diverge. At diversion points, we expect to see WrittenTo/Invalid attributes
containing a trace of how the address was modified. We use these to
construct the trace of impurity.
This checker is a complement to the purity checker that exists mainly
for Java (and used for cost and loop-hoisting analyses). The aim of
this new experimental checker is to rely on Pulse's precise
memory treatment and come up with a more precise im(purity)
analysis. To distinguish the two checkers, we introduce a new issue
type `IMPURE_FUNCTION` that reports when a function is impure, rather
than when it is pure (as in the purity checker).
TODO:
- improve the analysis to rely on impurity information of external
library calls. Currently, all library calls are assumed to be nops,
hence pure.
- de-entangle Pulse reporting from analysis.
Reviewed By: skcho
Differential Revision: D17051567
fbshipit-source-id: 5e10afb4f
Summary:
As per previous diff, attempt to allocate fewer strings. This doesn't
seem to affect perf although allocating less might reduce memory
pressure.
Reviewed By: mityal
Differential Revision: D17423973
fbshipit-source-id: e2e37b071
Summary:
My spidey senses were tingling. Next diff uses the `pp` functions
everywhere it was kind of obvious how to change the code to do so. It
doesn't improve perf but is less clowny that way. It might lessen memory
pressure since allocating strings is expensive and this code was doing a
lot of it.
Reviewed By: ngorogiannis
Differential Revision: D17450324
fbshipit-source-id: 632cee584
Summary:
The code was already trying to do that but failing. Now it works.
This revealed a slight bug where the progress bar would always stop at
N-1/N 99% jobs. Fixed by moving the progress bar updates *after* the
operation that might decrease the number of jobs left.
Reviewed By: mityal
Differential Revision: D17423978
fbshipit-source-id: fc32db5f3
Summary:
Previously we would incorrectly report the time for the whole process
and this could include capture time too.
Reviewed By: mityal
Differential Revision: D17423977
fbshipit-source-id: b3ed754b3
Summary: We should be able to run this processing ast steps without running linters or capture. This also adds a new module ProcessAST to do the processing, Capture.ml should not know anything else than calling the respective modules for capture, linting or processing.
Reviewed By: ngorogiannis
Differential Revision: D17501453
fbshipit-source-id: 30adba5b1
Summary:
`ModeledRange` represents how many times the interval value can be updated by modeled functions. This
domain is to support the case where there are mismatches between value of a control variable and
actual number of loop iterations. For example,
```
while((c = file_channel.read(buf)) != -1) { ... }
```
the loop will iterates as the file size, but the control variable `c` does not have that value. In
these cases, it assigns a symbolic value of the file size to the modeled range of `c`, then which
is used when calculating the overall cost.
Reviewed By: jvillard
Differential Revision: D17476621
fbshipit-source-id: 9a81376e8
Summary:
1/ Nikos Gorogiannis pointed out that
- for highly reused public types, records (especially when >= 3 params) are generally more readable than tuples.
- Records simplify code modifications, especially adding new fields. And we are going to add some, namely param flags, in the future.
2/ Let's make the fact that annotated signature is deprecated more
visible; it will also simplify searching for usages when we will be
getting rid of them.
Reviewed By: ngorogiannis
Differential Revision: D17475033
fbshipit-source-id: 7740c979b
Summary:
- Instead of merging one target DB into the main DB at a time, merge all target DBs into an in-memory DB (thus, no writing) and then dump it into the main DB at the end. This makes merging faster.
- When using the sqlite write daemon, there is no reason to drive the merge process from the master, sending each individual target to merge down the socket and doing one DB merge at a time. Here we move all the DB merging logic in the daemon, and expose a single function that does it all.
- Refactor some common functionality (notably the `iter_infer_deps` function is now in `Utils`) and remove dead files.
This can be also done using a temporary DB (which is not limited to memory) but this showed worse perf in tests than the in-memory solution as well as the current state of things (! possibly Sqlite-version related?).
Reviewed By: skcho
Differential Revision: D17182862
fbshipit-source-id: a6f81937d
Summary:
`get_field_annotation` is (together with
`get_modelled_annotated_signature`) an entry point when Nullsafe fetches
annotation information.
In follow up diffs we are going to utilize added information; see also
TODO in the code
Reviewed By: ngorogiannis
Differential Revision: D17475034
fbshipit-source-id: dab77bc7b
Summary:
"Unannotated" is misleading and ambiguous concept, it can have different
meanings depending on agreements.
The current logic treats them as Nonnull, which is exactly what we want
to preserve.
(If we need to partially model some functions where we don't have
opinion on some of types in the signature, we can explicitly model
unknown nullability later on).
Note that I am not aiming for substantial refactoring of
modelsTables.ml; the scope of this diff is merely to clarify things.
Reviewed By: ngorogiannis
Differential Revision: D17449347
fbshipit-source-id: 43c798ce7
Summary:
This function is the main entry point for getting annotated signature
for nullsafe.
We will modify it and its callees in follow up diffs to migrate other
features of Annot.items to specialized types.
Reviewed By: ngorogiannis
Differential Revision: D17448082
fbshipit-source-id: be00b4737
Summary:
This is a central abstraction for coming future unknown nullability support.
# Context
Annot.ml is a low-level module:
- it contains lists of raw (string) annotations
- no algebraic datatypes for annotations
- it mixes annotations that Nullsafe should be aware of with all sorts of other annotations
- some annotations make sense for return values, some make sense for params, and some make sense for methods.
But, most importantly, it does not contain information about source of an annotation, making it hard to distinct things like "Nonnull as default" vs "Nonnull as explicitly annotated" vs "Nonnull as modelled". Ditto for nullable.
Because of this, it is tricky to introduce unknown nullability in an elegant way.
Let's get rid of using Annot.Item.t in nullsafe code in the following way:
- Move nullability information associated with the Java type to a dedicated algebraic DT.
- Split other annotations that are important for nullsafe into param flags, ret value flags, and method flags, and introduce corresponding datatypes.
# This diff
This diff introduces NullsafeType and adds this to AnnotatedSignature.
It is not used yet, hence the diff is a no-op.
In future diffs, we are going to (see also TODOs in the code):
- actually use this information instead of accessing Annot.item
- add more information to AnnotatedSignature
- remove Annot.item from AnnnotatedSignature
- when this is done, introduce notion of unknown nullability.
Reviewed By: ngorogiannis
Differential Revision: D17420595
fbshipit-source-id: b30706d9b
Summary:
This diff extends the `Simple` alias domain to address Java's
temporary variables better. It now has an additional field to denote
an alias temporary variable.
Reviewed By: jvillard
Differential Revision: D17421907
fbshipit-source-id: 8b8b47461
Summary:
We historically had Model.Inference, which was an attempt to enhance
models with additional abilities to get the annotation.
This feature got removed in D9805110, including removing of the key
condition Models.Inference.field_is_marked.
This code also is not executed: `Config.eradicate` condition
was an old artefact of migrating Eradicate to callback infrastructure:
D1508451. We run eradicate only as a callback as of now, so this flag is
always true.
In follow up diffs we refactor AnnotationSignature module, and this
cleanup simplifies the refactoring.
Reviewed By: ngorogiannis
Differential Revision: D17419173
fbshipit-source-id: 1b30555de
Summary:
CONDITION_REDUNDANT_NONNULL was an attempt to reduce number of false
positives for condition redundant. (It is the most popular check as of
now).
The root case for most of false positives is that a lot of code is
simply not annotated (but should have been), so blaming developers for defense programming is
not actionable.
In attempt to solve the problem, a special issue type (for case when the
code is explicitly annotated with Nonnull) was introduced.
In follow up diffs we are going to introduce a generic way of doing the
same, not limited to this particular check only.
Namely, we will introduce notion of unknown nullability, so it will be
possible to distinguish not annotated yet (hence no warnings) and already
annotated (hence warnings) parts of code.
This piece of logic is incompatible with the aforementioned work, hence
we need to remove it.
Reviewed By: jvillard
Differential Revision: D17398768
fbshipit-source-id: 8bddf10e5
Summary:
This diff simplifies two similar alias targets: AliasTarget.Simple and
AliasTarget.SimplePlusA. Since the latter is simply extended version
of the former, they are better to have a common constructor.
Reviewed By: jvillard
Differential Revision: D17421416
fbshipit-source-id: e0946a73b
Summary:
This diff revises widening functions of bounds that have a linear form and a min/max form.
For example, for lower bounds,
* 3 ▽ (1+min(2, x)) = (1+min(2, x))
* 3+x ▽ (3+min(2, x)) = (3+min(2, x))
Reviewed By: jvillard
Differential Revision: D17420786
fbshipit-source-id: ff9eebed3
Summary: This diff ignores field's type in their comparisons. They should be distinguished by their names and struct types.
Reviewed By: dulmarod
Differential Revision: D17284621
fbshipit-source-id: ae8a33083
Summary:
This diff addresses collection adds in loop. For example,
```
ArrayList<...> a = new ArrayList<>();
for (int i = 0; i < size; i++) {
a.add(...);
}
// we want to know the size of `a` here!
```
This is a common pattern on initializing a collection in Java.
How we did: Instead of adopting general (but complicated) solutions such as relational domain, we
extended the current alias domain of inferbo, to be able to handle this specific case:
* An array `a` should have size 0, at the entry of the loop.
* The iterating variable `i` should start with 0.
* `add` should be called once inside the loop.
Reviewed By: jvillard
Differential Revision: D17319350
fbshipit-source-id: 99b6acae1
Summary:
Sqlite versions set their own default page and cache size. Old versions use crazy-non-optimal settings.
Allow setting both from command line and set up reasonable defaults. See, e.g.,
https://wiki.mozilla.org/Performance/Avoid_SQLite_In_Your_Next_Firefox_Feature
for page size notes.
The defaults will cost a maximum of 64Mb in cache per Infer process. These improve merging times significantly.
Reviewed By: jvillard
Differential Revision: D17364643
fbshipit-source-id: b9abab10f
Summary:
At some point, there was a custom equality function that deliberately ignored some fields in err_instance. It was deleted in D4232422, so having a custom hash function does not serve any purpose anymore.
Since 2016 there was no known problems with the change in D4232422.
If we decide that we need similar behavior that was before D4232422, it will be easier to reimplement the functionality again.
Reviewed By: jberdine
Differential Revision: D17313660
fbshipit-source-id: 5c6c29a0b
Summary:
We want to allow following declaration
```
CK::UIContext t(foo);
```
In this case t is only part of the scope and we don't want to check that is never mutated.
Reviewed By: kfirapps
Differential Revision: D17367040
fbshipit-source-id: 5312a1249
Summary: This calls the method `delete_capture_and_analysis_data` introduced in D17184424 once the appropriate specs files for incremental analysis have been deleted. This fixes two bugs that I observed in incremental analysis that were arising because of stale state left in the results directory.
Reviewed By: ngorogiannis
Differential Revision: D17184424
fbshipit-source-id: d63f59db9
Summary:
I observed a bug in incremental analysis for thread safety analysis, where a thread safety violation was not being reported because the folder `racerd` was not being cleaned. This meant that the violation was determined to be a preexisting issue when it was actually an introduced issue.
This method can be used to fix this problem by cleaning the `racerd` folder. It also cleans the `captured` folder, I've done this following the original version of the method (see D16602417).
I'm not sure if the `captured` folder is used; it wasn't used in the tests I did. Thoughts about this?
Reviewed By: ngorogiannis
Differential Revision: D17261504
fbshipit-source-id: 8fea23e98
Summary:
There is currently a bug in incremental analysis because the capture data is not reset once the specs files have been invalidated. This has caused a problem where cost issues that should be reported are not spotted. I'm introducing this method so I can use it to fix incremental analysis.
This method is resurrected from D16602417
Reviewed By: ngorogiannis
Differential Revision: D17184401
fbshipit-source-id: e84925324
Summary: It prints debug information when top values is generated.
Reviewed By: ngorogiannis
Differential Revision: D17285448
fbshipit-source-id: 0621fd36d
Summary:
This check was an incomplete attempt to make nullsafe check nutritious
annotations for fields that get modified.
This was never fully productionized, and this check is turned off by
default.
In near future, we don't anticipate supporting this feature, so let's
remove it to simplify the code.
Reviewed By: artempyanykh
Differential Revision: D17282015
fbshipit-source-id: d63a2f1f7
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: 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: 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:
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:
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:
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:
`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:
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
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:
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:
:
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:
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:
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:
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:
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
Summary:
Make it possible to re-use the graph visitor to compute all sorts of
things with a flexible API where you can pass a function that folds over
all addresses reachable from certain stack variables (specified with a
filter) and gets passed the access path that leads to each address.
This is used in later commits.
Reviewed By: mbouaziz
Differential Revision: D15824960
fbshipit-source-id: c424a71cb
Summary: Preanalysis is performed at the frontend now. Hence, we don't need to repeatedly check/set when/if it is performed.
Reviewed By: mbouaziz
Differential Revision: D15863175
fbshipit-source-id: f9c6b7ae1
Summary:
One "interesting" feature of the approach of merging the captured targets in Java, is that we union their type environments, as opposed to store partial tenvs together with each source file, which is the case for Clang.
This means
- the final global type environment is potentially huge because it contains all the types in all targets.
- all analysis workers start by loading that tenv in memory, meaning we consume `|size of tenv| x #cpus` memory, which can tip the balance towards OOMs
This diff attempts to economise on global tenv size. This is done by increasing sharing which is then preserved by marshalling. It's done in a brute force way, with hashtables for each struct component, and is not fully effective due to the recursion amongst types and types names, as well types appearing inside other constructs such as procnames.
This is done when calling `Tenv.store` so that
- the computation can be parallelised somewhat (capture is parallel, merging is not)
- buck caching will benefit from smaller tenvs.
This saves about 24% of total memory devoted to the type environment.
Reviewed By: mbouaziz
Differential Revision: D15840054
fbshipit-source-id: 6f03be1a4
Summary:
- Add allocation costs to `costs-report.json` and enable diffing over allocation costs.
- Also, let's be more consistent and modular in naming our cost issues.
- introduce a generic issue type `X_TIME_COMPLEXITY_INCREASE` where `X` can be one of the cost kinds. If the function is on the cold start, issue can have the `COLD_START` suffix. Similarly for infinite/zero/expensive calls.
- Change `PERFORMANCE_VARIATION` -> `EXECUTION_TIME_COMPLEXITY_INCREASE`
- Add new issue type for `ALLOCATION_COMPLEXITY_INCREASE_COLD_START` which will be enabled by default
- Refactor cost issues to be more modular and succinct. This also makes addition of a new cost kind very easy by adding the kind into the `enabled_cost_kinds` list in `CostKind.ml`
Reviewed By: mbouaziz
Differential Revision: D15822681
fbshipit-source-id: cf89ece59
Summary:
In a next diff temporaries will get destructed at the end of their
lifetimes and that naive model would be causing false positives.
The flipside is that we lose all reports on closures for now, will need
to model them separately later.
Reviewed By: mbouaziz
Differential Revision: D15695943
fbshipit-source-id: c2c482c02
Summary:
Needed for next diff: we'll need to do 2 passes on the AST to collect
the temporaries to destroy at the end of an `ExprWithCleanups`, but the
SIL names of these temporaries are generated freshly on the fly so they
would get different names if we do it naively.
This adds a hashmap to the translation context so the temporary
corresponding to a given `MaterializeTemporyExpr` is only generated once
and then reused.
Reviewed By: mbouaziz
Differential Revision: D15674212
fbshipit-source-id: 0e16062d9
Summary:
This started as an attempt to understand how to modify the frontend to
inject destructors for C++ temporaries (see next diffs).
This diff rewrites the existing logic for computing the list of
variables that should be destroyed at the end of each statement, either
because it's the end of their syntactic scope or because control flow
branches outside of their syntactic scope.
The frontend translates a function from the last instructions to the
first, but scope computation needs to be done in the other direction, so
it's done in a separate pass *before* the main translation happens. That
first pass creates a map from statements in the AST to the list of
variables that should be destroyed at the end of these statements. This
is still the case now.
Before, that map would be computed in a bit of a weird way: scopes are
naturally a stack but instead of that the structure maintained was a
flat list + a counter to know where the current scope ended in that
list.
In this diff, redo the computation maintaining a stack of scopes
instead, which is a bit cleaner. Also treat more instructions as
introducing a new scope, eg if, for, ...
Reviewed By: mbouaziz
Differential Revision: D15674208
fbshipit-source-id: c92429e82
Summary:
Somewhat trivial: add a string to "Destruction" nodes to indicate why
they were created. Rename the main `instruction_aux` function into
`instruction_translate` (see next diff for why).
Reviewed By: mbouaziz
Differential Revision: D15674211
fbshipit-source-id: 8a7eda72c
Summary: This allows to match `foo<int_&>` and many other horrible names.
Reviewed By: mbouaziz
Differential Revision: D15825403
fbshipit-source-id: c892033aa
Summary:
I realized that there was a discrepancy in the # of instructions between whether we run a single analysis or multiple analyses at the same time. It turns out that in biabduction, bufferoverrun and other HIL analyses we did Preanalysis step (which adds scope instructions and invokes liveness etc.) but not in others. This discrepancy results in inconsistent analysis results (e.g. in the new inefficient-keyset-iterator) that rely on instructions. We should be consistent. Hence, we now invoke Preanalysis in the frontend and remove all other uses in the rest of the checkers.
Consequently, I had to update the inefficient-keyset-checker to take the CFG resulting from Preanalysis with extra scoping instructions.
Reviewed By: mbouaziz, ngorogiannis, jvillard
Differential Revision: D15803492
fbshipit-source-id: 4e21eb610
Summary:
This is a simple checker that identifies inefficient uses of `keySet` iterator where (not only the key but also) the value is accessed via `get(key)`. It is more efficient to use `entrySet` iterator which already returns both key-value pairs. This optimization would get rid of many extra lookups which can be expensive.
We simply traverse the CFG starting from the loop head upwards and pick up the map that is iterated over. Then, we check in the loop nodes if there is a call to `get(...)` over this map. If, so we report.
Reviewed By: ngorogiannis
Differential Revision: D15737779
fbshipit-source-id: 702465b4e
Summary:
Move genrule capture integration logic from shell to OCaml.
Also, stop relying on side-effects of buck compilation for constructing the infer-deps.txt file used for merging. Now this is obtained by passing `--show-output` to buck, which spits out the `buck-out` output paths to the targets we asked to build.
Reviewed By: ezgicicek
Differential Revision: D15715608
fbshipit-source-id: 8fa896ba6
Summary:
The synthetic methods from `topl.Property` are now nonempty: they
simulate a nondeterministic automaton.
Reviewed By: jvillard
Differential Revision: D15668471
fbshipit-source-id: 050408283
Summary:
Instrument SIL according to TOPL properties. Roughly, the
instrumentation is a set of calls into procedures that simulate a
nondeterministic automaton. For now, those procedures are NOP dummies.
Reviewed By: jvillard
Differential Revision: D15063942
fbshipit-source-id: d22c2f6fa
Summary: Not sure how that happens but it does. Instead of crashing, log the error and continue.
Reviewed By: martintrojer
Differential Revision: D15660008
fbshipit-source-id: c87e724d4
Summary: The previous commit broke the `--foo arg` case because it matched `--foo` in the case looking for `--foo=`.
Reviewed By: mbouaziz
Differential Revision: D15670472
fbshipit-source-id: ab81c7357
Summary: There's currently no way to skip these when they are passed to clang.
Reviewed By: martintrojer
Differential Revision: D15669132
fbshipit-source-id: be97d2638
Summary:
It is unsafe to call protocol methods defined optional. Before calling them we should check it
the implementation exists by calling
`if ([object respondsToSelector:selector(...)]) ...`
Without the above check we get run time crashes.
Reviewed By: jvillard
Differential Revision: D15554951
fbshipit-source-id: f0560971b
Summary:
- take advantage more structured attributes in the exported AST
- circumvent new format of `if` and `switch`
- a few new features/nodes but nothing major there
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz, martintrojer
Differential Revision: D15453572
fbshipit-source-id: c0c24345f
Summary:
- Rename `invariantModels` to `purityModels`
- Track which arguments are modified in purity models. Before we were invalidating all arguments of impure modeled functions. Instead, now we only invalidate modified args given in the model. This should ideally result in more precision in the analysis.
- Add some more purity models for :`cast`, `new`, `new_array` and `Math.random`
Reviewed By: mbouaziz
Differential Revision: D15535332
fbshipit-source-id: 5395800d9
Summary:
`infer_events` table is a key-value storage that also have list of fields common for entire infer run.
Infer should be agnostic of many of such fields (e.g. diff number).
Hence we will pass such extra fields through CI.
Note that only "normals" (strings in scuba terminology) are currently supported.
Reason being: most of things that are technically ints (like IDs) should actually be normals (because average etc does not make sense for them; and group by, in contrast, does).
Reviewed By: jvillard
Differential Revision: D15376636
fbshipit-source-id: 729eaabfc
Summary: There can be A LOT of procedures -- currently we log two lines (started/done) for each one, when doing call graph scheduling. This leads to ridiculously long log files. Switch to only log these messages in the log file and only if we are verbose logging.
Reviewed By: jvillard
Differential Revision: D15413330
fbshipit-source-id: 6e26693e8
Summary:
Thanks to the newly added `StarField`, path length is better controlled before ondemand is used.
Hence there is no need to (unsoundly) canonicalize paths then anymore.
Reviewed By: ezgicicek
Differential Revision: D15409716
fbshipit-source-id: 9ea7b4717
Summary:
This messes with the deduplication heuristic when templated function
names show up in the error messages, since the heuristic demands that
the error messages are the same.
Reviewed By: mbouaziz
Differential Revision: D15374333
fbshipit-source-id: 70232d254
Summary:
Improve the error messages, change is more or less documented in the
code.
Reviewed By: mbouaziz
Differential Revision: D15374334
fbshipit-source-id: f1dd54180
Summary:
Some edge case involving casting field pointers to the structure type itself generated arbitrarily long paths when used in a loop.
Without changing the widening, this diff avoids repetitions of fields in paths by abstracting them with a star.
E.g. `x.a.b.c.b` will become `x.a.b.c*.b`, and so will `x.a.b.c.a.b`, `x.a.b.c.c.b`, or `x.a.b.c.b.b`.
Reviewed By: ngorogiannis
Differential Revision: D15352143
fbshipit-source-id: 5ea426c5e
Summary:
I was wondering what were the empty sessions and why inferbo was running twice.
Answer: the empty sessions were 'compute pre' and the second run of inferbo was the narrowing phase.
Reviewed By: ngorogiannis
Differential Revision: D15378138
fbshipit-source-id: 507a3df42
Summary:
This was hardcoded to `true` and its purpose is unclear to me. I kill
what confuses me.
Reviewed By: jeremydubreil
Differential Revision: D15294783
fbshipit-source-id: 3c1c469ee
Summary:
- Makes sure that `start_session` and `finish_session` are well parenthesized
- Avoids a try finally when debug is disabled
Reviewed By: ngorogiannis
Differential Revision: D15371841
fbshipit-source-id: 340203edb
Summary:
Before: the trace would explain how a value was invalidated and
accessed, but not how the value that was invalidated had been
constructed.
Now: `PulseTrace.t` records breadcrumbs of how the value was constructed
in addition to the interproc "action" trace leading to the invalidation
or access action.
Concretely:
```
void bad(X &x) {
X *y = x;
X *z = x;
delete y;
access(z);
}
```
will produce the trace:
Invalidation part:
y = x
delete y
Access part:
z = x
access(z)
access to z->f inside of access(z)
Before this diff the "Access part" would be missing the "z = x" part of
the trace, so it might be confusing why `z` has anything to do with `y`.
However, such "breadcrumbs" are not recorded in the inter-procedural
part, only the sequence of calls is. This is a trade-off for simplicity,
maybe it's enough for developers maybe it isn't, we'll find out later.
Reviewed By: jberdine
Differential Revision: D15354438
fbshipit-source-id: 8d0aed717
Summary:
In preparation for the next diff that re-uses `PulseTrace.t` for a type
that combines breadcrumbs + action.
No change intended.
Reviewed By: mbouaziz, jberdine
Differential Revision: D15354437
fbshipit-source-id: cbb8757b4
Summary:
Before: no links to procedure summary and nodes in header file debug html
Now: some or all of them if you are lucky enough
Reviewed By: jvillard
Differential Revision: D15279379
fbshipit-source-id: a145f9e66
Summary:
Before: they are written only when the file is fully analyzed.
Now: a first version is written as soon as the file gets analyzed so that we get links to nodes, the final version overwrites it
Reviewed By: jvillard
Differential Revision: D15279351
fbshipit-source-id: a3120aa31
Summary:
update-submodule: facebook-clang-plugins
We used to translate `offsetof` by an unknown value.
This fixes it. It is now translated like an integer literal.
Reviewed By: ddino
Differential Revision: D15317799
fbshipit-source-id: ae89e0ec5
Summary:
API and stub implementation for real-time logging capabilities.
Low-level implementation requires interaction with FB-specific deployment of Scribe, hence it is stubbed out.
Reviewed By: jberdine
Differential Revision: D15259559
fbshipit-source-id: 712cb99e1
Summary: Previously there was no way of getting that list from the manual.
Reviewed By: jeremydubreil
Differential Revision: D15158598
fbshipit-source-id: 1705ed59d
Summary:
A more dynamic scheduling scheme will potentially run into the situation where no new work packets can be scheduled, but more work will be possible to schedule in the future, perhaps when some dependent work packet finishes being analysed.
The current implementation prevents that, as it expects that if a worker goes idle, it stays idle.
The changes here address this in two parts:
- the `select` call is always given a finite timeout. If given an infinite timeout, we will not be able to poll the task generator for more work, where none were previously possible.
- when the `select` call times out without updates, check if there is an idle child, and if so if the task generator has more work right now.
See also ProcessPool.mli for comments.
Reviewed By: mbouaziz
Differential Revision: D15197749
fbshipit-source-id: babe5da8e
Ezgi Çiçek
Jules Villard
Dulma Churchill
Sungkeun Cho
Taras Tsugrii
Mitya Lyubarskiy
Nikos Gorogiannis
Fabio Milano
Phoebe Nichols
Martin Trojer
Artem Pianykh
David Pichardie
Mehdi Bouaziz
Radu Grigore
Dino Distefano
Josh Berdine
Peter O'Hearn
Jeremy Dubreil
Andrew Adams-Moran
David Lively