Trait BV

Source

pub trait BVwhere
    Self: Debug + LowerHex + UpperHex + Display + Copy + Clone + PartialEq + Eq + Hash + Send + Sync + Serialize + DeserializeOwned + Add<Output = Self> + Sub<Output = Self> + BitAnd<Output = Self> + BitOr<Output = Self> + BitXor<Output = Self> + Not<Output = Self> + Neg<Output = Self> + Shl<Output = Self> + Shr<Output = Self> + TryInto<u64, Error = ExecError>,{
    const BIT_ONE: Self;
    const BIT_ZERO: Self;
    const MAX_WIDTH: u32;
Show 35 methods
    // Required methods
    fn new(value: u64, len: u32) -> Self;
    fn len(self) -> u32;
    fn lower_u64(self) -> u64;
    fn lower_u8(self) -> u8;
    fn is_zero(self) -> bool;
    fn zeros(len: u32) -> Self;
    fn ones(len: u32) -> Self;
    fn leading_zeros(self) -> u32;
    fn from_u8(value: u8) -> Self;
    fn from_u16(value: u16) -> Self;
    fn from_u32(value: u32) -> Self;
    fn from_u64(value: u64) -> Self;
    fn from_bytes(bytes: &[u8]) -> Self;
    fn to_le_bytes(self) -> Vec<u8> ⓘ;
    fn to_be_bytes(self) -> Vec<u8> ⓘ;
    fn from_str(bv: &str) -> Option<Self>;
    fn add_i128(self, op: i128) -> Self;
    fn zero_extend(self, new_len: u32) -> Self;
    fn sign_extend(self, new_len: u32) -> Self;
    fn unsigned(self) -> i128;
    fn signed(self) -> i128;
    fn slice(self, from: u32, len: u32) -> Option<Self>;
    fn set_slice(self, n: u32, update: Self) -> Self;
    fn set_slice_int(int: i128, n: u32, update: Self) -> i128;
    fn get_slice_int(len: u32, int: i128, n: u32) -> Self;

    // Provided methods
    fn len_i128(self) -> i128 { ... }
    fn is_empty(self) -> bool { ... }
    fn sub_i128(self, op: i128) -> Self { ... }
    fn append(self, suffix: Self) -> Option<Self> { ... }
    fn extract(self, high: u32, low: u32) -> Option<Self> { ... }
    fn shiftr(self, shift: i128) -> Self { ... }
    fn arith_shiftr(self, shift: i128) -> Self { ... }
    fn shiftl(self, shift: i128) -> Self { ... }
    fn truncate_lsb(self, len: i128) -> Option<Self> { ... }
    fn replicate(self, times: i128) -> Option<Self> { ... }
}

Expand description

This trait allows us to be generic over the representation of concrete bitvectors. Specific users of isla-lib may then choose different representations depending on use case - B64 will likely be the most efficient for ordinary use, but B129 can represent CHERI compressed capabilities concretely.

Required Associated Constants§

Source

const BIT_ONE: Self

Source

const BIT_ZERO: Self

Source

const MAX_WIDTH: u32

In Isla concrete bitvectors are only represented up to a specific maximum width/length. Beyond this they will be promoted to symbolic variables which are equal to a concrete value represented in the SMT solver. This makes computation over concrete bitvectors below this max width very efficient, as they can be represented as simple Copy types like u64.

Required Methods§

Source

fn zeros(len: u32) -> Self

Make a small bitvector of all zeros.

§Panics

len must be less than or equal to MAX_WIDTH

Source

fn ones(len: u32) -> Self

Make a small bitvector of all ones.

§Panics

len must be less than or equal to MAX_WIDTH

Source

fn leading_zeros(self) -> u32

Source

fn from_u8(value: u8) -> Self

Source

fn from_u16(value: u16) -> Self

Source

fn from_u32(value: u32) -> Self

Source

fn from_u64(value: u64) -> Self

Source

fn from_bytes(bytes: &[u8]) -> Self

Byte order is: from_bytes(&[0xAB, 0xCD, 0xEF] == 0xABCDEF

§Panics

bytes.len() * 8 must be less than or equal to MAX_WIDTH

Source

fn to_le_bytes(self) -> Vec<u8> ⓘ

Source

fn to_be_bytes(self) -> Vec<u8> ⓘ

Source

fn from_str(bv: &str) -> Option<Self>

Parses a bitvector from a string slice. String must be prefixed by either #x/0x, or #b/0b (allowing both SMT style and Sail/C style prefixes) for hexadecimal or binary. Returns None if the string is not parseable for any reason

Source