add support for fp128
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -46,6 +46,9 @@ FloatConst::FloatConst(Type &type, double val)
FloatConst::FloatConst(Type &type, uint64_t val)
: Constant(type, to_string(val)), val(val) {}
+FloatConst::FloatConst(Type &type, string val)
+ : Constant(type, string(val)), val(move(val)) {}
+
expr FloatConst::getTypeConstraints() const {
return Value::getTypeConstraints() &&
getType().enforceFloatType();
@@ -58,12 +61,17 @@ StateValue FloatConst::toSMT(State &s) const {
true };
}
+ if (auto n = get_if<string>(&val))
+ return { expr::mkNumber(n->c_str(), getType().getDummyValue(true).value),
+ true };
+
expr e;
double v = get<double>(val);
switch (getType().getAsFloatType()->getFpType()) {
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::Quad:
case FloatType::Unknown: UNREACHABLE();
}
return { move(e), true };

MODIFY
ir/constant.h
ir/constant.h
@@ -32,10 +32,11 @@ public:
class FloatConst final : public Constant {
- std::variant<double, uint64_t> val;
+ std::variant<double, uint64_t, std::string> val;
public:
FloatConst(Type &type, double val);
FloatConst(Type &type, uint64_t val);
+ FloatConst(Type &type, std::string val);
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints() const override;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -371,10 +371,11 @@ void IntType::print(ostream &os) const {
// total bits, exponent bits
-static array<pair<unsigned, unsigned>, 3> float_sizes = {
+static array<pair<unsigned, unsigned>, 4> float_sizes = {
/* Half */ make_pair(16, 5),
/* Float */ make_pair(32, 8),
/* Double */ make_pair(64, 11),
+ /* Quad */ make_pair(128, 15),
};
unsigned FloatType::bits() const {
@@ -483,6 +484,7 @@ StateValue FloatType::getDummyValue(bool non_poison) const {
case Half: e = expr::mkHalf(0); break;
case Float: e = expr::mkFloat(0); break;
case Double: e = expr::mkDouble(0); break;
+ case Quad: e = expr::mkQuad(0); break;
case Unknown: UNREACHABLE();
}
return { move(e), non_poison };
@@ -539,6 +541,7 @@ expr FloatType::mkInput(State &s, const char *name,
case Half: return expr::mkHalfVar(name);
case Float: return expr::mkFloatVar(name);
case Double: return expr::mkDoubleVar(name);
+ case Quad: return expr::mkQuadVar(name);
case Unknown: UNREACHABLE();
}
UNREACHABLE();
@@ -572,6 +575,9 @@ void FloatType::print(ostream &os) const {
case Double:
os << "double";
break;
+ case Quad:
+ os << "fp128";
+ break;
case Unknown:
break;
}

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

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -30,6 +30,7 @@ vector<unique_ptr<PtrType>> ptr_types;
FloatType half_type("half", FloatType::Half);
FloatType float_type("float", FloatType::Float);
FloatType double_type("double", FloatType::Double);
+FloatType quad_type("fp128", FloatType::Quad);
// cache complex types
unordered_map<const llvm::Type*, unique_ptr<Type>> type_cache;
@@ -122,6 +123,8 @@ Type* llvm_type2alive(const llvm::Type *ty) {
return &float_type;
case llvm::Type::DoubleTyID:
return &double_type;
+ case llvm::Type::FP128TyID:
+ return &quad_type;
case llvm::Type::PointerTyID: {
// TODO: support for non-64 bits pointers
@@ -268,6 +271,10 @@ Value* get_operand(llvm::Value *v,
case FloatType::Double:
c = make_unique<FloatConst>(*ty, apfloat.convertToDouble());
break;
+ case FloatType::Quad:
+ c = make_unique<FloatConst>(*ty,
+ apfloat.bitcastToAPInt().toString(10, true));
+ break;
case FloatType::Unknown:
UNREACHABLE();
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -202,6 +202,10 @@ expr expr::mkDouble(double n) {
return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx()));
}
+expr expr::mkQuad(double n) {
+ return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_quadruple(ctx()));
+}
+
expr expr::mkNaN(const expr &type) {
C2(type);
return Z3_mk_fpa_nan(ctx(), type.sort());
@@ -252,6 +256,10 @@ expr expr::mkDoubleVar(const char *name) {
return ::mkVar(name, Z3_mk_fpa_sort_double(ctx()));
}
+expr expr::mkQuadVar(const char *name) {
+ return ::mkVar(name, Z3_mk_fpa_sort_quadruple(ctx()));
+}
+
expr expr::mkFreshVar(const char *prefix, const expr &type) {
C2(type);
return Z3_mk_fresh_const(ctx(), prefix, type.sort());

MODIFY
smt/expr.h
smt/expr.h
@@ -90,6 +90,7 @@ public:
static expr mkHalf(float n);
static expr mkFloat(float n);
static expr mkDouble(double n);
+ static expr mkQuad(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);
@@ -98,6 +99,7 @@ public:
static expr mkHalfVar(const char *name);
static expr mkFloatVar(const char *name);
static expr mkDoubleVar(const char *name);
+ static expr mkQuadVar(const char *name);
static expr mkFreshVar(const char *prefix, const expr &type);
// return a constant value of the given type

ADD
tests/alive-tv/fp128.srctgt.ll
+define fp128 @src(fp128 %a) {
+ %cmp = fcmp ogt fp128 %a, 0xL40008000000000000000000000000000
+ br i1 %cmp, label %then, label %else
+
+then:
+ ret fp128 %a
+
+else:
+ ret fp128 0xLA0008000000000000000000000000000
+}

add support for fp128