Convert unininitalized parameter to an annotation (#581)

* Convert unininitalized parameter to an annotation

* Make UninitializedAnnotation non-eliminatable

* Implement __eq__ for UninitializedAnnotation

claripy/algorithm/simplify.py

@@ -36,9 +36,6 @@ def simplify(expr: T) -> T:
         simplification_cache[expr.hash()] = expr
         return expr
 
-    # Copy some parameters (that should really go to the Annotation backend)
-    simplified._uninitialized = expr.uninitialized
-
     # dealing with annotations
     if expr.annotations:
         ast_args = tuple(a for a in expr.args if isinstance(a, Base))

claripy/annotation.py

@@ -126,3 +126,21 @@ def __hash__(self):
 
     def __repr__(self):
         return f"<RegionAnnotation {self.region_id}:{self.offset:#08x}>"
+
+
+class UninitializedAnnotation(Annotation):
+    """
+    Use UninitializedAnnotation to annotate ASTs that are uninitialized.
+    """
+
+    eliminatable = False
+    relocatable = True
+
+    def __hash__(self):
+        return hash("uninitialized")
+
+    def __eq__(self, other):
+        return isinstance(other, UninitializedAnnotation)
+
+    def __repr__(self):
+        return "<UninitializedAnnotation>"

claripy/ast/base.py

@@ -112,17 +112,13 @@ class Base:
     # Caching
     _cached_encoded_name: bytes | None
 
-    # Extra information
-    _uninitialized: bool
-
     __slots__ = [
         "__weakref__",
         "_cached_encoded_name",
         "_errored",
         "_hash",
         "_relocatable_annotations",
         "_uneliminatable_annotations",
-        "_uninitialized",
         "annotations",
         "args",
         "depth",
@@ -143,7 +139,6 @@ def __new__(  # pylint:disable=redefined-builtin
         symbolic: bool | None = None,
         variables: frozenset[str] | None = None,
         errored: set[Backend] | None = None,
-        uninitialized: bool = False,
         annotations: tuple[Annotation, ...] = (),
         skip_child_annotations: bool = False,
         length: int | None = None,
@@ -217,7 +212,6 @@ def __new__(  # pylint:disable=redefined-builtin
                 symbolic=symbolic,
                 length=length,
                 errored=errored,
-                uninitialized=uninitialized,
                 annotations=annotations,
                 encoded_name=encoded_name,
                 depth=depth,
@@ -240,7 +234,6 @@ def make_like(
         annotations: tuple[Annotation, ...] | None = None,
         variables: frozenset[str] | None = None,
         symbolic: bool | None = None,
-        uninitialized: bool = False,
         skip_child_annotations: bool = False,
         length: int | None = None,
     ) -> Self:
@@ -253,7 +246,6 @@ def make_like(
             and annotations
             and variables is None
             and symbolic is None
-            and uninitialized is False
             and skip_child_annotations
             and length is not None
         ):
@@ -281,7 +273,6 @@ def make_like(
                 symbolic=self.symbolic,
                 annotations=annotations,
                 length=length,
-                uninitialized=self._uninitialized,
             )
 
             result._hash = h
@@ -299,8 +290,6 @@ def make_like(
                 annotations = simplified.annotations
         if variables is None and op in all_operations:
             variables = self.variables
-        if uninitialized is None:
-            uninitialized = self._uninitialized
         if symbolic is None and op in all_operations:
             symbolic = self.symbolic
 
@@ -309,7 +298,6 @@ def make_like(
             args if simplified is None else simplified.args,
             annotations=annotations,
             variables=variables,
-            uninitialized=uninitialized,
             symbolic=symbolic,
             skip_child_annotations=skip_child_annotations,
             length=length,
@@ -324,7 +312,6 @@ def __a_init__(
         symbolic: bool | None = None,
         length: int | None = None,
         errored: set[Backend] | None = None,
-        uninitialized: bool = False,
         annotations: tuple[Annotation, ...] | None = None,
         encoded_name: bytes | None = None,
         depth: int | None = None,
@@ -355,8 +342,6 @@ def __a_init__(
 
         self._errored = errored if errored is not None else set()
 
-        self._uninitialized = uninitialized
-
         if len(self.args) == 0:
             raise ClaripyOperationError("AST with no arguments!")
 
@@ -899,16 +884,3 @@ def cardinality(self) -> int:
     @property
     def concrete(self) -> bool:
         return not self.symbolic
-
-    @property
-    def uninitialized(self) -> bool:
-        """
-        Whether this AST comes from an uninitialized dereference or not. It's only used in under-constrained symbolic
-        execution mode.
-
-        :returns:                   True/False/None (unspecified).
-        """
-
-        # TODO: It should definitely be moved to the proposed Annotation backend.
-
-        return self._uninitialized

claripy/ast/bv.py

@@ -291,9 +291,9 @@ def SI(
     )
 
 
-def TSI(bits, name=None, uninitialized=False, explicit_name=None):
+def TSI(bits, name=None, explicit_name=None):
     name = "unnamed" if name is None else name
-    return BVS(name, bits, uninitialized=uninitialized, explicit_name=explicit_name)
+    return BVS(name, bits, explicit_name=explicit_name)
 
 
 def ESI(bits, **kwargs):

claripy/ast/strings.py

@@ -47,13 +47,11 @@ def indexOf(self, pattern, start_idx):
         return StrIndexOf(self, pattern, start_idx)
 
 
-def StringS(name, uninitialized=False, explicit_name=False, **kwargs):
+def StringS(name, explicit_name=False, **kwargs):
     """
     Create a new symbolic string (analogous to z3.String())
 
     :param name:                 The name of the symbolic string (i. e. the name of the variable)
-    :param uninitialized:        Whether this value should be counted as an "uninitialized" value in the course of an
-                                 analysis.
     :param bool explicit_name:   If False, an identifier is appended to the name to ensure uniqueness.
 
     :returns:                    The String object representing the symbolic string
@@ -63,7 +61,6 @@ def StringS(name, uninitialized=False, explicit_name=False, **kwargs):
         "StringS",
         (n,),
         symbolic=True,
-        uninitialized=uninitialized,
         variables=frozenset((n,)),
         **kwargs,
     )

claripy/backends/backend_vsa/backend_vsa.py

@@ -7,7 +7,7 @@
 from functools import reduce
 
 import claripy
-from claripy.annotation import RegionAnnotation, StridedIntervalAnnotation
+from claripy.annotation import RegionAnnotation, StridedIntervalAnnotation, UninitializedAnnotation
 from claripy.ast import BV, Base
 from claripy.backends.backend import Backend
 from claripy.backends.backend_vsa.balancer import Balancer
@@ -270,6 +270,11 @@ def apply_annotation(self, o, a):
                     raise ClaripyVSAError(f"Unsupported offset type {type(offset)}")
                 return vs
 
+            if isinstance(a, UninitializedAnnotation):
+                o2 = o.copy()
+                o2.uninitialized = True
+                return o2
+
         if isinstance(o, ValueSet) and isinstance(a, StridedIntervalAnnotation):
             si = CreateStridedInterval(
                 bits=o.bits,
@@ -282,6 +287,10 @@ def apply_annotation(self, o, a):
             vs._merge_si(a.region_id, a.region_base_addr, si)
             return vs
 
+        if isinstance(o, BoolResult) and isinstance(a, UninitializedAnnotation):
+            # TODO: Do we want to do anything here?
+            return o
+
         raise ValueError(f"Unsupported annotation type {type(a)} for object {type(o)}")
 
     @staticmethod
@@ -462,8 +471,8 @@ def widen(self, ast):
         return ret
 
     @staticmethod
-    def CreateTopStridedInterval(bits, name=None, uninitialized=False):
-        return StridedInterval.top(bits, name, uninitialized=uninitialized)
+    def CreateTopStridedInterval(bits, name=None):
+        return StridedInterval.top(bits, name)
 
     @staticmethod
     def constraint_to_si(expr):

claripy/backends/backend_z3.py

@@ -289,9 +289,7 @@ def __init__(self, reuse_z3_solver=None, ast_cache_size=10000):
 
         self.solve_count = 0
 
-    # XXX this is a HUGE HACK that should be removed whenever uninitialized gets moved to the
-    # "proposed annotation backend" or wherever will prevent it from being part of the object
-    # identity. also whenever the VSA attributes get the fuck out of BVS as well
+    # This is necessary to be able to carry over annotations when round-tripping through Z3
     @property
     def bvs_annotations(self) -> dict[bytes, tuple[Annotation, ...]]:
         if not hasattr(self._tls, "bvs_annotations"):

claripy/operations.py

@@ -73,10 +73,6 @@ def _op(*args):
         if calc_length is not None:
             kwargs["length"] = calc_length(*fixed_args)
 
-        kwargs["uninitialized"] = None
-        if any(a.uninitialized is True for a in args if isinstance(a, claripy.ast.Base)):
-            kwargs["uninitialized"] = True
-
         return return_type(name, fixed_args, **kwargs)
 
     _op.calc_length = calc_length