z3-based model checking of tnum_scast() implementation from @dkanaliev

tnum_scast_check.py

#!/usr/bin/python3
from uuid import uuid4
from z3 import And, BitVec, BitVecRef, BitVecVal, Implies, prove, ULT, Extract, SignExt, ZeroExt

SIZE = 64 # Working with 64-bit integers

class Tnum:
    """A model of tristate number use in Linux kernel's BPF verifier.
    https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c
    """
    val: BitVecRef
    mask: BitVecRef

    def __init__(self, val=None, mask=None):
        uid = uuid4() # Ensure that the BitVec are uniq, required by the Z3 solver
        self.val = BitVec(f'Tnum-val-{uid}', bv=SIZE) if val is None else val
        self.mask = BitVec(f'Tnum-mask-{uid}', bv=SIZE) if mask is None else mask
    
    def contains(self, bitvec: BitVecRef):
        # Simplified version of tnum_in()
        # https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c#L167-L173
        return (~self.mask & bitvec) == self.val
    
    def wellformed(self):
        # Bit cannot be set in both val and mask, such tnum is not valid
        return self.val & self.mask == BitVecVal(0, bv=SIZE)

# The function that we want to check
# Based on https://github.com/dkanaliev/bpf/blob/b077218/kernel/bpf/tnum.c#L177-L201
def tnum_scast(a: Tnum, size: int):
    s = size * 8 - 1
    sign_mask = BitVecVal(1, bv=SIZE) << s
    value_mask = (BitVecVal(1, bv=SIZE) << (s + 1)) - 1

    new_value = a.val & value_mask
    new_mask = a.mask & value_mask

    sign_bit_unknown = ZeroExt(SIZE - 1, Extract(s, s, a.mask))
    sign_bit_value = ZeroExt(SIZE - 1, Extract(s, s, a.val))

    mask = ~value_mask

    new_mask = new_mask | (mask & -sign_bit_unknown)
    new_value = new_value | (mask & -(~sign_bit_unknown & sign_bit_value))

    return Tnum(new_value, new_mask)

for size in [1, 2, 4]:
    print(f'Proving tnum_scast() work with size={size}')
    t = Tnum()
    x = BitVec('x', SIZE)  # Any possible 64-bit value

    # Premises
    premises = And(
        t.wellformed(),
        t.contains(x),
    )

    # Proof condition
    prove(
        Implies(
            premises,
            tnum_scast(t, size).contains(
                # Simulate signed cast operation
                SignExt(SIZE - size*8, Extract(size*8 - 1, 0, x))
            )
        )
    )

tnum_scast_verify.c

/* Alternative CBMC-based version */
#include <stdint.h>
#include <assert.h>

// Define the tnum structure
struct tnum {
    uint64_t value;
    uint64_t mask;
};

// tnum_scast implementation from tnum.c
struct tnum tnum_scast(struct tnum a, uint8_t size)
{
    uint64_t s = size * 8 - 1;
    uint64_t sign_mask = 1ULL << s;
    uint64_t value_mask = (1ULL << (s + 1)) - 1;

    uint64_t new_value = a.value & value_mask;
    uint64_t new_mask = a.mask & value_mask;

    uint64_t sign_bit_unknown = (a.mask >> s) & 1;
    uint64_t sign_bit_value = (a.value >> s) & 1;

    uint64_t mask = ~value_mask;

    new_mask |= mask & (0 - sign_bit_unknown);
    new_value |= mask & (0 - ((sign_bit_unknown ^ 1) & sign_bit_value));

    return (struct tnum) { .value = new_value, .mask = new_mask };
}

// Helper function to check if a value is contained in a tnum
int tnum_contains(struct tnum a, uint64_t value)
{
    return (~a.mask & value) == a.value;
}

// Verification function
void verify_tnum_scast()
{
    struct tnum t;
    uint64_t x;
    uint8_t size;

    // Use CBMC's built-in nondeterministic functions to generate inputs
    t.value = __CPROVER_unsigned_long_long_input();
    t.mask = __CPROVER_unsigned_long_long_input();
    x = __CPROVER_unsigned_long_long_input();
    size = __CPROVER_unsigned_char_input();

    // Assume valid inputs
    __CPROVER_assume(size > 0 && size <= 8);
    __CPROVER_assume((t.value & t.mask) == 0); // tnum wellformedness
    __CPROVER_assume(tnum_contains(t, x));

    // Perform the cast
    struct tnum result = tnum_scast(t, size);

    // Simulate the signed cast operation
    uint64_t mask = (1ULL << (size * 8)) - 1;
    int64_t signed_x = (int64_t)((x & mask) << (64 - size * 8)) >> (64 - size * 8);

    // Assert that the result contains the casted value
    assert(tnum_contains(result, (uint64_t)signed_x));
}