================
@@ -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.
----------------
NagyDonat wrote:
This explanation seems to be suspicious: if we "discover a contradiction in the
accumulated constraints", i.e. we reach a posteriorly overconstrained state,
then the `assume` calls return two copies of the same non-null state [1] which
is marked as posteriorly overconstrained (by a hidden boolean field which
ensures that nodes with this state are marked as sinks).
If this assertion has failed, then it's not a posteriorly overconstrained state
but something else.
-------------------------
[1] see source code in `ConstraintManager::assumeDualImpl`:
```c++
if (!StTrue) {
ProgramStateRef StFalse = Assume(false);
if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
assert(StInfeasible->isPosteriorlyOverconstrained());
// Checkers might rely on the API contract that both returned states
// cannot be null. Thus, we return StInfeasible for both branches because
// it might happen that a Checker uncoditionally uses one of them if the
// other is a nullptr. This may also happen with the non-dual and
// adjacent `assume(true)` and `assume(false)` calls. By implementing
// assume in therms of assumeDual, we can keep our API contract there as
// well.
return ProgramStatePair(StInfeasible, StInfeasible);
}
return ProgramStatePair(nullptr, StFalse);
}
```
https://github.com/llvm/llvm-project/pull/210912
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
