Skip to content

JSON equality operator #4912

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.

Sign up for GitHub

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 3 commits into from
Jul 17, 2019
Merged

JSON equality operator #4912

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6ed1c12
Add size property to json_objectt
Jul 16, 2019
799768e
JSON equality operator and tests
Jul 15, 2019
c70cbab
Remove linter braces rule
Jul 16, 2019
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
54 changes: 0 additions & 54 deletions scripts/cpplint.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3928,60 +3928,6 @@ def CheckBracesSpacing(filename, clean_lines, linenum, nesting_state, error):
"""
line = clean_lines.elided[linenum]

# Except after an opening paren, or after another opening brace (in case of
# an initializer list, for instance), you should have spaces before your
# braces when they are delimiting blocks, classes, namespaces etc.
# And since you should never have braces at the beginning of a line,
# this is an easy test. Except that braces used for initialization don't
# follow the same rule; we often don't want spaces before those.
match = Match(r'^(.*[^ ({>]){', line)

if match:
# Try a bit harder to check for brace initialization. This
# happens in one of the following forms:
# Constructor() : initializer_list_{} { ... }
# Constructor{}.MemberFunction()
# Type variable{};
# FunctionCall(type{}, ...);
# LastArgument(..., type{});
# LOG(INFO) << type{} << " ...";
# map_of_type[{...}] = ...;
# ternary = expr ? new type{} : nullptr;
# OuterTemplate<InnerTemplateConstructor<Type>{}>
#
# We check for the character following the closing brace, and
# silence the warning if it's one of those listed above, i.e.
# "{.;,)<>]:".
#
# To account for nested initializer list, we allow any number of
# closing braces up to "{;,)<". We can't simply silence the
# warning on first sight of closing brace, because that would
# cause false negatives for things that are not initializer lists.
# Silence this: But not this:
# Outer{ if (...) {
# Inner{...} if (...){ // Missing space before {
# }; }
#
# There is a false negative with this approach if people inserted
# spurious semicolons, e.g. "if (cond){};", but we will catch the
# spurious semicolon with a separate check.
leading_text = match.group(1)
(endline, endlinenum, endpos) = CloseExpression(
clean_lines, linenum, len(match.group(1)))
trailing_text = ''
if endpos > -1:
trailing_text = endline[endpos:]
for offset in xrange(endlinenum + 1,
min(endlinenum + 3, clean_lines.NumLines() - 1)):
trailing_text += clean_lines.elided[offset]
# We also suppress warnings for `uint64_t{expression}` etc., as the style
# guide recommends brace initialization for integral types to avoid
# overflow/truncation.
if (not Match(r'^[\s}]*[{.;,)<>\]:]', trailing_text)
and not _IsType(clean_lines, nesting_state, leading_text)):
error(filename, linenum, 'whitespace/braces', 5,
'Missing space before {')
Copy link
Collaborator

Choose a reason for hiding this comment

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

Maybe removing this is the right thing to do, but then we should remove all the code computing leading_text, trailing_text above. Or maybe you should just use NOLINTNEXTLINE(whitespace/braces) in the test.

Copy link
Contributor Author

@LAJW LAJW Jul 16, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

clang-format already checks for positions and spacing of curly braces and parentheses. The problem stems from the fact this isn't aware of initializer lists/uniform initialization.

std::vector<std::pair<int, int>>{{1, 2}, {3, 4}, {5, 6}};

In the days of C++98, the above wasn't a valid syntax. Curly braces would appear only after if /for statements, as block scopes or surround function bodies. The linter expects this to still be the case.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Ok, in which case the linter should be cleaned properly so as not to leave in place unused code.


# You shouldn't have a space before a semicolon at the end of the line.
# There's a special case for "for" since the style guide allows space before
# the semicolon there.
Expand Down
42 changes: 42 additions & 0 deletions src/util/json.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
#include "json.h"

#include <ostream>
#include <algorithm>

const jsont jsont::null_json_object(jsont::kindt::J_NULL);

Expand Down Expand Up @@ -162,3 +163,44 @@ void jsont::swap(jsont &other)
other.object.swap(object);
other.value.swap(value);
}

bool operator==(const jsont &left, const jsont &right)
{
if(left.kind != right.kind)
return false;
switch(left.kind)
{
case jsont::kindt::J_NULL:
return true;
case jsont::kindt::J_TRUE:
return true;
case jsont::kindt::J_FALSE:
return true;
case jsont::kindt::J_NUMBER:
return left.value == right.value;
case jsont::kindt::J_STRING:
return left.value == right.value;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Overall design question: shouldn't we do this more in a visitor-style where each call deriving from jsont defines each own operator== and the switch-case here would only do the downcasts and then invoke the more specific equality operators?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, except jsont much like irept doesn't allow any virtual functions. Therefore the visitor pattern is not applicable.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Of course, hence me saying "visitor-style." But also my comment was intended as a thought, not any kind of hard requirement.

case jsont::kindt::J_ARRAY:
{
const auto &left_array = static_cast<const json_arrayt &>(left);
Copy link
Contributor

Choose a reason for hiding this comment

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

ℹ️ There is a function called to_json_array at the bottom of this file, which you could re-use instead of adding your own static casts.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

static_cast is a feature of C++, and not "my" cast. to_json_array checks for kind, which in this case is already checked. We'd be doing extra work, so no.

const auto &right_array = static_cast<const json_arrayt &>(right);
return left_array.size() == right_array.size() &&
std::equal(
left_array.begin(), left_array.end(), right_array.begin());
}
case jsont::kindt::J_OBJECT:
{
const auto &left_object = static_cast<const json_objectt &>(left);
const auto &right_object = static_cast<const json_objectt &>(right);
if(left_object.size() != left_object.size())
return false;
return std::all_of(
left_object.begin(),
left_object.end(),
[&](const std::pair<std::string, jsont> &pair) {
return right_object[pair.first] == pair.second;
Copy link
Collaborator

Choose a reason for hiding this comment

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

That's an unnecessary lookup when instead you could just use two iterators over the two containers.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yeah, but if someone decides to swap std::map for std::unordered_map, it could be difficult to debug, so this is more stable/doesn't rely on any invariants.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I do wonder which containers would exhibit differences in strict equality testing? But I suppose it is conceivable that two std::unordered_map had their elements constructed in a different order, yet should compare equal. So, yes, keep it as is.

Copy link
Contributor

@smowton smowton Jul 16, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

Personally I still favour

// This relies on ordered maps:
static_assert(std::is_same<typeof(jsont::object), std::map<std::string, jsont>>::value)

});
}
}
UNREACHABLE;
}
7 changes: 7 additions & 0 deletions src/util/json.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,11 @@ class json_objectt:public jsont
return object.find(key);
}

std::size_t size() const
{
return object.size();
}

iterator begin()
{
return object.begin();
Expand Down Expand Up @@ -458,4 +463,6 @@ inline const json_stringt &to_json_string(const jsont &json)
return static_cast<const json_stringt &>(json);
}

bool operator==(const jsont &left, const jsont &right);

#endif // CPROVER_UTIL_JSON_H
107 changes: 107 additions & 0 deletions unit/json/json_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,3 +133,110 @@ SCENARIO("Loading JSON files")
}
}
}

TEST_CASE("json equality", "[core][util][json]")
{
SECTION("null")
{
REQUIRE(jsont::null_json_object == jsont::null_json_object);
}

SECTION("boolean")
{
REQUIRE(jsont::json_boolean(false) == jsont::json_boolean(false));
REQUIRE(jsont::json_boolean(true) == jsont::json_boolean(true));
REQUIRE_FALSE(jsont::json_boolean(true) == jsont::json_boolean(false));
REQUIRE_FALSE(jsont::json_boolean(false) == jsont::null_json_object);
}

SECTION("number")
{
REQUIRE(json_numbert("0") == json_numbert("0"));
REQUIRE(json_numbert("1") == json_numbert("1"));
REQUIRE(json_numbert("-1") == json_numbert("-1"));
REQUIRE(json_numbert("1.578") == json_numbert("1.578"));
REQUIRE_FALSE(json_numbert("0") == json_numbert("1"));
REQUIRE_FALSE(json_numbert("1") == json_numbert("-1"));
REQUIRE_FALSE(json_numbert("-1") == json_numbert("1"));
REQUIRE_FALSE(json_numbert("1.578") == json_numbert("1.5789"));
REQUIRE_FALSE(json_numbert("0") == jsont::json_boolean(false));
REQUIRE_FALSE(jsont::json_boolean(false) == json_numbert("0"));
REQUIRE_FALSE(json_numbert("0") == jsont::null_json_object);
REQUIRE_FALSE(jsont::null_json_object == json_numbert("0"));
}

SECTION("string")
{
REQUIRE(json_stringt("") == json_stringt(""));
REQUIRE(json_stringt("foo") == json_stringt("foo"));
REQUIRE(json_stringt("bar") == json_stringt("bar"));
REQUIRE_FALSE(json_stringt("foo") == json_stringt("bar"));
REQUIRE_FALSE(json_stringt("bar") == json_stringt("baz"));
REQUIRE_FALSE(json_stringt("foo") == json_stringt("food"));
REQUIRE_FALSE(json_stringt("1") == json_numbert("1"));
REQUIRE_FALSE(json_stringt("true") == jsont::json_boolean("true"));
REQUIRE_FALSE(json_stringt("") == jsont::json_boolean("false"));
REQUIRE_FALSE(json_stringt("") == jsont::null_json_object);
}

SECTION("array")
{
REQUIRE(json_arrayt{} == json_arrayt{});
REQUIRE(
json_arrayt{jsont::null_json_object} ==
json_arrayt{jsont::null_json_object});
REQUIRE(
json_arrayt{json_numbert{"9"}, json_numbert{"6"}} ==
json_arrayt{json_numbert{"9"}, json_numbert{"6"}});
REQUIRE(
json_arrayt{
json_stringt{"foo"}, json_stringt{"bar"}, json_stringt{"baz"}} ==
json_arrayt{
json_stringt{"foo"}, json_stringt{"bar"}, json_stringt{"baz"}});

// different lengths
REQUIRE_FALSE(
json_arrayt{json_stringt{"foo"}, json_stringt{"bar"}} ==
json_arrayt{
json_stringt{"foo"}, json_stringt{"bar"}, json_stringt{"baz"}});
// different elements
REQUIRE_FALSE(
json_arrayt{
json_stringt{"foo"}, json_stringt{"bar"}, json_stringt{"foo"}} ==
json_arrayt{
json_stringt{"foo"}, json_stringt{"bar"}, json_stringt{"baz"}});
// different kind
REQUIRE_FALSE(json_arrayt{} == jsont::json_boolean(false));
REQUIRE_FALSE(json_arrayt{} == jsont::null_json_object);
}

SECTION("object")
{
REQUIRE(json_objectt{} == json_objectt{});
REQUIRE(
json_objectt{{"key", json_stringt{"value"}}} ==
json_objectt{{"key", json_stringt{"value"}}});
REQUIRE(
json_objectt{{"key1", json_stringt{"value1"}},
{"key2", json_stringt{"value2"}}} ==
json_objectt{{"key1", json_stringt{"value1"}},
{"key2", json_stringt{"value2"}}});

// Extra property
REQUIRE_FALSE(
json_objectt{{"key1", json_stringt{"value1"}},
{"key2", json_stringt{"value2"}},
{"key3", json_stringt{"value3"}}} ==
json_objectt{{"key1", json_stringt{"value1"}},
{"key2", json_stringt{"value2"}}});
// different field values
REQUIRE_FALSE(
json_objectt{{"key1", json_stringt{"foo"}},
{"key2", json_stringt{"bar"}}} ==
json_objectt{{"key1", json_stringt{"foo"}},
{"key2", json_stringt{"baz"}}});
// different kind
REQUIRE_FALSE(json_objectt{} == json_arrayt{});
REQUIRE_FALSE(json_objectt{} == jsont::null_json_object);
}
}