Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Missing API for BitVectors #332

Open
the-ssd opened this issue Jan 5, 2025 · 0 comments · May be fixed by #333
Open

Missing API for BitVectors #332

the-ssd opened this issue Jan 5, 2025 · 0 comments · May be fixed by #333

Comments

@the-ssd
Copy link

the-ssd commented Jan 5, 2025

Z3 can make bitvectors from arrays of bools. Something like this should work (I haven't tested it yet),

I am not sure about endianness, and how it will work

pub fn from_bit_vec(ctx: &'ctx Context, bit_vec: Vec<bool>) -> Option<BV<'ctx>> {
    let ast = unsafe {
        let size = bit_vec.len() as u32;
        let bits = bit_vec.as_ptr();

        let numeral_ptr = Z3_mk_bv_numeral(ctx.z3_ctx, size, bits);
        if numeral_ptr.is_null() {
            return None;
        }

        numeral_ptr
    };
    Some(unsafe { Self::wrap(ctx, ast) })
}

pub fn from_byte_vec(ctx: &'ctx Context, byte_vec: Vec<u8>) -> Option<BV<'ctx>> {
    let mut bit_vec = Vec::with_capacity(byte_vec.len() * 8);
    for item in byte_vec {
        for offset in 0..8 {
            let mask = 1 << offset;
            let bit = item & mask != 0;
            bit_vec.push(bit);
        }
    }

    Self::from_bit_vec(ctx, bit_vec)
}

I will make a PR when I test it.

@the-ssd the-ssd linked a pull request Jan 5, 2025 that will close this issue
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant