DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

added _multiprocess_can_split_ directive (#351)

Browse Source 
* added _multiprocess_can_split_ directive

* renamed Readme
This commit is contained in:
Theofilos Petsios
2017-06-23 17:53:19 -04:00
committed by GitHub
parent 6133a0e2ed
commit e2c0414dca
25 changed files with 12853 additions and 12790 deletions
Download Patch File Download Diff File Expand all files Collapse all files
README.md
+9
View File
@@ -104,6 +104,15 @@ nosetests tests/test_armv7cpu.py:Armv7CpuInstructions
nosetests tests/test_armv7cpu.py:Armv7CpuInstructions.test_mov_imm_min
```
Moreover, you can invoke multiprocess test invocation via the --processes
flag. Note, however, that several tests (e.g., tests/test_memdumps.py) require
longer execution times, thus you need to specify the appropriate timeout
period via the --process-timeout flag. E.g.,
```
nosetests --processes=8 --process-timeout=120 tests/test_binaries.py
```
## Usage
```
tests/auto/README
-18
View File
@@ -1,18 +0,0 @@
Auto unittest generation
------------------------
1) You need a linux program that exercises a bunch of interestings intructions.
Lets choose:
SymbolicExecutor/examples/linux/nostdlib
2) Run the tracer on it. It is a gdb wrapper that will execute the program step by step
printing pre/pos information on each instruction:
python SymbolicExecutor/tests/auto/make_dump.py SymbolicExecutor/examples/linux/nostdlib > mytest.dump
(Several dump can be concatenated togheter)
3) Generate the alcual python unittest based on the dump.
python SymbolicExecutor/tests/auto/make_tests.py mytest.dump > SymbolicExecutor/tests/test_$TESTNAME.py
This will get up to 1000 testcases for the same mnemonic in the dump.
4) Run the test like this (SymbolicExecutor/)
python -m unittest -c tests.test_$TESTNAME
tests/auto/Readme.md
+24
View File
@@ -0,0 +1,24 @@
Auto unittest generation
------------------------
1) You need a Linux program that exercises a set of interestings intructions.
For instance try `make` in examples/linux.
2) Run the tracer on your program. It is a gdb wrapper that will execute the program step by step
printing pre/pos information on each instruction:
```
python make_dump.py ../../examples/linux/nostdlib32 > mytest.dump
```
(Several dumps can be concatenated togheter)
3) Generate the actual python unittest based on the dump.
```
python make_tests.py mytest.dump > SymbolicExecutor/tests/test_example.py
```
This will get up to 1000 testcases for the same mnemonic in the dump.
4) Run the test:
```
python -m unittest -c test_example
```
tests/auto/make_tests.py
+43 -17
View File
@@ -26,12 +26,39 @@ for test in tests:
print """
import unittest
import functools
from manticore.core.cpu.x86 import *
from manticore.core.smtlib import Operators
from manticore.core.memory import *
def skipIfNotImplemented(f):
# XXX(yan) the inner function name must start with test_
@functools.wraps(f)
def test_inner(*args, **kwargs):
try:
return f(*args, **kwargs)
except NotImplementedError, e:
raise unittest.SkipTest(e.message)
return test_inner
def forAllTests(decorator):
def decorate(cls):
for attr in cls.__dict__:
if not attr.startswith('test_'):
continue
method = getattr(cls, attr)
if callable(method):
setattr(cls, attr, decorator(method))
return cls
return decorate
@forAllTests(skipIfNotImplemented)
class CPUTest(unittest.TestCase):
_multiprocess_can_split_ = True
class ROOperand(object):
''' Mocking class for operand ronly '''
def __init__(self, size, value):
@@ -45,12 +72,11 @@ class CPUTest(unittest.TestCase):
def write(self, value):
self.value = value & ((1<<self.size)-1)
return self.value
"""
def isFlag(x):
return x in ['OF', 'SF', 'ZF', 'AF', 'PF', 'CF', 'DF']
return x in ['OF', 'SF', 'ZF', 'AF', 'PF', 'CF', 'DF']
def regSize(x):
if x in ('BPL', 'AH', 'CH', 'DH', 'BH', 'AL', 'CL', 'DL', 'BL', 'SIL', 'DIL', 'SIH', 'DIH', 'R8B', 'R9B', 'R10B', 'R11B', 'R12B', 'R13B', 'R14B', 'R15B'):
@@ -75,7 +101,7 @@ def regSize(x):
raise Exception('FPU not supported')
raise Exception('%s not supported', x)
def get_maps(test):
pages = set()
@@ -95,23 +121,23 @@ def get_maps(test):
for test_name in sorted(test_dic.keys()):
for test_name in sorted(test_dic.keys()):
test = test_dic[test_name]
bits = {'i386': 32, 'amd64': 64}[test['arch']]
pc = {'i386': 'EIP', 'amd64': 'RIP'}[test['arch']]
print """
def test_%(test_name)s(self):
''' Instruction %(test_name)s
Groups: %(groups)s
''' Instruction %(test_name)s
Groups: %(groups)s
%(disassembly)s
'''
mem = Memory%(bits)d()
cpu = %(cpu)s(mem)"""%{ 'test_name': test_name,
'groups': ', '.join(map(str,test['groups'])),
'disassembly': test['disassembly'],
'bits': bits,
'disassembly': test['disassembly'],
'bits': bits,
'arch': test['arch'],
'cpu': {64:'AMD64Cpu', 32:'I386Cpu'}[bits], }
@@ -125,7 +151,7 @@ for test_name in sorted(test_dic.keys()):
for reg_name, value in test['pre']['registers'].items():
if isFlag(reg_name):
print """ cpu.%s = %r"""%(reg_name, value)
print """ cpu.%s = %r"""%(reg_name, value)
else:
print """ cpu.%s = 0x%x"""%(reg_name, value)
@@ -138,24 +164,24 @@ for test_name in sorted(test_dic.keys()):
for reg_name, value in test['pos']['registers'].items():
print """ self.assertEqual(cpu.%s, %r)"""%(reg_name, value)
for test_name in sorted(test_dic.keys()):
for test_name in sorted(test_dic.keys()):
test = test_dic[test_name]
bits = {'i386': 32, 'amd64': 64}[test['arch']]
pc = {'i386': 'EIP', 'amd64': 'RIP'}[test['arch']]
print """
def test_%(test_name)s_symbolic(self):
''' Instruction %(test_name)s
Groups: %(groups)s
''' Instruction %(test_name)s
Groups: %(groups)s
%(disassembly)s
'''
cs = ConstraintSet()
mem = SMemory%(bits)d(cs)
cpu = %(cpu)s(mem)"""%{ 'test_name': test_name,
'groups': ', '.join(map(str,test['groups'])),
'disassembly': test['disassembly'],
'bits': bits,
'disassembly': test['disassembly'],
'bits': bits,
'arch': test['arch'],
'cpu': {64:'AMD64Cpu', 32:'I386Cpu'}[bits] }
@@ -214,7 +240,7 @@ for test_name in sorted(test_dic.keys()):
print """ condition = Operators.AND(condition, cpu.%s == %r)"""%(reg_name, value)
else:
print """ condition = Operators.AND(condition, cpu.%s == 0x%x)"""%(reg_name, value)
print """
with cs as temp_cs:
tests/test_abi.py
+8 -7
View File
@@ -21,6 +21,7 @@ from manticore.core.memory import SMemory32, Memory32, SMemory64
from manticore.core.smtlib import ConstraintSet, Operators
class ABITests(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
mem32 = SMemory32(ConstraintSet())
mem32.mmap(0x1000, 0x1000, 'rw ')
@@ -51,7 +52,7 @@ class ABITests(unittest.TestCase):
def test_executor(self):
pass
def test_arm_abi_simple(self):
cpu = self._cpu_arm
@@ -148,7 +149,7 @@ class ABITests(unittest.TestCase):
def test_i386_cdecl(self):
cpu = self._cpu_x86
base = cpu.ESP
base = cpu.ESP
self.assertEqual(cpu.read_int(cpu.ESP), 0x80)
cpu.push(0x1234, cpu.address_bit_size)
@@ -170,7 +171,7 @@ class ABITests(unittest.TestCase):
def test_i386_stdcall(self):
cpu = self._cpu_x86
base = cpu.ESP
base = cpu.ESP
bwidth = cpu.address_bit_size / 8
self.assertEqual(cpu.read_int(cpu.ESP), 0x80)
@@ -201,7 +202,7 @@ class ABITests(unittest.TestCase):
cpu.push(0x1234, cpu.address_bit_size)
eip = 0xDEADBEEF
base = cpu.ESP
base = cpu.ESP
cpu.EIP = eip
def test(one, two, three, four, five):
raise ConcretizeArgument(2)
@@ -218,10 +219,10 @@ class ABITests(unittest.TestCase):
def test_i386_cdecl_concretize(self):
cpu = self._cpu_x86
base = cpu.ESP
base = cpu.ESP
prev_eax = 0xcc
cpu.EAX = prev_eax
self.assertEqual(cpu.read_int(cpu.ESP), 0x80)
cpu.push(0x1234, cpu.address_bit_size)
@@ -393,7 +394,7 @@ class ABITests(unittest.TestCase):
cpu.push(2, cpu.address_bit_size)
cpu.push(0x1234, cpu.address_bit_size)
def test(prefix, extracted):
self.assertEquals(prefix, 1)
self.assertEquals(extracted, 2)
tests/test_allinsts.py
+9125 -9124
View File
File diff suppressed because it is too large Load Diff
tests/test_armv7_bitwise.py
+2 -1
View File
@@ -1,9 +1,10 @@
import unittest
from manticore.core.cpu import bitwise
class Armv7RF(unittest.TestCase):
_multiprocess_can_split_ = True
def test_mask(self):
masked = bitwise.Mask(8)
tests/test_armv7cpu.py
+2
View File
@@ -23,6 +23,8 @@ def assemble(asm):
class Armv7CpuTest(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
self.c = Cpu(Memory32())
self.rf = self.c.regfile
tests/test_armv7rf.py
+3 -1
View File
@@ -1,11 +1,13 @@
import unittest
from manticore.core.cpu.arm import Armv7RegisterFile as RF
from manticore.core.cpu.arm import *
from capstone.arm import *
class Armv7RF(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
self.r = RF()
tests/test_binaries.py
+5 -4
View File
@@ -13,6 +13,7 @@ import time
# level = logging.DEBUG)
class IntegrationTest(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
# Create a temporary directory
self.test_dir = tempfile.mkdtemp()
@@ -26,7 +27,7 @@ class IntegrationTest(unittest.TestCase):
with open(os.path.join(os.pardir, logfile), "w") as output:
po = subprocess.Popen(procargs, stdout=output)
secs_used = 0
while po.poll() is None and secs_used < timeout:
time.sleep(1)
sys.stderr.write("~")
@@ -49,7 +50,7 @@ class IntegrationTest(unittest.TestCase):
with open(os.path.join(os.pardir, '%s/output.log'%self.test_dir), "w") as output:
subprocess.check_call(['python', '-m', 'manticore',
'--workspace', workspace,
'--timeout', '1',
'--timeout', '1',
'--procs', '4',
filename,
'+++++++++'], stdout=output)
@@ -85,7 +86,7 @@ class IntegrationTest(unittest.TestCase):
assertions = '%s/assertions.txt'%self.test_dir
file(assertions,'w').write('0x0000000000401003 ZF == 1')
with open(os.path.join(os.pardir, '%s/output.log'%self.test_dir), "w") as output:
self._runWithTimeout(['python', SE,
self._runWithTimeout(['python', SE,
'--workspace', workspace,
'--proc', '4',
'--assertions', assertions,
@@ -106,7 +107,7 @@ class IntegrationTest(unittest.TestCase):
self.assertEqual(len(data), 1828)
self.assertEqual(hashlib.md5(data).hexdigest() , '8955a29d51c1edd39b0e53794ebcf464')
workspace = '%s/workspace'%self.test_dir
self._runWithTimeout(['python', '-m', 'manticore',
self._runWithTimeout(['python', '-m', 'manticore',
'--workspace', workspace,
'--timeout', '20',
'--proc', '4',
tests/test_cpu_automatic.py
+2702 -2701
View File
File diff suppressed because it is too large Load Diff
tests/test_cpu_manual.py
+40 -39
View File
@@ -21,6 +21,7 @@ class RWOperand(ROOperand):
sizes = {'RAX': 64, 'EAX': 32, 'AX': 16, 'AL': 8, 'AH': 8, 'RCX': 64, 'ECX': 32, 'CX': 16, 'CL': 8, 'CH': 8, 'RDX': 64, 'EDX': 32, 'DX': 16, 'DL': 8, 'DH': 8, 'RBX': 64, 'EBX': 32, 'BX': 16, 'BL': 8, 'BH': 8, 'RSP': 64, 'ESP': 32, 'SP': 16, 'SPL': 8, 'RBP': 64, 'EBP': 32, 'BP': 16, 'BPL': 8, 'RSI': 64, 'ESI': 32, 'SI': 16, 'SIL': 8, 'RDI': 64, 'EDI': 32, 'DI': 16, 'DIL': 8, 'R8': 64, 'R8D': 32, 'R8W': 16, 'R8B': 8, 'R9': 64, 'R9D': 32, 'R9W': 16, 'R9B': 8, 'R10': 64, 'R10D': 32, 'R10W': 16, 'R10B': 8, 'R11': 64, 'R11D': 32, 'R11W': 16, 'R11B': 8, 'R12': 64, 'R12D': 32, 'R12W': 16, 'R12B': 8, 'R13': 64, 'R13D': 32, 'R13W': 16, 'R13B': 8, 'R14': 64, 'R14D': 32, 'R14W': 16, 'R14B': 8, 'R15': 64, 'R15D': 32, 'R15W': 16, 'R15B': 8, 'ES': 16, 'CS': 16, 'SS': 16, 'DS': 16, 'FS': 16, 'GS': 16, 'RIP': 64, 'EIP':32, 'IP': 16, 'RFLAGS': 64, 'EFLAGS': 32, 'FLAGS': 16, 'XMM0': 128, 'XMM1': 128, 'XMM2': 128, 'XMM3': 128, 'XMM4': 128, 'XMM5': 128, 'XMM6': 128, 'XMM7': 128, 'XMM8': 128, 'XMM9': 128, 'XMM10': 128, 'XMM11': 128, 'XMM12': 128, 'XMM13': 128, 'XMM14': 128, 'XMM15': 128, 'YMM0': 256, 'YMM1': 256, 'YMM2': 256, 'YMM3': 256, 'YMM4': 256, 'YMM5': 256, 'YMM6': 256, 'YMM7': 256, 'YMM8': 256, 'YMM9': 256, 'YMM10': 256, 'YMM11': 256, 'YMM12': 256, 'YMM13': 256, 'YMM14': 256, 'YMM15': 256}
class SymCPUTest(unittest.TestCase):
_multiprocess_can_split_ = True
_flag_offsets = {
'CF': 0,
'PF': 2,
@@ -41,7 +42,7 @@ class SymCPUTest(unittest.TestCase):
'DF': 0x00400,
'OF': 0x00800,
'IF': 0x00200,}
class ROOperand(object):
''' Mocking class for operand ronly '''
def __init__(self, size, value):
@@ -97,7 +98,7 @@ class SymCPUTest(unittest.TestCase):
cpu.SI = 0xAAAA
self.assertEqual(cpu.SI, 0xAAAA)
cpu.RAX = 0x12345678aabbccdd
self.assertEqual(cpu.ESI, 0x1234AAAA)
cpu.SI = 0xAAAA
@@ -464,7 +465,7 @@ class SymCPUTest(unittest.TestCase):
cpu.write_int(0x1000, 0x4142434445464748, 64)
cpu.write_int(0x1004, 0x5152535455565758, 64)
cpu.write_int(0x1008, 0x6162636465666768, 64)
self.assertEqual(cpu.read_int(0x1000,32), 0x45464748)
self.assertEqual(cpu.read_int(0x1004,32), 0x55565758)
self.assertEqual(cpu.read_int(0x1008,32), 0x65666768)
@@ -501,7 +502,7 @@ class SymCPUTest(unittest.TestCase):
cs.add(addr1 == 0x1004)
cpu.write_int(addr1, 0x58, 8)
# 48 47 46 45 58 43 42 41 68 67 66 65 64 63 62 61
# 48 47 46 45 58 43 42 41 68 67 66 65 64 63 62 61
value = cpu.read_int(0x1004, 16)
self.assertItemsEqual(solver.get_all_values(cs, value), [0x4358] )
@@ -509,14 +510,14 @@ class SymCPUTest(unittest.TestCase):
addr2 = cs.new_bitvec(64)
cs.add(Operators.AND(addr2>=0x1000, addr2<=0x100c))
cpu.write_int(addr2, 0x5959, 16)
cpu.write_int(addr2, 0x5959, 16)
solutions = solver.get_all_values(cs, cpu.read_int(addr2, 32) )
self.assertEqual( len(solutions), 0x100c-0x1000+1 )
self.assertEqual( set(solutions), set([0x45465959, 0x41425959, 0x58455959, 0x65665959, 0x67685959, 0x43585959, 0x68415959, 0x42435959, 0x66675959, 0x62635959, 0x64655959, 0x63645959, 0x61625959]))
def test_cache_004(self):
import random
cs = ConstraintSet()
@@ -615,7 +616,7 @@ class SymCPUTest(unittest.TestCase):
mem[code:code+3] = '\xf7\x7d\xf4'
cpu.EIP = code
cpu.EAX = cs.new_bitvec(32, 'EAX')
cpu.EAX = cs.new_bitvec(32, 'EAX')
cs.add(cpu.EAX == 116)
cpu.EBP = cs.new_bitvec(32, 'EBP')
cs.add(cpu.EBP == stack+0x700)
@@ -652,11 +653,11 @@ class SymCPUTest(unittest.TestCase):
mem[code:code+2] = '\xf7\xf9'
cpu.EIP = code
cpu.EAX = cs.new_bitvec(32, 'EAX')
cpu.EAX = cs.new_bitvec(32, 'EAX')
cs.add(cpu.EAX == 0xffffffff)
cpu.EDX = cs.new_bitvec(32, 'EDX')
cpu.EDX = cs.new_bitvec(32, 'EDX')
cs.add(cpu.EDX == 0xffffffff)
cpu.ECX = cs.new_bitvec(32, 'ECX')
cpu.ECX = cs.new_bitvec(32, 'ECX')
cs.add(cpu.ECX == 0x32)
cpu.execute()
@@ -695,11 +696,11 @@ class SymCPUTest(unittest.TestCase):
mem[code:code+2] = '\x13\xf2'
cpu.EIP = code
cpu.ESI = cs.new_bitvec(32, 'ESI')
cpu.ESI = cs.new_bitvec(32, 'ESI')
cs.add(cpu.ESI == 0)
cpu.EDX = cs.new_bitvec(32, 'EDX')
cpu.EDX = cs.new_bitvec(32, 'EDX')
cs.add(cpu.EDX == 0xffffffff)
cpu.CF = cs.new_bool('CF')
cpu.CF = cs.new_bool('CF')
cs.add(cpu.CF)
cpu.execute()
@@ -725,19 +726,19 @@ class SymCPUTest(unittest.TestCase):
mem[code:code+5] = '\xf0\x0f\xc7\x0f;'
cpu.EIP = code
cpu.EDI = cs.new_bitvec(32, 'EDI')
cpu.EDI = cs.new_bitvec(32, 'EDI')
cs.add( Operators.OR(cpu.EDI == 0x2000, cpu.EDI == 0x2100, cpu.EDI == 0x2200 ) )
self.assertEqual(sorted(solver.get_all_values(cs, cpu.EDI)),[0x2000,0x2100,0x2200])
self.assertEqual(cpu.read_int(0x2000,64), 0)
self.assertEqual(cpu.read_int(0x2100,64), 0)
self.assertEqual(cpu.read_int(0x2200,64), 0)
self.assertItemsEqual(solver.get_all_values(cs, cpu.read_int(cpu.EDI,64)), [0])
self.assertItemsEqual(solver.get_all_values(cs, cpu.read_int(cpu.EDI,64)), [0])
#self.assertEqual(cpu.read_int(cpu.EDI,64), 0 )
cpu.write_int(0x2100, 0x4142434445464748, 64)
cpu.EAX = cs.new_bitvec(32, 'EAX')
cpu.EAX = cs.new_bitvec(32, 'EAX')
cs.add( Operators.OR(cpu.EAX == 0x41424344, cpu.EAX == 0x0badf00d, cpu.EAX == 0xf7f7f7f7 ) )
cpu.EDX= 0x45464748
@@ -749,7 +750,7 @@ class SymCPUTest(unittest.TestCase):
def test_POPCNT(self):
'''POPCNT EAX, EAX
CPU Dump
Address Hex dump
Address Hex dump
00333689 F3 0F B8 C0
'''
@@ -768,8 +769,8 @@ class SymCPUTest(unittest.TestCase):
self.assertEqual(cpu.ZF, False)
def test_DEC_1(self):
''' Instruction DEC_1
Groups: mode64
''' Instruction DEC_1
Groups: mode64
0x41e10a: dec ecx
'''
mem = Memory64()
@@ -795,9 +796,9 @@ class SymCPUTest(unittest.TestCase):
self.assertEqual(cpu.ECX, 12L)
def test_PUSHFD_1(self):
''' Instruction PUSHFD_1
Groups: not64bitmode
0x8065f6f: pushfd
''' Instruction PUSHFD_1
Groups: not64bitmode
0x8065f6f: pushfd
'''
mem = Memory32()
cpu = I386Cpu(mem)
@@ -815,7 +816,7 @@ class SymCPUTest(unittest.TestCase):
cpu.ZF = True
cpu.PF = True
cpu.execute()
self.assertItemsEqual(mem[0xffffc600:0xffffc609], '\x55\x08\x00\x00\x02\x03\x00\x00\x00')
self.assertEqual(mem[0x8065f6f], '\x9c')
self.assertEqual(cpu.EIP, 0x8065f70)
@@ -823,9 +824,9 @@ class SymCPUTest(unittest.TestCase):
self.assertEqual(cpu.ESP, 0xffffc600)
def test_XLATB_1(self):
''' Instruction XLATB_1
Groups:
0x8059a8d: xlatb
''' Instruction XLATB_1
Groups:
0x8059a8d: xlatb
'''
mem = Memory32()
cpu = I386Cpu(mem)
@@ -838,16 +839,16 @@ class SymCPUTest(unittest.TestCase):
cpu.AL=0x0a
cpu.EIP = 0x8059a8d
cpu.execute()
self.assertEqual(mem[0x8059a8d], '\xd7')
self.assertEqual(mem[0xffffd00a], '\x41')
self.assertEqual(cpu.AL, 0x41)
self.assertEqual(cpu.AL, 0x41)
self.assertEqual(cpu.EIP, 134584974L)
def test_XLATB_1_symbolic(self):
''' Instruction XLATB_1
Groups:
0x8059a8d: xlatb
''' Instruction XLATB_1
Groups:
0x8059a8d: xlatb
'''
cs = ConstraintSet()
mem = SMemory32(cs)
@@ -862,8 +863,8 @@ class SymCPUTest(unittest.TestCase):
cpu.EBX=0xffffd000
def test_SAR_1(self):
''' Instruction SAR_1
Groups: mode64
''' Instruction SAR_1
Groups: mode64
0x41e10a: SAR cl, EBX
Using the SAR instruction to perform a division operation does not produce the same result as the IDIV instruction. The quotient from the IDIV instruction is rounded toward zero, whereas the "quotient" of the SAR instruction is rounded toward negative infinity. This difference is apparent only for negative numbers. For example, when the IDIV instruction is used to divide -9 by 4, the result is -2 with a remainder of -1. If the SAR instruction is used to shift -9 right by two bits, the result is -3 and the "remainder" is +3; however, the SAR instruction stores only the most significant bit of the remainder (in the CF flag).
@@ -931,10 +932,10 @@ Using the SAR instruction to perform a division operation does not produce the s
with cs as temp_cs:
temp_cs.add(condition == False)
self.assertFalse(solver.check(temp_cs))
def test_SAR_2(self):
''' Instruction SAR_2
''' Instruction SAR_2
'''
mem = Memory32()
@@ -1003,9 +1004,9 @@ Using the SAR instruction to perform a division operation does not produce the s
with cs as temp_cs:
temp_cs.add(condition == False)
self.assertFalse(solver.check(temp_cs))
def test_SAR_3_symbolic(self):
''' Instruction SAR_6
''' Instruction SAR_6
eax 0xffffd000 -12288
ecx 0x3d1ce0ff 1025302783
eip 0x80483f3 0x80483f3
tests/test_driver.py
+2 -1
View File
@@ -13,6 +13,7 @@ from manticore import Manticore, issymbolic
from manticore.core.smtlib import BitVecVariable
class ManticoreDriver(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
# Create a temporary directory
self.test_dir = tempfile.mkdtemp()
@@ -25,7 +26,7 @@ class ManticoreDriver(unittest.TestCase):
def testCreating(self):
m = Manticore('/bin/ls')
m.log_file = '/dev/null'
def test_issymbolic(self):
v = BitVecVariable(32, 'sym')
self.assertTrue(issymbolic(v))
tests/test_dyn.py
+253 -252
View File
File diff suppressed because it is too large Load Diff
tests/test_linux.py
+2 -1
View File
@@ -8,6 +8,7 @@ class LinuxTest(unittest.TestCase):
'''
TODO(mark): these tests assumes /bin/ls is a dynamic x64 binary
'''
_multiprocess_can_split_ = True
BIN_PATH = '/bin/ls'
def setUp(self):
@@ -79,4 +80,4 @@ class LinuxTest(unittest.TestCase):
model.syscall()
print ''.join(model.current.read_bytes(stat, 100)).encode('hex')
tests/test_manticore.py
+1
View File
@@ -3,6 +3,7 @@ import unittest
from manticore import Manticore
class ManticoreTest(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
self.m = Manticore('tests/binaries/arguments_linux_amd64')
tests/test_memdumps.py
+3 -3
View File
@@ -20,7 +20,7 @@ class IntegrationTest(unittest.TestCase):
def tearDown(self):
# Remove the directory after the test
shutil.rmtree(self.test_dir)
def _getDumpParams(self, jsonf):
self.assertTrue(os.path.exists(jsonf))
@@ -41,12 +41,12 @@ class IntegrationTest(unittest.TestCase):
with open(os.path.join(os.pardir, "logfile"), "w") as output:
po = subprocess.Popen(procargs, stdout=output)
secs_used = 0
while po.poll() is None and secs_used < timeout:
time.sleep(1)
sys.stderr.write("~")
secs_used += 1
self.assertTrue(secs_used < timeout)
sys.stderr.write("\n")
tests/test_memory.py
+81 -80
View File
@@ -15,6 +15,7 @@ def isconcrete(value):
class MemoryTest(unittest.TestCase):
_multiprocess_can_split_ = True
def get_open_fds(self):
fds = []
for fd in range(3, resource.RLIMIT_NOFILE):
@@ -76,14 +77,14 @@ class MemoryTest(unittest.TestCase):
#Check the default initial value
self.assertEqual(mem._search(0x1000, None), 0xf7fff000)
#alloc/map a byte at default address.
first = mem.mmap(None, 0x0001, 'r')
self.assertEqual(first, 0xf7fff000)
#Okay 2 maps
self.assertEqual(len(mem.mappings()), 1)
#check valid
#check valid
self.assertTrue(first in mem)
self.assertTrue(mem.access_ok((first), 'r'))
self.assertFalse(isinstance(mem[first], Expression))
@@ -99,7 +100,7 @@ class MemoryTest(unittest.TestCase):
second = mem.mmap(None, 0x1000, 'w')
#Okay 2 maps
self.assertEqual(len(mem.mappings()), 2)
#check valid
#check valid
self.assertTrue(second in mem)
self.assertTrue(mem.access_ok((second), 'w'))
self.assertTrue(second+0x1000-1 in mem)
@@ -107,10 +108,10 @@ class MemoryTest(unittest.TestCase):
#bytes outside the map should be not valid
self.assertFalse(second-1 in mem)
self.assertFalse(first+0x1000 in mem)
#alloc/map a byte
third = mem.mmap(None, 0x1000, 'x')
#Okay 3 maps
self.assertEqual(len(mem.mappings()), 3)
@@ -127,7 +128,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(first+0x1000 in mem)
self.assertFalse(mem.access_ok((second), 'x'))
mem.munmap(second,1)
mem.munmap(second,1)
self.assertFalse(second in mem)
self.assertEqual(len(mem.mappings()), 2)
@@ -136,7 +137,7 @@ class MemoryTest(unittest.TestCase):
self.assertEqual(forth, mem._ceil(third+1))
self.assertTrue(forth in mem)
self.assertTrue(mem.access_ok((forth), 'x'))
def test_search_and_mmap_several_chunks_testing_limits_memory_page_12(self):
mem = Memory32()
@@ -159,7 +160,7 @@ class MemoryTest(unittest.TestCase):
self.assertTrue(zero in mem)
self.assertRaises(AssertionError, mem.mmap, 0x0000F000, 0, 'r')
self.assertEqual(zero, 0)
def test_try_to_allocate_greater_than_last_space_memory_page_12(self):
@@ -225,7 +226,7 @@ class MemoryTest(unittest.TestCase):
self.assertRaises(MemoryException, mem.__setitem__, 0x1000, '\x41')
self.assertRaises(MemoryException, mem.__setitem__, sym, '\x41')
#alloc/map a byte
first = mem.mmap(0x1000, 0x1000, 'w')
@@ -238,7 +239,7 @@ class MemoryTest(unittest.TestCase):
self.assertRaises(MemoryException, mem.__setitem__, sym, val)
cs.add( sym.uge(0x1000))
mem[sym] = '\x40'
mem[sym] = val
@@ -336,7 +337,7 @@ class MemoryTest(unittest.TestCase):
def testBasicAnonMap(self):
m = AnonMap(0x10000000, 0x2000, 'rwx')
#Check the size
self.assertEqual(len(m), 0x2000)
@@ -370,7 +371,7 @@ class MemoryTest(unittest.TestCase):
def test_basic_get_char(self):
mem = SMemory32(ConstraintSet())
addr = mem.mmap(None, 0x10, 'rw')
mem[addr] = 'a'
mem[addr] = 'a'
mem[addr+0x10:addr+0x20] = 'Y'*0x10
self.assertItemsEqual(mem[addr+0x10-1:addr+0x20+1], '\x00' + 'Y'*0x10 +'\x00')
@@ -381,7 +382,7 @@ class MemoryTest(unittest.TestCase):
#start with no maps
self.assertEqual(len(mem.mappings()), 0)
#alloc/map a litlle mem
addr = mem.mmap(None, 0x10, 'r')
for c in xrange(0, 0x10):
@@ -509,7 +510,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr, size)
#Okay 0 maps
@@ -543,12 +544,12 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr+0x1000+0x1234, 0x1234)
'''
00000000f7ff0000-00000000f7ff2000 rwx 00000000
00000000f7ff4000-00000000f8000000 rwx 00000000
00000000f7ff0000-00000000f7ff2000 rwx 00000000
00000000f7ff4000-00000000f8000000 rwx 00000000
'''
#Okay 2 maps
@@ -584,7 +585,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr, size/2)
#Okay 1 maps
@@ -619,7 +620,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr+size/2, size)
#Okay 1 maps
@@ -651,7 +652,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr+size/3, size/3)
#Okay 2 maps
@@ -772,7 +773,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr-size/2, size)
#Okay 1 maps
self.assertEqual(len(mem.mappings()), 1)
@@ -802,7 +803,7 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr+size/2, size)
#limits
@@ -833,13 +834,13 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr, size/2)
#Okay 1 maps
self.assertEqual(len(mem.mappings()), 1)
#Okay unmap
#Okay unmap
mem.munmap(addr+size/2, size/2)
#Okay 1 maps
@@ -864,19 +865,19 @@ class MemoryTest(unittest.TestCase):
self.assertFalse(addr-1 in mem)
self.assertFalse(addr+size in mem)
#Okay unmap
#Okay unmap
mem.munmap(addr+size - size/3, size/2)
#Okay unmap
#Okay unmap
mem.munmap(addr - (size/2 - size/3), size/2)
#limits
self.assertTrue((addr+size - size/3 - 1) in mem )
self.assertFalse((addr+size - size/3) in mem )
self.assertFalse((addr - (size/2 - size/3) + size/2 - 1) in mem )
self.assertTrue((addr - (size/2 - size/3) + size/2) in mem )
self.assertFalse(addr in mem)
self.assertFalse(addr+size-1 in mem)
#Okay 1 maps
@@ -884,36 +885,36 @@ class MemoryTest(unittest.TestCase):
def test_mmapFile(self):
mem = SMemory32(ConstraintSet())
#start with no maps
self.assertEqual(len(mem.mappings()), 0)
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('a'*0x1001)
rwx_file.close()
addr_a = mem.mmapFile(0, 0x1000, 'rwx', rwx_file.name)
self.assertEqual(len(mem.mappings()), 1)
self.assertEqual(mem[addr_a], 'a')
self.assertEqual(mem[addr_a+(0x1000/2)], 'a')
self.assertEqual(mem[addr_a+(0x1000-1)], 'a')
self.assertRaises(MemoryException, mem.__getitem__, addr_a+(0x1000))
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('b'*0x1001)
rwx_file.close()
addr_b = mem.mmapFile(0, 0x1000, 'rw', rwx_file.name)
self.assertEqual(len(mem.mappings()), 2)
self.assertEqual(mem[addr_b], 'b')
self.assertEqual(mem[addr_b+(0x1000/2)], 'b')
self.assertEqual(mem[addr_b+(0x1000-1)], 'b')
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('c'*0x1001)
rwx_file.close()
@@ -921,41 +922,41 @@ class MemoryTest(unittest.TestCase):
addr_c = mem.mmapFile(0, 0x1000, 'rx', rwx_file.name)
self.assertEqual(len(mem.mappings()), 3)
self.assertEqual(mem[addr_c], 'c')
self.assertEqual(mem[addr_c+(0x1000/2)], 'c')
self.assertEqual(mem[addr_c+(0x1000-1)], 'c')
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('d'*0x1001)
rwx_file.close()
addr_d = mem.mmapFile(0, 0x1000, 'r', rwx_file.name)
self.assertEqual(len(mem.mappings()), 4)
self.assertEqual(mem[addr_d], 'd')
self.assertEqual(mem[addr_d+(0x1000/2)], 'd')
self.assertEqual(mem[addr_d+(0x1000-1)], 'd')
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('e'*0x1001)
rwx_file.close()
addr_e = mem.mmapFile(0, 0x1000, 'w', rwx_file.name)
self.assertEqual(len(mem.mappings()), 5)
self.assertRaises(MemoryException, mem.__getitem__, addr_e)
self.assertRaises(MemoryException, mem.__getitem__, addr_e+(0x1000/2))
self.assertRaises(MemoryException, mem.__getitem__, addr_e+(0x1000-1))
def test_basic_mapping_with_mmapFile(self):
mem = SMemory32(ConstraintSet())
#start with no maps
self.assertEqual(len(mem.mappings()), 0)
rwx_file = tempfile.NamedTemporaryFile('w+b', delete=False)
rwx_file.file.write('d'*0x1001)
rwx_file.close()
@@ -984,7 +985,7 @@ class MemoryTest(unittest.TestCase):
self.assertEqual(len(mem.mappings()), 1)
r_file = tempfile.NamedTemporaryFile('w+b', delete=False)
r_file.file.write('b'*0x1000)
r_file.close()
@@ -1006,17 +1007,17 @@ class MemoryTest(unittest.TestCase):
#Three mapping
self.assertEqual(len(mem.mappings()), 3)
size = 0x30000
w_file = tempfile.NamedTemporaryFile('w+b', delete=False)
w_file.file.write('abc'*(size/3))
w_file.close()
addr = mem.mmapFile(0x20000000, size, 'w', w_file.name)
#Four mapping
self.assertEqual(len(mem.mappings()), 4)
#Okay unmap
#Okay unmap
mem.munmap(addr+size/3, size/3)
#Okay 2 maps
@@ -1046,15 +1047,15 @@ class MemoryTest(unittest.TestCase):
#global mainsolver
cs = ConstraintSet()
mem = SMemory32(cs)
start_mapping_addr = mem.mmap(None, 0x1000, 'rwx')
concrete_addr = start_mapping_addr
symbolic_addr = start_mapping_addr+1
mem[concrete_addr] = 'C'
sym = cs.new_bitvec(8)
mem[symbolic_addr] = sym
cs.add(sym.uge(0xfe))
values = list(solver.get_all_values(cs, sym))
@@ -1068,7 +1069,7 @@ class MemoryTest(unittest.TestCase):
self.assertIn(0xfe, values)
self.assertIn(0xff, values)
self.assertNotIn(0x7f, values)
with cs as cs_temp:
cs_temp.add(sym==0xfe)
values = list(solver.get_all_values(cs_temp, sym))
@@ -1079,7 +1080,7 @@ class MemoryTest(unittest.TestCase):
self.assertIn(0xfe, values)
self.assertNotIn(0xff, values)
self.assertNotIn(0x7f, values)
values = list(solver.get_all_values(cs, sym))
self.assertIn(0xfe, values)
@@ -1093,15 +1094,15 @@ class MemoryTest(unittest.TestCase):
def test_mix_of_concrete_and_symbolic(self):
cs = ConstraintSet()
mem = SMemory32(cs)
start_mapping_addr = mem.mmap(None, 0x1000, 'rwx')
concretes = [0, 2, 4, 6]
symbolics = [1, 3, 5, 7]
for range in concretes:
mem[start_mapping_addr+range] = 'C'
for range in symbolics:
mem[start_mapping_addr+range] = cs.new_bitvec(8)
@@ -1110,16 +1111,16 @@ class MemoryTest(unittest.TestCase):
for range in concretes:
self.assertFalse(issymbolic(mem[start_mapping_addr+range]))
for range in symbolics:
self.assertTrue(issymbolic(mem[start_mapping_addr+range]))
self.assertTrue(issymbolic(mem[start_mapping_addr+range]))
for range in symbolics:
self.assertFalse(isconcrete(mem[start_mapping_addr+range]))
for range in symbolics:
mem[start_mapping_addr+range] = 'C'
for range in concretes:
mem[start_mapping_addr+range] = cs.new_bitvec(8)
@@ -1128,9 +1129,9 @@ class MemoryTest(unittest.TestCase):
for range in symbolics:
self.assertFalse(issymbolic(mem[start_mapping_addr+range]))
for range in concretes:
self.assertTrue(issymbolic(mem[start_mapping_addr+range]))
self.assertTrue(issymbolic(mem[start_mapping_addr+range]))
for range in concretes:
self.assertFalse(isconcrete(mem[start_mapping_addr+range]))
@@ -1139,29 +1140,29 @@ class MemoryTest(unittest.TestCase):
#global mainsolver
cs = ConstraintSet()
mem = SMemory32(cs)
addr_for_symbol1 = mem.mmap(None, 0x1000, 'rwx')
mem[addr_for_symbol1] = 'A'
symbol1 = cs.new_bitvec(8)
cs.add(Operators.OR(symbol1==Operators.ORD('B'), symbol1==Operators.ORD('C')))
mem[addr_for_symbol1+1] = symbol1
values = list(solver.get_all_values(cs, symbol1))
self.assertIn(Operators.ORD('B'), values)
self.assertIn(Operators.ORD('C'), values)
symbol2 = cs.new_bitvec(32)
cs.add(symbol2>=addr_for_symbol1)
cs.add(symbol2<=addr_for_symbol1+1)
c = mem[symbol2]
self.assertTrue(issymbolic(c))
self.assertTrue(issymbolic(c))
values = list(solver.get_all_values(cs, c))
self.assertIn(Operators.ORD('A'), values)
self.assertIn(Operators.ORD('B'), values)
self.assertIn(Operators.ORD('C'), values)
@@ -1183,7 +1184,7 @@ class MemoryTest(unittest.TestCase):
#make a free symbol of 32 bits
x = cs.new_bitvec(32)
x = cs.new_bitvec(32)
#constraint it to range into [addr, addr+10)
cs.add(x>=addr)
cs.add(x<addr+10)
@@ -1216,7 +1217,7 @@ class MemoryTest(unittest.TestCase):
cs.add(x<=addr)
#It shall be a solution
self.assertTrue(solver.check(cs))
#if we ask for a possible solution
#if we ask for a possible solution
sol = solver.get_value(cs, x)
#it must be addr
self.assertTrue(sol == addr)
@@ -1245,7 +1246,7 @@ class MemoryTest(unittest.TestCase):
mem[i] = Operators.CHR(100+i-addr)
#Make a char that ranges from 'A' to 'Z'
v = cs.new_bitvec(32)
v = cs.new_bitvec(32)
cs.add(v>=Operators.ORD('A'))
cs.add(v<=Operators.ORD('Z'))
@@ -1254,7 +1255,7 @@ class MemoryTest(unittest.TestCase):
#mak a free symbol of 32 bits
x = cs.new_bitvec(32)
x = cs.new_bitvec(32)
#constraint it to range into [addr, addr+10)
cs.add(x>=addr)
cs.add(x<addr+10)
@@ -1298,7 +1299,7 @@ class MemoryTest(unittest.TestCase):
#alloc/map a little mem
addr = mem.mmap(None, size, 'rwx')
#okay we should have 1 map
#okay we should have 1 map
self.assertEqual(len(mem.mappings()), 1)
#free middle page
@@ -1316,7 +1317,7 @@ class MemoryTest(unittest.TestCase):
self.assertEqual(mem[addr+0x2000], 'b')
#make a free symbol of 32 bits
x = cs.new_bitvec(32)
x = cs.new_bitvec(32)
#constraint it to range into [addr, addr+10)
cs.add(x>=addr)
cs.add(x<=addr+0x2000)
@@ -1498,7 +1499,7 @@ class MemoryTest(unittest.TestCase):
mem[addr_f] = sym
#save it
s = StringIO(pickle.dumps(mem))
#load it
tests/test_models.py
+1
View File
@@ -39,6 +39,7 @@ class ModelTest(unittest.TestCase):
class StrcmpTest(ModelTest):
_multiprocess_can_split_ = True
def _push2(self, s1, s2):
s1ptr = self._push_string(s1)
s2ptr = self._push_string(s2)
tests/test_register.py
+1
View File
@@ -4,6 +4,7 @@ from manticore.core.smtlib import Bool, BitVecConstant
from manticore.core.cpu.register import Register
class RegisterTest(unittest.TestCase):
_multiprocess_can_split_ = True
def test_rd(self):
r = Register(32)
self.assertEqual(r.read(), 0)
tests/test_signal.py
+2 -1
View File
@@ -9,6 +9,7 @@ class Sender(object):
self.sig2 = Signal()
class ManticoreDriver(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
self.state = {}
@@ -39,7 +40,7 @@ class ManticoreDriver(unittest.TestCase):
def test_method(self):
s = Sender()
s.sig += self.setReceived
s.sig('received', True)
self.assertEqual(self.state['received'], True)
tests/test_slam_regre.py
+518 -517
View File
File diff suppressed because it is too large Load Diff
tests/test_smtlibv2.py
+15 -14
View File
@@ -9,14 +9,15 @@ import sys
# level = logging.DEBUG)
class ExpressionTest(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
self.solver = Z3Solver()
def tearDown(self):
del self.solver
def testBasicAST_001(self):
''' Can't build abstract classes '''
@@ -45,7 +46,7 @@ class ExpressionTest(unittest.TestCase):
self.assertIsInstance(c, Expression)
self.assertTrue('SOURCE1' in c.taint)
self.assertTrue('SOURCE2' in c.taint)
def testBasicConstraints(self):
cs = ConstraintSet()
@@ -72,7 +73,7 @@ class ExpressionTest(unittest.TestCase):
cs = ConstraintSet()
#make array of 32->8 bits
array = cs.new_array(32)
#make free 32bit bitvector
#make free 32bit bitvector
key = cs.new_bitvec(32)
#assert that the array is 'A' at key position
@@ -84,13 +85,13 @@ class ExpressionTest(unittest.TestCase):
#1001 position of array can be 'A'
temp_cs.add(array[1001] == 'A')
self.assertTrue(self.solver.check(temp_cs))
with cs as temp_cs:
#1001 position of array can also be 'B'
temp_cs.add(array[1001] == 'B')
self.assertTrue(self.solver.check(temp_cs))
with cs as temp_cs:
#but if it is 'B' ...
temp_cs.add(array[1001] == 'B')
@@ -110,7 +111,7 @@ class ExpressionTest(unittest.TestCase):
cs = ConstraintSet()
#make array of 32->8 bits
array = cs.new_array(32, name=name)
#make free 32bit bitvector
#make free 32bit bitvector
key = cs.new_bitvec(32)
#assert that the array is 'A' at key position
@@ -147,7 +148,7 @@ class ExpressionTest(unittest.TestCase):
#make array of 32->8 bits
array = cs.new_array(32)
#make free 32bit bitvector
#make free 32bit bitvector
key = cs.new_bitvec(32)
#assert that the array is 'A' at key position
@@ -244,8 +245,8 @@ class ExpressionTest(unittest.TestCase):
x = BitVecConstant(32, 100, taint=('important',))
y = BitVecConstant(32, 200, taint=('stuff',))
z = constant_folder(x+y)
self.assertItemsEqual(z.taint, ('important', 'stuff'))
self.assertEqual(z.value, 300)
self.assertItemsEqual(z.taint, ('important', 'stuff'))
self.assertEqual(z.value, 300)
def test_arithmetic_simplifier(self):
cs = ConstraintSet()
@@ -265,7 +266,7 @@ class ExpressionTest(unittest.TestCase):
cs2 = ConstraintSet()
exp = cs2.new_bitvec(32)
exp |= 0
exp &= 1
exp &= 1
exp |= 0
self.assertEqual(get_depth(exp), 4)
self.assertEqual(translate_to_smtlib(exp), '(bvor (bvand (bvor V_1 #x00000000) #x00000001) #x00000000)')
@@ -414,7 +415,7 @@ class ExpressionTest(unittest.TestCase):
b = cs.new_bitvec(32)
c = cs.new_bitvec(32)
cs.add(c == Operators.SAR(32, a, b))
cs.add(c == Operators.SAR(32, a, b))
cs.add(a == A)
cs.add(b == B)
@@ -432,7 +433,7 @@ class ExpressionTest(unittest.TestCase):
#linear relation
#cs.add(x+y*5 == 0)
#Fork and divide in quadrants
#Fork and divide in quadrants
saved_up = None
saved_up_right = None
@@ -661,7 +662,7 @@ class ExpressionTest(unittest.TestCase):
import importlib
class Z3Test(unittest.TestCase):
def setUp(self):
#Manual mock for check_output
#Manual mock for check_output
self.module = importlib.import_module('manticore.core.smtlib.solver')
self.module.check_output = lambda *args, **kwargs: self.version
self.z3 = self.module.Z3Solver
tests/test_state.py
+9 -8
View File
@@ -36,6 +36,7 @@ class FakePlatform(object):
class StateTest(unittest.TestCase):
_multiprocess_can_split_ = True
def setUp(self):
l = linux.Linux('/bin/ls')
self.state = State(ConstraintSet(), l)
@@ -68,30 +69,30 @@ class StateTest(unittest.TestCase):
solved = self.state.concretize(expr, 'ONE')
self.assertEqual(len(solved), 1)
self.assertIn(solved[0], xrange(100))
def test_state(self):
constraints = ConstraintSet()
initial_state = State(constraints, FakePlatform())
arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA')
initial_state.constrain(arr[0] > 0x41)
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
with initial_state as new_state:
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(new_state.constraints.declarations) == 1 )
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(new_state.constraints.declarations) == 1 )
arrb = new_state.symbolicate_buffer('+'*100, label='SYMBB')
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(new_state.constraints.declarations) == 1 )
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(new_state.constraints.declarations) == 1 )
new_state.constrain(arrb[0] > 0x42)
self.assertTrue(len(new_state.constraints.declarations) == 2 )
self.assertTrue(len(new_state.constraints.declarations) == 2 )
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
def test_new_symbolic_buffer(self):
length = 64
tests/test_unicorn.py
+2 -1
View File
@@ -20,7 +20,7 @@ import logging
logger = logging.getLogger("ARM_TESTS")
__doc__ = '''
Test the Unicorn emulation stub. Armv7UnicornInstructions includes all
Test the Unicorn emulation stub. Armv7UnicornInstructions includes all
semantics from ARM tests to ensure that they match. UnicornConcretization tests
to make sure symbolic values get properly concretized.
'''
@@ -89,6 +89,7 @@ class Armv7UnicornInstructions(unittest.TestCase):
Import all of the tests from ARM, but execute with Unicorn to verify that
all semantics match.
'''
_multiprocess_can_split_ = True
def setUp(self):
self.cpu = Cpu(Memory32())
self.mem = self.cpu.memory