Additional context:

1. uBPF has a test case that generates random BPF programs + input data using libfuzzer.
2. It first executes the BPF program using the interpreter with bounds checking and records the final value of R0. Bounds checking today catches out-of-bounds accesss to packet and stack data.
3. Second execution is done using the JIT version and the resulting value of R0 is recorded.
4. If the value of R0 of interperet(BPF) != R0 if JIT(BPF) then there is a bug.

uBPF has been extended to have an option to invoke a debug callout prior to each BPF instruction. As part of the callout it provided a pointer to the stack and a pointer to all the register state.

The idea is to use compare this state to the state maintained by the verifier to assert that uBPF is correctly implementing the instructions.

Proposed API:

/**
 * @brief Given a label and a set of constraints, check if the constraints match the computed state at the label.
 *
 * @param[in,out] os Print output to this stream.
 * @param[in] label The location in the CFG to check against.
 * @param[in] constraints The concrete state to check.
 * @return true If the state is valid.
 * @return false If the state is invalid.
 */
bool ebpf_check_constraints_at_label(
    std::ostream& os,
    const std::string& label,
    const std::set<std::string>& constraints);

Call must first have called either ebpf_analyze_program_for_test or ebpf_verify_program with options->store_pre_invariants.