fixedbv.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "fixedbv.h"
 
#include "arith_tools.h"
#include "bitvector_types.h"
#include "std_expr.h"
 
fixedbv_spect::fixedbv_spect(const fixedbv_typet &type)
{
  integer_bits=type.get_integer_bits();
  width=type.get_width();
}
 
fixedbvt::fixedbvt(const constant_exprt &expr)
{
  from_expr(expr);
}
 
void fixedbvt::from_expr(const constant_exprt &expr)
{
  spec=fixedbv_spect(to_fixedbv_type(expr.type()));
  v = bvrep2integer(expr.get_value(), spec.width, true);
}
 
void fixedbvt::from_integer(const mp_integer &i)
{
  v=i*power(2, spec.get_fraction_bits());
}
 
mp_integer fixedbvt::to_integer() const
{
  // this rounds to zero, i.e., we just divide
  return v/power(2, spec.get_fraction_bits());
}
 
constant_exprt fixedbvt::to_expr() const
{
  fixedbv_typet type;
  type.set_width(spec.width);
  type.set_integer_bits(spec.integer_bits);
  PRECONDITION(spec.width != 0);
  return constant_exprt(integer2bvrep(v, spec.width), type);
}
 
void fixedbvt::round(const fixedbv_spect &dest_spec)
{
  std::size_t old_fraction_bits=spec.width-spec.integer_bits;
  std::size_t new_fraction_bits=dest_spec.width-dest_spec.integer_bits;
 
  mp_integer result;
 
  if(new_fraction_bits>old_fraction_bits)
    result=v*power(2, new_fraction_bits-old_fraction_bits);
  else if(new_fraction_bits<old_fraction_bits)
  {
    // may need to round
    mp_integer p=power(2, old_fraction_bits-new_fraction_bits);
    mp_integer div=v/p;
    mp_integer rem=v%p;
    if(rem<0)
      rem=-rem;
 
    if(rem*2>=p)
    {
      if(v<0)
        --div;
      else
        ++div;
    }
 
    result=div;
  }
  else // new_faction_bits==old_fraction_vits
  {
    // no change!
    result=v;
  }
 
  v=result;
  spec=dest_spec;
}
 
void fixedbvt::negate()
{
  v=-v;
}
 
fixedbvt &fixedbvt::operator*=(const fixedbvt &o)
{
  v*=o.v;
 
  fixedbv_spect old_spec=spec;
 
  spec.width+=o.spec.width;
  spec.integer_bits+=o.spec.integer_bits;
 
  round(old_spec);
 
  return *this;
}
 
fixedbvt &fixedbvt::operator+=(const fixedbvt &o)
{
  v += o.v;
  return *this;
}
 
fixedbvt &fixedbvt::operator-=(const fixedbvt &o)
{
  v -= o.v;
  return *this;
}
 
fixedbvt &fixedbvt::operator/=(const fixedbvt &o)
{
  v*=power(2, o.spec.get_fraction_bits());
  v/=o.v;
 
  return *this;
}
 
bool fixedbvt::operator==(int i) const
{
  return v==power(2, spec.get_fraction_bits())*i;
}
 
std::string fixedbvt::format(
  const format_spect &format_spec) const
{
  std::string dest;
  std::size_t fraction_bits=spec.get_fraction_bits();
 
  mp_integer int_value=v;
  mp_integer factor=power(2, fraction_bits);
 
  if(int_value.is_negative())
  {
    dest+='-';
    int_value.negate();
  }
 
  std::string base_10_string=
    integer2string(int_value*power(10, fraction_bits)/factor);
 
  while(base_10_string.size()<=fraction_bits)
    base_10_string="0"+base_10_string;
 
  std::string integer_part=
    std::string(base_10_string, 0, base_10_string.size()-fraction_bits);
 
  std::string fraction_part=
    std::string(base_10_string, base_10_string.size()-fraction_bits);
 
  dest+=integer_part;
 
  // strip trailing zeros
  while(!fraction_part.empty() &&
        fraction_part[fraction_part.size()-1]=='0')
    fraction_part.resize(fraction_part.size()-1);
 
  if(!fraction_part.empty())
    dest+="."+fraction_part;
 
  while(dest.size()<format_spec.min_width)
    dest=" "+dest;
 
  return dest;
}