================
@@ -75,16 +75,28 @@ void
Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
for (const auto &[Sym, Range] : Constraints) {
auto RangeIt = Range.begin();
- llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+ std::optional<llvm::SMTExprRef> SMTConstraintsOpt = SMTConv::getRangeExpr(
RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
/*InRange=*/true);
+ if (!SMTConstraintsOpt) {
+ continue;
+ }
+ auto SMTConstraints = SMTConstraintsOpt.value();
+ bool ShouldAddConstraint = true;
while ((++RangeIt) != Range.end()) {
- SMTConstraints = RefutationSolver->mkOr(
- SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
+ std::optional<llvm::SMTExprRef> ConstraintOpt = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ if (!ConstraintOpt) {
+ ShouldAddConstraint = false;
+ break;
+ }
+ SMTConstraints =
+ RefutationSolver->mkOr(SMTConstraints, ConstraintOpt.value());
+ }
+ if (ShouldAddConstraint) {
+ RefutationSolver->addConstraint(SMTConstraints);
}
- RefutationSolver->addConstraint(SMTConstraints);
----------------
steakhal wrote:
While the other parts are not critical because they only concern the Z3 solver.
This part is in production.
I'm concerned that this code grew by ~3x. It is also concerning that we are
loosening the contract here.
While in the past the result of `getRangeExpr` was never nullopt, now we handle
the case when it might be - while we didn't observe crashes to back this
scenario.
I'd prefer something simpler, and assert and gracefully skip - of even just let
it crash if this assumption is violated.
https://github.com/llvm/llvm-project/pull/205078
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
