Merge pull request #2184 from tautschnig/human-readable-output

Cleanup and extend user-directed output

Author: tautschnig

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,