From 320729118339aedad1375fc67121f93fc67ab76b Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 4 Apr 2018 10:16:25 +0100 Subject: [PATCH 01/12] Introduce nested exception printing --- src/util/Makefile | 1 + src/util/unwrap_nested_exception.cpp | 53 ++++++++++++++++++++++++++++ src/util/unwrap_nested_exception.h | 17 +++++++++ 3 files changed, 71 insertions(+) create mode 100644 src/util/unwrap_nested_exception.cpp create mode 100644 src/util/unwrap_nested_exception.h diff --git a/src/util/Makefile b/src/util/Makefile index cb9d221dd60..74fc5aec412 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -96,6 +96,7 @@ SRC = arith_tools.cpp \ unicode.cpp \ union_find.cpp \ union_find_replace.cpp \ + unwrap_nested_exception.cpp \ xml.cpp \ xml_expr.cpp \ xml_irep.cpp \ diff --git a/src/util/unwrap_nested_exception.cpp b/src/util/unwrap_nested_exception.cpp new file mode 100644 index 00000000000..a025376a0d0 --- /dev/null +++ b/src/util/unwrap_nested_exception.cpp @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: util + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "unwrap_nested_exception.h" +#include "invariant.h" +#include "string_utils.h" +#include "suffix.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', lines, 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 + { + std::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 new file mode 100644 index 00000000000..4e2903c2c00 --- /dev/null +++ b/src/util/unwrap_nested_exception.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +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 From 9bd5222896c4694191b35c5f76154284c30c7a7c Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 9 Apr 2018 17:18:47 +0100 Subject: [PATCH 02/12] Convert flatten_byte_extract to use structured exceptions Store error in string to avoid dangling pointers --- .../flatten_byte_extract_exceptions.h | 144 ++++++++++++++++++ .../flattening/flatten_byte_operators.cpp | 23 ++- 2 files changed, 160 insertions(+), 7 deletions(-) create mode 100644 src/solvers/flattening/flatten_byte_extract_exceptions.h diff --git a/src/solvers/flattening/flatten_byte_extract_exceptions.h b/src/solvers/flattening/flatten_byte_extract_exceptions.h new file mode 100644 index 00000000000..f8c389bcbe4 --- /dev/null +++ b/src/solvers/flattening/flatten_byte_extract_exceptions.h @@ -0,0 +1,144 @@ +/*******************************************************************\ + +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 array_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 noexcept override + { + return computed_error_message.c_str(); + } + +private: + exprt max_bytes; + array_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 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 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 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/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index c564b48df02..42054cc61dc 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "flatten_byte_extract_exceptions.h" #include "flatten_byte_operators.h" /// rewrite an object into its individual bytes @@ -25,6 +26,9 @@ Author: Daniel Kroening, kroening@kroening.com /// max_bytes if not nil, use as upper bound of the number of bytes to unpack /// ns namespace for type lookups /// \return array of bytes in the sequence found in memory +/// \throws flatten_byte_extract_exceptiont Raised is unable to unpack the +/// object because of either non constant size, byte misalignment or +/// non-constant component width. static exprt unpack_rec( const exprt &src, bool little_endian, @@ -63,7 +67,9 @@ static exprt unpack_rec( mp_integer num_elements; if(to_integer(max_bytes, num_elements) && to_integer(array_type.size(), num_elements)) - throw "cannot unpack array of non-const size:\n"+type.pretty(); + { + throw non_const_array_sizet(array_type, max_bytes); + } // all array members will have the same structure; do this just // once and then replace the dummy symbol by a suitable index @@ -97,8 +103,9 @@ static exprt unpack_rec( // the next member would be misaligned, abort if(element_width<=0 || element_width%8!=0) - throw "cannot unpack struct with non-byte aligned components:\n"+ - struct_type.pretty(); + { + throw non_byte_alignedt(struct_type, comp, element_width); + } member_exprt member(src, comp.get_name(), comp.type()); exprt sub=unpack_rec(member, little_endian, max_bytes, ns, true); @@ -115,8 +122,9 @@ static exprt unpack_rec( if(bits<0) { if(to_integer(max_bytes, bits)) - throw "cannot unpack object of non-constant width:\n"+ - src.pretty(); + { + throw non_constant_widtht(src, max_bytes); + } else bits*=8; } @@ -300,8 +308,9 @@ exprt flatten_byte_extract( { mp_integer op0_bits=pointer_offset_bits(unpacked.op().type(), ns); if(op0_bits<0) - throw "byte_extract flatting with non-constant size:\n"+ - unpacked.pretty(); + { + throw non_const_byte_extraction_sizet(unpacked); + } else size_bits=op0_bits; } From 12f25c2103ee1a03233a1561678e232784df3465 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 12 Apr 2018 14:20:51 +0100 Subject: [PATCH 03/12] Introduce throwing bv_conversion expection Remove suprisous namespace from bv_conversion_exceptions --- src/solvers/flattening/boolbv.cpp | 6 ++++ .../flattening/boolbv_byte_extract.cpp | 16 +++++++-- .../flattening/bv_conversion_exceptions.h | 34 +++++++++++++++++++ 3 files changed, 53 insertions(+), 3 deletions(-) create mode 100644 src/solvers/flattening/bv_conversion_exceptions.h diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index a61e50a0f33..ba164134f17 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -152,6 +152,12 @@ bvt boolbvt::conversion_failed(const exprt &expr) return prop.new_variables(width); } +/// TODO +/// \param expr: TODO +/// \return TODO +/// \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 0cc2c46bd89..e550eeee362 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -11,10 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include +#include +#include "bv_conversion_exceptions.h" +#include "flatten_byte_extract_exceptions.h" #include "flatten_byte_operators.h" bvt map_bv(const endianness_mapt &map, const bvt &src) @@ -42,8 +44,16 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // if we extract from an unbounded array, call the flattening code if(is_unbounded_array(expr.op().type())) { - exprt tmp=flatten_byte_extract(expr, ns); - return convert_bv(tmp); + try + { + exprt tmp = flatten_byte_extract(expr, ns); + return convert_bv(tmp); + } + catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception) + { + std::throw_with_nested( + bitvector_conversion_exceptiont("Can't convert byte_extraction", expr)); + } } std::size_t width=boolbv_width(expr.type()); diff --git a/src/solvers/flattening/bv_conversion_exceptions.h b/src/solvers/flattening/bv_conversion_exceptions.h new file mode 100644 index 00000000000..2d3bbd2410b --- /dev/null +++ b/src/solvers/flattening/bv_conversion_exceptions.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +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 From a97bc2809d2fa05bc357c5be5593e06a24b172b3 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 12 Apr 2018 14:27:25 +0100 Subject: [PATCH 04/12] Introduce throwing a guard conversion exception Throw the unwrapped exception as a string --- .../equation_conversion_exceptions.h | 50 +++++++++++++++++++ src/goto-symex/symex_target_equation.cpp | 30 +++++++++-- 2 files changed, 76 insertions(+), 4 deletions(-) create mode 100644 src/goto-symex/equation_conversion_exceptions.h diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h new file mode 100644 index 00000000000..66dfcff195f --- /dev/null +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -0,0 +1,50 @@ +/*******************************************************************\ + +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 "symex_target_equation.h" + +class guard_conversion_exceptiont : public std::runtime_error +{ +public: + guard_conversion_exceptiont( + const symex_target_equationt::SSA_stept &step, + const namespacet &ns) + : runtime_error("Error converting guard for step"), step(step) + { + std::ostringstream error_msg; + error_msg << runtime_error::what(); + error_msg << "\nStep:\n"; + step.output(ns, error_msg); + error_message = error_msg.str(); + } + + explicit guard_conversion_exceptiont( + const symex_target_equationt::SSA_stept &step) + : guard_conversion_exceptiont(step, namespacet{symbol_tablet{}}) + { + } + + const char *what() const noexcept override + { + return error_message.c_str(); + } + +private: + symex_target_equationt::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 27be83608f1..62d6b4b9268 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -12,12 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" #include +#include #include -#include -#include +#include #include +#include +#include +#include "equation_conversion_exceptions.h" #include "goto_symex_state.h" /// read from a shared variable @@ -368,7 +371,17 @@ void symex_target_equationt::constraint( void symex_target_equationt::convert( prop_convt &prop_conv) { - convert_guards(prop_conv); + try + { + convert_guards(prop_conv); + } + catch(guard_conversion_exceptiont &guard_conversion_exception) + { + // unwrap the except and throw like normal + const std::string full_error = unwrap_exception(guard_conversion_exception); + throw full_error; + } + convert_assignments(prop_conv); convert_decls(prop_conv); convert_assumptions(prop_conv); @@ -417,7 +430,16 @@ void symex_target_equationt::convert_guards( if(step.ignore) step.guard_literal=const_literal(false); else - step.guard_literal=prop_conv.convert(step.guard); + { + try + { + step.guard_literal = prop_conv.convert(step.guard); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + std::throw_with_nested(guard_conversion_exceptiont(step)); + } + } } } From b86601559ce2d156bba41124d4589f601ba2da77 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 12 Apr 2018 17:02:06 +0100 Subject: [PATCH 05/12] Provide the original goto statement in the error This required the symex target_equation having the namespace to resolve names --- src/cbmc/bmc.h | 2 +- src/goto-instrument/accelerate/scratch_program.h | 2 +- src/goto-symex/equation_conversion_exceptions.h | 3 +++ src/goto-symex/symex_target_equation.cpp | 2 +- src/goto-symex/symex_target_equation.h | 8 +++++++- 5 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0f394199fe0..54f4affecdd 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -78,7 +78,7 @@ class bmct:public safety_checkert options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table, symex_symbol_table), - equation(), + equation(ns), branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index 0bd76634bd0..afa58ba9fbb 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -40,7 +40,7 @@ class scratch_programt:public goto_programt symbol_table(_symbol_table), symex_symbol_table(), ns(symbol_table, symex_symbol_table), - equation(), + equation(ns), branch_worklist(), symex(mh, symbol_table, equation, branch_worklist), satcheck(util_make_unique()), diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index 66dfcff195f..2242d0bdc55 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -14,6 +14,7 @@ Author: Diffblue Ltd. #include #include +#include #include "symex_target_equation.h" class guard_conversion_exceptiont : public std::runtime_error @@ -26,6 +27,8 @@ class guard_conversion_exceptiont : public std::runtime_error { std::ostringstream error_msg; error_msg << runtime_error::what(); + error_msg << "\nSource GOTO statement: " + << from_expr(ns, "java", step.source.pc->code); error_msg << "\nStep:\n"; step.output(ns, error_msg); error_message = error_msg.str(); diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 62d6b4b9268..580d42f76e9 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -437,7 +437,7 @@ void symex_target_equationt::convert_guards( } catch(const bitvector_conversion_exceptiont &conversion_exception) { - std::throw_with_nested(guard_conversion_exceptiont(step)); + std::throw_with_nested(guard_conversion_exceptiont(step, ns)); } } } diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 178cbeae7ab..c4c8cdf8910 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -32,7 +32,10 @@ class prop_convt; class symex_target_equationt:public symex_targett { public: - symex_target_equationt() = default; + explicit symex_target_equationt(const namespacet &ns) : ns(ns) + { + } + virtual ~symex_target_equationt() = default; // read event @@ -320,6 +323,9 @@ class symex_target_equationt:public symex_targett // for enforcing sharing in the expressions stored merge_irept merge_irep; void merge_ireps(SSA_stept &SSA_step); + +private: + const namespacet &ns; }; inline bool operator<( From 9d41b0cdf151d73101ed969dfc72b96a9103cd5d Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 19 Apr 2018 15:07:28 +0100 Subject: [PATCH 06/12] Disable nested exception printing for Windows Due to bug in the VS2013 C++ compiler, using std::rethrow_if_nested or std::nested_exception is not supported. This disables trying to unwrap the exception and just prints a warning saying the nested exceptionc couldn't be printed. Don't use noexcept directly, pull both part of the nested exception into a separate file to handle discrepancies. --- .../equation_conversion_exceptions.h | 2 +- src/goto-symex/symex_target_equation.cpp | 3 +- .../flattening/boolbv_byte_extract.cpp | 3 +- .../flatten_byte_extract_exceptions.h | 8 +-- src/util/throw_with_nested.h | 60 +++++++++++++++++++ src/util/unwrap_nested_exception.cpp | 3 +- 6 files changed, 71 insertions(+), 8 deletions(-) create mode 100644 src/util/throw_with_nested.h diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index 2242d0bdc55..41ca9f42a0b 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -40,7 +40,7 @@ class guard_conversion_exceptiont : public std::runtime_error { } - const char *what() const noexcept override + const char *what() const optional_noexcept override { return error_message.c_str(); } diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 580d42f76e9..7e97d6caf9a 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" #include +#include #include #include @@ -437,7 +438,7 @@ void symex_target_equationt::convert_guards( } catch(const bitvector_conversion_exceptiont &conversion_exception) { - std::throw_with_nested(guard_conversion_exceptiont(step, ns)); + util_throw_with_nested(guard_conversion_exceptiont(step, ns)); } } } diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index e550eeee362..f3841a6f0f3 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "bv_conversion_exceptions.h" #include "flatten_byte_extract_exceptions.h" @@ -51,7 +52,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) } catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception) { - std::throw_with_nested( + util_throw_with_nested( bitvector_conversion_exceptiont("Can't convert byte_extraction", expr)); } } diff --git a/src/solvers/flattening/flatten_byte_extract_exceptions.h b/src/solvers/flattening/flatten_byte_extract_exceptions.h index f8c389bcbe4..a5ae22791b3 100644 --- a/src/solvers/flattening/flatten_byte_extract_exceptions.h +++ b/src/solvers/flattening/flatten_byte_extract_exceptions.h @@ -40,7 +40,7 @@ class non_const_array_sizet : public flatten_byte_extract_exceptiont computed_error_message = error_message.str(); } - const char *what() const noexcept override + const char *what() const optional_noexcept override { return computed_error_message.c_str(); } @@ -73,7 +73,7 @@ class non_byte_alignedt : public flatten_byte_extract_exceptiont computed_error_message = error_message.str(); } - const char *what() const noexcept override + const char *what() const optional_noexcept override { return computed_error_message.c_str(); } @@ -103,7 +103,7 @@ class non_constant_widtht : public flatten_byte_extract_exceptiont computed_error_message = error_message.str(); } - const char *what() const noexcept override + const char *what() const optional_noexcept override { return computed_error_message.c_str(); } @@ -130,7 +130,7 @@ class non_const_byte_extraction_sizet : public flatten_byte_extract_exceptiont computed_error_message = error_message.str(); } - const char *what() const noexcept override + const char *what() const optional_noexcept override { return computed_error_message.c_str(); } diff --git a/src/util/throw_with_nested.h b/src/util/throw_with_nested.h new file mode 100644 index 00000000000..444a7a60e6b --- /dev/null +++ b/src/util/throw_with_nested.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + +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 index a025376a0d0..0689391466b 100644 --- a/src/util/unwrap_nested_exception.cpp +++ b/src/util/unwrap_nested_exception.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include "invariant.h" #include "string_utils.h" #include "suffix.h" +#include "throw_with_nested.h" #include #include @@ -32,7 +33,7 @@ std::string unwrap_exception(const std::exception &e, int level) try { - std::rethrow_if_nested(e); + util_rethrow_if_nested(e); } catch(const std::exception &e) { From 015b2840cdd0d21059061a7b456742bee53f98bf Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 19 Apr 2018 17:37:50 +0100 Subject: [PATCH 07/12] Test demonstrating logging with clause for dealing with Windows --- .../TestClass.class | Bin 0 -> 399 bytes .../TestClass.java | 7 +++++++ .../dynamic-multi-dimensional-array/test.desc | 10 ++++++++++ 3 files changed, 17 insertions(+) create mode 100644 regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class create mode 100644 regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java create mode 100644 regression/cbmc-java/dynamic-multi-dimensional-array/test.desc diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.class new file mode 100644 index 0000000000000000000000000000000000000000..66e0d0732425724aad3f598846515a0603e8f0c3 GIT binary patch literal 399 zcmYL_O-sW-5Qg7L(!`{-AMsl}=&dRk6mNbUEEEbs5lb&UZDQ1v*g}#D{wz;|2X9{d zQR2I;)LnLG=b4>%cJ}+{;}gIswmej@?!dRMJix(*gH3^bo{rPa{(@nI=EdR8iRqiS|3W_N lf|ndxmoI2iT8r+^6VV{iU+bX-pRz86SIG1$R~a#|_6z5sIxGMH literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java new file mode 100644 index 00000000000..16d680bd804 --- /dev/null +++ b/regression/cbmc-java/dynamic-multi-dimensional-array/TestClass.java @@ -0,0 +1,7 @@ +public class TestClass { + public static void f(int y) { + float[][] a1 = new float[y][3]; + int j = 0; + a1[j][0] = 34.5f; + } +} diff --git a/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc b/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc new file mode 100644 index 00000000000..c9600f50852 --- /dev/null +++ b/regression/cbmc-java/dynamic-multi-dimensional-array/test.desc @@ -0,0 +1,10 @@ +CORE +TestClass.class +--function TestClass.f --cover location --unwind 2 +Source GOTO statement: .* +(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows) +^EXIT=6$ +-- +-- +The exception thrown in this test is the symptom of a bug; the purpose of this +test is the validate the output of that exception From 21997b2ed941914f856476afdfa9138040bf39e0 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 23 Apr 2018 11:12:46 +0100 Subject: [PATCH 08/12] Add documentation to convert_bitvector --- src/solvers/flattening/boolbv.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index ba164134f17..40ddc83e3d6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -152,9 +152,11 @@ bvt boolbvt::conversion_failed(const exprt &expr) return prop.new_variables(width); } -/// TODO -/// \param expr: TODO -/// \return TODO +/// Converts an expression into its gate-level representation and returns a +/// vector of literals corresponding to the outputs of the Boolean circuit. +/// \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). From 781bf7cb8ea5eabf4c5ef6c1627ff26fcc2245a8 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 23 Apr 2018 13:45:27 +0100 Subject: [PATCH 09/12] Introduce exceptions for all conversion steps. --- .../equation_conversion_exceptions.h | 15 ++-- src/goto-symex/symex_target_equation.cpp | 71 +++++++++++++++---- 2 files changed, 66 insertions(+), 20 deletions(-) diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index 41ca9f42a0b..099be66e239 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -13,17 +13,21 @@ Author: Diffblue Ltd. #define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H #include + #include + #include + #include "symex_target_equation.h" -class guard_conversion_exceptiont : public std::runtime_error +class equation_conversion_exceptiont : public std::runtime_error { public: - guard_conversion_exceptiont( + equation_conversion_exceptiont( + const std::string &message, const symex_target_equationt::SSA_stept &step, const namespacet &ns) - : runtime_error("Error converting guard for step"), step(step) + : runtime_error(message), step(step) { std::ostringstream error_msg; error_msg << runtime_error::what(); @@ -34,9 +38,10 @@ class guard_conversion_exceptiont : public std::runtime_error error_message = error_msg.str(); } - explicit guard_conversion_exceptiont( + explicit equation_conversion_exceptiont( + const std::string &message, const symex_target_equationt::SSA_stept &step) - : guard_conversion_exceptiont(step, namespacet{symbol_tablet{}}) + : equation_conversion_exceptiont(message, step, namespacet{symbol_tablet{}}) { } diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 7e97d6caf9a..be6fd3a42c2 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -375,21 +375,20 @@ void symex_target_equationt::convert( try { convert_guards(prop_conv); + convert_assignments(prop_conv); + convert_decls(prop_conv); + convert_assumptions(prop_conv); + convert_assertions(prop_conv); + convert_goto_instructions(prop_conv); + convert_io(prop_conv); + convert_constraints(prop_conv); } - catch(guard_conversion_exceptiont &guard_conversion_exception) + catch(const equation_conversion_exceptiont &conversion_exception) { // unwrap the except and throw like normal - const std::string full_error = unwrap_exception(guard_conversion_exception); + const std::string full_error = unwrap_exception(conversion_exception); throw full_error; } - - convert_assignments(prop_conv); - convert_decls(prop_conv); - convert_assumptions(prop_conv); - convert_assertions(prop_conv); - convert_goto_instructions(prop_conv); - convert_io(prop_conv); - convert_constraints(prop_conv); } /// converts assignments @@ -416,7 +415,16 @@ void symex_target_equationt::convert_decls( { // The result is not used, these have no impact on // the satisfiability of the formula. - prop_conv.convert(step.cond_expr); + try + { + prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting decls for step", step, ns)); + } } } } @@ -438,7 +446,9 @@ void symex_target_equationt::convert_guards( } catch(const bitvector_conversion_exceptiont &conversion_exception) { - util_throw_with_nested(guard_conversion_exceptiont(step, ns)); + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting guard for step", step, ns)); } } } @@ -456,7 +466,18 @@ void symex_target_equationt::convert_assumptions( if(step.ignore) step.cond_literal=const_literal(true); else - step.cond_literal=prop_conv.convert(step.cond_expr); + { + try + { + step.cond_literal = prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting assumptions for step", step, ns)); + } + } } } } @@ -473,7 +494,18 @@ void symex_target_equationt::convert_goto_instructions( if(step.ignore) step.cond_literal=const_literal(true); else - step.cond_literal=prop_conv.convert(step.cond_expr); + { + try + { + step.cond_literal = prop_conv.convert(step.cond_expr); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting goto instructions for step", step, ns)); + } + } } } } @@ -542,7 +574,16 @@ void symex_target_equationt::convert_assertions( step.cond_expr); // do the conversion - step.cond_literal=prop_conv.convert(implication); + try + { + step.cond_literal = prop_conv.convert(implication); + } + catch(const bitvector_conversion_exceptiont &conversion_exception) + { + util_throw_with_nested( + equation_conversion_exceptiont( + "Error converting assertions for step", step, ns)); + } // store disjunct disjuncts.push_back(literal_exprt(!step.cond_literal)); From 54fb9ab47602db8757619ff1b508095667e37726 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 23 Apr 2018 15:02:51 +0100 Subject: [PATCH 10/12] Use format rather than from_expr for output --- src/cbmc/bmc.h | 2 +- .../accelerate/scratch_program.h | 2 +- .../equation_conversion_exceptions.h | 19 +-- src/goto-symex/symex_target_equation.cpp | 111 +++++++++++++++++- src/goto-symex/symex_target_equation.h | 11 +- 5 files changed, 116 insertions(+), 29 deletions(-) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 54f4affecdd..0f394199fe0 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -78,7 +78,7 @@ class bmct:public safety_checkert options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table, symex_symbol_table), - equation(ns), + equation(), branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index afa58ba9fbb..0bd76634bd0 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -40,7 +40,7 @@ class scratch_programt:public goto_programt symbol_table(_symbol_table), symex_symbol_table(), ns(symbol_table, symex_symbol_table), - equation(ns), + equation(), branch_worklist(), symex(mh, symbol_table, equation, branch_worklist), satcheck(util_make_unique()), diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index 099be66e239..f2055c1c9ec 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -14,9 +14,7 @@ Author: Diffblue Ltd. #include -#include - -#include +#include #include "symex_target_equation.h" @@ -25,26 +23,17 @@ class equation_conversion_exceptiont : public std::runtime_error public: equation_conversion_exceptiont( const std::string &message, - const symex_target_equationt::SSA_stept &step, - const namespacet &ns) + const symex_target_equationt::SSA_stept &step) : runtime_error(message), step(step) { std::ostringstream error_msg; error_msg << runtime_error::what(); - error_msg << "\nSource GOTO statement: " - << from_expr(ns, "java", step.source.pc->code); + error_msg << "\nSource GOTO statement: " << format(step.source.pc->code); error_msg << "\nStep:\n"; - step.output(ns, error_msg); + step.output(error_msg); error_message = error_msg.str(); } - explicit equation_conversion_exceptiont( - const std::string &message, - const symex_target_equationt::SSA_stept &step) - : equation_conversion_exceptiont(message, step, namespacet{symbol_tablet{}}) - { - } - const char *what() const optional_noexcept override { return error_message.c_str(); diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index be6fd3a42c2..4f3fca4e81e 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -11,11 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target_equation.h" +#include #include #include #include +// Can be removed once deprecated SSA_stept::output is removed #include + #include #include #include @@ -423,7 +426,7 @@ void symex_target_equationt::convert_decls( { util_throw_with_nested( equation_conversion_exceptiont( - "Error converting decls for step", step, ns)); + "Error converting decls for step", step)); } } } @@ -448,7 +451,7 @@ void symex_target_equationt::convert_guards( { util_throw_with_nested( equation_conversion_exceptiont( - "Error converting guard for step", step, ns)); + "Error converting guard for step", step)); } } } @@ -475,7 +478,7 @@ void symex_target_equationt::convert_assumptions( { util_throw_with_nested( equation_conversion_exceptiont( - "Error converting assumptions for step", step, ns)); + "Error converting assumptions for step", step)); } } } @@ -503,7 +506,7 @@ void symex_target_equationt::convert_goto_instructions( { util_throw_with_nested( equation_conversion_exceptiont( - "Error converting goto instructions for step", step, ns)); + "Error converting goto instructions for step", step)); } } } @@ -582,7 +585,7 @@ void symex_target_equationt::convert_assertions( { util_throw_with_nested( equation_conversion_exceptiont( - "Error converting assertions for step", step, ns)); + "Error converting assertions for step", step)); } // store disjunct @@ -767,3 +770,101 @@ void symex_target_equationt::SSA_stept::output( out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n'; } + +void symex_target_equationt::SSA_stept::output(std::ostream &out) const +{ + if(source.is_set) + { + out << "Thread " << source.thread_nr; + + if(source.pc->source_location.is_not_nil()) + out << " " << source.pc->source_location << '\n'; + else + out << '\n'; + } + + switch(type) + { + case goto_trace_stept::typet::ASSERT: + out << "ASSERT " << format(cond_expr) << '\n'; break; + case goto_trace_stept::typet::ASSUME: + out << "ASSUME " << format(cond_expr) << '\n'; break; + case goto_trace_stept::typet::LOCATION: + out << "LOCATION" << '\n'; break; + case goto_trace_stept::typet::INPUT: + out << "INPUT" << '\n'; break; + case goto_trace_stept::typet::OUTPUT: + out << "OUTPUT" << '\n'; break; + + case goto_trace_stept::typet::DECL: + out << "DECL" << '\n'; + out << format(ssa_lhs) << '\n'; + break; + + case goto_trace_stept::typet::ASSIGNMENT: + out << "ASSIGNMENT ("; + switch(assignment_type) + { + case assignment_typet::HIDDEN: + out << "HIDDEN"; + break; + case assignment_typet::STATE: + out << "STATE"; + break; + case assignment_typet::VISIBLE_ACTUAL_PARAMETER: + out << "VISIBLE_ACTUAL_PARAMETER"; + break; + case assignment_typet::HIDDEN_ACTUAL_PARAMETER: + out << "HIDDEN_ACTUAL_PARAMETER"; + break; + case assignment_typet::PHI: + out << "PHI"; + break; + case assignment_typet::GUARD: + out << "GUARD"; + break; + default: + { + } + } + + out << ")\n"; + break; + + case goto_trace_stept::typet::DEAD: + out << "DEAD\n"; break; + case goto_trace_stept::typet::FUNCTION_CALL: + out << "FUNCTION_CALL\n"; break; + case goto_trace_stept::typet::FUNCTION_RETURN: + out << "FUNCTION_RETURN\n"; break; + case goto_trace_stept::typet::CONSTRAINT: + out << "CONSTRAINT\n"; break; + case goto_trace_stept::typet::SHARED_READ: + out << "SHARED READ\n"; break; + case goto_trace_stept::typet::SHARED_WRITE: + out << "SHARED WRITE\n"; break; + case goto_trace_stept::typet::ATOMIC_BEGIN: + out << "ATOMIC_BEGIN\n"; break; + case goto_trace_stept::typet::ATOMIC_END: + out << "AUTOMIC_END\n"; break; + case goto_trace_stept::typet::SPAWN: + out << "SPAWN\n"; break; + case goto_trace_stept::typet::MEMORY_BARRIER: + out << "MEMORY_BARRIER\n"; break; + case goto_trace_stept::typet::GOTO: + out << "IF " << format(cond_expr) << " GOTO\n"; break; + + default: UNREACHABLE; + } + + if(is_assert() || is_assume() || is_assignment() || is_constraint()) + out << format(cond_expr) << '\n'; + + if(is_assert() || is_constraint()) + out << comment << '\n'; + + if(is_shared_read() || is_shared_write()) + out << format(ssa_lhs) << '\n'; + + out << "Guard: " << format(guard) << '\n'; +} diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index c4c8cdf8910..079158f0374 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -32,10 +32,7 @@ class prop_convt; class symex_target_equationt:public symex_targett { public: - explicit symex_target_equationt(const namespacet &ns) : ns(ns) - { - } - + symex_target_equationt() = default; virtual ~symex_target_equationt() = default; // read event @@ -260,9 +257,12 @@ class symex_target_equationt:public symex_targett { } + DEPRECATED("Use output without ns param") void output( const namespacet &ns, std::ostream &out) const; + + void output(std::ostream &out) const; }; std::size_t count_assertions() const @@ -323,9 +323,6 @@ class symex_target_equationt:public symex_targett // for enforcing sharing in the expressions stored merge_irept merge_irep; void merge_ireps(SSA_stept &SSA_step); - -private: - const namespacet &ns; }; inline bool operator<( From f2a40542a47d06bc512e6f3d9b64c33dacecfd1a Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 23 Apr 2018 17:11:55 +0100 Subject: [PATCH 11/12] Remove redundant default constructor --- src/goto-symex/symex_target_equation.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 079158f0374..bada3f9d871 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -32,7 +32,6 @@ class prop_convt; class symex_target_equationt:public symex_targett { public: - symex_target_equationt() = default; virtual ~symex_target_equationt() = default; // read event From 9874a6ba72edda012c94678bee38153119b6003e Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 23 Apr 2018 17:22:22 +0100 Subject: [PATCH 12/12] Reformatting touched output function --- src/goto-symex/symex_target_equation.cpp | 51 ++++++++++++++++-------- 1 file changed, 34 insertions(+), 17 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 4f3fca4e81e..0d3709dde8e 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -786,15 +786,20 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const switch(type) { case goto_trace_stept::typet::ASSERT: - out << "ASSERT " << format(cond_expr) << '\n'; break; + out << "ASSERT " << format(cond_expr) << '\n'; + break; case goto_trace_stept::typet::ASSUME: - out << "ASSUME " << format(cond_expr) << '\n'; break; + out << "ASSUME " << format(cond_expr) << '\n'; + break; case goto_trace_stept::typet::LOCATION: - out << "LOCATION" << '\n'; break; + out << "LOCATION" << '\n'; + break; case goto_trace_stept::typet::INPUT: - out << "INPUT" << '\n'; break; + out << "INPUT" << '\n'; + break; case goto_trace_stept::typet::OUTPUT: - out << "OUTPUT" << '\n'; break; + out << "OUTPUT" << '\n'; + break; case goto_trace_stept::typet::DECL: out << "DECL" << '\n'; @@ -832,29 +837,41 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const break; case goto_trace_stept::typet::DEAD: - out << "DEAD\n"; break; + out << "DEAD\n"; + break; case goto_trace_stept::typet::FUNCTION_CALL: - out << "FUNCTION_CALL\n"; break; + out << "FUNCTION_CALL\n"; + break; case goto_trace_stept::typet::FUNCTION_RETURN: - out << "FUNCTION_RETURN\n"; break; + out << "FUNCTION_RETURN\n"; + break; case goto_trace_stept::typet::CONSTRAINT: - out << "CONSTRAINT\n"; break; + out << "CONSTRAINT\n"; + break; case goto_trace_stept::typet::SHARED_READ: - out << "SHARED READ\n"; break; + out << "SHARED READ\n"; + break; case goto_trace_stept::typet::SHARED_WRITE: - out << "SHARED WRITE\n"; break; + out << "SHARED WRITE\n"; + break; case goto_trace_stept::typet::ATOMIC_BEGIN: - out << "ATOMIC_BEGIN\n"; break; + out << "ATOMIC_BEGIN\n"; + break; case goto_trace_stept::typet::ATOMIC_END: - out << "AUTOMIC_END\n"; break; + out << "AUTOMIC_END\n"; + break; case goto_trace_stept::typet::SPAWN: - out << "SPAWN\n"; break; + out << "SPAWN\n"; + break; case goto_trace_stept::typet::MEMORY_BARRIER: - out << "MEMORY_BARRIER\n"; break; + out << "MEMORY_BARRIER\n"; + break; case goto_trace_stept::typet::GOTO: - out << "IF " << format(cond_expr) << " GOTO\n"; break; + out << "IF " << format(cond_expr) << " GOTO\n"; + break; - default: UNREACHABLE; + default: + UNREACHABLE; } if(is_assert() || is_assume() || is_assignment() || is_constraint())