================
@@ -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
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
