Skip to content

Implement parsing of hexadecimal Unicode characters from JSON #4590

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion src/json/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,15 @@ static std::string convert_TOK_STRING()
case 'r': result+='\r'; break;
case 't': result+='\t'; break;
case 'u':
{
// Character in hexadecimal Unicode representation, in the format
// \uABCD, i.e. the following four digits are part of this character.
assert(p + 4 < yyjsontext + len - 1);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggest p + 5 < yyjsontext + len would be better -- we're checking for 5-byte string uXXXX being in range, after all

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I found the current version to be clearer: when pointing to u, if you advance by four steps (pointing to the last hex character), then you have to still be to the left of the last " of the string. But I'm happy to change it in a follow-up PR if you think your version is more intuitive.

std::string hex(++p, 4);
result += std::stoi(hex, nullptr, 16);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this casts to a char (8-bit uint), so will only work for unicode characters <= 255

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is addressed in a follow-up PR: #4594

p += 3;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment that you're intentionally leaving p pointing to the last char of the escape

break;
}
default:; /* an error */
}
}
Expand Down
27 changes: 27 additions & 0 deletions unit/json/json_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -84,4 +84,31 @@ SCENARIO("Loading JSON files")
}
}
}
GIVEN("A JSON file containing a hexadecimal Unicode character")
{
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"
<< "}\n";
}
WHEN("Loading the JSON file with the special character")
{
jsont unicode_json;
const auto unicode_parse_error =
parse_json(unicode_json_path, null_message_handler, unicode_json);
THEN("The JSON file should be parsed correctly")
{
REQUIRE_FALSE(unicode_parse_error);
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");
}
}
}
}