fix add support for bfloat
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -71,6 +71,7 @@ StateValue FloatConst::toSMT(State &s) const {
case FloatType::Half: e = expr::mkHalf((float)v); break;
case FloatType::Float: e = expr::mkFloat((float)v); break;
case FloatType::Double: e = expr::mkDouble(v); break;
+ case FloatType::BFloat: e = expr::mkBFloat((float)v); break;
case FloatType::Quad:
case FloatType::Unknown: UNREACHABLE();
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -385,11 +385,12 @@ void IntType::print(ostream &os) const {
// total bits, exponent bits
-static array<pair<unsigned, unsigned>, 4> float_sizes = {
+static array<pair<unsigned, unsigned>, 5> float_sizes = {
/* Half */ make_pair(16, 5),
/* Float */ make_pair(32, 8),
/* Double */ make_pair(64, 11),
/* Quad */ make_pair(128, 15),
+ /* BFloat */ make_pair(16, 8),
};
unsigned FloatType::bits() const {
@@ -499,6 +500,7 @@ StateValue FloatType::getDummyValue(bool non_poison) const {
case Float: e = expr::mkFloat(0); break;
case Double: e = expr::mkDouble(0); break;
case Quad: e = expr::mkQuad(0); break;
+ case BFloat: e = expr::mkBFloat(0); break;
case Unknown: UNREACHABLE();
}
return { move(e), non_poison };
@@ -556,6 +558,7 @@ expr FloatType::mkInput(State &s, const char *name,
case Float: return expr::mkFloatVar(name);
case Double: return expr::mkDoubleVar(name);
case Quad: return expr::mkQuadVar(name);
+ case BFloat: return expr::mkBFloatVar(name);
case Unknown: UNREACHABLE();
}
UNREACHABLE();
@@ -579,22 +582,16 @@ void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
}
void FloatType::print(ostream &os) const {
+ const char *name = "";
switch (fpType) {
- case Half:
- os << "half";
- break;
- case Float:
- os << "float";
- break;
- case Double:
- os << "double";
- break;
- case Quad:
- os << "fp128";
- break;
- case Unknown:
- break;
- }
+ case Half: name = "half"; break;
+ case Float: name = "float"; break;
+ case Double: name = "double"; break;
+ case Quad: name = "fp128"; break;
+ case BFloat: name = "bfloat"; break;
+ case Unknown: break;
+ }
+ os << name;
}

MODIFY
ir/type.h
ir/type.h
@@ -178,7 +178,7 @@ public:
class FloatType final : public Type {
public:
enum FpType {
- Half, Float, Double, Quad, Unknown
+ Half, Float, Double, Quad, BFloat, Unknown
};
private:

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -32,6 +32,7 @@ FloatType half_type("half", FloatType::Half);
FloatType float_type("float", FloatType::Float);
FloatType double_type("double", FloatType::Double);
FloatType quad_type("fp128", FloatType::Quad);
+FloatType bfloat_type("bfloat", FloatType::BFloat);
// cache complex types
unordered_map<const llvm::Type*, unique_ptr<Type>> type_cache;
@@ -126,6 +127,8 @@ Type* llvm_type2alive(const llvm::Type *ty) {
return &double_type;
case llvm::Type::FP128TyID:
return &quad_type;
+ case llvm::Type::BFloatTyID:
+ return &bfloat_type;
case llvm::Type::PointerTyID: {
// TODO: support for non-64 bits pointers
@@ -267,6 +270,7 @@ Value* get_operand(llvm::Value *v,
apfloat.bitcastToAPInt().getLimitedValue());
break;
case FloatType::Float:
+ case FloatType::BFloat:
c = make_unique<FloatConst>(*ty, apfloat.convertToFloat());
break;
case FloatType::Double:

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -227,6 +227,14 @@ expr expr::mkHalf(float n) {
return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()));
}
+static Z3_sort mk_bfloat_sort() {
+ return Z3_mk_fpa_sort(ctx(), 8, 8);
+}
+
+expr expr::mkBFloat(float n) {
+ return Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort());
+}
+
expr expr::mkFloat(float n) {
return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx()));
}
@@ -299,6 +307,10 @@ expr expr::mkHalfVar(const char *name) {
return ::mkVar(name, Z3_mk_fpa_sort_half(ctx()));
}
+expr expr::mkBFloatVar(const char *name) {
+ return ::mkVar(name, mk_bfloat_sort());
+}
+
expr expr::mkFloatVar(const char *name) {
return ::mkVar(name, Z3_mk_fpa_sort_single(ctx()));
}

MODIFY
smt/expr.h
smt/expr.h
@@ -81,6 +81,7 @@ public:
static expr mkInt(const char *n, unsigned bits);
static expr mkFloat(double n, const expr &type);
static expr mkHalf(float n);
+ static expr mkBFloat(float n);
static expr mkFloat(float n);
static expr mkDouble(double n);
static expr mkQuad(double n);
@@ -90,6 +91,7 @@ public:
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);
static expr mkHalfVar(const char *name);
+ static expr mkBFloatVar(const char *name);
static expr mkFloatVar(const char *name);
static expr mkDoubleVar(const char *name);
static expr mkQuadVar(const char *name);

ADD
tests/alive-tv/fp/bfloat.srctgt.ll
+define i16 @src() {
+ %r = bitcast bfloat 3.0 to i16
+ ret i16 %r
+}
+
+define i16 @tgt() {
+ ret i16 16448
+}

fix #743: add support for bfloat