From 073c05c9126ebcf2a0edc73736454a95f5f4c7d8 Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Tue, 17 Sep 2024 10:46:52 -0700 Subject: [PATCH] Always use frozenset for variables --- claripy/ast/base.py | 18 +++++------------- claripy/ast/bool.py | 2 +- claripy/ast/bv.py | 2 +- claripy/ast/fp.py | 2 +- claripy/ast/strings.py | 2 +- claripy/backends/backend_z3.py | 8 +++++--- tests/test_expression.py | 4 ++-- 7 files changed, 16 insertions(+), 22 deletions(-) diff --git a/claripy/ast/base.py b/claripy/ast/base.py index c72c3c9b2..21514d0a4 100644 --- a/claripy/ast/base.py +++ b/claripy/ast/base.py @@ -218,10 +218,6 @@ def __new__( # pylint:disable=redefined-builtin errored = set(chain.from_iterable(a._errored for a in b_args)) arg_max_depth = max((a.depth for a in b_args), default=0) - # TODO: This shouldn't be nessessary - if not isinstance(variables, frozenset): - variables = frozenset(variables) - if add_variables: variables = frozenset.union(variables, add_variables) @@ -249,7 +245,7 @@ def __new__( # pylint:disable=redefined-builtin self.__a_init__( op, a_args, - variables=variables, + variables, symbolic=symbolic, length=length, errored=errored, @@ -310,10 +306,10 @@ def make_like( result.__a_init__( op, args, + self.variables, depth=self.depth, uneliminatable_annotations=uneliminatable_annotations, relocatable_annotations=relocatable_annotations, - variables=self.variables, symbolic=self.symbolic, annotations=annotations, length=length, @@ -353,7 +349,7 @@ def __a_init__( self, op: str, args: tuple[ArgType, ...], - variables: Iterable[str] | None = None, + variables: frozenset[str], symbolic: bool | None = None, length: int | None = None, simplified: SimplificationLevel = SimplificationLevel.UNSIMPLIFIED, @@ -377,7 +373,7 @@ def __a_init__( self.op = op self.args = args if type(args) is tuple else tuple(args) self.length = length - self.variables = frozenset(variables) if type(variables) is not frozenset else variables + self.variables = variables self.symbolic = symbolic self.annotations: tuple[Annotation] = annotations self._uneliminatable_annotations = uneliminatable_annotations @@ -565,7 +561,7 @@ def _rename(self, new_name: str) -> Self: if self.op not in {"BVS", "BoolS", "FPS"}: raise ClaripyOperationError("rename is only supported on leaf nodes") new_args = (new_name,) + self.args[1:] - return self.make_like(self.op, new_args, length=self.length, variables={new_name}) + return self.make_like(self.op, new_args, length=self.length, variables=frozenset((new_name,))) # # Annotations @@ -889,12 +885,8 @@ def swap_args(self, new_args: tuple[ArgType, ...], new_length: int | None = None if len(self.args) == len(new_args) and all(a is b for a, b in zip(self.args, new_args, strict=False)): return self - # symbolic = any(a.symbolic for a in new_args if isinstance(a, Base)) - # variables = frozenset.union(frozenset(), *(a.variables for a in new_args if isinstance(a, Base))) length = self.length if new_length is None else new_length return self.make_like(self.op, new_args, length=length, **kwargs) - # if a.op != self.op or a.symbolic != self.symbolic or a.variables != self.variables: - # raise ClaripyOperationError("major bug in swap_args()") # # Other helper functions diff --git a/claripy/ast/bool.py b/claripy/ast/bool.py index 5a99d5941..1298a3d9f 100644 --- a/claripy/ast/bool.py +++ b/claripy/ast/bool.py @@ -64,7 +64,7 @@ def BoolS(name, explicit_name=None) -> Bool: :return: A Bool object representing this symbol. """ n = _make_name(name, -1, False if explicit_name is None else explicit_name) - return Bool("BoolS", (n,), variables={n}, symbolic=True) + return Bool("BoolS", (n,), variables=frozenset((n,)), symbolic=True) def BoolV(val) -> Bool: diff --git a/claripy/ast/bv.py b/claripy/ast/bv.py index c28698b00..90668a6b3 100644 --- a/claripy/ast/bv.py +++ b/claripy/ast/bv.py @@ -263,7 +263,7 @@ def BVS( return BV( "BVS", (n, min, max, stride, uninitialized, discrete_set, discrete_set_max_card), - variables={n}, + variables=frozenset((n,)), length=size, symbolic=True, uninitialized=uninitialized, diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index 82b5219a3..a32540ad1 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -93,7 +93,7 @@ def FPS(name, sort, explicit_name=None): """ n = _make_name(name, sort.length, False if explicit_name is None else explicit_name, prefix="FP_") - return FP("FPS", (n, sort), variables={n}, symbolic=True, length=sort.length) + return FP("FPS", (n, sort), variables=frozenset((n,)), symbolic=True, length=sort.length) def FPV(value, sort): diff --git a/claripy/ast/strings.py b/claripy/ast/strings.py index bc65fa2a6..c70a4e3ba 100644 --- a/claripy/ast/strings.py +++ b/claripy/ast/strings.py @@ -141,7 +141,7 @@ def StringS(name, size, uninitialized=False, explicit_name=False, **kwargs): length=8 * size, symbolic=True, uninitialized=uninitialized, - variables={n}, + variables=frozenset((n,)), **kwargs, ) diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index e02544d78..8ff8f2d87 100644 --- a/claripy/backends/backend_z3.py +++ b/claripy/backends/backend_z3.py @@ -493,18 +493,20 @@ def _abstract_internal(self, ctx, ast, split_on=None): "BVS", ast_args, length=bv_size, - variables={symbol_str}, + variables=frozenset((symbol_str,)), symbolic=True, encoded_name=symbol_name, annotations=annots, ) if symbol_ty == z3.Z3_BOOL_SORT: - return Bool("BoolS", (symbol_str,), variables={symbol_str}, symbolic=True) + return Bool("BoolS", (symbol_str,), variables=frozenset((symbol_str,)), symbolic=True) if symbol_ty == z3.Z3_FLOATING_POINT_SORT: ebits = z3.Z3_fpa_get_ebits(ctx, z3_sort) sbits = z3.Z3_fpa_get_sbits(ctx, z3_sort) sort = FSort.from_params(ebits, sbits) - return FP("FPS", (symbol_str, sort), variables={symbol_str}, symbolic=True, length=sort.length) + return FP( + "FPS", (symbol_str, sort), variables=frozenset((symbol_str,)), symbolic=True, length=sort.length + ) if z3.Z3_is_string_sort(ctx, z3_sort): raise BackendError("Z3 backend does not support string symbols") raise BackendError("Unknown z3 term type %d...?" % symbol_ty) diff --git a/tests/test_expression.py b/tests/test_expression.py index aacaea0e3..42d9d0427 100644 --- a/tests/test_expression.py +++ b/tests/test_expression.py @@ -123,8 +123,8 @@ def test_expression(self): self.assertNotEqual(hash(old_formula), hash(ooo_formula)) self.assertNotEqual(hash(new_formula), hash(ooo_formula)) - self.assertEqual(old_formula.variables, {"old"}) - self.assertEqual(new_formula.variables, {"new"}) + self.assertEqual(old_formula.variables, frozenset(("old",))) + self.assertEqual(new_formula.variables, frozenset(("new",))) self.assertEqual(ooo_formula.variables, ooo.variables) self.assertTrue(old_formula.symbolic)