DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Update concolic.py (#887)

Browse Source 
* Update concolic.py

* update what evt we subscribe to
This commit is contained in:
Yan Ivnitskiy 2018-05-03 18:52:29 -04:00 committed by GitHub
parent 9307475af5
commit 9c258bd68d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 7 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
examples/script/concolic.py
View File

@ -28,7 +28,6 @@ import copy
from manticore.core.smtlib.expression import * from manticore.core.smtlib.expression import *
prog = '../linux/simpleassert' prog = '../linux/simpleassert'
main_end = 0x400ae9
VERBOSITY = 0 VERBOSITY = 0
def _partition(pred, iterable): def _partition(pred, iterable):
@ -164,15 +163,16 @@ def symbolic_run_get_cons(trace):
m2.verbosity(VERBOSITY) m2.verbosity(VERBOSITY)
m2.register_plugin(f) m2.register_plugin(f)
@m2.hook(main_end) def on_term_testcase(mcore, state, stateid, err):
def x(s):
with m2.locked_context() as ctx: with m2.locked_context() as ctx:
readdata = [] 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: if name in ('_receive', '_read') and fd == 0:
readdata.append(data) readdata.append(data)
ctx['readdata'] = readdata 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() m2.run()
@ -231,7 +231,7 @@ def concrete_input_to_constraints(ci, prev=None):
trc = concrete_run_get_trace(ci) trc = concrete_run_get_trace(ci)
# Only heed new traces # 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: if trace_rips in traces:
return [], [] return [], []
traces.add(trace_rips) traces.add(trace_rips)
@ -251,12 +251,6 @@ def concrete_input_to_constraints(ci, prev=None):
def main(): 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() q = Queue.Queue()

4
scripts/travis_test.sh
View File

@ -10,9 +10,7 @@ run_examples() {
# concolic assumes presence of ../linux/simpleassert # concolic assumes presence of ../linux/simpleassert
echo "Running concolic.py..." echo "Running concolic.py..."
HW=../linux/helloworld HW=../linux/helloworld
SA=../linux/simpleassert python ./concolic.py
END_OF_MAIN=$(objdump -d $SA|awk -v RS= '/^[[:xdigit:]].*<main>/'|grep ret|tr -d ' ' | awk -F: '{print "0x" $1}')
python ./concolic.py $END_OF_MAIN
if [ $? -ne 0 ]; then if [ $? -ne 0 ]; then
return 1 return 1
fi fi