[PATCH] D107636: [analyzer][solver] Compute adjustment for unsupported symbols as well

[Gabor Marton via Phabricator via cfe-commits]

martong requested changes to this revision.
martong added a comment.
This revision now requires changes to proceed.

I am not sure if this patch makes sense at all because the adjustment handling 
logic is restricted to handle SymInt expressions only.




Comment at: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:82-86
   if (IsExpectedEqual) {
 return assumeSymNE(State, CanonicalEquality, Zero, Zero);
   }
 
   return assumeSymEQ(State, CanonicalEquality, Zero, Zero);

ASDenysPetrov wrote:
> Do we need the same changes here as below?
I believe, the adjustment is deliberately Zero here. This is because we are 
dealing with a SymSym expr, and the adjustment logic is capable of handling 
only a SymInt expr.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D107636/new/

https://reviews.llvm.org/D107636

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D107636: [analyzer][solver] Compute adjustment for unsupported symbols as well

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.
Herald added a project: All.

I checked the tests file on the latest sources. It passes even without your 
changes. Maybe this patch is already outdated.




Comment at: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:82-86
   if (IsExpectedEqual) {
 return assumeSymNE(State, CanonicalEquality, Zero, Zero);
   }
 
   return assumeSymEQ(State, CanonicalEquality, Zero, Zero);

Do we need the same changes here as below?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D107636/new/

https://reviews.llvm.org/D107636

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D107636: [analyzer][solver] Compute adjustment for unsupported symbols as well

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D107636#2931302 , @steakhal wrote:

> Seems reasonable to me. Let's wait for someone else as well.

Sure, NP.

> This is a really elegant patch, I should tell!

Thanks!  I guess my take on this, that this path to the solver just got 
forgotten and that's what produced this inconsistency.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D107636/new/

https://reviews.llvm.org/D107636

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D107636: [analyzer][solver] Compute adjustment for unsupported symbols as well

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

Seems reasonable to me. Let's wait for someone else as well.
This is a really elegant patch, I should tell!


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D107636/new/

https://reviews.llvm.org/D107636

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D107636: [analyzer][solver] Compute adjustment for unsupported symbols as well

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko created this revision.
vsavchenko added reviewers: NoQ, xazax.hun, martong, steakhal, Szelethus, 
ASDenysPetrov, manas, RedDocMD.
Herald added subscribers: dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, 
rnkovacs, szepet, baloghadamsoftware.
vsavchenko requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

When the solver sees conditions like `a +/- INT cmp INT`, it disassembles
such expressions and uses the first integer constant as a so-called 
"Adjustment".
So it's easier later on to reason about the range of the symbol (`a`
in this case).

However, conditions of form `a +/- INT` are not treated the same way,
and we might end up with contradictory constraints.

This patch resolves this issue and extracts "Adjustment" for the
latter case as well.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D107636

Files:
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/infeasible_paths.c


Index: clang/test/Analysis/infeasible_paths.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible_paths.c
@@ -0,0 +1,25 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify 
%s
+
+// expected-no-diagnostics
+
+void clang_analyzer_warnIfReached();
+
+void unsupportedSymAssumption_1(int a) {
+  int b = a + 1;
+  if (b + 1)
+return;
+  // At this point, b == -1, a == -2
+  // and this condition is always true.
+  if (b < 1)
+return;
+  clang_analyzer_warnIfReached(); // no-warning
+}
+
+void unsupportedSymAssumption_2(int a) {
+  int b = a - 1;
+  if (!b)
+return;
+  if (b)
+return;
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -137,10 +137,13 @@
 
   // Reverse the operation and add directly to state.
   const llvm::APSInt &Zero = BVF.getValue(0, T);
+  llvm::APSInt Adjustment = Zero;
+  computeAdjustment(Sym, Adjustment);
+
   if (Assumption)
-return assumeSymNE(State, Sym, Zero, Zero);
-  else
-return assumeSymEQ(State, Sym, Zero, Zero);
+return assumeSymNE(State, Sym, Zero, Adjustment);
+
+  return assumeSymEQ(State, Sym, Zero, Adjustment);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,


Index: clang/test/Analysis/infeasible_paths.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible_paths.c
@@ -0,0 +1,25 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+// expected-no-diagnostics
+
+void clang_analyzer_warnIfReached();
+
+void unsupportedSymAssumption_1(int a) {
+  int b = a + 1;
+  if (b + 1)
+return;
+  // At this point, b == -1, a == -2
+  // and this condition is always true.
+  if (b < 1)
+return;
+  clang_analyzer_warnIfReached(); // no-warning
+}
+
+void unsupportedSymAssumption_2(int a) {
+  int b = a - 1;
+  if (!b)
+return;
+  if (b)
+return;
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -137,10 +137,13 @@
 
   // Reverse the operation and add directly to state.
   const llvm::APSInt &Zero = BVF.getValue(0, T);
+  llvm::APSInt Adjustment = Zero;
+  computeAdjustment(Sym, Adjustment);
+
   if (Assumption)
-return assumeSymNE(State, Sym, Zero, Zero);
-  else
-return assumeSymEQ(State, Sym, Zero, Zero);
+return assumeSymNE(State, Sym, Zero, Adjustment);
+
+  return assumeSymEQ(State, Sym, Zero, Adjustment);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits