From 4b621a472e02f34b6a3238eaa19492f6af656922 Mon Sep 17 00:00:00 2001 From: degrigis Date: Mon, 18 Dec 2023 11:32:25 -0800 Subject: [PATCH] comments on memory Signed-off-by: degrigis --- greed/memory/lambda_constraint.py | 81 +++++++++++++++++++- greed/memory/lambda_memory.py | 96 ++++++++++++++++++++++++ greed/memory/partial_concrete_storage.py | 54 +++++++++++++ 3 files changed, 228 insertions(+), 3 deletions(-) diff --git a/greed/memory/lambda_constraint.py b/greed/memory/lambda_constraint.py index a24c6bc..5392d67 100644 --- a/greed/memory/lambda_constraint.py +++ b/greed/memory/lambda_constraint.py @@ -31,9 +31,8 @@ def instantiate(self, index): Instantiate the constraint (on read) Args: index: The read index - - Returns: All instantiated constraints (recursively from the LambdaConstraint hierarchy) - + Returns: + All instantiated constraints (recursively from the LambdaConstraint hierarchy) """ return [] @@ -52,12 +51,26 @@ class LambdaMemsetConstraint(LambdaConstraint): Uninstantiated memset constraint """ def __init__(self, array, start, value, size, new_array, parent): + """ + Args: + array: the SMT array on which the memset is applied + start: the start index + value: the value to write + size: how many bytes to write + new_array: the new array (after the memset) + parent: the parent LambdaConstraint + """ super().__init__(array, new_array, parent) self.start = start self.value = value self.size = size def instantiate(self, index): + """ + Instantiate the constraint (on read) + Args: + index: The read index + """ if index in self.following_writes: return [] @@ -70,6 +83,11 @@ def instantiate(self, index): return [instance] + self.parent.instantiate(index) def copy(self, new_state): + """ + Copy the constraint (on state copy) + Args: + new_state: the new state + """ new_parent = None if self.parent is None else self.parent.copy(new_state=new_state) new_lambda_constraint = LambdaMemsetConstraint(array=self.array, start=self.start, value=self.value, size=self.size, new_array=self.new_array, parent=new_parent) @@ -86,11 +104,24 @@ class LambdaMemsetInfiniteConstraint(LambdaConstraint): Uninstantiated memset infinite constraint """ def __init__(self, array, start, value, new_array, parent): + """ + Args: + array: the SMT array on which the memset is applied + start: the start index + value: the value to write + new_array: the new array (after the memset) + parent: the parent LambdaConstraint + """ super().__init__(array, new_array, parent) self.start = start self.value = value def instantiate(self, index): + """ + Instantiate the constraint (on read) + Args: + index: The read index + """ if index in self.following_writes: return [] @@ -103,6 +134,11 @@ def instantiate(self, index): return [instance] + self.parent.instantiate(index) def copy(self, new_state): + """ + Copy the constraint (on state copy) + Args: + new_state: the new state + """ new_parent = None if self.parent is None else self.parent.copy(new_state=new_state) new_lambda_constraint = LambdaMemsetInfiniteConstraint(array=self.array, start=self.start, value=self.value, new_array=self.new_array, parent=new_parent) @@ -119,6 +155,16 @@ class LambdaMemcopyConstraint(LambdaConstraint): Uninstantiated memcopy constraint """ def __init__(self, array, start, source, source_start, size, new_array, parent): + """ + Args: + array: the SMT array src + start: the start index + source: the source array + source_start: the start index of the source array + size: how many bytes to write + new_array: the SMT array target of the memcopy + parent: the parent LambdaConstraint + """ super().__init__(array, new_array, parent) self.start = start # WARNING: memcopy source is of type "memory", CALLER SHOULD TAKE CARE OF .copy()ing IT @@ -127,6 +173,11 @@ def __init__(self, array, start, source, source_start, size, new_array, parent): self.size = size def instantiate(self, index): + """ + Instantiate the constraint (on read) + Args: + index: The read index + """ if index in self.following_writes: return [] @@ -143,6 +194,11 @@ def instantiate(self, index): return [instance] + self.parent.instantiate(index) def copy(self, new_state): + """ + Copy the constraint (on state copy) + Args: + new_state: the new state + """ new_parent = None if self.parent is None else self.parent.copy(new_state=new_state) new_source = self.source.copy(new_state=new_state) new_lambda_constraint = LambdaMemcopyConstraint(array=self.array, start=self.start, source=new_source, @@ -161,6 +217,15 @@ class LambdaMemcopyInfiniteConstraint(LambdaConstraint): Uninstantiated memcopy infinite constraint """ def __init__(self, array, start, source, source_start, new_array, parent): + """ + Args: + array: the SMT array src + start: the start index + source: the source array + source_start: the start index of the source array + new_array: the SMT array target of the memcopy + parent: the parent LambdaConstraint + """ super().__init__(array, new_array, parent) self.start = start # WARNING: memcopy source is of type "memory", CALLER SHOULD TAKE CARE OF .copy()ing IT @@ -168,6 +233,11 @@ def __init__(self, array, start, source, source_start, new_array, parent): self.source_start = source_start def instantiate(self, index): + """ + Instantiate the constraint (on read) + Args: + index: The read index + """ if index in self.following_writes: return [] @@ -183,6 +253,11 @@ def instantiate(self, index): return [instance] + self.parent.instantiate(index) def copy(self, new_state): + """ + Copy the constraint (on state copy) + Args: + new_state: the new state + """ new_parent = None if self.parent is None else self.parent.copy(new_state=new_state) new_source = self.source.copy(new_state=new_state) new_lambda_constraint = LambdaMemcopyInfiniteConstraint(array=self.array, start=self.start, source=new_source, diff --git a/greed/memory/lambda_memory.py b/greed/memory/lambda_memory.py index 508f45f..9bca17a 100644 --- a/greed/memory/lambda_memory.py +++ b/greed/memory/lambda_memory.py @@ -47,6 +47,15 @@ class LambdaMemory: uuid_generator = UUIDGenerator() def __init__(self, tag=None, value_sort=None, default=None, state=None, partial_init=False): + """ + Initialize the LambdaMemory. + Args: + tag: the tag of the memory, this is a unique identifier. + value_sort: the sort type of the values in the memory (e.g., BVSort(8)) + default: the default value of the memory when no writes have been performed + state: the SimState to which this memory belongs + partial_init: if True, do not initialize the memory + """ if partial_init: return assert tag is not None and value_sort is not None, "Invalid LambdaMemory initialization" @@ -68,21 +77,49 @@ def __init__(self, tag=None, value_sort=None, default=None, state=None, partial_ self.read_count = 0 def add_constraint(self, formula): + """ + Add a constraint to the memory. + Args: + formula: the constraint to add + """ self.state.solver.add_memory_constraints(formula) def add_constraints(self, formulas): + """ + Add constraints to the memory. + Args: + formulas: the constraints to add + """ for formula in formulas: self.add_constraint(formula) @property def layer_level(self): + """ + How many layers of lambda constraints are there? + Returns: + the number of layers + """ return self.root_lambda_constraint.depth - 1 @property def constraints(self): + """ + Get the constraints of the memory. + Returns: + the constraints + """ return self._constraints def __getitem__(self, index): + """ + Read from the memory at a specific index. + This will instantiate the lambda constraints at the index for the current layer. + Args: + index: the index to read from + Returns: + an Array_Select formula representing the read to that index + """ assert not isinstance(index, slice), "slice memory read not implemented" self.read_count += 1 @@ -93,11 +130,31 @@ def __getitem__(self, index): return Array_Select(self._base, index) def __setitem__(self, index, v): + """ + Write to the memory at a specific index. + This will register a write in the "following_writes" (caching). + Args: + index: the index to write to + v: the value to write + Returns: + an Array_Store formula representing the write to that index + """ self.write_count += 1 self.root_lambda_constraint.following_writes[index] = v self._base = Array_Store(self._base, index, v) def readn(self, index, n): + """ + Read n bytes from the memory at a specific index. + Args: + index: the index to read from + n: the number of bytes to read + Returns: + a BV_Concat formula representing the read + Raises: + AssertionError: if the length is symbolic + AssertionError: if the length is 0 + """ assert is_concrete(n), "readn with symbolic length not implemented" assert bv_unsigned_value(n) != 0, "invalid readn with length=0" if bv_unsigned_value(n) == 1: @@ -119,6 +176,13 @@ def readn(self, index, n): return res def memset(self, start, value, size): + """ + Perform a memset operation + Args: + start: the start index + value: the value to write + size: the number of bytes to write + """ old_base = self._base self._base = Array(f"{self.tag}_{LambdaMemory.uuid_generator.next()}_{self.layer_level}", BVSort(256), BVSort(8)) @@ -126,6 +190,12 @@ def memset(self, start, value, size): parent=self.root_lambda_constraint) def memsetinfinite(self, start, value): + """ + Perform a memsetinfinite operation + Args: + start: the start index + value: the value to write + """ old_base = self._base self._base = Array(f"{self.tag}_{LambdaMemory.uuid_generator.next()}_{self.layer_level}", BVSort(256), BVSort(8)) @@ -133,6 +203,16 @@ def memsetinfinite(self, start, value): parent=self.root_lambda_constraint) def memcopy(self, start, source, source_start, size): + """ + Perform a memcopy operation + Args: + start: the start index + source: the source memory + source_start: the start index of the source memory + size: the number of bytes to copy + Raises: + AssertionError: if the source memory is different from the current memory + """ assert source != self, "ERROR: memcopy source was not copied" old_base = self._base self._base = Array(f"{self.tag}_{LambdaMemory.uuid_generator.next()}_{self.layer_level}", BVSort(256), BVSort(8)) @@ -141,6 +221,15 @@ def memcopy(self, start, source, source_start, size): parent=self.root_lambda_constraint) def memcopyinfinite(self, start, source, source_start): + """ + Perform a memcopyinfinite operation + Args: + start: the start index + source: the source memory + source_start: the start index of the source memory + Raises: + AssertionError: if the source memory is different from the current memory + """ assert source != self, "ERROR: memcopy source was not copied" old_base = self._base self._base = Array(f"{self.tag}_{LambdaMemory.uuid_generator.next()}_{self.layer_level}", BVSort(256), BVSort(8)) @@ -149,6 +238,13 @@ def memcopyinfinite(self, start, source, source_start): parent=self.root_lambda_constraint) def copy(self, new_state): + """ + Perform a deep copy of the memory. + Args: + new_state: the state to which the new memory belongs + Returns: + A deep copy of the LambdaMemory + """ new_memory = LambdaMemory(partial_init=True) new_memory.tag = self.tag new_memory._base = self._base diff --git a/greed/memory/partial_concrete_storage.py b/greed/memory/partial_concrete_storage.py index a7836b0..572ccb1 100644 --- a/greed/memory/partial_concrete_storage.py +++ b/greed/memory/partial_concrete_storage.py @@ -12,10 +12,30 @@ class PartialConcreteStorage: + """ + This class represents a partial concrete storage. + When using the partial concrete storage, reads from the contract storage (SLOADs) are + initialized with the concrete value on-chain (at the given block number). + + To use this, we need a web3 connection to the blockchain, the address of the contract and the block number. + """ uuid_generator = UUIDGenerator() def __init__(self, tag=None, value_sort=None, state=None, partial_init=False): + """ + Initialize the partial concrete storage. + Args: + tag: The unique identifier of the storage + value_sort: The sort of the values stored in the storage + state: The SimState associated with this storage + partial_init: If true, the storage is partially initialized (used for copy) + Raises: + GreedException: If the partial concrete storage is not initialized with the contract address and block number + AssertionError: If the partial concrete storage is not initialized with the tag and value sort + AssertionError: If w3 is not connected + """ + if partial_init: return assert tag is not None and value_sort is not None, "Invalid PartialConcreteStorage initialization" @@ -50,9 +70,19 @@ def __init__(self, tag=None, value_sort=None, state=None, partial_init=False): self.concrete_cache = dict() def add_constraint(self, formula): + """ + Add a constraint to the storage. + Args: + formula: The constraint to add + """ self.state.solver.add_memory_constraints(formula) def add_constraints(self, formulas): + """ + Add a list of constraints to the storage. + Args: + formulas: The list of constraints to add + """ for formula in formulas: self.add_constraint(formula) @@ -65,6 +95,20 @@ def constraints(self): return self._constraints def __getitem__(self, index): + """ + Read from the storage at the given index (SLOAD). + IF the index is not concrete, this instantiate the lambda constraints and return an Array_Select. + Otherwise, it reads the concrete value from the concrete cache + (the concrete value is initialized with the value on-chain at the given block number). + + Args: + index: The index to read from + Returns: + The concreate value read from the storage (if the index is concrete) + an Array_Select (if the index is symbolic) + Raises: + AssertionError: If the index is a slice + """ assert not isinstance(index, slice), "slice memory read not implemented" self.read_count += 1 @@ -92,6 +136,11 @@ def __getitem__(self, index): return Array_Select(self._base, index) def __setitem__(self, index, v): + """ + Perform a write to the storage at the given index (SSTORE). + IF the index is not concrete, then return an Array_Store. + Otherwise just overwrite the concrete value in the concrete cache. + """ self.write_count += 1 if is_concrete(index): @@ -103,6 +152,11 @@ def __setitem__(self, index, v): self._base = Array_Store(self._base, index, v) def copy(self, new_state): + """ + Copy the partial concrete storage. + Args: + new_state: The new SimState associated with the new storage + """ new_memory = PartialConcreteStorage(partial_init=True) new_memory.tag = self.tag new_memory._base = self._base