Summary:
`AnalysisCallbacks.get_proc_desc` potentially introduces non-determinism because it first looks for the `proc_desc` in the capture DB and if absent it tries to retrieve it from a summary.
The problem is the two proc descs are generally different, as the one in the summary is preanalysed and the one in the capture DB is not.
Unless the caller specifically needs a preanalysed `procdesc`, calls to `AnalysisCallbacks.get_proc_desc` should be replaced with `Procdesc.load`.
Reviewed By: skcho
Differential Revision: D29826482
fbshipit-source-id: f8c7cb243
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:
Bumps [ssri](https://github.com/npm/ssri) from 6.0.1 to 6.0.2.
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a href="https://github.com/npm/ssri/blob/v6.0.2/CHANGELOG.md">ssri's changelog</a>.</em></p>
<blockquote>
<h2><a href="https://github.com/zkat/ssri/compare/v6.0.1...v6.0.2">6.0.2</a> (2021-04-07)</h2>
<h3>Bug Fixes</h3>
<ul>
<li>backport regex change from 8.0.1 (<a href="https://github.com/zkat/ssri/commit/b30dfdb">b30dfdb</a>), closes <a href="https://github-redirect.dependabot.com/zkat/ssri/issues/19">https://github.com/facebook/infer/issues/19</a></li>
</ul>
<p><!-- raw HTML omitted --><!-- raw HTML omitted --></p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a href="b7c8c7c61d"><code>b7c8c7c</code></a> chore(release): 6.0.2</li>
<li><a href="b30dfdb00b"><code>b30dfdb</code></a> fix: backport regex change from 8.0.1</li>
<li>See full diff in <a href="https://github.com/npm/ssri/compare/v6.0.1...v6.0.2">compare view</a></li>
</ul>
</details>
<details>
<summary>Maintainer changes</summary>
<p>This version was pushed to npm by <a href="https://www.npmjs.com/~nlf">nlf</a>, a new releaser for ssri since your current version.</p>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `dependabot rebase` will rebase this PR
- `dependabot recreate` will recreate this PR, overwriting any edits that have been made to it
- `dependabot merge` will merge this PR after your CI passes on it
- `dependabot squash and merge` will squash and merge this PR after your CI passes on it
- `dependabot cancel merge` will cancel a previously requested merge and block automerging
- `dependabot reopen` will reopen this PR if it is closed
- `dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
- `dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
- `dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
- `dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
- `dependabot use these labels` will set the current labels as the default for future PRs for this repo and language
- `dependabot use these reviewers` will set the current reviewers as the default for future PRs for this repo and language
- `dependabot use these assignees` will set the current assignees as the default for future PRs for this repo and language
- `dependabot use this milestone` will set the current milestone as the default for future PRs for this repo and language
You can disable automated security fix PRs for this repo from the [Security Alerts page](https://github.com/facebook/infer/network/alerts).
</details>
Pull Request resolved: https://github.com/facebook/infer/pull/1468
Reviewed By: ngorogiannis
Differential Revision: D29613083
Pulled By: jvillard
fbshipit-source-id: dc9d789d0
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:
This diff changes the analysis exploration algorithm from considering
only sequential executions to considering executions of the
interleaving semantics. As part of this, symbolic states are changed
so that each thread has its own registers, while all memory is shared
between them.
Currently only a simple threads interface is supported: they can be
created with `thread_create(&thread_routine)`, they can exit by
returning from `thread_routine`, and they can be joined with
`thread_join`. Current simplifications include that newly created
threads are already runnable, thread routines accept no arguments and
return no result, and no failures are possible.
The concurrent exploration algorithm gives preference to executions
which have fewer context switches, thereby performing an incremental
form of context-bounded analysis.
A form of partial-order reduction is performed, where the symbolic
states are joined across (prefixes of) executions with the same number
of context switches which reach a point where the instruction pointers
and call stacks of all threads are the same. This has the effect of
"dagifying" the concurrent execution tree by merging points after
e.g. threads perform actions that commute with each other. This is
unlike traditional partial-order reduction in that it relies on the
symbolic join to combine the results of commuting operations in a way
that the following symbolic execution can take advantage of, rather
than performing some up-front analysis to identify commuting
operations and quotienting the space of executions. The current state
of the symbolic join and execution is significantly suboptimal in this
regard.
Differential Revision: D29441149
fbshipit-source-id: cf801a6b1
Summary:
This diff reworks the analysis scheduler to explicitly use a notion of
"abstract machine state" which makes the distinction with the state of
the analysis exploration algorithm more clear. The instruction
pointer, call stack, symbolic state, and retreating edge depths were,
prior to this change, passed individually to the various `exec_*`
functions. After this change, all this information is combined into an
abstract machine state value.
Additionally, this change explicitly factors out the commonality
between abstract machine states, on which symbolic execution operates,
and the elements of the frontier of exploration, that the analysis
scheduler maintaines. In short, an element of the frontier is simply
an abstract machine state with a control-flow edge instead of an
instruction pointer.
This change is almost entirely a non-functional refactoring. While
this serves as an improvement in code clarity, the main motivation is
that it establishes a code structure which minimizes the structural
changes needed when adding the concurrency analysis.
Differential Revision: D29441152
fbshipit-source-id: 01be87d4e
Nikos Gorogiannis
Akos Hajdu
Sungkeun Cho
Radu Grigore
Loc Le
dependabot[bot]
Matthew Jin
Vladislav Prekel
Matteo Marescotti
Jules Villard
Daiva Naudziuniene
Josh Berdine
