Skip to content

Commit 474ed60

Browse files
peterschrammelpeterschrammel
committed
Add C test input generator
Replaces the test input extraction part of bmc_covert, which is entirely independent of producing traces now. To be moved into a prospective ccover tool.
1 parent 5be26d5 commit 474ed60

File tree

3 files changed

+246
-0
lines changed

3 files changed

+246
-0
lines changed

‎src/cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = all_properties.cpp \
22
bmc.cpp \
33
bmc_cover.cpp \
4+
c_test_input_generator.cpp \
45
cbmc_languages.cpp \
56
cbmc_main.cpp \
67
cbmc_parse_options.cpp \

‎src/cbmc/c_test_input_generator.cpp

Lines changed: 176 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,176 @@
1+
/*******************************************************************\
2+
3+
Module: Test Input Generator for C
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Test Input Generator for C
11+
12+
#include "c_test_input_generator.h"
13+
14+
#include <goto-checker/goto_trace_storage.h>
15+
16+
#include <langapi/language_util.h>
17+
18+
#include <util/json.h>
19+
#include <util/json_irep.h>
20+
#include <util/options.h>
21+
#include <util/xml.h>
22+
#include <util/xml_irep.h>
23+
24+
#include <goto-programs/json_expr.h>
25+
#include <goto-programs/json_goto_trace.h>
26+
#include <goto-programs/xml_expr.h>
27+
#include <goto-programs/xml_goto_trace.h>
28+
29+
c_test_input_generatort::c_test_input_generatort(
30+
ui_message_handlert &ui_message_handler,
31+
const optionst &options)
32+
: ui_message_handler(ui_message_handler), options(options)
33+
{
34+
}
35+
36+
void test_inputst::output_plain_text(
37+
std::ostream &out,
38+
const namespacet &ns,
39+
const goto_tracet &goto_trace,
40+
bool print_trace) const
41+
{
42+
bool first = true;
43+
for(const auto &step : goto_trace.steps)
44+
{
45+
if(step.is_input())
46+
{
47+
if(first)
48+
first = false;
49+
else
50+
out << ", ";
51+
52+
out << id2string(step.io_id) << "=";
53+
54+
if(step.io_args.size() == 1)
55+
out << from_expr(ns, "", step.io_args.front());
56+
}
57+
}
58+
out << '\n';
59+
60+
if(print_trace)
61+
{
62+
// currently ignored
63+
}
64+
}
65+
66+
json_objectt test_inputst::to_json(
67+
const namespacet &ns,
68+
const goto_tracet &goto_trace,
69+
bool print_trace) const
70+
{
71+
json_objectt json_result;
72+
json_arrayt &json_inputs = json_result["inputs"].make_array();
73+
74+
for(const auto &step : goto_trace.steps)
75+
{
76+
if(step.is_input())
77+
{
78+
json_objectt json_input({{"id", json_stringt(step.io_id)}});
79+
if(step.io_args.size() == 1)
80+
json_input["value"] = json(step.io_args.front(), ns, ID_unknown);
81+
json_inputs.push_back(std::move(json_input));
82+
}
83+
}
84+
85+
json_arrayt goal_refs;
86+
for(const auto &goal_id : goto_trace.get_all_property_ids())
87+
{
88+
goal_refs.push_back(json_stringt(goal_id));
89+
}
90+
json_result["coveredGoals"] = std::move(goal_refs);
91+
return json_result;
92+
}
93+
94+
xmlt test_inputst::to_xml(
95+
const namespacet &ns,
96+
const goto_tracet &goto_trace,
97+
bool print_trace) const
98+
{
99+
xmlt xml_result("test");
100+
if(print_trace)
101+
{
102+
convert(ns, goto_trace, xml_result.new_element());
103+
}
104+
else
105+
{
106+
xmlt &xml_test = xml_result.new_element("inputs");
107+
108+
for(const auto &step : goto_trace.steps)
109+
{
110+
if(step.is_input())
111+
{
112+
xmlt &xml_input = xml_test.new_element("input");
113+
xml_input.set_attribute("id", id2string(step.io_id));
114+
if(step.io_args.size() == 1)
115+
xml_input.new_element("value") = xml(step.io_args.front(), ns);
116+
}
117+
}
118+
}
119+
120+
for(const auto &goal_id : goto_trace.get_all_property_ids())
121+
{
122+
xmlt &xml_goal = xml_result.new_element("goal");
123+
xml_goal.set_attribute("id", id2string(goal_id));
124+
}
125+
126+
return xml_result;
127+
}
128+
129+
test_inputst c_test_input_generatort::
130+
operator()(const goto_tracet &goto_trace, const namespacet &ns)
131+
{
132+
test_inputst test_inputs;
133+
return test_inputs;
134+
}
135+
136+
void c_test_input_generatort::operator()(const goto_trace_storaget &traces)
137+
{
138+
const namespacet &ns = traces.get_namespace();
139+
const bool print_trace = options.get_bool_option("trace");
140+
messaget log(ui_message_handler);
141+
switch(ui_message_handler.get_ui())
142+
{
143+
case ui_message_handlert::uit::PLAIN:
144+
log.result() << "\nTest suite:\n";
145+
for(const auto trace : traces.all())
146+
{
147+
test_inputst test_inputs = (*this)(trace, ns);
148+
test_inputs.output_plain_text(log.result(), ns, trace, print_trace);
149+
}
150+
log.result() << messaget::eom;
151+
break;
152+
case ui_message_handlert::uit::JSON_UI:
153+
{
154+
if(log.status().tellp() > 0)
155+
log.status() << messaget::eom; // force end of previous message
156+
json_stream_objectt &json_result =
157+
ui_message_handler.get_json_stream().push_back_stream_object();
158+
json_stream_arrayt &tests_array =
159+
json_result.push_back_stream_array("tests");
160+
161+
for(const auto trace : traces.all())
162+
{
163+
test_inputst test_inputs = (*this)(trace, ns);
164+
tests_array.push_back(test_inputs.to_json(ns, trace, print_trace));
165+
}
166+
break;
167+
}
168+
case ui_message_handlert::uit::XML_UI:
169+
for(const auto trace : traces.all())
170+
{
171+
test_inputst test_inputs = (*this)(trace, ns);
172+
log.result() << test_inputs.to_xml(ns, trace, print_trace);
173+
}
174+
break;
175+
}
176+
}

‎src/cbmc/c_test_input_generator.h

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
/*******************************************************************\
2+
3+
Module: Test Input Generator for C
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Test Input Generator for C
11+
12+
#ifndef CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
13+
#define CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
14+
15+
#include <iosfwd>
16+
17+
#include <util/ui_message.h>
18+
19+
class goto_tracet;
20+
class goto_trace_storaget;
21+
class json_objectt;
22+
class namespacet;
23+
class optionst;
24+
25+
class test_inputst
26+
{
27+
public:
28+
/// Outputs the test inputs in plain text format
29+
/// including the trace if desired
30+
void output_plain_text(
31+
std::ostream &out,
32+
const namespacet &ns,
33+
const goto_tracet &goto_trace,
34+
bool print_trace) const;
35+
36+
/// Returns the test inputs in JSON format
37+
/// including the trace if desired
38+
json_objectt to_json(
39+
const namespacet &ns,
40+
const goto_tracet &goto_trace,
41+
bool print_trace) const;
42+
43+
/// Returns the test inputs in XML format
44+
/// including the trace if desired
45+
xmlt to_xml(
46+
const namespacet &ns,
47+
const goto_tracet &goto_trace,
48+
bool print_trace) const;
49+
};
50+
51+
class c_test_input_generatort
52+
{
53+
public:
54+
c_test_input_generatort(
55+
ui_message_handlert &ui_message_handler,
56+
const optionst &options);
57+
58+
/// Extracts test inputs for all traces and outputs them
59+
void operator()(const goto_trace_storaget &);
60+
61+
protected:
62+
ui_message_handlert &ui_message_handler;
63+
const optionst &options;
64+
65+
/// Extracts test inputs from the given \p goto_trace
66+
test_inputst operator()(const goto_tracet &goto_trace, const namespacet &ns);
67+
};
68+
69+
#endif // CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H

0 commit comments

Comments
 (0)