Skip to content

Commit 18f0b44

Browse files
committed
Fix XML rendering crash with non-printable characters
Handle non-printable characters in XML attributes by escaping them as numeric character references instead of aborting. Co-authored-by: Kiro autonomous agent Fixes: #7073
1 parent 76dd20f commit 18f0b44

4 files changed

Lines changed: 90 additions & 11 deletions

File tree

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include <assert.h>
2+
3+
int main(void)
4+
{
5+
const unsigned char *str = (unsigned char *)"\x00";
6+
assert(*str == '\x01');
7+
return 0;
8+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--trace --xml-ui
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
VERIFICATION FAILED
7+
--
8+
XML does not support escaping non-printable character
9+
--
10+
Test that cbmc with --trace --xml-ui handles non-printable characters
11+
gracefully without crashing when they appear in counterexample traces.
12+
This test verifies that the fix for character 0x01 allows XML generation
13+
to complete successfully by using numeric character references.

src/util/xml.cpp

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -107,11 +107,16 @@ void xmlt::escape(const std::string &s, std::ostream &out)
107107
break;
108108

109109
default:
110-
DATA_INVARIANT(
111-
static_cast<unsigned char>(ch) >= 32u,
112-
"XML does not support escaping non-printable character " +
113-
std::to_string((unsigned char)ch));
114-
out << ch;
110+
// Handle non-printable characters by escaping them as numeric character
111+
// references instead of crashing
112+
if(static_cast<unsigned char>(ch) < 32u)
113+
{
114+
out << "&#" << std::to_string((unsigned char)ch) << ';';
115+
}
116+
else
117+
{
118+
out << ch;
119+
}
115120
}
116121
}
117122
}
@@ -148,11 +153,16 @@ void xmlt::escape_attribute(const std::string &s, std::ostream &out)
148153
break;
149154

150155
default:
151-
DATA_INVARIANT(
152-
static_cast<unsigned char>(ch) >= 32u,
153-
"XML does not support escaping non-printable character " +
154-
std::to_string((unsigned char)ch));
155-
out << ch;
156+
// Handle non-printable characters by escaping them as numeric character
157+
// references instead of crashing
158+
if(static_cast<unsigned char>(ch) < 32u)
159+
{
160+
out << "&#" << std::to_string((unsigned char)ch) << ';';
161+
}
162+
else
163+
{
164+
out << ch;
165+
}
156166
}
157167
}
158168
}

unit/util/xml.cpp

Lines changed: 49 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,12 @@ Author: Thomas Kiley
66
77
\*******************************************************************/
88

9-
#include <testing-utils/use_catch.h>
109
#include <util/xml.h>
1110

11+
#include <testing-utils/use_catch.h>
12+
13+
#include <sstream>
14+
1215
TEST_CASE("xml_equal", "[core][util][xml]")
1316
{
1417
SECTION("Empty xml")
@@ -97,3 +100,48 @@ TEST_CASE("xml_equal", "[core][util][xml]")
97100
}
98101
}
99102
}
103+
104+
TEST_CASE("xml_escape_nonprintable", "[core][util][xml]")
105+
{
106+
SECTION("Escaping non-printable characters in attributes")
107+
{
108+
xmlt node{"test"};
109+
node.set_attribute("value", std::string("\x01\x02\x1F", 3));
110+
111+
std::ostringstream out;
112+
node.output(out);
113+
114+
std::string result = out.str();
115+
// Should contain numeric character references for non-printable chars
116+
REQUIRE(result.find("&#1;") != std::string::npos);
117+
REQUIRE(result.find("&#2;") != std::string::npos);
118+
REQUIRE(result.find("&#31;") != std::string::npos);
119+
}
120+
121+
SECTION("Escaping non-printable characters in data")
122+
{
123+
xmlt node{"test"};
124+
node.data = std::string("\x01\x02\x1F", 3);
125+
126+
std::ostringstream out;
127+
node.output(out);
128+
129+
std::string result = out.str();
130+
// Should contain numeric character references for non-printable chars
131+
REQUIRE(result.find("&#1;") != std::string::npos);
132+
REQUIRE(result.find("&#2;") != std::string::npos);
133+
REQUIRE(result.find("&#31;") != std::string::npos);
134+
}
135+
136+
SECTION("Standard printable characters unchanged")
137+
{
138+
xmlt node{"test"};
139+
node.set_attribute("value", "Hello World!");
140+
141+
std::ostringstream out;
142+
node.output(out);
143+
144+
std::string result = out.str();
145+
REQUIRE(result.find("Hello World!") != std::string::npos);
146+
}
147+
}

0 commit comments

Comments
 (0)