Custom cross check language specification

In many cases, we can add identical cross-checks to the original C and the transpiled Rust code, e.g., when the C code is naively translated to the perfectly equivalent Rust code, and everything just works. However, this might not always be the case, and we need to handle mismatches such as:

• Type mismatches between C and Rust, e.g., a C const char* (with or without an attached length parameter) being translated to a str. Additionally, if a string+length value pair (with the types const char* and size_t) gets translated to a single str, we may want to omit the cross-check on the length parameter.
• Whole functions added or removed by the transpiler or refactoring tool, e.g., helpers.

Note that this list is not exhaustive, so there may be many more cases of mismatches.

To handle all these cases, we need a language that lets us add new cross-checks, or modify or delete existing ones.

The cross-check language

TODO

Inline or external

The simplest way to link each configuration entry to its corresponding cross-check is to write the entries inline in the C/Rust source code. However, this approach could make the Rust code very ugly and difficult to maintain. It would also make it difficult to distribute the Rust code without the associated cross-checks, or distribute them as two separate packages and merge them on the client side.

In the current implementation of the Rust cross-checker, configuration settings are passed to the enclosing scope's #[cross_check] attribute, e.g.:

#[cross_check(yes, name=foo)]
fn bar() { }

#[cross_check(yes, id=0x1234)]
fn baz() { }

An alternative solution is to store all cross-check configuration entries in separate text files that exclusively contain the cross-check information. This solves the aforementioned problems, but comes with its own challenges. When making either manual or automated changes to either the C or Rust code, the corresponding cross-check metadata would have to be kept in sync. Additionally, we would need a mechanism to map configuration entries to their corresponding cross-checks, which is discussed in the next section.

Configuration keys

TODO