TV: wire up float support
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -55,17 +55,14 @@ expr FloatConst::getTypeConstraints() const {
}
pair<expr, expr> FloatConst::toSMT_cnst() const {
+ expr e;
switch (getType().getAsFloatType()->getFpType()) {
- case FloatType::Double: {
- return { expr::mkDouble(val), true };
- }
- case FloatType::Float: {
- return { expr::mkFloat((float) val), true };
- }
- default:
- // TODO: support other fp types
- UNREACHABLE();
+ case FloatType::Half: e = expr::mkHalf((float)val); break;
+ case FloatType::Float: e = expr::mkFloat((float)val); break;
+ case FloatType::Double: e = expr::mkDouble(val); break;
+ case FloatType::Unknown: UNREACHABLE();
}
+ return { move(e), true };
}

MODIFY
ir/constant.h
ir/constant.h
@@ -33,6 +33,7 @@ public:
auto getInt() const { return std::get_if<int64_t>(&val); }
};
+
class FloatConst final : public Constant {
double val;
public:
@@ -42,6 +43,7 @@ public:
smt::expr getTypeConstraints() const override;
};
+
class ConstantInput final : public Constant {
public:
ConstantInput(Type &type, std::string &&name)

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -56,8 +56,12 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case USub_Overflow:
case SMul_Overflow:
case UMul_Overflow:
+ // TODO: add support for fast-math flags
case FAdd:
case FSub:
+ case FMul:
+ case FDiv:
+ case FRem:
assert(flags == 0);
break;
}
@@ -93,6 +97,9 @@ void BinOp::print(ostream &os) const {
case UMul_Overflow: str = "umul_overflow"; break;
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;
}
const char *flag = nullptr;
@@ -281,6 +288,18 @@ StateValue BinOp::toSMT(State &s) const {
case FSub:
val = a.fsub(b);
break;
+
+ case FMul:
+ val = a.fmul(b);
+ break;
+
+ case FDiv:
+ val = a.fdiv(b);
+ break;
+
+ case FRem:
+ val = a.frem(b);
+ break;
}
return { move(val), move(not_poison) };
@@ -314,6 +333,9 @@ expr BinOp::getTypeConstraints(const Function &f) const {
break;
case FAdd:
case FSub:
+ case FMul:
+ case FDiv:
+ case FRem:
instrconstr = getType().enforceFloatType() &&
getType() == lhs.getType() &&
getType() == rhs.getType();

MODIFY
ir/instr.h
ir/instr.h
@@ -31,7 +31,7 @@ public:
SAdd_Sat, UAdd_Sat, SSub_Sat, USub_Sat,
SAdd_Overflow, UAdd_Overflow, SSub_Overflow, USub_Overflow,
SMul_Overflow, UMul_Overflow,
- FAdd, FSub,
+ FAdd, FSub, FMul, FDiv, FRem,
And, Or, Xor, Cttz, Ctlz };
enum Flags { None = 0, NSW = 1, NUW = 2, NSWNUW = 3, Exact = 4 };

MODIFY
ir/type.cpp
ir/type.cpp
@@ -246,20 +246,12 @@ void IntType::print(ostream &os) const {
unsigned FloatType::bits() const {
switch (fpType) {
- case Quarter:
- return 8;
case Half:
return 16;
- case BFloat16:
- return 16;
case Float:
return 32;
case Double:
return 64;
- case IEEE80:
- return 80;
- case FP128:
- return 128;
case Unknown:
UNREACHABLE();
}
@@ -276,15 +268,10 @@ expr FloatType::sizeVar() const {
expr FloatType::getDummyValue() const {
switch (fpType) {
- case Float:
- return expr::mkFloat(0);
- case Double:
- return expr::mkDouble(0);
- case Unknown:
- UNREACHABLE();
- default:
- // TODO
- return {};
+ case Half: return expr::mkHalf(0);
+ case Float: return expr::mkFloat(0);
+ case Double: return expr::mkDouble(0);
+ case Unknown: UNREACHABLE();
}
UNREACHABLE();
}
@@ -313,7 +300,7 @@ void FloatType::fixup(const Model &m) {
return;
unsigned fp_typ = m.getUInt(sizeVar());
- assert(fp_typ >= Quarter && fp_typ <= FP128);
+ assert(fp_typ < (unsigned)Unknown);
fpType = FpType(fp_typ);
}
@@ -324,14 +311,11 @@ expr FloatType::enforceFloatType() const {
pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
expr var;
switch (fpType) {
+ case Half: var = expr::mkHalfVar(name); break;
case Float: var = expr::mkFloatVar(name); break;
case Double: var = expr::mkDoubleVar(name); break;
case Unknown: UNREACHABLE();
- default:
- // TODO
- UNREACHABLE();
}
-
return { var, { var } };
}
@@ -341,27 +325,15 @@ void FloatType::printVal(ostream &os, const expr &e) const {
void FloatType::print(ostream &os) const {
switch (fpType) {
- case Quarter:
- os << "quarter";
- break;
case Half:
os << "half";
break;
- case BFloat16:
- os << "bfloat16";
- break;
case Float:
os << "float";
break;
case Double:
os << "double";
break;
- case IEEE80:
- os << "ieee80";
- break;
- case FP128:
- os << "fp128";
- break;
case Unknown:
break;
}

MODIFY
ir/type.h
ir/type.h
@@ -113,7 +113,7 @@ public:
class FloatType final : public Type {
public:
enum FpType {
- Quarter, Half, BFloat16, Float, Double, IEEE80, FP128, Unknown
+ Half, Float, Double, Unknown
};
private:

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -23,6 +23,9 @@ unsigned value_id_counter; // for %0, %1, etc..
vector<unique_ptr<IntType>> int_types;
vector<unique_ptr<PtrType>> ptr_types;
+FloatType half_type("half", FloatType::Half);
+FloatType float_type("float", FloatType::Float);
+FloatType double_type("double", FloatType::Double);
// cache complex types
unordered_map<const llvm::Type*, unique_ptr<Type>> type_cache;
@@ -89,6 +92,12 @@ Type* llvm_type2alive(const llvm::Type *ty) {
return &Type::voidTy;
case llvm::Type::IntegerTyID:
return make_int_type(cast<llvm::IntegerType>(ty)->getBitWidth());
+ case llvm::Type::HalfTyID:
+ return &half_type;
+ case llvm::Type::FloatTyID:
+ return &float_type;
+ case llvm::Type::DoubleTyID:
+ return &double_type;
case llvm::Type::PointerTyID: {
// TODO: support for non-64 bits pointers
@@ -141,6 +150,23 @@ Value* get_operand(llvm::Value *v) {
return ret;
}
+ if (auto cnst = dyn_cast<llvm::ConstantFP>(v)) {
+ auto &apfloat = cnst->getValueAPF();
+ auto apint = apfloat.bitcastToAPInt();
+ double val;
+ if (apint.getBitWidth() == 32) {
+ val = apfloat.convertToFloat();
+ } else if (apint.getBitWidth() == 64) {
+ val = apfloat.convertToDouble();
+ } else // TODO
+ return nullptr;
+
+ auto c = make_unique<FloatConst>(*ty, val);
+ auto ret = c.get();
+ current_fn->addConstant(move(c));
+ return ret;
+ }
+
if (isa<llvm::UndefValue>(v)) {
auto val = make_unique<UndefValue>(*ty);
auto ret = val.get();
@@ -220,6 +246,11 @@ public:
case llvm::Instruction::And: alive_op = BinOp::And; break;
case llvm::Instruction::Or: alive_op = BinOp::Or; break;
case llvm::Instruction::Xor: alive_op = BinOp::Xor; break;
+ case llvm::Instruction::FAdd: alive_op = BinOp::FAdd; break;
+ case llvm::Instruction::FSub: alive_op = BinOp::FSub; break;
+ case llvm::Instruction::FMul: alive_op = BinOp::FMul; break;
+ case llvm::Instruction::FDiv: alive_op = BinOp::FDiv; break;
+ case llvm::Instruction::FRem: alive_op = BinOp::FRem; break;
default:
return error(i);
}
@@ -232,6 +263,10 @@ public:
if (isa<llvm::PossiblyExactOperator>(i) && i.isExact())
flags = BinOp::Exact;
+ // TODO: support FP fast-math stuff
+ if (isa<llvm::FPMathOperator>(i) && i.getFastMathFlags().any())
+ return error(i);
+
RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, alive_op,
(BinOp::Flags)flags));
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -174,6 +174,10 @@ expr expr::mkInt(const char *n, unsigned bits) {
return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr();
}
+expr expr::mkHalf(float n) {
+ return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()));
+}
+
expr expr::mkFloat(float n) {
return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx()));
}
@@ -199,6 +203,10 @@ expr expr::mkBoolVar(const char *name) {
return ::mkVar(name, Z3_mk_bool_sort(ctx()));
}
+expr expr::mkHalfVar(const char *name) {
+ return ::mkVar(name, Z3_mk_fpa_sort_half(ctx()));
+}
+
expr expr::mkFloatVar(const char *name) {
return ::mkVar(name, Z3_mk_fpa_sort_single(ctx()));
}
@@ -700,15 +708,34 @@ expr expr::ctpop() const {
// TODO: make rounding mode customizable
expr expr::fadd(const expr &rhs) const {
+ C(rhs);
auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
return Z3_mk_fpa_add(ctx(), rm, ast(), rhs());
}
expr expr::fsub(const expr &rhs) const {
+ C(rhs);
auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
return Z3_mk_fpa_sub(ctx(), rm, ast(), rhs());
}
+expr expr::fmul(const expr &rhs) const {
+ C(rhs);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return Z3_mk_fpa_mul(ctx(), rm, ast(), rhs());
+}
+
+expr expr::fdiv(const expr &rhs) const {
+ C(rhs);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return Z3_mk_fpa_div(ctx(), rm, ast(), rhs());
+}
+
+expr expr::frem(const expr &rhs) const {
+ C(rhs);
+ return Z3_mk_fpa_rem(ctx(), ast(), rhs());
+}
+
expr expr::operator&(const expr &rhs) const {
if (eq(rhs))
return *this;

MODIFY
smt/expr.h
smt/expr.h
@@ -73,11 +73,13 @@ public:
static expr mkUInt(uint64_t n, unsigned bits);
static expr mkInt(int64_t n, unsigned bits);
static expr mkInt(const char *n, unsigned bits);
- static expr mkDouble(double n);
+ static expr mkHalf(float n);
static expr mkFloat(float n);
+ static expr mkDouble(double n);
static expr mkVar(const char *name, const expr &type);
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);
+ static expr mkHalfVar(const char *name);
static expr mkFloatVar(const char *name);
static expr mkDoubleVar(const char *name);
@@ -199,6 +201,9 @@ public:
expr toBVBool() const;
expr fadd(const expr &rhs) const;
expr fsub(const expr &rhs) const;
+ expr fmul(const expr &rhs) const;
+ expr fdiv(const expr &rhs) const;
+ expr frem(const expr &rhs) const;
// we don't expose SMT expr types, so range must be passed as a dummy value
// of the desired type

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -222,8 +222,12 @@ re2c:yyfill:check = 0;
"umul_overflow" { return UMUL_OVERFLOW; }
"fadd" { return FADD; }
"fsub" { return FSUB; }
-"float" { return FLOAT_TYPE;}
-"double" { return DOUBLE_TYPE;}
+"fmul" { return FMUL; }
+"fdiv" { return FDIV; }
+"frem" { return FREM; }
+"half" { return HALF;}
+"float" { return FLOAT;}
+"double" { return DOUBLE;}
"unreachable" { return UNREACH; }
[a-zA-Z][a-zA-Z0-9]* {

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -34,8 +34,9 @@ static void error(const char *s, token t) {
}
static vector<unique_ptr<IntType>> int_types;
-static unique_ptr<FloatType> float_type;
-static unique_ptr<FloatType> double_type;
+static FloatType half_type("half", FloatType::Half);
+static FloatType float_type("float", FloatType::Float);
+static FloatType double_type("double", FloatType::Double);
static unordered_map<string, Value*> identifiers;
static Function *fn;
@@ -274,11 +275,14 @@ static Type& parse_type(bool optional = true) {
error("Int type too long: " + to_string(yylval.num));
return get_int_type(yylval.num);
- case DOUBLE_TYPE:
- return *double_type.get();
+ case HALF:
+ return half_type;
- case FLOAT_TYPE:
- return *float_type.get();
+ case FLOAT:
+ return float_type;
+
+ case DOUBLE:
+ return double_type;
default:
if (optional) {
@@ -787,15 +791,10 @@ vector<Transform> parse(string_view buf) {
parser_initializer::parser_initializer() {
int_types.resize(65);
int_types[1] = make_unique<IntType>("i1", 1);
-
- float_type = make_unique<FloatType>("float", FloatType::Float);
- double_type = make_unique<FloatType>("double", FloatType::Double);
}
parser_initializer::~parser_initializer() {
for_each(int_types.begin(), int_types.end(), [](auto &e) { e.reset(); });
- float_type.reset();
- double_type.reset();
sym_types.clear();
overflow_aggregate_types.clear();
}

MODIFY
tools/tokens.h
tools/tokens.h
@@ -22,20 +22,24 @@ TOKEN(CTPOP)
TOKEN(CTTZ)
TOKEN(CULT)
TOKEN(CUGT)
-TOKEN(DOUBLE_TYPE)
+TOKEN(DOUBLE)
TOKEN(EQ)
TOKEN(EQUALS)
TOKEN(EXACT)
TOKEN(EXTRACTVALUE)
TOKEN(FADD)
TOKEN(FALSE)
-TOKEN(FLOAT_TYPE)
+TOKEN(FDIV)
+TOKEN(FLOAT)
+TOKEN(FMUL)
TOKEN(FP_NUM)
TOKEN(FREEZE)
+TOKEN(FREM)
TOKEN(FSHL)
TOKEN(FSHR)
TOKEN(FSUB)
TOKEN(GLOBAL_NAME)
+TOKEN(HALF)
TOKEN(ICMP)
TOKEN(IDENTIFIER)
TOKEN(INT_TYPE)

TV: wire up float support