Execution tree based on reduced TB capture yields incorrect results

[moralismercatus]

Using the experimental TB selection for execution tree construction where only those TBs that are capable of conditional branching are used.

Try a simple program e.g.,

if(x == 'c' && y == 'b')
return 1;
else if(x == 'w' && y == 'z')
return 2;
else
return 0;

After convergence, the trace pool claims to only have 3 non-redundant traces.

I believe there should be 4 non-redundant traces.

[moralismercatus]

Regardless of the original sample used, the following clearly shows the inadequacy of the approach:

int counter = 0;
char in[100];
for (int i = 0; i < 100; ++i)
  if (in[i] == 'C')
    ++counter;
if (counter == 42)
  ...;

The problem with this is that, by only capturing the 'branching' TB - the one that corresponds to if (in[i] == 'C'), this will effectively yield the same single trace sequence. Whereas, there are actually 2^100 paths through the loop. The execution tree will think every trace dump is a redundant trace.

This fact was actually realized while debugging taint analysis without the experimental reduced TB capture for the execution tree. The effect is the same though: when in is the only symbolic, only the TB for if (in[i] == 'C') is captured, and thus the execution tree rejects all subsequent traces as being redundant.