memory: allow float<->int type punning
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -191,7 +191,7 @@ ostream& operator<<(ostream &os, const Byte &byte) {
}
static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
- const Memory &mem) {
+ const Memory &mem, State *s) {
vector<Byte> bytes;
if (fromType.isPtrType()) {
Pointer p(mem, val.value);
@@ -200,7 +200,7 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
for (unsigned i = 0; i < bytesize; ++i)
bytes.emplace_back(p, i, val.non_poison);
} else {
- StateValue bvval = fromType.toBV(val);
+ StateValue bvval = fromType.toInt(*s, val);
unsigned bitsize = bvval.bits();
unsigned bytesize = divide_up(bitsize, bits_byte);
@@ -261,7 +261,7 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
val = first ? move(v) : v.concat(val);
first = false;
}
- return toType.fromBV(val.trunc(bitsize));
+ return toType.fromInt(val.trunc(bitsize));
}
}
@@ -1166,7 +1166,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
assert(byteofs == getStoreByteSize(type));
} else {
- vector<Byte> bytes = valueToBytes(v, type, *this);
+ vector<Byte> bytes = valueToBytes(v, type, *this, state);
assert(!v.isValid() || bytes.size() * bytesz == getStoreByteSize(type));
for (unsigned i = 0, e = bytes.size(); i < e; ++i) {
@@ -1238,7 +1238,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytesize, align, true);
- vector<Byte> bytes = valueToBytes(val, IntType("", bits_byte), *this);
+ vector<Byte> bytes = valueToBytes(val, IntType("", bits_byte), *this, state);
assert(bytes.size() == 1);
uint64_t n;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -256,7 +256,7 @@ ostream& operator<<(ostream &os, const Type &t) {
}
string Type::toString() const {
- stringstream s;
+ ostringstream s;
print(s);
return s.str();
}
@@ -425,6 +425,49 @@ StateValue FloatType::toInt(State &s, StateValue v) const {
return Type::toInt(s, move(v));
}
+bool FloatType::isNaNInt(const expr &e) const {
+ if (!e.isValid())
+ return false;
+
+ auto bw = e.bits();
+ unsigned exp_bits = float_sizes[fpType].second;
+ unsigned fraction_bits = bw - exp_bits - 1;
+
+ expr sign = e.extract(bw - 1, bw - 1);
+ expr exponent = e.extract(bw - 2, fraction_bits);
+ expr fraction = e.extract(fraction_bits - 1, 0);
+ assert(exponent.bits() == exp_bits);
+
+ expr nan, nan2;
+ unsigned h, l;
+ bool ok = sign.isExtract(nan, h, l) && fraction.isExtract(nan2, h, l) &&
+ nan.eq(nan2);
+ auto nan_name = nan.str();
+ ok &= string_view(nan_name).substr(0, 4) == "NaN!";
+
+ return ok && exponent.isAllOnes();
+}
+
+expr FloatType::fromInt(expr e) const {
+ if (isNaNInt(e))
+ return expr::mkNaN(getDummyValue(true).value);
+
+ expr cond, then, els, n, n2;
+ // match (ite (isNaN x) int_nan (fp.to_ieee_bv x))
+ if (e.isIf(cond, then, els) &&
+ cond.isNaNCheck(n) &&
+ isNaNInt(then) &&
+ els.isfloat2BV(n2) &&
+ n.eq(n2))
+ return n;
+
+ return fromBV(move(e));
+}
+
+StateValue FloatType::fromInt(StateValue v) const {
+ return Type::fromInt(move(v));
+}
+
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(bits(), var_bw_bits) : Type::sizeVar();
}

MODIFY
ir/type.h
ir/type.h
@@ -179,6 +179,8 @@ private:
FpType fpType = Unknown;
bool defined = false;
+ bool isNaNInt(const smt::expr &e) const;
+
public:
FloatType(std::string &&name) : Type(std::move(name)) {}
FloatType(std::string &&name, FpType fpType)
@@ -200,6 +202,8 @@ public:
IR::StateValue fromBV(IR::StateValue v) const override;
smt::expr toInt(State &s, smt::expr v) const override;
IR::StateValue toInt(State &s, IR::StateValue v) const override;
+ smt::expr fromInt(smt::expr v) const override;
+ IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -197,6 +197,11 @@ expr expr::mkDouble(double n) {
return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx()));
}
+expr expr::mkNaN(const expr &type) {
+ C2(type);
+ return Z3_mk_fpa_nan(ctx(), type.sort());
+}
+
expr expr::mkNumber(const char *n, const expr &type) {
C2(type);
return Z3_mk_numeral(ctx(), n, type.sort());
@@ -395,6 +400,22 @@ bool expr::isStore(expr &array, expr &idx, expr &val) const {
return false;
}
+bool expr::isNaNCheck(expr &fp) const {
+ if (auto app = isAppOf(Z3_OP_FPA_IS_NAN)) {
+ fp = Z3_get_app_arg(ctx(), app, 0);
+ return true;
+ }
+ return false;
+}
+
+bool expr::isfloat2BV(expr &fp) const {
+ if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) {
+ fp = Z3_get_app_arg(ctx(), app, 0);
+ return true;
+ }
+ return false;
+}
+
unsigned expr::min_leading_zeros() const {
expr a, b;
uint64_t n;
@@ -1543,6 +1564,10 @@ string expr::numeral_string() const {
return Z3_get_numeral_decimal_string(ctx(), ast(), 12);
}
+string expr::str() const {
+ return isValid() ? Z3_ast_to_string(ctx(), ast()) : "(null)";
+}
+
ostream& operator<<(ostream &os, const expr &e) {
return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}

MODIFY
smt/expr.h
smt/expr.h
@@ -85,6 +85,7 @@ public:
static expr mkHalf(float n);
static expr mkFloat(float n);
static expr mkDouble(double n);
+ static expr mkNaN(const expr &type);
static expr mkNumber(const char *n, const expr &type);
static expr mkVar(const char *name, const expr &type);
static expr mkVar(const char *name, unsigned bits);
@@ -125,6 +126,9 @@ public:
bool isConstArray(expr &val) const;
bool isStore(expr &array, expr &idx, expr &val) const;
+ bool isNaNCheck(expr &fp) const;
+ bool isfloat2BV(expr &fp) const;
+
// best effort; returns number of statically known bits
unsigned min_leading_zeros() const;
@@ -285,6 +289,7 @@ public:
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;
std::string numeral_string() const;
+ std::string str() const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only

ADD
tests/alive-tv/cast.src.ll
+; TEST-ARGS: -smt-to=10000
+
+define i16 @f1(half %x) {
+ %a = alloca half
+ store half %x, half* %a
+ %p = bitcast half* %a to i16*
+ %i = load i16, i16* %p
+ ret i16 %i
+}

ADD
tests/alive-tv/cast.tgt.ll
+define i16 @f1(half %x) {
+ %i = bitcast half %x to i16
+ ret i16 %i
+}

MODIFY
tests/alive-tv/memory/store-nan.src.ll
tests/alive-tv/memory/store-nan.src.ll
-define float @f(float* %ptr) {
- %f = fdiv float 0.0, 0.0
- store float %f, float* %ptr
- %x = load float, float* %ptr
- ret float %x
+define half @f(half* %ptr) {
+ %f = fdiv half 0.0, 0.0
+ store half %f, half* %ptr
+ %x = load half, half* %ptr
+ ret half %x
}

MODIFY
tests/alive-tv/memory/store-nan.tgt.ll
tests/alive-tv/memory/store-nan.tgt.ll
-define float @f(float* %ptr) {
- %f = fdiv float 0.0, 0.0
- store float %f, float* %ptr
- ret float %f
+define half @f(half* %ptr) {
+ %f = fdiv half 0.0, 0.0
+ store half %f, half* %ptr
+ ret half %f
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -72,9 +72,7 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
// needed, not because it's undef
bool found_undef = false;
for (auto &var : partial.vars()) {
- ostringstream ss;
- ss << var;
- auto name = ss.str();
+ auto name = var.str();
found_undef |= string_view(name).substr(0, 6) == "undef!";
}
if (found_undef)

memory: allow float<->int type punning