module greed.memory.lambda_memory

class LambdaMemory

Implementation of an instantiation-based lambda memory

Extending the Theory of Arrays: memset, memcpy, and Beyond (https://llbmc.org/files/papers/VSTTE13.pdf) see 5.3 "Instantiating Quantifiers"

This is a memory implementation with memset/memsetinfinite/memcpy/memcpyinfinite primitives

To provide such primitives, we generate constraints such as "for all indices in the copied range, read from the source array, else read from the old array"

To make such constraints compatible with a Quantifier-Free logic, we use an instantiation-based approach, with layers of "uninstantiated constraints". The constraints are then instantiated ON READ (i.e., after reading index 42: "if 42 is in the copied range, read from the source array, else read from the old array").

Two successive copies can overlap with each other (RANGES CAN BE SYMBOLIC), which is why the layered architecture -and possibly useless constraints- are needed.

Example: memcopy(start1, end1, source1, memory1) # uninstantiated constraints: "for all indices i in (start1, end1), memory2[i] == source1[i], else memory2[i] == memory1[i]" # instantiated constraints:

memcopy(start2, end2, source2, memory2) # uninstantiated constraints: "for all indices i in (start1, end1), memory2[i] == source1[i], else memory2[i] == memory1[i]" "for all indices i in (start2, end2), memory3[i] == source2[i], else memory3[i] == memory2[i]" # instantiated constraints:

read(42) --> return memory3[42] # uninstantiated constraints: "for all indices i in (start1, end1), memory2[i] == source1[i], else memory2[i] == memory1[i]" "for all indices i in (start2, end2), memory3[i] == source2[i], else memory3[i] == memory2[i]" # instantiated constraints: "if 42 in (start1, end1), memory2[42] == source1[42], else memory2[42] == memory1[42]" "if 42 in (start2, end2), memory3[42] == source2[42], else memory3[42] == memory2[42]"

method __init__

__init__(
    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

property constraints

Get the constraints of the memory.

Returns: the constraints

property layer_level

How many layers of lambda constraints are there?

Returns: the number of layers

method add_constraint

add_constraint(formula)

Add a constraint to the memory.

Args:

  • formula: the constraint to add

method add_constraints

add_constraints(formulas)

Add constraints to the memory.

Args:

  • formulas: the constraints to add

method copy

copy(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

method memcopy

memcopy(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

method memcopyinfinite

memcopyinfinite(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

method memset

memset(start, value, size)

Perform a memset operation

Args:

  • start: the start index
  • value: the value to write
  • size: the number of bytes to write

method memsetinfinite

memsetinfinite(start, value)

Perform a memsetinfinite operation

Args:

  • start: the start index
  • value: the value to write

method readn

readn(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

This file was automatically generated via lazydocs.