Skip to content

Commit 9e045dd

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #4585 from peterschrammel/json-cmdline-interface
JSON cmdline interface
2 parents 0c1e0f4 + 651c6aa commit 9e045dd

File tree

11 files changed

+217
-3
lines changed

11 files changed

+217
-3
lines changed

‎regression/cbmc/json-interface1/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
3+
void foo(int x)
4+
{
5+
for(int i = 0; i < 5; ++i)
6+
{
7+
if(x)
8+
assert(0);
9+
assert(0);
10+
}
11+
assert(0);
12+
}

‎regression/cbmc/json-interface1/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE broken-smt-backend
2+
--json-interface
3+
< test.json
4+
activate-multi-line-match
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
8+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
9+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
10+
VERIFICATION FAILED
11+
--
12+
"property": "foo\.assertion\.2"

‎regression/cbmc/json-interface1/test.json

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"arguments": [
3+
"main.c"
4+
],
5+
"options": {
6+
"function": "foo",
7+
"unwind": 3,
8+
"property": [
9+
"foo.assertion.1",
10+
"foo.assertion.3"
11+
],
12+
"trace": true,
13+
"show-properties": false
14+
}
15+
}

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ Author: Daniel Kroening, [email protected]
7979

8080
#include <langapi/mode.h>
8181

82+
#include <json/json_interface.h>
8283
#include <xmllang/xml_interface.h>
8384

8485
#include "c_test_input_generator.h"
@@ -90,6 +91,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
9091
argv,
9192
std::string("CBMC ") + CBMC_VERSION)
9293
{
94+
json_interface(cmdline, ui_message_handler);
9395
xml_interface(cmdline, ui_message_handler);
9496
}
9597

@@ -103,6 +105,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
103105
argv,
104106
std::string("CBMC ") + CBMC_VERSION)
105107
{
108+
json_interface(cmdline, ui_message_handler);
106109
xml_interface(cmdline, ui_message_handler);
107110
}
108111

@@ -1021,6 +1024,7 @@ void cbmc_parse_optionst::help()
10211024
" --xml-ui use XML-formatted output\n"
10221025
" --xml-interface bi-directional XML interface\n"
10231026
" --json-ui use JSON-formatted output\n"
1027+
" --json-interface bi-directional JSON interface\n"
10241028
// NOLINTNEXTLINE(whitespace/line_length)
10251029
HELP_VALIDATE
10261030
HELP_GOTO_TRACE

‎src/cbmc/cbmc_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,9 @@ class optionst;
4747
"(object-bits):" \
4848
OPT_GOTO_CHECK \
4949
"(no-assertions)(no-assumptions)" \
50-
"(xml-ui)(xml-interface)(json-ui)" \
50+
"(xml-ui)(xml-interface)" \
51+
"(json-interface)" \
52+
"(json-ui)" \
5153
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
5254
"(cprover-smt2)" \
5355
"(no-sat-preprocessor)" \

‎src/cbmc/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ goto-instrument
77
goto-programs
88
goto-symex
99
jsil
10+
json
1011
json-symtab-language
1112
langapi # should go away
1213
linking

‎src/json/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
SRC = json_lex.yy.cpp \
1+
SRC = json_interface.cpp \
2+
json_lex.yy.cpp \
23
json_parser.cpp \
34
json_y.tab.cpp \
45
# Empty last line

‎src/json/json_interface.cpp

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
/*******************************************************************\
2+
3+
Module: JSON Commandline Interface
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// JSON Commandline Interface
11+
12+
#include "json_interface.h"
13+
14+
#include <util/cmdline.h>
15+
#include <util/exception_utils.h>
16+
#include <util/json.h>
17+
#include <util/message.h>
18+
19+
#include "json_parser.h"
20+
21+
#include <iostream>
22+
23+
/// Parse commandline options from \p json into \p cmdline
24+
static void get_json_options(const json_objectt &json, cmdlinet &cmdline)
25+
{
26+
const jsont &arguments = json["arguments"];
27+
if(!arguments.is_array())
28+
{
29+
throw invalid_command_line_argument_exceptiont(
30+
"array expected", "'arguments'");
31+
}
32+
33+
for(const auto &argument : to_json_array(arguments))
34+
{
35+
if(!argument.is_string())
36+
{
37+
throw invalid_command_line_argument_exceptiont(
38+
"string expected", "argument");
39+
}
40+
41+
cmdline.args.push_back(argument.value);
42+
}
43+
44+
const jsont &options = json["options"];
45+
if(!options.is_object())
46+
{
47+
throw invalid_command_line_argument_exceptiont(
48+
"array expected", "'options'");
49+
}
50+
51+
for(const auto &option_pair : to_json_object(options))
52+
{
53+
if(option_pair.second.is_string() || option_pair.second.is_number())
54+
{
55+
// e.g. --option x
56+
cmdline.set(option_pair.first, option_pair.second.value);
57+
}
58+
else if(option_pair.second.is_boolean())
59+
{
60+
// e.g. --flag
61+
if(option_pair.second.is_true())
62+
cmdline.set(option_pair.first);
63+
}
64+
else if(option_pair.second.is_array())
65+
{
66+
// e.g. --option x --option y
67+
for(const auto &element : to_json_array(option_pair.second))
68+
{
69+
if(element.is_string())
70+
cmdline.set(option_pair.first, element.value);
71+
else
72+
{
73+
throw invalid_command_line_argument_exceptiont(
74+
"string expected", option_pair.first);
75+
}
76+
}
77+
}
78+
else
79+
{
80+
throw invalid_command_line_argument_exceptiont(
81+
"unrecognized commandline option format",
82+
option_pair.first,
83+
"Boolean, string, number, or string array expected");
84+
}
85+
}
86+
}
87+
88+
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
89+
{
90+
if(cmdline.isset("json-interface"))
91+
{
92+
jsont json;
93+
94+
parse_json(std::cin, "", message_handler, json);
95+
96+
try
97+
{
98+
if(!json.is_object())
99+
{
100+
throw invalid_command_line_argument_exceptiont(
101+
"JSON object expected at top-level", "command-line JSON input");
102+
}
103+
104+
get_json_options(to_json_object(json), cmdline);
105+
106+
// Add this so that it gets propagated into optionst;
107+
// the ui_message_handlert::uit has already been set on the basis
108+
// of the json-interface flag.
109+
cmdline.set("json-ui");
110+
}
111+
catch(const invalid_command_line_argument_exceptiont &e)
112+
{
113+
messaget log(message_handler);
114+
log.error() << e.what() << messaget::eom;
115+
116+
// make sure we fail with a usage error
117+
cmdline.clear();
118+
}
119+
}
120+
}

‎src/json/json_interface.h

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/*******************************************************************\
2+
3+
Module: JSON Commandline Interface
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// JSON Commandline Interface
11+
12+
#ifndef CPROVER_JSON_JSON_INTERFACE_H
13+
#define CPROVER_JSON_JSON_INTERFACE_H
14+
15+
class cmdlinet;
16+
class message_handlert;
17+
18+
/// Parses the JSON-formatted command line from stdin
19+
///
20+
/// Example:
21+
/// \code{.json}
22+
/// {
23+
/// "arguments": [
24+
/// "main.c"
25+
/// ],
26+
/// "options": {
27+
/// "function": "foo",
28+
/// "unwind": 3,
29+
/// "property": [
30+
/// "foo.assertion.1",
31+
/// "foo.assertion.3"
32+
/// ],
33+
/// "trace": true,
34+
/// "show-properties": false
35+
/// }
36+
/// }
37+
/// \endcode
38+
void json_interface(cmdlinet &, message_handlert &);
39+
40+
#endif // CPROVER_JSON_JSON_INTERFACE_H

‎src/util/json.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,11 @@ class jsont
6161
return kind==kindt::J_ARRAY;
6262
}
6363

64+
bool is_boolean() const
65+
{
66+
return kind == kindt::J_TRUE || kind == kindt::J_FALSE;
67+
}
68+
6469
bool is_true() const
6570
{
6671
return kind==kindt::J_TRUE;

‎src/util/ui_message.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,9 @@ ui_message_handlert::ui_message_handlert(
6767
nullptr,
6868
cmdline.isset("xml-ui") || cmdline.isset("xml-interface")
6969
? uit::XML_UI
70-
: cmdline.isset("json-ui") ? uit::JSON_UI : uit::PLAIN,
70+
: cmdline.isset("json-ui") || cmdline.isset("json-interface")
71+
? uit::JSON_UI
72+
: uit::PLAIN,
7173
program,
7274
cmdline.isset("flush"),
7375
cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic"

0 commit comments

Comments
 (0)