Convert flatten_byte_extract to use structured exceptions

Store error in string to avoid dangling pointers

Author: thk123

src/solvers/flattening/flatten_byte_extract_exceptions.h

@@ -0,0 +1,147 @@
+/*******************************************************************\
+
+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 <sstream>
+#include <iostream>
+#include <util/simplify_expr.h>
+#include <util/namespace.h>
+#include <util/byte_operators.h>
+#include <util/pointer_offset_size.h>
+#include <util/arith_tools.h>
+#include <util/std_expr.h>
+#include <util/c_types.h>
+
+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

src/solvers/flattening/flatten_byte_operators.cpp

@@ -18,13 +18,17 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 
 #include "flatten_byte_operators.h"
+#include "flatten_byte_extract_exceptions.h"
 
 /// rewrite an object into its individual bytes
 /// \par parameters: src  object to unpack
 /// little_endian  true, iff assumed endianness is little-endian
 /// 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;
   }