[SMT incremental] Produce segfault when verifying a multi-threaded program

[lucasccordeiro]

$ esbmc main.c --no-div-by-zero-check --force-malloc-success --no-align-check --k-step 2 --floatbv --unlimited-k-steps --unwind 2 --compact-trace --context-bound 3 --smt-during-symex

#include <stdlib.h>
#include <pthread.h>

// This is based on the weaver benchmark

int lA=2, lB=2;
int *A, *B; // will be initialized with NONDET
int iA, iB; // initialized with: 0

// increments iA until A[iA] != B[iA]
void* thread1() {
  //int c = 0;
  while(iA < lA && iA < lB)
    if(A[iA] == B[iA]) iA++;
    else break;

  return 0;
}

// increments iB until A[iB] != B[iB]
void* thread2() {

  while(iB < lB && iB < lA)
    if(A[iB] == B[iB]) iB++;
    else break;

  return 0;
}

int main() {
  // Nondet arrays
  A = malloc(sizeof(int) * lA);
  B = malloc(sizeof(int) * lB);

  pthread_t t1, t2;
  pthread_create(&t1, 0, thread1, 0);
  pthread_create(&t2, 0, thread2, 0);
  pthread_join(t1, 0);
  pthread_join(t2, 0);

  __ESBMC_assert(iA == iB, "iA and iB must be equal");
}

This is a previous PR, where @fbrausse solved a segfault in our SMT incremental: https://github.com/esbmc/esbmc/pull/1915.

[XLiZHI]

I learned the SMT code. Under my investigation, I found that the problem comes from assertion.

__ESBMC_assert(iA == iB, "iA and iB must be equal"); It works just fine if we remove this line.

https://github.com/esbmc/esbmc/blob/1af829d440e4f46af3987c7dd606427f95072593/src/goto-symex/symex_target_equation.cpp#L474-L482 An invalid iterator was encountered here. Earlier, we stored some iterators in a list and extracted them.

https://github.com/esbmc/esbmc/blob/1af829d440e4f46af3987c7dd606427f95072593/src/goto-symex/symex_target_equation.cpp#L365-L378 In this method, we seem to have removed some SSA assertions directly, and if we comment out this method, it works just fine.

[lucasccordeiro]

Closed via https://github.com/esbmc/esbmc/issues/2102.