[klee-dev] memcmp generate too many paths

[Sylvain Gault]

Hello,

It seems that when a program use memcmp, klee generate as many path as
the array size since its loop can exit anytime. While all I'm interested
in is whether the arrays are equal or not.

For instance this code would generate 5 paths.

char a1[] = {0, 1, 2, 3};
char a2[sizeof(a1)];

klee_make_symbolic(a2, sizeof(a2), "a2");

if (memcmp(a1, a2, sizeof(a1)))
	printf("Winner!\n");
else
	printf("Loser!\n");


I understand that during the execution of memcmp, there are different
path depending on the loop iteration that exists. But once the
function exists, most of these path end in the exact same state.

But I'm only interested in the paths in my code. So is there a way to
make klee merge the test cases that differ only in the path through the
libc?

My real case has an array of 168 bytes. So a memcmp generate 168 paths
by itself. Which means that the code after it will be run 168 times for
the exact same result. This is a bit insane.


Sylvain Gault