Adjustments for new location of program checks

src/cbmc/cbmc_parse_options.cpp

@@ -553,11 +553,10 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("validate-goto-model"))
   {
-    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_validation_optionst goto_model_validation_options{true};
+    // this option is temporarily disabled until all source locations
+    // are reliably set correctly
+    goto_model_validation_options.check_source_location = false;
     goto_model.validate(
       validation_modet::INVARIANT, goto_model_validation_options);
   }

src/goto-programs/abstract_goto_model.h

@@ -54,7 +54,10 @@ 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);
@@ -61,3 +72,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
 
   validate_full_type(type, ns, vm);
 }
+

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

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

@@ -144,12 +144,14 @@ 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);
 
     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,25 @@ void goto_programt::instructiont::validate(
       }
     };
 
+  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);
     }
   }
 

src/goto-programs/lazy_goto_model.h

@@ -247,9 +247,11 @@ 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,
+    const goto_model_validation_optionst &goto_model_validation_options) const override
   {
-    goto_model->validate(vm);
+    goto_model->validate(vm, goto_model_validation_options);
   }
 
 private:

src/goto-programs/validate_goto_model.cpp

@@ -59,24 +59,8 @@ class validate_goto_modelt
   /// a corresponding entry exists in the function_map
   void check_called_functions();
 
-  /// Check that goto-programs that have a body end with an END_FUNCTION
-  /// instruction.
-  ///
-  /// NB functions that are only declared, and not used will not appear in the
-  /// function map. Functions that are declared only and used to e.g.
-  /// initialise a function pointer will have no body.
-  void check_last_instruction();
-
-  /// Check both
-  /// 1. every instruction \"code\" field, has a non nil source location"
-  /// 2. every instruction source_location field is nil
-  /// NB this check is not expected to pass until setting these locations is
-  /// patched up.
-  void check_sourcecode_location();
-
   const validation_modet vm;
   const function_mapt &function_map;
-  const goto_model_validation_optionst validation_options;
 };
 } // namespace
 
@@ -86,9 +70,6 @@ void validate_goto_modelt::do_goto_program_checks(
   if(validation_options.entry_point_exists)
     entry_point_exists();
 
-  if(validation_options.check_last_instruction)
-    check_last_instruction();
-
   /// NB function pointer calls must have been removed before removing
   /// returns - so 'check_returns_removed' also enables
   // 'function_pointer_calls_removed'
@@ -102,9 +83,6 @@ void validate_goto_modelt::do_goto_program_checks(
 
   if(validation_options.check_called_functions)
     check_called_functions();
-
-  if(validation_options.check_sourcecode_location)
-    check_sourcecode_location();
 }
 
 void validate_goto_modelt::entry_point_exists()
@@ -158,7 +136,10 @@ void validate_goto_modelt::check_returns_removed()
           "function call return should be nil");
 
         const auto &callee = to_code_type(function_call.function().type());
-        DATA_CHECK(vm, callee.return_type().id() == ID_empty, "");
+        DATA_CHECK(
+          vm,
+          callee.return_type().id() == ID_empty,
+          "called function must have empty return type");
       }
     }
   }
@@ -222,41 +203,6 @@ void validate_goto_modelt::check_called_functions()
   }
 }
 
-void validate_goto_modelt::check_last_instruction()
-{
-  for(const auto &fun : function_map)
-  {
-    if(fun.second.body_available())
-    {
-      DATA_CHECK(
-        vm,
-        fun.second.body.instructions.back().is_end_function(),
-        "last instruction should be of end function type");
-    }
-  }
-}
-
-void validate_goto_modelt::check_sourcecode_location()
-{
-  // Assumption is that if every instruction is checked - then there is no
-  // need to check targets.
-  for(const auto &fun : function_map)
-  {
-    for(auto &instr : fun.second.body.instructions)
-    {
-      DATA_CHECK(
-        vm,
-        instr.code.source_location().is_not_nil(),
-        "each instruction \"code\" field, must have non nil source location");
-
-      DATA_CHECK(
-        vm,
-        instr.source_location.is_not_nil(),
-        "each instruction source location must not be nil");
-    }
-  }
-}
-
 void validate_goto_model(
   const goto_functionst &goto_functions,
   const validation_modet vm,

src/goto-programs/validate_goto_model.h

@@ -18,16 +18,14 @@ struct goto_model_validation_optionst
   bool function_pointer_calls_removed;
   bool check_returns_removed;
   bool check_called_functions;
-  bool check_last_instruction;
-  bool check_sourcecode_location;
+  bool check_source_location;
 
   goto_model_validation_optionst()
     : entry_point_exists{true},
       function_pointer_calls_removed{false},
       check_returns_removed{false},
       check_called_functions{false},
-      check_last_instruction{false},
-      check_sourcecode_location{false}
+      check_source_location{false}
   {
   }
 
@@ -36,8 +34,7 @@ struct goto_model_validation_optionst
       function_pointer_calls_removed{options_value},
       check_returns_removed{options_value},
       check_called_functions{options_value},
-      check_last_instruction{options_value},
-      check_sourcecode_location{options_value}
+      check_source_location{options_value}
   {
   }
 };

unit/Makefile

@@ -22,6 +22,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_function_call.cpp \
        goto-programs/goto_program_goto_target.cpp \
+       goto-programs/goto_program_instruction.cpp \
        goto-programs/goto_program_symbol_type_table_consistency.cpp \
        goto-programs/goto_program_table_consistency.cpp \
        goto-programs/goto_program_validate.cpp \

unit/goto-programs/goto_model_function_type_consistency.cpp

@@ -35,7 +35,10 @@ SCENARIO(
     goto_model.goto_functions.function_map[function_symbol.name].type =
       fun_type1;
 
-    goto_model_validation_optionst validation_options{false};
+    goto_model_validation_optionst validation_options;
+    // required as this test has no entry point, but calls the top-level
+    // 'goto_model.validate()'
+    validation_options.entry_point_exists = false;
 
     WHEN("Symbol table has the right type")
     {