diff --git a/examples/script/concolic.py b/examples/script/concolic.py index 5c3ec99..7a1ed3c 100755 --- a/examples/script/concolic.py +++ b/examples/script/concolic.py @@ -28,7 +28,6 @@ import copy from manticore.core.smtlib.expression import * prog = '../linux/simpleassert' -main_end = 0x400ae9 VERBOSITY = 0 def _partition(pred, iterable): @@ -164,15 +163,16 @@ def symbolic_run_get_cons(trace): m2.verbosity(VERBOSITY) m2.register_plugin(f) - @m2.hook(main_end) - def x(s): + def on_term_testcase(mcore, state, stateid, err): with m2.locked_context() as ctx: readdata = [] - for name, fd, data in s.platform.syscall_trace: + for name, fd, data in state.platform.syscall_trace: if name in ('_receive', '_read') and fd == 0: readdata.append(data) ctx['readdata'] = readdata - ctx['constraints'] = list(s.constraints.constraints) + ctx['constraints'] = list(state.constraints.constraints) + + m2.subscribe('will_terminate_state', on_term_testcase) m2.run() @@ -231,7 +231,7 @@ def concrete_input_to_constraints(ci, prev=None): trc = concrete_run_get_trace(ci) # Only heed new traces - trace_rips = tuple(x['values']['RIP'] for x in trc if x['type'] == 'regs') + trace_rips = tuple(x['values']['RIP'] for x in trc if x['type'] == 'regs' and 'RIP' in x['values']) if trace_rips in traces: return [], [] traces.add(trace_rips) @@ -251,12 +251,6 @@ def concrete_input_to_constraints(ci, prev=None): def main(): - global main_end - - # Read the address of main's `ret` from cmdline if we're passed it. Used for testing. - if len(sys.argv) > 1: - main_end = int(sys.argv[1], 0) - log("Got end of main: {:x}".format(main_end)) q = Queue.Queue() diff --git a/scripts/travis_test.sh b/scripts/travis_test.sh index 27dca47..b92fd29 100755 --- a/scripts/travis_test.sh +++ b/scripts/travis_test.sh @@ -10,9 +10,7 @@ run_examples() { # concolic assumes presence of ../linux/simpleassert echo "Running concolic.py..." HW=../linux/helloworld - SA=../linux/simpleassert - END_OF_MAIN=$(objdump -d $SA|awk -v RS= '/^[[:xdigit:]].*
/'|grep ret|tr -d ' ' | awk -F: '{print "0x" $1}') - python ./concolic.py $END_OF_MAIN + python ./concolic.py if [ $? -ne 0 ]; then return 1 fi