[clang] [analyzer] Fix null-pointer dereference in PthreadLockChecker (PR #210912)

[Arseniy Zaostrovnykh via cfe-commits]

================
@@ -493,8 +493,11 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
       default:
         llvm_unreachable("Unknown tryLock locking semantics");
       }
-      assert(lockFail && lockSucc);
-      C.addTransition(lockFail);
+      // The state where the lock failed can be infeasible if the constraint
+      // solver only now discovers a contradiction in the accumulated
+      // constraints; only take that transition when it is feasible.
----------------
necto wrote:

It only discovers constraint contradiction in one of the branches. so it does not take the `ProgramStatePair(StInfeasible, StInfeasible);` case.
Roughly that's how it goes:

1. first branch: the complex expression `(global_var >> 48 & (1ULL << 8) - 1)` (call it `x`) is treated as opaque symbol, and it is assumed to be equal to 2. There is a simplification pass in  RangeConstraintManager, but it is moot.
2. second branch: introduces a constraint `(global_var >> 48 & (1ULL << 8) - 1) & 8 != 0`, i.e. `x&8 != 0`. Note that it contradicts the first constraint, but constraint manager does not see this immediately, because there is no simplification pass.
3. Constraining `pthread_mutex_lock()` return value. The checkers invokes `state->assume(*DefinedRetVal, false)` which eventually calls `assumeDualImpl` you cited. `assumeDualImpl` clones the state and introduces 2 different assumptions `ret == 0` and `ret != 0`. Note, that simplification pass runs only when a symbol (`ret`) is constrained to a concrete value, so it runs only in one of the copies. This results in one of the states coming back null, while the other (which is still infeasible / overconstrained) comes non-null.
4. Because of that it returns `ProgramStatePair(StTrue, nullptr)` (a few lines after your snippet).
5. `assume(..., false)` then only takes the second part of that - nullptr, so the checker receives nullptr.

This goes for the `pthread_mutex_lock`. For `pthread_mutex_tryLock` logic is similar, but step 5 is different - it does not select one branch, but returns back both of them, and one of them comes back as nullptr because it was discovered to be infeasible, but since it is only one of the two, it did not hit the `ProgramStatePair(StInfeasible, StInfeasible);` case.

Thank you for the comment. I did not realize this subtlety.
Now that I know more of it, I realize that this fix is symptomatic. There might be another checker with the same problem.

Do you have an idea for a small but more generic fix?

As I understand, many checkers do rely on nullptr states after `assume` calls to detect bugs, so we cannot simply always return "StInfeasible" for all infeasible calls.
Would it make sense to skip simplification when a symbol being assign a concrete value is unrelated to any constraints?
Would it make sense to run simplification not only when introducing a constraint `a == N`, but also `a != N`?

I'm afraid both of the options above aren't quick&safe unlike this, admittedly symptomatic fix.

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