Fix XML rendering crash with non-printable characters

Replace DATA_INVARIANT crash with proper escaping when non-printable
characters appear in XML output. Characters valid in XML 1.0 (TAB, LF,
CR) use numeric character references (e.g., 	). Characters invalid
in XML 1.0 (null, other control chars, DEL) use C-style escape
sequences (\0, \xNN). Backslashes are escaped as \\ to avoid
ambiguity.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc/xml-nonprintable-chars/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main(void)
+{
+  const unsigned char *str = (unsigned char *)"\x00";
+  assert(*str == '\x01');
+  return 0;
+}

regression/cbmc/xml-nonprintable-chars/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--trace --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+XML does not support escaping non-printable character
+--
+Test that cbmc with --trace --xml-ui handles non-printable characters
+gracefully without crashing when they appear in counterexample traces.
+This test verifies that the fix for character 0x01 allows XML generation
+to complete successfully by using numeric character references.

src/util/xml.cpp

@@ -101,17 +101,34 @@ void xmlt::escape(const std::string &s, std::ostream &out)
       out << '\n';
       break;
 
-    case 0x9:  // TAB
-    case 0x7F: // DEL
+    case 0x9: // TAB
       out << "&#" << std::to_string((unsigned char)ch) << ';';
       break;
 
+    case 0x7F: // DEL
+      out << "\\x7f";
+      break;
+
     default:
-      DATA_INVARIANT(
-        static_cast<unsigned char>(ch) >= 32u,
-        "XML does not support escaping non-printable character " +
-          std::to_string((unsigned char)ch));
-      out << ch;
+      // Non-printable characters below 0x20 (other than TAB, LF, CR which
+      // are handled above) are not valid in XML 1.0, not even as numeric
+      // character references. Encode them as C-style escape sequences.
+      if(static_cast<unsigned char>(ch) < 32u)
+      {
+        if(ch == '\0')
+          out << "\\0";
+        else
+          out << "\\x" << std::hex << (unsigned int)(unsigned char)ch
+              << std::dec;
+      }
+      else if(ch == '\\')
+      {
+        out << "\\\\";
+      }
+      else
+      {
+        out << ch;
+      }
     }
   }
 }
@@ -143,16 +160,33 @@ void xmlt::escape_attribute(const std::string &s, std::ostream &out)
     case 0x9:  // TAB
     case 0xA:  // LF
     case 0xD:  // CR
-    case 0x7F: // DEL
       out << "&#" << std::to_string((unsigned char)ch) << ';';
       break;
 
+    case 0x7F: // DEL
+      out << "\\x7f";
+      break;
+
     default:
-      DATA_INVARIANT(
-        static_cast<unsigned char>(ch) >= 32u,
-        "XML does not support escaping non-printable character " +
-          std::to_string((unsigned char)ch));
-      out << ch;
+      // Non-printable characters below 0x20 (other than TAB, LF, CR which
+      // are handled above) are not valid in XML 1.0, not even as numeric
+      // character references. Encode them as C-style escape sequences.
+      if(static_cast<unsigned char>(ch) < 32u)
+      {
+        if(ch == '\0')
+          out << "\\0";
+        else
+          out << "\\x" << std::hex << (unsigned int)(unsigned char)ch
+              << std::dec;
+      }
+      else if(ch == '\\')
+      {
+        out << "\\\\";
+      }
+      else
+      {
+        out << ch;
+      }
     }
   }
 }

unit/util/xml.cpp

@@ -6,9 +6,12 @@ Author: Thomas Kiley
 
 \*******************************************************************/
 
-#include <testing-utils/use_catch.h>
 #include <util/xml.h>
 
+#include <testing-utils/use_catch.h>
+
+#include <sstream>
+
 TEST_CASE("xml_equal", "[core][util][xml]")
 {
   SECTION("Empty xml")
@@ -97,3 +100,75 @@ TEST_CASE("xml_equal", "[core][util][xml]")
     }
   }
 }
+
+TEST_CASE("xml_escape_nonprintable", "[core][util][xml]")
+{
+  SECTION("Escaping non-printable characters in attributes")
+  {
+    xmlt node{"test"};
+    node.set_attribute("value", std::string("\x00\x01\x02\x1F", 4));
+
+    std::ostringstream out;
+    node.output(out);
+
+    std::string result = out.str();
+    // Characters invalid in XML 1.0 are encoded as C-style escapes
+    REQUIRE(result.find("\\0") != std::string::npos);
+    REQUIRE(result.find("\\x1") != std::string::npos);
+    REQUIRE(result.find("\\x2") != std::string::npos);
+    REQUIRE(result.find("\\x1f") != std::string::npos);
+  }
+
+  SECTION("Escaping non-printable characters in data")
+  {
+    xmlt node{"test"};
+    node.data = std::string("\x00\x01\x02\x1F", 4);
+
+    std::ostringstream out;
+    node.output(out);
+
+    std::string result = out.str();
+    // Characters invalid in XML 1.0 are encoded as C-style escapes
+    REQUIRE(result.find("\\0") != std::string::npos);
+    REQUIRE(result.find("\\x1") != std::string::npos);
+    REQUIRE(result.find("\\x2") != std::string::npos);
+    REQUIRE(result.find("\\x1f") != std::string::npos);
+  }
+
+  SECTION("Valid XML 1.0 control characters use numeric references")
+  {
+    xmlt node{"test"};
+    node.set_attribute("value", std::string("\x09", 1));
+
+    std::ostringstream out;
+    node.output(out);
+
+    std::string result = out.str();
+    // TAB is valid in XML 1.0 and uses numeric character reference
+    REQUIRE(result.find("&#9;") != std::string::npos);
+  }
+
+  SECTION("Backslashes are escaped")
+  {
+    xmlt node{"test"};
+    node.set_attribute("value", "back\\slash");
+
+    std::ostringstream out;
+    node.output(out);
+
+    std::string result = out.str();
+    REQUIRE(result.find("back\\\\slash") != std::string::npos);
+  }
+
+  SECTION("Standard printable characters unchanged")
+  {
+    xmlt node{"test"};
+    node.set_attribute("value", "Hello World!");
+
+    std::ostringstream out;
+    node.output(out);
+
+    std::string result = out.str();
+    REQUIRE(result.find("Hello World!") != std::string::npos);
+  }
+}