Goto programs validation

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -550,7 +550,10 @@ int jbmc_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{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     if(
@@ -691,7 +694,10 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("validate-goto-model"))
     {
-      lazy_goto_model.validate(validation_modet::INVARIANT);
+      lazy_goto_model.validate(
+        validation_modet::INVARIANT,
+        goto_model_validation_optionst{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     // 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,10 @@ int cbmc_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{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   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,10 @@ 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{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   // 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,10 @@ 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(
+      validation_modet::INVARIANT,
+      goto_model_validation_optionst{
+        goto_model_validation_optionst::set_optionst::all_true});
   }
 
   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>
@@ -134,7 +135,10 @@ 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{
+            goto_model_validation_optionst::set_optionst::all_true});
 
         if(validate_only)
         {
@@ -147,7 +151,10 @@ 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{
+          goto_model_validation_optionst::set_optionst::all_true});
     }
 
     {

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

@@ -54,7 +54,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

@@ -33,10 +33,21 @@ void get_local_identifiers(
 ///
 /// The validation mode indicates whether well-formedness check failures are
 /// reported via DATA_INVARIANT violations or exceptions.
-void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
-  const
+void goto_functiont::validate(
+  const namespacet &ns,
+  const validation_modet vm,
+  const goto_model_validation_optionst &goto_model_validation_options) const
 {
-  body.validate(ns, vm);
+  // 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, goto_model_validation_options);
 
   find_symbols_sett typetags;
   find_type_symbols(type, typetags);

src/goto-programs/goto_function.h

@@ -21,6 +21,7 @@ Date: May 2018
 #include <util/std_types.h>
 
 #include "goto_program.h"
+#include "validate_goto_model.h"
 
 /// A goto function, consisting of function type (see #type), function body (see
 /// #body), and parameter identifiers (see #parameter_identifiers).
@@ -119,7 +120,10 @@ class goto_functiont
   ///
   /// 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;
 };
 
 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/goto_functions.h

@@ -111,7 +111,10 @@ 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
   {
     for(const auto &entry : function_map)
     {
@@ -148,7 +151,7 @@ class goto_functionst
         ++it;
       }
 
-      goto_function.validate(ns, vm);
+      goto_function.validate(ns, vm, goto_model_validation_options);
     }
   }
 };

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,12 +95,20 @@ 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,
+    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);
+    goto_functions.validate(ns, vm, goto_model_validation_options);
   }
 };
 
@@ -142,12 +151,20 @@ 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);
+    goto_functions.validate(ns, vm, goto_model_validation_options);
   }
 
 private:

src/goto-programs/goto_program.cpp

@@ -674,7 +674,8 @@ bool goto_programt::instructiont::equals(const instructiont &other) const
 
 void goto_programt::instructiont::validate(
   const namespacet &ns,
-  const validation_modet vm) const
+  const validation_modet vm,
+  const goto_model_validation_optionst &goto_model_validation_options) const
 {
   validate_full_code(code, ns, vm);
   validate_full_expr(guard, ns, vm);
@@ -776,6 +777,27 @@ void goto_programt::instructiont::validate(
       }
     };
 
+  // this option is always set to false until all source locations
+  // are reliably set correctly (future work)
+  if(goto_model_validation_options.check_source_location)
+  {
+    DATA_CHECK(
+      vm,
+      source_location.is_not_nil(),
+      "each instruction source location must not be nil");
+
+    DATA_CHECK(
+      vm,
+      code.source_location().is_not_nil(),
+      "each instruction code field, must have non nil source location");
+
+    DATA_CHECK(
+      vm,
+      source_location == code.source_location(),
+      "instruction source location and"
+      " instruction code field source location must be the same");
+  }
+
   const symbolt *table_symbol;
   switch(type)
   {

src/goto-programs/goto_program.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <string>
 
+#include "validate_goto_model.h"
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
@@ -554,7 +555,11 @@ class goto_programt
     ///
     /// 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;
 
     /// Apply given transformer to all expressions; no return value
     /// means no change needed.
@@ -814,11 +819,14 @@ class goto_programt
   ///
   /// 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
   {
     for(const instructiont &ins : instructions)
     {
-      ins.validate(ns, vm);
+      ins.validate(ns, vm, goto_model_validation_options);
     }
   }