Add support for UTF-16 in the JSON parser

The previous implementation only supported UTF-8 (up to \u007F) as
characters, and all remaining characters up to \u00FF as integers.
The new implementation supports all UTF-16 (single) characters.

Author: antlechner

src/json/parser.y

@@ -18,6 +18,8 @@
 %{
 #include "json_parser.h"
 
+#include <util/unicode.h>
+
 int yyjsonlex();
 extern char *yyjsontext;
 extern int yyjsonleng; // really an int, not a size_t
@@ -51,7 +53,7 @@ static std::string convert_TOK_STRING()
         // \uABCD, i.e. the following four digits are part of this character.
         assert(p + 4 < yyjsontext + len - 1);
         std::string hex(++p, 4);
-        result += std::stoi(hex, nullptr, 16);
+        result += utf16_hex_to_utf8(hex);
         p += 3;
         break;
       }

src/util/unicode.cpp

@@ -8,11 +8,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "unicode.h"
 
+#include <codecvt>
+#include <cstdint>
 #include <cstring>
-#include <locale>
 #include <iomanip>
+#include <locale>
 #include <sstream>
-#include <cstdint>
+
+#include "invariant.h"
 
 #ifdef _WIN32
 #include <util/pragma_push.def>
@@ -315,3 +318,12 @@ std::string utf16_native_endian_to_java(const std::wstring &in)
     utf16_native_endian_to_java(ch, result, loc);
   return result.str();
 }
+
+std::string utf16_hex_to_utf8(const std::string &hex)
+{
+  PRECONDITION(hex.length() == 4);
+  const char16_t utf16_char = std::strtol(hex.c_str(), nullptr, 16);
+  const std::u16string u16(1, utf16_char);
+  return std::wstring_convert<std::codecvt_utf8_utf16<char16_t>, char16_t>{}
+    .to_bytes(u16);
+}

src/util/unicode.h

@@ -31,6 +31,11 @@ std::string utf16_native_endian_to_java(const std::wstring &in);
 
 std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);
 
+/// \param hex: a representation of a UTF-16 character as a four-digit string
+///   (e.g.\ "0041" for \u0041)
+/// \return the UTF-8 encoding of the character.
+std::string utf16_hex_to_utf8(const std::string &hex);
+
 template <typename It>
 std::vector<const char *> to_c_str_array(It b, It e)
 {

unit/json/json_parser.cpp

@@ -84,17 +84,21 @@ SCENARIO("Loading JSON files")
       }
     }
   }
-  GIVEN("A JSON file containing a hexadecimal Unicode character")
+  GIVEN("A JSON file containing hexadecimal Unicode characters")
   {
     temporary_filet unicode_json_file("cbmc_unit_json_parser_unicode", ".json");
     const std::string unicode_json_path = unicode_json_file();
     {
       std::ofstream unicode_json_out(unicode_json_path);
       unicode_json_out << "{\n"
-                       << "  \"special character\": \"\\u0001\"\n"
+                       << "  \"one\": \"\\u0001\",\n"
+                       << "  \"latin\": \"\\u0042\",\n"
+                       << "  \"grave\": \"\\u00E0\",\n"
+                       << "  \"trema\": \"\\u00FF\",\n"
+                       << "  \"high\": \"\\uFFFF\"\n"
                        << "}\n";
     }
-    WHEN("Loading the JSON file with the special character")
+    WHEN("Loading the JSON file with the special characters")
     {
       jsont unicode_json;
       const auto unicode_parse_error =
@@ -105,9 +109,22 @@ SCENARIO("Loading JSON files")
         REQUIRE(unicode_json.is_object());
 
         const json_objectt &json_object = to_json_object(unicode_json);
-        REQUIRE(json_object.find("special character") != json_object.end());
-        REQUIRE(json_object["special character"].value.size() == 1);
-        REQUIRE(json_object["special character"].value == "\u0001");
+
+        REQUIRE(json_object.find("one") != json_object.end());
+        REQUIRE(json_object["one"].value.size() == 1);
+        REQUIRE(json_object["one"].value == "\u0001");
+
+        REQUIRE(json_object.find("latin") != json_object.end());
+        REQUIRE(json_object["latin"].value == "B");
+
+        REQUIRE(json_object.find("grave") != json_object.end());
+        REQUIRE(json_object["grave"].value == "à");
+
+        REQUIRE(json_object.find("trema") != json_object.end());
+        REQUIRE(json_object["trema"].value == "ÿ");
+
+        REQUIRE(json_object.find("high") != json_object.end());
+        REQUIRE(json_object["high"].value == "\uFFFF");
       }
     }
   }