35 return pc->source_location().as_string() ==
36 other.
pc->source_location().as_string();
45 std::size_t ssa_index,
46 const exprt ssa_expression,
55 if(!pre_existing.second)
75 const exprt ssa_expression,
76 const std::vector<goto_programt::const_targett> &pcs)
91 const size_t cnf_clause_index,
97 for(
const auto &literal : bv)
105 std::cout << cnf_clause_index <<
": ";
106 for(
const auto &literal : cnf)
107 std::cout << literal.dimacs() <<
" ";
128 std::size_t ssa_set_bit_offset = 0;
129 const std::size_t one = 1;
131 ++ssa_set_bit_offset;
139 if(ssa_step_hardness.empty())
143 for(
const auto &key_value_pair : ssa_step_hardness)
145 auto const &ssa = key_value_pair.first;
146 auto const &hardness = key_value_pair.second;
148 hardness_stats_json[
"SSA_expr"] =
json_stringt{ssa.ssa_expression};
149 hardness_stats_json[
"GOTO"] =
156 hardness_stats_json[
"GOTO_ID"] =
158 hardness_stats_json[
"Source"] =
json(ssa.pc->source_location());
161 sat_hardness_json[
"Clauses"] =
163 sat_hardness_json[
"Literals"] =
165 sat_hardness_json[
"Variables"] =
169 for(
auto const &clause : hardness.clause_set)
174 sat_hardness_json[
"ClauseSet"] = sat_hardness_clause_set_json;
176 hardness_stats_json[
"SAT_hardness"] = sat_hardness_json;
178 json_stream_array.
push_back(hardness_stats_json);
186 assertion_stats_json[
"SSA_expr"] =
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);
198 assertion_stats_json[
"Sources"] = assertion_stats_pcs_json;
201 assertion_hardness_json[
"Clauses"] =
203 assertion_hardness_json[
"Literals"] =
208 json_arrayt assertion_sat_hardness_clause_set_json;
211 assertion_sat_hardness_clause_set_json.
push_back(
214 assertion_hardness_json[
"ClauseSet"] =
215 assertion_sat_hardness_clause_set_json;
217 assertion_stats_json[
"SAT_hardness"] = assertion_hardness_json;
219 json_stream_array.
push_back(assertion_stats_json);
226 std::stringstream out;
227 auto instruction = *pc;
229 if(!instruction.labels.empty())
231 out <<
" // Labels:";
232 for(
const auto &label : instruction.labels)
236 if(instruction.is_target())
237 out << std::setw(6) << instruction.target_number <<
": ";
239 switch(instruction.type())
242 out <<
"NO INSTRUCTION TYPE SET";
247 if(!instruction.get_condition().is_true())
249 out <<
"IF " <<
format(instruction.get_condition()) <<
" THEN ";
254 if(instruction.is_incomplete_goto())
256 out <<
"(incomplete)";
260 for(
auto gt_it = instruction.targets.begin();
261 gt_it != instruction.targets.end();
264 if(gt_it != instruction.targets.begin())
266 out << (*gt_it)->target_number;
272 out <<
"SET RETURN VALUE" <<
format(instruction.return_value());
280 out <<
format(instruction.get_code());
285 if(instruction.is_assume())
290 out <<
format(instruction.get_condition());
298 out <<
"END_FUNCTION";
310 instruction.get_code().find(ID_exception_list).get_sub();
312 for(
const auto &ex : exception_list)
313 out <<
" " << ex.id();
316 if(instruction.get_code().operands().size() == 1)
317 out <<
": " <<
format(instruction.get_code().op0());
323 if(instruction.get_code().get_statement() == ID_exception_landingpad)
326 out <<
"EXCEPTION LANDING PAD (" <<
format(landingpad.catch_expr().type())
327 <<
' ' <<
format(landingpad.catch_expr()) <<
")";
329 else if(instruction.get_code().get_statement() == ID_push_catch)
331 out <<
"CATCH-PUSH ";
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();
344 if(gt_it != instruction.targets.begin())
346 out << exception_list[i].id() <<
"->" << (*gt_it)->target_number;
349 else if(instruction.get_code().get_statement() == ID_pop_catch)
361 out <<
"ATOMIC_BEGIN";
369 out <<
"START THREAD " << instruction.get_target()->target_number;
382 std::stringstream ss;
Base class for all expressions.
instructionst::const_iterator const_targett
jsont & push_back(const jsont &json)
Provides methods for streaming JSON arrays.
std::vector< literalt > bvt
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
static code_landingpadt & to_code_landingpad(codet &code)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::vector< goto_programt::const_targett > pcs
sat_hardnesst sat_hardness
std::string ssa_expression
goto_programt::const_targett pc
bool operator==(const hardness_ssa_keyt &other) const
std::string ssa_expression
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::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)