Skip to content

Commit

Permalink
Add functions for configuring x87 floating-point unit.
Browse files Browse the repository at this point in the history
* On x86_32, gcc sets the x87 floating-point unit to extended
  precision mode by default. Provide a function for setting
  double precision mode so that floating point computations
  behave similar to x84_64 builds (which use SSE).

* NOTE: Instead of resetting the x87 precision mode, one should
  probably enable SSE on x86_32 (e.g. via -mfpmath=sse -msse2).
  • Loading branch information
BenKaufmann committed Dec 3, 2024
1 parent 7e112cc commit cc7b8c7
Show file tree
Hide file tree
Showing 3 changed files with 50 additions and 1 deletion.
2 changes: 1 addition & 1 deletion potassco/basic_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,7 @@ class AbstractProgram {
virtual void project(const AtomSpan& atoms);
//! Output @c str whenever condition is true in a stable model.
virtual void output(const std::string_view& str, const LitSpan& condition);
//! If @c v is not equal to @c Value_t::release, mark a as external and assume value @c v. Otherwise, treat @c a as
//! If `v` is not equal to `Value_t::release`, mark `a` as external and assume value `v`. Otherwise, treat `a` as
//! regular atom.
virtual void external(Atom_t a, Value_t v);
//! Assume the given literals to true during solving.
Expand Down
10 changes: 10 additions & 0 deletions potassco/platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,16 @@ using AbortHandler = void (*)(const char* msg);
*/
extern AbortHandler setAbortHandler(AbortHandler handler);

//! Sets x87 floating-point unit to double precision if needed and returns the previous configuration.
/*!
* \note This function does nothing (and returns 0) if x87 floating-point unit is not active.
* \note x87 floating-point unit is typically only used on x86_32 (x86_64 uses SSE by default).
* \return The previous configuration or UINT32_MAX if configuration failed.
*/
unsigned initFpuPrecision();
//! Restores x87 floating-point unit to a previous configuration `r` returned from initFpuPrecision().
void restoreFpuPrecision(unsigned r);

} // namespace Potassco

///@}
Expand Down
39 changes: 39 additions & 0 deletions src/error.cpp
Original file line number Diff line number Diff line change
@@ -1,16 +1,55 @@
#include <potassco/error.h>

#if __has_include(<fpu_control.h>)
#include <fpu_control.h>
#endif

#include <cfloat>
#include <charconv>
#include <cstdarg>
#include <cstdio>
#include <span>
#include <utility>

#if FLT_EVAL_METHOD == 2 || FLT_EVAL_METHOD < 0
#if defined(_MSC_VER) || defined(_WIN32)
#pragma fenv_access(on)
#endif
static unsigned setFpuPrecision(unsigned* r) {
#if defined(_FPU_GETCW) && defined(_FPU_SETCW) && defined(_FPU_DOUBLE)
fpu_control_t cw;
_FPU_GETCW(cw);
if (r && cw == static_cast<fpu_control_t>(*r)) {
return *r;
}
auto nw = static_cast<fpu_control_t>(
not r ? (cw & ~static_cast<fpu_control_t>(_FPU_EXTENDED) & ~static_cast<fpu_control_t>(_FPU_SINGLE)) |
static_cast<fpu_control_t>(_FPU_DOUBLE)
: static_cast<fpu_control_t>(*r));
_FPU_SETCW(nw);
return static_cast<unsigned>(cw);
#elif defined(_MSC_VER) || defined(_WIN32)
unsigned cw = _controlfp(0, 0);
unsigned nw = not r ? static_cast<unsigned>(_PC_53) : *r;
_controlfp(nw, _MCW_PC);
return cw;
#else
return UINT32_MAX;
#endif
return 0u;
}
#else
constexpr unsigned setFpuPrecision(unsigned*) { return 0u; }
#endif

namespace Potassco {
using namespace std::literals;

static constexpr auto c_file = std::string_view{__FILE__};

unsigned initFpuPrecision() { return setFpuPrecision(nullptr); }
void restoreFpuPrecision(unsigned r) { setFpuPrecision(&r); }

const char* ExpressionInfo::relativeFileName(const std::source_location& loc) {
auto res = loc.file_name();
for (auto cmp = c_file; *res && not cmp.empty() && *res == cmp.front(); cmp.remove_prefix(1), ++res) { ; }
Expand Down

0 comments on commit cc7b8c7

Please sign in to comment.