Symbol consistency between goto programs and symbol table

Introduce a chain of methods that (at the lowest level) iterate over all symbols
in a goto program and for each one check that it is present in the symbol table
as well. On the lower levels, the methods collect inconsistency messages and
print them to error output. On the top level, e.g. cbmc-parser, they return a
Boolean value to be caught by an invariant check.

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_id_consistency_symbol_table(),
+    "identifier inconsistency between goto program and symbol table");
+
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {

src/goto-programs/goto_function.h

@@ -110,6 +110,13 @@ class goto_functiont
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }
+
+  void check_id_consistency_symbol_table(
+    const symbol_tablet &table,
+    std::vector<std::string> &message_collector) const
+  {
+    body.check_id_consistency_symbol_table(table, message_collector);
+  }
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_model.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #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.
 
@@ -95,6 +97,29 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            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
+  {
+    std::vector<std::string> message_collector;
+    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;
+    }
+    else
+      return true;
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/goto-programs/goto_program.cpp

@@ -668,6 +668,28 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
+void goto_programt::instructiont::check_id_consistency_symbol_table(
+  const symbol_tablet &table,
+  std::vector<std::string> &message_collector) const
+{
+  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");
+    }
+  };
+
+  code.visit(symbol_finder);
+  if(!table.has_symbol(function))
+  {
+    message_collector.push_back("function id not found");
+  }
+  guard.visit(symbol_finder);
+}
+
 bool goto_programt::equals(const goto_programt &other) const
 {
   if(instructions.size() != other.instructions.size())
@@ -699,6 +721,16 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
+void goto_programt::check_id_consistency_symbol_table(
+  const symbol_tablet &table,
+  std::vector<std::string> &message_collector) const
+{
+  forall_goto_program_instructions(it, (*this))
+  {
+    it->check_id_consistency_symbol_table(table, message_collector);
+  }
+}
+
 /// 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

@@ -398,6 +398,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 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;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -677,6 +685,10 @@ 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;
+
+  void check_id_consistency_symbol_table(
+    const symbol_tablet &table,
+    std::vector<std::string> &message_collector) 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();