Re: r329780 - [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

2018-04-16 Thread Artem Dergachev via cfe-commits 
That's a combination of the simplifySVal() mechanism and the new 
rearrangement mechanism that causes the regression. I guess that's where 
we get when we try to squeeze more stuff into our solver. It seems safe 
to reduce simplifySVal() complexity threshold to 10 or 20 but i'm also 
curious whether something could be fixed in the rearrangement algorithm 
(probably it also needs a threshold?). I'll see what i can do, but i'll 
be relatively busy this week.


On 4/16/18 5:39 AM, Mikael Holmén wrote:

Hi Adam and Artem,

If I run

clang-tidy -header-filter=.\* 
-checks=clang-analyzer-\*,-clang-analyzer-unix\*,-clang-analyzer-osx\*,-clang-analyzer-security\*,-clang-analyzer-valist\*,-clang-analyzer-optin\*,-clang-analyzer-nullability\*,-clang-analyzer-llvm.Conventions,-clang-analyzer-deadcode.DeadStores,-clang-analyzer-cplusplus\*,-clang-analyzer-apiModeling\* 
test.c --


on the attached test.c it takes seemingly forever, but if I peel off a 
number of calls to "f" it starts terminating.


It seems like every additional level of calls to "f" doubles the 
compilation time with your commit.


Without your commit even the full repriducer terminates quickly.

Regards,
Mikael

On 04/11/2018 08:21 AM, Adam Balogh via cfe-commits wrote:

Author: baloghadamsoftware
Date: Tue Apr 10 23:21:12 2018
New Revision: 329780

URL: http://llvm.org/viewvc/llvm-project?rev=329780=rev
Log:
[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


Added:
 cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
 cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
 cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
 cfe/trunk/test/Analysis/conditional-path-notes.c
 cfe/trunk/test/Analysis/explain-svals.cpp

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=329780=329779=329780=diff
== 

--- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h 
(original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Tue 
Apr 10 23:21:12 2018

@@ -312,6 +312,9 @@ private:
    /// \sa shouldDisplayNotesAsEvents
    Optional DisplayNotesAsEvents;
  +  /// \sa shouldAggressivelySimplifyRelationalComparison
+  Optional AggressiveRelationalComparisonSimplification;
+
    /// \sa getCTUDir
    Optional CTUDir;
  @@ -666,6 +669,20 @@ public:
    /// to false when unset.
    bool shouldDisplayNotesAsEvents();
  +  /// Returns true if SValBuilder should rearrange comparisons of 
symbolic
+  /// expressions which consist of a sum of a symbol and a concrete 
integer
+  /// into the format where symbols are on the left-hand side and 
the integer
+  /// is on the right. This is only done if both symbols and both 
concrete
+  /// integers are signed, greater than or equal to the quarter of 
the minimum
+  /// value of the type and less than or equal to the quarter of the 
maximum

+  /// value of that type.
+  ///
+  /// A + n  B + m becomes A - B  m - n, where A and B 
symbolic,
+  /// n and m are integers.  is any of '==', '!=', '<', '<=', 
'>' or '>='.
+  /// The rearrangement also happens with '-' instead of '+' on 
either or both

+  /// side and also if any or both integers are missing.
+  bool shouldAggressivelySimplifyRelationalComparison();
+
    /// Returns the directory containing the CTU related files.
    StringRef getCTUDir();

Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=329780=329779=329780=diff
== 


---

Re: r329780 - [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

2018-04-16 Thread Mikael Holmén via cfe-commits 

Hi Adam and Artem,

If I run

clang-tidy -header-filter=.\* 
-checks=clang-analyzer-\*,-clang-analyzer-unix\*,-clang-analyzer-osx\*,-clang-analyzer-security\*,-clang-analyzer-valist\*,-clang-analyzer-optin\*,-clang-analyzer-nullability\*,-clang-analyzer-llvm.Conventions,-clang-analyzer-deadcode.DeadStores,-clang-analyzer-cplusplus\*,-clang-analyzer-apiModeling\* 
test.c --


on the attached test.c it takes seemingly forever, but if I peel off a 
number of calls to "f" it starts terminating.


It seems like every additional level of calls to "f" doubles the 
compilation time with your commit.


Without your commit even the full repriducer terminates quickly.

Regards,
Mikael

On 04/11/2018 08:21 AM, Adam Balogh via cfe-commits wrote:

Author: baloghadamsoftware
Date: Tue Apr 10 23:21:12 2018
New Revision: 329780

URL: http://llvm.org/viewvc/llvm-project?rev=329780=rev
Log:
[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


Added:
 cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
Modified:
 cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
 cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
 cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
 cfe/trunk/test/Analysis/conditional-path-notes.c
 cfe/trunk/test/Analysis/explain-svals.cpp

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=329780=329779=329780=diff
==
--- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Tue Apr 10 
23:21:12 2018
@@ -312,6 +312,9 @@ private:
/// \sa shouldDisplayNotesAsEvents
Optional DisplayNotesAsEvents;
  
+  /// \sa shouldAggressivelySimplifyRelationalComparison

+  Optional AggressiveRelationalComparisonSimplification;
+
/// \sa getCTUDir
Optional CTUDir;
  
@@ -666,6 +669,20 @@ public:

/// to false when unset.
bool shouldDisplayNotesAsEvents();
  
+  /// Returns true if SValBuilder should rearrange comparisons of symbolic

+  /// expressions which consist of a sum of a symbol and a concrete integer
+  /// into the format where symbols are on the left-hand side and the integer
+  /// is on the right. This is only done if both symbols and both concrete
+  /// integers are signed, greater than or equal to the quarter of the minimum
+  /// value of the type and less than or equal to the quarter of the maximum
+  /// value of that type.
+  ///
+  /// A + n  B + m becomes A - B  m - n, where A and B symbolic,
+  /// n and m are integers.  is any of '==', '!=', '<', '<=', '>' or '>='.
+  /// The rearrangement also happens with '-' instead of '+' on either or both
+  /// side and also if any or both integers are missing.
+  bool shouldAggressivelySimplifyRelationalComparison();
+
/// Returns the directory containing the CTU related files.
StringRef getCTUDir();
  


Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=329780=329779=329780=diff
==
--- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Tue Apr 10 23:21:12 
2018
@@ -445,6 +445,14 @@ bool AnalyzerOptions::shouldDisplayNotes
return DisplayNotesAsEvents.getValue();
  }
  
+bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {

+  if (!AggressiveRelationalComparisonSimplification.hasValue())
+AggressiveRelationalComparisonSimplification =
+  getBooleanOption("aggressive-relational-comparison-simplification",
+

r329780 - [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

2018-04-11 Thread Adam Balogh via cfe-commits 
Author: baloghadamsoftware
Date: Tue Apr 10 23:21:12 2018
New Revision: 329780

URL: http://llvm.org/viewvc/llvm-project?rev=329780=rev
Log:
[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


Added:
cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
cfe/trunk/test/Analysis/conditional-path-notes.c
cfe/trunk/test/Analysis/explain-svals.cpp

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=329780=329779=329780=diff
==
--- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Tue Apr 10 
23:21:12 2018
@@ -312,6 +312,9 @@ private:
   /// \sa shouldDisplayNotesAsEvents
   Optional DisplayNotesAsEvents;
 
+  /// \sa shouldAggressivelySimplifyRelationalComparison
+  Optional AggressiveRelationalComparisonSimplification;
+
   /// \sa getCTUDir
   Optional CTUDir;
 
@@ -666,6 +669,20 @@ public:
   /// to false when unset.
   bool shouldDisplayNotesAsEvents();
 
+  /// Returns true if SValBuilder should rearrange comparisons of symbolic
+  /// expressions which consist of a sum of a symbol and a concrete integer
+  /// into the format where symbols are on the left-hand side and the integer
+  /// is on the right. This is only done if both symbols and both concrete
+  /// integers are signed, greater than or equal to the quarter of the minimum
+  /// value of the type and less than or equal to the quarter of the maximum
+  /// value of that type.
+  ///
+  /// A + n  B + m becomes A - B  m - n, where A and B symbolic,
+  /// n and m are integers.  is any of '==', '!=', '<', '<=', '>' or '>='.
+  /// The rearrangement also happens with '-' instead of '+' on either or both
+  /// side and also if any or both integers are missing.
+  bool shouldAggressivelySimplifyRelationalComparison();
+
   /// Returns the directory containing the CTU related files.
   StringRef getCTUDir();
 

Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=329780=329779=329780=diff
==
--- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Tue Apr 10 23:21:12 
2018
@@ -445,6 +445,14 @@ bool AnalyzerOptions::shouldDisplayNotes
   return DisplayNotesAsEvents.getValue();
 }
 
+bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() {
+  if (!AggressiveRelationalComparisonSimplification.hasValue())
+AggressiveRelationalComparisonSimplification =
+  getBooleanOption("aggressive-relational-comparison-simplification",
+   /*Default=*/false);
+  return AggressiveRelationalComparisonSimplification.getValue();
+}
+
 StringRef AnalyzerOptions::getCTUDir() {
   if (!CTUDir.hasValue()) {
 CTUDir = getOptionAsString("ctu-dir", "");

Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
URL: 
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp?rev=329780=329779=329780=diff
==
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp Tue Apr 10 23:21:12 
2018
@@ -12,8 +12,10 @@
 
//===--===//
 
 #include