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