[PATCH] D39707: [analyzer] assume bitwise arithmetic axioms

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov created this revision.
Herald added subscribers: szepet, xazax.hun.

Patches the solver to assume that bitwise OR of an unsigned value with a constant always produces a value larger-or-equal than the constant, and bitwise AND with a constant always produces a value less-or-equal than the constant.

This patch is especially useful in the context of using bitwise arithmetic for error code encoding: the analyzer would be able to state that the error code produced using a bitwise OR is non-zero.

I have considered in very great detail the option of adding the matching code in ExprEngine / SimpleSValBuilder and have found it unfeasible: ideally we would like to pattern match in a great variety of situations: whether the created bitwise value is stored, compared, or added to other values.
Considering all those cases would have led to a very large amount of code duplication.


https://reviews.llvm.org/D39707

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


Index: test/Analysis/constant-folding.c
===================================================================
--- test/Analysis/constant-folding.c
+++ test/Analysis/constant-folding.c
@@ -76,3 +76,18 @@
   clang_analyzer_eval(b >= a); // expected-warning{{TRUE}}
   clang_analyzer_eval(a != b); // expected-warning{{TRUE}}
 }
+
+void testBitwiseRules(unsigned int a, int b) {
+  clang_analyzer_eval((a | 1) > 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval((1 | a) > 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a & 1) < 2); // expected-warning{{TRUE}}
+  clang_analyzer_eval((1 & a) < 2); // expected-warning{{TRUE}}
+
+  unsigned int c = a;
+  c |= 1;
+  clang_analyzer_eval((c | 0) == 0); // expected-warning{{FALSE}}
+
+  // Rules don't apply to signed typed, as the values might be negative.
+  clang_analyzer_eval((b | 1) > 0); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval((b | 1) == 0); // expected-warning{{UNKNOWN}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -460,6 +460,44 @@
   return Changed ? State->set<ConstraintRange>(CR) : State;
 }
 
+/// \brief Apply implicit constraints for bitwise OR- and AND-.
+/// For unsigned types, bitwise OR with a constant always returns
+/// a value greater-or-equal than the constant, and bitwise AND
+/// returns a value less-or-equal then the constant.
+///
+/// Pattern matches the expression \p Sym against those rule,
+/// and applies the required constraints.
+static RangeSet applyBitwiseConstraints(
+    BasicValueFactory &BV,
+    RangeSet::Factory &F,
+    QualType T,
+    RangeSet Result,
+    SymbolRef Sym) {
+
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+
+    // Only apply the rule to unsigned types, otherwise sign
+    // may change and ordering will be violated.
+    if (!SIE->getLHS()->getType()->isUnsignedIntegerType())
+      return Result;
+
+    switch (SIE->getOpcode()) {
+      case BO_Or:
+
+        // result >= constant
+        return Result.Intersect(BV, F, SIE->getRHS(), BV.getMaxValue(T));
+      case BO_And:
+
+        // result <= constant
+        return Result.Intersect(BV, F, BV.getMinValue(T), SIE->getRHS());
+      default:
+        break;
+    }
+  }
+  return Result;
+
+}
+
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           SymbolRef Sym) {
   if (ConstraintRangeTy::data_type *V = State->get<ConstraintRange>(Sym))
@@ -479,6 +517,7 @@
                               --IntType.getZeroValue());
   }
 
+  Result = applyBitwiseConstraints(BV, F, T, Result, Sym);
   return Result;
 }
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D39707.121812.patch
Type: text/x-patch
Size: 2783 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20171107/c79bcc27/attachment.bin>