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