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

[Balázs Benics via cfe-commits]

================
@@ -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