From ad37447e06ef6a60acb20c1301010e415c5d9801 Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Thu, 2 Jan 2025 15:35:37 -0700 Subject: [PATCH] Fix some low hanging type issues --- claripy/__init__.py | 4 +++- claripy/annotation.py | 30 +++++-------------------- claripy/ast/base.py | 25 ++++++++++++--------- claripy/ast/bool.py | 4 ++-- claripy/ast/bv.py | 17 +++++++------- claripy/ast/fp.py | 4 ++-- claripy/ast/strings.py | 6 ++--- claripy/backends/backend.py | 26 ++++++++++----------- claripy/backends/backend_concrete/bv.py | 10 ++++++--- claripy/backends/backend_z3.py | 2 +- claripy/operations.py | 6 ++--- 11 files changed, 62 insertions(+), 72 deletions(-) diff --git a/claripy/__init__.py b/claripy/__init__.py index 30fc4e3e9..a790a3e7f 100644 --- a/claripy/__init__.py +++ b/claripy/__init__.py @@ -95,7 +95,7 @@ ClaripyZeroDivisionError, UnsatError, ) -from claripy.fp import FSORT_DOUBLE, FSORT_FLOAT +from claripy.fp import FSORT_DOUBLE, FSORT_FLOAT, RM, FSort from claripy.solvers import ( Solver, SolverCacheless, @@ -117,6 +117,7 @@ "FPV", "FSORT_DOUBLE", "FSORT_FLOAT", + "RM", "SGE", "SGT", "SI", @@ -139,6 +140,7 @@ "ClaripyZeroDivisionError", "Concat", "Extract", + "FSort", "If", "IntToStr", "LShR", diff --git a/claripy/annotation.py b/claripy/annotation.py index d27f0391e..8f64e8800 100644 --- a/claripy/annotation.py +++ b/claripy/annotation.py @@ -14,23 +14,10 @@ class Annotation: They provide a means to pass extra information to the claripy backends. """ - @property - def eliminatable(self) -> bool: # pylint:disable=no-self-use - """ - Returns whether this annotation can be eliminated in a simplification. - - :return: True if eliminatable, False otherwise - """ - return True - - @property - def relocatable(self) -> bool: # pylint:disable=no-self-use - """ - Returns whether this annotation can be relocated in a simplification. - - :return: True if it can be relocated, false otherwise. - """ - return False + # Whether this annotation can be eliminated in a simplification. + eliminatable: bool = True + # Whether this annotation can be relocated in a simplification. + relocatable: bool = False def relocate(self, src: claripy.ast.Base, dst: claripy.ast.Base): # pylint:disable=no-self-use,unused-argument """ @@ -70,13 +57,8 @@ def relocate(self, src: claripy.ast.Base, dst: claripy.ast.Base): # pylint:disa class SimplificationAvoidanceAnnotation(Annotation): """SimplificationAvoidanceAnnotation is an annotation that prevents simplification of an AST.""" - @property - def eliminatable(self): - return False - - @property - def relocatable(self): - return False + eliminatable = False + relocatable = False class StridedIntervalAnnotation(SimplificationAvoidanceAnnotation): diff --git a/claripy/ast/base.py b/claripy/ast/base.py index b805323ca..7e18e4c83 100644 --- a/claripy/ast/base.py +++ b/claripy/ast/base.py @@ -131,7 +131,7 @@ class Base: _hash_cache: WeakValueDictionary[int, Base] = WeakValueDictionary() def __new__( # pylint:disable=redefined-builtin - cls: type[Base], + cls: type[T], op: str, args: Iterable[ArgType], add_variables: Iterable[str] | None = None, @@ -143,7 +143,7 @@ def __new__( # pylint:disable=redefined-builtin skip_child_annotations: bool = False, length: int | None = None, encoded_name: bytes | None = None, - ): + ) -> T: """ This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes @@ -229,7 +229,7 @@ def __new__( # pylint:disable=redefined-builtin def make_like( self, op: str, - args: Iterable[ArgType], + args: tuple[ArgType, ...], simplify: bool = False, annotations: tuple[Annotation, ...] | None = None, variables: frozenset[str] | None = None, @@ -309,14 +309,14 @@ def __a_init__( op: str, args: tuple[ArgType, ...], variables: frozenset[str], - symbolic: bool | None = None, + symbolic: bool, length: int | None = None, errored: set[Backend] | None = None, - annotations: tuple[Annotation, ...] | None = None, + annotations: tuple[Annotation, ...] = (), encoded_name: bytes | None = None, depth: int | None = None, - uneliminatable_annotations: frozenset[Annotation] | None = None, - relocatable_annotations: frozenset[Annotation] | None = None, + uneliminatable_annotations: frozenset[Annotation] = frozenset(), + relocatable_annotations: frozenset[Annotation] = frozenset(), ) -> None: """ Initializes an AST. Takes the same arguments as ``Base.__new__()`` @@ -332,7 +332,7 @@ def __a_init__( self.length = length self.variables = variables self.symbolic = symbolic - self.annotations: tuple[Annotation] = annotations + self.annotations = annotations self._uneliminatable_annotations = uneliminatable_annotations self._relocatable_annotations = relocatable_annotations @@ -361,7 +361,7 @@ def __init__(self, *args, **kwargs): @staticmethod def _calc_hash( op: str, - args: tuple[Base, ...], + args: tuple[ArgType, ...], annotations: tuple[Annotation, ...], length: int | None, ) -> int: @@ -452,7 +452,10 @@ def hash(self) -> int: @property def _encoded_name(self) -> bytes: if self._cached_encoded_name is None: - self._cached_encoded_name = self.args[0].encode() + if isinstance(self.args[0], str): + self._cached_encoded_name = self.args[0].encode() + else: + self._cached_encoded_name = self._hash.to_bytes(8, "little") return self._cached_encoded_name def identical(self, other: Self) -> bool: @@ -836,7 +839,7 @@ def structurally_match(self, o: Base) -> bool: return True - def canonicalize(self, var_map=None, counter=None) -> Self: + def canonicalize(self, var_map=None, counter=None) -> tuple[dict[str, str], itertools.count, Self]: counter = itertools.count() if counter is None else counter var_map = {} if var_map is None else var_map diff --git a/claripy/ast/bool.py b/claripy/ast/bool.py index 2b6cabe37..d818f0000 100644 --- a/claripy/ast/bool.py +++ b/claripy/ast/bool.py @@ -50,7 +50,7 @@ def size(self): # pylint:disable=no-self-use __len__ = size -def BoolS(name, explicit_name=None) -> Bool: +def BoolS(name: str, explicit_name: bool = False) -> Bool: """ Creates a boolean symbol (i.e., a variable). @@ -59,7 +59,7 @@ def BoolS(name, explicit_name=None) -> Bool: :return: A Bool object representing this symbol. """ - n = _make_name(name, -1, False if explicit_name is None else explicit_name) + n = _make_name(name, -1, explicit_name) return Bool("BoolS", (n,), variables=frozenset((n,)), symbolic=True) diff --git a/claripy/ast/bv.py b/claripy/ast/bv.py index 69bd5585d..125fa02ce 100644 --- a/claripy/ast/bv.py +++ b/claripy/ast/bv.py @@ -162,9 +162,9 @@ def val_to_fp(self, sort, signed=True, rm=None): :return: An FP AST whose value is the same as this BV """ if rm is None: - rm = claripy.fp.RM.default() + rm = claripy.RM.default() if sort is None: - sort = claripy.fp.FSort.from_size(self.length) + sort = claripy.FSort.from_size(self.length) op = claripy.ast.fp.fpToFP if signed else claripy.ast.fp.fpToFPUnsigned return op(rm, self, sort) @@ -176,7 +176,7 @@ def raw_to_fp(self): :return: An FP AST whose bit-pattern is the same as this BV """ - sort = claripy.fp.FSort.from_size(self.length) + sort = claripy.FSort.from_size(self.length) return claripy.ast.fp.fpToFP(self, sort) def raw_to_bv(self): @@ -197,7 +197,7 @@ def identical(self, other: Self) -> bool: def BVS( # pylint:disable=redefined-builtin name, size, - explicit_name=None, + explicit_name: bool = False, **kwargs, ) -> BV: """ @@ -220,7 +220,7 @@ def BVS( # pylint:disable=redefined-builtin if size is None or not isinstance(size, int): raise TypeError("Size value for BVS must be an integer") - n = _make_name(name, size, False if explicit_name is None else explicit_name) + n = _make_name(name, size, explicit_name) encoded_name = n.encode() return BV( @@ -284,15 +284,14 @@ def SI( lower_bound=None, upper_bound=None, stride=None, - explicit_name=None, + explicit_name=False, ): return BVS(name, bits, explicit_name=explicit_name).annotate( - claripy.annotation.StridedIntervalAnnotation(stride, lower_bound, upper_bound) + claripy.annotation.StridedIntervalAnnotation(stride or 1, lower_bound or 0, upper_bound or 2**bits - 1) ) -def TSI(bits, name=None, explicit_name=None): - name = "unnamed" if name is None else name +def TSI(bits, name="unnamed", explicit_name=False): return BVS(name, bits, explicit_name=explicit_name) diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index e27afb823..76ce8a8c1 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -82,7 +82,7 @@ def _from_float(like, value) -> FP: _from_str = _from_float -def FPS(name, sort, explicit_name=None) -> FP: +def FPS(name, sort, explicit_name: bool = False) -> FP: """ Creates a floating-point symbol. @@ -92,7 +92,7 @@ def FPS(name, sort, explicit_name=None) -> FP: :return: An FP AST. """ - n = _make_name(name, sort.length, False if explicit_name is None else explicit_name, prefix="FP_") + n = _make_name(name, sort.length, explicit_name, prefix="FP_") return FP("FPS", (n, sort), variables=frozenset((n,)), symbolic=True, length=sort.length) diff --git a/claripy/ast/strings.py b/claripy/ast/strings.py index 4ab09f41f..a1b1f46fb 100644 --- a/claripy/ast/strings.py +++ b/claripy/ast/strings.py @@ -47,7 +47,7 @@ def indexOf(self, pattern, start_idx): return StrIndexOf(self, pattern, start_idx) -def StringS(name, explicit_name=False, **kwargs): +def StringS(name, explicit_name: bool = False, **kwargs): """ Create a new symbolic string (analogous to z3.String()) @@ -56,7 +56,7 @@ def StringS(name, explicit_name=False, **kwargs): :returns: The String object representing the symbolic string """ - n = _make_name(name, 0, False if explicit_name is None else explicit_name) + n = _make_name(name, 0, explicit_name) return String( "StringS", (n,), @@ -66,7 +66,7 @@ def StringS(name, explicit_name=False, **kwargs): ) -def StringV(value, **kwargs): +def StringV(value: str, **kwargs): """ Create a new Concrete string (analogous to z3.StringVal()) diff --git a/claripy/backends/backend.py b/claripy/backends/backend.py index 5e7a77175..620c5837c 100644 --- a/claripy/backends/backend.py +++ b/claripy/backends/backend.py @@ -7,7 +7,7 @@ import threading from contextlib import suppress -from claripy.ast import Base +from claripy.ast import BV, Base from claripy.errors import BackendError, BackendUnsupportedError, ClaripyRecursionError log = logging.getLogger(__name__) @@ -282,7 +282,7 @@ def _call(self, op, args): # Abstraction and resolution. # - def _abstract(self, e): # pylint:disable=W0613,R0201 + def _abstract(self, e) -> Base: # pylint:disable=W0613,R0201 """ Abstracts the BackendObject e to an AST. @@ -464,7 +464,7 @@ def solver(self, timeout=None): # pylint:disable=no-self-use,unused-argument """ raise BackendError("backend doesn't support solving") - def add(self, s, c, track=False): + def add(self, s, c, track=False) -> None: """ This function adds constraints to the backend solver. @@ -474,7 +474,7 @@ def add(self, s, c, track=False): """ return self._add(s, self.convert_list(c), track=track) - def _add(self, s, c, track=False): # pylint:disable=no-self-use,unused-argument + def _add(self, s, c, track=False) -> None: # pylint:disable=no-self-use,unused-argument """ This function adds constraints to the backend solver. @@ -612,7 +612,7 @@ def min(self, expr, extra_constraints=(), signed=False, solver=None, model_callb def _min( self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None - ): # pylint:disable=unused-argument,no-self-use + ) -> BV: # pylint:disable=unused-argument,no-self-use """ Return the minimum value of expr. @@ -708,7 +708,7 @@ def satisfiable(self, extra_constraints=(), solver=None, model_callback=None): def _satisfiable( self, extra_constraints=(), solver=None, model_callback=None - ): # pylint:disable=no-self-use,unused-argument + ) -> bool: # pylint:disable=no-self-use,unused-argument """ This function does a constraint check and returns a model for a solver. @@ -719,7 +719,7 @@ def _satisfiable( """ raise BackendError("backend doesn't support solving") - def solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None): + def solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None) -> bool: """ Return True if `v` is a solution of `expr` with the extra constraints, False otherwise. @@ -744,7 +744,7 @@ def solution(self, expr, v, extra_constraints=(), solver=None, model_callback=No def _solution( self, expr, v, extra_constraints=(), solver=None, model_callback=None - ): # pylint:disable=unused-argument,no-self-use + ) -> bool: # pylint:disable=unused-argument,no-self-use """ Return True if v is a solution of expr with the extra constraints, False otherwise. @@ -770,7 +770,7 @@ def name(self, a): """ return self._name(self.convert(a)) - def _name(self, o): # pylint:disable=no-self-use,unused-argument + def _name(self, o) -> str | None: # pylint:disable=no-self-use,unused-argument """ This should return the name of an object. @@ -778,7 +778,7 @@ def _name(self, o): # pylint:disable=no-self-use,unused-argument """ raise BackendError("backend doesn't support name()") - def identical(self, a, b): + def identical(self, a, b) -> bool: """ This should return whether `a` is identical to `b`. Of course, this isn't always clear. True should mean that it is definitely identical. False eans that, conservatively, it might not be. @@ -788,7 +788,7 @@ def identical(self, a, b): """ return self._identical(self.convert(a), self.convert(b)) - def _identical(self, a, b): # pylint:disable=no-self-use,unused-argument + def _identical(self, a, b) -> bool: # pylint:disable=no-self-use,unused-argument """ This should return whether `a` is identical to `b`. This is the native version of ``identical()``. @@ -797,7 +797,7 @@ def _identical(self, a, b): # pylint:disable=no-self-use,unused-argument """ raise BackendError("backend doesn't support identical()") - def cardinality(self, a): + def cardinality(self, a) -> int: """ This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation. @@ -807,7 +807,7 @@ def cardinality(self, a): """ return self._cardinality(self.convert(a)) - def _cardinality(self, a): # pylint:disable=no-self-use,unused-argument + def _cardinality(self, a) -> int: # pylint:disable=no-self-use,unused-argument """ This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation. diff --git a/claripy/backends/backend_concrete/bv.py b/claripy/backends/backend_concrete/bv.py index da1ba3ba6..6f8a862e2 100644 --- a/claripy/backends/backend_concrete/bv.py +++ b/claripy/backends/backend_concrete/bv.py @@ -53,9 +53,13 @@ class BVV(BackendObject): Any use outside of claripy should use `claripy.BVV` instead. """ + _value: int + bits: int + mod: int + __slots__ = ["_value", "bits", "mod"] - def __init__(self, value, bits): + def __init__(self, value: int, bits: int): if _d._DEBUG: if not isinstance(bits, numbers.Number) or bits < 0: raise ClaripyOperationError("BVV needs a non-negative length and an int value") @@ -86,8 +90,8 @@ def value(self): return self._value @value.setter - def value(self, v): - self._value = v & (self.mod - 1) if v is not None else None + def value(self, v: int): + self._value = v & (self.mod - 1) @property def signed(self): diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index 29604125b..cecd71e75 100644 --- a/claripy/backends/backend_z3.py +++ b/claripy/backends/backend_z3.py @@ -956,7 +956,7 @@ def _is_false(self, e, extra_constraints=(), solver=None, model_callback=None): def _is_true(self, e, extra_constraints=(), solver=None, model_callback=None): return z3.simplify(e).eq(z3.BoolVal(True, ctx=self._context)) - def _solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None): + def _solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None) -> bool: return self._satisfiable( extra_constraints=(expr == v, *tuple(extra_constraints)), solver=solver, model_callback=model_callback ) diff --git a/claripy/operations.py b/claripy/operations.py index 23dc9d0bc..8a31bd748 100644 --- a/claripy/operations.py +++ b/claripy/operations.py @@ -28,8 +28,8 @@ def op(name, arg_types, return_type: type[T], extra_check=None, calc_length=None def _type_fixer(args): num_args = len(args) if expected_num_args is not None and num_args != expected_num_args: - if num_args + 1 == expected_num_args and arg_types[0] is claripy.fp.RM: - args = (claripy.fp.RM.default(), *args) + if num_args + 1 == expected_num_args and arg_types[0] is claripy.RM: + args = (claripy.RM.default(), *args) else: raise ClaripyTypeError(f"Operation {name} takes exactly {len(arg_types)} arguments ({len(args)} given)") @@ -37,7 +37,7 @@ def _type_fixer(args): matches = list(itertools.starmap(isinstance, zip(args, actual_arg_types, strict=False))) # heuristically, this works! - thing = args[matches.index(True, 1 if actual_arg_types[0] is claripy.fp.RM else 0)] if True in matches else None + thing = args[matches.index(True, 1 if actual_arg_types[0] is claripy.RM else 0)] if True in matches else None for arg, argty, match in zip(args, actual_arg_types, matches, strict=False): if not match: