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, [email protected]
 #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, [email protected]
 #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, [email protected]
 #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, [email protected]
   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, [email protected]
 #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())