llvm-project
ec8d68b5 - [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (#143310)

Commit
89 days ago
[clang][analyzer] Correct SMT Layer for _BitInt cases refutations (#143310) 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. ... <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&) --------- Co-authored-by: Vince Bridgers <vince.a.bridgers@ericsson.com>
Author
Parents
Loading