From 7191e58e5561a159c0cd3b81fddbe311ba70a45b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 19 Nov 2020 14:05:31 -0800 Subject: [PATCH] floatingpoint.h: Split in preparation to cleanly separate symFPU glue code. (#5478) --- src/util/CMakeLists.txt | 5 + src/util/floatingpoint.cpp | 419 -------------------------------- src/util/floatingpoint.h.in | 334 +------------------------ src/util/floatingpoint_size.cpp | 34 +++ src/util/floatingpoint_size.h | 97 ++++++++ src/util/roundingmode.h | 50 ++++ src/util/symfpu_literal.cpp | 409 +++++++++++++++++++++++++++++++ src/util/symfpu_literal.h.in | 259 ++++++++++++++++++++ 8 files changed, 858 insertions(+), 749 deletions(-) create mode 100644 src/util/floatingpoint_size.cpp create mode 100644 src/util/floatingpoint_size.h create mode 100644 src/util/roundingmode.h create mode 100644 src/util/symfpu_literal.cpp create mode 100644 src/util/symfpu_literal.h.in diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 462c9090d..94ded3777 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -8,6 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## +configure_file(symfpu_literal.h.in symfpu_literal.h) configure_file(floatingpoint.h.in floatingpoint.h) configure_file(rational.h.in rational.h) configure_file(integer.h.in integer.h) @@ -26,6 +27,8 @@ libcvc4_add_sources( divisible.cpp divisible.h floatingpoint.cpp + floatingpoint_size.cpp + floatingpoint_size.h gmp_util.h hash.h iand.h @@ -44,6 +47,7 @@ libcvc4_add_sources( result.h regexp.cpp regexp.h + roundingmode.h safe_print.cpp safe_print.h sampler.cpp @@ -58,6 +62,7 @@ libcvc4_add_sources( statistics_registry.h string.cpp string.h + symfpu_literal.cpp tuple.h unsafe_interrupt_exception.h utility.cpp diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index cfb0120fb..ae6197791 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -64,427 +64,8 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); } #endif -#ifndef CVC4_USE_SYMFPU -#define PRECONDITION(X) Assert((X)) -#endif - namespace CVC4 { -FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size) - : d_exp_size(exp_size), d_sig_size(sig_size) -{ - PrettyCheckArgument(validExponentSize(exp_size), - exp_size, - "Invalid exponent size : %d", - exp_size); - PrettyCheckArgument(validSignificandSize(sig_size), - sig_size, - "Invalid significand size : %d", - sig_size); -} - -FloatingPointSize::FloatingPointSize(const FloatingPointSize& old) - : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size) -{ - PrettyCheckArgument(validExponentSize(d_exp_size), - d_exp_size, - "Invalid exponent size : %d", - d_exp_size); - PrettyCheckArgument(validSignificandSize(d_sig_size), - d_sig_size, - "Invalid significand size : %d", - d_sig_size); -} - -namespace symfpuLiteral { - -// To simplify the property macros -typedef traits t; - -template -wrappedBitVector wrappedBitVector::one( - const CVC4BitWidth& w) -{ - return wrappedBitVector(w, 1); -} - -template -wrappedBitVector wrappedBitVector::zero( - const CVC4BitWidth& w) -{ - return wrappedBitVector(w, 0); -} - -template -wrappedBitVector wrappedBitVector::allOnes( - const CVC4BitWidth& w) -{ - return ~wrappedBitVector::zero(w); -} - -template -CVC4Prop wrappedBitVector::isAllOnes() const -{ - return (*this == wrappedBitVector::allOnes(this->getWidth())); -} -template -CVC4Prop wrappedBitVector::isAllZeros() const -{ - return (*this == wrappedBitVector::zero(this->getWidth())); -} - -template -wrappedBitVector wrappedBitVector::maxValue( - const CVC4BitWidth& w) -{ - if (isSigned) - { - BitVector base(w - 1, 0U); - return wrappedBitVector((~base).zeroExtend(1)); - } - else - { - return wrappedBitVector::allOnes(w); - } -} - -template -wrappedBitVector wrappedBitVector::minValue( - const CVC4BitWidth& w) -{ - if (isSigned) - { - BitVector base(w, 1U); - BitVector shiftAmount(w, w - 1); - BitVector result(base.leftShift(shiftAmount)); - return wrappedBitVector(result); - } - else - { - return wrappedBitVector::zero(w); - } -} - -/*** Operators ***/ -template -wrappedBitVector wrappedBitVector::operator<<( - const wrappedBitVector &op) const -{ - return this->BitVector::leftShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector &op) const -{ - return this->BitVector::arithRightShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector &op) const -{ - return this->BitVector::logicalRightShift(op); -} - -template -wrappedBitVector wrappedBitVector::operator|( - const wrappedBitVector &op) const -{ - return this->BitVector::operator|(op); -} - -template -wrappedBitVector wrappedBitVector::operator&( - const wrappedBitVector &op) const -{ - return this->BitVector::operator&(op); -} - -template -wrappedBitVector wrappedBitVector::operator+( - const wrappedBitVector &op) const -{ - return this->BitVector::operator+(op); -} - -template -wrappedBitVector wrappedBitVector::operator-( - const wrappedBitVector &op) const -{ - return this->BitVector::operator-(op); -} - -template -wrappedBitVector wrappedBitVector::operator*( - const wrappedBitVector &op) const -{ - return this->BitVector::operator*(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator/( - const wrappedBitVector &op) const -{ - return this->BitVector::unsignedDivTotal(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator%( - const wrappedBitVector &op) const -{ - return this->BitVector::unsignedRemTotal(op); -} - -template -wrappedBitVector wrappedBitVector::operator-(void) const -{ - return this->BitVector::operator-(); -} - -template -wrappedBitVector wrappedBitVector::operator~(void)const -{ - return this->BitVector::operator~(); -} - -template -wrappedBitVector wrappedBitVector::increment() const -{ - return *this + wrappedBitVector::one(this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::decrement() const -{ - return *this - wrappedBitVector::one(this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::signExtendRightShift( - const wrappedBitVector &op) const -{ - return this->BitVector::arithRightShift(BitVector(this->getWidth(), op)); -} - -/*** Modular opertaions ***/ -// No overflow checking so these are the same as other operations -template -wrappedBitVector wrappedBitVector::modularLeftShift( - const wrappedBitVector &op) const -{ - return *this << op; -} - -template -wrappedBitVector wrappedBitVector::modularRightShift( - const wrappedBitVector &op) const -{ - return *this >> op; -} - -template -wrappedBitVector wrappedBitVector::modularIncrement() const -{ - return this->increment(); -} - -template -wrappedBitVector wrappedBitVector::modularDecrement() const -{ - return this->decrement(); -} - -template -wrappedBitVector wrappedBitVector::modularAdd( - const wrappedBitVector &op) const -{ - return *this + op; -} - -template -wrappedBitVector wrappedBitVector::modularNegate() const -{ - return -(*this); -} - -/*** Comparisons ***/ - -template -CVC4Prop wrappedBitVector::operator==( - const wrappedBitVector& op) const -{ - return this->BitVector::operator==(op); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return this->signedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(this->signedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return this->signedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(this->signedLessThanEq(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return this->unsignedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(this->unsignedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return this->unsignedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(this->unsignedLessThanEq(op)); -} - -/*** Type conversion ***/ -// CVC4 nodes make no distinction between signed and unsigned, thus ... -template -wrappedBitVector wrappedBitVector::toSigned(void) const -{ - return wrappedBitVector(*this); -} - -template -wrappedBitVector wrappedBitVector::toUnsigned(void) const -{ - return wrappedBitVector(*this); -} - -/*** Bit hacks ***/ - -template -wrappedBitVector wrappedBitVector::extend( - CVC4BitWidth extension) const -{ - if (isSigned) - { - return this->BitVector::signExtend(extension); - } - else - { - return this->BitVector::zeroExtend(extension); - } -} - -template -wrappedBitVector wrappedBitVector::contract( - CVC4BitWidth reduction) const -{ - PRECONDITION(this->getWidth() > reduction); - - return this->extract((this->getWidth() - 1) - reduction, 0); -} - -template -wrappedBitVector wrappedBitVector::resize( - CVC4BitWidth newSize) const -{ - CVC4BitWidth width = this->getWidth(); - - if (newSize > width) - { - return this->extend(newSize - width); - } - else if (newSize < width) - { - return this->contract(width - newSize); - } - else - { - return *this; - } -} - -template -wrappedBitVector wrappedBitVector::matchWidth( - const wrappedBitVector &op) const -{ - PRECONDITION(this->getWidth() <= op.getWidth()); - return this->extend(op.getWidth() - this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::append( - const wrappedBitVector &op) const -{ - return this->BitVector::concat(op); -} - -// Inclusive of end points, thus if the same, extracts just one bit -template -wrappedBitVector wrappedBitVector::extract( - CVC4BitWidth upper, CVC4BitWidth lower) const -{ - PRECONDITION(upper >= lower); - return this->BitVector::extract(upper, lower); -} - -// Explicit instantiation -template class wrappedBitVector; -template class wrappedBitVector; - -traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; -traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; -traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; -traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; -traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; -// This is a literal back-end so props are actually bools -// so these can be handled in the same way as the internal assertions above - -void traits::precondition(const traits::prop& p) -{ - Assert(p); - return; -} -void traits::postcondition(const traits::prop& p) -{ - Assert(p); - return; -} -void traits::invariant(const traits::prop& p) -{ - Assert(p); - return; -} -} - #ifndef CVC4_USE_SYMFPU void FloatingPointLiteral::unfinished(void) const { diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index 7e430ad87..bcf792c56 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -20,10 +20,11 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H -#include - #include "util/bitvector.h" +#include "util/floatingpoint_size.h" #include "util/rational.h" +#include "util/roundingmode.h" +#include "util/symfpu_literal.h" // clang-format off #if @CVC4_USE_SYMFPU@ @@ -31,339 +32,12 @@ #include #endif /* @CVC4_USE_SYMFPU@ */ -namespace CVC4 { -// Inline these! -inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; } -inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; } - -/* -------------------------------------------------------------------------- */ - -/** - * Floating point sorts are parameterised by two constants > 1 giving the - * width (in bits) of the exponent and significand (including the hidden bit). - * So, IEEE-754 single precision, a.k.a. float, is described as 8 24. - */ -class CVC4_PUBLIC FloatingPointSize -{ - public: - /** Constructors. */ - FloatingPointSize(uint32_t exp_size, uint32_t sig_size); - FloatingPointSize(const FloatingPointSize& old); - - /** Operator overload for equality comparison. */ - bool operator==(const FloatingPointSize& fps) const - { - return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size); - } - - /** Implement the interface that symfpu uses for floating-point formats. */ - - /** Get the exponent bit-width of this floating-point format. */ - inline uint32_t exponentWidth(void) const { return this->d_exp_size; } - /** Get the significand bit-width of this floating-point format. */ - inline uint32_t significandWidth(void) const { return this->d_sig_size; } - /** - * Get the bit-width of the packed representation of this floating-point - * format (= exponent + significand bit-width, convenience wrapper). - */ - inline uint32_t packedWidth(void) const - { - return this->exponentWidth() + this->significandWidth(); - } - /** - * Get the exponent bit-width of the packed representation of this - * floating-point format (= exponent bit-width). - */ - inline uint32_t packedExponentWidth(void) const - { - return this->exponentWidth(); - } - /** - * Get the significand bit-width of the packed representation of this - * floating-point format (= significand bit-width - 1). - */ - inline uint32_t packedSignificandWidth(void) const - { - return this->significandWidth() - 1; - } - - private: - /** Exponent bit-width. */ - uint32_t d_exp_size; - /** Significand bit-width. */ - uint32_t d_sig_size; - -}; /* class FloatingPointSize */ - -/** - * Hash function for floating point formats. - */ -struct CVC4_PUBLIC FloatingPointSizeHashFunction -{ - static inline size_t ROLL(size_t X, size_t N) - { - return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N)))); - } - - inline size_t operator()(const FloatingPointSize& t) const - { - return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t)) - | t.significandWidth()); - } -}; /* struct FloatingPointSizeHashFunction */ - /* -------------------------------------------------------------------------- */ -/** - * A concrete instance of the rounding mode sort - */ -enum CVC4_PUBLIC RoundingMode -{ - roundNearestTiesToEven = FE_TONEAREST, - roundTowardPositive = FE_UPWARD, - roundTowardNegative = FE_DOWNWARD, - roundTowardZero = FE_TOWARDZERO, - // Initializes this to the diagonalization of the 4 other values. - roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) - | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) -}; /* enum RoundingMode */ - -/** - * Hash function for rounding mode values. - */ -struct CVC4_PUBLIC RoundingModeHashFunction -{ - inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } -}; /* struct RoundingModeHashFunction */ +namespace CVC4 { /* -------------------------------------------------------------------------- */ -/** - * This is a symfpu literal "back-end". It allows the library to be used as - * an arbitrary precision floating-point implementation. This is effectively - * the glue between symfpu's notion of "signed bit-vector" and CVC4's - * BitVector. - */ -namespace symfpuLiteral { - -/** - * Forward declaration of wrapper so that traits can be defined early and so - * used in the implementation of wrappedBitVector. - */ -template -class wrappedBitVector; - -using CVC4BitWidth = uint32_t; -using CVC4Prop = bool; -using CVC4RM = ::CVC4::RoundingMode; -using CVC4FPSize = ::CVC4::FloatingPointSize; -using CVC4UnsignedBitVector = wrappedBitVector; -using CVC4SignedBitVector = wrappedBitVector; - -/** - * This is the template parameter for symfpu's templates. - */ -class traits -{ - public: - /** The six key types that symfpu uses. */ - using bwt = CVC4BitWidth; // bit-width type - using prop = CVC4Prop; // boolean type - using rm = CVC4RM; // rounding-mode type - using fpt = CVC4FPSize; // floating-point format type - using ubv = CVC4UnsignedBitVector; // unsigned bit-vector type - using sbv = CVC4SignedBitVector; // signed bit-vector type - - /** Give concrete instances of each rounding mode, mainly for comparisons. */ - static rm RNE(void); - static rm RNA(void); - static rm RTP(void); - static rm RTN(void); - static rm RTZ(void); - - /** The sympfu properties. */ - static void precondition(const prop& p); - static void postcondition(const prop& p); - static void invariant(const prop& p); -}; - -/** - * Type function for mapping between types. - */ -template -struct signedToLiteralType; - -template <> -struct signedToLiteralType -{ - using literalType = int32_t; -}; -template <> -struct signedToLiteralType -{ - using literalType = uint32_t; -}; - -/** - * This extends the interface for CVC4::BitVector for compatibility with symFPU. - * The template parameter distinguishes signed and unsigned bit-vectors, a - * distinction symfpu uses. - */ -template -class wrappedBitVector : public BitVector -{ - protected: - using literalType = typename signedToLiteralType::literalType; - friend wrappedBitVector; // To allow conversion between types - -// clang-format off -#if @CVC4_USE_SYMFPU@ - // clang-format on - friend ::symfpu::ite >; // For ITE -#endif /* @CVC4_USE_SYMFPU@ */ - - public: - /** Constructors. */ - wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {} - wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {} - wrappedBitVector(const wrappedBitVector& old) : BitVector(old) {} - wrappedBitVector(const BitVector& old) : BitVector(old) {} - - /** Get the bit-width of this wrapped bit-vector. */ - CVC4BitWidth getWidth(void) const { return getSize(); } - - /** Create a zero value of given bit-width 'w'. */ - static wrappedBitVector one(const CVC4BitWidth& w); - /** Create a one value of given bit-width 'w'. */ - static wrappedBitVector zero(const CVC4BitWidth& w); - /** Create a ones value (all bits 1) of given bit-width 'w'. */ - static wrappedBitVector allOnes(const CVC4BitWidth& w); - /** Create a maximum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector maxValue(const CVC4BitWidth& w); - /** Create a minimum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector minValue(const CVC4BitWidth& w); - - /** Return true if this a bit-vector representing a ones value. */ - CVC4Prop isAllOnes() const; - /** Return true if this a bit-vector representing a zero value. */ - CVC4Prop isAllZeros() const; - - /** Left shift. */ - wrappedBitVector operator<<( - const wrappedBitVector& op) const; - /** Logical (unsigned) and arithmetic (signed) right shift. */ - wrappedBitVector operator>>( - const wrappedBitVector& op) const; - - /** - * Inherited but ... - * *sigh* if we use the inherited version then it will return a - * CVC4::BitVector which can be converted back to a - * wrappedBitVector but isn't done automatically when working - * out types for templates instantiation. ITE is a particular - * problem as expressions and constants no longer derive the - * same type. There aren't any good solutions in C++, we could - * use CRTP but Liana wouldn't appreciate that, so the following - * pointless wrapping functions are needed. - */ - - /** Bit-wise or. */ - wrappedBitVector operator|( - const wrappedBitVector& op) const; - /** Bit-wise and. */ - wrappedBitVector operator&( - const wrappedBitVector& op) const; - /** Bit-vector addition. */ - wrappedBitVector operator+( - const wrappedBitVector& op) const; - /** Bit-vector subtraction. */ - wrappedBitVector operator-( - const wrappedBitVector& op) const; - /** Bit-vector multiplication. */ - wrappedBitVector operator*( - const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned division. */ - wrappedBitVector operator/( - const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned remainder. */ - wrappedBitVector operator%( - const wrappedBitVector& op) const; - /** Bit-vector negation. */ - wrappedBitVector operator-(void) const; - /** Bit-wise not. */ - wrappedBitVector operator~(void) const; - - /** Bit-vector increment. */ - wrappedBitVector increment() const; - /** Bit-vector decrement. */ - wrappedBitVector decrement() const; - /** - * Bit-vector logical/arithmetic right shift where 'op' extended to the - * bit-width of this wrapped bit-vector. - */ - wrappedBitVector signExtendRightShift( - const wrappedBitVector& op) const; - - /** - * Modular operations. - * Note: No overflow checking so these are the same as other operations. - */ - wrappedBitVector modularLeftShift( - const wrappedBitVector& op) const; - wrappedBitVector modularRightShift( - const wrappedBitVector& op) const; - wrappedBitVector modularIncrement() const; - wrappedBitVector modularDecrement() const; - wrappedBitVector modularAdd( - const wrappedBitVector& op) const; - wrappedBitVector modularNegate() const; - - /** Bit-vector equality. */ - CVC4Prop operator==(const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned less or equal than. */ - CVC4Prop operator<=(const wrappedBitVector& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>=(const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned less than. */ - CVC4Prop operator<(const wrappedBitVector& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>(const wrappedBitVector& op) const; - - /** Convert this bit-vector to a signed bit-vector. */ - wrappedBitVector toSigned(void) const; - /** Convert this bit-vector to an unsigned bit-vector. */ - wrappedBitVector toUnsigned(void) const; - - /** Bit-vector signed/unsigned (zero) extension. */ - wrappedBitVector extend(CVC4BitWidth extension) const; - /** - * Create a "contracted" bit-vector by cutting off the 'reduction' number of - * most significant bits, i.e., by extracting the (bit-width - reduction) - * least significant bits. - */ - wrappedBitVector contract(CVC4BitWidth reduction) const; - /** - * Create a "resized" bit-vector of given size bei either extending (if new - * size is larger) or contracting (if it is smaller) this wrapped bit-vector. - */ - wrappedBitVector resize(CVC4BitWidth newSize) const; - /** - * Create an extension of this bit-vector that matches the bit-width of the - * given bit-vector. - * Note: The size of the given bit-vector may not be larger than the size of - * this bit-vector. - */ - wrappedBitVector matchWidth( - const wrappedBitVector& op) const; - /** Bit-vector concatenation. */ - wrappedBitVector append(const wrappedBitVector& op) const; - - /** Inclusive of end points, thus if the same, extracts just one bit. */ - wrappedBitVector extract(CVC4BitWidth upper, - CVC4BitWidth lower) const; -}; -} // namespace symfpuLiteral - /** * A concrete floating point value. */ diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp new file mode 100644 index 000000000..e068eb69a --- /dev/null +++ b/src/util/floatingpoint_size.cpp @@ -0,0 +1,34 @@ +/********************* */ +/*! \file floatingpoint_size.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The class representing a floating-point format. + **/ +#include "util/floatingpoint_size.h" + +#include "base/check.h" + +namespace CVC4 { + +FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size) + : d_exp_size(exp_size), d_sig_size(sig_size) +{ + Assert(validExponentSize(exp_size)); + Assert(validSignificandSize(sig_size)); +} + +FloatingPointSize::FloatingPointSize(const FloatingPointSize& old) + : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size) +{ + Assert(validExponentSize(d_exp_size)); + Assert(validSignificandSize(d_sig_size)); +} + +} // namespace CVC4 diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h new file mode 100644 index 000000000..20684ca42 --- /dev/null +++ b/src/util/floatingpoint_size.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \file floatingpoint_size.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The class representing a floating-point format. + **/ +#include "cvc4_public.h" + +#ifndef CVC4__FLOATINGPOINT_SIZE_H +#define CVC4__FLOATINGPOINT_SIZE_H + +namespace CVC4 { + +// Inline these! +inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; } +inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; } + +/** + * Floating point sorts are parameterised by two constants > 1 giving the + * width (in bits) of the exponent and significand (including the hidden bit). + * So, IEEE-754 single precision, a.k.a. float, is described as 8 24. + */ +class CVC4_PUBLIC FloatingPointSize +{ + public: + /** Constructors. */ + FloatingPointSize(uint32_t exp_size, uint32_t sig_size); + FloatingPointSize(const FloatingPointSize& old); + + /** Operator overload for equality comparison. */ + bool operator==(const FloatingPointSize& fps) const + { + return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size); + } + + /** Implement the interface that symfpu uses for floating-point formats. */ + + /** Get the exponent bit-width of this floating-point format. */ + inline uint32_t exponentWidth(void) const { return d_exp_size; } + /** Get the significand bit-width of this floating-point format. */ + inline uint32_t significandWidth(void) const { return d_sig_size; } + /** + * Get the bit-width of the packed representation of this floating-point + * format (= exponent + significand bit-width, convenience wrapper). + */ + inline uint32_t packedWidth(void) const + { + return exponentWidth() + significandWidth(); + } + /** + * Get the exponent bit-width of the packed representation of this + * floating-point format (= exponent bit-width). + */ + inline uint32_t packedExponentWidth(void) const { return exponentWidth(); } + /** + * Get the significand bit-width of the packed representation of this + * floating-point format (= significand bit-width - 1). + */ + inline uint32_t packedSignificandWidth(void) const + { + return significandWidth() - 1; + } + + private: + /** Exponent bit-width. */ + uint32_t d_exp_size; + /** Significand bit-width. */ + uint32_t d_sig_size; + +}; /* class FloatingPointSize */ + +/** + * Hash function for floating point formats. + */ +struct CVC4_PUBLIC FloatingPointSizeHashFunction +{ + static inline size_t ROLL(size_t X, size_t N) + { + return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N)))); + } + + inline size_t operator()(const FloatingPointSize& t) const + { + return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t)) + | t.significandWidth()); + } +}; /* struct FloatingPointSizeHashFunction */ +} // namespace CVC4 + +#endif diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h new file mode 100644 index 000000000..181755a60 --- /dev/null +++ b/src/util/roundingmode.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file roundingmode.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The definition of rounding mode values. + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ +#include "cvc4_public.h" + +#ifndef CVC4__ROUNDINGMODE_H +#define CVC4__ROUNDINGMODE_H + +#include + +namespace CVC4 { + +/** + * A concrete instance of the rounding mode sort + */ +enum CVC4_PUBLIC RoundingMode +{ + roundNearestTiesToEven = FE_TONEAREST, + roundTowardPositive = FE_UPWARD, + roundTowardNegative = FE_DOWNWARD, + roundTowardZero = FE_TOWARDZERO, + // Initializes this to the diagonalization of the 4 other values. + roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) + | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) +}; /* enum RoundingMode */ + +/** + * Hash function for rounding mode values. + */ +struct CVC4_PUBLIC RoundingModeHashFunction +{ + inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } +}; /* struct RoundingModeHashFunction */ + +} // namespace CVC4 + +#endif diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp new file mode 100644 index 000000000..a547daccd --- /dev/null +++ b/src/util/symfpu_literal.cpp @@ -0,0 +1,409 @@ +/********************* */ +/*! \file symfpu_literal.cpp + ** \verbatim + ** Top contributors (to current version): + ** Martin Brain, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief SymFPU glue code for floating-point values. + **/ +#include "util/symfpu_literal.h" + +#include "base/check.h" + +namespace CVC4 { + +namespace symfpuLiteral { + +// To simplify the property macros +typedef traits t; + +template +wrappedBitVector wrappedBitVector::one( + const CVC4BitWidth& w) +{ + return wrappedBitVector(w, 1); +} + +template +wrappedBitVector wrappedBitVector::zero( + const CVC4BitWidth& w) +{ + return wrappedBitVector(w, 0); +} + +template +wrappedBitVector wrappedBitVector::allOnes( + const CVC4BitWidth& w) +{ + return ~wrappedBitVector::zero(w); +} + +template +CVC4Prop wrappedBitVector::isAllOnes() const +{ + return (*this == wrappedBitVector::allOnes(this->getWidth())); +} +template +CVC4Prop wrappedBitVector::isAllZeros() const +{ + return (*this == wrappedBitVector::zero(this->getWidth())); +} + +template +wrappedBitVector wrappedBitVector::maxValue( + const CVC4BitWidth& w) +{ + if (isSigned) + { + BitVector base(w - 1, 0U); + return wrappedBitVector((~base).zeroExtend(1)); + } + else + { + return wrappedBitVector::allOnes(w); + } +} + +template +wrappedBitVector wrappedBitVector::minValue( + const CVC4BitWidth& w) +{ + if (isSigned) + { + BitVector base(w, 1U); + BitVector shiftAmount(w, w - 1); + BitVector result(base.leftShift(shiftAmount)); + return wrappedBitVector(result); + } + else + { + return wrappedBitVector::zero(w); + } +} + +/*** Operators ***/ +template +wrappedBitVector wrappedBitVector::operator<<( + const wrappedBitVector& op) const +{ + return this->BitVector::leftShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return this->BitVector::arithRightShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return this->BitVector::logicalRightShift(op); +} + +template +wrappedBitVector wrappedBitVector::operator|( + const wrappedBitVector& op) const +{ + return this->BitVector::operator|(op); +} + +template +wrappedBitVector wrappedBitVector::operator&( + const wrappedBitVector& op) const +{ + return this->BitVector::operator&(op); +} + +template +wrappedBitVector wrappedBitVector::operator+( + const wrappedBitVector& op) const +{ + return this->BitVector::operator+(op); +} + +template +wrappedBitVector wrappedBitVector::operator-( + const wrappedBitVector& op) const +{ + return this->BitVector::operator-(op); +} + +template +wrappedBitVector wrappedBitVector::operator*( + const wrappedBitVector& op) const +{ + return this->BitVector::operator*(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator/( + const wrappedBitVector& op) const +{ + return this->BitVector::unsignedDivTotal(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator%( + const wrappedBitVector& op) const +{ + return this->BitVector::unsignedRemTotal(op); +} + +template +wrappedBitVector wrappedBitVector::operator-(void) const +{ + return this->BitVector::operator-(); +} + +template +wrappedBitVector wrappedBitVector::operator~(void) const +{ + return this->BitVector::operator~(); +} + +template +wrappedBitVector wrappedBitVector::increment() const +{ + return *this + wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::decrement() const +{ + return *this - wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::signExtendRightShift( + const wrappedBitVector& op) const +{ + return this->BitVector::arithRightShift(BitVector(this->getWidth(), op)); +} + +/*** Modular opertaions ***/ +// No overflow checking so these are the same as other operations +template +wrappedBitVector wrappedBitVector::modularLeftShift( + const wrappedBitVector& op) const +{ + return *this << op; +} + +template +wrappedBitVector wrappedBitVector::modularRightShift( + const wrappedBitVector& op) const +{ + return *this >> op; +} + +template +wrappedBitVector wrappedBitVector::modularIncrement() const +{ + return this->increment(); +} + +template +wrappedBitVector wrappedBitVector::modularDecrement() const +{ + return this->decrement(); +} + +template +wrappedBitVector wrappedBitVector::modularAdd( + const wrappedBitVector& op) const +{ + return *this + op; +} + +template +wrappedBitVector wrappedBitVector::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template +CVC4Prop wrappedBitVector::operator==( + const wrappedBitVector& op) const +{ + return this->BitVector::operator==(op); +} + +template <> +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return this->signedLessThanEq(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(this->signedLessThan(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return this->signedLessThan(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(this->signedLessThanEq(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return this->unsignedLessThanEq(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(this->unsignedLessThan(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return this->unsignedLessThan(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(this->unsignedLessThanEq(op)); +} + +/*** Type conversion ***/ +// CVC4 nodes make no distinction between signed and unsigned, thus ... +template +wrappedBitVector wrappedBitVector::toSigned(void) const +{ + return wrappedBitVector(*this); +} + +template +wrappedBitVector wrappedBitVector::toUnsigned(void) const +{ + return wrappedBitVector(*this); +} + +/*** Bit hacks ***/ + +template +wrappedBitVector wrappedBitVector::extend( + CVC4BitWidth extension) const +{ + if (isSigned) + { + return this->BitVector::signExtend(extension); + } + else + { + return this->BitVector::zeroExtend(extension); + } +} + +template +wrappedBitVector wrappedBitVector::contract( + CVC4BitWidth reduction) const +{ + Assert(this->getWidth() > reduction); + + return this->extract((this->getWidth() - 1) - reduction, 0); +} + +template +wrappedBitVector wrappedBitVector::resize( + CVC4BitWidth newSize) const +{ + CVC4BitWidth width = this->getWidth(); + + if (newSize > width) + { + return this->extend(newSize - width); + } + else if (newSize < width) + { + return this->contract(width - newSize); + } + else + { + return *this; + } +} + +template +wrappedBitVector wrappedBitVector::matchWidth( + const wrappedBitVector& op) const +{ + Assert(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::append( + const wrappedBitVector& op) const +{ + return this->BitVector::concat(op); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template +wrappedBitVector wrappedBitVector::extract( + CVC4BitWidth upper, CVC4BitWidth lower) const +{ + Assert(upper >= lower); + return this->BitVector::extract(upper, lower); +} + +// Explicit instantiation +template class wrappedBitVector; +template class wrappedBitVector; + +traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; +traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; +traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; +traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; +traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; +// This is a literal back-end so props are actually bools +// so these can be handled in the same way as the internal assertions above + +void traits::precondition(const traits::prop& p) +{ + Assert(p); + return; +} +void traits::postcondition(const traits::prop& p) +{ + Assert(p); + return; +} +void traits::invariant(const traits::prop& p) +{ + Assert(p); + return; +} +} // namespace symfpuLiteral + +} // namespace CVC4 diff --git a/src/util/symfpu_literal.h.in b/src/util/symfpu_literal.h.in new file mode 100644 index 000000000..e0cd95d52 --- /dev/null +++ b/src/util/symfpu_literal.h.in @@ -0,0 +1,259 @@ +/********************* */ +/*! \file symfpu_literal.h.in + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief SymFPU glue code for floating-point values. + **/ +#include "cvc4_public.h" + +#ifndef CVC4__SYMFPULITERAL__SYMFPU_LITERAL_H +#define CVC4__SYMFPULITERAL__SYMFPU_LITERAL_H + +#include "util/bitvector.h" +#include "util/roundingmode.h" + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on +#include +#endif /* @CVC4_USE_SYMFPU@ */ + +namespace CVC4 { + +class FloatingPointSize; + +/** + * This is a symfpu literal "back-end". It allows the library to be used as + * an arbitrary precision floating-point implementation. This is effectively + * the glue between symfpu's notion of "signed bit-vector" and CVC4's + * BitVector. + */ +namespace symfpuLiteral { + +/** + * Forward declaration of wrapper so that traits can be defined early and so + * used in the implementation of wrappedBitVector. + */ +template +class wrappedBitVector; + +using CVC4BitWidth = uint32_t; +using CVC4Prop = bool; +using CVC4RM = ::CVC4::RoundingMode; +using CVC4FPSize = ::CVC4::FloatingPointSize; +using CVC4UnsignedBitVector = wrappedBitVector; +using CVC4SignedBitVector = wrappedBitVector; + +/** + * This is the template parameter for symfpu's templates. + */ +class traits +{ + public: + /** The six key types that symfpu uses. */ + using bwt = CVC4BitWidth; // bit-width type + using prop = CVC4Prop; // boolean type + using rm = CVC4RM; // rounding-mode type + using fpt = CVC4FPSize; // floating-point format type + using ubv = CVC4UnsignedBitVector; // unsigned bit-vector type + using sbv = CVC4SignedBitVector; // signed bit-vector type + + /** Give concrete instances of each rounding mode, mainly for comparisons. */ + static rm RNE(void); + static rm RNA(void); + static rm RTP(void); + static rm RTN(void); + static rm RTZ(void); + + /** The sympfu properties. */ + static void precondition(const prop& p); + static void postcondition(const prop& p); + static void invariant(const prop& p); +}; + +/** + * Type function for mapping between types. + */ +template +struct signedToLiteralType; + +template <> +struct signedToLiteralType +{ + using literalType = int32_t; +}; +template <> +struct signedToLiteralType +{ + using literalType = uint32_t; +}; + +/** + * This extends the interface for CVC4::BitVector for compatibility with symFPU. + * The template parameter distinguishes signed and unsigned bit-vectors, a + * distinction symfpu uses. + */ +template +class wrappedBitVector : public BitVector +{ + protected: + using literalType = typename signedToLiteralType::literalType; + friend wrappedBitVector; // To allow conversion between types + +// clang-format off +#if @CVC4_USE_SYMFPU@ + // clang-format on + friend ::symfpu::ite >; // For ITE +#endif /* @CVC4_USE_SYMFPU@ */ + + public: + /** Constructors. */ + wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {} + wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {} + wrappedBitVector(const wrappedBitVector& old) : BitVector(old) {} + wrappedBitVector(const BitVector& old) : BitVector(old) {} + + /** Get the bit-width of this wrapped bit-vector. */ + CVC4BitWidth getWidth(void) const { return getSize(); } + + /** Create a zero value of given bit-width 'w'. */ + static wrappedBitVector one(const CVC4BitWidth& w); + /** Create a one value of given bit-width 'w'. */ + static wrappedBitVector zero(const CVC4BitWidth& w); + /** Create a ones value (all bits 1) of given bit-width 'w'. */ + static wrappedBitVector allOnes(const CVC4BitWidth& w); + /** Create a maximum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector maxValue(const CVC4BitWidth& w); + /** Create a minimum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector minValue(const CVC4BitWidth& w); + + /** Return true if this a bit-vector representing a ones value. */ + CVC4Prop isAllOnes() const; + /** Return true if this a bit-vector representing a zero value. */ + CVC4Prop isAllZeros() const; + + /** Left shift. */ + wrappedBitVector operator<<( + const wrappedBitVector& op) const; + /** Logical (unsigned) and arithmetic (signed) right shift. */ + wrappedBitVector operator>>( + const wrappedBitVector& op) const; + + /** + * Inherited but ... + * *sigh* if we use the inherited version then it will return a + * CVC4::BitVector which can be converted back to a + * wrappedBitVector but isn't done automatically when working + * out types for templates instantiation. ITE is a particular + * problem as expressions and constants no longer derive the + * same type. There aren't any good solutions in C++, we could + * use CRTP but Liana wouldn't appreciate that, so the following + * pointless wrapping functions are needed. + */ + + /** Bit-wise or. */ + wrappedBitVector operator|( + const wrappedBitVector& op) const; + /** Bit-wise and. */ + wrappedBitVector operator&( + const wrappedBitVector& op) const; + /** Bit-vector addition. */ + wrappedBitVector operator+( + const wrappedBitVector& op) const; + /** Bit-vector subtraction. */ + wrappedBitVector operator-( + const wrappedBitVector& op) const; + /** Bit-vector multiplication. */ + wrappedBitVector operator*( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned division. */ + wrappedBitVector operator/( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned remainder. */ + wrappedBitVector operator%( + const wrappedBitVector& op) const; + /** Bit-vector negation. */ + wrappedBitVector operator-(void) const; + /** Bit-wise not. */ + wrappedBitVector operator~(void) const; + + /** Bit-vector increment. */ + wrappedBitVector increment() const; + /** Bit-vector decrement. */ + wrappedBitVector decrement() const; + /** + * Bit-vector logical/arithmetic right shift where 'op' extended to the + * bit-width of this wrapped bit-vector. + */ + wrappedBitVector signExtendRightShift( + const wrappedBitVector& op) const; + + /** + * Modular operations. + * Note: No overflow checking so these are the same as other operations. + */ + wrappedBitVector modularLeftShift( + const wrappedBitVector& op) const; + wrappedBitVector modularRightShift( + const wrappedBitVector& op) const; + wrappedBitVector modularIncrement() const; + wrappedBitVector modularDecrement() const; + wrappedBitVector modularAdd( + const wrappedBitVector& op) const; + wrappedBitVector modularNegate() const; + + /** Bit-vector equality. */ + CVC4Prop operator==(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less or equal than. */ + CVC4Prop operator<=(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + CVC4Prop operator>=(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less than. */ + CVC4Prop operator<(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + CVC4Prop operator>(const wrappedBitVector& op) const; + + /** Convert this bit-vector to a signed bit-vector. */ + wrappedBitVector toSigned(void) const; + /** Convert this bit-vector to an unsigned bit-vector. */ + wrappedBitVector toUnsigned(void) const; + + /** Bit-vector signed/unsigned (zero) extension. */ + wrappedBitVector extend(CVC4BitWidth extension) const; + /** + * Create a "contracted" bit-vector by cutting off the 'reduction' number of + * most significant bits, i.e., by extracting the (bit-width - reduction) + * least significant bits. + */ + wrappedBitVector contract(CVC4BitWidth reduction) const; + /** + * Create a "resized" bit-vector of given size bei either extending (if new + * size is larger) or contracting (if it is smaller) this wrapped bit-vector. + */ + wrappedBitVector resize(CVC4BitWidth newSize) const; + /** + * Create an extension of this bit-vector that matches the bit-width of the + * given bit-vector. + * Note: The size of the given bit-vector may not be larger than the size of + * this bit-vector. + */ + wrappedBitVector matchWidth( + const wrappedBitVector& op) const; + /** Bit-vector concatenation. */ + wrappedBitVector append(const wrappedBitVector& op) const; + + /** Inclusive of end points, thus if the same, extracts just one bit. */ + wrappedBitVector extract(CVC4BitWidth upper, + CVC4BitWidth lower) const; +}; +} // namespace symfpuLiteral +} + +#endif -- 2.30.2