https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/212050
>From a299379de113e1cdec6c8a0027328ff8ceff5b27 Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Sat, 25 Jul 2026 18:38:44 +0000 Subject: [PATCH 1/3] [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) { + } +} >From fe297093b93d746c7752b26d94cf63c52b4d3149 Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Sun, 26 Jul 2026 10:37:59 +0000 Subject: [PATCH 2/3] Remove redundant -analyzer-checker=core from z3-atomic.c --- clang/test/Analysis/z3/z3-atomic.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Analysis/z3/z3-atomic.c b/clang/test/Analysis/z3/z3-atomic.c index a49ef846bf573..337d62d7a328d 100644 --- a/clang/test/Analysis/z3/z3-atomic.c +++ b/clang/test/Analysis/z3/z3-atomic.c @@ -1,4 +1,4 @@ -// RUN: %clang_analyze_cc1 -analyzer-checker=core \ +// RUN: %clang_analyze_cc1 \ // RUN: -analyzer-checker=core,debug.ExprInspection \ // RUN: -analyzer-constraints=unsupported-z3 -verify %s // REQUIRES: z3 >From f90499981c1d0c9da7c08295558e8f99a835a61c Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Sun, 26 Jul 2026 11:01:28 +0000 Subject: [PATCH 3/3] Add no-crash annotation to z3-atomic.c --- clang/test/Analysis/z3/z3-atomic.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/clang/test/Analysis/z3/z3-atomic.c b/clang/test/Analysis/z3/z3-atomic.c index 337d62d7a328d..4238c074dcba5 100644 --- a/clang/test/Analysis/z3/z3-atomic.c +++ b/clang/test/Analysis/z3/z3-atomic.c @@ -4,6 +4,7 @@ // REQUIRES: z3 // expected-no-diagnostics +// no-crash void atomic_bool(_Bool input) { _Atomic(_Bool) value = input; if (value) { @@ -13,6 +14,7 @@ void atomic_bool(_Bool input) { typedef _Bool B1; typedef _Bool B2; +// no-crash void atomic_bool_typedef(B1 input) { _Atomic(B2) value = input; if (value) { _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
