From a5d2d428233bc0586bc3f011fe41840e8a75ae54 Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Fri, 4 Oct 2024 11:50:14 -0700 Subject: [PATCH] Remove uninitialized member from Base --- claripy/algorithm/simplify.py | 3 - claripy/ast/base.py | 28 ---- claripy/ast/bv.py | 4 +- claripy/ast/strings.py | 5 +- claripy/backends/backend_vsa/backend_vsa.py | 4 +- .../backends/backend_vsa/strided_interval.py | 144 ++++-------------- claripy/operations.py | 4 - tests/test_simplify.py | 2 +- tests/test_strings.py | 2 +- tests/test_vsa.py | 1 - 10 files changed, 34 insertions(+), 163 deletions(-) diff --git a/claripy/algorithm/simplify.py b/claripy/algorithm/simplify.py index 9bbd3940b..8ecbea53e 100644 --- a/claripy/algorithm/simplify.py +++ b/claripy/algorithm/simplify.py @@ -24,9 +24,6 @@ def simplify(expr: T) -> T: log.debug("Unable to simplify expression") return expr - # Copy some parameters (that should really go to the Annotation backend) - simplified._uninitialized = expr.uninitialized - # dealing with annotations if expr.annotations: ast_args = tuple(a for a in expr.args if isinstance(a, Base)) diff --git a/claripy/ast/base.py b/claripy/ast/base.py index 93fa5c5ac..b9e339149 100644 --- a/claripy/ast/base.py +++ b/claripy/ast/base.py @@ -124,9 +124,6 @@ class Base: # Caching _cached_encoded_name: bytes | None - # Extra information - _uninitialized: bool - __slots__ = [ "op", "args", @@ -141,7 +138,6 @@ class Base: "_relocatable_annotations", "_errored", "_cached_encoded_name", - "_uninitialized", "__weakref__", ] @@ -156,7 +152,6 @@ def __new__( # pylint:disable=redefined-builtin symbolic: bool | None = None, variables: frozenset[str] | None = None, errored: set[Backend] | None = None, - uninitialized: bool = False, annotations: tuple[Annotation, ...] = (), skip_child_annotations: bool = False, length: int | None = None, @@ -230,7 +225,6 @@ def __new__( # pylint:disable=redefined-builtin symbolic=symbolic, length=length, errored=errored, - uninitialized=uninitialized, annotations=annotations, encoded_name=encoded_name, depth=depth, @@ -253,7 +247,6 @@ def make_like( annotations: tuple[Annotation, ...] | None = None, variables: frozenset[str] | None = None, symbolic: bool | None = None, - uninitialized: bool = False, skip_child_annotations: bool = False, length: int | None = None, ) -> Self: @@ -266,7 +259,6 @@ def make_like( and annotations and variables is None and symbolic is None - and uninitialized is False and skip_child_annotations and length is not None ): @@ -294,7 +286,6 @@ def make_like( symbolic=self.symbolic, annotations=annotations, length=length, - uninitialized=self._uninitialized, ) result._hash = h @@ -309,8 +300,6 @@ def make_like( annotations = self.annotations if not args or not any(self is arg for arg in args) else () if variables is None and op in all_operations: variables = self.variables - if uninitialized is None: - uninitialized = self._uninitialized if symbolic is None and op in all_operations: symbolic = self.symbolic @@ -319,7 +308,6 @@ def make_like( args if simplified is None else simplified.args, annotations=annotations, variables=variables, - uninitialized=uninitialized, symbolic=symbolic, skip_child_annotations=skip_child_annotations, length=length, @@ -335,7 +323,6 @@ def __a_init__( length: int | None = None, simplified: SimplificationLevel = SimplificationLevel.UNSIMPLIFIED, errored: set[Backend] | None = None, - uninitialized: bool = False, annotations: tuple[Annotation, ...] | None = None, encoded_name: bytes | None = None, depth: int | None = None, @@ -368,8 +355,6 @@ def __a_init__( self._simplified = simplified - self._uninitialized = uninitialized - if len(self.args) == 0: raise ClaripyOperationError("AST with no arguments!") @@ -1061,16 +1046,3 @@ def cardinality(self) -> int: @property def concrete(self) -> bool: return not self.symbolic - - @property - def uninitialized(self) -> bool: - """ - Whether this AST comes from an uninitialized dereference or not. It's only used in under-constrained symbolic - execution mode. - - :returns: True/False/None (unspecified). - """ - - # TODO: It should definitely be moved to the proposed Annotation backend. - - return self._uninitialized diff --git a/claripy/ast/bv.py b/claripy/ast/bv.py index fee0b1cd9..0bb5b647d 100644 --- a/claripy/ast/bv.py +++ b/claripy/ast/bv.py @@ -291,9 +291,9 @@ def SI( ) -def TSI(bits, name=None, uninitialized=False, explicit_name=None): +def TSI(bits, name=None, explicit_name=None): name = "unnamed" if name is None else name - return BVS(name, bits, uninitialized=uninitialized, explicit_name=explicit_name) + return BVS(name, bits, explicit_name=explicit_name) def ESI(bits, **kwargs): diff --git a/claripy/ast/strings.py b/claripy/ast/strings.py index ab81d8cd9..4ab09f41f 100644 --- a/claripy/ast/strings.py +++ b/claripy/ast/strings.py @@ -47,13 +47,11 @@ def indexOf(self, pattern, start_idx): return StrIndexOf(self, pattern, start_idx) -def StringS(name, uninitialized=False, explicit_name=False, **kwargs): +def StringS(name, explicit_name=False, **kwargs): """ Create a new symbolic string (analogous to z3.String()) :param name: The name of the symbolic string (i. e. the name of the variable) - :param uninitialized: Whether this value should be counted as an "uninitialized" value in the course of an - analysis. :param bool explicit_name: If False, an identifier is appended to the name to ensure uniqueness. :returns: The String object representing the symbolic string @@ -63,7 +61,6 @@ def StringS(name, uninitialized=False, explicit_name=False, **kwargs): "StringS", (n,), symbolic=True, - uninitialized=uninitialized, variables=frozenset((n,)), **kwargs, ) diff --git a/claripy/backends/backend_vsa/backend_vsa.py b/claripy/backends/backend_vsa/backend_vsa.py index 35c83ba52..a3f9c8dbf 100644 --- a/claripy/backends/backend_vsa/backend_vsa.py +++ b/claripy/backends/backend_vsa/backend_vsa.py @@ -465,8 +465,8 @@ def widen(self, ast): return ret @staticmethod - def CreateTopStridedInterval(bits, name=None, uninitialized=False): - return StridedInterval.top(bits, name, uninitialized=uninitialized) + def CreateTopStridedInterval(bits, name=None): + return StridedInterval.top(bits, name) def constraint_to_si(self, expr): return Balancer(self, expr).compat_ret diff --git a/claripy/backends/backend_vsa/strided_interval.py b/claripy/backends/backend_vsa/strided_interval.py index 264cae785..4f0338832 100644 --- a/claripy/backends/backend_vsa/strided_interval.py +++ b/claripy/backends/backend_vsa/strided_interval.py @@ -106,7 +106,7 @@ def normalizer(self, o): # Force reverse and bear the loss in precision def _lossless_reverse(a): - return a.uninitialized or a.is_top or a.is_integer + return a.is_top or a.is_integer reverse_back = False @@ -146,11 +146,6 @@ def _lossless_reverse(a): o = o._reverse() ret = f(self, o) - if isinstance(ret, StridedInterval): - if isinstance(self, StridedInterval) and self.uninitialized: - ret.uninitialized = True - if isinstance(o, StridedInterval) and o.uninitialized: - ret.uninitialized = True if reverse_back and isinstance(ret, StridedInterval): ret = ret.reverse() return ret @@ -186,9 +181,7 @@ class StridedInterval(BackendObject): # pylint: disable=too-many-positional-arguments - def __init__( - self, name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, bottom=False - ): + def __init__(self, name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, bottom=False): self._name = name if self._name is None: @@ -209,8 +202,6 @@ def __init__( self._is_bottom = bottom - self.uninitialized = uninitialized - if self._upper_bound is not None and bits == 0: self._bits = self._min_bits() @@ -233,7 +224,6 @@ def copy(self): stride=self.stride, lower_bound=self.lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, bottom=self._is_bottom, ) si._reversed = self._reversed @@ -246,7 +236,6 @@ def nameless_copy(self): stride=self.stride, lower_bound=self.lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, bottom=self._is_bottom, ) si._reversed = self._reversed @@ -327,7 +316,6 @@ def __hash__(self): ( f"{self.bits:x} {self.lower_bound:x} {self.upper_bound:x} {self.stride:x}", self._reversed, - self.uninitialized, ) ) @@ -362,7 +350,6 @@ def _ssplit(self): stride=self.stride, lower_bound=self.lower_bound, upper_bound=a_upper_bound, - uninitialized=self.uninitialized, ) b_lower_bound = self._modular_add(a_upper_bound, self.stride, self.bits) @@ -371,7 +358,6 @@ def _ssplit(self): stride=self.stride, lower_bound=b_lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, ) return [a, b] @@ -408,7 +394,6 @@ def _nsplit(self): stride=self.stride, lower_bound=self.lower_bound, upper_bound=a_upper_bound, - uninitialized=self.uninitialized, ) b_lower_bound = a_upper_bound + self.stride @@ -417,7 +402,6 @@ def _nsplit(self): stride=self.stride, lower_bound=b_lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, ) return [a, b] @@ -523,9 +507,7 @@ def _rshift_logical(self, shift_amount): u = self.upper_bound >> shift_amount stride = max(self.stride >> shift_amount, 1) - return StridedInterval( - bits=self.bits, lower_bound=l, upper_bound=u, stride=stride, uninitialized=self.uninitialized - ) + return StridedInterval(bits=self.bits, lower_bound=l, upper_bound=u, stride=stride) a = ssplit[0]._rshift_logical(shift_amount) b = ssplit[1]._rshift_logical(shift_amount) @@ -563,9 +545,7 @@ def _rshift_arithmetic(self, shift_amount): u = u | mask if l == u: stride = 0 - return StridedInterval( - bits=self.bits, lower_bound=l, upper_bound=u, stride=stride, uninitialized=self.uninitialized - ) + return StridedInterval(bits=self.bits, lower_bound=l, upper_bound=u, stride=stride) a = nsplit[0]._rshift_arithmetic(shift_amount) b = nsplit[1]._rshift_arithmetic(shift_amount) @@ -998,9 +978,6 @@ def __repr__(self): "R" if self._reversed else "", ) - if self.uninitialized: - s += "(uninit)" - return s # @@ -1073,7 +1050,6 @@ def complement(self): upper_bound=x_minus_1, bits=self.bits, stride=new_stride, - uninitialized=self.uninitialized, ) @property @@ -1326,7 +1302,7 @@ def _gap(src_interval, tar_interval): return StridedInterval.empty(w) @staticmethod - def top(bits, name=None, uninitialized=False): + def top(bits, name=None): """ Get a TOP StridedInterval. @@ -1338,7 +1314,6 @@ def top(bits, name=None, uninitialized=False): stride=1, lower_bound=0, upper_bound=StridedInterval.max_int(bits), - uninitialized=uninitialized, ) @staticmethod @@ -1461,7 +1436,6 @@ def _wrapped_unsigned_mul(a, b): bits = max(a.bits, b.bits) lb = a.lower_bound * b.lower_bound ub = a.upper_bound * b.upper_bound - uninit_flag = a.uninitialized | b.uninitialized if (ub - lb) < (2**bits): if b.is_integer: @@ -1476,10 +1450,9 @@ def _wrapped_unsigned_mul(a, b): stride=stride, lower_bound=lb, upper_bound=ub, - uninitialized=uninit_flag, ) # Overflow occurred - return StridedInterval.top(bits, uninitialized=False) + return StridedInterval.top(bits) @staticmethod def _wrapped_signed_mul(a, b): @@ -1504,7 +1477,6 @@ def _wrapped_signed_mul(a, b): a_ub_positive = StridedInterval._is_msb_zero(a.upper_bound, bits) b_lb_positive = StridedInterval._is_msb_zero(b.lower_bound, bits) b_ub_positive = StridedInterval._is_msb_zero(b.upper_bound, bits) - uninit_flag = a.uninitialized | b.uninitialized if b.is_integer: if b_lb_positive: @@ -1527,10 +1499,8 @@ def _wrapped_signed_mul(a, b): ub = a.upper_bound * b.upper_bound if ub - lb < (2**bits): - return StridedInterval( - bits=bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninit_flag - ) - return StridedInterval.top(bits, uninitialized=uninit_flag) + return StridedInterval(bits=bits, stride=stride, lower_bound=lb, upper_bound=ub) + return StridedInterval.top(bits) if not a_lb_positive and not a_ub_positive and not b_lb_positive and not b_ub_positive: # [-5, -2] * [-20, -10] = [20, 100] @@ -1542,10 +1512,8 @@ def _wrapped_signed_mul(a, b): ) if ub - lb < (2**bits): - return StridedInterval( - bits=bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninit_flag - ) - return StridedInterval.top(bits, uninitialized=uninit_flag) + return StridedInterval(bits=bits, stride=stride, lower_bound=lb, upper_bound=ub) + return StridedInterval.top(bits) if not a_lb_positive and not a_ub_positive and b_lb_positive and b_ub_positive: # [-10, -2] * [2, 5] = [-50, -4] @@ -1555,10 +1523,8 @@ def _wrapped_signed_mul(a, b): if ub - lb < (2**bits): lb &= 2**bits - 1 ub &= 2**bits - 1 - return StridedInterval( - bits=bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninit_flag - ) - return StridedInterval.top(bits, uninitialized=uninit_flag) + return StridedInterval(bits=bits, stride=stride, lower_bound=lb, upper_bound=ub) + return StridedInterval.top(bits) if a_lb_positive and a_ub_positive and not b_lb_positive and not b_ub_positive: # [2, 10] * [-5, -2] = [-50, -4] @@ -1568,10 +1534,8 @@ def _wrapped_signed_mul(a, b): if ub - lb < (2**bits): lb &= 2**bits - 1 ub &= 2**bits - 1 - return StridedInterval( - bits=bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninit_flag - ) - return StridedInterval.top(bits, uninitialized=uninit_flag) + return StridedInterval(bits=bits, stride=stride, lower_bound=lb, upper_bound=ub) + return StridedInterval.top(bits) raise ClaripyVSAError(f"We shouldn't see this case: {a} * {b}") @@ -1588,7 +1552,6 @@ def _wrapped_unsigned_div(a, b): bits = max(a.bits, b.bits) divisor_lb, divisor_ub = b.lower_bound, b.upper_bound - uninit_flag = a.uninitialized | b.uninitialized # Make sure divisor_lb and divisor_ub is not 0 if divisor_lb == 0: @@ -1612,7 +1575,6 @@ def _wrapped_unsigned_div(a, b): stride=stride, lower_bound=lb, upper_bound=ub, - uninitialized=uninit_flag, ) @staticmethod @@ -1630,7 +1592,6 @@ def _wrapped_signed_div(a, b): # Make sure the divisor is not 0 divisor_lb = b.lower_bound divisor_ub = b.upper_bound - uninit_flag = a.uninitialized | b.uninitialized if divisor_lb == 0: # Try to increment it @@ -1675,7 +1636,6 @@ def _wrapped_signed_div(a, b): stride=stride, lower_bound=lb, upper_bound=ub, - uninitialized=uninit_flag, ) # @@ -1757,9 +1717,7 @@ def neg(self): :return: 0 - self """ - si = StridedInterval(bits=self.bits, stride=0, lower_bound=0, upper_bound=0).sub(self) - si.uninitialized = self.uninitialized - return si + return StridedInterval(bits=self.bits, stride=0, lower_bound=0, upper_bound=0).sub(self) @normalize_types def add(self, b): @@ -1794,15 +1752,10 @@ def add(self, b): lb = self._modular_add(self.lower_bound, b.lower_bound, new_bits) ub = self._modular_add(self.upper_bound, b.upper_bound, new_bits) - # Is it initialized? - uninitialized = self.uninitialized or b.uninitialized - # Take the GCD of two operands' strides stride = math.gcd(self.stride, b.stride) - return StridedInterval( - bits=new_bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninitialized - ).normalize() + return StridedInterval(bits=new_bits, stride=stride, lower_bound=lb, upper_bound=ub).normalize() @normalize_types def sub(self, b): @@ -1821,15 +1774,10 @@ def sub(self, b): lb = self._modular_sub(self.lower_bound, b.upper_bound, new_bits) ub = self._modular_sub(self.upper_bound, b.lower_bound, new_bits) - # Is it initialized? - uninitialized = self.uninitialized or b.uninitialized - # Take the GCD of two operands' strides stride = math.gcd(self.stride, b.stride) - return StridedInterval( - bits=new_bits, stride=stride, lower_bound=lb, upper_bound=ub, uninitialized=uninitialized - ).normalize() + return StridedInterval(bits=new_bits, stride=stride, lower_bound=lb, upper_bound=ub).normalize() @normalize_types def mul(self, o): @@ -1905,7 +1853,6 @@ def udiv(self, o): return StridedInterval.least_upper_bound(*resulting_intervals).normalize() - # FIXME: preserve uninitialized flag? @reversed_processor def bitwise_not(self): """ @@ -1926,10 +1873,7 @@ def bitwise_not(self): tmp = StridedInterval(bits=self.bits, stride=stride, lower_bound=lb, upper_bound=ub) result_interval.append(tmp) - si = StridedInterval.least_upper_bound(*result_interval).normalize() - # preserve the uninitialized flag - si.uninitialized = self.uninitialized - return si + return StridedInterval.least_upper_bound(*result_interval).normalize() @normalize_types def bitwise_or(self, t): @@ -2112,7 +2056,6 @@ def rshift_logical(self, shift_amount): return StridedInterval.top(self.bits) ret.normalize() - ret.uninitialized = self.uninitialized return ret def _unrev_rshift_logical(self, shift_amount): @@ -2139,7 +2082,6 @@ def _unrev_rshift_logical(self, shift_amount): return StridedInterval.top(self.bits) ret.normalize() - ret.uninitialized = self.uninitialized return ret @reversed_processor @@ -2167,7 +2109,6 @@ def rshift_arithmetic(self, shift_amount): return StridedInterval.top(self.bits) ret.normalize() - ret.uninitialized = self.uninitialized return ret @reversed_processor @@ -2195,7 +2136,6 @@ def lshift(self, shift_amount): stride=max(self.stride << lower, 1), lower_bound=new_lower_bound, upper_bound=new_upper_bound, - uninitialized=self.uninitialized, ) ret.normalize() @@ -2220,7 +2160,6 @@ def cast_low(self, tok): stride=self.stride, lower_bound=self.lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, ) # the range between lower bound and upper bound can be represented @@ -2228,25 +2167,21 @@ def cast_low(self, tok): if 0 <= (self.upper_bound - self.lower_bound) <= mask: l = self.lower_bound & mask u = self.upper_bound & mask - return StridedInterval( - bits=tok, stride=self.stride, lower_bound=l, upper_bound=u, uninitialized=self.uninitialized - ) + return StridedInterval(bits=tok, stride=self.stride, lower_bound=l, upper_bound=u) if (self.upper_bound & mask == self.lower_bound & mask) and ((self.upper_bound - self.lower_bound) & mask == 0): # This operation doesn't affect the stride. Stride should be 0 then. bound = self.lower_bound & mask - return StridedInterval( - bits=tok, stride=0, lower_bound=bound, upper_bound=bound, uninitialized=self.uninitialized - ) + return StridedInterval(bits=tok, stride=0, lower_bound=bound, upper_bound=bound) ntz = StridedInterval._ntz(self.stride) if tok > ntz: new_lower = self.lower_bound & ((2**ntz) - 1) stride = 2**ntz - ret = self.top(tok, uninitialized=self.uninitialized) + ret = self.top(tok) ret.stride = stride ret.lower_bound = new_lower k = (ret.upper_bound - ret.lower_bound) // ret.stride @@ -2278,7 +2213,6 @@ def _unrev_cast_low(self, tok): stride=self.stride, lower_bound=self.lower_bound, upper_bound=self.upper_bound, - uninitialized=self.uninitialized, ) # the range between lower bound and upper bound can be represented @@ -2295,21 +2229,17 @@ def _unrev_cast_low(self, tok): # how this should happen ? log.warning("Upper bound value is less than 0") u = StridedInterval._to_negative(u, tok) - return StridedInterval( - bits=tok, stride=self.stride, lower_bound=l, upper_bound=u, uninitialized=self.uninitialized - ) + return StridedInterval(bits=tok, stride=self.stride, lower_bound=l, upper_bound=u) if (self.upper_bound & mask == self.lower_bound & mask) and ((self.upper_bound - self.lower_bound) & mask == 0): # This operation doesn't affect the stride. Stride should be 0 then. bound = self.lower_bound & mask - return StridedInterval( - bits=tok, stride=0, lower_bound=bound, upper_bound=bound, uninitialized=self.uninitialized - ) + return StridedInterval(bits=tok, stride=0, lower_bound=bound, upper_bound=bound) # TODO: How can we do better here? For example, keep the stride information? - return self.top(tok, uninitialized=self.uninitialized) + return self.top(tok) @normalize_types def concat(self, b): @@ -2341,7 +2271,6 @@ def extract(self, high_bit, low_bit): if bits != self.bits: ret = ret.cast_low(bits) - ret.uninitialized = self.uninitialized return ret.normalize() def _unrev_extract(self, high_bit, low_bit): @@ -2353,7 +2282,6 @@ def _unrev_extract(self, high_bit, low_bit): if bits != self.bits: ret = ret._unrev_cast_low(bits) - ret.uninitialized = self.uninitialized return ret.normalize() @reversed_processor @@ -2486,7 +2414,6 @@ def sign_extend(self, new_length): all_resulting_intervals.append(si_) si = StridedInterval.least_upper_bound(*all_resulting_intervals).normalize() - si.uninitialized = self.uninitialized return si @normalize_types @@ -2595,9 +2522,6 @@ def least_upper_bound(*intervals_to_join): if ret is None or ret.n_values > si.n_values: ret = si - if any(x for x in intervals_to_join if x.uninitialized): - ret.uninitialized = True - return ret @normalize_types @@ -2633,8 +2557,6 @@ def pseudo_join(s, b, smart_join=True): if s._reversed != b._reversed: log.warning("Incoherent reversed flag between operands %s and %s", s, b) - uninit_flag = s.uninitialized | b.uninitialized - # # Trivial cases # @@ -2648,7 +2570,7 @@ def pseudo_join(s, b, smart_join=True): u = max(s.upper_bound, b.upper_bound) if smart_join else b.upper_bound l = min(s.lower_bound, b.lower_bound) if smart_join else s.lower_bound stride = abs(u - l) - return StridedInterval(bits=w, stride=stride, lower_bound=l, upper_bound=u, uninitialized=uninit_flag) + return StridedInterval(bits=w, stride=stride, lower_bound=l, upper_bound=u) # # Other cases @@ -2663,7 +2585,6 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride, lower_bound=b.lower_bound, upper_bound=b.upper_bound, - uninitialized=uninit_flag, ) if b._is_surrounded(s): @@ -2676,7 +2597,6 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride, lower_bound=s.lower_bound, upper_bound=s.upper_bound, - uninitialized=uninit_flag, ) if ( @@ -2686,7 +2606,7 @@ def pseudo_join(s, b, smart_join=True): and b._surrounds_member(s.upper_bound) ): # The union of them covers the entire sphere - return StridedInterval.top(w, uninitialized=uninit_flag) + return StridedInterval.top(w) if s._surrounds_member(b.lower_bound): # Overlapping. Nor s or b are integer here. @@ -2698,7 +2618,6 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride, lower_bound=s.lower_bound, upper_bound=b.upper_bound, - uninitialized=uninit_flag, ) if b._surrounds_member(s.lower_bound): # Overlapping. Nor s or b are integer here. @@ -2710,7 +2629,6 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride, lower_bound=b.lower_bound, upper_bound=s.upper_bound, - uninitialized=uninit_flag, ) # no overlapping. # we join the two intervals according on the order they are given @@ -2729,7 +2647,6 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride, lower_bound=s.lower_bound, upper_bound=b.upper_bound, - uninitialized=uninit_flag, ) # Else: smart join. @@ -2754,14 +2671,12 @@ def pseudo_join(s, b, smart_join=True): stride=new_stride1, lower_bound=b.lower_bound, upper_bound=s.upper_bound, - uninitialized=uninit_flag, ) si2 = StridedInterval( bits=w, stride=new_stride2, lower_bound=s.lower_bound, upper_bound=b.upper_bound, - uninitialized=uninit_flag, ) if si1.n_values <= si2.n_values: @@ -3270,7 +3185,6 @@ def _reverse(self): for b in list_bytes: si = b if si is None else si.concat(b) - si.uninitialized = self.uninitialized si._reversed = o._reversed return si @@ -3326,9 +3240,7 @@ def inv_is_top(si): si_ub <<= 8 si_ub |= b - si = StridedInterval( - bits=o.bits, lower_bound=si_lb, upper_bound=si_ub, stride=o._stride, uninitialized=o.uninitialized - ) + si = StridedInterval(bits=o.bits, lower_bound=si_lb, upper_bound=si_ub, stride=o._stride) si._reversed = o._reversed if not o.is_integer: @@ -3344,7 +3256,6 @@ def CreateStridedInterval( # pylint: disable=too-many-positional-arguments stride=None, lower_bound=None, upper_bound=None, - uninitialized=False, to_conv=None, discrete_set=False, discrete_set_max_cardinality=None, @@ -3389,7 +3300,6 @@ def CreateStridedInterval( # pylint: disable=too-many-positional-arguments stride=stride, lower_bound=lower_bound, upper_bound=upper_bound, - uninitialized=uninitialized, ) if not discrete_set: return bi diff --git a/claripy/operations.py b/claripy/operations.py index ed677f0e8..48a1fcd7c 100644 --- a/claripy/operations.py +++ b/claripy/operations.py @@ -62,10 +62,6 @@ def _op(*args): if calc_length is not None: kwargs["length"] = calc_length(*fixed_args) - kwargs["uninitialized"] = None - if any(a.uninitialized is True for a in args if isinstance(a, claripy.ast.Base)): - kwargs["uninitialized"] = True - return return_type(name, fixed_args, **kwargs) _op.calc_length = calc_length diff --git a/tests/test_simplify.py b/tests/test_simplify.py index 895c0b0b9..2331b17dd 100644 --- a/tests/test_simplify.py +++ b/tests/test_simplify.py @@ -58,7 +58,7 @@ def assert_correct(a, b): def test_rotate_shift_mask_simplification(self): a = claripy.BVS("N", 32).annotate(claripy.annotation.StridedIntervalAnnotation(1, 0x1, 0xC)) - extend_ = claripy.BVS("extend", 32, uninitialized=True) + extend_ = claripy.BVS("extend", 32) a_ext = extend_.concat(a) expr = ((a_ext << 3) | (claripy.LShR(a_ext, 61))) & 0x7FFFFFFF8 model_vsa = claripy.backends.vsa.convert(expr) diff --git a/tests/test_strings.py b/tests/test_strings.py index a8435b35a..e5f67082e 100644 --- a/tests/test_strings.py +++ b/tests/test_strings.py @@ -289,7 +289,7 @@ def test_index_of_symbolic_start_idx(self): self.assertTrue(32 < s.index("an") < 38) def test_str_to_int(self): - str_symb = claripy.StringS("symb_strtoint", 4, explicit_name=True) + str_symb = claripy.StringS("symb_strtoint", explicit_name=True) res = claripy.StrToInt(str_symb) solver = self.get_solver() target_num = 12 if KEEP_TEST_PERFORMANT else 100000 diff --git a/tests/test_vsa.py b/tests/test_vsa.py index a6e54755b..62f212e75 100644 --- a/tests/test_vsa.py +++ b/tests/test_vsa.py @@ -580,7 +580,6 @@ def test_sign_extension(self): def test_comparison_si_bvv(self): # Comparison between claripy.SI and BVV si = claripy.SI(bits=32, stride=1, lower_bound=-0x7F, upper_bound=0x7F) - claripy.backends.vsa.convert(si).uninitialized = True bvv = claripy.BVV(0x30, 32) comp = si < bvv assert claripy.backends.vsa.convert(comp).identical(MaybeResult())