Summary:
In order to handle the example added:
changed domain of `MethodCalled`
from `CreatedLocation -> (IsBuildCalled X IsChecked X Set(MethodCall))`
to `(CreatedLocation X IsBuildCalled) -> (IsChecked X Set(MethodCall))`
This avoids joining of two method calls where one is build-called and the other is not, e.g.,
```
if(b) {
o.build();
} else {
// no build call
}
```
changed domain of `NewDomain`
from `Created X MethodCalled`
to `(Created X MethodCalled) X (Created X MethodCalled)`
One is for no returned memory and the other is returned memory. This keeps precision some join
points of branches, e.g.,
```
if(b) {
return;
} else {
// no return
}
```
Reviewed By: ezgicicek
Differential Revision: D18909768
fbshipit-source-id: c39d1a1ef
Summary:
A plus is a plus, no need to give up when +/- is about pointers. This
gets rid of some false positives involving pointer arithmetic.
However, the problem remains if we make things a bit more
inter-procedural. This is documented in an added test.
Reviewed By: ezgicicek
Differential Revision: D18932877
fbshipit-source-id: 4ad1cfe72
Summary: It is not used anywhere and there are no plans to revive it. Kill it!
Reviewed By: skcho
Differential Revision: D18934719
fbshipit-source-id: b9b069b96
Summary: Under the buck/java integration, the classpath is propagated to all infer command lines. Logging that leads to huge waste and full disks. Make the logging conditional to debug mode.
Reviewed By: skcho
Differential Revision: D18934088
fbshipit-source-id: 7e2f410f5
Summary:
The `Typ.FIeldname` module has many issues. Among those:
- It has 5 different string/printing functions and most of them do radically different things in Java and in Clang.
- There is no type safety: creating a Clang field and calling a Java function on it will lead to a crash (`rindex_exn` etc, there are usually no dots in Clang fields).
- It uses a single string for Java fields, containing the package, the class and the field, e.g., `java.lang.Object.field`. This is wasteful, because
- there is no sharing of strings for packages/classes, and,
- string operations need to be performed every time we need the field or the class or the package alone.
This diff preserves the behaviour of the module's interface, so the API problems remain.
However, by using a saner representation for Java fields we can get small performance and large memory gains (the type environment in Java is much smaller, about 30-40%).
In addition, many functions on clang fields would previously do string manipulations (look for `.` and split on it) before returning the final field unchanged -- now they use the type of the field for that.
Reviewed By: jvillard
Differential Revision: D18908864
fbshipit-source-id: a72d847cc
Summary:
That class does some complicated accounting of memory that depends on
whether the string is "small", "medium" or "large". In the latter case
it does its own ref-counting and copy-on-write to save memory, and that
trips up pulse. Pretending all strings are small avoids that issue.
Reviewed By: skcho
Differential Revision: D18909030
fbshipit-source-id: 1c14d909b
Summary:
Including the current call state is useful because the contradiction
sometimes refers to abstract values that have been materialised since
the last call state so we cannot make sense of them unless we print the
current call state.
Reviewed By: skcho
Differential Revision: D18908424
fbshipit-source-id: 297f397a6
Summary:
- Do most of the work of `solve_arithmetic_constraints` inside `subst_attribute` instead, since we need to re-use the latter function for post-conditions where the first function is not appropriate.
- When substituting arithmetic constraints, we refine arithmetic information (both concrete intervals and inferbo), which can lead to inconsistent states. Instead of recording the new arithmetic facts by returning a new current state, just act as a map on attributes. This is to enable doing the point above.
- All this lead to a somewhat messy refactoring...
- Rename `CannotApplyPre` to `Contradiction` since it's used for post-conditions as well now
Reviewed By: skcho
Differential Revision: D18889120
fbshipit-source-id: d81647143
Summary:
After passing a `PRUNE` instruction we can refine the current inferbo
intervals for the values involved.
Reviewed By: ezgicicek
Differential Revision: D18889103
fbshipit-source-id: b521046aa
Summary:
This exposes a more general interface to other modules, at the cost of
hiding the fact that it won't deal with all binary operations with equal
precision.
Reviewed By: ezgicicek
Differential Revision: D18908095
fbshipit-source-id: 0c0653bb6
Summary: Guava uses assertions to ensure a future can be gotten without blocking (this means that if the future is not done, the app will crash). This diff teaches the starvation analyser about a number of such assertions, by treating them as assumes (since we don't care about exceptions).
Reviewed By: jvillard
Differential Revision: D18893427
fbshipit-source-id: 4d26a202b
Summary: A future is guaranteed not to block if `isDone()` has returned true first. Add logic for supporting that by remembering the objects that we have called `isDone` on and by making `assume` do the right thing with that knowledge. All this is achieved with the attribute domain.
Reviewed By: ezgicicek
Differential Revision: D18833901
fbshipit-source-id: 7f4ea0cd1
Summary: The formals of callees will be used in the following diff.
Reviewed By: ezgicicek
Differential Revision: D18878044
fbshipit-source-id: 6c01af826
Summary:
When retrieving a value from a container, we previously had an arbitrary hack which would
- In java, give no ownership to the returned object (trying to be sound)
- In C++ give conditional ownership to the current method's first argument (trying to be complete, but doing it badly, as the first argument may not be the `this` object in a static method, or we might be accessing it through another parameter altogether).
Harmonise both by using the existing ownership of the container as ownership value for the returned object (leaning towards completeness).
Reviewed By: jvillard
Differential Revision: D18882800
fbshipit-source-id: f98f8d315
Summary:
Every time we add an arithmetic information, add the corresponding
inferbo one.
Reviewed By: skcho
Differential Revision: D18888863
fbshipit-source-id: ab4afd372
Summary:
Pointers are hard... The previous test had no chance of doing
initialisation of the pointer by reference and was in fact a false
negative (and still is, fix incoming). Renamed functions to stress the
false negative and added a test that is really (potentially) doing
pointer initialisation by reference.
Reviewed By: skcho
Differential Revision: D18888008
fbshipit-source-id: 1e72408c7
Summary:
This reverts commit 4fd6165d190bab32544f9f040b777565432c15b2.
We don't need to check for reporting each node anymore. It suffices to just check per function.
Reviewed By: skcho
Differential Revision: D18883833
fbshipit-source-id: 2591b3af3
Summary:
Making `MethodCalled` an inverted map from created location to method calls results in not being able to track a builder that is created in two different branches of a conditional with different types. Instead, we can make `MethodCalled` simply a map and also change `Created` to be a map from access paths to a set of created locations.
To deal with the case of setting a prop only in one branch, we need to ensure that whenever we call a create method, we add a binding to `MethodCalled` with an empty list of methods so that its intersection with a non-empty one is empty.
Reviewed By: skcho
Differential Revision: D18883097
fbshipit-source-id: b3464ca20
Summary: As long as the types match, it should be possible to call build on two components that are created at different locations.
Reviewed By: skcho
Differential Revision: D18881740
fbshipit-source-id: 356f9e168
Summary:
Finally use information from the inferbo intervals in pulse's domain to
make decisions about whether conditionals are feasible or not.
Reviewed By: skcho
Differential Revision: D18811193
fbshipit-source-id: d80a28657
Summary:
Refine the type of inferbo intervals attributes to "pure" (non-bottom)
ones. This is because were we to get a Bottom value from inferbo we
should stop the abstract execution instead of recording it in the state.
Reviewed By: ezgicicek
Differential Revision: D18811165
fbshipit-source-id: fff8664b7
Summary:
Similarly to binops, let inferbo evaluate unary operations and record
the results.
Reviewed By: ezgicicek
Differential Revision: D18811146
fbshipit-source-id: 8f9e16bbd
Summary: Add a FN that is detected by the old domain but not the new one
Reviewed By: ngorogiannis
Differential Revision: D18854389
fbshipit-source-id: 9bdc90a6b
Summary: The map from `CreatedLocation` to `MethodCalls` already takes care of the association from create methods to their set props. `MethodCall` comparison should be oblivious the the receiver, otherwise, we risk mistakenly considering two props set at different locations as different.
Reviewed By: skcho
Differential Revision: D18829388
fbshipit-source-id: b5a0d628d
Summary: This diff check and report on every nodes. Problem of the previous design is that it has to report alarms only with the abstract memory of the exit node. However, the new abstract value becomes imprecise at every join points on the path to the exit node, since it is using inverted map, i.e., under-approximation on collecting called methods. As a solution, this diff report on every nodes where `.build` is called with the abstract memory at that node.
Reviewed By: ezgicicek
Differential Revision: D18809449
fbshipit-source-id: 4fd6165d1
Summary: Current method call comparison is too strong. As exemplified with the new test, one can also set the required prop by calling a version which contains the suffixes. The domain should take care of such cases now.
Reviewed By: skcho
Differential Revision: D18808869
fbshipit-source-id: 9f7672e75
Summary:
Sometimes clang9 does not return a boxing method (a name of function to apply), e.g., [@("str")].
To solve the issue, this diff uses "unknownSelector:" instead of giving up the translation.
Reviewed By: dulmarod
Differential Revision: D18831844
fbshipit-source-id: b9324ba39
Summary: This enables us to quickly pick up the Component typ when checking which required props to check.
Reviewed By: skcho
Differential Revision: D18807925
fbshipit-source-id: 47e407394
Summary: This diff checks litho condition on the new abstract value. This is triggered with `--new-litho-domain`, but it is intra-procedural as of now.
Reviewed By: ezgicicek
Differential Revision: D18783203
fbshipit-source-id: 98570104e
Summary: This diff adds a map from an object to a set of methods that has been called.
Reviewed By: ezgicicek
Differential Revision: D18781461
fbshipit-source-id: 47c10adaa
Summary: This adds a map from access expressions to locations where specific object is created by `create` method call.
Reviewed By: ezgicicek
Differential Revision: D18779985
fbshipit-source-id: f327450cd
Summary: This diff stack is to revise overall domain and semantics of litho checker. Some of the following diffs will not have visible changes until we replace the current checker with the new one.
Reviewed By: ezgicicek
Differential Revision: D18779592
fbshipit-source-id: d210d9bd1
Summary:
This can happen for a number of reasons that are not errors (mostly the exit node being unreachable) so isn't actionable, and definitely not worth showing the user. It could be a debug message but I don't think that's even worth it. Other checkers don't warn in similar circumstances.
With OCaml 4.08 we started actually seeing these error messages (differences in flushing behaviour?) so their annoying nature was revealed.
Reviewed By: ngorogiannis
Differential Revision: D18808460
fbshipit-source-id: a47a1dcb4
Summary:
Also add logic for recognising excessive timeouts. Refactor the code
around timeouts a little.
Reviewed By: artempyanykh
Differential Revision: D18807836
fbshipit-source-id: df5a1b566
Artem Pyanykh
Sungkeun Cho
Jules Villard
Ezgi Çiçek
Nikos Gorogiannis
Mitya Lyubarskiy
Martin Trojer
Scott Owens