Symbol consistency between goto programs and symbol table

Iterate over all symbols in a goto program and for each one check that it is
present in the symbol table as well. Includes a unit test for the check.

Author: Petr Bauch

src/goto-programs/goto_function.h

@@ -117,7 +117,59 @@ class goto_functiont
   /// reported via DATA_INVARIANT violations or exceptions.
   void validate(const namespacet &ns, const validation_modet vm) const
   {
-    body.validate(ns, vm);
+    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)
+        {
+          const symbolt *symbol;
+          if(location.is_nil())
+            DATA_CHECK(
+              !ns.lookup(identifier, symbol),
+              id2string(identifier) + " not found");
+          else
+            DATA_CHECK_WITH_DIAGNOSTICS(
+              !ns.lookup(identifier, symbol),
+              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)
+        {
+          const symbolt *symbol;
+          auto identifier = to_symbol_expr(e).get_identifier();
+          DATA_CHECK_WITH_DIAGNOSTICS(
+            !ns.lookup(identifier, symbol),
+            id2string(identifier) + " not found",
+            location);
+        }
+      };
+
+    body.validate(expr_symbol_finder, ns, vm);
+    source_locationt nil_location;
+    nil_location.make_nil();
+    forall_subtypes(it, type)
+    {
+      type_symbol_finder(*it, nil_location);
+    }
+
     validate_full_type(type, ns, vm);
   }
 };

src/goto-programs/goto_program.cpp

@@ -670,12 +670,24 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
 }
 
 void goto_programt::instructiont::validate(
+  const std::function<void(const exprt &, const source_locationt &)>
+    &symbol_finder,
   const namespacet &ns,
   const validation_modet vm) const
 {
   validate_full_code(code, ns, vm);
   validate_full_expr(guard, ns, vm);
 
+  const symbolt *symbol;
+  DATA_CHECK_WITH_DIAGNOSTICS(
+    !ns.lookup(function, symbol),
+    id2string(function) + " not found",
+    source_location);
+
+  auto expr_symbol_finder = [&](const exprt &e) {
+    symbol_finder(e, source_location);
+  };
+
   switch(type)
   {
   case NO_INSTRUCTION_TYPE:
@@ -685,6 +697,7 @@ void goto_programt::instructiont::validate(
   case ASSUME:
     break;
   case ASSERT:
+    guard.visit(expr_symbol_finder);
     break;
   case OTHER:
     break;
@@ -715,6 +728,7 @@ void goto_programt::instructiont::validate(
   case DEAD:
     break;
   case FUNCTION_CALL:
+    code.visit(expr_symbol_finder);
     break;
   case THROW:
     break;

src/goto-programs/goto_program.h

@@ -405,7 +405,11 @@ class goto_programt
     ///
     /// The validation mode indicates whether well-formedness check failures are
     /// reported via DATA_INVARIANT violations or exceptions.
-    void validate(const namespacet &ns, const validation_modet vm) const;
+    void validate(
+      const std::function<void(const exprt &, const source_locationt &)>
+        &symbol_finder,
+      const namespacet &ns,
+      const validation_modet vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -690,11 +694,15 @@ class goto_programt
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const namespacet &ns, const validation_modet vm) const
+  void validate(
+    const std::function<void(const exprt &, const source_locationt &)>
+      &symbol_finder,
+    const namespacet &ns,
+    const validation_modet vm) const
   {
     for(const instructiont &ins : instructions)
     {
-      ins.validate(ns, vm);
+      ins.validate(symbol_finder, ns, vm);
     }
   }
 };

src/util/expr.cpp

@@ -327,6 +327,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

@@ -309,6 +309,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();

unit/Makefile

@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        compound_block_locations.cpp \
        goto-programs/goto_trace_output.cpp \
+       goto-programs/goto_program_table_consistency.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_table_consistency.cpp

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+  Module: Unit tests for goto_program::validate
+  Author: Diffblue Ltd.
+
+ \*******************************************************************/
+
+#include <goto-programs/goto_function.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of consistent program/table pair",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assertion")
+  {
+    symbol_tablet symbol_table;
+    const typet type = signedbv_typet(32);
+    symbolt symbol;
+    irep_idt symbol_name = "a";
+    symbol.name = symbol_name;
+    symbol_exprt varx(symbol_name, type);
+    symbolt function_symbol;
+    irep_idt function_name = "fun";
+    function_symbol.name = function_name;
+
+    exprt val10 = from_integer(10, type);
+    binary_relation_exprt x_le_10(varx, ID_le, val10);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
+    instructions.back().make_assertion(x_le_10);
+    instructions.back().function = function_symbol.name;
+
+    symbol_table.insert(function_symbol);
+    WHEN("Symbol table has the right symbol")
+    {
+      symbol_table.insert(symbol);
+      const namespacet ns(symbol_table);
+      THEN("The consistency check succeeds")
+      {
+        goto_function.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+    WHEN("Symbol table does not have the symbol")
+    {
+      const namespacet ns(symbol_table);
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_function.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}