Symex wrongly nondets local variable inherited after START_THREAD

[cesaro]

When cbmc as in current develop is given this program:

int __CPROVER_thread_local thlocal = 4;

int test3 ()
{
  int loc;

  loc = 123;

  __CPROVER_ASYNC_3:
    thlocal = loc,
    __CPROVER_assert (thlocal == 123, "hello");
}

it finds a violation to the assertion using the following equation:

VERIFICATION CONDITIONS:

file test.c line 71 function test3
hello
[...]
{-10} __CPROVER_thread_id!0#1 == 0ul
{-11} __CPROVER_threads_exited#1 == ARRAY_OF(FALSE)
{-12} thlocal!0#1 == 4
{-13} loc!0@1#2 == 123
{-14} __CPROVER_rounding_mode!1#1 == 0
{-15} __CPROVER_thread_id!1#1 == 0ul
{-16} thlocal!1#1 == 4
{-17} main#return_value!1#1 == 0
{-18} test3#return_value!1#1 == 0
{-19} test3#return_value!0#1 == nondet_symbol(symex::nondet0)
{-20} main#return_value!0#1 == 0
{-21} return'!0#1 == 0
{-22} thlocal!1#2 == loc!1@0#0
{-23} !(__CPROVER_dead_object#1$wclk$8 >= __CPROVER_deallocated#1$wclk$8)
{-24} !(__CPROVER_deallocated#1$wclk$8 >= __CPROVER_malloc_is_new_array#1$wclk$8)
{-25} !(__CPROVER_malloc_is_new_array#1$wclk$8 >= __CPROVER_malloc_object#1$wclk$8)
{-26} !(__CPROVER_malloc_object#1$wclk$8 >= __CPROVER_malloc_size#1$wclk$8)
{-27} !(__CPROVER_malloc_size#1$wclk$8 >= __CPROVER_memory_leak#1$wclk$8)
{-28} !(__CPROVER_memory_leak#1$wclk$8 >= __CPROVER_next_thread_id#1$wclk$8)
{-29} !(__CPROVER_next_thread_id#1$wclk$8 >= __CPROVER_pipe_count#1$wclk$8)
{-30} !(__CPROVER_pipe_count#1$wclk$8 >= __CPROVER_threads_exited#1$wclk$8)
{-31} !(__CPROVER_threads_exited#1$wclk$8 >= t1$9$spwnclk$8)
|--------------------------
{1} thlocal!1#2 == 123

in which it is possible to see that the copy of variable loc in thread 1 that is being assigned to the thread-local variable thlocal is a free variable in the equation (loc!1@0#0), which therefore can be assigned any value, thus triggering the assertion violation.

Now, an almost identical code is used in the internal model of pthread_create in src/ansi-c/library to compute a thread id right before a new thread started, and pass it to the thread. There, reading a local variable (loc here, this_thread_id there) from the "host" function (test3 here, pthread_create there) rightly transfers the value from the host function (123 here) to the thread.

@tautschnig, could you explain why this mechanism works correctly in pthread_create but not here?

[tautschnig]

I'm not sure why this loop isn't creating a copy of loc!0 into loc!1 in your example.

[tautschnig]

This will be fixed once #2220 is merged - I'll add it as a regression test.