From e39513b1cb68d66fa5d5b9438d098e3ca7dcd0da Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 17 Jun 2024 17:31:34 +0200 Subject: [PATCH 01/28] Add getOpName and getCondName --- ir/instr.cpp | 154 ++++++++++++++++++++++++++++----------------------- ir/instr.h | 6 ++ 2 files changed, 90 insertions(+), 70 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index e6861ceaf..7a301d4df 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -629,21 +629,24 @@ void FpBinOp::rauw(const Value &what, Value &with) { RAUW(rhs); } -void FpBinOp::print(ostream &os) const { - const char *str = nullptr; +const char* FpBinOp::getOpName() const { switch (op) { - case FAdd: str = "fadd "; break; - case FSub: str = "fsub "; break; - case FMul: str = "fmul "; break; - case FDiv: str = "fdiv "; break; - case FRem: str = "frem "; break; - case FMax: str = "fmax "; break; - case FMin: str = "fmin "; break; - case FMaximum: str = "fmaximum "; break; - case FMinimum: str = "fminimum "; break; - case CopySign: str = "copysign "; break; - } - os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName(); + case FAdd: return "fadd"; break; + case FSub: return "fsub"; break; + case FMul: return "fmul"; break; + case FDiv: return "fdiv"; break; + case FRem: return "frem"; break; + case FMax: return "fmax"; break; + case FMin: return "fmin"; break; + case FMaximum: return "fmaximum"; break; + case FMinimum: return "fminimum"; break; + case CopySign: return "copysign"; break; + } + UNREACHABLE(); +} + +void FpBinOp::print(ostream &os) const { + os << getName() << " = " << getOpName() << " " << fmath << *lhs << ", " << rhs->getName(); if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) @@ -1094,23 +1097,25 @@ void FpUnaryOp::rauw(const Value &what, Value &with) { RAUW(val); } -void FpUnaryOp::print(ostream &os) const { - const char *str = nullptr; +const char* FpUnaryOp::getOpName() const { switch (op) { - case FAbs: str = "fabs "; break; - case FNeg: str = "fneg "; break; - case Canonicalize: str = "canonicalize "; break; - case Ceil: str = "ceil "; break; - case Floor: str = "floor "; break; - case RInt: str = "rint "; break; - case NearbyInt: str = "nearbyint "; break; - case Round: str = "round "; break; - case RoundEven: str = "roundeven "; break; - case Trunc: str = "trunc "; break; - case Sqrt: str = "sqrt "; break; - } - - os << getName() << " = " << str << fmath << *val; + case FAbs: return "fabs"; break; + case FNeg: return "fneg"; break; + case Canonicalize: return "canonicalize"; break; + case Ceil: return "ceil"; break; + case Floor: return "floor"; break; + case RInt: return "rint"; break; + case NearbyInt: return "nearbyint"; break; + case Round: return "round"; break; + case RoundEven: return "roundeven"; break; + case Trunc: return "trunc"; break; + case Sqrt: return "sqrt"; break; + } + UNREACHABLE(); +} + +void FpUnaryOp::print(ostream &os) const { + os << getName() << " = " << getOpName() << " " << fmath << *val; if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) @@ -1400,14 +1405,16 @@ void FpTernaryOp::rauw(const Value &what, Value &with) { RAUW(c); } -void FpTernaryOp::print(ostream &os) const { - const char *str = nullptr; +const char* FpTernaryOp::getOpName() const { switch (op) { - case FMA: str = "fma "; break; - case MulAdd: str = "fmuladd "; break; + case FMA: return "fma"; break; + case MulAdd: return "fmuladd"; break; } + UNREACHABLE(); +} - os << getName() << " = " << str << fmath << *a << ", " << *b << ", " << *c; +void FpTernaryOp::print(ostream &os) const { + os << getName() << " = " << getOpName() << " " << fmath << *a << ", " << *b << ", " << *c; if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) @@ -1485,13 +1492,15 @@ void TestOp::rauw(const Value &what, Value &with) { RAUW(rhs); } -void TestOp::print(ostream &os) const { - const char *str = nullptr; +const char* TestOp::getOpName() const { switch (op) { - case Is_FPClass: str = "is.fpclass "; break; + case Is_FPClass: return "is.fpclass"; break; } + UNREACHABLE(); +} - os << getName() << " = " << str << *lhs << ", " << *rhs; +void TestOp::print(ostream &os) const { + os << getName() << " = " << getOpName() << " " << *lhs << ", " << *rhs; } StateValue TestOp::toSMT(State &s) const { @@ -1732,20 +1741,22 @@ void FpConversionOp::rauw(const Value &what, Value &with) { RAUW(val); } -void FpConversionOp::print(ostream &os) const { - const char *str = nullptr; +const char* FpConversionOp::getOpName() const { switch (op) { - case SIntToFP: str = "sitofp "; break; - case UIntToFP: str = "uitofp "; break; - case FPToSInt: str = "fptosi "; break; - case FPToUInt: str = "fptoui "; break; - case FPExt: str = "fpext "; break; - case FPTrunc: str = "fptrunc "; break; - case LRInt: str = "lrint "; break; - case LRound: str = "lround "; break; + case SIntToFP: return "sitofp"; break; + case UIntToFP: return "uitofp"; break; + case FPToSInt: return "fptosi"; break; + case FPToUInt: return "fptoui"; break; + case FPExt: return "fpext"; break; + case FPTrunc: return "fptrunc"; break; + case LRInt: return "lrint"; break; + case LRound: return "lround"; break; } + UNREACHABLE(); +} - os << getName() << " = " << str; +void FpConversionOp::print(ostream &os) const { + os << getName() << " = " << getOpName() << " "; if (flags & NNEG) os << "nneg "; os << *val << print_type(getType(), " to ", ""); @@ -2731,27 +2742,30 @@ void FCmp::rauw(const Value &what, Value &with) { RAUW(b); } -void FCmp::print(ostream &os) const { - const char *condtxt = nullptr; +const char* FCmp::getCondName() const { switch (cond) { - case OEQ: condtxt = "oeq "; break; - case OGT: condtxt = "ogt "; break; - case OGE: condtxt = "oge "; break; - case OLT: condtxt = "olt "; break; - case OLE: condtxt = "ole "; break; - case ONE: condtxt = "one "; break; - case ORD: condtxt = "ord "; break; - case UEQ: condtxt = "ueq "; break; - case UGT: condtxt = "ugt "; break; - case UGE: condtxt = "uge "; break; - case ULT: condtxt = "ult "; break; - case ULE: condtxt = "ule "; break; - case UNE: condtxt = "une "; break; - case UNO: condtxt = "uno "; break; - case TRUE: condtxt = "true "; break; - case FALSE: condtxt = "false "; break; - } - os << getName() << " = fcmp " << fmath << condtxt << *a << ", " + case OEQ: return "oeq"; break; + case OGT: return "ogt"; break; + case OGE: return "oge"; break; + case OLT: return "olt"; break; + case OLE: return "ole"; break; + case ONE: return "one"; break; + case ORD: return "ord"; break; + case UEQ: return "ueq"; break; + case UGT: return "ugt"; break; + case UGE: return "uge"; break; + case ULT: return "ult"; break; + case ULE: return "ule"; break; + case UNE: return "une"; break; + case UNO: return "uno"; break; + case TRUE: return "true"; break; + case FALSE: return "false"; break; + } + UNREACHABLE(); +} + +void FCmp::print(ostream &os) const { + os << getName() << " = fcmp " << fmath << getCondName() << " " << *a << ", " << b->getName(); if (signaling) os << ", signaling"; diff --git a/ir/instr.h b/ir/instr.h index 57fd75e50..072259244 100644 --- a/ir/instr.h +++ b/ir/instr.h @@ -82,6 +82,7 @@ class FpBinOp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getOpName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; @@ -143,6 +144,7 @@ class FpUnaryOp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getOpName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; @@ -225,6 +227,7 @@ class FpTernaryOp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getOpName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; @@ -249,6 +252,7 @@ class TestOp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getOpName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; @@ -307,6 +311,7 @@ class FpConversionOp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getOpName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; @@ -437,6 +442,7 @@ class FCmp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; + const char* getCondName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; From 263f62c8656fc8b6f2bd19e9dded65389e9a5bbe Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 17 Jun 2024 17:41:08 +0200 Subject: [PATCH 02/28] Add --uf-float command line option --- llvm_util/cmd_args_def.h | 2 ++ llvm_util/cmd_args_list.h | 5 +++++ util/config.cpp | 1 + util/config.h | 7 +++++++ 4 files changed, 15 insertions(+) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index 5a252aca4..4a85b651c 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -29,6 +29,8 @@ if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) { config::disable_poison_input = true; } +config::fp_mapping_mode = opt_uf_float ? config::FpMappingMode::UninterpretedFunctions : config::FpMappingMode::FloatingPoint; + func_names.insert(opt_funcs.begin(), opt_funcs.end()); if (!report_dir_created && !opt_report_dir.empty()) { diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index b732ec92a..0ca0d5786 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -185,4 +185,9 @@ llvm::cl::opt opt_disallow_ub_exploitation( llvm::cl::desc("Disallow UB exploitation by optimizations (default=allow)"), llvm::cl::init(false), llvm::cl::cat(alive_cmdargs)); +llvm::cl::opt opt_uf_float( + LLVM_ARGS_PREFIX "uf-float", + llvm::cl::desc("Approximate floating point operations as uninterpreted functions"), + llvm::cl::init(false), llvm::cl::cat(alive_cmdargs)); + } diff --git a/util/config.cpp b/util/config.cpp index 82ab5f66a..d2ca40877 100644 --- a/util/config.cpp +++ b/util/config.cpp @@ -23,6 +23,7 @@ unsigned src_unroll_cnt = 0; unsigned tgt_unroll_cnt = 0; unsigned max_offset_bits = 64; unsigned max_sizet_bits = 64; +FpMappingMode fp_mapping_mode = FpMappingMode::FloatingPoint; ostream &dbg() { return *debug_os; diff --git a/util/config.h b/util/config.h index 57f58c888..e5a30a416 100644 --- a/util/config.h +++ b/util/config.h @@ -44,6 +44,13 @@ extern unsigned max_offset_bits; // size and size of pointers (not to be confused with program pointer size). extern unsigned max_sizet_bits; +enum FpMappingMode { + FloatingPoint, + UninterpretedFunctions +}; + +extern FpMappingMode fp_mapping_mode; + std::ostream &dbg(); void set_debug(std::ostream &os); From d67f7aa25c0eb0a6adbea810fcac56a31d748249 Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 17 Jun 2024 18:27:26 +0200 Subject: [PATCH 03/28] Map floating point operations to uninterpreted functions --- ir/instr.cpp | 454 +++++++++++++++++++++++++++--------------------- util/config.cpp | 4 + util/config.h | 1 + 3 files changed, 263 insertions(+), 196 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 7a301d4df..6a232a485 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -843,74 +843,83 @@ StateValue FpBinOp::toSMT(State &s) const { function fn; bool bitwise = false; - switch (op) { - case FAdd: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fadd(b, rm); + if (config::is_uf_float()) { + fn = [&](const expr &a, const expr &b, const expr &rm) { + s.doesApproximation("uf_float", true); + ostringstream os; + os << getOpName() << "." << getType(); + return expr::mkUF(os.str(), {a, b}, a); }; - break; + } else { + switch (op) { + case FAdd: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fadd(b, rm); + }; + break; - case FSub: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fsub(b, rm); - }; - break; + case FSub: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fsub(b, rm); + }; + break; - case FMul: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fmul(b, rm); - }; - break; + case FMul: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fmul(b, rm); + }; + break; - case FDiv: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fdiv(b, rm); - }; - break; + case FDiv: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fdiv(b, rm); + }; + break; - case FRem: - fn = [&](const expr &a, const expr &b, const expr &rm) { - // TODO; Z3 has no support for LLVM's frem which is actually an fmod - auto val = a.frem(b); - s.doesApproximation("frem", val); - return val; - }; - break; + case FRem: + fn = [&](const expr &a, const expr &b, const expr &rm) { + // TODO; Z3 has no support for LLVM's frem which is actually an fmod + auto val = a.frem(b); + s.doesApproximation("frem", val); + return val; + }; + break; - case FMin: - case FMax: - fn = [&](const expr &a, const expr &b, const expr &rm) { - expr ndet = s.getFreshNondetVar("maxminnondet", true); - expr cmp = op == FMin ? a.fole(b) : a.foge(b); - return expr::mkIf(a.isNaN(), b, - expr::mkIf(b.isNaN(), a, - expr::mkIf(a.foeq(b), - expr::mkIf(ndet, a, b), - expr::mkIf(cmp, a, b)))); - }; - break; + case FMin: + case FMax: + fn = [&](const expr &a, const expr &b, const expr &rm) { + expr ndet = s.getFreshNondetVar("maxminnondet", true); + expr cmp = op == FMin ? a.fole(b) : a.foge(b); + return expr::mkIf(a.isNaN(), b, + expr::mkIf(b.isNaN(), a, + expr::mkIf(a.foeq(b), + expr::mkIf(ndet, a, b), + expr::mkIf(cmp, a, b)))); + }; + break; - case FMinimum: - case FMaximum: - fn = [&](const expr &a, const expr &b, const expr &rm) { - expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a); - expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b); - expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative()) - : (a.isFPNegative() && b.isFPNegative()); - expr e = expr::mkIf(a.isFPZero() && b.isFPZero(), - expr::mkIf(neg_cond, zneg, zpos), - expr::mkIf(cmp, a, b)); - - return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e)); - }; - break; + case FMinimum: + case FMaximum: + fn = [&](const expr &a, const expr &b, const expr &rm) { + expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a); + expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b); + expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative()) + : (a.isFPNegative() && b.isFPNegative()); + expr e = expr::mkIf(a.isFPZero() && b.isFPZero(), + expr::mkIf(neg_cond, zneg, zpos), + expr::mkIf(cmp, a, b)); + + return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e)); + }; + break; - case CopySign: - bitwise = true; - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.copysign(b); - }; - break; + case CopySign: + bitwise = true; + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.copysign(b); + }; + break; + } } auto scalar = [&](const auto &a, const auto &b, const Type &ty) { @@ -1123,44 +1132,53 @@ void FpUnaryOp::print(ostream &os) const { } StateValue FpUnaryOp::toSMT(State &s) const { - expr (*fn)(const expr&, const expr&) = nullptr; + function fn = nullptr; bool bitwise = false; - switch (op) { - case FAbs: - bitwise = true; - fn = [](const expr &v, const expr &rm) { return v.fabs(); }; - break; - case FNeg: - bitwise = true; - fn = [](const expr &v, const expr &rm) { return v.fneg(); }; - break; - case Canonicalize: - fn = [](const expr &v, const expr &rm) { return v; }; - break; - case Ceil: - fn = [](const expr &v, const expr &rm) { return v.ceil(); }; - break; - case Floor: - fn = [](const expr &v, const expr &rm) { return v.floor(); }; - break; - case RInt: - case NearbyInt: - // TODO: they differ in exception behavior - fn = [](const expr &v, const expr &rm) { return v.round(rm); }; - break; - case Round: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rna()); }; - break; - case RoundEven: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rne()); }; - break; - case Trunc: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rtz()); }; - break; - case Sqrt: - fn = [](const expr &v, const expr &rm) { return v.sqrt(rm); }; - break; + if (config::is_uf_float()) { + fn = [&](const expr &v, const expr &rm) { + s.doesApproximation("uf_float", true); + ostringstream os; + os << getOpName() << "." << getType(); + return expr::mkUF(os.str(), {v}, v); + }; + } else { + switch (op) { + case FAbs: + bitwise = true; + fn = [](const expr &v, const expr &rm) { return v.fabs(); }; + break; + case FNeg: + bitwise = true; + fn = [](const expr &v, const expr &rm) { return v.fneg(); }; + break; + case Canonicalize: + fn = [](const expr &v, const expr &rm) { return v; }; + break; + case Ceil: + fn = [](const expr &v, const expr &rm) { return v.ceil(); }; + break; + case Floor: + fn = [](const expr &v, const expr &rm) { return v.floor(); }; + break; + case RInt: + case NearbyInt: + // TODO: they differ in exception behavior + fn = [](const expr &v, const expr &rm) { return v.round(rm); }; + break; + case Round: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rna()); }; + break; + case RoundEven: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rne()); }; + break; + case Trunc: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rtz()); }; + break; + case Sqrt: + fn = [](const expr &v, const expr &rm) { return v.sqrt(rm); }; + break; + } } auto scalar = [&](const StateValue &v, const Type &ty) { @@ -1424,18 +1442,27 @@ void FpTernaryOp::print(ostream &os) const { StateValue FpTernaryOp::toSMT(State &s) const { function fn; - switch (op) { - case FMA: - fn = [](const expr &a, const expr &b, const expr &c, const expr &rm) { - return expr::fma(a, b, c, rm); - }; - break; - case MulAdd: + if (config::is_uf_float()) { fn = [&](const expr &a, const expr &b, const expr &c, const expr &rm) { - expr var = s.getFreshNondetVar("nondet", expr(false)); - return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm)); + s.doesApproximation("uf_float", true); + ostringstream os; + os << getOpName() << "." << getType(); + return expr::mkUF(os.str(), {a, b, c}, a); }; - break; + } else { + switch (op) { + case FMA: + fn = [](const expr &a, const expr &b, const expr &c, const expr &rm) { + return expr::fma(a, b, c, rm); + }; + break; + case MulAdd: + fn = [&](const expr &a, const expr &b, const expr &c, const expr &rm) { + expr var = s.getFreshNondetVar("nondet", expr(false)); + return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm)); + }; + break; + } } auto scalar = [&](const StateValue &a, const StateValue &b, @@ -1508,14 +1535,23 @@ StateValue TestOp::toSMT(State &s) const { auto &b = s[*rhs]; function fn; - switch (op) { - case Is_FPClass: + if (config::is_uf_float()) { fn = [&](const expr &v, const Type &ty) -> expr { - uint64_t mask; - ENSURE(b.value.isUInt(mask) && b.non_poison.isTrue()); - return isfpclass(v, ty, mask).toBVBool(); + s.doesApproximation("uf_float", true); + ostringstream os; + os << getOpName() << "." << lhs->getType(); + return expr::mkUF(os.str(), {v}, expr::mkUInt(0, 1)); }; - break; + } else { + switch (op) { + case Is_FPClass: + fn = [&](const expr &v, const Type &ty) -> expr { + uint64_t mask; + ENSURE(b.value.isUInt(mask) && b.non_poison.isTrue()); + return isfpclass(v, ty, mask).toBVBool(); + }; + break; + } } auto scalar = [&](const StateValue &v, const Type &ty) -> StateValue { @@ -1770,72 +1806,82 @@ StateValue FpConversionOp::toSMT(State &s) const { auto &v = s[*val]; function fn; - switch (op) { - case SIntToFP: - fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { - return { val.sint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), - true }; + if (config::is_uf_float()) { + fn = [&](auto &v, auto &to_type, auto &rm) -> StateValue { + s.doesApproximation("uf_float", true); + ostringstream os; + os << getOpName() << "." << val->getType() << ".to." << to_type; + expr range = to_type.getAsFloatType()->getDummyFloat(); // TODO + return { expr::mkUF(os.str(), {v}, range), true }; }; - break; - case UIntToFP: - fn = [&](auto &val, auto &to_type, auto &rm) -> StateValue { - return {val.uint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), - (flags & NNEG) ? !val.isNegative() : true}; - }; - break; - case FPToSInt: - case LRInt: - case LRound: - fn = [&](auto &val, auto &to_type, auto &rm_in) -> StateValue { - expr rm; - bool is_poison = false; - switch (op) { - case FPToSInt: - rm = expr::rtz(); - is_poison = true; - break; - case LRInt: - rm = rm_in; - break; - case LRound: - rm = expr::rna(); - break; - default: UNREACHABLE(); - } - expr bv = val.fp2sint(to_type.bits(), rm); - expr fp2 = bv.sint2fp(val, rm); - // -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert - expr val_rounded = val.round(rm); - expr overflow = val_rounded.isFPZero() || fp2 == val_rounded; - - expr np; - if (is_poison) { - np = std::move(overflow); - } else { - np = true; - bv = expr::mkIf(overflow, s.getFreshNondetVar("nondet", bv), bv); - } + } else { + switch (op) { + case SIntToFP: + fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { + return { val.sint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), + true }; + }; + break; + case UIntToFP: + fn = [&](auto &val, auto &to_type, auto &rm) -> StateValue { + return {val.uint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), + (flags & NNEG) ? !val.isNegative() : true}; + }; + break; + case FPToSInt: + case LRInt: + case LRound: + fn = [&](auto &val, auto &to_type, auto &rm_in) -> StateValue { + expr rm; + bool is_poison = false; + switch (op) { + case FPToSInt: + rm = expr::rtz(); + is_poison = true; + break; + case LRInt: + rm = rm_in; + break; + case LRound: + rm = expr::rna(); + break; + default: UNREACHABLE(); + } + expr bv = val.fp2sint(to_type.bits(), rm); + expr fp2 = bv.sint2fp(val, rm); + // -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert + expr val_rounded = val.round(rm); + expr overflow = val_rounded.isFPZero() || fp2 == val_rounded; + + expr np; + if (is_poison) { + np = std::move(overflow); + } else { + np = true; + bv = expr::mkIf(overflow, s.getFreshNondetVar("nondet", bv), bv); + } - return { std::move(bv), std::move(np) }; - }; - break; - case FPToUInt: - fn = [](auto &val, auto &to_type, auto &rm_) -> StateValue { - expr rm = expr::rtz(); - expr bv = val.fp2uint(to_type.bits(), rm); - expr fp2 = bv.uint2fp(val, rm); - // -0.xx must be converted to 0, not poison. - expr val_rounded = val.round(rm); - return { std::move(bv), val_rounded.isFPZero() || fp2 == val_rounded }; - }; - break; - case FPExt: - case FPTrunc: - fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { - return { val.float2Float(to_type.getAsFloatType()->getDummyFloat(), rm), - true }; - }; - break; + return { std::move(bv), std::move(np) }; + }; + break; + case FPToUInt: + fn = [](auto &val, auto &to_type, auto &rm_) -> StateValue { + expr rm = expr::rtz(); + expr bv = val.fp2uint(to_type.bits(), rm); + expr fp2 = bv.uint2fp(val, rm); + // -0.xx must be converted to 0, not poison. + expr val_rounded = val.round(rm); + return { std::move(bv), val_rounded.isFPZero() || fp2 == val_rounded }; + }; + break; + case FPExt: + case FPTrunc: + fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { + return { val.float2Float(to_type.getAsFloatType()->getDummyFloat(), rm), + true }; + }; + break; + } } auto scalar = [&](const StateValue &sv, const Type &from_type, @@ -2778,26 +2824,42 @@ StateValue FCmp::toSMT(State &s) const { auto &b_eval = s[*b]; auto fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { - auto cmp = [&](const expr &a, const expr &b, auto &rm) { - switch (cond) { - case OEQ: return a.foeq(b); - case OGT: return a.fogt(b); - case OGE: return a.foge(b); - case OLT: return a.folt(b); - case OLE: return a.fole(b); - case ONE: return a.fone(b); - case ORD: return a.ford(b); - case UEQ: return a.fueq(b); - case UGT: return a.fugt(b); - case UGE: return a.fuge(b); - case ULT: return a.fult(b); - case ULE: return a.fule(b); - case UNE: return a.fune(b); - case UNO: return a.funo(b); - case TRUE: return expr(true); - case FALSE: return expr(false); - } - }; + function cmp; + if (config::is_uf_float()) { + cmp = [&](const expr &a, const expr &b, auto &rm) { + switch (cond) { + case TRUE: return expr(true); + case FALSE: return expr(false); + default: { + s.doesApproximation("uf_float", true); + ostringstream os; + os << getCondName() << "." << this->a->getType(); + return expr::mkUF(os.str(), {a, b}, false); + } + } + }; + } else { + cmp = [&](const expr &a, const expr &b, auto &rm) { + switch (cond) { + case OEQ: return a.foeq(b); + case OGT: return a.fogt(b); + case OGE: return a.foge(b); + case OLT: return a.folt(b); + case OLE: return a.fole(b); + case ONE: return a.fone(b); + case ORD: return a.ford(b); + case UEQ: return a.fueq(b); + case UGT: return a.fugt(b); + case UGE: return a.fuge(b); + case ULT: return a.fult(b); + case ULE: return a.fule(b); + case UNE: return a.fune(b); + case UNO: return a.funo(b); + case TRUE: return expr(true); + case FALSE: return expr(false); + } + }; + } auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, cmp, ty, fmath, {}, false, true); return { val.toBVBool(), std::move(np) }; diff --git a/util/config.cpp b/util/config.cpp index d2ca40877..78e417f24 100644 --- a/util/config.cpp +++ b/util/config.cpp @@ -33,4 +33,8 @@ void set_debug(ostream &os) { debug_os = &os; } +bool is_uf_float() { + return fp_mapping_mode == FpMappingMode::UninterpretedFunctions; +} + } diff --git a/util/config.h b/util/config.h index e5a30a416..2170fa15e 100644 --- a/util/config.h +++ b/util/config.h @@ -53,5 +53,6 @@ extern FpMappingMode fp_mapping_mode; std::ostream &dbg(); void set_debug(std::ostream &os); +bool is_uf_float(); } From e5661c275d869b60ec92ebd3a05d10d3cc2a09f8 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 11:55:16 +0200 Subject: [PATCH 04/28] Handle poison values in FpBinOp --- ir/instr.cpp | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 6a232a485..84e56f31c 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -841,14 +841,26 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, StateValue FpBinOp::toSMT(State &s) const { function fn; + function scalar; bool bitwise = false; if (config::is_uf_float()) { - fn = [&](const expr &a, const expr &b, const expr &rm) { + scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); + ostringstream os; os << getOpName() << "." << getType(); - return expr::mkUF(os.str(), {a, b}, a); + auto value = expr::mkUF(os.str(), {a.value, b.value}, a.value); + + AndExpr non_poison; + non_poison.add(a.non_poison); + non_poison.add(b.non_poison); + if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { + os << ".np"; + non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false)); + } + + return { move(value), non_poison() }; }; } else { switch (op) { @@ -920,13 +932,13 @@ StateValue FpBinOp::toSMT(State &s) const { }; break; } - } - auto scalar = [&](const auto &a, const auto &b, const Type &ty) { - return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - [&](auto &a, auto &b, auto &rm){ return fn(a, b, rm); }, - ty, fmath, rm, bitwise); - }; + scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) { + return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + [&](auto &a, auto &b, auto &rm){ return fn(a, b, rm); }, + ty, fmath, rm, bitwise); + }; + } auto &a = s[*lhs]; auto &b = s[*rhs]; From 4dd1cab10f56797af4c5a9ede5afb5b907c004cc Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 13:15:35 +0200 Subject: [PATCH 05/28] Encode commutativity --- ir/instr.cpp | 25 +++++++++++++++++++++++-- ir/instr.h | 1 + 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 84e56f31c..7a9823acf 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -645,6 +645,20 @@ const char* FpBinOp::getOpName() const { UNREACHABLE(); } +bool FpBinOp::isCommutative() const { + switch (op) { + case FAdd: + case FMin: + case FMax: + case FMinimum: + case FMaximum: + return true; + default: + return false; + } + UNREACHABLE(); +} + void FpBinOp::print(ostream &os) const { os << getName() << " = " << getOpName() << " " << fmath << *lhs << ", " << rhs->getName(); if (!rm.isDefault()) @@ -847,17 +861,24 @@ StateValue FpBinOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); - + ostringstream os; os << getOpName() << "." << getType(); auto value = expr::mkUF(os.str(), {a.value, b.value}, a.value); + if (isCommutative()) { + value = value & expr::mkUF(os.str(), {b.value, a.value}, a.value); + } AndExpr non_poison; non_poison.add(a.non_poison); non_poison.add(b.non_poison); if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false)); + auto poison_uf = expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false); + if (isCommutative()) { + poison_uf &= expr::mkUF(os.str(), {b.non_poison, a.non_poison}, false); + } + non_poison.add(poison_uf); } return { move(value), non_poison() }; diff --git a/ir/instr.h b/ir/instr.h index 072259244..75826512c 100644 --- a/ir/instr.h +++ b/ir/instr.h @@ -83,6 +83,7 @@ class FpBinOp final : public Instr { bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; const char* getOpName() const; + bool isCommutative() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; From 14d14d440c63dd90990963614e15be17145203fc Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 14:01:50 +0200 Subject: [PATCH 06/28] Handle poison --- ir/instr.cpp | 211 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 130 insertions(+), 81 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 7a9823acf..c9e228e11 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -1166,14 +1166,24 @@ void FpUnaryOp::print(ostream &os) const { StateValue FpUnaryOp::toSMT(State &s) const { function fn = nullptr; + function scalar = nullptr; bool bitwise = false; if (config::is_uf_float()) { - fn = [&](const expr &v, const expr &rm) { + scalar = [&](const StateValue &v, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); + ostringstream os; os << getOpName() << "." << getType(); - return expr::mkUF(os.str(), {v}, v); + auto value = expr::mkUF(os.str(), {v.value}, v.value); + + auto non_poison = v.non_poison; + if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { + os << ".np"; + non_poison &= expr::mkUF(os.str(), {v.non_poison}, false); + } + + return {move(value), move(non_poison)}; }; } else { switch (op) { @@ -1212,13 +1222,13 @@ StateValue FpUnaryOp::toSMT(State &s) const { fn = [](const expr &v, const expr &rm) { return v.sqrt(rm); }; break; } - } - auto scalar = [&](const StateValue &v, const Type &ty) { - return fm_poison(s, v.value, v.non_poison, - [fn](auto &v, auto &rm) {return fn(v, rm);}, ty, fmath, rm, - bitwise, false); - }; + scalar = [&](const StateValue &v, const Type &ty) { + return fm_poison(s, v.value, v.non_poison, + [fn](auto &v, auto &rm) {return fn(v, rm);}, ty, fmath, rm, + bitwise, false); + }; + } auto &v = s[*val]; @@ -1474,13 +1484,27 @@ void FpTernaryOp::print(ostream &os) const { StateValue FpTernaryOp::toSMT(State &s) const { function fn; + function scalar; if (config::is_uf_float()) { - fn = [&](const expr &a, const expr &b, const expr &c, const expr &rm) { + scalar = [&](const StateValue &a, const StateValue &b, + const StateValue &c, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); + ostringstream os; os << getOpName() << "." << getType(); - return expr::mkUF(os.str(), {a, b, c}, a); + auto value = expr::mkUF(os.str(), {a.value, b.value, c.value}, a.value); + + AndExpr non_poison; + non_poison.add(a.non_poison); + non_poison.add(b.non_poison); + non_poison.add(c.non_poison); + if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { + os << ".np"; + non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison, c.non_poison}, false)); + } + + return {move(value), non_poison()}; }; } else { switch (op) { @@ -1496,14 +1520,14 @@ StateValue FpTernaryOp::toSMT(State &s) const { }; break; } + + scalar = [&](const StateValue &a, const StateValue &b, + const StateValue &c, const Type &ty) { + return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + c.value, c.non_poison, fn, ty, fmath, rm, false); + }; } - auto scalar = [&](const StateValue &a, const StateValue &b, - const StateValue &c, const Type &ty) { - return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - c.value, c.non_poison, fn, ty, fmath, rm, false); - }; - auto &av = s[*a]; auto &bv = s[*b]; auto &cv = s[*c]; @@ -1838,14 +1862,26 @@ void FpConversionOp::print(ostream &os) const { StateValue FpConversionOp::toSMT(State &s) const { auto &v = s[*val]; function fn; + function scalar; if (config::is_uf_float()) { - fn = [&](auto &v, auto &to_type, auto &rm) -> StateValue { + scalar = [&](const StateValue &sv, const Type &from_type, + const Type &to_type) -> StateValue { s.doesApproximation("uf_float", true); + ostringstream os; - os << getOpName() << "." << val->getType() << ".to." << to_type; - expr range = to_type.getAsFloatType()->getDummyFloat(); // TODO - return { expr::mkUF(os.str(), {v}, range), true }; + os << getOpName() << "." << from_type << ".to." << to_type; + expr range = to_type.getDummyValue(true).value; + auto value = expr::mkUF(os.str(), {sv.value}, range); + + AndExpr non_poison; + non_poison.add(sv.non_poison); + if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && op != FPTrunc && op != FPExt) { + os << ".np"; + non_poison.add(expr::mkUF(os.str(), {v.non_poison}, false)); + } + + return { move(value), non_poison() }; }; } else { switch (op) { @@ -1915,32 +1951,32 @@ StateValue FpConversionOp::toSMT(State &s) const { }; break; } - } - auto scalar = [&](const StateValue &sv, const Type &from_type, - const Type &to_type) -> StateValue { - auto val = sv.value; + scalar = [&](const StateValue &sv, const Type &from_type, + const Type &to_type) -> StateValue { + auto val = sv.value; - if (from_type.isFloatType()) { - auto ty = from_type.getAsFloatType(); - val = ty->getFloat(val); - } + if (from_type.isFloatType()) { + auto ty = from_type.getAsFloatType(); + val = ty->getFloat(val); + } - function fn_rm - = [&](auto &rm) { return fn(val, to_type, rm); }; - AndExpr np; - np.add(sv.non_poison); + function fn_rm + = [&](auto &rm) { return fn(val, to_type, rm); }; + AndExpr np; + np.add(sv.non_poison); - StateValue ret = to_type.isFloatType() ? round_value(s, rm, np, fn_rm) - : fn(val, to_type, rm.toSMT()); - np.add(std::move(ret.non_poison)); + StateValue ret = to_type.isFloatType() ? round_value(s, rm, np, fn_rm) + : fn(val, to_type, rm.toSMT()); + np.add(std::move(ret.non_poison)); - return { to_type.isFloatType() - ? to_type.getAsFloatType() - ->fromFloat(s, ret.value, from_type, from_type.isFloatType(), - sv.value) - : std::move(ret.value), np()}; - }; + return { to_type.isFloatType() + ? to_type.getAsFloatType() + ->fromFloat(s, ret.value, from_type, from_type.isFloatType(), + sv.value) + : std::move(ret.value), np()}; + }; + } if (getType().isVectorType()) { vector vals; @@ -2856,47 +2892,60 @@ StateValue FCmp::toSMT(State &s) const { auto &a_eval = s[*a]; auto &b_eval = s[*b]; - auto fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { - function cmp; - if (config::is_uf_float()) { - cmp = [&](const expr &a, const expr &b, auto &rm) { - switch (cond) { - case TRUE: return expr(true); - case FALSE: return expr(false); - default: { - s.doesApproximation("uf_float", true); - ostringstream os; - os << getCondName() << "." << this->a->getType(); - return expr::mkUF(os.str(), {a, b}, false); - } - } - }; - } else { - cmp = [&](const expr &a, const expr &b, auto &rm) { - switch (cond) { - case OEQ: return a.foeq(b); - case OGT: return a.fogt(b); - case OGE: return a.foge(b); - case OLT: return a.folt(b); - case OLE: return a.fole(b); - case ONE: return a.fone(b); - case ORD: return a.ford(b); - case UEQ: return a.fueq(b); - case UGT: return a.fugt(b); - case UGE: return a.fuge(b); - case ULT: return a.fult(b); - case ULE: return a.fule(b); - case UNE: return a.fune(b); - case UNO: return a.funo(b); - case TRUE: return expr(true); - case FALSE: return expr(false); + function cmp; + function fn; + if (config::is_uf_float()) { + fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + switch (cond) { + case TRUE: return {true, true}; + case FALSE: return {false, true}; + default: { + s.doesApproximation("uf_float", true); + + ostringstream os; + os << getCondName() << "." << this->a->getType(); + auto value = expr::mkUF(os.str(), {a.value, b.value}, false); + + AndExpr non_poison; + non_poison.add(a.non_poison); + non_poison.add(b.non_poison); + if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { + os << ".np"; + non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false)); } - }; - } - auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - cmp, ty, fmath, {}, false, true); - return { val.toBVBool(), std::move(np) }; - }; + + return {move(value), non_poison()}; + } + } + }; + } else { + cmp = [&](const expr &a, const expr &b, auto &rm) { + switch (cond) { + case OEQ: return a.foeq(b); + case OGT: return a.fogt(b); + case OGE: return a.foge(b); + case OLT: return a.folt(b); + case OLE: return a.fole(b); + case ONE: return a.fone(b); + case ORD: return a.ford(b); + case UEQ: return a.fueq(b); + case UGT: return a.fugt(b); + case UGE: return a.fuge(b); + case ULT: return a.fult(b); + case ULE: return a.fule(b); + case UNE: return a.fune(b); + case UNO: return a.funo(b); + case TRUE: return expr(true); + case FALSE: return expr(false); + } + }; + + fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + cmp, ty, fmath, {}, false, true); + return { val.toBVBool(), std::move(np) }; + }; + } if (auto agg = a->getType().getAsAggregateType()) { vector vals; From d2fb02173dfaecd1c54ddd868c9e26e480776191 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 15:07:01 +0200 Subject: [PATCH 07/28] Fix return type for FCmp --- ir/instr.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index c9e228e11..be0387eda 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2904,7 +2904,7 @@ StateValue FCmp::toSMT(State &s) const { ostringstream os; os << getCondName() << "." << this->a->getType(); - auto value = expr::mkUF(os.str(), {a.value, b.value}, false); + auto value = expr::mkUF(os.str(), {a.value, b.value}, expr::mkUInt(0, 1)); AndExpr non_poison; non_poison.add(a.non_poison); From 233f6b539c5690172716617734555937227845c0 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 15:08:23 +0200 Subject: [PATCH 08/28] Use qualified call to std::move --- ir/instr.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index be0387eda..91d317b04 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -881,7 +881,7 @@ StateValue FpBinOp::toSMT(State &s) const { non_poison.add(poison_uf); } - return { move(value), non_poison() }; + return { std::move(value), non_poison() }; }; } else { switch (op) { @@ -1183,7 +1183,7 @@ StateValue FpUnaryOp::toSMT(State &s) const { non_poison &= expr::mkUF(os.str(), {v.non_poison}, false); } - return {move(value), move(non_poison)}; + return {std::move(value), std::move(non_poison)}; }; } else { switch (op) { @@ -1504,7 +1504,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison, c.non_poison}, false)); } - return {move(value), non_poison()}; + return {std::move(value), non_poison()}; }; } else { switch (op) { @@ -1881,7 +1881,7 @@ StateValue FpConversionOp::toSMT(State &s) const { non_poison.add(expr::mkUF(os.str(), {v.non_poison}, false)); } - return { move(value), non_poison() }; + return { std::move(value), non_poison() }; }; } else { switch (op) { @@ -2914,7 +2914,7 @@ StateValue FCmp::toSMT(State &s) const { non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false)); } - return {move(value), non_poison()}; + return {std::move(value), non_poison()}; } } }; From 4149c54d14b36b7bcae4ad3e58aa2025619cefc8 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 18 Jun 2024 15:45:52 +0200 Subject: [PATCH 09/28] Add tests --- .../alive-tv/uf-float/add-assoc-fail.srctgt.ll | 14 ++++++++++++++ tests/alive-tv/uf-float/add-comm.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/select.srctgt.ll | 17 +++++++++++++++++ 3 files changed, 42 insertions(+) create mode 100644 tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm.srctgt.ll create mode 100644 tests/alive-tv/uf-float/select.srctgt.ll diff --git a/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll new file mode 100644 index 000000000..33a3d5323 --- /dev/null +++ b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float +; ERROR: Couldn't prove the correctness of the transformation + +define float @src(float noundef %x, float noundef %y, float noundef %z) { + %a = fadd float %x, %y + %b = fadd float %a, %z + ret float %b +} + +define float @tgt(float noundef %x, float noundef %y, float noundef %z) { + %a = fadd float %y, %z + %b = fadd float %x, %a + ret float %b +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm.srctgt.ll b/tests/alive-tv/uf-float/add-comm.srctgt.ll new file mode 100644 index 000000000..7f9fa9728 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd float %y, %x + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/select.srctgt.ll b/tests/alive-tv/uf-float/select.srctgt.ll new file mode 100644 index 000000000..2dcc46005 --- /dev/null +++ b/tests/alive-tv/uf-float/select.srctgt.ll @@ -0,0 +1,17 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + %a = fsub float %y, %x + %b = fsub float %x, %y + %c = select i1 %cmp, float %a, float %b + ret float %c +} + +define float @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + %min = select i1 %cmp, float %x, float %y + %max = select i1 %cmp, float %y, float %x + %res = fsub float %max, %min + ret float %res +} \ No newline at end of file From aaf6b367ddd7159da16b1f7f7e029dd13db289db Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 19 Jun 2024 10:41:47 +0200 Subject: [PATCH 10/28] Use scalar type as suffix for UF --- ir/instr.cpp | 10 +++++----- tests/alive-tv/uf-float/vector-binop.srctgt.ll | 14 ++++++++++++++ tests/alive-tv/uf-float/vector-cmp.srctgt.ll | 14 ++++++++++++++ tests/alive-tv/uf-float/vector-unop.srctgt.ll | 13 +++++++++++++ 4 files changed, 46 insertions(+), 5 deletions(-) create mode 100644 tests/alive-tv/uf-float/vector-binop.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-cmp.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-unop.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index 91d317b04..a62157c12 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -863,7 +863,7 @@ StateValue FpBinOp::toSMT(State &s) const { s.doesApproximation("uf_float", true); ostringstream os; - os << getOpName() << "." << getType(); + os << getOpName() << "." << ty; auto value = expr::mkUF(os.str(), {a.value, b.value}, a.value); if (isCommutative()) { value = value & expr::mkUF(os.str(), {b.value, a.value}, a.value); @@ -1174,7 +1174,7 @@ StateValue FpUnaryOp::toSMT(State &s) const { s.doesApproximation("uf_float", true); ostringstream os; - os << getOpName() << "." << getType(); + os << getOpName() << "." << ty; auto value = expr::mkUF(os.str(), {v.value}, v.value); auto non_poison = v.non_poison; @@ -1492,7 +1492,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { s.doesApproximation("uf_float", true); ostringstream os; - os << getOpName() << "." << getType(); + os << getOpName() << "." << ty; auto value = expr::mkUF(os.str(), {a.value, b.value, c.value}, a.value); AndExpr non_poison; @@ -1596,7 +1596,7 @@ StateValue TestOp::toSMT(State &s) const { fn = [&](const expr &v, const Type &ty) -> expr { s.doesApproximation("uf_float", true); ostringstream os; - os << getOpName() << "." << lhs->getType(); + os << getOpName() << "." << ty; return expr::mkUF(os.str(), {v}, expr::mkUInt(0, 1)); }; } else { @@ -2903,7 +2903,7 @@ StateValue FCmp::toSMT(State &s) const { s.doesApproximation("uf_float", true); ostringstream os; - os << getCondName() << "." << this->a->getType(); + os << getCondName() << "." << ty; auto value = expr::mkUF(os.str(), {a.value, b.value}, expr::mkUInt(0, 1)); AndExpr non_poison; diff --git a/tests/alive-tv/uf-float/vector-binop.srctgt.ll b/tests/alive-tv/uf-float/vector-binop.srctgt.ll new file mode 100644 index 000000000..98c599077 --- /dev/null +++ b/tests/alive-tv/uf-float/vector-binop.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = insertelement <2 x float> poison, float %y, i32 0 + %vec3 = fadd <2 x float> %vec1, %vec2 + %sum = extractelement <2 x float> %vec3, i32 0 + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-cmp.srctgt.ll b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll new file mode 100644 index 000000000..ddc62145b --- /dev/null +++ b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %res = fcmp olt float %x, %y + ret i1 %res +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = insertelement <2 x float> poison, float %y, i32 0 + %vec3 = fcmp olt <2 x float> %vec1, %vec2 + %res = extractelement <2 x i1> %vec3, i32 0 + ret i1 %res +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-unop.srctgt.ll b/tests/alive-tv/uf-float/vector-unop.srctgt.ll new file mode 100644 index 000000000..09e70791d --- /dev/null +++ b/tests/alive-tv/uf-float/vector-unop.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + %res = fneg float %x + ret float %res +} + +define float @tgt(float noundef %x) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = fneg <2 x float> %vec1 + %res = extractelement <2 x float> %vec2, i32 0 + ret float %res +} \ No newline at end of file From 9c2384d2748f6261c38736faa95098f251554b58 Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 19 Jun 2024 11:42:52 +0200 Subject: [PATCH 11/28] Encode all fcmp conditions using oeq, ueq, olt, ult, ord --- ir/instr.cpp | 43 +++++++++++++++++-- tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll | 11 +++++ tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll | 12 ++++++ tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll | 11 +++++ tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll | 12 ++++++ .../uf-float/cmp-olt-ult-fail.srctgt.ll | 12 ++++++ tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll | 12 ++++++ 7 files changed, 110 insertions(+), 3 deletions(-) create mode 100644 tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index a62157c12..81cb23942 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2900,18 +2900,55 @@ StateValue FCmp::toSMT(State &s) const { case TRUE: return {true, true}; case FALSE: return {false, true}; default: { + // All conditions are encoded using only 5 uninterpreted functions: + // oeq, ueq, olt, ult, ord + s.doesApproximation("uf_float", true); + StateValue lhs = a; + StateValue rhs = b; + + const char *name = nullptr; + bool negate = false; + bool commutative = false; + switch (cond) { + case OEQ: name = "oeq"; commutative = true; break; + case OGT: name = "olt"; std::swap(lhs, rhs); break; + case OGE: name = "ult"; negate = true; break; + case OLT: name = "olt"; break; + case OLE: name = "ult"; std::swap(lhs, rhs); negate = true; break; + case ONE: name = "ueq"; negate = true; commutative = true; break; + case ORD: name = "ord"; commutative = true; break; + case UEQ: name = "ueq"; commutative = true; break; + case UGT: name = "olt"; std::swap(lhs, rhs); break; + case UGE: name = "ult"; negate = true; break; + case ULT: name = "ult"; break; + case ULE: name = "olt"; negate = true; std::swap(lhs, rhs); break; + case UNE: name = "oeq"; negate = true; commutative = true; break; + case UNO: name = "ord"; negate = true; commutative = true; break; + default: UNREACHABLE(); + } + ostringstream os; - os << getCondName() << "." << ty; - auto value = expr::mkUF(os.str(), {a.value, b.value}, expr::mkUInt(0, 1)); + os << name << "." << ty; + auto value = expr::mkUF(os.str(), {lhs.value, rhs.value}, expr::mkUInt(0, 1)); + if (commutative) { + value = value & expr::mkUF(os.str(), {rhs.value, lhs.value}, expr::mkUInt(0, 1)); + } + if (negate) { + value = ~value; + } AndExpr non_poison; non_poison.add(a.non_poison); non_poison.add(b.non_poison); if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false)); + auto poison_uf = expr::mkUF(os.str(), {lhs.non_poison, rhs.non_poison}, false); + if (commutative) { + poison_uf &= expr::mkUF(os.str(), {rhs.non_poison, lhs.non_poison}, false); + } + non_poison.add(poison_uf); } return {std::move(value), non_poison()}; diff --git a/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll new file mode 100644 index 000000000..573ade1a4 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %y, %x + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll new file mode 100644 index 000000000..779b655e0 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp une float %x, %y + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll new file mode 100644 index 000000000..4b3ccdbbb --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ogt float %y, %x + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll new file mode 100644 index 000000000..ad124452e --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ule float %y, %x + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll new file mode 100644 index 000000000..b9f92c905 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float +; ERROR: Couldn't prove the correctness of the transformation + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ult float %x, %y + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll new file mode 100644 index 000000000..9e0d7a0fd --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp ord float %x, %y + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp uno float %y, %x + ret i1 %cmp +} \ No newline at end of file From 35247eae66fd292430450eeb43b9bf4d1e322f2b Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 19 Jun 2024 11:46:16 +0200 Subject: [PATCH 12/28] Fix poison for fast math --- ir/instr.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 81cb23942..332f88a69 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -874,9 +874,9 @@ StateValue FpBinOp::toSMT(State &s) const { non_poison.add(b.non_poison); if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - auto poison_uf = expr::mkUF(os.str(), {a.non_poison, b.non_poison}, false); + auto poison_uf = expr::mkUF(os.str(), {a.value, b.value}, false); if (isCommutative()) { - poison_uf &= expr::mkUF(os.str(), {b.non_poison, a.non_poison}, false); + poison_uf &= expr::mkUF(os.str(), {b.value, a.value}, false); } non_poison.add(poison_uf); } @@ -1180,7 +1180,7 @@ StateValue FpUnaryOp::toSMT(State &s) const { auto non_poison = v.non_poison; if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - non_poison &= expr::mkUF(os.str(), {v.non_poison}, false); + non_poison &= expr::mkUF(os.str(), {v.value}, false); } return {std::move(value), std::move(non_poison)}; @@ -1501,7 +1501,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { non_poison.add(c.non_poison); if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {a.non_poison, b.non_poison, c.non_poison}, false)); + non_poison.add(expr::mkUF(os.str(), {a.value, b.value, c.value}, false)); } return {std::move(value), non_poison()}; @@ -1878,7 +1878,7 @@ StateValue FpConversionOp::toSMT(State &s) const { non_poison.add(sv.non_poison); if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && op != FPTrunc && op != FPExt) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {v.non_poison}, false)); + non_poison.add(expr::mkUF(os.str(), {v.value}, false)); } return { std::move(value), non_poison() }; @@ -2944,9 +2944,9 @@ StateValue FCmp::toSMT(State &s) const { non_poison.add(b.non_poison); if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { os << ".np"; - auto poison_uf = expr::mkUF(os.str(), {lhs.non_poison, rhs.non_poison}, false); + auto poison_uf = expr::mkUF(os.str(), {lhs.value, rhs.value}, false); if (commutative) { - poison_uf &= expr::mkUF(os.str(), {rhs.non_poison, lhs.non_poison}, false); + poison_uf &= expr::mkUF(os.str(), {rhs.value, lhs.value}, false); } non_poison.add(poison_uf); } From 0ccb8f4810e14dec69eb78ee12af5f47c46972b2 Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 1 Jul 2024 19:27:49 +0200 Subject: [PATCH 13/28] Add more tests --- tests/alive-tv/uf-float/add-comm-double.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm-half.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/load-bitcast.srctgt.ll | 13 +++++++++++++ tests/alive-tv/uf-float/load-store.srctgt.ll | 12 ++++++++++++ 5 files changed, 58 insertions(+) create mode 100644 tests/alive-tv/uf-float/add-comm-double.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-half.srctgt.ll create mode 100644 tests/alive-tv/uf-float/load-bitcast.srctgt.ll create mode 100644 tests/alive-tv/uf-float/load-store.srctgt.ll diff --git a/tests/alive-tv/uf-float/add-comm-double.srctgt.ll b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll new file mode 100644 index 000000000..4981661a4 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define double @src(double noundef %x, double noundef %y) { + %sum = fadd double %x, %y + ret double %sum +} + +define double @tgt(double noundef %x, double noundef %y) { + %sum = fadd double %y, %x + ret double %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll new file mode 100644 index 000000000..deb6c3213 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define fp128 @src(fp128 noundef %x, fp128 noundef %y) { + %sum = fadd fp128 %x, %y + ret fp128 %sum +} + +define fp128 @tgt(fp128 noundef %x, fp128 noundef %y) { + %sum = fadd fp128 %y, %x + ret fp128 %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-half.srctgt.ll b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll new file mode 100644 index 000000000..731eae0d5 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define half @src(half noundef %x, half noundef %y) { + %sum = fadd half %x, %y + ret half %sum +} + +define half @tgt(half noundef %x, half noundef %y) { + %sum = fadd half %y, %x + ret half %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/load-bitcast.srctgt.ll b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll new file mode 100644 index 000000000..8ec87e261 --- /dev/null +++ b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --uf-float + +define i32 @src(float noundef %x) { + %a = bitcast float %x to i32 + ret i32 %a +} + +define i32 @tgt(float noundef %x) { + %a = alloca float + store float %x, ptr %a + %b = load i32, ptr %a + ret i32 %b +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/load-store.srctgt.ll b/tests/alive-tv/uf-float/load-store.srctgt.ll new file mode 100644 index 000000000..1c397c404 --- /dev/null +++ b/tests/alive-tv/uf-float/load-store.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + ret float %x +} + +define float @tgt(float noundef %x) { + %a = alloca float + store float %x, ptr %a + %b = load float, ptr %a + ret float %b +} \ No newline at end of file From 736ff33cb67c290b7478ec2d4e06a52eb220843f Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 1 Jul 2024 19:32:33 +0200 Subject: [PATCH 14/28] Rename FpMappingMode to FpEncodingMode --- llvm_util/cmd_args_def.h | 2 +- util/config.cpp | 4 ++-- util/config.h | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index 4a85b651c..c8202d31c 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -29,7 +29,7 @@ if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) { config::disable_poison_input = true; } -config::fp_mapping_mode = opt_uf_float ? config::FpMappingMode::UninterpretedFunctions : config::FpMappingMode::FloatingPoint; +config::fp_encoding_mode = opt_uf_float ? config::FpEncodingMode::UninterpretedFunctions : config::FpEncodingMode::FloatingPoint; func_names.insert(opt_funcs.begin(), opt_funcs.end()); diff --git a/util/config.cpp b/util/config.cpp index 78e417f24..35b4dcb78 100644 --- a/util/config.cpp +++ b/util/config.cpp @@ -23,7 +23,7 @@ unsigned src_unroll_cnt = 0; unsigned tgt_unroll_cnt = 0; unsigned max_offset_bits = 64; unsigned max_sizet_bits = 64; -FpMappingMode fp_mapping_mode = FpMappingMode::FloatingPoint; +FpEncodingMode fp_encoding_mode = FpEncodingMode::FloatingPoint; ostream &dbg() { return *debug_os; @@ -34,7 +34,7 @@ void set_debug(ostream &os) { } bool is_uf_float() { - return fp_mapping_mode == FpMappingMode::UninterpretedFunctions; + return fp_encoding_mode == FpEncodingMode::UninterpretedFunctions; } } diff --git a/util/config.h b/util/config.h index 2170fa15e..3a6488e15 100644 --- a/util/config.h +++ b/util/config.h @@ -44,12 +44,12 @@ extern unsigned max_offset_bits; // size and size of pointers (not to be confused with program pointer size). extern unsigned max_sizet_bits; -enum FpMappingMode { +enum FpEncodingMode { FloatingPoint, UninterpretedFunctions }; -extern FpMappingMode fp_mapping_mode; +extern FpEncodingMode fp_encoding_mode; std::ostream &dbg(); void set_debug(std::ostream &os); From 0a4c47c74f017ddb54c2a1f95a4472b3fefc6bbd Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 2 Jul 2024 11:25:50 +0200 Subject: [PATCH 15/28] Refactor --- ir/instr.cpp | 140 +++++++++--------- .../alive-tv/uf-float/add-comm-ninf.srctgt.ll | 11 ++ .../alive-tv/uf-float/add-comm-nnan.srctgt.ll | 11 ++ 3 files changed, 88 insertions(+), 74 deletions(-) create mode 100644 tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index 332f88a69..418e74f53 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -853,35 +853,60 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, ty, fmath, rm, bitwise, flags_in_only, 1); } +static StateValue uf_float(const string &name, + const vector &args, + const expr &res, + FastMathFlags fmath = FastMathFlags(), + bool is_commutative = false) { + + vector arg_values; + arg_values.reserve(args.size()); + for (auto &arg : args) { + arg_values.push_back(arg.value); + } + + auto value = expr::mkUF(name, arg_values, res); + if (is_commutative) { + assert(args.size() == 2); + value = value & expr::mkUF(name, {arg_values[1], arg_values[0]}, res); + } + + AndExpr non_poison; + for (auto &arg : args) { + non_poison.add(arg.non_poison); + } + + auto fast_math_flag = [&](unsigned flag, const char* suffix){ + if (fmath.flags & flag) { + auto np_name = name + ".np_" + suffix; + auto poison_uf = expr::mkUF(np_name, arg_values, false); + if (is_commutative) { + assert(args.size() == 2); + poison_uf &= expr::mkUF(np_name, {arg_values[1], arg_values[0]}, false); + } + non_poison.add(poison_uf); + } + }; + + fast_math_flag(FastMathFlags::NNaN, "nnan"); + fast_math_flag(FastMathFlags::NInf, "ninf"); + + return { std::move(value), non_poison() }; +} + StateValue FpBinOp::toSMT(State &s) const { function fn; function scalar; bool bitwise = false; if (config::is_uf_float()) { - scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) -> StateValue { + scalar = [&](const StateValue &a, const StateValue &b, + const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); - ostringstream os; - os << getOpName() << "." << ty; - auto value = expr::mkUF(os.str(), {a.value, b.value}, a.value); - if (isCommutative()) { - value = value & expr::mkUF(os.str(), {b.value, a.value}, a.value); - } - - AndExpr non_poison; - non_poison.add(a.non_poison); - non_poison.add(b.non_poison); - if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { - os << ".np"; - auto poison_uf = expr::mkUF(os.str(), {a.value, b.value}, false); - if (isCommutative()) { - poison_uf &= expr::mkUF(os.str(), {b.value, a.value}, false); - } - non_poison.add(poison_uf); - } - - return { std::move(value), non_poison() }; + ostringstream name; + name << getOpName() << "." << ty; + return uf_float(name.str(), {a, b}, a.value, fmath, isCommutative()); }; } else { switch (op) { @@ -1173,17 +1198,9 @@ StateValue FpUnaryOp::toSMT(State &s) const { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); - ostringstream os; - os << getOpName() << "." << ty; - auto value = expr::mkUF(os.str(), {v.value}, v.value); - - auto non_poison = v.non_poison; - if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { - os << ".np"; - non_poison &= expr::mkUF(os.str(), {v.value}, false); - } - - return {std::move(value), std::move(non_poison)}; + ostringstream name; + name << getOpName() << "." << ty; + return uf_float(name.str(), {v}, v.value, fmath, false); }; } else { switch (op) { @@ -1491,20 +1508,9 @@ StateValue FpTernaryOp::toSMT(State &s) const { const StateValue &c, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); - ostringstream os; - os << getOpName() << "." << ty; - auto value = expr::mkUF(os.str(), {a.value, b.value, c.value}, a.value); - - AndExpr non_poison; - non_poison.add(a.non_poison); - non_poison.add(b.non_poison); - non_poison.add(c.non_poison); - if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { - os << ".np"; - non_poison.add(expr::mkUF(os.str(), {a.value, b.value, c.value}, false)); - } - - return {std::move(value), non_poison()}; + ostringstream name; + name << getOpName() << "." << ty; + return uf_float(name.str(), {a, b, c}, a.value, fmath); }; } else { switch (op) { @@ -1591,13 +1597,14 @@ StateValue TestOp::toSMT(State &s) const { auto &a = s[*lhs]; auto &b = s[*rhs]; function fn; + function scalar; if (config::is_uf_float()) { - fn = [&](const expr &v, const Type &ty) -> expr { + scalar = [&](const StateValue &v, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); - ostringstream os; - os << getOpName() << "." << ty; - return expr::mkUF(os.str(), {v}, expr::mkUInt(0, 1)); + ostringstream name; + name << getOpName() << "." << ty; + return uf_float(name.str(), {v}, expr::mkUInt(0, 1)); }; } else { switch (op) { @@ -1609,11 +1616,11 @@ StateValue TestOp::toSMT(State &s) const { }; break; } - } - auto scalar = [&](const StateValue &v, const Type &ty) -> StateValue { - return { fn(v.value, ty), expr(v.non_poison) }; - }; + scalar = [&](const StateValue &v, const Type &ty) -> StateValue { + return { fn(v.value, ty), expr(v.non_poison) }; + }; + } if (getType().isVectorType()) { vector vals; @@ -1866,7 +1873,7 @@ StateValue FpConversionOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &sv, const Type &from_type, - const Type &to_type) -> StateValue { + const Type &to_type) -> StateValue { s.doesApproximation("uf_float", true); ostringstream os; @@ -2931,27 +2938,12 @@ StateValue FCmp::toSMT(State &s) const { ostringstream os; os << name << "." << ty; - auto value = expr::mkUF(os.str(), {lhs.value, rhs.value}, expr::mkUInt(0, 1)); - if (commutative) { - value = value & expr::mkUF(os.str(), {rhs.value, lhs.value}, expr::mkUInt(0, 1)); - } - if (negate) { - value = ~value; - } + auto value = uf_float(os.str(), {lhs, rhs}, expr::mkUInt(0, 1), fmath, commutative); - AndExpr non_poison; - non_poison.add(a.non_poison); - non_poison.add(b.non_poison); - if ((fmath.flags & FastMathFlags::NNaN) || (fmath.flags & FastMathFlags::NInf)) { - os << ".np"; - auto poison_uf = expr::mkUF(os.str(), {lhs.value, rhs.value}, false); - if (commutative) { - poison_uf &= expr::mkUF(os.str(), {rhs.value, lhs.value}, false); - } - non_poison.add(poison_uf); + if (negate) { + value.value = ~value.value; } - - return {std::move(value), non_poison()}; + return value; } } }; diff --git a/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll new file mode 100644 index 000000000..c52c7779c --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd ninf float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd ninf float %y, %x + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll new file mode 100644 index 000000000..50d7a7c7e --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd nnan float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd nnan float %y, %x + ret float %sum +} \ No newline at end of file From 69178f83ac715626af74af92b9ffe4d77980629b Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 15 Jul 2024 14:48:09 +0200 Subject: [PATCH 16/28] Fix FpConversionOp for vectors --- ir/instr.cpp | 2 +- tests/alive-tv/uf-float/vector-convert.srctgt.ll | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 tests/alive-tv/uf-float/vector-convert.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index 418e74f53..8a75ff63a 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -1885,7 +1885,7 @@ StateValue FpConversionOp::toSMT(State &s) const { non_poison.add(sv.non_poison); if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && op != FPTrunc && op != FPExt) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {v.value}, false)); + non_poison.add(expr::mkUF(os.str(), {sv.value}, false)); } return { std::move(value), non_poison() }; diff --git a/tests/alive-tv/uf-float/vector-convert.srctgt.ll b/tests/alive-tv/uf-float/vector-convert.srctgt.ll new file mode 100644 index 000000000..05636d146 --- /dev/null +++ b/tests/alive-tv/uf-float/vector-convert.srctgt.ll @@ -0,0 +1,15 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + %a = fptosi float %x to i32 + %res = sitofp i32 %a to float + ret float %res +} + +define float @tgt(float noundef %x) { + %vec1 = insertelement <4 x float> poison, float %x, i32 0 + %vec2 = fptosi <4 x float> %vec1 to <4 x i32> + %vec3 = sitofp <4 x i32> %vec2 to <4 x float> + %res = extractelement <4 x float> %vec3, i32 0 + ret float %res +} \ No newline at end of file From 6c8050465964b628edcb4a25de73cfe8981c2daf Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 15 Jul 2024 16:55:23 +0200 Subject: [PATCH 17/28] Fix code style --- ir/instr.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 8a75ff63a..182fd858b 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -906,7 +906,7 @@ StateValue FpBinOp::toSMT(State &s) const { ostringstream name; name << getOpName() << "." << ty; - return uf_float(name.str(), {a, b}, a.value, fmath, isCommutative()); + return uf_float(std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); }; } else { switch (op) { @@ -1200,7 +1200,7 @@ StateValue FpUnaryOp::toSMT(State &s) const { ostringstream name; name << getOpName() << "." << ty; - return uf_float(name.str(), {v}, v.value, fmath, false); + return uf_float(std::move(name).str(), {v}, v.value, fmath, false); }; } else { switch (op) { @@ -1510,7 +1510,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { ostringstream name; name << getOpName() << "." << ty; - return uf_float(name.str(), {a, b, c}, a.value, fmath); + return uf_float(std::move(name).str(), {a, b, c}, a.value, fmath); }; } else { switch (op) { @@ -1604,7 +1604,7 @@ StateValue TestOp::toSMT(State &s) const { s.doesApproximation("uf_float", true); ostringstream name; name << getOpName() << "." << ty; - return uf_float(name.str(), {v}, expr::mkUInt(0, 1)); + return uf_float(std::move(name).str(), {v}, expr::mkUInt(0, 1)); }; } else { switch (op) { @@ -2938,7 +2938,8 @@ StateValue FCmp::toSMT(State &s) const { ostringstream os; os << name << "." << ty; - auto value = uf_float(os.str(), {lhs, rhs}, expr::mkUInt(0, 1), fmath, commutative); + auto value = uf_float(std::move(os).str(), {lhs, rhs}, + expr::mkUInt(0, 1), fmath, commutative); if (negate) { value.value = ~value.value; From 9c21f56f81151931fba12176c66d69feed12e82c Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 5 Aug 2024 12:18:54 +0200 Subject: [PATCH 18/28] Split long lines --- ir/instr.cpp | 3 ++- llvm_util/cmd_args_def.h | 6 +++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 3c2f1ca6e..9687356d1 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -664,7 +664,8 @@ bool FpBinOp::isCommutative() const { } void FpBinOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " " << fmath << *lhs << ", " << rhs->getName(); + os << getName() << " = " << getOpName() << " " << fmath + << *lhs << ", " << rhs->getName(); if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index c8202d31c..5c48cc372 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -29,7 +29,11 @@ if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) { config::disable_poison_input = true; } -config::fp_encoding_mode = opt_uf_float ? config::FpEncodingMode::UninterpretedFunctions : config::FpEncodingMode::FloatingPoint; +if (opt_uf_float) { + config::fp_encoding_mode = config::FpEncodingMode::UninterpretedFunctions; +} else { + config::fp_encoding_mode = config::FpEncodingMode::FloatingPoint; +} func_names.insert(opt_funcs.begin(), opt_funcs.end()); From 055172e2ad6dc6c9534ea1739789618a944d9caf Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 5 Aug 2024 12:30:14 +0200 Subject: [PATCH 19/28] Unindent existing code --- ir/instr.cpp | 543 ++++++++++++++++++++++++++------------------------- 1 file changed, 272 insertions(+), 271 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 9687356d1..96864da1d 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -904,90 +904,90 @@ StateValue FpBinOp::toSMT(State &s) const { function scalar; bool bitwise = false; - if (config::is_uf_float()) { - scalar = [&](const StateValue &a, const StateValue &b, - const Type &ty) -> StateValue { - s.doesApproximation("uf_float", true); + switch (op) { + case FAdd: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fadd(b, rm); + }; + break; - ostringstream name; - name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); + case FSub: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fsub(b, rm); }; - } else { - switch (op) { - case FAdd: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fadd(b, rm); - }; - break; + break; - case FSub: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fsub(b, rm); - }; - break; + case FMul: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fmul(b, rm); + }; + break; - case FMul: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fmul(b, rm); - }; - break; + case FDiv: + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.fdiv(b, rm); + }; + break; - case FDiv: - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.fdiv(b, rm); - }; - break; + case FRem: + fn = [&](const expr &a, const expr &b, const expr &rm) { + // TODO; Z3 has no support for LLVM's frem which is actually an fmod + auto val = a.frem(b); + s.doesApproximation("frem", val); + return val; + }; + break; - case FRem: - fn = [&](const expr &a, const expr &b, const expr &rm) { - // TODO; Z3 has no support for LLVM's frem which is actually an fmod - auto val = a.frem(b); - s.doesApproximation("frem", val); - return val; - }; - break; + case FMin: + case FMax: + fn = [&](const expr &a, const expr &b, const expr &rm) { + expr ndet = s.getFreshNondetVar("maxminnondet", true); + expr cmp = op == FMin ? a.fole(b) : a.foge(b); + return expr::mkIf(a.isNaN(), b, + expr::mkIf(b.isNaN(), a, + expr::mkIf(a.foeq(b), + expr::mkIf(ndet, a, b), + expr::mkIf(cmp, a, b)))); + }; + break; - case FMin: - case FMax: - fn = [&](const expr &a, const expr &b, const expr &rm) { - expr ndet = s.getFreshNondetVar("maxminnondet", true); - expr cmp = op == FMin ? a.fole(b) : a.foge(b); - return expr::mkIf(a.isNaN(), b, - expr::mkIf(b.isNaN(), a, - expr::mkIf(a.foeq(b), - expr::mkIf(ndet, a, b), - expr::mkIf(cmp, a, b)))); - }; - break; + case FMinimum: + case FMaximum: + fn = [&](const expr &a, const expr &b, const expr &rm) { + expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a); + expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b); + expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative()) + : (a.isFPNegative() && b.isFPNegative()); + expr e = expr::mkIf(a.isFPZero() && b.isFPZero(), + expr::mkIf(neg_cond, zneg, zpos), + expr::mkIf(cmp, a, b)); + + return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e)); + }; + break; - case FMinimum: - case FMaximum: - fn = [&](const expr &a, const expr &b, const expr &rm) { - expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a); - expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b); - expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative()) - : (a.isFPNegative() && b.isFPNegative()); - expr e = expr::mkIf(a.isFPZero() && b.isFPZero(), - expr::mkIf(neg_cond, zneg, zpos), - expr::mkIf(cmp, a, b)); - - return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e)); - }; - break; + case CopySign: + bitwise = true; + fn = [](const expr &a, const expr &b, const expr &rm) { + return a.copysign(b); + }; + break; + } - case CopySign: - bitwise = true; - fn = [](const expr &a, const expr &b, const expr &rm) { - return a.copysign(b); - }; - break; - } + scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) { + return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + [&](auto &a, auto &b, auto &rm){ return fn(a, b, rm); }, + ty, fmath, rm, bitwise); + }; + + if (config::is_uf_float()) { + scalar = [&](const StateValue &a, const StateValue &b, + const Type &ty) -> StateValue { + s.doesApproximation("uf_float", true); - scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) { - return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - [&](auto &a, auto &b, auto &rm){ return fn(a, b, rm); }, - ty, fmath, rm, bitwise); + ostringstream name; + name << getOpName() << "." << ty; + return uf_float(std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); }; } @@ -1208,6 +1208,49 @@ StateValue FpUnaryOp::toSMT(State &s) const { function scalar = nullptr; bool bitwise = false; + switch (op) { + case FAbs: + bitwise = true; + fn = [](const expr &v, const expr &rm) { return v.fabs(); }; + break; + case FNeg: + bitwise = true; + fn = [](const expr &v, const expr &rm) { return v.fneg(); }; + break; + case Canonicalize: + fn = [](const expr &v, const expr &rm) { return v; }; + break; + case Ceil: + fn = [](const expr &v, const expr &rm) { return v.ceil(); }; + break; + case Floor: + fn = [](const expr &v, const expr &rm) { return v.floor(); }; + break; + case RInt: + case NearbyInt: + // TODO: they differ in exception behavior + fn = [](const expr &v, const expr &rm) { return v.round(rm); }; + break; + case Round: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rna()); }; + break; + case RoundEven: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rne()); }; + break; + case Trunc: + fn = [](const expr &v, const expr &rm) { return v.round(expr::rtz()); }; + break; + case Sqrt: + fn = [](const expr &v, const expr &rm) { return v.sqrt(rm); }; + break; + } + + scalar = [&](const StateValue &v, const Type &ty) { + return fm_poison(s, v.value, v.non_poison, + [fn](auto &v, auto &rm) {return fn(v, rm);}, ty, fmath, rm, + bitwise, false); + }; + if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); @@ -1216,49 +1259,6 @@ StateValue FpUnaryOp::toSMT(State &s) const { name << getOpName() << "." << ty; return uf_float(std::move(name).str(), {v}, v.value, fmath, false); }; - } else { - switch (op) { - case FAbs: - bitwise = true; - fn = [](const expr &v, const expr &rm) { return v.fabs(); }; - break; - case FNeg: - bitwise = true; - fn = [](const expr &v, const expr &rm) { return v.fneg(); }; - break; - case Canonicalize: - fn = [](const expr &v, const expr &rm) { return v; }; - break; - case Ceil: - fn = [](const expr &v, const expr &rm) { return v.ceil(); }; - break; - case Floor: - fn = [](const expr &v, const expr &rm) { return v.floor(); }; - break; - case RInt: - case NearbyInt: - // TODO: they differ in exception behavior - fn = [](const expr &v, const expr &rm) { return v.round(rm); }; - break; - case Round: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rna()); }; - break; - case RoundEven: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rne()); }; - break; - case Trunc: - fn = [](const expr &v, const expr &rm) { return v.round(expr::rtz()); }; - break; - case Sqrt: - fn = [](const expr &v, const expr &rm) { return v.sqrt(rm); }; - break; - } - - scalar = [&](const StateValue &v, const Type &ty) { - return fm_poison(s, v.value, v.non_poison, - [fn](auto &v, auto &rm) {return fn(v, rm);}, ty, fmath, rm, - bitwise, false); - }; } auto &v = s[*val]; @@ -1517,6 +1517,26 @@ StateValue FpTernaryOp::toSMT(State &s) const { function fn; function scalar; + switch (op) { + case FMA: + fn = [](const expr &a, const expr &b, const expr &c, const expr &rm) { + return expr::fma(a, b, c, rm); + }; + break; + case MulAdd: + fn = [&](const expr &a, const expr &b, const expr &c, const expr &rm) { + expr var = s.getFreshNondetVar("nondet", expr(false)); + return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm)); + }; + break; + } + + scalar = [&](const StateValue &a, const StateValue &b, + const StateValue &c, const Type &ty) { + return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + c.value, c.non_poison, fn, ty, fmath, rm, false); + }; + if (config::is_uf_float()) { scalar = [&](const StateValue &a, const StateValue &b, const StateValue &c, const Type &ty) -> StateValue { @@ -1526,26 +1546,6 @@ StateValue FpTernaryOp::toSMT(State &s) const { name << getOpName() << "." << ty; return uf_float(std::move(name).str(), {a, b, c}, a.value, fmath); }; - } else { - switch (op) { - case FMA: - fn = [](const expr &a, const expr &b, const expr &c, const expr &rm) { - return expr::fma(a, b, c, rm); - }; - break; - case MulAdd: - fn = [&](const expr &a, const expr &b, const expr &c, const expr &rm) { - expr var = s.getFreshNondetVar("nondet", expr(false)); - return expr::mkIf(var, expr::fma(a, b, c, rm), a.fmul(b, rm).fadd(c, rm)); - }; - break; - } - - scalar = [&](const StateValue &a, const StateValue &b, - const StateValue &c, const Type &ty) { - return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - c.value, c.non_poison, fn, ty, fmath, rm, false); - }; } auto &av = s[*a]; @@ -1613,6 +1613,20 @@ StateValue TestOp::toSMT(State &s) const { function fn; function scalar; + switch (op) { + case Is_FPClass: + fn = [&](const expr &v, const Type &ty) -> expr { + uint64_t mask; + ENSURE(b.value.isUInt(mask) && b.non_poison.isTrue()); + return isfpclass(v, ty, mask).toBVBool(); + }; + break; + } + + scalar = [&](const StateValue &v, const Type &ty) -> StateValue { + return { fn(v.value, ty), expr(v.non_poison) }; + }; + if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); @@ -1620,20 +1634,6 @@ StateValue TestOp::toSMT(State &s) const { name << getOpName() << "." << ty; return uf_float(std::move(name).str(), {v}, expr::mkUInt(0, 1)); }; - } else { - switch (op) { - case Is_FPClass: - fn = [&](const expr &v, const Type &ty) -> expr { - uint64_t mask; - ENSURE(b.value.isUInt(mask) && b.non_poison.isTrue()); - return isfpclass(v, ty, mask).toBVBool(); - }; - break; - } - - scalar = [&](const StateValue &v, const Type &ty) -> StateValue { - return { fn(v.value, ty), expr(v.non_poison) }; - }; } if (getType().isVectorType()) { @@ -1885,6 +1885,99 @@ StateValue FpConversionOp::toSMT(State &s) const { function fn; function scalar; + switch (op) { + case SIntToFP: + fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { + return { val.sint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), + true }; + }; + break; + case UIntToFP: + fn = [&](auto &val, auto &to_type, auto &rm) -> StateValue { + return {val.uint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), + (flags & NNEG) ? !val.isNegative() : true}; + }; + break; + case FPToSInt: + case LRInt: + case LRound: + fn = [&](auto &val, auto &to_type, auto &rm_in) -> StateValue { + expr rm; + bool is_poison = false; + switch (op) { + case FPToSInt: + rm = expr::rtz(); + is_poison = true; + break; + case LRInt: + rm = rm_in; + break; + case LRound: + rm = expr::rna(); + break; + default: UNREACHABLE(); + } + expr bv = val.fp2sint(to_type.bits(), rm); + expr fp2 = bv.sint2fp(val, rm); + // -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert + expr val_rounded = val.round(rm); + expr overflow = val_rounded.isFPZero() || fp2 == val_rounded; + + expr np; + if (is_poison) { + np = std::move(overflow); + } else { + np = true; + bv = expr::mkIf(overflow, s.getFreshNondetVar("nondet", bv), bv); + } + + return { std::move(bv), std::move(np) }; + }; + break; + case FPToUInt: + fn = [](auto &val, auto &to_type, auto &rm_) -> StateValue { + expr rm = expr::rtz(); + expr bv = val.fp2uint(to_type.bits(), rm); + expr fp2 = bv.uint2fp(val, rm); + // -0.xx must be converted to 0, not poison. + expr val_rounded = val.round(rm); + return { std::move(bv), val_rounded.isFPZero() || fp2 == val_rounded }; + }; + break; + case FPExt: + case FPTrunc: + fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { + return { val.float2Float(to_type.getAsFloatType()->getDummyFloat(), rm), + true }; + }; + break; + } + + scalar = [&](const StateValue &sv, const Type &from_type, + const Type &to_type) -> StateValue { + auto val = sv.value; + + if (from_type.isFloatType()) { + auto ty = from_type.getAsFloatType(); + val = ty->getFloat(val); + } + + function fn_rm + = [&](auto &rm) { return fn(val, to_type, rm); }; + AndExpr np; + np.add(sv.non_poison); + + StateValue ret = to_type.isFloatType() ? round_value(s, rm, np, fn_rm) + : fn(val, to_type, rm.toSMT()); + np.add(std::move(ret.non_poison)); + + return { to_type.isFloatType() + ? to_type.getAsFloatType() + ->fromFloat(s, ret.value, from_type, from_type.isFloatType(), + sv.value) + : std::move(ret.value), np()}; + }; + if (config::is_uf_float()) { scalar = [&](const StateValue &sv, const Type &from_type, const Type &to_type) -> StateValue { @@ -1904,99 +1997,6 @@ StateValue FpConversionOp::toSMT(State &s) const { return { std::move(value), non_poison() }; }; - } else { - switch (op) { - case SIntToFP: - fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { - return { val.sint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), - true }; - }; - break; - case UIntToFP: - fn = [&](auto &val, auto &to_type, auto &rm) -> StateValue { - return {val.uint2fp(to_type.getAsFloatType()->getDummyFloat(), rm), - (flags & NNEG) ? !val.isNegative() : true}; - }; - break; - case FPToSInt: - case LRInt: - case LRound: - fn = [&](auto &val, auto &to_type, auto &rm_in) -> StateValue { - expr rm; - bool is_poison = false; - switch (op) { - case FPToSInt: - rm = expr::rtz(); - is_poison = true; - break; - case LRInt: - rm = rm_in; - break; - case LRound: - rm = expr::rna(); - break; - default: UNREACHABLE(); - } - expr bv = val.fp2sint(to_type.bits(), rm); - expr fp2 = bv.sint2fp(val, rm); - // -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert - expr val_rounded = val.round(rm); - expr overflow = val_rounded.isFPZero() || fp2 == val_rounded; - - expr np; - if (is_poison) { - np = std::move(overflow); - } else { - np = true; - bv = expr::mkIf(overflow, s.getFreshNondetVar("nondet", bv), bv); - } - - return { std::move(bv), std::move(np) }; - }; - break; - case FPToUInt: - fn = [](auto &val, auto &to_type, auto &rm_) -> StateValue { - expr rm = expr::rtz(); - expr bv = val.fp2uint(to_type.bits(), rm); - expr fp2 = bv.uint2fp(val, rm); - // -0.xx must be converted to 0, not poison. - expr val_rounded = val.round(rm); - return { std::move(bv), val_rounded.isFPZero() || fp2 == val_rounded }; - }; - break; - case FPExt: - case FPTrunc: - fn = [](auto &val, auto &to_type, auto &rm) -> StateValue { - return { val.float2Float(to_type.getAsFloatType()->getDummyFloat(), rm), - true }; - }; - break; - } - - scalar = [&](const StateValue &sv, const Type &from_type, - const Type &to_type) -> StateValue { - auto val = sv.value; - - if (from_type.isFloatType()) { - auto ty = from_type.getAsFloatType(); - val = ty->getFloat(val); - } - - function fn_rm - = [&](auto &rm) { return fn(val, to_type, rm); }; - AndExpr np; - np.add(sv.non_poison); - - StateValue ret = to_type.isFloatType() ? round_value(s, rm, np, fn_rm) - : fn(val, to_type, rm.toSMT()); - np.add(std::move(ret.non_poison)); - - return { to_type.isFloatType() - ? to_type.getAsFloatType() - ->fromFloat(s, ret.value, from_type, from_type.isFloatType(), - sv.value) - : std::move(ret.value), np()}; - }; } if (getType().isVectorType()) { @@ -2940,6 +2940,34 @@ StateValue FCmp::toSMT(State &s) const { function cmp; function fn; + + cmp = [&](const expr &a, const expr &b, auto &rm) { + switch (cond) { + case OEQ: return a.foeq(b); + case OGT: return a.fogt(b); + case OGE: return a.foge(b); + case OLT: return a.folt(b); + case OLE: return a.fole(b); + case ONE: return a.fone(b); + case ORD: return a.ford(b); + case UEQ: return a.fueq(b); + case UGT: return a.fugt(b); + case UGE: return a.fuge(b); + case ULT: return a.fult(b); + case ULE: return a.fule(b); + case UNE: return a.fune(b); + case UNO: return a.funo(b); + case TRUE: return expr(true); + case FALSE: return expr(false); + } + }; + + fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, + cmp, ty, fmath, {}, false, true); + return { val.toBVBool(), std::move(np) }; + }; + if (config::is_uf_float()) { fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { switch (cond) { @@ -2987,33 +3015,6 @@ StateValue FCmp::toSMT(State &s) const { } } }; - } else { - cmp = [&](const expr &a, const expr &b, auto &rm) { - switch (cond) { - case OEQ: return a.foeq(b); - case OGT: return a.fogt(b); - case OGE: return a.foge(b); - case OLT: return a.folt(b); - case OLE: return a.fole(b); - case ONE: return a.fone(b); - case ORD: return a.ford(b); - case UEQ: return a.fueq(b); - case UGT: return a.fugt(b); - case UGE: return a.fuge(b); - case ULT: return a.fult(b); - case ULE: return a.fule(b); - case UNE: return a.fune(b); - case UNO: return a.funo(b); - case TRUE: return expr(true); - case FALSE: return expr(false); - } - }; - - fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { - auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, - cmp, ty, fmath, {}, false, true); - return { val.toBVBool(), std::move(np) }; - }; } if (auto agg = a->getType().getAsAggregateType()) { From 4b5ffe42359d8e6c1dd5b0d834c2a3e4d0fa610e Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 5 Aug 2024 12:39:45 +0200 Subject: [PATCH 20/28] Smaller diff --- ir/instr.cpp | 42 ++++++++++++++++++++---------------------- 1 file changed, 20 insertions(+), 22 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 96864da1d..a5b5d0e59 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2938,31 +2938,29 @@ StateValue FCmp::toSMT(State &s) const { auto &a_eval = s[*a]; auto &b_eval = s[*b]; - function cmp; function fn; - cmp = [&](const expr &a, const expr &b, auto &rm) { - switch (cond) { - case OEQ: return a.foeq(b); - case OGT: return a.fogt(b); - case OGE: return a.foge(b); - case OLT: return a.folt(b); - case OLE: return a.fole(b); - case ONE: return a.fone(b); - case ORD: return a.ford(b); - case UEQ: return a.fueq(b); - case UGT: return a.fugt(b); - case UGE: return a.fuge(b); - case ULT: return a.fult(b); - case ULE: return a.fule(b); - case UNE: return a.fune(b); - case UNO: return a.funo(b); - case TRUE: return expr(true); - case FALSE: return expr(false); - } - }; - fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + auto cmp = [&](const expr &a, const expr &b, auto &rm) { + switch (cond) { + case OEQ: return a.foeq(b); + case OGT: return a.fogt(b); + case OGE: return a.foge(b); + case OLT: return a.folt(b); + case OLE: return a.fole(b); + case ONE: return a.fone(b); + case ORD: return a.ford(b); + case UEQ: return a.fueq(b); + case UGT: return a.fugt(b); + case UGE: return a.fuge(b); + case ULT: return a.fult(b); + case ULE: return a.fule(b); + case UNE: return a.fune(b); + case UNO: return a.funo(b); + case TRUE: return expr(true); + case FALSE: return expr(false); + } + }; auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, cmp, ty, fmath, {}, false, true); return { val.toBVBool(), std::move(np) }; From fa3cf88344222335eb8c3ee6bf03fefcc3298db8 Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 5 Aug 2024 12:45:14 +0200 Subject: [PATCH 21/28] Reference paper in comment --- ir/instr.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/ir/instr.cpp b/ir/instr.cpp index a5b5d0e59..a25304783 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -872,6 +872,12 @@ static StateValue uf_float(const string &name, auto value = expr::mkUF(name, arg_values, res); if (is_commutative) { + // Commutative functions are encoded as + // op(x, y) = op'(x, y) & op'(y, x) + // where & is the bitwise and operator and op' is an uninterpreted function. + // This encoding comes from "SMT-based Translation Validation for Machine + // Learning Compiler" by Seongwon Bang, Seunghyeon Nam, Inwhan Chun, + // Ho Young Jhoo, and Juneyoung Lee assert(args.size() == 2); value = value & expr::mkUF(name, {arg_values[1], arg_values[0]}, res); } From 8eef61cecc2e58331518777cb7be61f27d353f85 Mon Sep 17 00:00:00 2001 From: Can Date: Mon, 5 Aug 2024 12:51:47 +0200 Subject: [PATCH 22/28] Split long lines --- ir/instr.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index a25304783..a809ce0e9 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -993,7 +993,8 @@ StateValue FpBinOp::toSMT(State &s) const { ostringstream name; name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); + return uf_float(std::move(name).str(), {a, b}, a.value, + fmath, isCommutative()); }; } @@ -1996,7 +1997,8 @@ StateValue FpConversionOp::toSMT(State &s) const { AndExpr non_poison; non_poison.add(sv.non_poison); - if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && op != FPTrunc && op != FPExt) { + if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && + op != FPTrunc && op != FPExt) { os << ".np"; non_poison.add(expr::mkUF(os.str(), {sv.value}, false)); } From 35f65ade3d5645fb1d0d77b2657e3d860d803642 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 6 Aug 2024 17:13:38 +0200 Subject: [PATCH 23/28] Fix formatting --- ir/instr.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index a809ce0e9..570a7461e 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -1537,7 +1537,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { }; break; } - + scalar = [&](const StateValue &a, const StateValue &b, const StateValue &c, const Type &ty) { return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, @@ -1546,7 +1546,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &a, const StateValue &b, - const StateValue &c, const Type &ty) -> StateValue { + const StateValue &c, const Type &ty) -> StateValue { s.doesApproximation("uf_float", true); ostringstream name; From 123ee99548bfaa760384d64bff300ea66ac5e788 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 6 Aug 2024 17:29:48 +0200 Subject: [PATCH 24/28] Use doesApproximation correctly --- ir/instr.cpp | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 570a7461e..de7d83d33 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -858,7 +858,7 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, ty, fmath, rm, bitwise, flags_in_only, 1); } -static StateValue uf_float(const string &name, +static StateValue uf_float(State &s, const string &name, const vector &args, const expr &res, FastMathFlags fmath = FastMathFlags(), @@ -871,6 +871,7 @@ static StateValue uf_float(const string &name, } auto value = expr::mkUF(name, arg_values, res); + s.doesApproximation("uf_float", value); if (is_commutative) { // Commutative functions are encoded as // op(x, y) = op'(x, y) & op'(y, x) @@ -891,6 +892,7 @@ static StateValue uf_float(const string &name, if (fmath.flags & flag) { auto np_name = name + ".np_" + suffix; auto poison_uf = expr::mkUF(np_name, arg_values, false); + s.doesApproximation("uf_float", poison_uf); if (is_commutative) { assert(args.size() == 2); poison_uf &= expr::mkUF(np_name, {arg_values[1], arg_values[0]}, false); @@ -989,11 +991,9 @@ StateValue FpBinOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) -> StateValue { - s.doesApproximation("uf_float", true); - ostringstream name; name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {a, b}, a.value, + return uf_float(s, std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); }; } @@ -1260,11 +1260,9 @@ StateValue FpUnaryOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { - s.doesApproximation("uf_float", true); - ostringstream name; name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {v}, v.value, fmath, false); + return uf_float(s, std::move(name).str(), {v}, v.value, fmath, false); }; } @@ -1547,11 +1545,9 @@ StateValue FpTernaryOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &a, const StateValue &b, const StateValue &c, const Type &ty) -> StateValue { - s.doesApproximation("uf_float", true); - ostringstream name; name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {a, b, c}, a.value, fmath); + return uf_float(s, std::move(name).str(), {a, b, c}, a.value, fmath); }; } @@ -1636,10 +1632,9 @@ StateValue TestOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { - s.doesApproximation("uf_float", true); ostringstream name; name << getOpName() << "." << ty; - return uf_float(std::move(name).str(), {v}, expr::mkUInt(0, 1)); + return uf_float(s, std::move(name).str(), {v}, expr::mkUInt(0, 1)); }; } @@ -1988,19 +1983,20 @@ StateValue FpConversionOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &sv, const Type &from_type, const Type &to_type) -> StateValue { - s.doesApproximation("uf_float", true); - ostringstream os; os << getOpName() << "." << from_type << ".to." << to_type; expr range = to_type.getDummyValue(true).value; auto value = expr::mkUF(os.str(), {sv.value}, range); + s.doesApproximation("uf_float", value); AndExpr non_poison; non_poison.add(sv.non_poison); if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && op != FPTrunc && op != FPExt) { os << ".np"; - non_poison.add(expr::mkUF(os.str(), {sv.value}, false)); + auto poison_uf = expr::mkUF(os.str(), {sv.value}, false); + s.doesApproximation("uf_float", poison_uf); + non_poison.add(poison_uf); } return { std::move(value), non_poison() }; @@ -2983,8 +2979,6 @@ StateValue FCmp::toSMT(State &s) const { // All conditions are encoded using only 5 uninterpreted functions: // oeq, ueq, olt, ult, ord - s.doesApproximation("uf_float", true); - StateValue lhs = a; StateValue rhs = b; @@ -3011,7 +3005,7 @@ StateValue FCmp::toSMT(State &s) const { ostringstream os; os << name << "." << ty; - auto value = uf_float(std::move(os).str(), {lhs, rhs}, + auto value = uf_float(s, std::move(os).str(), {lhs, rhs}, expr::mkUInt(0, 1), fmath, commutative); if (negate) { From 0685b96f5eba916bbd9fd559b63b98fa5d627ea8 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 6 Aug 2024 17:44:52 +0200 Subject: [PATCH 25/28] Remove unused FCmp::getCondName --- ir/instr.cpp | 45 +++++++++++++++++++++------------------------ ir/instr.h | 1 - 2 files changed, 21 insertions(+), 25 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index de7d83d33..5b8ba8510 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2907,30 +2907,27 @@ void FCmp::rauw(const Value &what, Value &with) { RAUW(b); } -const char* FCmp::getCondName() const { - switch (cond) { - case OEQ: return "oeq"; break; - case OGT: return "ogt"; break; - case OGE: return "oge"; break; - case OLT: return "olt"; break; - case OLE: return "ole"; break; - case ONE: return "one"; break; - case ORD: return "ord"; break; - case UEQ: return "ueq"; break; - case UGT: return "ugt"; break; - case UGE: return "uge"; break; - case ULT: return "ult"; break; - case ULE: return "ule"; break; - case UNE: return "une"; break; - case UNO: return "uno"; break; - case TRUE: return "true"; break; - case FALSE: return "false"; break; - } - UNREACHABLE(); -} - void FCmp::print(ostream &os) const { - os << getName() << " = fcmp " << fmath << getCondName() << " " << *a << ", " + const char *condtxt = nullptr; + switch (cond) { + case OEQ: condtxt = "oeq "; break; + case OGT: condtxt = "ogt "; break; + case OGE: condtxt = "oge "; break; + case OLT: condtxt = "olt "; break; + case OLE: condtxt = "ole "; break; + case ONE: condtxt = "one "; break; + case ORD: condtxt = "ord "; break; + case UEQ: condtxt = "ueq "; break; + case UGT: condtxt = "ugt "; break; + case UGE: condtxt = "uge "; break; + case ULT: condtxt = "ult "; break; + case ULE: condtxt = "ule "; break; + case UNE: condtxt = "une "; break; + case UNO: condtxt = "uno "; break; + case TRUE: condtxt = "true "; break; + case FALSE: condtxt = "false "; break; + } + os << getName() << " = fcmp " << fmath << condtxt << *a << ", " << b->getName(); if (signaling) os << ", signaling"; @@ -2944,7 +2941,7 @@ StateValue FCmp::toSMT(State &s) const { function fn; - fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { auto cmp = [&](const expr &a, const expr &b, auto &rm) { switch (cond) { case OEQ: return a.foeq(b); diff --git a/ir/instr.h b/ir/instr.h index a74ced54a..a1d426d44 100644 --- a/ir/instr.h +++ b/ir/instr.h @@ -480,7 +480,6 @@ class FCmp final : public Instr { bool propagatesPoison() const override; bool hasSideEffects() const override; void rauw(const Value &what, Value &with) override; - const char* getCondName() const; void print(std::ostream &os) const override; StateValue toSMT(State &s) const override; smt::expr getTypeConstraints(const Function &f) const override; From 51e4cc5f74160159de81826f102f285d9718da7c Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 6 Aug 2024 18:12:05 +0200 Subject: [PATCH 26/28] Refactor FpConversionOp --- ir/instr.cpp | 55 +++++++++++++++++++++++++--------------------------- 1 file changed, 26 insertions(+), 29 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 5b8ba8510..bfd928b1a 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -862,7 +862,8 @@ static StateValue uf_float(State &s, const string &name, const vector &args, const expr &res, FastMathFlags fmath = FastMathFlags(), - bool is_commutative = false) { + bool is_commutative = false, + bool is_partial = false) { vector arg_values; arg_values.reserve(args.size()); @@ -888,21 +889,25 @@ static StateValue uf_float(State &s, const string &name, non_poison.add(arg.non_poison); } - auto fast_math_flag = [&](unsigned flag, const char* suffix){ - if (fmath.flags & flag) { - auto np_name = name + ".np_" + suffix; - auto poison_uf = expr::mkUF(np_name, arg_values, false); - s.doesApproximation("uf_float", poison_uf); - if (is_commutative) { - assert(args.size() == 2); - poison_uf &= expr::mkUF(np_name, {arg_values[1], arg_values[0]}, false); - } - non_poison.add(poison_uf); + auto poison_condition = [&](const char* suffix){ + auto np_name = name + ".np_" + suffix; + auto poison_uf = expr::mkUF(np_name, arg_values, false); + s.doesApproximation("uf_float", poison_uf); + if (is_commutative) { + assert(args.size() == 2); + poison_uf &= expr::mkUF(np_name, {arg_values[1], arg_values[0]}, false); } + non_poison.add(poison_uf); }; - fast_math_flag(FastMathFlags::NNaN, "nnan"); - fast_math_flag(FastMathFlags::NInf, "ninf"); + if (fmath.flags & FastMathFlags::NNaN) + poison_condition("nnan"); + if (fmath.flags & FastMathFlags::NInf) + poison_condition("ninf"); + + // Partial functions may produce poison for inputs where they are not defined. + if (is_partial) + poison_condition("partial"); return { std::move(value), non_poison() }; } @@ -1983,23 +1988,15 @@ StateValue FpConversionOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &sv, const Type &from_type, const Type &to_type) -> StateValue { - ostringstream os; - os << getOpName() << "." << from_type << ".to." << to_type; + ostringstream name; + name << getOpName() << "." << from_type << ".to." << to_type; expr range = to_type.getDummyValue(true).value; - auto value = expr::mkUF(os.str(), {sv.value}, range); - s.doesApproximation("uf_float", value); - - AndExpr non_poison; - non_poison.add(sv.non_poison); - if (op != SIntToFP && !(op == UIntToFP && !(flags & NNEG)) && - op != FPTrunc && op != FPExt) { - os << ".np"; - auto poison_uf = expr::mkUF(os.str(), {sv.value}, false); - s.doesApproximation("uf_float", poison_uf); - non_poison.add(poison_uf); - } - - return { std::move(value), non_poison() }; + bool is_partial = (op == UIntToFP && (flags & NNEG)) || + op == FPToSInt || + op == FPToUInt; + + return uf_float(s, std::move(name).str(), {sv}, range, + FastMathFlags(), false, is_partial); }; } From c397911317f1c8f62aa31109dfc155d3b78db056 Mon Sep 17 00:00:00 2001 From: Can Date: Tue, 6 Aug 2024 19:19:25 +0200 Subject: [PATCH 27/28] Move variable declarations to same line as definitions --- ir/instr.cpp | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index bfd928b1a..2decbc391 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -914,7 +914,6 @@ static StateValue uf_float(State &s, const string &name, StateValue FpBinOp::toSMT(State &s) const { function fn; - function scalar; bool bitwise = false; switch (op) { @@ -987,7 +986,8 @@ StateValue FpBinOp::toSMT(State &s) const { break; } - scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) { + function scalar = + [&](const StateValue &a, const StateValue &b, const Type &ty) { return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, [&](auto &a, auto &b, auto &rm){ return fn(a, b, rm); }, ty, fmath, rm, bitwise); @@ -1525,7 +1525,6 @@ void FpTernaryOp::print(ostream &os) const { StateValue FpTernaryOp::toSMT(State &s) const { function fn; - function scalar; switch (op) { case FMA: @@ -1541,8 +1540,10 @@ StateValue FpTernaryOp::toSMT(State &s) const { break; } - scalar = [&](const StateValue &a, const StateValue &b, - const StateValue &c, const Type &ty) { + function scalar = + [&](const StateValue &a, const StateValue &b, + const StateValue &c, const Type &ty) { return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison, c.value, c.non_poison, fn, ty, fmath, rm, false); }; @@ -1619,7 +1620,6 @@ StateValue TestOp::toSMT(State &s) const { auto &a = s[*lhs]; auto &b = s[*rhs]; function fn; - function scalar; switch (op) { case Is_FPClass: @@ -1631,7 +1631,8 @@ StateValue TestOp::toSMT(State &s) const { break; } - scalar = [&](const StateValue &v, const Type &ty) -> StateValue { + function scalar = + [&](const StateValue &v, const Type &ty) -> StateValue { return { fn(v.value, ty), expr(v.non_poison) }; }; @@ -1890,7 +1891,6 @@ void FpConversionOp::print(ostream &os) const { StateValue FpConversionOp::toSMT(State &s) const { auto &v = s[*val]; function fn; - function scalar; switch (op) { case SIntToFP: @@ -1960,8 +1960,9 @@ StateValue FpConversionOp::toSMT(State &s) const { break; } - scalar = [&](const StateValue &sv, const Type &from_type, - const Type &to_type) -> StateValue { + function scalar = + [&](const StateValue &sv, const Type &from_type, + const Type &to_type) -> StateValue { auto val = sv.value; if (from_type.isFloatType()) { From b8d2f8390574da60cae3367fccb199a88a0fe407 Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 7 Aug 2024 12:22:36 +0200 Subject: [PATCH 28/28] Fix formatting --- ir/instr.cpp | 100 +++++++++++++++++++++++++-------------------------- 1 file changed, 50 insertions(+), 50 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 2decbc391..935c37cb9 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -635,16 +635,16 @@ void FpBinOp::rauw(const Value &what, Value &with) { const char* FpBinOp::getOpName() const { switch (op) { - case FAdd: return "fadd"; break; - case FSub: return "fsub"; break; - case FMul: return "fmul"; break; - case FDiv: return "fdiv"; break; - case FRem: return "frem"; break; - case FMax: return "fmax"; break; - case FMin: return "fmin"; break; - case FMaximum: return "fmaximum"; break; - case FMinimum: return "fminimum"; break; - case CopySign: return "copysign"; break; + case FAdd: return "fadd"; + case FSub: return "fsub"; + case FMul: return "fmul"; + case FDiv: return "fdiv"; + case FRem: return "frem"; + case FMax: return "fmax"; + case FMin: return "fmin"; + case FMaximum: return "fmaximum"; + case FMinimum: return "fminimum"; + case CopySign: return "copysign"; } UNREACHABLE(); } @@ -664,7 +664,7 @@ bool FpBinOp::isCommutative() const { } void FpBinOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " " << fmath + os << getName() << " = " << getOpName() << ' ' << fmath << *lhs << ", " << rhs->getName(); if (!rm.isDefault()) os << ", rounding=" << rm; @@ -889,7 +889,7 @@ static StateValue uf_float(State &s, const string &name, non_poison.add(arg.non_poison); } - auto poison_condition = [&](const char* suffix){ + auto poison_condition = [&](const char* suffix) { auto np_name = name + ".np_" + suffix; auto poison_uf = expr::mkUF(np_name, arg_values, false); s.doesApproximation("uf_float", poison_uf); @@ -997,7 +997,7 @@ StateValue FpBinOp::toSMT(State &s) const { scalar = [&](const StateValue &a, const StateValue &b, const Type &ty) -> StateValue { ostringstream name; - name << getOpName() << "." << ty; + name << getOpName() << '.' << ty; return uf_float(s, std::move(name).str(), {a, b}, a.value, fmath, isCommutative()); }; @@ -1192,23 +1192,23 @@ void FpUnaryOp::rauw(const Value &what, Value &with) { const char* FpUnaryOp::getOpName() const { switch (op) { - case FAbs: return "fabs"; break; - case FNeg: return "fneg"; break; - case Canonicalize: return "canonicalize"; break; - case Ceil: return "ceil"; break; - case Floor: return "floor"; break; - case RInt: return "rint"; break; - case NearbyInt: return "nearbyint"; break; - case Round: return "round"; break; - case RoundEven: return "roundeven"; break; - case Trunc: return "trunc"; break; - case Sqrt: return "sqrt"; break; + case FAbs: return "fabs"; + case FNeg: return "fneg"; + case Canonicalize: return "canonicalize"; + case Ceil: return "ceil"; + case Floor: return "floor"; + case RInt: return "rint"; + case NearbyInt: return "nearbyint"; + case Round: return "round"; + case RoundEven: return "roundeven"; + case Trunc: return "trunc"; + case Sqrt: return "sqrt"; } UNREACHABLE(); } void FpUnaryOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " " << fmath << *val; + os << getName() << " = " << getOpName() << ' ' << fmath << *val; if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) @@ -1216,8 +1216,7 @@ void FpUnaryOp::print(ostream &os) const { } StateValue FpUnaryOp::toSMT(State &s) const { - function fn = nullptr; - function scalar = nullptr; + expr (*fn)(const expr&, const expr&) = nullptr; bool bitwise = false; switch (op) { @@ -1257,7 +1256,8 @@ StateValue FpUnaryOp::toSMT(State &s) const { break; } - scalar = [&](const StateValue &v, const Type &ty) { + function scalar = + [&](const StateValue &v, const Type &ty) { return fm_poison(s, v.value, v.non_poison, [fn](auto &v, auto &rm) {return fn(v, rm);}, ty, fmath, rm, bitwise, false); @@ -1266,7 +1266,7 @@ StateValue FpUnaryOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { ostringstream name; - name << getOpName() << "." << ty; + name << getOpName() << '.' << ty; return uf_float(s, std::move(name).str(), {v}, v.value, fmath, false); }; } @@ -1509,14 +1509,15 @@ void FpTernaryOp::rauw(const Value &what, Value &with) { const char* FpTernaryOp::getOpName() const { switch (op) { - case FMA: return "fma"; break; - case MulAdd: return "fmuladd"; break; + case FMA: return "fma"; + case MulAdd: return "fmuladd"; } UNREACHABLE(); } void FpTernaryOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " " << fmath << *a << ", " << *b << ", " << *c; + os << getName() << " = " << getOpName() << ' ' << fmath + << *a << ", " << *b << ", " << *c; if (!rm.isDefault()) os << ", rounding=" << rm; if (!ex.ignore()) @@ -1552,7 +1553,7 @@ StateValue FpTernaryOp::toSMT(State &s) const { scalar = [&](const StateValue &a, const StateValue &b, const StateValue &c, const Type &ty) -> StateValue { ostringstream name; - name << getOpName() << "." << ty; + name << getOpName() << '.' << ty; return uf_float(s, std::move(name).str(), {a, b, c}, a.value, fmath); }; } @@ -1607,13 +1608,13 @@ void TestOp::rauw(const Value &what, Value &with) { const char* TestOp::getOpName() const { switch (op) { - case Is_FPClass: return "is.fpclass"; break; + case Is_FPClass: return "is.fpclass"; } UNREACHABLE(); } void TestOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " " << *lhs << ", " << *rhs; + os << getName() << " = " << getOpName() << ' ' << *lhs << ", " << *rhs; } StateValue TestOp::toSMT(State &s) const { @@ -1639,7 +1640,7 @@ StateValue TestOp::toSMT(State &s) const { if (config::is_uf_float()) { scalar = [&](const StateValue &v, const Type &ty) -> StateValue { ostringstream name; - name << getOpName() << "." << ty; + name << getOpName() << '.' << ty; return uf_float(s, std::move(name).str(), {v}, expr::mkUInt(0, 1)); }; } @@ -1865,20 +1866,20 @@ void FpConversionOp::rauw(const Value &what, Value &with) { const char* FpConversionOp::getOpName() const { switch (op) { - case SIntToFP: return "sitofp"; break; - case UIntToFP: return "uitofp"; break; - case FPToSInt: return "fptosi"; break; - case FPToUInt: return "fptoui"; break; - case FPExt: return "fpext"; break; - case FPTrunc: return "fptrunc"; break; - case LRInt: return "lrint"; break; - case LRound: return "lround"; break; + case SIntToFP: return "sitofp"; + case UIntToFP: return "uitofp"; + case FPToSInt: return "fptosi"; + case FPToUInt: return "fptoui"; + case FPExt: return "fpext"; + case FPTrunc: return "fptrunc"; + case LRInt: return "lrint"; + case LRound: return "lround"; } UNREACHABLE(); } void FpConversionOp::print(ostream &os) const { - os << getName() << " = " << getOpName() << " "; + os << getName() << " = " << getOpName() << ' '; if (flags & NNEG) os << "nneg "; os << *val << print_type(getType(), " to ", ""); @@ -1990,7 +1991,7 @@ StateValue FpConversionOp::toSMT(State &s) const { scalar = [&](const StateValue &sv, const Type &from_type, const Type &to_type) -> StateValue { ostringstream name; - name << getOpName() << "." << from_type << ".to." << to_type; + name << getOpName() << '.' << from_type << ".to." << to_type; expr range = to_type.getDummyValue(true).value; bool is_partial = (op == UIntToFP && (flags & NNEG)) || op == FPToSInt || @@ -2937,9 +2938,8 @@ StateValue FCmp::toSMT(State &s) const { auto &a_eval = s[*a]; auto &b_eval = s[*b]; - function fn; - - fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue { + function fn = + [&](const auto &a, const auto &b, const Type &ty) -> StateValue { auto cmp = [&](const expr &a, const expr &b, auto &rm) { switch (cond) { case OEQ: return a.foeq(b); @@ -2999,7 +2999,7 @@ StateValue FCmp::toSMT(State &s) const { } ostringstream os; - os << name << "." << ty; + os << name << '.' << ty; auto value = uf_float(s, std::move(os).str(), {lhs, rhs}, expr::mkUInt(0, 1), fmath, commutative);