Skip to content

Commit

Permalink
polishing for test-comp
Browse files Browse the repository at this point in the history
  • Loading branch information
mchalupa committed Feb 2, 2019
1 parent 14f3a9b commit 9bbfec9
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 110 deletions.
1 change: 1 addition & 0 deletions lib/symbioticpy/symbiotic/options.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ def __init__(self, env):
self.sources = []

self.tool_name = 'klee'
self.environment = env
self.is32bit = False
self.stats = False
self.generate_ll = False
Expand Down
121 changes: 22 additions & 99 deletions lib/symbioticpy/symbiotic/tools/klee_testcomp.py
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,15 @@

from . kleebase import SymbioticTool as KleeBase

from os import listdir
from os.path import join

def has_tests(working_dir):
for f in listdir(join(working_dir, 'klee-last')):
if f.endswith('.ktest'):
return True
return False

class SymbioticTool(KleeBase):
"""
Symbiotic tool info object
Expand All @@ -38,117 +47,31 @@ class SymbioticTool(KleeBase):
def __init__(self, opts):
KleeBase.__init__(self, opts)

# define and compile regular expressions for parsing klee's output
self._patterns = [
('ASSERTIONFAILED', re.compile('.*ASSERTION FAIL:.*')),
('ASSERTIONFAILED2', re.compile('.Assertion .* failed.*')),
('ESTPTIMEOUT', re.compile('.*query timed out (resolve).*')),
('EKLEETIMEOUT', re.compile('.*HaltTimer invoked.*')),
('EEXTENCALL', re.compile('.*failed external call.*')),
('ELOADSYM', re.compile('.*ERROR: unable to load symbol.*')),
('EINVALINST', re.compile('.*LLVM ERROR: Code generator does not support.*')),
('EINITVALS', re.compile('.*unable to compute initial values.*')),
('ESYMSOL', re.compile('.*unable to get symbolic solution.*')),
('ESILENTLYCONCRETIZED', re.compile('.*silently concretizing.*')),
('EEXTRAARGS', re.compile('.*calling .* with extra arguments.*')),
#('EABORT' , re.compile('.*abort failure.*')),
('EMALLOC', re.compile('.*found huge malloc, returning 0.*')),
('ESKIPFORK', re.compile('.*skipping fork.*')),
('EKILLSTATE', re.compile('.*killing.*states \(over memory cap\).*')),
('EMEMERROR', re.compile('.*memory error: out of bound pointer.*')),
('EMAKESYMBOLIC', re.compile(
'.*memory error: invalid pointer: make_symbolic.*')),
('EVECTORUNSUP', re.compile('.*XXX vector instructions unhandled.*')),
('EFREE', re.compile('.*memory error: invalid pointer: free.*')),
('EMEMALLOC', re.compile('.*KLEE: WARNING: Allocating memory failed.*')),
('EMEMLEAK', re.compile('.*memory error: memory leak detected.*')),
('EFREEALLOCA', re.compile('.*ERROR:.*free of alloca.*')),
('ERESOLV', re.compile('.*ERROR:.*Could not resolve.*'))
]

def actions_after_compilation(self, symbiotic):
if symbiotic.options.property.signedoverflow() and \
not symbiotic.options.overflow_with_clang:
symbiotic.link_undefined()


def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
"""
Compose the command line to execute from the name of the executable
"""

cmd = [executable, '-write-paths',
'-dump-states-on-halt=0', '-silent-klee-assume=1',
'-output-stats=0', '-disable-opt', '-only-output-states-covering-new=1',
'-max-time={0}'.format(self._options.timeout),
'-external-calls=none']
'-output-stats=0', '-disable-opt',
'-only-output-states-covering-new=1',
'-max-memory=7000000']

return cmd + options + tasks
if self._options.property.errorcall():
cmd.append('-exit-on-error-type=Assert')
cmd.append('-dump-states-on-halt=0')
else:
cmd.append('-max-time=840')

def _parse_klee_output_line(self, line):
for (key, pattern) in self._patterns:
if pattern.match(line):
# return True so that we know we should terminate
if key.startswith('ASSERTIONFAILED'):
return result.RESULT_FALSE_REACH
elif key == 'EFREE' or key == 'EFREEALLOCA':
return result.RESULT_FALSE_FREE
elif key == 'EMEMERROR':
return result.RESULT_FALSE_DEREF
elif key == 'EMEMLEAK':
if self._options.property.memcleanup():
return result.RESULT_FALSE_MEMCLEANUP
else:
return result.RESULT_FALSE_MEMTRACK
return key

return None
return cmd + options + tasks

def determine_result(self, returncode, returnsignal, output, isTimeout):
if isTimeout:
return 'timeout'

if output is None:
return 'ERROR (no output)'

found = []
for line in output:
fnd = self._parse_klee_output_line(line.decode('ascii'))
if fnd:
found.append(fnd)

if not found:
if returncode != 0:
return result.RESULT_ERROR
elif self._options.property.errorcall() or self._options.property.coverage():
return result.RESULT_DONE
else:
# we haven't found anything
return result.RESULT_TRUE_PROP
else:
if 'EINITVALS' in found: # EINITVALS would break the validity of the found error
return "{0}({1})".format(result.RESULT_UNKNOWN, " ".join(found))

for f in found:
# we found error that we sought for?
if f == result.RESULT_FALSE_REACH and self._options.property.assertions():
return f
elif f == result.RESULT_FALSE_OVERFLOW and self._options.property.signedoverflow():
return f
elif f in [result.RESULT_FALSE_FREE, result.RESULT_FALSE_DEREF, result.RESULT_FALSE_MEMTRACK]\
and self._options.property.memsafety():
return f
elif f == result.RESULT_FALSE_MEMCLEANUP and self._options.property.memcleanup():
return f
elif f == result.RESULT_FALSE_TERMINATION and self._options.property.termination():
return f
elif f == result.RESULT_FALSE_REACH and self._options.property.errorcall():
return result.RESULT_DONE
elif f == result.RESULT_FALSE_REACH and self._options.property.coverage():
return result.RESULT_DONE



return "{0}({1})".format(result.RESULT_UNKNOWN, " ".join(found))

return result.RESULT_ERROR
if has_tests(self._options.environment.working_dir):
return result.RESULT_DONE

return result.RESULT_UNKNOWN
11 changes: 0 additions & 11 deletions lib/symbioticpy/symbiotic/tools/kleebase.py
Original file line number Diff line number Diff line change
Expand Up @@ -162,11 +162,6 @@ def passes_after_compilation(self):

return passes

def actions_after_compilation(self, symbiotic):
if not symbiotic.check_llvmfile(symbiotic.llvmfile, '-check-concurr'):
from symbiotic.exceptions import SymbioticExceptionalResult as Result
raise Result('unknown (unsupported call (pthread API)')

def passes_after_slicing(self):
"""
Prepare the bitcode for verification after slicing:
Expand Down Expand Up @@ -201,12 +196,6 @@ def passes_before_verification(self):

return passes

def actions_before_verification(self, symbiotic):
if not symbiotic.check_llvmfile(symbiotic.llvmfile):
dbg('Unsupported call (probably floating handling)')
from symbiotic.exceptions import SymbioticExceptionalResult as Result
raise Result('unknown (call to unsupported function)')

def describe_error(self, llvmfile):
dump_error(dirname(llvmfile), self._options.property.memsafety())

0 comments on commit 9bbfec9

Please sign in to comment.