Use xmllint instead of java xml validator

Author: hannes-steffenhagen-diffblue

regression/validate-trace-xml-schema/CMakeLists.txt

@@ -1,11 +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 $<TARGET_FILE:cbmc>
-            WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR})
+      COMMAND ${PYTHON_EXECUTABLE} check.py $<TARGET_FILE:cbmc> ${XMLLINT}
+      WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR})
     set_tests_properties(validate-trace-xml-schema
-            PROPERTIES
-            LABELS "CBMC;CORE")
+      PROPERTIES
+      LABELS "CBMC;CORE")
+  endif()
 else()
     message(WARNING "Python >= 3.5 not found, skipping trace schema tests")
 endif()

regression/validate-trace-xml-schema/check.py

@@ -55,10 +55,12 @@
     'integer-assignments1/test.desc'
 ]))
 
-if len(sys.argv) != 2:
-    sys.stderr.write('Usage: check.py <path-to-cbmc>')
+# 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 <path-to-cbmc> <path-to-xmllint>')
 CbmcPath = os.path.abspath(sys.argv[1])
-XsdValidateJar = os.path.join(this_script_dir, 'validate-xsd/build/libs/validate-xsd-1.0-SNAPSHOT-uber.jar')
+XmlLintPath = os.path.abspath(sys.argv[2])
 
 
 class ChangeDir:
@@ -89,7 +91,8 @@ def __init__(self, total_specs):
 
     def check_spec(self, spec_path):
         self.total_test_count += 1
-        sys.stdout.write('*** Checking [{}/{}] {}... '.format(self.total_test_count, self.total_specs, spec_path))
+        sys.stdout.write('*** Checking [{}/{}] {}... '.format(
+            self.total_test_count, self.total_specs, spec_path))
         sys.stdout.flush()
         spec_dir = os.path.dirname(spec_path)
         spec = self.read_spec(spec_path)
@@ -113,17 +116,21 @@ def read_trace_into(self, trace_file, args):
                        stdout=trace_file)
 
     def check_trace(self, spec_path, trace_file):
-        validate_result = subprocess.run(['java', '-jar', XsdValidateJar, TraceXsdSpec],
+        validate_result = subprocess.run([XmlLintPath,
+                                          '--noout',  # we don't want it to print the XML we pipe in
+                                          '--schema', TraceXsdSpec,
+                                          '-'  # read from STDIN
+                                          ],
                                          stdin=trace_file,
                                          stdout=subprocess.PIPE,
                                          stderr=subprocess.PIPE)
         if validate_result.returncode == 0:
-            print('[SUCCESS]')
+            sys.stdout.buffer.write(b'[SUCCESS]\n')
         else:
-            print('[FAILURE]')
+            sys.stdout.buffer.write(b'[FAILURE]\n')
             self.failed_tests.append(spec_path)
-        sys.stdout.buffer.write(validate_result.stdout)
-        sys.stdout.buffer.write(validate_result.stderr)
+            sys.stdout.buffer.write(validate_result.stdout)
+            sys.stdout.buffer.write(validate_result.stderr)
 
     def read_spec(self, spec_path):
         with open(spec_path) as spec_file:
@@ -149,17 +156,6 @@ def report(self):
                 print(spec)
 
 
-def run_gradle(args):
-    with ChangeDir('validate-xsd'):
-        if os.name == 'nt':
-            subprocess.check_call(['cmd', '/c', 'gradlew.bat'] + args)
-        else:
-            subprocess.check_call(['./gradlew'] + args)
-
-
-# ensure that the uberjar exists and is up to date
-run_gradle(['uberjar'])
-
 test_desc_files = list(
     filter(lambda s: s not in ExcludedTests, glob.glob(os.path.join(test_base_dir, '*/*.desc'))))
 validator = Validator(total_specs=len(test_desc_files))

regression/validate-trace-xml-schema/check.sh

@@ -10,9 +10,9 @@ if [ $python_minor_version -lt 5 ]; then
     exit
 fi
 
-if ! command -v javac > /dev/null; then
-    echo "javac not found, skipping XSD tests"
-    exit
+xmllint="$(command -v xmllint)"
+if [ $? -ne 0 ] > /dev/null; then
+    echo "xmllint not found, skipping XSD tests"
 fi
 
-python3 check.py ../../src/cbmc/cbmc
+python3 check.py ../../src/cbmc/cbmc "$xmllint"