Add a highlevel api to test types on exprt and typet

The CBMC code base normaly checks the id of an irept subtype
against some magic id. But for some tests, it is necessary to check against
more than one id. So this functions are use do the checks.

This should further support code readability as a combination of different ids
gets a name.

Author: mmuesly

src/ansi-c/c_typecast.cpp

@@ -55,14 +55,14 @@ bool c_implicit_typecast_arithmetic(
   return !c_typecast.errors.empty();
 }
 
-bool is_void_pointer(const typet &type)
+bool has_a_void_pointer(const typet &type)
 {
   if(type.id()==ID_pointer)
   {
     if(type.subtype().id()==ID_empty)
       return true;
 
-    return is_void_pointer(type.subtype());
+    return has_a_void_pointer(type.subtype());
   }
   else
     return false;
@@ -214,10 +214,11 @@ bool check_c_implicit_typecast(
       const irept &dest_subtype=dest_type.subtype();
       const irept &src_subtype =src_type.subtype();
 
-      if(src_subtype==dest_subtype)
+      if(src_subtype == dest_subtype)
         return false;
-      else if(is_void_pointer(src_type) || // from void to anything
-              is_void_pointer(dest_type))  // to void from anything
+      else if(
+        has_a_void_pointer(src_type) || // from void to anything
+        has_a_void_pointer(dest_type))  // to void from anything
         return false;
     }
 
@@ -516,10 +517,9 @@ void c_typecastt::implicit_typecast_followed(
       // we are quite generous about pointers
 
       const typet &src_sub=ns.follow(src_type.subtype());
-      const typet &dest_sub=ns.follow(dest_type.subtype());
+      const typet &dest_sub = ns.follow(dest_type.subtype());
 
-      if(is_void_pointer(src_type) ||
-         is_void_pointer(dest_type))
+      if(has_a_void_pointer(src_type) || has_a_void_pointer(dest_type))
       {
         // from/to void is always good
       }

src/util/c_types_util.h

@@ -0,0 +1,109 @@
+// Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// This file contains functions, that should support test for underlying
+/// c types, in cases where this is required for anlysis purpose.
+#ifndef CPROVER_UTIL_C_TYPES_UTIL_H
+#define CPROVER_UTIL_C_TYPES_UTIL_H
+
+#include "arith_tools.h"
+#include "invariant.h"
+#include "std_types.h"
+#include "type.h"
+
+#include <algorithm>
+#include <string>
+
+/// This function checks, whether this has been a char type in the c program.
+inline bool is_c_char(const typet &type)
+{
+  const irep_idt &c_type = type.get(ID_C_c_type);
+  return is_signed_or_unsigned_bitvector(type) &&
+         (c_type == ID_char || c_type == ID_unsigned_char ||
+          c_type == ID_signed_char);
+}
+
+/// This function checks, whether the type
+/// has been a bool type in the c program.
+inline bool is_c_bool(const typet &type)
+{
+  return type.id() == ID_c_bool;
+}
+
+/// This function checks, whether the type is has been some kind of integer
+/// type in the c program.
+/// It considers the signed and unsigned verison of
+/// int, short, long and long long as integer types in c.
+inline bool is_c_int_derivate(const typet &type)
+{
+  const irep_idt &c_type = type.get(ID_C_c_type);
+  return is_signed_or_unsigned_bitvector(type) &&
+         (c_type == ID_signed_int || c_type == ID_unsigned_int ||
+          c_type == ID_signed_short_int || c_type == ID_unsigned_int ||
+          c_type == ID_unsigned_short_int || c_type == ID_signed_long_int ||
+          c_type == ID_signed_long_long_int || c_type == ID_unsigned_long_int ||
+          c_type == ID_unsigned_long_long_int);
+}
+
+/// This function checks, whether type is a pointer and the target type
+/// of the pointer has been a char type in the c program.
+inline bool is_c_char_pointer(const typet &type)
+{
+  return is_pointer(type) && is_c_char(type.subtype());
+}
+
+/// This function checks, whether type is a pointer and the target type
+/// has been some kind of int type in the c program.
+/// is_c_int_derivate answers is used for checking the int type.
+inline bool is_c_int_derivate_pointer(const typet &type)
+{
+  return is_pointer(type) && is_c_int_derivate(type.subtype());
+}
+
+/// This function checks, whether the type
+/// has been an enum type in the c program.
+inline bool is_c_enum(const typet &type)
+{
+  return type.id() == ID_c_enum;
+}
+
+/// This function creates a constant representing the
+/// bitvector encoded integer value of a string in the enum.
+/// \param member_name is a string that should be in the enum.
+/// \param c_enum the enum type memeber_name is supposed to be part of.
+/// \return value a constant, that could be assigned as value for an expression
+/// with type c_enum.
+constant_exprt convert_memeber_name_to_enum_value(
+  const std::string &member_name,
+  const c_enum_typet &c_enum)
+{
+  for(const auto &enum_value : c_enum.members())
+  {
+    if(id2string(enum_value.get_identifier()) == member_name)
+    {
+      mp_integer int_value = string2integer(id2string(enum_value.get_value()));
+      return from_integer(int_value, c_enum);
+    }
+  }
+  INVARIANT(false, "member_name must be a valid value in the c_enum.");
+}
+
+/// This function creates a constant representing either 0 or 1 as value of
+/// type type.
+/// \param bool_value: A string that is compared to "true" ignoring case.
+/// \param type: The type, the resulting constant is supposed to have.
+/// \return a constant of type \param type with either 0 or 1 as value.
+constant_exprt from_c_boolean_value(std::string bool_value, const typet &type)
+{
+  std::transform(
+    bool_value.begin(), bool_value.end(), bool_value.begin(), ::tolower);
+  if(bool_value == "true")
+  {
+    return from_integer(mp_integer(1), type);
+  }
+  else
+  {
+    return from_integer(mp_integer(0), type);
+  }
+}
+#endif // CPROVER_UTIL_C_TYPES_UTIL_H

src/util/std_types.h

@@ -25,6 +25,13 @@ Author: Daniel Kroening, [email protected]
 
 class constant_exprt;
 
+/// This method tests,
+/// if the given typet is a constant
+inline bool is_constant(const typet &type)
+{
+  return type.id() == ID_constant;
+}
+
 /*!
  *  Conversion to subclasses of @ref typet
 */
@@ -305,6 +312,13 @@ class struct_typet:public struct_union_typet
   bool is_prefix_of(const struct_typet &other) const;
 };
 
+/// This method tests,
+/// if the given typet is a struct
+inline bool is_struct(const typet &type)
+{
+  return type.id() == ID_struct;
+}
+
 /*! \brief Cast a generic typet to a \ref struct_typet
  *
  * This is an unchecked conversion. \a type must be known to be \ref
@@ -1040,6 +1054,12 @@ class array_typet:public type_with_subtypet
     return size().is_nil();
   }
 };
+/// This method tests,
+/// if the given typet is an array_typet
+inline bool is_array(const typet &type)
+{
+  return type.id() == ID_array;
+}
 
 /*! \brief Cast a generic typet to an \ref array_typet
  *
@@ -1146,6 +1166,13 @@ class bitvector_typet:public type_with_subtypet
   }
 };
 
+/// This method tests,
+/// if the given typet is a signed or unsigned bitvector.
+inline bool is_signed_or_unsigned_bitvector(const typet &type)
+{
+  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
+}
+
 /*! \brief Cast a generic typet to a \ref bitvector_typet
  *
  * This is an unchecked conversion. \a type must be known to be \ref
@@ -1487,6 +1514,20 @@ inline void validate_type(const pointer_typet &type)
   DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
 }
 
+/// This method tests,
+/// if the given typet is a pointer.
+inline bool is_pointer(const typet &type)
+{
+  return type.id() == ID_pointer;
+}
+
+/// This method tests,
+/// if the given typet is a pointer of type void.
+inline bool is_void_pointer(const typet &type)
+{
+  return is_pointer(type) && type.subtype().id() == ID_empty;
+}
+
 /*! \brief The reference type
 */
 class reference_typet:public pointer_typet