Introduce a configuration system (#1139)

This PR introduces a config/globals management system that addresses a few concerns about manticore:

1. The lack of a method to update certain configuration constants from Manticore's environment (such as solver timeout).
2. The ability to maintain a configuration file with a set of persistent flags and settings to simplify manticore invocation. (i.e. always enable all EVM detectors)
3. Make a central global place for configuration constants.

## Implementation

This PR adds the `manticore.utils.config` module. It implements a way to create and set configuration groups. Manticore's `main` tries loading all groups/values from yaml files in `$PWD` (file can be `.manticore.yml`, `manticore.yml`, `.mcore.yml`, or `mcore.yml`). A `manticore.yml` is also now produced in workspace directory upon a run's completion.

Variable values take the following precedence, lowest to highest:

1. The default value declared in the top of a module.
2. The configuration file read
3. The CLI if the variable is also a command line argument. (All command line arguments can be set in the yml under the key `cli`)

New flag, `--config` has been added to specify a config file if it's not one of the files that are automatically discovered. `--config-print` dumps all declared constants that can be set.

Declaring a configuration group is pretty straightforward. The following is a snippet from the top of `solver.py`:
```
consts = config.get_group('smt')
consts.add('timeout', default=240, description='Timeout, in seconds, for each Z3 invocation')
consts.add('memory', default=16384, description='Max memory for Z3 to use (in Megabytes)')
consts.add('maxsolutions', default=10000, description='Maximum solutions to provide when solving for all values')
```

Then using it later is as simple as referring to `consts.memory` or `consts.timeout`.

Fixes #372 	

<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/trailofbits/manticore/1139)
<!-- Reviewable:end -->

manticore/__main__.py

@@ -4,13 +4,15 @@
 import argparse
 
 from . import Manticore
-from .utils import log
+from .utils import log, config
 
 # XXX(yan): This would normally be __name__, but then logger output will be pre-
 # pended by 'm.__main__: ', which is not very pleasing. hard-coding to 'main'
 logger = logging.getLogger('manticore.main')
 
-sys.setrecursionlimit(10000)
+consts = config.get_group('main')
+consts.add('recursionlimit', default=10000,
+           description="Value to set for Python recursion limit")
 
 
 def parse_arguments():
@@ -20,26 +22,12 @@ def positive(value):
             raise argparse.ArgumentTypeError("Argument must be positive")
         return ivalue
 
-    parser = argparse.ArgumentParser(description='Symbolic execution tool')
-    parser.add_argument('--assertions', type=str, default=None,
-                        help=argparse.SUPPRESS)
-    parser.add_argument('--buffer', type=str,
-                        help=argparse.SUPPRESS)
+    parser = argparse.ArgumentParser(description='Symbolic execution tool', prog='manticore',
+                                     formatter_class=argparse.ArgumentDefaultsHelpFormatter)
     parser.add_argument('--context', type=str, default=None,
                         help=argparse.SUPPRESS)
     parser.add_argument('--coverage', type=str, default=None,
                         help='Where to write the coverage data')
-    parser.add_argument('--data', type=str, default='',
-                        help='Initial concrete concrete_data for the input symbolic buffer')
-    parser.add_argument('--env', type=str, nargs=1, default=[], action='append',
-                        help='Add an environment variable. Use "+" for symbolic bytes. (VARNAME=++++)')
-    #TODO allow entry as an address
-    #parser.add_argument('--entry', type=str, default=None,
-    #                    help='address as entry point')
-    parser.add_argument('--entrysymbol', type=str, default=None,
-                        help='Symbol as entry point')
-    parser.add_argument('--file', type=str, default=[], action='append', dest='files',
-                        help='Specify symbolic input file, \'+\' marks symbolic bytes')
     parser.add_argument('--names', type=str, default=None,
                         help=argparse.SUPPRESS)
     parser.add_argument('--no-colors', action='store_true',
@@ -55,7 +43,7 @@ def positive(value):
                         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='+',
+    parser.add_argument('argv', type=str, nargs='*', default=[],
                         help="Path to program, and arguments ('+' in arguments indicates symbolic byte).")
     parser.add_argument('--timeout', type=int, default=0,
                         help='Timeout. Abort exploration after TIMEOUT seconds')
@@ -66,73 +54,99 @@ def positive(value):
                               "(default mcore_?????)"))
     parser.add_argument('--version', action='version', version='Manticore 0.2.1.1',
                         help='Show program version information')
-    parser.add_argument('--txlimit', type=positive,
-                        help='Maximum number of symbolic transactions to run (positive integer) (Ethereum only)')
+    parser.add_argument('--config', type=str,
+                        help='Manticore config file (.yml) to use. (default config file pattern is: ./[.]m[anti]core.yml)')
+
+    bin_flags = parser.add_argument_group('Binary flags')
+    bin_flags.add_argument('--entrysymbol', type=str, default=None,
+                           help='Symbol as entry point')
+    bin_flags.add_argument('--assertions', type=str, default=None,
+                           help=argparse.SUPPRESS)
+    bin_flags.add_argument('--buffer', type=str,
+                           help=argparse.SUPPRESS)
+    bin_flags.add_argument('--data', type=str, default='',
+                           help='Initial concrete concrete_data for the input symbolic buffer')
+    bin_flags.add_argument('--file', type=str, default=[], action='append', dest='files',
+                           help='Specify symbolic input file, \'+\' marks symbolic bytes')
+    bin_flags.add_argument('--env', type=str, nargs=1, default=[], action='append',
+                           help='Add an environment variable. Use "+" for symbolic bytes. (VARNAME=++++)')
+
+    eth_flags = parser.add_argument_group('Ethereum flags')
+    eth_flags.add_argument('--verbose-trace', action='store_true',
+                           help='Dump an extra verbose trace for each state')
+    eth_flags.add_argument('--txlimit', type=positive,
+                           help='Maximum number of symbolic transactions to run (positive integer)')
 
-    parser.add_argument('--txnocoverage', action='store_true',
-                        help='Do not use coverage as stopping criteria (Ethereum only)')
+    eth_flags.add_argument('--txnocoverage', action='store_true',
+                           help='Do not use coverage as stopping criteria')
 
-    parser.add_argument('--txnoether', action='store_true',
-                        help='Do not attempt to send ether to contract (Ethereum only)')
+    eth_flags.add_argument('--txnoether', action='store_true',
+                           help='Do not attempt to send ether to contract')
 
-    parser.add_argument('--txaccount', type=str, default="attacker",
-                        help='Account used as caller in the symbolic transactions, either "attacker" or "owner" (Ethereum only)')
+    eth_flags.add_argument('--txaccount', type=str, default="attacker",
+                           help='Account used as caller in the symbolic transactions, either "attacker" or "owner"')
 
-    parser.add_argument('--contract', type=str,
-                        help='Contract name to analyze in case of multiple contracts (Ethereum only)')
+    eth_flags.add_argument('--contract', type=str,
+                           help='Contract name to analyze in case of multiple contracts')
 
-    parser.add_argument('--detect-overflow', action='store_true',
-                        help='Enable integer overflow detection (Ethereum only)')
+    eth_flags.add_argument('--detect-overflow', action='store_true',
+                           help='Enable integer overflow detection')
 
-    parser.add_argument('--detect-invalid', action='store_true',
-                        help='Enable INVALID instruction detection (Ethereum only)')
+    eth_flags.add_argument('--detect-invalid', action='store_true',
+                           help='Enable INVALID instruction detection')
 
-    parser.add_argument('--detect-uninitialized-memory', action='store_true',
-                        help='Enable detection of uninitialized memory usage (Ethereum only)')
+    eth_flags.add_argument('--detect-uninitialized-memory', action='store_true',
+                           help='Enable detection of uninitialized memory usage')
 
-    parser.add_argument('--detect-uninitialized-storage', action='store_true',
-                        help='Enable detection of uninitialized storage usage (Ethereum only)')
+    eth_flags.add_argument('--detect-uninitialized-storage', action='store_true',
+                           help='Enable detection of uninitialized storage usage')
 
-    parser.add_argument('--detect-reentrancy', action='store_true',
-                        help='Enable detection of reentrancy bug (Ethereum only)')
+    eth_flags.add_argument('--detect-reentrancy', action='store_true',
+                           help='Enable detection of reentrancy bug')
 
-    parser.add_argument('--detect-reentrancy-advanced', action='store_true',
-                        help='Enable detection of reentrancy bug -- this detector is better used via API (Ethereum only)')
+    eth_flags.add_argument('--detect-reentrancy-advanced', action='store_true',
+                           help='Enable detection of reentrancy bug -- this detector is better used via API')
 
-    parser.add_argument('--detect-unused-retval', action='store_true',
-                        help='Enable detection of unused internal transaction return value (Ethereum only)')
+    eth_flags.add_argument('--detect-unused-retval', action='store_true',
+                           help='Enable detection of unused internal transaction return value')
 
-    parser.add_argument('--detect-delegatecall', action='store_true',
-                        help='Enable detection of problematic uses of DELEGATECALL instruction (Ethereum only)')
+    eth_flags.add_argument('--detect-delegatecall', action='store_true',
+                           help='Enable detection of problematic uses of DELEGATECALL instruction')
 
-    parser.add_argument('--detect-selfdestruct', action='store_true',
-                        help='Enable detection of reachable selfdestruct instructions')
+    eth_flags.add_argument('--detect-selfdestruct', action='store_true',
+                           help='Enable detection of reachable selfdestruct instructions')
 
-    parser.add_argument('--detect-externalcall', action='store_true',
-                        help='Enable detection of reachable external call or ether leak to sender or arbitrary address')
+    eth_flags.add_argument('--detect-externalcall', action='store_true',
+                           help='Enable detection of reachable external call or ether leak to sender or arbitrary address')
 
-    parser.add_argument('--detect-env-instr', action='store_true',
-                        help='Enable detection of use of potentially unsafe/manipulable instructions')
+    eth_flags.add_argument('--detect-env-instr', action='store_true',
+                           help='Enable detection of use of potentially unsafe/manipulable instructions')
 
-    parser.add_argument('--detect-all', action='store_true',
-                        help='Enable all detector heuristics (Ethereum only)')
+    eth_flags.add_argument('--detect-all', action='store_true',
+                           help='Enable all detector heuristics')
 
-    parser.add_argument('--avoid-constant', action='store_true',
-                        help='Avoid exploring constant functions for human transactions (Ethereum only)')
+    eth_flags.add_argument('--avoid-constant', action='store_true',
+                           help='Avoid exploring constant functions for human transactions')
 
-    parser.add_argument('--limit-loops', action='store_true',
-                        help='Avoid exploring constant functions for human transactions (Ethereum only)')
+    eth_flags.add_argument('--limit-loops', action='store_true',
+                           help='Avoid exploring constant functions for human transactions')
 
-    parser.add_argument('--no-testcases', action='store_true',
-                        help='Do not generate testcases for discovered states when analysis finishes (Ethereum only)')
+    eth_flags.add_argument('--no-testcases', action='store_true',
+                           help='Do not generate testcases for discovered states when analysis finishes')
 
-    parser.add_argument('--verbose-trace', action='store_true',
-                        help='Dump an extra verbose trace for each state (Ethereum only)')
+    config_flags = parser.add_argument_group('Constants')
+    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:
+        print(parser.format_usage() + "error: the following arguments are required: argv")
+        sys.exit(1)
+
     if parsed.policy.startswith('min'):
         parsed.policy = '-' + parsed.policy[3:]
     elif parsed.policy.startswith('max'):
@@ -199,6 +213,8 @@ def main():
     if args.no_colors:
         log.disable_colors()
 
+    sys.setrecursionlimit(consts.recursionlimit)
+
     Manticore.verbosity(args.v)
 
     # TODO(mark): Temporarily hack ethereum support into manticore cli

manticore/core/executor.py

@@ -7,6 +7,7 @@
 from ..exceptions import ExecutorError, SolverException
 from ..utils.nointerrupt import WithKeyboardInterruptAs
 from ..utils.event import Eventful
+from ..utils import config
 from .smtlib import Z3Solver, Expression
 from .state import Concretize, TerminateState
 
@@ -16,10 +17,14 @@
 
 # This is the single global manager that will handle all shared memory among workers
 
+consts = config.get_group('executor')
+consts.add('seed', default=1337, description='The seed to use when randomly selecting states')
+
 
 def mgr_init():
     signal.signal(signal.SIGINT, signal.SIG_IGN)
 
+
 logger = logging.getLogger(__name__)
 
 
@@ -78,7 +83,7 @@ def choice(self, state_ids):
 class Random(Policy):
     def __init__(self, executor, *args, **kwargs):
         super().__init__(executor, *args, **kwargs)
-        random.seed(1337)  # For repeatable results
+        random.seed(consts.seed)  # For repeatable results
 
     def choice(self, state_ids):
         return random.choice(state_ids)

manticore/core/smtlib/solver.py

@@ -27,11 +27,17 @@
 import time
 from .visitors import *
 from ...utils.helpers import issymbolic, istainted, taint_with, get_taints
+from ...utils import config
 import io
 import collections
 
 logger = logging.getLogger(__name__)
 
+consts = config.get_group('smt')
+consts.add('timeout', default=240, description='Timeout, in seconds, for each Z3 invocation')
+consts.add('memory', default=16384, description='Max memory for Z3 to use (in Megabytes)')
+consts.add('maxsolutions', default=10000, description='Maximum solutions to provide when solving for all values')
+consts.add('z3_bin', default='z3', description='Z3 binary to use')
 
 class Solver(object, metaclass=ABCMeta):
     @abstractmethod
@@ -114,7 +120,7 @@ def __init__(self):
         super().__init__()
         self._proc = None
 
-        self._command = 'z3 -t:240000 -memory:16384 -smt2 -in'
+        self._command = f'{consts.z3_bin} -t:{consts.timeout*1000} -memory:{consts.memory} -smt2 -in'
         self._init = ['(set-logic QF_AUFBV)', '(set-option :global-decls false)']
         self._get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ #x(?P<value>([0-9a-fA-F]*))\)\)'), 16)
 
@@ -344,13 +350,16 @@ def can_be_true(self, constraints, expression):
 
     # get-all-values min max minmax
     #@memoized
-    def get_all_values(self, constraints, expression, maxcnt=30000, silent=False):
+    def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
         ''' Returns a list with all the possible values for the symbol x'''
         if not isinstance(expression, Expression):
             return [expression]
         assert isinstance(constraints, ConstraintSet)
         assert isinstance(expression, Expression)
 
+        if maxcnt is None:
+            maxcnt = consts.maxsolutions
+
         with constraints as temp_cs:
             if isinstance(expression, Bool):
                 var = temp_cs.new_bool()

manticore/core/workspace.py

@@ -9,12 +9,17 @@
 from contextlib import contextmanager
 from multiprocessing.managers import SyncManager
 
+from manticore.utils import config
 from manticore.utils.helpers import PickleSerializer
 from .smtlib import solver
 from .state import State
 
 logger = logging.getLogger(__name__)
 
+consts = config.get_group('workspace')
+consts.add('prefix', default='mcore_', description="The prefix to use for output and workspace directories")
+consts.add('dir', default='.', description="Location of where to create workspace directories")
+
 _manager = None
 
 
@@ -168,7 +173,7 @@ def __init__(self, uri=None):
         :param uri: The path to on-disk workspace, or None.
         """
         if not uri:
-            uri = os.path.abspath(tempfile.mkdtemp(prefix="mcore_", dir='./'))
+            uri = os.path.abspath(tempfile.mkdtemp(prefix=consts.prefix, dir=consts.dir))
 
         if os.path.exists(uri):
             assert os.path.isdir(uri), 'Store must be a directory'

manticore/ethereum.py

@@ -16,6 +16,7 @@
 from .platforms import evm
 from .core.state import State
 from .utils.helpers import istainted, issymbolic, PickleSerializer
+from .utils import config
 import tempfile
 from subprocess import Popen, PIPE, check_output
 from multiprocessing import Process, Queue
@@ -2757,6 +2758,9 @@ def worker_finalize(q):
                         global_findings.write('    '.join(source_code_snippet.splitlines(True)))
                         global_findings.write('\n')
 
+        with self._output.save_stream('manticore.yml') as f:
+            config.save(f)
+
         with self._output.save_stream('global.summary') as global_summary:
             # (accounts created by contract code are not in this list )
             global_summary.write("Global runtime coverage:\n")

manticore/ethereum/__init__.py

@@ -11,6 +11,7 @@
 from ..platforms import evm
 from ..core.state import State, TerminateState
 from ..utils.helpers import issymbolic, PickleSerializer
+from ..utils import config
 from ..utils.log import init_logging
 import tempfile
 from subprocess import Popen, PIPE, check_output
@@ -1439,6 +1440,9 @@ def worker_finalize(q):
                         global_findings.write('    '.join(source_code_snippet.splitlines(True)))
                         global_findings.write('\n')
 
+        with self._output.save_stream('manticore.yml') as f:
+            config.save(f)
+
         with self._output.save_stream('global.summary') as global_summary:
             # (accounts created by contract code are not in this list )
             global_summary.write("Global runtime coverage:\n")

manticore/manticore.py

@@ -23,6 +23,7 @@
 from .core.smtlib import solver, ConstraintSet
 from .core.workspace import ManticoreOutput
 from .platforms import linux, evm, decree
+from .utils import config
 from .utils.helpers import issymbolic
 from .utils.nointerrupt import WithKeyboardInterruptAs
 from .utils.event import Eventful
@@ -678,6 +679,9 @@ def _did_finish_run_callback(self):
         with self._output.save_stream('command.sh') as f:
             f.write(' '.join(sys.argv))
 
+        with self._output.save_stream('manticore.yml') as f:
+            config.save(f)
+
         elapsed = time.time() - self._time_started
         logger.info('Results in %s', self._output.store.uri)
         logger.info('Total time: %s', elapsed)