Fix some low hanging type issues

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",

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):

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
 

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)
 
 

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)
 
 

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)
 
 

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())
 

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,15 +770,15 @@ 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.
 
         :param o: the (backend-native) object
         """
         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.