cprover
solver_hardness.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: measure and track the complexity of solver queries
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "solver_hardness.h"
10 
11 #include <algorithm>
12 #include <iomanip>
13 #include <iostream>
14 
15 #include <cstdint>
16 
17 #include <util/format_expr.h>
18 #include <util/format_type.h>
19 #include <util/json_irep.h>
20 #include <util/json_stream.h>
21 #include <util/string2int.h>
22 
25 {
26  clauses += other.clauses;
27  literals += other.literals;
28  variables.insert(other.variables.begin(), other.variables.end());
29  return *this;
30 }
31 
34 {
35  if(ssa_expression != other.ssa_expression)
36  return false;
37  return pc->source_location.as_string() ==
38  other.pc->source_location.as_string();
39 }
40 
42 {
43  return pcs.empty();
44 }
45 
47  std::size_t ssa_index,
48  const exprt ssa_expression,
50 {
51  PRECONDITION(ssa_index < hardness_stats.size());
52 
53  current_ssa_key.ssa_expression = expr2string(ssa_expression);
54  current_ssa_key.pc = pc;
55  auto pre_existing =
56  hardness_stats[ssa_index].insert({current_ssa_key, current_hardness});
57  if(!pre_existing.second)
58  { // there already was an element with the same key
59  pre_existing.first->second += current_hardness;
60  }
61  if(hardness_stats[ssa_index].size() > max_ssa_set_size)
62  max_ssa_set_size = hardness_stats[ssa_index].size();
63  current_ssa_key = {};
64  current_hardness = {};
65 }
66 
68 {
69  // do not shrink
70  if(size <= hardness_stats.size())
71  return;
72 
73  hardness_stats.resize(size);
74 }
75 
77  const exprt ssa_expression,
78  const std::vector<goto_programt::const_targett> &pcs)
79 {
81  return;
82 
84  assertion_stats.ssa_expression = expr2string(ssa_expression);
85  assertion_stats.pcs = pcs;
86  current_ssa_key = {};
87  current_hardness = {};
88 }
89 
91 {
93  current_hardness.literals += bv.size();
94  for(const auto &literal : bv)
95  {
96  current_hardness.variables.insert(literal.var_no());
97  }
98 }
99 
100 void solver_hardnesst::set_outfile(const std::string &file_name)
101 {
102  outfile = file_name;
103 }
104 
106 {
107  PRECONDITION(!outfile.empty());
108 
109  // The SSA steps and indexed internally (by the position in the SSA equation)
110  // but if the `--paths` option is used, there are multiple equations, some
111  // sharing SSA steps. We only store the unique ones in a set but now we want
112  // to identify them by a single number. So we shift the SSA index to make room
113  // for the set index.
114  std::size_t ssa_set_bit_offset = 0;
115  const std::size_t one = 1;
116  while((one << ssa_set_bit_offset) < max_ssa_set_size)
117  ++ssa_set_bit_offset;
118 
119  std::ofstream out{outfile};
120  json_stream_arrayt json_stream_array{out};
121 
122  for(std::size_t i = 0; i < hardness_stats.size(); i++)
123  {
124  const auto &ssa_step_hardness = hardness_stats[i];
125  if(ssa_step_hardness.empty())
126  continue;
127 
128  std::size_t j = 0;
129  for(const auto &key_value_pair : ssa_step_hardness)
130  {
131  auto const &ssa = key_value_pair.first;
132  auto const &hardness = key_value_pair.second;
133  auto hardness_stats_json = json_objectt{};
134  hardness_stats_json["SSA_expr"] = json_stringt{ssa.ssa_expression};
135  hardness_stats_json["GOTO"] =
137 
138  // It might be desirable to collect all SAT hardness statistics pertaining
139  // to a particular GOTO instruction, since there may be a number of SSA
140  // steps per GOTO instruction. The following JSON contains a unique
141  // identifier for each one.
142  hardness_stats_json["GOTO_ID"] =
143  json_numbert{std::to_string((i << ssa_set_bit_offset) + j)};
144  hardness_stats_json["Source"] = json(ssa.pc->source_location);
145 
146  auto sat_hardness_json = json_objectt{};
147  sat_hardness_json["Clauses"] =
148  json_numbert{std::to_string(hardness.clauses)};
149  sat_hardness_json["Literals"] =
150  json_numbert{std::to_string(hardness.literals)};
151  sat_hardness_json["Variables"] =
152  json_numbert{std::to_string(hardness.variables.size())};
153 
154  hardness_stats_json["SAT_hardness"] = sat_hardness_json;
155 
156  json_stream_array.push_back(hardness_stats_json);
157  ++j;
158  }
159  }
160 
161  if(!assertion_stats.empty())
162  {
163  auto assertion_stats_json = json_objectt{};
164  assertion_stats_json["SSA_expr"] =
166 
167  auto assertion_stats_pcs_json = json_arrayt{};
168  for(const auto &pc : assertion_stats.pcs)
169  {
170  auto assertion_stats_pc_json = json_objectt{};
171  assertion_stats_pc_json["GOTO"] =
173  assertion_stats_pc_json["Source"] = json(pc->source_location);
174  assertion_stats_pcs_json.push_back(assertion_stats_pc_json);
175  }
176  assertion_stats_json["Sources"] = assertion_stats_pcs_json;
177 
178  auto assertion_hardness_json = json_objectt{};
179  assertion_hardness_json["Clauses"] =
181  assertion_hardness_json["Literals"] =
183  assertion_hardness_json["Variables"] = json_numbert{
185 
186  assertion_stats_json["SAT_hardness"] = assertion_hardness_json;
187 
188  json_stream_array.push_back(assertion_stats_json);
189  }
190 }
191 
192 std::string
194 {
195  std::stringstream out;
196  auto instruction = *pc;
197 
198  if(!instruction.labels.empty())
199  {
200  out << " // Labels:";
201  for(const auto &label : instruction.labels)
202  out << " " << label;
203  }
204 
205  if(instruction.is_target())
206  out << std::setw(6) << instruction.target_number << ": ";
207 
208  switch(instruction.type)
209  {
210  case NO_INSTRUCTION_TYPE:
211  out << "NO INSTRUCTION TYPE SET";
212  break;
213 
214  case GOTO:
215  case INCOMPLETE_GOTO:
216  if(!instruction.get_condition().is_true())
217  {
218  out << "IF " << format(instruction.get_condition()) << " THEN ";
219  }
220 
221  out << "GOTO ";
222 
223  if(instruction.is_incomplete_goto())
224  {
225  out << "(incomplete)";
226  }
227  else
228  {
229  for(auto gt_it = instruction.targets.begin();
230  gt_it != instruction.targets.end();
231  gt_it++)
232  {
233  if(gt_it != instruction.targets.begin())
234  out << ", ";
235  out << (*gt_it)->target_number;
236  }
237  }
238  break;
239 
240  case RETURN:
241  case OTHER:
242  case DECL:
243  case DEAD:
244  case FUNCTION_CALL:
245  case ASSIGN:
246  out << format(instruction.code);
247  break;
248 
249  case ASSUME:
250  case ASSERT:
251  if(instruction.is_assume())
252  out << "ASSUME ";
253  else
254  out << "ASSERT ";
255 
256  out << format(instruction.get_condition());
257  break;
258 
259  case SKIP:
260  out << "SKIP";
261  break;
262 
263  case END_FUNCTION:
264  out << "END_FUNCTION";
265  break;
266 
267  case LOCATION:
268  out << "LOCATION";
269  break;
270 
271  case THROW:
272  out << "THROW";
273 
274  {
275  const irept::subt &exception_list =
276  instruction.code.find(ID_exception_list).get_sub();
277 
278  for(const auto &ex : exception_list)
279  out << " " << ex.id();
280  }
281 
282  if(instruction.code.operands().size() == 1)
283  out << ": " << format(instruction.code.op0());
284 
285  break;
286 
287  case CATCH:
288  {
289  if(instruction.code.get_statement() == ID_exception_landingpad)
290  {
291  const auto &landingpad = to_code_landingpad(instruction.code);
292  out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type())
293  << ' ' << format(landingpad.catch_expr()) << ")";
294  }
295  else if(instruction.code.get_statement() == ID_push_catch)
296  {
297  out << "CATCH-PUSH ";
298 
299  unsigned i = 0;
300  const irept::subt &exception_list =
301  instruction.code.find(ID_exception_list).get_sub();
303  instruction.targets.size() == exception_list.size(),
304  "unexpected discrepancy between sizes of instruction"
305  "targets and exception list");
306  for(auto gt_it = instruction.targets.begin();
307  gt_it != instruction.targets.end();
308  gt_it++, i++)
309  {
310  if(gt_it != instruction.targets.begin())
311  out << ", ";
312  out << exception_list[i].id() << "->" << (*gt_it)->target_number;
313  }
314  }
315  else if(instruction.code.get_statement() == ID_pop_catch)
316  {
317  out << "CATCH-POP";
318  }
319  else
320  {
321  UNREACHABLE;
322  }
323  break;
324  }
325 
326  case ATOMIC_BEGIN:
327  out << "ATOMIC_BEGIN";
328  break;
329 
330  case ATOMIC_END:
331  out << "ATOMIC_END";
332  break;
333 
334  case START_THREAD:
335  out << "START THREAD " << instruction.get_target()->target_number;
336  break;
337 
338  case END_THREAD:
339  out << "END THREAD";
340  break;
341  }
342 
343  return out.str();
344 }
345 
346 std::string solver_hardnesst::expr2string(const exprt expr)
347 {
348  std::stringstream ss;
349  ss << format(expr);
350  return ss.str();
351 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
json_numbert
Definition: json.h:291
format
static format_containert< T > format(const T &o)
Definition: format.h:35
solver_hardnesst::register_ssa_size
void register_ssa_size(std::size_t size)
Definition: solver_hardness.cpp:67
solver_hardnesst::sat_hardnesst
Definition: solver_hardness.h:49
bvt
std::vector< literalt > bvt
Definition: literal.h:201
json_stream.h
solver_hardnesst::expr2string
static std::string expr2string(const exprt expr)
Definition: solver_hardness.cpp:346
solver_hardnesst::goto_instruction2string
static std::string goto_instruction2string(goto_programt::const_targett pc)
Definition: solver_hardness.cpp:193
solver_hardness.h
exprt
Base class for all expressions.
Definition: expr.h:53
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
string2int.h
THROW
@ THROW
Definition: goto_program.h:50
coverage_criteriont::LOCATION
@ LOCATION
solver_hardnesst::assertion_stats
assertion_statst assertion_stats
Definition: solver_hardness.h:136
GOTO
@ GOTO
Definition: goto_program.h:34
solver_hardnesst::current_ssa_key
hardness_ssa_keyt current_ssa_key
Definition: solver_hardness.h:134
solver_hardnesst::hardness_ssa_keyt::ssa_expression
std::string ssa_expression
Definition: solver_hardness.h:63
solver_hardnesst::assertion_statst::pcs
std::vector< goto_programt::const_targett > pcs
Definition: solver_hardness.h:76
solver_hardnesst::sat_hardnesst::variables
std::unordered_set< size_t > variables
Definition: solver_hardness.h:52
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
solver_hardnesst::sat_hardnesst::clauses
size_t clauses
Definition: solver_hardness.h:50
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
solver_hardnesst::register_clause
void register_clause(const bvt &bv)
Called e.g.
Definition: solver_hardness.cpp:90
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
solver_hardnesst::outfile
std::string outfile
Definition: solver_hardness.h:131
solver_hardnesst::assertion_statst::sat_hardness
sat_hardnesst sat_hardness
Definition: solver_hardness.h:74
solver_hardnesst::hardness_stats
std::vector< std::unordered_map< hardness_ssa_keyt, sat_hardnesst > > hardness_stats
Definition: solver_hardness.h:133
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
OTHER
@ OTHER
Definition: goto_program.h:37
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
solver_hardnesst::register_ssa
void register_ssa(std::size_t ssa_index, const exprt ssa_expression, goto_programt::const_targett pc)
Called from the symtex_target_equationt::convert_*, this function associates an SSA step to all the s...
Definition: solver_hardness.cpp:46
solver_hardnesst::register_assertion_ssas
void register_assertion_ssas(const exprt ssa_expression, const std::vector< goto_programt::const_targett > &pcs)
Called from the symtex_target_equationt::convert_assertions, this function associates the disjunction...
Definition: solver_hardness.cpp:76
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
RETURN
@ RETURN
Definition: goto_program.h:45
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
format_expr.h
to_code_landingpad
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2415
solver_hardnesst::set_outfile
void set_outfile(const std::string &file_name)
Definition: solver_hardness.cpp:100
CATCH
@ CATCH
Definition: goto_program.h:51
solver_hardnesst::max_ssa_set_size
std::size_t max_ssa_set_size
Definition: solver_hardness.h:137
DECL
@ DECL
Definition: goto_program.h:47
solver_hardnesst::sat_hardnesst::literals
size_t literals
Definition: solver_hardness.h:51
solver_hardnesst::hardness_ssa_keyt::operator==
bool operator==(const hardness_ssa_keyt &other) const
Definition: solver_hardness.cpp:33
ASSUME
@ ASSUME
Definition: goto_program.h:35
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
DEAD
@ DEAD
Definition: goto_program.h:48
solver_hardnesst::hardness_ssa_keyt::pc
goto_programt::const_targett pc
Definition: solver_hardness.h:64
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
ASSERT
@ ASSERT
Definition: goto_program.h:36
format_type.h
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
solver_hardnesst::produce_report
void produce_report()
Print the statistics to a JSON file (specified via command-line option).
Definition: solver_hardness.cpp:105
solver_hardnesst::assertion_statst::empty
bool empty() const
Definition: solver_hardness.cpp:41
solver_hardnesst::hardness_ssa_keyt
Definition: solver_hardness.h:62
solver_hardnesst::current_hardness
sat_hardnesst current_hardness
Definition: solver_hardness.h:135
solver_hardnesst::sat_hardnesst::operator+=
sat_hardnesst & operator+=(const sat_hardnesst &other)
Definition: solver_hardness.cpp:24
json_stringt
Definition: json.h:270
solver_hardnesst::assertion_statst::ssa_expression
std::string ssa_expression
Definition: solver_hardness.h:75