From cd578d9ad680d56e4fd67197a77cccf40c452558 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Mon, 23 Mar 2020 16:45:30 +0000 Subject: [PATCH] Add validation tests for trace XSD We have a XSD for cbmc --trace --xml-ui in our documentation, this adds a new test run which essentially validates the XML output of all tests in regression/cbmc against that XSD. Not all tests in there actually produce traces, but most do so we just exclude the few that don't. --- buildspec.yml | 2 +- regression/CMakeLists.txt | 1 + regression/Makefile | 3 +- .../validate-trace-xml-schema/CMakeLists.txt | 16 ++ regression/validate-trace-xml-schema/Makefile | 8 + regression/validate-trace-xml-schema/check.py | 166 ++++++++++++++++++ regression/validate-trace-xml-schema/check.sh | 18 ++ 7 files changed, 212 insertions(+), 2 deletions(-) create mode 100644 regression/validate-trace-xml-schema/CMakeLists.txt create mode 100644 regression/validate-trace-xml-schema/Makefile create mode 100644 regression/validate-trace-xml-schema/check.py create mode 100644 regression/validate-trace-xml-schema/check.sh diff --git a/buildspec.yml b/buildspec.yml index 3348cb54515..078896c1477 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -13,7 +13,7 @@ phases: commands: - sed -i 's#/archive.ubuntu.com#/us-east-1.ec2.archive.ubuntu.com#g' /etc/apt/sources.list - apt-get update -y - - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb + - apt-get install -y flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb libxml2-utils build: commands: - echo Build started on `date` diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index c33c86a0ca4..25e769ce941 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -55,6 +55,7 @@ add_subdirectory(goto-harness) add_subdirectory(goto-cc-file-local) add_subdirectory(linking-goto-binaries) add_subdirectory(symtab2gb) +add_subdirectory(validate-trace-xml-schema) if(WITH_MEMORY_ANALYZER) add_subdirectory(snapshot-harness) diff --git a/regression/Makefile b/regression/Makefile index c3096661e25..ab47a8c4917 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -32,7 +32,8 @@ DIRS = cbmc \ symtab2gb \ solver-hardness \ goto-ld \ - # Empty last line + validate-trace-xml-schema \ + # Empty last line ifeq ($(OS),Windows_NT) detected_OS := Windows diff --git a/regression/validate-trace-xml-schema/CMakeLists.txt b/regression/validate-trace-xml-schema/CMakeLists.txt new file mode 100644 index 00000000000..28d9a42de93 --- /dev/null +++ b/regression/validate-trace-xml-schema/CMakeLists.txt @@ -0,0 +1,16 @@ +find_package(PythonInterp 3.5) +if(${PYTHONINTERP_FOUND}) + find_program(XMLLINT xmllint) + if(NOT XMLLINT) + message(WARNING "xmllint not found, skipping trace schema tests") + else() + add_test(NAME validate-trace-xml-schema + COMMAND ${PYTHON_EXECUTABLE} check.py $ ${XMLLINT} + WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR}) + set_tests_properties(validate-trace-xml-schema + PROPERTIES + LABELS "CBMC;CORE") + endif() +else() + message(WARNING "Python >= 3.5 not found, skipping trace schema tests") +endif() diff --git a/regression/validate-trace-xml-schema/Makefile b/regression/validate-trace-xml-schema/Makefile new file mode 100644 index 00000000000..2512192bbec --- /dev/null +++ b/regression/validate-trace-xml-schema/Makefile @@ -0,0 +1,8 @@ +.PHONY: test +test: + sh check.sh +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log + diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py new file mode 100644 index 00000000000..eaec65c09c7 --- /dev/null +++ b/regression/validate-trace-xml-schema/check.py @@ -0,0 +1,166 @@ +import os +import subprocess +import sys +import tempfile +import glob + +this_script_dir = os.path.abspath(os.path.dirname(__file__)) + +TraceXsd = os.path.abspath(os.path.join(this_script_dir, '..', '..', 'doc/assets/xml_spec.xsd')) + +test_base_dir = os.path.abspath(os.path.join(this_script_dir, '..', 'cbmc')) + +# some tests in the cbmc suite don't work for the trace checks for one reason or another +ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s), [ + # these tests except input from stdin + 'json-interface1/test_wrong_option.desc', + 'json-interface1/test.desc', + 'json-interface1/test_wrong_flag.desc', + 'xml-interface1/test_wrong_option.desc', + 'xml-interface1/test.desc', + 'xml-interface1/test_wrong_flag.desc', + # these want --show-goto-functions instead of producing a trace + 'destructors/compound_literal.desc', + 'destructors/enter_lexical_block.desc', + 'reachability-slice-interproc2/test.desc', + # this one wants show-properties instead producing a trace + 'show_properties1/test.desc', + # program-only instead of trace + 'vla1/program-only.desc', + 'Quantifiers-simplify/simplify_not_forall.desc', + # this one doesn't work for me locally at all + # 'integer-assignments1/test.desc', + # these test for invalid command line handling + 'bad_option/test_multiple.desc', + 'bad_option/test.desc', + # this one produces XML intermingled with main XML output when used with --xml-ui + 'graphml_witness2/test.desc', + # produces intermingled XML on the command line + 'coverage_report1/test.desc', + 'coverage_report1/paths.desc', + 'graphml_witness1/test.desc', + 'switch8/program-only.desc', + # this uses json-ui (fails for a different reason actually, but should also + # fail because of command line incompatibility) + 'json1/test.desc', + # uses show-goto-functions + 'reachability-slice/test.desc', + 'reachability-slice/test2.desc', + 'reachability-slice/test3.desc', + 'reachability-slice-interproc/test.desc', + 'unsigned1/test.desc', + 'reachability-slice-interproc3/test.desc', + 'sync_lock_release-1/symbol_per_type.desc', + # this test is marked broken-smt-backend and doesn't work for me locally + 'integer-assignments1/test.desc' +])) + +# TODO maybe consider looking them up on PATH, but direct paths are +# harder to get wrong +if len(sys.argv) != 3: + sys.stderr.write('Usage: check.py ') +CbmcPath = os.path.abspath(sys.argv[1]) +XmlLintPath = os.path.abspath(sys.argv[2]) + + +class ChangeDir: + def __init__(self, change_to_wd): + self.current_wd = os.getcwd() + self.change_to_wd = change_to_wd + + def __enter__(self): + os.chdir(self.change_to_wd) + + def __exit__(self, _type, _value, _tb): + os.chdir(self.current_wd) + + +class TestSpec: + def __init__(self, args, is_knownbug, is_future, is_thorough): + self.args = args + self.is_knownbug = is_knownbug + self.is_future = is_future + self.is_thorough = is_thorough + + +class Validator: + def __init__(self, total_desc_count): + self.failed_tests = [] + self.total_desc_count = total_desc_count + self.checked_desc_count = 0 + + def check_test_desc(self, test_desc_path): + self.checked_desc_count += 1 + sys.stdout.write('*** Checking [{}/{}] {}... '.format( + self.checked_desc_count, self.total_desc_count, test_desc_path)) + sys.stdout.flush() + spec = self.read_spec(test_desc_path) + if spec.is_knownbug: + print('[Skipping KNOWNBUG]') + return + elif spec.is_future: + print('[Skipping FUTURE]') + return + elif spec.is_thorough: + print('[Skipping THOROUGH]') + return + test_desc_dir = os.path.dirname(test_desc_path) + with ChangeDir(test_desc_dir): + with tempfile.TemporaryFile() as trace_file: + self.read_trace_into(trace_file, spec.args) + trace_file.seek(0) + self.check_trace(test_desc_path, trace_file) + + def read_trace_into(self, trace_file, args): + subprocess.run([CbmcPath, '--trace', '--xml-ui'] + args, + stdout=trace_file) + + def check_trace(self, test_desc_path, trace_file): + validate_result = subprocess.run([XmlLintPath, + '--noout', # we don't want it to print the XML we pipe in + '--schema', TraceXsd, + '-' # read from STDIN + ], + stdin=trace_file, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE) + if validate_result.returncode == 0: + sys.stdout.buffer.write(b'[SUCCESS]\n') + else: + sys.stdout.buffer.write(b'[FAILURE]\n') + self.failed_tests.append(test_desc_path) + sys.stdout.buffer.write(validate_result.stdout) + sys.stdout.buffer.write(validate_result.stderr) + + def read_spec(self, test_desc_path): + with open(test_desc_path) as test_desc_file: + test_tags = test_desc_file.readline().split() + source_file = test_desc_file.readline().strip() + extra_args = test_desc_file.readline().split() + is_future = 'FUTURE' in test_tags + is_thorough = 'THOROUGH' in test_tags + is_knownbug = 'KNOWNBUG' in test_tags + return TestSpec(args=[source_file] + extra_args, + is_thorough=is_thorough, + is_future=is_future, + is_knownbug=is_knownbug) + + def has_failed_tests(self): + return len(self.failed_tests) > 0 + + def report(self): + print('{}/{} tests succeed'.format(self.checked_desc_count - len(self.failed_tests), self.checked_desc_count)) + if self.has_failed_tests(): + print('Failed tests:') + for spec in self.failed_tests: + print(spec) + + +test_desc_files = list( + filter(lambda s: s not in ExcludedTests, glob.glob(os.path.join(test_base_dir, '*/*.desc')))) +validator = Validator(total_desc_count=len(test_desc_files)) +for test_desc in test_desc_files: + validator.check_test_desc(test_desc) +validator.report() +if validator.has_failed_tests(): + sys.exit(1) diff --git a/regression/validate-trace-xml-schema/check.sh b/regression/validate-trace-xml-schema/check.sh new file mode 100644 index 00000000000..656a215b3e9 --- /dev/null +++ b/regression/validate-trace-xml-schema/check.sh @@ -0,0 +1,18 @@ +if ! command -v python3 > /dev/null; then + echo "python3 not found, skipping XSD tests" + exit +fi + +python_minor_version=$(python3 --version | cut -d ' ' -f 2 | cut -d '.' -f 2) + +if [ $python_minor_version -lt 5 ]; then + echo "python version less than 3.5, skipping XSD tests" + exit +fi + +xmllint="$(command -v xmllint)" +if [ $? -ne 0 ] > /dev/null; then + echo "xmllint not found, skipping XSD tests" +fi + +python3 check.py ../../src/cbmc/cbmc "$xmllint"