Skip to content

Commit 3f8f315

Browse files
committed
Make all unicode operations use native endianness
We do not transfer data to another system, thus using architecture-native endianness is sufficient. Fixes: #2559
1 parent 37ab6e7 commit 3f8f315

File tree

10 files changed

+41
-102
lines changed

10 files changed

+41
-102
lines changed

jbmc/src/java_bytecode/expr2java.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -202,7 +202,7 @@ std::string expr2javat::convert_constant(
202202
if(to_integer(src, int_value))
203203
UNREACHABLE;
204204

205-
dest += "(char)'" + utf16_little_endian_to_java(int_value.to_long()) + '\'';
205+
dest += "(char)'" + utf16_native_endian_to_java(int_value.to_long()) + '\'';
206206
return dest;
207207
}
208208
else if(src.type()==java_byte_type())

jbmc/src/java_bytecode/java_string_literals.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ symbol_exprt get_or_create_string_literal_symbol(
106106
if(string_refinement_enabled)
107107
{
108108
const array_exprt data =
109-
utf16_to_array(utf8_to_utf16(id2string(value), false));
109+
utf16_to_array(utf8_to_utf16_native_endian(id2string(value)));
110110

111111
struct_exprt literal_init(new_symbol.type);
112112
literal_init.operands().resize(jls_struct.components().size());

src/ansi-c/literals/convert_string_literal.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ std::basic_string<unsigned int> convert_one_string_literal(
3434
unescape_wide_string(std::string(src, 3, src.size()-4));
3535

3636
// turn into utf-8
37-
std::string utf8_value=utf32_to_utf8(value);
37+
const std::string utf8_value = utf32_native_endian_to_utf8(value);
3838

3939
// pad into wide string
4040
value.resize(utf8_value.size());

src/ansi-c/literals/unescape_string.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ static void append_universal_char(
2323
std::basic_string<unsigned int> value_str(1, value);
2424

2525
// turn into utf-8
26-
std::string utf8_value=utf32_to_utf8(value_str);
26+
const std::string utf8_value = utf32_native_endian_to_utf8(value_str);
2727

2828
dest.append(utf8_value);
2929
}

src/ansi-c/scanner.l

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ int make_identifier()
6767
utf32+=letter;
6868

6969
// turn into utf-8
70-
std::string utf8_value=utf32_to_utf8(utf32);
70+
const std::string utf8_value = utf32_native_endian_to_utf8(utf32);
7171
final_base_name+=utf8_value;
7272
}
7373
else

src/solvers/refinement/string_constraint_generator_format.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -444,7 +444,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
444444
INVARIANT(!conversion_failed, "constant should be convertible to unsigned");
445445
out[i]=c;
446446
}
447-
return utf16_little_endian_to_java(out);
447+
return utf16_native_endian_to_java(out);
448448
}
449449

450450
/// Formatted string using a format string and list of arguments

src/util/file_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ void delete_directory_utf16(const std::wstring &path)
9595
void delete_directory(const std::string &path)
9696
{
9797
#ifdef _WIN32
98-
delete_directory_utf16(utf8_to_utf16_little_endian(path));
98+
delete_directory_utf16(utf8_to_utf16_native_endian(path));
9999
#else
100100
DIR *dir=opendir(path.c_str());
101101
if(dir!=nullptr)

src/util/unicode.cpp

Lines changed: 22 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,6 @@ Author: Daniel Kroening, [email protected]
1818
#include <windows.h>
1919
#endif
2020

21-
/// Determine endianness of the architecture
22-
/// \return True if the architecture is little_endian
23-
bool is_little_endian_arch()
24-
{
25-
uint32_t i=1;
26-
return reinterpret_cast<uint8_t &>(i) != 0;
27-
}
28-
2921
#define BUFSIZE 100
3022

3123
std::string narrow(const wchar_t *s)
@@ -138,9 +130,10 @@ static void utf8_append_code(unsigned int c, std::string &result)
138130
}
139131
}
140132

141-
/// \param utf32:encoded wide string
133+
/// \param s UTF-32 encoded wide string
142134
/// \return utf8-encoded string with the same unicode characters as the input.
143-
std::string utf32_to_utf8(const std::basic_string<unsigned int> &s)
135+
std::string
136+
utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s)
144137
{
145138
std::string result;
146139

@@ -166,52 +159,37 @@ std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide)
166159
return argv_narrow;
167160
}
168161

169-
/// A helper function for dealing with different UTF16 endians
170-
/// \par parameters: A 16-bit integer
171-
/// \return A 16-bit integer with bytes swapped
172-
uint16_t do_swap_bytes(uint16_t x)
173-
{
174-
const uint16_t b1 = x & 0xFFu;
175-
const uint16_t b2 = x & 0xFF00u;
176-
return static_cast<uint16_t>((b1 << 8) | (b2 >> 8));
177-
}
178-
179-
180-
void utf16_append_code(unsigned int code, bool swap_bytes, std::wstring &result)
162+
static void utf16_append_code(unsigned int code, std::wstring &result)
181163
{
182164
// we do not treat 0xD800 to 0xDFFF, although
183165
// they are not valid unicode symbols
184166

185167
if(code<0xFFFF)
186-
{ // code is encoded as one UTF16 character
187-
// we just take the code and possibly swap the bytes
188-
const unsigned int a =
189-
swap_bytes ? do_swap_bytes(static_cast<uint16_t>(code)) : code;
190-
result+=static_cast<wchar_t>(a);
168+
{
169+
// code is encoded as one UTF16 character
170+
result += static_cast<wchar_t>(code);
191171
}
192172
else // code is encoded as two UTF16 characters
193173
{
194174
// if this is valid unicode, we have
195175
// code<0x10FFFF
196176
// but let's not check it programmatically
197177

198-
// encode the code in UTF16, possibly swapping bytes.
178+
// encode the code in UTF16
199179
code=code-0x10000;
200180
const uint16_t i1 = static_cast<uint16_t>(((code >> 10) & 0x3ff) | 0xD800);
201-
const uint16_t a1 = swap_bytes ? do_swap_bytes(i1) : i1;
202-
result+=static_cast<wchar_t>(a1);
181+
result += static_cast<wchar_t>(i1);
203182
const uint16_t i2 = static_cast<uint16_t>((code & 0x3ff) | 0xDC00);
204-
const uint16_t a2 = swap_bytes ? do_swap_bytes(i2) : i2;
205-
result+=static_cast<wchar_t>(a2);
183+
result += static_cast<wchar_t>(i2);
206184
}
207185
}
208186

209187

210-
/// \par parameters: String in UTF-8 format, bool value indicating whether the
211-
/// endianness should be different from the architecture one.
188+
/// Convert UTF8-encoded string to UTF-16 with architecture-native endianness.
189+
/// \par parameters: String in UTF-8 format
212190
/// \return String in UTF-16 format. The encoding follows the endianness of the
213191
/// architecture iff swap_bytes is true.
214-
std::wstring utf8_to_utf16(const std::string& in, bool swap_bytes)
192+
std::wstring utf8_to_utf16_native_endian(const std::string &in)
215193
{
216194
std::wstring result;
217195
result.reserve(in.size());
@@ -264,33 +242,17 @@ std::wstring utf8_to_utf16(const std::string& in, bool swap_bytes)
264242
code=32;
265243
}
266244

267-
utf16_append_code(code, swap_bytes, result);
245+
utf16_append_code(code, result);
268246
}
269247

270248
return result;
271249
}
272250

273-
/// \par parameters: String in UTF-8 format
274-
/// \return String in UTF-16BE format
275-
std::wstring utf8_to_utf16_big_endian(const std::string &in)
276-
{
277-
bool swap_bytes=is_little_endian_arch();
278-
return utf8_to_utf16(in, swap_bytes);
279-
}
280-
281-
/// \par parameters: String in UTF-8 format
282-
/// \return String in UTF-16LE format
283-
std::wstring utf8_to_utf16_little_endian(const std::string &in)
284-
{
285-
bool swap_bytes=!is_little_endian_arch();
286-
return utf8_to_utf16(in, swap_bytes);
287-
}
288-
289-
/// \param ch: UTF-16LE character
251+
/// \param ch: UTF-16 character in architecture-native endianness encoding
290252
/// \param result: stream to receive string in US-ASCII format, with \\uxxxx
291253
/// escapes for other characters
292254
/// \param loc: locale to check for printable characters
293-
static void utf16_little_endian_to_java(
255+
static void utf16_native_endian_to_java(
294256
const wchar_t ch,
295257
std::ostringstream &result,
296258
const std::locale &loc)
@@ -327,23 +289,23 @@ static void utf16_little_endian_to_java(
327289
}
328290
}
329291

330-
/// \param ch: UTF-16LE character
292+
/// \param ch: UTF-16 character in architecture-native endianness encoding
331293
/// \return String in US-ASCII format, with \\uxxxx escapes for other characters
332-
std::string utf16_little_endian_to_java(const wchar_t ch)
294+
std::string utf16_native_endian_to_java(const wchar_t ch)
333295
{
334296
std::ostringstream result;
335297
const std::locale loc;
336-
utf16_little_endian_to_java(ch, result, loc);
298+
utf16_native_endian_to_java(ch, result, loc);
337299
return result.str();
338300
}
339301

340-
/// \param in: String in UTF-16LE format
302+
/// \param in: String in UTF-16 (native endianness) format
341303
/// \return String in US-ASCII format, with \\uxxxx escapes for other characters
342-
std::string utf16_little_endian_to_java(const std::wstring &in)
304+
std::string utf16_native_endian_to_java(const std::wstring &in)
343305
{
344306
std::ostringstream result;
345307
const std::locale loc;
346308
for(const auto ch : in)
347-
utf16_little_endian_to_java(ch, result, loc);
309+
utf16_native_endian_to_java(ch, result, loc);
348310
return result.str();
349311
}

src/util/unicode.h

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,12 @@ std::wstring widen(const char *s);
2222
std::string narrow(const std::wstring &s);
2323
std::wstring widen(const std::string &s);
2424

25-
std::string utf32_to_utf8(const std::basic_string<unsigned int> &s);
25+
std::string
26+
utf32_native_endian_to_utf8(const std::basic_string<unsigned int> &s);
2627

27-
std::wstring utf8_to_utf16(const std::string &in, bool swap_bytes);
28-
std::wstring utf8_to_utf16_big_endian(const std::string &);
29-
std::wstring utf8_to_utf16_little_endian(const std::string &);
30-
std::string utf16_little_endian_to_java(const wchar_t ch);
31-
std::string utf16_little_endian_to_java(const std::wstring &in);
28+
std::wstring utf8_to_utf16_native_endian(const std::string &in);
29+
std::string utf16_native_endian_to_java(const wchar_t ch);
30+
std::string utf16_native_endian_to_java(const std::wstring &in);
3231

3332
std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);
3433

unit/util/unicode.cpp

Lines changed: 7 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -53,65 +53,43 @@ static void wstr_print(const std::wstring &a, const std::wstring &b)
5353
}
5454
#endif
5555

56-
#if 0
57-
// big-endian test is broken, will be fixed in subsequent commit
58-
static bool compare_utf8_to_utf16_big_endian(const std::string &in)
56+
static bool compare_utf8_to_utf16(const std::string &in)
5957
{
60-
std::wstring s1=utf8_to_utf16_big_endian(in);
58+
const std::wstring s1 = utf8_to_utf16_native_endian(in);
6159

6260
typedef std::codecvt_utf8_utf16<wchar_t> codecvt_utf8_utf16t;
6361
std::wstring_convert<codecvt_utf8_utf16t> converter;
6462
std::wstring s2=converter.from_bytes(in);
6563

6664
return paranoid_wstr_equals(s1, s2);
6765
}
68-
#endif
69-
70-
static bool compare_utf8_to_utf16_little_endian(const std::string &in)
71-
{
72-
std::wstring s1=utf8_to_utf16_little_endian(in);
73-
74-
const std::codecvt_mode mode=std::codecvt_mode::little_endian;
75-
const unsigned long maxcode=0x10ffff;
76-
77-
typedef std::codecvt_utf8_utf16<wchar_t, maxcode, mode> codecvt_utf8_utf16t;
78-
std::wstring_convert<codecvt_utf8_utf16t> converter;
79-
std::wstring s2=converter.from_bytes(in);
80-
81-
return paranoid_wstr_equals(s1, s2);
82-
}
8366

8467
TEST_CASE("unicode0", "[core][util][unicode]")
8568
{
8669
const std::string s = u8"abc";
87-
// REQUIRE(compare_utf8_to_utf16_big_endian(s));
88-
REQUIRE(compare_utf8_to_utf16_little_endian(s));
70+
REQUIRE(compare_utf8_to_utf16(s));
8971
}
9072

9173
TEST_CASE("unicode1", "[core][util][unicode]")
9274
{
9375
const std::string s = u8"\u0070\u00DF\u00E0\u00EF\u00F0\u00F7\u00F8";
94-
// REQUIRE(compare_utf8_to_utf16_big_endian(s));
95-
REQUIRE(compare_utf8_to_utf16_little_endian(s));
76+
REQUIRE(compare_utf8_to_utf16(s));
9677
}
9778

9879
TEST_CASE("unicode2", "[core][util][unicode]")
9980
{
10081
const std::string s = u8"$¢€𐍈";
101-
// REQUIRE(compare_utf8_to_utf16_big_endian(s));
102-
REQUIRE(compare_utf8_to_utf16_little_endian(s));
82+
REQUIRE(compare_utf8_to_utf16(s));
10383
}
10484

10585
TEST_CASE("unicode3", "[core][util][unicode]")
10686
{
10787
const std::string s = u8"𐐏𤭢";
108-
// REQUIRE(compare_utf8_to_utf16_big_endian(s));
109-
REQUIRE(compare_utf8_to_utf16_little_endian(s));
88+
REQUIRE(compare_utf8_to_utf16(s));
11089
}
11190

11291
TEST_CASE("unicode4", "[core][util][unicode]")
11392
{
11493
const std::string s = u8"дȚȨɌṡʒʸͼἨѶݔݺ→⅒⅀▤▞╢◍⛳⻥龍ンㄗㄸ";
115-
// REQUIRE(compare_utf8_to_utf16_big_endian(s));
116-
REQUIRE(compare_utf8_to_utf16_little_endian(s));
94+
REQUIRE(compare_utf8_to_utf16(s));
11795
}

0 commit comments

Comments
 (0)