Check some assumptions about goto programs before starting an analysis

The current set of checks is certainly very incomplete, but at least provides
some entry points for adding further tests.

Author: tautschnig

src/cbmc/cbmc_parse_options.cpp

@@ -728,6 +728,12 @@ int cbmc_parse_optionst::get_goto_program(
 
     goto_convert(symbol_table, goto_functions, ui_message_handler);
 
+    if(goto_functions.check_internal_invariants())
+    {
+      error() << "GOTO program violates internal invariants" << eom;
+      return 6;
+    }
+
     if(process_goto_program(options, goto_functions))
       return 6;
 

src/clobber/clobber_parse_options.cpp

@@ -170,6 +170,12 @@ int clobber_parse_optionst::doit()
     if(get_goto_program(options, goto_functions))
       return 6;
 
+    if(goto_functions.check_internal_invariants())
+    {
+      error() << "GOTO program violates internal invariants" << eom;
+      return 6;
+    }
+
     label_properties(goto_functions);
 
     if(cmdline.isset("show-properties"))

src/goto-cc/compile.cpp

@@ -133,6 +133,12 @@ bool compilet::doit()
       return true;
   }
 
+  if(compiled_functions.check_internal_invariants())
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return true;
+  }
+
   return false;
 }
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -333,6 +333,18 @@ int goto_diff_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
+  if(goto_model1.goto_functions.check_internal_invariants())
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
+  if(goto_model2.goto_functions.check_internal_invariants())
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
   if(cmdline.isset("show-goto-functions"))
   {
     show_goto_functions(goto_model1, get_ui());

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -952,6 +952,12 @@ void goto_instrument_parse_optionst::get_goto_program()
 
   config.set(cmdline);
   config.set_from_symbol_table(symbol_table);
+
+  if(goto_functions.check_internal_invariants())
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    throw 0;
+  }
 }
 
 /*******************************************************************\

src/goto-programs/goto_functions.cpp

@@ -39,3 +39,25 @@ void get_local_identifiers(
       dest.insert(identifier);
   }
 }
+
+/*******************************************************************\
+
+Function: goto_functionst::check_internal_invariants
+
+  Inputs:
+
+ Outputs: Returns true iff an invariant is violated
+
+ Purpose: Ensure that all functions satisfy all assumptions
+          about consistent goto programs.
+
+\*******************************************************************/
+
+bool goto_functionst::check_internal_invariants() const
+{
+  forall_goto_functions(it, *this)
+    if(it->second.body.check_internal_invariants())
+      return true;
+
+  return false;
+}

src/goto-programs/goto_functions.h

@@ -17,6 +17,7 @@ Date: June 2003
 class goto_functionst:public goto_functions_templatet<goto_programt>
 {
 public:
+  bool check_internal_invariants() const;
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_program.cpp

@@ -609,3 +609,32 @@ std::string as_string(
 
   return "";
 }
+
+/*******************************************************************\
+
+Function: goto_programt::check_internal_invariants
+
+  Inputs:
+
+ Outputs: Returns true iff an invariant is violated
+
+ Purpose: Ensure the current goto_programt satisfies all assumptions
+          about consistent goto programs.
+
+\*******************************************************************/
+
+bool goto_programt::check_internal_invariants() const
+{
+  if(empty())
+    return false;
+
+  forall_goto_program_instructions(it, *this)
+    if(it->check_internal_invariants())
+      return true;
+
+  // the last instruction must be END_FUNCTION
+  if(!get_end_function()->is_end_function())
+    return true;
+
+  return false;
+}

src/goto-programs/goto_program.h

@@ -39,6 +39,8 @@ class goto_programt:public goto_program_templatet<codet, exprt>
   // get the variables in decl statements
   typedef std::set<irep_idt> decl_identifierst;
   void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
+
+  bool check_internal_invariants() const;
 };
 
 #define forall_goto_program_instructions(it, program) \

src/goto-programs/goto_program_template.h

@@ -250,6 +250,55 @@ class goto_program_templatet
       instruction_id_builder << type;
       return instruction_id_builder.str();
     }
+
+    bool check_internal_invariants() const
+    {
+      if(function.empty())
+        return true;
+
+      switch(type)
+      {
+        case GOTO:
+        case ASSUME:
+        case ASSERT:
+          if(code.is_not_nil() ||
+             guard.is_nil())
+            return true;
+          return false;
+        case OTHER:
+          return false;
+        case SKIP:
+        case LOCATION:
+        case END_FUNCTION:
+          return code.is_not_nil();
+        case START_THREAD:
+          return false;
+        case END_THREAD:
+          return false;
+        case ATOMIC_BEGIN:
+          return false;
+        case ATOMIC_END:
+          return false;
+        case RETURN:
+          return false;
+        case ASSIGN:
+          if(code.get_statement()!=ID_assign)
+            return true;
+          return false;
+        case DECL:
+          return code.is_nil();
+        case DEAD:
+          return code.is_nil();
+        case FUNCTION_CALL:
+          return code.is_nil();
+        case THROW:
+          return false;
+        case CATCH:
+          return false;
+        default:
+          return true;
+      }
+    }
   };
 
   typedef std::list<instructiont> instructionst;
@@ -460,6 +509,14 @@ class goto_program_templatet
     return end_function;
   }
 
+  const_targett get_end_function() const
+  {
+    assert(!instructions.empty());
+    const auto end_function=std::prev(instructions.end());
+    assert(end_function->is_end_function());
+    return end_function;
+  }
+
   //! Copy a full goto program, preserving targets
   void copy_from(const goto_program_templatet<codeT, guardT> &src);