Validation checks for Goto Programs

There are several checks, implemented with separate methods, and
some flagged as optional.
NB use of validate_goto_model(*this, vm) in goto_functions.h is to avoid
circular inclusion as function_mapt is a nested type and so cannot be
forward declared.

Author: Sonny Martin

src/cbmc/cbmc_parse_options.cpp

@@ -30,32 +30,32 @@ Author: Daniel Kroening, [email protected]
 
 #include <cpp/cprover_library.h>
 
+#include <goto-instrument/cover.h>
+#include <goto-instrument/full_slicer.h>
+#include <goto-instrument/nondet_static.h>
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
 #include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_asm.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_vector.h>
 #include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/show_symbol_table.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-
-#include <goto-instrument/reachability_slicer.h>
-#include <goto-instrument/full_slicer.h>
-#include <goto-instrument/nondet_static.h>
-#include <goto-instrument/cover.h>
+#include <goto-programs/validate_goto_model.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -532,7 +532,13 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::INVARIANT);
+    goto_model_validation_optionst goto_model_validation_options;
+    goto_model_validation_options.function_pointer_calls_removed = true;
+    goto_model_validation_options.check_returns_removed = true;
+    goto_model_validation_options.check_called_functions = true;
+    goto_model_validation_options.check_last_instruction = true;
+    goto_model.validate(
+      validation_modet::INVARIANT, goto_model_validation_options);
   }
 
   return bmct::do_language_agnostic_bmc(

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -39,6 +39,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
+#include <goto-programs/validate_goto_model.h>
 
 #include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
@@ -408,7 +409,8 @@ int goto_analyzer_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::INVARIANT);
+    goto_model.validate(
+      validation_modet::INVARIANT, goto_model_validation_optionst{});
   }
 
   // show it?

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -24,26 +24,27 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/remove_calls_no_body.h>
-#include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_inline.h>
-#include <goto-programs/show_properties.h>
-#include <goto-programs/set_properties.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/write_goto_binary.h>
 #include <goto-programs/interpreter.h>
-#include <goto-programs/string_abstraction.h>
-#include <goto-programs/string_instrumentation.h>
-#include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
-#include <goto-programs/remove_returns.h>
+#include <goto-programs/loop_ids.h>
+#include <goto-programs/parameter_assignments.h>
+#include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_calls_no_body.h>
+#include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_returns.h>
+#include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
-#include <goto-programs/parameter_assignments.h>
-#include <goto-programs/slice_global_inits.h>
+#include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/set_properties.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
+#include <goto-programs/slice_global_inits.h>
+#include <goto-programs/string_abstraction.h>
+#include <goto-programs/string_instrumentation.h>
+#include <goto-programs/validate_goto_model.h>
+#include <goto-programs/write_goto_binary.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -130,7 +131,8 @@ int goto_instrument_parse_optionst::doit()
 
       if(validate_only || cmdline.isset("validate-goto-model"))
       {
-        goto_model.validate(validation_modet::EXCEPTION);
+        goto_model.validate(
+          validation_modet::EXCEPTION, goto_model_validation_optionst{});
 
         if(validate_only)
         {
@@ -143,7 +145,8 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      goto_model.validate(validation_modet::INVARIANT);
+      goto_model.validate(
+        validation_modet::INVARIANT, goto_model_validation_optionst{});
     }
 
     {

src/goto-programs/Makefile

@@ -64,6 +64,7 @@ SRC = adjust_float_expressions.cpp \
       string_abstraction.cpp \
       string_instrumentation.cpp \
       system_library_symbols.cpp \
+      validate_goto_model.cpp \
       vcd_goto_trace.cpp \
       wp.cpp \
       write_goto_binary.cpp \

src/goto-programs/goto_functions.h

@@ -16,6 +16,7 @@ Date: June 2003
 
 #include "goto_function.h"
 
+#include "validate_goto_model.h"
 #include <util/cprover_prefix.h>
 
 /// A collection of goto functions
@@ -122,8 +123,12 @@ class goto_functionst
   ///
   /// 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
+  void validate(
+    const namespacet &ns,
+    const validation_modet vm,
+    const goto_model_validation_optionst &goto_model_validation_options) const
   {
+    validate_goto_model(*this, vm, goto_model_validation_options);
     for(const auto &entry : function_map)
     {
       const goto_functiont &goto_function = entry.second;

src/goto-programs/goto_model.h

@@ -94,12 +94,14 @@ class goto_modelt : public abstract_goto_modelt
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const validation_modet vm) const
+  void validate(
+    const validation_modet vm,
+    const goto_model_validation_optionst &goto_model_validation_options) const
   {
     symbol_table.validate(vm);
 
     const namespacet ns(symbol_table);
-    goto_functions.validate(ns, vm);
+    goto_functions.validate(ns, vm, goto_model_validation_options);
   }
 };
 

src/goto-programs/initialize_goto_model.cpp

@@ -167,7 +167,8 @@ goto_modelt initialize_goto_model(
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::EXCEPTION);
+    goto_model.validate(
+      validation_modet::EXCEPTION, goto_model_validation_optionst{});
   }
 
   // stupid hack