[analyzer] assume bitwise arithmetic axioms

[george.karpenkov]

Summary

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.

[xazax.hun]

This looks like a great addition! Apart from some nits, LGTM.

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

487

Comments should be sentences (start with capital letter and have a period).

498

This new line is redundant. Also, there are way more new lines in this method than there usually are in LLVM.

[NoQ]

Yep, nice and clean~

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

528

That's more and more "special case"s, i guess we'd have to make them legal. The getRange() function is not only a simple wrapper around State->get<>(), but it is also the single source of truth regarding constraints that can be assumed about the values by simply looking at the values, without exploring the program state. I think this should be reflected in the comments.

test/Analysis/constant-folding.c

92

Can we still assume that b | 1 is non-zero? Maybe FIXME here?

[dcoughlin]

I believe your motivating examples used errno_t, which is a signed type.

I'm fine with assuming a two's complement value representation for signed integers, which would make Artem's suggestion work. That assumption definitely deserves a comment, though.

[george.karpenkov]

Handle non-zero case, more tests cases, cleaner code.

[dcoughlin]

This looks good to me. It is very clean! But please add a comment in the places where you are assuming a two's complement value representation for signed integers.

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

if (SymReaper.maybeDead(Sym)) {
       Changed = true;
       CR = CRFactory.remove(CR, Sym);
     }
   }
 
   return Changed ? State->set<ConstraintRange>(CR) : State;
 }
 
+/// Return a range set subtracting zero from \p Domain.
+static RangeSet assumeNonZero(
+    BasicValueFactory &BV,
+    RangeSet::Factory &F,
+    SymbolRef Sym,
+    RangeSet Domain) {
+  APSIntType IntType = BV.getAPSIntType(Sym->getType());
+  return Domain.Intersect(BV, F, ++IntType.getZeroValue(),
+      --IntType.getZeroValue());
+}
+
+/// \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.
+/// \p Input Previously established expression range set
+static RangeSet applyBitwiseConstraints(
+    BasicValueFactory &BV,
+    RangeSet::Factory &F,
+    RangeSet Input,
+    const SymIntExpr* SIE) {
+  QualType T = SIE->getType();
+  bool IsUnsigned = T->isUnsignedIntegerType();
+  const llvm::APSInt &RHS = SIE->getRHS();
+  const llvm::APSInt &Zero = BV.getAPSIntType(T).getZeroValue();
+
+  // For unsigned types, the output of bitwise-or is bigger-or-equal than RHS.
+  if (SIE->getOpcode() == BO_Or && IsUnsigned)
+    return Input.Intersect(BV, F, RHS, BV.getMaxValue(T));
+
+  // Bitwise-or with a non-zero constant is always non-zero.
+  if (SIE->getOpcode() == BO_Or && RHS != Zero)
+    return assumeNonZero(BV, F, SIE, Input);
+
+  // For unsigned types, or positive RHS,
+  // bitwise-and output is always smaller-or-equal than RHS.
+  if (SIE->getOpcode() == BO_And && (IsUnsigned || RHS >= Zero))
+    return Input.Intersect(BV, F, BV.getMinValue(T), RHS);
+
+  return Input;
+}
+
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           SymbolRef Sym) {
   if (ConstraintRangeTy::data_type *V = State->get<ConstraintRange>(Sym))
     return *V;
 
   // Lazily generate a new RangeSet representing all possible values for the
   // given symbol type.
   BasicValueFactory &BV = getBasicVals();
   QualType T = Sym->getType();
 
   RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
 
-  // Special case: references are known to be non-zero.
-  if (T->isReferenceType()) {
-    APSIntType IntType = BV.getAPSIntType(T);
-    Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
-                              --IntType.getZeroValue());
-  }
+  // References are known to be non-zero.
+  if (T->isReferenceType())
+    return assumeNonZero(BV, F, Sym, Result);
+
+  // Known constraints on ranges of bitwise expressions.
+  if (const SymIntExpr* SIE = dyn_cast<SymIntExpr>(Sym))
+    return applyBitwiseConstraints(BV, F, Result, SIE);
 
   return Result;
 }
 
 //===------------------------------------------------------------------------===
 // assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
 // and (x, y) for open ranges. These ranges are modular, corresponding with

test/Analysis/constant-folding.c

 void testMixedTypeComparisons (char a, unsigned long b) {
   if (a != 0) return;
   if (b != 0x100) return;
 
   clang_analyzer_eval(a <= b); // expected-warning{{TRUE}}
   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) >= 1); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a | -1) >= -1); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a | 2) >= 2); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a | 5) >= 5); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a | 10) >= 10); // expected-warning{{TRUE}}
+
+  // Argument order should not influence this
+  clang_analyzer_eval((1 | a) >= 1); // expected-warning{{TRUE}}
+
+  clang_analyzer_eval((a & 1) <= 1); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a & 2) <= 2); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a & 5) <= 5); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a & 10) <= 10); // expected-warning{{TRUE}}
+  clang_analyzer_eval((a & -10) <= 10); // expected-warning{{UNKNOWN}}
+
+  // Again, check for different argument order.
+  clang_analyzer_eval((1 & a) <= 1); // 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}}
+
+  // Even for signed values, bitwise OR with a non-zero is always non-zero.
+  clang_analyzer_eval((b | 1) == 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval((b | -2) == 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval((b | 10) == 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval((b | 0) == 0); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval((b | -2) >= 0); // expected-warning{{UNKNOWN}}
+
+  // Check that dynamically computed constants also work.
+  int constant = 1 << 3;
+  unsigned int d = a | constant;
+  clang_analyzer_eval(constant > 0); // expected-warning{{TRUE}}
+}