Add improved functionality for the construction of json_arrayt and json_objectt #3862

thomasspriggs · 2019-01-20T21:37:19Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Much of the existing code which constructs instances of json_arrayt and json_objectt are based around creating an empty instance as then mutating it to add the contained information. This PR adds extra functionality to enable these two types to be constructed using a coding style which no longer requires mutation and is more readable.

tautschnig · 2019-01-20T23:03:22Z

src/util/json.h

@@ -283,6 +283,12 @@ class json_objectt:public jsont
  {
  }

+  explicit json_objectt(
+    std::initializer_list<typename objectt::value_type> initializer_list)
+    : json_objectt{objectt{initializer_list}}


Thank you for this further improvement! I suspect it's kind of a painful ask, but would you mind adding a commit that now removes the outermost parentheses from various bits touched in 64df79e?

tautschnig · 2019-01-20T23:07:41Z

src/goto-analyzer/static_verifier.cpp

@@ -16,52 +16,47 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/goto_model.h>

 #include <analyses/ai.h>
+#include <util/range.h>


Please move this 5 lines up so that it becomes part of the util block.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 55051ea).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97979428

tautschnig

Thank you for the extra work!

kroening · 2019-01-21T08:53:58Z

Does this work with Visual Studio 2013?

thomasspriggs · 2019-01-21T10:13:59Z

@kroening I wrote this PR under Debian 9 "Stretch" using gcc 6. So I haven't tried building in VS 2013 myself. However the windows CI build has passed.

thk123

Love it.

thk123 · 2019-01-21T12:14:19Z

src/util/range.h

+  /// Constructs a collection containing the values, which this range iterates
+  /// over.
+  template <typename containert>
+  containert collect() const


thk123 · 2019-01-21T12:15:19Z

src/util/constructor_of.h

+
+/// A type of functor which wraps around the set of constructors of a type.
+/// \tparam constructedt: The type which this functor constructs.
+template <typename constructedt>


❓ What is the use of this? Currently only used in the unit test so was thinking it should live there, but of course if it has general utility then here is fine

Is used in a later commit.

thk123 · 2019-01-21T12:17:07Z

src/util/range.h

@@ -359,6 +359,12 @@ struct ranget final
    return containert(begin(), end());
  }

+  template <typename containert>


thomasspriggs · 2019-01-21T13:43:23Z

@kroening Do you want any additional checks done around visual studio 2013 compatibility? CI passing + reviewer approval would normally be considered to be sufficient. Given that the new code is both unit tested and used, there should have been compile errors, or failing tests if any issues were introduced.

This PR now touches a wide range of directories, due to the bracket removal requested by Michael Tautschnig. Which means that it seems to require review from a unknown number of reviewers. It would save time if you would merge this.

smowton · 2019-01-21T14:40:50Z

src/goto-analyzer/static_verifier.cpp

  // clang-format on
  source_locationt source_location;
  irep_idt function_id;
 };

+/// Makes a status message string from a status.
+static std::string message(const static_verifier_resultt::statust &status)


Suggest const char * since this only ever returns constants (no need to bind our caller to necessarily go through std::string)

smowton · 2019-01-21T14:41:46Z

src/goto-analyzer/unreachable_instructions.cpp

@@ -152,8 +152,8 @@ static void add_to_json(

    // print info for file actually with full path
    const source_locationt &l=it->second->source_location;
-    json_objectt i_entry(
-      {{"sourceLocation", json(l)}, {"statement", json_stringt(s)}});
+    json_objectt i_entry{{"sourceLocation", json(l)},


Surprising formatting -- break after first {?

If I insert a new line, then clang format will just remove it again. I agree that left alignment of the enclosed pairs would be preferable. However I prefer the sub optimal formatting over the extra comments to switch off the formatting in this case.

smowton · 2019-01-21T14:42:12Z

src/goto-programs/json_expr.cpp

@@ -172,8 +172,8 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
      to_struct_type(type).components();
    for(const auto &component : components)
    {
-      json_objectt e({{"name", json_stringt(component.get_name())},
-                      {"type", json(component.type(), ns, mode)}});
+      json_objectt e{{"name", json_stringt(component.get_name())},


Same formatting nitpick as above

smowton · 2019-01-21T14:45:00Z

src/util/json.h

+  {
+  }
+
+  template <typename begin_iteratort, typename end_iteratort>


Surely these have to be the same type?

Forwarding these parameters separately means that the template can match when the two iterators have different const or reference qualifiers. For example .begin() on a range returns a mutable instance of the iterator by value, whereas the .end() on a range returns a const reference to the end iterator.
I will however add a static_assert to these constructors, in order to give a sensible error message if the types of the iterators are different once any const or reference modifiers are removed.

smowton · 2019-01-21T14:47:57Z

src/util/options.cpp

@@ -90,14 +92,12 @@ const optionst::value_listt &optionst::get_list_option(
 /// Returns the options as JSON key value pairs


Worth noting this is now lazy, so calling this then mutating optionst then trying to iterate over the range may be undefined behaviour

Please note that the return type of the function is still a value of type json_objectt, not a range. So there is no laziness beyond the scope of this function.

@thomasspriggs might be worth adding an explicit constructor call to make that more obvious?

smowton

(notes above, meant to approve)

kroening · 2019-01-21T18:11:02Z

@thomasspriggs The CI uses 2015, so may still fail with 2013.
I can try tomorrow.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: a8b278c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98067771
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a859b17).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98072678

thomasspriggs · 2019-01-21T22:02:50Z

@kroening I have made a cursory attempt at compiling cbmc develop with visual studio 2013. This resulted in numerous build errors. Some of these were likely to be due to not having my build environment correctly setup. However a substantial number of these appear to be existing compatibility issues.

kroening · 2019-01-22T13:24:28Z

This doesn't compile with VS 2013.
I.e., merging this requires ditching this target.

thomasspriggs · 2019-01-22T13:28:37Z

Can you compile develop with VS 2013? If you can't, then VS 2013 support has already been lost without this PR.

Upgrading to VS2015 enables #3862, noexcept (e.g. #2502), UTF8 strings and constexpr (#2133).

This new constructor facilitates the construction of instances of `json_objectt` which are const, because it gives a tidy way to construct an entire `json_objectt`.

thomasspriggs · 2019-01-28T16:54:17Z

I have pushed two rebases to

Rename constructort to constructor_oft to avoid naming conflicts.
Rebase on develop. Resolving a merge conflict in the process.

This new constructor facilitates the construction of instances of `json_arrayt` which are const, because it gives a tidy way to construct an entire `json_arrayt`.

The end result of this commit is that code like the following example can be used to construct `json_arrayt` / `json_objectt` - ``` const std::vector<std::string> input{"foo", "bar"}; const auto json_array = make_range(input) .map(constructor_of<json_stringt>()) .collect<json_arrayt>(); ``` This commit includes - * Constructors from iterators for json_arrayt and json_objectt, so that the iterators from a range can be used to construct these classes. * A `collect` member function for `ranget`, so that a chain of range operations can finish with the construction of a resulting container containing a collection of the results. * A `constructor_of` template function, which provides syntactic sugar when using `map` to call a constructor, compared to writing a new lambda function each time such an operation is carried out. * Unit tests covering all of the above functionality.

This commit is included in this PR, as a demonstration of the coding style which is enabled by the proceeding commits.

Adding `.collect` to the end of a chain of range operations can add clutter to the code, rather than improving readability, in places where the type of container being constructed is apparent from the context. This commit adds a cast operation in order to improve readability in this scenario. In addition to the operator, this commit includes a refactor of `optionst::to_json` in order to demonstrate an example usage of the proposed change.

With the new constructors, these brackets are no longer required and can be removed, in order to improve readability.

Removing this constructor simplifies the interface, by reducing the number of different ways to construct the classes and avoiding exposing the implementation detail of what type of container `json_objectt` and `json_arrayt` are backed by.

thomasspriggs · 2019-01-28T17:40:17Z

Rebased to fix include of catch in unit test.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 2a4d8ff).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98867160
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

martin-cs

I don't see a problem with my part.

thomasspriggs requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners January 20, 2019 21:37

tautschnig approved these changes Jan 20, 2019

View reviewed changes

thomasspriggs force-pushed the tas/json_construction branch from 775e950 to f4952c6 Compare January 20, 2019 23:16

thomasspriggs requested review from cesaro, cristina-david and thk123 as code owners January 20, 2019 23:33

thomasspriggs force-pushed the tas/json_construction branch 4 times, most recently from 0ec1923 to 55051ea Compare January 21, 2019 02:11

allredj reviewed Jan 21, 2019

View reviewed changes

tautschnig approved these changes Jan 21, 2019

View reviewed changes

tautschnig assigned smowton, peterschrammel and chrisr-diffblue Jan 21, 2019

thk123 approved these changes Jan 21, 2019

View reviewed changes

smowton reviewed Jan 21, 2019

View reviewed changes

smowton approved these changes Jan 21, 2019

View reviewed changes

thomasspriggs force-pushed the tas/json_construction branch 2 times, most recently from a8b278c to a859b17 Compare January 21, 2019 17:17

tautschnig assigned kroening Jan 21, 2019

allredj reviewed Jan 21, 2019

View reviewed changes

kroening pushed a commit that referenced this pull request Jan 22, 2019

Drop the desire to do VS2013 builds

1547ab0

Upgrading to VS2015 enables #3862, noexcept (e.g. #2502), UTF8 strings and constexpr (#2133).

kroening mentioned this pull request Jan 22, 2019

Drop the desire to do VS2013 builds #3894

Merged

2 tasks

tautschnig unassigned smowton Jan 23, 2019

thomasspriggs force-pushed the tas/json_construction branch from a859b17 to 000dfa4 Compare January 28, 2019 14:03

Add initializer_list constructor to json_objectt

a8de5e5

This new constructor facilitates the construction of instances of `json_objectt` which are const, because it gives a tidy way to construct an entire `json_objectt`.

thomasspriggs force-pushed the tas/json_construction branch from 000dfa4 to b99f300 Compare January 28, 2019 16:52

thomasspriggs added 6 commits January 28, 2019 17:39

Add initializer_list constructor to json_arrayt

5be69b7

This new constructor facilitates the construction of instances of `json_arrayt` which are const, because it gives a tidy way to construct an entire `json_arrayt`.

Refactor static_verifier_json using range

74bbcf0

This commit is included in this PR, as a demonstration of the coding style which is enabled by the proceeding commits.

Remove unnecessary brackets in constructon of json_objectt

d2c756a

With the new constructors, these brackets are no longer required and can be removed, in order to improve readability.

thomasspriggs force-pushed the tas/json_construction branch from b99f300 to 2a4d8ff Compare January 28, 2019 17:39

allredj reviewed Jan 28, 2019

View reviewed changes

peterschrammel approved these changes Jan 28, 2019

View reviewed changes

peterschrammel removed their assignment Jan 28, 2019

martin-cs approved these changes Jan 28, 2019

View reviewed changes

thomasspriggs merged commit 085fd6a into diffblue:develop Jan 28, 2019

thomasspriggs deleted the tas/json_construction branch January 28, 2019 23:19

		@@ -90,14 +92,12 @@ const optionst::value_listt &optionst::get_list_option(
		/// Returns the options as JSON key value pairs

Add improved functionality for the construction of json_arrayt and json_objectt #3862

Add improved functionality for the construction of json_arrayt and json_objectt #3862

Uh oh!

Conversation

thomasspriggs commented Jan 20, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 21, 2019

Uh oh!

thomasspriggs commented Jan 21, 2019

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Jan 21, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 21, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Jan 21, 2019

Uh oh!

kroening commented Jan 22, 2019

Uh oh!

thomasspriggs commented Jan 22, 2019

Uh oh!

thomasspriggs commented Jan 28, 2019

Uh oh!

thomasspriggs commented Jan 28, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

thomasspriggs commented Jan 20, 2019 •

edited

Loading