liblisa::smt

Trait SmtBV

pub trait SmtBV<'a, S: SmtSolver<'a, BV = Self>>:
    Clone
    + Debug
    + Display
    + Add<Output = Self>
    + Sub<Output = Self>
    + Mul<Output = Self>
    + BitOr<Output = Self>
    + BitAnd<Output = Self>
    + BitXor<Output = Self>
    + Not<Output = Self>
    + Sized {
Show 28 methods // Required methods fn is_identical(&self, other: &Self) -> bool; fn concat(self, other: Self) -> Self; fn extract(self, hi: u32, lo: u32) -> Self; fn zero_ext(self, num: u32) -> Self; fn sign_ext(self, num: u32) -> Self; fn bvshl(self, count: Self) -> Self; fn bvlshr(self, count: Self) -> Self; fn bvashr(self, count: Self) -> Self; fn bvurem(self, n: Self) -> Self; fn bvsrem(self, n: Self) -> Self; fn bvudiv(self, n: Self) -> Self; fn bvsdiv(self, n: Self) -> Self; fn bvrotl(self, count: Self) -> Self; fn bvrotr(self, count: Self) -> Self; fn bvslt(self, other: Self) -> S::Bool; fn bvsge(self, other: Self) -> S::Bool; fn bvsgt(self, other: Self) -> S::Bool; fn bvugt(self, other: Self) -> S::Bool; fn bvult(self, other: Self) -> S::Bool; fn bvule(self, other: Self) -> S::Bool; fn bvuge(self, other: Self) -> S::Bool; fn _eq(self, other: Self) -> S::Bool; fn simplify(self) -> Self; fn get_size(&self) -> u32; fn as_u64(&self) -> Option<u64>; // Provided methods fn into_dynamic(self) -> Dynamic<'a, S> { ... } fn swap_bytes(self, num_bytes: usize) -> Self { ... } fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self { ... }
}
Expand description

BitVector expressions in the SMT solver.

Most operation names correspond directly to the SMT functions and are not documented here.

Required Methods§

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn concat(self, other: Self) -> Self

fn extract(self, hi: u32, lo: u32) -> Self

fn zero_ext(self, num: u32) -> Self

fn sign_ext(self, num: u32) -> Self

fn bvshl(self, count: Self) -> Self

fn bvlshr(self, count: Self) -> Self

fn bvashr(self, count: Self) -> Self

fn bvurem(self, n: Self) -> Self

fn bvsrem(self, n: Self) -> Self

fn bvudiv(self, n: Self) -> Self

fn bvsdiv(self, n: Self) -> Self

fn bvrotl(self, count: Self) -> Self

fn bvrotr(self, count: Self) -> Self

fn bvslt(self, other: Self) -> S::Bool

fn bvsge(self, other: Self) -> S::Bool

fn bvsgt(self, other: Self) -> S::Bool

fn bvugt(self, other: Self) -> S::Bool

fn bvult(self, other: Self) -> S::Bool

fn bvule(self, other: Self) -> S::Bool

fn bvuge(self, other: Self) -> S::Bool

fn _eq(self, other: Self) -> S::Bool

Returns an SMT expression that performs an equality comparison between the two bitvectors.

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn get_size(&self) -> u32

Returns the size of the bitvector.

fn as_u64(&self) -> Option<u64>

Converts the bitvector to an u64, if possible.

Provided Methods§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bitvector into a Dynamic expression.

fn swap_bytes(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector.

fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector, and zero-extends to an 128-bit bitvector.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§

§

impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx>

§

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBV<'ctx, CachedSolver<'ctx, S, C>> for CacheBV<'ctx, S>