Support for validating pointer-rich formats given a probe to check for pointer validity

[nikswamy]

This PR provides support for a "probe and copy" feature, allowing input formats to contain pointers that will be followed by the validator after a user-provided "probe" function checks that the pointer refers to legal memory for a given extent.

The following example illustrates (from tests/Probe.3d)

extern probe ProbeAndCopy

typedef struct _T {
  UINT32 x { x >= 17 };
  UINT32 y { y >= x };
} T;

entrypoint
typedef struct _S(EVERPARSE_COPY_BUFFER_T dest) {
  UINT8 tag;
  T *t probe (length = 8, destination = dest);
} S;

• You can declare an extern probe function, say ProbeAndCopy. In the generated C code, we produce the following extern declaration for it, which you can provide at link time:

extern BOOLEAN ProbeAndCopy(uint64_t pointer_value, uint64_t length, EVERPARSE_COPY_BUFFER_T destination);

This function should probe the pointer_value​, and if successful, it will copy length​ bytes into destination. You can use whatever existing (typically kernel) primitive you have for this and it should take care of the exception handling etc. and just return a boolean.

• In the specification of the type S​ above, we take a EVERPARSE_COPY_BUFFER_T dest​ as an argument.

• The field t​ of S​ is a pointer to a T​, and the annotation says that it should be probed and copied (using the declared ProbeAndCopy​ in scope) and then the contents of dest​ will be validated to contain a T​.

• You chose how to implement EVERPARSE_COPY_BUFFER_T: EverParse.h defines typedef void* EVERPARSE_COPY_BUFFER_T. So, you can implement that type as you like and call the validator with a pointer to your type; a typical choice is that it can itself be a UINT8* with a length. See https://github.com/project-everest/everparse/blob/8572ec9cf8d3abb49ac76e2a218dbf7fcbb48fbc/src/3d/tests/probe/README.md for more details.

• At the top-level, EverParse gives you the following function to validate an S. When calling it from C, you should make sure that dest​ does not alias base​ (or any other out parameters you may have).
  ​

BOOLEAN CheckS(EVERPARSE_COPY_BUFFER_T dest, uint8_t *base, uint32_t len);

Disjointness preconditions

This required a change to the abstraction of validators and actions. Now, they are indexed by an additional "disjointness precondition", which is used ensure that when validating the contents of a copy buffer, that an action running during that process does not modify the copy buffer itself. For example, the disjointness precondition causes us to (rightfully) reject this specification---to validate S *s we copy into dest, but in the process of validating S we again copy into dest when encountering T *t. This is detected and rejected.

//Nested probing of the same buffer; should fail
entrypoint
typedef struct _R(EVERPARSE_COPY_BUFFER_T dest) {
  UINT8 tag;
  S(dest) *s probe (length = 9, destination = dest);
} R;

Compiler performance

The addition of the disjointness precondition adds an overhead to the verification of all 3D specs, even those that do not use copy buffers, since the abstraction forces us to compute the disjointness precondition anyway. On small specifications, this overhead does not seem to be observable significantly. However, on a large internal benchmark, I measured an end-to-end overhead of around a 20% slowdown in verification time. I am still contemplating ways to reduce that overhead, though at least some overhead seems unavoidable, since we do have to compute this disjointness precondition for soundness. Perhaps there's a way to avoid computing it for the common case in which probing is not used.

[nikswamy]

Note, pointers widths are fixed to UINT64

[nikswamy]

cf. previous remark re pointers

[nikswamy]

This is the main new functionality: turning a validator into an action