Add support for FNeg
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -355,6 +355,7 @@ void UnaryOp::print(ostream &os) const {
case BitReverse: str = "bitreverse "; break;
case BSwap: str = "bswap "; break;
case Ctpop: str = "ctpop "; break;
+ case FNeg: str = "fneg "; break;
}
os << getName() << " = " << str << val;
@@ -377,6 +378,9 @@ StateValue UnaryOp::toSMT(State &s) const {
case Ctpop:
newval = v.ctpop();
break;
+ case FNeg:
+ newval = v.fneg();
+ break;
}
return { move(newval), expr(vp) };
}
@@ -392,6 +396,9 @@ expr UnaryOp::getTypeConstraints(const Function &f) const {
instrconstr &= getType().enforceIntOrVectorType();
case Copy:
break;
+ case FNeg:
+ instrconstr = getType().enforceFloatType();
+ break;
}
return Value::getTypeConstraints() &&

MODIFY
ir/instr.h
ir/instr.h
@@ -53,7 +53,7 @@ public:
class UnaryOp final : public Instr {
public:
- enum Op { Copy, BitReverse, BSwap, Ctpop };
+ enum Op { Copy, BitReverse, BSwap, Ctpop, FNeg };
private:
Value &val;

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -229,6 +229,17 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
public:
llvm2alive_(llvm::Function &f) : f(f) {}
+ RetTy visitUnaryOperator(llvm::UnaryOperator &i) {
+ PARSE_UNOP();
+ UnaryOp::Op op;
+ switch (i.getOpcode()) {
+ case llvm::Instruction::FNeg: op = UnaryOp::FNeg; break;
+ default:
+ return error(i);
+ }
+ RETURN_IDENTIFIER(make_unique<UnaryOp>(*ty, value_name(i), *val, op));
+ }
+
RetTy visitBinaryOperator(llvm::BinaryOperator &i) {
PARSE_BINOP();
BinOp::Op alive_op;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -814,6 +814,11 @@ expr expr::funo(const expr &rhs) const {
return !ford(rhs());
}
+expr expr::fneg() const {
+ C();
+ return Z3_mk_fpa_neg(ctx(), ast());
+}
+
expr expr::operator&(const expr &rhs) const {
if (eq(rhs))
return *this;

MODIFY
smt/expr.h
smt/expr.h
@@ -178,6 +178,7 @@ public:
expr fule(const expr &rhs) const;
expr fune(const expr &rhs) const;
expr funo(const expr &rhs) const;
+ expr fneg() const;
expr operator&(const expr &rhs) const;
expr operator|(const expr &rhs) const;

ADD
tests/unit/fp/fneg.opt
+Name: identity
+%t = fneg %a
+ =>
+%t = fneg %a
+
+
+Name: fsub 0.0 => neg
+%t = fsub -0.0, %a
+ =>
+%t = fneg %a
+
+
+Name: -a + 1.0 => 1.0 - a
+%t1 = fneg half %a
+%t = fadd half %t1, 1.0
+ =>
+%t1 = fneg half %a
+%t = fsub half 1.0, %a

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -236,6 +236,7 @@ re2c:yyfill:check = 0;
"ueq" { return UEQ; }
"une" { return UNE; }
"uno" { return UNO; }
+"fneg" { return FNEG; }
"half" { return HALF;}
"float" { return FLOAT;}
"double" { return DOUBLE;}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -515,6 +515,7 @@ static unique_ptr<Instr> parse_unaryop(string_view name, token op_token) {
case BITREVERSE: op = UnaryOp::BitReverse; break;
case BSWAP: op = UnaryOp::BSwap; break;
case CTPOP: op = UnaryOp::Ctpop; break;
+ case FNEG: op = UnaryOp::FNeg; break;
default:
UNREACHABLE();
}
@@ -737,6 +738,7 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case BITREVERSE:
case BSWAP:
case CTPOP:
+ case FNEG:
return parse_unaryop(name, t);
case FSHL:
case FSHR:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -33,6 +33,7 @@ TOKEN(FCMP)
TOKEN(FDIV)
TOKEN(FLOAT)
TOKEN(FMUL)
+TOKEN(FNEG)
TOKEN(FP_NUM)
TOKEN(FREEZE)
TOKEN(FREM)

Add support for FNeg (#75)