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,29 @@ int goto_instrument_parse_optionst::doit()
 
     get_goto_program();
 
+    {
+      const bool b = cmdline.isset("validate-goto-binary");
+
+      if(b || cmdline.isset("validate-goto-model"))
+      {
+        const namespacet ns(goto_model.symbol_table);
+        goto_model.validate(ns, validation_modet::EXCEPTION);
+
+        if(b)
+        {
+          return CPROVER_EXIT_SUCCESS;
+        }
+      }
+    }
+
     instrument_goto_program();
 
+    if(cmdline.isset("validate-goto-model"))
+    {
+      const namespacet ns(goto_model.symbol_table);
+      goto_model.validate(ns, validation_modet::INVARIANT);
+    }
+
     {
       bool unwind_given=cmdline.isset("unwind");
       bool unwindset_given=cmdline.isset("unwindset");
@@ -1569,6 +1590,12 @@ 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(*)
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --validate-goto-model        enable additional well-formedness checks on the\n"
+    "                              goto program\n"
+    // 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

@@ -101,6 +101,8 @@ Author: Daniel Kroening, [email protected]
   OPT_GOTO_PROGRAM_STATS \
   "(show-local-safe-pointers)(show-safe-dereferences)" \
   OPT_REPLACE_CALLS \
+  "(validate-goto-binary)" \
+  "(validate-goto-model)" \
   // empty last line
 
 // clang-format on