Summary:
`AnalysisCallbacks.proc_resolve_attributes` introduces non-determinism because it first looks for the attributes in a (procdesc in a) summary and if it doesn't find it then returns the value in the attribute column from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc in some cases.
The plan is to eliminate these calls one by one, replacing with `Attributes.load` which only looks at the capture DB attribute column.
Reviewed By: skcho
Differential Revision: D29817582
fbshipit-source-id: 24f9dfcc3
Summary:
`AnalysisCallbacks.proc_resolve_attributes` introduces non-determinism because it first looks for the attributes in a (procdesc in a) summary and if it doesn't find it then returns the value in the attribute column from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc in some cases.
The plan is to eliminate these calls one by one, replacing with `Attributes.load` which only looks at the capture DB attribute column.
Reviewed By: skcho
Differential Revision: D29817404
fbshipit-source-id: b3fe8ec4d
Summary:
`AnalysisCallbacks.proc_resolve_attributes` introduces non-determinism because it first looks for the attributes in a (procdesc in a) summary and if it doesn't find it then returns the value in the attribute column from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc in some cases.
The plan is to eliminate these calls one by one, replacing with `Attributes.load` which only looks at the capture DB attribute column.
Reviewed By: skcho
Differential Revision: D29816458
fbshipit-source-id: 681c55f4c
Summary:
`AnalysisCallbacks.proc_resolve_attributes` introduces non-determinism because it first looks for the attributes in a (procdesc in a) summary and if it doesn't find it then returns the value in the attribute column from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc in some cases.
The plan is to eliminate these calls one by one, replacing with `Attributes.load` which only looks at the capture DB attribute column.
Reviewed By: skcho
Differential Revision: D29816411
fbshipit-source-id: d06c4bd48
Summary:
`AnalysisCallbacks.proc_resolve_attributes` introduces non-determinism because it first looks for the attributes in a (procdesc in a) summary and if it doesn't find it then returns the value in the attribute column from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc in some cases.
The plan is to eliminate these calls one by one, replacing with `Attributes.load` which only looks at the capture DB attribute column.
Reviewed By: skcho
Differential Revision: D29816181
fbshipit-source-id: e7a2f809c
Summary: Add support for the xor operator by reducing `(X xor Y)` to `(X and not Y) or (not X and Y)`. Alternatively, `(X != Y)` could have been used but that might not be safe since SIL models Booleans with integers.
Reviewed By: skcho
Differential Revision: D29816793
fbshipit-source-id: 2496b718b
Summary: Add support for short circuit counterparts (andalso, orelse) of the logic operators (and, or).
Reviewed By: skcho
Differential Revision: D29815177
fbshipit-source-id: 98d28deed
Summary: There are multiple operators in Erlang that require special treatment and cannot be simply mapped to a SIL operator (for example andalso, orelse, exactly equal, xor). Therefore it is not practical to have a helper function mapping these operators to SIL operators.
Reviewed By: skcho
Differential Revision: D29814373
fbshipit-source-id: 892219fd3
Summary: Pulse evaluated (e1+e2) as a new value that is a sum of evaluation results of e1 and e2. However, when e2 is known as zero, we can have a simpler evaluation result without introducing the new value. This diff returns the evaluation result of e1 when e2 is known as zero.
Reviewed By: ngorogiannis
Differential Revision: D29736444
fbshipit-source-id: d5ce5a60e
Summary:
This call back introduces non-determinism because it first looks for the proc desc in a summary and if it doesn't find it then returns the one from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc potentially.
The plan is to eliminate these calls one by one using the CI for correctness.
Reviewed By: skcho
Differential Revision: D29792603
fbshipit-source-id: 129054541
Summary:
This call back introduces non-determinism because it first looks for the proc desc in a summary and if it doesn't find it then returns the one from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc potentially.
The plan is to eliminate these calls one by one using the CI for correctness.
Reviewed By: skcho
Differential Revision: D29793530
fbshipit-source-id: 6d9269cee
Summary:
This call back introduces non-determinism because it first looks for the proc desc in a summary and if it doesn't find it then returns the one from the capture DB.
The problem is:
- the main factor affecting the existence of a summary on-disk is timing;
- the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not;
- this extends to the attributes included in the proc desc potentially.
The plan is to eliminate these calls one by one using the CI for correctness.
Reviewed By: skcho
Differential Revision: D29792757
fbshipit-source-id: 744472950
Summary: Previously we just reported NONEXHAUSTIVE_PATTERN_MATCH, which was (1) not correct because not only patterns can cause nonexhaustive behavior, but also guards, and (2) the Erlang runtime reports errors more precisely, indicating whether the nonexhaustive behavior occurs with `if`, `case`, functions or match expressions.
Reviewed By: rgrig
Differential Revision: D29681637
fbshipit-source-id: 74a25b371
Summary:
This fixes a bug that caused imprecise tracking of dynamic types.
Suppose we knew
term_eqs:
(x instanceof T)=v1
(y instanceof T)=v2
0=v2
attrs:
x has DynamicType T
y has DynamicType T
The simplification used to produce
term_eqs:
1=v1
0=v2
That's because term_eqs is a map and 1 can appear at most once as a key.
Note that the missing fact (1=v2) contradicts (0=v2). The imprecision
came from not noticing such contradictions. Most of these imprecisions
were observed in Erlang tests.
The fix is to go from using Term.VarMap to the smarter functions in
PulseFormula.Normalizer.
Reviewed By: jvillard
Differential Revision: D29541209
fbshipit-source-id: e4e077c87
Summary: Add support for guards, both in function clauses and case clauses.
Reviewed By: rgrig
Differential Revision: D29634937
fbshipit-source-id: 5a9f8ec2d
Summary: Small refactor to make the code more readable and possibly reusable in the future.
Reviewed By: rgrig
Differential Revision: D29614102
fbshipit-source-id: 3173b945a
Summary: Add support for *unary minus* and *logical not* in the Erlang translation, both as expression (e.g., `X = -Y`) and pattern (e.g., `case X of -3 -> ...`).
Reviewed By: rgrig
Differential Revision: D29582176
fbshipit-source-id: 17ef89496
Summary: The --suffix option of mktemp is not available on macos. Changed to rename the temp file created by adding the extension.
Reviewed By: skcho
Differential Revision: D29587977
fbshipit-source-id: b7a5adda8
Summary: Group tests based on the different constructs: functions, case expressions and match expressions.
Reviewed By: rgrig
Differential Revision: D29559982
fbshipit-source-id: eb645ed8d
Summary: Add some tests for binary expressions. The idea is that tests come in pairs: in both cases we do the same calculations, one is asserting the good result and one is not, where only the latter should trigger a warning.
Reviewed By: rgrig
Differential Revision: D29556364
fbshipit-source-id: 5b601d141
Summary:
The creation of the inital state has evolved several times recently,
time for a refactor:
- do not create then pass the initial state around when callees can
create it instead
- slightly hackish assertions that creating the initial state conditions
cannot fail to simplify the types (could eventually be moved in
AbductiveDomain.ml to avoid breaking abstraction layers like this, but
trivial enough that it doesn't really matter I think)
Reviewed By: skcho
Differential Revision: D29550319
fbshipit-source-id: 63919ae71
Summary:
This way we don't rely on existing summaries already having a
MustBeValid for self and on them having possibly other conditions that
might prevent a report.
Reviewed By: skcho
Differential Revision: D29550321
fbshipit-source-id: b9822fcd4
Summary: Typ.pp does not print types by default, use Typ.pp_full instead.
Reviewed By: ngorogiannis
Differential Revision: D29557158
fbshipit-source-id: 62ae20bd5
Summary:
Before, atoms we didn't understand but could be a contradiction became
"true" if they were only about dead variables. This is unsound for
incorrectness logic, and introduces false positives.
Be more conservative and try to identify when that could happen and
prune these paths instead, thus regaining under-approximation.
This is a bit ad-hoc: we expect reasoning on equalities and
disequalities to be precise enough, but we know that inequalities have
very little solving power at the moment (eg we don't detect `x < 0, x >
0 => false`). In addition, we remark that having *one* `<` atom can
never be a contradiction. So, we claim a possible contradiction whenever
we find *two* (>1) atoms containing inequalities and involving the same
variable.
Reviewed By: skcho
Differential Revision: D29232544
fbshipit-source-id: ff91eb1e4
Summary: Add some test cases to potentially non-exhaustive case clauses.
Reviewed By: rgrig
Differential Revision: D29555525
fbshipit-source-id: f710e93e6
Summary: New inferconfig flags which will pass through to buck config flags. Purpose is to allow using a buck target to distribute and use infer binaries as a buck toolchain.
Reviewed By: martintrojer
Differential Revision: D29485801
fbshipit-source-id: 86169cdae
Summary: If a test function `F` has multiple calls to a possibly problematic function `G`, our current expected output does not tell exactly which call to `G` causes the problem. This diff splits up such functions `F` into smaller parts `F1`, `F2`, ..., so that each part only calls `G` once. This way our expected output can match more precisely.
Reviewed By: rgrig
Differential Revision: D29554848
fbshipit-source-id: bdc62731c
Summary:
"glue" together the trace from the caller with the trace from the callee
to form the access trace when applying LatentInvalidAccess summaries.
This is consistent with what happens in function calls and allows Pulse
to better keep track of the history of the value. The goal is to prevent
bugs from getting filtered out because the access trace doesn't contain
the invalidation event for the value.
Reviewed By: da319
Differential Revision: D29550320
fbshipit-source-id: b600c188d
Summary:
There should be no change in semantics:
- before: the "crash node" modelling throwing an exception was connected directly to the exit of the procedure
- now: the "crash node" goes to exit_failure, which should end up being connected to the exit of the procedure by the `translate_one_function`
The latter is closer to what we'd need to do when we eventually model
throwing and catching exceptions (rather than just reporting an error
the moment we see them thrown).
Differential Revision: D29540834
fbshipit-source-id: c4de4c391
Summary:
Topl matches procedure names against whatever Procname.hashable_name
returns. For Java, it returns something like "java.util.ArrayList.add(...)",
but for Erlang it used to return something like "add/1": no module and
no parenthesis after. Now, Erlang returns "lists:add/1"; that is, it
includes module name. Also, Topl doesn't insist anymore on having a
paranthesis after the name.
Differential Revision: D29520365
fbshipit-source-id: d23be1cc8
Summary: `call-graph-schedule` was a boolean, now we have a variant type for scheduler.
Reviewed By: jvillard
Differential Revision: D29547773
fbshipit-source-id: ec787065c
Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
- __erlang_make_nil, for creating an empty list like []
- __erlang_make_cons, for creating a nonempty list like [1|[]]
- __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.
The diff also includes a test.
And also a few bugfixes:
- a type ErlangAny was used sometimes instead of ErlangAny*
- a load that was meant to be n=13 was instead n=*13;
changed to (*tmp=13; n=*tmp)
- the Makefile's guard for the rebar build-system test was inside the large
guard for java analyzers; of course, we don't need java to run rebar
Reviewed By: jvillard
Differential Revision: D29230161
fbshipit-source-id: c8fd6d88a
Summary: Adding more logging for cases where we see a lock/unlock but we see no arguments.
Reviewed By: skcho
Differential Revision: D29427413
fbshipit-source-id: 58b76b865
Summary: Add support for translating binary expressions, and implement a few operators.
Reviewed By: rgrig
Differential Revision: D29452471
fbshipit-source-id: d7c25ae91
Summary: Extract helper methods related to block creation into a module.
Reviewed By: rgrig
Differential Revision: D29436139
fbshipit-source-id: 92f9466d3
Summary: Add support for translating case expressions (without guards yet) and integer literals (including in patterns). Note that we use the same infrastructure for case expressions and function clauses, so adding support for guards will only have to be implemented once.
Reviewed By: rgrig
Differential Revision: D29424141
fbshipit-source-id: 0d6f1e661
Summary: Flag defaults to false. (For now, only the buck integration supports capturing any Kotlin.)
Reviewed By: jvillard
Differential Revision: D29388274
fbshipit-source-id: 8dbec9555
Summary: Adding constraint `self > 0` after computing specs for Objective-C instance methods were causing false positives of the heuristics not to discard `self=0 /\ self|->-` (added new test testAnotherObjectUseSelfOk was FP). This diff adds constrain `self > 0` before computing Objective-C specs, discarding unsatisfiable `self > 0 /\ self =0`.
Reviewed By: skcho
Differential Revision: D29462462
fbshipit-source-id: 088ee447e
Summary: Useful to write other tests, and also probably worth modelling.
Reviewed By: ezgicicek
Differential Revision: D29232545
fbshipit-source-id: ecb24f6f7
Nikos Gorogiannis
Akos Hajdu
Sungkeun Cho
Radu Grigore
Loc Le
Matthew Jin
Matteo Marescotti
Jules Villard
Daiva Naudziuniene