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.

Also fixes unit tests that these new checks brake.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/expr_iterator.h>
 #include <util/find_symbols.h>
 #include <util/std_expr.h>
 #include <util/validate.h>
@@ -699,6 +700,25 @@ void goto_programt::instructiont::validate(
     }
   };
 
+  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:
@@ -729,7 +749,9 @@ void goto_programt::instructiont::validate(
       targets.empty(),
       "assert instruction should not have a target",
       source_location);
+
     std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
+    std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
     break;
   case OTHER:
     break;
@@ -794,7 +816,9 @@ void goto_programt::instructiont::validate(
       code.get_statement() == ID_function_call,
       "function call instruction should contain a call statement",
       source_location);
+
     std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
+    std::for_each(code.depth_begin(), code.depth_end(), type_finder);
     break;
   case THROW:
     break;

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