Why Infer doesn’t find error with LOCK_CONSISTENCY_VIOLATION?

[junhyung-lee38]

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

• [v0.17.0 ] The version of infer from infer --version.
• [ubuntu14.04 ] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.
• [infer -- gcc ] Which command you ran, for example infer -- make.
• [ ] The full output in a paste, for instance a gist.
• [ok ] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

infer version : v0.17.0 OS : ubuntu 14.04

I used command : infer -- gcc -c testcode.c -lpthread testcode.c is test code including LOCK_CONSISTENCY_VIOLATION error. but, Infer not found this. ( No issue found ) Why Infer doesn’t find this error?

also, I found infer option " --report-custom-error --developer-mode ". It can find incorrect Mutex usage. Where can I find options that aren't in the doc?

Smart guys, please help me.

/*

• Copyright (c) Facebook, Inc. and its affiliates.
• This source code is licensed under the MIT license found in the
• LICENSE file in the root directory of this source tree. */

include

include

include

include

pthread_mutex_t mutex_lock;

int g_count = 0;

void t_function(void data) { int i; char thread_name = (char)data; // critical section g_count = 0;
for (i = 0; i < 5; i++) { printf("%s COUNT %d\n", thread_name, g_count); g_count++; sleep(1); } } int main() { pthread_t p_thread1, p_thread2; int status; pthread_create(&p_thread1, NULL, t_function, (void )"Thread1"); pthread_create(&p_thread2, NULL, t_function, (void )"Thread2"); pthread_join(p_thread1, (void )&status); pthread_join(p_thread2, (void )&status); }

[ngorogiannis]

Infer does not report races on plain C code, only on C++/Obj/Java. Infer also does not recognise pthread_mutex lock operations.

[junhyung-lee38]

Dear ngorogiannis,

Thank you for your prompt reply. It helped me a lot.

If you don't mind can I get some more advice with this brilliant tool ?

I have encountered lots of problems regarding misuse of MUTEX_LOCK (which results in race conditions). So I really would like to detect potential errornous statements in advance before running at real situations.

Below are my questions (or naive ideas ) ... 

1.Are there any plan to make 'infer' smarter by adding feature like recognizing 'pthread_mutex lock' ( Because I really need this for the moment and pthread_mutex is so common in POSIX based OS like Linux ). I'm just wondering if there is any specific reason for not supporting this . It would be very helpful and thankful to support this feature, I think.

2.Is it possible or are there any plans for 'infer' command-line option to provide some efficient way to train additional tokens which could be defined by user (programmer) or some standards ? ( Tokens might be user-defined or C++ STL funtions like std::vector::iterator type and shared variable which is defined as that type ) Actually I got to think about above idea as Ocaml is an language for AI applications, I heard..

They are just naive ideas but it would be appreciated if I could have your thoughtful opinion or answers .

I look forward to hearing from you. Best regards,

[ngorogiannis]

1. Infer does not have a general data race checker. What it focuses on is classes and their methods that may be called concurrently -- this reduces the search space a lot. pthread_mutexes in plain C code make this a lot harder, and since the code we check does not primarily use these features, such support is not planned. We are always open to pull requests :)

2. I don't understand what you mean by tokens.

[junhyung-lee38]

I want to thank you for taking the time out of your busy schedule. Thank you very much!

[i-ky]

@junhyung-lee38 Have you heard about clang's Thread Safety Analysis? It isn't perfect, but it can do a lot and it's a compiler warning, i.e. it's fast. As far as I know, clang already ships C++ standard library with thread safety annotations. I believe you can push libpthreads developers to annotate their headers as well (if they haven't done that already).

[junhyung-lee38]

Dear @ngorogiannis,

Regarding 'Tokens', I assume that Tokens are some kinds of 'Data Types' or 'Identifiers'.

As far as I know, 'Tokens' ( or 'lexeme') are used for Lexical analysis stage and 'Data Types' or 'Idendifiers' are commonly used for Syntax Analysis stage in compiler.

There is one more question.

I want to apply infer to qcc compiler. Is there any way I can do to use qcc compiler (QNX) in infer?