JSON cmdline interface #4585

peterschrammel · 2019-04-28T20:41:43Z

Allows reading the commandline in JSON format from stdin

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.

tautschnig · 2019-04-28T21:06:33Z

src/json/json_interface.cpp

+
+#include "json_interface.h"
+
+#include <iostream>


Nit pick: I'd prefer for standard-library includes to come last, see also some recent exchange that @kroening and I had; the idea is that any included header file should parse even without additional includes being present. So do the most minimal ones (the ones from util) first, and then by increasing complexity.

tautschnig · 2019-04-28T21:08:10Z

src/json/json_interface.cpp

+    throw invalid_command_line_argument_exceptiont(
+      "array expected", "'options'");
+  }
+  for(const auto &option_pair : to_json_object(options))


Nit pick: add a blank line before this one to be consistent with the code a few lines above.

tautschnig · 2019-04-28T21:11:21Z

src/json/json_interface.cpp

+  {
+    if(argument.is_string())
+      cmdline.args.push_back(argument.value);
+    else


I believe you could increase readability by doing

if(!argument.is_string()) { throw ... } cmdline.args.push_back(argument.value);

because it reduces the number of closing braces that immediately follow each other. This applies even more so down below, where you currently have three closing braces.

tautschnig · 2019-04-28T21:12:39Z

src/json/json_interface.cpp

+  }
+}
+
+/// Parse JSON-formatted commandline options from stdin


I think this should just be removed - or at least I have no idea what Doxygen makes of documentation at both declaration and definition when they aren't the same.

tautschnig · 2019-04-28T21:13:42Z

src/json/json_interface.h

+
+class cmdlinet;
+
+/// Parses the JSON-formatted command line from stdin


I think it would be rather important to document the expected JSON syntax! Otherwise you're bound to trial and error...

tautschnig · 2019-04-28T21:16:27Z

src/cbmc/cbmc_parse_options.cpp

@@ -1030,6 +1033,7 @@ void cbmc_parse_optionst::help()
    " --xml-ui                     use XML-formatted output\n"
    " --xml-interface              bi-directional XML interface\n"
    " --json-ui                    use JSON-formatted output\n"
+    " --json-interface             bi-directional JSON interface\n"


Is this actually bi-directional?! Doesn't it only become "bi"directional when using both --json-interface and --json-ui? (The same is of course true for XML.)

I was wondering about that and have now more investigated in the XML case (see comments there). The original intention was that --xml-interface subsumes --xml-ui.
Actually, the current behaviour was broken because the UI was set before the option could have been parsed from stdin, which seems difficult to fix without splitting the parse_optionst constructor into two phases and adding a set_ui to ui_message_handlert (rather no).
Also, the question is what happens with errors during parsing the options - they should already be output in a proper format. Thus, I'd rather stick with the original intention of 'bi-directional',

I'm not sure I fully understand - I agree that --{json,xml}-interface should subsume --{json,xml}-ui - but I don't think that was actually work as such? If things can be made to work as such then we'd have the desired bi-directional interface.

--json-interface now implies --json-ui, and --xml-interface now implies --xml-ui.

but I don't think that was actually work as such?

Not sure, I understand...

Let me retry, my apologies for completely broken English:

A "bi"-directional interface is about input and output.

--{json,xml}-ui set up the output side of an interface.

The comment claims that --{json,xml}-interface configure a bi-directional interface.

The actual implementation, however, only reads input when using --{json,xml}-interface.

One possible fix would be that upon seeing --{json,xml}-interface we also set the option for --{json,xml}-ui.

This might not actually work as it could be too late, in which case a more extensive change would be required. If this is the case, a simple fix would be to change the comment such as not to promise a bi-directional interface. Users wanting to use a bi-directional interface would then need to provide both --{json,xml}-interface and --{json,xml}-ui.

yes

yes

yes

yes

is being fixed here (was broken)

not required because 5 works.

return true if a property is either true or false.

json-interface subsumes json-ui. When json-interface is enabled then other commandline options haven't been parsed yet when the UI is set.

allows reading the command line in JSON format from stdin.

Allows reading the commandline in JSON format from stdin.

peterschrammel requested review from kroening, pkesseli, smowton and tautschnig as code owners April 28, 2019 20:41

peterschrammel force-pushed the json-cmdline-interface branch from ebc6165 to 9a6f74a Compare April 28, 2019 20:45

tautschnig approved these changes Apr 28, 2019

View reviewed changes

tautschnig assigned peterschrammel Apr 28, 2019

peterschrammel added the do not merge label Apr 28, 2019

peterschrammel force-pushed the json-cmdline-interface branch from 9a6f74a to 8d7230b Compare April 28, 2019 22:42

peterschrammel removed the do not merge label Apr 28, 2019

peterschrammel force-pushed the json-cmdline-interface branch 4 times, most recently from f4fa2e6 to cf56b53 Compare April 29, 2019 10:56

peterschrammel added 4 commits April 29, 2019 11:57

Add jsont::is_boolean

a39c5d2

return true if a property is either true or false.

Use JSON_UI with json-interface

3e07354

json-interface subsumes json-ui. When json-interface is enabled then other commandline options haven't been parsed yet when the UI is set.

Add JSON cmdline interface

fd6e0e0

allows reading the command line in JSON format from stdin.

Add json-interface to CBMC

651c6aa

Allows reading the commandline in JSON format from stdin.

peterschrammel force-pushed the json-cmdline-interface branch from cf56b53 to 651c6aa Compare April 29, 2019 11:05

peterschrammel merged commit 9e045dd into diffblue:develop Apr 29, 2019

peterschrammel deleted the json-cmdline-interface branch April 29, 2019 12:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

JSON cmdline interface #4585

JSON cmdline interface #4585

Uh oh!

peterschrammel commented Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

peterschrammel Apr 28, 2019 •

edited

Loading

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

peterschrammel Apr 28, 2019

Uh oh!

tautschnig Apr 28, 2019

Uh oh!

peterschrammel Apr 29, 2019

Uh oh!

Uh oh!


		class cmdlinet;

		/// Parses the JSON-formatted command line from stdin


		#include "json_interface.h"

		#include <iostream>

JSON cmdline interface #4585

JSON cmdline interface #4585

Uh oh!

Conversation

peterschrammel commented Apr 28, 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!

peterschrammel Apr 28, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Uh oh!

peterschrammel Apr 28, 2019 •

edited

Loading