Consistency between goto programs and symbol table

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,18 @@ class goto_functiont
   void validate(const namespacet &ns, const validation_modet vm) const
   {
     body.validate(ns, vm);
+
+    find_symbols_sett typetags;
+    find_type_symbols(type, typetags);
+    const symbolt *symbol;
+    for(const auto &identifier : typetags)
+    {
+      DATA_CHECK(
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found");
+    }
+
     validate_full_type(type, ns, vm);
   }
 };

src/goto-programs/goto_functions.h

@@ -127,6 +127,15 @@ class goto_functionst
     for(const auto &entry : function_map)
     {
       const goto_functiont &goto_function = entry.second;
+      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() +
+          "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
+
       goto_function.validate(ns, vm);
     }
   }

src/goto-programs/goto_program.cpp

@@ -14,6 +14,8 @@ 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>
 
@@ -677,6 +679,45 @@ void goto_programt::instructiont::validate(
   validate_full_expr(guard, ns, vm);
 
   const symbolt *table_symbol;
+  DATA_CHECK_WITH_DIAGNOSTICS(
+    vm,
+    !ns.lookup(function, table_symbol),
+    id2string(function) + " not found",
+    source_location);
+
+  auto expr_symbol_finder = [&](const exprt &e) {
+    find_symbols_sett typetags;
+    find_type_symbols(e.type(), typetags);
+    find_symbols(e, typetags);
+    const symbolt *symbol;
+    for(const auto &identifier : typetags)
+    {
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found",
+        source_location);
+    }
+  };
+
+  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)
   {
@@ -708,6 +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;
@@ -772,6 +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

@@ -15,11 +15,14 @@ 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_model_function_type_consistency.cpp \
        goto-programs/goto_program_assume.cpp \
        goto-programs/goto_program_dead.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 \
        interpreter/interpreter.cpp \

unit/goto-programs/goto_model_function_type_consistency.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+ Module: Unit tests for goto_model::validate
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <goto-programs/goto_model.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of consistent program/table pair (function type)",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A model with one function")
+  {
+    const typet type1 = signedbv_typet(32);
+    const typet type2 = signedbv_typet(64);
+    code_typet fun_type1({}, type1);
+    code_typet fun_type2({}, type2);
+
+    symbolt function_symbol;
+    irep_idt function_symbol_name = "foo";
+    function_symbol.name = function_symbol_name;
+
+    goto_modelt goto_model;
+    goto_model.goto_functions.function_map[function_symbol.name] =
+      goto_functiont();
+    goto_model.goto_functions.function_map[function_symbol.name].type =
+      fun_type1;
+
+    WHEN("Symbol table has the right type")
+    {
+      function_symbol.type = fun_type1;
+      goto_model.symbol_table.insert(function_symbol);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_model.validate(validation_modet::INVARIANT);
+
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Symbol table has the wrong type")
+    {
+      function_symbol.type = fun_type2;
+      goto_model.symbol_table.insert(function_symbol);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_model.validate(validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}

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