[clang] 7a9bbe0 - [analyzer] Fix unary/binary op support for SMT symbolic execution (#205078)
via cfe-commits
cfe-commits at lists.llvm.org
Mon Jul 13 05:07:19 PDT 2026
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;
+}
More information about the cfe-commits
mailing list