[clang][Checkers] Extend PthreadLockChecker state dump (NFC).

[balazske]

Summary

Add printing of map 'DestroyRetVal'.

[balazske]

This patch makes one TODO less and it is possible to debug cases like in the next (in stack) change.

[NoQ]

That's what i like to see!

You can test this via clang_analyzer_printState().

clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

343

I think this should be passive. The mutex doesn't actively destroy anybody.

[balazske]

clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

343

Maybe "Mutex destroy calls with unknown result:"? This is a title of a list, not about a single mutex.

[NoQ]

clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

343

Oh that's what you meant, I see.

"Mutexes in unresolved possibly destroyed state:"?

[balazske]

Change of text in dump, add a test.

[balazske]

Add accidentally removed empty line.

[steakhal]

clang/test/Analysis/pthreadlock_state.c

55 ↗

(On Diff #331485)

Out of curiosity, what is the purpose of this 'empty' line? I've seen it many times in other tests but I still don't know.

70 ↗

(On Diff #331485)

I recommend not hardcoding symbol identifier numbers. reg$NN, conj_$NN, LCNN, SNNNN
It would result in a less fragile test.
I'm pretty sure you can use some regexp to achieve this.

[balazske]

Add regular expression to test, removed space characters from line endings.

[balazske]

clang/test/Analysis/pthreadlock_state.c

55 ↗

(On Diff #331485)

This is an issue with the state dump, the checker does not print the empty line but the state dump shows it always.

[steakhal]

clang/test/Analysis/pthreadlock_state.c

70 ↗

(On Diff #331485)

AFAIK only the line prefix is checked.
So you could use simply "SymRegion{reg_${{[0-9]+}}<pthread_mutex_t * mtx1>}: conj_$"

Make sure you mask the number out of the reg_$12 as well, etc.

[balazske]

Simplified the test somewhat.

[steakhal]

Everything looks fine.
I like that regexp matcher so much. <3

[balazske]

clang/test/Analysis/pthreadlock_state.c

59 ↗

(On Diff #332293)

This test fails at some buildbots because ordering of the lines ("mtx" and "SymRegion") is reversed.

[steakhal]

clang/test/Analysis/pthreadlock_state.c

59 ↗

(On Diff #332293)

Uh yea. That's a mapping over pointer values - which is nondeterministic.

You have two options. Either rework the test to have a single entry in that mapping at most, or sort them somehow.
TBH I think the first is the easier :D

[balazske]

Test failures occurred, fix of the problem is not trivial, probably the test file should be split.

[balazske]

Test should be updated.

[balazske]

Split the test file.

[steakhal]

clang/test/Analysis/pthreadlock_state.c

1 ↗

(On Diff #334609)

AFAIK core should be enabled for all checks. Same for the other file.

[balazske]

Add 'core' to enabled checks in test.

clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

ProgramStateRef PthreadLockChecker::resolvePossiblyDestroyedMutex(
   ConditionTruthVal retZero = CMgr.isNull(state, *sym);
   if (retZero.isConstrainedFalse()) {
     if (lstate->isUntouchedAndPossiblyDestroyed())
       state = state->remove<LockMap>(lockR);
     else if (lstate->isUnlockedAndPossiblyDestroyed())
       state = state->set<LockMap>(lockR, LockState::getUnlocked());
   } else
     state = state->set<LockMap>(lockR, LockState::getDestroyed());
-
   // Removing the map entry (lockR, sym) from DestroyRetVal as the lock state is
   // now resolved.
   state = state->remove<DestroyRetVal>(lockR);
   return state;
 }
 
 void PthreadLockChecker::printState(raw_ostream &Out, ProgramStateRef State,
                                     const char *NL, const char *Sep) const {
void PthreadLockChecker::printState(raw_ostream &Out, ProgramStateRef State,
   if (!LS.isEmpty()) {
     Out << Sep << "Mutex lock order:" << NL;
     for (auto I : LS) {
       I->dumpToStream(Out);
       Out << NL;
     }
   }
 
-  // TODO: Dump destroyed mutex symbols?
+  DestroyRetValTy DRV = State->get<DestroyRetVal>();
+  if (!DRV.isEmpty()) {
+    Out << Sep << "Mutex destroys with unknown result:" << NL;
+    for (auto I : DRV) {
+      I.first->dumpToStream(Out);
+      Out << ": ";
+      I.second->dumpToStream(Out);
+      Out << NL;
+    }
+  }
 }
 
 void PthreadLockChecker::AcquirePthreadLock(const CallEvent &Call,
                                             CheckerContext &C,
                                             CheckerKind CheckKind) const {
   AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), false,
                  PthreadSemantics, CheckKind);
 }