diff --git a/docs/api.rst b/docs/api.rst index 72a8ae4..533f2d4 100644 --- a/docs/api.rst +++ b/docs/api.rst @@ -20,7 +20,7 @@ State ----- .. autoclass:: manticore.core.state.State - :members: abandon, constrain, new_symbolic_buffer, new_symbolic_value, solve_n, solve_one, symbolicate_buffer, invoke_model + :members: abandon, constrain, new_symbolic_buffer, new_symbolic_value, solve_n, solve_one, solve_buffer, symbolicate_buffer, invoke_model Cpu --- diff --git a/manticore/core/state.py b/manticore/core/state.py index d631d00..4196cf1 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -232,6 +232,24 @@ class State(object): ''' return self._solver.get_all_values(self.constraints, expr, nsolves, silent=True) + def solve_buffer(self, addr, nbytes): + ''' + Reads `nbytes` of symbolic data from a buffer in memory at `addr` and attempts to + concretize it + + :param int address: Address of buffer to concretize + :param int nbytes: Size of buffer to concretize + :return: Concrete contents of buffer + :rtype: list[int] + ''' + buffer = self.cpu.read_bytes(addr, nbytes) + result = [] + with self.constraints as temp_cs: + for c in buffer: + result.append(self._solver.get_value(temp_cs, c)) + temp_cs.add(c == result[-1]) + return result + def record_branches(self, targets): _, branch = self.last_pc for target in targets: