Revert "add array storage layout"

This reverts commit bfaa7dd.
a16z · Nov 29, 2023 · 7e03f18 · 7e03f18
1 parent c78a755
commit 7e03f18
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 55 deletions.
diff --git a/src/halmos/parser.py b/src/halmos/parser.py
@@ -67,7 +67,7 @@ def mk_arg_parser() -> argparse.ArgumentParser:
 
     parser.add_argument(
         "--storage-layout",
-        choices=["solidity", "generic", "array"],
+        choices=["solidity", "generic"],
         default="solidity",
         help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.",
     )

diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -1266,53 +1266,6 @@ def add_all(cls, args: List) -> BitVecRef:
         return simplify(res)
 
 
-class ArrayStorage(Storage):
-    @classmethod
-    def empty(cls, addr: BitVecRef) -> ArrayRef:
-        return Array(
-            f"storage_{id_str(addr)}_00",
-            BitVecSort256,
-            BitVecSort256,
-        )
-
-    @classmethod
-    def init(cls, ex: Exec, addr: Any) -> None:
-        assert_address(addr)
-        if "storage" not in ex.storage[addr]:
-            ex.storage[addr]["storage"] = cls.empty(addr)
-
-    @classmethod
-    def load(cls, ex: Exec, addr: Any, loc: Word) -> Word:
-        loc = cls.decode(ex, loc)
-        cls.init(ex, addr)
-        if not ex.symbolic:
-            # generate emptyness axiom for each array index, instead of using quantified formula; see init()
-            ex.path.append(Select(cls.empty(addr), loc) == con(0))
-        return ex.select(ex.storage[addr]["storage"], loc, ex.storages)
-
-    @classmethod
-    def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
-        loc = cls.decode(ex, loc)
-        cls.init(ex, addr)
-        new_storage_var = Array(
-            f"storage_{id_str(addr)}_{1+len(ex.storages):>02}",
-            BitVecSort256,
-            BitVecSort256,
-        )
-        new_storage = Store(ex.storage[addr]["storage"], loc, val)
-        ex.path.append(new_storage_var == new_storage)
-        ex.storage[addr]["storage"] = new_storage_var
-        ex.storages[new_storage_var] = new_storage
-
-    @classmethod
-    def decode(cls, ex: Exec, loc: Any) -> Any:
-        if is_bv_value(loc):
-            (preimage, delta) = restore_precomputed_hashes(loc.as_long())
-            if preimage:  # loc == hash(preimage) + delta
-                return ex.sha3_data(con(preimage), 32) + con(delta)
-        return loc
-
-
 SomeStorage = TypeVar("SomeStorage", bound=Storage)
 
 
@@ -1400,13 +1353,8 @@ def __init__(self, options: Dict) -> None:
         self.logs = HalmosLogs()
         self.steps: Steps = {}
 
-        storage_layout = self.options["storage_layout"]
-        if storage_layout == "generic":
-            self.storage_model = GenericStorage
-        elif storage_layout == "array":
-            self.storage_model = ArrayStorage
-        else:
-            self.storage_model = SolidityStorage
+        is_generic = self.options["storage_layout"] == "generic"
+        self.storage_model = GenericStorage if is_generic else SolidityStorage
 
     def div_xy_y(self, w1: Word, w2: Word) -> Word:
         # return the number of bits required to represent the given value. default = 256