Skip to content

[analyzer] RangeConstraint: deduce subtraction from equality #66065

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
danix800 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[analyzer] RangeConstraint: deduce subtraction from equality #66065

danix800 wants to merge 1 commit into from

Conversation

@danix800
Copy link
Member

@danix800 danix800 commented Sep 12, 2023

  1. Arithmetic difference 'a - b' could be deduced from 'a != b';
  2. For pointer comparison 'a rel_op b', only do conversion to 'b - a reverse(rel_op) 0' if 'rel_op' is '==' or '!=', otherwise fallback to general 'assumeSymUnsupported'.

Fixes #59963

@danix800
[analyzer] RangeConstraint: deduce subtraction from equality
68c443c 
1. Arithmetic difference 'a - b' could be deduced from 'a != b';
2. For pointer comparison 'a rel_op b', only do conversion to
   'b - a reverse(rel_op) 0' if 'rel_op' is '==' or '!=', otherwise
   fallback to general 'assumeSymUnsupported'.

Fixes llvm#59963
@danix800 danix800 requested review from a team as code owners September 12, 2023 10:27
@llvmbot llvmbot added clang Clang issues not falling into any other category clang:static analyzer clang:dataflow Clang Dataflow Analysis framework - https://clang.llvm.org/docs/DataFlowAnalysisIntro.html labels Sep 12, 2023
@llvmbot
Copy link
Member

llvmbot commented Sep 12, 2023

@llvm/pr-subscribers-clang

Changes
  1. Arithmetic difference 'a - b' could be deduced from 'a != b';
  2. For pointer comparison 'a rel_op b', only do conversion to 'b - a reverse(rel_op) 0' if 'rel_op' is '==' or '!=', otherwise fallback to general 'assumeSymUnsupported'.

Fixes #59963

Full diff: https://github.com/llvm/llvm-project/pull/66065.diff

5 Files Affected:

  • (modified) clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (+8)
  • (modified) clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (+2-2)
  • (added) clang/test/Analysis/constraint_manager_diff_negate.cpp (+24)
  • (added) clang/test/Analysis/constraint_manager_ptr_conditions.cpp (+24)
  • (modified) clang/test/Analysis/ptr-arith.c (-17)
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 5de99384449a4c8..ce66ea2123783d9 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1589,6 +1589,14 @@ class SymbolicRangeInferrer
       }
       // Opposite combinations result in false.
       return getFalseRange(Sym->getType());
+    } else if (Sym->getOpcode() == BO_Sub) {
+      QualType CondTy =
+          State->getStateManager().getSValBuilder().getConditionType();
+      const SymSymExpr *SSE = State->getSymbolManager().getSymSymExpr(
+          Sym->getRHS(), BO_NE, Sym->getLHS(), CondTy);
+      if (auto Constraint = getRangeForComparisonSymbol(SSE))
+        return Constraint->encodesFalseRange() ? getFalseRange(Sym->getType())
+                                               : getTrueRange(Sym->getType());
     }
 
     return std::nullopt;
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 4bbe933be2129e1..d023975e2e1947a 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -52,7 +52,8 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
 
       // We convert equality operations for pointers only.
       if (Loc::isLocType(SSE->getLHS()->getType()) &&
-          Loc::isLocType(SSE->getRHS()->getType())) {
+          Loc::isLocType(SSE->getRHS()->getType()) &&
+          BinaryOperator::isEqualityOp(Op)) {
         // Translate "a != b" to "(b - a) != 0".
         // We invert the order of the operands as a heuristic for how loop
         // conditions are usually written ("begin != end") as compared to length
@@ -66,7 +67,6 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
             SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
 
         const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
-        Op = BinaryOperator::reverseComparisonOp(Op);
         if (!Assumption)
           Op = BinaryOperator::negateComparisonOp(Op);
         return assumeSymRel(State, Subtraction, Op, Zero);
diff --git a/clang/test/Analysis/constraint_manager_diff_negate.cpp b/clang/test/Analysis/constraint_manager_diff_negate.cpp
new file mode 100644
index 000000000000000..163dd18ca183f7e
--- /dev/null
+++ b/clang/test/Analysis/constraint_manager_diff_negate.cpp
@@ -0,0 +1,24 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+void top(int b, int c) {
+  if (c >= b) {
+    clang_analyzer_eval(c >= b); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b <= c); // expected-warning{{TRUE}}
+    clang_analyzer_eval((b - 0) <= (c + 0)); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b + 0 <= c + 0); // expected-warning{{TRUE}}
+  }
+}
+
+void comparisons_imply_size(unsigned long lhs, unsigned long rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if (lhs > rhs) {
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+    clang_analyzer_eval(lhs - rhs == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval(rhs - lhs == 0); // expected-warning{{FALSE}}
+  }
+}
diff --git a/clang/test/Analysis/constraint_manager_ptr_conditions.cpp b/clang/test/Analysis/constraint_manager_ptr_conditions.cpp
new file mode 100644
index 000000000000000..0ce3544cc7b6c9e
--- /dev/null
+++ b/clang/test/Analysis/constraint_manager_ptr_conditions.cpp
@@ -0,0 +1,24 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+void top(int *b, int *c) {
+  if (c >= b) {
+    clang_analyzer_eval(c >= b); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b <= c); // expected-warning{{TRUE}}
+    clang_analyzer_eval((b - 0) <= (c + 0)); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b + 0 <= c + 0); // expected-warning{{TRUE}}
+  }
+}
+
+void comparisons_imply_size(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if (lhs > rhs) {
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+    clang_analyzer_eval(lhs - rhs == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval(rhs - lhs == 0); // expected-warning{{FALSE}}
+  }
+}
diff --git a/clang/test/Analysis/ptr-arith.c b/clang/test/Analysis/ptr-arith.c
index 40c8188704e811b..0ef812aea09bdd2 100644
--- a/clang/test/Analysis/ptr-arith.c
+++ b/clang/test/Analysis/ptr-arith.c
@@ -214,12 +214,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-// FIXME: In Z3ConstraintManager, ptrdiff_t is mapped to signed bitvector. However, this does not directly imply the unsigned comparison.
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
   if (lhs >= rhs) {
@@ -229,11 +224,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
   clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
-#endif
 }
 
 void size_implies_comparison(int *lhs, int *rhs) {
@@ -244,11 +235,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
     return;
   }
 
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
@@ -258,11 +245,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
 }

@llvmbot
Copy link
Member

llvmbot commented Sep 12, 2023

@llvm/pr-subscribers-clang-static-analyzer-1

Changes
  1. Arithmetic difference 'a - b' could be deduced from 'a != b';
  2. For pointer comparison 'a rel_op b', only do conversion to 'b - a reverse(rel_op) 0' if 'rel_op' is '==' or '!=', otherwise fallback to general 'assumeSymUnsupported'.

Fixes #59963

Full diff: https://github.com/llvm/llvm-project/pull/66065.diff

5 Files Affected:

  • (modified) clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (+8)
  • (modified) clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (+2-2)
  • (added) clang/test/Analysis/constraint_manager_diff_negate.cpp (+24)
  • (added) clang/test/Analysis/constraint_manager_ptr_conditions.cpp (+24)
  • (modified) clang/test/Analysis/ptr-arith.c (-17)
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 5de99384449a4c8..ce66ea2123783d9 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1589,6 +1589,14 @@ class SymbolicRangeInferrer
       }
       // Opposite combinations result in false.
       return getFalseRange(Sym->getType());
+    } else if (Sym->getOpcode() == BO_Sub) {
+      QualType CondTy =
+          State->getStateManager().getSValBuilder().getConditionType();
+      const SymSymExpr *SSE = State->getSymbolManager().getSymSymExpr(
+          Sym->getRHS(), BO_NE, Sym->getLHS(), CondTy);
+      if (auto Constraint = getRangeForComparisonSymbol(SSE))
+        return Constraint->encodesFalseRange() ? getFalseRange(Sym->getType())
+                                               : getTrueRange(Sym->getType());
     }
 
     return std::nullopt;
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 4bbe933be2129e1..d023975e2e1947a 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -52,7 +52,8 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
 
       // We convert equality operations for pointers only.
       if (Loc::isLocType(SSE->getLHS()->getType()) &&
-          Loc::isLocType(SSE->getRHS()->getType())) {
+          Loc::isLocType(SSE->getRHS()->getType()) &&
+          BinaryOperator::isEqualityOp(Op)) {
         // Translate "a != b" to "(b - a) != 0".
         // We invert the order of the operands as a heuristic for how loop
         // conditions are usually written ("begin != end") as compared to length
@@ -66,7 +67,6 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
             SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
 
         const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
-        Op = BinaryOperator::reverseComparisonOp(Op);
         if (!Assumption)
           Op = BinaryOperator::negateComparisonOp(Op);
         return assumeSymRel(State, Subtraction, Op, Zero);
diff --git a/clang/test/Analysis/constraint_manager_diff_negate.cpp b/clang/test/Analysis/constraint_manager_diff_negate.cpp
new file mode 100644
index 000000000000000..163dd18ca183f7e
--- /dev/null
+++ b/clang/test/Analysis/constraint_manager_diff_negate.cpp
@@ -0,0 +1,24 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+void top(int b, int c) {
+  if (c >= b) {
+    clang_analyzer_eval(c >= b); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b <= c); // expected-warning{{TRUE}}
+    clang_analyzer_eval((b - 0) <= (c + 0)); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b + 0 <= c + 0); // expected-warning{{TRUE}}
+  }
+}
+
+void comparisons_imply_size(unsigned long lhs, unsigned long rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if (lhs > rhs) {
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+    clang_analyzer_eval(lhs - rhs == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval(rhs - lhs == 0); // expected-warning{{FALSE}}
+  }
+}
diff --git a/clang/test/Analysis/constraint_manager_ptr_conditions.cpp b/clang/test/Analysis/constraint_manager_ptr_conditions.cpp
new file mode 100644
index 000000000000000..0ce3544cc7b6c9e
--- /dev/null
+++ b/clang/test/Analysis/constraint_manager_ptr_conditions.cpp
@@ -0,0 +1,24 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+void top(int *b, int *c) {
+  if (c >= b) {
+    clang_analyzer_eval(c >= b); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b <= c); // expected-warning{{TRUE}}
+    clang_analyzer_eval((b - 0) <= (c + 0)); // expected-warning{{TRUE}}
+    clang_analyzer_eval(b + 0 <= c + 0); // expected-warning{{TRUE}}
+  }
+}
+
+void comparisons_imply_size(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if (lhs > rhs) {
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+    clang_analyzer_eval(lhs - rhs == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval(rhs - lhs == 0); // expected-warning{{FALSE}}
+  }
+}
diff --git a/clang/test/Analysis/ptr-arith.c b/clang/test/Analysis/ptr-arith.c
index 40c8188704e811b..0ef812aea09bdd2 100644
--- a/clang/test/Analysis/ptr-arith.c
+++ b/clang/test/Analysis/ptr-arith.c
@@ -214,12 +214,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-// FIXME: In Z3ConstraintManager, ptrdiff_t is mapped to signed bitvector. However, this does not directly imply the unsigned comparison.
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
   if (lhs >= rhs) {
@@ -229,11 +224,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
   clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
-#endif
 }
 
 void size_implies_comparison(int *lhs, int *rhs) {
@@ -244,11 +235,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
     return;
   }
 
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
@@ -258,11 +245,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
   clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
-#else
-  clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
 }

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

clang:dataflow Clang Dataflow Analysis framework - https://clang.llvm.org/docs/DataFlowAnalysisIntro.html clang:static analyzer clang Clang issues not falling into any other category

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

CSA evaluates ( ((b)-0) <= ((c)-0) ) to be FALSE in the true branch of if (c >= b)

2 participants

@danix800 @llvmbot