Add codeclimate, tox, and pycodestyle configs (#772)

* pep8

autopep8 -r -i -a -a manticore

* tox for testing py3k

* minimal codeclimate

* Add correct Code Climate ID

* unignore max line endings since it's set to 160

* more badges

* turn off pep8 in code climate

* need to remove for codeclimate to work right

* re-enable most checks with looser thresholds

* remove unused imports

autoflake --in-place -r manticore

* revert the autoflakes changes

* set tox to only py27 for now

* cache is hardcoded to python 2.7.13

* Comment cleanup

* Try autoflake again

* Add dev environment dependency management to tox.ini

* Remove count/statistics options from tox.ini

Per Dan, these crash pep8 analysis on codeclimate at present

* Revert setstate initialization

* Re-introduce explicit compare for flags

* add back structural comment

* rm unneeeded ` as e`

* bump py tox

.codeclimate.yml

@@ -0,0 +1,62 @@
+version: "2"
+checks:
+  argument-count:
+    enabled: true
+    config:
+      threshold: 7
+  complex-logic:
+    enabled: true
+    config:
+      threshold: 4
+  file-lines:
+    enabled: true
+    config:
+      threshold: 1000
+  method-complexity:
+    enabled: true
+    config:
+      threshold: 25
+  method-count:
+    enabled: true
+    config:
+      threshold: 30
+  method-lines:
+    enabled: true
+    config:
+      threshold: 50
+  nested-control-flow:
+    enabled: true
+    config:
+      threshold: 5
+  return-statements:
+    enabled: true
+    config:
+      threshold: 5
+  similar-code:
+    enabled: true
+    config:
+      threshold: 100
+  identical-code:
+    enabled: true
+    config:
+      threshold: 65
+plugins:
+  pep8:
+    enabled: true
+  sonar-python:
+    enabled: false
+    config:
+      minimum_severity: critical
+  radon:
+    enabled: false
+    config:
+      python_version: 2
+      threshold: "D"
+exclude_patterns:
+  - "docs/"
+  - "examples/"
+  - "scripts/"
+  - "tests/"
+  - "mcore_*/"
+  - ".tox/"
+

.travis.yml

@@ -1,20 +1,36 @@
+dist: trusty
+sudo: required
+os:
+  - linux
+language: python
+python:
+  - 2.7.13
+
+env:
+  global:
+    - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a
+
 branches:
   only:
   - master
   - /^(?!wip-).+$/
-language: python
+
 cache:
   pip: true
   directories:
   - $HOME/virtualenv/python2.7.13/lib/python2.7/site-packages
   - $HOME/virtualenv/python2.7.13/bin/
-dist: trusty
-sudo: required
-os:
-- linux
-python:
-- 2.7.13
+
 install:
-- scripts/travis_install.sh
+  - scripts/travis_install.sh
+
+before_script:
+  - curl -L https://codeclimate.com/downloads/test-reporter/test-reporter-latest-linux-amd64 > ./cc-test-reporter
+  - chmod +x ./cc-test-reporter
+  - ./cc-test-reporter before-build
+
 script:
-- scripts/travis_test.sh
+  - scripts/travis_test.sh
+
+after_script:
+  - ./cc-test-reporter after-build --exit-code $TRAVIS_TEST_RESULT

README.md

@@ -4,6 +4,8 @@
 [![PyPI version](https://badge.fury.io/py/manticore.svg)](https://badge.fury.io/py/manticore)
 [![Slack Status](https://empireslacking.herokuapp.com/badge.svg)](https://empireslacking.herokuapp.com)
 [![Documentation Status](https://readthedocs.org/projects/manticore/badge/?version=latest)](http://manticore.readthedocs.io/en/latest/?badge=latest)
+[![Maintainability](https://api.codeclimate.com/v1/badges/9161568d8378cea903f4/maintainability)](https://codeclimate.com/github/trailofbits/manticore/maintainability)
+[![Test Coverage](https://api.codeclimate.com/v1/badges/9161568d8378cea903f4/test_coverage)](https://codeclimate.com/github/trailofbits/manticore/test_coverage)
 
 Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
 

manticore/__main__.py

@@ -61,7 +61,7 @@ def parse_arguments():
                         help=("A folder name for temporaries and results."
                               "(default mcore_?????)"))
     parser.add_argument('--version', action='version', version='Manticore 0.1.7',
-                         help='Show program version information')
+                        help='Show program version information')
     parser.add_argument('--txlimit', type=positive,
                         help='Maximum number of symbolic transactions to run (positive integer) (Ethereum only)')
     parser.add_argument('--contract', type=str,
@@ -94,6 +94,7 @@ def ethereum_cli(args):
 
     m.multi_tx_analysis(args.argv[0], args.contract, args.txlimit)
 
+
 def main():
     log.init_logging()
     args = parse_arguments()
@@ -105,11 +106,11 @@ def main():
         ethereum_cli(args)
         return
 
-    env = {key:val for key, val in map(lambda env: env[0].split('='), args.env)}
+    env = {key: val for key, val in map(lambda env: env[0].split('='), args.env)}
 
     m = Manticore(args.argv[0], argv=args.argv[1:], env=env, workspace_url=args.workspace,  policy=args.policy, disasm=args.disasm, concrete_start=args.data)
 
-    #Fixme(felipe) remove this, move to plugin
+    # Fixme(felipe) remove this, move to plugin
     m.coverage_file = args.coverage
 
     if args.names is not None:
@@ -125,5 +126,6 @@ def main():
 
     m.run(procs=args.procs, timeout=args.timeout, should_profile=args.profile)
 
+
 if __name__ == '__main__':
     main()

manticore/binary/__init__.py

@@ -1,5 +1,5 @@
-''' Common binary formats interface 
-Ideally you should be able to do something like 
+''' Common binary formats interface
+Ideally you should be able to do something like
 
         from binary import Binary
         binary = Binary(filename)
@@ -15,8 +15,10 @@ and common API.  interpreters? linkers? linked DLLs?
 
 '''
 
+
 class Binary(object):
-    magics = { }
+    magics = {}
+
     def __new__(cls, path):
         if cls is Binary:
             cl = cls.magics[file(path).read(4)]
@@ -38,14 +40,15 @@ class Binary(object):
         pass
 
 
-
 from elftools.elf.elffile import ELFFile
 import StringIO
+
+
 class CGCElf(Binary):
 
     @staticmethod
     def _cgc2elf(filename):
-        #hack begin so we can use upstream Elftool
+        # hack begin so we can use upstream Elftool
         with open(filename, 'rb') as fd:
             stream = StringIO.StringIO(fd.read())
             stream.write('\x7fELF')
@@ -56,7 +59,7 @@ class CGCElf(Binary):
         super(CGCElf, self).__init__(filename)
         stream = self._cgc2elf(filename)
         self.elf = ELFFile(stream)
-        self.arch = {'x86':'i386','x64':'amd64'}[self.elf.get_machine_arch()]
+        self.arch = {'x86': 'i386', 'x64': 'amd64'}[self.elf.get_machine_arch()]
 
         assert 'i386' == self.arch
         assert self.elf.header.e_type in ['ET_EXEC']
@@ -70,17 +73,17 @@ class CGCElf(Binary):
                 continue
 
             flags = elf_segment.header.p_flags
-            #PF_X 0x1 Execute - PF_W 0x2 Write - PF_R 0x4 Read
-            perms = ['   ', '  x', ' w ', ' wx', 'r  ', 'r x', 'rw ', 'rwx'][flags&7]
+            # PF_X 0x1 Execute - PF_W 0x2 Write - PF_R 0x4 Read
+            perms = ['   ', '  x', ' w ', ' wx', 'r  ', 'r x', 'rw ', 'rwx'][flags & 7]
             if 'r' not in perms:
                 raise Exception("Not readable map from cgc elf not supported")
 
-            #CGCMAP--
-            assert elf_segment.header.p_filesz != 0 or elf_segment.header.p_memsz != 0 
+            # CGCMAP--
+            assert elf_segment.header.p_filesz != 0 or elf_segment.header.p_memsz != 0
             yield((elf_segment.header.p_vaddr,
-                  elf_segment.header.p_memsz,
-                  perms, 
-                  elf_segment.stream.name, elf_segment.header.p_offset, elf_segment.header.p_filesz))
+                   elf_segment.header.p_memsz,
+                   perms,
+                   elf_segment.stream.name, elf_segment.header.p_offset, elf_segment.header.p_filesz))
 
     def threads(self):
         yield(('Running', {'EIP': self.elf.header.e_entry}))
@@ -89,40 +92,38 @@ class CGCElf(Binary):
 class Elf(Binary):
     def __init__(self, filename):
         super(Elf, self).__init__(filename)
-        self.elf = ELFFile(file(filename)) 
-        self.arch = {'x86':'i386','x64':'amd64'}[self.elf.get_machine_arch()]
+        self.elf = ELFFile(file(filename))
+        self.arch = {'x86': 'i386', 'x64': 'amd64'}[self.elf.get_machine_arch()]
         assert self.elf.header.e_type in ['ET_DYN', 'ET_EXEC', 'ET_CORE']
 
-
-        #Get interpreter elf
+        # Get interpreter elf
         self.interpreter = None
         for elf_segment in self.elf.iter_segments():
             if elf_segment.header.p_type != 'PT_INTERP':
                 continue
             self.interpreter = Elf(elf_segment.data()[:-1])
             break
-        if not self.interpreter is None:
+        if self.interpreter is not None:
             assert self.interpreter.arch == self.arch
             assert self.interpreter.elf.header.e_type in ['ET_DYN', 'ET_EXEC']
 
-
     def maps(self):
         for elf_segment in self.elf.iter_segments():
             if elf_segment.header.p_type != 'PT_LOAD' or elf_segment.header.p_memsz == 0:
                 continue
 
             flags = elf_segment.header.p_flags
-            #PF_X 0x1 Execute - PF_W 0x2 Write - PF_R 0x4 Read
-            perms = ['   ', '  x', ' w ', ' wx', 'r  ', 'r x', 'rw ', 'rwx'][flags&7]
+            # PF_X 0x1 Execute - PF_W 0x2 Write - PF_R 0x4 Read
+            perms = ['   ', '  x', ' w ', ' wx', 'r  ', 'r x', 'rw ', 'rwx'][flags & 7]
             if 'r' not in perms:
                 raise Exception("Not readable map from cgc elf not supported")
 
-            #CGCMAP--
-            assert elf_segment.header.p_filesz != 0 or elf_segment.header.p_memsz != 0 
+            # CGCMAP--
+            assert elf_segment.header.p_filesz != 0 or elf_segment.header.p_memsz != 0
             yield((elf_segment.header.p_vaddr,
-                  elf_segment.header.p_memsz,
-                  perms, 
-                  elf_segment.stream.name, elf_segment.header.p_offset, elf_segment.header.p_filesz))
+                   elf_segment.header.p_memsz,
+                   perms,
+                   elf_segment.stream.name, elf_segment.header.p_offset, elf_segment.header.p_filesz))
 
     def getInterpreter(self):
         return self.interpreter
@@ -131,13 +132,11 @@ class Elf(Binary):
         yield(('Running', {'EIP': self.elf.header.e_entry}))
 
 
-Binary.magics= { '\x7fCGC': CGCElf,
-                 '\x7fELF': Elf }
+Binary.magics = {'\x7fCGC': CGCElf,
+                 '\x7fELF': Elf}
 
 
 if __name__ == '__main__':
     import sys
     print list(Binary(sys.argv[1]).threads())
     print list(Binary(sys.argv[1]).maps())
-
-

manticore/core/cpu/abstractcpu.py

@@ -2,8 +2,6 @@ import inspect
 import logging
 import StringIO
 import string
-import sys
-import types
 
 from functools import wraps
 from itertools import islice, imap
@@ -24,44 +22,50 @@ logger = logging.getLogger(__name__)
 register_logger = logging.getLogger('{}.registers'.format(__name__))
 
 ###################################################################################
-#Exceptions
+# Exceptions
+
+
 class CpuException(Exception):
     ''' Base cpu exception '''
-    pass
 
 class DecodeException(CpuException):
     '''
     Raised when trying to decode an unknown or invalid instruction '''
+
     def __init__(self, pc, bytes):
         super(DecodeException, self).__init__("Error decoding instruction @%08x", pc)
-        self.pc=pc
-        self.bytes=bytes
+        self.pc = pc
+        self.bytes = bytes
+
 
 class InstructionNotImplementedError(CpuException):
     '''
     Exception raised when you try to execute an instruction that is not yet
     implemented in the emulator. Add it to the Cpu-specific implementation.
     '''
-    pass
+
 
 class InstructionEmulationError(CpuException):
     '''
     Exception raised when failing to emulate an instruction outside of Manticore.
     '''
-    pass
+
 
 class DivideByZeroError(CpuException):
     ''' A division by zero '''
-    pass
+
 
 class Interruption(CpuException):
     ''' A software interrupt. '''
+
     def __init__(self, N):
-        super(Interruption,self).__init__("CPU Software Interruption %08x", N)
+        super(Interruption, self).__init__("CPU Software Interruption %08x", N)
         self.N = N
 
+
 class Syscall(CpuException):
     ''' '''
+
     def __init__(self):
         super(Syscall, self).__init__("CPU Syscall")
 
@@ -70,6 +74,7 @@ class ConcretizeRegister(CpuException):
     '''
     Raised when a symbolic register needs to be concretized.
     '''
+
     def __init__(self, cpu, reg_name, message=None, policy='MINMAX'):
         self.message = message if message else "Concretizing {}".format(reg_name)
 
@@ -77,18 +82,22 @@ class ConcretizeRegister(CpuException):
         self.reg_name = reg_name
         self.policy = policy
 
+
 class ConcretizeArgument(CpuException):
     '''
     Raised when a symbolic argument needs to be concretized.
     '''
+
     def __init__(self, cpu, argnum, policy='MINMAX'):
-        self.message = "Concretizing argument #%d."%(argnum,)
+        self.message = "Concretizing argument #%d." % (argnum,)
         self.cpu = cpu
         self.policy = policy
         self.argnum = argnum
 
 
 SANE_SIZES = {8, 16, 32, 64, 80, 128, 256}
+
+
 class Operand(object):
     """This class encapsulates how to access operands (regs/mem/immediates) for
     different CPUs
@@ -98,6 +107,7 @@ class Operand(object):
         Auxiliary class wraps capstone operand 'mem' attribute. This will
         return register names instead of Ids
         '''
+
         def __init__(self, parent):
             self.parent = parent
         segment = property(lambda self: self.parent._reg_name(self.parent.op.mem.segment))
@@ -172,6 +182,8 @@ class Operand(object):
 
 #  Basic register file structure not actually need to abstract as it's used
 #  only from the cpu implementation
+
+
 class RegisterFile(object):
     def __init__(self, aliases=None):
         # dict mapping from alias register name ('PC') to actual register
@@ -224,6 +236,7 @@ class RegisterFile(object):
         '''
         return self._alias(register) in self.all_registers
 
+
 class Abi(object):
     '''
     Represents the ability to extract arguments from the environment and write
@@ -231,6 +244,7 @@ class Abi(object):
 
     Used for function call and system call models.
     '''
+
     def __init__(self, cpu):
         '''
         :param manticore.core.cpu.Cpu cpu: CPU to initialize with
@@ -341,7 +355,7 @@ class Abi(object):
 
             # Arguments were lazily computed in case of variadic, so recompute here
             descriptors = self.get_arguments()
-            src = next(islice(descriptors, idx, idx+1))
+            src = next(islice(descriptors, idx, idx + 1))
 
             msg = 'Concretizing due to model invocation'
             if isinstance(src, str):
@@ -356,8 +370,10 @@ class Abi(object):
 
         return result
 
+
 platform_logger = logging.getLogger('manticore.platforms.platform')
 
+
 class SyscallAbi(Abi):
     '''
     A system-call specific ABI.
@@ -411,6 +427,8 @@ class SyscallAbi(Abi):
 
 ############################################################################
 # Abstract cpu encapsulating common cpu methods used by platforms and executor.
+
+
 class Cpu(Eventful):
     '''
     Base class for all Cpu architectures. Functionality common to all
@@ -428,7 +446,7 @@ class Cpu(Eventful):
     '''
 
     _published_events = {'write_register', 'read_register', 'write_memory', 'read_memory', 'decode_instruction',
-                           'execute_instruction'}
+                         'execute_instruction'}
 
     def __init__(self, regfile, memory, **kwargs):
         assert isinstance(regfile, RegisterFile)
@@ -546,7 +564,6 @@ class Cpu(Eventful):
             return self.write_register(name, value)
         object.__setattr__(self, name, value)
 
-
     #############################
     # Memory access
     @property
@@ -573,7 +590,6 @@ class Cpu(Eventful):
 
         self._publish('did_write_memory', where, expression, size)
 
-
     def read_int(self, where, size=None, force=False):
         '''
         Reads int from memory
@@ -589,14 +605,13 @@ class Cpu(Eventful):
         assert size in SANE_SIZES
         self._publish('will_read_memory', where, size)
 
-        data = self._memory.read(where, size/8, force)
+        data = self._memory.read(where, size / 8, force)
         assert (8 * len(data)) == size
         value = Operators.CONCAT(size, *map(Operators.ORD, reversed(data)))
 
         self._publish('did_read_memory', where, value, size)
         return value
 
-
     def write_bytes(self, where, data, force=False):
         '''
         Write a concrete or symbolic (or mixed) buffer to memory
@@ -634,12 +649,12 @@ class Cpu(Eventful):
             limit. This includes the NULL terminator.
         :param force: whether to ignore memory permissions
         '''
-        
+
         if max_length is not None:
-            string = string[:max_length-1]
-        
+            string = string[:max_length - 1]
+
         self.write_bytes(where, string + '\x00', force)
-        
+
     def read_string(self, where, max_length=None, force=False):
         '''
         Read a NUL-terminated concrete buffer from memory. Stops reading at first symbolic byte.
@@ -714,7 +729,6 @@ class Cpu(Eventful):
         self.STACK += self.address_bit_size / 8
         return value
 
-
     #######################################
     # Decoder
     def _wrap_operands(self, operands):
@@ -738,16 +752,16 @@ class Cpu(Eventful):
 
         text = ''
         # Read Instruction from memory
-        for address in xrange(pc, pc+self.max_instr_width):
-            #This reads a byte from memory ignoring permissions
-            #and concretize it if symbolic
+        for address in xrange(pc, pc + self.max_instr_width):
+            # This reads a byte from memory ignoring permissions
+            # and concretize it if symbolic
             if not self.memory.access_ok(address, 'x'):
                 break
 
             c = self.memory[address]
 
             if issymbolic(c):
-                assert isinstance(c, BitVec) and  c.size == 8
+                assert isinstance(c, BitVec) and c.size == 8
                 if isinstance(c, Constant):
                     c = chr(c.value)
                 else:
@@ -758,8 +772,7 @@ class Cpu(Eventful):
                                            policy='INSTRUCTION')
             text += c
 
-
-        #Pad potentially incomplete instruction with zeroes
+        # Pad potentially incomplete instruction with zeroes
 
         code = text.ljust(self.max_instr_width, '\x00')
 
@@ -769,7 +782,7 @@ class Cpu(Eventful):
         except StopIteration as e:
             raise DecodeException(pc, code)
 
-        #Check that the decoded instruction is contained in executable memory
+        # Check that the decoded instruction is contained in executable memory
         if not self.memory.access_ok(slice(pc, pc + insn.size), 'x'):
             logger.info("Trying to execute instructions from non-executable memory")
             raise InvalidMemoryAccess(pc, 'x')
@@ -815,7 +828,7 @@ class Cpu(Eventful):
             return
 
         name = self.canonicalize_instruction_name(insn)
-            
+
         if logger.level == logging.DEBUG:
             logger.debug(self.render_instruction(insn))
             for l in self.render_registers():
@@ -839,7 +852,7 @@ class Cpu(Eventful):
         else:
             self._publish_instruction_as_executed(insn)
 
-    #FIXME(yan): In the case the instruction implementation invokes a system call, we would not be able to
+    # FIXME(yan): In the case the instruction implementation invokes a system call, we would not be able to
     # publish the did_execute_instruction event from here, so we capture and attach it to the syscall
     # exception for the platform to emit it for us once the syscall has successfully been executed.
     def _publish_instruction_as_executed(self, insn):
@@ -862,9 +875,9 @@ class Cpu(Eventful):
             emu.emulate(insn)
         except unicorn.UcError as e:
             if e.errno == unicorn.UC_ERR_INSN_INVALID:
-                text_bytes = ' '.join('%02x'%x for x in insn.bytes)
+                text_bytes = ' '.join('%02x' % x for x in insn.bytes)
                 logger.error("Unimplemented instruction: 0x%016x:\t%s\t%s\t%s",
-                  insn.address, text_bytes, insn.mnemonic, insn.op_str)
+                             insn.address, text_bytes, insn.mnemonic, insn.op_str)
             raise InstructionEmulationError(str(e))
         finally:
             # We have been seeing occasional Unicorn issues with it not clearing
@@ -887,7 +900,7 @@ class Cpu(Eventful):
         value = self.read_register(reg_name)
 
         if issymbolic(value):
-            aux = "%3s: "%reg_name +"%16s"%value
+            aux = "%3s: " % reg_name + "%16s" % value
             result += aux
         elif isinstance(value, (int, long)):
             result += "%3s: 0x%016x" % (reg_name, value)
@@ -903,7 +916,7 @@ class Cpu(Eventful):
         return map(self.render_register,
                    sorted(self._regfile.canonical_registers))
 
-    #Generic string representation
+    # Generic string representation
     def __str__(self):
         '''
         Returns a string representation of cpu state
@@ -915,9 +928,11 @@ class Cpu(Eventful):
         result += '\n'.join(self.render_registers())
         return result
 
-#Instruction decorators
+# Instruction decorators
+
+
 def instruction(old_method):
-    #This should decorate every instruction implementation
+    # This should decorate every instruction implementation
     @wraps(old_method)
     def new_method(cpu, *args, **kw_args):
         cpu.PC += cpu.instruction.size

manticore/core/cpu/arm.py

@@ -180,9 +180,9 @@ class Armv7Operand(Operand):
                 logger.debug("ARM mode PC relative addressing: PC + offset: 0x{:x} + 0x{:x}".format(base, 4))
                 return base + 4
             else:
-                #base currently has the value PC + len(current_instruction)
-                #we need (PC & 0xFFFFFFFC) + 4
-                #thus:
+                # base currently has the value PC + len(current_instruction)
+                # we need (PC & 0xFFFFFFFC) + 4
+                # thus:
                 new_base = (base - self.cpu.instruction.size) & 0xFFFFFFFC
                 logger.debug("THUMB mode PC relative addressing: ALIGN(PC) + offset => 0x{:x} + 0x{:x}".format(new_base, 4))
                 return new_base + 4
@@ -252,10 +252,14 @@ class Armv7RegisterFile(RegisterFile):
                     make_apsr_flag(C, 29) |
                     make_apsr_flag(V, 28))
         else:
-            if N: apsr |= 1 << 31
-            if Z: apsr |= 1 << 30
-            if C: apsr |= 1 << 29
-            if V: apsr |= 1 << 28
+            if N:
+                apsr |= 1 << 31
+            if Z:
+                apsr |= 1 << 30
+            if C:
+                apsr |= 1 << 29
+            if V:
+                apsr |= 1 << 28
         return apsr
 
     def _write_APSR(self, apsr):
@@ -287,7 +291,7 @@ class Armv7RegisterFile(RegisterFile):
     @property
     def all_registers(self):
         return super(Armv7RegisterFile, self).all_registers + \
-               ('R0', 'R1', 'R2', 'R3', 'R4', 'R5', 'R6', 'R7', 'R8', 'R9', 'R10', 'R11', 'R12', 'R13', 'R14', 'R15',
+            ('R0', 'R1', 'R2', 'R3', 'R4', 'R5', 'R6', 'R7', 'R8', 'R9', 'R10', 'R11', 'R12', 'R13', 'R14', 'R15',
                 'D0', 'D1', 'D2', 'D3', 'D4', 'D5', 'D6', 'D7', 'D8', 'D9', 'D10', 'D11', 'D12', 'D13', 'D14', 'D15',
                 'D16', 'D17', 'D18', 'D19', 'D20', 'D21', 'D22', 'D23', 'D24', 'D25', 'D26', 'D27', 'D28', 'D29',
                 'D30', 'D31', 'APSR', 'APSR_N',
@@ -392,6 +396,7 @@ class Armv7Cpu(Cpu):
 
         if issymbolic(new_mode):
             from ..state import Concretize
+
             def set_concrete_mode(state, value):
                 state.cpu.mode = value
             raise Concretize("Concretizing ARMv7 mode", expression=new_mode, setstate=set_concrete_mode)
@@ -759,7 +764,6 @@ class Armv7Cpu(Cpu):
     @instruction
     def PLD(cpu, addr, offset=None):
         """PLD instructs the cpu that the address at addr might be loaded soon."""
-        pass
 
     def _compute_writeback(cpu, operand, offset):
         if offset:
@@ -956,7 +960,7 @@ class Armv7Cpu(Cpu):
         if dest.type == 'immediate':
             logger.debug("swapping mode due to BLX at inst 0x{:x}".format(address))
             cpu._swap_mode()
-        elif dest.type=='register':
+        elif dest.type == 'register':
             cpu._set_mode_by_val(dest.read())
 
     @instruction
@@ -1250,9 +1254,7 @@ class Armv7Cpu(Cpu):
         Used by the the __kuser_dmb ARM Linux user-space handler. This is a nop
         under Manticore's memory and execution model.
         """
-        pass
 
     @instruction
     def LDCL(cpu, *operands):
         """Occasionally used in glibc (longjmp in ld.so). Nop under our execution model."""
-        pass

manticore/core/cpu/binja.py

@@ -1,10 +1,8 @@
 import ctypes
 import logging
 import os
-import re
 
 from collections import defaultdict
-from functools import wraps
 
 import capstone as cs
 
@@ -15,10 +13,12 @@ from .cpufactory import CpuFactory
 from ...core.cpu.disasm import BinjaILDisasm
 from ..smtlib import Operators, BitVecConstant, operator
 from ...utils.helpers import issymbolic
+from functools import reduce
 
 logger = logging.getLogger(__name__)
 register_logger = logging.getLogger('{}.registers'.format(__name__))
 
+
 class BinjaRegisterFile(RegisterFile):
 
     def __init__(self, arch, platform_regs):
@@ -26,12 +26,12 @@ class BinjaRegisterFile(RegisterFile):
         self.arch = arch
         arch = Architecture[arch]
         self.reg_aliases = {
-            'STACK' : str(arch.stack_pointer),
-            'PC' : self.get_pc(),
-            'CS' : 'cs',
-            'SS' : 'ss',
-            'DS' : 'ds',
-            'ES' : 'es'
+            'STACK': str(arch.stack_pointer),
+            'PC': self.get_pc(),
+            'CS': 'cs',
+            'SS': 'ss',
+            'DS': 'ds',
+            'ES': 'es'
         }
         super(BinjaRegisterFile, self).__init__(aliases=self.reg_aliases)
 
@@ -55,7 +55,7 @@ class BinjaRegisterFile(RegisterFile):
 
         # all regs are: architecture, aliases and flags
         all_regs = arch_regs + self.reg_aliases.values() + f_regs
-        self.registers = {reg : 0 for reg in all_regs}
+        self.registers = {reg: 0 for reg in all_regs}
 
         # FIXME get these from the platform!! they are already part of registers
         self.segment_registers = (['cs', 'ds', 'es', 'ss'] +
@@ -146,6 +146,7 @@ class BinjaRegisterFile(RegisterFile):
         else:
             raise NotImplementedError
 
+
 class BinjaOperand(Operand):
     def __init__(self, cpu, parent_il, op, **kwargs):
         self.llil = parent_il
@@ -157,9 +158,9 @@ class BinjaOperand(Operand):
     def type(self):
         from binaryninja import lowlevelil as il
         type_map = {
-            il.ILRegister : 'register',
-            il.LowLevelILInstruction : 'instruction',
-            il.ILFlag : 'flag',
+            il.ILRegister: 'register',
+            il.LowLevelILInstruction: 'instruction',
+            il.ILFlag: 'flag',
         }
 
         try:
@@ -202,22 +203,28 @@ class BinjaOperand(Operand):
     def __getattr__(self, name):
         return getattr(self.op, name)
 
+
 def _carry_ult(left, right):
     return Operators.ULT(left, right)
 
+
 def _adjust_flag(result, left, right):
     return ((left ^ right) ^ result) & 0x10 != 0
 
+
 def _zero_flag(res):
     return res == 0
 
+
 def _sign_flag(res, size):
     mask = 1 << (size - 1)
     return (res & mask) != 0
 
+
 def _parity_flag(v):
     return (v ^ v >> 1 ^ v >> 2 ^ v >> 3 ^ v >> 4 ^ v >> 5 ^ v >> 6 ^ v >> 7) & 1 == 0
 
+
 def _overflow_flag(res, right, left, size):
     mask = 1 << (size - 1)
     sign_r = (right & mask) == mask
@@ -225,12 +232,13 @@ def _overflow_flag(res, right, left, size):
     sign_res = (res & mask) == mask
     return Operators.AND(sign_r ^ sign_l, sign_r ^ sign_res)
 
+
 def binja_platform_regmap(binja_arch_regs, binja_arch_flags, binja_arch_aliases,
                           x86_cpu_regs):
     all_x86_regs = [r.lower() for r in x86_cpu_regs]
 
     # get all registers that are present already in the arch
-    x86_to_binja = {r.upper() : r for r in all_x86_regs
+    x86_to_binja = {r.upper(): r for r in all_x86_regs
                     if r in binja_arch_regs}
 
     # map flag registers
@@ -268,10 +276,12 @@ def binja_platform_regmap(binja_arch_regs, binja_arch_flags, binja_arch_aliases,
 
     return x86_to_binja, binja_to_x86
 
+
 class BinjaCpu(Cpu):
     '''
     A Virtual CPU model for Binary Ninja's IL
     '''
+
     def __init__(self, memory):
         '''
         Builds a CPU model.
@@ -334,9 +344,9 @@ class BinjaCpu(Cpu):
         '''
         text = ''
         # Read Instruction from memory
-        for address in xrange(pc, pc+self.max_instr_width):
-            #This reads a byte from memory ignoring permissions
-            #and concretize it if symbolic
+        for address in xrange(pc, pc + self.max_instr_width):
+            # This reads a byte from memory ignoring permissions
+            # and concretize it if symbolic
             if not self.memory.access_ok(address, 'x'):
                 break
 
@@ -354,8 +364,7 @@ class BinjaCpu(Cpu):
                                            policy='INSTRUCTION')
             text += c
 
-
-        #Pad potentially incomplete instruction with zeroes
+        # Pad potentially incomplete instruction with zeroes
 
         code = text.ljust(self.max_instr_width, '\x00')
 
@@ -365,7 +374,7 @@ class BinjaCpu(Cpu):
         except StopIteration as e:
             raise DecodeException(pc, code)
 
-        #Check that the decoded instruction is contained in executable memory
+        # Check that the decoded instruction is contained in executable memory
         if not self.memory.access_ok(slice(pc, pc + insn.size), 'x'):
             logger.info("Trying to execute instructions from non-executable memory")
             raise InvalidMemoryAccess(pc, 'x')
@@ -402,6 +411,7 @@ class BinjaCpu(Cpu):
             return
 
         name = self.canonicalize_instruction_name(insn)
+
         def fallback_to_emulate(*operands):
             if (isinstance(self.disasm, BinjaILDisasm) and
                     isinstance(insn, cs.CsInsn)):
@@ -411,7 +421,7 @@ class BinjaCpu(Cpu):
                 # XXX after this point self.PC != self._last_pc but that is
                 # OK because we will update the PC  properly
             else:
-                text_bytes = ' '.join('%02x'%x for x in insn.bytes)
+                text_bytes = ' '.join('%02x' % x for x in insn.bytes)
                 logger.info("Unimplemented instruction: 0x%016x:\t%s\t%s\t%s",
                             insn.address, text_bytes, insn.mnemonic, insn.op_str)
 
@@ -421,7 +431,7 @@ class BinjaCpu(Cpu):
 
         implementation = getattr(self, name, fallback_to_emulate)
 
-        if logger.level == logging.DEBUG :
+        if logger.level == logging.DEBUG:
             logger.debug(self.render_instruction(insn))
             for l in self.render_registers():
                 register_logger.debug(l)
@@ -457,7 +467,8 @@ class BinjaCpu(Cpu):
 
     def update_platform_cpu_regs(self):
         for pl_reg, binja_reg in self.regfile.pl2b_map.items():
-            if isinstance(binja_reg, tuple) or binja_reg is None: continue
+            if isinstance(binja_reg, tuple) or binja_reg is None:
+                continue
             self.platform_cpu.write_register(pl_reg,
                                              self.regfile.read(binja_reg))
 
@@ -848,10 +859,10 @@ class BinjaCpu(Cpu):
         rsize = reg.llil.size * 8
         count = shift.read()
         value = reg.read()
-        countMask = {8 : 0x1f,
+        countMask = {8: 0x1f,
                      16: 0x1f,
                      32: 0x1f,
-                     64: 0x3f }[rsize]
+                     64: 0x3f}[rsize]
         temp = Operators.ZEXTEND(count & countMask, rsize)
 
         tempD = value = reg.read()
@@ -940,7 +951,7 @@ class BinjaCpu(Cpu):
         dividend_sign = (dividend & sign_mask) != 0
         divisor_sign = (divisor & sign_mask) != 0
 
-        if isinstance(divisor, (int,long)):
+        if isinstance(divisor, (int, long)):
             if divisor_sign:
                 divisor = ((~divisor) + 1) & mask
                 divisor = -divisor
@@ -952,7 +963,7 @@ class BinjaCpu(Cpu):
 
         quotient = Operators.SDIV(dividend, divisor)
         if (isinstance(dividend, (int, long)) and
-                isinstance(dividend, (int,long))):
+                isinstance(dividend, (int, long))):
             remainder = dividend - (quotient * divisor)
         else:
             remainder = Operators.SREM(dividend, divisor)
@@ -1066,7 +1077,7 @@ class BinjaCpu(Cpu):
         size = left_expr.llil.size * 8
         count = right_expr.read()
         countMask = {
-            8 : 0x1f,
+            8: 0x1f,
             16: 0x1f,
             32: 0x1f,
             64: 0x3f
@@ -1090,10 +1101,10 @@ class BinjaCpu(Cpu):
         # FIXME refactor ROL, ROR
         size = left_expr.llil.size * 8
         count = right_expr.read()
-        countMask = { 8 : 0x1f,
-                      16: 0x1f,
-                      32: 0x1f,
-                      64: 0x3f }[size]
+        countMask = {8: 0x1f,
+                     16: 0x1f,
+                     32: 0x1f,
+                     64: 0x3f}[size]
         tempCount = Operators.ZEXTEND((count & countMask) % (size), size)
 
         value = left_expr.read()
@@ -1104,8 +1115,8 @@ class BinjaCpu(Cpu):
                           Operators.ITE(tempCount != 0,
                                         ((res >> (size - 1)) & 0x1) == 1,
                                         cpu.regfile.read('cf')))
-        s_MSB = ((res >> (size-1)) & 0x1) == 1
-        s_MSB2 = ((res >> (size-2)) & 0x1) == 1
+        s_MSB = ((res >> (size - 1)) & 0x1) == 1
+        s_MSB2 = ((res >> (size - 2)) & 0x1) == 1
         cpu.regfile.write('of',
                           Operators.ITE(tempCount == 1,
                                         s_MSB ^ s_MSB2,
@@ -1206,7 +1217,6 @@ class BinjaCpu(Cpu):
     def ZX(cpu, expr):
         return Operators.ZEXTEND(expr.read(), expr.llil.size * 8)
 
-
     def FALLBACK(cpu, name, *operands):
         """Fallback for unimplemented instructions
         """
@@ -1215,7 +1225,8 @@ class BinjaCpu(Cpu):
                        name)
         # update registers
         for pl_reg, binja_reg in cpu.regfile.pl2b_map.items():
-            if isinstance(binja_reg, tuple) or binja_reg is None: continue
+            if isinstance(binja_reg, tuple) or binja_reg is None:
+                continue
             cpu.platform_cpu.write_register(pl_reg, cpu.regfile.read(binja_reg))
 
         # as well as all the required attributes
@@ -1227,7 +1238,8 @@ class BinjaCpu(Cpu):
 
         # restore registers to BinjaCpu
         for pl_reg, binja_reg in cpu.regfile.pl2b_map.items():
-            if isinstance(binja_reg, tuple) or binja_reg is None: continue
+            if isinstance(binja_reg, tuple) or binja_reg is None:
+                continue
             cpu.regfile.write(binja_reg, cpu.platform_cpu.read_register(pl_reg))
 
 #
@@ -1236,6 +1248,7 @@ class BinjaCpu(Cpu):
 #
 #
 
+
 def x86_get_eflags(cpu, reg):
     def make_symbolic(flag_expr):
         register_size = 32 if reg == 'EFLAGS' else 64
@@ -1266,6 +1279,7 @@ def x86_get_eflags(cpu, reg):
             res += flag << offset
     return res
 
+
 def insn_flags(cpu):
     # FIXME temporary hack due to binja issue with flags
     f = cpu.disasm.current_func
@@ -1276,6 +1290,7 @@ def insn_flags(cpu):
     #  assert mod_flags2 == mod_flags
     return mod_flags
 
+
 def x86_calculate_cmp_flags(cpu, size, res, left_v, right_v):
     mod_flags = insn_flags(cpu)
     if not mod_flags:
@@ -1292,6 +1307,7 @@ def x86_calculate_cmp_flags(cpu, size, res, left_v, right_v):
 
     cpu.update_flags(flags)
 
+
 def x86_update_logic_flags(cpu, result, size):
     mod_flags = insn_flags(cpu)
     if not mod_flags:
@@ -1306,6 +1322,7 @@ def x86_update_logic_flags(cpu, result, size):
     }
     cpu.update_flags(flags)
 
+
 def x86_add(cpu, dest, src, carry=False):
     size = dest.llil.size * 8
     MASK = (1 << size) - 1
@@ -1322,7 +1339,7 @@ def x86_add(cpu, dest, src, carry=False):
         to_add = src_v + cv
 
     res = (dest_v + to_add) & MASK
-    #Affected flags: oszapc
+    # Affected flags: oszapc
     tempCF = Operators.OR(_carry_ult(res, dest_v & MASK),
                           _carry_ult(res, src_v & MASK))
     if carry:
@@ -1331,12 +1348,12 @@ def x86_add(cpu, dest, src, carry=False):
                               Operators.AND(res == MASK,
                                             cpu.regfile.registers['cf']))
     flags = {
-        'c' : tempCF,
-        'a' : _adjust_flag(res, dest_v, src_v),
-        'z' : res == 0,
-        's' : _sign_flag(res, size),
-        'o' : (((dest_v ^ src_v ^ SIGN_MASK) & (res ^ src_v)) & SIGN_MASK) != 0,
-        'p' : _parity_flag(res)
+        'c': tempCF,
+        'a': _adjust_flag(res, dest_v, src_v),
+        'z': res == 0,
+        's': _sign_flag(res, size),
+        'o': (((dest_v ^ src_v ^ SIGN_MASK) & (res ^ src_v)) & SIGN_MASK) != 0,
+        'p': _parity_flag(res)
     }
     cpu.update_flags(flags)
     return res

manticore/core/cpu/bitwise.py

@@ -3,6 +3,7 @@
 from ..smtlib import Operators
 from ..smtlib.expression import BitVec
 
+
 def Mask(width):
     '''
     Return a mask with the low `width` bits set.
@@ -12,6 +13,7 @@ def Mask(width):
     '''
     return (1 << width) - 1
 
+
 def Bit(value, idx):
     '''
     Extract `idx` bit from `value`.
@@ -23,6 +25,7 @@ def Bit(value, idx):
     '''
     return Operators.EXTRACT(value, idx, 1)
 
+
 def GetNBits(value, nbits):
     '''
     Get the first `nbits` from `value`.
@@ -42,6 +45,7 @@ def GetNBits(value, nbits):
         else:
             return Operators.EXTRACT(value, 0, nbits)
 
+
 def SInt(value, width):
     '''
     Convert a bitstring `value` of `width` bits to a signed integer
@@ -53,9 +57,10 @@ def SInt(value, width):
     :return: The converted value
     :rtype int or long or BitVec
     '''
-    return Operators.ITEBV(width, Bit(value, width-1) == 1,
-                                      GetNBits(value, width) - 2**width,
-                                      GetNBits(value, width))
+    return Operators.ITEBV(width, Bit(value, width - 1) == 1,
+                           GetNBits(value, width) - 2**width,
+                           GetNBits(value, width))
+
 
 def UInt(value, width):
     '''
@@ -69,6 +74,7 @@ def UInt(value, width):
     '''
     return GetNBits(value, width)
 
+
 def LSL_C(value, amount, width):
     '''
     The ARM LSL_C (logical left shift with carry) operation.
@@ -81,12 +87,13 @@ def LSL_C(value, amount, width):
     :rtype tuple
     '''
     assert amount > 0
-    value = Operators.ZEXTEND(value, width*2)
+    value = Operators.ZEXTEND(value, width * 2)
     shifted = value << amount
     result = GetNBits(shifted, width)
     carry = Bit(shifted, width)
     return (result, carry)
 
+
 def LSL(value, amount, width):
     '''
     The ARM LSL (logical left shift) operation.
@@ -104,6 +111,7 @@ def LSL(value, amount, width):
     result, _ = LSL_C(value, amount, width)
     return result
 
+
 def LSR_C(value, amount, width):
     '''
     The ARM LSR_C (logical shift right with carry) operation.
@@ -120,6 +128,7 @@ def LSR_C(value, amount, width):
     carry = Bit(value >> (amount - 1), 0)
     return (result, carry)
 
+
 def LSR(value, amount, width):
     '''
     The ARM LSR (logical shift right) operation.
@@ -136,6 +145,7 @@ def LSR(value, amount, width):
     result, _ = LSR_C(value, amount, width)
     return result
 
+
 def ASR_C(value, amount, width):
     '''
     The ARM ASR_C (arithmetic shift right with carry) operation.
@@ -151,10 +161,11 @@ def ASR_C(value, amount, width):
     assert amount > 0
     assert amount + width <= width * 2
     value = Operators.SEXTEND(value, width, width * 2)
-    result = GetNBits(value >>  amount     , width) 
-    carry =  Bit(value, amount - 1)
+    result = GetNBits(value >> amount, width)
+    carry = Bit(value, amount - 1)
     return (result, carry)
 
+
 def ASR(value, amount, width):
     '''
     The ARM ASR (arithmetic shift right) operation.
@@ -172,6 +183,7 @@ def ASR(value, amount, width):
     result, _ = ASR_C(value, amount, width)
     return result
 
+
 def ROR_C(value, amount, width):
     '''
     The ARM ROR_C (rotate right with carry) operation.
@@ -192,6 +204,7 @@ def ROR_C(value, amount, width):
     carry = Bit(result, width - 1)
     return (result, carry)
 
+
 def ROR(value, amount, width):
     '''
     The ARM ROR (rotate right) operation.
@@ -208,6 +221,7 @@ def ROR(value, amount, width):
     result, _ = ROR_C(value, amount, width)
     return result
 
+
 def RRX_C(value, carry, width):
     '''
     The ARM RRX (rotate right with extend and with carry) operation.
@@ -220,9 +234,10 @@ def RRX_C(value, carry, width):
     :rtype tuple
     '''
     carry_out = Bit(value, 0)
-    result = (value >> 1) | (carry << (width-1))
+    result = (value >> 1) | (carry << (width - 1))
     return (result, carry_out)
 
+
 def RRX(value, carry, width):
     '''
     The ARM RRX (rotate right with extend) operation.
@@ -236,4 +251,3 @@ def RRX(value, carry, width):
     '''
     result, _ = RRX_C(value, carry, width)
     return result
-

manticore/core/cpu/cpufactory.py

@@ -1,6 +1,7 @@
 from .x86 import AMD64Cpu, I386Cpu, AMD64LinuxSyscallAbi, I386LinuxSyscallAbi, I386CdeclAbi, SystemVAbi
 from .arm import Armv7Cpu, Armv7CdeclAbi, Armv7LinuxSyscallAbi
 
+
 class CpuFactory(object):
     _cpus = {
         'i386': I386Cpu,
@@ -33,5 +34,3 @@ class CpuFactory(object):
             return Armv7LinuxSyscallAbi(cpu)
         else:
             return NotImplementedError("OS and machine combination not supported: {}/{}".format(os, machine))
-
-

manticore/core/cpu/disasm.py

@@ -2,6 +2,7 @@ from abc import abstractproperty, abstractmethod
 
 import capstone as cs
 
+
 class Instruction(object):
     """Capstone-like instruction to be used internally
     """
@@ -34,6 +35,7 @@ class Instruction(object):
     def name(self):
         pass
 
+
 class Disasm(object):
     """Abstract class for different disassembler interfaces"""
 
@@ -47,7 +49,7 @@ class Disasm(object):
         :param str code: binary blob to be disassembled
         :param long pc: program counter
         """
-        pass
+
 
 class CapstoneDisasm(Disasm):
     def __init__(self, arch, mode):
@@ -67,6 +69,7 @@ class CapstoneDisasm(Disasm):
         """
         return next(self.disasm.disasm(code, pc))
 
+
 class BinjaILDisasm(Disasm):
 
     def __init__(self, view):
@@ -185,7 +188,7 @@ class BinjaILDisasm(Disasm):
             return self.fallback_disasm.disassemble_instruction(code, pc)
         for idx, qil in [(0, il)] + self.il_queue:
             if (any((self.unimplemented(op)
-                    for op in qil.operands if hasattr(qil, "operands"))) or
+                     for op in qil.operands if hasattr(qil, "operands"))) or
                     self.unimplemented(qil)):
                 # clear queue and return from fallback disassembler
                 del self.il_queue[:]
@@ -197,7 +200,6 @@ class BinjaILDisasm(Disasm):
                                        self.disasm_insn_size,
                                        self.current_llil_func)
 
-
     class BinjaILInstruction(Instruction):
         def __init__(self, llil, offset, size, function):
             self.llil = llil
@@ -261,6 +263,7 @@ class BinjaILDisasm(Disasm):
                                           self.llil.operation.name,
                                           self.llil.address)
 
+
 def init_disassembler(disassembler, arch, mode, view=None):
     if disassembler == "capstone":
         return CapstoneDisasm(arch, mode)

manticore/core/cpu/register.py

@@ -1,5 +1,6 @@
 from ..smtlib import Operators, BitVec, Bool
 
+
 class Register(object):
     '''
     Generic variable width register. For 1 bit registers, allows writes of types

manticore/core/executor.py

@@ -1,13 +1,7 @@
-import time
 import os
-import cPickle
 import random
 import logging
 import signal
-try:
-    import cStringIO as StringIO
-except:
-    import StringIO
 
 from ..utils.nointerrupt import WithKeyboardInterruptAs
 from ..utils.event import Eventful
@@ -17,9 +11,13 @@ from workspace import Workspace
 from multiprocessing.managers import SyncManager
 from contextlib import contextmanager
 
-#This is the single global manager that will handle all shared memory among workers
+# This is the single global manager that will handle all shared memory among workers
+
+
 def mgr_init():
     signal.signal(signal.SIGINT, signal.SIG_IGN)
+
+
 manager = SyncManager()
 manager.start(mgr_init)
 
@@ -28,6 +26,7 @@ logger = logging.getLogger(__name__)
 
 def sync(f):
     """ Synchronization decorator. """
+
     def newFunction(self, *args, **kw):
         self._lock.acquire()
         try:
@@ -39,6 +38,7 @@ def sync(f):
 
 class Policy(object):
     ''' Base class for prioritization of state search '''
+
     def __init__(self, executor, *args, **kwargs):
         super(Policy, self).__init__(*args, **kwargs)
         self._executor = executor
@@ -54,7 +54,7 @@ class Policy(object):
             yield policy_context
 
     def _add_state_callback(self, state_id, state):
-        ''' Save summarize(state) on policy shared context before 
+        ''' Save summarize(state) on policy shared context before
             the state is stored
         '''
         summary = self.summarize(state)
@@ -75,19 +75,21 @@ class Policy(object):
             self.context has a dict mapping state_ids -> summarize(state)'''
         raise NotImplementedError
 
+
 class Random(Policy):
     def __init__(self, executor, *args, **kwargs):
         super(Random, self).__init__(executor, *args, **kwargs)
-        random.seed(1337) # For repeatable results
+        random.seed(1337)  # For repeatable results
 
     def choice(self, state_ids):
         return random.choice(state_ids)
 
+
 class Uncovered(Policy):
     def __init__(self, executor, *args, **kwargs):
         super(Uncovered, self).__init__(executor, *args, **kwargs)
-        #hook on the necesary executor signals
-        #on callbacks save data in executor.context['policy']
+        # hook on the necesary executor signals
+        # on callbacks save data in executor.context['policy']
         self._executor.subscribe('will_load_state', self._register)
 
     def _register(self, *args):
@@ -115,6 +117,7 @@ class Uncovered(Policy):
                     interesting.add(_id)
         return random.choice(tuple(interesting))
 
+
 class BranchLimited(Policy):
     def __init__(self, executor, *args, **kwargs):
         super(BranchLimited, self).__init__(executor, *args, **kwargs)
@@ -136,7 +139,7 @@ class BranchLimited(Policy):
 
     def choice(self, state_ids):
         interesting = set(state_ids)
-        with self.locked_context() as policy_ctx: 
+        with self.locked_context() as policy_ctx:
             visited = policy_ctx.get('visited', dict())
             summaries = policy_ctx.get('summaries', dict())
             lst = []
@@ -154,7 +157,6 @@ class BranchLimited(Policy):
             return None
 
 
-
 class Executor(Eventful):
     '''
     The executor guides the execution of a single state, handles state forking
@@ -167,7 +169,6 @@ class Executor(Eventful):
     def __init__(self, initial=None, store=None, policy='random', context=None, **kwargs):
         super(Executor, self).__init__(**kwargs)
 
-
         # Signals / Callbacks handlers will be invoked potentially at different
         # worker processes. State provides a local context to save data.
 
@@ -183,7 +184,7 @@ class Executor(Eventful):
         self._states = manager.list()
 
         # Number of currently running workers. Initially no running workers
-        self._running = manager.Value('i', 0 )
+        self._running = manager.Value('i', 0)
 
         self._workspace = Workspace(self._lock, store)
 
@@ -192,9 +193,9 @@ class Executor(Eventful):
             context = {}
         self._shared_context = manager.dict(context)
 
-        #scheduling priority policy (wip)
-        #Set policy
-        policies = {'random': Random, 
+        # scheduling priority policy (wip)
+        # Set policy
+        policies = {'random': Random,
                     'uncovered': Uncovered,
                     'branchlimited': BranchLimited,
                     }
@@ -210,7 +211,7 @@ class Executor(Eventful):
 
     @contextmanager
     def locked_context(self, key=None, default=dict):
-        ''' Executor context is a shared memory object. All workers share this. 
+        ''' Executor context is a shared memory object. All workers share this.
             It needs a lock. Its used like this:
 
             with executor.context() as context:
@@ -242,7 +243,7 @@ class Executor(Eventful):
             Install forwarding callbacks in state so the events can go up.
             Going up, we prepend state in the arguments.
         '''
-        #Forward all state signals
+        # Forward all state signals
         self.forward_events_from(state, True)
 
     def enqueue(self, state):
@@ -251,14 +252,14 @@ class Executor(Eventful):
             Save state on storage, assigns an id to it, then add it to the
             priority queue
         '''
-        #save the state to secondary storage
+        # save the state to secondary storage
         state_id = self._workspace.save_state(state)
         self.put(state_id)
         self._publish('did_enqueue_state', state_id, state)
         return state_id
 
     def load_workspace(self):
-        #Browse and load states in a workspace in case we are trying to
+        # Browse and load states in a workspace in case we are trying to
         # continue from paused run
         loaded_state_ids = self._workspace.try_loading_workspace()
         if not loaded_state_ids:
@@ -273,20 +274,19 @@ class Executor(Eventful):
     # Synchronization helpers
     @sync
     def _notify_start_run(self):
-        #notify siblings we are about to start a run()
+        # notify siblings we are about to start a run()
         self._running.value += 1
 
     @sync
     def _notify_stop_run(self):
-        #notify siblings we are about to stop this run()
+        # notify siblings we are about to stop this run()
         self._running.value -= 1
         if self._running.value < 0:
             raise SystemExit
         self._lock.notify_all()
 
-
     ################################################
-    #Public API
+    # Public API
     @property
     def running(self):
         ''' Report an estimate  of how many workers are currently running '''
@@ -300,7 +300,6 @@ class Executor(Eventful):
         ''' Returns True if shutdown was requested '''
         return self._shutdown.is_set()
 
-
     ###############################################
     # Priority queue
     @sync
@@ -314,26 +313,26 @@ class Executor(Eventful):
     def get(self):
         ''' Dequeue a state with the max priority '''
 
-        #A shutdown has been requested
+        # A shutdown has been requested
         if self.is_shutdown():
             return None
 
-        #if not more states in the queue lets wait for some forks
+        # if not more states in the queue lets wait for some forks
         while len(self._states) == 0:
-            #if no worker is running bail out
+            # if no worker is running bail out
             if self.running == 0:
                 return None
-            #if a shutdown has been requested bail out
+            # if a shutdown has been requested bail out
             if self.is_shutdown():
                 return None
-            #if there is actually some workers running wait for state forks
+            # if there is actually some workers running wait for state forks
             logger.debug("Waiting for available states")
             self._lock.wait()
 
         state_id = self._policy.choice(list(self._states))
         if state_id is None:
             return None
-        del  self._states[self._states.index(state_id)]
+        del self._states[self._states.index(state_id)]
         return state_id
 
     def list(self):
@@ -349,8 +348,8 @@ class Executor(Eventful):
         :param message: Accompanying message
         '''
 
-        #broadcast test generation. This is the time for other modules
-        #to output whatever helps to understand this testcase
+        # broadcast test generation. This is the time for other modules
+        # to output whatever helps to understand this testcase
         self._publish('will_generate_testcase', state, 'test', message)
 
     def fork(self, state, expression, policy='ALL', setstate=None):
@@ -375,9 +374,9 @@ class Executor(Eventful):
         assert isinstance(expression, Expression)
 
         if setstate is None:
-            setstate = lambda x,y: None
+            setstate = lambda x, y: None
 
-        #Find a set of solutions for expression
+        # Find a set of solutions for expression
         solutions = state.concretize(expression, policy)
 
         if len(solutions) == 1:
@@ -390,21 +389,21 @@ class Executor(Eventful):
 
         self._publish('will_fork_state', state, expression, solutions, policy)
 
-        #Build and enqueue a state for each solution
+        # Build and enqueue a state for each solution
         children = []
         for new_value in solutions:
             with state as new_state:
                 new_state.constrain(expression == new_value)
 
-                #and set the PC of the new state to the concrete pc-dest
+                # and set the PC of the new state to the concrete pc-dest
                 #(or other register or memory address to concrete)
                 setstate(new_state, new_value)
 
                 self._publish('did_fork_state', new_state, expression, new_value, policy)
 
-                #enqueue new_state
+                # enqueue new_state
                 state_id = self.enqueue(new_state)
-                #maintain a list of childres for logging purpose
+                # maintain a list of childres for logging purpose
                 children.append(state_id)
 
         logger.debug("Forking current state into states %r", children)
@@ -414,41 +413,40 @@ class Executor(Eventful):
         '''
         Entry point of the Executor; called by workers to start analysis.
         '''
-        #policy_order=self.policy_order
-        #policy=self.policy
+        # policy_order=self.policy_order
+        # policy=self.policy
         current_state = None
         current_state_id = None
 
         with WithKeyboardInterruptAs(self.shutdown):
-            #notify siblings we are about to start a run
+            # notify siblings we are about to start a run
             self._notify_start_run()
 
-            logger.debug("Starting Manticore Symbolic Emulator Worker (pid %d).",os.getpid())
-
+            logger.debug("Starting Manticore Symbolic Emulator Worker (pid %d).", os.getpid())
 
             while not self.is_shutdown():
                 try:  # handle fatal errors: exceptions in Manticore
                     try:  # handle external (e.g. solver) errors, and executor control exceptions
-                        #select a suitable state to analyze
+                        # select a suitable state to analyze
                         if current_state is None:
                             with self._lock:
-                                #notify siblings we are about to stop this run
+                                # notify siblings we are about to stop this run
                                 self._notify_stop_run()
                                 try:
-                                    #Select a single state_id
+                                    # Select a single state_id
                                     current_state_id = self.get()
-                                    #load selected state from secondary storage
+                                    # load selected state from secondary storage
                                     if current_state_id is not None:
                                         self._publish('will_load_state', current_state_id)
                                         current_state = self._workspace.load_state(current_state_id)
                                         self.forward_events_from(current_state, True)
                                         self._publish('did_load_state', current_state, current_state_id)
                                         logger.info("load state %r", current_state_id)
-                                    #notify siblings we have a state to play with
+                                    # notify siblings we have a state to play with
                                 finally:
                                     self._notify_start_run()
 
-                        #If current_state is still None. We are done.
+                        # If current_state is still None. We are done.
                         if current_state is None:
                             logger.debug("No more states in the queue, byte bye!")
                             break
@@ -456,29 +454,26 @@ class Executor(Eventful):
                         assert current_state is not None
                         assert current_state.constraints is current_state.platform.constraints
 
-
-
                         # Allows to terminate manticore worker on user request
                         while not self.is_shutdown():
                             if not current_state.execute():
                                 break
                         else:
-                            #Notify this worker is done
+                            # Notify this worker is done
                             self._publish('will_terminate_state', current_state, current_state_id, 'Shutdown')
                             current_state = None
 
-
-                    #Handling Forking and terminating exceptions
+                    # Handling Forking and terminating exceptions
                     except Concretize as e:
-                        #expression
-                        #policy
-                        #setstate()
+                        # expression
+                        # policy
+                        # setstate()
 
                         logger.debug("Generic state fork on condition")
                         current_state = self.fork(current_state, e.expression, e.policy, e.setstate)
 
                     except TerminateState as e:
-                        #Notify this worker is done
+                        # Notify this worker is done
                         self._publish('will_terminate_state', current_state, current_state_id, e)
 
                         logger.debug("Generic terminate state")
@@ -491,7 +486,7 @@ class Executor(Eventful):
                         trace = traceback.format_exc()
                         logger.error("Exception: %s\n%s", str(e), trace)
 
-                        #Notify this state is done
+                        # Notify this state is done
                         self._publish('will_terminate_state', current_state, current_state_id, e)
 
                         if solver.check(current_state.constraints):
@@ -502,12 +497,12 @@ class Executor(Eventful):
                     import traceback
                     trace = traceback.format_exc()
                     logger.error("Exception: %s\n%s", str(e), trace)
-                    #Notify this worker is done
+                    # Notify this worker is done
                     self._publish('will_terminate_state', current_state, current_state_id, e)
                     current_state = None
                     logger.setState(None)
 
             assert current_state is None
 
-            #notify siblings we are about to stop this run
+            # notify siblings we are about to stop this run
             self._notify_stop_run()

manticore/core/memory.py

@@ -1,6 +1,5 @@
 from abc import ABCMeta, abstractmethod, abstractproperty
 from weakref import WeakValueDictionary
-from cStringIO import StringIO
 from .smtlib import *
 import logging
 from ..utils.mappings import _mmap, _munmap
@@ -13,6 +12,7 @@ class MemoryException(Exception):
     '''
     Memory exceptions
     '''
+
     def __init__(self, message, address=None):
         '''
         Builds a memory exception.
@@ -33,6 +33,7 @@ class ConcretizeMemory(MemoryException):
     '''
     Raised when a symbolic memory cell needs to be concretized.
     '''
+
     def __init__(self, mem, address, size, policy='MINMAX'):
         self.message = "Concretizing memory address {} size {}".format(address, size)
         self.mem = mem
@@ -57,7 +58,7 @@ class InvalidSymbolicMemoryAccess(InvalidMemoryAccess):
 
     def __init__(self, address, mode, size, constraint):
         super(InvalidSymbolicMemoryAccess, self, ).__init__(address, mode)
-        #the crashing constraint you need to assert
+        # the crashing constraint you need to assert
         self.constraint = constraint
         self.size = size
 
@@ -75,6 +76,7 @@ class Map(object):
 
     '''
     __metaclass__ = ABCMeta
+
     def __init__(self, start, size, perms, name=None):
         '''
         Abstract memory map.
@@ -105,7 +107,7 @@ class Map(object):
         assert isinstance(perms, str) and len(perms) <= 3 and perms.strip() in ['', 'r', 'w', 'x', 'rw', 'r x', 'rx', 'rwx', 'wx', ]
         self._perms = perms
 
-    #Property
+    # Property
     perms = property(_get_perms, _set_perms)
 
     def access_ok(self, access):
@@ -137,7 +139,7 @@ class Map(object):
 
         :rtype: str
         '''
-        return '<%s 0x%016x-0x%016x %s>'%(self.__class__.__name__, self.start, self.end, self.perms)
+        return '<%s 0x%016x-0x%016x %s>' % (self.__class__.__name__, self.start, self.end, self.perms)
 
     def __cmp__(self, other):
         result = cmp(self.start, other.start)
@@ -146,7 +148,7 @@ class Map(object):
         result = cmp(self.end, other.end)
         if result != 0:
             return result
-        # go by each char permission 
+        # go by each char permission
         result = cmp(self.perms, other.perms)
         if result != 0:
             return result
@@ -156,11 +158,11 @@ class Map(object):
         ''' Returns True if index is in range '''
         if isinstance(index, slice):
             in_range = index.start < index.stop and \
-                       index.start >= self.start and \
-                       index.stop <= self.end
+                index.start >= self.start and \
+                index.stop <= self.end
         else:
             in_range = index >= self.start and \
-                       index <= self.end
+                index <= self.end
         return in_range
 
     def _get_offset(self, index):
@@ -175,7 +177,7 @@ class Map(object):
         if not self._in_range(index):
             raise IndexError('Map index out of range')
         if isinstance(index, slice):
-            index = slice(index.start-self.start,  index.stop-self.start)
+            index = slice(index.start - self.start, index.stop - self.start)
         else:
             index -= self.start
         return index
@@ -189,7 +191,6 @@ class Map(object):
         :return: the character or sequence at the specified address.
         :rtype: byte or array
         '''
-        pass
 
     @abstractmethod
     def __setitem__(self, index, value):
@@ -199,8 +200,6 @@ class Map(object):
         :param index: the address or slice where to put the data.
         :param value: byte or sequence of bytes to put in this map.
         '''
-        pass
-
 
     @abstractmethod
     def split(self, address):
@@ -209,11 +208,11 @@ class Map(object):
 
         :param address: The address at which to split the Map.
         '''
-        pass
 
 
 class AnonMap(Map):
     ''' A concrete anonymous memory map '''
+
     def __init__(self, start, size, perms, data_init=None, **kwargs):
         '''
         Builds a concrete anonymous memory map.
@@ -225,7 +224,7 @@ class AnonMap(Map):
         '''
         super(AnonMap, self).__init__(start, size, perms, **kwargs)
         self._data = bytearray(size)
-        if not data_init is None:
+        if data_init is not None:
             assert len(data_init) <= size, 'More initial data than reserved memory'
             self._data[0:len(data_init)] = data_init
 
@@ -239,13 +238,13 @@ class AnonMap(Map):
             return self, None
 
         assert address > self.start and address < self.end
-        head = AnonMap(self.start, address-self.start, self.perms, self[self.start:address])
-        tail = AnonMap(address, self.end-address, self.perms, self[address:self.end])
-        return head,tail
+        head = AnonMap(self.start, address - self.start, self.perms, self[self.start:address])
+        tail = AnonMap(address, self.end - address, self.perms, self[address:self.end])
+        return head, tail
 
     def __setitem__(self, index, value):
         assert not isinstance(index, slice) or \
-               len(value) == index.stop-index.start
+            len(value) == index.stop - index.start
         index = self._get_offset(index)
         self._data[index] = value
 
@@ -300,15 +299,15 @@ class FileMap(Map):
         _munmap(self._data, self._mapped_size)
 
     def __repr__(self):
-        return '<%s [%s+%x] 0x%016x-0x%016x %s>'%(self.__class__.__name__, self._filename, self._offset, self.start, self.end, self.perms)
+        return '<%s [%s+%x] 0x%016x-0x%016x %s>' % (self.__class__.__name__, self._filename, self._offset, self.start, self.end, self.perms)
 
     def __setitem__(self, index, value):
         assert not isinstance(index, slice) or \
-               len(value) == index.stop-index.start
+            len(value) == index.stop - index.start
         index = self._get_offset(index)
         if isinstance(index, slice):
-            for i in xrange(index.stop-index.start):
-                self._overlay[index.start+i] = value[i]
+            for i in xrange(index.stop - index.start):
+                self._overlay[index.start + i] = value[i]
         else:
             self._overlay[index] = value
 
@@ -318,14 +317,14 @@ class FileMap(Map):
                 return self._overlay[offset]
             else:
                 if offset >= self._mapped_size:
-                     return '\x00' # , 'Extra data must initially be zero'
+                    return '\x00'  # , 'Extra data must initially be zero'
                 return self._data[offset]
 
         index = self._get_offset(index)
         if isinstance(index, slice):
             result = []
-            for i in xrange(index.stop-index.start):
-                result.append(get_byte_at_offset(i+index.start))
+            for i in xrange(index.stop - index.start):
+                result.append(get_byte_at_offset(i + index.start))
             return result
         else:
             return get_byte_at_offset(index)
@@ -337,8 +336,8 @@ class FileMap(Map):
             return self, None
 
         assert address > self.start and address <= self.end
-        head = COWMap(self, size=address-self.start)
-        tail = COWMap(self, offset=address-self.start)
+        head = COWMap(self, size=address - self.start)
+        tail = COWMap(self, offset=address - self.start)
         return head, tail
 
 
@@ -346,6 +345,7 @@ class COWMap(Map):
     '''
     Copy-on-write based map.
     '''
+
     def __init__(self, parent, offset=0, perms=None, size=None, **kwargs):
         '''
         A copy on write copy of parent. Writes to the parent after a copy on
@@ -359,12 +359,12 @@ class COWMap(Map):
         assert isinstance(parent, Map)
         assert offset >= 0 and offset < len(parent)
         if size is None:
-            size=len(parent)-offset
-        assert parent.start+offset+size <= parent.end
+            size = len(parent) - offset
+        assert parent.start + offset + size <= parent.end
         if perms is None:
-            perms=parent.perms
+            perms = parent.perms
 
-        super(COWMap, self).__init__(parent.start+offset, size, perms, **kwargs)
+        super(COWMap, self).__init__(parent.start + offset, size, perms, **kwargs)
         self._parent = parent
         self._parent.__setitem__ = False
         self._cow = {}
@@ -372,8 +372,8 @@ class COWMap(Map):
     def __setitem__(self, index, value):
         assert self._in_range(index)
         if isinstance(index, slice):
-            for i in xrange(index.stop-index.start):
-                self._cow[index.start+i] = value[i]
+            for i in xrange(index.stop - index.start):
+                self._cow[index.start + i] = value[i]
         else:
             self._cow[index] = value
 
@@ -401,10 +401,11 @@ class COWMap(Map):
             return self, None
 
         assert address > self.start and address < self.end
-        head = COWMap(self, size=address-self.start)
-        tail = COWMap(self, offset=address-self.start)
+        head = COWMap(self, size=address - self.start)
+        tail = COWMap(self, offset=address - self.start)
         return head, tail
 
+
 class Memory(object):
     __metaclass__ = ABCMeta
 
@@ -412,6 +413,7 @@ class Memory(object):
     The memory manager.
     This class handles all virtual memory mappings and symbolic chunks.
     '''
+
     def __init__(self, maps=None):
         '''
         Builds a memory manager.
@@ -421,7 +423,7 @@ class Memory(object):
             self._maps = set()
         else:
             self._maps = set(maps)
-        self._page2map = WeakValueDictionary()   #{page -> ref{MAP}}
+        self._page2map = WeakValueDictionary()  # {page -> ref{MAP}}
         self._recording_stack = []
         for m in self._maps:
             for i in range(self._page(m.start), self._page(m.end)):
@@ -437,7 +439,7 @@ class Memory(object):
 
     @abstractproperty
     def page_bit_size(self):
-         return 12
+        return 12
 
     @property
     def memory_size(self):
@@ -466,7 +468,7 @@ class Memory(object):
         :param address: the address to calculate its ceil.
         :return: the ceil of C{address}.
         '''
-        return (((address-1)+self.page_size) & ~self.page_mask) & self.memory_mask
+        return (((address - 1) + self.page_size) & ~self.page_mask) & self.memory_mask
 
     def _floor(self, address):
         '''
@@ -504,26 +506,26 @@ class Memory(object):
         '''
         assert size & self.page_mask == 0
         if start is None:
-            end = {32:0xf8000000, 64: 0x0000800000000000}[self.memory_bit_size]
-            start = end-size
+            end = {32: 0xf8000000, 64: 0x0000800000000000}[self.memory_bit_size]
+            start = end - size
         else:
             if start > self.memory_size - size:
-                start =  self.memory_size - size
-            end = start+size
+                start = self.memory_size - size
+            end = start + size
 
         consecutive_free = 0
-        for p in xrange(self._page(end-1),-1,-1):
+        for p in xrange(self._page(end - 1), -1, -1):
             if p not in self._page2map:
                 consecutive_free += 0x1000
             else:
                 consecutive_free = 0
             if consecutive_free >= size:
                 return p << self.page_bit_size
-            counter+=1
-            if counter >= self.memory_size/self.page_size:
+            counter += 1
+            if counter >= self.memory_size / self.page_size:
                 raise MemoryException('Not enough memory')
 
-        return self._search( size, self.memory_size-size, counter  )
+        return self._search(size, self.memory_size - size, counter)
 
     def mmapFile(self, addr, size, perms, filename, offset=0):
         '''
@@ -544,29 +546,29 @@ class Memory(object):
                    - '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.
+        # If addr is NULL, the system determines where to allocate the region.
         assert addr is None or isinstance(addr, (int, long)), 'Address shall be concrete'
         assert addr < self.memory_size, 'Address too big'
         assert size > 0
 
-        #address is rounded down to the nearest multiple of the allocation granularity
+        # 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 value is rounded up to the next page boundary
         size = self._ceil(size)
 
-        #If zero search for a spot
+        # If zero search for a spot
         addr = self._search(size, addr)
 
-        #It should not be allocated
-        for i in xrange(self._page(addr), self._page(addr+size)):
-            assert not i in self._page2map, 'Map already used'
+        # It should not be allocated
+        for i in xrange(self._page(addr), self._page(addr + size)):
+            assert i not in self._page2map, 'Map already used'
 
-        #Create the map
+        # Create the map
         m = FileMap(addr, size, perms, filename, offset)
 
-        #Okay, ready to alloc
+        # Okay, ready to alloc
         self._add(m)
 
         logger.debug('New file-memory map @%x size:%x', addr, size)
@@ -590,29 +592,28 @@ class Memory(object):
         :rtype: int
 
         '''
-        #If addr is NULL, the system determines where to allocate the region.
+        # If addr is NULL, the system determines where to allocate the region.
         assert addr is None or type(addr) in [int, long], 'Address shall be concrete'
         assert addr < self.memory_size, 'Address too big'
 
-
-        #address is rounded down to the nearest multiple of the allocation granularity
-        if addr is not  None:
+        # 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 value is rounded up to the next page boundary
         size = self._ceil(size)
 
-        #If zero search for a spot
+        # If zero search for a spot
         addr = self._search(size, addr)
 
-        #It should not be allocated
-        for i in xrange(self._page(addr), self._page(addr+size)):
-            assert not i in self._page2map, 'Map already used'
+        # It should not be allocated
+        for i in xrange(self._page(addr), self._page(addr + size)):
+            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 )
+        # Create the anonymous map
+        m = AnonMap(start=addr, size=size, perms=perms, data_init=data_init)
 
-        #Okay, ready to alloc
+        # Okay, ready to alloc
         self._add(m)
 
         logger.debug('New memory map @%x size:%x', addr, size)
@@ -621,20 +622,20 @@ class Memory(object):
     def _add(self, m):
         assert isinstance(m, Map)
         assert m not in self._maps
-        assert m.start & self.page_mask ==0
-        assert m.end & self.page_mask ==0
+        assert m.start & self.page_mask == 0
+        assert m.end & self.page_mask == 0
         self._maps.add(m)
-        #updating the page to map translation
+        # updating the page to map translation
         for i in range(self._page(m.start), self._page(m.end)):
             self._page2map[i] = m
 
     def _del(self, m):
         assert isinstance(m, Map)
         assert m in self._maps
-        #remove m pages from the page2maps..
+        # remove m pages from the page2maps..
         for p in xrange(self._page(m.start), self._page(m.end)):
             del self._page2map[p]
-        #remove m from the maps set
+        # remove m from the maps set
         self._maps.remove(m)
 
     def map_containing(self, address):
@@ -670,7 +671,7 @@ class Memory(object):
         return sorted(result)
 
     def __str__(self):
-        return '\n'.join(['%016x-%016x % 4s %08x %s'%(start, end, p, offset, name or '') for start, end, p, offset, name in self.mappings()])
+        return '\n'.join(['%016x-%016x % 4s %08x %s' % (start, end, p, offset, name or '') for start, end, p, offset, name in self.mappings()])
 
     def _maps_in_range(self, start, end):
         '''
@@ -679,7 +680,7 @@ class Memory(object):
 
         # Search for the first matching map
         addr = start
-        while addr < end :
+        while addr < end:
             if addr not in self:
                 addr += self.page_size
             else:
@@ -697,7 +698,7 @@ class Memory(object):
         :param size: the length of the unmapping.
         '''
         start = self._floor(start)
-        end = self._ceil(start+size)
+        end = self._ceil(start + size)
 
         for m in self._maps_in_range(start, end):
             self._del(m)
@@ -709,13 +710,12 @@ class Memory(object):
             if tail:
                 self._add(tail)
 
-
         logger.debug('Unmap memory @%x size:%x', start, size)
 
     def mprotect(self, start, size, perms):
         assert size > 0
         start = self._floor(start)
-        end = self._ceil(start+size)
+        end = self._ceil(start + size)
 
         for m in self._maps_in_range(start, end):
             self._del(m)
@@ -724,7 +724,7 @@ class Memory(object):
             middle, tail = tail.split(end)
 
             assert middle is not None
-            middle.perms=perms
+            middle.perms = perms
             self._add(middle)
 
             if head:
@@ -732,7 +732,7 @@ class Memory(object):
             if tail:
                 self._add(tail)
 
-    #Permissions
+    # Permissions
     def __contains__(self, address):
         return self._page(address) in self._page2map
 
@@ -756,7 +756,7 @@ class Memory(object):
                 if not force and not m.access_ok(access):
                     return False
 
-                until_next_page = min(m.end-addr, index.stop-addr)
+                until_next_page = min(m.end - addr, index.stop - addr)
                 addr += until_next_page
             assert addr == index.stop
             return True
@@ -766,26 +766,25 @@ class Memory(object):
             m = self.map_containing(index)
             return force or m.access_ok(access)
 
-    #write and read potentially symbolic bytes at symbolic indexes
+    # write and read potentially symbolic bytes at symbolic indexes
     def read(self, addr, size, force=False):
-        if not self.access_ok(slice(addr, addr+size), 'r', force):
+        if not self.access_ok(slice(addr, addr + size), 'r', force):
             raise InvalidMemoryAccess(addr, 'r')
 
         assert size > 0
         result = []
-        stop = addr+size
+        stop = addr + size
         p = addr
         while p < stop:
             m = self.map_containing(p)
 
-            _size = min(m.end-p, stop-p)
-            result += m[p:p+_size]
-            p+=_size
+            _size = min(m.end - p, stop - p)
+            result += m[p:p + _size]
+            p += _size
         assert p == stop
 
         return result
 
-
     def push_record_writes(self):
         '''
         Begin recording all writes. Retrieve all writes with `pop_record_writes()`
@@ -832,9 +831,9 @@ class Memory(object):
 
         while addr < stop:
             m = self.map_containing(addr)
-            size = min(m.end-addr, stop-addr)
-            m[addr:addr+size] = buf[addr-start:addr-start+size]
-            addr+=size
+            size = min(m.end - addr, stop - addr)
+            m[addr:addr + size] = buf[addr - start:addr - start + size]
+            addr += size
         assert addr == stop
 
     def _get_size(self, size):
@@ -842,8 +841,8 @@ class Memory(object):
 
     def __setitem__(self, index, value):
         if isinstance(index, slice):
-            size = self._get_size(index.stop-index.start)
-            assert len(value) == size #raise proper Error?
+            size = self._get_size(index.stop - index.start)
+            assert len(value) == size  # raise proper Error?
             self.write(index.start, value)
         else:
             self.write(index, (value,))
@@ -863,6 +862,7 @@ class SMemory(Memory):
 
     :todo: improve comments
     '''
+
     def __init__(self, constraints, symbols=None, *args, **kwargs):
         '''
         Builds a memory.
@@ -879,7 +879,7 @@ class SMemory(Memory):
             self._symbols = dict(symbols)
 
     def __reduce__(self):
-        return (self.__class__, (self.constraints, self._symbols, self._maps, ) )
+        return (self.__class__, (self.constraints, self._symbols, self._maps, ))
 
     @property
     def constraints(self):
@@ -897,7 +897,6 @@ class SMemory(Memory):
         assert isinstance(size, BitVecConstant)
         return size.value
 
-
     def munmap(self, start, size):
         '''
         Deletes the mappings for the specified address range and causes further
@@ -907,10 +906,10 @@ class SMemory(Memory):
         :param start: the starting address to delete.
         :param size: the length of the unmapping.
         '''
-        for addr in xrange(start,start+size):
+        for addr in xrange(start, start + size):
             if addr in self._symbols:
                 del self._symbols[addr]
-        super(SMemory, self).munmap(start,size)
+        super(SMemory, self).munmap(start, size)
 
     def read(self, address, size, force=False):
         '''
@@ -937,33 +936,32 @@ class SMemory(Memory):
 
                 # The force param shouldn't affect this, as this is checking for unmapped reads, not bad perms
                 crashing_condition = True
-                for start, end, perms, offset, name  in self.mappings():
-                    if start <= M+size and end >= m :
+                for start, end, perms, offset, name in self.mappings():
+                    if start <= M + size and end >= m:
                         if 'r' in perms:
-                            crashing_condition = Operators.AND(Operators.OR( (address+size).ult(start), address.uge(end) ), crashing_condition)
+                            crashing_condition = Operators.AND(Operators.OR((address + size).ult(start), address.uge(end)), crashing_condition)
 
                 if solver.can_be_true(self.constraints, crashing_condition):
                     raise InvalidSymbolicMemoryAccess(address, 'r', size, crashing_condition)
 
-
-                #INCOMPLETE Result! We could also fork once for every map
+                # INCOMPLETE Result! We could also fork once for every map
                 logger.info('INCOMPLETE Result! Using the sampled solutions we have as result')
                 condition = False
                 for base in e.solutions:
-                    condition = Operators.OR(address == base, condition )
+                    condition = Operators.OR(address == base, condition)
                 from .state import ForkState
                 raise ForkState("Forking state on incomplete result", condition)
 
-            #So here we have all potential solutions to address
+            # So here we have all potential solutions to address
 
             condition = False
             for base in solutions:
-                condition = Operators.OR(address == base, condition )
+                condition = Operators.OR(address == base, condition)
 
             result = []
-            #consider size ==1 to read following code
+            # consider size ==1 to read following code
             for offset in range(size):
-                #Given ALL solutions for the symbolic address
+                # Given ALL solutions for the symbolic address
                 for base in solutions:
                     addr_value = base + offset
                     byte = Operators.ORD(self.map_containing(addr_value)[addr_value])
@@ -974,13 +972,13 @@ class SMemory(Memory):
                         result[offset] = Operators.ITEBV(8, address == base, byte, result[offset])
                     else:
                         result.append(byte)
-                    assert len(result) == offset+1
+                    assert len(result) == offset + 1
             return map(Operators.CHR, result)
         else:
             result = map(Operators.ORD, super(SMemory, self).read(address, size, force))
             for offset in range(size):
-                if address+offset in self._symbols:
-                    for condition, value in self._symbols[address+offset]:
+                if address + offset in self._symbols:
+                    for condition, value in self._symbols[address + offset]:
                         if condition is True:
                             result[offset] = Operators.ORD(value)
                         else:
@@ -1004,19 +1002,19 @@ class SMemory(Memory):
             for offset in xrange(size):
                 for base in solutions:
                     condition = base == address
-                    self._symbols.setdefault(base+offset, []).append((condition, value[offset]))
+                    self._symbols.setdefault(base + offset, []).append((condition, value[offset]))
         else:
 
             for offset in xrange(size):
                 if issymbolic(value[offset]):
-                    if not self.access_ok(address+offset, 'w', force):
-                        raise InvalidMemoryAccess(address+offset, 'w')
-                    self._symbols[address+offset] = [(True, value[offset])]
+                    if not self.access_ok(address + offset, 'w', force):
+                        raise InvalidMemoryAccess(address + offset, 'w')
+                    self._symbols[address + offset] = [(True, value[offset])]
                 else:
                     # overwrite all previous items
-                    if address+offset in self._symbols:
-                        del self._symbols[address+offset]
-                    super(SMemory, self).write(address+offset, [value[offset]], force)
+                    if address + offset in self._symbols:
+                        del self._symbols[address + offset]
+                    super(SMemory, self).write(address + offset, [value[offset]], force)
 
     def _try_get_solutions(self, address, size, access, max_solutions=0x1000, force=False):
         '''
@@ -1035,7 +1033,7 @@ class SMemory(Memory):
 
         crashing_condition = False
         for base in solutions:
-            if not self.access_ok(slice(base,base+size), access, force):
+            if not self.access_ok(slice(base, base + size), access, force):
                 crashing_condition = Operators.OR(address == base, crashing_condition)
 
         if solver.can_be_true(self.constraints, crashing_condition):
@@ -1044,23 +1042,26 @@ class SMemory(Memory):
         return solutions
 
 
-
 class Memory32(Memory):
     memory_bit_size = 32
     page_bit_size = 12
 
+
 class Memory64(Memory):
     memory_bit_size = 64
     page_bit_size = 12
 
+
 class SMemory32(SMemory):
     memory_bit_size = 32
     page_bit_size = 12
 
+
 class SMemory32L(SMemory):
     memory_bit_size = 32
     page_bit_size = 13
 
+
 class SMemory64(SMemory):
     memory_bit_size = 64
     page_bit_size = 12

manticore/core/parser/__init__.py

@@ -1 +0,0 @@
-from parser import *

manticore/core/parser/parser.py

@@ -1,8 +1,8 @@
 # Minimal INTEL assembler expression calculator
 import ply.yacc as yacc
-import copy,struct
-from ..smtlib import Operators,Bool
-#Lexer
+import copy
+from ..smtlib import Operators, Bool
+# Lexer
 # ------------------------------------------------------------
 # calclex.py
 #
@@ -13,23 +13,23 @@ import ply.lex as lex
 import re
 # List of token names.   This is always required
 tokens = (
-   'NUMBER',
-   'PLUS',
-   'MINUS',
-   'TIMES',
-   'DIVIDE',
-   'AND',
-   'OR',
-   'NEG',
-   'LPAREN',
-   'RPAREN',
-   'LBRAKET',
-   'RBRAKET',
-   'REGISTER',
-   'SEGMENT',
-   'COLOM',
-   'PTR',
-   'TYPE',
+    'NUMBER',
+    'PLUS',
+    'MINUS',
+    'TIMES',
+    'DIVIDE',
+    'AND',
+    'OR',
+    'NEG',
+    'LPAREN',
+    'RPAREN',
+    'LBRAKET',
+    'RBRAKET',
+    'REGISTER',
+    'SEGMENT',
+    'COLOM',
+    'PTR',
+    'TYPE',
     'RSHIFT',
     'LSHIFT',
 
@@ -45,79 +45,86 @@ tokens = (
 )
 
 # Regular expression rules for simple tokens
-t_PLUS    = r'\+'
-t_MINUS   = r'-'
-t_TIMES   = r'\*'
-t_DIVIDE  = r'/'
-t_LPAREN  = r'\('
-t_RPAREN  = r'\)'
-t_LBRAKET  = r'\['
-t_RBRAKET  = r'\]'
-t_COLOM  = r':'
+t_PLUS = r'\+'
+t_MINUS = r'-'
+t_TIMES = r'\*'
+t_DIVIDE = r'/'
+t_LPAREN = r'\('
+t_RPAREN = r'\)'
+t_LBRAKET = r'\['
+t_RBRAKET = r'\]'
+t_COLOM = r':'
 
-t_AND    = r'&'
-t_OR   = r'\|'
-t_NEG   = r'~'
-t_LSHIFT    = r'<<'
-t_RSHIFT   = r'>>'
+t_AND = r'&'
+t_OR = r'\|'
+t_NEG = r'~'
+t_LSHIFT = r'<<'
+t_RSHIFT = r'>>'
 
-t_LAND    = r'&&'
-t_LOR   = r'\|\|'
-t_LNOT   = r'!'
-
-t_EQ   = r'=='
-t_LT   = r'<'
-t_LE   = r'<='
-t_GT   = r'>'
-t_GE   = r'>='
+t_LAND = r'&&'
+t_LOR = r'\|\|'
+t_LNOT = r'!'
 
+t_EQ = r'=='
+t_LT = r'<'
+t_LE = r'<='
+t_GT = r'>'
+t_GE = r'>='
 
 
 re_NUMBER = re.compile(r'^(0x[a-fA-F0-9]+|[a-fA-F0-9]+)$')
 re_REGISTER = re.compile(r'^(EAX|EBX|ECX|EDX|ESI|EDI|ESP|EBP|RAX|RBX|RCX|RDX|RSI|RDI|RSP|RBP|ZF|CF|SF|EFLAGS)$')
 re_SEGMENT = re.compile(r'^(SS|DS|ES|SS|CS)$')
-re_TYPE  = re.compile(r'^(QWORD|DWORD|WORD|BYTE)$')
-re_PTR  = re.compile(r'^PTR$')
+re_TYPE = re.compile(r'^(QWORD|DWORD|WORD|BYTE)$')
+re_PTR = re.compile(r'^PTR$')
 
 # A regular expression rule with some action code
+
+
 def t_TOKEN(t):
     '[a-zA-Z0-9]+'
     #print t.value,t.lexer.lexdata[t.lexer.lexpos-len(t.value):],re_TYPE.match(t.lexer.lexdata,t.lexer.lexpos-len(t.value))
     if re_TYPE.match(t.value):
-        t.type='TYPE'
+        t.type = 'TYPE'
     elif re_PTR.match(t.value):
-        t.type='PTR'
+        t.type = 'PTR'
     elif re_NUMBER.match(t.value):
         if t.value.startswith('0x'):
             t.value = t.value[2:]
-        t.value = int(t.value,16)
-        t.type= 'NUMBER'
+        t.value = int(t.value, 16)
+        t.type = 'NUMBER'
     elif re_REGISTER.match(t.value):
-        t.type= 'REGISTER'
+        t.type = 'REGISTER'
     elif re_SEGMENT.match(t.value):
-        t.type= 'SEGMENT'
+        t.type = 'SEGMENT'
     else:
-        raise Exception("Unknown:<%s>"%t.value)
+        raise Exception("Unknown:<%s>" % t.value)
     return t
 
 # Define a rule so we can track line numbers
+
+
 def t_newline(t):
     r'\n+'
     t.lexer.lineno += len(t.value)
 
+
 # A string containing ignored characters (spaces and tabs)
-t_ignore  = ' \t'
+t_ignore = ' \t'
 
 # Error handling rule
+
+
 def t_error(t):
     print "Illegal character '%s'" % t.value[0]
     t.lexer.skip(1)
 
+
 # Build the lexer
 lexer = lex.lex()
 
 
-#parser
+# parser
 
 
 precedence = (
@@ -129,65 +136,79 @@ precedence = (
 )
 
 
-
 def default_read_memory(address, size):
-    return "READM(%08x,%d)"%(address,size)
+    return "READM(%08x,%d)" % (address, size)
+
+
 def default_read_register(reg):
-    return "REG(%s)"%(reg)
+    return "REG(%s)" % (reg)
+
+
 def default_get_descriptor(selector):
     return (0, 0xfffff000, 'rwx')
 
-default_sizes_32 = { 'QWORD': 8,
-          'DWORD': 4,
-          'WORD': 2,
-          'BYTE': 1 }
 
-default_sizes_64 = { 'QWORD': 8,
-          'DWORD': 4,
-          'WORD': 2,
-          'BYTE': 1 }
-functions = { 'read_memory': default_read_memory,
-              'read_register': default_read_register,
-              'get_descriptor': default_get_descriptor,
-            }
-sizes = copy.copy(default_sizes_32) 
+default_sizes_32 = {'QWORD': 8,
+                    'DWORD': 4,
+                    'WORD': 2,
+                    'BYTE': 1}
+
+default_sizes_64 = {'QWORD': 8,
+                    'DWORD': 4,
+                    'WORD': 2,
+                    'BYTE': 1}
+functions = {'read_memory': default_read_memory,
+             'read_register': default_read_register,
+             'get_descriptor': default_get_descriptor,
+             }
+sizes = copy.copy(default_sizes_32)
+
 
 def p_expression_div(p):
     'expression : expression DIVIDE expression'
     p[0] = p[1] / p[3]
 
+
 def p_expression_mul(p):
     'expression : expression TIMES expression'
     p[0] = p[1] * p[3]
 
+
 def p_expression_plus(p):
     'expression : expression PLUS expression'
     p[0] = p[1] + p[3]
 
+
 def p_expression_minus(p):
     'expression : expression MINUS expression'
     p[0] = p[1] - p[3]
 
+
 def p_expression_and(p):
     'expression : expression AND expression'
     p[0] = p[1] & p[3]
 
+
 def p_expression_or(p):
     'expression : expression OR expression'
     p[0] = p[1] | p[3]
 
+
 def p_expression_neg(p):
     'expression : NEG expression '
     p[0] = ~p[1]
 
+
 def p_expression_lshift(p):
     'expression : expression LSHIFT expression'
     p[0] = p[1] << p[3]
 
+
 def p_expression_rshift(p):
     'expression : expression RSHIFT expression'
     p[0] = p[1] >> p[3]
 
+
 def p_expression_deref(p):
     'expression : TYPE PTR LBRAKET expression RBRAKET'
     size = sizes[p[1]]
@@ -196,6 +217,7 @@ def p_expression_deref(p):
     value = Operators.CONCAT(8 * len(char_list), *reversed(map(Operators.ORD, char_list)))
     p[0] = value
 
+
 def p_expression_derefseg(p):
     'expression : TYPE PTR SEGMENT COLOM LBRAKET expression RBRAKET'
     size = sizes[p[1]]
@@ -207,53 +229,65 @@ def p_expression_derefseg(p):
     value = Operators.CONCAT(8 * len(char_list), *reversed(map(Operators.ORD, char_list)))
     p[0] = value
 
+
 def p_expression_term(p):
     'expression : term'
     p[0] = p[1]
 
+
 def p_factor_expr(p):
     'expression : LPAREN expression RPAREN'
     p[0] = p[2]
 
+
 def p_term_num(p):
     'term : NUMBER'
     p[0] = p[1]
 
+
 def p_term_reg(p):
     'term : REGISTER'
     p[0] = functions['read_register'](p[1])
 
+
 def p_expression_eq(p):
     'expression : expression EQ expression'
     p[0] = p[1] == p[3]
 
+
 def p_expression_land(p):
     'expression : expression LAND expression'
     p[0] = p[1] and p[3]
 
+
 def p_expression_lor(p):
     'expression : expression LOR expression'
     p[0] = p[1] or p[3]
 
+
 def p_expression_lnot(p):
     'expression : LNOT expression'
     p[0] = not p[1]
 
+
 def p_expression_lt(p):
     'expression : expression LT expression'
     #p[0] = p[1] < p[3]
     p[0] = Operators.ULT(p[1], p[3])
 
+
 def p_expression_le(p):
     'expression : expression LE expression'
     #p[0] = p[1] <= p[3]
     p[0] = Operators.ULE(p[1], p[3])
 
+
 def p_expression_gt(p):
     'expression : expression GT expression'
     #p[0] = p[1] > p[3]
     p[0] = Operators.UGT(p[1], p[3])
 
+
 def p_expression_ge(p):
     'expression : expression GE expression'
     #p[0] = p[1] >= p[3]
@@ -262,51 +296,53 @@ def p_expression_ge(p):
 
 # Error rule for syntax errors
 def p_error(p):
-    print "Syntax error in input:",p
+    print "Syntax error in input:", p
 
 # Build the parser
 
+
 parser = yacc.yacc(debug=0, write_tables=0)
 
 
-def parse(expression,read_memory=None,read_register=None,get_descriptor=None,word_size=32):
+def parse(expression, read_memory=None, read_register=None, get_descriptor=None, word_size=32):
     global functions, sizes
 
-    if read_memory != None:
+    if read_memory is not None:
         functions['read_memory'] = read_memory
     else:
         functions['read_memory'] = default_read_memory
 
-    if read_register != None:
+    if read_register is not None:
         functions['read_register'] = read_register
     else:
         functions['read_register'] = default_read_register
 
-    if get_descriptor != None:
+    if get_descriptor is not None:
         functions['get_descriptor'] = get_descriptor
     else:
         functions['get_descriptor'] = default_get_descriptor
 
     if word_size == 32:
-        sizes = copy.copy(default_sizes_32) 
+        sizes = copy.copy(default_sizes_32)
     elif word_size == 64:
-        sizes = copy.copy(default_sizes_64) 
+        sizes = copy.copy(default_sizes_64)
     else:
-        raise Exception ("Not Supported")
-    result = parser.parse(expression,tracking=True)
+        raise Exception("Not Supported")
+    result = parser.parse(expression, tracking=True)
     del functions['read_memory']
     del functions['read_register']
     del functions['get_descriptor']
 
     return result
 
+
 if __name__ == '__main__':
     while True:
-       try:
-           s = raw_input('calc > ')
-       except EOFError:
-           break
-       if not s: continue
-       result = parse(s)
-       print result
-
+        try:
+            s = raw_input('calc > ')
+        except EOFError:
+            break
+        if not s:
+            continue
+        result = parse(s)
+        print result

manticore/core/plugin.py

@@ -32,10 +32,11 @@ class Plugin(object):
             self.manticore.context[plugin_context_name] = {}
         return self.manticore.context[plugin_context_name]
 
-    def __init__(self): 
+    def __init__(self):
         self.manticore = None
         self.last_reg_state = {}
 
+
 def _dict_diff(d1, d2):
     '''
     Produce a dict that includes all the keys in d2 that represent different values in d1, as well as values that
@@ -53,6 +54,7 @@ def _dict_diff(d1, d2):
         d[key] = d2[key]
     return d
 
+
 class Tracer(Plugin):
     def will_start_run_callback(self, state):
         state.context['trace'] = []
@@ -60,6 +62,7 @@ class Tracer(Plugin):
     def did_execute_instruction_callback(self, state, pc, target_pc, instruction):
         state.context['trace'].append(pc)
 
+
 class ExtendedTracer(Plugin):
     def __init__(self):
         '''
@@ -123,6 +126,7 @@ class ExtendedTracer(Plugin):
         }
         state.context[self.context_key].append(entry)
 
+
 class Follower(Plugin):
     def __init__(self, trace):
         self.index = 0
@@ -133,7 +137,7 @@ class Follower(Plugin):
         super(self.__class__, self).__init__()
 
     def add_symbolic_range(self, pc_start, pc_end):
-        self.symbolic_ranges.append((pc_start,pc_end))
+        self.symbolic_ranges.append((pc_start, pc_end))
 
     def get_next(self, type):
         event = self.trace[self.index]
@@ -164,6 +168,7 @@ class Follower(Plugin):
                 if start <= pc <= stop:
                     self.active = False
 
+
 class RecordSymbolicBranches(Plugin):
     def will_start_run_callback(self, state):
         state.context['branches'] = {}
@@ -181,10 +186,11 @@ class RecordSymbolicBranches(Plugin):
         if issymbolic(target_pc):
             state.context['forking_pc'] = True
 
+
 class InstructionCounter(Plugin):
 
     def will_terminate_state_callback(self, state, state_id, ex):
-        if state is None: #FIXME Can it be None?
+        if state is None:  # FIXME Can it be None?
             return
         state_instructions_count = state.context.get('instructions_count', 0)
 
@@ -205,7 +211,7 @@ class InstructionCounter(Plugin):
 
 
 class Visited(Plugin):
-    def __init__(self, coverage_file='visited.txt'): 
+    def __init__(self, coverage_file='visited.txt'):
         super(Visited, self).__init__()
         self.coverage_file = coverage_file
 
@@ -231,7 +237,7 @@ class Visited(Plugin):
     def did_finish_run_callback(self):
         _shared_context = self.manticore.context
         executor_visited = _shared_context.get('visited', set())
-        #Fixme this is duplicated?
+        # Fixme this is duplicated?
         if self.coverage_file is not None:
             with self.manticore._output.save_stream(self.coverage_file) as f:
                 fmt = "0x{:016x}\n"
@@ -239,6 +245,7 @@ class Visited(Plugin):
                     f.write(fmt.format(m))
         logger.info('Coverage: %d different instructions executed', len(executor_visited))
 
+
 class ConcreteTraceFollower(Plugin):
     def __init__(self, source=None):
         '''
@@ -268,19 +275,23 @@ class ConcreteTraceFollower(Plugin):
         if self.saved_flags:
             state.cpu.RFLAGS = self.saved_flags
 
-#TODO document all callbacks
+# TODO document all callbacks
+
+
 class ExamplePlugin(Plugin):
     def will_decode_instruction_callback(self, state, pc):
         logger.info('will_decode_instruction', state, pc)
+
     def will_execute_instruction_callback(self, state, pc, instruction):
         logger.info('will_execute_instruction', state, pc, instruction)
 
     def did_execute_instruction_callback(self, state, pc, target_pc, instruction):
         logger.info('did_execute_instruction', state, pc, target_pc, instruction)
+
     def will_start_run_callback(self, state):
-        ''' Called once at the begining of the run. 
-            state is the initial root state 
-        ''' 
+        ''' Called once at the begining of the run.
+            state is the initial root state
+        '''
         logger.info('will_start_run')
 
     def did_finish_run_callback(self):
@@ -291,36 +302,43 @@ class ExamplePlugin(Plugin):
         logger.info('did_enqueue_state %r %r', state_id, state)
 
     def will_fork_state_callback(self, parent_state, expression, solutions, policy):
-        logger.info('will_fork_state %r %r %r %r',parent_state, expression, solutions, policy)
+        logger.info('will_fork_state %r %r %r %r', parent_state, expression, solutions, policy)
+
     def did_fork_state_callback(self, child_state, expression, new_value, policy):
         logger.info('did_fork_state %r %r %r %r', child_state, expression, new_value, policy)
+
     def did_load_state_callback(self, state, state_id):
         logger.info('did_load_state %r %r', state, state_id)
+
     def did_enqueue_state_callback(self, state, state_id):
         logger.info('did_enqueue_state %r %r', state, state_id)
+
     def will_terminate_state_callback(self, state, state_id, exception):
         logger.info('will_terminate_state %r %r %r', state, state_id, exception)
-    def will_generate_testcase_callback(self,  state, testcase_id, message):
+
+    def will_generate_testcase_callback(self, state, testcase_id, message):
         logger.info('will_generate_testcase %r %r %r', state, testcase_id, message)
 
     def will_read_memory_callback(self, state, where, size):
         logger.info('will_read_memory %r %r %r', state, where, size)
+
     def did_read_memory_callback(self, state, where, value, size):
         logger.info('did_read_memory %r %r %r %r', state, where, value, size)
 
     def will_write_memory_callback(self, state, where, value, size):
         logger.info('will_write_memory %r %r %r', state, where, value, size)
+
     def did_write_memory_callback(self, state, where, value, size):
         logger.info('did_write_memory %r %r %r %r', state, where, value, size)
 
     def will_read_register_callback(self, state, register):
         logger.info('will_read_register %r %r', state, register)
+
     def did_read_register_callback(self, state, register, value):
         logger.info('did_read_register %r %r %r', state, register, value)
 
     def will_write_register_callback(self, state, register, value):
         logger.info('will_write_register %r %r %r', state, register, value)
+
     def did_write_register_callback(self, state, register, value):
         logger.info('did_write_register %r %r %r', state, register, value)
-
-

manticore/core/smtlib/__init__.py

@@ -1,9 +1,7 @@
 from expression import Expression, Bool, BitVec, Array
 from constraints import ConstraintSet
-from functools import wraps
 from solver import *
 import operators as Operators
-import math
 
 
 import logging

manticore/core/smtlib/constraints.py

@@ -1,24 +1,25 @@
 from expression import BitVecVariable, BoolVariable, ArrayVariable, Array, Bool, BitVec, BitVecConstant, BoolConstant, ArrayProxy
 from visitors import GetDeclarations, TranslatorSmtlib, ArithmeticSimplifier, PrettyPrinter, pretty_print, translate_to_smtlib, get_depth, get_variables, arithmetic_simplifier
-import logging, weakref
+import logging
 
 logger = logging.getLogger(__name__)
 
+
 class ConstraintSet(object):
     ''' Constraint Sets
 
         An object containing a set of constraints. Serves also as a factory for
         new variables.
     '''
+
     def __init__(self):
         self._constraints = list()
         self._parent = None
         self._sid = 0
         self._child = None
 
-
     def __reduce__(self):
-        return (self.__class__, ( ), {'_parent': self._parent, '_constraints': self._constraints, '_sid':self._sid} )
+        return (self.__class__, (), {'_parent': self._parent, '_constraints': self._constraints, '_sid': self._sid})
 
     def __enter__(self):
         assert self._child is None
@@ -31,7 +32,6 @@ class ConstraintSet(object):
         self._child._parent = None
         self._child = None
 
-        
     def __len__(self):
         if self._parent is not None:
             return len(self._constraints) + len(self._parent)
@@ -52,7 +52,7 @@ class ConstraintSet(object):
         constraint = arithmetic_simplifier(constraint)
         if isinstance(constraint, BoolConstant) and not constraint.value:
             logger.info("Adding an imposible constant constraint")
-        # If self._child is not None this constraint set has been forked and a 
+        # If self._child is not None this constraint set has been forked and a
         # a derived constraintset may be using this. So we can't add any more
         # constraints to this one. After the child constraintSet is deleted
         # we regain the ability to add constraints.
@@ -86,7 +86,7 @@ class ConstraintSet(object):
                     related_constraints.add(constraint)
                     related_variables |= variables
                     added = True
-                    
+
         result = ''
         for var in related_variables:
             result += var.declaration + '\n'
@@ -99,7 +99,7 @@ class ConstraintSet(object):
 
         for name, exp, smtlib in translator.bindings:
             if isinstance(exp, BitVec):
-                result += '(declare-fun %s () (_ BitVec %d))'%(name, exp.size)
+                result += '(declare-fun %s () (_ BitVec %d))' % (name, exp.size)
             elif isinstance(exp, Bool):
                 result += '(declare-fun %s () Bool)' % name
             elif isinstance(exp, Array):
@@ -124,8 +124,8 @@ class ConstraintSet(object):
         for a in self.constraints:
             try:
                 declarations.visit(a)
-            except:
-                # there recursion limit exceeded problem, 
+            except BaseException:
+                # there recursion limit exceeded problem,
                 # try a slower, iterative solution
                 #logger.info('WARNING: using iterpickle to dump recursive expression')
                 #from utils import iterpickle
@@ -159,7 +159,7 @@ class ConstraintSet(object):
 
         for name, exp, smtlib in translator.bindings:
             if isinstance(exp, BitVec):
-                result += '(declare-fun %s () (_ BitVec %d))'%(name, exp.size)
+                result += '(declare-fun %s () (_ BitVec %d))' % (name, exp.size)
             elif isinstance(exp, Bool):
                 result += '(declare-fun %s () Bool)' % name
             elif isinstance(exp, Array):
@@ -220,5 +220,3 @@ class ConstraintSet(object):
         '''
         name = self._get_new_name(name)
         return ArrayProxy(ArrayVariable(index_bits, index_max, value_bits, name, taint=taint))
-
-

manticore/core/smtlib/expression.py

@@ -1,8 +1,9 @@
-import operator
-import weakref
+from functools import reduce
+
 
 class Expression(object):
     ''' Abstract taintable Expression. '''
+
     def __init__(self, taint=()):
         if self.__class__ is Expression:
             raise TypeError
@@ -12,6 +13,7 @@ class Expression(object):
 
     def __repr__(self):
         return "<%s at %x>" % (type(self).__name__, id(self))
+
     @property
     def is_tainted(self):
         return len(self._taint) != 0
@@ -120,6 +122,7 @@ class Bool(Expression):
     def __nonzero__(self):
         raise NotImplementedError("__nonzero__ for Bool")
 
+
 class BoolVariable(Bool, Variable):
     def __init__(self, name, *args, **kwargs):
         super(BoolVariable, self).__init__(name, *args, **kwargs)
@@ -180,6 +183,7 @@ class BoolITE(BoolOperation):
 
 class BitVec(Expression):
     ''' This adds a bitsize to the Expression class '''
+
     def __init__(self, size, *operands, **kwargs):
         super(BitVec, self).__init__(*operands, **kwargs)
         self.size = size
@@ -245,7 +249,7 @@ class BitVec(Expression):
         return BitVecDiv(self, self.cast(other))
 
     def __floordiv__(self, other):
-        return self /other
+        return self / other
 
     # These methods are called to implement the binary arithmetic operations
     # (+, # -, *, /, %, divmod(), pow(), **, <<, >>, &, ^, |) with reflected
@@ -420,10 +424,12 @@ class BitVecMod(BitVecOperation):
     def __init__(self, a, b, *args, **kwargs):
         super(BitVecMod, self).__init__(a.size, a, b, *args, **kwargs)
 
+
 class BitVecRem(BitVecOperation):
     def __init__(self, a, b, *args, **kwargs):
         super(BitVecRem, self).__init__(a.size, a, b, *args, **kwargs)
 
+
 class BitVecUnsignedRem(BitVecOperation):
     def __init__(self, a, b, *args, **kwargs):
         super(BitVecUnsignedRem, self).__init__(a.size, a, b, *args, **kwargs)
@@ -629,6 +635,7 @@ class ArrayStore(ArrayOperation):
     def byte(self):
         return self.operands[2]
 
+
 class ArrayProxy(Array):
     def __init__(self, array):
         assert isinstance(array, Array)
@@ -663,7 +670,7 @@ class ArrayProxy(Array):
     @property
     def index_bits(self):
         return self._array.index_bits
-    
+
     @property
     def index_max(self):
         return self._array.index_max
@@ -671,7 +678,7 @@ class ArrayProxy(Array):
     @property
     def value_bits(self):
         return self._array.value_bits
-   
+
     @property
     def taint(self):
         return self._array.taint
@@ -691,7 +698,7 @@ class ArrayProxy(Array):
         if stop is None:
             stop = len(self)
         return start, stop
-        
+
     def _get_size(self, index):
         start, stop = self._fix_index(index)
         size = stop - start
@@ -711,13 +718,13 @@ class ArrayProxy(Array):
             new_array = ArrayVariable(self.index_bits, size, self.value_bits, name='%s_b%d_e%d'%(self.name, start, stop), taint=self.taint)
             new_array = ArrayProxy(new_array)
             for i in xrange(size):
-                if self.index_max is not None and not isinstance(i+start, Expression) and i+start >= self.index_max:
+                if self.index_max is not None and not isinstance(i + start, Expression) and i + start >= self.index_max:
                     new_array[i] = 0
                 else:
-                    new_array[i] = self._array.select(start+i)
+                    new_array[i] = self._array.select(start + i)
             return new_array
         else:
-            if self.index_max is not None :
+            if self.index_max is not None:
                 if not isinstance(index, Expression) and index >= self.index_max:
                     raise IndexError
             return self._array.select(index)
@@ -728,7 +735,7 @@ class ArrayProxy(Array):
             size = self._get_size(index)
             assert len(value) == size
             for i in xrange(size):
-                self.store(start+i, value[i])
+                self.store(start + i, value[i])
         else:
             self.store(index, value)
 
@@ -777,7 +784,7 @@ class BitVecZeroExtend(BitVecOperation):
         assert isinstance(size_dest, (int, long))
         assert size_dest >= operand.size
         super(BitVecZeroExtend, self).__init__(size_dest, operand, *args, **kwargs)
-        self.extend = size_dest-operand.size
+        self.extend = size_dest - operand.size
 
 
 class BitVecExtract(BitVecOperation):
@@ -803,5 +810,4 @@ class BitVecITE(BitVecOperation):
         assert isinstance(true_value, BitVec)
         assert isinstance(false_value, BitVec)
         assert true_value.size == false_value.size
-        super(BitVecITE, self).__init__(size, condition, true_value, false_value, *args, **kwargs)  
-
+        super(BitVecITE, self).__init__(size, condition, true_value, false_value, *args, **kwargs)

manticore/core/smtlib/operators.py

@@ -35,6 +35,7 @@ def NOT(a):
         return ~a
     return a == False
 
+
 def AND(a, b, *others):
     if len(others) > 0:
         b = AND(b, others[0], *others[1:])
@@ -65,6 +66,7 @@ def XOR(a, b):
         result = ITE(result != 0, True, False)
     return result
 
+
 def UGT(a, b):
     if isinstance(a, BitVec):
         return a.ugt(b)
@@ -162,6 +164,7 @@ def CONCAT(total_size, *args):
             result = (result << arg_size) | (arg & ((1 << arg_size) - 1))
         return result
 
+
 def ITE(cond, true_value, false_value):
     assert isinstance(true_value, (Bool, bool, BitVec, int, long))
     assert isinstance(false_value, (Bool, bool, BitVec, int, long))
@@ -180,6 +183,7 @@ def ITE(cond, true_value, false_value):
 
     return BoolITE(cond, true_value, false_value)
 
+
 def ITEBV(size, cond, true_value, false_value):
     if isinstance(cond, BitVec):
         cond = cond.Bool()
@@ -204,13 +208,14 @@ def ITEBV(size, cond, true_value, false_value):
         false_value = BitVecConstant(size, false_value)
     return BitVecITE(size, cond, true_value, false_value)
 
+
 def UDIV(dividend, divisor):
     if isinstance(dividend, BitVec):
         return dividend.udiv(divisor)
     elif isinstance(divisor, BitVec):
         return divisor.rudiv(dividend)
     assert dividend >= 0 or divisor > 0  # unsigned-es
-    return dividend/divisor
+    return dividend / divisor
 
 
 def UREM(a, b):
@@ -268,6 +273,5 @@ def SAR(size, a, b):
         sign = tempDest & (1 << (size - 1))
         while tempCount != 0:
             tempDest = (tempDest >> 1) | sign
-            tempCount = tempCount-1
+            tempCount = tempCount - 1
         return tempDest
-

manticore/core/smtlib/solver.py

@@ -3,7 +3,7 @@
 # A solver maintains a companion smtlib capable process connected via stdio.
 # It can be in 4 main states: None, unknown, sat, unsat
 # None      nothing was yet sent to the smtlib process. Al the state is only at the python side
-# unknown   is an error state. Some query sent early was unsuccessful or timed out. Further 
+# unknown   is an error state. Some query sent early was unsuccessful or timed out. Further
 #           interaction with the smtlib process will probably kept beign unknown. An exception is raised.
 # sat       the current set of constraints is satisfiable and has at least one solution
 # unsat     the current set of constraints is impossible
@@ -15,7 +15,6 @@
 
 from subprocess import PIPE, Popen, check_output
 from abc import ABCMeta, abstractmethod
-from copy import copy, deepcopy
 import operators as Operators
 from expression import *
 from constraints import *
@@ -28,20 +27,25 @@ import collections
 
 logger = logging.getLogger(__name__)
 
+
 class Z3NotFoundError(EnvironmentError):
     pass
 
+
 class SolverException(Exception):
     pass
 
+
 class SolverUnknown(SolverException):
     pass
 
+
 class TooManySolutions(SolverException):
     def __init__(self, solutions):
         super(TooManySolutions, self).__init__("Max number of different solutions hit")
         self.solutions = solutions
 
+
 class Solver(object):
     __metaclass__ = ABCMeta
 
@@ -51,12 +55,11 @@ class Solver(object):
 
     @abstractmethod
     def optimize(self, X, operation, M=10000):
-        ''' Iterativelly finds the maximum or minimal value for the operation 
+        ''' Iterativelly finds the maximum or minimal value for the operation
             (Normally Operators.UGT or Operators.ULT)
             :param X: a symbol or expression
             :param M: maximum number of iterations allowed
         '''
-        pass
 
     def check(self, constraints):
         ''' Check if expression can be valid '''
@@ -65,12 +68,10 @@ class Solver(object):
     @abstractmethod
     def can_be_true(self, constraints, expression):
         ''' Check if expression can be valid '''
-        pass
 
     @abstractmethod
     def get_all_values(self, constraints, x, maxcnt=10000, silent=False):
         ''' Returns a list with all the possible values for the symbol x'''
-        pass
 
     @abstractmethod
     def get_value(self, constraints, expression):
@@ -78,7 +79,6 @@ class Solver(object):
             of constraints.
             The current set of assertions must be sat.
             :param val: an expression or symbol '''
-        pass
 
     def max(self, constraints, X, M=10000):
         ''' Iterativelly finds the maximum value for a symbol.
@@ -105,11 +105,14 @@ class Solver(object):
         else:
             return x, x
 
-#FixME move this \/ This configuration should be registered as global config 
+
+# FixME move this \/ This configuration should be registered as global config
 consider_unknown_as_unsat = True
 
 
 Version = collections.namedtuple('Version', 'major minor patch')
+
+
 class Z3Solver(Solver):
     def __init__(self):
         ''' Build a Z3 solver instance.
@@ -117,7 +120,7 @@ class Z3Solver(Solver):
         '''
         super(Z3Solver, self).__init__()
         self._proc = None
-        self._log = '' #this should be enabled only if we are debugging
+        self._log = ''  # this should be enabled only if we are debugging
 
         self.version = self._solver_version()
 
@@ -147,13 +150,13 @@ class Z3Solver(Solver):
         If we
         fail to parse the version, we assume z3's output has changed, meaning it's a newer
         version than what's used now, and therefore ok.
-        
+
         Anticipated version_cmd_output format: 'Z3 version 4.4.2'
                                                'Z3 version 4.4.5 - 64 bit - build hashcode $Z3GITHASH'
 
-    
+
         '''
-        their_version = Version(0,0,0)
+        their_version = Version(0, 0, 0)
         try:
             version_cmd_output = check_output('z3 -version'.split())
         except OSError:
@@ -165,17 +168,16 @@ class Z3Solver(Solver):
             pass
         return their_version
 
-        
     def _start_proc(self):
         ''' Auxiliary method to spawn the external solver process'''
         assert '_proc' not in dir(self) or self._proc is None
         try:
-            self._proc = Popen(self._command.split(' '), stdin=PIPE, stdout=PIPE )
+            self._proc = Popen(self._command.split(' '), stdin=PIPE, stdout=PIPE)
         except OSError:
-            #Z3 was removed from the system in the middle of operation
+            # Z3 was removed from the system in the middle of operation
             raise Z3NotFoundError  # TODO(mark) don't catch this exception in two places
 
-        #run solver specific initializations
+        # run solver specific initializations
         for cfg in self._init:
             self._send(cfg)
 
@@ -188,11 +190,11 @@ class Z3Solver(Solver):
             self._proc.wait()
         try:
             self._proc.kill()
-        except:
+        except BaseException:
             pass
         self._proc = None
 
-    #marshaling/pickle
+    # marshaling/pickle
     def __getstate__(self):
         raise Exception()
 
@@ -203,7 +205,7 @@ class Z3Solver(Solver):
         try:
             self._proc.stdin.writelines(('(exit)\n',))
             self._proc.wait()
-        except Exception,e:
+        except Exception:
             pass
 
     def _reset(self, constraints=None):
@@ -213,25 +215,24 @@ class Z3Solver(Solver):
         else:
             if self.support_reset:
                 self._send("(reset)")
-                
+
                 for cfg in self._init:
                     self._send(cfg)
-            else: 
+            else:
                 self._stop_proc()
                 self._start_proc()
         if constraints is not None:
             self._send(constraints)
 
-
     def _send(self, cmd):
         ''' Send a string to the solver.
             :param cmd: a SMTLIBv2 command (ex. (check-sat))
         '''
-        logger.debug('>%s',cmd)
+        logger.debug('>%s', cmd)
         self._log += str(cmd) + '\n'
         try:
             buf = str(cmd)
-            self._proc.stdin.write(buf+'\n')
+            self._proc.stdin.write(buf + '\n')
         except IOError as e:
             raise SolverException(e)
 
@@ -243,30 +244,30 @@ class Z3Solver(Solver):
         bufl = []
         left = 0
         right = 0
-        buf,l,r = readline()
+        buf, l, r = readline()
         bufl.append(buf)
-        left +=l
-        right+=r
+        left += l
+        right += r
         while left != right:
-            buf,l,r = readline()
+            buf, l, r = readline()
             bufl.append(buf)
-            left +=l
-            right+=r
+            left += l
+            right += r
         buf = ''.join(bufl).strip()
         logger.debug('<%s', buf)
         if '(error' in bufl[0]:
             raise Exception("Error in smtlib: {}".format(bufl[0]))
         return buf
 
-    ## UTILS: check-sat get-value 
+    # UTILS: check-sat get-value
     def _check(self):
         ''' Check the satisfiability of the current state '''
         logger.debug("Solver.check() ")
         start = time.time()
         self._send('(check-sat)')
         _status = self._recv()
-        logger.debug("Check took %s seconds (%s)", time.time()- start, _status)
-        if _status not in ('sat','unsat','unknown'):
+        logger.debug("Check took %s seconds (%s)", time.time() - start, _status)
+        if _status not in ('sat', 'unsat', 'unknown'):
             raise SolverException(_status)
         if consider_unknown_as_unsat:
             if _status == 'unknown':
@@ -282,7 +283,7 @@ class Z3Solver(Solver):
         ''' Auxiliary method to send an assert '''
         assert isinstance(expression, Bool)
         smtlib = translate_to_smtlib(expression)
-        self._send('(assert %s)'%smtlib)
+        self._send('(assert %s)' % smtlib)
 
     def _getvalue(self, expression):
         ''' Ask the solver for one possible assignment for val using current set
@@ -293,7 +294,7 @@ class Z3Solver(Solver):
             return expression
         assert isinstance(expression, Variable)
 
-        self._send('(get-value (%s))'%expression.name)
+        self._send('(get-value (%s))' % expression.name)
         ret = self._recv()
         assert ret.startswith('((') and ret.endswith('))')
 
@@ -315,13 +316,11 @@ class Z3Solver(Solver):
         ''' Recall the last pushed constraint store  and state. '''
         self._send('(pop 1)')
 
-
-
     #@memoized
     def can_be_true(self, constraints, expression):
         ''' Check if two potentially symbolic values can be equal '''
         if isinstance(expression, bool):
-            if expression == False:
+            if not expression:
                 return expression
             else:
                 expression = BoolConstant(expression)
@@ -332,8 +331,7 @@ class Z3Solver(Solver):
             self._reset(temp_cs.related_to(expression))
             return self._check() == 'sat'
 
-
-    #get-all-values min max minmax
+    # get-all-values min max minmax
     #@memoized
     def get_all_values(self, constraints, expression, maxcnt=3000, silent=False):
         ''' Returns a list with all the possible values for the symbol x'''
@@ -350,7 +348,7 @@ class Z3Solver(Solver):
             else:
                 raise NotImplementedError("get_all_values only implemted for Bool and BitVec")
 
-            temp_cs.add(var==expression)
+            temp_cs.add(var == expression)
             self._reset(temp_cs.related_to(var))
 
             result = []
@@ -359,38 +357,38 @@ class Z3Solver(Solver):
                 value = self._getvalue(var)
                 result.append(value)
 
-                # Reset the solver to avoid the incremental mode 
+                # Reset the solver to avoid the incremental mode
                 # Triggered with two consecutive calls to check-sat
                 # Yet, if the number of solution is large, sending back
                 # the whole formula is more expensive
                 if len(result) < 50:
-                    self._reset(temp_cs.related_to(var) )
+                    self._reset(temp_cs.related_to(var))
                     for value in result:
-                        self._assert( var != value )
+                        self._assert(var != value)
                 else:
                     self._assert(var != value)
-                    
+
                 if len(result) >= maxcnt:
                     if silent:
                         # do not throw an exception if set to silent
                         # Default is not silent, assume user knows
                         # what they are doing and will check the size
                         # of returned vals list (previous smtlib behavior)
-                        break 
+                        break
                     else:
                         raise TooManySolutions(result)
             return result
 
     #@memoized
     def optimize(self, constraints, x, goal, M=10000):
-        ''' Iterativelly finds the maximum or minimal value for the operation 
+        ''' Iterativelly finds the maximum or minimal value for the operation
             (Normally Operators.UGT or Operators.ULT)
             :param X: a symbol or expression
             :param M: maximum number of iterations allowed
         '''
         assert goal in ('maximize', 'minimize')
         assert isinstance(x, BitVec)
-        operation = {'maximize':Operators.UGE, 'minimize': Operators.ULE}[goal]
+        operation = {'maximize': Operators.UGE, 'minimize': Operators.ULE}[goal]
 
         with constraints as temp_cs:
             X = temp_cs.new_bitvec(x.size)
@@ -402,8 +400,8 @@ class Z3Solver(Solver):
             if getattr(self, 'support_{}'.format(goal)):
                 self._push()
                 try:
-                    self._assert( operation(X, aux) )
-                    self._send('(%s %s)' % (goal, aux.name) )
+                    self._assert(operation(X, aux))
+                    self._send('(%s %s)' % (goal, aux.name))
                     self._send('(check-sat)')
                     _status = self._recv()
                     if _status not in ('sat', 'unsat', 'unknown'):
@@ -421,7 +419,7 @@ class Z3Solver(Solver):
                         if not (ret.startswith('(') and ret.endswith(')')):
                             raise SolverException('bad output on max, z3 may have been killed')
 
-                        pattern = re.compile('\(objectives.*\((?P<expr>.*) (?P<value>\d*)\).*\).*', re.MULTILINE|re.DOTALL)
+                        pattern = re.compile('\(objectives.*\((?P<expr>.*) (?P<value>\d*)\).*\).*', re.MULTILINE | re.DOTALL)
                         m = pattern.match(ret)
                         expr, value = m.group('expr'), m.group('value')
                         assert expr == aux.name
@@ -431,17 +429,17 @@ class Z3Solver(Solver):
                     self._reset(temp_cs)
                     self._send(aux.declaration)
 
-            operation = {'maximize':Operators.UGT, 'minimize': Operators.ULT}[goal]
-            self._assert( aux == X )
+            operation = {'maximize': Operators.UGT, 'minimize': Operators.ULT}[goal]
+            self._assert(aux == X)
             last_value = None
             i = 0
-            while self._check() == 'sat' :
+            while self._check() == 'sat':
                 last_value = self._getvalue(aux)
                 self._assert(operation(aux, last_value))
                 i = i + 1
                 if (i > M):
                     raise SolverException("Optimizing error, maximum number of iterations was reached")
-            if last_value != None:
+            if last_value is not None:
                 return last_value
             raise SolverException("Optimizing error, unsat or unknown core")
 
@@ -465,14 +463,14 @@ class Z3Solver(Solver):
                 for i in xrange(expression.index_max):
                     subvar = temp_cs.new_bitvec(expression.value_bits)
                     var.append(subvar)
-                    temp_cs.add(subvar==expression[i])
+                    temp_cs.add(subvar == expression[i])
 
                 self._reset(temp_cs)
                 if self._check() != 'sat':
                     raise SolverException('Model is not available')
 
                 for i in xrange(expression.index_max):
-                    self._send('(get-value (%s))'%var[i].name)
+                    self._send('(get-value (%s))' % var[i].name)
                     ret = self._recv()
                     assert ret.startswith('((') and ret.endswith('))')
                     pattern, base = self._get_value_fmt
@@ -488,13 +486,13 @@ class Z3Solver(Solver):
         if self._check() != 'sat':
             raise SolverException('Model is not available')
 
-        self._send('(get-value (%s))'%var.name)
+        self._send('(get-value (%s))' % var.name)
         ret = self._recv()
-        if  not ( ret.startswith('((') and ret.endswith('))') ):
+        if not (ret.startswith('((') and ret.endswith('))')):
             raise SolverException('SMTLIB error parsing response: %s' % ret)
 
         if isinstance(expression, Bool):
-            return {'true':True, 'false':False}[ret[2:-2].split(' ')[1]]
+            return {'true': True, 'false': False}[ret[2:-2].split(' ')[1]]
         if isinstance(expression, BitVec):
             pattern, base = self._get_value_fmt
             m = pattern.match(ret)

manticore/core/smtlib/visitors.py

@@ -1,7 +1,9 @@
 from expression import *
 import logging
+import operator
 logger = logging.getLogger(__name__)
 
+
 class Visitor(object):
     ''' Class/Type Visitor
 
@@ -25,6 +27,7 @@ class Visitor(object):
         visit_Array()
 
     '''
+
     def __init__(self, cache=None, **kwargs):
         super(Visitor, self).__init__()
         self._stack = []
@@ -117,10 +120,12 @@ class Visitor(object):
             return aux
         return type(expression)(*operands, taint=expression.taint)
 
+
 class GetDeclarations(Visitor):
     ''' Simple visitor to collect all variables in an expression or set of
         expressions
     '''
+
     def __init__(self, **kwargs):
         super(GetDeclarations, self).__init__(**kwargs)
         self.variables = set()
@@ -133,15 +138,18 @@ class GetDeclarations(Visitor):
     def result(self):
         return self.variables
 
+
 def get_variables(expression):
     visitor = GetDeclarations()
     visitor.visit(expression)
     return visitor.result
 
+
 class GetDepth(Visitor):
     ''' Simple visitor to collect all variables in an expression or set of
         expressions
     '''
+
     def __init__(self, *args, **kwargs):
         super(GetDepth, self).__init__(*args, **kwargs)
 
@@ -151,20 +159,22 @@ class GetDepth(Visitor):
     def visit_Operation(self, expression, *operands):
         return 1 + max(operands)
 
+
 def get_depth(exp):
     visitor = GetDepth()
     visitor.visit(exp)
     return visitor.result
 
+
 class PrettyPrinter(Visitor):
-    def __init__(self, depth=None,  **kwargs):
+    def __init__(self, depth=None, **kwargs):
         super(PrettyPrinter, self).__init__(**kwargs)
         self.output = ''
         self.indent = 0
         self.depth = depth
 
     def _print(self, s, e=None):
-        self.output += ' '*self.indent + str(s) # + '(%016x)'%hash(e)
+        self.output += ' ' * self.indent + str(s)  # + '(%016x)'%hash(e)
         self.output += '\n'
 
     def visit(self, expression):
@@ -194,7 +204,7 @@ class PrettyPrinter(Visitor):
     def visit_Operation(self, expression, *operands):
         self._print(expression.__class__.__name__, expression)
         self.indent += 2
-        if self.depth is None or self.indent < self.depth*2:
+        if self.depth is None or self.indent < self.depth * 2:
             for o in expression.operands:
                 self.visit(o)
         else:
@@ -203,9 +213,9 @@ class PrettyPrinter(Visitor):
         return ''
 
     def visit_BitVecExtract(self, expression):
-        self._print(expression.__class__.__name__+'{%d:%d}'%(expression.begining,expression.end), expression)
+        self._print(expression.__class__.__name__ + '{%d:%d}' % (expression.begining, expression.end), expression)
         self.indent += 2
-        if self.depth is None or self.indent < self.depth*2:
+        if self.depth is None or self.indent < self.depth * 2:
             for o in expression.operands:
                 self.visit(o)
         else:
@@ -233,30 +243,31 @@ def pretty_print(expression, **kwargs):
     pp.visit(expression)
     return pp.result
 
+
 class ConstantFolderSimplifier(Visitor):
     def __init__(self, **kw):
         super(ConstantFolderSimplifier, self).__init__(**kw)
 
-    operations = {  BitVecAdd : operator.__add__ ,
-                    BitVecSub : operator.__sub__ ,
-                    BitVecMul : operator.__mul__ ,
-                    BitVecDiv : operator.__div__ ,
-                    BitVecShiftLeft : operator.__lshift__ ,
-                    BitVecShiftRight : operator.__rshift__ ,
-                    BitVecAnd : operator.__and__ ,
-                    BitVecOr : operator.__or__ ,
-                    BitVecXor : operator.__xor__ ,
-                    BitVecNot : operator.__not__ ,
-                    BitVecNeg : operator.__invert__ ,
-                    LessThan : operator.__lt__ ,
-                    LessOrEqual : operator.__le__ ,
-                    Equal : operator.__eq__ ,
-                    GreaterThan : operator.__gt__ ,
-                    GreaterOrEqual : operator.__ge__ ,
-                 }
+    operations = {BitVecAdd: operator.__add__,
+                  BitVecSub: operator.__sub__,
+                  BitVecMul: operator.__mul__,
+                  BitVecDiv: operator.__div__,
+                  BitVecShiftLeft: operator.__lshift__,
+                  BitVecShiftRight: operator.__rshift__,
+                  BitVecAnd: operator.__and__,
+                  BitVecOr: operator.__or__,
+                  BitVecXor: operator.__xor__,
+                  BitVecNot: operator.__not__,
+                  BitVecNeg: operator.__invert__,
+                  LessThan: operator.__lt__,
+                  LessOrEqual: operator.__le__,
+                  Equal: operator.__eq__,
+                  GreaterThan: operator.__gt__,
+                  GreaterOrEqual: operator.__ge__,
+                  }
 
     def visit_BitVecConcat(self, expression, *operands):
-        if all( isinstance(o, Constant) for o in operands):
+        if all(isinstance(o, Constant) for o in operands):
             result = 0
             for o in operands:
                 result <<= o.size
@@ -264,16 +275,16 @@ class ConstantFolderSimplifier(Visitor):
             return BitVecConstant(expression.size, result, taint=expression.taint)
 
     def visit_BitVecZeroExtend(self, expression, *operands):
-        if all( isinstance(o, Constant) for o in operands):
+        if all(isinstance(o, Constant) for o in operands):
             return BitVecConstant(expression.size, operands[0].value, taint=expression.taint)
 
     def visit_BitVecExtract(self, expression, *operands):
-        if all( isinstance(o, Constant) for o in expression.operands):
-            value=expression.operands[0].value
+        if all(isinstance(o, Constant) for o in expression.operands):
+            value = expression.operands[0].value
             begining = expression.begining
             end = expression.end
             value = value >> begining
-            mask = 2**(end - begining +1) - 1
+            mask = 2**(end - begining + 1) - 1
             value = value & mask
             return BitVecConstant(expression.size, value, taint=expression.taint)
 
@@ -281,7 +292,7 @@ class ConstantFolderSimplifier(Visitor):
         ''' constant folding, if all operands of an expression are a Constant do the math '''
         operation = self.operations.get(type(expression), None)
         if operation is not None and \
-                all( isinstance(o, Constant) for o in operands) :
+                all(isinstance(o, Constant) for o in operands):
             value = operation(*(x.value for x in operands))
             if isinstance(expression, BitVec):
                 return BitVecConstant(expression.size, value, taint=expression.taint)
@@ -289,7 +300,7 @@ class ConstantFolderSimplifier(Visitor):
                 isinstance(expression, Bool)
                 return BoolConstant(value, taint=expression.taint)
         else:
-            if any( operands[i] is not expression.operands[i] for i in xrange(len(operands))):
+            if any(operands[i] is not expression.operands[i] for i in xrange(len(operands))):
                 expression = type(expression)(*operands, taint=expression.taint)
         return expression
 
@@ -299,26 +310,27 @@ def constant_folder(expression):
     simp.visit(expression)
     return simp.result
 
+
 class ArithmeticSimplifier(Visitor):
     def __init__(self, parent=None, **kw):
         super(ArithmeticSimplifier, self).__init__(**kw)
 
     @staticmethod
-    def _same_constant(a,b):
+    def _same_constant(a, b):
         return isinstance(a, Constant) and\
-           isinstance(b, Constant) and\
+            isinstance(b, Constant) and\
             a.value == b.value or a is b
 
     @staticmethod
     def _changed(expression, operands):
-        if isinstance(expression, Constant) and len(operands)>0:
+        if isinstance(expression, Constant) and len(operands) > 0:
             return True
         arity = len(operands)
-        return any( operands[i] is not expression.operands[i] for i in range(arity))
+        return any(operands[i] is not expression.operands[i] for i in range(arity))
 
     def visit_Operation(self, expression, *operands):
         ''' constant folding, if all operands of an expression are a Constant do the math '''
-        if all( isinstance(o, Constant) for o in operands) :
+        if all(isinstance(o, Constant) for o in operands):
             expression = constant_folder(expression)
         if self._changed(expression, operands):
             expression = self._rebuild(expression, operands)
@@ -331,7 +343,7 @@ class ArithmeticSimplifier(Visitor):
             return expression
 
     def visit_BitVecITE(self, expression, *operands):
-        if isinstance( expression.operands[0], Constant):
+        if isinstance(expression.operands[0], Constant):
             if expression.operands[0].value:
                 return expression.operands[1]
             else:
@@ -358,7 +370,8 @@ class ArithmeticSimplifier(Visitor):
                         new_operands.append(item)
                     bitcount += item.size
             if begining != expression.begining:
-                return BitVecExtract(BitVecConcat(sum(map(lambda x: x.size, new_operands)), *reversed(new_operands)), begining, expression.size, taint=expression.taint)
+                return BitVecExtract(BitVecConcat(sum(map(lambda x: x.size, new_operands)), *reversed(new_operands)),
+                                     begining, expression.size, taint=expression.taint)
 
     def visit_BitVecAdd(self, expression, *operands):
         ''' a + 0  ==> a
@@ -381,7 +394,7 @@ class ArithmeticSimplifier(Visitor):
         left = expression.operands[0]
         right = expression.operands[1]
         if isinstance(left, BitVecAdd):
-            if self._same_constant( left.operands[0], right):
+            if self._same_constant(left.operands[0], right):
                 return left.operands[1]
             elif self._same_constant(left.operands[1], right):
                 return left.operands[0]
@@ -395,7 +408,7 @@ class ArithmeticSimplifier(Visitor):
         '''
         left = expression.operands[0]
         right = expression.operands[1]
-        if isinstance( right, BitVecConstant):
+        if isinstance(right, BitVecConstant):
             if right.value == 0:
                 return left
             elif right.value == left.mask:
@@ -404,11 +417,10 @@ class ArithmeticSimplifier(Visitor):
                 left_left = left.operands[0]
                 left_right = left.operands[1]
                 if isinstance(right, Constant):
-                    return BitVecOr(left_left, (left_right|right), taint=expression.taint)
+                    return BitVecOr(left_left, (left_right | right), taint=expression.taint)
         elif isinstance(left, BitVecConstant):
             return BitVecOr(right, left, taint=expression.taint)
 
-
     def visit_BitVecAnd(self, expression, *operands):
         ''' ct & x => x & ct                move constants to the right
             a & 0 => 0                      remove zero
@@ -427,16 +439,15 @@ class ArithmeticSimplifier(Visitor):
                 left_left = left.operands[0]
                 left_right = left.operands[1]
                 if isinstance(right, Constant):
-                    return BitVecAnd(left_left, left_right&right, taint=expression.taint)
+                    return BitVecAnd(left_left, left_right & right, taint=expression.taint)
             elif isinstance(left, BitVecOr):
                 left_left = left.operands[0]
                 left_right = left.operands[1]
-                return BitVecOr(right&left_left, right&left_right, taint=expression.taint)
+                return BitVecOr(right & left_left, right & left_right, taint=expression.taint)
 
         elif isinstance(left, BitVecConstant):
             return BitVecAnd(right, left, taint=expression.taint)
 
-
     def visit_BitVecShiftLeft(self, expression, *operands):
         ''' a << 0 => a                       remove zero
             a << ct => 0 if ct > sizeof(a)    remove big constant shift
@@ -457,8 +468,8 @@ class ArithmeticSimplifier(Visitor):
         index = expression.index
 
         if isinstance(index, BitVecConstant) \
-            and isinstance(arr, ArrayStore) \
-            and isinstance(arr.index, BitVecConstant):
+                and isinstance(arr, ArrayStore) \
+                and isinstance(arr.index, BitVecConstant):
             if arr.index.value == index.value:
                 return arr.byte
             else:
@@ -469,25 +480,29 @@ class ArithmeticSimplifier(Visitor):
         assert not isinstance(expression, Operation)
         return expression
 
-#FIXME this should forget old expressions lru?
+
+# FIXME this should forget old expressions lru?
 arithmetic_simplifier_cache = {}
+
+
 def arithmetic_simplifier(expression):
-    global arithmetic_simplifier_cache    
+    global arithmetic_simplifier_cache
     simp = ArithmeticSimplifier(cache=arithmetic_simplifier_cache)
     simp.visit(expression, use_fixed_point=True)
     return simp.result
 
+
 class TranslatorSmtlib(Visitor):
     ''' Simple visitor to translate an expression to its smtlib representation
     '''
     unique = 0
+
     def __init__(self, use_bindings=False, *args, **kw):
         assert 'bindings' not in kw
         super(TranslatorSmtlib, self).__init__(*args, **kw)
-        self.use_bindings=use_bindings
+        self.use_bindings = use_bindings
         self._bindings = []
 
-
     def _add_binding(self, expression, smtlib):
         if not self.use_bindings or len(smtlib) <= 10:
             return smtlib
@@ -498,8 +513,8 @@ class TranslatorSmtlib(Visitor):
             if smtlib == smt:
                 return nm #fixme change to dict
         '''
-        TranslatorSmtlib.unique+=1
-        name ='aux%d'% TranslatorSmtlib.unique
+        TranslatorSmtlib.unique += 1
+        name = 'aux%d' % TranslatorSmtlib.unique
 
         self._bindings.append((name, expression, smtlib))
 
@@ -557,9 +572,8 @@ class TranslatorSmtlib(Visitor):
         if expression.size == 1:
             return '#' + bin(expression.value & expression.mask)[1:]
         else:
-            return '#x%0*x' % (int(expression.size/4),
-                                 expression.value & expression.mask)
-
+            return '#x%0*x' % (int(expression.size / 4),
+                               expression.value & expression.mask)
 
     def visit_BoolConstant(self, expression):
         return expression.value and 'true' or 'false'
@@ -591,9 +605,8 @@ class TranslatorSmtlib(Visitor):
         #self._bindings = []
         return output
 
+
 def translate_to_smtlib(expression, **kwargs):
     translator = TranslatorSmtlib(**kwargs)
     translator.visit(expression)
     return translator.result
-
-

manticore/core/state.py

@@ -1,8 +1,5 @@
-import os
 import copy
 import logging
-from collections import OrderedDict
-from weakref import WeakSet
 
 from .smtlib import solver, Bool, ArrayProxy, Array
 from ..utils.helpers import issymbolic
@@ -15,13 +12,14 @@ from ..platforms.platform import *
 
 logger = logging.getLogger(__name__)
 
+
 class StateException(Exception):
     ''' All state related exceptions '''
-    pass
 
 
 class TerminateState(StateException):
     ''' Terminates current state exploration '''
+
     def __init__(self, message, testcase=False):
         super(TerminateState, self).__init__(message)
         self.testcase = testcase
@@ -37,12 +35,13 @@ class Concretize(StateException):
 
     '''
     _ValidPolicies = ['MINMAX', 'ALL', 'SAMPLED', 'ONE']
-    def __init__(self, message, expression, setstate=None, policy='ALL',  **kwargs):
-        assert policy in self._ValidPolicies, "Policy must be one of: %s"%(', '.join(self._ValidPolicies),)
+
+    def __init__(self, message, expression, setstate=None, policy='ALL', **kwargs):
+        assert policy in self._ValidPolicies, "Policy must be one of: %s" % (', '.join(self._ValidPolicies),)
         self.expression = expression
         self.setstate = setstate
         self.policy = policy
-        self.message = "Concretize: %s (Policy: %s)"%(message, policy)
+        self.message = "Concretize: %s (Policy: %s)" % (message, policy)
         super(Concretize, self).__init__(**kwargs)
 
 
@@ -54,6 +53,7 @@ class ForkState(Concretize):
         to the state. So the expression could still by symbolic(but constrained)
         in forked states.
     '''
+
     def __init__(self, message, expression, **kwargs):
         assert isinstance(expression, Bool), 'Need a Bool to fork a state in two states'
         super(ForkState, self).__init__(message, expression, policy='ALL', **kwargs)
@@ -79,11 +79,11 @@ class State(Eventful):
         self._input_symbols = list()
         self._child = None
         self._context = dict()
-        ##################################################################33
+        # 33
         # Events are lost in serialization and fork !!
         self.forward_events_from(platform)
-        
-        #FIXME(felipe) This should go into some event callback in a plugin (start_run?)
+
+        # FIXME(felipe) This should go into some event callback in a plugin (start_run?)
         self._init_context()
 
     def __getstate__(self):
@@ -102,11 +102,11 @@ class State(Eventful):
         self._input_symbols = state['input_symbols']
         self._child = state['child']
         self._context = state['context']
-        ##################################################################33
+        # 33
         # Events are lost in serialization and fork !!
         self.forward_events_from(self._platform)
 
-    #Fixme(felipe) change for with "state.cow_copy() as st_temp":.
+    # Fixme(felipe) change for with "state.cow_copy() as st_temp":.
     def __enter__(self):
         assert self._child is None
         new_state = State(self._constraints.__enter__(), self._platform)
@@ -114,7 +114,7 @@ class State(Eventful):
         new_state._context = copy.deepcopy(self._context)
         self._child = new_state
 
-        #fixme NEW State won't inherit signals (pro: added signals to new_state wont affect parent)
+        # fixme NEW State won't inherit signals (pro: added signals to new_state wont affect parent)
         return new_state
 
     def __exit__(self, ty, value, traceback):
@@ -125,29 +125,31 @@ class State(Eventful):
         try:
             result = self._platform.execute()
 
-        #Instead of State importing SymbolicRegisterException and SymbolicMemoryException
+        # Instead of State importing SymbolicRegisterException and SymbolicMemoryException
         # from cpu/memory shouldn't we import Concretize from linux, cpu, memory ??
         # We are forcing State to have abstractcpu
         except ConcretizeRegister as e:
             expression = self.cpu.read_register(e.reg_name)
+
             def setstate(state, value):
                 state.cpu.write_register(e.reg_name, value)
             raise Concretize(e.message,
-                                expression=expression,
-                                setstate=setstate,
-                                policy=e.policy)
+                             expression=expression,
+                             setstate=setstate,
+                             policy=e.policy)
         except ConcretizeMemory as e:
             expression = self.cpu.read_int(e.address, e.size)
+
             def setstate(state, value):
                 state.cpu.write_int(e.address, value, e.size)
             raise Concretize(e.message,
-                                expression=expression,
-                                setstate=setstate,
-                                policy=e.policy)
+                             expression=expression,
+                             setstate=setstate,
+                             policy=e.policy)
         except MemoryException as e:
             raise TerminateState(e.message, testcase=True)
 
-        #Remove when code gets stable?
+        # Remove when code gets stable?
         assert self.platform.constraints is self.constraints
         return result
 
@@ -270,7 +272,6 @@ class State(Eventful):
         '''
         assert self.constraints == self.platform.constraints
 
-
         vals = []
         if policy == 'MINMAX':
             vals = self._solver.minmax(self._constraints, symbolic)
@@ -297,7 +298,6 @@ class State(Eventful):
         from .smtlib import solver
         return solver
 
-
     def can_be_true(self, expr):
         return self._solver.can_be_true(self._constraints, expr)
 
@@ -356,7 +356,7 @@ class State(Eventful):
         self._platform.invoke_model(model, prefix_args=(self,))
 
     ################################################################################################
-    #The following should be moved to specific class StatePosix?
+    # The following should be moved to specific class StatePosix?
     @property
     def cpu(self):
         return self._platform.current
@@ -365,11 +365,11 @@ class State(Eventful):
     def mem(self):
         return self._platform.current.memory
 
-    #FIXME(felipe) Remove this
+    # FIXME(felipe) Remove this
     def _init_context(self):
         self.context['branches'] = dict()
 
-    #FIXME(felipe) Remove this
+    # FIXME(felipe) Remove this
     def record_branch(self, target):
         branches = self.context['branches']
         branch = (self.cpu._last_pc, target)

manticore/core/workspace.py

@@ -28,6 +28,7 @@ class StateSerializer(object):
     StateSerializer can serialize and deserialize :class:`~manticore.core.state.State` objects from and to
     stream-like objects.
     """
+
     def __init__(self):
         pass
 
@@ -254,7 +255,7 @@ class MemoryStore(Store):
     """
     store_type = 'mem'
 
-    #TODO(yan): Once we get a global config store, check it to make sure
+    # TODO(yan): Once we get a global config store, check it to make sure
     # we're executing in a single-worker or test environment.
 
     def __init__(self, uri=None):
@@ -273,6 +274,7 @@ class MemoryStore(Store):
     def ls(self, glob_str):
         return list(self._data)
 
+
 class RedisStore(Store):
     """
     A redis-backed Manticore workspace
@@ -321,6 +323,7 @@ class RedisStore(Store):
 # This is copied from Executor to not create a dependency on the naming of the lock field
 def sync(f):
     """ Synchronization decorator. """
+
     def new_function(self, *args, **kw):
         self._lock.acquire()
         try:
@@ -412,6 +415,7 @@ class ManticoreOutput(object):
     Invoked only from :class:`manticore.Manticore` from a single parent process, so
     locking is not required.
     """
+
     def __init__(self, desc=None):
         """
         Create an object capable of producing Manticore output.
@@ -439,7 +443,7 @@ class ManticoreOutput(object):
             def open_stream(self, suffix=''):
                 stream_name = '{}_{:08x}.{}'.format(self._prefix, self._num, suffix)
                 return self._ws.save_stream(stream_name)
- 
+
         return Testcase(self, prefix)
 
     @property

manticore/manticore.py

@@ -2,7 +2,6 @@ import os
 import sys
 import time
 import types
-import binascii
 import functools
 import cProfile
 import pstats
@@ -12,13 +11,12 @@ from contextlib import contextmanager
 
 from threading import Timer
 
-#FIXME: remove this three
+# FIXME: remove this three
 import elftools
 from elftools.elf.elffile import ELFFile
 from elftools.elf.sections import SymbolTableSection
 
 from .core.executor import Executor
-from .core.parser import parse
 from .core.state import State, TerminateState
 from .core.smtlib import solver, ConstraintSet
 from .core.workspace import ManticoreOutput
@@ -34,6 +32,7 @@ from .utils import log
 logger = logging.getLogger(__name__)
 log.init_logging()
 
+
 def make_binja(program, disasm, argv, env, symbolic_files, concrete_start=''):
     def _check_disassembler_present(disasm):
         if is_binja_disassembler(disasm):
@@ -56,6 +55,7 @@ def make_binja(program, disasm, argv, env, symbolic_files, concrete_start=''):
     initial_state = State(constraints, platform)
     return initial_state
 
+
 def make_decree(program, concrete_start='', **kwargs):
     constraints = ConstraintSet()
     platform = decree.SDecree(constraints, program)
@@ -68,10 +68,11 @@ def make_decree(program, concrete_start='', **kwargs):
     platform.input.transmit(initial_state.symbolicate_buffer('+'*14, label='RECEIVE'))
     return initial_state
 
-def make_linux(program, argv=None, env=None, symbolic_files=None, concrete_start = ''):
+
+def make_linux(program, argv=None, env=None, symbolic_files=None, concrete_start=''):
     env = {} if env is None else env
     argv = [] if argv is None else argv
-    env = ['%s=%s'%(k,v) for k,v in env.items()]
+    env = ['%s=%s' % (k, v) for k, v in env.items()]
 
     logger.info('Loading program %s', program)
 
@@ -85,10 +86,10 @@ def make_linux(program, argv=None, env=None, symbolic_files=None, concrete_start
         logger.info('Starting with concrete input: %s', concrete_start)
 
     for i, arg in enumerate(argv):
-        argv[i] = initial_state.symbolicate_buffer(arg, label='ARGV%d' % (i+1))
+        argv[i] = initial_state.symbolicate_buffer(arg, label='ARGV%d' % (i + 1))
 
     for i, evar in enumerate(env):
-        env[i] = initial_state.symbolicate_buffer(evar, label='ENV%d' % (i+1))
+        env[i] = initial_state.symbolicate_buffer(evar, label='ENV%d' % (i + 1))
 
     # If any of the arguments or environment refer to symbolic values, re-
     # initialize the stack
@@ -97,7 +98,7 @@ def make_linux(program, argv=None, env=None, symbolic_files=None, concrete_start
 
     platform.input.write(concrete_start)
 
-    #set stdin input...
+    # set stdin input...
     platform.input.write(initial_state.symbolicate_buffer('+' * 256,
                                                           label='STDIN'))
     return initial_state
@@ -122,6 +123,7 @@ def make_initial_state(binary_path, **kwargs):
         raise NotImplementedError("Binary {} not supported.".format(binary_path))
     return state
 
+
 class Manticore(Eventful):
     '''
     The central analysis object.
@@ -154,17 +156,15 @@ class Manticore(Eventful):
                 raise Exception('Invalid workspace')
             ws_path = None
 
-
-
         self._output = ManticoreOutput(ws_path)
         self._context = {}
 
-        #sugar for 'will_execute_instruction"
+        # sugar for 'will_execute_instruction"
         self._hooks = {}
         self._executor = Executor(store=self._output.store, policy=policy)
         self._workers = []
 
-        #Link Executor events to default callbacks in manticore object
+        # Link Executor events to default callbacks in manticore object
         self.forward_events_from(self._executor)
 
         if isinstance(path_or_state, str):
@@ -181,24 +181,23 @@ class Manticore(Eventful):
 
         self.plugins = set()
 
-        #Move the folowing into a plugin
+        # Move the folowing into a plugin
         self._assertions = {}
         self._coverage_file = None
         self.trace = None
 
-        #FIXME move the folowing to aplugin
+        # FIXME move the folowing to aplugin
         self.subscribe('will_generate_testcase', self._generate_testcase_callback)
         self.subscribe('did_finish_run', self._did_finish_run_callback)
 
-        #Default plugins for now.. FIXME?
+        # Default plugins for now.. FIXME?
         self.register_plugin(InstructionCounter())
         self.register_plugin(Visited())
         self.register_plugin(Tracer())
         self.register_plugin(RecordSymbolicBranches())
 
-
     def register_plugin(self, plugin):
-        #Global enumeration of valid events
+        # Global enumeration of valid events
         assert isinstance(plugin, Plugin)
         assert plugin not in self.plugins, "Plugin instance already registered"
         assert plugin.manticore is None, "Plugin instance already owned"
@@ -208,42 +207,40 @@ class Manticore(Eventful):
 
         events = Eventful.all_events()
         prefix = Eventful.prefixes
-        all_events = [x+y for x, y in itertools.product(prefix, events)]
+        all_events = [x + y for x, y in itertools.product(prefix, events)]
         for event_name in all_events:
             callback_name = '{}_callback'.format(event_name)
             callback = getattr(plugin, callback_name, None)
             if callback is not None:
                 self.subscribe(event_name, callback)
 
-        #Safety checks
+        # Safety checks
         for callback_name in dir(plugin):
             if callback_name.endswith('_callback'):
                 event_name = callback_name[:-9]
                 if event_name not in all_events:
-                    logger.warning("There is no event named %s for callback on plugin %s", event_name, type(plugin).__name__ )
+                    logger.warning("There is no event named %s for callback on plugin %s", event_name, type(plugin).__name__)
 
         for event_name in all_events:
             for plugin_method_name in dir(plugin):
                 if event_name in plugin_method_name:
-                    if not plugin_method_name.endswith('_callback') :
+                    if not plugin_method_name.endswith('_callback'):
                         if plugin_method_name.startswith('on_') or \
                            plugin_method_name.startswith('will_') or \
                            plugin_method_name.startswith('did_'):
-                            logger.warning("Plugin methods named '%s()' should end with '_callback' on plugin %s", plugin_method_name, type(plugin).__name__ )
+                            logger.warning("Plugin methods named '%s()' should end with '_callback' on plugin %s", plugin_method_name, type(plugin).__name__)
                     if plugin_method_name.endswith('_callback') and \
-                        not plugin_method_name.startswith('on_') and \
-                        not plugin_method_name.startswith('will_') and \
-                        not plugin_method_name.startswith('did_'):
-                            logger.warning("Plugin methods named '%s()' should start with 'on_', 'will_' or 'did_' on plugin %s", plugin_method_name, type(plugin).__name__)
-
+                            not plugin_method_name.startswith('on_') and \
+                            not plugin_method_name.startswith('will_') and \
+                            not plugin_method_name.startswith('did_'):
+                        logger.warning("Plugin methods named '%s()' should start with 'on_', 'will_' or 'did_' on plugin %s",
+                                       plugin_method_name, type(plugin).__name__)
 
     def unregister_plugin(self, plugin):
         assert plugin in self.plugins, "Plugin instance not registered"
         self.plugins.remove(plugin)
         plugin.manticore = None
 
-
-
     @classmethod
     def linux(cls, path, argv=None, envp=None, symbolic_files=None, concrete_start='', **kwargs):
         """
@@ -291,9 +288,9 @@ class Manticore(Eventful):
         :return: Manticore instance, initialized with a EVM State
         :rtype: Manticore
         """
-        #Make the constraint store
+        # Make the constraint store
         constraints = ConstraintSet()
-        #make the ethereum world state
+        # make the ethereum world state
         world = evm.EVMWorld(constraints)
         return cls(State(constraints, world), **kwargs)
 
@@ -303,9 +300,9 @@ class Manticore(Eventful):
 
     def subscribe(self, name, callback):
         from types import MethodType
-        if not isinstance(callback,MethodType):
+        if not isinstance(callback, MethodType):
             callback = MethodType(callback, self)
-        super(Manticore,self).subscribe(name, callback)
+        super(Manticore, self).subscribe(name, callback)
 
     @property
     def context(self):
@@ -316,7 +313,6 @@ class Manticore(Eventful):
             logger.warning("Using shared context without a lock")
             return self._executor._shared_context
 
-
     @contextmanager
     def locked_context(self, key=None, value_type=list):
         """
@@ -344,7 +340,7 @@ class Manticore(Eventful):
 
         @contextmanager
         def _real_context():
-            if not self.running :
+            if not self.running:
                 yield self._context
             else:
                 with self._executor.locked_context() as context:
@@ -418,7 +414,6 @@ class Manticore(Eventful):
             while len(self._workers) > 0:
                 self._workers.pop().join()
 
-
     ############################################################################
     # Common hooks + callback
     ############################################################################
@@ -485,7 +480,7 @@ class Manticore(Eventful):
     ############################################################################
 
     def apply_model_hooks(self, path):
-        #TODO(yan): Simplify the partial function application
+        # TODO(yan): Simplify the partial function application
 
         # Imported straight from __main__.py; this will be re-written once the new
         # event code is in place.
@@ -500,14 +495,14 @@ class Manticore(Eventful):
                 name_parts = name.split('.')
                 importlib.import_module(".platforms.{}".format(name_parts[0]), 'manticore')
                 for n in name_parts:
-                    fmodel = getattr(fmodel,n)
+                    fmodel = getattr(fmodel, n)
                 assert fmodel != platforms
+
                 def cb_function(state):
                     state.platform.invoke_model(fmodel, prefix_args=(state.platform,))
-                self._model_hooks.setdefault(int(address,0), set()).add(cb_function)
+                self._model_hooks.setdefault(int(address, 0), set()).add(cb_function)
                 self._executor.subscribe('will_execute_instruction', self._model_hook_callback)
 
-
     def _model_hook_callback(self, state, instruction):
         pc = state.cpu.PC
         if pc not in self._model_hooks:
@@ -516,7 +511,6 @@ class Manticore(Eventful):
         for cb in self._model_hooks[pc]:
             cb(state)
 
-
     ############################################################################
     # Assertion hooks + callback
     ############################################################################
@@ -534,26 +528,25 @@ class Manticore(Eventful):
         if pc not in self._assertions:
             return
 
-        from core.parser import parse
+        from .core.parser.parser import parse
 
         program = self._assertions[pc]
 
-        #This will interpret the buffer specification written in INTEL ASM.
+        # This will interpret the buffer specification written in INTEL ASM.
         # (It may dereference pointers)
         assertion = parse(program, state.cpu.read_int, state.cpu.read_register)
         if not solver.can_be_true(state.constraints, assertion):
             logger.info(str(state.cpu))
             logger.info("Assertion %x -> {%s} does not hold. Aborting state.",
-                    state.cpu.pc, program)
+                        state.cpu.pc, program)
             raise TerminateState()
 
-        #Everything is good add it.
+        # Everything is good add it.
         state.constraints.add(assertion)
 
-
     ##########################################################################
-    #Some are placeholders Remove FIXME
-    #Any platform specific callback should go to a plugin
+    # Some are placeholders Remove FIXME
+    # Any platform specific callback should go to a plugin
 
     def _generate_testcase_callback(self, state, name, message):
         '''
@@ -568,6 +561,7 @@ class Manticore(Eventful):
         class PstatsFormatted:
             def __init__(self, d):
                 self.stats = dict(d)
+
             def create_stats(self):
                 pass
         with self.locked_context('profiling_stats') as profiling_stats:
@@ -600,12 +594,12 @@ class Manticore(Eventful):
             self.enqueue(self._initial_state)
             self._initial_state = None
 
-        #Copy the local main context to the shared conext
+        # Copy the local main context to the shared conext
         self._executor._shared_context.update(self._context)
 
     def _finish_run(self, profiling=False):
         assert not self.running
-        #Copy back the shared context
+        # Copy back the shared context
         self._context = dict(self._executor._shared_context)
 
         if profiling:
@@ -636,7 +630,6 @@ class Manticore(Eventful):
                 t.cancel()
         self._finish_run(profiling=should_profile)
 
-
     def terminate(self):
         '''
         Gracefully terminate the currently-executing run. Typically called from within
@@ -644,7 +637,6 @@ class Manticore(Eventful):
         '''
         self._executor.shutdown()
 
-
     #############################################################################
     #############################################################################
     #############################################################################
@@ -659,7 +651,6 @@ class Manticore(Eventful):
         if self._binary_type == 'ELF':
             self._binary_obj = ELFFile(file(self._binary))
 
-
         if self._binary_obj is None:
             return NotImplementedError("Symbols aren't supported")
 
@@ -673,14 +664,13 @@ class Manticore(Eventful):
 
             return symbols[0].entry['st_value']
 
-
     @property
     def coverage_file(self):
         return self._coverage_file
 
     @property
     def workspace(self):
-         return self._output.store.uri
+        return self._output.store.uri
 
     @coverage_file.setter
     def coverage_file(self, path):
@@ -696,4 +686,3 @@ class Manticore(Eventful):
         elapsed = time.time() - self._time_started
         logger.info('Results in %s', self._output.store.uri)
         logger.info('Total time: %s', elapsed)
-

manticore/models.py

@@ -10,6 +10,7 @@ from .core.smtlib.operators import ITEBV, ZEXTEND
 
 VARIADIC_FUNC_ATTR = '_variadic'
 
+
 def isvariadic(model):
     """
     :param callable model: Function model
@@ -18,6 +19,7 @@ def isvariadic(model):
     """
     return getattr(model, VARIADIC_FUNC_ATTR, False)
 
+
 def variadic(func):
     """
     A decorator used to mark a function model as variadic. This function should
@@ -29,6 +31,7 @@ def variadic(func):
     setattr(func, VARIADIC_FUNC_ATTR, True)
     return func
 
+
 def _find_zero(cpu, constrs, ptr):
     """
     Helper for finding the closest NULL or, effectively NULL byte from a starting address.
@@ -132,7 +135,7 @@ def strlen(state, s):
 
     ret = zero_idx
 
-    for offset in xrange(zero_idx-1, -1, -1):
+    for offset in xrange(zero_idx - 1, -1, -1):
         byt = cpu.read_int(s + offset, 8)
         if issymbolic(byt):
             ret = ITEBV(cpu.address_bit_size, byt == 0, offset, ret)

manticore/platforms/cgcrandom.py

@@ -1,6 +1,6 @@
-#./print_random seed=0000000000000000000000000000000000000000000000000000000000000000000000000000000000 
-seed    = '0000000000000000000000000000000000000000000000000000000000000000000000000000000000'
-stream  = 'f795bd4a52e29ed713d313fa20e98dbcc8d1e5115952f7fa3738b4c5ceb2b09a0d9cc50d16e1bcedcf6062099d20837e6f39e0cb767c0debffa00e54'
+#./print_random seed=0000000000000000000000000000000000000000000000000000000000000000000000000000000000
+seed = '0000000000000000000000000000000000000000000000000000000000000000000000000000000000'
+stream = 'f795bd4a52e29ed713d313fa20e98dbcc8d1e5115952f7fa3738b4c5ceb2b09a0d9cc50d16e1bcedcf6062099d20837e6f39e0cb767c0debffa00e54'
 stream += 'e89ba679f60865f512d37070e748b00ea5a090cbe226cbffd135f48cee4e1ae66923369a97729ba14591a4908ae16fb07a3226bafa494f2501e95dee'
 stream += 'd7149ad824c0f2d5cc23f0059dc83fc17efbb4409773bfaed54d441d46768ed7ed878408f8de121ed411a6dfa262c78d37f7366e1803a4c56e1e0b76'
 stream += 'b815690de5f9908eeae544e7988698cbebdf49da51c9d88a729cfc40a2dfe92037a6c1c5f9a8b72642a5c725f94415a153ba4f036899c78fd1fcf093'

manticore/platforms/decree.py

@@ -1,6 +1,4 @@
 import cgcrandom
-import weakref
-import sys, os, struct
 # TODO use cpu factory
 from ..core.cpu.x86 import I386Cpu
 from ..core.cpu.abstractcpu import Interruption, Syscall, ConcretizeRegister
@@ -10,47 +8,49 @@ from ..core.executor import TerminateState
 from ..utils.helpers import issymbolic
 from ..binary import CGCElf
 from ..platforms.platform import Platform
-from contextlib import closing
-import StringIO
 import logging
 import random
 
 logger = logging.getLogger(__name__)
 
+
 class RestartSyscall(Exception):
     pass
 
+
 class Deadlock(Exception):
     pass
 
+
 class SymbolicSyscallArgument(ConcretizeRegister):
     def __init__(self, cpu, number, message='Concretizing syscall argument', policy='SAMPLED'):
-        reg_name = ['EBX', 'ECX', 'EDX', 'ESI', 'EDI', 'EBP' ][number]
+        reg_name = ['EBX', 'ECX', 'EDX', 'ESI', 'EDI', 'EBP'][number]
         super(SymbolicSyscallArgument, self).__init__(cpu, reg_name, message, policy)
 
+
 class Socket(object):
     @staticmethod
     def pair():
         a = Socket()
         b = Socket()
         a.connect(b)
-        return a,b
+        return a, b
 
     def __init__(self):
-        self.buffer = [] #queue os bytes
+        self.buffer = []  # queue os bytes
         self.peer = None
 
     def __repr__(self):
-        return "SOCKET(%x, %r, %x)"%(hash(self), self.buffer, hash(self.peer))
+        return "SOCKET(%x, %r, %x)" % (hash(self), self.buffer, hash(self.peer))
 
     def is_connected(self):
         return self.peer is not None
 
     def is_empty(self):
-        return len(self.buffer)==0
+        return len(self.buffer) == 0
 
     def is_full(self):
-        return len(self.buffer)>2*1024
+        return len(self.buffer) > 2 * 1024
 
     def connect(self, peer):
         assert not self.is_connected()
@@ -72,7 +72,7 @@ class Socket(object):
 
     def _transmit(self, buf):
         for c in buf:
-            self.buffer.insert(0,c)
+            self.buffer.insert(0, c)
         return len(buf)
 
 
@@ -81,15 +81,15 @@ class Decree(Platform):
     A simple Decree Operating System.
     This class emulates the most common Decree system calls
     '''
-    CGC_EBADF=1
-    CGC_EFAULT=2
-    CGC_EINVAL=3
-    CGC_ENOMEM=4
-    CGC_ENOSYS=5
-    CGC_EPIPE=6
-    CGC_SSIZE_MAX=2147483647
-    CGC_SIZE_MAX=4294967295
-    CGC_FD_SETSIZE=32
+    CGC_EBADF = 1
+    CGC_EFAULT = 2
+    CGC_EINVAL = 3
+    CGC_ENOMEM = 4
+    CGC_ENOSYS = 5
+    CGC_EPIPE = 6
+    CGC_SSIZE_MAX = 2147483647
+    CGC_SIZE_MAX = 4294967295
+    CGC_FD_SETSIZE = 32
 
     def __init__(self, programs, **kwargs):
         '''
@@ -114,23 +114,23 @@ class Decree(Platform):
         stdin = Socket()
         stdout = Socket()
         stderr = Socket()
-        #A transmit to stdin,stdout or stderr will be directed to out
+        # A transmit to stdin,stdout or stderr will be directed to out
         stdin.peer = self.output
         stdout.peer = self.output
         stderr.peer = self.output
-        #A receive from stdin will get data from inp
+        # A receive from stdin will get data from inp
         self.input.peer = stdin
-        #A receive on stdout or stderr will return no data (rx_bytes: 0)
+        # A receive on stdout or stderr will return no data (rx_bytes: 0)
 
         assert self._open(stdin) == 0
         assert self._open(stdout) == 1
         assert self._open(stderr) == 2
 
-        #Load process and setup socketpairs
+        # Load process and setup socketpairs
         self.procs = []
         for program in programs:
             self.procs += self.load(program)
-            socka,sockb = Socket.pair()
+            socka, sockb = Socket.pair()
             self._open(socka)
             self._open(sockb)
 
@@ -140,17 +140,16 @@ class Decree(Platform):
         self.running = range(nprocs)
         self._current = 0
 
-        #Each process can wait for one timeout
-        self.timers = [ None ] * nprocs
-        #each fd has a waitlist
+        # Each process can wait for one timeout
+        self.timers = [None] * nprocs
+        # each fd has a waitlist
         self.rwait = [set() for _ in xrange(nfiles)]
         self.twait = [set() for _ in xrange(nfiles)]
 
-        #Install event forwarders
+        # Install event forwarders
         for proc in self.procs:
             self.forward_events_from(proc)
 
-
     def _mk_proc(self):
         return I386Cpu(Memory32())
 
@@ -208,7 +207,7 @@ class Decree(Platform):
 
         self.syscall_trace = state['syscall_trace']
 
-        #Install event forwarders
+        # Install event forwarders
         for proc in self.procs:
             self.forward_events_from(proc)
 
@@ -218,14 +217,13 @@ class Decree(Platform):
         :todo: FIX. move to cpu or memory
         """
         filename = ""
-        for i in xrange(0,1024):
-            c = Operators.CHR(cpu.read_int(buf+i,8))
+        for i in xrange(0, 1024):
+            c = Operators.CHR(cpu.read_int(buf + i, 8))
             if c == '\x00':
                 break
             filename += c
         return filename
 
-
     def load(self, filename):
         '''
         Loads a CGC-ELF program in memory and prepares the initial CPU state
@@ -233,24 +231,27 @@ class Decree(Platform):
 
         :param filename: pathname of the file to be executed.
         '''
-        CGC_MIN_PAGE_SIZE   = 4096
-        CGC_MIN_ALIGN       = CGC_MIN_PAGE_SIZE
-        TASK_SIZE=0x80000000
+        CGC_MIN_PAGE_SIZE = 4096
+        CGC_MIN_ALIGN = CGC_MIN_PAGE_SIZE
+        TASK_SIZE = 0x80000000
 
         def CGC_PAGESTART(_v):
-            return  ((_v) & ~ (CGC_MIN_ALIGN-1))
+            return ((_v) & ~ (CGC_MIN_ALIGN - 1))
+
         def CGC_PAGEOFFSET(_v):
-            return ((_v) & (CGC_MIN_ALIGN-1))
+            return ((_v) & (CGC_MIN_ALIGN - 1))
+
         def CGC_PAGEALIGN(_v):
-            return  (((_v) + CGC_MIN_ALIGN - 1) & ~(CGC_MIN_ALIGN - 1))
+            return (((_v) + CGC_MIN_ALIGN - 1) & ~(CGC_MIN_ALIGN - 1))
+
         def BAD_ADDR(x):
             return ((x) >= TASK_SIZE)
 
-        #load elf See https://github.com/CyberdyneNYC/linux-source-3.13.2-cgc/blob/master/fs/binfmt_cgc.c
-        #read the ELF object file
+        # load elf See https://github.com/CyberdyneNYC/linux-source-3.13.2-cgc/blob/master/fs/binfmt_cgc.c
+        # read the ELF object file
         cgc = CGCElf(filename)
-        logger.info("Loading %s as a %s elf"%(filename, cgc.arch))
-        #make cpu and memory (Only 1 thread in Decree)
+        logger.info("Loading %s as a %s elf" % (filename, cgc.arch))
+        # make cpu and memory (Only 1 thread in Decree)
         cpu = self._mk_proc()
 
         bss = brk = 0
@@ -264,10 +265,10 @@ class Decree(Platform):
                 start_data = vaddr
 
             if vaddr > TASK_SIZE or filesz > memsz or \
-                 memsz > TASK_SIZE or TASK_SIZE - memsz < vaddr :
+                    memsz > TASK_SIZE or TASK_SIZE - memsz < vaddr:
                 raise Exception("Set_brk can never work. avoid overflows")
 
-            #CGCMAP--
+            # CGCMAP--
             addr = None
             if filesz > 0:
                 hint = CGC_PAGESTART(vaddr)
@@ -283,28 +284,26 @@ class Decree(Platform):
                 lo = CGC_PAGESTART(vaddr + filesz)
                 hi = CGC_PAGEALIGN(vaddr + memsz)
 
-
-            #map anon pages for the rest (no prefault)
+            # map anon pages for the rest (no prefault)
             if hi - lo > 0:
-                zaddr = cpu.memory.mmap(lo, hi-lo,perms)
+                zaddr = cpu.memory.mmap(lo, hi - lo, perms)
                 assert not BAD_ADDR(zaddr)
 
             lo = vaddr + filesz
             hi = CGC_PAGEALIGN(vaddr + memsz)
-            if hi - lo > 0 :
+            if hi - lo > 0:
                 old_perms = cpu.memory.perms(lo)
-                cpu.memory.mprotect(lo, hi-lo, 'rw')
+                cpu.memory.mprotect(lo, hi - lo, 'rw')
                 try:
-                    cpu.memory[lo:hi] = '\x00' *(hi-lo)
-                except Exception, e:
-                    logger.debug("Exception zeroing main elf fractional pages: %s"%str(e))
+                    cpu.memory[lo:hi] = '\x00' * (hi - lo)
+                except Exception as e:
+                    logger.debug("Exception zeroing main elf fractional pages: %s" % str(e))
                 cpu.memory.mprotect(lo, hi, old_perms)
 
             if addr is None:
                 addr = zaddr
             assert addr is not None
 
-
             k = vaddr + filesz
             if k > bss:
                 bss = k
@@ -317,38 +316,37 @@ class Decree(Platform):
             if k > brk:
                 brk = k
 
-
         bss = brk
         stack_base = 0xbaaaaffc
         stack_size = 0x800000
-        stack = cpu.memory.mmap(0xbaaab000-stack_size, stack_size,'rwx')+stack_size-4
-        assert (stack_base) in cpu.memory and (stack_base-stack_size+4) in cpu.memory
+        stack = cpu.memory.mmap(0xbaaab000 - stack_size, stack_size, 'rwx') + stack_size - 4
+        assert (stack_base) in cpu.memory and (stack_base - stack_size + 4) in cpu.memory
 
-        #Only one thread in Decree
+        # Only one thread in Decree
         status, thread = next(cgc.threads())
         assert status == 'Running'
 
         logger.info("Setting initial cpu state")
-        #set initial CPU state
-        cpu.write_register('EAX',            0x0)
-        cpu.write_register('ECX',            0x0)
-        cpu.write_register('EDX',            0x0)
-        cpu.write_register('EBX',            0x0)
-        cpu.write_register('ESP',            stack)
-        cpu.write_register('EBP',            0x0)
-        cpu.write_register('ESI',            0x0)
-        cpu.write_register('EDI',            0x0)
-        cpu.write_register('EIP',            thread['EIP'])
-        cpu.write_register('RFLAGS',         0x202)
-        cpu.write_register('CS',             0x0)
-        cpu.write_register('SS',             0x0)
-        cpu.write_register('DS',             0x0)
-        cpu.write_register('ES',             0x0)
-        cpu.write_register('FS',             0x0)
-        cpu.write_register('GS',             0x0)
+        # set initial CPU state
+        cpu.write_register('EAX', 0x0)
+        cpu.write_register('ECX', 0x0)
+        cpu.write_register('EDX', 0x0)
+        cpu.write_register('EBX', 0x0)
+        cpu.write_register('ESP', stack)
+        cpu.write_register('EBP', 0x0)
+        cpu.write_register('ESI', 0x0)
+        cpu.write_register('EDI', 0x0)
+        cpu.write_register('EIP', thread['EIP'])
+        cpu.write_register('RFLAGS', 0x202)
+        cpu.write_register('CS', 0x0)
+        cpu.write_register('SS', 0x0)
+        cpu.write_register('DS', 0x0)
+        cpu.write_register('ES', 0x0)
+        cpu.write_register('FS', 0x0)
+        cpu.write_register('GS', 0x0)
 
-        cpu.memory.mmap(0x4347c000,0x1000, 'r')
-        #cpu.memory[0x4347c000:0x4347d000] = 'A' 0x1000
+        cpu.memory.mmap(0x4347c000, 0x1000, 'r')
+        # cpu.memory[0x4347c000:0x4347d000] = 'A' 0x1000
 
         logger.info("Entry point: %016x", cpu.EIP)
         logger.info("Stack start: %016x", cpu.ESP)
@@ -361,7 +359,7 @@ class Decree(Platform):
     def _open(self, f):
         if None in self.files:
             fd = self.files.index(None)
-            self.files[fd]=f
+            self.files[fd] = f
         else:
             fd = len(self.files)
             self.files.append(f)
@@ -418,19 +416,19 @@ class Decree(Platform):
                    ENOMEM   No memory is available or the process' maximum number of allocations
                             would have been exceeded.
         '''
-        #TODO: check 4 bytes from addr
-        if not addr in cpu.memory:
+        # TODO: check 4 bytes from addr
+        if addr not in cpu.memory:
             logger.info("ALLOCATE: addr points to invalid address. Returning EFAULT")
             return Decree.CGC_EFAULT
 
-        perms = [ 'rw ', 'rwx'][bool(isX)]
+        perms = ['rw ', 'rwx'][bool(isX)]
         try:
             result = cpu.memory.mmap(None, length, perms)
-        except Exception, e:
+        except Exception as e:
             logger.info("ALLOCATE exception %s. Returning ENOMEM %r", str(e), length)
             return Decree.CGC_ENOMEM
         cpu.write_int(addr, result, 32)
-        logger.info("ALLOCATE(%d, %s, 0x%08x) -> 0x%08x"%(length, perms, addr, result))
+        logger.info("ALLOCATE(%d, %s, 0x%08x) -> 0x%08x" % (length, perms, addr, result))
         self.syscall_trace.append(("_allocate", -1, length))
         return 0
 
@@ -457,22 +455,22 @@ class Decree(Platform):
                 ret = Decree.CGC_EINVAL
             else:
                 # TODO check count bytes from buf
-                if buf not in cpu.memory or (buf+count) not in cpu.memory:
+                if buf not in cpu.memory or (buf + count) not in cpu.memory:
                     logger.info("RANDOM: buf points to invalid address. Returning EFAULT")
                     return Decree.CGC_EFAULT
 
-                data = file("/dev/urandom","r").read(count)
+                data = file("/dev/urandom", "r").read(count)
                 self.syscall_trace.append(("_random", -1, data))
                 cpu.write_bytes(buf, data)
 
         # TODO check 4 bytes from rx_bytes
         if rx_bytes:
-            if rx_bytes not in cpu.memory :
+            if rx_bytes not in cpu.memory:
                 logger.info("RANDOM: Not valid rx_bytes. Returning EFAULT")
                 return Decree.CGC_EFAULT
             cpu.write_int(rx_bytes, len(data), 32)
 
-        logger.info("RANDOM(0x%08x, %d, 0x%08x) -> <%s>)"%(buf, count, rnd_bytes, repr(data[:10])))
+        logger.info("RANDOM(0x%08x, %d, 0x%08x) -> <%s>)" % (buf, count, rnd_bytes, repr(data[:10])))
         return ret
 
     def sys_receive(self, cpu, fd, buf, count, rx_bytes):
@@ -498,7 +496,7 @@ class Decree(Platform):
                 return Decree.CGC_EBADF
 
             # TODO check count bytes from buf
-            if buf not in cpu.memory: # or not  buf+count in cpu.memory:
+            if buf not in cpu.memory:  # or not  buf+count in cpu.memory:
                 logger.info("RECEIVE: buf points to invalid address. Returning EFAULT")
                 return Decree.CGC_EFAULT
 
@@ -509,8 +507,8 @@ class Decree(Platform):
                 self.wait([fd], [], None)
                 raise RestartSyscall()
 
-            #get some potential delay
-            #if random.randint(5) == 0 and count > 1:
+            # get some potential delay
+            # if random.randint(5) == 0 and count > 1:
             #    count = count/2
 
             # Read the data and put in tin memory
@@ -520,7 +518,6 @@ class Decree(Platform):
 
             self.signal_receive(fd)
 
-
         # TODO check 4 bytes from rx_bytes
         if rx_bytes:
             if rx_bytes not in cpu.memory:
@@ -528,7 +525,7 @@ class Decree(Platform):
                 return Decree.CGC_EFAULT
             cpu.write_int(rx_bytes, len(data), 32)
 
-        logger.info("RECEIVE(%d, 0x%08x, %d, 0x%08x) -> <%s> (size:%d)"%(fd, buf, count, rx_bytes, repr(data)[:min(count,10)],len(data)))
+        logger.info("RECEIVE(%d, 0x%08x, %d, 0x%08x) -> <%s> (size:%d)" % (fd, buf, count, rx_bytes, repr(data)[:min(count, 10)], len(data)))
         return 0
 
     def sys_transmit(self, cpu, fd, buf, count, tx_bytes):
@@ -554,30 +551,30 @@ class Decree(Platform):
                 return Decree.CGC_EBADF
 
             # TODO check count bytes from buf
-            if buf not in cpu.memory or (buf+count) not in cpu.memory:
+            if buf not in cpu.memory or (buf + count) not in cpu.memory:
                 logger.debug("TRANSMIT: buf points to invalid address. Rerurning EFAULT")
                 return Decree.CGC_EFAULT
 
             if fd > 2 and self.files[fd].is_full():
                 cpu.PC -= cpu.instruction.size
-                self.wait([],[fd],None)
+                self.wait([], [fd], None)
                 raise RestartSyscall()
 
             for i in xrange(0, count):
-                value = Operators.CHR(cpu.read_int(buf+i,8))
+                value = Operators.CHR(cpu.read_int(buf + i, 8))
                 if not isinstance(value, str):
                     logger.debug("TRANSMIT: Writing symbolic values to file %d", fd)
                     #value = str(value)
                 data.append(value)
             self.files[fd].transmit(data)
 
-            logger.info("TRANSMIT(%d, 0x%08x, %d, 0x%08x) -> <%.24r>"%(fd, buf, count, tx_bytes, ''.join([str(x) for x in data])))
+            logger.info("TRANSMIT(%d, 0x%08x, %d, 0x%08x) -> <%.24r>" % (fd, buf, count, tx_bytes, ''.join([str(x) for x in data])))
             self.syscall_trace.append(("_transmit", fd, data))
             self.signal_transmit(fd)
 
         # TODO check 4 bytes from tx_bytes
         if tx_bytes:
-            if tx_bytes not in cpu.memory :
+            if tx_bytes not in cpu.memory:
                 logger.debug("TRANSMIT: Not valid tx_bytes pointer on transmit. Returning EFAULT")
                 return Decree.CGC_EFAULT
             cpu.write_int(tx_bytes, len(data), 32)
@@ -593,12 +590,12 @@ class Decree(Platform):
         procid = self.procs.index(cpu)
         self.sched()
         self.running.remove(procid)
-        #self.procs[procid] = None #let it there so we can report?
+        # self.procs[procid] = None #let it there so we can report?
         if issymbolic(error_code):
-           logger.info("TERMINATE PROC_%02d with symbolic exit code [%d,%d]", procid, solver.minmax(self.constraints, error_code))
+            logger.info("TERMINATE PROC_%02d with symbolic exit code [%d,%d]", procid, solver.minmax(self.constraints, error_code))
         else:
             logger.info("TERMINATE PROC_%02d %x", procid, error_code)
-        if len(self.running) == 0 :
+        if len(self.running) == 0:
             raise TerminateState('Process exited correctly. Code: {}'.format(error_code))
         return error_code
 
@@ -629,16 +626,16 @@ class Decree(Platform):
         :param cpu: current CPU.
         :return: C{0} on success.
         '''
-        logger.info("DEALLOCATE(0x%08x, %d)"%(addr, size))
+        logger.info("DEALLOCATE(0x%08x, %d)" % (addr, size))
 
         if addr & 0xfff != 0:
             logger.info("DEALLOCATE: addr is not page aligned")
             return Decree.CGC_EINVAL
-        if size == 0 :
+        if size == 0:
             logger.info("DEALLOCATE:length is zero")
             return Decree.CGC_EINVAL
-        #unlikely AND WRONG!!!
-        #if addr > Decree.CGC_SSIZE_MAX or addr+size > Decree.CGC_SSIZE_MAX:
+        # unlikely AND WRONG!!!
+        # if addr > Decree.CGC_SSIZE_MAX or addr+size > Decree.CGC_SSIZE_MAX:
         #    logger.info("DEALLOCATE: part of the region being deallocated is outside the valid address range of the process")
         #    return Decree.CGC_EINVAL
 
@@ -649,30 +646,30 @@ class Decree(Platform):
     def sys_fdwait(self, cpu, nfds, readfds, writefds, timeout, readyfds):
         ''' fdwait - wait for file descriptors to become ready
         '''
-        logger.debug("FDWAIT(%d, 0x%08x, 0x%08x, 0x%08x, 0x%08x)"%(nfds, readfds, writefds, timeout, readyfds))
+        logger.debug("FDWAIT(%d, 0x%08x, 0x%08x, 0x%08x, 0x%08x)" % (nfds, readfds, writefds, timeout, readyfds))
 
         if timeout:
-            if timeout not in cpu.memory : #todo: size
+            if timeout not in cpu.memory:  # todo: size
                 logger.info("FDWAIT: timeput is pointing to invalid memory. Returning EFAULT")
                 return Decree.CGC_EFAULT
 
         if readyfds:
-            if readyfds not in cpu.memory :
+            if readyfds not in cpu.memory:
                 logger.info("FDWAIT: readyfds pointing to invalid memory. Returning EFAULT")
                 return Decree.CGC_EFAULT
 
         writefds_wait = set()
         writefds_ready = set()
 
-        fds_bitsize = (nfds+7)&~7
+        fds_bitsize = (nfds + 7) & ~7
         if writefds:
-            if writefds not in cpu.memory :
+            if writefds not in cpu.memory:
                 logger.info("FDWAIT: writefds pointing to invalid memory. Returning EFAULT")
                 return Decree.CGC_EFAULT
             bits = cpu.read_int(writefds, fds_bitsize)
 
             for fd in range(nfds):
-                if (bits & 1<<fd):
+                if (bits & 1 << fd):
                     if self.files[fd].is_full():
                         writefds_wait.add(fd)
                     else:
@@ -681,46 +678,48 @@ class Decree(Platform):
         readfds_wait = set()
         readfds_ready = set()
         if readfds:
-            if readfds not in cpu.memory :
+            if readfds not in cpu.memory:
                 logger.info("FDWAIT: readfds pointing to invalid memory. Returning EFAULT")
                 return Decree.CGC_EFAULT
             bits = cpu.read_int(readfds, fds_bitsize)
             for fd in range(nfds):
-                if (bits & 1<<fd):
+                if (bits & 1 << fd):
                     if self.files[fd].is_empty():
                         readfds_wait.add(fd)
                     else:
                         readfds_ready.add(fd)
         n = len(readfds_ready) + len(writefds_ready)
         if n == 0:
-            #TODO FIX timout symbolic
+            # TODO FIX timout symbolic
             if timeout != 0:
                 seconds = cpu.read_int(timeout, 32)
-                microseconds = cpu.read_int(timeout+4, 32)
-                logger.info("FDWAIT: waiting for read on fds: {%s} and write to: {%s} timeout: %d", repr(list(readfds_wait)), repr(list(writefds_wait)), microseconds+1000*seconds)
-                to = microseconds+1000*seconds
-                #no ready file, wait
+                microseconds = cpu.read_int(timeout + 4, 32)
+                logger.info("FDWAIT: waiting for read on fds: {%s} and write to: {%s} timeout: %d", repr(
+                    list(readfds_wait)), repr(list(writefds_wait)), microseconds + 1000 * seconds)
+                to = microseconds + 1000 * seconds
+                # no ready file, wait
             else:
                 to = None
-                logger.info("FDWAIT: waiting for read on fds: {%s} and write to: {%s} timeout: INDIFENITELY", repr(list(readfds_wait)), repr(list(writefds_wait)))
+                logger.info("FDWAIT: waiting for read on fds: {%s} and write to: {%s} timeout: INDIFENITELY",
+                            repr(list(readfds_wait)), repr(list(writefds_wait)))
 
             cpu.PC -= cpu.instruction.size
             self.wait(readfds_wait, writefds_wait, to)
-            raise RestartSyscall() #When comming back from a timeout remember
-            #not to backtrack instruction and set EAX to 0! :( uglyness alert!
+            raise RestartSyscall()  # When comming back from a timeout remember
+            # not to backtrack instruction and set EAX to 0! :( uglyness alert!
 
         if readfds:
             bits = 0
             for fd in readfds_ready:
-                bits |= 1<<fd
-            for byte in range(0, nfds,8):
-                cpu.write_int(readfds, (bits>>byte)&0xff, 8)
+                bits |= 1 << fd
+            for byte in range(0, nfds, 8):
+                cpu.write_int(readfds, (bits >> byte) & 0xff, 8)
         if writefds:
             bits = 0
             for fd in writefds_ready:
-                bits |= 1<<fd
-            for byte in range(0, nfds,8):
-                cpu.write_int(writefds, (bits>>byte)&0xff, 8)
+                bits |= 1 << fd
+            for byte in range(0, nfds, 8):
+                cpu.write_int(writefds, (bits >> byte) & 0xff, 8)
 
         logger.info("FDWAIT: continuing. Some file is ready Readyfds: %08x", readyfds)
         if readyfds:
@@ -735,22 +734,21 @@ class Decree(Platform):
         :param cpu: current CPU.
         _terminate, transmit, receive, fdwait, allocate, deallocate and random
         '''
-        syscalls = { 0x00000001: self.sys_terminate,
-                     0x00000002: self.sys_transmit,
-                     0x00000003: self.sys_receive,
-                     0x00000004: self.sys_fdwait,
-                     0x00000005: self.sys_allocate,
-                     0x00000006: self.sys_deallocate,
-                     0x00000007: self.sys_random,
+        syscalls = {0x00000001: self.sys_terminate,
+                    0x00000002: self.sys_transmit,
+                    0x00000003: self.sys_receive,
+                    0x00000004: self.sys_fdwait,
+                    0x00000005: self.sys_allocate,
+                    0x00000006: self.sys_deallocate,
+                    0x00000007: self.sys_random,
                     }
         if cpu.EAX not in syscalls.keys():
             raise TerminateState("32 bit DECREE system call number {} Not Implemented".format(cpu.EAX))
         func = syscalls[cpu.EAX]
         logger.debug("SYSCALL32: %s (nargs: %d)", func.func_name, func.func_code.co_argcount)
         nargs = func.func_code.co_argcount
-        args = [ cpu, cpu.EBX, cpu.ECX, cpu.EDX, cpu.ESI, cpu.EDI, cpu.EBP ]
-        cpu.EAX = func(*args[:nargs-1])
-
+        args = [cpu, cpu.EBX, cpu.ECX, cpu.EDX, cpu.ESI, cpu.EDI, cpu.EBP]
+        cpu.EAX = func(*args[:nargs - 1])
 
     def sched(self):
         ''' Yield CPU.
@@ -758,7 +756,7 @@ class Decree(Platform):
             current running process. May give the same cpu if only one running
             proccess.
         '''
-        if len(self.procs)>1:
+        if len(self.procs) > 1:
             logger.info("SCHED:")
             logger.info("\tProcess: %r", self.procs)
             logger.info("\tRunning: %r", self.running)
@@ -772,14 +770,14 @@ class Decree(Platform):
             logger.info("None running checking if there is some process waiting for a timeout")
             if all([x is None for x in self.timers]):
                 raise Deadlock()
-            self.clocks = min(filter(lambda x: x is not None, self.timers))+1
+            self.clocks = min(filter(lambda x: x is not None, self.timers)) + 1
             self.check_timers()
             assert len(self.running) != 0, "DEADLOCK!"
             self._current = self.running[0]
             return
         next_index = (self.running.index(self._current) + 1) % len(self.running)
-        next = self.running[ next_index ]
-        if len(self.procs)>1:
+        next = self.running[next_index]
+        if len(self.procs) > 1:
             logger.info("\tTransfer control from process %d to %d", self._current, next)
         self._current = next
 
@@ -796,7 +794,6 @@ class Decree(Platform):
         logger.info("\tTWait: %r", self.twait)
         logger.info("\tTimers: %r", self.timers)
 
-
         for fd in readfds:
             self.rwait[fd].add(self._current)
         for fd in writefds:
@@ -806,15 +803,15 @@ class Decree(Platform):
         else:
             self.timers[self._current] = None
         procid = self._current
-        #self.sched()
+        # self.sched()
         next_index = (self.running.index(procid) + 1) % len(self.running)
-        self._current = self.running[ next_index ]
+        self._current = self.running[next_index]
         logger.info("\tTransfer control from process %d to %d", procid, self._current)
-        logger.info( "\tREMOVING %r from %r. Current: %r",procid, self.running, self._current)
+        logger.info("\tREMOVING %r from %r. Current: %r", procid, self.running, self._current)
         self.running.remove(procid)
         if self._current not in self.running:
-            logger.info( "\tCurrent not running. Checking for timers...")
-            self._current=None
+            logger.info("\tCurrent not running. Checking for timers...")
+            self._current = None
             if all([x is None for x in self.timers]):
                 raise Deadlock()
             self.check_timers()
@@ -823,18 +820,20 @@ class Decree(Platform):
         ''' Remove procid from waitlists and restablish it in the running list '''
         logger.info("Remove procid:%d from waitlists and restablish it in the running list", procid)
         for wait_list in self.rwait:
-            if procid in wait_list: wait_list.remove(procid)
+            if procid in wait_list:
+                wait_list.remove(procid)
         for wait_list in self.twait:
-            if procid in wait_list: wait_list.remove(procid)
-        self.timers[procid]=None
+            if procid in wait_list:
+                wait_list.remove(procid)
+        self.timers[procid] = None
         self.running.append(procid)
         if self._current is None:
             self._current = procid
 
     def connections(self, fd):
-        if fd in [0,1,2]:
+        if fd in [0, 1, 2]:
             return None
-        if fd%2:
+        if fd % 2:
             return fd + 1
         else:
             return fd - 1
@@ -856,8 +855,8 @@ class Decree(Platform):
     def check_timers(self):
         ''' Awake proccess if timer has expired '''
         if self._current is None:
-            #Advance the clocks. Go to future!!
-            advance = min(filter( lambda x: x is not None, self.timers)) +1
+            # Advance the clocks. Go to future!!
+            advance = min(filter(lambda x: x is not None, self.timers)) + 1
             logger.info("Advancing the clock from %d to %d", self.clocks, advance)
             self.clocks = advance
         for procid in range(len(self.timers)):
@@ -880,7 +879,7 @@ class Decree(Platform):
             if self.clocks % 10000 == 0:
                 self.check_timers()
                 self.sched()
-        except Interruption, e:
+        except Interruption as e:
             if e.N != 0x80:
                 raise
             try:
@@ -893,10 +892,12 @@ class Decree(Platform):
 ############################################################################
 # Symbolic versions follows
 
+
 class SDecree(Decree):
     '''
     A symbolic extension of a Decree Operating System .
     '''
+
     def __init__(self, constraints, programs, symbolic_random=None):
         '''
         Builds a symbolic extension of a Decree OS
@@ -921,7 +922,7 @@ class SDecree(Decree):
         for proc in self.procs:
             proc.memory.constraints = constraints
 
-    #marshaling/pickle
+    # marshaling/pickle
     def __getstate__(self):
         state = super(SDecree, self).__getstate__()
         state['constraints'] = self.constraints
@@ -933,116 +934,113 @@ class SDecree(Decree):
         self.random = state['random']
         super(SDecree, self).__setstate__(state)
 
-
     def sys_receive(self, cpu, fd, buf, count, rx_bytes):
         ''' Symbolic version of Decree.sys_receive
         '''
         if issymbolic(fd):
             logger.info("Ask to read from a symbolic file descriptor!!")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 0)
 
         if issymbolic(buf):
             logger.info("Ask to read to a symbolic buffer")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 1)
 
         if issymbolic(count):
             logger.info("Ask to read a symbolic number of bytes ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 2)
 
         if issymbolic(rx_bytes):
             logger.info("Ask to return size to a symbolic address ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 3)
 
         return super(SDecree, self).sys_receive(cpu, fd, buf, count, rx_bytes)
 
-
     def sys_transmit(self, cpu, fd, buf, count, tx_bytes):
         ''' Symbolic version of Decree.sys_receive
         '''
         if issymbolic(fd):
             logger.info("Ask to write to a symbolic file descriptor!!")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 0)
 
         if issymbolic(buf):
             logger.info("Ask to write to a symbolic buffer")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 1)
 
         if issymbolic(count):
             logger.info("Ask to write a symbolic number of bytes ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 2)
 
         if issymbolic(tx_bytes):
             logger.info("Ask to return size to a symbolic address ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 3)
 
         return super(SDecree, self).sys_transmit(cpu, fd, buf, count, tx_bytes)
 
-
     def sys_allocate(self, cpu, length, isX, address_p):
         if issymbolic(length):
             logger.info("Ask to ALLOCATE a symbolic number of bytes ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 0)
         if issymbolic(isX):
             logger.info("Ask to ALLOCATE potentially executable or not executable memory")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 1)
         if issymbolic(address_p):
             logger.info("Ask to return ALLOCATE result to a symbolic reference ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 2)
         return super(SDecree, self).sys_allocate(cpu, length, isX, address_p)
 
     def sys_deallocate(self, cpu, addr, size):
         if issymbolic(addr):
             logger.info("Ask to DEALLOCATE a symbolic pointer?!")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 0)
         if issymbolic(size):
             logger.info("Ask to DEALLOCATE a symbolic size?!")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 1)
         return super(SDecree, self).sys_deallocate(cpu, addr, size)
 
     def sys_random(self, cpu, buf, count, rnd_bytes):
         if issymbolic(buf):
             logger.info("Ask to write random bytes to a symbolic buffer")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 0)
 
         if issymbolic(count):
             logger.info("Ask to read a symbolic number of random bytes ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 1)
 
         if issymbolic(rnd_bytes):
             logger.info("Ask to return rnd size to a symbolic address ")
-            cpu.PC = cpu.PC-cpu.instruction.size
+            cpu.PC = cpu.PC - cpu.instruction.size
             raise SymbolicSyscallArgument(cpu, 2)
 
         data = []
         for i in xrange(count):
             if False:
-                #Too slow for the new age.
-                value = self.constraints.new_bitvec(8, name="RANDOM_%04d"%self.random)
-                self.constraints.add(symb==cgcrandom.stream[self.random])
+                # Too slow for the new age.
+                value = self.constraints.new_bitvec(8, name="RANDOM_%04d" % self.random)
+                self.constraints.add(symb == cgcrandom.stream[self.random])
             else:
                 value = cgcrandom.stream[self.random]
             data.append(value)
-            self.random+=1
+            self.random += 1
 
         cpu.write_bytes(buf, data)
         if rnd_bytes:
             cpu.write_int(rnd_bytes, len(data), 32)
-        logger.info("RANDOM(0x%08x, %d, 0x%08x) -> %d", buf,count,rnd_bytes,len(data))
+        logger.info("RANDOM(0x%08x, %d, 0x%08x) -> %d", buf, count, rnd_bytes, len(data))
         return 0
 
 
@@ -1082,5 +1080,3 @@ class DecreeEmu(object):
             cpu.store(rnd_bytes, len(data), 32)
         logger.info("RANDOM(0x%08x, %d, 0x%08x) -> %d", buf, count, rnd_bytes, len(data))
         return 0
-
-

manticore/platforms/platform.py

@@ -1,7 +1,5 @@
 
 from manticore.utils.event import Eventful
-from itertools import islice, imap
-import inspect
 
 class OSException(Exception):
     pass
@@ -11,10 +9,12 @@ class SyscallNotImplemented(OSException):
     ''' Exception raised when you try to call a not implemented
         system call. Go to linux.py and add it!
     '''
+
     def __init__(self, idx, name):
         msg = 'Syscall index "{}" ({}) not implemented.'.format(idx, name)
         super(SyscallNotImplemented, self).__init__(msg)
 
+
 class ConcretizeSyscallArgument(OSException):
     def __init__(self, reg_num, message='Concretizing syscall argument', policy='SAMPLED'):
         self.reg_num = reg_num
@@ -22,10 +22,12 @@ class ConcretizeSyscallArgument(OSException):
         self.policy = policy
         super(ConcretizeSyscallArgument, self).__init__(message)
 
+
 class Platform(Eventful):
     '''
     Base class for all operating system platforms.
     '''
+
     def __init__(self, path, **kwargs):
         super(Platform, self).__init__(**kwargs)
 

manticore/utils/emulate.py

@@ -1,5 +1,4 @@
 import logging
-import inspect
 
 from ..core.memory import MemoryException, FileMap, AnonMap
 
@@ -17,17 +16,19 @@ from capstone.x86 import *
 
 logger = logging.getLogger(__name__)
 
+
 class UnicornEmulator(object):
     '''
     Helper class to emulate a single instruction via Unicorn.
     '''
+
     def __init__(self, cpu):
         self._cpu = cpu
 
         text = cpu.memory.map_containing(cpu.PC)
         # Keep track of all memory mappings. We start with just the text section
         self._should_be_mapped = {
-                text.start: (len(text), UC_PROT_READ | UC_PROT_EXEC)
+            text.start: (len(text), UC_PROT_READ | UC_PROT_EXEC)
         }
 
         # Keep track of all the memory Unicorn needs while executing this
@@ -96,7 +97,6 @@ class UnicornEmulator(object):
             elif self._cpu.mode == CS_MODE_64:
                 return self._emu.reg_read(UC_X86_REG_RIP)
 
-
     def _hook_xfer_mem(self, uc, access, address, size, value, data):
         '''
         Handle memory operations from unicorn.
@@ -104,7 +104,7 @@ class UnicornEmulator(object):
         assert access in (UC_MEM_WRITE, UC_MEM_READ, UC_MEM_FETCH)
 
         if access == UC_MEM_WRITE:
-            self._cpu.write_int(address, value, size*8)
+            self._cpu.write_int(address, value, size * 8)
 
         # If client code is attempting to read a value, we need to bring it
         # in from Manticore state. If we try to mem_write it here, Unicorn
@@ -123,7 +123,6 @@ class UnicornEmulator(object):
 
         return True
 
-
     def _hook_unmapped(self, uc, access, address, size, value, data):
         '''
         We hit an unmapped region; map it into unicorn.
@@ -197,7 +196,6 @@ class UnicornEmulator(object):
             if not self._should_try_again:
                 break
 
-
     def _step(self, instruction):
         '''
         A single attempt at executing an instruction.
@@ -209,7 +207,7 @@ class UnicornEmulator(object):
         if self._cpu.arch == CS_ARCH_X86:
             # The last 8 canonical registers of x86 are individual flags; replace
             # with the eflags
-            registers -= set(['CF','PF','AF','ZF','SF','IF','DF','OF'])
+            registers -= set(['CF', 'PF', 'AF', 'ZF', 'SF', 'IF', 'DF', 'OF'])
             registers.add('EFLAGS')
 
             # TODO(mark): Unicorn 1.0.1 does not support reading YMM registers,
@@ -218,8 +216,10 @@ class UnicornEmulator(object):
             # incorrect zero value being actually written to the XMM register. This is
             # fixed in Unicorn PR #819, so when that is included in a release, delete
             # these two lines.
-            registers -= set(['YMM0', 'YMM1', 'YMM2', 'YMM3', 'YMM4', 'YMM5', 'YMM6', 'YMM7', 'YMM8', 'YMM9', 'YMM10', 'YMM11', 'YMM12', 'YMM13', 'YMM14', 'YMM15'])
-            registers |= set(['XMM0', 'XMM1', 'XMM2', 'XMM3', 'XMM4', 'XMM5', 'XMM6', 'XMM7', 'XMM8', 'XMM9', 'XMM10', 'XMM11', 'XMM12', 'XMM13', 'XMM14', 'XMM15'])
+            registers -= set(['YMM0', 'YMM1', 'YMM2', 'YMM3', 'YMM4', 'YMM5', 'YMM6', 'YMM7',
+                              'YMM8', 'YMM9', 'YMM10', 'YMM11', 'YMM12', 'YMM13', 'YMM14', 'YMM15'])
+            registers |= set(['XMM0', 'XMM1', 'XMM2', 'XMM3', 'XMM4', 'XMM5', 'XMM6', 'XMM7',
+                              'XMM8', 'XMM9', 'XMM10', 'XMM11', 'XMM12', 'XMM13', 'XMM14', 'XMM15'])
 
         # XXX(yan): This concretizes the entire register state. This is overly
         # aggressive. Once capstone adds consistent support for accessing
@@ -238,17 +238,17 @@ class UnicornEmulator(object):
         text_bytes = self._cpu.read_bytes(self._cpu.PC, instruction.size)
         self._emu.mem_write(self._cpu.PC, ''.join(text_bytes))
 
-        self._emu.hook_add(UC_HOOK_MEM_READ_UNMAPPED,  self._hook_unmapped)
+        self._emu.hook_add(UC_HOOK_MEM_READ_UNMAPPED, self._hook_unmapped)
         self._emu.hook_add(UC_HOOK_MEM_WRITE_UNMAPPED, self._hook_unmapped)
         self._emu.hook_add(UC_HOOK_MEM_FETCH_UNMAPPED, self._hook_unmapped)
-        self._emu.hook_add(UC_HOOK_MEM_READ,           self._hook_xfer_mem)
-        self._emu.hook_add(UC_HOOK_MEM_WRITE,          self._hook_xfer_mem)
-        self._emu.hook_add(UC_HOOK_INTR,               self._interrupt)
+        self._emu.hook_add(UC_HOOK_MEM_READ, self._hook_xfer_mem)
+        self._emu.hook_add(UC_HOOK_MEM_WRITE, self._hook_xfer_mem)
+        self._emu.hook_add(UC_HOOK_INTR, self._interrupt)
 
         saved_PC = self._cpu.PC
 
         try:
-            self._emu.emu_start(self._cpu.PC, self._cpu.PC+instruction.size, count=1)
+            self._emu.emu_start(self._cpu.PC, self._cpu.PC + instruction.size, count=1)
         except UcError as e:
             # We request re-execution by signaling error; if we we didn't set
             # _should_try_again, it was likely an actual error
@@ -259,19 +259,19 @@ class UnicornEmulator(object):
             return
 
         if logger.isEnabledFor(logging.DEBUG):
-            logger.debug("="*10)
+            logger.debug("=" * 10)
             for register in self._cpu.canonical_registers:
                 logger.debug("Register % 3s  Manticore: %08x, Unicorn %08x",
-                        register, self._cpu.read_register(register),
-                        self._emu.reg_read(self._to_unicorn_id(register)) )
-            logger.debug(">"*10)
+                             register, self._cpu.read_register(register),
+                             self._emu.reg_read(self._to_unicorn_id(register)))
+            logger.debug(">" * 10)
 
         # Bring back Unicorn registers to Manticore
         for reg in registers:
             val = self._emu.reg_read(self._to_unicorn_id(reg))
             self._cpu.write_register(reg, val)
 
-        #Unicorn hack. On single step unicorn wont advance the PC register
+        # Unicorn hack. On single step unicorn wont advance the PC register
         mu_pc = self.get_unicorn_pc()
         if saved_PC == mu_pc:
             self._cpu.PC = saved_PC + instruction.size
@@ -281,4 +281,3 @@ class UnicornEmulator(object):
             raise self._to_raise
 
         return
-

manticore/utils/event.py

@@ -1,9 +1,10 @@
 import inspect
 import logging
-from weakref import ref, WeakSet, WeakKeyDictionary, WeakValueDictionary
+from weakref import WeakKeyDictionary, ref
 
 logger = logging.getLogger(__name__)
 
+
 class EventsGatherMetaclass(type):
     '''
     Metaclass that is used for Eventful to gather events that classes declare to
@@ -33,6 +34,7 @@ class EventsGatherMetaclass(type):
 
         return eventful_sub
 
+
 class Eventful(object):
     '''
         Abstract class for objects emitting and receiving events
@@ -49,7 +51,7 @@ class Eventful(object):
     # Set in subclass to advertise the events it plans to publish
     _published_events = set()
 
-    #Event names prefixes
+    # Event names prefixes
     prefixes = ('will_', 'did_', 'on_')
 
     @classmethod
@@ -94,23 +96,22 @@ class Eventful(object):
             del self._signals[name]
 
     def _get_signal_bucket(self, name):
-        #Each event name has a bucket of callback methods
-        #A bucket is a dictionary obj -> set(method1, method2...)
-        return self._signals.setdefault(name,  dict())
+        # Each event name has a bucket of callback methods
+        # A bucket is a dictionary obj -> set(method1, method2...)
+        return self._signals.setdefault(name, dict())
 
-    def _check_event(self, _name):        
+    def _check_event(self, _name):
         basename = _name
         for prefix in self.prefixes:
             if _name.startswith(prefix):
                 basename = _name[len(prefix):]
-        
+
         cls = self.__class__
         if basename not in cls.__all_events__[cls]:
             logger.warning("Event '%s' not pre-declared. (self: %s)", _name, repr(self))
 
-
     # Wrapper for _publish_impl that also makes sure the event is published from
-    # a class that supports it. 
+    # a class that supports it.
     # The underscore _name is to avoid naming collisions with callback params
     def _publish(self, _name, *args, **kwargs):
         self._check_event(_name)
@@ -124,7 +125,7 @@ class Eventful(object):
             for callback in methods:
                 callback(robj(), *args, **kwargs)
 
-        #The include_source flag indicates to prepend the source of the event in
+        # The include_source flag indicates to prepend the source of the event in
         # the callback signature. This is set on forward_events_from/to
         for sink, include_source in self._forwards.items():
             if include_source:
@@ -137,7 +138,7 @@ class Eventful(object):
             raise TypeError
         obj, callback = method.__self__, method.__func__
         bucket = self._get_signal_bucket(name)
-        robj = ref(obj, self._unref)  #see unref() for explanation
+        robj = ref(obj, self._unref)  # see unref() for explanation
         bucket.setdefault(robj, set()).add(callback)
 
     def forward_events_from(self, source, include_source=False):

manticore/utils/helpers.py

@@ -1,6 +1,7 @@
 import collections
 from ..core.smtlib import Expression
 
+
 def issymbolic(value):
     '''
     Helper to determine whether an object is symbolic (e.g checking
@@ -12,34 +13,40 @@ def issymbolic(value):
     '''
     return isinstance(value, Expression)
 
+
 import functools
 
+
 class memoized(object):
-   '''Decorator. Caches a function's return value each time it is called.
-   If called later with the same arguments, the cached value is returned
-   (not reevaluated).
-   '''
-   def __init__(self, func):
-      self.func = func
-      self.cache = {}
-   def __call__(self, *args, **kwargs):
-      key = args + tuple(sorted(kwargs.items()))
-      if not isinstance(key, collections.Hashable):
-         # uncacheable. a list, for instance.
-         # better to not cache than blow up.
-         return self.func(*args, **kwargs)
-      if key in self.cache:
-         return self.cache[key]
-      else:
-         value = self.func(*args, **kwargs)
-         self.cache[key] = value
-         return value
-   def __repr__(self):
-      '''Return the function's docstring.'''
-      return self.func.__doc__
-   def __get__(self, obj, objtype):
-      '''Support instance methods.'''
-      return functools.partial(self.__call__, obj)
+    '''Decorator. Caches a function's return value each time it is called.
+    If called later with the same arguments, the cached value is returned
+    (not reevaluated).
+    '''
+
+    def __init__(self, func):
+        self.func = func
+        self.cache = {}
+
+    def __call__(self, *args, **kwargs):
+        key = args + tuple(sorted(kwargs.items()))
+        if not isinstance(key, collections.Hashable):
+            # uncacheable. a list, for instance.
+            # better to not cache than blow up.
+            return self.func(*args, **kwargs)
+        if key in self.cache:
+            return self.cache[key]
+        else:
+            value = self.func(*args, **kwargs)
+            self.cache[key] = value
+            return value
+
+    def __repr__(self):
+        '''Return the function's docstring.'''
+        return self.func.__doc__
+
+    def __get__(self, obj, objtype):
+        '''Support instance methods.'''
+        return functools.partial(self.__call__, obj)
 
 
 def is_binja_disassembler(disasm):

manticore/utils/iterpickle.py

@@ -55,16 +55,17 @@ HIGHEST_PROTOCOL = 2
 # marshal.loads() is twice as fast as struct.unpack()!
 mloads = marshal.loads
 
+
 class PickleError(Exception):
     """A common base class for the other pickling exceptions."""
-    pass
+
 
 class PicklingError(PickleError):
     """This exception is raised when an unpicklable object is passed to the
     dump() method.
 
     """
-    pass
+
 
 class UnpicklingError(PickleError):
     """This exception is raised when there is a problem unpickling an object,
@@ -75,14 +76,16 @@ class UnpicklingError(PickleError):
     and IndexError.
 
     """
-    pass
 
 # An instance of _Stop is raised by Unpickler.load_stop() in response to
 # the STOP opcode, passing the object that is the result of unpickling.
+
+
 class _Stop(Exception):
     def __init__(self, value):
         self.value = value
 
+
 # Jython has PyStringMap; it's a dict subclass with string keys
 try:
     from org.python.core import PyStringMap
@@ -99,70 +102,70 @@ except NameError:
 # here is in kind-of alphabetical order of 1-character pickle code.
 # pickletools groups them by purpose.
 
-MARK            = '('   # push special markobject on stack
-STOP            = '.'   # every pickle ends with STOP
-POP             = '0'   # discard topmost stack item
-POP_MARK        = '1'   # discard stack top through topmost markobject
-DUP             = '2'   # duplicate top stack item
-FLOAT           = 'F'   # push float object; decimal string argument
-INT             = 'I'   # push integer or bool; decimal string argument
-BININT          = 'J'   # push four-byte signed int
-BININT1         = 'K'   # push 1-byte unsigned int
-LONG            = 'L'   # push long; decimal string argument
-BININT2         = 'M'   # push 2-byte unsigned int
-NONE            = 'N'   # push None
-PERSID          = 'P'   # push persistent object; id is taken from string arg
-BINPERSID       = 'Q'   #  "       "         "  ;  "  "   "     "  stack
-REDUCE          = 'R'   # apply callable to argtuple, both on stack
-STRING          = 'S'   # push string; NL-terminated string argument
-BINSTRING       = 'T'   # push string; counted binary string argument
-SHORT_BINSTRING = 'U'   #  "     "   ;    "      "       "      " < 256 bytes
-UNICODE         = 'V'   # push Unicode string; raw-unicode-escaped'd argument
-BINUNICODE      = 'X'   #   "     "       "  ; counted UTF-8 string argument
-APPEND          = 'a'   # append stack top to list below it
-BUILD           = 'b'   # call __setstate__ or __dict__.update()
-GLOBAL          = 'c'   # push self.find_class(modname, name); 2 string args
-DICT            = 'd'   # build a dict from stack items
-EMPTY_DICT      = '}'   # push empty dict
-APPENDS         = 'e'   # extend list on stack by topmost stack slice
-GET             = 'g'   # push item from memo on stack; index is string arg
-BINGET          = 'h'   #   "    "    "    "   "   "  ;   "    " 1-byte arg
-INST            = 'i'   # build & push class instance
-LONG_BINGET     = 'j'   # push item from memo on stack; index is 4-byte arg
-LIST            = 'l'   # build list from topmost stack items
-EMPTY_LIST      = ']'   # push empty list
-OBJ             = 'o'   # build & push class instance
-PUT             = 'p'   # store stack top in memo; index is string arg
-BINPUT          = 'q'   #   "     "    "   "   " ;   "    " 1-byte arg
-LONG_BINPUT     = 'r'   #   "     "    "   "   " ;   "    " 4-byte arg
-SETITEM         = 's'   # add key+value pair to dict
-TUPLE           = 't'   # build tuple from topmost stack items
-EMPTY_TUPLE     = ')'   # push empty tuple
-SETITEMS        = 'u'   # modify dict by adding topmost key+value pairs
-BINFLOAT        = 'G'   # push float; arg is 8-byte float encoding
+MARK = '('   # push special markobject on stack
+STOP = '.'   # every pickle ends with STOP
+POP = '0'   # discard topmost stack item
+POP_MARK = '1'   # discard stack top through topmost markobject
+DUP = '2'   # duplicate top stack item
+FLOAT = 'F'   # push float object; decimal string argument
+INT = 'I'   # push integer or bool; decimal string argument
+BININT = 'J'   # push four-byte signed int
+BININT1 = 'K'   # push 1-byte unsigned int
+LONG = 'L'   # push long; decimal string argument
+BININT2 = 'M'   # push 2-byte unsigned int
+NONE = 'N'   # push None
+PERSID = 'P'   # push persistent object; id is taken from string arg
+BINPERSID = 'Q'  # "       "         "  ;  "  "   "     "  stack
+REDUCE = 'R'   # apply callable to argtuple, both on stack
+STRING = 'S'   # push string; NL-terminated string argument
+BINSTRING = 'T'   # push string; counted binary string argument
+SHORT_BINSTRING = 'U'  # "     "   ;    "      "       "      " < 256 bytes
+UNICODE = 'V'   # push Unicode string; raw-unicode-escaped'd argument
+BINUNICODE = 'X'  # "     "       "  ; counted UTF-8 string argument
+APPEND = 'a'   # append stack top to list below it
+BUILD = 'b'   # call __setstate__ or __dict__.update()
+GLOBAL = 'c'   # push self.find_class(modname, name); 2 string args
+DICT = 'd'   # build a dict from stack items
+EMPTY_DICT = '}'   # push empty dict
+APPENDS = 'e'   # extend list on stack by topmost stack slice
+GET = 'g'   # push item from memo on stack; index is string arg
+BINGET = 'h'  # "    "    "    "   "   "  ;   "    " 1-byte arg
+INST = 'i'   # build & push class instance
+LONG_BINGET = 'j'   # push item from memo on stack; index is 4-byte arg
+LIST = 'l'   # build list from topmost stack items
+EMPTY_LIST = ']'   # push empty list
+OBJ = 'o'   # build & push class instance
+PUT = 'p'   # store stack top in memo; index is string arg
+BINPUT = 'q'  # "     "    "   "   " ;   "    " 1-byte arg
+LONG_BINPUT = 'r'  # "     "    "   "   " ;   "    " 4-byte arg
+SETITEM = 's'   # add key+value pair to dict
+TUPLE = 't'   # build tuple from topmost stack items
+EMPTY_TUPLE = ')'   # push empty tuple
+SETITEMS = 'u'   # modify dict by adding topmost key+value pairs
+BINFLOAT = 'G'   # push float; arg is 8-byte float encoding
 
-TRUE            = 'I01\n'  # not an opcode; see INT docs in pickletools.py
-FALSE           = 'I00\n'  # not an opcode; see INT docs in pickletools.py
+TRUE = 'I01\n'  # not an opcode; see INT docs in pickletools.py
+FALSE = 'I00\n'  # not an opcode; see INT docs in pickletools.py
 
 # Protocol 2
 
-PROTO           = '\x80'  # identify pickle protocol
-NEWOBJ          = '\x81'  # build object by applying cls.__new__ to argtuple
-EXT1            = '\x82'  # push object from extension registry; 1-byte index
-EXT2            = '\x83'  # ditto, but 2-byte index
-EXT4            = '\x84'  # ditto, but 4-byte index
-TUPLE1          = '\x85'  # build 1-tuple from stack top
-TUPLE2          = '\x86'  # build 2-tuple from two topmost stack items
-TUPLE3          = '\x87'  # build 3-tuple from three topmost stack items
-NEWTRUE         = '\x88'  # push True
-NEWFALSE        = '\x89'  # push False
-LONG1           = '\x8a'  # push long from < 256 bytes
-LONG4           = '\x8b'  # push really big long
+PROTO = '\x80'  # identify pickle protocol
+NEWOBJ = '\x81'  # build object by applying cls.__new__ to argtuple
+EXT1 = '\x82'  # push object from extension registry; 1-byte index
+EXT2 = '\x83'  # ditto, but 2-byte index
+EXT4 = '\x84'  # ditto, but 4-byte index
+TUPLE1 = '\x85'  # build 1-tuple from stack top
+TUPLE2 = '\x86'  # build 2-tuple from two topmost stack items
+TUPLE3 = '\x87'  # build 3-tuple from three topmost stack items
+NEWTRUE = '\x88'  # push True
+NEWFALSE = '\x89'  # push False
+LONG1 = '\x8a'  # push long from < 256 bytes
+LONG4 = '\x8b'  # push really big long
 
 _tuplesize2code = [EMPTY_TUPLE, TUPLE1, TUPLE2, TUPLE3]
 
 
-__all__.extend([x for x in dir() if re.match("[A-Z][A-Z0-9_]+$",x)])
+__all__.extend([x for x in dir() if re.match("[A-Z][A-Z0-9_]+$", x)])
 del x
 
 
@@ -221,11 +224,11 @@ class Pickler:
         """Write a pickled representation of obj to the open file."""
         if self.proto >= 2:
             self.write(PROTO + chr(self.proto))
-        
+
         # By faking recursion using generators, pickle is no longer dependent
         # on python's recursion limit. This means that hugely recursive data
         # structures can be pickled without a problem! It's also still just
-        # about as fast as it was for simple structures, albeit slower for 
+        # about as fast as it was for simple structures, albeit slower for
         # large structures.
         callstack = [self.save(obj)]
         while callstack:
@@ -236,7 +239,7 @@ class Pickler:
             else:
                 if result is not None:
                     callstack.append(result)
-        
+
         self.write(STOP)
 
     def memoize(self, obj):
@@ -298,7 +301,7 @@ class Pickler:
         t = type(obj)
         f = self.dispatch.get(t)
         if f:
-            yield f(self, obj) # Call unbound method with explicit self
+            yield f(self, obj)  # Call unbound method with explicit self
             return
 
         # Check copy_reg.dispatch_table
@@ -309,7 +312,7 @@ class Pickler:
             # Check for a class with a custom metaclass; treat as regular class
             try:
                 issc = issubclass(t, TypeType)
-            except TypeError: # t is not a class (old Boost; see SF #502085)
+            except TypeError:  # t is not a class (old Boost; see SF #502085)
                 issc = 0
             if issc:
                 yield self.save_global(obj)
@@ -328,12 +331,12 @@ class Pickler:
                                         (t.__name__, obj))
 
         # Check for string returned by reduce(), meaning "save as global"
-        if type(rv) is StringType:
+        if isinstance(rv, StringType):
             yield self.save_global(obj, rv)
             return
 
         # Assert that reduce() returned a tuple
-        if type(rv) is not TupleType:
+        if not isinstance(rv, TupleType):
             raise PicklingError("%s must return string or tuple" % reduce)
 
         # Assert that it returned an appropriately sized tuple
@@ -460,7 +463,7 @@ class Pickler:
                     self.write(BININT1 + chr(obj))
                     return
                 if obj <= 0xffff:
-                    self.write("%c%c%c" % (BININT2, obj&0xff, obj>>8))
+                    self.write("%c%c%c" % (BININT2, obj & 0xff, obj >> 8))
                     return
             # Next check for 4-byte signed ints:
             high_bits = obj >> 31  # note that Python shift sign-extends
@@ -588,7 +591,7 @@ class Pickler:
             if proto:
                 write(POP_MARK + get)
             else:   # proto 0 -- POP_MARK not available
-                write(POP * (n+1) + get)
+                write(POP * (n + 1) + get)
             return
 
         # No recursion.
@@ -664,7 +667,7 @@ class Pickler:
         yield self._batch_setitems(obj.iteritems())
 
     dispatch[DictionaryType] = save_dict
-    if not PyStringMap is None:
+    if PyStringMap is not None:
         dispatch[PyStringMap] = save_dict
 
     def _batch_setitems(self, items):
@@ -705,13 +708,13 @@ class Pickler:
     def save_inst(self, obj):
         cls = obj.__class__
 
-        memo  = self.memo
+        memo = self.memo
         write = self.write
-        save  = self.save
+        save = self.save
 
         if hasattr(obj, '__getinitargs__'):
             args = obj.__getinitargs__()
-            len(args) # XXX Assert it's a sequence
+            len(args)  # XXX Assert it's a sequence
             _keep_alive(args, memo)
         else:
             args = ()
@@ -774,7 +777,7 @@ class Pickler:
                 if code <= 0xff:
                     write(EXT1 + chr(code))
                 elif code <= 0xffff:
-                    write("%c%c%c" % (EXT2, code&0xff, code>>8))
+                    write("%c%c%c" % (EXT2, code & 0xff, code >> 8))
                 else:
                     write(EXT4 + pack("<i", code))
                 return
@@ -789,6 +792,7 @@ class Pickler:
 
 # Pickling helpers
 
+
 def _keep_alive(x, memo):
     """Keeps a reference to the object x in the memo.
 
@@ -803,13 +807,14 @@ def _keep_alive(x, memo):
         memo[id(memo)].append(x)
     except KeyError:
         # aha, this is the first one :-)
-        memo[id(memo)]=[x]
+        memo[id(memo)] = [x]
 
 
 # A cache for whichmodule(), mapping a function object to the name of
 # the module in which the function was found.
 
-classmap = {} # called classmap for backwards compatibility
+classmap = {}  # called classmap for backwards compatibility
+
 
 def whichmodule(func, funcname):
     """Figure out the module in which a function occurs.
@@ -828,7 +833,7 @@ def whichmodule(func, funcname):
 
     for name, module in sys.modules.items():
         if module is None:
-            continue # skip dummy package entries
+            continue  # skip dummy package entries
         if name != '__main__' and getattr(module, funcname, None) is func:
             break
     else:
@@ -862,16 +867,16 @@ class Unpickler:
 
         Return the reconstituted object hierarchy specified in the file.
         """
-        self.mark = object() # any new unique object
+        self.mark = object()  # any new unique object
         self.stack = []
         self.append = self.stack.append
         read = self.read
         dispatch = self.dispatch
         try:
-            while 1:
+            while True:
                 key = read(1)
                 dispatch[key](self)
-        except _Stop, stopinst:
+        except _Stop as stopinst:
             return stopinst.value
 
     # Return largest index k such that self.stack[k] is self.mark.
@@ -885,8 +890,9 @@ class Unpickler:
     def marker(self):
         stack = self.stack
         mark = self.mark
-        k = len(stack)-1
-        while stack[k] is not mark: k = k-1
+        k = len(stack) - 1
+        while stack[k] is not mark:
+            k = k - 1
         return k
 
     dispatch = {}
@@ -975,7 +981,7 @@ class Unpickler:
 
     def load_string(self):
         rep = self.readline()[:-1]
-        for q in "\"'": # double or single quote
+        for q in "\"'":  # double or single quote
             if rep.startswith(q):
                 if len(rep) < 2 or not rep.endswith(q):
                     raise ValueError, "insecure string pickle"
@@ -992,12 +998,12 @@ class Unpickler:
     dispatch[BINSTRING] = load_binstring
 
     def load_unicode(self):
-        self.append(unicode(self.readline()[:-1],'raw-unicode-escape'))
+        self.append(unicode(self.readline()[:-1], 'raw-unicode-escape'))
     dispatch[UNICODE] = load_unicode
 
     def load_binunicode(self):
         len = mloads('i' + self.read(4))
-        self.append(unicode(self.read(len),'utf-8'))
+        self.append(unicode(self.read(len), 'utf-8'))
     dispatch[BINUNICODE] = load_binunicode
 
     def load_short_binstring(self):
@@ -1007,7 +1013,7 @@ class Unpickler:
 
     def load_tuple(self):
         k = self.marker()
-        self.stack[k:] = [tuple(self.stack[k+1:])]
+        self.stack[k:] = [tuple(self.stack[k + 1:])]
     dispatch[TUPLE] = load_tuple
 
     def load_empty_tuple(self):
@@ -1036,16 +1042,16 @@ class Unpickler:
 
     def load_list(self):
         k = self.marker()
-        self.stack[k:] = [self.stack[k+1:]]
+        self.stack[k:] = [self.stack[k + 1:]]
     dispatch[LIST] = load_list
 
     def load_dict(self):
         k = self.marker()
         d = {}
-        items = self.stack[k+1:]
+        items = self.stack[k + 1:]
         for i in range(0, len(items), 2):
             key = items[i]
-            value = items[i+1]
+            value = items[i + 1]
             d[key] = value
         self.stack[k:] = [d]
     dispatch[DICT] = load_dict
@@ -1056,11 +1062,11 @@ class Unpickler:
     # klass is the class to instantiate, and k points to the topmost mark
     # object, following which are the arguments for klass.__init__.
     def _instantiate(self, klass, k):
-        args = tuple(self.stack[k+1:])
+        args = tuple(self.stack[k + 1:])
         del self.stack[k:]
         instantiated = 0
         if (not args and
-                type(klass) is ClassType and
+                isinstance(klass, ClassType) and
                 not hasattr(klass, "__getinitargs__")):
             try:
                 value = _EmptyClass()
@@ -1073,7 +1079,7 @@ class Unpickler:
         if not instantiated:
             try:
                 value = klass(*args)
-            except TypeError, err:
+            except TypeError as err:
                 raise TypeError, "in constructor for %s: %s" % (
                     klass.__name__, str(err)), sys.exc_info()[2]
         self.append(value)
@@ -1088,7 +1094,7 @@ class Unpickler:
     def load_obj(self):
         # Stack is ... markobject classobject arg1 arg2 ...
         k = self.marker()
-        klass = self.stack.pop(k+1)
+        klass = self.stack.pop(k + 1)
         self._instantiate(klass, k)
     dispatch[OBJ] = load_obj
 
@@ -1273,13 +1279,16 @@ class Unpickler:
 
 # Helper class for load_inst/load_obj
 
+
 class _EmptyClass:
     pass
 
 # Encode/decode longs in linear time.
 
+
 import binascii as _binascii
 
+
 def encode_long(x):
     r"""Encode a long to a two's complement little-endian binary string.
     Note that 0L is a special case, returning an empty string, to save a
@@ -1327,7 +1336,7 @@ def encode_long(x):
             # Extend to a full byte.
             nibbles += 1
         nbits = nibbles * 4
-        x += 1L << nbits
+        x += 1 << nbits
         assert x > 0
         ashex = hex(x)
         njunkchars = 2 + ashex.endswith('L')
@@ -1346,6 +1355,7 @@ def encode_long(x):
     binary = _binascii.unhexlify(ashex)
     return binary[::-1]
 
+
 def decode_long(data):
     r"""Decode a long from a two's complement little-endian binary string.
 
@@ -1367,40 +1377,47 @@ def decode_long(data):
 
     nbytes = len(data)
     if nbytes == 0:
-        return 0L
+        return 0
     ashex = _binascii.hexlify(data[::-1])
-    n = long(ashex, 16) # quadratic time before Python 2.3; linear now
+    n = long(ashex, 16)  # quadratic time before Python 2.3; linear now
     if data[-1] >= '\x80':
-        n -= 1L << (nbytes * 8)
+        n -= 1 << (nbytes * 8)
     return n
 
 # Shorthands
 
+
 try:
     from cStringIO import StringIO
 except ImportError:
     from StringIO import StringIO
 
+
 def dump(obj, file, protocol=None):
     Pickler(file, protocol).dump(obj)
 
+
 def dumps(obj, protocol=None):
     file = StringIO()
     Pickler(file, protocol).dump(obj)
     return file.getvalue()
 
+
 def load(file):
     return Unpickler(file).load()
 
+
 def loads(str):
     file = StringIO(str)
     return Unpickler(file).load()
 
 # Doctest
 
+
 def _test():
     import doctest
     return doctest.testmod()
 
+
 if __name__ == "__main__":
     _test()

manticore/utils/log.py

@@ -2,10 +2,12 @@ import logging
 import sys
 import types
 
+
 class ContextFilter(logging.Filter):
     '''
     This is a filter which injects contextual information into the log.
     '''
+
     def summarized_name(self, name):
         '''
         Produce a summarized record name
@@ -24,13 +26,15 @@ class ContextFilter(logging.Filter):
         record.name = self.summarized_name(record.name)
         return True
 
+
 manticore_verbosity = 0
 all_loggers = []
 
+
 def init_logging():
     global all_loggers
     loggers = logging.getLogger().manager.loggerDict.keys()
-        
+
     ctxfilter = ContextFilter()
     logfmt = ("%(asctime)s: [%(process)d]%(stateid)s %(name)s:%(levelname)s:"
               " %(message)s")
@@ -51,9 +55,11 @@ def init_logging():
         all_loggers.append(name)
     set_verbosity(manticore_verbosity)
 
+
 def loggerSetState(logger, stateid):
     logger.filters[0].stateid = stateid
 
+
 def set_verbosity(setting):
     global manticore_verbosity, all_loggers
     zero = map(lambda x: (x, logging.WARNING), all_loggers)
@@ -88,7 +94,7 @@ def set_verbosity(setting):
             ('manticore.manticore', logging.DEBUG),
             ('manticore.core.smtlib', logging.DEBUG),
             ('manticore.core.smtlib.*', logging.DEBUG)
-         ]
+        ]
     ]
 
     def match(name, pattern):

manticore/utils/mappings.py

@@ -18,23 +18,21 @@ if osname == "darwin" or osname.startswith("linux"):
     mmap_function = libc.mmap
     mmap_function.restype = ctypes.c_void_p
     mmap_function.argtype = [ctypes.c_void_p, ctypes.c_size_t,
-        ctypes.c_int, ctypes.c_int, ctypes.c_int, ctypes.c_size_t]
+                             ctypes.c_int, ctypes.c_int, ctypes.c_int, ctypes.c_size_t]
     # int munmap(void* addr, size_t len)
     munmap_function = libc.munmap
     munmap_function.restype = ctypes.c_int
     munmap_function.argtype = [ctypes.c_void_p, ctypes.c_size_t]
 
-
-    def _munmap(address,size):
+    def _munmap(address, size):
         result = munmap_function(address, size)
         assert result == 0
 
-
     def _mmap(fd, offset, size):
         prot = MMAP.PROT_READ | MMAP.PROT_WRITE
         flags = MMAP.MAP_PRIVATE
 
-        if size &0xfff !=0:
+        if size & 0xfff != 0:
             size = (size & ~0xfff) + 0x1000
 
         assert size > 0
@@ -47,4 +45,3 @@ if osname == "darwin" or osname.startswith("linux"):
 
 else:
     raise ValueError("Unsupported host OS: " + osname)
-

manticore/utils/nointerrupt.py

@@ -1,6 +1,7 @@
 import signal
 import logging
 
+
 class WithKeyboardInterruptAs(object):
     def __init__(self, callback):
         if callback is None:

tox.ini

@@ -0,0 +1,12 @@
+[tox]
+envlist = py27,py35
+
+[testenv]
+deps = .[dev]
+commands = nosetests
+install_command = pip install --no-binary keystone-engine {opts} {packages}
+
+[pep8]
+ignore = E265,E501
+max-line-length = 160
+exclude = docs/,examples/,scripts/,tests/