add support for fpext & fptrunc
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -770,6 +770,8 @@ void ConversionOp::print(ostream &os) const {
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 Ptr2Int: str = "ptrtoint "; break;
case Int2Ptr: str = "int2ptr "; break;
}
@@ -828,6 +830,12 @@ StateValue ConversionOp::toSMT(State &s) const {
!val.isInf() };
};
break;
+ case FPExt:
+ case FPTrunc:
+ fn = [](auto &&val, auto &to_type) -> StateValue {
+ return { val.float2Float(to_type.getDummyValue(false).value), true };
+ };
+ break;
case Ptr2Int:
fn = [&](auto &&val, auto &to_type) -> StateValue {
return { s.getMemory().ptr2int(val).zextOrTrunc(to_type.bits()), true };
@@ -904,6 +912,16 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
c = getType().enforceIntOrVectorType() &&
val->getType().enforceFloatOrVectorType();
break;
+ case FPExt:
+ c = getType().enforceFloatOrVectorType() &&
+ val->getType().enforceFloatOrVectorType() &&
+ val->getType().scalarSize().ult(getType().scalarSize());
+ break;
+ case FPTrunc:
+ c = getType().enforceFloatOrVectorType() &&
+ val->getType().enforceFloatOrVectorType() &&
+ val->getType().scalarSize().ugt(getType().scalarSize());
+ break;
case Ptr2Int:
c = getType().enforceIntOrVectorType() &&
val->getType().enforcePtrOrVectorType();

MODIFY
ir/instr.h
ir/instr.h
@@ -116,7 +116,7 @@ public:
class ConversionOp final : public Instr {
public:
enum Op { SExt, ZExt, Trunc, BitCast, SIntToFP, UIntToFP, FPToSInt, FPToUInt,
- Ptr2Int, Int2Ptr };
+ FPExt, FPTrunc, Ptr2Int, Int2Ptr };
private:
Value *val;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -624,12 +624,12 @@ AggregateType::AggregateType(string &&name, bool symbolic)
return;
// create symbolic type with a finite number of children
- unsigned num = 4;
- sym.resize(num);
- children.resize(num);
+ elements = 4;
+ sym.resize(elements);
+ children.resize(elements);
// FIXME: limitation below is for vectors; what about structs and arrays?
- for (unsigned i = 0; i < num; ++i) {
+ for (unsigned i = 0; i < elements; ++i) {
sym[i] = make_unique<SymbolicType>("v#" + to_string(i) + '_' + name,
(1 << SymbolicType::Int) |
(1 << SymbolicType::Float) |
@@ -642,6 +642,7 @@ AggregateType::AggregateType(string &&name, vector<Type*> &&vchildren,
vector<bool> &&vis_padding)
: Type(move(name)), children(move(vchildren)), is_padding(move(vis_padding)) {
assert(children.size() == is_padding.size());
+ elements = children.size();
}
expr AggregateType::numElements() const {
@@ -1033,6 +1034,22 @@ SymbolicType::SymbolicType(string &&name, unsigned type_mask)
} \
UNREACHABLE()
+#define DISPATCH_EXPR(call) \
+ expr ret; \
+ if (i) \
+ ret = i->call; \
+ if (f) \
+ ret = ret.isValid() ? expr::mkIf(isFloat(), f->call, ret) : f->call; \
+ if (p) \
+ ret = ret.isValid() ? expr::mkIf(isPtr(), p->call, ret) : p->call; \
+ if (a) \
+ ret = ret.isValid() ? expr::mkIf(isArray(), a->call, ret) : a->call; \
+ if (v) \
+ ret = ret.isValid() ? expr::mkIf(isVector(), v->call, ret) : v->call; \
+ if (s) \
+ ret = ret.isValid() ? expr::mkIf(isStruct(), s->call, ret) : s->call; \
+ return ret
+
unsigned SymbolicType::bits() const {
DISPATCH(bits(), UNREACHABLE());
}
@@ -1052,6 +1069,14 @@ expr SymbolicType::getTypeConstraints() const {
return c;
}
+expr SymbolicType::sizeVar() const {
+ DISPATCH_EXPR(sizeVar());
+}
+
+expr SymbolicType::scalarSize() const {
+ DISPATCH_EXPR(scalarSize());
+}
+
expr SymbolicType::operator==(const Type &b) const {
if (this == &b)
return true;

MODIFY
ir/type.h
ir/type.h
@@ -352,6 +352,8 @@ public:
unsigned bits() const override;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
+ smt::expr sizeVar() const override;
+ smt::expr scalarSize() const override;
smt::expr operator==(const Type &rhs) const;
void fixup(const smt::Model &m) override;
bool isIntType() const override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -207,6 +207,8 @@ public:
case llvm::Instruction::FPToUI: op = ConversionOp::FPToUInt; break;
case llvm::Instruction::PtrToInt: op = ConversionOp::Ptr2Int; break;
case llvm::Instruction::IntToPtr: op = ConversionOp::Int2Ptr; break;
+ case llvm::Instruction::FPExt: op = ConversionOp::FPExt; break;
+ case llvm::Instruction::FPTrunc: op = ConversionOp::FPTrunc; break;
default:
return error(i);
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1212,6 +1212,12 @@ expr expr::BV2float(const expr &type) const {
return simplify_const(Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort()), *this);
}
+expr expr::float2Float(const expr &type) const {
+ C(type);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return Z3_mk_fpa_to_fp_float(ctx(), rm, ast(), type.sort());
+}
+
expr expr::fp2sint(unsigned bits) const {
C();
auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());

MODIFY
smt/expr.h
smt/expr.h
@@ -245,6 +245,7 @@ public:
expr float2BV() const;
expr float2Real() const;
expr BV2float(const expr &type) const;
+ expr float2Float(const expr &type) const;
expr fp2sint(unsigned bits) const;
expr fp2uint(unsigned bits) const;

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -270,6 +270,8 @@ space+ {
"fptoui" { return FPTOUI; }
"sitofp" { return SITOFP; }
"uitofp" { return UITOFP; }
+"fpext" { return FPEXT; }
+"fptrunc" { return FPTRUNC; }
"ptrtoint" { return PTRTOINT; }
"half" { return HALF;}
"float" { return FLOAT;}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -784,6 +784,8 @@ static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
case UITOFP: op = ConversionOp::UIntToFP; break;
case FPTOSI: op = ConversionOp::FPToSInt; break;
case FPTOUI: op = ConversionOp::FPToUInt; break;
+ case FPEXT: op = ConversionOp::FPExt; break;
+ case FPTRUNC: op = ConversionOp::FPTrunc; break;
case PTRTOINT: op = ConversionOp::Ptr2Int; break;
default:
UNREACHABLE();
@@ -1025,6 +1027,8 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case UITOFP:
case FPTOSI:
case FPTOUI:
+ case FPEXT:
+ case FPTRUNC:
case PTRTOINT:
return parse_conversionop(name, t);
case SELECT:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -38,8 +38,10 @@ TOKEN(FLOAT)
TOKEN(FMUL)
TOKEN(FNEG)
TOKEN(FP_NUM)
+TOKEN(FPEXT)
TOKEN(FPTOSI)
TOKEN(FPTOUI)
+TOKEN(FPTRUNC)
TOKEN(FREEZE)
TOKEN(FREE)
TOKEN(FREM)

add support for fpext & fptrunc