[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 ↗

(On Diff #149344)

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

1154 ↗

(On Diff #149344)

that's a separate change, but OK

1426 ↗

(On Diff #149344)

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> ?

1640 ↗

(On Diff #149344)

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 ↗

(On Diff #149344)

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.

1154 ↗

(On Diff #149344)

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?

1426 ↗

(On Diff #149344)

Sure.

[ddcc]

Add test, address comments

[george.karpenkov]

Thanks!

cfe/trunk/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
 }

cfe/trunk/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(); });
+}