[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

344

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

[balazske]

clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

344

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

344

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

56

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.

71

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

56

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

71

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

60

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

[steakhal]

clang/test/Analysis/pthreadlock_state.c

60

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

2

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

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 << "Mutexes in unresolved possibly destroyed state:" << 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);
 }

clang/test/Analysis/pthreadlock_state.c

+// RUN: %clang_analyze_cc1 -analyzer-checker=core,alpha.unix.PthreadLock,debug.ExprInspection 2>&1 %s | FileCheck %s
+
+#include "Inputs/system-header-simulator-for-pthread-lock.h"
+
+#define NULL 0
+
+void clang_analyzer_printState();
+
+pthread_mutex_t mtx;
+
+void test() {
+  clang_analyzer_printState();
+  // CHECK:    "checker_messages": null
+
+  pthread_mutex_init(&mtx, NULL);
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "mtx: unlocked",
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+
+  pthread_mutex_lock(&mtx);
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "mtx: locked",
+  // CHECK-NEXT:      "Mutex lock order:",
+  // CHECK-NEXT:      "mtx",
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+
+  pthread_mutex_unlock(&mtx);
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "mtx: unlocked",
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+
+  int ret = pthread_mutex_destroy(&mtx);
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "mtx: unlocked, possibly destroyed",
+  // CHECK-NEXT:      "Mutexes in unresolved possibly destroyed state:",
+  // CHECK-NEXT:      "mtx: conj_$
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+
+  if (ret)
+    return;
+
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "mtx: destroyed",
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+}

clang/test/Analysis/pthreadlock_state_nottracked.c

+// RUN: %clang_analyze_cc1 -analyzer-checker=core,alpha.unix.PthreadLock,debug.ExprInspection 2>&1 %s | FileCheck %s
+
+#include "Inputs/system-header-simulator-for-pthread-lock.h"
+
+#define NULL 0
+
+void clang_analyzer_printState();
+
+void test(pthread_mutex_t *mtx) {
+  int ret = pthread_mutex_destroy(mtx);
+  clang_analyzer_printState();
+  // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex states:",
+  // CHECK-NEXT:      "SymRegion{reg_$[[REG:[0-9]+]]<pthread_mutex_t * mtx>}: not tracked, possibly destroyed",
+  // CHECK-NEXT:      "Mutexes in unresolved possibly destroyed state:",
+  // CHECK-NEXT:      "SymRegion{reg_$[[REG]]<pthread_mutex_t * mtx>}: conj_$
+  // CHECK-NEXT:      ""
+  // CHECK-NEXT:    ]}
+  if (ret)
+    return;
+  pthread_mutex_init(mtx, NULL);
+}