[Analyzer][solver] Handle adjustments in constraint assignor remainder

[martong]

Summary

We can reuse the "adjustment" handling logic in the higher level
of the solver by calling assumeSymRel.

(Actually, this shows us that there is no point in separating the
RangeConstraintManager from the RangedConstraintManager, that
separation is in fact artificial. A follow-up NFC patch might
address this.)

[steakhal]

<3

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

What I see, you're still trying to avoid using State->assume, which I recommend in a parent revision, but coming closer using its guts.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

So, it would look like this:

State = State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);

The main reason why we cannot use State->assume is that it boils down to RangedConstraintManager::assumeSym that has a specific logic for the boolean assumption. I.e. the operator is being negated in a case:

if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
  if (!Assumption)
    op = BinaryOperator::negateComparisonOp(op);

  return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
}

You can try it for yourself, and see that the test case added in this patch will not pass if we were to use State->assume. Essentially, we have to evade the special "bool" logic, and the closest we can get is using assumeSymRel.

Besides that, by using State->assume we would have a superfluous conversion chain Symbol->SVal->Symbol until we reach assumeSymRel.

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

You can try it for yourself, and see that the test case added in this patch will not pass if we were to use State->assume.

I can't confirm. Your test case passed when I replaced with State = State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);.

specific logic for the boolean assumption. I.e. the operator is being negated in a case:

That just simplifies the expression, say, you want to find whether x > 5 is false, than the Solver finds for you whether
x <= 5 is true, which is an equivalent.

Essentially, we have to evade the special "bool" logic

There is no problem with bool logic. It's an equivalent of SVal != 0 when true, and SVal == 0 when false. Nothing more.

All in all I see the problem to use assume. Not because of this function itself, but because you do it incorrect by getting an SVal from LHS with makeSymbolVal. We should get it with State->getSVal which needs LocationContext as a second parameter. And that's the challenge, to pass LocationContext here, since RangedConstraintManager doesn't use it, at least for now.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

I can't confirm. Your test case passed when I replaced with State = State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);.

Actually, since the last time I tried with State->assume we merged D110913. If you revert the changes of that patch you'll see that this test case indeed fails. However, here is a slightly modified case that fails even on the current llvm/main branch with State->assume but passes with assumeSymRel:

void rem_constant_adj(int x, int y) {
  if ((x + y + 1) % 3 == 0) // (x + y + 1) % 3 != 0 -> x + y + 1 != 0 -> x != -1
    return;
  clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
  clang_analyzer_eval(x + y != -1);    // expected-warning{{TRUE}}
  (void)(x * y); // keep the constraints alive.
}

The only change is that we have x + y instead of x.

Now, the explanation for the original test case when we have (x + 1) % 3: When we ask the value of x != -1 then assumeDual evaluates the TRUE case which is feasible and then it tries to evaluate the FALSE case, so it queries x == -1 is true. However, this kicks in the simplification, which simplifies the previous constraint of x+1, [not 0] to -1 + 1, [not 0] which is a contradiction, thus an infeasible state is returned.
When we have x + y in the test case, then simplification cannot simplify x + y + 1, thus the situation is different.

So, the main problem with State->assume is that it does not compute the adjustment. I.e. when we have x + 1 as LHS then assumeSym(LHS) calls into assumeSymUnsupported and that does not compute the adjustment. The only functions that compute the adjustment are assumeSymRel and assumeSymInclusiveRange.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

BTW, if D103317 was merged, then I'd have to find another test case that fails here, but I think I could find one. Anyway, the point is that we need a function here, that handles the adjustments.

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

So, the main problem with State->assume is that it does not compute the adjustment. I.e. when we have x + 1 as LHS then assumeSym(LHS) calls into assumeSymUnsupported and that does not compute the adjustment. The only functions that compute the adjustment are assumeSymRel and assumeSymInclusiveRange.

Wow, I've just seen a possible solution in the game of words. If assumeSym(LHS) leads to assumeSymUnsupported, then we just need to support it, namely, make it go to assumeSymRel. IMO it's worth to investigate such a chance.

[steakhal]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

+1, Thank you for pushing this @ASDenysPetrov

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1618–1619

So, the main problem with State->assume is that it does not compute the adjustment. I.e. when we have x + 1 as LHS then assumeSym(LHS) calls into assumeSymUnsupported and that does not compute the adjustment. The only functions that compute the adjustment are assumeSymRel and assumeSymInclusiveRange.

Wow, I've just seen a possible solution in the game of words. If assumeSym(LHS) leads to assumeSymUnsupported, then we just need to support it, namely, make it go to assumeSymRel. IMO it's worth to investigate such a chance.

Okay, that could be a good alternative, good idea!

[martong]

• Handle adjustment in assumeSym for non-comparison ops.

[martong]

• Remove superflous change.

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

46–49

52

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

44–50

Actually what you are trying to do here is already inside assumeSymUnsupported and it will work for all SymIntExpr.
Please, proveide a test case which works with assumeSymRel and doesn't with asume from the previous change. That is what we are trying to fix here.

[martong]

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

44–50

Thanks for suggesting the use of the ternary op, the code is way more elegant that way!

Actually what you are trying to do here is already inside assumeSymUnsupported and it will work for all SymIntExpr.

I see your point and I acknowledge that this new code resembles to the one in assumeSymUnsupported. However, there is a subtle but very important difference. In assumeSymUnsupported we use assumeSymNE/EQ, but here I use assumeSymRel. And assumeSymRel does compute the adjustment, but assumeSymNE/EQ do not. Also, it makes sense to compute the adjustment only in case of SymIntExprs, thus this could not be done in assumeSymUnsupported.

Please, proveide a test case which works with assumeSymRel and doesn't with asume from the previous change. That is what we are trying to fix here.

You are right, it desires a test case, so I just added the one I had pasted here previously (with (x + y + 1) % 3). If you comment-out the modifications here in assumSym then that test case will fail.

46–49

52

Yep, good point.

[martong]

• Add new test case
• Adapt style changes

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

44–50

However, there is a subtle but very important difference.

Now I see the difference. OK, then. Your solution is sensible.

[steakhal]

clang/test/Analysis/constraint-assignor.c

7

Expect an int parameter.

[martong]

@ASDenysPetrov @steakhal Thanks for the assiduous reviews!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

assign(ProgramStateRef State, RangeConstraintManager &RCM,
     return Assignor.assign(CoS, NewConstraint);
   }
 
   /// Handle expressions like: a % b != 0.
   template <typename SymT>
   bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) {
     if (Sym->getOpcode() != BO_Rem)
       return true;
-    const SymbolRef LHS = Sym->getLHS();
-    const llvm::APSInt &Zero =
-        Builder.getBasicValueFactory().getValue(0, Sym->getType());
     // a % b != 0 implies that a != 0.
     if (!Constraint.containsZero()) {
-      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+      SVal SymSVal = Builder.makeSymbolVal(Sym->getLHS());
+      if (auto NonLocSymSVal = SymSVal.getAs<nonloc::SymbolVal>()) {
+        State = State->assume(*NonLocSymSVal, true);
         if (!State)
           return false;
       }
+    }
     return true;
   }
 
   inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint);
   inline bool assignSymIntExprToRangeSet(const SymIntExpr *Sym,
                                          RangeSet Constraint) {
     return handleRemainderOp(Sym, Constraint);
   }

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
     BinaryOperator::Opcode op = SIE->getOpcode();
     if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
       if (!Assumption)
         op = BinaryOperator::negateComparisonOp(op);
 
       return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
     }
 
-  } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    // Handle adjustment with non-comparison ops.
+    const llvm::APSInt &Zero = getBasicVals().getValue(0, SIE->getType());
+    return assumeSymRel(State, SIE, (Assumption ? BO_NE : BO_EQ), Zero);
+  }
+
+  if (const auto *SSE = dyn_cast<SymSymExpr>(Sym)) {
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
     // We convert equality operations for pointers only.
     if (Loc::isLocType(SSE->getLHS()->getType()) &&
         Loc::isLocType(SSE->getRHS()->getType())) {
       // 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
       // calculations ("end - begin"). The more correct thing to do would be to
       // canonicalize "a - b" and "b - a", which would allow us to treat

clang/test/Analysis/constraint-assignor.c

 // RUN: %clang_analyze_cc1 %s \
 // RUN:   -analyzer-checker=core \
 // RUN:   -analyzer-checker=debug.ExprInspection \
 // RUN:   -verify
 
-// expected-no-diagnostics
-
 void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
 
 void rem_constant_rhs_ne_zero(int x, int y) {
   if (x % 3 == 0) // x % 3 != 0 -> x != 0
     return;
   if (x * y != 0) // x * y == 0
     return;
   if (y != 1)     // y == 1     -> x == 0
     return;
void internal_unsigned_signed_mismatch(unsigned a) {
   int d = a;
   // Implicit casts are not handled, thus the analyzer models `d % 2` as
   // `(reg_$0<unsigned int a>) % 2`
   // However, this should not result in internal signedness mismatch error when
   // we assign new constraints below.
   if (d % 2 != 0)
     return;
 }
+
+void remainder_with_adjustment(int x) {
+  if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+    return;
+  clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x != -1);    // expected-warning{{TRUE}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_with_adjustment_of_composit_lhs(int x, int y) {
+  if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+    return;
+  clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x + y != -1);    // expected-warning{{TRUE}}
+  (void)(x * y); // keep the constraints alive.
+}