Type consistency between goto programs and symbol table

This first commit is just PR #3118 to reuse the common structure of checking
this kind of consistency.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -515,6 +515,10 @@ 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
   {

src/goto-programs/goto_function.h

@@ -110,6 +110,12 @@ class goto_functiont
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }
+
+  bool
+  check_internal_invariants(const symbol_tablet &table, messaget &msg) const
+  {
+    return body.check_internal_invariants(table, msg);
+  }
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_model.h

@@ -14,6 +14,7 @@ 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"
@@ -95,6 +96,21 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            goto_functions.function_map.end();
   }
+
+  /// 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
+  {
+    bool found_violation = false;
+    forall_goto_functions(it, goto_functions)
+    {
+      found_violation = found_violation ||
+                        it->second.check_internal_invariants(symbol_table, msg);
+    }
+    return found_violation;
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/goto-programs/goto_program.cpp

@@ -668,6 +668,65 @@ 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
+{
+  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()));
+    }
+  };
+
+  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())
+  {
+    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
 {
   if(instructions.size() != other.instructions.size())
@@ -699,6 +758,19 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
+bool goto_programt::check_internal_invariants(
+  const symbol_tablet &table,
+  messaget &msg) const
+{
+  bool found_violation = false;
+  forall_goto_program_instructions(it, (*this))
+  {
+    found_violation =
+      found_violation || it->check_internal_invariants(table, msg);
+  }
+  return found_violation;
+}
+
 /// Outputs a string representation of a `goto_program_instruction_typet`
 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
 {

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
@@ -398,6 +399,14 @@ class goto_programt
     /// only be evaluated in the context of a goto_programt (see
     /// goto_programt::equals).
     bool equals(const instructiont &other) const;
+
+    /// 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;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -677,6 +686,9 @@ class goto_programt
   /// the same number of instructions, each pair of instructions compares equal,
   /// 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;
 };
 
 /// Get control-flow successors of a given instruction. The instruction is

src/util/expr.cpp

@@ -322,6 +322,24 @@ void exprt::visit(const_expr_visitort &visitor) const
   }
 }
 
+void exprt::visit(const std::function<void(const exprt &)> &f) const
+{
+  std::stack<const exprt *> stack;
+
+  stack.push(this);
+
+  while(!stack.empty())
+  {
+    const exprt &expr = *stack.top();
+    stack.pop();
+
+    f(expr);
+
+    forall_operands(it, expr)
+      stack.push(&(*it));
+  }
+}
+
 depth_iteratort exprt::depth_begin()
 { return depth_iteratort(*this); }
 depth_iteratort exprt::depth_end()

src/util/expr.h

@@ -224,6 +224,7 @@ class exprt:public irept
 public:
   void visit(class expr_visitort &visitor);
   void visit(class const_expr_visitort &visitor) const;
+  void visit(const std::function<void(const exprt &)> &f) const;
 
   depth_iteratort depth_begin();
   depth_iteratort depth_end();