Cleanup types [DOC-12]

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -12,10 +12,11 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
 
-#include <vector>
 #include <set>
 #include <unordered_set>
+#include <util/namespace.h>
 #include <util/symbol_table.h>
+#include <vector>
 
 class select_pointer_typet;
 class pointer_typet;

src/util/Makefile

@@ -41,6 +41,7 @@ SRC = arith_tools.cpp \
       json_stream.cpp \
       lispexpr.cpp \
       lispirep.cpp \
+      mathematical_types.cpp \
       memory_info.cpp \
       merge_irep.cpp \
       message.cpp \

src/util/mathematical_types.cpp

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Mathematical types
+
+#include "mathematical_types.h"
+
+/// Returns true if the type is a rational, real, integer, natural, complex,
+/// unsignedbv, signedbv, floatbv or fixedbv.
+bool is_number(const typet &type)
+{
+  const irep_idt &id = type.id();
+  return id == ID_rational || id == ID_real || id == ID_integer ||
+         id == ID_natural || id == ID_complex || id == ID_unsignedbv ||
+         id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv;
+}

src/util/mathematical_types.h

@@ -0,0 +1,162 @@
+/*******************************************************************\
+
+Module: Mathematical types
+
+Author: Daniel Kroening, [email protected]
+        Maria Svorenova, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Mathematical types
+
+#ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H
+#define CPROVER_UTIL_MATHEMATICAL_TYPES_H
+
+#include "expr_cast.h"
+#include "invariant.h"
+#include "type.h"
+
+/// Unbounded, signed integers (mathematical integers, not bitvectors)
+class integer_typet : public typet
+{
+public:
+  integer_typet() : typet(ID_integer)
+  {
+  }
+};
+
+/// Natural numbers including zero (mathematical integers, not bitvectors)
+class natural_typet : public typet
+{
+public:
+  natural_typet() : typet(ID_natural)
+  {
+  }
+};
+
+/// Unbounded, signed rational numbers
+class rational_typet : public typet
+{
+public:
+  rational_typet() : typet(ID_rational)
+  {
+  }
+};
+
+/// Unbounded, signed real numbers
+class real_typet : public typet
+{
+public:
+  real_typet() : typet(ID_real)
+  {
+  }
+};
+
+/// A type for mathematical functions (do not confuse with functions/methods
+/// in code)
+class mathematical_function_typet : public typet
+{
+public:
+  // the domain of the function is composed of zero, one, or
+  // many variables
+  class variablet : public irept
+  {
+  public:
+    // the identifier is optional
+    irep_idt get_identifier() const
+    {
+      return get(ID_identifier);
+    }
+
+    void set_identifier(const irep_idt &identifier)
+    {
+      return set(ID_identifier, identifier);
+    }
+
+    typet &type()
+    {
+      return static_cast<typet &>(add(ID_type));
+    }
+
+    const typet &type() const
+    {
+      return static_cast<const typet &>(find(ID_type));
+    }
+  };
+
+  using domaint = std::vector<variablet>;
+
+  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
+    : typet(ID_mathematical_function)
+  {
+    subtypes().resize(2);
+    domain() = _domain;
+    codomain() = _codomain;
+  }
+
+  domaint &domain()
+  {
+    return (domaint &)subtypes()[0].subtypes();
+  }
+
+  const domaint &domain() const
+  {
+    return (const domaint &)subtypes()[0].subtypes();
+  }
+
+  variablet &add_variable()
+  {
+    auto &d = domain();
+    d.push_back(variablet());
+    return d.back();
+  }
+
+  /// Return the codomain, i.e., the set of values that the function maps to
+  /// (the "target").
+  typet &codomain()
+  {
+    return subtypes()[1];
+  }
+
+  /// \copydoc codomain()
+  const typet &codomain() const
+  {
+    return subtypes()[1];
+  }
+};
+
+/// Check whether a reference to a typet is a \ref mathematical_function_typet.
+/// \param type Source type.
+/// \return True if \param type is a \ref mathematical_function_typet.
+template <>
+inline bool can_cast_type<mathematical_function_typet>(const typet &type)
+{
+  return type.id() == ID_mathematical_function;
+}
+
+/// \brief Cast a typet to a \ref mathematical_function_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// mathematical_function_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type Source type.
+/// \return Object of type \ref mathematical_function_typet.
+inline const mathematical_function_typet &
+to_mathematical_function_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<mathematical_function_typet>(type));
+  return static_cast<const mathematical_function_typet &>(type);
+}
+
+/// \copydoc to_mathematical_function_type(const typet &)
+inline mathematical_function_typet &to_mathematical_function_type(typet &type)
+{
+  PRECONDITION(can_cast_type<mathematical_function_typet>(type));
+  return static_cast<mathematical_function_typet &>(type);
+}
+
+bool is_number(const typet &type);
+
+#endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H

src/util/simplify_expr_int.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
+#include "mathematical_types.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "rational.h"

src/util/std_expr.h

@@ -13,10 +13,10 @@ Author: Daniel Kroening, [email protected]
 /// \file util/std_expr.h
 /// API to expression classes
 
+#include "expr_cast.h"
 #include "invariant.h"
+#include "mathematical_types.h"
 #include "std_types.h"
-#include "expr_cast.h"
-
 
 /// Transition system, consisting of state invariant, initial state predicate,
 /// and transition predicate.

src/util/std_types.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_types.h"
 
-#include "string2int.h"
 #include "arith_tools.h"
+#include "namespace.h"
 #include "std_expr.h"
+#include "string2int.h"
 
 std::size_t fixedbv_typet::get_integer_bits() const
 {
@@ -195,3 +196,74 @@ constant_exprt unsignedbv_typet::largest_expr() const
 {
   return from_integer(largest(), *this);
 }
+
+/// Identify whether a given type is constant itself or contains constant
+/// components.
+/// Examples include:
+///  - const int a;
+///  - struct contains_constant_pointer {  int x; int * const p; };
+///  - const int b[3];
+/// \param type The type we want to query constness of.
+/// \param ns The namespace, needed for resolution of symbols.
+/// \return Whether passed in type is const or not.
+bool is_constant_or_has_constant_components(
+  const typet &type,
+  const namespacet &ns)
+{
+  // Helper function to avoid the code duplication in the branches
+  // below.
+  const auto has_constant_components = [&ns](const typet &subtype) -> bool {
+    if(subtype.id() == ID_struct || subtype.id() == ID_union)
+    {
+      const auto &struct_union_type = to_struct_union_type(subtype);
+      for(const auto &component : struct_union_type.components())
+      {
+        if(is_constant_or_has_constant_components(component.type(), ns))
+          return true;
+      }
+    }
+    return false;
+  };
+
+  // There are 4 possibilities the code below is handling.
+  // The possibilities are enumerated as comments, to show
+  // what each code is supposed to be handling. For more
+  // comprehensive test case for this, take a look at
+  // regression/cbmc/no_nondet_static/main.c
+
+  // const int a;
+  if(type.get_bool(ID_C_constant))
+    return true;
+
+  // This is a termination condition to break the recursion
+  // for recursive types such as the following:
+  // struct list { const int datum; struct list * next; };
+  // NOTE: the difference between this condition and the previous
+  // one is that this one always returns.
+  if(type.id() == ID_pointer)
+    return type.get_bool(ID_C_constant);
+
+  // When we have a case like the following, we don't immediately
+  // see the struct t. Instead, we only get to see symbol t1, which
+  // we have to use the namespace to resolve to its definition:
+  // struct t { const int a; };
+  // struct t t1;
+  if(type.id() == ID_symbol_type)
+  {
+    const auto &resolved_type = ns.follow(type);
+    return has_constant_components(resolved_type);
+  }
+
+  // In a case like this, where we see an array (b[3] here), we know that
+  // the array contains subtypes. We get the first one, and
+  // then resolve it to its  definition through the usage of the namespace.
+  // struct contains_constant_pointer { int x; int * const p; };
+  // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} };
+  if(type.has_subtype())
+  {
+    const auto &subtype = type.subtype();
+    return is_constant_or_has_constant_components(subtype, ns);
+  }
+
+  return false;
+}