[analyzer] Hotfix a boolean conversion crash in the Z3 SMTConv

[vabridgers]

If a UnarySymExpr with an arithmetic negation of a logical operation to obtain a SMTRefExpr, the Z3 engine will crash. Since an arithmetic negation of a logical operation makes no sense and has no effect, the arithmetic negation is detected and removed to avoid the crash in Z3.

This shows up following this C snippet

1: void bb(int a) {
2:  if (-(&c && a)) {
3:     int *d;
4:     *d; // expected-warning{{Dereference of undefined pointer value}}
5:  }
6: }

Line 2 is expressed as SymExpr -((reg_$1) != 0) , which is then attempted to be converted to SMTRefExpr (not (= reg_$1 #x00000000)). This does not make sense to Z3 since a logical expression cannot be arithmetically negated.

A solution is to detect that the result of a comparison is attempted to be arithmetically negated and remove that arithmetic negation since the negation of a bool is the same as the positive of a bool. Bool's have no sign, they are only True or False.

[llvmbot]

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

@llvm/pr-subscribers-clang

Author: None (vabridgers)

Changes

If a UnarySymExpr with an arithmetic negation of a logical operation to obtain a SMTRefExpr, the Z3 engine will crash. Since an arithmetic negation of a logical operation makes no sense and has no effect, the arithmetic negation is detected and removed to avoid the crash in Z3.

This shows up following this C snippet

1: void bb(int a) {
2: if (-(&c && a)) {
3: int *d;
4: *d; // expected-warning{{Dereference of undefined pointer value}}
5: }
6: }

Line 2 is expressed as SymExpr -((reg_$1<int a>) != 0) , which is then attempted to be converted to SMTRefExpr (not (= reg_$1 #x00000000)). This does not make sense to Z3 since a logical expression cannot be arithmetically negated.

A solution is to detect that the result of a comparison is attempted to be arithmetically negated and remove that arithmetic negation since the negation of a bool is the same as the positive of a bool. Bool's have no sign, they are only True or False.

---

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

2 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (+7)
• (modified) clang/test/Analysis/z3-unarysymexpr.c (+26)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index a6cb6c0f12a8c..66c99551969b7 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -455,6 +455,13 @@ class SMTConv {
       QualType OperandTy;
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
+
+      if (const BinarySymExpr *BSE =
+              dyn_cast<BinarySymExpr>(USE->getOperand())) {
+        if (BinaryOperator::isComparisonOp(BSE->getOpcode()))
+          return getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
+      }
+
       llvm::SMTExprRef UnaryExp =
           OperandTy->isRealFloatingType()
               ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
index ed9ba72468422..427c92f4bdd7c 100644
--- a/clang/test/Analysis/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -13,3 +13,29 @@ int negate(int x, int y) {
     return 0;
   return 1;
 }
+
+void c();
+void case004(int *a, int *b) {
+  void *e;
+  b != a;
+  c(e); // expected-warning{{1st function call argument is an uninitialized value}}
+}
+
+void z3crash(int a, int b) {
+  b = a || b;
+  (-b == a) / a; // expected-warning{{expression result unused}}
+                 // expected-warning@-1{{Division by zero [core.DivideZero]}}
+}
+
+void z3_nocrash(float a, float b) {
+  b = a || b;
+  (-b == a) / a; // expected-warning{{expression result unused}}
+}
+
+void z3_crash2(int a) {
+  if (-(&c && a)) {
+    int *d;
+    *d; // expected-warning{{Dereference of undefined pointer value}}
+        // expected-warning@-1{{expression result unused}}
+  }
+}

[steakhal]

The tests look really fragile. Without knowing exactly how did we end up with a SymExpr that fails to convert to a Z3 formula, I'm tempted to push back. I think I've seen similar conversion errors and fixes from you. This suggests to me that we need to understand the underlying reasons why we have these SymExprs and systematically solve these issues.

My gut instincts suggests that this SymExpr lacks some SymbolCast (due to the inappropriate modeling of casts), which bites back here as well. If that's the case, we could provide a translation layer that would visit a SymExpr and output a valid SymExpr that has the bit-widening/truncating SymbolCasts where needed. That way only Z3 would have a different "view" of these symbols while the engine could still have the wrong SymExprs. The added benefit would be to have a centralized place of the hacks that we currently embed into the Z3 expr converter.

[NagyDonat]

I added some inline comments; but I know almost nothing about the Z3 solver and related code, so I would be grateful if somebody with more knowledge would also review this change.

[vabridgers]

The tests look really fragile. Without knowing exactly how did we end up with a SymExpr that fails to convert to a Z3 formula, I'm tempted to push back. I think I've seen similar conversion errors and fixes from you. This suggests to me that we need to understand the underlying reasons why we have these SymExprs and systematically solve these issues.

My gut instincts suggests that this SymExpr lacks some SymbolCast (due to the inappropriate modeling of casts), which bites back here as well. If that's the case, we could provide a translation layer that would visit a SymExpr and output a valid SymExpr that has the bit-widening/truncating SymbolCasts where needed. That way only Z3 would have a different "view" of these symbols while the engine could still have the wrong SymExprs. The added benefit would be to have a centralized place of the hacks that we currently embed into the Z3 expr converter.

Hi @steakhal , thanks for the comment. I agree there could be some deeper issue here, but my immediate concern is to avoid the crash. Is it ok if we separate those concerns and first come up with a way to avoid the crash, then follow up with understanding and fixing the deeper concern? I admit I do not understand the details of SymExprs, but I needed to get attention on this new issue - hence this PR as a starting point.

[vabridgers]

I'll rework this change a bit more and update. Turns out the test case I chose to add these cases is for z3 as a constraint manager, not refutation. These cases were discovered using z3 for refutation, so will require some rework to the PR. Thanks for the comments.

[vabridgers]

Ping! Any comments on the changes I made? I merged the equivalent change in our downstream fork and that resolved the crash on our side. Thanks

[NagyDonat]

I agree that it's unfortunate that we don't have a more general solution for this problem. However, not crashing is still better than crashing, so if nobody has capacity to develop a more general solution, then I think we should still merge this PR (with big TODO notes that ask for a later cleanup) because it's better than the status quo.

Unfortunately I'm not familiar with this "glue" code between the analyzer and Z3, so I cannot help with developing a better solution for this in the foreseeable future. If I understand correctly @vabridgers is also leaning towards merging this quickfix instead of investing additional work into systemic improvements of this area.

@steakhal What do you think about this?

[vabridgers]

Thank you for the comments, @NagyDonat . I'll update the PR accordingly, and respond to the comments.

[vabridgers]

Thanks for the comments @NagyDonat . I believe all comments have been resolved.

[github-actions]

✅ With the latest revision this PR passed the C/C++ code formatter.

[steakhal]

Following this thread gave me a sense of urgency.
I'll admit, it took me much longer to write this comment than doing the review.

I think the patch looks okay, given the circumstances. I'd only highlight here that I think using the argument that anything is better than having a crash - while is true, still leaves a bitter taste.
I have not counted how many similar crashes we had within the Z3 conversion layer, but I still stand by what I've said, that we need to investigate these and put an end to this.
I'll also acknowledge the fact that probably its just a personal bias that @vabridgers, you, happen to stand guard at your fuzzer target/bot (or real user reports) and not only report but also propose quickfixes to the found issues.
I deeply appreciate that.

[NagyDonat]

LGTM.

I'd only highlight here that I think using the argument that anything is better than having a crash - while is true, still leaves a bitter taste.
I have not counted how many similar crashes we had within the Z3 conversion layer, but I still stand by what I've said, that we need to investigate these and put an end to this.

I agree that this leaves a bitter taste. I feel an urge to jump into this and clean up the situation after a through investigation, but there are too many issues where I feel this urge and I think some others are more relevant than this one. (E.g. now I'm working on generalizing the security.ArrayBound logic for other checkers that do bounds checking and I hope that it will provide tangible improvements.)

[vabridgers]

Thanks @NagyDonat and @steakhal for the review comments and acknowledgements. Even characterizing these issues can be difficult, and frankly I would like to do more than just report crashes with reproducers and post half-step solutions. But we are trying to make use of these tools internally in time constrained release cycles, and crashes prevent us from enabling Z3 to refute the cases that we can. Having worked together on these issues in the past, I'm confident you understand my POV here.

I will create a github issue to follow up on the root cause and link this PR.