Always use frozenset for variables

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

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:

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,

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):

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,
     )
 

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)

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)