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

ManticoreBase refactor #1385

Merged
merged 63 commits into from May 9, 2019

Conversation

2 participants
@feliam
Copy link
Contributor

commented Mar 7, 2019

  • Executor.py deleted
  • ManticoreBase now responsible for base functionality doh
  • Worker is the base class for a worker
  • 3 types of workers:
    * Single: runs in main. Perfect for profiling underlaying archs
    * Threads
    * Multiprocessing Processs
  • fs:Workspace lock does not depend on an external process multiprocessing manager.
  • state lists are well defined and at ManticoreBase level (All subclasses get the same kind of lists)
  • Added Enums as valid type for config.py

Lots of documentation added and refined.


                   Manticore symbolically explores program states.


        Manticore phases
        ****************

        Manticore has multiprocessing capabilities. Several worker processes
        could be registered to do concurrent exploration of the READY states.
        Manticore can be itself at different phases: STANDBY, RUNNING.

                      +---------+               +---------+
                ----->| STANDBY +<------------->+ RUNNING |
                      +---------+               +----+----+

        = Phase STANDBY =
        Manticore starts at STANDBY with a single initial state. Here the user
        can inspect, modify and generate testcases for the different states. The
        workers are paused and not doing any work. Actions: run()


        = Phase RUNNING =
        At RUNNING the workers consume states from the READY state list and
        potentially fork new states or terminate states. A RUNNING manticore can
        be stopped back to STANDBY. Actions: stop()


        States and state lists
        **********************

        A state contains all the information of the running program at a given
        moment. State snapshots are saved to the workspace often. Internally
        Manticore associates a fresh id with each saved state. The memory copy
        of the state is then changed by the emulation of the specific arch.
        Stored snapshots are periodically updated using: _save() and _load().

                      _save     +-------------+  _load
            State  +----------> |  WORKSPACE  +----------> State
                                +-------------+

        During exploration Manticore spawns a number of temporary states that are
        maintained in different lists:

                Initial
                State
                  |   +-+---{fork}-----+
                  |   | |              |
                  V   V V              |
                +---------+        +---+----+      +------------+
                |  READY  +------->|  BUSY  +----->| TERMINATED |
                +---------+        +---+----+      +------------+
                     |
                     |                             +--------+
                     +---------------------------->| KILLED |
                                                   +--------+

        At any given time a state must be at the READY, BUSY, TERMINATED or
        KILLED list.

        State list: READY
        =================
        The READY list holds all the runnable states. Internally a state is
        added to the READY list via method `_put_state(state)`. Workers take
        states from the READY list via the `_get_state(wait=True|False)` method.
        A worker mainloop will consume states from the READY list and mark them
        as BUSYwhile working on them. States in the READY list can go to BUSY or
        KILLED


        State list: BUSY
        =================
        When a state is selected for exploration from the READY list it is
        marked as busy and put in the BUSY list. States being explored will be
        constantly modified  and only saved back to storage when moved out of
        the BUSY list. Hence, when at BUSY the stored copy of the state will be
        potentially outdated. States in the BUSY list can go to TERMINATED,
        KILLED or they can be {forked} back to READY. The forking process
        could involve generating new child states and removing the parent
        from all the lists.


        State list: TERMINATED
        ======================
        TERMINATED contains states that have reached a final condition and raised
        TerminateState. Workers mainloop simpliy move the states that requested
        termination to the TERMINATED list. This is a final list.

        ```An inherited Manticore class like ManticoreEVM could internally revive
        the states in TERMINATED that pass some condition and move them back to
        READY so the user can apply a following transaction.```

        State list: KILLED
        ==================
        KILLED contains all the READY and BUSY states found at a cancel event.
        Manticore supports interactive analysis and has a prominetnt event system
        A useror ui can stop or cancel the exploration at any time. The unfinnished
        states cought at this situation are simply moved to its own list for
        further user action. This is a final list.


This change is Reviewable

feliam added some commits Mar 7, 2019

@feliam feliam changed the title [WIP][WIP][WIP] ManticoreBase refactor [WIP][WIP] ManticoreBase refactor Mar 18, 2019

feliam added some commits Mar 18, 2019

@feliam feliam changed the title [WIP][WIP] ManticoreBase refactor [WIP] ManticoreBase refactor Mar 20, 2019

@feliam feliam marked this pull request as ready for review Mar 26, 2019

feliam added some commits Apr 18, 2019

@feliam feliam changed the title [WIP] ManticoreBase refactor ManticoreBase refactor Apr 25, 2019

@feliam
Copy link
Contributor Author

left a comment

Reviewable status: 29 of 56 files reviewed, 10 unresolved discussions (waiting on @ehennenfent)


examples/evm/simple_value_check.sol, line 1 at r1 (raw file):

Previously, feliam (feliam) wrote…

No particular reason. I will upgrade all examples to the newest and greatest soliditi version

Done.

@ehennenfent
Copy link
Contributor

left a comment

Reviewed 1 of 49 files at r1, 2 of 6 files at r2, 25 of 25 files at r3.
Reviewable status: all files reviewed, 3 unresolved discussions (waiting on @feliam)


.codeclimate.yml, line 20 at r3 (raw file):

      threshold: 40
  method-count:
    enabled: true

I'm surprised this isn't a merge conflict. I was pretty sure I disabled the method-count metric since we've ignored all the ones on codeclimate so far.


manticore/core/manticore.py, line 78 at r1 (raw file):

Previously, feliam (feliam) wrote…

This may by used by an user specializing a ManticoreBase. (like ManticoreEVM, ManticoreLinux). The idea is to decorate functions that only make sense when at running/not_running so bugs can be caught early. Maybe it should be an assert in this case instead of an Exception

A more specific exception would be better, but it's not a huge problem


manticore/ethereum/plugins.py, line 123 at r1 (raw file):

Previously, feliam (feliam) wrote…

Yes. There is no more online(while running) testcase generation nor generate_testcase event. The idea is that, at the end/finalize manticore will loop over all registered plugins and let them potentially generate testcase files for each state.

Fine by me, but we should be sure to document this in the changelog and update our examples if necessary

@feliam
Copy link
Contributor Author

left a comment

Reviewable status: 53 of 56 files reviewed, 4 unresolved discussions (waiting on @ehennenfent and @feliam)


.codeclimate.yml, line 20 at r3 (raw file):

Previously, ehennenfent (Eric Hennenfent) wrote…

I'm surprised this isn't a merge conflict. I was pretty sure I disabled the method-count metric since we've ignored all the ones on codeclimate so far.

Should I set it to enabled: false ?


manticore/core/manticore.py, line 91 at r5 (raw file):

This may by used by an user specializing a ManticoreBase. (like ManticoreEVM, ManticoreLinux). The idea is to decorate functions that only make sense when at running/not_running so bugs can be caught early. Maybe it should be an assert in this case instead of an Exception

@ehennenfent
Copy link
Contributor

left a comment

Reviewed 1 of 1 files at r4, 2 of 2 files at r5.
Reviewable status: all files reviewed, 3 unresolved discussions (waiting on @feliam)


.codeclimate.yml, line 20 at r3 (raw file):

Previously, feliam (feliam) wrote…

Should I set it to enabled: false ?

I edited the enabled line, not the count line, so it makes sense that it's not a conflict. Don't worry about it; everything should get squared away once you merge.

@ehennenfent
Copy link
Contributor

left a comment

Reviewed 11 of 11 files at r6.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @feliam)


manticore/core/manticore.py, line 91 at r5 (raw file):

Previously, feliam (feliam) wrote…

This may by used by an user specializing a ManticoreBase. (like ManticoreEVM, ManticoreLinux). The idea is to decorate functions that only make sense when at running/not_running so bugs can be caught early. Maybe it should be an assert in this case instead of an Exception

This is fine with me but it seems like Reviewable wants me to reply to it for some reason.

@ehennenfent
Copy link
Contributor

left a comment

Reviewed 1 of 1 files at r7.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @feliam)

@feliam feliam merged commit a527e81 into master May 9, 2019

5 of 6 checks passed

code-review/reviewable 1 discussion left (feliam)
Details
Travis CI - Branch Build Passed
Details
Travis CI - Pull Request Build Passed
Details
codeclimate 1 fixed issue
Details
codeclimate/total-coverage 75% (0.2% change)
Details
license/cla Contributor License Agreement is signed.
Details

Manticore Releases automation moved this from In progress to Included in 0.2.6! May 9, 2019

@feliam feliam deleted the dev-executor-refactor branch May 10, 2019

ekilmer added a commit that referenced this pull request May 17, 2019

Merge branch 'master' into native-arb-cf-redirect-detector
* master: (28 commits)
  AArch64: fix ldrb size (#1433)
  System Call Audit (#1384)
  ManticoreBase refactor (#1385)
  Add missing checks for ARM boundaries (#1429)
  aarch64: add instruction tests: T-U (#1423)
  aarch64: add instruction tests: M-S (#1422)
  aarch64: add instruction tests: C-L (#1421)
  aarch64: add instruction tests: A-B (#1420)
  aarch64: add everything except instructions (#1418)
  fixup: support ARM64 in '_reg_name'
  Revert "fixup: remove x86-specific code from '_reg_name'"
  review: avoid wildcard imports
  review: rename the file
  fixup: remove x86-specific code from '_reg_name'
  fixup: do not use relative imports
  Generates a more sensible symbolic default for constructor arguments (#1414)
  aarch64: add instructions
  aarch64: add everything except instructions
  Switches the Travis-CI badge from .org to .com (#1416)
  Performance optimization : use set instead of list (#1415)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.