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

[via cfe-commits]

https://github.com/rdevshp created https://github.com/llvm/llvm-project/pull/212050

This PR fixes _Atomic crashes for Z3 symbolic execution.

Assisted-by: Codex

>From a299379de113e1cdec6c8a0027328ff8ceff5b27 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Sat, 25 Jul 2026 18:38:44 +0000
Subject: [PATCH] [analyzer] Fix _Atomic crashes for Z3 symbolic execution

Assisted-by: Codex
---
 .../Core/PathSensitive/SMTConv.h              | 24 +++++++++++++------
 clang/test/Analysis/z3/z3-atomic.c            | 20 ++++++++++++++++
 2 files changed, 37 insertions(+), 7 deletions(-)
 create mode 100644 clang/test/Analysis/z3/z3-atomic.c

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 61a71545fb1a6..2206b0af62f59 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -31,6 +31,10 @@ class SMTConv {
     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 +274,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 +477,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 +495,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 +533,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..a49ef846bf573
--- /dev/null
+++ b/clang/test/Analysis/z3/z3-atomic.c
@@ -0,0 +1,20 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core \
+// 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) {
+  }
+}
+
+typedef _Bool B1;
+typedef _Bool B2;
+
+void atomic_bool_typedef(B1 input) {
+  _Atomic(B2) value = input;
+  if (value) {
+  }
+}