Commit Graph

8 Commits

Author SHA1 Message Date
Adam Balogh 471d0864df lyzer] [HOTFIX!] SValBuilder crash when `aggressive-binary-operation-simplification` enabled
During the review of D41938 a condition check with an early exit accidentally
slipped into a branch, leaving the other branch unprotected. This may result in
an assertion later on. This hotfix moves this contition check outside of the
branch.

Differential Revision: https://reviews.llvm.org/D55051

llvm-svn: 347981
2018-11-30 10:37:44 +00:00
Artem Dergachev e527df03c4 [analyzer] Add a testing facility for testing relationships between symbols.
Tests introduced in r329780 was disabled in r342317 because these tests
were accidentally testing dump infrastructure, when all they cared about was
how symbols relate to each other. So when dump infrastructure changed,
tests became annoying to maintain.

Add a new feature to ExprInspection: clang_analyzer_denote() and
clang_analyzer_explain(). The former adds a notation to a symbol, the latter
expresses another symbol in terms of previously denoted symbols.

It's currently a bit wonky - doesn't print parentheses and only supports
denoting atomic symbols. But it's even more readable that way.

Differential Revision: https://reviews.llvm.org/D52133

llvm-svn: 343048
2018-09-25 23:50:53 +00:00
George Karpenkov c40719e335 [analyzer] Temporary disabling svalbuilder-rearrange-comparisons test
As debug printing has changed, and format was not guaranteed to be
stable.
Artem is currently working on a better solution.

llvm-svn: 342317
2018-09-15 02:35:06 +00:00
George Karpenkov a393e68b27 [analyzer] Move analyzer-eagerly-assume to AnalyzerOptions, enable by default
Differential Revision: https://reviews.llvm.org/D51251

llvm-svn: 340963
2018-08-29 20:29:17 +00:00
Adam Balogh dcde8acc32 [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions
Patch https://reviews.llvm.org/rC329780 not only rearranges comparisons but
also binary expressions. This latter behavior is not protected by the analyzer
option. Hower, since no complexity threshold is enforced to the symbols this
may result in exponential execution time if the expressions are too complex:
https://bugs.llvm.org/show_bug.cgi?id=38208. For a quick fix we extended the
analyzer option to also cover the additive cases.

This is only a temporary fix, the final solution should be enforcing the
complexity threshold to the symbols.

Differential Revision: https://reviews.llvm.org/D49536

llvm-svn: 337678
2018-07-23 10:50:20 +00:00
Mikhail R. Gadelha e254b0f8c7 [analyzer] Fix constraint being dropped when analyzing a program without taint tracking enabled
Summary:
This patch removes the constraint dropping when taint tracking is disabled.

It also voids the crash reported in D28953 by treating a SymSymExpr with non pointer symbols as an opaque expression.

Updated the regressions and verifying the big projects now; I'll update here when they're done.

Based on the discussion on the mailing list and the patches by @ddcc.

Reviewers: george.karpenkov, NoQ, ddcc, baloghadamsoftware

Reviewed By: george.karpenkov

Subscribers: delcypher, llvm-commits, rnkovacs, xazax.hun, szepet, a.sidorin, ddcc

Differential Revision: https://reviews.llvm.org/D48650

llvm-svn: 337167
2018-07-16 13:14:46 +00:00
Adam Balogh 13e186c088 [Analyzer] Fix for SValBuilder expressions rearrangement
Expression rearrangement in SValBuilder (see rL329780) crashes with an assert if the type of the integer is different from the type of the symbol. This fix adds a check that prevents rearrangement in such cases.

Differential Revision: https://reviews.llvm.org/D45557

llvm-svn: 330064
2018-04-13 20:23:02 +00:00
Adam Balogh 2bbccca9f7 [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. A + n >= B + m becomes A - B >= m - n which enables the constraint manager to store a range m - n .. MAX_VALUE for the symbolic expression A - B. This can be used later to check whether e.g. A + k == B + l can be true, which is also rearranged to A - B == l - k so the constraint manager can check whether l - k is in the range (thus greater than or equal to m - n).

The restriction in this version is the the rearrangement happens only if both the symbols and the concrete integers are within the range [min/4 .. max/4] where min and max are the minimal and maximal values of their type.

The rearrangement is not enabled by default. It has to be enabled by using -analyzer-config aggressive-relational-comparison-simplification=true.

Co-author of this patch is Artem Dergachev (NoQ).

Differential Revision: https://reviews.llvm.org/D41938

llvm-svn: 329780
2018-04-11 06:21:12 +00:00