Expose API to compare abstract state to concrete state

[Alan-Jowett]

Proposal: 1) Assume a series of BPF instructions have been parsed, a control flow graph has been created along with a set of pre and post conditions. 2) Assume that the BPF instructions are being executed one at a time. 3) Prior to executing any BPF instruction the concrete state of the VM should be entailed by the abstract state of the CFG at that label. 4) If the concrete state violated the pre-conditions, then either the pre-conditions or the implementation of the BPF VM are wrong.

Notes from discussion with @dthaler

something like this:
ebpf_domain_t from_inv(pre_invariants.at(label));
to get the expected set of pre-invariants

then create a crab::linear_constraint_t that checks register Y against value Z

then do
if (inv.intersect(cst)) to check it

where cst is the linear constraint

[Alan-Jowett]

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.

[Alan-Jowett]

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.