Skip to content

Commit

Permalink
comments on memory
Browse files Browse the repository at this point in the history 
Signed-off-by: degrigis <[email protected]>
  • Loading branch information
@degrigis
degrigis committed Dec 18, 2023
1 parent c7d800f commit 4b621a4
Show file tree
Hide file tree
Showing 3 changed files with 228 additions and 3 deletions.
81 changes: 78 additions & 3 deletions greed/memory/lambda_constraint.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 []

Expand All @@ -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 []

Expand All @@ -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)
Expand All @@ -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 []

Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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 []

Expand All @@ -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,
Expand All @@ -161,13 +217,27 @@ 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
self.source = source
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 []

Expand All @@ -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,
Expand Down
96 changes: 96 additions & 0 deletions greed/memory/lambda_memory.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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

Expand All @@ -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:
Expand All @@ -119,20 +176,43 @@ 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))

self.root_lambda_constraint = LambdaMemsetConstraint(old_base, start, value, size, self._base,
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))

self.root_lambda_constraint = LambdaMemsetInfiniteConstraint(old_base, start, value, self._base,
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))
Expand All @@ -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))
Expand All @@ -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
Expand Down
Loading

0 comments on commit 4b621a4

Please sign in to comment.