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

Fix config.py so it is reproducible #1636

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all 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
261 changes: 23 additions & 238 deletions manticore/__main__.py
Original file line number Diff line number Diff line change
@@ -1,267 +1,52 @@
"""
This is the Manticore's CLI `manticore` script.
"""
import argparse
import logging
import sys

import pkg_resources

from crytic_compile import is_supported, cryticparser
from .core.manticore import ManticoreBase, set_verbosity
from .ethereum.cli import ethereum_main
from .wasm.cli import wasm_main
from .utils import config, log, install_helper, resources

consts = config.get_group("main")
consts = config.get_group("cli")
consts.add("recursionlimit", default=10000, description="Value to set for Python recursion limit")
consts.add("no-colors", default=True, description="Disable ANSI color escape sequences in output")
consts.add("verbosity", default=1, description="Specify verbosity level [1-4]")


# 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")

if install_helper.has_native:
from manticore.native.cli import native_main

def is_eth():
for arg in sys.argv[1:]:
if not arg.startswith("-") and (arg.endswith(".sol") or is_supported(arg)):
return True
return False

def main() -> None:
"""
Dispatches execution into one of Manticore's engines: evm or native.
"""
args = parse_arguments()

if args.no_colors:
log.disable_colors()
def is_wasm():
for arg in sys.argv[1:]:
if not arg.startswith("-") and (arg.endswith(".wasm") or arg.endswith(".wat")):
return True
return False

sys.setrecursionlimit(consts.recursionlimit)

set_verbosity(args.v)
if __name__ == "__main__":
"""
Dispatches execution into one of Manticore's engines: evm or native or wasm.
"""

resources.check_disk_usage()
resources.check_memory_usage()

if args.argv[0].endswith(".sol") or is_supported(args.argv[0]):
ethereum_main(args, logger)
elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"):
wasm_main(args, logger)

if is_eth():
ethereum_main()
elif is_wasm():
wasm_main()
else:
install_helper.ensure_native_deps()
native_main(args, logger)


def parse_arguments() -> argparse.Namespace:
def positive(value):
ivalue = int(value)
if ivalue <= 0:
raise argparse.ArgumentTypeError("Argument must be positive")
return ivalue

parser = argparse.ArgumentParser(
description="Symbolic execution tool",
prog="manticore",
formatter_class=argparse.ArgumentDefaultsHelpFormatter,
)

# Add crytic compile arguments
# See https://github.com/crytic/crytic-compile/wiki/Configuration
cryticparser.init(parser)

parser.add_argument("--context", type=str, default=None, help=argparse.SUPPRESS)
parser.add_argument(
"--coverage", type=str, default="visited.txt", help="Where to write the coverage data"
)
parser.add_argument("--names", type=str, default=None, help=argparse.SUPPRESS)
parser.add_argument(
"--no-colors", action="store_true", help="Disable ANSI color escape sequences in output"
)
parser.add_argument("--offset", type=int, default=16, help=argparse.SUPPRESS)
# FIXME (theo) Add some documentation on the different search policy options
parser.add_argument(
"--policy",
type=str,
default="random",
help=(
"Search policy. random|adhoc|uncovered|dicount"
"|icount|syscount|depth. (use + (max) or - (min)"
" to specify order. e.g. +random)"
),
)
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, help="Specify verbosity level from -v to -vvvv"
)
parser.add_argument(
"--workspace",
type=str,
default=None,
help=("A folder name for temporaries and results." "(default mcore_?????)"),
)

current_version = pkg_resources.get_distribution("manticore").version
parser.add_argument(
"--version",
action="version",
version=f"Manticore {current_version}",
help="Show program version information",
)
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=++++)',
)
bin_flags.add_argument(
"--pure-symbolic", action="store_true", help="Treat all writable memory as symbolic"
)

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)",
)

eth_flags.add_argument(
"--txnocoverage", action="store_true", help="Do not use coverage as stopping criteria"
)

eth_flags.add_argument(
"--txnoether", action="store_true", help="Do not attempt to send ether to contract"
)

eth_flags.add_argument(
"--txaccount",
type=str,
default="attacker",
help='Account used as caller in the symbolic transactions, either "attacker" or '
'"owner" or "combo1" (uses both)',
)

eth_flags.add_argument(
"--txpreconstrain",
action="store_true",
help="Constrain human transactions to avoid exceptions in the contract function dispatcher",
)

eth_flags.add_argument(
"--contract", type=str, help="Contract name to analyze in case of multiple contracts"
)

eth_detectors = parser.add_argument_group("Ethereum detectors")

eth_detectors.add_argument(
"--list-detectors",
help="List available detectors",
action=ListEthereumDetectors,
nargs=0,
default=False,
)

eth_detectors.add_argument(
"--exclude",
help="Comma-separated list of detectors that should be excluded",
action="store",
dest="detectors_to_exclude",
default="",
)

eth_detectors.add_argument(
"--exclude-all", help="Excludes all detectors", action="store_true", default=False
)

eth_flags.add_argument(
"--avoid-constant",
action="store_true",
help="Avoid exploring constant functions for human transactions",
)

eth_flags.add_argument(
"--limit-loops",
action="store_true",
help="Avoid exploring constant functions for human transactions",
)

eth_flags.add_argument(
"--no-testcases",
action="store_true",
help="Do not generate testcases for discovered states when analysis finishes",
)

eth_flags.add_argument(
"--only-alive-testcases",
action="store_true",
help="Do not generate testcases for invalid/throwing states when analysis finishes",
)

eth_flags.add_argument(
"--quick-mode",
action="store_true",
help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, "
"do not explore constant functions. Disable all detectors.",
)

config_flags = parser.add_argument_group("Constants")
config.add_config_vars_to_argparse(config_flags)

parsed = parser.parse_args(sys.argv[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"):
parsed.policy = "+" + parsed.policy[3:]

return parsed


class ListEthereumDetectors(argparse.Action):
def __call__(self, parser, *args, **kwargs):
from .ethereum.cli import get_detectors_classes
from .utils.command_line import output_detectors

output_detectors(get_detectors_classes())
parser.exit()


if __name__ == "__main__":
main()
native_main()
58 changes: 36 additions & 22 deletions manticore/core/manticore.py
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,17 @@
import signal
from enum import Enum

consts = config.get_group("core")
consts.add(
"workspace",
default="",
description="A folder name for temporaries and results." "(default mcore_?????)",
)
consts.add(
"outputspace",
default="",
description="Folder to place final output. Defaults to workspace (default: use the worspace)",
)

class MProcessingType(Enum):
"""Used as configuration constant for choosing multiprocessing flavor"""
Expand Down Expand Up @@ -189,9 +200,12 @@ def newFunction(self, *args, **kw):
"terminate_execution",
}

def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kwargs):
def __init__(self, initial_state, cfg: config.Config = None, **kwargs):
"""
Manticore symbolically explores program states.
:param initial_state: State to start from.
:param cfg: The configuration constants

Manticore symbolically explores program states.


**Manticore phases**
Expand Down Expand Up @@ -297,10 +311,12 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw


:param initial_state: the initial root `State` object to start from
:param workspace_url: workspace folder name
:param outputspace_url: Folder to place final output. Defaults to workspace
:param kwargs: other kwargs, e.g.
"""
if cfg is None:
cfg = config.get_default_config()
self.config = cfg
self.config.freeze()
super().__init__()
random.seed(consts.seed)
{
Expand Down Expand Up @@ -330,15 +346,15 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw
# Manticore will use the output to save the final reports.
# By default the output folder and the workspace folder are the same.
# Check type, default to fs:
if isinstance(workspace_url, str):
if ":" not in workspace_url:
workspace_url = f"fs:{workspace_url}"
else:
if workspace_url is not None:
raise TypeError(f"Invalid workspace type: {type(workspace_url).__name__}")
workspace_url = cfg["core"].workspace
outputspace_url = cfg["core"].outputspace
if not isinstance(workspace_url, str):
raise TypeError(f"Invalid workspace type: {type(workspace).__name__}")
if ":" not in workspace_url:
workspace_url = f"fs:{workspace_url}"
self._workspace = Workspace(workspace_url)
# reuse the same workspace if not specified
if outputspace_url is None:
if not outputspace_url:
outputspace_url = f"fs:{self._workspace.uri}"
self._output = ManticoreOutput(outputspace_url)

Expand Down Expand Up @@ -962,19 +978,17 @@ def kill_timeout(self, timeout=None):

# Run forever is timeout is negative
if timeout <= 0:
yield
else:

# THINKME kill grabs the lock. Is npt this a deadlock hazard?
timer = threading.Timer(timeout, self.kill)
timer.start()

try:
yield
finally:
return

# THINKME kill grabs the lock. Is npt this a deadlock hazard?
timer = threading.Timer(timeout, self.kill)
timer.start()

try:
yield
finally:
timer.cancel()
timer.cancel()

@at_not_running
def run(self):
Expand Down Expand Up @@ -1057,6 +1071,6 @@ def save_run_data(self):
f.write(" ".join(map(shlex.quote, sys.argv)))

with self._output.save_stream("manticore.yml") as f:
config.save(f)
self.config.save(f)

logger.info("Results in %s", self._output.store.uri)
Loading