Implement symbolic branch tracking in core, add new fork event (#433)

* Add fork_state event for individual state forks

* Rename to forking_state, add branch tracking to state

* Remove unnecessary locking around event publishing

manticore/core/executor.py

@@ -315,18 +315,20 @@ class Executor(Eventful):
         #Find a set of solutions for expression
         solutions = state.concretize(expression, policy)
 
-        #We are about to fork current_state
-        with self._lock:
         self.publish('will_fork_state', state, expression, solutions, policy)
 
         #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) #We already know it's sat
+                new_state.constrain(expression == new_value)
+
                 #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('forking_state', new_state, expression, new_value, policy)
+
                 #enqueue new_state
                 state_id = self.add(new_state)
                 #maintain a list of childres for logging purpose

manticore/core/state.py

@@ -76,10 +76,19 @@ class State(Eventful):
         self._input_symbols = list()
         self._child = None
         self._context = dict()
+        self._init_context()
         ##################################################################33
         # Events are lost in serialization and fork !!
         self.forward_events_from(platform)
 
+    def record_branch(self, target):
+        branches = self.context['branches']
+        branch = (self.cpu._last_pc, target)
+        if branch in branches:
+            branches[branch] += 1
+        else:
+            branches[branch] = 1
+
     def __getstate__(self):
         state = super(State, self).__getstate__()
         state['platform'] = self._platform
@@ -352,3 +361,6 @@ class State(Eventful):
     @property
     def mem(self):
         return self._platform.current.memory
+
+    def _init_context(self):
+        self.context['branches'] = dict()

manticore/manticore.py

@@ -564,6 +564,9 @@ class Manticore(object):
             manticore_instructions_count = manticore_context.get('instructions_count', 0)
             manticore_context['instructions_count'] = manticore_instructions_count + state_instructions_count
 
+    def _forking_state_callback(self, state, expression, value, policy):
+        state.record_branch(value)
+
     def _fork_state_callback(self, state, expression, values, policy):
         state_visited = state.context.get('visited_since_last_fork', set())
         with self.locked_context() as manticore_context:
@@ -721,6 +724,7 @@ class Manticore(object):
         self._executor.subscribe('will_store_state', self._store_state_callback)
         self._executor.subscribe('will_load_state', self._load_state_callback)
         self._executor.subscribe('will_fork_state', self._fork_state_callback)
+        self._executor.subscribe('forking_state', self._forking_state_callback)
         self._executor.subscribe('will_terminate_state', self._terminate_state_callback)
         self._executor.subscribe('will_generate_testcase', self._generate_testcase_callback)