Nondeterministic indexes unsound

[pkesseli]

CBMC marks the followong program as safe when run with "-D NONDET_INDEX", which is incorrect. The assertion should fail for index=0, and CBMC works as expected if it is set statically.

C program:

unsigned int *GLOBAL_POINTER[1];

#ifdef NONDET_INDEX
extern int index;
#else
int index;
#endif

void f(void)
{
  unsigned int actual=0u;
  GLOBAL_POINTER[0] = &actual;

  if(index==0)
    *GLOBAL_POINTER[index] = 1u;
  else
    actual = 2u;

  __CPROVER_assume(1u == actual);
}

void main(void)
{
  f();
  f();
  __CPROVER_assert(0==1, "");
}

VCC (nondet index case):

VERIFICATION CONDITIONS:

file combined.c line 26 function main
assertion
{-1} GLOBAL_POINTER#1 == { ((unsigned int *)NULL) }
{-2} __CPROVER_dead_object#1 == NULL
{-3} __CPROVER_deallocated#1 == NULL
{-4} __CPROVER_malloc_is_new_array#1 == FALSE
{-5} __CPROVER_malloc_object#1 == NULL
{-6} __CPROVER_malloc_size#1 == 0u
{-7} __CPROVER_memory_leak#1 == NULL
{-8} __CPROVER_next_thread_id#1 == 0u
{-9} __CPROVER_pipe_count#1 == 0u
{-10} __CPROVER_rounding_mode!0#1 == 0
{-11} __CPROVER_thread_id!0#1 == 0u
{-12} __CPROVER_threads_exited#1 == ARRAY_OF(FALSE)
{-13} actual!0@1#2 == 0u
{-14} GLOBAL_POINTER#2 == { &actual!0@1 }
{-15} \guard#1 == (index#0 == 0)
{-16} actual!0@1#3 == ({ &actual!0@1 }[index#0] == &actual!0@1 ? 1u : 0u)
{-17} invalid_object0#1 == ({ &actual!0@1 }[index#0] == &actual!0@1 ? invalid_ob
ject0#0 : 1u)
{-18} invalid_object0#2 == invalid_object0#0
{-19} actual!0@1#4 == 0u
{-20} actual!0@1#5 == 2u
{-21} invalid_object0#3 == (\guard#1 ? invalid_object0#1 : invalid_object0#2)
{-22} actual!0@1#6 == (\guard#1 ? actual!0@1#3 : 2u)
{-23} actual!0@1#6 == 1u
{-24} actual!0@2#2 == 0u
{-25} GLOBAL_POINTER#3 == { &actual!0@2 }
{-26} \guard#2 == (index#0 == 0)
{-27} actual!0@2#3 == ({ &actual!0@2 }[index#0] == &actual!0@2 ? 1u : 0u)
{-28} actual!0@1#1 == ({ &actual!0@2 }[index#0] == &actual!0@1 && !({ &actual!0@
2 }[index#0] == &actual!0@2) ? 1u : actual!0@1#0)
{-29} invalid_object1#1 == (!({ &actual!0@2 }[index#0] == &actual!0@1) && !({ &a
ctual!0@2 }[index#0] == &actual!0@2) ? 1u : invalid_object1#0)
{-30} invalid_object1#2 == invalid_object1#0
{-31} actual!0@2#4 == 0u
{-32} actual!0@1#2 == actual!0@1#0
{-33} actual!0@2#5 == 2u
{-34} invalid_object1#3 == (\guard#2 ? invalid_object1#1 : invalid_object1#2)
{-35} actual!0@2#6 == (\guard#2 ? actual!0@2#3 : 2u)
{-36} actual!0@1#3 == (\guard#2 ? actual!0@1#1 : actual!0@1#2)
{-37} actual!0@2#6 == 1u
|--------------------------
{1} FALSE

CBMC Version:
32b68ce

[tautschnig]

Just for the record: I'm looking at this, and I'm trying to figure out where {-32} actual!0@1#2 == actual!0@1#0 is coming from.

[tautschnig]

There are two bits that are happening here: 1) an object that has gone out-of-scope is chosen to be assigned to and 2) a phi-node is generated on that same object. The former ought to be optimised away, and the latter should certainly never be done (even though a direct consequence of the former). I'm working on fixes.