Author: rdevshp
Date: 2026-07-13T13:07:14+01:00
New Revision: 7a9bbe00493434ad70bd3de0840c980fd88abde6

URL: 
https://github.com/llvm/llvm-project/commit/7a9bbe00493434ad70bd3de0840c980fd88abde6
DIFF: 
https://github.com/llvm/llvm-project/commit/7a9bbe00493434ad70bd3de0840c980fd88abde6.diff

LOG: [analyzer] Fix unary/binary op support for SMT symbolic execution (#205078)

SMT symbolic execution: 

The patch fixes unary op support, converts operands of logical operators
to boolean in getBinExpr, and clears the hasComparison flag in
getSymExpr when a boolean operand is converted to a non-bool integer.

This PR allows C functions like 
```
int f(int x, int y) {
  if (~(x && y))
    return 0;
  return 1;
}
```
to be analyzed with `-cc1 -analyze -analyzer-checker=core
-analyzer-constraints=z3`

Fixes #205037.

Assisted-by: Codex

Added: 
    clang/test/Analysis/z3/z3-logicalexpr-eval.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
    clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
    clang/test/Analysis/z3/z3-unarysymexpr.c

Removed: 
    


################################################################################
diff  --git 
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
index ef04f9c485e88..38eaabf74dd34 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
@@ -265,6 +265,9 @@ class BasicValueFactory {
   accumCXXBase(llvm::iterator_range<CastExpr::path_const_iterator> PathRange,
                const nonloc::PointerToMember &PTM, const clang::CastKind 
&kind);
 
+  std::optional<APSIntPtr> evalAPSInt(UnaryOperator::Opcode Op,
+                                      const llvm::APSInt &V1);
+
   std::optional<APSIntPtr> evalAPSInt(BinaryOperator::Opcode Op,
                                       const llvm::APSInt &V1,
                                       const llvm::APSInt &V2);

diff  --git 
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 7ea6d4ee3b72e..88902aeddb96e 100644
--- 
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -52,17 +52,19 @@ class SMTConstraintManager : public 
clang::ento::SimpleConstraintManager {
     QualType RetTy;
     bool hasComparison;
 
-    llvm::SMTExprRef Exp =
+    std::optional<llvm::SMTExprRef> Exp =
         SMTConv::getExpr(Solver, Ctx, Sym, RetTy, &hasComparison);
-
+    if (!Exp)
+      return assumeSymUnsupported(State, Sym, Assumption);
     // Create zero comparison for implicit boolean cast, with reversed
     // assumption
     if (!hasComparison && !RetTy->isBooleanType())
       return assumeExpr(
           State, Sym,
-          SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
+          SMTConv::getZeroExpr(Solver, Ctx, Exp.value(), RetTy, !Assumption));
 
-    return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
+    return assumeExpr(State, Sym,
+                      Assumption ? Exp.value() : Solver->mkNot(Exp.value()));
   }
 
   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
@@ -70,8 +72,11 @@ class SMTConstraintManager : public 
clang::ento::SimpleConstraintManager {
                                           const llvm::APSInt &To,
                                           bool InRange) override {
     ASTContext &Ctx = getBasicVals().getContext();
-    return assumeExpr(
-        State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, 
InRange));
+    std::optional<llvm::SMTExprRef> Expr =
+        SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange);
+    if (!Expr)
+      return assumeSymUnsupported(State, Sym, false);
+    return assumeExpr(State, Sym, Expr.value());
   }
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
@@ -89,13 +94,16 @@ class SMTConstraintManager : public 
clang::ento::SimpleConstraintManager {
 
     QualType RetTy;
     // The expression may be casted, so we cannot call getZ3DataExpr() directly
-    llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, RetTy);
-    llvm::SMTExprRef Exp =
-        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
+    std::optional<llvm::SMTExprRef> VarExp =
+        SMTConv::getExpr(Solver, Ctx, Sym, RetTy);
+    if (!VarExp)
+      return ConditionTruthVal();
+    llvm::SMTExprRef Exp = SMTConv::getZeroExpr(Solver, Ctx, VarExp.value(),
+                                                RetTy, /*Assumption=*/true);
 
     // Negate the constraint
-    llvm::SMTExprRef NotExp =
-        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
+    llvm::SMTExprRef NotExp = SMTConv::getZeroExpr(Solver, Ctx, VarExp.value(),
+                                                   RetTy, 
/*Assumption=*/false);
 
     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
     ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
@@ -171,6 +179,14 @@ class SMTConstraintManager : public 
clang::ento::SimpleConstraintManager {
       return BVF.Convert(SC->getType(), *Value).get();
     }
 
+    if (const auto *USE = dyn_cast<UnarySymExpr>(Sym)) {
+      const llvm::APSInt *Value;
+      if (!(Value = getSymVal(State, USE->getOperand())))
+        return nullptr;
+      std::optional<APSIntPtr> Res = BVF.evalAPSInt(USE->getOpcode(), *Value);
+      return Res ? Res.value().get() : nullptr;
+    }
+
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       const llvm::APSInt *LHS, *RHS;
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
@@ -281,10 +297,8 @@ class SMTConstraintManager : public 
clang::ento::SimpleConstraintManager {
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
-    // UnarySymExpr support is not yet implemented in the Z3 wrapper.
-    if (isa<UnarySymExpr>(Sym)) {
-      return false;
-    }
+    if (const auto *USE = dyn_cast<UnarySymExpr>(Sym))
+      return canReasonAbout(SVB.makeSymbolVal(USE->getOperand()));
 
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))

diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index c8c7a1ac7cc45..a494177372b6e 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -342,24 +342,56 @@ class SMTConv {
                     Ctx.getTypeSize(FromTy));
   }
 
+  static inline std::optional<llvm::SMTExprRef>
+  convertToBoolExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
+                    const llvm::SMTExprRef &Exp, QualType Ty) {
+    if (Ty->isBooleanType())
+      return Exp;
+
+    if (Ty->isRealFloatingType()) {
+      llvm::APFloat Zero =
+          llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+      return fromFloatBinOp(Solver, Exp, BO_NE, Solver->mkFloat(Zero));
+    }
+
+    if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
+        Ty->isBlockPointerType() || Ty->isReferenceType())
+      return fromBinOp(Solver, Exp, BO_NE,
+                       Solver->mkBitvector(llvm::APSInt::getUnsigned(0),
+                                           Ctx.getTypeSize(Ty)),
+                       Ty->isSignedIntegerOrEnumerationType());
+    assert(false && "Unsupported type for boolean conversion!");
+    return std::nullopt;
+  }
+
   // Wrapper to generate SMTSolverRef from unpacked binary symbolic
   // expression. Sets the RetTy parameter. See getSMTSolverRef().
-  static inline llvm::SMTExprRef
+  static inline std::optional<llvm::SMTExprRef>
   getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
              const llvm::SMTExprRef &LHS, QualType LTy,
              BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
              QualType RTy, QualType &RetTy) {
     llvm::SMTExprRef NewLHS = LHS;
     llvm::SMTExprRef NewRHS = RHS;
-    doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
 
     // Update the return type parameter if the output type has changed.
     // A boolean result can be represented as an integer type in C/C++, but at
     // this point we only care about the SMT sorts. Set it as a boolean type
     // to avoid subsequent SMT errors.
-    if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) 
{
+    if (BinaryOperator::isComparisonOp(Op)) {
+      doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
+      RetTy = Ctx.BoolTy;
+    } else if (BinaryOperator::isLogicalOp(Op)) {
       RetTy = Ctx.BoolTy;
+      auto LHSOpt = convertToBoolExpr(Solver, Ctx, LHS, LTy);
+      auto RHSOpt = convertToBoolExpr(Solver, Ctx, RHS, RTy);
+      if (!LHSOpt || !RHSOpt)
+        return std::nullopt;
+      NewLHS = LHSOpt.value();
+      NewRHS = RHSOpt.value();
+      return fromBinOp(Solver, NewLHS, Op, NewRHS, false);
     } else {
+      doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
       RetTy = LTy;
     }
 
@@ -377,22 +409,23 @@ class SMTConv {
 
   // Wrapper to generate SMTSolverRef from BinarySymExpr.
   // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
-  static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
-                                               ASTContext &Ctx,
-                                               const BinarySymExpr *BSE,
-                                               bool *hasComparison,
-                                               QualType &RetTy) {
+  static inline std::optional<llvm::SMTExprRef>
+  getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
+                const BinarySymExpr *BSE, bool *hasComparison,
+                QualType &RetTy) {
     QualType LTy, RTy;
     BinaryOperator::Opcode Op = BSE->getOpcode();
 
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-      llvm::SMTExprRef LHS =
+      std::optional<llvm::SMTExprRef> LHS =
           getSymExpr(Solver, Ctx, SIE->getLHS(), LTy, hasComparison);
+      if (!LHS)
+        return std::nullopt;
       llvm::APSInt NewRInt;
       std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
       llvm::SMTExprRef RHS =
           Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
-      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+      return getBinExpr(Solver, Ctx, LHS.value(), LTy, Op, RHS, RTy, RetTy);
     }
 
     if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
@@ -400,28 +433,33 @@ class SMTConv {
       std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
       llvm::SMTExprRef LHS =
           Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
-      llvm::SMTExprRef RHS =
+      std::optional<llvm::SMTExprRef> RHS =
           getSymExpr(Solver, Ctx, ISE->getRHS(), RTy, hasComparison);
-      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+      if (!RHS)
+        return std::nullopt;
+      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS.value(), RTy, RetTy);
     }
 
     if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-      llvm::SMTExprRef LHS =
+      std::optional<llvm::SMTExprRef> LHS =
           getSymExpr(Solver, Ctx, SSM->getLHS(), LTy, hasComparison);
-      llvm::SMTExprRef RHS =
+      std::optional<llvm::SMTExprRef> RHS =
           getSymExpr(Solver, Ctx, SSM->getRHS(), RTy, hasComparison);
-      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+      if (!LHS || !RHS)
+        return std::nullopt;
+      return getBinExpr(Solver, Ctx, LHS.value(), LTy, Op, RHS.value(), RTy,
+                        RetTy);
     }
 
-    llvm_unreachable("Unsupported BinarySymExpr type!");
+    assert(false && "Unsupported BinarySymExpr type!");
+    return std::nullopt;
   }
 
   // Recursive implementation to unpack and generate symbolic expression.
   // Sets the hasComparison and RetTy parameters. See getExpr().
-  static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
-                                            ASTContext &Ctx, SymbolRef Sym,
-                                            QualType &RetTy,
-                                            bool *hasComparison) {
+  static inline std::optional<llvm::SMTExprRef>
+  getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
+             QualType &RetTy, bool *hasComparison) {
     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
       RetTy = Sym->getType();
 
@@ -432,39 +470,45 @@ class SMTConv {
       RetTy = Sym->getType();
 
       QualType FromTy;
-      llvm::SMTExprRef Exp =
+      std::optional<llvm::SMTExprRef> Exp =
           getSymExpr(Solver, Ctx, SC->getOperand(), FromTy, hasComparison);
-
+      if (!Exp)
+        return std::nullopt;
       // Casting an expression with a comparison invalidates it. Note that this
       // must occur after the recursive call above.
       // e.g. (signed char) (x > 0)
       if (hasComparison)
         *hasComparison = false;
-      return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
+      return getCastExpr(Solver, Ctx, Exp.value(), FromTy, Sym->getType());
     }
 
     if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
       RetTy = Sym->getType();
 
       QualType OperandTy;
-      llvm::SMTExprRef OperandExp =
+      std::optional<llvm::SMTExprRef> OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), OperandTy, hasComparison);
-
+      if (!OperandExp)
+        return std::nullopt;
       // When the operand is a bool expr, but the operator is an integeral
       // operator, casting the bool expr to the integer before creating the
       // unary operator.
       // E.g. -(5 && a)
       if (OperandTy == Ctx.BoolTy && OperandTy != RetTy &&
           RetTy->isIntegerType()) {
-        OperandExp = fromCast(Solver, OperandExp, RetTy, 
Ctx.getTypeSize(RetTy),
-                              OperandTy, 1);
+
+        if (hasComparison)
+          *hasComparison = false;
+
+        OperandExp = fromCast(Solver, OperandExp.value(), RetTy,
+                              Ctx.getTypeSize(RetTy), OperandTy, 1);
         OperandTy = RetTy;
       }
 
       llvm::SMTExprRef UnaryExp =
           OperandTy->isRealFloatingType()
-              ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
-              : fromUnOp(Solver, USE->getOpcode(), OperandExp);
+              ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp.value())
+              : fromUnOp(Solver, USE->getOpcode(), OperandExp.value());
 
       // Currently, without the `support-symbolic-integer-casts=true` option,
       // we do not emit `SymbolCast`s for implicit casts.
@@ -479,25 +523,24 @@ class SMTConv {
     }
 
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-      llvm::SMTExprRef Exp =
+      std::optional<llvm::SMTExprRef> Exp =
           getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
       // Set the hasComparison parameter, in post-order traversal order.
       if (hasComparison)
         *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
       return Exp;
     }
-
-    llvm_unreachable("Unsupported SymbolRef type!");
+    assert(false && "Unsupported SymbolRef type!");
+    return std::nullopt;
   }
 
   // Generate an SMTSolverRef that represents the given symbolic expression.
   // Sets the hasComparison parameter if the expression has a comparison
   // operator. Sets the RetTy parameter to the final return type after
   // promotions and casts.
-  static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
-                                         ASTContext &Ctx, SymbolRef Sym,
-                                         QualType &RetTy,
-                                         bool *hasComparison = nullptr) {
+  static inline std::optional<llvm::SMTExprRef>
+  getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
+          QualType &RetTy, bool *hasComparison = nullptr) {
     if (hasComparison) {
       *hasComparison = false;
     }
@@ -536,7 +579,7 @@ class SMTConv {
 
   // Wrapper to generate SMTSolverRef from a range. If From == To, an
   // equality will be created instead.
-  static inline llvm::SMTExprRef
+  static inline std::optional<llvm::SMTExprRef>
   getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
                const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) 
{
     // Convert lower bound
@@ -548,13 +591,15 @@ class SMTConv {
 
     // Convert symbol
     QualType SymTy;
-    llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, SymTy);
-
+    std::optional<llvm::SMTExprRef> Exp = getExpr(Solver, Ctx, Sym, SymTy);
+    if (!Exp)
+      return std::nullopt;
     // Construct single (in)equality
     if (From == To) {
       QualType UnusedRetTy;
-      return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
-                        FromExp, FromTy, /*RetTy=*/UnusedRetTy);
+      return getBinExpr(Solver, Ctx, Exp.value(), SymTy,
+                        InRange ? BO_EQ : BO_NE, FromExp, FromTy,
+                        /*RetTy=*/UnusedRetTy);
     }
 
     QualType ToTy;
@@ -566,15 +611,16 @@ class SMTConv {
 
     // Construct two (in)equalities, and a logical and/or
     QualType UnusedRetTy;
-    llvm::SMTExprRef LHS =
-        getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
-                   FromTy, /*RetTy=*/UnusedRetTy);
-    llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
-                                      InRange ? BO_LE : BO_GT, ToExp, ToTy,
-                                      /*RetTy=*/UnusedRetTy);
-
-    return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
-                     SymTy->isSignedIntegerOrEnumerationType());
+    std::optional<llvm::SMTExprRef> LHS =
+        getBinExpr(Solver, Ctx, Exp.value(), SymTy, InRange ? BO_GE : BO_LT,
+                   FromExp, FromTy, /*RetTy=*/UnusedRetTy);
+    std::optional<llvm::SMTExprRef> RHS = getBinExpr(
+        Solver, Ctx, Exp.value(), SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
+        /*RetTy=*/UnusedRetTy);
+    if (!LHS || !RHS)
+      return std::nullopt;
+    return fromBinOp(Solver, LHS.value(), InRange ? BO_LAnd : BO_LOr,
+                     RHS.value(), SymTy->isSignedIntegerOrEnumerationType());
   }
 
   // Recover the QualType of an APSInt.

diff  --git a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp 
b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
index c905ee6bc9fc9..b86f0e8309dc7 100644
--- a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
@@ -242,12 +242,28 @@ const PointerToMemberData 
*BasicValueFactory::accumCXXBase(
   return getPointerToMemberData(ND, BaseSpecList);
 }
 
+std::optional<APSIntPtr> BasicValueFactory::evalAPSInt(UnaryOperator::Opcode 
Op,
+                                                       const llvm::APSInt &V1) 
{
+  switch (Op) {
+  default:
+    assert(false && "Invalid Opcode.");
+    return std::nullopt;
+
+  case UO_Minus:
+    return getValue(-V1);
+
+  case UO_Not:
+    return getValue(~V1);
+  }
+}
+
 std::optional<APSIntPtr>
 BasicValueFactory::evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt 
&V1,
                               const llvm::APSInt &V2) {
   switch (Op) {
     default:
-      llvm_unreachable("Invalid Opcode.");
+      assert(false && "Invalid Opcode.");
+      return std::nullopt;
 
     case BO_Mul:
       return getValue(V1 * V2);

diff  --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp 
b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
index f965bfb590d80..f609798042639 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -75,14 +75,17 @@ void 
Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
   for (const auto &[Sym, Range] : Constraints) {
     auto RangeIt = Range.begin();
 
-    llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
-        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
-        /*InRange=*/true);
+    llvm::SMTExprRef SMTConstraints =
+        SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, RangeIt->From(),
+                              RangeIt->To(),
+                              /*InRange=*/true)
+            .value();
     while ((++RangeIt) != Range.end()) {
       SMTConstraints = RefutationSolver->mkOr(
           SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
                                                 RangeIt->From(), RangeIt->To(),
-                                                /*InRange=*/true));
+                                                /*InRange=*/true)
+                              .value());
     }
     RefutationSolver->addConstraint(SMTConstraints);
   }

diff  --git a/clang/test/Analysis/z3/z3-logicalexpr-eval.c 
b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
new file mode 100644
index 0000000000000..2f2fb2e94b7d5
--- /dev/null
+++ b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
@@ -0,0 +1,13 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-constraints=z3 -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void unary_not_logical_result(int x, int y) {
+  clang_analyzer_eval(~(x && y) != 0); // expected-warning{{TRUE}}
+}
+
+void unary_minus_logical_result(int x, int y) {
+  clang_analyzer_eval(-(x && y) <= 0); // expected-warning{{TRUE}}
+}

diff  --git a/clang/test/Analysis/z3/z3-unarysymexpr.c 
b/clang/test/Analysis/z3/z3-unarysymexpr.c
index bcdc2b6a66f10..1a29f7a23727d 100644
--- a/clang/test/Analysis/z3/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3/z3-unarysymexpr.c
@@ -60,3 +60,10 @@ long z3_crash3(long a) {
   }
   return 0;
 }
+
+// Previously Z3 analysis crashed in this case, validate
+// that this no longer happens.
+// no-crash: GH #205037
+int unary_operand_in_binary_op(int size, int mask) {
+  return size & ~mask;
+}


        
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to