Reworked based on the well-formedness checking skeleton of PR #3123

The condition to be checked is the same. Interface function name was changed to
follow the above PR. Also the check is now optional via command line.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -515,10 +515,6 @@ int cbmc_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
-  INVARIANT(
-    !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
   {
@@ -530,6 +526,12 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    namespacet ns(goto_model.symbol_table);
+    goto_model.validate(ns, validation_modet::INVARIANT);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -976,6 +978,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --validate-goto-model        enables additional well-formedness checks on the goto program\n" // NOLINT(*)
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -72,6 +72,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  "(validate-goto-model)" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-programs/goto_function.h

@@ -111,10 +111,9 @@ class goto_functiont
     return *this;
   }
 
-  bool
-  check_internal_invariants(const symbol_tablet &table, messaget &msg) const
+  void validate(const symbol_tablet &table, const validation_modet &vm) const
   {
-    return body.check_internal_invariants(table, msg);
+    return body.validate(table, vm);
   }
 };
 

src/goto-programs/goto_model.h

@@ -99,17 +99,14 @@ class goto_modelt : public abstract_goto_modelt
 
   /// 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
+  /// \param ns namespace for the environment
+  /// \param vm validation mode to be used for error reporting
+  void validate(const namespacet &ns, const validation_modet &vm) const
   {
-    bool found_violation = false;
     forall_goto_functions(it, goto_functions)
     {
-      found_violation = found_violation ||
-                        it->second.check_internal_invariants(symbol_table, msg);
+      it->second.validate(symbol_table, vm);
     }
-    return found_violation;
   }
 };
 

src/goto-programs/goto_program.cpp

@@ -669,25 +669,29 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
-bool goto_programt::instructiont::check_internal_invariants(
+void goto_programt::instructiont::validate(
   const symbol_tablet &table,
-  messaget &msg) const
+  const validation_modet &vm) const
 {
   namespacet ns(table);
-  bool found_violation = false;
   std::vector<std::vector<std::string>> type_collector;
+  std::stringstream location_stream;
+  location_stream << source_location;
+
   auto type_finder = [&](const exprt &e) {
     if(e.id() == ID_symbol)
     {
       auto symbol_expr = to_symbol_expr(e);
       const auto &symbol_id = symbol_expr.get_identifier();
-      if(
-        table.has_symbol(symbol_id) &&
-        !base_type_eq(symbol_expr.type(), table.lookup_ref(symbol_id).type, ns))
-        type_collector.push_back(
-          {id2string(symbol_id),
-           symbol_expr.type().id_string(),
-           table.lookup_ref(symbol_id).type.id_string()});
+
+      if(table.has_symbol(symbol_id))
+        DATA_CHECK(
+          base_type_eq(
+            symbol_expr.type(), table.lookup_ref(symbol_id).type, ns),
+          id2string(symbol_id) + " type inconsistency (" +
+            location_stream.str() + ")\n" + "goto program type: " +
+            symbol_expr.type().id_string() + "\n " + "symbol table type: " +
+            table.lookup_ref(symbol_id).type.id_string());
     }
   };
 
@@ -719,20 +723,6 @@ bool goto_programt::instructiont::check_internal_invariants(
   case INCOMPLETE_GOTO:
     break;
   }
-
-  if(!type_collector.empty())
-  {
-    for(const auto &type_triple : type_collector)
-    {
-      INVARIANT(type_triple.size() > 2, "should have 3 elements");
-      msg.error() << type_triple[0] << " type inconsistency ("
-                  << source_location << ")\n"
-                  << "goto program type: " << type_triple[1] << "\n "
-                  << "symbol table type: " << type_triple[2] << messaget::eom;
-    }
-    found_violation = true;
-  }
-  return found_violation;
 }
 
 bool goto_programt::equals(const goto_programt &other) const
@@ -766,17 +756,14 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
-bool goto_programt::check_internal_invariants(
+void goto_programt::validate(
   const symbol_tablet &table,
-  messaget &msg) const
+  const validation_modet &vm) const
 {
-  bool found_violation = false;
   forall_goto_program_instructions(it, (*this))
   {
-    found_violation =
-      found_violation || it->check_internal_invariants(table, msg);
+    it->validate(table, vm);
   }
-  return found_violation;
 }
 
 /// Outputs a string representation of a `goto_program_instruction_typet`

src/goto-programs/goto_program.h

@@ -403,10 +403,8 @@ class goto_programt
     /// Iterate over code and guard and collect inconsistencies with symbol
     /// table.
     /// \param table the symbol table
-    /// \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;
+    /// \param vm validation mode
+    void validate(const symbol_tablet &table, const validation_modet &vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -687,8 +685,7 @@ class goto_programt
   /// and relative jumps have the same distance.
   bool equals(const goto_programt &other) const;
 
-  bool
-  check_internal_invariants(const symbol_tablet &table, messaget &msg) const;
+  void validate(const symbol_tablet &table, const validation_modet &vm) const;
 };
 
 /// Get control-flow successors of a given instruction. The instruction is

src/util/expr.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_EXPR_H
 
 #include "type.h"
+#include "validate.h"
 
 #include <functional>
 #include <list>