ManticoreBase refactor (#1385)

* [WIP][WIP][WIP] Moving executor functionality to ManticoreBase and refactor concurrency shared data

* Workspace locks

* Concurrency flavor configurable from commandline

* Asserts and refactorrrrrrrs

* Remove unused callback

* Some CC

* Some CC

* Some CC

* Fix solver vs Z3Solver

* Make solver a singleton based on tid/pid. REfactor m._save. Fix some tests

* typo and evm bugfix

* Fix some tests referecing global solver

* Fix concolic tests and more global solver refs

* Fix tests

* CC fixes

* Fix tests. Fix testcase id generation

* Move profiling to a plugin and fix tests

* Add solver intance ref to mem test

* Fix mem workspace tests

* Fix output checking tests

* Fix z3solver ref

* Relax verbosity/log tests

* Moved Workers to its own file

* Relax output tests

* Relax output tests

* Fix profiling test

* merge

* Fix more tests

* Default multiprocessing

* Try to clean mcore __del__

* Change Worker life span

* Fix Single mode

* CC

* Merge branch 'master' into dev-executor-refactor

* revert verbosity travis

* CC and solver ref fix

* Relax ouput checking tests and some bugfixes

* running -> ready

* Fixing teeests

* add weak cache to _load

* del debug prints

* Adding config.py support for Enums

* Try/Remove generate_testcase event as it never occurs online. Fix tests

* Fix CC

* Kill the cache when start/stop run. Remove debugprints. clean tests

* Fix travis test _other_

* Fix native tests and timeout

* Fix state.must_be_true

* fix CC

* Merge and fix more tests

* Changing fstat tets...:
~'

* LLLLLLLLinux tests

* Skip unicorn concrete test for now

* Try fix CodeClimate

* Try fix CodeClimate

* Update evm examples to newest solidity

* Complete transformation of consts.mprocessing to enum

* Add blank line (codeclimate)

* Using the enum instead of the string

* Merge branch 'dev-executor-refactor' of github.com:trailofbits/manticore into dev-executor-refactor

* Using the enum instead of the string

* Merge branch 'master' into dev-executor-refactor

* Fix solver instance reference

.codeclimate.yml

@@ -19,7 +19,7 @@ checks:
   method-count:
     enabled: false
     config:
-      threshold: 35
+      threshold: 45
   method-lines:
     enabled: true
     config:

examples/evm/coverage.sol

@@ -2,7 +2,6 @@
 `explore` is the first level of exploration; you have to call it multiple times to explore the path
 `explore2` is a bit more complex; the owner has to call first the `enable_exploration` function
 */
-pragma solidity ^0.4.15;
 
 contract Coverage{
     address private owner;
@@ -74,7 +73,7 @@ contract Coverage{
         if(give){
             remove(msg.sender, value);
             add(user, value);
-            Give(msg.sender, user, value);
+            emit Give(msg.sender, user, value);
         }
         else{
             if( balances[user] > balances[msg.sender]){
@@ -84,7 +83,7 @@ contract Coverage{
                 value = diff >value ? value : diff;
                 add(msg.sender, value);
                 remove(user, value);
-                Take(msg.sender, user, value);
+                emit Take(msg.sender, user, value);
             }
             else{
                 // If you try to take to someone poorer than you
@@ -104,7 +103,7 @@ contract Coverage{
         if(give){
             remove(msg.sender, value);
             add(user, value);
-            Give(msg.sender, user, value);
+            emit Give(msg.sender, user, value);
         }
         else{
             uint diff;
@@ -113,7 +112,7 @@ contract Coverage{
             value = diff >value ? value : diff;
             add(msg.sender, value);
             remove(user, value);
-            Take(msg.sender, user, value);
+            emit Take(msg.sender, user, value);
         }
     }
 }

examples/evm/simple_int_overflow.sol

@@ -1,4 +1,3 @@
-pragma solidity ^0.4.15;
 contract Overflow {
     uint private sellerBalance=0;
 

examples/evm/simple_multi_func.sol

@@ -1,5 +1,3 @@
-pragma solidity ^0.4.13;
-
 contract Test {
     event Log(string);
     mapping(address => uint) private balances;

examples/evm/simple_value_check.sol

@@ -1,13 +1,12 @@
-pragma solidity ^0.4.13;
 
 contract Test {
     event Log(string);
 
     function target() payable public {
         if (msg.value > 10)
-            Log("Value greater than 10");
+            emit Log("Value greater than 10");
         else
-            Log("Value less or equal than 10");
+            emit Log("Value less or equal than 10");
 
     } 
 

examples/evm/two_tx_ovf.sol

@@ -1,5 +1,3 @@
-pragma solidity ^0.4.15;
-
 contract SymExExample {
     uint did_init = 0;
 
@@ -9,18 +7,18 @@ contract SymExExample {
     function test_me(int input) {
         if (did_init == 0) {
             did_init = 1;
-            Log("initialized");
+            emit Log("initialized");
             return;
         }
 
         if (input < 42) {
             // safe
-            Log("safe");
+            emit Log("safe");
             return;
         } else {
             // overflow possibly!
             int could_overflow = input + 1;
-            Log("overflow");
+            emit Log("overflow");
         }
 
     }

examples/evm/umd_example.sol

@@ -2,8 +2,6 @@
 // by Michael Hicks, University of Maryland.
 // https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf
 
-pragma solidity ^0.4.15;
-
 contract SymExExample {
 
 

examples/script/concolic.py

@@ -20,7 +20,8 @@
 from manticore.native import Manticore
 from manticore.core.plugin import ExtendedTracer, Follower, Plugin
 from manticore.core.smtlib.constraints import ConstraintSet
-from manticore.core.smtlib import solver
+from manticore.core.smtlib.solver import Z3Solver
+from manticore.utils import config
 
 import copy
 from manticore.core.smtlib.expression import *
@@ -45,7 +46,7 @@ def __init__(self, tracer):
     def trace(self):
         return self._trace
 
-    def will_generate_testcase_callback(self, state, testcase, msg):
+    def will_terminate_state_callback(self, state, reason):
         self._trace = state.context.get(self._tracer.context_key, [])
 
         instructions, writes = _partition(lambda x: x['type'] == 'regs', self._trace)
@@ -139,33 +140,39 @@ def make_chr(c):
     ret = ''
     for data in datas:
         for c in data:
-            ret += make_chr(solver.get_value(newset, c))
+            ret += make_chr(Z3Solver.instance().get_value(newset, c))
     return ret
 
 # Run a concrete run with |inp| as stdin
 def concrete_run_get_trace(inp):
+
+    consts = config.get_group('core')
+    consts.mprocessing = consts.mprocessing.single
+
     m1 = Manticore.linux(prog, concrete_start=inp, workspace_url='mem:')
     t = ExtendedTracer()
-    r = TraceReceiver(t)
+    #r = TraceReceiver(t)
     m1.verbosity(VERBOSITY)
     m1.register_plugin(t)
-    m1.register_plugin(r)
-    m1.run(procs=1)
-    return r.trace
+    #m1.register_plugin(r)
+    m1.run()
+    for st in m1.all_states:
+        return t.get_trace(st) 
+    #return r.trace
 
 
 def symbolic_run_get_cons(trace):
     '''
     Execute a symbolic run that follows a concrete run; return constraints generated
     and the stdin data produced
     '''
-
+    # mem: has no concurrency support. Manticore should be 'Single' process
     m2 = Manticore.linux(prog, workspace_url='mem:')
     f = Follower(trace)
     m2.verbosity(VERBOSITY)
     m2.register_plugin(f)
 
-    def on_term_testcase(mcore, state, stateid, err):
+    def on_term_testcase(mm, state, err):
         with m2.locked_context() as ctx:
             readdata = []
             for name, fd, data in state.platform.syscall_trace:
@@ -193,7 +200,7 @@ def getnew(oldcons, newcons):
 
 def constraints_are_sat(cons):
     'Whether constraints are sat'
-    return solver.check(constraints_to_constraintset(cons))
+    return Z3Solver.instance().check(constraints_to_constraintset(cons))
 
 def get_new_constrs_for_queue(oldcons, newcons):
     ret = []

examples/script/count_instructions.py

@@ -25,6 +25,6 @@ def explore(state):
         with m.locked_context() as context:
             context['count'] += 1
 
-    m.run(procs=1)
+    m.run()
 
     print(f"Executed {m.context['count']} instructions.")

manticore/__init__.py

@@ -5,6 +5,7 @@
     sys.exit(-1)
 
 from .utils import config, log
+from .utils.log import set_verbosity
 from .utils.helpers import issymbolic, istainted
-
-__all__ = [issymbolic.__name__, istainted.__name__]
+from .ethereum.manticore import ManticoreEVM
+__all__ = [issymbolic.__name__, istainted.__name__, ManticoreEVM.__name__, set_verbosity.__name__]

manticore/__main__.py

@@ -7,7 +7,7 @@
 
 import pkg_resources
 
-from .core.manticore import ManticoreBase
+from .core.manticore import ManticoreBase, set_verbosity
 from .ethereum.cli import ethereum_main
 from .utils import config, log, install_helper
 
@@ -35,7 +35,7 @@ def main():
 
     sys.setrecursionlimit(consts.recursionlimit)
 
-    ManticoreBase.verbosity(args.v)
+    set_verbosity(args.v)
 
     if args.argv[0].endswith('.sol'):
         ethereum_main(args, logger)
@@ -68,10 +68,6 @@ def positive(value):
                         help=("Search policy. random|adhoc|uncovered|dicount"
                               "|icount|syscount|depth. (use + (max) or - (min)"
                               " to specify order. e.g. +random)"))
-    parser.add_argument('--profile', action='store_true',
-                        help='Enable profiling mode.')
-    parser.add_argument('--procs', type=int, default=1,
-                        help='Number of parallel processes to spawn')
     parser.add_argument('argv', type=str, nargs='*', default=[],
                         help="Path to program, and arguments ('+' in arguments indicates symbolic byte).")
     parser.add_argument('-v', action='count', default=1,
@@ -156,9 +152,6 @@ def positive(value):
     config.add_config_vars_to_argparse(config_flags)
 
     parsed = parser.parse_args(sys.argv[1:])
-    if parsed.procs <= 0:
-        parsed.procs = 1
-
     config.process_config_values(parser, parsed)
 
     if not parsed.argv: