Enum haybale_pitchfork::secret::BV

pub enum BV {
    Public(BV<Rc<Btor>>),
    Secret {
        btor: BtorRef,
        width: u32,
        symbol: Option<String>,
    },
    PartiallySecret {
        secret_mask: Vec<bool>,
        data: BV<Rc<Btor>>,
        symbol: Option<String>,
    },
}

A wrapper around boolector::BV which can represent either public or secret data.

Variants

Public(BV<Rc<Btor>>)

Secret

Secret values are opaque because we don't care about their actual value, only how they are used.

Fields of Secret

btor: BtorRefwidth: u32symbol: Option<String>

PartiallySecret

PartiallySecret values have some secret and some not-secret bits. Currently we make just a best-effort attempt to handle these; for now, some functions may just fall back on treating the entire value as Secret.

Fields of PartiallySecret

secret_mask: Vec<bool>

A vector the length of the PartiallySecret value's bitwidth, where each true indicates that the corresponding position in the PartiallySecret is secret, and likewise false indicates public. secret_mask[0] corresponds to the bit at position 0, which is the rightmost (least-significant) bit.

data: BV<Rc<Btor>>

A BV, which must have bitwidth exactly equal to the length of secret_mask. In positions where secret_mask is false, this gives the value of the public bits. In positions where secret_mask is true, the data here is invalid and should not be used for anything.

symbol: Option<String>

Methods

impl BV

pub fn is_secret(&self) -> bool

pub fn as_public(&self) -> &BV<Rc<Btor>>

Gets the value out of a BV::Public, panicking if it is instead a BV::Secret

Trait Implementations

impl BV for BV

type SolverRef = BtorRef

fn new(btor: BtorRef, width: u32, name: Option<&str>) -> Self

fn from_bool(btor: BtorRef, b: bool) -> Self

fn from_i32(btor: BtorRef, i: i32, width: u32) -> Self

fn from_u32(btor: BtorRef, u: u32, width: u32) -> Self

fn from_i64(btor: BtorRef, i: i64, width: u32) -> Self

fn from_u64(btor: BtorRef, u: u64, width: u32) -> Self

fn zero(btor: BtorRef, width: u32) -> Self

fn one(btor: BtorRef, width: u32) -> Self

fn ones(btor: BtorRef, width: u32) -> Self

fn from_binary_str(btor: BtorRef, bits: &str) -> Self

fn from_dec_str(btor: BtorRef, num: &str, width: u32) -> Self

fn from_hex_str(btor: BtorRef, num: &str, width: u32) -> Self

fn as_binary_str(&self) -> Option<String>

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

fn as_bool(&self) -> Option<bool>

fn get_a_solution(&self) -> Result<BVSolution>

fn get_solver(&self) -> Self::SolverRef

fn get_id(&self) -> i32

fn get_width(&self) -> u32

fn get_symbol(&self) -> Option<&str>

fn set_symbol(&mut self, symbol: Option<&str>)

fn is_const(&self) -> bool

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

fn assert(&self) -> Result<()>

fn is_failed_assumption(&self) -> bool

fn _eq(&self, other: &Self) -> Self

fn _ne(&self, other: &Self) -> Self

fn add(&self, other: &Self) -> Self

fn sub(&self, other: &Self) -> Self

fn mul(&self, other: &Self) -> Self

fn udiv(&self, other: &Self) -> Self

fn sdiv(&self, other: &Self) -> Self

fn urem(&self, other: &Self) -> Self

fn srem(&self, other: &Self) -> Self

fn smod(&self, other: &Self) -> Self

fn inc(&self) -> Self

fn dec(&self) -> Self

fn neg(&self) -> Self

fn uaddo(&self, other: &Self) -> Self

fn saddo(&self, other: &Self) -> Self

fn usubo(&self, other: &Self) -> Self

fn ssubo(&self, other: &Self) -> Self

fn umulo(&self, other: &Self) -> Self

fn smulo(&self, other: &Self) -> Self

fn sdivo(&self, other: &Self) -> Self

fn not(&self) -> Self

fn and(&self, other: &Self) -> Self

fn or(&self, other: &Self) -> Self

fn xor(&self, other: &Self) -> Self

fn nand(&self, other: &Self) -> Self

fn nor(&self, other: &Self) -> Self

fn xnor(&self, other: &Self) -> Self

fn sll(&self, other: &Self) -> Self

fn srl(&self, other: &Self) -> Self

fn sra(&self, other: &Self) -> Self

fn rol(&self, other: &Self) -> Self

fn ror(&self, other: &Self) -> Self

fn redand(&self) -> Self

fn redor(&self) -> Self

fn redxor(&self) -> Self

fn ugt(&self, other: &Self) -> Self

fn ugte(&self, other: &Self) -> Self

fn sgt(&self, other: &Self) -> Self

fn sgte(&self, other: &Self) -> Self

fn ult(&self, other: &Self) -> Self

fn ulte(&self, other: &Self) -> Self

fn slt(&self, other: &Self) -> Self

fn slte(&self, other: &Self) -> Self

fn uadds(&self, other: &Self) -> Self

Saturating addition, unsigned. The result will be the same as normal addition, except that if the operation would (unsigned) overflow, the maximum value (for that bitwidth) is returned instead.

fn sadds(&self, other: &Self) -> Self

Saturating addition, signed. The result will be the same as normal addition, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead.

fn usubs(&self, other: &Self) -> Self

Saturating subtraction, unsigned. The result will be the same as normal subtraction, except that if the operation would overflow (result in a negative number), zero is returned instead.

fn ssubs(&self, other: &Self) -> Self

Saturating subtraction, signed. The result will be the same as normal subtraction, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead.

fn zext(&self, i: u32) -> Self

fn sext(&self, i: u32) -> Self

fn slice(&self, high: u32, low: u32) -> Self

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

fn repeat(&self, n: u32) -> Self

fn iff(&self, other: &Self) -> Self

fn implies(&self, other: &Self) -> Self

fn cond_bv(&self, truebv: &Self, falsebv: &Self) -> Self

fn zero_extend_to_bits(&self, bits: u32) -> Self

Zero-extend a BV to the specified number of bits. The input BV can be already the desired size (in which case this function is a no-op) or smaller (in which case this function will extend), but not larger (in which case this function will panic).

fn sign_extend_to_bits(&self, bits: u32) -> Self

Sign-extend a BV to the specified number of bits. The input BV can be already the desired size (in which case this function is a no-op) or smaller (in which case this function will extend), but not larger (in which case this function will panic).

impl Clone for BV

fn clone(&self) -> BV

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BV

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Eq for BV

impl PartialEq<BV> for BV

fn eq(&self, other: &BV) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &BV) -> bool

This method tests for !=.

impl StructuralEq for BV

impl StructuralPartialEq for BV