Cleanup and extend user-directed output

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<bool, source_locationt> 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

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<bool, source_locationt>  operator()() const;
 
 private:
   bool does_expr_lose_const(const exprt &expr) const;

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;
   }

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)
     {

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(

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

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<exprt, irep_hash> functionst;
+  typedef std::unordered_set<symbol_exprt, irep_hash> functionst;
   typedef std::list<exprt> expressionst;
   remove_const_function_pointerst(
     message_handlert &message_handler,

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;
   }
@@ -341,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);
     }
   }
 
@@ -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(

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())

src/goto-symex/symex_assign.cpp

@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/byte_operators.h>
-#include <util/cprover_prefix.h>
-
 #include <util/c_types.h>
+#include <util/cprover_prefix.h>
+#include <util/pointer_offset_size.h>
 
 #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,

src/goto-symex/symex_goto.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/invariant.h>
+#include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
@@ -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(),

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);

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<void(mstreamt &)> &output_generator) const
+{
+  if(
+    message_handler &&
+    message_handler->get_verbosity() >= mstream.message_level)
+  {
+    output_generator(mstream);
+  }
+}

src/util/message.h

@@ -10,9 +10,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_MESSAGE_H
 #define CPROVER_UTIL_MESSAGE_H
 
-#include <string>
+#include <functional>
 #include <iosfwd>
 #include <sstream>
+#include <string>
 
 #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<void(mstreamt &)> &output_generator) const;
+
 protected:
   message_handlert *message_handler;
   mutable mstreamt mstream;