Check some assumptions about goto programs before starting an analysis

src/cbmc/cbmc_parse_options.cpp

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

src/clobber/clobber_parse_options.cpp

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

src/goto-cc/compile.cpp

@@ -129,6 +129,12 @@ bool compilet::doit()
       return true;
   }
 
+  if(compiled_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return true;
+  }
+
   return
     warning_is_fatal &&
     get_message_handler().get_message_count(messaget::M_WARNING)!=

src/goto-diff/goto_diff_parse_options.cpp

@@ -278,6 +278,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(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
+  if(goto_model2.goto_functions.check_internal_invariants(*this))
+  {
+    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

@@ -868,6 +868,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(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    throw 0;
+  }
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()

src/goto-programs/goto_functions.cpp

@@ -30,3 +30,16 @@ void get_local_identifiers(
       dest.insert(identifier);
   }
 }
+
+/// Ensure that all functions satisfy all assumptions about
+/// consistent goto programs.
+/// \param msg Message output
+/// \return True, iff at least one invariant is violated
+bool goto_functionst::check_internal_invariants(messaget &msg) const
+{
+  forall_goto_functions(it, *this)
+    if(it->second.body.check_internal_invariants(msg))
+      return true;
+
+  return false;
+}

src/goto-programs/goto_functions.h

@@ -43,6 +43,8 @@ class goto_functionst:public goto_functions_templatet<goto_programt>
     goto_functions_templatet::operator=(std::move(other));
     return *this;
   }
+
+  bool check_internal_invariants(messaget &msg) const;
 };
 
 #define Forall_goto_functions(it, functions) \

src/goto-programs/goto_program.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include <util/message.h>
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
@@ -483,3 +484,129 @@ std::string as_string(
 
   return "";
 }
+
+/// Ensure the current goto_programt satisfies all assumptions
+/// about consistent goto programs.
+/// \param msg Message output
+/// \return True, iff at least one invariant is violated
+bool goto_programt::check_internal_invariants(messaget &msg) const
+{
+  if(empty())
+    return false;
+
+  unsigned prev_loc_number=0;
+  bool prev_loc_number_set=false;
+
+  forall_goto_program_instructions(it, *this)
+  {
+    const goto_programt::instructiont &ins=*it;
+
+    if(ins.check_internal_invariants(msg))
+      return true;
+
+    if(prev_loc_number_set &&
+       ins.location_number<=prev_loc_number)
+    {
+      msg.error().source_location=ins.source_location;
+      msg.error() << "location number not strictly increasing"
+                  << messaget::eom;
+      return true;
+    }
+    else if(!prev_loc_number_set)
+    {
+      prev_loc_number=ins.location_number;
+      prev_loc_number_set=true;
+    }
+
+    switch(ins.type)
+    {
+      case GOTO:
+      case ASSUME:
+      case ASSERT:
+        if(ins.guard.type()!=bool_typet())
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " has non-Boolean guard"
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case OTHER:
+      case SKIP:
+      case LOCATION:
+      case END_FUNCTION:
+      case START_THREAD:
+      case END_THREAD:
+      case ATOMIC_BEGIN:
+      case ATOMIC_END:
+      case RETURN:
+        break;
+      case ASSIGN:
+        if(ins.code.get_statement()!=ID_assign)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        return false;
+      case DECL:
+        if(ins.code.get_statement()!=ID_decl)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        else if(to_code_decl(ins.code).symbol().id()!=ID_symbol)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << "declaration operand is not a symbol"
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case DEAD:
+        if(ins.code.get_statement()!=ID_dead)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case FUNCTION_CALL:
+        if(ins.code.get_statement()!=ID_function_call)
+        {
+          msg.error().source_location=ins.source_location;
+          msg.error() << ins.type << " instruction has code "
+                      << ins.code.get_statement()
+                      << messaget::eom;
+          return true;
+        }
+        break;
+      case THROW:
+      case CATCH:
+        break;
+      case NO_INSTRUCTION_TYPE:
+        msg.error().source_location=ins.source_location;
+        msg.error() << ins.type << " not permitted"
+                    << messaget::eom;
+        return true;
+    }
+  }
+
+  // the last instruction must be END_FUNCTION
+  if(!get_end_function()->is_end_function())
+  {
+    msg.error().source_location=get_end_function()->source_location;
+    msg.error() << "end of function is of type "
+                << get_end_function()->type << messaget::eom;
+    return true;
+  }
+
+  return false;
+}

src/goto-programs/goto_program.h

@@ -64,6 +64,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(messaget &msg) const;
 };
 
 #define forall_goto_program_instructions(it, program) \

src/goto-programs/goto_program_template.h

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <string>
 
+#include <util/invariant.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 #include <util/source_location.h>
@@ -262,6 +264,84 @@ class goto_program_templatet
       instruction_id_builder << type;
       return instruction_id_builder.str();
     }
+
+    /// Ensure the current instruction satisfies all assumptions
+    /// within consistent goto programs.
+    /// \param msg Message output
+    /// \return True, iff at least one invariant is violated
+    bool check_internal_invariants(messaget &msg) const
+    {
+      if(function.empty())
+      {
+        msg.error().source_location=source_location;
+        msg.error() << "instruction has no function name"
+                    << messaget::eom;
+        return true;
+      }
+
+      switch(type)
+      {
+        case GOTO:
+        case ASSUME:
+        case ASSERT:
+          if(code!=irept() && code.is_not_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has non-nil code\n"
+                        << code.pretty() << messaget::eom;
+            return true;
+          }
+          else if(guard.is_nil() || guard==irept())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has nil guard"
+                        << messaget::eom;
+            return true;
+          }
+          return false;
+        case OTHER:
+          return false;
+        case SKIP:
+        case LOCATION:
+        case END_FUNCTION:
+          if(code!=irept() && code.is_not_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has non-nil code\n"
+                        << code.pretty() << messaget::eom;
+            return true;
+          }
+          return false;
+        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:
+        case DECL:
+        case DEAD:
+        case FUNCTION_CALL:
+          if(code==irept() || code.is_nil())
+          {
+            msg.error().source_location=source_location;
+            msg.error() << type << " has nil code"
+                        << messaget::eom;
+            return true;
+          }
+          return false;
+        case THROW:
+          return false;
+        case CATCH:
+          return false;
+        default:
+          return true;
+      }
+    }
   };
 
   typedef std::list<instructiont> instructionst;
@@ -466,9 +546,17 @@ class goto_program_templatet
 
   targett get_end_function()
   {
-    assert(!instructions.empty());
+    PRECONDITION(!instructions.empty());
+    const auto end_function=std::prev(instructions.end());
+    DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
+    return end_function;
+  }
+
+  const_targett get_end_function() const
+  {
+    PRECONDITION(!instructions.empty());
     const auto end_function=std::prev(instructions.end());
-    assert(end_function->is_end_function());
+    DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
     return end_function;
   }
 

src/musketeer/musketeer_parse_options.cpp

@@ -141,6 +141,12 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
     throw 0;
 
   config.set_from_symbol_table(symbol_table);
+
+  if(goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    throw 0;
+  }
 }
 
 void goto_fence_inserter_parse_optionst::instrument_goto_program(

src/symex/symex_parse_options.cpp

@@ -138,6 +138,12 @@ int symex_parse_optionst::doit()
   if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
     return 6;
 
+  if(goto_model.goto_functions.check_internal_invariants(*this))
+  {
+    error() << "GOTO program violates internal invariants" << eom;
+    return 6;
+  }
+
   if(process_goto_program(options))
     return 6;