cprover
c_test_input_generator.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Test Input Generator for C
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "c_test_input_generator.h"
13 
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/string_utils.h>
22 #include <util/xml.h>
23 #include <util/xml_irep.h>
24 
27 #include <goto-programs/xml_expr.h>
29 
31  ui_message_handlert &ui_message_handler,
32  const optionst &options)
33  : ui_message_handler(ui_message_handler), options(options)
34 {
35 }
36 
38  std::ostream &out,
39  const namespacet &ns,
40  const goto_tracet &goto_trace) const
41 {
42  const auto input_assignments =
43  make_range(goto_trace.steps)
44  .filter([](const goto_trace_stept &step) { return step.is_input(); })
45  .map([ns](const goto_trace_stept &step) {
46  return id2string(step.io_id) + '=' +
47  from_expr(ns, step.function_id, step.io_args.front());
48  });
49  join_strings(out, input_assignments.begin(), input_assignments.end(), ", ");
50  out << '\n';
51 }
52 
54  const namespacet &ns,
55  const goto_tracet &goto_trace,
56  bool print_trace) const
57 {
58  json_objectt json_result;
59  json_arrayt &json_inputs = json_result["inputs"].make_array();
60 
61  for(const auto &step : goto_trace.steps)
62  {
63  if(step.is_input())
64  {
65  json_objectt json_input({{"id", json_stringt(step.io_id)}});
66  if(step.io_args.size() == 1)
67  json_input["value"] =
68  json(step.io_args.front(), ns, ns.lookup(step.function_id).mode);
69  json_inputs.push_back(std::move(json_input));
70  }
71  }
72 
73  json_arrayt goal_refs;
74  for(const auto &goal_id : goto_trace.get_failed_property_ids())
75  {
76  goal_refs.push_back(json_stringt(goal_id));
77  }
78  json_result["coveredGoals"] = std::move(goal_refs);
79 
80  if(print_trace)
81  {
82  json_arrayt json_trace;
83  convert(ns, goto_trace, json_trace);
84  json_result["trace"] = std::move(json_trace);
85  }
86  return json_result;
87 }
88 
90  const namespacet &ns,
91  const goto_tracet &goto_trace,
92  bool print_trace) const
93 {
94  xmlt xml_result("test");
95  if(print_trace)
96  {
97  convert(ns, goto_trace, xml_result.new_element());
98  }
99  else
100  {
101  xmlt &xml_test = xml_result.new_element("inputs");
102 
103  for(const auto &step : goto_trace.steps)
104  {
105  if(step.is_input())
106  {
107  xmlt &xml_input = xml_test.new_element("input");
108  xml_input.set_attribute("id", id2string(step.io_id));
109  if(step.io_args.size() == 1)
110  xml_input.new_element("value") = xml(step.io_args.front(), ns);
111  }
112  }
113  }
114 
115  for(const auto &goal_id : goto_trace.get_failed_property_ids())
116  {
117  xmlt &xml_goal = xml_result.new_element("goal");
118  xml_goal.set_attribute("id", id2string(goal_id));
119  }
120 
121  return xml_result;
122 }
123 
125 operator()(const goto_tracet &goto_trace, const namespacet &ns)
126 {
127  test_inputst test_inputs;
128  return test_inputs;
129 }
130 
132 {
133  const namespacet &ns = traces.get_namespace();
134  const bool print_trace = options.get_bool_option("trace");
136  switch(ui_message_handler.get_ui())
137  {
139  log.result() << "\nTest suite:\n";
140  for(const auto &trace : traces.all())
141  {
142  test_inputst test_inputs = (*this)(trace, ns);
143  test_inputs.output_plain_text(log.result(), ns, trace);
144  }
145  log.result() << messaget::eom;
146  break;
148  {
149  if(log.status().tellp() > 0)
150  log.status() << messaget::eom; // force end of previous message
151  json_stream_objectt &json_result =
153  json_stream_arrayt &tests_array =
154  json_result.push_back_stream_array("tests");
155 
156  for(const auto &trace : traces.all())
157  {
158  test_inputst test_inputs = (*this)(trace, ns);
159  tests_array.push_back(test_inputs.to_json(ns, trace, print_trace));
160  }
161  break;
162  }
164  for(const auto &trace : traces.all())
165  {
166  test_inputst test_inputs = (*this)(trace, ns);
167  log.result() << test_inputs.to_xml(ns, trace, print_trace);
168  }
169  break;
170  }
171 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
goto_tracet::get_failed_property_ids
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:783
ui_message_handlert
Definition: ui_message.h:20
ui_message_handlert::uit::XML_UI
@ XML_UI
optionst
Definition: options.h:23
string_utils.h
messaget::status
mstreamt & status() const
Definition: message.h:414
goto_trace_storaget::all
const std::vector< goto_tracet > & all() const
Definition: goto_trace_storage.cpp:46
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
xml_irep.h
options.h
Options.
goto_trace_stept::is_input
bool is_input() const
Definition: goto_trace.h:64
messaget::eom
static eomt eom
Definition: message.h:297
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
xml.h
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
convert
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: builtin_factory.cpp:42
c_test_input_generator.h
Test Input Generator for C.
messaget::result
mstreamt & result() const
Definition: message.h:409
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
ui_message_handlert::uit::JSON_UI
@ JSON_UI
language_util.h
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:64
xml_goto_trace.h
Traces of GOTO Programs.
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
c_test_input_generatort::c_test_input_generatort
c_test_input_generatort(ui_message_handlert &ui_message_handler, const optionst &options)
Definition: c_test_input_generator.cpp:30
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
goto_trace_storage.h
Goto Trace Storage.
test_inputst::to_xml
xmlt to_xml(const namespacet &ns, const goto_tracet &goto_trace, bool print_trace) const
Returns the test inputs in XML format including the trace if desired.
Definition: c_test_input_generator.cpp:89
json_expr.h
Expressions in JSON.
c_test_input_generatort::operator()
void operator()(const goto_trace_storaget &)
Extracts test inputs for all traces and outputs them.
Definition: c_test_input_generator.cpp:131
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
json_goto_trace.h
Traces of GOTO Programs.
xmlt
Definition: xml.h:21
test_inputst::to_json
json_objectt to_json(const namespacet &ns, const goto_tracet &goto_trace, bool print_trace) const
Returns the test inputs in JSON format including the trace if desired.
Definition: c_test_input_generator.cpp:53
c_test_input_generatort::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: c_test_input_generator.h:60
goto_trace_storaget
Definition: goto_trace_storage.h:18
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
test_inputst
Definition: c_test_input_generator.h:26
ui_message_handlert::uit::PLAIN
@ PLAIN
goto_trace_storaget::get_namespace
const namespacet & get_namespace() const
Definition: goto_trace_storage.cpp:60
test_inputst::output_plain_text
void output_plain_text(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace) const
Outputs the test inputs in plain text format.
Definition: c_test_input_generator.cpp:37
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
json.h
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
c_test_input_generatort::options
const optionst & options
Definition: c_test_input_generator.h:61
goto_trace_stept::io_id
irep_idt io_id
Definition: goto_trace.h:135
json_stream_arrayt::push_back
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
goto_trace_stept::io_args
io_argst io_args
Definition: goto_trace.h:137
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
goto_trace_stept::function_id
irep_idt function_id
Definition: goto_trace.h:111
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
xml_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270