Compare symbolic lists symbolically

crosshair/libimpl/builtinslib.py

@@ -1636,17 +1636,23 @@ def __bool__(self) -> bool:
         return SymbolicBool(self._len() != 0).__bool__()
 
     def __eq__(self, other):
-        if self is other:
-            return True
-        (self_arr, self_len) = self.var
-        if not is_iterable(other):
-            return False
+        with NoTracing():
+            if self is other:
+                return True
+            (self_arr, self_len) = self.var
+            if isinstance(other, SymbolicArrayBasedUniformTuple):
+                return SymbolicBool(
+                    z3.And(self_len == other._len(), self_arr == other._arr())
+                )
+            if not is_iterable(other):
+                return False
         if len(self) != len(other):
             return False
-        for idx, v in enumerate(other):
-            if self[idx] is v:
+        for idx, otherval in enumerate(other):
+            myval = self[idx]
+            if myval is otherval:
                 continue
-            if self[idx] != v:
+            if myval != otherval:
                 return False
         return True
 

crosshair/libimpl/builtinslib_test.py

@@ -12,6 +12,7 @@
     SymbolicArrayBasedUniformTuple,
     SymbolicByteArray,
     SymbolicBytes,
+    SymbolicList,
     SymbolicType,
 )
 from crosshair.libimpl.builtinslib import SymbolicBool
@@ -1496,6 +1497,18 @@ def test_list_copy(space):
         assert copy.copy(lst) is not lst
 
 
+def test_list_copy_compare_without_forking(space):
+    lst = proxy_for_type(List[int], "lst")
+    with ResumedTracing():
+        lst2 = copy.deepcopy(lst)
+    assert type(lst2) is SymbolicList
+    assert lst.inner.var is lst2.inner.var
+    with ResumedTracing():
+        are_same = lst == lst2
+    assert type(are_same) is SymbolicBool
+    assert not space.is_possible(z3.Not(are_same.var))
+
+
 class DictionariesTest(unittest.TestCase):
     def test_dict_basic_fail(self) -> None:
         def f(a: Dict[int, int], k: int, v: int) -> None:

crosshair/simplestructs.py

@@ -8,6 +8,7 @@
 from typing import *
 
 from crosshair.core import CrossHairValue
+from crosshair.tracers import NoTracing
 from crosshair.tracers import ResumedTracing
 from crosshair.util import is_iterable
 from crosshair.util import is_hashable
@@ -521,6 +522,12 @@ def _spawn(self, items: Sequence) -> "ShellMutableSequence":
         # For overriding in subclasses.
         return ShellMutableSequence(items)
 
+    def __eq__(self, other):
+        with NoTracing():
+            if isinstance(other, ShellMutableSequence):
+                other = other.inner
+        return self.inner.__eq__(other)
+
     def __setitem__(self, k, v):
         inner = self.inner
         if hasattr(inner, "__setitem__"):