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