claripy.vsa.strided_interval.StridedInterval

class documentation

class StridedInterval(BackendObject): (source)

Known subclasses: claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

View In Hierarchy

A Strided Interval is represented in the following form:: <bits> stride[lower_bound, upper_bound] For more details, please refer to relevant papers like TIE and WYSINWYE. This implementation is signedness-agostic, please refer to [1] *Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code* by Jorge A. Navas, etc. for more details. Note that this implementation only takes hint from [1]. Such a work has been improved to be more precise (and still sound) when dealing with strided intervals. DO NOT expect to see a 1-to-1 reproduction of [1]. Thanks all corresponding authors for their outstanding works.

Static Method diop_natural_solution_linear It finds the fist natural solution of the diophantine equation a*x + b*y = c. Some lines of this code are taken from the project sympy.
Static Method empty Undocumented
Static Method extended_euclid It calculates the GCD of a and b, and two values x and y such that: a*x + b*y = GCD(a,b). This code has been taken from the project sympy.
Static Method gcd Get the greatest common divisor.
Static Method highbit Undocumented
Static Method igcd :param a: First integer :param b: Second integer :return: the integer GCD between a and b
Static Method lcm Get the least common multiple.
Static Method least_upper_bound Pseudo least upper bound. Join the given set of intervals into a big interval. The resulting strided interval is the one which in all the possible joins of the presented SI, presented the least number of values.
Static Method lower :return:
Static Method max_int Undocumented
Static Method min_bits Undocumented
Static Method min_int Undocumented
Static Method pseudo_join It two intervals in a way that the resulting SI is the one that has the least SI cardinality (i.e., which represents the least number of elements) possible if the smart_join flag is enabled, otherwise it just joins the SI according the order they are passed to the function.
Static Method sign Undocumented
Static Method signed_max_int Undocumented
Static Method signed_min_int Undocumented
Static Method top Get a TOP StridedInterval.
Static Method upper :return:
Method __add__ Undocumented
Method __and__ Undocumented
Method __eq__ Undocumented
Method __floordiv__ Unsigned division
Method __ge__ Unsigned greater than or equal to
Method __gt__ Unsigned greater than
Method __hash__ Undocumented
Method __init__ Undocumented
Method __invert__ Undocumented
Method __le__ Unsigned less than or equal to
Method __len__ Get the length in bits of this variable. :return:
Method __lshift__ Undocumented
Method __lt__ Unsigned less than
Method __mod__ Undocumented
Method __mul__ Undocumented
Method __ne__ Undocumented
Method __neg__ Undocumented
Method __or__ Undocumented
Method __radd__ Undocumented
Method __rand__ Undocumented
Method __repr__ Undocumented
Method __rshift__ Arithmetic shift right.
Method __rsub__ Undocumented
Method __rxor__ Undocumented
Method __sub__ Undocumented
Method __truediv__ Undocumented
Method __xor__ Undocumented
Method add Binary operation: add
Method agnostic_extend Unary operation: SignExtend
Method bitwise_and Binary operation: logical and
Method bitwise_not Unary operation: bitwise not
Method bitwise_or Binary operation: logical or
Method bitwise_xor Operation xor
Method cast_low Undocumented
Method concat Undocumented
Method copy Undocumented
Method eq Equal
Method eval Evaluate this StridedInterval to obtain a list of concrete integers.
Method extract Undocumented
Method identical Used to make exact comparisons between two StridedIntervals. Usually it is only used in test cases.
Method intersection Undocumented
Method lower_bound.setter Undocumented
Method lshift Undocumented
Method LShR Logical shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval object :rtype: StridedInterval
Method mul Binary operation: multiplication
Method nameless_copy Undocumented
Method neg Unary operation: neg
Method normalize Undocumented
Method reverse This is a delayed reversing function. All it really does is to invert the _reversed property of this StridedInterval object.
Method rshift_arithmetic Arithmetic shift right.
Method rshift_logical Logical shift right.
Method sdiv Binary operation: signed division
Method SGE Signed greater than or equal to.
Method SGT Signed greater than.
Method sign_extend Unary operation: SignExtend
Method SLE Signed less than or equal to.
Method SLT Signed less than
Method solution Checks whether an integer is solution of the current strided Interval :param b: integer to check :return: True if b belongs to the current Strided Interval, False otherwhise
Method stride.setter Undocumented
Method sub Binary operation: sub
Method udiv Binary operation: unsigned division
Method UGE Unsigned greater than or equal to.
Method UGT Signed greater than.
Method ULE Unsigned less than or equal to.
Method ULT Unsigned less than.
Method union The union operation. It might return a DiscreteStridedIntervalSet to allow for better precision in analysis.
Method upper_bound.setter Undocumented
Method widen Undocumented
Method zero_extend Unary operation: ZeroExtend
Instance Variable uninitialized Undocumented
Property bits Undocumented
Property cardinality Undocumented
Property complement Return the complement of the interval Refer section 3.1 augmented for managing strides
Property is_bottom Whether this StridedInterval is a BOTTOM, in other words, describes an empty set of integers.
Property is_empty The same as is_bottom :return: True/False
Property is_integer If this is an integer, i.e. self.lower_bound == self.upper_bound.
Property is_interval Undocumented
Property is_top If this is a TOP value.
Property lower_bound Undocumented
Property max Treat this StridedInterval as a set of unsigned numbers, and return the greatest one
Property min Treat this StridedInterval as a set of unsigned numbers, and return the smallest one
Property n_values Undocumented
Property name Undocumented
Property reversed Undocumented
Property size Undocumented
Property stride Undocumented
Property unique Undocumented
Property upper_bound Undocumented
Static Method _bigger Return interval with bigger cardinality Refer Section 3.1
Static Method _gap Refer section 3.1; gap function.
Static Method _get_msb Get the MSB (most significant bit).
Static Method _is_msb_one Checks if the most significant bit is one (i.e. is the integer negative under signed arithmetic).
Static Method _is_msb_zero Checks if the most significant bit is zero (i.e. is the integer positive under signed arithmetic).
Static Method _lex_lt Lexicographical LT comparison
Static Method _lex_lte Lexicographical LTE comparison
Static Method _minimal_common_integer Calculates the minimal integer that appears in both StridedIntervals. As a wrapper method of _minimal_common_integer_splitted(), this method takes arbitrary StridedIntervals. For more information, please refer to the comment of _minimal_common_integer_splitted().
Static Method _minimal_common_integer_splitted Calculates the minimal integer that appears in both StridedIntervals. It's equivalent to finding an integral solution for equation `ax + b = cy + d` that makes `ax + b` minimal si_0.stride, si_1.stride being a and c, and si_0...
Static Method _modular_add Undocumented
Static Method _modular_mul Undocumented
Static Method _modular_sub Undocumented
Static Method _ntz Get the number of consecutive zeros :param x: :return:
Static Method _to_negative Undocumented
Static Method _unsigned_to_signed Convert an unsigned integer to a signed integer.
Static Method _wrapped_cardinality Return the cardinality for a set of number (| x, y |) on the wrapped-interval domain.
Static Method _wrapped_overflow_add Determines if an overflow happens during the addition of `a` and `b`.
Static Method _wrapped_overflow_sub Determines if an overflow happens during the subtraction of `a` and `b`.
Static Method _wrapped_signed_div Perform wrapped unsigned division on two StridedIntervals.
Static Method _wrapped_signed_mul Perform wrapped signed multiplication on two StridedIntervals.
Static Method _wrapped_unsigned_div Perform wrapped unsigned division on two StridedIntervals.
Static Method _wrapped_unsigned_mul Perform wrapped unsigned multiplication on two StridedIntervals.
Method _involuted_reverse This method reverses the StridedInterval object for real. Do expect loss of precision for most cases!
Method _is_surrounded Perform a wrapped LTE comparison only considering the SI bounds
Method _min_bits Undocumented
Method _multi_valued_intersection Undocumented
Method _normalize_top Undocumented
Method _nsplit Split `self` at the north pole, which is the same as in signed arithmetic.
Method _pre_shift Undocumented
Method _psplit Split `self` at both north and south poles.
Method _reverse This method reverses the StridedInterval object for real. Do expect loss of precision for most cases!
Method _rshift_arithmetic Arithmetic shift right with a concrete shift amount
Method _rshift_logical Logical shift right with a concrete shift amount
Method _signed_bounds Get lower bound and upper bound for `self` in signed arithmetic.
Method _ssplit Split `self` at the south pole, which is the same as in unsigned arithmetic. When returning two StridedIntervals (which means a splitting occurred), it is guaranteed that the first StridedInterval is on the right side of the south pole.
Method _surrounds_member Undocumented
Method _union Undocumented
Method _unrev_cast_low Undocumented
Method _unrev_extract Undocumented
Method _unrev_rshift_logical Logical shift right.
Method _unsigned_bounds Get lower bound and upper bound for `self` in unsigned arithmetic.
Instance Variable _bits Undocumented
Instance Variable _is_bottom Undocumented
Instance Variable _lower_bound Undocumented
Instance Variable _name Undocumented
Instance Variable _reversed Undocumented
Instance Variable _stride Undocumented
Instance Variable _upper_bound Undocumented

Inherited from BackendObject:

Method to_claripy Claripy calls this to retrieve something that it can directly reason about.
Class Variable __slots__ Undocumented
@staticmethod
def diop_natural_solution_linear(c, a, b): (source)

It finds the fist natural solution of the diophantine equation a*x + b*y = c. Some lines of this code are taken from the project sympy. :param c: constant :param a: quotient of x :param b: quotient of y :return: the first natural solution of the diophatine equation

@staticmethod
def empty(bits): (source)

Undocumented

@staticmethod
def extended_euclid(a, b): (source)

It calculates the GCD of a and b, and two values x and y such that: a*x + b*y = GCD(a,b). This code has been taken from the project sympy. :param a: first integer :param b: second integer :return: x,y and the GCD of a and b

@staticmethod
def gcd(a, b): (source)

Get the greatest common divisor. :param a: The first operand (integer) :param b: The second operand (integer) :return: Their GCD

@staticmethod
def highbit(k): (source)

Undocumented

@staticmethod
def igcd(a, b): (source)

:param a: First integer :param b: Second integer :return: the integer GCD between a and b

@staticmethod
def lcm(a, b): (source)

Get the least common multiple. :param a: The first operand (integer) :param b: The second operand (integer) :return: Their LCM

@staticmethod
def least_upper_bound(*intervals_to_join): (source)

Pseudo least upper bound. Join the given set of intervals into a big interval. The resulting strided interval is the one which in all the possible joins of the presented SI, presented the least number of values. The number of joins to compute is linear with the number of intervals to join. Draft of proof: Considering three generic SI (a,b, and c) ordered from their lower bounds, such that a.lower_bund <= b.lower_bound <= c.lower_bound, where <= is the lexicographic less or equal. The only joins which have sense to compute are: * a U b U c * b U c U a * c U a U b All the other combinations fall in either one of these cases. For example: b U a U c does not make make sense to be calculated. In fact, if one draws this union, the result is exactly either (b U c U a) or (a U b U c) or (c U a U b). :param intervals_to_join: Intervals to join :return: Interval that contains all intervals

@staticmethod
def lower(bits, i, stride): (source)

:return:

@staticmethod
def max_int(k): (source)

Undocumented

@staticmethod
def min_bits(val, max_bits=None): (source)

Undocumented

@staticmethod
def min_int(k): (source)

Undocumented

@staticmethod
def pseudo_join(s, b, smart_join=True): (source)

It two intervals in a way that the resulting SI is the one that has the least SI cardinality (i.e., which represents the least number of elements) possible if the smart_join flag is enabled, otherwise it just joins the SI according the order they are passed to the function. The pseudo-join operation is not associative in wrapping intervals (please refer to section 3.1 paper 'Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code'), Therefore the join of three WI may give us different results according on the order we join them. All of the results will be sound, though. Please use the function least_upper_bound as a stub. :param s: The first SI :param b: The other SI. :param smart_join: Enable the smart join behavior. If this flag is set, this function joins the two SI in a way that the resulting Si has least number of elements (more precise). If it is unset, this function will join the two SI according on the order they are passed to the function. :return: A new StridedInterval

@staticmethod
def sign(a): (source)

Undocumented

@staticmethod
def signed_max_int(k): (source)

Undocumented

@staticmethod
def signed_min_int(k): (source)

Undocumented

@staticmethod
def top(bits, name=None, uninitialized=False): (source)

Get a TOP StridedInterval. :return:

@staticmethod
def upper(bits, i, stride): (source)

:return:

def __add__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def __and__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __eq__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def __floordiv__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unsigned division :param o: The divisor :return: The quotient (self / o)

def __ge__(self, other): (source)

Unsigned greater than or equal to :param other: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

def __gt__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unsigned greater than :param other: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

def __hash__(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __init__(self, name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, bottom=False): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __invert__(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __le__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unsigned less than or equal to :param other: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

def __len__(self): (source)

Get the length in bits of this variable. :return:

def __lshift__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __lt__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unsigned less than :param other: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def __mod__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def __mul__(self, o): (source)

Undocumented

def __ne__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __neg__(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def __or__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __radd__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __rand__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __repr__(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __rshift__(self, shift_amount): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Arithmetic shift right. :param StridedInterval shift_amount: Number of bits to shift right. :return: The shifted StridedInterval object :rtype: StridedInterval

def __rsub__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __rxor__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __sub__(self, o): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def __truediv__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def __xor__(self, other): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def add(self, b): (source)

Binary operation: add :param b: The other operand :return: self + b

@reversed_processor
def agnostic_extend(self, new_length): (source)

Unary operation: SignExtend :param new_length: New length after sign-extension :return: A new StridedInterval

@normalize_types
def bitwise_and(self, t): (source)

Binary operation: logical and :param b: The other operand :return:

@reversed_processor
def bitwise_not(self): (source)

Unary operation: bitwise not :return: ~self

@normalize_types
def bitwise_or(self, t): (source)

Binary operation: logical or :param b: The other operand :return: self | b

@normalize_types
def bitwise_xor(self, t): (source)

Operation xor :param t: The other operand.

@reversed_processor
def cast_low(self, tok): (source)

Undocumented

@normalize_types
def concat(self, b): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def copy(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@normalize_types
def eq(self, o): (source)

Equal :param o: The ohter operand :return: TrueResult(), FalseResult(), or MaybeResult()

def eval(self, n, signed=False): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Evaluate this StridedInterval to obtain a list of concrete integers. :param n: Upper bound for the number of concrete integers :param signed: Treat this StridedInterval as signed or unsigned :return: A list of at most `n` concrete integers

@reversed_processor
def extract(self, high_bit, low_bit): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def identical(self, o): (source)

Used to make exact comparisons between two StridedIntervals. Usually it is only used in test cases. :param o: The other StridedInterval to compare with. :return: True if they are exactly same, False otherwise.

@normalize_types
def intersection(self, b): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@lower_bound.setter
def lower_bound(self, value): (source)

Undocumented

@reversed_processor
def lshift(self, shift_amount): (source)

Undocumented

def LShR(self, shift_amount): (source)

Logical shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval object :rtype: StridedInterval

@normalize_types
def mul(self, o): (source)

Binary operation: multiplication :param o: The other operand :return: self * o

def nameless_copy(self): (source)

Undocumented

@reversed_processor
def neg(self): (source)

Unary operation: neg :return: 0 - self

def normalize(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

def reverse(self): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

This is a delayed reversing function. All it really does is to invert the _reversed property of this StridedInterval object. :return: None

@reversed_processor
def rshift_arithmetic(self, shift_amount): (source)

Arithmetic shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval :rtype: StridedInterval

@reversed_processor
def rshift_logical(self, shift_amount): (source)

Logical shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval :rtype: StridedInterval

@normalize_types
def sdiv(self, o): (source)

Binary operation: signed division :param o: The divisor :return: (self / o) in signed arithmetic

@normalize_types
def SGE(self, o): (source)

Signed greater than or equal to. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def SGT(self, o): (source)

Signed greater than. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@reversed_processor
def sign_extend(self, new_length): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unary operation: SignExtend :param new_length: New length after sign-extension :return: A new StridedInterval

@normalize_types
def SLE(self, o): (source)

Signed less than or equal to. :param o: The other operand. :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def SLT(self, o): (source)

Signed less than :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

def solution(self, b): (source)

Checks whether an integer is solution of the current strided Interval :param b: integer to check :return: True if b belongs to the current Strided Interval, False otherwhise

@stride.setter
def stride(self, value): (source)

Undocumented

@normalize_types
def sub(self, b): (source)

Binary operation: sub :param b: The other operand :return: self - b

@normalize_types
def udiv(self, o): (source)

Binary operation: unsigned division :param o: The divisor :return: (self / o) in unsigned arithmetic

@normalize_types
def UGE(self, o): (source)

Unsigned greater than or equal to. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def UGT(self, o): (source)

Signed greater than. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def ULE(self, o): (source)

Unsigned less than or equal to. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def ULT(self, o): (source)

Unsigned less than. :param o: The other operand :return: TrueResult(), FalseResult(), or MaybeResult()

@normalize_types
def union(self, b): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

The union operation. It might return a DiscreteStridedIntervalSet to allow for better precision in analysis. :param b: Operand :return: A new DiscreteStridedIntervalSet, or a new StridedInterval.

@upper_bound.setter
def upper_bound(self, value): (source)

Undocumented

@normalize_types
def widen(self, b): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@reversed_processor
def zero_extend(self, new_length): (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Unary operation: ZeroExtend :param new_length: New length after zero-extension :return: A new StridedInterval

uninitialized = (source)

Undocumented

@property
bits = (source)

Undocumented

@property
cardinality = (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@property
complement = (source)

Return the complement of the interval Refer section 3.1 augmented for managing strides :return:

@property
is_bottom = (source)

Whether this StridedInterval is a BOTTOM, in other words, describes an empty set of integers. :return: True/False

@property
is_empty = (source)

The same as is_bottom :return: True/False

@property
is_integer = (source)

If this is an integer, i.e. self.lower_bound == self.upper_bound. :return: True if this is an integer, False otherwise

@property
is_interval = (source)

Undocumented

@property
is_top = (source)

If this is a TOP value. :return: True if this is a TOP

@property
lower_bound = (source)

Undocumented

@property
@reversed_processor
max = (source)

Treat this StridedInterval as a set of unsigned numbers, and return the greatest one :return: the greatest number in this StridedInterval when evaluated as unsigned, or None if empty

@property
@reversed_processor
min = (source)

Treat this StridedInterval as a set of unsigned numbers, and return the smallest one :return: the smallest number in this StridedInterval when evaluated as unsigned, or None if empty

@property
n_values = (source)

Undocumented

@property
name = (source)

Undocumented

@property
reversed = (source)

Undocumented

@property
size = (source)

Undocumented

@property
stride = (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

@property
unique = (source)

Undocumented

@property
upper_bound = (source)

Undocumented

@staticmethod
def _bigger(interval1, interval2): (source)

Return interval with bigger cardinality Refer Section 3.1 :param interval1: first interval :param interval2: second interval :return: Interval or interval2 whichever has greater cardinality

@staticmethod
def _gap(src_interval, tar_interval): (source)

Refer section 3.1; gap function. :param src_interval: first argument or interval 1 :param tar_interval: second argument or interval 2 :return: Interval representing gap between two intervals

@staticmethod
def _get_msb(v, bits): (source)

Get the MSB (most significant bit). :param v: The integer :param bits: Bits of the integer :return: the MSB

@staticmethod
def _is_msb_one(v, bits): (source)

Checks if the most significant bit is one (i.e. is the integer negative under signed arithmetic). :param v: The integer to check with :param bits: Bits of the integer :return: True or False

@staticmethod
def _is_msb_zero(v, bits): (source)

Checks if the most significant bit is zero (i.e. is the integer positive under signed arithmetic). :param v: The integer to check with :param bits: Bits of the integer :return: True or False

@staticmethod
def _lex_lt(x, y, bits): (source)

Lexicographical LT comparison :param x: The first operand (integer) :param y: The second operand (integer) :param bits: bit-width of the operands :return: True or False

@staticmethod
def _lex_lte(x, y, bits): (source)

Lexicographical LTE comparison :param x: The first operand (integer) :param y: The second operand (integer) :param bits: bit-width of the operands :return: True or False

@staticmethod
def _minimal_common_integer(si_0, si_1): (source)

Calculates the minimal integer that appears in both StridedIntervals. As a wrapper method of _minimal_common_integer_splitted(), this method takes arbitrary StridedIntervals. For more information, please refer to the comment of _minimal_common_integer_splitted(). :param si_0: the first StridedInterval :type si_0: StridedInterval :param si_1: the second StridedInterval :type si_1: StridedInterval :return: the minimal common integer, or None if there is no common integer

@staticmethod
def _minimal_common_integer_splitted(si_0, si_1): (source)

Calculates the minimal integer that appears in both StridedIntervals. It's equivalent to finding an integral solution for equation `ax + b = cy + d` that makes `ax + b` minimal si_0.stride, si_1.stride being a and c, and si_0.lower_bound, si_1.lower_bound being b and d, respectively. Upper bounds are used to check whether the minimal common integer exceeds the bound or not. None is returned if no minimal common integers can be found within the range. Some assumptions: # - None of the StridedIntervals straddles the south pole. Consequently, we have x <= max_int(si.bits) and y <= # max_int(si.bits) # - a, b, c, d are all positive integers # - x >= 0, y >= 0 :param StridedInterval si_0: the first StridedInterval :param StridedInterval si_1: the second StrideInterval :return: the minimal common integer, or None if there is no common integer

@staticmethod
def _modular_add(a, b, bits): (source)

Undocumented

@staticmethod
def _modular_mul(a, b, bits): (source)

Undocumented

@staticmethod
def _modular_sub(a, b, bits): (source)

Undocumented

@staticmethod
def _ntz(x): (source)

Get the number of consecutive zeros :param x: :return:

@staticmethod
def _to_negative(a, bits): (source)

Undocumented

@staticmethod
def _unsigned_to_signed(v, bits): (source)

Convert an unsigned integer to a signed integer. :param v: The unsigned integer :param bits: How many bits this integer should be :return: The converted signed integer

@staticmethod
def _wrapped_cardinality(x, y, bits): (source)

Return the cardinality for a set of number (| x, y |) on the wrapped-interval domain. :param x: The first operand (an integer) :param y: The second operand (an integer) :return: The cardinality

@staticmethod
def _wrapped_overflow_add(a, b): (source)

Determines if an overflow happens during the addition of `a` and `b`. :param a: The first operand (StridedInterval) :param b: The other operand (StridedInterval) :return: True if overflows, False otherwise

@staticmethod
def _wrapped_overflow_sub(a, b): (source)

Determines if an overflow happens during the subtraction of `a` and `b`. :param a: The first operand (StridedInterval) :param b: The other operand (StridedInterval) :return: True if overflows, False otherwise

@staticmethod
def _wrapped_signed_div(a, b): (source)

Perform wrapped unsigned division on two StridedIntervals. :param a: The dividend (StridedInterval) :param b: The divisor (StridedInterval) :return: The quotient

@staticmethod
def _wrapped_signed_mul(a, b): (source)

Perform wrapped signed multiplication on two StridedIntervals. :param a: The first operand (StridedInterval) :param b: The second operand (StridedInterval) :return: The product

@staticmethod
def _wrapped_unsigned_div(a, b): (source)

Perform wrapped unsigned division on two StridedIntervals. :param a: The dividend (StridedInterval) :param b: The divisor (StridedInterval) :return: The quotient

@staticmethod
def _wrapped_unsigned_mul(a, b): (source)

Perform wrapped unsigned multiplication on two StridedIntervals. :param a: The first operand (StridedInterval) :param b: The second operand (StridedInterval) :return: The multiplication result

def _involuted_reverse(self): (source)

This method reverses the StridedInterval object for real. Do expect loss of precision for most cases! :return: A new reversed StridedInterval instance

def _is_surrounded(self, b): (source)

Perform a wrapped LTE comparison only considering the SI bounds :param a: The first operand :param b: The second operand :return: True if a <= b, False otherwise

def _min_bits(self): (source)

Undocumented

@normalize_types
def _multi_valued_intersection(self, b): (source)

Undocumented

def _normalize_top(self): (source)

Undocumented

def _nsplit(self): (source)

Split `self` at the north pole, which is the same as in signed arithmetic. :return: A list of split StridedIntervals

def _pre_shift(self, shift_amount): (source)

Undocumented

def _psplit(self): (source)

Split `self` at both north and south poles. :return: A list of split StridedIntervals

def _reverse(self): (source)

This method reverses the StridedInterval object for real. Do expect loss of precision for most cases! :return: A new reversed StridedInterval instance

def _rshift_arithmetic(self, shift_amount): (source)

Arithmetic shift right with a concrete shift amount :param int shift_amount: Number of bits to shift right. :return: The new StridedInterval after right shifting :rtype: StridedInterval

def _rshift_logical(self, shift_amount): (source)

Logical shift right with a concrete shift amount :param int shift_amount: Number of bits to shift right. :return: The new StridedInterval after right shifting :rtype: StridedInterval

def _signed_bounds(self): (source)

Get lower bound and upper bound for `self` in signed arithmetic. :return: a list of (lower_bound, upper_bound) tuples

def _ssplit(self): (source)

Split `self` at the south pole, which is the same as in unsigned arithmetic. When returning two StridedIntervals (which means a splitting occurred), it is guaranteed that the first StridedInterval is on the right side of the south pole. :return: a list of split StridedIntervals, that contains either one or two StridedIntervals

def _surrounds_member(self, v): (source)

Undocumented

@normalize_types
def _union(self, b): (source)

Undocumented

def _unrev_cast_low(self, tok): (source)

Undocumented

def _unrev_extract(self, high_bit, low_bit): (source)

Undocumented

def _unrev_rshift_logical(self, shift_amount): (source)

Logical shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval :rtype: StridedInterval

def _unsigned_bounds(self): (source)

Get lower bound and upper bound for `self` in unsigned arithmetic. :return: a list of (lower_bound, upper_bound) tuples.

_bits = (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

_is_bottom = (source)

Undocumented

_lower_bound = (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented

_name = (source)

Undocumented

_reversed: bool = (source)

Undocumented

_stride = (source)

Undocumented

_upper_bound = (source)
overridden in claripy.vsa.discrete_strided_interval_set.DiscreteStridedIntervalSet

Undocumented