Merge pull request #3123 from danpoe/feature/well-formedness-checking

Skeleton for well-formedness checking of goto models [blocks: #3118, #3147, #3188, #3191, #3187, #3193]

Author: tautschnig

src/cbmc/cbmc_parse_options.cpp

@@ -530,6 +530,11 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::INVARIANT);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -977,6 +982,8 @@ 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"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    HELP_VALIDATE
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
+#include <util/validation_interface.h>
 
 #include <langapi/language.h>
 
@@ -73,6 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
+  OPT_VALIDATE \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -406,6 +406,11 @@ int goto_analyzer_parse_optionst::doit()
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::INVARIANT);
+  }
+
   // show it?
   if(cmdline.isset("show-symbol-table"))
   {
@@ -875,6 +880,7 @@ void goto_analyzer_parse_optionst::help()
     HELP_GOTO_CHECK
     "\n"
     "Other options:\n"
+    HELP_VALIDATE
     " --version                    show version and exit\n"
     HELP_FLUSH
     HELP_TIMESTAMP

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -101,9 +101,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
+#include <util/validation_interface.h>
 
 #include <langapi/language.h>
 
@@ -148,6 +149,7 @@ class optionst;
   "(show)(verify)(simplify):" \
   "(location-sensitive)(concurrent)" \
   "(no-simplify-slicing)" \
+  OPT_VALIDATE \
 // clang-format on
 
 class goto_analyzer_parse_optionst:

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -125,8 +125,27 @@ int goto_instrument_parse_optionst::doit()
 
     get_goto_program();
 
+    {
+      const bool validate_only = cmdline.isset("validate-goto-binary");
+
+      if(validate_only || cmdline.isset("validate-goto-model"))
+      {
+        goto_model.validate(validation_modet::EXCEPTION);
+
+        if(validate_only)
+        {
+          return CPROVER_EXIT_SUCCESS;
+        }
+      }
+    }
+
     instrument_goto_program();
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      goto_model.validate(validation_modet::INVARIANT);
+    }
+
     {
       bool unwind_given=cmdline.isset("unwind");
       bool unwindset_given=cmdline.isset("unwindset");
@@ -1572,6 +1591,10 @@ void goto_instrument_parse_optionst::help()
     " --show-local-safe-pointers   show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
     " --show-safe-dereferences     show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
     "                              *and* used as a dereference operand\n" // NOLINT(*)
+    HELP_VALIDATE
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --validate-goto-binary       check the well-formedness of the passed in goto\n"
+    "                              binary and then exit\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
+#include <util/validation_interface.h>
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_functions.h>
@@ -101,6 +102,8 @@ Author: Daniel Kroening, kroening@kroening.com
   OPT_GOTO_PROGRAM_STATS \
   "(show-local-safe-pointers)(show-safe-dereferences)" \
   OPT_REPLACE_CALLS \
+  "(validate-goto-binary)" \
+  OPT_VALIDATE \
   // empty last line
 
 // clang-format on

src/goto-programs/goto_function.h

@@ -110,6 +110,16 @@ class goto_functiont
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }
+
+  /// Check that the goto function is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    body.validate(ns, vm);
+    validate_full_type(type, ns, vm);
+  }
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_functions.h

@@ -117,6 +117,19 @@ class goto_functionst
 
   std::vector<function_mapt::const_iterator> sorted() const;
   std::vector<function_mapt::iterator> sorted();
+
+  /// Check that the goto functions are well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    for(const auto &entry : function_map)
+    {
+      const goto_functiont &goto_function = entry.second;
+      goto_function.validate(ns, vm);
+    }
+  }
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_model.h

@@ -89,6 +89,18 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            goto_functions.function_map.end();
   }
+
+  /// Check that the goto model is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const validation_modet vm) const
+  {
+    symbol_table.validate();
+
+    const namespacet ns(symbol_table);
+    goto_functions.validate(ns, vm);
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated

src/goto-programs/goto_program.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iomanip>
 
 #include <util/std_expr.h>
+#include <util/validate.h>
 
 #include <langapi/language_util.h>
 
@@ -668,6 +669,62 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
   // clang-format on
 }
 
+void goto_programt::instructiont::validate(
+  const namespacet &ns,
+  const validation_modet vm) const
+{
+  validate_full_code(code, ns, vm);
+  validate_full_expr(guard, ns, vm);
+
+  switch(type)
+  {
+  case NO_INSTRUCTION_TYPE:
+    break;
+  case GOTO:
+    break;
+  case ASSUME:
+    break;
+  case ASSERT:
+    break;
+  case OTHER:
+    break;
+  case SKIP:
+    break;
+  case START_THREAD:
+    break;
+  case END_THREAD:
+    break;
+  case LOCATION:
+    break;
+  case END_FUNCTION:
+    break;
+  case ATOMIC_BEGIN:
+    break;
+  case ATOMIC_END:
+    break;
+  case RETURN:
+    break;
+  case ASSIGN:
+    DATA_CHECK(
+      code.get_statement() == ID_assign,
+      "assign instruction should contain an assign statement");
+    DATA_CHECK(targets.empty(), "assign instruction should not have a target");
+    break;
+  case DECL:
+    break;
+  case DEAD:
+    break;
+  case FUNCTION_CALL:
+    break;
+  case THROW:
+    break;
+  case CATCH:
+    break;
+  case INCOMPLETE_GOTO:
+    break;
+  }
+}
+
 bool goto_programt::equals(const goto_programt &other) const
 {
   if(instructions.size() != other.instructions.size())

src/goto-programs/goto_program.h

@@ -20,10 +20,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/symbol_table.h>
 #include <util/source_location.h>
-#include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+enum class validation_modet;
 
 /// The type of an instruction in a GOTO program.
 enum goto_program_instruction_typet
@@ -398,6 +400,12 @@ class goto_programt
     /// only be evaluated in the context of a goto_programt (see
     /// goto_programt::equals).
     bool equals(const instructiont &other) const;
+
+    /// Check that the instruction is well-formed
+    ///
+    /// The validation mode indicates whether well-formedness check failures are
+    /// reported via DATA_INVARIANT violations or exceptions.
+    void validate(const namespacet &ns, const validation_modet vm) const;
   };
 
   // Never try to change this to vector-we mutate the list while iterating
@@ -677,6 +685,18 @@ 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;
+
+  /// Check that the goto program is well-formed
+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    for(const instructiont &ins : instructions)
+    {
+      ins.validate(ns, vm);
+    }
+  }
 };
 
 /// Get control-flow successors of a given instruction. The instruction is

src/goto-programs/initialize_goto_model.cpp

@@ -165,6 +165,11 @@ goto_modelt initialize_goto_model(
     goto_model.goto_functions,
     message_handler);
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    goto_model.validate(validation_modet::EXCEPTION);
+  }
+
   // stupid hack
   config.set_object_bits_from_symbol_table(
     goto_model.symbol_table);

src/util/Makefile

@@ -96,6 +96,9 @@ SRC = arith_tools.cpp \
       union_find.cpp \
       union_find_replace.cpp \
       unwrap_nested_exception.cpp \
+      validate_code.cpp \
+      validate_expressions.cpp \
+      validate_types.cpp \
       version.cpp \
       xml.cpp \
       xml_expr.cpp \

src/util/exception_utils.cpp

@@ -55,25 +55,23 @@ std::string deserialization_exceptiont::what() const
 }
 
 incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
-  std::string message,
-  source_locationt source_location)
-  : message(std::move(message)), source_location(std::move(source_location))
+  std::string message)
+  : message(std::move(message))
 {
+  source_location.make_nil();
 }
 
 std::string incorrect_goto_program_exceptiont::what() const
 {
-  if(source_location.is_nil())
-    return message;
-  else
-    return message + " (at: " + source_location.as_string() + ")";
-}
+  std::string ret(message);
 
-incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
-  std::string message)
-  : message(std::move(message))
-{
-  source_location.make_nil();
+  if(!source_location.is_nil())
+    ret += " (at: " + source_location.as_string() + ")";
+
+  if(!diagnostics.empty())
+    ret += "\n" + diagnostics;
+
+  return ret;
 }
 
 unsupported_operation_exceptiont::unsupported_operation_exceptiont(