Function type consistency between goto programs and symbol table

src/cbmc/cbmc_parse_options.cpp

@@ -526,6 +526,12 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    namespacet ns(goto_model.symbol_table);
+    goto_model.validate(ns, validation_modet::INVARIANT);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -972,6 +978,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --validate-goto-model        enables additional well-formedness checks on the goto program\n" // NOLINT(*)
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -72,6 +72,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  "(validate-goto-model)" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-programs/goto_model.h

@@ -12,8 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 
-#include <util/symbol_table.h>
+#include <util/base_type.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table.h>
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
@@ -95,6 +97,23 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            goto_functions.function_map.end();
   }
+
+  /// Iterates over the functions inside the goto model and checks invariants
+  /// in all of them. Prints out error message collected.
+  /// \param ns namespace for the environment
+  /// \param vm validation mode to be used for error reporting
+  void validate(const namespacet &ns, const validation_modet &vm) const
+  {
+    forall_goto_functions(it, goto_functions)
+    {
+      DATA_CHECK(
+        base_type_eq(
+          it->second.type, symbol_table.lookup_ref(it->first).type, ns),
+        id2string(it->first) + " type inconsistency\ngoto program type: " +
+          it->second.type.id_string() + "\nsymbol table type: " +
+          symbol_table.lookup_ref(it->first).type.id_string());
+    }
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/util/expr.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_EXPR_H
 
 #include "type.h"
+#include "validate.h"
 
 #include <functional>
 #include <list>

src/util/validate.h

@@ -0,0 +1,61 @@
+/*******************************************************************\
+
+Module: Goto program validation
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_VALIDATE_H
+#define CPROVER_UTIL_VALIDATE_H
+
+#include <type_traits>
+
+#include "exception_utils.h"
+#include "invariant.h"
+#include "irep.h"
+
+enum class validation_modet
+{
+  INVARIANT,
+  EXCEPTION
+};
+
+#define GET_FIRST(A, ...) A
+
+/// This macro takes a condition which denotes a well-formedness criterion on
+/// goto programs, expressions, instructions, etc. Based on the value of the
+/// variable vm (the validation mode), it either uses DATA_INVARIANT() to check
+/// those conditions, or throws an exception when a condition does not hold.
+#define DATA_CHECK(condition, message)                                         \
+  do                                                                           \
+  {                                                                            \
+    switch(vm)                                                                 \
+    {                                                                          \
+    case validation_modet::INVARIANT:                                          \
+      DATA_INVARIANT(condition, message);                                      \
+      break;                                                                   \
+    case validation_modet::EXCEPTION:                                          \
+      if(!(condition))                                                         \
+        throw incorrect_goto_program_exceptiont(message);                      \
+      break;                                                                   \
+    }                                                                          \
+  } while(0)
+
+#define DATA_CHECK_WITH_DIAGNOSTICS(condition, message, ...)                   \
+  do                                                                           \
+  {                                                                            \
+    switch(vm)                                                                 \
+    {                                                                          \
+    case validation_modet::INVARIANT:                                          \
+      DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__);        \
+      break;                                                                   \
+    case validation_modet::EXCEPTION:                                          \
+      if(!(condition))                                                         \
+        throw incorrect_goto_program_exceptiont(                               \
+          message, GET_FIRST(__VA_ARGS__, dummy));                             \
+      break;                                                                   \
+    }                                                                          \
+  } while(0)
+
+#endif /* CPROVER_UTIL_VALIDATE_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 \
        goto-programs/goto_trace_output.cpp \
+       goto-programs/goto_model_function_type_consistency.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_model_function_type_consistency.cpp

@@ -0,0 +1,69 @@
+/*******************************************************************\
+
+ 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);
+      namespacet ns(goto_model.symbol_table);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_model.validate(ns, validation_modet::INVARIANT);
+
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Symbol table has the wrong type")
+    {
+      function_symbol.type = fun_type2;
+      goto_model.symbol_table.insert(function_symbol);
+      namespacet ns(goto_model.symbol_table);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_model.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}