util.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Loop Acceleration
 
Author: Matt Lewis
 
\*******************************************************************/
 
 
#include "util.h"
 
#include <iostream>
#include <algorithm>
 
#include <util/c_types.h>
#include <util/std_types.h>
 
signedbv_typet signed_poly_type()
{
  return signed_int_type();
}
signedbv_typet signed_poly_type() {…}
 
unsignedbv_typet unsigned_poly_type()
{
  return unsigned_int_type();
}
unsignedbv_typet unsigned_poly_type() {…}
 
bool is_bitvector(const typet &t)
{
  return t.id()==ID_bv ||
         t.id()==ID_signedbv ||
         t.id()==ID_unsignedbv ||
         t.id()==ID_pointer ||
         t.id()==ID_bool;
}
bool is_bitvector(const typet &t) {…}
 
bool is_signed(const typet &t)
{
  return t.id()==ID_signedbv;
}
bool is_signed(const typet &t) {…}
 
 
bool is_unsigned(const typet &t)
{
  return t.id()==ID_bv ||
         t.id()==ID_unsignedbv ||
         t.id()==ID_pointer ||
         t.id()==ID_bool;
}
bool is_unsigned(const typet &t) {…}
 
typet join_types(const typet &t1, const typet &t2)
{
  // Handle the simple case first...
  if(t1==t2)
  {
    return t1;
  }
 
  // OK, they're not the same type.  Are they both bitvectors?
  if(is_bitvector(t1) && is_bitvector(t2))
  {
    // They are.  That makes things easy!  There are three cases to consider:
    // both types are unsigned, both types are signed or there's one of each.
 
    bitvector_typet b1=to_bitvector_type(t1);
    bitvector_typet b2=to_bitvector_type(t2);
 
    if(is_unsigned(b1) && is_unsigned(b2))
    {
      // We just need to take the max of their widths.
      std::size_t width=std::max(b1.get_width(), b2.get_width());
      return unsignedbv_typet(width);
    }
    else if(is_signed(b1) && is_signed(b2))
    {
      // Again, just need to take the max of the widths.
      std::size_t width=std::max(b1.get_width(), b2.get_width());
      return signedbv_typet(width);
    }
    else
    {
      // This is the (slightly) tricky case.  If we have a signed and an
      // unsigned type, we're going to return a signed type.  And to cast
      // an unsigned type to a signed type, we need the signed type to be
      // at least one bit wider than the unsigned type we're casting from.
      std::size_t signed_width=is_signed(t1) ? b1.get_width() :
                                                 b2.get_width();
      std::size_t unsigned_width=is_signed(t1) ? b2.get_width() :
                                                   b1.get_width();
      // unsigned_width++;
 
      std::size_t width=std::max(signed_width, unsigned_width);
 
      return signedbv_typet(width);
    }
  }
 
  std::cerr << "Tried to join types: "
            << t1.pretty() << " and " << t2.pretty()
            << '\n';
 
  INVARIANT(false, "failed to join types");
}
typet join_types(const typet &t1, const typet &t2) {…}