Move all frontends under frontend sub-package (#512)

* Move all frontends under frontend sub-package

* Improve lint

* Improve lint for solvers.py

claripy/frontend/__init__.py

@@ -0,0 +1,19 @@
+from __future__ import annotations
+
+from claripy.frontend import mixin
+from claripy.frontend.composite_frontend import CompositeFrontend
+from claripy.frontend.frontend import Frontend
+from claripy.frontend.full_frontend import FullFrontend
+from claripy.frontend.hybrid_frontend import HybridFrontend
+from claripy.frontend.light_frontend import LightFrontend
+from claripy.frontend.replacement_frontend import ReplacementFrontend
+
+__all__ = (
+    "Frontend",
+    "CompositeFrontend",
+    "FullFrontend",
+    "HybridFrontend",
+    "LightFrontend",
+    "ReplacementFrontend",
+    "mixin",
+)

claripy/frontends/composite_frontend.py → claripy/frontend/composite_frontend.py

@@ -9,20 +9,28 @@
 from claripy.ast import Base
 from claripy.ast.bool import Or
 from claripy.errors import BackendError, UnsatError
-from claripy.frontend_mixins.model_cache_mixin import ModelCacheMixin
-from claripy.frontend_mixins.simplify_skipper_mixin import SimplifySkipperMixin
 
 from .constrained_frontend import ConstrainedFrontend
+from .mixin import ModelCacheMixin, SimplifySkipperMixin
 
 if TYPE_CHECKING:
-    from claripy import SolverCompositeChild
+    from claripy.solvers import SolverCompositeChild
 
 
 log = logging.getLogger(__name__)
 symbolic_count = itertools.count()
 
 
 class CompositeFrontend(ConstrainedFrontend):
+    """Composite Solver splits constraints into independent sets, allowing
+    caching to be done on a per-set basis. Additionally, by allowing constraints
+    to be solved independently, the solver can be more efficient in some cases
+    ("divide and conquer").
+
+    For example, the constraints (a==b, b==1, c==4) would be split into two
+    sets: one containing a==b and b==1, and the other containing c==4.
+    """
+
     def __init__(self, template_frontend, track=False, **kwargs):
         super().__init__(**kwargs)
         self._solvers = {}
@@ -502,12 +510,5 @@ def merge(self, others, merge_conditions, common_ancestor=None):
         merged.constraints = list(itertools.chain.from_iterable(a.constraints for a in merged._solver_list))
         return True, merged
 
-    def combine(self, others):
-        combined = self.blank_copy()
-        combined.add(self.constraints)
-        for o in others:
-            combined.add(o.constraints)
-        return combined
-
     def split(self):
         return [s.branch() for s in self._solver_list]

claripy/frontends/constrained_frontend.py → claripy/frontend/constrained_frontend.py

@@ -5,7 +5,8 @@
 from claripy.annotation import SimplificationAvoidanceAnnotation
 from claripy.ast.base import simplify
 from claripy.ast.bool import And, Or
-from claripy.frontend import Frontend
+
+from .frontend import Frontend
 
 log = logging.getLogger(__name__)
 
@@ -82,7 +83,7 @@ def merge(self, others, merge_conditions, common_ancestor=None):
     def combine(self, others):
         combined = self.blank_copy()
 
-        combined.add(self.constraints)  # pylint:disable=E1101
+        combined.add(self.constraints)
         for o in others:
             combined.add(o.constraints)
         return combined

claripy/frontend.py → claripy/frontend/frontend.py

@@ -4,13 +4,17 @@
 import numbers
 
 from claripy.ast.bool import BoolV
-
-from . import ast
+from claripy.ast.bv import BV, BVV
+from claripy.ast.strings import String, StringV
 
 log = logging.getLogger(__name__)
 
 
 class Frontend:
+    """Frontend is the base class for all claripy Solvers, which are the
+    interfaces to the backend constraint solvers.
+    """
+
     def __init__(self):
         pass
 
@@ -54,10 +58,10 @@ def eval_to_ast(self, e, n, extra_constraints=(), exact=None):
         """
         values = self.eval(e, n, extra_constraints=extra_constraints, exact=exact)
 
-        if isinstance(e, ast.BV):
-            return [ast.bv.BVV(v, e.size()) for v in values]
-        if isinstance(e, ast.String):
-            return [ast.strings.StringV(v, length=e.string_length) for v in values]
+        if isinstance(e, BV):
+            return [BVV(v, e.size()) for v in values]
+        if isinstance(e, String):
+            return [StringV(v, length=e.string_length) for v in values]
 
         # TODO: Implement support for other types
         raise NotImplementedError

claripy/frontends/full_frontend.py → claripy/frontend/full_frontend.py

@@ -2,7 +2,7 @@
 
 import logging
 import threading
-from typing import TYPE_CHECKING, Any, TypeVar, overload
+from typing import TYPE_CHECKING, Any, overload
 
 from claripy import backends
 from claripy.ast.bv import SGE, SLE, UGE, ULE
@@ -13,16 +13,20 @@
 if TYPE_CHECKING:
     from collections.abc import Iterable
 
+    from typing_extensions import Self
+
     from claripy.ast.bool import Bool
     from claripy.ast.bv import BV
     from claripy.ast.fp import FP
 
 log = logging.getLogger(__name__)
 
-T = TypeVar("T", bound="FullFrontend")
-
 
 class FullFrontend(ConstrainedFrontend):
+    """FullFrontend is a frontend that supports all claripy operations and is
+    backed by a full solver backend.
+    """
+
     def __init__(self, solver_backend, timeout=None, max_memory=None, track=False, **kwargs):
         ConstrainedFrontend.__init__(self, **kwargs)
         self._track = track
@@ -330,7 +334,7 @@ def downsize(self) -> None:
     # Merging and splitting
     #
 
-    def merge(self: T, others, merge_conditions, common_ancestor=None) -> tuple[bool, T]:
+    def merge(self, others, merge_conditions, common_ancestor=None) -> tuple[bool, Self]:
         return (
             self._solver_backend.__class__.__name__ == "BackendZ3",
             ConstrainedFrontend.merge(self, others, merge_conditions, common_ancestor=common_ancestor)[1],

claripy/frontends/hybrid_frontend.py → claripy/frontend/hybrid_frontend.py

@@ -10,6 +10,13 @@
 
 
 class HybridFrontend(Frontend):
+    """HybridFrontend is a frontend that uses two backends, one exact and one
+    approximate, to solve constraints.
+
+    In practice this allows there to be a solver that can use the VSA backend or
+    the Z3 backend depending on the constraints.
+    """
+
     def __init__(self, exact_frontend, approximate_frontend, approximate_first=False, **kwargs):
         Frontend.__init__(self, **kwargs)
         self._exact_frontend = exact_frontend
@@ -62,9 +69,7 @@ def __setstate__(self, s):
     # Hybrid solving
     #
 
-    def _do_call(self, f_name, *args, **kwargs):
-        exact = kwargs.pop("exact", True)
-
+    def _do_call(self, f_name, *args, exact=True, **kwargs):
         # if approximating, try the approximation backend
         if exact is False:
             try:
@@ -76,8 +81,7 @@ def _do_call(self, f_name, *args, **kwargs):
         return True, getattr(self._exact_frontend, f_name)(*args, **kwargs)
 
     def _hybrid_call(self, f_name, *args, **kwargs):
-        _, solution = self._do_call(f_name, *args, **kwargs)
-        return solution
+        return self._do_call(f_name, *args, **kwargs)[1]
 
     def _approximate_first_call(self, f_name, e, n, *args, **kwargs):
         exact_used, solutions = self._do_call(f_name, e, n + 1, *args, exact=False, **kwargs)
@@ -103,10 +107,10 @@ def eval(self, e, n, extra_constraints=(), exact=None):
             return self._approximate_first_call("eval", e, n, extra_constraints=extra_constraints)
         return self._hybrid_call("eval", e, n, extra_constraints=extra_constraints, exact=exact)
 
-    def batch_eval(self, e, n, extra_constraints=(), exact=None):
+    def batch_eval(self, exprs, n, extra_constraints=(), exact=None):
         if self._approximate_first and exact is None and n > 2:
-            return self._approximate_first_call("batch_eval", e, n, extra_constraints=extra_constraints)
-        return self._hybrid_call("batch_eval", e, n, extra_constraints=extra_constraints, exact=exact)
+            return self._approximate_first_call("batch_eval", exprs, n, extra_constraints=extra_constraints)
+        return self._hybrid_call("batch_eval", exprs, n, extra_constraints=extra_constraints, exact=exact)
 
     def max(self, e, extra_constraints=(), signed=False, exact=None):
         return self._hybrid_call("max", e, extra_constraints=extra_constraints, signed=signed, exact=exact)

claripy/frontends/light_frontend.py → claripy/frontend/light_frontend.py

@@ -11,6 +11,11 @@
 
 
 class LightFrontend(ConstrainedFrontend):
+    """LightFrontend is an extremely simple frontend that is used primarily for
+    the purpose of quickly evaluating expressions using the concrete and VSA
+    backends.
+    """
+
     def __init__(self, solver_backend, **kwargs):
         # since the LightFrontend mostly cannot handle extra_constriants, it horribly misuses the cache.
         # Because of this, we have to disable the caching here.
@@ -23,6 +28,7 @@ def _blank_copy(self, c):
 
     def _copy(self, c):
         super()._copy(c)
+        c._solver_backend = self._solver_backend
 
     #
     # Serialization support
@@ -43,32 +49,32 @@ def __setstate__(self, s):
     def eval(self, e, n, extra_constraints=(), exact=None):
         try:
             return tuple(self._solver_backend.eval(e, n))
-        except BackendError as e:
-            raise ClaripyFrontendError("Light solver can't handle this eval().") from e
+        except BackendError as err:
+            raise ClaripyFrontendError("Light solver can't handle this eval().") from err
 
     def batch_eval(self, exprs, n, extra_constraints=(), exact=None):
         try:
             return self._solver_backend._batch_eval(exprs, n)
-        except BackendError as e:
-            raise ClaripyFrontendError("Light solver can't handle this batch_eval().") from e
+        except BackendError as err:
+            raise ClaripyFrontendError("Light solver can't handle this batch_eval().") from err
 
     def max(self, e, extra_constraints=(), signed=False, exact=None):
         try:
             return self._solver_backend.max(e, signed=signed)
-        except BackendError as e:
-            raise ClaripyFrontendError("Light solver can't handle this max().") from e
+        except BackendError as err:
+            raise ClaripyFrontendError("Light solver can't handle this max().") from err
 
     def min(self, e, extra_constraints=(), signed=False, exact=None):
         try:
             return self._solver_backend.min(e, signed=signed)
-        except BackendError as e:
-            raise ClaripyFrontendError("Light solver can't handle this min().") from e
+        except BackendError as err:
+            raise ClaripyFrontendError("Light solver can't handle this min().") from err
 
     def solution(self, e, v, extra_constraints=(), exact=None):
         try:
             return self._solver_backend.solution(e, v)
-        except BackendError as e:
-            raise ClaripyFrontendError("Light solver can't handle this solution().") from e
+        except BackendError as err:
+            raise ClaripyFrontendError("Light solver can't handle this solution().") from err
 
     def is_true(self, e, extra_constraints=(), exact=None):
         try:

claripy/frontend_mixins/__init__.py → claripy/frontend/mixin/__init__.py

@@ -1,12 +1,10 @@
-# mixins for frontends
 from __future__ import annotations
 
 from .composited_cache_mixin import CompositedCacheMixin
 from .concrete_handler_mixin import ConcreteHandlerMixin
 from .constraint_deduplicator_mixin import ConstraintDeduplicatorMixin
 from .constraint_expansion_mixin import ConstraintExpansionMixin
 from .constraint_filter_mixin import ConstraintFilterMixin
-from .debug_mixin import DebugMixin
 from .eager_resolution_mixin import EagerResolutionMixin
 from .model_cache_mixin import ModelCacheMixin
 from .sat_cache_mixin import SatCacheMixin
@@ -20,7 +18,6 @@
     "ConstraintDeduplicatorMixin",
     "ConstraintExpansionMixin",
     "ConstraintFilterMixin",
-    "DebugMixin",
     "EagerResolutionMixin",
     "ModelCacheMixin",
     "SatCacheMixin",

claripy/frontend_mixins/concrete_handler_mixin.py → claripy/frontend/mixin/concrete_handler_mixin.py

@@ -2,6 +2,10 @@
 
 
 class ConcreteHandlerMixin:
+    """ConcreteHandlerMixin is a mixin that handles concrete expressions
+    evaluation to prevent invoking the backend solver.
+    """
+
     def eval(self, e, n, extra_constraints=(), exact=None):
         c = self._concrete_value(e)
         if c is not None:
@@ -15,9 +19,9 @@ def batch_eval(self, exprs, n, extra_constraints=(), exact=None):
         if len(symbolic_exprs) == 0:
             return [concrete_exprs]
 
-        symbolic_results = map(
-            list, super().batch_eval(symbolic_exprs, n, extra_constraints=extra_constraints, exact=exact)
-        )
+        symbolic_results = [
+            list(r) for r in super().batch_eval(symbolic_exprs, n, extra_constraints=extra_constraints, exact=exact)
+        ]
         return [tuple((c if c is not None else r.pop(0)) for c in concrete_exprs) for r in symbolic_results]
 
     def max(self, e, extra_constraints=(), signed=False, exact=None):

claripy/frontend_mixins/constraint_deduplicator_mixin.py → claripy/frontend/mixin/constraint_deduplicator_mixin.py

@@ -2,6 +2,10 @@
 
 
 class ConstraintDeduplicatorMixin:
+    """ConstraintDeduplicatorMixin is a mixin that prevents duplicate
+    constraints from being added to a solver.
+    """
+
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         self._constraint_hashes = set()

claripy/frontend_mixins/constraint_expansion_mixin.py → claripy/frontend/mixin/constraint_expansion_mixin.py

@@ -9,6 +9,10 @@
 
 
 class ConstraintExpansionMixin:
+    """ConstraintExpansionMixin is a mixin that adds evaluation results as
+    constraints for future evaluations.
+    """
+
     def eval(self, e, n, extra_constraints=(), exact=None):
         results = super().eval(e, n, extra_constraints=extra_constraints, exact=exact)
 

claripy/frontend_mixins/constraint_filter_mixin.py → claripy/frontend/mixin/constraint_filter_mixin.py

@@ -5,6 +5,8 @@
 
 
 class ConstraintFilterMixin:
+    """ConstraintFilterMixin is a mixin that filters True and False constraints."""
+
     def _constraint_filter(self, constraints):
         if type(constraints) not in (tuple, list):
             raise ClaripyValueError("The extra_constraints argument should be a list of constraints.")

claripy/frontend_mixins/model_cache_mixin.py → claripy/frontend/mixin/model_cache_mixin.py

@@ -10,6 +10,8 @@
 
 
 class ModelCache:
+    """ModelCache is a wrapper around a model that provides some additional functionality."""
+
     def __init__(self, model):
         self.model = model
         self.replacements = weakref.WeakKeyDictionary()

claripy/frontend_mixins/sat_cache_mixin.py → claripy/frontend/mixin/sat_cache_mixin.py

@@ -5,6 +5,8 @@
 
 
 class SatCacheMixin:
+    """SatCacheMixin is a mixin that caches the satisfiability of the constraints."""
+
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         self._cached_satness = None

claripy/frontend_mixins/simplify_helper_mixin.py → claripy/frontend/mixin/simplify_helper_mixin.py

@@ -2,6 +2,8 @@
 
 
 class SimplifyHelperMixin:
+    """SimplifyHelperMixin is a mixin that simplifies constraints before evaluation."""
+
     def max(self, e, extra_constraints=(), signed=False, exact=None):
         self.simplify()
         return super().max(e, extra_constraints=extra_constraints, signed=signed, exact=exact)

claripy/frontend_mixins/simplify_skipper_mixin.py → claripy/frontend/mixin/simplify_skipper_mixin.py

@@ -2,6 +2,10 @@
 
 
 class SimplifySkipperMixin:
+    """SimplifySkipperMixin is a mixin that skips simplification when the
+    constraints are already simplified.
+    """
+
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         self._simplified = True