Simpify simplify routines (#525)

claripy/ast/base.py

@@ -132,6 +132,7 @@ class Base:
     depth: int
     _hash: int
     _simplified: SimplificationLevel
+    _relocatable_annotations: frozenset[Annotation]
     _uneliminatable_annotations: frozenset[Annotation]
 
     # Backend information
@@ -1262,7 +1263,7 @@ def uninitialized(self) -> bool:
 
 
 def simplify(e: T) -> T:
-    if isinstance(e, Base) and e.is_leaf():
+    if e.is_leaf() or e._simplified == SimplificationLevel.FULL_SIMPLIFY:
         return e
 
     s = e._first_backend("simplify")
@@ -1272,7 +1273,6 @@ def simplify(e: T) -> T:
 
     # Copy some parameters (that should really go to the Annotation backend)
     s._uninitialized = e.uninitialized
-    s._simplified = SimplificationLevel.FULL_SIMPLIFY
 
     # dealing with annotations
     if e.annotations:

claripy/backends/backend.py

@@ -296,13 +296,10 @@ def _abstract(self, e):  # pylint:disable=W0613,R0201
     # These functions simplify expressions.
     #
 
-    def simplify(self, e):
-        o = self._abstract(self._simplify(self.convert(e)))
-        o._simplified = SimplificationLevel.FULL_SIMPLIFY
-        return o
-
-    def _simplify(self, e):  # pylint:disable=R0201,unused-argument
-        raise BackendError(f"backend {self.__class__.__name__} can't simplify")
+    def simplify(self, expr):
+        result = self._abstract(self.convert(expr))
+        result._simplified = SimplificationLevel.FULL_SIMPLIFY
+        return result
 
     #
     # Some other helpers

claripy/backends/backend_concrete/backend_concrete.py

@@ -142,9 +142,6 @@ def _convert(self, r):
             return r
         raise BackendError(f"can't handle AST of type {type(r)}")
 
-    def _simplify(self, e):
-        return e
-
     def _abstract(self, e):  # pylint:disable=no-self-use
         if isinstance(e, bv.BVV):
             return BVV(e.value, e.size())

claripy/backends/backend_vsa/backend_vsa.py

@@ -137,12 +137,6 @@ def _abstract(self, e):
             )
         raise BackendError(f"Don't know how to abstract {type(e)}")
 
-    def _simplify(self, e):
-        """This _simplify impementation works because the simplification is done
-        during the conversion from AST to VSA backend objects.
-        """
-        return e
-
     def _eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None):
         if isinstance(expr, StridedInterval | ValueSet):
             return expr.eval(n)

claripy/backends/backend_z3.py

@@ -877,40 +877,20 @@ def _min(self, expr, extra_constraints=(), signed=False, solver=None, model_call
     def _max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None):
         return self._extrema(True, expr, extra_constraints, signed, solver, model_callback)
 
-    def _simplify(self, e):  # pylint:disable=W0613,R0201
-        raise Exception("This shouldn't be called. Bug Yan.")
-
     @condom
-    def simplify(self, expr):  # pylint:disable=arguments-renamed
-        if expr._simplified:
-            return expr
-
-        # l.debug("SIMPLIFYING EXPRESSION")
-
+    def simplify(self, expr):
         expr_raw = self.convert(expr)
 
-        # l.debug("... before:\n%s", z3_expr_to_smt2(expr_raw))
-
-        # s = expr_raw
         if isinstance(expr_raw, z3.BoolRef):
             boolref_tactics = self._boolref_tactics
-            s = boolref_tactics(expr_raw).as_expr()
-            # n = s.decl().name()
-            # if n == 'true':
-            #    s = True
-            # elif n == 'false':
-            #    s = False
-        elif isinstance(expr_raw, z3.BitVecRef):
-            s = z3.simplify(expr_raw)
+            simplified = boolref_tactics(expr_raw).as_expr()
         else:
-            s = expr_raw
-
-        # l.debug("... after:\n%s", z3_expr_to_smt2(s))
+            simplified = z3.simplify(expr_raw)
 
-        o = self._abstract(s)
-        o._simplified = SimplificationLevel.FULL_SIMPLIFY
+        result = self._abstract(simplified)
+        result._simplified = SimplificationLevel.FULL_SIMPLIFY
 
-        return o
+        return result
 
     def _is_false(self, e, extra_constraints=(), solver=None, model_callback=None):
         return z3.simplify(e).eq(z3.BoolVal(False, ctx=self._context))