Program table symbol type consistency

Look up the symbol id in symbol table and call base_type_eq on every symbol
expression in guard and code whenever relevant. Includes a unit test.

Author: Petr Bauch

src/goto-programs/goto_functions.h

@@ -130,6 +130,7 @@ class goto_functionst
       const auto &function_name = entry.first;
 
       DATA_CHECK(
+        vm,
         goto_function.type == ns.lookup(function_name).type,
         id2string(function_name) + " type inconsistency\ngoto program type: " +
           goto_function.type.id_string() +

src/goto-programs/goto_program.cpp

@@ -677,9 +677,10 @@ void goto_programt::instructiont::validate(
   validate_full_code(code, ns, vm);
   validate_full_expr(guard, ns, vm);
 
-  const symbolt *symbol;
+  const symbolt *table_symbol;
   DATA_CHECK_WITH_DIAGNOSTICS(
-    !ns.lookup(function, symbol),
+    vm,
+    !ns.lookup(function, table_symbol),
     id2string(function) + " not found",
     source_location);
 
@@ -691,6 +692,25 @@ void goto_programt::instructiont::validate(
     find_symbol_in_namespace(e, source_location, ns, vm);
   };
 
+  auto &current_source_location = source_location;
+  auto type_finder =
+    [&ns, vm, &table_symbol, &current_source_location](const exprt &e) {
+      if(e.id() == ID_symbol)
+      {
+        const auto &goto_symbol_expr = to_symbol_expr(e);
+        const auto &goto_id = goto_symbol_expr.get_identifier();
+
+        if(!ns.lookup(goto_id, table_symbol))
+          DATA_CHECK_WITH_DIAGNOSTICS(
+            vm,
+            base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns),
+            id2string(goto_id) + " type inconsistency\n" +
+              "goto program type: " + goto_symbol_expr.type().id_string() +
+              "\n" + "symbol table type: " + table_symbol->type.id_string(),
+            current_source_location);
+      }
+    };
+
   switch(type)
   {
   case NO_INSTRUCTION_TYPE:
@@ -701,6 +721,7 @@ void goto_programt::instructiont::validate(
     break;
   case ASSERT:
     guard.visit(expr_symbol_finder);
+    guard.visit(type_finder);
     break;
   case OTHER:
     break;
@@ -734,6 +755,7 @@ void goto_programt::instructiont::validate(
     break;
   case FUNCTION_CALL:
     code.visit(expr_symbol_finder);
+    code.visit(type_finder);
     break;
   case THROW:
     break;

src/util/find_symbols.cpp

@@ -233,9 +233,12 @@ void find_typetag_in_namespace(
     const symbolt *symbol;
     if(location.is_nil())
       DATA_CHECK(
-        !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found");
     else
       DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         !ns.lookup(identifier, symbol),
         id2string(identifier) + " not found",
         location);
@@ -253,6 +256,7 @@ void find_symbol_in_namespace(
     const symbolt *symbol;
     auto identifier = to_symbol_expr(src).get_identifier();
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       !ns.lookup(identifier, symbol),
       id2string(identifier) + " not found",
       location);

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_model_function_type_consistency.cpp \
+       goto-programs/goto_program_symbol_type_table_consistency.cpp \
        goto-programs/goto_program_table_consistency.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-symex/ssa_equation.cpp \

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ 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 (type-wise)",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assertion")
+  {
+    symbol_tablet symbol_table;
+    const typet type1 = signedbv_typet(32);
+    const typet type2 = signedbv_typet(64);
+    symbolt symbol;
+    irep_idt symbol_name = "a";
+    symbol.name = symbol_name;
+    symbol_exprt varx(symbol_name, type1);
+    symbolt function_symbol;
+    irep_idt function_name = "fun";
+    function_symbol.name = function_name;
+
+    exprt val10 = from_integer(10, type1);
+    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 type")
+    {
+      symbol.type = type1;
+      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 has the wrong symbol type")
+    {
+      symbol.type = type2;
+      symbol_table.insert(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);
+      }
+    }
+  }
+}

unit/goto-programs/goto_program_table_consistency.cpp

@@ -37,6 +37,7 @@ SCENARIO(
     symbol_table.insert(function_symbol);
     WHEN("Symbol table has the right symbol")
     {
+      symbol.type = type;
       symbol_table.insert(symbol);
       const namespacet ns(symbol_table);
       THEN("The consistency check succeeds")