Add BackendAny (#561)

* Add BackendAny

* Rename backends.any to backends.any_backend

* Improve lint

* Handle BackendError being raise in simplify()

claripy/algorithm/simplify.py

@@ -5,7 +5,9 @@
 from typing import TypeVar, cast
 from weakref import WeakValueDictionary
 
+import claripy
 from claripy.ast import Base
+from claripy.errors import BackendError
 
 log = logging.getLogger(__name__)
 
@@ -25,7 +27,10 @@ def simplify(expr: T) -> T:
     if expr.hash() in simplification_cache and simplification_cache[expr.hash()] is not None:
         return cast(T, simplification_cache[expr.hash()])
 
-    simplified = expr._first_backend("simplify")
+    try:
+        simplified = claripy.backends.any_backend.simplify(expr)
+    except BackendError:
+        simplified = None
     if simplified is None:
         log.debug("Unable to simplify expression")
         simplification_cache[expr.hash()] = expr

claripy/ast/base.py

@@ -929,17 +929,6 @@ def canonicalize(self, var_map=None, counter=None) -> Self:
     # these are convenience operations
     #
 
-    def _first_backend(self, what):
-        for b in claripy.backends.all_backends:
-            if b in self._errored:
-                continue
-
-            try:
-                return getattr(b, what)(self)
-            except BackendError:
-                pass
-        return None
-
     @property
     def concrete_value(self):
         try:
@@ -952,15 +941,15 @@ def concrete_value(self):
 
     @property
     def singlevalued(self) -> bool:
-        return self._first_backend("singlevalued")
+        return claripy.backends.any_backend.singlevalued(self)
 
     @property
     def multivalued(self) -> bool:
-        return self._first_backend("multivalued")
+        return claripy.backends.any_backend.multivalued(self)
 
     @property
     def cardinality(self) -> int:
-        return self._first_backend("cardinality")
+        return claripy.backends.any_backend.cardinality(self)
 
     @property
     def concrete(self) -> bool:

claripy/backends/__init__.py

@@ -1,13 +1,15 @@
 from __future__ import annotations
 
 from .backend import Backend
+from .backend_any import BackendAny
 from .backend_concrete import BackendConcrete
 from .backend_vsa import BackendVSA
 from .backend_z3 import BackendZ3
 
 concrete = BackendConcrete()
 z3 = BackendZ3()
 vsa = BackendVSA()
+any_backend = BackendAny()
 
 all_backends = [concrete, z3, vsa]
 backends_by_type = {b.__class__.__name__: b for b in all_backends}
@@ -22,4 +24,5 @@
     "concrete",
     "z3",
     "vsa",
+    "any_backend",
 )

claripy/backends/backend_any.py

@@ -0,0 +1,74 @@
+from __future__ import annotations
+
+import logging
+
+import claripy
+from claripy.backends.backend import Backend
+from claripy.errors import BackendError
+
+log = logging.getLogger(__name__)
+
+
+class BackendAny(Backend):
+    """
+    BackendAny is a wrapper backend that tries all backends in order until
+    one succeeds.
+    """
+
+    # pylint: disable=too-many-positional-arguments,unused-argument
+
+    __slots__ = ()
+
+    @staticmethod
+    def _first_backend(obj, what):
+        for b in claripy.backends.all_backends:
+            if b in obj._errored:
+                continue
+
+            try:
+                return getattr(b, what)(obj)
+            except BackendError:
+                pass
+        raise BackendError(f"All backends failed to {what}")
+
+    def convert(self, expr):
+        return self._first_backend(expr, "convert")
+
+    def simplify(self, expr):
+        return self._first_backend(expr, "simplify")
+
+    def is_true(self, e, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(e, "is_true")
+
+    def is_false(self, e, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(e, "is_false")
+
+    def has_true(self, e, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(e, "has_true")
+
+    def has_false(self, e, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(e, "has_false")
+
+    def eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(expr, "eval")
+
+    def batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(exprs, "batch_eval")
+
+    def min(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None):
+        return self._first_backend(expr, "min")
+
+    def max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None):
+        return self._first_backend(expr, "max")
+
+    def satisfiable(self, extra_constraints=(), solver=None, model_callback=None):
+        return self._first_backend(extra_constraints, "satisfiable")
+
+    def name(self, a):
+        return self._first_backend(a, "name")
+
+    def identical(self, a, b):
+        return self._first_backend(a, "identical")
+
+    def cardinality(self, a):
+        return self._first_backend(a, "cardinality")