diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h deleted file mode 100644 index 300c547974d..00000000000 --- a/src/goto-symex/equation_conversion_exceptions.h +++ /dev/null @@ -1,47 +0,0 @@ -/*******************************************************************\ - -Module: Symbolic Execution - -Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Exceptions that can be raised during the equation conversion phase - -#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H -#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H - -#include - -#include - -#include "ssa_step.h" - -class equation_conversion_exceptiont : public std::runtime_error -{ -public: - equation_conversion_exceptiont( - const std::string &message, - const SSA_stept &step) - : runtime_error(message), step(step) - { - std::ostringstream error_msg; - error_msg << runtime_error::what(); - error_msg << "\nSource GOTO statement: " << format(step.source.pc->code); - error_msg << "\nStep:\n"; - step.output(error_msg); - error_message = error_msg.str(); - } - - const char *what() const optional_noexcept override - { - return error_message.c_str(); - } - -private: - SSA_stept step; - std::string error_message; -}; - -#endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index c33cd895bd1..9d04578b48c 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -14,13 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include -#include -#include "equation_conversion_exceptions.h" #include "goto_symex_state.h" #include "ssa_step.h" @@ -329,24 +325,15 @@ void symex_target_equationt::constraint( void symex_target_equationt::convert(decision_proceduret &decision_procedure) { - try - { - convert_guards(decision_procedure); - convert_assignments(decision_procedure); - convert_decls(decision_procedure); - convert_assumptions(decision_procedure); - convert_assertions(decision_procedure); - convert_goto_instructions(decision_procedure); - convert_function_calls(decision_procedure); - convert_io(decision_procedure); - convert_constraints(decision_procedure); - } - catch(const equation_conversion_exceptiont &conversion_exception) - { - // unwrap the except and throw like normal - const std::string full_error = unwrap_exception(conversion_exception); - throw full_error; - } + convert_guards(decision_procedure); + convert_assignments(decision_procedure); + convert_decls(decision_procedure); + convert_assumptions(decision_procedure); + convert_assertions(decision_procedure); + convert_goto_instructions(decision_procedure); + convert_function_calls(decision_procedure); + convert_io(decision_procedure); + convert_constraints(decision_procedure); } void symex_target_equationt::convert_assignments( @@ -376,17 +363,8 @@ void symex_target_equationt::convert_decls( { // The result is not used, these have no impact on // the satisfiability of the formula. - try - { - decision_procedure.handle(step.cond_expr); - step.converted = true; - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested( - equation_conversion_exceptiont( - "Error converting decls for step", step)); - } + decision_procedure.handle(step.cond_expr); + step.converted = true; } } } @@ -405,16 +383,7 @@ void symex_target_equationt::convert_guards( mstream << messaget::eom; }); - try - { - step.guard_handle = decision_procedure.handle(step.guard); - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested( - equation_conversion_exceptiont( - "Error converting guard for step", step)); - } + step.guard_handle = decision_procedure.handle(step.guard); } } } @@ -436,16 +405,7 @@ void symex_target_equationt::convert_assumptions( mstream << messaget::eom; }); - try - { - step.cond_handle = decision_procedure.handle(step.cond_expr); - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested( - equation_conversion_exceptiont( - "Error converting assumptions for step", step)); - } + step.cond_handle = decision_procedure.handle(step.cond_expr); } } } @@ -468,16 +428,7 @@ void symex_target_equationt::convert_goto_instructions( mstream << messaget::eom; }); - try - { - step.cond_handle = decision_procedure.handle(step.cond_expr); - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested( - equation_conversion_exceptiont( - "Error converting goto instructions for step", step)); - } + step.cond_handle = decision_procedure.handle(step.cond_expr); } } } @@ -495,16 +446,8 @@ void symex_target_equationt::convert_constraints( mstream << messaget::eom; }); - try - { - decision_procedure.set_to_true(step.cond_expr); - step.converted = true; - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested(equation_conversion_exceptiont( - "Error converting constraints for step", step)); - } + decision_procedure.set_to_true(step.cond_expr); + step.converted = true; } } } @@ -569,16 +512,7 @@ void symex_target_equationt::convert_assertions( step.cond_expr); // do the conversion - try - { - step.cond_handle = decision_procedure.handle(implication); - } - catch(const bitvector_conversion_exceptiont &) - { - util_throw_with_nested( - equation_conversion_exceptiont( - "Error converting assertions for step", step)); - } + step.cond_handle = decision_procedure.handle(implication); // store disjunct disjuncts.push_back(not_exprt(step.cond_handle)); diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index b68f09aa023..9fd2dfb43a6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -171,9 +171,6 @@ bvt boolbvt::conversion_failed(const exprt &expr) /// \param expr: Expression to convert /// \return A vector of literals corresponding to the outputs of the Boolean /// circuit -/// \throws bitvector_conversion_exceptiont raised if converting byte_extraction -/// goes wrong. -/// TODO: extend for other types of conversion exception (diffblue/cbmc#2103). bvt boolbvt::convert_bitvector(const exprt &expr) { if(expr.type().id()==ID_bool) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index f62dc552642..3ca5d126a21 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -15,12 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include -#include -#include "bv_conversion_exceptions.h" #include "bv_endianness_map.h" bvt map_bv(const bv_endianness_mapt &map, const bvt &src) @@ -45,15 +42,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // unbounded arrays if(is_unbounded_array(expr.op().type())) { - try - { - return convert_bv(lower_byte_extract(expr, ns)); - } - catch(const flatten_byte_extract_exceptiont &) - { - util_throw_with_nested( - bitvector_conversion_exceptiont("Can't convert byte_extraction", expr)); - } + return convert_bv(lower_byte_extract(expr, ns)); } const std::size_t width = boolbv_width(expr.type()); diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 843e5223d54..2210fc48cb7 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -12,12 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include -#include -#include "bv_conversion_exceptions.h" #include "bv_endianness_map.h" bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) @@ -28,15 +25,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) is_unbounded_array(expr.op().type()) || is_unbounded_array(expr.value().type())) { - try - { - return convert_bv(lower_byte_update(expr, ns)); - } - catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception) - { - util_throw_with_nested( - bitvector_conversion_exceptiont("Can't convert byte_update", expr)); - } + return convert_bv(lower_byte_update(expr, ns)); } const exprt &op = expr.op(); diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 1be84441cf2..881e0551879 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "bv_conversion_exceptions.h" - literalt boolbvt::convert_equality(const equal_exprt &expr) { const bool equality_types_match = expr.lhs().type() == expr.rhs().type(); diff --git a/src/solvers/flattening/bv_conversion_exceptions.h b/src/solvers/flattening/bv_conversion_exceptions.h deleted file mode 100644 index 2d3bbd2410b..00000000000 --- a/src/solvers/flattening/bv_conversion_exceptions.h +++ /dev/null @@ -1,34 +0,0 @@ -/*******************************************************************\ - -Module: Bit vector conversion - -Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Exceptions that can be raised in bv_conversion - -#ifndef CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H -#define CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H - -#include -#include - -#include - -class bitvector_conversion_exceptiont : public std::runtime_error -{ -public: - bitvector_conversion_exceptiont( - const std::string &exception_message, - const exprt &bv_expr) - : runtime_error(exception_message), bv_expr(bv_expr) - { - } - -private: - exprt bv_expr; -}; - -#endif // CPROVER_SOLVERS_FLATTENING_BV_CONVERSION_EXCEPTIONS_H diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 9f93823407c..e05809d9044 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "flatten_byte_extract_exceptions.h" - static exprt bv_to_expr( const exprt &bitvector_expr, const typet &target_type, diff --git a/src/solvers/lowering/flatten_byte_extract_exceptions.h b/src/solvers/lowering/flatten_byte_extract_exceptions.h deleted file mode 100644 index b1964518c36..00000000000 --- a/src/solvers/lowering/flatten_byte_extract_exceptions.h +++ /dev/null @@ -1,144 +0,0 @@ -/*******************************************************************\ - -Module: Byte flattening - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#ifndef CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H -#define CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H - -#include -#include -#include - -#include -#include - -class flatten_byte_extract_exceptiont : public std::runtime_error -{ -public: - explicit flatten_byte_extract_exceptiont(const std::string &exception_message) - : runtime_error(exception_message) - { - } -}; - -class non_const_array_sizet : public flatten_byte_extract_exceptiont -{ -public: - non_const_array_sizet(const typet &array_type, const exprt &max_bytes) - : flatten_byte_extract_exceptiont("cannot unpack array of non-const size"), - max_bytes(max_bytes), - array_type(array_type) - { - std::ostringstream error_message; - error_message << runtime_error::what() << "\n"; - error_message << "array_type: " << array_type.pretty(); - error_message << "\nmax_bytes: " << max_bytes.pretty(); - computed_error_message = error_message.str(); - } - - const char *what() const optional_noexcept override - { - return computed_error_message.c_str(); - } - -private: - exprt max_bytes; - typet array_type; - - std::string computed_error_message; -}; - -class non_byte_alignedt : public flatten_byte_extract_exceptiont -{ -public: - non_byte_alignedt( - const struct_typet &struct_type, - const struct_union_typet::componentt &component, - const mp_integer &byte_width) - : flatten_byte_extract_exceptiont( - "cannot unpack struct with non-byte aligned components"), - struct_type(struct_type), - component(component), - byte_width(byte_width) - { - std::ostringstream error_message; - error_message << runtime_error::what() << "\n"; - error_message << "width: " << byte_width << "\n"; - error_message << "component:" << component.get_name() << "\n"; - error_message << "struct_type: " << struct_type.pretty(); - computed_error_message = error_message.str(); - } - - const char *what() const optional_noexcept override - { - return computed_error_message.c_str(); - } - -private: - const struct_typet struct_type; - const struct_union_typet::componentt component; - const mp_integer byte_width; - - std::string computed_error_message; -}; - -class non_constant_widtht : public flatten_byte_extract_exceptiont -{ -public: -public: - non_constant_widtht(const exprt &src, const exprt &max_bytes) - : flatten_byte_extract_exceptiont( - "cannot unpack object of non-constant width"), - src(src), - max_bytes(max_bytes) - { - std::ostringstream error_message; - error_message << runtime_error::what() << "\n"; - error_message << "array_type: " << src.pretty(); - error_message << "\nmax_bytes: " << max_bytes.pretty(); - computed_error_message = error_message.str(); - } - - const char *what() const optional_noexcept override - { - return computed_error_message.c_str(); - } - -private: - exprt src; - exprt max_bytes; - - std::string computed_error_message; -}; - -class non_const_byte_extraction_sizet : public flatten_byte_extract_exceptiont -{ -public: - explicit non_const_byte_extraction_sizet( - const byte_extract_exprt &unpack_expr) - : flatten_byte_extract_exceptiont( - "byte_extract flatting with non-constant size"), - unpack_expr(unpack_expr) - { - std::ostringstream error_message; - error_message << runtime_error::what() << "\n"; - error_message << "unpack_expr: " << unpack_expr.pretty(); - computed_error_message = error_message.str(); - } - - const char *what() const optional_noexcept override - { - return computed_error_message.c_str(); - } - -private: - const byte_extract_exprt unpack_expr; - - std::string computed_error_message; -}; - -#endif // CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H diff --git a/src/util/Makefile b/src/util/Makefile index dd3b6cc43ad..ae7ca9702d9 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -96,7 +96,6 @@ SRC = allocate_objects.cpp \ unicode.cpp \ union_find.cpp \ union_find_replace.cpp \ - unwrap_nested_exception.cpp \ validate_code.cpp \ validate_expressions.cpp \ validate_types.cpp \ diff --git a/src/util/throw_with_nested.h b/src/util/throw_with_nested.h deleted file mode 100644 index 444a7a60e6b..00000000000 --- a/src/util/throw_with_nested.h +++ /dev/null @@ -1,60 +0,0 @@ -/*******************************************************************\ - -Module: util - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_THROW_WITH_NESTED_H -#define CPROVER_UTIL_THROW_WITH_NESTED_H - -#include - -#ifdef _MSC_VER -#include -// TODO(tkiley): Nested exception logging not supported on windows due to a bug -// TODO(tkiley): in MSVC++ Compiler (diffblue/cbmc#2104): -// TODO(tkiley): https://blogs.msdn.microsoft.com/vcblog/2016/01/22/vs-2015-update-2s-stl-is-c17-so-far-feature-complete - -#define DISABLE_NESTED_EXCEPTIONS - -class non_nested_exception_support : public std::runtime_error -{ -public: - non_nested_exception_support() - : std::runtime_error("Nested exception printing not supported on Windows") - { - } -}; - -#endif - -template -#ifdef __GNUC__ -__attribute__((noreturn)) -#endif -void util_throw_with_nested(T &&t) -{ -#ifndef DISABLE_NESTED_EXCEPTIONS - std::throw_with_nested(t); -#else - throw t; -#endif -} - -template -void util_rethrow_if_nested(const E &e) -{ -#ifndef DISABLE_NESTED_EXCEPTIONS - std::rethrow_if_nested(e); -#else - // Check we've not already thrown the non_nested_support_exception - if(!dynamic_cast(&e)) - { - throw non_nested_exception_support(); - } -#endif -} - -#endif // CPROVER_UTIL_THROW_WITH_NESTED_H diff --git a/src/util/unwrap_nested_exception.cpp b/src/util/unwrap_nested_exception.cpp deleted file mode 100644 index 7f54b313a19..00000000000 --- a/src/util/unwrap_nested_exception.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/*******************************************************************\ - -Module: util - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include "unwrap_nested_exception.h" -#include "invariant.h" -#include "string_utils.h" -#include "suffix.h" -#include "throw_with_nested.h" - -#include -#include - -/// Given a potentially nested exception, produce a string with all of nested -/// exceptions information. If a nested exception string contains new lines -/// then the newlines are indented to the correct level. -/// \param e: The outer exeception -/// \param level: How many exceptions have already been unrolled -/// \return A string with all nested exceptions printed and indented -std::string unwrap_exception(const std::exception &e, int level) -{ - const std::string msg = e.what(); - std::vector lines = - split_string(msg, '\n', false, true); - std::ostringstream message_stream; - message_stream << std::string(level, ' ') << "exception: "; - join_strings( - message_stream, lines.begin(), lines.end(), "\n" + std::string(level, ' ')); - - try - { - util_rethrow_if_nested(e); - } - catch(const std::exception &e) - { - std::string nested_message = unwrap_exception(e, level + 1); - // Some exception messages already end in a new line (e.g. as they have - // dumped an irept. Most do not so add a new line on. - if(nested_message.back() != '\n') - { - message_stream << '\n'; - } - message_stream << nested_message; - } - catch(...) - { - UNREACHABLE; - } - return message_stream.str(); -} diff --git a/src/util/unwrap_nested_exception.h b/src/util/unwrap_nested_exception.h deleted file mode 100644 index 4e2903c2c00..00000000000 --- a/src/util/unwrap_nested_exception.h +++ /dev/null @@ -1,17 +0,0 @@ -/*******************************************************************\ - -Module: util - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H -#define CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H - -#include -#include - -std::string unwrap_exception(const std::exception &e, int level = 0); - -#endif // CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H