Small rework to allow further invariant checking

This commit follows the style of PR diffblue#918 in terms of case analysis of goto
instructions. The errors are now directly send to messaget instance and source
location are added. No functionality was added, just a different form.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -517,8 +517,8 @@ int cbmc_parse_optionst::doit()
     return get_goto_program_ret;
 
   INVARIANT(
-    goto_model.check_id_consistency_symbol_table(),
-    "identifier inconsistency between goto program and symbol table");
+    !goto_model.check_internal_invariants(*this),
+    "goto program internal invariants failed");
 
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one

src/goto-programs/goto_function.h

@@ -111,11 +111,10 @@ class goto_functiont
     return *this;
   }
 
-  void check_id_consistency_symbol_table(
-    const symbol_tablet &table,
-    std::vector<std::string> &message_collector) const
+  bool
+  check_internal_invariants(const symbol_tablet &table, messaget &msg) const
   {
-    body.check_id_consistency_symbol_table(table, message_collector);
+    return body.check_internal_invariants(table, msg);
   }
 };
 

src/goto-programs/goto_model.h

@@ -14,12 +14,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
 
-#include <iostream>
-
 // A model is a pair consisting of a symbol table
 // and the CFGs for the functions.
 
@@ -98,27 +97,19 @@ class goto_modelt : public abstract_goto_modelt
            goto_functions.function_map.end();
   }
 
-  /// Iterates over the symbols in this goto-model and checks that each one is
-  /// present in the symbol table.
-  /// \return true if no inconsistency was found
-  bool check_id_consistency_symbol_table() const
+  /// Iterates over the functions inside the goto model and checks invariants
+  /// in all of them. Prints out error message collected.
+  /// \param msg message instance to collect errors
+  /// \return true if any violation was found
+  bool check_internal_invariants(messaget &msg) const
   {
-    std::vector<std::string> message_collector;
+    bool found_violation = false;
     forall_goto_functions(it, goto_functions)
     {
-      it->second.check_id_consistency_symbol_table(
-        symbol_table, message_collector);
-    }
-    if(!message_collector.empty())
-    {
-      std::cerr << "Error messages collected while checking the goto "
-                   "program/symbol table\n consistency:\n";
-      for(const auto &m : message_collector)
-        std::cerr << m << std::endl;
-      return false;
+      found_violation = found_violation ||
+                        it->second.check_internal_invariants(symbol_table, msg);
     }
-    else
-      return true;
+    return found_violation;
   }
 };
 

src/goto-programs/goto_program.cpp

@@ -668,26 +668,63 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
-void goto_programt::instructiont::check_id_consistency_symbol_table(
+bool goto_programt::instructiont::check_internal_invariants(
   const symbol_tablet &table,
-  std::vector<std::string> &message_collector) const
+  messaget &msg) const
 {
+  bool found_violation = false;
+  std::vector<std::string> id_collector;
   auto symbol_finder = [&](const exprt &e) {
     if(e.id() == ID_symbol)
     {
       auto symbol_expr = to_symbol_expr(e);
       if(!table.has_symbol(symbol_expr.get_identifier()))
-        message_collector.push_back(
-          id2string(symbol_expr.get_identifier()) + " not found");
+        id_collector.push_back(id2string(symbol_expr.get_identifier()));
     }
   };
 
-  code.visit(symbol_finder);
   if(!table.has_symbol(function))
+    id_collector.push_back(id2string(function));
+
+  switch(type)
+  {
+  case GOTO:
+  case ASSUME:
+  case ASSERT:
+    guard.visit(symbol_finder);
+    break;
+  case ASSIGN:
+  case DECL:
+  case DEAD:
+  case FUNCTION_CALL:
+    code.visit(symbol_finder);
+    break;
+  case OTHER:
+  case SKIP:
+  case LOCATION:
+  case END_FUNCTION:
+  case START_THREAD:
+  case END_THREAD:
+  case ATOMIC_BEGIN:
+  case ATOMIC_END:
+  case RETURN:
+  case THROW:
+  case CATCH:
+  case NO_INSTRUCTION_TYPE:
+  case INCOMPLETE_GOTO:
+    break;
+  }
+
+  if(!id_collector.empty())
   {
-    message_collector.push_back("function id not found");
+    for(const auto &id : id_collector)
+    {
+      msg.error() << id << " not found (" << source_location << ")"
+                  << messaget::eom;
+    }
+    found_violation = true;
   }
-  guard.visit(symbol_finder);
+  return found_violation;
 }
 
 bool goto_programt::equals(const goto_programt &other) const
@@ -721,14 +758,17 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
-void goto_programt::check_id_consistency_symbol_table(
+bool goto_programt::check_internal_invariants(
   const symbol_tablet &table,
-  std::vector<std::string> &message_collector) const
+  messaget &msg) const
 {
+  bool found_violation = false;
   forall_goto_program_instructions(it, (*this))
   {
-    it->check_id_consistency_symbol_table(table, message_collector);
+    found_violation =
+      found_violation || it->check_internal_invariants(table, msg);
   }
+  return found_violation;
 }
 
 /// Outputs a string representation of a `goto_program_instruction_typet`

src/goto-programs/goto_program.h

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/message.h>
 
 /// The type of an instruction in a GOTO program.
 enum goto_program_instruction_typet
@@ -402,10 +403,10 @@ class goto_programt
     /// Iterate over code and guard and collect inconsistencies with symbol
     /// table.
     /// \param table the symbol table
-    /// \param message_collector container to store the error messages
-    void check_id_consistency_symbol_table(
-      const symbol_tablet &table,
-      std::vector<std::string> &message_collector) const;
+    /// \param msg container to store the error messages
+    /// \return true if any violation was found
+    bool
+    check_internal_invariants(const symbol_tablet &table, messaget &msg) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -686,9 +687,8 @@ class goto_programt
   /// and relative jumps have the same distance.
   bool equals(const goto_programt &other) const;
 
-  void check_id_consistency_symbol_table(
-    const symbol_tablet &table,
-    std::vector<std::string> &message_collector) const;
+  bool
+  check_internal_invariants(const symbol_tablet &table, messaget &msg) const;
 };
 
 /// Get control-flow successors of a given instruction. The instruction is