Implement FPSE-like memory model (#1127)

Implements am fpse-like memory model.

.codeclimate.yml

@@ -11,7 +11,7 @@ checks:
   file-lines:
     enabled: true
     config:
-      threshold: 1000
+      threshold: 9000
   method-complexity:
     enabled: true
     config:

manticore/__main__.py

@@ -98,6 +98,8 @@ def parse_arguments():
                            help='Specify symbolic input file, \'+\' marks symbolic bytes')
     bin_flags.add_argument('--env', type=str, nargs=1, default=[], action='append',
                            help='Add an environment variable. Use "+" for symbolic bytes. (VARNAME=++++)')
+    bin_flags.add_argument('--pure-symbolic', action='store_true',
+                           help='Treat all writable memory as symbolic')
 
     eth_flags = parser.add_argument_group('Ethereum flags')
     eth_flags.add_argument('--verbose-trace', action='store_true',

manticore/core/smtlib/expression.py

@@ -609,11 +609,12 @@ class Array(Expression):
         return index
 
     def cast_value(self, value):
-        if isinstance(value, str) and len(value) == 1:
+        if isinstance(value, (str, bytes)) and len(value) == 1:
             value = ord(value)
         if isinstance(value, int):
             return BitVecConstant(self.value_bits, value)
-        assert isinstance(value, BitVec) and value.size == self.value_bits
+        assert isinstance(value, BitVec)
+        assert value.size == self.value_bits
         return value
 
     def __len__(self):

manticore/core/smtlib/solver.py

@@ -281,7 +281,7 @@ class Z3Solver(Solver):
             raise SolverException(_status)
         if consider_unknown_as_unsat:
             if _status == 'unknown':
-                logger.warning('Found an unknown core, probably a solver timeout')
+                logger.info('Found an unknown core, probably a solver timeout')
                 _status = 'unsat'
 
         if _status == 'unknown':

manticore/core/smtlib/visitors.py

@@ -751,6 +751,30 @@ def replace(expression, bindings):
     return result_expression
 
 
+class ArraySelectSimplifier(Visitor):
+    class ExpressionNotSimple(RuntimeError):
+        pass
+
+    def __init__(self, target_index, **kwargs):
+        super().__init__(**kwargs)
+        self._target_index = target_index
+        self.stores = []
+
+    def visit_ArrayStore(self, exp, target, where, what):
+        if not isinstance(what, BitVecConstant):
+            raise self.ExpressionNotSimple
+
+        if where.value == self._target_index:
+            self.stores.append(what.value)
+
+
+def simplify_array_select(array_exp):
+    assert isinstance(array_exp, ArraySelect)
+    simplifier = ArraySelectSimplifier(array_exp.index.value)
+    simplifier.visit(array_exp)
+    return simplifier.stores
+
+
 def get_variables(expression):
     visitor = GetDeclarations()
     visitor.visit(expression)

manticore/native/cli.py

@@ -7,7 +7,7 @@ def native_main(args, logger_):
 
     m = Manticore(args.argv[0], argv=args.argv[1:], env=env, entry_symbol=args.entrysymbol,
                   workspace_url=args.workspace, policy=args.policy,
-                  concrete_start=args.data, stdin_size=args.stdin_size)
+                  concrete_start=args.data, pure_symbolic=args.pure_symbolic, stdin_size=args.stdin_size)
 
     # Default plugins for now.. FIXME REMOVE!
     m.register_plugin(InstructionCounter())

manticore/native/cpu/abstractcpu.py

@@ -3,12 +3,14 @@ import logging
 from itertools import islice
 
 import io
+import struct
 import unicorn
 from functools import wraps
 
 from .disasm import init_disassembler
-from ..memory import ConcretizeMemory, InvalidMemoryAccess
-from ...core.smtlib import BitVec, Operators, Constant
+from ..memory import ConcretizeMemory, InvalidMemoryAccess, LazySMemory
+from ...core.smtlib import BitVec, Operators, Constant, visitors
+from ...core.smtlib.solver import solver
 from ...utils.emulate import UnicornEmulator
 from ...utils.event import Eventful
 from ...utils.helpers import issymbolic
@@ -29,7 +31,7 @@ class DecodeException(CpuException):
     Raised when trying to decode an unknown or invalid instruction '''
 
     def __init__(self, pc, bytes):
-        super().__init__("Error decoding instruction @%08x" % pc)
+        super().__init__("Error decoding instruction @ 0x{:x}".format(pc))
         self.pc = pc
         self.bytes = bytes
 
@@ -759,8 +761,14 @@ class Cpu(Eventful):
             c = self.memory[address]
 
             if issymbolic(c):
-                assert isinstance(c, BitVec) and c.size == 8
-                if isinstance(c, Constant):
+                # In case of fully symbolic memory, eagerly get a valid ptr
+                if isinstance(self.memory, LazySMemory):
+                    try:
+                        vals = visitors.simplify_array_select(c)
+                        c = bytes([vals[0]])
+                    except visitors.ArraySelectSimplifier.ExpressionNotSimple:
+                        c = struct.pack('B', solver.get_value(self.memory.constraints, c))
+                elif isinstance(c, Constant):
                     c = bytes([c.value])
                 else:
                     logger.error('Concretize executable memory %r %r', c, text)

manticore/native/manticore.py

@@ -34,7 +34,7 @@ class Manticore(ManticoreBase):
         super().__init__(initial_state, workspace_url=workspace_url, policy=policy, **kwargs)
 
     @classmethod
-    def linux(cls, path, argv=None, envp=None, entry_symbol=None, symbolic_files=None, concrete_start='', stdin_size=consts.stdin_size, **kwargs):
+    def linux(cls, path, argv=None, envp=None, entry_symbol=None, symbolic_files=None, concrete_start='', pure_symbolic=False, stdin_size=consts.stdin_size, **kwargs):
         """
         Constructor for Linux binary analysis.
 
@@ -54,7 +54,7 @@ class Manticore(ManticoreBase):
         :rtype: Manticore
         """
         try:
-            return cls(_make_linux(path, argv, envp, entry_symbol, symbolic_files, concrete_start, stdin_size), **kwargs)
+            return cls(_make_linux(path, argv, envp, entry_symbol, symbolic_files, concrete_start, pure_symbolic, stdin_size), **kwargs)
         except elftools.common.exceptions.ELFError:
             raise Exception(f'Invalid binary: {path}')
 
@@ -131,7 +131,7 @@ def _make_decree(program, concrete_start='', **kwargs):
     return initial_state
 
 
-def _make_linux(program, argv=None, env=None, entry_symbol=None, symbolic_files=None, concrete_start='', stdin_size=consts.stdin_size):
+def _make_linux(program, argv=None, env=None, entry_symbol=None, symbolic_files=None, concrete_start='', pure_symbolic=False, stdin_size=consts.stdin_size):
     from ..platforms import linux
 
     env = {} if env is None else env
@@ -142,7 +142,8 @@ def _make_linux(program, argv=None, env=None, entry_symbol=None, symbolic_files=
 
     constraints = ConstraintSet()
     platform = linux.SLinux(program, argv=argv, envp=env,
-                            symbolic_files=symbolic_files)
+                            symbolic_files=symbolic_files,
+                            pure_symbolic=pure_symbolic)
     if entry_symbol is not None:
         entry_pc = platform._find_symbol(entry_symbol)
         if entry_pc is None:
@@ -158,6 +159,9 @@ def _make_linux(program, argv=None, env=None, entry_symbol=None, symbolic_files=
     if concrete_start != '':
         logger.info('Starting with concrete input: %s', concrete_start)
 
+    if pure_symbolic:
+        logger.warning('[EXPERIMENTAL] Using purely symbolic memory.')
+
     for i, arg in enumerate(argv):
         argv[i] = initial_state.symbolicate_buffer(arg, label=f'ARGV{i + 1}')
 

manticore/native/memory.py

@@ -1,9 +1,11 @@
 from abc import ABCMeta, abstractmethod
 from weakref import WeakValueDictionary
-from ..core.smtlib import Operators, ConstraintSet, arithmetic_simplify, solver, TooManySolutions, BitVec, BitVecConstant
-import logging
+from ..core.smtlib import Operators, ConstraintSet, arithmetic_simplify, solver, TooManySolutions, BitVec, BitVecConstant, expression
 from ..native.mappings import mmap, munmap
-from ..utils.helpers import issymbolic
+from ..utils.helpers import issymbolic, interval_intersection
+
+import functools
+import logging
 
 logger = logging.getLogger(__name__)
 
@@ -158,6 +160,12 @@ class Map(object, metaclass=ABCMeta):
         '''
         return f'<{self.__class__.__name__} 0x{self.start:016x}-0x{self.end:016x} {self.perms}>'
 
+    def __iter__(self):
+        """
+        Iterate all valid addresses
+        """
+        return iter(range(self._start, self._end))
+
     def __eq__(self, other):
         return self.start == other.start and \
             self.end == other.end and \
@@ -236,7 +244,7 @@ class Map(object, metaclass=ABCMeta):
 class AnonMap(Map):
     ''' A concrete anonymous memory map '''
 
-    def __init__(self, start, size, perms, data_init=None, **kwargs):
+    def __init__(self, start, size, perms, data_init=None, name=None, **kwargs):
         '''
         Builds a concrete anonymous memory map.
 
@@ -245,7 +253,7 @@ class AnonMap(Map):
         :param perms: the access permissions of the map.
         :param data_init: the data to initialize the map.
         '''
-        super().__init__(start, size, perms, **kwargs)
+        super().__init__(start, size, perms, name, **kwargs)
         self._data = bytearray(size)
         if data_init is not None:
             assert len(data_init) <= size, 'More initial data than reserved memory'
@@ -256,7 +264,7 @@ class AnonMap(Map):
                 self._data[0:len(data_init)] = [ord(s) for s in data_init]
 
     def __reduce__(self):
-        return (self.__class__, (self.start, len(self), self.perms, self._data, ))
+        return (self.__class__, (self.start, len(self), self.perms, self._data, self.name))
 
     def split(self, address):
         if address <= self.start:
@@ -273,6 +281,10 @@ class AnonMap(Map):
         assert not isinstance(index, slice) or \
             len(value) == index.stop - index.start
         index = self._get_offset(index)
+
+        if issymbolic(value[0]) and isinstance(self._data, bytearray):
+            self._data = [Operators.ORD(b) for b in self._data]  # completely convert everything to a list if we need to store some symbolic data, just copying fpse
+
         if isinstance(index, slice):
             if not isinstance(value[0], int):
                 value = [Operators.ORD(n) for n in value]
@@ -283,8 +295,48 @@ class AnonMap(Map):
     def __getitem__(self, index):
         index = self._get_offset(index)
         if isinstance(index, slice):
-            return [bytes([i]) for i in self._data[index]]
-        return bytes([self._data[index]])
+            return [Operators.CHR(i) for i in self._data[index]]
+        return Operators.CHR(self._data[index])
+
+
+class ArrayMap(Map):
+    def __init__(self, address, size, perms, index_bits, backing_array=None, name=None, **kwargs):
+        super(ArrayMap, self).__init__(address, size, perms)
+        if name is None:
+            name = 'ArrayMap_{:x}'.format(address)
+        if backing_array is not None:
+            self._array = backing_array
+        else:
+            self._array = expression.ArrayProxy(expression.ArrayVariable(index_bits, index_max=size, value_bits=8, name=name))
+
+    def __reduce__(self):
+        return self.__class__, (self.start, len(self), self._perms, self._array.index_bits, self._array, self._array.name)
+
+    def __setitem__(self, key, value):
+        self._array[key] = value
+
+    def __getitem__(self, key):
+        return self._array[key]
+
+    def split(self, address):
+        if address <= self.start:
+            return None, self
+        if address >= self.end:
+            return self, None
+
+        assert self.start < address < self.end
+        index_bits, value_bits = self._array.index_bits, self._array.value_bits
+
+        left_size, right_size = address - self.start, self.end - address
+        left_name, right_name = ['{}_{:d}'.format(self._array.name, i) for i in range(2)]
+
+        head_arr = expression.ArrayProxy(expression.ArrayVariable(index_bits, left_size, value_bits, name=left_name))
+        tail_arr = expression.ArrayProxy(expression.ArrayVariable(index_bits, right_size, value_bits, name=right_name))
+
+        head = ArrayMap(self.start, left_size, self.perms, index_bits, head_arr, left_name)
+        tail = ArrayMap(address, right_size, self.perms, index_bits, tail_arr, right_name)
+
+        return head, tail
 
 
 class FileMap(Map):
@@ -638,7 +690,7 @@ class Memory(object, metaclass=ABCMeta):
             assert i not in self._page2map, 'Map already used'
 
         # Create the anonymous map
-        m = AnonMap(start=addr, size=size, perms=perms, data_init=data_init)
+        m = AnonMap(start=addr, size=size, perms=perms, data_init=data_init, name=name)
 
         # Okay, ready to alloc
         self._add(m)
@@ -881,6 +933,16 @@ class Memory(object, metaclass=ABCMeta):
             result = self.read(index, 1)[0]
         return result
 
+    def __iter__(self):
+        """
+        Iterate all valid addresses
+        """
+        for page_addr in sorted(self._page2map.keys()):
+            start = page_addr * self.page_size
+            end = start + self.page_size
+            for addr in range(start, end):
+                yield addr
+
 
 class SMemory(Memory):
     '''
@@ -1071,6 +1133,211 @@ class SMemory(Memory):
         return solutions
 
 
+class LazySMemory(SMemory):
+    '''
+    A fully symbolic memory.
+
+    Currently does not support cross-page reads/writes.
+    '''
+
+    def __init__(self, constraints, *args, **kwargs):
+        super(LazySMemory, self).__init__(constraints, *args, **kwargs)
+        self.backing_array = constraints.new_array(index_bits=self.memory_bit_size)
+        self.backed_by_symbolic_store = set()
+
+    def __reduce__(self):
+        return (self.__class__, (self.constraints, self._symbols, self._maps),
+                {'backing_array': self.backing_array,
+                 'backed_by_symbolic_store': self.backed_by_symbolic_store})
+
+    def __setstate__(self, state):
+        self.backing_array = state['backing_array']
+        self.backed_by_symbolic_store = state['backed_by_symbolic_store']
+
+    def mmapFile(self, addr, size, perms, filename, offset=0):
+        '''
+        Creates a new file mapping in the memory address space.
+
+        :param addr: the starting address (took as hint). If C{addr} is C{0} the first big enough
+                     chunk of memory will be selected as starting address.
+        :param size: the contents of a file mapping are initialized using C{size} bytes starting
+                     at offset C{offset} in the file C{filename}.
+        :param perms: the access permissions to this memory.
+        :param filename: the pathname to the file to map.
+        :param offset: the contents of a file mapping are initialized using C{size} bytes starting
+                      at offset C{offset} in the file C{filename}.
+        :return: the starting address where the file was mapped.
+        :rtype: int
+        :raises error:
+                   - 'Address shall be concrete' if C{addr} is not an integer number.
+                   - 'Address too big' if C{addr} goes beyond the limit of the memory.
+                   - 'Map already used' if the piece of memory starting in C{addr} and with length C{size} isn't free.
+        '''
+        # If addr is NULL, the system determines where to allocate the region.
+        assert addr is None or isinstance(addr, int), 'Address shall be concrete'
+        assert addr < self.memory_size, 'Address too big'
+        assert size > 0
+
+        map = AnonMap(addr, size, perms)
+        self._add(map)
+
+        # address is rounded down to the nearest multiple of the allocation granularity
+        if addr is not None:
+            addr = self._floor(addr)
+
+        # size value is rounded up to the next page boundary
+        size = self._ceil(size)
+
+        with open(filename, 'rb') as f:
+            fdata = f.read()  # fdata is a bytes now
+
+        # this worked
+        fdata = fdata[offset:]
+        fdata = fdata.ljust(size, b'\0')
+
+        for i in range(size):
+            Memory.write(self, addr + i, chr(fdata[i]), force=True)
+
+        logger.debug('New file-memory map @%x size:%x', addr, size)
+
+        return addr
+
+    def _deref_can_succeed(self, mapping, address, size):
+        if not issymbolic(address):
+            return address >= mapping.start and address + size < mapping.end
+        else:
+            constraint = Operators.AND(address >= mapping.start, address + size < mapping.end)
+            return solver.can_be_true(self.constraints, constraint)
+
+    def _import_concrete_memory(self, from_addr, to_addr):
+        """
+        for each address in this range need to read from concrete and write to symbolic
+        it's possible that there will be invalid/unmapped addresses in this range. need to skip to next map if so
+        also need to mark all of these addresses as now in the symbolic store
+
+        :param int from_addr:
+        :param int to_addr:
+        :return:
+        """
+        logger.debug("Importing concrete memory: {:x} - {:x} ({} bytes)".format(from_addr, to_addr, to_addr - from_addr))
+
+        for m in self.maps:
+            span = interval_intersection(m.start, m.end, from_addr, to_addr)
+            if span is None:
+                continue
+
+            start, stop = span
+
+            for addr in range(start, stop):
+                if addr in self.backed_by_symbolic_store:
+                    continue
+
+                self.backing_array[addr] = Memory.read(self, addr, 1)[0]
+                self.backed_by_symbolic_store.add(addr)
+
+    def _map_deref_expr(self, map, address):
+        return Operators.AND(
+            Operators.UGE(address, map.start),
+            Operators.ULT(address, map.end))
+
+    def _reachable_range(self, sym_address, size):
+        addr_min, addr_max = solver.minmax(self.constraints, sym_address)
+        return addr_min, addr_max + size - 1
+
+    def valid_ptr(self, address):
+        assert issymbolic(address)
+
+        expressions = [self._map_deref_expr(m, address) for m in self._maps]
+        valid = functools.reduce(Operators.OR, expressions)
+
+        return valid
+
+    def invalid_ptr(self, address):
+        return Operators.NOT(self.valid_ptr(address))
+
+    def read(self, address, size, force=False):
+
+        access_min, access_max = self._reachable_range(address, size)
+
+        if issymbolic(address):
+            self._import_concrete_memory(access_min, access_max)
+
+        retvals = []
+        # Not range() because `address` can be symbolic.
+        addrs_to_access = [address + i for i in range(size)]
+        for addr in addrs_to_access:
+
+            # If the deref is symbolic, or it's backed by a symbolic store on a page
+            # that is writeable, go from backing_array. (if page is r-- or r-x, it would
+            # not have had symbolic data written to it.)
+            if issymbolic(addr):
+                from_array = True
+            elif addr in self.backed_by_symbolic_store:
+                m = self.map_containing(addr)
+                from_array = not m or 'w' in m.perms
+            else:
+                from_array = False
+
+            if from_array:
+                val = self.backing_array[addr]
+            else:
+                val = Memory.read(self, addr, 1)[0]
+
+            retvals.append(val)
+
+        return retvals
+
+    def write(self, address, value, force=False):
+
+        size = len(value)
+
+        addrs_to_access = [address + i for i in range(size)]
+
+        if issymbolic(address):
+            access_min, access_max = self._reachable_range(address, size)
+
+            self._import_concrete_memory(access_min, access_max)
+
+            for addr, byte in zip(addrs_to_access, value):
+                self.backing_array[addr] = Operators.ORD(byte)
+        else:
+            self.backed_by_symbolic_store -= set(addrs_to_access)
+            Memory.write(self, address, value)
+
+    def scan_mem(self, data_to_find):
+        """
+        Scan for concrete bytes in all mapped memory. Successively yield addresses of all matches.
+
+        :param bytes data_to_find: String to locate
+        :return:
+        """
+
+        # TODO: for the moment we just treat symbolic bytes as bytes that don't match.
+        # for our simple test cases right now, the bytes we're interested in scanning
+        # for will all just be there concretely
+        # TODO: Can probably do something smarter here like Boyer-Moore, but unnecessary
+        # if we're looking for short strings.
+
+        # Querying mem with an index returns [bytes]
+        if isinstance(data_to_find, bytes):
+            data_to_find = [bytes([c]) for c in data_to_find]
+
+        for mapping in sorted(self.maps):
+            for ptr in mapping:
+                if ptr + len(data_to_find) >= mapping.end:
+                    break
+
+                candidate = mapping[ptr:ptr + len(data_to_find)]
+
+                # TODO: treat symbolic bytes as bytes that don't match. for our simple tests right now, the
+                # bytes will be there concretely
+                if issymbolic(candidate[0]):
+                    break
+
+                if candidate == data_to_find:
+                    yield ptr
+
+
 class Memory32(Memory):
     memory_bit_size = 32
     page_bit_size = 12
@@ -1094,3 +1361,13 @@ class SMemory32L(SMemory):
 class SMemory64(SMemory):
     memory_bit_size = 64
     page_bit_size = 12
+
+
+class LazySMemory32(LazySMemory):
+    memory_bit_size = 32
+    page_bit_size = 12
+
+
+class LazySMemory64(LazySMemory):
+    memory_bit_size = 64
+    page_bit_size = 12

manticore/platforms/linux.py

@@ -22,7 +22,7 @@ from ..core.smtlib import Expression
 from ..exceptions import SolverException
 from ..native.cpu.abstractcpu import Syscall, ConcretizeArgument, Interruption
 from ..native.cpu.cpufactory import CpuFactory
-from ..native.memory import SMemory32, SMemory64, Memory32, Memory64
+from ..native.memory import SMemory32, SMemory64, Memory32, Memory64, LazySMemory32, LazySMemory64
 from ..platforms.platform import Platform, SyscallNotImplemented
 from ..utils.helpers import issymbolic
 
@@ -2450,21 +2450,28 @@ class SLinux(Linux):
     """
 
     def __init__(self, programs, argv=None, envp=None, symbolic_files=None,
-                 disasm='capstone'):
+                 disasm='capstone', pure_symbolic=False):
         argv = [] if argv is None else argv
         envp = [] if envp is None else envp
         symbolic_files = [] if symbolic_files is None else symbolic_files
 
         self._constraints = ConstraintSet()
+        self._pure_symbolic = pure_symbolic
         self.random = 0
         self.symbolic_files = symbolic_files
         super().__init__(programs, argv=argv, envp=envp, disasm=disasm)
 
     def _mk_proc(self, arch):
         if arch in {'i386', 'armv7'}:
-            mem = SMemory32(self.constraints)
+            if self._pure_symbolic:
+                mem = LazySMemory32(self.constraints)
+            else:
+                mem = SMemory32(self.constraints)
         else:
-            mem = SMemory64(self.constraints)
+            if self._pure_symbolic:
+                mem = LazySMemory64(self.constraints)
+            else:
+                mem = SMemory64(self.constraints)
 
         cpu = CpuFactory.get_cpu(mem, arch)
         return cpu

manticore/utils/helpers.py

@@ -84,6 +84,17 @@ def taint_with(arg, taint, value_bits=256, index_bits=256):
     return arg
 
 
+def interval_intersection(min1, max1, min2, max2):
+    """
+    Given two intervals, (min1, max1) and (min2, max2) return their intersecting interval,
+    or None if they do not overlap.
+    """
+    left, right = max(min1, min2), min(max1, max2)
+    if left < right:
+        return left, right
+    return None
+
+
 class CacheDict(OrderedDict):
     def __init__(self, *args, max_size=30000, flush_perc=30, **kwargs):
         self._max_size = max_size

tests/test_lazy_memory.py

@@ -0,0 +1,270 @@
+from io import BytesIO
+import unittest
+import tempfile
+import os
+import gc
+import pickle
+import fcntl
+import resource
+from itertools import *
+import sys
+
+from manticore.native.memory import *
+from manticore.utils.helpers import issymbolic
+from manticore.core.smtlib import Solver, Operators
+from manticore.core.smtlib.expression import *
+from manticore.core.smtlib.visitors import *
+
+
+class LazyMemoryTest(unittest.TestCase):
+    _multiprocess_can_split_ = True
+
+    def test_basic(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+        mem.mmap(0, 4096, 'rwx', name='map')
+
+        m = mem.maps.pop()
+        self.assertIsInstance(m, AnonMap)
+        self.assertEqual(m.name, 'map')
+
+    def test_read(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+        mem.mmap(0, 4096, 'rwx', name='map')
+
+        val_mapped = mem.read(0, 4)
+
+        for val in val_mapped:
+            self.assertIsInstance(val, bytes)
+
+        with self.assertRaises(InvalidMemoryAccess):
+            mem.read(8096, 4)
+
+    def test_sym_read_mapped(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+        mem.mmap(0, 4096, 'rwx', name='map')
+
+        addr = cs.new_bitvec(32)
+
+        # constrain on a boundary
+        cs.add(addr >= 0xffc)
+        cs.add(addr < 0x1002)
+
+        # Ensure that all valid derefs are within mapped memory
+        with cs as new_cs:
+            new_cs.add(mem.valid_ptr(addr))
+            vals = solver.get_all_values(new_cs, addr)
+            self.assertGreater(len(vals), 0)
+            for v in vals:
+                print(v)
+                self.assertTrue(0 <= v < 4096)
+
+        # Ensure that all invalid derefs are outside of mapped memory
+        with cs as new_cs:
+            new_cs.add(mem.invalid_ptr(addr))
+            vals = solver.get_all_values(new_cs, addr)
+            self.assertGreater(len(vals), 0)
+            for v in vals:
+                self.assertFalse(0 <= v < 4096)
+
+        val = mem.read(addr, 1)[0]
+
+        self.assertIsInstance(val, Expression)
+
+    def test_lazysymbolic_basic_constrained_read(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+        sym = cs.new_bitvec(32)
+
+        cs.add(sym.uge(0xfff))
+        cs.add(sym.ule(0x1010))
+
+        # Make sure reading with no mappings raises an issue
+        self.assertRaises(MemoryException, mem.__getitem__, 0x1000)
+
+        first = mem.mmap(0x1000, 0x1000, 'rw')
+
+        self.assertEqual(first, 0x1000)
+
+        mem.write(0x1000, b'\x00')
+
+        self.assertEqual(solver.get_all_values(cs, mem[0x1000]), [b'\x00'])
+
+    def test_arraymap(self):
+        m = ArrayMap(0x1000, 0x1000, 'rwx', 32)
+        head, tail = m.split(0x1800)
+
+        self.assertEqual(head.start, 0x1000)
+        self.assertEqual(tail.start, 0x1800)
+
+        self.assertEqual(len(head), 0x800)
+        self.assertEqual(len(tail), 0x800)
+
+        self.assertEquals(head.perms, m.perms)
+        self.assertEquals(tail.perms, m.perms)
+
+        reduced = m.__reduce__()
+        self.assertIs(reduced[0], ArrayMap)
+
+        sel = m[0x1]
+        self.assertIsInstance(sel, ArraySelect)
+
+        pre_array = m._array.array
+        m[0x1] = 1
+        post_array = m._array.array
+        self.assertIsNot(pre_array, post_array)
+
+    def test_lazysymbolic_mmapfile(self):
+        mem = LazySMemory32(ConstraintSet())
+
+        #start with no maps
+        self.assertEqual(len(mem.mappings()), 0)
+
+        rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
+        rwx_file.file.write(b'a' * 0x1001)
+        rwx_file.close()
+
+        addr_a = mem.mmapFile(0, 0x1000, 'rwx', rwx_file.name)
+
+        self.assertEqual(len(mem.mappings()), 1)
+
+        self.assertEqual(mem[addr_a], b'a')
+        self.assertEqual(mem[addr_a + 0x1000 // 2], b'a')
+        self.assertEqual(mem[addr_a + (0x1000 - 1)], b'a')
+        self.assertRaises(MemoryException, mem.__getitem__, addr_a + (0x1000))
+
+        rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
+        rwx_file.file.write(b'b' * 0x1001)
+        rwx_file.close()
+
+        addr_b = mem.mmapFile(0, 0x1000, 'rw', rwx_file.name)
+
+        self.assertEqual(len(mem.mappings()), 2)
+
+        self.assertEqual(mem[addr_b], b'b')
+        self.assertEqual(mem[addr_b + (0x1000 // 2)], b'b')
+        self.assertEqual(mem[addr_b + (0x1000 - 1)], b'b')
+
+        rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
+        rwx_file.file.write(b'c' * 0x1001)
+        rwx_file.close()
+
+        addr_c = mem.mmapFile(0, 0x1000, 'rx', rwx_file.name)
+
+        self.assertEqual(len(mem.mappings()), 3)
+
+        self.assertEqual(mem[addr_c], b'c')
+        self.assertEqual(mem[addr_c + (0x1000 // 2)], b'c')
+        self.assertEqual(mem[addr_c + (0x1000 - 1)], b'c')
+
+        rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
+        rwx_file.file.write(b'd' * 0x1001)
+        rwx_file.close()
+
+        addr_d = mem.mmapFile(0, 0x1000, 'r', rwx_file.name)
+
+        self.assertEqual(len(mem.mappings()), 4)
+
+        self.assertEqual(mem[addr_d], b'd')
+        self.assertEqual(mem[addr_d + (0x1000 // 2)], b'd')
+        self.assertEqual(mem[addr_d + (0x1000 - 1)], b'd')
+
+        rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
+        rwx_file.file.write(b'e' * 0x1001)
+        rwx_file.close()
+
+        addr_e = mem.mmapFile(0, 0x1000, 'w', rwx_file.name)
+
+        self.assertEqual(len(mem.mappings()), 5)
+
+        self.assertRaises(MemoryException, mem.__getitem__, addr_e)
+        self.assertRaises(MemoryException, mem.__getitem__, addr_e + (0x1000 // 2))
+        self.assertRaises(MemoryException, mem.__getitem__, addr_e + (0x1000 - 1))
+
+    def test_lazysymbolic_map_containing(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+        valid = cs.new_bitvec(32)
+        invalid = cs.new_bitvec(32)
+
+        mem.mmap(0x1000, 0x1000, 'rw')
+        m = list(mem._maps)[0]
+
+        cs.add(valid > 0x1000)
+        cs.add(valid < 0x1002)
+
+        cs.add(invalid < 0x1000)
+
+        ret = mem._deref_can_succeed(m, valid, 1)
+        self.assertTrue(ret)
+
+        ret = mem._deref_can_succeed(m, invalid, 1)
+        self.assertFalse(ret)
+
+        ret = mem._deref_can_succeed(m, 0x1000, 1)
+        self.assertTrue(ret)
+
+        ret = mem._deref_can_succeed(m, 0x800, 1)
+        self.assertFalse(ret)
+
+        ret = mem._deref_can_succeed(m, 0xFFF, 2);
+        self.assertFalse(ret)
+
+        ret = mem._deref_can_succeed(m, 0x1000, 2);
+        self.assertTrue(ret)
+
+        ret = mem._deref_can_succeed(m, 0x1000, 0xFFF);
+        self.assertTrue(ret)
+
+        ret = mem._deref_can_succeed(m, 0x1000, 0x1000);
+        self.assertFalse(ret)
+
+    @unittest.skip("Disabled because it takes 4+ minutes; get_all_values() isn't returning all possible addresses")
+    def test_lazysymbolic_constrained_deref(self):
+        cs = ConstraintSet()
+        mem = LazySMemory32(cs)
+
+        mem.page_bit_size = 12
+        Size = 0x1000
+        PatternSize = 0x100
+        Constant = 0x48
+        ConstantMask = 0xff
+
+        if False:
+            mem.page_bit_size = 10
+            Size = 0x800
+            PatternSize = 0x80
+            Constant = 0x48
+            ConstantMask = 0xff
+
+        first = mem.mmap(Size, Size, 'rw')
+
+        # Fill with increasing bytes
+        mem.write(first, bytes(islice(cycle(range(PatternSize)), Size)))
+
+        sym = cs.new_bitvec(32)
+        #cs.add(mem.valid_ptr(sym))
+
+        vals = mem.read(sym, 4)
+        # print("sym:")
+        # print(translate_to_smtlib(sym))
+
+        cs.add(vals[0] == Constant)
+        cs.add(vals[1] == (Constant + 1))
+
+        # print("\nvals:")
+        # print(translate_to_smtlib(cs))
+
+        possible_addrs = solver.get_all_values(cs, sym)
+        print("possible addrs: ", [hex(a) for a in sorted(possible_addrs)])
+        for i in possible_addrs:
+            self.assertTrue((i & ConstantMask) == Constant)
+
+        # There are 16 spans with 0x48 in [0x1000, 0x2000]
+        self.assertEqual(len(possible_addrs), Size // PatternSize)
+
+
+if __name__ == '__main__':
+    unittest.main()

tests/test_memory.py

@@ -15,6 +15,7 @@ from manticore.native.memory import *
 from manticore import issymbolic
 
 
+
 def isconcrete(value):
     return not issymbolic(value)
 
@@ -1057,6 +1058,18 @@ class MemoryTest(unittest.TestCase):
         os.unlink(r_file.name)
         os.unlink(w_file.name)
 
+    def test_mem_iter(self):
+        cs = ConstraintSet()
+        mem = SMemory32(cs)
+
+        mem.mmap(0x1000, 0x2000, 'rw ')
+        mem.mmap(0x4000, 0x1000, 'rw ')
+
+        all_addresses = [x for x in mem]
+
+        self.assertEqual(len(all_addresses), 0x2000 + 0x1000)
+        self.assertIn(0x1000, all_addresses)
+        self.assertNotIn(0x3000, all_addresses)
 
     def test_mix_of_concrete_and_symbolic__push_pop_cleaning_store(self):
         #global mainsolver