Goto programs validation

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -550,7 +550,7 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      goto_model.validate(validation_modet::INVARIANT);
+      goto_model.validate();
     }
 
     if(
@@ -691,7 +691,7 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      lazy_goto_model.validate(validation_modet::INVARIANT);
+      lazy_goto_model.validate();
     }
 
     // Provide show-goto-functions and similar dump functions after symex

src/cbmc/cbmc_parse_options.cpp

@@ -53,24 +53,25 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
 #include <goto-programs/read_goto_binary.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_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-programs/validate_goto_model.h>
 
-#include <goto-instrument/reachability_slicer.h>
+#include <goto-instrument/cover.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
-#include <goto-instrument/cover.h>
+#include <goto-instrument/reachability_slicer.h>
 
 #include <goto-symex/path_storage.h>
 
@@ -550,7 +551,7 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::INVARIANT);
+    goto_model.validate();
   }
 
   if(

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -40,6 +40,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>
@@ -405,7 +406,7 @@ int goto_analyzer_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::INVARIANT);
+    goto_model.validate();
   }
 
   // show it?

src/goto-cc/compile.cpp

@@ -35,6 +35,7 @@ Date: June 2006
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/read_goto_binary.h>
+#include <goto-programs/validate_goto_model.h>
 #include <goto-programs/write_goto_binary.h>
 
 #include <langapi/language_file.h>
@@ -546,7 +547,7 @@ bool compilet::write_bin_object_file(
   if(validate_goto_model)
   {
     status() << "Validating goto model" << eom;
-    src_goto_model.validate(validation_modet::INVARIANT);
+    src_goto_model.validate();
   }
 
   statistics() << "Writing binary format object `"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -25,25 +25,26 @@ 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/loop_ids.h>
+#include <goto-programs/parameter_assignments.h>
+#include <goto-programs/read_goto_binary.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>
@@ -147,7 +148,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      goto_model.validate(validation_modet::INVARIANT);
+      goto_model.validate();
     }
 
     {

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/abstract_goto_model.h

@@ -13,6 +13,7 @@ Author: Diffblue Ltd.
 #define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
 
 #include "goto_functions.h"
+#include "validate_goto_model.h"
 #include <util/symbol_table.h>
 
 /// Abstract interface to eager or lazy GOTO models
@@ -54,7 +55,11 @@ class abstract_goto_modelt
   ///
   /// The validation mode indicates whether well-formedness check failures are
   /// reported via DATA_INVARIANT violations or exceptions.
-  virtual void validate(const validation_modet vm) const = 0;
+  // virtual void validate(const validation_modet vm) const = 0;
+  virtual void validate(
+    const validation_modet vm,
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const = 0;
 };
 
 #endif

src/goto-programs/goto_function.cpp

@@ -36,6 +36,15 @@ void get_local_identifiers(
 void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
   const
 {
+  // function body must end with an END_FUNCTION instruction
+  if(body_available())
+  {
+    DATA_CHECK(
+      vm,
+      body.instructions.back().is_end_function(),
+      "last instruction should be of end function type");
+  }
+
   body.validate(ns, vm);
 
   find_symbols_sett typetags;

src/goto-programs/goto_model.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
+#include "validate_goto_model.h"
 
 // A model is a pair consisting of a symbol table
 // and the CFGs for the functions.
@@ -94,10 +95,18 @@ 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 override
+  void validate(
+    const validation_modet vm = validation_modet::INVARIANT,
+    const goto_model_validation_optionst &goto_model_validation_options =
+      goto_model_validation_optionst{}) const override
   {
     symbol_table.validate(vm);
 
+    // Does a number of checks at the function_mapt level to ensure the
+    // goto_program is well formed. Does not call any validate methods
+    // (at the goto_functiont level or below)
+    validate_goto_model(goto_functions, vm, goto_model_validation_options);
+
     const namespacet ns(symbol_table);
     goto_functions.validate(ns, vm);
   }
@@ -142,10 +151,18 @@ class wrapper_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 override
+  void validate(
+    const validation_modet vm,
+    const goto_model_validation_optionst &goto_model_validation_options)
+    const override
   {
     symbol_table.validate(vm);
 
+    // Does a number of checks at the function_mapt level to ensure the
+    // goto_program is well formed. Does not call any validate methods
+    // (at the goto_functiont level or below)
+    validate_goto_model(goto_functions, vm, goto_model_validation_options);
+
     const namespacet ns(symbol_table);
     goto_functions.validate(ns, vm);
   }

src/goto-programs/initialize_goto_model.cpp

@@ -194,7 +194,11 @@ goto_modelt initialize_goto_model(
 
   if(options.is_set("validate-goto-model"))
   {
-    goto_model.validate(validation_modet::EXCEPTION);
+    goto_model_validation_optionst goto_model_validation_options{
+      goto_model_validation_optionst ::set_optionst::all_false};
+
+    goto_model.validate(
+      validation_modet::INVARIANT, goto_model_validation_options);
   }
 
   // stupid hack

src/goto-programs/lazy_goto_model.h

@@ -247,9 +247,12 @@ class lazy_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 override
+  void validate(
+    const validation_modet vm = validation_modet::INVARIANT,
+    const goto_model_validation_optionst &goto_model_validation_options =
+      goto_model_validation_optionst{}) const override
   {
-    goto_model->validate(vm);
+    goto_model->validate(vm, goto_model_validation_options);
   }
 
 private: