Add checks that type identifiers are consistent

Moved the checking functions to goto_function to be more easily reusable. Added
check for type variable inside goto_functions and all types in expressions in
goto programs.

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,62 @@ class goto_functiont
     return *this;
   }
 
-  bool
-  check_internal_invariants(const symbol_tablet &table, messaget &msg) const
+  /// Iterates over the functions inside the goto model and checks invariants
+  /// in all of them. Prints out error message collected.
+  /// \param table symbol table to be checked for consistency
+  /// \param vm validation mode to be used for error reporting
+  void validate(const symbol_tablet &table, const validation_modet &vm) const
   {
-    return body.check_internal_invariants(table, msg);
+    auto type_symbol_finder = [&](
+      const typet &t, const source_locationt &location) {
+      irep_idt identifier = ID_nil;
+      if(t.id() == ID_symbol_type)
+      {
+        identifier = to_symbol_type(t).get_identifier();
+      }
+      else if(
+        t.id() == ID_c_enum_tag || t.id() == ID_struct_tag ||
+        t.id() == ID_union_tag)
+      {
+        identifier = to_tag_type(t).get_identifier();
+      }
+      if(identifier != ID_nil)
+      {
+        if(location.is_nil())
+          DATA_CHECK(
+            table.has_symbol(identifier), id2string(identifier) + " not found");
+        else
+          DATA_CHECK_WITH_DIAGNOSTICS(
+            table.has_symbol(identifier),
+            id2string(identifier) + " not found",
+            location);
+      }
+    };
+
+    auto expr_symbol_finder =
+      [&](const exprt &e, const source_locationt &location) {
+        forall_subtypes(it, e.type())
+        {
+          type_symbol_finder(*it, location);
+        }
+        if(e.id() == ID_symbol)
+        {
+          auto identifier = to_symbol_expr(e).get_identifier();
+          DATA_CHECK_WITH_DIAGNOSTICS(
+            table.has_symbol(identifier),
+            id2string(identifier) + " not found",
+            location);
+        }
+      };
+
+    body.validate(expr_symbol_finder, vm);
+
+    source_locationt nil_location;
+    nil_location.make_nil();
+    forall_subtypes(it, type)
+    {
+      type_symbol_finder(*it, nil_location);
+    }
   }
 };
 

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

@@ -668,36 +668,27 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
-bool goto_programt::instructiont::check_internal_invariants(
-  const symbol_tablet &table,
-  messaget &msg) const
+void goto_programt::instructiont::validate(
+  const std::function<void(const exprt &, const source_locationt &)>
+    &symbol_finder,
+  const validation_modet &vm) 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()))
-        id_collector.push_back(id2string(symbol_expr.get_identifier()));
-    }
+  auto expr_symbol_finder = [&](const exprt &e) {
+    symbol_finder(e, source_location);
   };
 
-  if(!table.has_symbol(function))
-    id_collector.push_back(id2string(function));
-
   switch(type)
   {
   case GOTO:
   case ASSUME:
   case ASSERT:
-    guard.visit(symbol_finder);
+    guard.visit(expr_symbol_finder);
     break;
   case ASSIGN:
   case DECL:
   case DEAD:
   case FUNCTION_CALL:
-    code.visit(symbol_finder);
+    code.visit(expr_symbol_finder);
     break;
   case OTHER:
   case SKIP:
@@ -714,17 +705,6 @@ bool goto_programt::instructiont::check_internal_invariants(
   case INCOMPLETE_GOTO:
     break;
   }
-
-  if(!id_collector.empty())
-  {
-    for(const auto &id : id_collector)
-    {
-      msg.error() << id << " not found (" << source_location << ")"
-                  << messaget::eom;
-    }
-    found_violation = true;
-  }
-  return found_violation;
 }
 
 bool goto_programt::equals(const goto_programt &other) const
@@ -758,17 +738,15 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
-bool goto_programt::check_internal_invariants(
-  const symbol_tablet &table,
-  messaget &msg) const
+void goto_programt::validate(
+  const std::function<void(const exprt &, const source_locationt &)>
+    &symbol_finder,
+  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(symbol_finder, vm);
   }
-  return found_violation;
 }
 
 /// Outputs a string representation of a `goto_program_instruction_typet`

src/goto-programs/goto_program.h

@@ -402,11 +402,12 @@ 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 symbol_finder function that locates symbols in a symbol table
+    /// \param vm validation mode
+    void validate(
+      const std::function<void(const exprt &, const source_locationt &)>
+        &symbol_finder,
+      const validation_modet &vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -687,8 +688,10 @@ 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 std::function<void(const exprt &, const source_locationt &)>
+      &symbol_finder,
+    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>