Validate goto models in goto-instrument (if enabled via command line flags)

There are two flags: --validate-goto-binary reads in a goto binary and checks
that it is well formed and then exits; --validate-goto-model enables additional
well-formedness checks at various points during the execution of goto-instrument
in addition to the normal analyses that it runs.

Author: danpoe

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

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.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