Skip to content

Commit edd679e

Browse files
author
Vince Bridgers
committed
[clang][analyzer] Correct SMT Layer for _BitInt cases refutations
Since _BitInt was added later, ASTContext did not comprehend getting a type by bitwidth that's not a power of 2, and the SMT layer also did not comprehend this. This led to unexpected crashes using Z3 refutation during randomized testing. The assertion and redacted and summarized crash stack is shown here. clang: ../../clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:103: static llvm::SMTExprRef clang::ento::SMTConv::fromBinOp(llvm::SMTSolverRef &, const llvm::SMTExprRef &, const BinaryOperator::Opcode, const llvm::SMTExprRef &, bool): Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"' failed. ...  #9 <address> clang::ento::SMTConv::fromBinOp(std::shared_ptr<llvm::SMTSolver>&, llvm::SMTExpr const* const&, clang::BinaryOperatorKind, llvm::SMTExpr const* const&, bool) SMTConstraintManager.cpp clang::ASTContext&, llvm::SMTExpr const* const&, clang::QualType, clang::BinaryOperatorKind, llvm::SMTExpr const* const&, clang::QualType, clang::QualType*) SMTConstraintManager.cpp clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&, llvm::APSInt const&, bool) SMTConstraintManager.cpp clang::ento::ExplodedNode const*, clang::ento::PathSensitiveBugReport&)
1 parent ce603a0 commit edd679e

File tree

3 files changed

+44
-4
lines changed

3 files changed

+44
-4
lines changed

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

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -573,20 +573,30 @@ class SMTConv {
573573
return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
574574
}
575575

576+
static inline bool IsPower2(unsigned bits) {
577+
return bits > 0 && (bits & (bits - 1)) == 0;
578+
}
579+
576580
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
577581
static inline std::pair<llvm::APSInt, QualType>
578582
fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
579583
llvm::APSInt NewInt;
584+
unsigned APSIntBitwidth = Int.getBitWidth();
585+
QualType Ty = getAPSIntType(Ctx, Int);
580586

581587
// FIXME: This should be a cast from a 1-bit integer type to a boolean type,
582588
// but the former is not available in Clang. Instead, extend the APSInt
583589
// directly.
584-
if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
590+
if (APSIntBitwidth == 1 && Ty.isNull()) {
585591
NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
592+
Ty = getAPSIntType(Ctx, NewInt);
593+
} else if (!IsPower2(APSIntBitwidth) && !getAPSIntType(Ctx, Int).isNull()) {
594+
Ty = getAPSIntType(Ctx, Int);
595+
NewInt = Int.extend(Ctx.getTypeSize(Ty));
586596
} else
587597
NewInt = Int;
588598

589-
return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
599+
return std::make_pair(NewInt, Ty);
590600
}
591601

592602
// Perform implicit type conversion on binary symbolic expressions.

clang/lib/AST/ASTContext.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13209,9 +13209,16 @@ size_t ASTContext::getSideTableAllocatedMemory() const {
1320913209
/// Returns empty type if there is no appropriate target types.
1321013210
QualType ASTContext::getIntTypeForBitwidth(unsigned DestWidth,
1321113211
unsigned Signed) const {
13212-
TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(DestWidth, Signed);
13212+
// round up to next power of 2 for _BitInt cases
13213+
unsigned pow2DestWidth = llvm::bit_ceil(DestWidth);
13214+
// if (pow2DestWidth == 4) pow2DestWidth = 8;
13215+
if (pow2DestWidth < 8)
13216+
pow2DestWidth = 8;
13217+
13218+
TargetInfo::IntType Ty =
13219+
getTargetInfo().getIntTypeByWidth(pow2DestWidth, Signed);
1321313220
CanQualType QualTy = getFromTargetType(Ty);
13214-
if (!QualTy && DestWidth == 128)
13221+
if (!QualTy && pow2DestWidth == 128)
1321513222
return Signed ? Int128Ty : UnsignedInt128Ty;
1321613223
return QualTy;
1321713224
}

clang/test/Analysis/bitint-z3.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s
2+
// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
3+
// REQUIRES: z3
4+
5+
// The SMTConv layer did not comprehend _BitInt types (because this was an
6+
// evolved feature) and was crashing due to needed updates in 2 places.
7+
// Analysis is expected to find these cases using _BitInt without crashing.
8+
9+
_BitInt(35) a;
10+
int b;
11+
void c() {
12+
int d;
13+
if (a)
14+
b = d; // expected-warning{{Assigned value is uninitialized [core.uninitialized.Assign]}}
15+
}
16+
17+
int *d;
18+
_BitInt(3) e;
19+
void f() {
20+
int g;
21+
d = &g;
22+
e ?: 0; // expected-warning{{Address of stack memory associated with local variable 'g' is still referred to by the global variable 'd' upon returning to the caller. This will be a dangling reference [core.StackAddressEscape]}}
23+
}

0 commit comments

Comments
 (0)