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

@@ -678,7 +678,8 @@ void goto_programt::instructiont::validate(
   validate_full_expr(guard, ns, vm);
 
   const symbolt *table_symbol;
-  DATA_CHECK_WITH_DIAGNOSTICS(vm,
+  DATA_CHECK_WITH_DIAGNOSTICS(
+    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:
@@ -723,6 +743,7 @@ void goto_programt::instructiont::validate(
       source_location);
 
     guard.visit(expr_symbol_finder);
+    guard.visit(type_finder);
     break;
   case OTHER:
     break;
@@ -789,6 +810,7 @@ void goto_programt::instructiont::validate(
       source_location);
 
     code.visit(expr_symbol_finder);
+    code.visit(type_finder);
     break;
   case THROW:
     break;

src/util/find_symbols.cpp

@@ -232,10 +232,13 @@ void find_typetag_in_namespace(
   {
     const symbolt *symbol;
     if(location.is_nil())
-      DATA_CHECK(vm,
-        !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
+      DATA_CHECK(
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found");
     else
-      DATA_CHECK_WITH_DIAGNOSTICS(vm,
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         !ns.lookup(identifier, symbol),
         id2string(identifier) + " not found",
         location);
@@ -252,7 +255,8 @@ void find_symbol_in_namespace(
   {
     const symbolt *symbol;
     auto identifier = to_symbol_expr(src).get_identifier();
-    DATA_CHECK_WITH_DIAGNOSTICS(vm,
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       !ns.lookup(identifier, symbol),
       id2string(identifier) + " not found",
       location);

unit/Makefile

@@ -21,6 +21,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_function_call.cpp \
        goto-programs/goto_program_goto_target.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_assume.cpp

@@ -19,6 +19,9 @@ SCENARIO(
     symbol_tablet symbol_table;
     const typet type1 = signedbv_typet(32);
     symbolt symbol;
+    symbolt fun_symbol;
+    irep_idt fun_name = "foo";
+    fun_symbol.name = fun_name;
     irep_idt symbol_name = "a";
     symbol.name = symbol_name;
     symbol_exprt varx(symbol_name, type1);
@@ -31,8 +34,10 @@ SCENARIO(
 
     symbol.type = type1;
     symbol_table.insert(symbol);
+    symbol_table.insert(fun_symbol);
     namespacet ns(symbol_table);
     instructions.back().make_assertion(x_le_10);
+    instructions.back().function = fun_name;
 
     WHEN("Instruction has no targets")
     {

unit/goto-programs/goto_program_dead.cpp

@@ -19,6 +19,10 @@ SCENARIO(
     symbol_tablet symbol_table;
     const signedbv_typet type1(32);
 
+    symbolt fun_symbol;
+    irep_idt fun_name = "foo";
+    fun_symbol.name = fun_name;
+
     symbolt var_symbol;
     irep_idt var_symbol_name = "a";
     var_symbol.type = type1;
@@ -31,6 +35,8 @@ SCENARIO(
     code_deadt removal(var_a);
     instructions.back().make_dead();
     instructions.back().code = removal;
+    instructions.back().function = fun_name;
+    symbol_table.insert(fun_symbol);
 
     WHEN("Removing known symbol")
     {

unit/goto-programs/goto_program_declaration.cpp

@@ -19,6 +19,10 @@ SCENARIO(
     symbol_tablet symbol_table;
     const signedbv_typet type1(32);
 
+    symbolt fun_symbol;
+    irep_idt fun_name = "foo";
+    fun_symbol.name = fun_name;
+
     symbolt var_symbol;
     irep_idt var_symbol_name = "a";
     var_symbol.type = type1;
@@ -30,6 +34,8 @@ SCENARIO(
     instructions.emplace_back(goto_program_instruction_typet::DECL);
     code_declt declaration(var_a);
     instructions.back().make_decl(declaration);
+    instructions.back().function = fun_name;
+    symbol_table.insert(fun_symbol);
 
     WHEN("Declaring known symbol")
     {

unit/goto-programs/goto_program_function_call.cpp

@@ -34,15 +34,16 @@ SCENARIO(
     symbolt fun_symbol;
     irep_idt fun_symbol_name = "foo";
     fun_symbol.name = fun_symbol_name;
+    fun_symbol.type = code_type;
     symbol_exprt fun_foo(fun_symbol_name, code_type);
 
     goto_functiont goto_function;
     auto &instructions = goto_function.body.instructions;
     instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL);
+    instructions.back().function = fun_symbol_name;
 
     var_symbol.type = type1;
     var_symbol2.type = type2;
-    fun_symbol.type = type1;
     symbol_table.insert(var_symbol);
     symbol_table.insert(var_symbol2);
     symbol_table.insert(fun_symbol);

unit/goto-programs/goto_program_goto_target.cpp

@@ -18,6 +18,10 @@ SCENARIO(
   {
     symbol_tablet symbol_table;
     const typet type1 = signedbv_typet(32);
+    symbolt fun_symbol;
+    irep_idt fun_name = "foo";
+    fun_symbol.name = fun_name;
+
     symbolt symbol;
     irep_idt symbol_name = "a";
     symbol.name = symbol_name;
@@ -29,12 +33,15 @@ SCENARIO(
     auto &instructions = goto_function.body.instructions;
     instructions.emplace_back(goto_program_instruction_typet::ASSERT);
     instructions.back().make_assertion(x_le_10);
+    instructions.back().function = fun_name;
 
     instructions.emplace_back(goto_program_instruction_typet::GOTO);
     instructions.back().make_goto(instructions.begin());
+    instructions.back().function = fun_name;
 
     symbol.type = type1;
     symbol_table.insert(symbol);
+    symbol_table.insert(fun_symbol);
     namespacet ns(symbol_table);
 
     WHEN("Target is a target")

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);
+      }
+    }
+  }
+}