Allow simplifications to handle annotations (#548)

claripy/ast/base.py

@@ -246,7 +246,7 @@ def make_like(
         length: int | None = None,
     ) -> Self:
         # Try to simplify the expression again
-        simplified = claripy.simplifications.simplify(op, args) if simplify else None
+        simplified, annotated = claripy.simplifications.simplify(op, args) if simplify else (None, False)
         if simplified is not None:
             op = simplified.op
         if (  # fast path
@@ -294,7 +294,10 @@ def make_like(
         # special case: if self is one of the args, we do not copy annotations over from self since child
         # annotations will be re-processed during AST creation.
         if annotations is None:
-            annotations = self.annotations if not args or not any(self is arg for arg in args) else ()
+            if not annotated:
+                annotations = self.annotations if not args or not any(self is arg for arg in args) else ()
+            else:
+                annotations = simplified.annotations
         if variables is None and op in all_operations:
             variables = self.variables
         if uninitialized is None:

claripy/operations.py

@@ -54,9 +54,12 @@ def _op(*args):
                     raise ClaripyOperationError(msg)
 
         # pylint:disable=too-many-nested-blocks
-        simp = _handle_annotations(claripy.simplifications.simplify(name, fixed_args), args)
+        simp, annotated = claripy.simplifications.simplify(name, fixed_args)
         if simp is not None:
-            return simp
+            if not annotated:
+                simp = _handle_annotations(simp, fixed_args)
+            if simp is not None:
+                return simp
 
         kwargs = {}
         if calc_length is not None:
@@ -73,9 +76,6 @@ def _op(*args):
 
 
 def _handle_annotations(simp, args):
-    if simp is None:
-        return None
-
     # pylint:disable=isinstance-second-argument-not-valid-type
     ast_args = tuple(a for a in args if isinstance(a, claripy.ast.Base))
     preserved_relocatable = frozenset(simp._relocatable_annotations)

claripy/simplifications.py

@@ -5,10 +5,14 @@
 import itertools
 import operator
 from functools import reduce
+from typing import TYPE_CHECKING
 
 import claripy
 from claripy.fp import FSORT_DOUBLE, FSORT_FLOAT
 
+if TYPE_CHECKING:
+    from claripy.ast.base import Base
+
 SIMPLE_OPS = ("Concat", "SignExt", "ZeroExt")
 
 extract_distributable = {
@@ -829,7 +833,7 @@ def extract_simplifier(high, low, val):
 
             # avoid extracting if we need the full value
             if new_high == result.length - 1 and low_loc == 0:
-                return result
+                return result, True
 
             # else extract the part we need
             return result[new_high:low_loc]
@@ -1110,13 +1114,10 @@ def zeroext_comparing_against_simplifier(op, a, b):
     return None
 
 
-_simple_bool_simplifiers = {
+_all_simplifiers = {
     "And": boolean_and_simplifier,
     "Or": boolean_or_simplifier,
     "Not": boolean_not_simplifier,
-}
-
-_all_simplifiers = _simple_bool_simplifiers | {
     "Reverse": bv_reverse_simplifier,
     "Extract": extract_simplifier,
     "Concat": concat_simplifier,
@@ -1141,16 +1142,21 @@ def zeroext_comparing_against_simplifier(op, a, b):
     "__invert__": invert_simplifier,
 }
 
-# the actual functions
+# the actual function
 
 
-def simplify_bool_condition(op, args):
-    if op not in _simple_bool_simplifiers:
-        return None
-    return _simple_bool_simplifiers[op](*args)
-
+def simplify(op, args) -> tuple[Base | None, bool]:
+    """Simplifies the given operation with the given arguments. Returns the
+    simplified result if possible, along with a boolean representing whether
+    annotations were handled by the simplifier.
+    """
 
-def simplify(op, args):
     if op not in _all_simplifiers:
-        return None
-    return _all_simplifiers[op](*args)
+        return None, False
+
+    simplified = _all_simplifiers[op](*args)
+
+    if isinstance(simplified, tuple):
+        return simplified[0], simplified[1]
+
+    return simplified, False