Simplify ValueSet constructor logic (#605)

* Simplify ValueSet constructor logic

* Fix lint and format errors

Author: twizmwazin

claripy/ast/bv.py

@@ -1,7 +1,6 @@
 from __future__ import annotations
 
 import logging
-import numbers
 import weakref
 from contextlib import suppress
 
@@ -300,44 +299,12 @@ def ESI(bits, **kwargs):
     return BVV(None, bits, **kwargs)
 
 
-def ValueSet(bits, region=None, region_base_addr=None, value=None, name=None, val=None):
-    # Backward compatibility
-    if value is None and val is not None:
-        value = val
-    if region_base_addr is None:
-        region_base_addr = 0
-
-    v = region_base_addr + value
-    if isinstance(v, claripy.ast.Base):
-        v = claripy.simplify(v)
-
-    # Backward compatibility
-    if isinstance(v, numbers.Number):
-        min_v, max_v = v, v
-        stride = 0
-    elif isinstance(v, claripy.ast.Base):
-        si_anno = v.get_annotation(claripy.annotation.StridedIntervalAnnotation)
-        if si_anno is not None:
-            min_v = si_anno.lower_bound
-            max_v = si_anno.upper_bound
-            stride = si_anno.stride
-        elif v.op == "BVV":
-            min_v = v.args[0]
-            max_v = v.args[0]
-            stride = 0
-        else:
-            raise ClaripyValueError(f"ValueSet() does not take `value` ast with op {v.op}")
-    else:
-        raise ClaripyValueError(f"ValueSet() does not take `value` of type {type(value)}")
-
-    if name is None:
-        name = "ValueSet"
-    bvs = BVS(name, bits).annotate(
-        claripy.annotation.StridedIntervalAnnotation(stride, region_base_addr + min_v, region_base_addr + max_v)
-    )
-
+def ValueSet(bits: int, region: str, region_base_addr: int, value: BV | int):
+    if isinstance(value, int):
+        value = BVV(value, bits)
+    value = value + region_base_addr
     # Annotate the bvs and return the new AST
-    return bvs.annotate(claripy.annotation.RegionAnnotation(region, region_base_addr, value))
+    return value.annotate(claripy.annotation.RegionAnnotation(region, region_base_addr, value))
 
 
 VS = ValueSet

tests/test_vsa.py

@@ -626,8 +626,8 @@ def test_extraction_from_reversed_value(self):
 
     def test_value_set_operations(self):
         # ValueSet operations
-        vs_1 = VS(bits=32, value=0)
-        vs_1 = vs_1.intersection(VS(bits=32, value=1))
+        vs_1 = VS(32, "global", 0, 0)
+        vs_1 = vs_1.intersection(VS(32, "global", 0, 1))
         assert vsa_model(vs_1).is_empty
 
         # Test merging two addresses
@@ -640,8 +640,8 @@ def test_value_set_operations(self):
         )
         assert len(vsa_model(vs_1)) == 32
 
-        vs_1 = VS(name="boo", bits=32, value=0).intersection(VS(name="makeitempty", bits=32, value=1))
-        vs_2 = VS(name="foo", bits=32, value=0).intersection(VS(name="makeitempty", bits=32, value=1))
+        vs_1 = VS(32, "global", 0, 0).intersection(VS(32, "global", 0, 1))
+        vs_2 = VS(32, "global", 0, 0).intersection(VS(32, "global", 0, 1))
         assert self.is_equal(vs_1, vs_1)
         assert self.is_equal(vs_2, vs_2)
         vs_1 = vs_1.union(VS(32, "global", 0, claripy.SI(bits=32, stride=0, lower_bound=10, upper_bound=10)))
@@ -654,8 +654,8 @@ def test_value_set_operations(self):
 
     def test_value_set_subtraction(self):
         # Subtraction of two pointers yields a concrete value
-        vs_1 = claripy.ValueSet(name="foo", region="global", bits=32, value=0x400010)
-        vs_2 = claripy.ValueSet(name="bar", region="global", bits=32, value=0x400000)
+        vs_1 = claripy.ValueSet(32, "global", 0, 0x400010)
+        vs_2 = claripy.ValueSet(32, "global", 0, 0x400000)
         si = vs_1 - vs_2
         # assert isinstance(vsa_model(si), claripy.SI)
         assert type(vsa_model(si)) is StridedInterval
@@ -700,31 +700,29 @@ def test_if_proxy_identical(self):
 
     def test_if_proxy_and_operations(self):
         # if_1 = And(VS_2, IfProxy(si == 0, 0, 1))
-        vs_2 = claripy.ValueSet(region="global", bits=32, value=0xFA7B00B)
+        vs_2 = claripy.ValueSet(32, "global", 0, 0xFA7B00B)
         si = claripy.SI(bits=32, stride=1, lower_bound=0, upper_bound=1)
         if_1 = vs_2 & claripy.If(
             si == 0,
             claripy.SI(bits=32, stride=0, lower_bound=0, upper_bound=0),
             claripy.SI(bits=32, stride=0, lower_bound=0xFFFFFFFF, upper_bound=0xFFFFFFFF),
         )
         assert claripy.backends.vsa.is_true(
-            vsa_model(claripy.excavate_ite(if_1).args[1])
-            == vsa_model(claripy.ValueSet(region="global", bits=32, value=0))
+            vsa_model(claripy.excavate_ite(if_1).args[1]) == vsa_model(claripy.ValueSet(32, "global", 0, 0))
         )
         assert claripy.backends.vsa.is_true(vsa_model(claripy.excavate_ite(if_1).args[2]) == vsa_model(vs_2))
 
     def test_if_proxy_or_operations(self):
         # if_2 = And(VS_3, IfProxy(si != 0, 0, 1))
-        vs_3 = claripy.ValueSet(region="global", bits=32, value=0xDEADCA7)
+        vs_3 = claripy.ValueSet(32, "global", 0, 0xDEADCA7)
         si = claripy.SI(bits=32, stride=1, lower_bound=0, upper_bound=1)
         if_2 = vs_3 & claripy.If(
             si != 0,
             claripy.SI(bits=32, stride=0, lower_bound=0, upper_bound=0),
             claripy.SI(bits=32, stride=0, lower_bound=0xFFFFFFFF, upper_bound=0xFFFFFFFF),
         )
         assert claripy.backends.vsa.is_true(
-            vsa_model(claripy.excavate_ite(if_2).args[1])
-            == vsa_model(claripy.ValueSet(region="global", bits=32, value=0))
+            vsa_model(claripy.excavate_ite(if_2).args[1]) == vsa_model(claripy.ValueSet(32, "global", 0, 0))
         )
         assert claripy.backends.vsa.is_true(vsa_model(claripy.excavate_ite(if_2).args[2]) == vsa_model(vs_3))
 
@@ -1072,7 +1070,7 @@ def test_solution_on_strided_interval(self):
 
     def test_solution_on_valueset(self):
         # Testing solution method with ValueSet (VS) objects
-        vs = claripy.ValueSet(region="global", bits=32, value=0xDEADCA7)
+        vs = claripy.ValueSet(32, "global", 0, 0xDEADCA7)
         assert self.solver.solution(vs, 0xDEADCA7)
         assert not self.solver.solution(vs, 0xDEADBEEF)
 
@@ -1081,8 +1079,8 @@ def test_solution_on_combined_valueset(self):
         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 = claripy.ValueSet(bits=si.size(), region="foo", value=si)
-        vs2 = claripy.ValueSet(bits=si2.size(), region="foo", value=si2)
+        vs = claripy.ValueSet(si.size(), "foo", 0, si)
+        vs2 = claripy.ValueSet(si2.size(), "foo", 0, si2)
         vs = vs.union(vs2)
 
         assert self.solver.solution(vs, 3)