Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Initial master merge into experimental state merging for native #1482

Merged
merged 9 commits into from
Aug 5, 2019
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 30 additions & 0 deletions examples/script/basic_statemerging.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
#!/usr/bin/env python

import sys

from manticore.native.plugins import Merger
from manticore.utils import config

from manticore.native import Manticore
from manticore import set_verbosity

"""
Demonstrates the ability to do state merging on a simple program by merging states with id 2, 4 that happen to be
at the same program location 0x40060d. This script uses the Merger plugin to apply opportunistic state merging.
"""
if __name__ == "__main__":
config.get_group("core").seed = 2
config.get_group("core").mprocessing = config.get_group("core").mprocessing.single
path = sys.argv[1]
m = Manticore(path, policy="random")

def will_load_state_callback(_, state_id):
print("about to load state_id = " + str(state_id))

def did_load_state_callback(_, state, state_id):
print("loaded state_id = " + str(state_id) + " at cpu = " + hex(state.cpu.PC))

m.subscribe("will_load_state", will_load_state_callback)
m.subscribe("did_load_state", did_load_state_callback)
m.register_plugin(Merger())
m.run()
16 changes: 8 additions & 8 deletions manticore/core/manticore.py
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ def to_class(self):
default=MProcessingType.multiprocessing,
description="single: No multiprocessing at all. Single process.\n threading: use threads\m multiprocessing: use forked processes",
)
consts.add("seed", default=1337, description="The seed to use when randomly selecting states")


class ManticoreBase(Eventful):
Expand Down Expand Up @@ -112,6 +113,7 @@ def at_not_running(func):
@functools.wraps(func)
def newFunction(self, *args, **kw):
if self.is_running():
print("Calling at running not allowed")
raise Exception(f"{func.__name__} only allowed while NOT exploring states")
return func(self, *args, **kw)

Expand Down Expand Up @@ -350,12 +352,8 @@ def setstate(x, y):
setstate(new_state, new_value)

# enqueue new_state, assign new state id
new_state_id = self._save(new_state, state_id=None)
with self._lock:
self._ready_states.append(new_state_id)
self._lock.notify_all() # Must notify one!
new_state_id = self._put_state(new_state)

self._publish("did_fork_state", new_state, expression, new_value, policy)
# maintain a list of children for logging purpose
children.append(new_state_id)

Expand All @@ -365,6 +363,8 @@ def setstate(x, y):
state._id = None
self._lock.notify_all()

self._publish("did_fork_state", new_state, expression, new_value, policy)

logger.debug("Forking current state %r into states %r", state.id, children)

@staticmethod
Expand All @@ -377,6 +377,7 @@ def verbosity(level):
set_verbosity(level)

# State storage
@Eventful.will_did("save_state")
def _save(self, state, state_id=None):
""" Store or update a state in secondary storage under state_id.
Use a fresh id is None is provided.
Expand All @@ -389,26 +390,25 @@ def _save(self, state, state_id=None):
state._id = self._workspace.save_state(state, state_id=state_id)
return state.id

@Eventful.will_did("load_state")
def _load(self, state_id):
""" Load the state from the secondary storage

:param state_id: a estate id
:type state_id: int
:returns: the state id used
"""

if not hasattr(self, "stcache"):
self.stcache = weakref.WeakValueDictionary()
if state_id in self.stcache:
return self.stcache[state_id]
self._publish("will_load_state", state_id)
state = self._workspace.load_state(state_id, delete=False)
state._id = state_id
self.forward_events_from(state, True)
self._publish("did_load_state", state, state_id)
self.stcache[state_id] = state
return state

@Eventful.will_did("remove_state")
def _remove(self, state_id):
""" Remove a state from secondary storage

Expand Down
3 changes: 3 additions & 0 deletions manticore/ethereum/account.py
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ def __int__(self):
def __str__(self):
return str(self._address)

def __hash__(self):
return self._address


class EVMContract(EVMAccount):
"""
Expand Down
126 changes: 126 additions & 0 deletions manticore/native/plugins.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,126 @@
from ..core.plugin import Plugin
from .state_merging import merge_constraints, is_merge_possible, merge


class Merger(Plugin):
def on_register(self):
p = self.manticore._publish
self.manticore._publish = lambda *args, **kwargs: None
for state in self.manticore.ready_states:
self.did_fork_state_callback(state, None, None, None)

self.manticore._publish = p

def load_state(self, state_id, delete=False):
"""
Loads a state in Manticore with state-id = `state_id` by using the corresponding API in Executor
:param state_id: state-id for state that is being loaded
:param delete: If set to True, deletes the state with state-id = `state_id`
:return: None
"""
state = self.manticore._workspace.load_state(state_id, delete=delete)
return state

def delete_state(self, state_id):
"""
Deletes a state in Manticore with state-id = `state_id` by using the corresponding API in Executor
:param state_id: state-id for state that is being deleted
:return: None
"""
with self.manticore._lock:
self.manticore._ready_states.remove(state_id)
self.manticore._remove(state_id)

def replace_state(self, state_id, state):
"""
Replaces a state in Manticore with state-id = `state_id` by using the corresponding API in Executor
:param state_id: state-id for state that is being replaced
:param state: State object that is replacing the existing state with `state_id`
:return: None
"""
return self.manticore._save(state, state_id=state_id)

def did_fork_state_callback(self, state, expression, new_value, policy):
state_id = state.id
"""That means no one else has to offer one Message Input

Maintains a `cpu_stateid_dict` in context that keeps maps program counter values to a list of state-id values
for states that will execute the instruction that that program counter as the next instruction
:param state_id: id for state that was just enqueued
:param state: State object that was just enqueued
:return: None
"""
# when a new state is addded to the list we save it so we do not have
# to repload all states when try to merges last PC
with self.locked_context("cpu_stateid_dict", dict) as cpu_stateid_dict:
# as we may be running in a different process we need to access this
# on a lock and over shared memory like this
state_id_list = cpu_stateid_dict.get(state.cpu.PC, list())
state_id_list.append(state_id)
cpu_stateid_dict[state.cpu.PC] = state_id_list

def will_load_state_callback(self, current_state_id):
"""
Checks if the state to be loaded (referenced by `current_state_id` can be merged with another currently enqueued
state and replaced by the merged state
:param current_state_id: state about to be loaded
:return: None
"""
# When a state is loaded for exploration lets check if we can find it a
# mate for merging
with self.locked_context("cpu_stateid_dict", dict) as cpu_stateid_dict:
# we get the lock and get a copy of the shared context
merged_state = self.load_state(current_state_id)
states_at_pc = cpu_stateid_dict.get(merged_state.cpu.PC, [])

# lets remove ourself from the list of waiting states
# assert current_state_id in states_at_pc #???
if current_state_id in states_at_pc:
states_at_pc.remove(current_state_id)

# Iterate over all remaining states that are waiting for exploration
# at the same PC
merged_ids = []
for new_state_id in states_at_pc:
new_state = self.load_state(new_state_id)
(exp_merged_state, exp_new_state, merged_constraint) = merge_constraints(
merged_state.constraints, new_state.constraints
)
is_mergeable, reason = is_merge_possible(merged_state, new_state, merged_constraint)

if is_mergeable:
# Ok we'll merge it!
merged_state = merge(
merged_state, new_state, exp_merged_state, merged_constraint
)

# lets remove the vestigial links to the old state
self.delete_state(new_state_id)

merged_ids.append(new_state_id)
is_mergeable = "succeeded"
else:
is_mergeable = "failed because of " + reason
debug_string = (
"at PC = "
+ hex(merged_state.cpu.PC)
+ ", merge "
+ is_mergeable
+ " for state id = "
+ str(current_state_id)
+ " and "
+ str(new_state_id)
)
print(debug_string)

for i in merged_ids:
states_at_pc.remove(i)

cpu_stateid_dict[merged_state.cpu.PC] = states_at_pc

# Ok so we have merged current_state_id with {merged_ids}
# And removed all merged_ids from everywhere

# UGLY we are replacing a state_id. This may be breaking caches in
# the future
self.replace_state(current_state_id, merged_state)
Loading