From 509fc35fcbf1aa0847428fbfb4310ca712f684a0 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 10 Dec 2018 16:55:21 +0100
Subject: [PATCH] Implements array type

---
 mythril/laser/smt/array.py  | 43 +++++++++++++++++++++++++++++++++++++
 mythril/laser/smt/solver.py |  0
 2 files changed, 43 insertions(+)
 create mode 100644 mythril/laser/smt/array.py
 create mode 100644 mythril/laser/smt/solver.py

diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py
new file mode 100644
index 00000000..b906b6e5
--- /dev/null
+++ b/mythril/laser/smt/array.py
@@ -0,0 +1,43 @@
+from mythril.laser.smt.bitvec import BitVec
+import z3
+
+
+class BaseArray:
+    """
+    Base array type, implements basic store and set operations
+    """
+    def __getitem__(self, item: BitVec):
+        """ Gets item from the array, item can be symbolic"""
+        if isinstance(item, slice):
+            raise ValueError("Instance of BaseArray, does not support getitem with slices")
+        return z3.Select(self.raw, item.raw)
+
+    def __setitem__(self, key: BitVec, value: BitVec):
+        """ Sets an item in the array, key can be symbolic"""
+        self.raw = z3.Store(self.raw, key, value)
+
+
+class Array(BaseArray):
+    def __init__(self, name: str, domain: int, value_range: int):
+        """
+        Initializes a symbolic array
+        :param name: Name of the array
+        :param domain: The domain for the array (10 -> all the values that a bv of size 10 could take)
+        :param range: The range for the values in the array (10 -> all the values that a bv of size 10 could take)
+        """
+        self.domain = z3.BitVecSort(domain)
+        self.range = z3.BitVecSort(value_range)
+        self.raw = z3.Array(name, self.domain, self.range)
+
+
+class K(BaseArray):
+    def __init__(self, domain: int, value_range: int, value: int):
+        """
+        Initializes an array with a default value
+        :param domain: The domain for the array (10 -> all the values that a bv of size 10 could take)
+        :param value_range: The range for the values in the array (10 -> all the values that a bv of size 10 could take)
+        :param value: The default value to use for this array
+        """
+        self.domain = z3.BitVecSort(domain)
+        self.value = z3.BitVecVal(value, value_range)
+        self.raw = z3.K(self.domain, self.value)
diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py
new file mode 100644
index 00000000..e69de29b