[clang] [analyzer] Correct crash in Z3 wrapper (PR #158276)

[via cfe-commits]

llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-clang

Author: None (vabridgers)

<details>
<summary>Changes</summary>

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
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 at -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 at -1{{expression result unused}}
+  }
+}

``````````

</details>


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