From 0f437a4174fd0ce4edf808f74be75e18b78e867d Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Thu, 2 Jan 2025 14:39:15 -0700 Subject: [PATCH] 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 | 3 --- claripy/annotation.py | 18 +++++++++++++ claripy/ast/base.py | 28 --------------------- claripy/ast/bv.py | 4 +-- claripy/ast/strings.py | 5 +--- claripy/backends/backend_vsa/backend_vsa.py | 15 ++++++++--- claripy/backends/backend_z3.py | 4 +-- claripy/operations.py | 4 --- 8 files changed, 34 insertions(+), 47 deletions(-) diff --git a/claripy/algorithm/simplify.py b/claripy/algorithm/simplify.py index 6e00befac..5aef0ed51 100644 --- a/claripy/algorithm/simplify.py +++ b/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)) diff --git a/claripy/annotation.py b/claripy/annotation.py index 552a67e80..d27f0391e 100644 --- a/claripy/annotation.py +++ b/claripy/annotation.py @@ -126,3 +126,21 @@ def __hash__(self): def __repr__(self): return f"" + + +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 "" diff --git a/claripy/ast/base.py b/claripy/ast/base.py index 50982fa38..b805323ca 100644 --- a/claripy/ast/base.py +++ b/claripy/ast/base.py @@ -112,9 +112,6 @@ class Base: # Caching _cached_encoded_name: bytes | None - # Extra information - _uninitialized: bool - __slots__ = [ "__weakref__", "_cached_encoded_name", @@ -122,7 +119,6 @@ class Base: "_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 diff --git a/claripy/ast/bv.py b/claripy/ast/bv.py index a0bfaf3a1..69bd5585d 100644 --- a/claripy/ast/bv.py +++ b/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): diff --git a/claripy/ast/strings.py b/claripy/ast/strings.py index ab81d8cd9..4ab09f41f 100644 --- a/claripy/ast/strings.py +++ b/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, ) diff --git a/claripy/backends/backend_vsa/backend_vsa.py b/claripy/backends/backend_vsa/backend_vsa.py index 3d905b30e..4084c845b 100644 --- a/claripy/backends/backend_vsa/backend_vsa.py +++ b/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): diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index efe74b6ea..29604125b 100644 --- a/claripy/backends/backend_z3.py +++ b/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"): diff --git a/claripy/operations.py b/claripy/operations.py index bdbc3d1f1..23dc9d0bc 100644 --- a/claripy/operations.py +++ b/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