CBMC test: s64/u64 intersection after JLE refinement

Formal verification that regs_refine_cond_op(BPF_JLE) followed by deduce_bounds_64_from_64() never produces well-formed but non-intersecting s64 and u64 ranges.

main.c contains a self-contained extract of the following functions from kernel/bpf/verifier.c:

• deduce_bounds_64_from_64
• regs_refine_cond_op (unsigned 64-bit comparisons only)
• is_scalar_branch_taken (unsigned 64-bit comparisons only)

Uses a stripped-down struct bpf_reg_state with only 64-bit bounds (smin/smax/umin/umax).

Property checked

For two registers with arbitrary but valid initial state (each has at least one concrete value satisfying both its u64 and s64 bounds), after applying the BPF_JLE TRUE-branch refinement and re-running deduce_bounds_64_from_64(), the s64 and u64 ranges of each register still intersect.

Usage

make          # run the check
cbmc main.c   # equivalent

Requires cbmc in PATH.