Slicer support for Arrays/Structs

[rafaelsamenezes]

This PR intends to expand our slicer to work with fields and structs by replacing the WITH operations with just the plain symbol. SMT solvers have big trouble dealing with all the updates. For example, the following program:

#define N 50
int main()
{  
  int arr[N];
  for (unsigned long i = 0; i < N; i++)
    arr[i] = (int)i;

  __ESBMC_assert(arr[42] == 42, "");
}

Will generate:

Thread 0 file test.c line 9 column 3 function main
ASSIGNMENT ()
arr?1!0&0#44 == (arr?1!0&0#43 WITH [42:=42])
... 
Thread 0 file test.c line 7 column 5 function main
ASSIGNMENT ()
arr?1!0&0#51 == (arr?1!0&0#50 WITH [49:=49])

Thread 0 file test.c line 9 column 3 function main
ASSERT
execution_statet::\guard_exec?0!0 => arr?1!0&0#51[42] == 42
assertion

The increasing number of WITH takes progressively larger solving time. The slicer could replace the with id operations:

Thread 0 file test.c line 9 column 3 function main
ASSIGNMENT ()
arr?1!0&0#44 == (arr?1!0&0#43 WITH [42:=42])
... 
Thread 0 file test.c line 7 column 5 function main
ASSIGNMENT ()
arr?1!0&0#51 == (arr?1!0&0#50

Thread 0 file test.c line 9 column 3 function main
ASSERT
execution_statet::\guard_exec?0!0 => arr?1!0&0#51[42] == 42
assertion

For the program above, changing the N resulted in the following Runtime decision procedure times with Z3 v4.12.4:

N	Master	Array Slicing
50	0.00s	0.00s
500	0.03s	0.001s
5 000	0.141s	0.004s
50 000	18.807s	0.051s
500 000	+300s	5.506s

The implementation still requires a bit of testing, specially when an assertion depends on a symbolic index. Also, it would be great if we had some way of recursively replacing the equivalences. I think this could be done in another pass though.

[fbrausse]

I'm not sure this is sound. You're using the unadorned symbol name as key into the map. The array symbol could be touched in other ways (e.g. by non-constant index), in which case this change would overwrite that, wouldn't it?

[rafaelsamenezes]

I'm not sure this is sound. You're using the unardorned symbol name as key into the map. The array symbol could be touched (e.g. by non-constant index), in which case this change would overwrite that, wouldn't it?

Hm, depends. Right now the pre-requisite is that the index operation in the assertion contains a constant for the index. Similarly, for the WITH operation that its going to be replaced, it needs to be a constant index. Which means that

int n = 1; arr[0] = 1; arr[n] = 2; assert(arr[n] == 2) would not slice anything at all.

The main limitation is... if we have an assert that mix! I guess having a list of array that depends on a symbol should suffice.

[lucasccordeiro]

@rafaelsamenezes: can you please add some regression tests with the corner cases discussed in this issue?

[lucasccordeiro]

@Anthonysdu: can you please evaluate this PR over the RMM project?

[lucasccordeiro]

@rafaelsamenezes: we could also move forward with this PR: #1398.

@Anthonysdu started working on it, but there was not much progress for some reason.

[lucasccordeiro]

#1556 is also related to this PR.

[rafaelsamenezes]

@rafaelsamenezes: we could also move forward with this PR: #1398.

@Anthonysdu started working on it, but there was not much progress for some reason.

Hm, I think that the main issue is that this could increase the Symex time by a lot (since we need to compute huge arrays every time). This is fine for reasonably sized arrays, but computing an array of 50k positions everytime might be not worth (specially when just one index is needed).

The slicer right now is trying to take advantage as a "lazy-evaluation". That being said, it would be great to do the WITH propagation on the sliced SSA!