[clang] c94c90b - [analyzer] Fix _Atomic crashes for Z3 symbolic execution (#212050)

[via cfe-commits]

Author: rdevshp
Date: 2026-07-26T15:08:15+01:00
New Revision: c94c90b2efaa46520024b2bc8aa2caa30114cd55

URL: https://github.com/llvm/llvm-project/commit/c94c90b2efaa46520024b2bc8aa2caa30114cd55
DIFF: https://github.com/llvm/llvm-project/commit/c94c90b2efaa46520024b2bc8aa2caa30114cd55.diff

LOG: [analyzer] Fix _Atomic crashes for Z3 symbolic execution (#212050)

This PR fixes _Atomic crashes for Z3 symbolic execution by passing the
types through getAtomicUnqualifiedType and getCanonicalType and skip
casting in fromCast if `FromTy == ToTy && FromBitWidth == ToBitWidth`.

Assisted-by: Codex

Added: 
    clang/test/Analysis/z3/z3-atomic.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 61a71545fb1a6..975536aeb37e9 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -26,11 +26,16 @@ namespace ento {
 class SMTConv {
 public:
   static inline uint64_t getSMTBitWidth(ASTContext &Ctx, QualType Ty) {
+    Ty = getSymbolicValueType(Ty);
     if (Ty->isIntegralOrEnumerationType())
       return Ctx.getIntWidth(Ty);
     return Ctx.getTypeSize(Ty);
   }
 
+  static inline QualType getSymbolicValueType(QualType Ty) {
+    return Ty.getAtomicUnqualifiedType().getCanonicalType();
+  }
+
   // Returns an appropriate sort, given a QualType and it's bit width.
   static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
                                         const QualType &Ty, unsigned BitWidth) {
@@ -270,8 +275,14 @@ class SMTConv {
                                           QualType ToTy, uint64_t ToBitWidth,
                                           QualType FromTy,
                                           uint64_t FromBitWidth) {
-    if ((FromTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType() &&
-         ToTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType()) ||
+    FromTy = getSymbolicValueType(FromTy);
+    ToTy = getSymbolicValueType(ToTy);
+
+    if (FromTy == ToTy && FromBitWidth == ToBitWidth)
+      return Exp;
+
+    if ((FromTy->isIntegralOrEnumerationType() &&
+         ToTy->isIntegralOrEnumerationType()) ||
         (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
         (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
         (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
@@ -467,13 +478,13 @@ class SMTConv {
   getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
              QualType &RetTy, bool *hasComparison) {
     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
-      RetTy = Sym->getType();
+      RetTy = getSymbolicValueType(Sym->getType());
 
       return fromData(Solver, Ctx, SD);
     }
 
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
-      RetTy = Sym->getType();
+      RetTy = getSymbolicValueType(Sym->getType());
 
       QualType FromTy;
       std::optional<llvm::SMTExprRef> Exp =
@@ -485,11 +496,11 @@ class SMTConv {
       // e.g. (signed char) (x > 0)
       if (hasComparison)
         *hasComparison = false;
-      return getCastExpr(Solver, Ctx, Exp.value(), FromTy, Sym->getType());
+      return getCastExpr(Solver, Ctx, Exp.value(), FromTy, RetTy);
     }
 
     if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
-      RetTy = Sym->getType();
+      RetTy = getSymbolicValueType(Sym->getType());
 
       QualType OperandTy;
       std::optional<llvm::SMTExprRef> OperandExp =
@@ -523,7 +534,7 @@ class SMTConv {
       if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
         if (hasComparison)
           *hasComparison = false;
-        return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
+        return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, RetTy);
       }
       return UnaryExp;
     }

diff  --git a/clang/test/Analysis/z3/z3-atomic.c b/clang/test/Analysis/z3/z3-atomic.c
new file mode 100644
index 0000000000000..05dd1952496c8
--- /dev/null
+++ b/clang/test/Analysis/z3/z3-atomic.c
@@ -0,0 +1,20 @@
+// RUN: %clang_analyze_cc1 \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-constraints=unsupported-z3 -verify %s
+// REQUIRES: z3
+// expected-no-diagnostics
+
+void atomic_bool(_Bool input) {
+  _Atomic(_Bool) value = input;
+  if (value) { // no-crash
+  }
+}
+
+typedef _Bool B1;
+typedef _Bool B2;
+
+void atomic_bool_typedef(B1 input) {
+  _Atomic(B2) value = input;
+  if (value) { // no-crash
+  }
+}