Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.
Sign up[WIP] Opportunistic state merging for Manticore #1351
Conversation
This commit introduces a new attribute -- cpu_stateid_dict -- in Executor that keeps track of the Program Counter register of each state and maps PC values to a list of state ids. States that are at the same PC are checked for mergeability. ** Warning: The is_merge_possible and merge methods in state_merging.py have not been implemented. However, this commit should not affect current exploration of Manticore
…example to test state merging 1. Building the constraint that can be used to check if the solver thinks that the buffers in input and output sockets are equal when comparing states for merging 2. Puttng the state merging example in that runs into 3 opportunities for state merging when the Random policy is seeded with the seed = 2 (not sure how to set it up from the Python script)
… it to 2 in Random policy object
**caution: I am in the process of finishing the memory maps comparison
This comment has been minimized.
This comment has been minimized.
|
If you're okay including |
This comment has been minimized.
This comment has been minimized.
|
Yes, I didn't realize most of this check is already implemented in |
This comment has been minimized.
This comment has been minimized.
|
|
This comment has been minimized.
This comment has been minimized.
|
I didn't realize that. Thanks for letting me know. I've dropped the |
This comment has been minimized.
This comment has been minimized.
|
Or just |
This comment has been minimized.
This comment has been minimized.
|
This also only checks the first |
This comment has been minimized.
This comment has been minimized.
|
Thanks for catching this. I was planning on adding the check for the two buffer lengths to be equal but I forgot about it when looking at other parts of the |
…hing comparison of memory in the two states
…y implementing the `merge` method that merges the CPU canonical registers between states
The merged constraint is simply a logical OR of the constraints in the states being merged.
* load/save/replace as needed by state merging * WIP Move merging to a plugin
…ample is now using the Merge plugin 1. Using Merge plugin and the newly added APIs in Executor to load, delete, replace states 2. Completing the memory objects comparison by comparing both memory object's symbolic writes instead of only comparing the first memory object against the second 3. Adding documentation for all of the newly introduced methods in state_merging.py
…basic_statemerging.py to work + moving Merger Plugin to plugin.py These changes now allow state merging to correctly merge two states in basic_statemerging.c
…my hack to avoid importing SMemory into state_merging.py
… example I've been using to test state merging
| 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) |
|
|
||
| @sync | ||
| def _replace_state(self, state_id, state): | ||
| # self._workspace.rm_state(state_id) |
disconnect3d
Jan 25, 2019
Member
Delete comment?
Delete comment?
|
Closing this as it's now being tracked in #1482 |
This PR is a work-in-progress as of now. The central idea is to merge states that happen to be at the same program location. This requires us to implement a
is_merge_possiblepredicate that compares two states and amergemethod that creates a mergedStatefrom two mergeableStateobjects.I am still working on finishing the implementation of
is_merge_possibleby adding checks for the array of byte values in variousMapobjects that describe the state's memory. The next step is to implement themergemethod by merging just the CPU and copy everything else from one of the two states.So far, the changes affect the main loop in
Executor. But, I am waiting for 3 APIs to be implemented that will allow me to move my code out ofExecutorand into a separate state-merging plugin. The design of the APIs is as follows:load_stateloads a state given astate_idwithout deleting it.delete_statedeletes a state given astate_idreplace_statereplaces the state with a valuestate_idin its workspace with another state given in its argumentAll three APIs return an error if the state with
state_iddoes not exist inExecutor's workspace. @feliam is currently working on implementing these APIs.With these APIs implemented, I plan to create a state-merging plugin that adds a callback for
will_load_state. The callback would merge the state that is about to be executed with other states if any happen to be at the same program location. To figure out which states are at the same program location without loading all the states into memory, the plugin would add a handler fordid_enqueue_stateand maintain a global dictionary that mapsstate_idvalues to that state's program counter.This change is