[clang] [clang][analyzer] Fix liveness and analysis of [[assume]] attributes (PR #198618)

[Donát Nagy via cfe-commits]

================
@@ -1224,16 +1224,33 @@ void ExprEngine::VisitLambdaExpr(const LambdaExpr *LE, ExplodedNode *Pred,
 
 void ExprEngine::VisitAttributedStmt(const AttributedStmt *A,
                                      ExplodedNode *Pred, ExplodedNodeSet &Dst) {
+  const LocationContext *LCtx = Pred->getLocationContext();
   ExplodedNodeSet CheckerPreStmt;
   getCheckerManager().runCheckersForPreStmt(CheckerPreStmt, Pred, A, *this);
 
   ExplodedNodeSet EvalSet;
-  NodeBuilder Bldr(CheckerPreStmt, EvalSet, *currBldrCtx);
 
-  for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
-    for (ExplodedNode *N : CheckerPreStmt) {
-      Visit(Attr->getAssumption()->IgnoreParens(), N, EvalSet);
+  for (ExplodedNode *N : CheckerPreStmt) {
+    ProgramStateRef State = N->getState();
+    for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
+      SVal AssumedVal = State->getSVal(Attr->getAssumption(), LCtx);
+      if (auto ValidAssumedVal = AssumedVal.getAs<DefinedOrUnknownSVal>()) {
+        State = State->assume(*ValidAssumedVal, true);
+      } else {
+        // The assumption expression has evaluated to UndefinedVal.
----------------
NagyDonat wrote:

> Traditionally, just because something produced undef, we usually don't terminate the exploration.

You are right that _producing_ an undefined (not just unknown) value is not always reported (e.g. the contents of the buffer returned by `malloc` are undef and this is fine), although even there we have `core.UndefinedBinaryOperatorResult` which reports situations when a binary operator produces undef.

On the other hand, all the reasonably common ways of _using_ undef are all reported by various `core` checkers:
- assigning undef to a variable is reported by `core.uninitialized.Assign`,
- using undef in the condition of a control flow statement is reported by `core.uninitialized.Branch`,
- passing undef to a function is reported by `core.CallAndMessage`, ...

> What is the rationale here?

I think using a value in `[[assume(...)]]`` is analogous to passing it to a function or using it in the condition of an `if`, so the analyzer should behave analogously, i.e. sink the execution path. This would be consistent with the behavior of an `assert(...)` call.

Also, I think it would be very rare to `[[assume(...)]]` expressions that are really undefined, so is suspect that a significant fraction of the (rare) `UndefinedVal`s encountered at this point would be produced by bugs in the analyzer engine. (And in that case discarding the inconsistent state is the right thing to do.)

However I can also accept "just ignore the undefined assumption" if you strongly prefer that.

https://github.com/llvm/llvm-project/pull/198618