add support for [su]itofp & fpto[su]i
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -540,6 +540,10 @@ void ConversionOp::print(ostream &os) const {
case ZExt: str = "zext "; break;
case Trunc: str = "trunc "; break;
case BitCast: str = "bitcast "; break;
+ case SIntToFP: str = "sitofp "; break;
+ case UIntToFP: str = "uitofp "; break;
+ case FPToSInt: str = "fptosi "; break;
+ case FPToUInt: str = "fptoui "; break;
case Ptr2Int: str = "ptrtoint "; break;
case Int2Ptr: str = "int2ptr "; break;
}
@@ -574,6 +578,18 @@ StateValue ConversionOp::toSMT(State &s) const {
else
UNREACHABLE();
break;
+ case SIntToFP:
+ newval = v.sint2fp(getType().getDummyValue(false).value);
+ break;
+ case UIntToFP:
+ newval = v.uint2fp(getType().getDummyValue(false).value);
+ break;
+ case FPToSInt:
+ newval = v.fp2sint(to_bw);
+ break;
+ case FPToUInt:
+ newval = v.fp2uint(to_bw);
+ break;
case Ptr2Int:
newval = s.getMemory().ptr2int(v).zextOrTrunc(getType().bits());
break;
@@ -603,6 +619,17 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
c = getType().enforceIntOrPtrOrVectorType() &&
getType().sizeVar() == val->getType().sizeVar();
break;
+ case SIntToFP:
+ case UIntToFP:
+ // FIXME: output is vector iff input is vector
+ c = getType().enforceFloatOrVectorType() &&
+ val->getType().enforceIntOrVectorType();
+ break;
+ case FPToSInt:
+ case FPToUInt:
+ c = getType().enforceIntOrVectorType() &&
+ val->getType().enforceFloatOrVectorType();
+ break;
case Ptr2Int:
c = getType().enforceIntType() &&
val->getType().enforcePtrType();

MODIFY
ir/instr.h
ir/instr.h
@@ -100,7 +100,8 @@ public:
class ConversionOp final : public Instr {
public:
- enum Op { SExt, ZExt, Trunc, BitCast, Ptr2Int, Int2Ptr };
+ enum Op { SExt, ZExt, Trunc, BitCast, SIntToFP, UIntToFP, FPToSInt, FPToUInt,
+ Ptr2Int, Int2Ptr };
private:
Value *val;
@@ -350,7 +351,6 @@ public:
};
-// TODO: only supports alloca for now
class Alloc final : public Instr {
Value *size;
unsigned align;
@@ -366,6 +366,7 @@ public:
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
};
+
class Malloc final : public Instr {
Value *size;
public:

MODIFY
ir/type.cpp
ir/type.cpp
@@ -130,18 +130,14 @@ expr Type::enforceIntType(unsigned bits) const {
return false;
}
-expr Type::enforceIntOrVectorType() const {
- return false;
+expr Type::enforceIntType() const {
+ return enforceIntType(0);
}
expr Type::enforceIntOrPtrType() const {
return enforceIntType() || enforcePtrType();
}
-expr Type::enforceIntOrPtrOrVectorType() const {
- return false;
-}
-
expr Type::enforcePtrType() const {
return false;
}
@@ -158,6 +154,26 @@ expr Type::enforceFloatType() const {
return false;
}
+expr Type::enforceVectorType(expr(Type::*elementTy)() const) const {
+ return false;
+}
+
+expr Type::enforceScalarOrVectorType(expr(Type::*elementTy)() const) const {
+ return (this->*elementTy)() || enforceVectorType(elementTy);
+}
+
+expr Type::enforceIntOrVectorType() const {
+ return enforceScalarOrVectorType(&Type::enforceIntType);
+}
+
+expr Type::enforceIntOrPtrOrVectorType() const {
+ return enforceScalarOrVectorType(&Type::enforceIntOrPtrType);
+}
+
+expr Type::enforceFloatOrVectorType() const {
+ return enforceScalarOrVectorType(&Type::enforceFloatType);
+}
+
const FloatType* Type::getAsFloatType() const {
return nullptr;
}
@@ -279,14 +295,6 @@ expr IntType::enforceIntType(unsigned bits) const {
return bits ? sizeVar() == bits : true;
}
-expr IntType::enforceIntOrVectorType() const {
- return true;
-}
-
-expr IntType::enforceIntOrPtrOrVectorType() const {
- return true;
-}
-
pair<expr, expr>
IntType::refines(const StateValue &src, const StateValue &tgt) const {
return { src.non_poison.implies(tgt.non_poison),
@@ -476,14 +484,6 @@ bool PtrType::isPtrType() const {
return true;
}
-expr PtrType::enforceIntOrVectorType() const {
- return false;
-}
-
-expr PtrType::enforceIntOrPtrOrVectorType() const {
- return true;
-}
-
expr PtrType::enforcePtrType() const {
return true;
}
@@ -737,12 +737,8 @@ bool VectorType::isVectorType() const {
return true;
}
-expr VectorType::enforceIntOrVectorType() const {
- return children[0]->enforceIntType();
-}
-
-expr VectorType::enforceIntOrPtrOrVectorType() const {
- return children[0]->enforceIntOrPtrType();
+expr VectorType::enforceVectorType(expr(Type::*elementTy)() const) const {
+ return (children[0]->*elementTy)();
}
void VectorType::print(ostream &os) const {
@@ -950,16 +946,6 @@ expr SymbolicType::enforceIntType(unsigned bits) const {
return isInt() && (i ? i->enforceIntType(bits) : false);
}
-expr SymbolicType::enforceIntOrVectorType() const {
- return isInt() ||
- (isVector() && (v ? v->enforceIntOrPtrOrVectorType() : false));
-}
-
-expr SymbolicType::enforceIntOrPtrOrVectorType() const {
- return isInt() || isPtr() ||
- (isVector() && (v ? v->enforceIntOrPtrOrVectorType() : false));
-}
-
expr SymbolicType::enforcePtrType() const {
return isPtr();
}
@@ -978,6 +964,10 @@ expr SymbolicType::enforceFloatType() const {
return isFloat();
}
+expr SymbolicType::enforceVectorType(expr(Type::*elementTy)() const) const {
+ return v ? (isVector() && v->enforceVectorType(elementTy)) : false;
+}
+
const FloatType* SymbolicType::getAsFloatType() const {
return &*f;
}

MODIFY
ir/type.h
ir/type.h
@@ -58,16 +58,24 @@ public:
virtual bool isVectorType() const;
bool isAggregateType() const;
- virtual smt::expr enforceIntType(unsigned bits = 0) const;
- virtual smt::expr enforceIntOrVectorType() const;
+ virtual smt::expr enforceIntType(unsigned bits) const;
+ smt::expr enforceIntType() const;
smt::expr enforceIntOrPtrType() const;
- virtual smt::expr enforceIntOrPtrOrVectorType() const;
virtual smt::expr enforcePtrType() const;
virtual smt::expr enforceStructType() const;
virtual smt::expr enforceAggregateType(
std::vector<Type*> *element_types = nullptr) const;
virtual smt::expr enforceFloatType() const;
+ virtual smt::expr enforceVectorType(
+ smt::expr (Type::*elementTy)() const) const;
+ smt::expr enforceScalarOrVectorType(
+ smt::expr(Type::*elementTy)() const) const;
+
+ smt::expr enforceIntOrVectorType() const;
+ smt::expr enforceIntOrPtrOrVectorType() const;
+ smt::expr enforceFloatOrVectorType() const;
+
virtual const FloatType* getAsFloatType() const;
virtual const AggregateType* getAsAggregateType() const;
virtual const StructType* getAsStructType() const;
@@ -130,8 +138,6 @@ public:
void fixup(const smt::Model &m) override;
bool isIntType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
- smt::expr enforceIntOrVectorType() const override;
- smt::expr enforceIntOrPtrOrVectorType() const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
@@ -193,8 +199,6 @@ public:
smt::expr sameType(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
bool isPtrType() const override;
- smt::expr enforceIntOrVectorType() const override;
- smt::expr enforceIntOrPtrOrVectorType() const override;
smt::expr enforcePtrType() const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
@@ -262,8 +266,8 @@ public:
smt::expr getTypeConstraints() const override;
bool isVectorType() const override;
- smt::expr enforceIntOrVectorType() const override;
- smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr
+ enforceVectorType(smt::expr(Type::*elementTy)() const) const override;
void print(std::ostream &os) const override;
};
@@ -311,13 +315,13 @@ public:
bool isStructType() const override;
bool isVectorType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
- smt::expr enforceIntOrVectorType() const override;
- smt::expr enforceIntOrPtrOrVectorType() const override;
smt::expr enforcePtrType() const override;
smt::expr enforceStructType() const override;
smt::expr enforceAggregateType(
std::vector<Type*> *element_types) const override;
smt::expr enforceFloatType() const override;
+ smt::expr
+ enforceVectorType(smt::expr(Type:: *elementTy)() const) const override;
const FloatType* getAsFloatType() const override;
const AggregateType* getAsAggregateType() const override;
const StructType* getAsStructType() const override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -155,6 +155,10 @@ public:
case llvm::Instruction::ZExt: op = ConversionOp::ZExt; break;
case llvm::Instruction::Trunc: op = ConversionOp::Trunc; break;
case llvm::Instruction::BitCast: op = ConversionOp::BitCast; break;
+ case llvm::Instruction::SIToFP: op = ConversionOp::SIntToFP; break;
+ case llvm::Instruction::UIToFP: op = ConversionOp::UIntToFP; break;
+ case llvm::Instruction::FPToSI: op = ConversionOp::FPToSInt; break;
+ case llvm::Instruction::FPToUI: op = ConversionOp::FPToUInt; break;
case llvm::Instruction::PtrToInt: op = ConversionOp::Ptr2Int; break;
case llvm::Instruction::IntToPtr: op = ConversionOp::Int2Ptr; break;
default:

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1084,6 +1084,32 @@ expr expr::BV2float(const expr &type) const {
return simplify_const(Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort()), *this);
}
+expr expr::fp2sint(unsigned bits) const {
+ C();
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm, ast(), bits), *this);
+}
+
+expr expr::fp2uint(unsigned bits) const {
+ C();
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm, ast(), bits), *this);
+}
+
+expr expr::sint2fp(const expr &type) const {
+ C(type);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return simplify_const(Z3_mk_fpa_to_fp_signed(ctx(), rm, ast(), type.sort()),
+ *this);
+}
+
+expr expr::uint2fp(const expr &type) const {
+ C(type);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return simplify_const(Z3_mk_fpa_to_fp_unsigned(ctx(), rm, ast(), type.sort()),
+ *this);
+}
+
expr expr::mkUF(const char *name, const vector<expr> &args, const expr &range) {
C2(range);
auto num_args = args.size();

MODIFY
smt/expr.h
smt/expr.h
@@ -240,6 +240,11 @@ public:
expr float2Real() const;
expr BV2float(const expr &type) const;
+ expr fp2sint(unsigned bits) const;
+ expr fp2uint(unsigned bits) const;
+ expr sint2fp(const expr &type) const;
+ expr uint2fp(const expr &type) const;
+
// we don't expose SMT expr types, so range must be passed as a dummy value
// of the desired type
static expr mkUF(const char *name, const std::vector<expr> &args,

ADD
tests/unit/fp-casts.opt
+Name: sitofp
+%r = sitofp -1
+ =>
+%r = -1.0
+
+Name: uitofp
+%r = uitofp i8 -1
+ =>
+%r = 255.0
+
+Name: sitofp
+%r = fptosi -1.0
+ =>
+%r = -1
+
+Name: sitofp
+%r = fptoui 255.0 to i8
+ =>
+%r = -1

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -236,6 +236,7 @@ space+ {
"fdiv" { return FDIV; }
"frem" { return FREM; }
"fcmp" { return FCMP; }
+"fneg" { return FNEG; }
"oeq" { return OEQ; }
"ogt" { return OGT; }
"oge" { return OGE; }
@@ -246,7 +247,10 @@ space+ {
"ueq" { return UEQ; }
"une" { return UNE; }
"uno" { return UNO; }
-"fneg" { return FNEG; }
+"fptosi" { return FPTOSI; }
+"fptoui" { return FPTOUI; }
+"sitofp" { return SITOFP; }
+"uitofp" { return UITOFP; }
"half" { return HALF;}
"float" { return FLOAT;}
"double" { return DOUBLE;}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -740,6 +740,10 @@ static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
case SEXT: op = ConversionOp::SExt; break;
case ZEXT: op = ConversionOp::ZExt; break;
case TRUNC: op = ConversionOp::Trunc; break;
+ case SITOFP: op = ConversionOp::SIntToFP; break;
+ case UITOFP: op = ConversionOp::UIntToFP; break;
+ case FPTOSI: op = ConversionOp::FPToSInt; break;
+ case FPTOUI: op = ConversionOp::FPToUInt; break;
default:
UNREACHABLE();
}
@@ -939,6 +943,10 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case SEXT:
case ZEXT:
case TRUNC:
+ case SITOFP:
+ case UITOFP:
+ case FPTOSI:
+ case FPTOUI:
return parse_conversionop(name, t);
case SELECT:
return parse_select(name);
@@ -966,6 +974,7 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case REGISTER:
return parse_copyop(name, t);
default:
+ tokenizer.unget(t);
return nullptr;
}
UNREACHABLE();
@@ -1008,8 +1017,9 @@ static void parse_fn(Function &f) {
auto i = parse_instr(name);
if (!i) {
- tokenizer.unget(t);
+ if (name.empty())
goto exit;
+ error("Instruction expected", *tokenizer);
}
if (!name.empty()) {

MODIFY
tools/tokens.h
tools/tokens.h
@@ -36,6 +36,8 @@ TOKEN(FLOAT)
TOKEN(FMUL)
TOKEN(FNEG)
TOKEN(FP_NUM)
+TOKEN(FPTOSI)
+TOKEN(FPTOUI)
TOKEN(FREEZE)
TOKEN(FREE)
TOKEN(FREM)
@@ -83,6 +85,7 @@ TOKEN(SEXT)
TOKEN(SGE)
TOKEN(SGT)
TOKEN(SHL)
+TOKEN(SITOFP)
TOKEN(SLE)
TOKEN(SLT)
TOKEN(SMUL_OVERFLOW)
@@ -100,6 +103,7 @@ TOKEN(UDIV)
TOKEN(UEQ)
TOKEN(UGE)
TOKEN(UGT)
+TOKEN(UITOFP)
TOKEN(ULE)
TOKEN(ULT)
TOKEN(UMUL_OVERFLOW)

add support for [su]itofp & fpto[su]i