[clang] [clang][analyzer] Model more getline/getdelim pre and postconditions (PR #83027)

[Balazs Benics via cfe-commits]

Alejandro =?utf-8?q?Álvarez_Ayllón?Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/83027 at github.com>


================
@@ -1183,6 +1315,20 @@ void StreamChecker::evalGetdelim(const FnDescription *Desc,
         State->BindExpr(E.CE, C.getLocationContext(), RetVal);
     StateNotFailed =
         E.assumeBinOpNN(StateNotFailed, BO_GE, RetVal, E.getZeroVal(Call));
+    // The buffer size `*n` must be enough to hold the whole line, and
+    // greater than the return value, since it has to account for '\0'.
+    auto SizePtrSval = Call.getArgSVal(1);
+    auto NVal = getPointeeDefVal(SizePtrSval, State);
+    if (NVal) {
+      StateNotFailed = StateNotFailed->assume(
+          E.SVB
+              .evalBinOp(StateNotFailed, BinaryOperator::Opcode::BO_GT, *NVal,
+                         RetVal, E.SVB.getConditionType())
+              .castAs<DefinedOrUnknownSVal>(),
+          true);
----------------
steakhal wrote:

```suggestion
      StateNotFailed = StateNotFailed->assume(
          E.SVB
              .evalBinOp(StateNotFailed, BO_GT, *NVal, RetVal, E.SVB.getConditionType())
              .castAs<DefinedOrUnknownSVal>(),
          true);
```
I'm worried a bit that we already constrained retVal: `0 <= retVal`, with the previous assumption.
And here `NVal` comes from user code, which we use as an upperbound: `retVal < NVal`, which we assume `true`.
This makes me wonder if we could make them contradict and return us a null state; which we then unconditionally dereference.

Could you have a test for like this?
```
size_t n = -1;
getline(&buffer, &n, F1); // no-crash
```

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