Invariant cleanup goto programs i r

regression/cbmc/return6/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 f_def.c
-^EXIT=6$
+^EXIT=1$
 ^SIGNAL=0$
 CONVERSION ERROR
 --

src/goto-programs/initialize_goto_model.cpp

@@ -1,3 +1,5 @@
+#include <utility>
+
 /*******************************************************************\
 
 Module: Get a Goto Program
@@ -21,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 
 #include <goto-programs/rebuild_goto_start_function.h>
+#include <util/exception_utils.h>
 
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
@@ -33,8 +36,9 @@ goto_modelt initialize_goto_model(
   const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    msg.error() << "Please provide a program" << messaget::eom;
-    throw 0;
+    throw invalid_user_input_exceptiont("missing program argument",
+      "",
+      "one or more paths to program files");
   }
 
   std::vector<std::string> binaries, sources;
@@ -66,21 +70,20 @@ goto_modelt initialize_goto_model(
 
       if(!infile)
       {
-        msg.error() << "failed to open input file `" << filename
-          << '\'' << messaget::eom;
-        throw 0;
+        throw system_exceptiont(
+          "failed to open input file `" + filename + '\'');
       }
 
       language_filet &lf=language_files.add_file(filename);
       lf.language=get_language_from_filename(filename);
 
       if(lf.language==nullptr)
       {
+
         source_locationt location;
         location.set_file(filename);
-        msg.error().source_location=location;
-        msg.error() << "failed to figure out type of file" << messaget::eom;
-        throw 0;
+        throw goto_model_initialization_errort(
+          "failed to figure out type of file", location);
       }
 
       languaget &language=*lf.language;
@@ -91,8 +94,7 @@ goto_modelt initialize_goto_model(
 
       if(language.parse(infile, filename))
       {
-        msg.error() << "PARSING ERROR" << messaget::eom;
-        throw 0;
+        throw goto_model_initialization_errort("language parsing failed");
       }
 
       lf.get_modules();
@@ -102,17 +104,19 @@ goto_modelt initialize_goto_model(
 
     if(language_files.typecheck(goto_model.symbol_table))
     {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      throw goto_model_initialization_errort(
+        "type-checking of interfaces/files/modules failed");
     }
   }
 
   for(const auto &file : binaries)
   {
     msg.status() << "Reading GOTO program from file" << messaget::eom;
 
-    if(read_object_and_link(file, goto_model, message_handler))
-      throw 0;
+    if(read_object_and_link(file, goto_model, message_handler)) {
+      throw goto_model_initialization_errort(
+        "failed to read object or link in file `" + file + '\'');
+    }
   }
 
   bool binaries_provided_start=
@@ -149,14 +153,13 @@ goto_modelt initialize_goto_model(
 
   if(entry_point_generation_failed)
   {
-    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
-    throw 0;
+    throw goto_model_initialization_errort("failed to generate entry point");
   }
 
   if(language_files.final(goto_model.symbol_table))
   {
-    msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
-    throw 0;
+    throw goto_model_initialization_errort(
+      "failed to finish final conversion adjustments");
   }
 
   msg.status() << "Generating GOTO Program" << messaget::eom;
@@ -172,3 +175,22 @@ goto_modelt initialize_goto_model(
 
   return goto_model;
 }
+
+goto_model_initialization_errort::goto_model_initialization_errort(std::string message)
+  : goto_model_initialization_errort(std::move(message), source_locationt())
+{}
+
+std::string goto_model_initialization_errort::what() const noexcept {
+  std::string what_msg = message;
+  if(source_location.is_not_nil())
+  {
+    what_msg += "\nsource location: " + source_location.as_string();
+  }
+  return what_msg;
+}
+
+goto_model_initialization_errort::goto_model_initialization_errort(std::string message, source_locationt source_location)
+  : message(std::move(message)), source_location(std::move(source_location))
+{
+
+}

src/goto-programs/initialize_goto_model.h

@@ -16,6 +16,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cmdline.h>
 
 #include "goto_model.h"
+#include <string>
+#include <util/exception_utils.h>
+
+class goto_model_initialization_errort : public cprover_exception_baset
+{
+public:
+  explicit goto_model_initialization_errort(std::string message);
+  goto_model_initialization_errort(std::string message, source_locationt source_location);
+  std::string what() const noexcept override;
+private:
+  std::string message;
+  source_locationt source_location;
+};
 
 goto_modelt initialize_goto_model(
   const cmdlinet &cmdline,

src/goto-programs/interpreter.cpp

@@ -69,12 +69,12 @@ void interpretert::initialize(bool init)
     main_it=goto_functions.function_map.find(goto_functionst::entry_point());
 
   if(main_it==goto_functions.function_map.end())
-    throw "main not found";
+    throw interpreter_errort("main not found");
 
   const goto_functionst::goto_functiont &goto_function=main_it->second;
 
   if(!goto_function.body_available())
-    throw "main has no body";
+    throw interpreter_errort("main has no body");
 
   pc=goto_function.body.instructions.begin();
   function=main_it;
@@ -291,8 +291,11 @@ void interpretert::step()
 
   case RETURN:
     trace_step.type=goto_trace_stept::typet::FUNCTION_RETURN;
-    if(call_stack.empty())
-      throw "RETURN without call"; // NOLINT(readability/throw)
+    if(call_stack.empty()) {
+      // FIXME I left this as an exception because I think this
+      //       could happen if fed with a broken goto program?
+      throw interpreter_errort("RETURN without call"); // NOLINT(readability/throw)
+    }
 
     if(pc->code.operands().size()==1 &&
        call_stack.top().return_value_address!=0)
@@ -317,19 +320,20 @@ void interpretert::step()
 
   case START_THREAD:
     trace_step.type=goto_trace_stept::typet::SPAWN;
-    throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
+    // Could be triggered by wrong input, therefore throw?
+    throw interpreter_errort("START_THREAD not yet implemented"); // NOLINT(readability/throw)
 
   case END_THREAD:
-    throw "END_THREAD not yet implemented"; // NOLINT(readability/throw)
+    throw interpreter_errort("END_THREAD not yet implemented"); // NOLINT(readability/throw)
     break;
 
   case ATOMIC_BEGIN:
     trace_step.type=goto_trace_stept::typet::ATOMIC_BEGIN;
-    throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw)
+    throw interpreter_errort("ATOMIC_BEGIN not yet implemented"); // NOLINT(readability/throw)
 
   case ATOMIC_END:
     trace_step.type=goto_trace_stept::typet::ATOMIC_END;
-    throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw)
+    throw interpreter_errort("ATOMIC_END not yet implemented"); // NOLINT(readability/throw)
 
   case DEAD:
     trace_step.type=goto_trace_stept::typet::DEAD;
@@ -359,7 +363,7 @@ void interpretert::step()
   case CATCH:
     break;
   default:
-    throw "encountered instruction with undefined instruction type";
+    UNREACHABLE; // I'm assuming we'd catch such a thing before this point
   }
   pc=next_pc;
 }
@@ -369,11 +373,8 @@ void interpretert::execute_goto()
 {
   if(evaluate_boolean(pc->guard))
   {
-    if(pc->targets.empty())
-      throw "taken goto without target";
-
-    if(pc->targets.size()>=2)
-      throw "non-deterministic goto encountered";
+    DATA_INVARIANT(pc->targets.size() == 1,
+      "a goto should have exactly one target location");
 
     next_pc=pc->targets.front();
   }
@@ -383,6 +384,10 @@ void interpretert::execute_goto()
 void interpretert::execute_other()
 {
   const irep_idt &statement=pc->code.get_statement();
+  PRECONDITION(statement == ID_expression
+  || statement == ID_array_set
+  || statement == ID_output);
+
   if(statement==ID_expression)
   {
     DATA_INVARIANT(
@@ -410,8 +415,6 @@ void interpretert::execute_other()
   {
     return;
   }
-  else
-    throw "unexpected OTHER statement: "+id2string(statement);
 }
 
 void interpretert::execute_decl()
@@ -427,8 +430,7 @@ struct_typet::componentt interpretert::get_component(
 {
   const symbolt &symbol=ns.lookup(object);
   const typet real_type=ns.follow(symbol.type);
-  if(real_type.id()!=ID_struct)
-    throw "request for member of non-struct";
+  PRECONDITION(real_type.id() == ID_struct);
 
   const struct_typet &struct_type=to_struct_type(real_type);
   const struct_typet::componentst &components=struct_type.components();
@@ -443,7 +445,9 @@ struct_typet::componentt interpretert::get_component(
     tmp_offset-=get_size(c.type());
   }
 
-  throw "access out of struct bounds";
+  // FIXME not sure if its possible to catch this in advance
+  //       so I've left it as an exception for now
+  throw interpreter_errort("access out of struct bounds");
 }
 
 /// returns the type object corresponding to id
@@ -639,7 +643,7 @@ exprt interpretert::get_value(
     error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
             << " > object count " << memory.size() << eom;
 
-    throw "interpreter: reading from invalid pointer";
+    throw interpreter_errort("interpreter: reading from invalid pointer");
   }
   else if(real_type.id()==ID_string)
   {
@@ -729,15 +733,15 @@ void interpretert::assign(
 void interpretert::execute_assume()
 {
   if(!evaluate_boolean(pc->guard))
-    throw "assumption failed";
+    throw interpreter_errort("assumption failed");
 }
 
 void interpretert::execute_assert()
 {
   if(!evaluate_boolean(pc->guard))
   {
     if((target_assert==pc) || stop_on_assertion)
-      throw "program assertion reached";
+      throw interpreter_errort("program assertion reached");
     else if(show)
       error() << "assertion failed at " << pc->location_number
               << "\n" << eom;
@@ -753,9 +757,9 @@ void interpretert::execute_function_call()
   mp_integer address=evaluate_address(function_call.function());
 
   if(address==0)
-    throw "function call to NULL";
+    throw interpreter_errort("function call to NULL");
   else if(address>=memory.size())
-    throw "out-of-range function call";
+    throw interpreter_errort("out-of-range function call");
 
   // Retrieve the empty last trace step struct we pushed for this step
   // of the interpreter run to fill it with the corresponding data
@@ -769,8 +773,8 @@ void interpretert::execute_function_call()
   const goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);
 
-  if(f_it==goto_functions.function_map.end())
-    throw "failed to find function "+id2string(identifier);
+  INVARIANT(f_it != goto_functions.function_map.end(),
+    "FIXME I don't think this can happen if we have a typechecking phase before this?");
 
   // return value
   mp_integer return_value_address;
@@ -815,8 +819,8 @@ void interpretert::execute_function_call()
     const code_typet::parameterst &parameters=
       to_code_type(f_it->second.type).parameters();
 
-    if(argument_values.size()<parameters.size())
-      throw "not enough arguments";
+    INVARIANT(argument_values.size() != parameters.size(),
+              "FIXME I don't think this can happen if we have a typechecking phase before this?");
 
     for(std::size_t i=0; i<parameters.size(); i++)
     {
@@ -1090,3 +1094,11 @@ void interpreter(
     message_handler);
   interpreter();
 }
+
+interpreter_errort::interpreter_errort(std::string message)
+  : message(message)
+{}
+
+std::string interpreter_errort::what() const noexcept {
+  return message;
+}

src/goto-programs/interpreter.h

@@ -13,9 +13,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_PROGRAMS_INTERPRETER_H
 
 #include <util/message.h>
+#include <util/exception_utils.h>
+
+#include <string>
 
 #include "goto_model.h"
 
+class interpreter_errort : public cprover_exception_baset
+{
+public:
+  explicit interpreter_errort(std::string message);
+  std::string what() const noexcept override;
+private:
+  std::string message;
+};
+
 void interpreter(
   const goto_modelt &,
   message_handlert &);

src/goto-programs/interpreter_class.h

@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_functions.h"
 #include "goto_trace.h"
 #include "json_goto_trace.h"
+#include "interpreter.h"
 
 class interpretert:public messaget
 {
@@ -279,8 +280,7 @@ class interpretert:public messaget
   {
     mp_vectort v;
     evaluate(expr, v);
-    if(v.size()!=1)
-      throw "invalid boolean value";
+    INVARIANT(v.size() == 1, "expression cannot be evaluated to a Boolean");
     return v.front()!=0;
   }