34 return pc->source_location.as_string() ==
35 other.
pc->source_location.as_string();
44 std::size_t ssa_index,
45 const exprt ssa_expression,
54 if(!pre_existing.second)
74 const exprt ssa_expression,
75 const std::vector<goto_programt::const_targett> &pcs)
90 const size_t cnf_clause_index,
96 for(
const auto &literal : bv)
104 std::cout << cnf_clause_index <<
": ";
105 for(
const auto &literal : cnf)
106 std::cout << literal.dimacs() <<
" ";
127 std::size_t ssa_set_bit_offset = 0;
128 const std::size_t one = 1;
130 ++ssa_set_bit_offset;
138 if(ssa_step_hardness.empty())
142 for(
const auto &key_value_pair : ssa_step_hardness)
144 auto const &ssa = key_value_pair.first;
145 auto const &hardness = key_value_pair.second;
147 hardness_stats_json[
"SSA_expr"] =
json_stringt{ssa.ssa_expression};
148 hardness_stats_json[
"GOTO"] =
155 hardness_stats_json[
"GOTO_ID"] =
157 hardness_stats_json[
"Source"] =
json(ssa.pc->source_location);
160 sat_hardness_json[
"Clauses"] =
162 sat_hardness_json[
"Literals"] =
164 sat_hardness_json[
"Variables"] =
168 for(
auto const &clause : hardness.clause_set)
173 sat_hardness_json[
"ClauseSet"] = sat_hardness_clause_set_json;
175 hardness_stats_json[
"SAT_hardness"] = sat_hardness_json;
177 json_stream_array.
push_back(hardness_stats_json);
185 assertion_stats_json[
"SSA_expr"] =
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);
197 assertion_stats_json[
"Sources"] = assertion_stats_pcs_json;
200 assertion_hardness_json[
"Clauses"] =
202 assertion_hardness_json[
"Literals"] =
207 json_arrayt assertion_sat_hardness_clause_set_json;
210 assertion_sat_hardness_clause_set_json.
push_back(
213 assertion_hardness_json[
"ClauseSet"] =
214 assertion_sat_hardness_clause_set_json;
216 assertion_stats_json[
"SAT_hardness"] = assertion_hardness_json;
218 json_stream_array.
push_back(assertion_stats_json);
225 std::stringstream out;
226 auto instruction = *pc;
228 if(!instruction.labels.empty())
230 out <<
" // Labels:";
231 for(
const auto &label : instruction.labels)
235 if(instruction.is_target())
236 out << std::setw(6) << instruction.target_number <<
": ";
238 switch(instruction.type)
241 out <<
"NO INSTRUCTION TYPE SET";
246 if(!instruction.get_condition().is_true())
248 out <<
"IF " <<
format(instruction.get_condition()) <<
" THEN ";
253 if(instruction.is_incomplete_goto())
255 out <<
"(incomplete)";
259 for(
auto gt_it = instruction.targets.begin();
260 gt_it != instruction.targets.end();
263 if(gt_it != instruction.targets.begin())
265 out << (*gt_it)->target_number;
271 out <<
"SET RETURN VALUE" <<
format(instruction.return_value());
279 out <<
format(instruction.get_code());
284 if(instruction.is_assume())
289 out <<
format(instruction.get_condition());
297 out <<
"END_FUNCTION";
309 instruction.get_code().find(ID_exception_list).get_sub();
311 for(
const auto &ex : exception_list)
312 out <<
" " << ex.id();
315 if(instruction.get_code().operands().size() == 1)
316 out <<
": " <<
format(instruction.get_code().op0());
322 if(instruction.get_code().get_statement() == ID_exception_landingpad)
325 out <<
"EXCEPTION LANDING PAD (" <<
format(landingpad.catch_expr().type())
326 <<
' ' <<
format(landingpad.catch_expr()) <<
")";
328 else if(instruction.get_code().get_statement() == ID_push_catch)
330 out <<
"CATCH-PUSH ";
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();
343 if(gt_it != instruction.targets.begin())
345 out << exception_list[i].id() <<
"->" << (*gt_it)->target_number;
348 else if(instruction.get_code().get_statement() == ID_pop_catch)
360 out <<
"ATOMIC_BEGIN";
368 out <<
"START THREAD " << instruction.get_target()->target_number;
381 std::stringstream ss;