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

@@ -16,6 +16,7 @@ Date: May 2018
 
 #include <iosfwd>
 
+#include <util/find_symbols.h>
 #include <util/std_types.h>
 
 #include "goto_program.h"
@@ -118,6 +119,13 @@ class goto_functiont
   void validate(const namespacet &ns, const validation_modet vm) const
   {
     body.validate(ns, vm);
+    source_locationt nil_location;
+    nil_location.make_nil();
+    forall_subtypes(it, type)
+    {
+      find_typetag_in_namespace(*it, nil_location, ns, vm);
+    }
+
     validate_full_type(type, ns, vm);
   }
 };

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/find_symbols.h>
 #include <util/std_expr.h>
 #include <util/validate.h>
 
@@ -676,6 +677,20 @@ void goto_programt::instructiont::validate(
   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) {
+    forall_subtypes(it, e.type())
+    {
+      find_typetag_in_namespace(*it, source_location, ns, vm);
+    }
+    find_symbol_in_namespace(e, source_location, ns, vm);
+  };
+
   switch(type)
   {
   case NO_INSTRUCTION_TYPE:
@@ -685,6 +700,7 @@ void goto_programt::instructiont::validate(
   case ASSUME:
     break;
   case ASSERT:
+    guard.visit(expr_symbol_finder);
     break;
   case OTHER:
     break;
@@ -717,6 +733,7 @@ void goto_programt::instructiont::validate(
   case DEAD:
     break;
   case FUNCTION_CALL:
+    code.visit(expr_symbol_finder);
     break;
   case THROW:
     break;

src/util/find_symbols.cpp

@@ -210,3 +210,51 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 {
   find_symbols(kindt::F_BOTH, src, dest);
 }
+
+void find_typetag_in_namespace(
+  const typet &src,
+  const source_locationt &location,
+  const namespacet &ns,
+  const validation_modet vm)
+{
+  irep_idt identifier = ID_nil;
+  if(src.id() == ID_symbol_type)
+  {
+    identifier = to_symbol_type(src).get_identifier();
+  }
+  else if(
+    src.id() == ID_c_enum_tag || src.id() == ID_struct_tag ||
+    src.id() == ID_union_tag)
+  {
+    identifier = to_tag_type(src).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);
+  }
+}
+
+void find_symbol_in_namespace(
+  const exprt &src,
+  const source_locationt &location,
+  const namespacet &ns,
+  const validation_modet vm)
+{
+  if(src.id() == ID_symbol)
+  {
+    const symbolt *symbol;
+    auto identifier = to_symbol_expr(src).get_identifier();
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      !ns.lookup(identifier, symbol),
+      id2string(identifier) + " not found",
+      location);
+  }
+}

src/util/find_symbols.h

@@ -14,10 +14,14 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include "irep.h"
+#include "namespace.h"
+#include "validate.h"
 
 class exprt;
 class symbol_exprt;
 class typet;
+class symbolt;
+class source_locationt;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
@@ -67,4 +71,16 @@ void find_type_and_expr_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
+void find_typetag_in_namespace(
+  const typet &src,
+  const source_locationt &location,
+  const namespacet &ns,
+  const validation_modet vm);
+
+void find_symbol_in_namespace(
+  const exprt &src,
+  const source_locationt &location,
+  const namespacet &ns,
+  const validation_modet vm);
+
 #endif // CPROVER_UTIL_FIND_SYMBOLS_H

unit/Makefile

@@ -15,6 +15,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        compound_block_locations.cpp \
+       goto-programs/goto_program_table_consistency.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-symex/ssa_equation.cpp \
        interpreter/interpreter.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);
+      }
+    }
+  }
+}