[all-commits] [llvm/llvm-project] ec8d68: [clang][analyzer] Correct SMT Layer for _BitInt ca...

[vabridgers via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: ec8d68b59f82423e5a6bf452e33ee8c5f64b0edc
      https://github.com/llvm/llvm-project/commit/ec8d68b59f82423e5a6bf452e33ee8c5f64b0edc
  Author: vabridgers <58314289+vabridgers at users.noreply.github.com>
  Date:   2025-06-11 (Wed, 11 Jun 2025)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    A clang/test/Analysis/bitint-z3.c

  Log Message:
  -----------
  [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 at ericsson.com>



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications