Trace following mode (#513)

* WIP New Policy class

* WIP pubsub

* Update Signal tests

* small fixes from github comments

* Fix event decode_instruction signature

* Good merge

* Good good merge

* WIP manticore refactor

* Fix default old-style initial state

* add -> enqueue

* @m.init

* Fix workspace url

* Some test skipped

* Ad Fixme to platform specific stuff in State

* add -> enqueue

* Enqueue created state

* Fix m.init

Use a messy hack to adhere to the spec (callback func receive 1 state argument)

* Add _coverage_file ivar to Manticore

* Fix symbolic files

* remove extra enqueue

* Fixing __main__

* comments

* Experimental plugin system

* tests fixed

* Fix plugins

* Some reporting moved to plugin

* Fix assertions test

* Add published events to classes that publish them

* Update how we verify callbacks

* Update Eventful._publish

* Yet another flavor for event name checking

* really it's a bunch of minimal bugfixes

* Remove get_all_event_names from Plugin

* Update where we get all events

* Use new metaclass-based event registry

* Initial concrete trace follower

* Add extended (json) trace support

* More stubs for condition gather

* Update trace saving to new format

* Produce trace regardless of contents

* Record register deltas in trace

* Move initialization to _start_run so we can call run() multiple times

* Re-fix multiple workspace bug

* Fix it correctly

* Add extended trace and accessors

* make sure did_execute_instruction is always published

* Produce a consistent version

* move extended tracing to separate class

* Reorg of extended tracing plugins

* Add concolic tracing script

* Clean up old hooks

* Sync memory as well; cleanups

* Revert binary tests

* simplify concolic follower

* Move trace follower to plugin.py

* Simplify follower

* Add skip ranges to Follower

* Update concolic.py

* Remove redundant state init

* Clean up driver script

* Update header line

* Move trace follower

* Move Follower to follow_trace.py

* rm unused import

* Remove unnecessary property

* rm ConcreteTraceFollower

* Revert start_run behavior

manticore/core/plugin.py

@@ -1,12 +1,32 @@
 import logging
+
+from capstone import CS_GRP_JUMP
+
 from ..utils.helpers import issymbolic
-from ..utils.event import Eventful
 logger = logging.getLogger('MANTICORE')
 
 
 class Plugin(object):
     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
+    aren't in d1.
+
+    :param dict d1: First dict
+    :param dict d2: Dict to compare with
+    :rtype: dict
+    '''
+    d = {}
+    for key in set(d1).intersection(set(d2)):
+        if d2[key] != d1[key]:
+            d[key] = d2[key]
+    for key in set(d2).difference(set(d1)):
+        d[key] = d2[key]
+    return d
 
 class Tracer(Plugin):
     def will_start_run_callback(self, state):
@@ -15,6 +35,69 @@ 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):
+        '''
+        Record a detailed execution trace
+        '''
+        super(ExtendedTracer, self).__init__()
+        self.last_dict = {}
+        self.current_pc = None
+        self.context_key = 'e_trace'
+
+    def will_start_run_callback(self, state):
+        state.context[self.context_key] = []
+
+    def register_state_to_dict(self, cpu):
+        d = {}
+        for reg in cpu.canonical_registers:
+            val = cpu.read_register(reg)
+            d[reg] = val if not issymbolic(val) else '<sym>'
+        return d
+
+    def will_execute_instruction_callback(self, state, pc, instruction):
+        self.current_pc = pc
+
+    def did_execute_instruction_callback(self, state, pc, target_pc, instruction):
+        reg_state = self.register_state_to_dict(state.cpu)
+        entry = {
+            'type': 'regs',
+            'values': _dict_diff(self.last_dict, reg_state)
+        }
+        self.last_dict = reg_state
+        state.context[self.context_key].append(entry)
+
+    def will_read_memory_callback(self, state, where, size):
+        if self.current_pc == where:
+            return
+
+        #print 'will_read_memory %x %r, current_pc %x'%(where, size, self.current_pc)
+
+    def did_read_memory_callback(self, state, where, value, size):
+        if self.current_pc == where:
+            return
+
+        #print 'did_read_memory %x %r %r, current_pc %x'%(where, value, size, self.current_pc)
+
+    def will_write_memory_callback(self, state, where, value, size):
+        if self.current_pc == where:
+            return
+
+        #print 'will_write_memory %x %r %r, current_pc %x'%(where, value, size, self.current_pc)
+
+    def did_write_memory_callback(self, state, where, value, size):
+        if self.current_pc == where:
+            raise Exception
+            return
+
+        entry = {
+            'type': 'mem_write',
+            'where': where,
+            'value': value,
+            'size': size
+        }
+        state.context[self.context_key].append(entry)
+
 class RecordSymbolicBranches(Plugin):
     def will_start_run_callback(self, state):
         state.context['branches'] = {}
@@ -91,7 +174,6 @@ class Visited(Plugin):
         logger.info('Coverage: %d different instructions executed', len(executor_visited))
 
 
-
 #TODO document all callbacks
 class ExamplePlugin(Plugin):
     def will_decode_instruction_callback(self, state, pc):

manticore/core/workspace.py

@@ -517,8 +517,8 @@ class ManticoreOutput(object):
         with self._named_stream('trace') as f:
             if 'trace' not in state.context:
                 return
-            for pc in state.context['trace']:
+            for entry in state.context['trace']:
-                f.write('0x{:08x}\n'.format(pc))
+                f.write('0x{:x}'.format(entry))
 
     def save_constraints(self, state):
         # XXX(yan): We want to conditionally enable this check

manticore/manticore.py

@@ -181,6 +181,7 @@ class Manticore(Eventful):
         #Move the folowing into a plugin
         self._assertions = {}
         self._coverage_file = None
+        self.trace = None
 
         #FIXME move the folowing to aplugin
         self.subscribe('will_generate_testcase', self._generate_testcase_callback)

manticore/platforms/linux.py

@@ -1238,7 +1238,7 @@ class Linux(Platform):
         def pad(s):
             return s +'\x00'*(65-len(s))
 
-        now = datetime.now().strftime("%a %b %d %H:%M:%S ART %Y")
+        now = datetime(2017, 8, 01).strftime("%a %b %d %H:%M:%S ART %Y")
         info = (('sysname', 'Linux'),
                 ('nodename', 'ubuntu'),
                 ('release', '4.4.0-77-generic'),

scripts/follow_trace.py

@@ -0,0 +1,118 @@
+#!/usr/bin/env python
+
+'''
+A simple trace following execution driver script. Only supports passing symbolic arguments via argv.
+
+'''
+
+import sys
+import time
+import argparse
+import itertools
+
+from manticore import Manticore, issymbolic
+from manticore.core.plugin import ExtendedTracer, Plugin
+
+def _partition(pred, iterable):
+    t1, t2 = itertools.tee(iterable)
+    return (list(itertools.ifilterfalse(pred, t1)), filter(pred, t2))
+
+
+class TraceReceiver(Plugin):
+    def __init__(self, tracer):
+        self._trace = None
+        self._tracer = tracer
+        super(self.__class__, self).__init__()
+
+    @property
+    def trace(self):
+        return self._trace
+
+    def will_generate_testcase_callback(self, state, test_id, msg):
+        self._trace = state.context[self._tracer.context_key]
+
+        instructions, writes = _partition(lambda x: x['type'] == 'regs', self._trace)
+        total = len(self._trace)
+        print 'Recorded concrete trace: {}/{} instructions, {}/{} writes'.format(
+            len(instructions), total, len(writes), total)
+
+
+class Follower(Plugin):
+    def __init__(self, trace):
+        self.index = 0
+        self.trace = trace
+        self.last_instruction = None
+        self.symbolic_ranges = []
+        self.active = True
+        super(self.__class__, self).__init__()
+
+    def add_symbolic_range(self, pc_start, pc_end):
+        self.symbolic_ranges.append((pc_start,pc_end))
+
+    def get_next(self, type):
+        event = self.trace[self.index]
+        assert event['type'] == type
+        self.index += 1
+        return event
+
+    def did_write_memory_callback(self, state, where, value, size):
+        if not self.active:
+            return
+        write = self.get_next('mem_write')
+
+        if not issymbolic(value):
+            return
+
+        assert write['where'] == where and write['size'] == size
+        state.constrain(value == write['value'])
+
+    def did_execute_instruction_callback(self, state, last_pc, pc, insn):
+        if not self.active:
+            return
+        event = self.get_next('regs')
+        self.last_instruction = event['values']
+        if issymbolic(pc):
+            state.constrain(state.cpu.RIP == self.last_instruction['RIP'])
+        else:
+            for start, stop in self.symbolic_ranges:
+                if start <= pc <= stop:
+                    self.active = False
+
+
+def main():
+    parser = argparse.ArgumentParser(description='Follow a concrete trace')
+    parser.add_argument('-f', '--explore_from', help='Value of PC from which to explore symbolically', type=str)
+    parser.add_argument('-t', '--explore_to', type=str, default=sys.maxint,
+                        help="Value of PC until which to explore symbolically. (Probably don't want this set)")
+    parser.add_argument('--verbose', '-v', action='count', help='Increase verbosity')
+    parser.add_argument('cmd', type=str, nargs='+',
+                        help='Program and arguments. Use "--" to separate script arguments from target arguments')
+    args = parser.parse_args(sys.argv[1:])
+
+    range = None
+    if args.explore_from:
+        range = (args.explore_from, args.explore_to)
+
+    # Create a concrete Manticore and record it
+    m1 = Manticore.linux(args.cmd[0], args.cmd[1:])
+    t = ExtendedTracer()
+    r = TraceReceiver(t)
+    m1.verbosity(args.verbose)
+    m1.register_plugin(t)
+    m1.register_plugin(r)
+    m1.run(procs=1)
+
+    time.sleep(3)
+
+    # Create a symbolic Manticore and follow last trace
+    symbolic_args = ['+'*len(arg) for arg in args.cmd[1:]]
+    m2 = Manticore.linux(args.cmd[0], symbolic_args)
+    f = Follower(r.trace)
+    if range:
+        f.add_symbolic_range(*range)
+    m2.verbosity(args.verbose)
+    m2.register_plugin(f)
+    m2.run()
+
+if __name__=='__main__':
+    main()