Repository: angr/claripy

Issue:
Base.replace cannot work on Bool
### Description

```python
import claripy
b = claripy.BoolS("b")
expr = claripy.If(b, claripy.BVV(2, 32), claripy.BVV(3, 32))
new_expr = expr.replace(b, claripy.BoolV(True))
```
Error:
```
    @staticmethod
     41     def _check_replaceability(old, new):
---> 42         if old.size() != new.size():
     43             raise ClaripyOperationError('replacements must have matching sizes')

AttributeError: size
```

Current workaround:
```python
new_expr = expr.replace_dict({b.cache_key: claripy.BoolV(True)})
```


### Steps to reproduce the bug

_No response_

### Environment

_No response_

### Additional context

_No response_

Discussion:

Patch:
diff --git a/claripy/ast/base.py b/claripy/ast/base.py
index 36a1ef3a..f16ddc57 100644
--- a/claripy/ast/base.py
+++ b/claripy/ast/base.py
@@ -525,12 +525,6 @@ class Base:
     # Collapsing and simplification
     #
 
-    # def _models_for(self, backend):
-    #    for a in self.args:
-    #        backend.convert_expr(a)
-    #        else:
-    #            yield backend.convert(a)
-
     def make_like(
         self: T,
         op: str,
@@ -1254,7 +1248,7 @@ class Base:
 
     def _first_backend(self, what):
         for b in backends._all_backends:
-            if b in self._errored or b.is_smt_backend:
+            if b in self._errored:
                 continue
 
             try:
@@ -1265,17 +1259,10 @@ class Base:
 
     @property
     def concrete_value(self):
-        return self._model_concrete.value
-
-    # yan I'm gonna kill you
-
-    @property
-    def cv(self):
-        return self._model_concrete.value
-
-    @property
-    def v(self):
-        return self._model_concrete.value
+        try:
+            return backends.concrete.convert(self).value
+        except BackendError:
+            return self
 
     @property
     def singlevalued(self) -> bool:
@@ -1332,23 +1319,6 @@ class Base:
         """
         return self
 
-    #
-    # Backwards compatibility crap
-    #
-
-    def __getattr__(self, a):
-        if not a.startswith("_model_"):
-            raise AttributeError(a)
-
-        model_name = a[7:]
-        if not hasattr(backends, model_name):
-            raise AttributeError(a)
-
-        try:
-            return getattr(backends, model_name).convert(self)
-        except BackendError:
-            return self
-
 
 def simplify(e: T) -> T:
     if isinstance(e, Base) and e.op in operations.leaf_operations:
diff --git a/claripy/ast/bool.py b/claripy/ast/bool.py
index ab6f5e5e..73351eea 100644
--- a/claripy/ast/bool.py
+++ b/claripy/ast/bool.py
@@ -46,6 +46,10 @@ class Bool(Base):
         """
         return is_false(self)
 
+    def size(self):
+        """Returns the size of the AST in bits. A boolean is 1 bit."""
+        return 1
+
 
 def BoolS(name, explicit_name=None) -> Bool:
     """
diff --git a/claripy/vsa/strided_interval.py b/claripy/vsa/strided_interval.py
index 5802e2d1..59b67d71 100644
--- a/claripy/vsa/strided_interval.py
+++ b/claripy/vsa/strided_interval.py
@@ -7,6 +7,7 @@ import math
 import numbers
 from functools import reduce
 
+import claripy
 from claripy.ast.base import Base
 from claripy.backend_object import BackendObject
 from claripy.bv import BVV
@@ -3567,7 +3568,7 @@ def CreateStridedInterval(
     """
     if to_conv is not None:
         if isinstance(to_conv, Base):
-            to_conv = to_conv._model_vsa
+            to_conv = claripy.backends.vsa.convert(to_conv)
         if isinstance(to_conv, StridedInterval):
             # No conversion will be done
             return to_conv
diff --git a/claripy/vsa/valueset.py b/claripy/vsa/valueset.py
index a6660fa1..fd971ed0 100644
--- a/claripy/vsa/valueset.py
+++ b/claripy/vsa/valueset.py
@@ -5,6 +5,7 @@ import functools
 import itertools
 import numbers
 
+import claripy
 from claripy.annotation import Annotation
 from claripy.ast.base import Base
 from claripy.backend_object import BackendObject
@@ -63,9 +64,9 @@ class RegionAnnotation(Annotation):
 
         # Do necessary conversion here
         if isinstance(self.region_base_addr, Base):
-            self.region_base_addr = self.region_base_addr._model_vsa
+            self.region_base_addr = claripy.backends.vsa.convert(self.region_base_addr)
         if isinstance(self.offset, Base):
-            self.offset = self.offset._model_vsa
+            self.offset = claripy.backends.vsa.convert(self.offset)
 
     @property
     def eliminatable(self):


Test patch:
diff --git a/tests/test_balancer.py b/tests/test_balancer.py
index 00f1347e..8c18d7a8 100644
--- a/tests/test_balancer.py
+++ b/tests/test_balancer.py
@@ -71,7 +71,7 @@ class TestBalancer(unittest.TestCase):
         s, r = claripy.balancer.Balancer(claripy.backends.vsa, x + 1 <= claripy.BVV(39, 32)).compat_ret
         assert s
         assert r[0][0] is x
-        all_vals = r[0][1]._model_vsa.eval(1000)
+        all_vals = claripy.backends.vsa.convert(r[0][1]).eval(1000)
         assert len(all_vals)
         assert min(all_vals) == 0
         assert max(all_vals) == 4294967295
@@ -90,7 +90,7 @@ class TestBalancer(unittest.TestCase):
         assert s
         assert r[0][0] is w
         assert claripy.backends.vsa.min(r[0][1]) == 0
-        all_vals = r[0][1]._model_vsa.eval(1000)
+        all_vals = claripy.backends.vsa.convert(r[0][1]).eval(1000)
         assert set(all_vals) == {4294967295, 0, 1}
 
     def test_overflow(self):
diff --git a/tests/test_expression.py b/tests/test_expression.py
index 3488f938..af37e6a0 100644
--- a/tests/test_expression.py
+++ b/tests/test_expression.py
@@ -563,6 +563,15 @@ class TestExpression(unittest.TestCase):
         except claripy.ClaripyOperationError:
             pass
 
+    def test_bool_replace_in_ite(self):
+        b = claripy.BoolS("b")
+        expr = claripy.If(b, claripy.BVV(2, 32), claripy.BVV(3, 32))
+        new_expr = expr.replace(b, claripy.BoolV(True))
+
+        # Replace calls make_like which will simplify the expression. As a
+        # result, the new expression will be a BVV.
+        assert new_expr.op == "BVV" and new_expr.args == (2, 32)
+
 
 if __name__ == "__main__":
     unittest.main()
diff --git a/tests/test_simplify.py b/tests/test_simplify.py
index eba030e6..619b57df 100644
--- a/tests/test_simplify.py
+++ b/tests/test_simplify.py
@@ -60,7 +60,7 @@ class TestSimplify(unittest.TestCase):
         extend_ = claripy.BVS("extend", 32, uninitialized=True)
         a_ext = extend_.concat(a)
         expr = ((a_ext << 3) | (claripy.LShR(a_ext, 61))) & 0x7FFFFFFF8
-        model_vsa = expr._model_vsa
+        model_vsa = claripy.backends.vsa.convert(expr)
         assert model_vsa.lower_bound == 8
         assert model_vsa.upper_bound == 0x60
         assert model_vsa.cardinality == 12
diff --git a/tests/test_vsa.py b/tests/test_vsa.py
index 18012f63..b29e0c7e 100644
--- a/tests/test_vsa.py
+++ b/tests/test_vsa.py
@@ -69,16 +69,16 @@ class TestVSA(unittest.TestCase):  # pylint: disable=no-member,function-redefine
         assert claripy.backends.vsa.max(reversed_b) == 0xFF000000
 
         a_concat_b = claripy.Concat(a, b)
-        assert a_concat_b._model_vsa._reversed is False
+        assert claripy.backends.vsa.convert(a_concat_b)._reversed is False
 
         ra_concat_b = claripy.Concat(reversed_a, b)
-        assert ra_concat_b._model_vsa._reversed is False
+        assert claripy.backends.vsa.convert(ra_concat_b)._reversed is False
 
         a_concat_rb = claripy.Concat(a, reversed_b)
-        assert a_concat_rb._model_vsa._reversed is False
+        assert claripy.backends.vsa.convert(a_concat_rb)._reversed is False
 
         ra_concat_rb = claripy.Concat(reversed_a, reversed_b)
-        assert ra_concat_rb._model_vsa._reversed is False
+        assert claripy.backends.vsa.convert(ra_concat_rb)._reversed is False
 
     def test_simple_cardinality(self):
         x = claripy.BVS("x", 32, 0xA, 0x14, 0xA)
@@ -523,7 +523,7 @@ class TestVSA(unittest.TestCase):  # pylint: disable=no-member,function-redefine
 
         # Comparison between claripy.SI and BVV
         si = claripy.SI(bits=32, stride=1, lower_bound=-0x7F, upper_bound=0x7F)
-        si._model_vsa.uninitialized = True
+        claripy.backends.vsa.convert(si).uninitialized = True
         bvv = BVV(0x30, 32)
         comp = si < bvv
         assert vsa_model(comp).identical(MaybeResult())
@@ -1028,9 +1028,9 @@ class TestVSA(unittest.TestCase):  # pylint: disable=no-member,function-redefine
         si = claripy.SI(bits=32, stride=0, lower_bound=3, upper_bound=3)
         si2 = claripy.SI(bits=32, stride=10, lower_bound=32, upper_bound=320)
 
-        vs = VS(bits=si.size(), region="foo", val=si._model_vsa)
+        vs = VS(bits=si.size(), region="foo", val=claripy.backends.vsa.convert(si))
         # vs = vs.annotate(RegionAnnotation('foo', 0, si2))
-        vs2 = VS(bits=si2.size(), region="foo", val=si2._model_vsa)
+        vs2 = VS(bits=si2.size(), region="foo", val=claripy.backends.vsa.convert(si2))
         vs = vs.union(vs2)
 
         assert s.solution(vs, 3)
@@ -1088,10 +1088,10 @@ class TestVSA(unittest.TestCase):  # pylint: disable=no-member,function-redefine
         r2 = x.intersection(y.reversed).reversed
         r3 = x.reversed.intersection(y.reversed).reversed
 
-        assert r0._model_vsa.max == 1337
-        assert r1._model_vsa.max == 1337
-        assert r2._model_vsa.max == 1337
-        assert r3._model_vsa.max == 1337
+        assert claripy.backends.vsa.convert(r0).max == 1337
+        assert claripy.backends.vsa.convert(r1).max == 1337
+        assert claripy.backends.vsa.convert(r2).max == 1337
+        assert claripy.backends.vsa.convert(r3).max == 1337
 
         # See claripy issue #95 for details.
         si0 = StridedInterval(name="a", bits=32, stride=0, lower_bound=0xFFFF0000, upper_bound=0xFFFF0000)