Summary:
`ProcData.t` contains a `Summary.t`. Eventually we want to fix this too
so that checkers don't depend on backend/, i.e. on all the other
checkers via Summary.ml. But in order to migrate progressively we can
first migrate absint/ and one step on the way is for it to not know what
kind of analysis data it is passing around.
This extra flexibility only costs us passing an extra `Procdesc.t` in a
couple more functions so it's actually not a bad change in itself.
Reviewed By: ngorogiannis
Differential Revision: D21257466
fbshipit-source-id: a91f7b191
Summary:
This is a step in disentangling the various analyses: that file used to
make every checker on biabduction because of a few of its functions that
use biabduction datatypes.
Split reporting.ml into:
- Reporting.ml: the functions all checkers need to report errors. This
is put in absint/ with the other files that are needed by all
checkers.
- SummaryReporting.ml: functions that need to depend on Summary.ml
(useful for later). This is put in backend/ where Summary.ml lives.
- BiabductionReporting.ml: for the biabduction analysis
The rest of the changes are renames to use the appropriate module
amongst the above.
Reviewed By: ngorogiannis
Differential Revision: D21257468
fbshipit-source-id: fa28cefbc
Summary:
Previous implementation supported only stringy params (strings and
stringified bools). Current one exposes a proper variant `Annot.t`,
with support for all possible param values in Java except
numbers (more on that below).
This change is required for implementing `Nullsafe(LOCAL)` as the
annotation used to specify nullsafe behaviour has a more complex
structure than what we've dealt with before.
**Why support for number values was not added**: supporting numbers
requires using `int64`. Unfortunately, adding another variant `Vnum
int64` to `Annot.t` causes a runtime failure on assert in
`MaximumSharing.ml:133`. It seems that it might be enough to flip
`fail_on_nonstring` from `true` to `false`, but since this would
require additional testing and is not required for my case, I'll leave
checking this to whoever needs to use numeric annot params in future.
Reviewed By: ezgicicek
Differential Revision: D19855923
fbshipit-source-id: 878e33856
Summary:
The big one:
- stop using polymorphic `<>`, `<`, `>`, ..
- add `<>` to `PolyVariantEqual` escape hatch now that `<>` is as taboo as `=`
- Interestingly, there were a lot of uses of `Z.(x < y)`, which although
they seem to use `Z.lt` actually used polymorphic comparison. The actual
comparison infix operators of `Z` are cleverly hidden in `Z.Compare`
instead, which makes them impractical to use...
Reviewed By: jberdine
Differential Revision: D19861584
fbshipit-source-id: 5dce08ad9
Summary:
This diff avoids that null-retuned path's abstract value ruins that of non-null-returned path.
What this diff does is: when joining two abstract states, one is null-return-path and the other is
non-null-return-path (`return obj;`), it keeps the method calls of `obj` from the
non-null-return-path.
While this design is unsound, I think it should work in practice.
Reviewed By: ezgicicek
Differential Revision: D19348313
fbshipit-source-id: cf5d0f3ff
Summary: It is confusing to report missing props at the the beginning of the method (especially when there are many components created or when the method has many lines). Let's report them at create methods to better contextualize. Also, make the missing prop bold.
Reviewed By: skcho
Differential Revision: D19141135
fbshipit-source-id: a23d2e7c9
Summary:
We do not have the create method in the trace which makes it difficult to understand
- inter-procedural issues where create and prop setting are in different methods
- there are multiple create-build chains in a method
Let's add the create to the beginning of the trace. Moreover, let's simplify the prop printing to make traces easier to understand.
Reviewed By: ngorogiannis
Differential Revision: D19020213
fbshipit-source-id: 7f8a5d4ec
Summary: The new domain is much better than the old one. Let's kill the old one (along with old litho tests) and simplify things.
Reviewed By: skcho
Differential Revision: D18959627
fbshipit-source-id: df77ae20e
Summary:
Remove Clang and Java submodules of Typ.Fieldname. They are unnecessary and they reflect a fake dichotomy: there is only one fieldname type. To distinguish between fields of Java classes and other C constructs, there is a helper function provided, but the idea is simple: obtain the class type the field belongs to, and check if it's a Java class.
This diff still preserves behaviour, but removes as many functions as possible from the interface, to leave a small surface.
Reviewed By: mityal
Differential Revision: D18962423
fbshipit-source-id: ffe6933ee
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:
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: 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: 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: Due to the weakness of the analysis which can't detect side-effecting prop setting (e.g. as in `builder.prop1(..)`), we currently have many broken chains that do do have any `create` method in their prefixes. Let's not report on these broken chains.
Reviewed By: skcho
Differential Revision: D18503523
fbshipit-source-id: 7506e34b7
Summary:
We were not tracking static `create ` and `build` methods intra-procedurally in the analysis and we just looked up their summaries. This resulted in not having static `create` methods in the trace. Let's fix that by pushing static check into `satisfy_heuristic`.
This results in a few FPs, but such cases are not very common in the codebase.
Reviewed By: skcho
Differential Revision: D18451955
fbshipit-source-id: d4ccf46f5
Summary: We stop tracking at builder boundaries. Let's tract create methods as well so that trace is more informative.
Reviewed By: skcho
Differential Revision: D18038637
fbshipit-source-id: a99b6431f
Summary: Before, we didn't track litho framework callees on client code which was wrong. Now, we replace this with the following: If the callee is `build()` itself or doesn't contain a `build()` in its summary, then we want to track it in the domain. The former makes sense since we always want to track `build()` methods. The latter also makes sense since such a method could be a setter for a prop (as in the case of `prop1` in `buildPropLithoOK` which we were missing before due to the imprecise heuristic that prevented picking up callees in litho).
Reviewed By: ngorogiannis
Differential Revision: D17810704
fbshipit-source-id: 87d88e921
Summary:
Improve the trace by incorporating the callees and their locations in the call chain (i.e. chain of methods starting from `build()` call)
- extend the domain to contain the callee location
- replace the test results with the new traces
This makes our job much easier to debug FPs in a big codebase.
Reviewed By: skcho
Differential Revision: D17788996
fbshipit-source-id: 31938b5fe
Summary: `litho` checker contained two checkers: required-props and graphQL field accesses. Although they use the same domain, their reporting conditions and analysis details are different. However, they were bundled into the same analysis by adding disjunctions to `exec_instr` to handle both cases. Let's separate them into two different checkers, keeping a modular transfer function and analyzer that is reused by these two checkers.
Reviewed By: skcho
Differential Revision: D17788834
fbshipit-source-id: 47d77063b
Jules Villard
Ezgi Çiçek
Artem Pianykh
Sungkeun Cho
Nikos Gorogiannis
Josh Berdine