Test case generation for probes

So far the Z3 test case generation for 3D (#101) was unidimensional and did not support probes (#118)

This PR switches to bidimensional test cases. We instruct Z3 to generate each test case as an array of byte arrays, where the probe "pointer" is an index in the array of arrays, parsed as a little-endian unsigned 64-bit integer. Then, in the test case executable, we implement all probe functions uniformly to "follow" those indices accordingly.

Example

Consider the following 3D specification:

extern probe MyProbe
typedef struct _inner {
  UINT8 contents[2];
} inner;
entrypoint typedef struct _outer(EVERPARSE_COPY_BUFFER_T dest) {
  UINT8 prefix;
  inner *foo probe MyProbe (length = 2, destination = dest);
  UINT8 suffix[3];
} outer;

Then, here is a C representation of a positive test case for outer:

uint8_t witness_0[12] = {18, 1, 0, 0, 0, 0, 0, 0, 0, 42, 17, 29};
uint8_t witness_1[2] = {12, 34};
witness_layer_t witness[2] = {
  { .buf = witness_0, .len = 12 },
  { .buf = witness_1, .len = 2 }
};

In this test case, the initial input buffer passed to the outer validator is witness[0].buf, i.e. witness_0. Then, at offset 1, corresponding to the field foo, this input buffer contains an index into the witness array of arrays, as a little-endian unsigned 64-bit integer: here 1 encoded as 8 little-endian bytes. This instructs the probe function to take the byte array at index 1 in witness, i.e. witness[1].buf , i.e. witness_1, which in turn contains binary data valid wrt. inner. Once witness_1 is validated wrt. inner, outer resumes validation of witness_0 with the remaining 3 bytes for the suffix field.

Z3 constraints

We constrain Z3 to always construct valid such indices and probe sizes: no negative test cases with invalid such pointers will be produced. The reason is twofold:

1. we are testing the data format specification, not the probe function;
2. we do not want to risk producing test cases with cycles (e.g. a single indirection buffer reused by several different probes.)

Produced binary test files

For each test case n, we are producing one binary file for the initial input buffer and one binary file for each indirection buffer. Then, the index i of each such binary file within the array of byte arrays now appears in the name of the file as witness.n.POS.i.validatorname.args.dat (or witness.n.NEG.i.validatorname.args.dat)

Other fixes

This PR also brings a few more (slightly unrelated) fixes:

• The user can now specify --z3_flight_name myflight so that each C test case name starts with witnessmyflight
• Given a module A, for each entrypoint probe B.myprobe in A, 3D now adds #include "B_ExternalAPI.h" into AWrapper.c. With that fix, the probe example now also works in --batch mode.
• This PR adds test case generation tests for ELF.3d and probe/src/Probe.3d

What this PR does not fix

This PR does not add support for probes in the test checker executable generated by --test_checker that takes a binary file name as argument. This test checker executable still only supports unidimensional test cases.