[PATCH] D105436: [analyzer][solver] Use all sources of constraints

[Valeriy Savchenko via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rG6017cb31bb35: [analyzer][solver] Use all sources of constraints (authored by vsavchenko).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D105436

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/constant-folding.c


Index: clang/test/Analysis/constant-folding.c
===================================================================
--- clang/test/Analysis/constant-folding.c
+++ clang/test/Analysis/constant-folding.c
@@ -179,6 +179,36 @@
   }
 }
 
+unsigned reset();
+
+void testCombinedSources(unsigned a, unsigned b) {
+  if (b >= 10 && (a | b) <= 30) {
+    // Check that we can merge constraints from (a | b), a, and b.
+    // Because of the order of assumptions, we already know that (a | b) is [10, 30].
+    clang_analyzer_eval((a | b) >= 10 && (a | b) <= 30); // expected-warning{{TRUE}}
+  }
+
+  a = reset();
+  b = reset();
+
+  if ((a | b) <= 30 && b >= 10) {
+    // Check that we can merge constraints from (a | b), a, and b.
+    // At this point, we know that (a | b) is [0, 30], but the knowledge
+    // of b >= 10 added later can help us to refine it and change it to [10, 30].
+    clang_analyzer_eval(10 <= (a | b) && (a | b) <= 30); // expected-warning{{TRUE}}
+  }
+
+  a = reset();
+  b = reset();
+
+  unsigned c = (a | b) & (a != b);
+  if (c <= 40 && a == b) {
+    // Even though we have a directo constraint for c [0, 40],
+    // we can get a more precise range by looking at the expression itself.
+    clang_analyzer_eval(c == 0); // expected-warning{{TRUE}}
+  }
+}
+
 void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
   // Check that we know that remainder of zero divided by any number is still 0.
   clang_analyzer_eval((0 % c) == 0); // expected-warning{{TRUE}}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -884,26 +884,28 @@
   }
 
   RangeSet infer(SymbolRef Sym) {
-    if (Optional<RangeSet> ConstraintBasedRange = intersect(
-            RangeFactory, getConstraint(State, Sym),
-            // If Sym is a difference of symbols A - B, then maybe we have range
-            // set stored for B - A.
-            //
-            // If we have range set stored for both A - B and B - A then
-            // calculate the effective range set by intersecting the range set
-            // for A - B and the negated range set of B - A.
-            getRangeForNegatedSub(Sym), getRangeForEqualities(Sym))) {
-      return *ConstraintBasedRange;
-    }
-
-    // If Sym is a comparison expression (except <=>),
-    // find any other comparisons with the same operands.
-    // See function description.
-    if (Optional<RangeSet> CmpRangeSet = getRangeForComparisonSymbol(Sym)) {
-      return *CmpRangeSet;
-    }
-
-    return Visit(Sym);
+    return intersect(
+        RangeFactory,
+        // Of course, we should take the constraint directly associated with
+        // this symbol into consideration.
+        getConstraint(State, Sym),
+        // If Sym is a difference of symbols A - B, then maybe we have range
+        // set stored for B - A.
+        //
+        // If we have range set stored for both A - B and B - A then
+        // calculate the effective range set by intersecting the range set
+        // for A - B and the negated range set of B - A.
+        getRangeForNegatedSub(Sym),
+        // If Sym is (dis)equality, we might have some information on that
+        // in our equality classes data structure.
+        getRangeForEqualities(Sym),
+        // If Sym is a comparison expression (except <=>),
+        // find any other comparisons with the same operands.
+        // See function description.
+        getRangeForComparisonSymbol(Sym),
+        // Apart from the Sym itself, we can infer quite a lot if we look
+        // into subexpressions of Sym.
+        Visit(Sym));
   }
 
   RangeSet infer(EquivalenceClass Class) {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D105436.356628.patch
Type: text/x-patch
Size: 3824 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210706/1b5e0331/attachment-0001.bin>