cprover
symex_cover.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symex Test Suite Generation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "symex_parse_options.h"
13 
14 #include <iostream>
15 
16 #include <util/json_expr.h>
17 #include <util/xml_expr.h>
18 
21 
22 std::string symex_parse_optionst::get_test(const goto_tracet &goto_trace)
23 {
24  bool first=true;
25  std::string test;
27 
28  for(const auto &step : goto_trace.steps)
29  {
30  if(step.is_input())
31  {
32  if(first)
33  first=false;
34  else
35  test+=", ";
36 
37  test+=id2string(step.io_id)+"=";
38 
39  if(step.io_args.size()==1)
40  test+=from_expr(ns, "", step.io_args.front());
41  }
42  }
43  return test;
44 }
45 
47  const path_searcht::property_mapt &property_map)
48 {
49  // report
50  unsigned goals_covered=0;
51 
52  for(const auto &prop_pair : property_map)
53  if(prop_pair.second.is_failure())
54  goals_covered++;
55 
56  switch(get_ui())
57  {
59  {
60  status() << "\n** coverage results:" << eom;
61 
62  for(const auto &prop_pair : property_map)
63  {
64  const auto &property=prop_pair.second;
65 
66  status() << "[" << prop_pair.first << "]";
67 
68  if(property.source_location.is_not_nil())
69  status() << ' ' << property.source_location;
70 
71  if(!property.description.empty())
72  status() << ' ' << property.description;
73 
74  status() << ": " << (property.is_failure()?"SATISFIED":"FAILED")
75  << eom;
76  }
77 
78  status() << '\n';
79 
80  break;
81  }
82 
84  {
85  for(const auto &prop_pair : property_map)
86  {
87  const auto &property=prop_pair.second;
88 
89  xmlt xml_result("result");
90  xml_result.set_attribute("goal", id2string(prop_pair.first));
91  xml_result.set_attribute(
92  "description", id2string(property.description));
93  xml_result.set_attribute(
94  "status", property.is_failure()?"SATISFIED":"FAILED");
95 
96  if(property.source_location.is_not_nil())
97  xml_result.new_element()=xml(property.source_location);
98 
99  if(property.is_failure())
100  {
102 
103  if(cmdline.isset("trace"))
104  {
105  convert(ns, property.error_trace, xml_result.new_element());
106  }
107  else
108  {
109  xmlt &xml_test=xml_result.new_element("test");
110 
111  for(const auto &step : property.error_trace.steps)
112  {
113  if(step.is_input())
114  {
115  xmlt &xml_input=xml_test.new_element("input");
116  xml_input.set_attribute("id", id2string(step.io_id));
117  if(step.io_args.size()==1)
118  xml_input.new_element("value")=
119  xml(step.io_args.front(), ns);
120  }
121  }
122  }
123  }
124 
125  std::cout << xml_result << "\n";
126  }
127 
128  break;
129  }
131  {
132  json_objectt json_result;
133  json_arrayt &result_array=json_result["results"].make_array();
134  for(const auto &prop_pair : property_map)
135  {
136  const auto &property=prop_pair.second;
137 
138  json_objectt &result=result_array.push_back().make_object();
139  result["status"]=
140  json_stringt(property.is_failure()?"satisfied":"failed");
141  result["goal"]=json_stringt(id2string(prop_pair.first));
142  result["description"]=json_stringt(id2string(property.description));
143 
144  if(property.source_location.is_not_nil())
145  result["sourceLocation"]=json(property.source_location);
146 
147  if(property.is_failure())
148  {
150 
151  if(cmdline.isset("trace"))
152  {
153  jsont &json_trace=result["trace"];
154  convert(ns, property.error_trace, json_trace);
155  }
156  else
157  {
158  json_arrayt &json_test=result["test"].make_array();
159 
160  for(const auto &step : property.error_trace.steps)
161  {
162  if(step.is_input())
163  {
164  json_objectt json_input;
165  json_input["id"]=json_stringt(id2string(step.io_id));
166  if(step.io_args.size()==1)
167  json_input["value"]=json(step.io_args.front(), ns);
168  json_test.push_back(json_input);
169  }
170  }
171  }
172  }
173  }
174  json_result["totalGoals"]=
175  json_numbert(std::to_string(property_map.size()));
176  json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
177  std::cout << ",\n" << json_result;
178  break;
179  }
180  }
181 
182  status() << "** " << goals_covered
183  << " of " << property_map.size() << " covered ("
184  << std::fixed << std::setw(1) << std::setprecision(1)
185  << (property_map.empty()?
186  100.0:100.0*goals_covered/property_map.size())
187  << "%)"
188  << eom;
189 
191  {
192  std::set<std::string> tests;
193 
194  for(const auto &prop_pair : property_map)
195  if(prop_pair.second.is_failure())
196  tests.insert(get_test(prop_pair.second.error_trace));
197 
198  std::cout << "Test suite:" << '\n';
199 
200  for(const auto &t : tests)
201  std::cout << t << '\n';
202  }
203 }
Command Line Parsing.
mstreamt & result()
Definition: message.h:233
void report_cover(const path_searcht::property_mapt &)
Definition: symex_cover.cpp:46
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::map< irep_idt, property_entryt > property_mapt
Definition: path_search.h:102
mstreamt & status()
Definition: message.h:238
uit get_ui()
Definition: language_ui.h:47
Definition: json.h:21
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
symbol_tablet symbol_table
Definition: goto_model.h:25
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
stepst steps
Definition: goto_trace.h:150
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
json_arrayt & make_array()
Definition: json.h:228
jsont & push_back(const jsont &json)
Definition: json.h:157
virtual bool isset(char option) const
Definition: cmdline.cpp:30
Traces of GOTO Programs.
source_locationt source_location
Definition: message.h:175
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
Traces of GOTO Programs.
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
xmlt & new_element(const std::string &name)
Definition: xml.h:86
json_objectt & make_object()
Definition: json.h:234
std::string get_test(const goto_tracet &goto_trace)
Definition: symex_cover.cpp:22
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23