Summary:
Strengthen computation of solution substitutions used for existential
witnessing by using the solver for the memory contents theory. This
uses a generalization of the equation solver implementation which
accepts a predicate used as a filter for equations added to the
solution substitution. When used for solving for a given set of
variables, this filter excludes equations which do not meet the
desired variable conditions.
Reviewed By: jvillard
Differential Revision: D20120275
fbshipit-source-id: 4203d5e41
Summary:
Strengthen existential quantifier witnessing to enable witnessing an
existential with a term containing another existential if no universal
witness is available. Additionally, strengthen existential witnessing
to enable terms of interpreted theories to witness existential
variables.
Also strengthen and simplify the representation invariant checking for
existential witnessing code.
Reviewed By: jvillard
Differential Revision: D20120271
fbshipit-source-id: 4c44fe9ef
Summary:
Handle the case the universal context of a goal does not stay in sync
with that of the minuend.
The need for this indicates that there is some problematic redundancy
in the representation of solver goals.
Reviewed By: ngorogiannis
Differential Revision: D20120268
fbshipit-source-id: 44a4d6260
Summary:
It can happen that canonizing subterms can change the classification
of a term e.g. to the literal true. In such cases, it is not useful or
correct use `Equality.lookup` (which expects to only be used on
uninterpreted applications) to search for some other equation equal to
the literal and use its representative instead.
Reviewed By: ngorogiannis
Differential Revision: D20120279
fbshipit-source-id: 3e2160233
Summary: When equating Concat terms, drop any common prefix or suffix.
Reviewed By: ngorogiannis
Differential Revision: D20120264
fbshipit-source-id: afdeb990e
Summary: No code change, only reordering definitions in prep for later changes.
Reviewed By: ngorogiannis
Differential Revision: D20120263
fbshipit-source-id: b312dfc9a
Summary: Add `Equality.and_term` and replace most of `Sh.pure` with it.
Reviewed By: ngorogiannis
Differential Revision: D20029742
fbshipit-source-id: 07c2f1fe6
Summary:
Replace `Equality.Subst.trim` with `partition_valid` which has a
logical specification (and unsurprisingly fixes some corner case
bugs):
```
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν
are maximal where ∃ks. ν is universally valid, xs ⊇ ks and ks ∩
fv(τ) = ∅. *)
```
Reviewed By: ngorogiannis
Differential Revision: D20004974
fbshipit-source-id: 5cb3b3835
Summary:
Sh.var_strength determines, in part, if an existential variable has
only a single occurrence. The objective of this is to determine that a
variable is merely a placeholder and not used to express additional
constraints. For this, it suffices to check the weaker condition that
there is a single occurrence in each branch of a DNF expansion.
Reviewed By: ngorogiannis
Differential Revision: D19973779
fbshipit-source-id: 2c90c61f4
Summary:
The result of promoting expect tests is not necessarily formatted, so
try to reduce iterations by formatting after testing.
Reviewed By: ngorogiannis
Differential Revision: D20004973
fbshipit-source-id: 53af4c034
Summary:
This is so that all pre-analyses are together instead of spread across
several modules.
PS: this function is the worst.
Reviewed By: ngorogiannis
Differential Revision: D19973285
fbshipit-source-id: b326e99cd
Summary: Sometimes, we want to run/clean/replace tests for **only cost analysis**. Let's introduce a set of commands for this purpose.
Reviewed By: skcho
Differential Revision: D20141657
fbshipit-source-id: d0ad267b2
Summary:
The check for whether a buck target needs quoting is incorrect, since it uses `-` inside a character class to denote a dash, not a character range. The correct way to do this is to put the dash as the first character in the class (or last).
Facebook
iknowthis_regex
Reviewed By: jberdine
Differential Revision: D20159112
fbshipit-source-id: be6750ed8
Summary:
This diff renames `ZERO_XXX` issues to more appropriately named and descriptive
`XXX_UNREACHABLE_AT_EXIT` and replaces bottom with
unreachable in cost kinds and issues.
Reviewed By: skcho
Differential Revision: D20140301
fbshipit-source-id: eb6076b30
Summary:
1. It is convenient to stick with the policy "ERROR if and only if it is
enforced". Among other, it makes CI integration much easier to implement
(enforcemend, UI and messaging is decided based on severity).
2. Since Nullsafe annotation is an idiomatic way to indicate classes
with enforced nullability checking, we want it to be the only way to
enforce issues.
3. This means we decrease the priority of GraphQL violation issues.
(In practice they were not enforced so we have plenty of violations in
codebase to reflect reality). The proper way dealing with GraphQL will
be detecting such issues as a special issue type and prioritizing fixing
and Nullsafe-ifying corresponding classes.
4. Among other, we downgrade severity of field overannotated to advice
to keep it consistent with condition redundant.
Reviewed By: artempyanykh
Differential Revision: D20141420
fbshipit-source-id: e2f12835a
Summary:
The issue type `ZERO_EXECUTION_TIME` actually corresponds to bottom state but has been mistakenly used to mean
- unreachable nodes (program never reaching exit state)
- having zero cost (e.g. for allocations).
Note that, for execution costs, the latter doesn't make sense since we always incur a unit cost for the start node. Hence, a function with empty body will have unit cost. For allocations or IO however, we only incur costs for specific primitives, so a function with no allocations/IO could have a zero cost. However, there is no point reporting functions with zero cost as a specific issue type. Instead, what we want to track is the former, i.e. functions whose cost becomes 0 due to program never reaching exit state.
This diff aims to split these cases into two by only reporting on the latter and adds traces to bottom/unreachable cost by creating a special category in polynomials.
Next diff will rename `ZERO_XXX` to `XXX_UNREACHABLE_AT_EXIT`.
Reviewed By: skcho
Differential Revision: D20005774
fbshipit-source-id: 46b9abd5a
Summary: When the progress bar was off (`--no-progress-bar`) the `TaskBar` didn't log updates but the workers still sent them to the master process. Now, the workers no longer send updates to the master process when the progress bar is off.
Reviewed By: ngorogiannis
Differential Revision: D20140577
fbshipit-source-id: 560d56991
Summary:
For Mode.Local this is kind of obvious decision.
But this diff does the same for strict mode as well.
See comment in [ExplicitNonnullThirdParty] for the detailed explanation.
Reviewed By: artempyanykh
Differential Revision: D20140056
fbshipit-source-id: 13c66df81
Summary:
In the previos diff we restructured error rendering utils for
TypeOrigin.MethodCall.
In this diff we do the same with TypeOrigin field: lets make the code
consistent.
We also clearly distinct third party from all other possible cases in
this branch.
This changes messaging and reported errors for strict modes (see test cases), and I believe this is a net improvement.
Reviewed By: artempyanykh
Differential Revision: D20139741
fbshipit-source-id: 84f502553
Summary:
Since artempyanykh introduced proper type for third party methods, we don't need
to write a sketchy heuristic in this place.
This will simplify shipping a feature in the follow up diff (otherwise
it would break here).
Reviewed By: artempyanykh
Differential Revision: D20139460
fbshipit-source-id: 00144dc48
Summary:
> We don't report when the cost is Top as it corresponds to subsequent 'don't know's. Instead, we
> report Top cost only at the top level per function
The previous code just ignored top costed nodes, so it was able to report a non-top cost that was
from another node. For example,
```
void foo() {
linear-cost();
top-cost();
}
```
It reported inconsistent reports: `EXPENSIVE_EXECUTION_TIME` with a linear cost and
`INFINITE_EXECUTION_TIME` at the same time.
This diff fixes it not to report `EXPENSIVE_EXECUTION_TIME` when there is a node with the top cost.
Reviewed By: ezgicicek
Differential Revision: D20139408
fbshipit-source-id: 9fedd4aec
Summary:
In the previous report, it reported the first cost of node that exceeds a threshold. However, this
may hide a bigger cost of node that appears later. This diff changes this to report the biggest
cost of node among the costs exceeding the threshold.
Reviewed By: ezgicicek
Differential Revision: D20116162
fbshipit-source-id: 06199fb46
Summary: No need to print the whole trace when there are other ways to view it.
Reviewed By: jberdine
Differential Revision: D20138515
fbshipit-source-id: 9765db2f0
Summary: The analysis time wall time was logged but not it wasn't a part of `BackendStats`. The analysis time has metric has been moved to `BackendStats` and also includes the user and sys times of the scheduler process.
Reviewed By: ngorogiannis
Differential Revision: D20115345
fbshipit-source-id: bd3f3d276
Summary:
Current domain of Inferbo cannot handle float values. This diff evaluates float constants to the top
interval.
Reviewed By: ezgicicek
Differential Revision: D20116361
fbshipit-source-id: e6e398bbd
Summary:
This syntax
- is less confusing (according to several people who are not me);
objectively, there's less magic under the hood
- gives fine control over register number (because condition/action are separated)
- lets one compare values of different arguments of the same call
(e.g., one could have a transition that is taken only if two
arguments of a method call are equal)
Reviewed By: ngorogiannis
Differential Revision: D20005403
fbshipit-source-id: fad8f3b3d
Summary:
The test shows what that TOPL can express, in addition to bugs,
efficiency properties. However, there seems to be an underlying problem
in biabdaction that prevents this particular problem from being caught.
Reviewed By: ngorogiannis
Differential Revision: D20005404
fbshipit-source-id: 466f79050
Summary:
# Current design
Infer analysis is currently two staged:
1) proc-level callbacks calculate summary, including writing down the
issues if applicable.
2) file-level callbacks (formerly cluster callbacks, see the prev diff) are executed next; they are supposed to emit
additional issues that are impossible to emit based on mere
proc-context.
Currently RacerD and Starvation use file-level callback; in near future
we plan to onboard Nullsafe checker as well.
# Problem
Contract of callback (1) is clear: given a proc and existing
summary, the checker updates it and returns a modified summary. This
summary later on gets serialized (in-memory + external) and can be consumed by
other chechers. Issues written in summary will get reported when
analysis is over.
In constrast, contract of (2) is wild west: the function returns unit.
In practice, what the checkers do is create IssueLog and serialize it to
checker-specific directory.
Then another part of program (InferPrint.ml) knows about this side
effect, reads the error log for checkers and ultimately get it reported
together with errors written at stage (1).
This is problematic because it is hard to reason about the system and it
makes onboarding new checkers to (2) error-prone.
# This diff
This diff brings (2) on par with (1): now file-level callback has a
clear contract: it should be side effect free, and the only
responsibility is to fill out and return IssueLog.
Additionally, we make the notion of "checker-specific issue directory"
an official thing, so the checker only needs to specify the name,
everything else will be made automatically by orchestation layer,
including cleanup.
# Starvation
Implementing the new contract is starvation is possible and desirable, but involved: see comment
in the code, so we leave it up to the future work to fix that.
Reviewed By: ngorogiannis
Differential Revision: D20115024
fbshipit-source-id: fb2f9b7e6
Summary: Add the wall time to the ExecutionDuration. If this is not included we are not considering off-cpu time.
Reviewed By: ngorogiannis
Differential Revision: D20099667
fbshipit-source-id: 49dbfd739
Summary:
Currently the call graph of all captured procedures is loaded and then traversed to flag reachable procedures from modified files, followed by deleting the unflagged part, and unflagging the rest. This is a bit wasteful, and doesn't lend itself nicely to constructing directly the reverse call graph, which further diffs will do.
This diff loads all captured procedures and callees in a hashconsed table, and performs a BFS from procedures in modified files, to build the call graph in one pass.
Reviewed By: fgasperij
Differential Revision: D19888965
fbshipit-source-id: eeb59356e
Summary:
To ease scheduling, it would be best to only load the procnames of procedures that are (a) defined and (b) reachable from the modified files. The frontends play various games with the DB properties:
- In Clang all methods have a CFG even if they are undefined. Also, looking for non-NULL CFG rows in the DB brings up methods unreachable from modified files (?).
- In Java, some procedures have NULL CFGs. In addition, some of those have `attr_kind!=0`.
We only load those procedures that have both non-NULL CFGs and `attr_kind!=0`. That seems to give meaningful numbers, esp. wrt reachable procedures from files.
Reviewed By: jberdine
Differential Revision: D20068376
fbshipit-source-id: 992b65b4a
Summary: The semantics of the `values` function of Java enum class was missing, when it is called outside the class initializer. This diff gets the size of the enum elements from the summary of class initializer function, `<clinit>`.
Reviewed By: ezgicicek
Differential Revision: D20094880
fbshipit-source-id: 7362bba1c
Summary: We had no tests that resulted in `ZERO_EXECUTION_COST`. Let's fix that.
Reviewed By: skcho
Differential Revision: D20097504
fbshipit-source-id: 56c23fea0
Summary:
1. Some invariants are tricky enough to be documented. This is especially
important for cases related with error reporting. Lets document it.
2. Cluster callback -> File callback rename.
Reviewed By: ngorogiannis
Differential Revision: D20093932
fbshipit-source-id: e716f1f5b
Summary:
When trying to add annotations to code examples, Javadoc gets confused about `@` sign and there's no good way to fix it so it's both OK to read as a comment in the editor and as a Javadoc HTML, no matter what combination of <code>/<pre>/{code} or escaping you use.
Here we prioritise ability to read the code comment from the editor and therefore the comments are detached from annotations.
Facebook
Reviewed By: mityal
Differential Revision: D20093801
fbshipit-source-id: 25867c27a
Summary:
Now when typechecking a class `A` marked with `Nullsafe(LOCAL)`,
classes from trusted list are properly recognized and nullability of
method params and return value are refined to `LocallyCheckedNonnull`
in a context of class `A`.
NOTE: refininng nullability when **accessing fields** on trusted classes
is **not implemented yet**, because the whole business of handling fields
in nullsafe is somewhat convoluted. This should not be a huge issue
though, since in Java fields are commonly accessed via getters any
way.
Reviewed By: mityal
Differential Revision: D20056158
fbshipit-source-id: 496433d90
Summary:
This ignores the error memory status (e.g. when condition expression is evaluated to bottom), in
order to keep analyze following code.
```
if ( e ) // e is evaluated to bottom due to a problem of Inferbo {
... // code here was not analyzed before
}
```
Reviewed By: ezgicicek
Differential Revision: D20067434
fbshipit-source-id: a1713722c
Josh Berdine
Jules Villard
Dulma Churchill
Ezgi Çiçek
Nikos Gorogiannis
Mitya Lyubarskiy
Fernando Gasperi Jabalera
Sungkeun Cho
Radu Grigore
Artem Pyanykh
Artem Pianykh