[analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager

[ddcc]

Summary

Clang does not have a corresponding QualType for a 1-bit APSInt, so use the BoolTy and extend the APSInt. Split from D35450. Fixes PR37622.

[george.karpenkov]

Thanks! Looks good with minor changes.

Would it be possible to add tests? I know we have very few unit tests, but I assume you could actually use an integration test to exercise this path?

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1044–1047

What does L stand for here? It's confusing because L/R usually stand for left/right-hand-side in this context.

1156

that's a separate change, but OK

1430

It's redundant to mutate the argument passed by reference and also return it.
Could we take a single APSInt parameter by value and return std::pair<APSInt, QualType> ?

1641–1643

that's a separate change, but OK

[vlad.tsyrklevich]

In D47603#1118106, @george.karpenkov wrote:

Would it be possible to add tests? I know we have very few unit tests, but I assume you could actually use an integration test to exercise this path?

I tested this change and it fixes PR37622. There's a simple crash reproducer included there.

[ddcc]

In D47603#1118138, @vlad.tsyrklevich wrote:

In D47603#1118106, @george.karpenkov wrote:

Would it be possible to add tests? I know we have very few unit tests, but I assume you could actually use an integration test to exercise this path?

I tested this change and it fixes PR37622. There's a simple crash reproducer included there.

Cool, thanks for the repro! It's been long enough since I've touched this code that I don't recall the original failing testcase. I'll add the test to this revision.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1044–1047

They correspond to the inferred left/right hand-side inferred types, but inside the subsequent Z3Expr LHS and RHS variables. This is confusing, so I'll rename them to FromTy and ToTy.

1156

Yeah, this is one of several small miscellaneous changes that didn't make the original commit. It seemed a bit excessive to open separate revisions for each, so I've just been merging them into the next patch. I'm not sure which is preferable?

1430

Sure.

[ddcc]

Add test, address comments

[george.karpenkov]

Thanks!

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

private:
   //===------------------------------------------------------------------===//
   // Helper functions.
   //===------------------------------------------------------------------===//
 
   // Recover the QualType of an APSInt.
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt &Int) const;
 
+  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+  std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
+
   // Perform implicit type conversion on binary symbolic expressions.
   // May modify all input parameters.
   // TODO: Refactor to use built-in conversion functions
   void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
                         QualType &RTy) const;
 
   // Perform implicit integer type conversion.
   // May modify all input parameters.

 
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
   Z3Expr Exp = getZ3Expr(Sym, &RetTy);
 
-  assert((getAPSIntType(From) == getAPSIntType(To)) &&
-         "Range values have different types!");
-  QualType RTy = getAPSIntType(From);
-  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
-  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
-  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+  QualType FromTy;
+  llvm::APSInt NewFromInt;
+  std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+  Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
 
   // Construct single (in)equality
   if (From == To)
     return assumeZ3Expr(State, Sym,
                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
-                                     FromExp, RTy, nullptr));
+                                     FromExp, FromTy, nullptr));
 
+  QualType ToTy;
+  llvm::APSInt NewToInt;
+  std::tie(NewToInt, ToTy) = fixAPSInt(To);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+  assert(FromTy == ToTy && "Range values have different types!");
   // Construct two (in)equalities, and a logical and/or
-  Z3Expr LHS =
-      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+  Z3Expr LHS = getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp,
+                            FromTy, nullptr);
   Z3Expr RHS =
-      getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
+      getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, nullptr);
   return assumeZ3Expr(
       State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                        RetTy->isSignedIntegerOrEnumerationType()));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                                           SymbolRef Sym,
                                                           bool Assumption) {
   // Skip anything that is unsupported
   return State;
 }
else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
     return false;
 
   // Zero may be a solution
   return ConditionTruthVal();
 }
 
 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
                                                    SymbolRef Sym) const {
-  BasicValueFactory &BV = getBasicVals();
-  ASTContext &Ctx = BV.getContext();
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
 
   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
     QualType Ty = Sym->getType();
     assert(!Ty->isRealFloatingType());
     llvm::APSInt Value(Ctx.getTypeSize(Ty),
                        !Ty->isSignedIntegerOrEnumerationType());
 
     Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
Z3Expr NotExp = Z3Expr::fromBinOp(
                             : Z3Expr::fromAPSInt(Value),
         false);
 
     Solver.addConstraint(NotExp);
     if (Solver.check() == Z3_L_TRUE)
       return nullptr;
 
     // This is the only solution, store it
-    return &BV.getValue(Value);
+    return &BVF.getValue(Value);
   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
     SymbolRef CastSym = SC->getOperand();
     QualType CastTy = SC->getType();
     // Skip the void type
     if (CastTy->isVoidType())
       return nullptr;
 
     const llvm::APSInt *Value;
     if (!(Value = getSymVal(State, CastSym)))
       return nullptr;
-    return &BV.Convert(SC->getType(), *Value);
+    return &BVF.Convert(SC->getType(), *Value);
   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
     const llvm::APSInt *LHS, *RHS;
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
       LHS = getSymVal(State, SIE->getLHS());
       RHS = &SIE->getRHS();
     } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
       LHS = &ISE->getLHS();
       RHS = getSymVal(State, ISE->getRHS());
     } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
       // Early termination to avoid expensive call
       LHS = getSymVal(State, SSM->getLHS());
       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
     } else {
       llvm_unreachable("Unsupported binary expression to get symbol value!");
     }
 
     if (!LHS || !RHS)
       return nullptr;
 
     llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
     QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
     doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
         ConvertedLHS, LTy, ConvertedRHS, RTy);
-    return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
   }
 
   llvm_unreachable("Unsupported expression to get symbol value!");
 }
 
 ProgramStateRef
 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
                                         SymbolReaper &SymReaper) {

 
 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
                                             bool *hasComparison,
                                             QualType *RetTy) const {
   QualType LTy, RTy;
   BinaryOperator::Opcode Op = BSE->getOpcode();
 
   if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-    RTy = getAPSIntType(SIE->getRHS());
     Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
-    Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+    llvm::APSInt NewRInt;
+    std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
+    Z3Expr RHS = Z3Expr::fromAPSInt(NewRInt);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-    LTy = getAPSIntType(ISE->getLHS());
-    Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+    llvm::APSInt NewLInt;
+    std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
+    Z3Expr LHS = Z3Expr::fromAPSInt(NewLInt);
     Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
     Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
     Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else {
     llvm_unreachable("Unsupported BinarySymExpr type!");

 // Helper functions.
 //===------------------------------------------------------------------===//
 
 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
 }
 
+std::pair<llvm::APSInt, QualType>
+Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
+  llvm::APSInt NewInt;
+
+  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+  // but the former is not available in Clang. Instead, extend the APSInt
+  // directly.
+  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+    ASTContext &Ctx = getBasicVals().getContext();
+    NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+  } else
+    NewInt = Int;
+
+  return std::make_pair(NewInt, getAPSIntType(NewInt));
+}
+
 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
                                            QualType &LTy, QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
       RTy->isIntegralOrEnumerationType()) {
     if (LTy->isArithmeticType() && RTy->isArithmeticType())
       return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
   } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
     return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
   } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
   // TODO: Refine behavior for invalid type casts
 }
 
 template <typename T,
           T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
                                               QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
-
   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Always perform integer promotion before checking type equality.
   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
   if (LTy->isPromotableIntegerType()) {
     QualType NewTy = Ctx.getPromotedIntegerType(LTy);
     uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
     LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
     LTy = NewTy;
     LBitWidth = NewBitWidth;

 
 #endif
 
 std::unique_ptr<ConstraintManager>
 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
-  llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
+                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           false);
   return nullptr;
 #endif
 }

test/Analysis/apsint.c

+// REQUIRES: z3
+// RUN: %clang_analyze_cc1 -triple x86_64-unknown-linux-gnu -analyzer-checker=core -verify %s
+// expected-no-diagnostics
+
+_Bool a() {
+  return !({ a(); });
+}