Potential data race in util/gparams.cpp #1604
Description
I found an insufficient synchronization that may cause data race in the following code.
Lines 440 to 448 in c64d044
When the above function returns, the local variable "params_ref result" will be destructed. Thus, if there are two threads calling the function and returning at the same time, the destructor of params_ref, i.e., ~params_ref(), will be called at the same time in the two threads. The code of the destructor is as following:
Lines 507 to 510 in c64d044
Line 509 will be called at the same time, which will crash the program.
The above idea is also verified by Adress Sanitizer, which outputs the following info:
==28245==ERROR: AddressSanitizer: attempting double-free on 0x6060019bb5a0 in thread T3:
#0 0x7fb5392da2ca in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x982ca)
#1 0x7fb538917dfd in memory::deallocate(void*) (/home/qingkaishi/pinpoint/build-asan/Debug+Asserts/bin/../lib/libz3.so+0xee9dfd)
#2 0x7fb538932abe in params_ref::~params_ref() (/home/qingkaishi/pinpoint/build-asan/Debug+Asserts/bin/../lib/libz3.so+0xf04abe)
#3 0x7fb538339fd3 in context_params::context_params() (/home/qingkaishi/pinpoint/build-asan/Debug+Asserts/bin/../lib/libz3.so+0x90bfd3)
#4 0x7fb537abc04f in Z3_mk_config (/home/qingkaishi/pinpoint/build-asan/Debug+Asserts/bin/../lib/libz3.so+0x8e04f)
#5 0x1a28760 in z3::config::config() /home/qingkaishi/pinpoint/build-asan/submodule/SMT/../../../submodule/SMT/third-party/z3/src/api/c++/z3++.h:105
#6 0x1a28954 in z3::context::context() /home/qingkaishi/pinpoint/build-asan/submodule/SMT/../../../submodule/SMT/third-party/z3/src/api/c++/z3++.h:159
A potential fix may move the return statement into the critical section.