Summary:
Change Arith.map to not descend through non-interpreted arithmetic
operators. For example, in `2×(x × y) + 3×z + 4`, `map ~f` will apply
`f` to the subterms `x × y` and `z`, but not `x` or `y`.
The logical notion of "subterm" that is needed by the solver does not
coincide with the representation. This is essentially due to not
"flattening" or "purifying" terms. That is, traditionally `x × y`
would not be permitted as an indeterminate of a polynomial. Instead, a
new variable would need to be introduced: `v = x × y` and then the
polynomial would be expressed as `2×v + 3×z + 4`. Taking maximal
non-interpreted subterms as the definition of "subterm" results in
subterms in the non-flattened representation that are equivalent to
those that would result from flattening the representation.
Reviewed By: jvillard
Differential Revision: D24746235
fbshipit-source-id: d8fcf46a1
Summary:
The implementation of Arithmetic relies on the partial projection from
terms to polynomials. This diff enables it to also embed polynomials
back into terms.
Reviewed By: jvillard
Differential Revision: D24746223
fbshipit-source-id: b6010e7b7
Summary:
Add a distinction between interpreted and uninterpreted arithmetic
terms, and use it in Context.classify. This enables correctly
classifying non-linear terms such as `x × y` as uninterpreted.
Reviewed By: ngorogiannis
Differential Revision: D24746228
fbshipit-source-id: 1a4b0e3bd
Summary:
It was possible for the scope of existentials to be violated. In
particular, before this diff the order of re-quantifying the
existentials and conjoining the non-eliminated equations from the
solution of solving for existentials was wrong.
Reviewed By: ngorogiannis
Differential Revision: D24746231
fbshipit-source-id: d96cc60a6
Summary: In cpp, lambda's operator() name includes line and column numbers which were not ignore in proc name when computing bug hash.
Reviewed By: ngorogiannis
Differential Revision: D24890545
fbshipit-source-id: 95e6735f3
Summary:
As per title, plus de-quadratic-ify substitution of actuals into formals.
Also, fix a bug in treatment of callee summaries where the caller lock state was updated first and then used to process accesses in the callee (so should only take into account the original caller state).
Reviewed By: jvillard
Differential Revision: D24857922
fbshipit-source-id: 07ce6999c
Summary:
Otherwise this gets serialized in an unconventional way; `nullable` serializes it as a
standard `null` or string value.
Reviewed By: artempyanykh
Differential Revision: D24827593
fbshipit-source-id: a5a9afc80
Summary: As per title, plus minor improvements in interfaces and a couple of FIXMEs.
Reviewed By: skcho
Differential Revision: D24836125
fbshipit-source-id: f7a4dc196
Summary:
The starvation domain keeps a domain element per distinct pair of lock object and source location. This was used to counteract the imprecision of implicit Quandary-style traces. Starvation has used explicit traces for a long time now, so keeping all these elements is expensive (in fact, in some cases exponential) and of no value. Now, lock object identity is the only distinguishing feature of a domain element.
Also, fix some pretty printing for debugging purposes.
Reviewed By: jvillard
Differential Revision: D24829306
fbshipit-source-id: 22e12f9c1
Summary:
This diff fixes `degree_with_term` to ignore function pointer symbols. `degree_with_term` does
* calculate the degree
* simplify the polynomial only for printing them to users
thus, there is no problem to ignore the function pointer symbols always, ie which does not affect semantics or summary values.
Reviewed By: ezgicicek
Differential Revision: D24596479
fbshipit-source-id: 1e29d2de0
Summary: We recently introduced a more precise model for constructing an optional from a value by making a shallow copy. However, this introduced Use After Delete false positives. For now, we go back to a less precise model by creating a fresh value. A proper model would be to either make a deep copy or call the copy constructor for a value. We will address this in the following diff.
Reviewed By: jvillard
Differential Revision: D24826749
fbshipit-source-id: 3e5e4edeb
Summary: Refactor `folly::Optional` models to make them easier to reuse for `std::optional`
Reviewed By: jvillard
Differential Revision: D24760053
fbshipit-source-id: f665e84c8
Summary:
- log trans_state for each instruction
- create boxes to indent logs
- hunt down "@." that would prematurely close the boxes
- improve messages
Reviewed By: ngorogiannis
Differential Revision: D24794798
fbshipit-source-id: 80d51a8c5
Summary:
They are indirectly encoded in "procedure" field already, but:
1/ To extract name and params one needs to parse the procedure on the
client side
2/ We already have class, package, and field: method and its params is a
consistent change
Reviewed By: artempyanykh
Differential Revision: D24731064
fbshipit-source-id: fae478e7e
Summary:
If the issue one of:
- Field Not Nullable
- Field Not Initialized
- Field Overannotated,
we record field_name to .json result.
NoTE: Design choice for representation. For Field Not Initialized and Field Overannotated
this is always internal (relative to the class) field, but for Field Not
Nullable it can be either internal or external. We could have a
structured output, or always output full name. I preferred to output
short name for convenience of the main usacase I am anticipating.
NOTE: not to be confused with the case where the field is nullable but
we e.g. try to dereference it. This is indirectly related to the issue
(can be several such fields for starters) and if we one day output it,
it will be provided in a separate way (similarly to how we output
nullable_methods).
Reviewed By: artempyanykh
Differential Revision: D24730320
fbshipit-source-id: c995ec221
Summary:
We never tested params dependent on things (tested only things dependend
on params).
Reviewed By: artempyanykh
Differential Revision: D24726858
fbshipit-source-id: a0861cfc3
Summary:
Since we report issues types without a prefix (e.g. ERADICATE_) and
with spaces we should also allow for prefix-less issue types in
SuppressLint, so both should work
- SuppressLint("eradicate-field-not-initialized")
- SuppressLint("Field Not Initialized")
Reviewed By: jvillard
Differential Revision: D24760341
fbshipit-source-id: 1590cf6d0
Summary:
In the process of computing `Context.solve`, fresh variables can be
generated. Not all of these end up in the final solution
substitution. Currently all of the freshly generated variables are
returned to the client, which leads to extraneous existentials. This
diff trims the returned fresh variables to only those that appear in
the final solution.
Reviewed By: ngorogiannis
Differential Revision: D24746241
fbshipit-source-id: 59a2f221b
Summary:
Since floats of any width are interpreted the same (as exact rationals
where possible and uninterpreted constants otherwise), this does not
introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746225
fbshipit-source-id: bc8e7bdb9
Summary:
Since non-integral address spaces are not currently supported anyhow,
this does not introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746234
fbshipit-source-id: 1f6887a78
Summary: Just to make the source and destination types of the conversion more clear.
Reviewed By: da319
Differential Revision: D24746239
fbshipit-source-id: 592c7d0f1
Summary:
Since Context treats only equality directly, formulas involving other
literals can normalize to false when the context is not unsat. This
diff changes Sh.star to check this case, and return the canonical
false symbolic heap.
Reviewed By: da319
Differential Revision: D24746227
fbshipit-source-id: 50a51b8a6
Summary:
- Treat missing baseline files as if empty
- Only filter unchanged results if a baseline file is given
- Minor optimization
- Sort multiple statuses
- Fix total computation
- List tests with failing statues first
- Do not use `Format.formatter_of_out_channel` since it sometimes does
not work for some unknown reason, e.g. when the output should have
only one line, none are emitted.
Reviewed By: da319
Differential Revision: D24746236
fbshipit-source-id: f4ead1531
Summary:
There is a feature in Nullsafe that is interfering with "annotation
graph" feature. Because of this we would not detect provisional
violations for misuses of params of equals() (They will be recorded
as user facing rather than provisional issues).
This diff turns this feature off for annotation graph mode.
Reviewed By: artempyanykh
Differential Revision: D24726655
fbshipit-source-id: 4b7577667
Summary:
Virtual "this" invisible param exists in the annotated signature, but
does not exist in some other places, which causes a lot of annoyance in
different places.
This diff does not intend to solve all this, but makes one step forward.
1/ AnnotatedNullability now explicitly distincts normal params and
VirtualThis.
2/ AnnotatedSignature accounts for this via: a) not having redundant
fake annotation points b) having corrent param indices (those were off
by 1 in non-virtul methods).
Reviewed By: artempyanykh
Differential Revision: D24726480
fbshipit-source-id: fdb8bb0fb
Summary: This is a complex enough feature so iterating on it in a safe manner will be useful.
Reviewed By: artempyanykh
Differential Revision: D24725406
fbshipit-source-id: 81b247143
Summary: `folly::Optional::value()` returns a reference, hence an error was shown when the actual value was being accessed. Since `value()` throws an exception in case of `folly::none`, we want to show the error message at the call site of `value()`. We do this by dereferencing the result of `value()` in the model.
Reviewed By: jvillard
Differential Revision: D24702875
fbshipit-source-id: ca9f30349
Summary:
This is needed for `infer reportdiff` to report issues that are in files
in the same workspace but were captured under a different project root,
but it's also legit to do so in general as "under project root" really
means "this file belongs to the project under analysis".
Reviewed By: martintrojer
Differential Revision: D24755592
fbshipit-source-id: fa8fab127
Summary: In cpp, lambda's `operator()` name includes line and column numbers which were not ignore when computing bug hash.
Reviewed By: jberdine
Differential Revision: D24649125
fbshipit-source-id: 7a235fd3e
Summary: Includes all changes made from the last time of `make doc-publish`
Reviewed By: jvillard
Differential Revision: D24728644
fbshipit-source-id: c0006a8dd
Summary:
The problem in Reporting.ml:log_issue_from_summary is that it merely
checks the presence of `SuppressLint` annotation on method's body to
decide whether to log or not the issue. This means that regardless of
issue types specified in `SuppressLint`, all issues on such method will
get blocked.
Here we fix that.
Reviewed By: ngorogiannis, mityal
Differential Revision: D24726604
fbshipit-source-id: c9cae3833
Summary:
This diff glues the previous work together.
The ClassLevelAnalysis finds list of provisional violation, builds the
graph based on them, and outputs this graph as a separate issue.
Reviewed By: artempyanykh
Differential Revision: D24682802
fbshipit-source-id: 8174da91a
Summary:
When exceptions are used due to the lack of goto, use `raise_notrace`
instead of `raise` to avoid the overhead of populating the backtrace.
Reviewed By: ngorogiannis
Differential Revision: D24630525
fbshipit-source-id: c5051d9c4
Summary:
Adding quotes is needed only to avoid clashes between LLVM integer
literals and anonmous value names.
Reviewed By: ngorogiannis
Differential Revision: D24630527
fbshipit-source-id: 97339740c
Josh Berdine
Ezgi Çiçek
Daiva Naudziuniene
Nikos Gorogiannis
Sungkeun Cho
Mitya Lyubarskiy
Jules Villard
Artem Pianykh