From 0ff138419b0590accd748a878a29a766338b2263 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 14:57:05 +0100 Subject: [PATCH 01/10] Remove unused local variable --- src/goto-programs/json_goto_trace.cpp | 2 +- src/goto-programs/xml_goto_trace.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 552de9cee29..0d1b01f668e 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -84,7 +84,7 @@ void convert_decl( if(!json_location.is_null()) json_assignment["sourceLocation"] = json_location; - std::string value_string, binary_string, type_string, full_lhs_string; + std::string value_string, type_string, full_lhs_string; json_objectt full_lhs_value; DATA_INVARIANT( diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 08a12d1e82e..5a816cb186d 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -76,7 +76,7 @@ void convert( if(xml_location.name!="") xml_assignment.new_element().swap(xml_location); - std::string value_string, binary_string, type_string, + std::string value_string, type_string, full_lhs_string, full_lhs_value_string; if(step.lhs_object_value.is_not_nil()) From 6f72d9b1ab779a25f57b1b09cbc1865b71a45718 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 11 May 2018 14:59:50 +0100 Subject: [PATCH 02/10] Split binary string in plain-text output of goto trace in groups of 8 --- src/goto-programs/goto_trace.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index e7f05e09e96..dde36acec56 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -122,7 +122,18 @@ std::string trace_value_binary( type.id()==ID_c_enum || type.id()==ID_c_enum_tag) { - return expr.get_string(ID_value); + const std::string & str = expr.get_string(ID_value); + + std::ostringstream oss; + std::string::size_type i = 0; + for(const auto c : str) + { + oss << c; + if(++i % 8 == 0 && str.size() != i) + oss << ' '; + } + + return oss.str(); } else if(type.id()==ID_bool) { From 65f0ec043efde59140eb91481da9f37719738800 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 14:46:24 +0100 Subject: [PATCH 03/10] Provide a source location when analysis finds constness is lost --- src/analyses/does_remove_const.cpp | 8 ++++---- src/analyses/does_remove_const.h | 2 +- src/goto-programs/remove_function_pointers.cpp | 6 ++++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/analyses/does_remove_const.cpp b/src/analyses/does_remove_const.cpp index b012cef6167..8464980917c 100644 --- a/src/analyses/does_remove_const.cpp +++ b/src/analyses/does_remove_const.cpp @@ -31,7 +31,7 @@ does_remove_constt::does_remove_constt( /// A naive analysis to look for casts that remove const-ness from pointers. /// \return Returns true if the program contains a const-removing cast -bool does_remove_constt::operator()() const +std::pair does_remove_constt::operator()() const { for(const goto_programt::instructiont &instruction : goto_program.instructions) @@ -49,16 +49,16 @@ bool does_remove_constt::operator()() const // const that the lhs if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type)) { - return true; + return {true, assign.find_source_location()}; } if(does_expr_lose_const(assign.rhs())) { - return true; + return {true, assign.rhs().find_source_location()}; } } - return false; + return {false, source_locationt()}; } /// Search the expression tree to look for any children that have the same base diff --git a/src/analyses/does_remove_const.h b/src/analyses/does_remove_const.h index 5c54daec888..a80117c536d 100644 --- a/src/analyses/does_remove_const.h +++ b/src/analyses/does_remove_const.h @@ -22,7 +22,7 @@ class does_remove_constt { public: does_remove_constt(const goto_programt &goto_program, const namespacet &ns); - bool operator()() const; + std::pair operator()() const; private: bool does_expr_lose_const(const exprt &expr) const; diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index e426a36ad59..a69a3e5a4db 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -285,9 +285,11 @@ void remove_function_pointerst::remove_function_pointer( const exprt &pointer=function.op0(); remove_const_function_pointerst::functionst functions; does_remove_constt const_removal_check(goto_program, ns); - if(const_removal_check()) + const auto does_remove_const = const_removal_check(); + if(does_remove_const.first) { - warning() << "Cast from const to non-const pointer found, only worst case" + warning().source_location = does_remove_const.second; + warning() << "cast from const to non-const pointer found, only worst case" << " function pointer removal will be done." << eom; found_functions=false; } From 75f021c46d58caeb8418eca31c71cea8bb32f206 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 18:10:31 +0100 Subject: [PATCH 04/10] Print current depth in BMC progress debug logging --- src/cbmc/symex_bmc.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index abdda442a5b..a2a08be03b4 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -38,9 +38,8 @@ void symex_bmct::symex_step( if(!source_location.is_nil() && last_source_location!=source_location) { - log.debug() << "BMC at file " << source_location.get_file() << " line " - << source_location.get_line() << " function " - << source_location.get_function() << log.eom; + log.debug() << "BMC at " << source_location.as_string() + << " (depth " << state.depth << ')' << log.eom; last_source_location=source_location; } From 07ef32da141ffa1c18f76d5d65b32046a3a6ab94 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 18:25:01 +0100 Subject: [PATCH 05/10] remove_const_function_pointerst::functionst only holds symbol expressions --- src/goto-programs/remove_const_function_pointers.cpp | 2 +- src/goto-programs/remove_const_function_pointers.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index d113af01230..ec7fa86af20 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -160,7 +160,7 @@ bool remove_const_function_pointerst::try_resolve_function_call( { if(simplified_expr.type().id()==ID_code) { - resolved_functions.insert(simplified_expr); + resolved_functions.insert(to_symbol_expr(simplified_expr)); resolved=true; } else diff --git a/src/goto-programs/remove_const_function_pointers.h b/src/goto-programs/remove_const_function_pointers.h index 0299de8b383..ecffbefb921 100644 --- a/src/goto-programs/remove_const_function_pointers.h +++ b/src/goto-programs/remove_const_function_pointers.h @@ -32,7 +32,7 @@ class typecast_exprt; class remove_const_function_pointerst:public messaget { public: - typedef std::unordered_set functionst; + typedef std::unordered_set functionst; typedef std::list expressionst; remove_const_function_pointerst( message_handlert &message_handler, From e698be9163ad647be4a10b3f769961dec4988b0a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 18:25:20 +0100 Subject: [PATCH 06/10] Cleanup: use most suitable symbol_exprt constructor --- src/goto-programs/remove_function_pointers.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index a69a3e5a4db..5852a92b5fe 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -343,10 +343,8 @@ void remove_function_pointerst::remove_function_pointer( if(t.first=="pthread_mutex_cleanup") continue; - symbol_exprt expr; - expr.type()=t.second; - expr.set_identifier(t.first); - functions.insert(expr); + symbol_exprt expr(t.first, t.second); + functions.insert(expr); } } From 9717af2867492bd0510349af15627191c4c894b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Jun 2018 17:25:43 +0000 Subject: [PATCH 07/10] messaget helper to encapsulate if(debug-verbosity) { complex output } --- src/util/message.cpp | 18 ++++++++++++++++++ src/util/message.h | 7 ++++++- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/util/message.cpp b/src/util/message.cpp index dece45a2d9b..06c28b746ad 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -103,3 +103,21 @@ unsigned messaget::eval_verbosity( return v; } + +/// Generate output to \p mstream using \p output_generator if the configured +/// verbosity is at least as high as that of \p mstream. Use whenever +/// generating output involves additional computational effort that should only +/// be spent when such output will actually be displayed. +/// \param mstream Output message stream +/// \param output_generator Function generating output +void messaget::conditional_output( + mstreamt &mstream, + const std::function &output_generator) const +{ + if( + message_handler && + message_handler->get_verbosity() >= mstream.message_level) + { + output_generator(mstream); + } +} diff --git a/src/util/message.h b/src/util/message.h index a20b4cc3041..7f17398cc2d 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -10,9 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_MESSAGE_H #define CPROVER_UTIL_MESSAGE_H -#include +#include #include #include +#include #include "invariant.h" #include "json.h" @@ -333,6 +334,10 @@ class messaget return get_mstream(M_DEBUG); } + void conditional_output( + mstreamt &mstream, + const std::function &output_generator) const; + protected: message_handlert *message_handler; mutable mstreamt mstream; From e515f2674d628fdeabb5b29cd967811b16694261 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 18:25:56 +0100 Subject: [PATCH 08/10] List all candidate functions for a function pointer at debug verbosity --- .../remove_function_pointers.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 5852a92b5fe..3c63b54ff4d 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -430,6 +430,25 @@ void remove_function_pointerst::remove_function_pointer( statistics().source_location=target->source_location; statistics() << "replacing function pointer by " << functions.size() << " possible targets" << eom; + + // list the names of functions when verbosity is at debug level + conditional_output( + debug(), + [this, &functions](mstreamt &mstream) { + mstream << "targets: "; + + bool first = true; + for(const auto &function : functions) + { + if(!first) + mstream << ", "; + + mstream << function.get_identifier(); + first = false; + } + + mstream << eom; + }); } bool remove_function_pointerst::remove_function_pointers( From b0fce606ad078b7ed98eb35211b53741c76c1b22 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 18:56:55 +0100 Subject: [PATCH 09/10] Print (at debug level) the size of assignments during symex --- src/goto-symex/symex_assign.cpp | 12 ++++++++++-- src/goto-symex/symex_goto.cpp | 17 +++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 9642d148e56..6465fb9f7d3 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" #include -#include - #include +#include +#include #include "goto_symex_state.h" @@ -251,6 +251,14 @@ void goto_symext::symex_assign_symbol( if(symbol.is_auxiliary) assignment_type=symex_targett::assignment_typet::HIDDEN; + log.conditional_output( + log.debug(), + [this, &ssa_lhs](messaget::mstreamt &mstream) { + mstream << "Assignment to " << ssa_lhs.get_identifier() + << " [" << pointer_offset_bits(ssa_lhs.type(), ns) << " bits]" + << messaget::eom; + }); + target.assignment( tmp_guard.as_expr(), ssa_lhs, diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 517b749e163..115a10007f1 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -249,6 +250,14 @@ void goto_symext::symex_goto(statet &state) guardt guard; + log.conditional_output( + log.debug(), + [this, &new_lhs](messaget::mstreamt &mstream) { + mstream << "Assignment to " << new_lhs.get_identifier() + << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]" + << messaget::eom; + }); + target.assignment( guard.as_expr(), new_lhs, new_lhs, guard_symbol_expr, @@ -473,6 +482,14 @@ void goto_symext::phi_function( dest_state.assignment(new_lhs, rhs, ns, true, true); dest_state.record_events=record_events; + log.conditional_output( + log.debug(), + [this, &new_lhs](messaget::mstreamt &mstream) { + mstream << "Assignment to " << new_lhs.get_identifier() + << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]" + << messaget::eom; + }); + target.assignment( true_exprt(), new_lhs, new_lhs, new_lhs.get_original_expr(), From 6f51513a962c5e356157e90c4a97dc4a3ac51f0a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 May 2018 21:56:02 +0100 Subject: [PATCH 10/10] Print (at debug level) the current SSA step being converted --- src/goto-symex/symex_target_equation.cpp | 42 ++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 9554f1fd3a0..1f906f3f8d7 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -403,7 +403,17 @@ void symex_target_equationt::convert_assignments( for(const auto &step : SSA_steps) { if(step.is_assignment() && !step.ignore) + { + decision_procedure.conditional_output( + decision_procedure.debug(), + [&step](messaget::mstreamt &mstream) { + std::ostringstream oss; + step.output(oss); + mstream << oss.str() << messaget::eom; + }); + decision_procedure.set_to_true(step.cond_expr); + } } } @@ -443,6 +453,14 @@ void symex_target_equationt::convert_guards( step.guard_literal=const_literal(false); else { + prop_conv.conditional_output( + prop_conv.debug(), + [&step](messaget::mstreamt &mstream) { + std::ostringstream oss; + step.output(oss); + mstream << oss.str() << messaget::eom; + }); + try { step.guard_literal = prop_conv.convert(step.guard); @@ -470,6 +488,14 @@ void symex_target_equationt::convert_assumptions( step.cond_literal=const_literal(true); else { + prop_conv.conditional_output( + prop_conv.debug(), + [&step](messaget::mstreamt &mstream) { + std::ostringstream oss; + step.output(oss); + mstream << oss.str() << messaget::eom; + }); + try { step.cond_literal = prop_conv.convert(step.cond_expr); @@ -498,6 +524,14 @@ void symex_target_equationt::convert_goto_instructions( step.cond_literal=const_literal(true); else { + prop_conv.conditional_output( + prop_conv.debug(), + [&step](messaget::mstreamt &mstream) { + std::ostringstream oss; + step.output(oss); + mstream << oss.str() << messaget::eom; + }); + try { step.cond_literal = prop_conv.convert(step.cond_expr); @@ -525,6 +559,14 @@ void symex_target_equationt::convert_constraints( { if(!step.ignore) { + decision_procedure.conditional_output( + decision_procedure.debug(), + [&step](messaget::mstreamt &mstream) { + std::ostringstream oss; + step.output(oss); + mstream << oss.str() << messaget::eom; + }); + try { decision_procedure.set_to_true(step.cond_expr);