Program table symbol type consistency

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_function.h

@@ -110,6 +110,11 @@ class goto_functiont
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }
+
+  void validate(const symbol_tablet &table, const validation_modet &vm) const
+  {
+    return body.validate(table, vm);
+  }
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_model.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
@@ -95,6 +96,18 @@ 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)
+    {
+      it->second.validate(symbol_table, vm);
+    }
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/base_type.h>
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
@@ -668,6 +669,61 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
+void goto_programt::instructiont::validate(
+  const symbol_tablet &table,
+  const validation_modet &vm) const
+{
+  namespacet ns(table);
+  std::vector<std::vector<std::string>> type_collector;
+
+  auto type_finder = [&](const exprt &e) {
+    if(e.id() == ID_symbol)
+    {
+      auto symbol_expr = to_symbol_expr(e);
+      const auto &symbol_id = symbol_expr.get_identifier();
+
+      if(table.has_symbol(symbol_id))
+        DATA_CHECK_WITH_DIAGNOSTICS(
+          base_type_eq(
+            symbol_expr.type(), table.lookup_ref(symbol_id).type, ns),
+          id2string(symbol_id) + " type inconsistency\n" +
+            "goto program type: " + symbol_expr.type().id_string() + "\n " +
+            "symbol table type: " +
+            table.lookup_ref(symbol_id).type.id_string(),
+          source_location);
+    }
+  };
+
+  switch(type)
+  {
+  case GOTO:
+  case ASSUME:
+  case ASSERT:
+    guard.visit(type_finder);
+    break;
+  case ASSIGN:
+  case DECL:
+  case DEAD:
+  case FUNCTION_CALL:
+    code.visit(type_finder);
+    break;
+  case OTHER:
+  case SKIP:
+  case LOCATION:
+  case END_FUNCTION:
+  case START_THREAD:
+  case END_THREAD:
+  case ATOMIC_BEGIN:
+  case ATOMIC_END:
+  case RETURN:
+  case THROW:
+  case CATCH:
+  case NO_INSTRUCTION_TYPE:
+  case INCOMPLETE_GOTO:
+    break;
+  }
+}
+
 bool goto_programt::equals(const goto_programt &other) const
 {
   if(instructions.size() != other.instructions.size())
@@ -699,6 +755,16 @@ bool goto_programt::equals(const goto_programt &other) const
   return true;
 }
 
+void goto_programt::validate(
+  const symbol_tablet &table,
+  const validation_modet &vm) const
+{
+  forall_goto_program_instructions(it, (*this))
+  {
+    it->validate(table, vm);
+  }
+}
+
 /// Outputs a string representation of a `goto_program_instruction_typet`
 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
 {

src/goto-programs/goto_program.h

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/message.h>
 
 /// The type of an instruction in a GOTO program.
 enum goto_program_instruction_typet
@@ -398,6 +399,12 @@ class goto_programt
     /// only be evaluated in the context of a goto_programt (see
     /// goto_programt::equals).
     bool equals(const instructiont &other) const;
+
+    /// Iterate over code and guard and collect inconsistencies with symbol
+    /// table.
+    /// \param table the symbol table
+    /// \param vm validation mode
+    void validate(const symbol_tablet &table, const validation_modet &vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -677,6 +684,8 @@ class goto_programt
   /// the same number of instructions, each pair of instructions compares equal,
   /// and relative jumps have the same distance.
   bool equals(const goto_programt &other) const;
+
+  void validate(const symbol_tablet &table, const validation_modet &vm) const;
 };
 
 /// Get control-flow successors of a given instruction. The instruction is

src/util/expr.cpp

@@ -322,6 +322,24 @@ void exprt::visit(const_expr_visitort &visitor) const
   }
 }
 
+void exprt::visit(const std::function<void(const exprt &)> &f) const
+{
+  std::stack<const exprt *> stack;
+
+  stack.push(this);
+
+  while(!stack.empty())
+  {
+    const exprt &expr = *stack.top();
+    stack.pop();
+
+    f(expr);
+
+    forall_operands(it, expr)
+      stack.push(&(*it));
+  }
+}
+
 depth_iteratort exprt::depth_begin()
 { return depth_iteratort(*this); }
 depth_iteratort exprt::depth_end()

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>
@@ -224,6 +225,7 @@ class exprt:public irept
 public:
   void visit(class expr_visitort &visitor);
   void visit(class const_expr_visitort &visitor) const;
+  void visit(const std::function<void(const exprt &)> &f) const;
 
   depth_iteratort depth_begin();
   depth_iteratort depth_end();

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_program_symbol_type_table_consistency.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

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