Merge pull request #2968 from xbauch/cleanup_goto-s-z

Invariant cleanup goto programs sz

Author: petr-bauch

src/goto-programs/set_properties.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "set_properties.h"
 
+#include <util/exception_utils.h>
+
 #include <algorithm>
 #include <unordered_set>
 
@@ -111,7 +113,9 @@ void set_properties(
       set_properties(it->second.body, property_set);
 
   if(!property_set.empty())
-    throw "property "+id2string(*property_set.begin())+" not found";
+    throw invalid_command_line_argument_exceptiont(
+      "property " + id2string(*property_set.begin()) + " unknown",
+      "--property id");
 }
 
 void label_properties(goto_functionst &goto_functions)

src/goto-programs/slice_global_inits.cpp

@@ -21,6 +21,8 @@ Date:   December 2016
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
+#include <util/invariant.h>
+
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/remove_skip.h>
 
@@ -32,8 +34,8 @@ void slice_global_inits(goto_modelt &goto_model)
   const irep_idt entry_point=goto_functionst::entry_point();
   goto_functionst &goto_functions=goto_model.goto_functions;
 
-  if(!goto_functions.function_map.count(entry_point))
-    throw "entry point not found";
+  if(goto_functions.function_map.count(entry_point) == 0)
+    throw user_input_error_exceptiont("entry point not found");
 
   // Get the call graph restricted to functions reachable from
   // the entry point:
@@ -73,7 +75,8 @@ void slice_global_inits(goto_modelt &goto_model)
 
   goto_functionst::function_mapt::iterator f_it;
   f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
-  assert(f_it!=goto_functions.function_map.end());
+  if(f_it == goto_functions.function_map.end())
+    throw incorrect_goto_program_exceptiont("initialize function not found");
 
   goto_programt &goto_program=f_it->second.body;
 

src/goto-programs/slice_global_inits.h

@@ -14,8 +14,27 @@ Date:   December 2016
 #ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
 #define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
 
+#include <util/exception_utils.h>
+
 class goto_modelt;
 
+class user_input_error_exceptiont : public cprover_exception_baset
+{
+public:
+  explicit user_input_error_exceptiont(std::string message)
+    : message(std::move(message))
+  {
+  }
+
+  std::string what() const override
+  {
+    return message;
+  }
+
+private:
+  std::string message;
+};
+
 void slice_global_inits(goto_modelt &);
 
 #endif

src/goto-programs/string_instrumentation.cpp

@@ -16,9 +16,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/message.h>
-#include <util/std_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/format_strings.h>
@@ -279,9 +280,9 @@ void string_instrumentationt::do_sprintf(
 
   if(arguments.size()<2)
   {
-    error().source_location=target->source_location;
-    error() << "sprintf expected to have two or more arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "sprintf expected to have two or more arguments",
+      target->source_location);
   }
 
   goto_programt tmp;
@@ -321,10 +322,9 @@ void string_instrumentationt::do_snprintf(
 
   if(arguments.size()<3)
   {
-    error().source_location=target->source_location;
-    error() << "snprintf expected to have three or more arguments"
-            << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "snprintf expected to have three or more arguments",
+      target->source_location);
   }
 
   goto_programt tmp;
@@ -364,9 +364,8 @@ void string_instrumentationt::do_fscanf(
 
   if(arguments.size()<2)
   {
-    error().source_location=target->source_location;
-    error() << "fscanf expected to have two or more arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "fscanf expected to have two or more arguments", target->source_location);
   }
 
   goto_programt tmp;
@@ -650,9 +649,8 @@ void string_instrumentationt::do_strchr(
 
   if(arguments.size()!=2)
   {
-    error().source_location=target->source_location;
-    error() << "strchr expected to have two arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "strchr expected to have two arguments", target->source_location);
   }
 
   goto_programt tmp;
@@ -677,9 +675,8 @@ void string_instrumentationt::do_strrchr(
 
   if(arguments.size()!=2)
   {
-    error().source_location=target->source_location;
-    error() << "strrchr expected to have two arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "strrchr expected to have two arguments", target->source_location);
   }
 
   goto_programt tmp;
@@ -704,9 +701,8 @@ void string_instrumentationt::do_strstr(
 
   if(arguments.size()!=2)
   {
-    error().source_location=target->source_location;
-    error() << "strstr expected to have two arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "strstr expected to have two arguments", target->source_location);
   }
 
   goto_programt tmp;
@@ -738,9 +734,8 @@ void string_instrumentationt::do_strtok(
 
   if(arguments.size()!=2)
   {
-    error().source_location=target->source_location;
-    error() << "strtok expected to have two arguments" << eom;
-    throw 0;
+    throw incorrect_source_program_exceptiont(
+      "strtok expected to have two arguments", target->source_location);
   }
 
   goto_programt tmp;

src/goto-programs/string_instrumentation.h

@@ -14,9 +14,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_functions.h"
 
+#include <util/exception_utils.h>
+
 class message_handlert;
 class goto_modelt;
 
+class incorrect_source_program_exceptiont : public cprover_exception_baset
+{
+public:
+  incorrect_source_program_exceptiont(
+    std::string message,
+    source_locationt source_location)
+    : message(std::move(message)), source_location(std::move(source_location))
+  {
+  }
+  std::string what() const override
+  {
+    return message + " (at: " + source_location.as_string() + ")";
+  }
+
+private:
+  std::string message;
+  source_locationt source_location;
+};
+
 void string_instrumentation(
   symbol_tablet &,
   message_handlert &,

src/goto-programs/vcd_goto_trace.cpp

@@ -13,7 +13,6 @@ Date: June 2011
 
 #include "vcd_goto_trace.h"
 
-#include <cassert>
 #include <ctime>
 
 #include <util/numbering.h>
@@ -55,8 +54,7 @@ std::string as_vcd_binary(
   }
   else if(expr.id()==ID_union)
   {
-    assert(expr.operands().size()==1);
-    return as_vcd_binary(expr.op0(), ns);
+    return as_vcd_binary(to_union_expr(expr).op(), ns);
   }
 
   // build "xxx"

src/goto-programs/wp.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/base_type.h>
 
+#include <util/invariant.h>
+
 bool has_nondet(const exprt &dest)
 {
   forall_operands(it, dest)
@@ -263,6 +265,6 @@ exprt wp(
     return post; // ignored
   else if(statement==ID_fence)
     return post; // ignored
-  else
-    throw "sorry, wp("+id2string(statement)+"...) not implemented";
+  INVARIANT_WITH_DIAGNOSTICS(
+    false, "sorry, wp(", id2string(statement), "...) is not implemented");
 }

src/goto-programs/write_goto_binary.cpp

@@ -13,8 +13,10 @@ Author: CM Wintersteiger
 
 #include <fstream>
 
-#include <util/message.h>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
 #include <util/irep_serialization.h>
+#include <util/message.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_model.h>
@@ -148,22 +150,18 @@ bool write_goto_binary(
   irep_serializationt::ireps_containert irepc;
   irep_serializationt irepconverter(irepc);
 
-  switch(version)
-  {
-  case 1:
-  case 2:
-  case 3:
-    throw "version no longer supported";
-
-  case 4:
+  const int current_goto_version = 4;
+  if(version < current_goto_version)
+    throw invalid_command_line_argument_exceptiont(
+      "version " + std::to_string(version) + " no longer supported",
+      "supported version = " + std::to_string(current_goto_version));
+  else if(version > current_goto_version)
+    throw invalid_command_line_argument_exceptiont(
+      "unknown goto binary version " + std::to_string(version),
+      "supported version = " + std::to_string(current_goto_version));
+  else
     return write_goto_binary_v4(
       out, symbol_table, goto_functions, irepconverter);
-
-  default:
-    throw "unknown goto binary version";
-  }
-
-  return false;
 }
 
 /// Writes a goto program to disc

src/util/exception_utils.cpp

@@ -64,6 +64,17 @@ incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
 std::string incorrect_goto_program_exceptiont::what() const
 {
   return message + " (at: " + source_location.as_string() + ")";
+  if(source_location.is_nil())
+    return message;
+  else
+    return message + " (at: " + source_location.as_string() + ")";
+}
+
+incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
+  std::string message)
+  : message(std::move(message))
+{
+  source_location.make_nil();
 }
 
 unsupported_operation_exceptiont::unsupported_operation_exceptiont(

src/util/exception_utils.h

@@ -86,6 +86,7 @@ class incorrect_goto_program_exceptiont : public cprover_exception_baset
   incorrect_goto_program_exceptiont(
     std::string message,
     source_locationt source_location);
+  explicit incorrect_goto_program_exceptiont(std::string message);
   std::string what() const override;
 
 private: