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
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
63 commits
Select commit Hold shift + click to select a range
75a0f25
[WIP][WIP][WIP] Moving executor functionality to ManticoreBase and re…
feliam Mar 7, 2019
6fd87c3
Workspace locks
feliam Mar 12, 2019
fa7785b
Concurrency flavor configurable from commandline
feliam Mar 14, 2019
74209fe
Asserts and refactorrrrrrrs
feliam Mar 14, 2019
3749ab7
Remove unused callback
feliam Mar 18, 2019
1e61fc7
Some CC
feliam Mar 18, 2019
d0b6301
Some CC
feliam Mar 18, 2019
1a1d9e1
Some CC
feliam Mar 18, 2019
8730d0f
Fix solver vs Z3Solver
feliam Mar 18, 2019
b19d267
Make solver a singleton based on tid/pid. REfactor m._save. Fix some …
feliam Mar 20, 2019
32fb373
typo and evm bugfix
feliam Mar 20, 2019
84cccb6
Fix some tests referecing global solver
feliam Mar 21, 2019
b8f96b2
Fix concolic tests and more global solver refs
feliam Mar 21, 2019
e8d918a
Fix tests
feliam Mar 21, 2019
ce4c0fd
CC fixes
feliam Mar 21, 2019
d6eb5c7
Fix tests. Fix testcase id generation
feliam Mar 21, 2019
a7c083e
Move profiling to a plugin and fix tests
feliam Mar 21, 2019
4bd5c3b
Add solver intance ref to mem test
feliam Mar 22, 2019
86446bf
Fix mem workspace tests
feliam Mar 25, 2019
946e69c
Fix output checking tests
feliam Mar 25, 2019
943dfbe
Fix z3solver ref
feliam Mar 25, 2019
df387b1
Relax verbosity/log tests
feliam Mar 26, 2019
0203531
Moved Workers to its own file
feliam Mar 26, 2019
b8eb691
Relax output tests
feliam Mar 26, 2019
7c908fc
Relax output tests
feliam Mar 26, 2019
5e22b41
Fix profiling test
feliam Mar 26, 2019
6482053
merge
feliam Mar 26, 2019
dc73fc2
Fix more tests
feliam Mar 27, 2019
1ec6044
Default multiprocessing
feliam Mar 27, 2019
9ebb3b4
Try to clean mcore __del__
feliam Mar 27, 2019
6889f4d
Change Worker life span
feliam Mar 27, 2019
9d4b2e1
Fix Single mode
feliam Mar 28, 2019
f9dfa4c
CC
feliam Mar 28, 2019
7f9452b
Merge branch 'master' into dev-executor-refactor
feliam Mar 28, 2019
8c6155e
revert verbosity travis
feliam Mar 29, 2019
ff3941a
CC and solver ref fix
feliam Mar 29, 2019
b304ad2
Relax ouput checking tests and some bugfixes
feliam Mar 29, 2019
449ec92
running -> ready
feliam Mar 29, 2019
c02b4ee
Fixing teeests
feliam Mar 29, 2019
7f806e8
add weak cache to _load
feliam Mar 30, 2019
ba35d64
del debug prints
feliam Mar 30, 2019
1959066
Adding config.py support for Enums
feliam Apr 8, 2019
fb1f798
Try/Remove generate_testcase event as it never occurs online. Fix tests
feliam Apr 9, 2019
3e535d2
Fix CC
feliam Apr 9, 2019
110f7e6
Kill the cache when start/stop run. Remove debugprints. clean tests
feliam Apr 12, 2019
78665f1
Fix travis test _other_
feliam Apr 16, 2019
62938fd
Fix native tests and timeout
feliam Apr 18, 2019
ea7bac0
Fix state.must_be_true
feliam Apr 18, 2019
15dd6cb
fix CC
feliam Apr 18, 2019
da71509
Merge and fix more tests
feliam Apr 18, 2019
a6c9bf2
Changing fstat tets...:
feliam Apr 22, 2019
8ff874f
LLLLLLLLinux tests
feliam Apr 22, 2019
8ef7246
Skip unicorn concrete test for now
feliam Apr 25, 2019
1b83156
Try fix CodeClimate
feliam Apr 25, 2019
8d8c1d5
Try fix CodeClimate
feliam Apr 25, 2019
ed251fb
Update evm examples to newest solidity
feliam Apr 25, 2019
4b75e0d
Complete transformation of consts.mprocessing to enum
feliam Apr 25, 2019
e6cf11d
Add blank line (codeclimate)
Apr 26, 2019
1c25bff
Using the enum instead of the string
feliam Apr 30, 2019
ee9bb2c
Merge branch 'dev-executor-refactor' of github.com:trailofbits/mantic…
feliam Apr 30, 2019
cb5d416
Using the enum instead of the string
feliam Apr 30, 2019
433b9ba
Merge branch 'master' into dev-executor-refactor
feliam May 7, 2019
c3c4677
Fix solver instance reference
feliam May 9, 2019
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
2 changes: 1 addition & 1 deletion .codeclimate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ checks:
method-count:
enabled: false
config:
threshold: 35
threshold: 45
method-lines:
enabled: true
config:
Expand Down
9 changes: 4 additions & 5 deletions examples/evm/coverage.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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]){
Expand All @@ -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
Expand All @@ -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;
Expand All @@ -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);
}
}
}
Expand Down
1 change: 0 additions & 1 deletion examples/evm/simple_int_overflow.sol
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
pragma solidity ^0.4.15;
contract Overflow {
uint private sellerBalance=0;

Expand Down
2 changes: 0 additions & 2 deletions examples/evm/simple_multi_func.sol
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
pragma solidity ^0.4.13;

contract Test {
event Log(string);
mapping(address => uint) private balances;
Expand Down
5 changes: 2 additions & 3 deletions examples/evm/simple_value_check.sol
Original file line number Diff line number Diff line change
@@ -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");

}

Expand Down
8 changes: 3 additions & 5 deletions examples/evm/two_tx_ovf.sol
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
pragma solidity ^0.4.15;

contract SymExExample {
uint did_init = 0;

Expand All @@ -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");
}

}
Expand Down
2 changes: 0 additions & 2 deletions examples/evm/umd_example.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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 {


Expand Down
27 changes: 17 additions & 10 deletions examples/script/concolic.py
Original file line number Diff line number Diff line change
Expand Up @@ -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 *
Expand All @@ -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)
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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 = []
Expand Down
2 changes: 1 addition & 1 deletion examples/script/count_instructions.py
Original file line number Diff line number Diff line change
Expand Up @@ -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.")
5 changes: 3 additions & 2 deletions manticore/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -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__]
11 changes: 2 additions & 9 deletions manticore/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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:
Expand Down
Loading