Merge pull request #2967 from hannes-steffenhagen-diffblue/invariant_cleanup-goto_programs-jr

Invariant cleanup goto programs jr

Author: hannes-steffenhagen-diffblue

regression/goto-instrument/replace-calls-03/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g
-Functions f and g are not type-compatible
-^EXIT=11$
+functions f and g are not type-compatible
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-instrument/replace-calls-04/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g
-Functions f and g are not type-compatible
-^EXIT=11$
+functions f and g are not type-compatible
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-instrument/replace-calls-05/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g --replace-calls h:f
-Function f cannot both be replaced and be a replacement
-^EXIT=11$
+function f cannot both be replaced and be a replacement
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/goto-programs/lazy_goto_model.cpp

@@ -11,6 +11,7 @@
 
 #include <util/cmdline.h>
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
 #include <util/unicode.h>
 
@@ -96,8 +97,11 @@ void lazy_goto_modelt::initialize(
   const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    msg.error() << "Please provide a program" << messaget::eom;
-    throw 0;
+    throw invalid_command_line_argument_exceptiont(
+      "no program provided",
+      "source file names",
+      "one or more paths to a goto binary or a source file in a supported "
+      "language");
   }
 
   std::vector<std::string> binaries, sources;
@@ -124,21 +128,17 @@ void lazy_goto_modelt::initialize(
 
       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=add_language_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 invalid_source_file_exceptiont(
+          "failed to figure out type of file `" + filename + '\'');
       }
 
       languaget &language=*lf.language;
@@ -149,8 +149,7 @@ void lazy_goto_modelt::initialize(
 
       if(language.parse(infile, filename))
       {
-        msg.error() << "PARSING ERROR" << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont("PARSING ERROR");
       }
 
       lf.get_modules();
@@ -160,8 +159,7 @@ void lazy_goto_modelt::initialize(
 
     if(language_files.typecheck(symbol_table))
     {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      throw invalid_source_file_exceptiont("CONVERSION ERROR");
     }
   }
 
@@ -170,7 +168,12 @@ void lazy_goto_modelt::initialize(
     msg.status() << "Reading GOTO program from file" << messaget::eom;
 
     if(read_object_and_link(file, *goto_model, message_handler))
-      throw 0;
+    {
+      source_locationt source_location;
+      source_location.set_file(file);
+      throw incorrect_goto_program_exceptiont(
+        "failed to read/link goto model", source_location);
+    }
   }
 
   bool binaries_provided_start =
@@ -205,8 +208,7 @@ void lazy_goto_modelt::initialize(
 
   if(entry_point_generation_failed)
   {
-    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
-    throw 0;
+    throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
   }
 
   // stupid hack

src/goto-programs/link_goto_model.cpp

@@ -18,6 +18,7 @@ Author: Michael Tautschnig, Daniel Kroening
 #include <util/rename_symbol.h>
 
 #include <linking/linking_class.h>
+#include <util/exception_utils.h>
 
 #include "goto_model.h"
 
@@ -171,15 +172,18 @@ void link_goto_model(
                    message_handler);
 
   if(linking.typecheck_main())
-    throw 0;
-
+  {
+    throw invalid_source_file_exceptiont("typechecking main failed");
+  }
   if(link_functions(
-      dest.symbol_table,
-      dest.goto_functions,
-      src.symbol_table,
-      src.goto_functions,
-      linking.rename_symbol,
-      weak_symbols,
-      linking.object_type_updates))
-    throw 0;
+       dest.symbol_table,
+       dest.goto_functions,
+       src.symbol_table,
+       src.goto_functions,
+       linking.rename_symbol,
+       weak_symbols,
+       linking.object_type_updates))
+  {
+    throw invalid_source_file_exceptiont("linking failed");
+  }
 }

src/goto-programs/loop_ids.cpp

@@ -79,7 +79,7 @@ void show_loop_ids_json(
   const goto_programt &goto_program,
   json_arrayt &loops)
 {
-  assert(ui==ui_message_handlert::uit::JSON_UI); // use function above
+  PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above
 
   forall_goto_program_instructions(it, goto_program)
   {

src/goto-programs/osx_fat_reader.cpp

@@ -11,8 +11,9 @@ Module: Read Mach-O
 
 #include "osx_fat_reader.h"
 
-#include <cassert>
 #include <cstdlib>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
 
 #ifdef __APPLE__
 #include <mach-o/fat.h>
@@ -46,12 +47,13 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
   in.read(reinterpret_cast<char*>(&fh), sizeof(struct fat_header));
 
   if(!in)
-    throw "failed to read OSX fat header";
+    throw system_exceptiont("failed to read OSX fat header");
 
   if(!is_osx_fat_magic(reinterpret_cast<char*>(&(fh.magic))))
-    throw "OSX fat header malformed (magic)"; // NOLINT(readability/throw)
+    throw deserialization_exceptiont("OSX fat header malformed (magic)");
 
-  assert(sizeof(fh.nfat_arch)==4);
+  static_assert(
+    sizeof(fh.nfat_arch) == 4, "fat_header::nfat_arch is of type uint32_t");
   unsigned narch=__builtin_bswap32(fh.nfat_arch);
 
   for(unsigned i=0; !has_gb_arch && i<narch; ++i)
@@ -61,9 +63,10 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
     // NOLINTNEXTLINE(readability/identifiers)
     in.read(reinterpret_cast<char*>(&fa), sizeof(struct fat_arch));
 
-    assert(sizeof(fa.cputype)==4 &&
-           sizeof(fa.cpusubtype)==4 &&
-           sizeof(fa.size)==4);
+    static_assert(
+      sizeof(fa.cputype) == 4 && sizeof(fa.cpusubtype) == 4 &&
+        sizeof(fa.size) == 4,
+      "This requires a specific fat architecture");
     int cputype=__builtin_bswap32(fa.cputype);
     int cpusubtype=__builtin_bswap32(fa.cpusubtype);
     unsigned size=__builtin_bswap32(fa.size);
@@ -79,7 +82,7 @@ bool osx_fat_readert::extract_gb(
   const std::string &source,
   const std::string &dest) const
 {
-  assert(has_gb_arch);
+  PRECONDITION(has_gb_arch);
 
   return run("lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source});
 }

src/goto-programs/parameter_assignments.cpp

@@ -46,7 +46,7 @@ void parameter_assignmentst::do_function_calls(
 
       // add x=y for f(y) where x is the parameter
 
-      assert(function_call.function().id()==ID_symbol);
+      PRECONDITION(function_call.function().id() == ID_symbol);
 
       const irep_idt &identifier=
         to_symbol_expr(function_call.function()).get_identifier();

src/goto-programs/pointer_arithmetic.cpp

@@ -32,32 +32,33 @@ void pointer_arithmetict::read(const exprt &src)
   }
   else if(src.id()==ID_minus)
   {
-    assert(src.operands().size()==2);
-    read(src.op0());
-    const unary_minus_exprt o(src.op1(), src.op1().type());
-    add_to_offset(o);
+    auto const &minus_src = to_minus_expr(src);
+    read(minus_src.op0());
+    const unary_minus_exprt unary_minus(
+      minus_src.op1(), minus_src.op1().type());
+    add_to_offset(unary_minus);
   }
   else if(src.id()==ID_address_of)
   {
-    assert(src.operands().size()==1);
-    if(src.op0().id()==ID_index)
+    auto const &address_of_src = to_address_of_expr(src);
+    if(address_of_src.op().id() == ID_index)
     {
-      const index_exprt &index_expr=
-        to_index_expr(src.op0());
+      const index_exprt &index_expr = to_index_expr(address_of_src.op());
 
       if(index_expr.index().is_zero())
-        make_pointer(src);
+        make_pointer(address_of_src);
       else
       {
         add_to_offset(index_expr.index());
         // produce &x[0] + i instead of &x[i]
-        exprt new_src=src;
-        new_src.op0().op1()=from_integer(0, index_expr.index().type());
-        make_pointer(new_src);
+        auto new_address_of_src = address_of_src;
+        new_address_of_src.op().op1() =
+          from_integer(0, index_expr.index().type());
+        make_pointer(new_address_of_src);
       }
     }
     else
-      make_pointer(src);
+      make_pointer(address_of_src);
   }
   else
     make_pointer(src);

src/goto-programs/printf_formatter.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "printf_formatter.h"
 
-#include <cassert>
 #include <sstream>
 
 #include <util/c_types.h>

src/goto-programs/read_bin_goto_object.cpp

@@ -145,7 +145,10 @@ static bool read_bin_goto_object_v4(
       {
         unsigned n=*nit;
         rev_target_mapt::const_iterator entry=rev_target_map.find(n);
-        assert(entry!=rev_target_map.end());
+        INVARIANT(
+          entry != rev_target_map.end(),
+          "something from the target map should also be in the reverse target "
+          "map");
         ins->targets.push_back(entry->second);
       }
     }