Skip to content

Commit

Permalink
fix #922: implement support for nofpclass in fn args and ret value
Browse files Browse the repository at this point in the history
  • Loading branch information
@nunoplopes
nunoplopes committed Jul 22, 2023
1 parent d0c6800 commit 8f12144
Show file tree
Hide file tree
Showing 5 changed files with 88 additions and 76 deletions.
44 changes: 43 additions & 1 deletion ir/attrs.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ ostream& operator<<(ostream &os, const ParamAttrs &attr) {
os << "dereferenceable(" << attr.derefBytes << ") ";
if (attr.has(ParamAttrs::NoUndef))
os << "noundef ";
if (attr.has(ParamAttrs::NoFPClass))
os << " nofpclass(" << attr.nofpclass << ')';
if (attr.has(ParamAttrs::Align))
os << "align(" << attr.align << ") ";
if (attr.has(ParamAttrs::Returned))
Expand Down Expand Up @@ -80,6 +82,8 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
os << " nofree";
if (attr.has(FnAttrs::NoUndef))
os << " noundef";
if (attr.has(FnAttrs::NoFPClass))
os << " nofpclass(" << attr.nofpclass << ')';
if (attr.has(FnAttrs::Align))
os << " align(" << attr.align << ')';
if (attr.has(FnAttrs::NoThrow))
Expand Down Expand Up @@ -373,6 +377,11 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
}

StateValue ParamAttrs::encode(State &s, StateValue &&val, const Type &ty) const{
if (has(NoFPClass)) {
assert(ty.isFloatType());
val.non_poison &= !isfpclass(val.value, ty, nofpclass);
}

if (ty.isPtrType())
val.non_poison &=
encodePtrAttrs(s, val.value, getDerefBytes(), derefOrNullBytes, align,
Expand Down Expand Up @@ -473,11 +482,16 @@ bool FnAttrs::refinedBy(const FnAttrs &other) const {
StateValue FnAttrs::encode(State &s, StateValue &&val, const Type &ty,
const expr &allocsize,
Value *allocalign) const {
if (has(FnAttrs::NNaN)) {
if (has(NNaN)) {
assert(ty.isFloatType());
val.non_poison &= !ty.getAsFloatType()->getFloat(val.value).isNaN();
}

if (has(NoFPClass)) {
assert(ty.isFloatType());
val.non_poison &= !isfpclass(val.value, ty, nofpclass);
}

if (ty.isPtrType())
val.non_poison &=
encodePtrAttrs(s, val.value, derefBytes, derefOrNullBytes, align,
Expand All @@ -492,6 +506,34 @@ StateValue FnAttrs::encode(State &s, StateValue &&val, const Type &ty,
}


expr isfpclass(const expr &v, const Type &ty, uint16_t mask) {
auto *fpty = ty.getAsFloatType();
auto a = fpty->getFloat(v);
OrExpr result;
if (mask & (1 << 0))
result.add(fpty->isNaN(v, true));
if (mask & (1 << 1))
result.add(fpty->isNaN(v, false));
if (mask & (1 << 2))
result.add(a.isFPNegative() && a.isInf());
if (mask & (1 << 3))
result.add(a.isFPNegative() && a.isFPNormal());
if (mask & (1 << 4))
result.add(a.isFPNegative() && a.isFPSubNormal());
if (mask & (1 << 5))
result.add(a.isFPNegZero());
if (mask & (1 << 6))
result.add(a.isFPZero() && !a.isFPNegative());
if (mask & (1 << 7))
result.add(!a.isFPNegative() && a.isFPSubNormal());
if (mask & (1 << 8))
result.add(!a.isFPNegative() && a.isFPNormal());
if (mask & (1 << 9))
result.add(!a.isFPNegative() && a.isInf());
return std::move(result)();
}


ostream& operator<<(ostream &os, const FastMathFlags &fm) {
if (fm.flags == FastMathFlags::FastMath)
return os << "fast ";
Expand Down
9 changes: 7 additions & 2 deletions ir/attrs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,14 +64,15 @@ class ParamAttrs final {
NoUndef = 1<<6, Align = 1<<7, Returned = 1<<8,
NoAlias = 1<<9, DereferenceableOrNull = 1<<10,
AllocPtr = 1<<11, AllocAlign = 1<<12,
ZeroExt = 1<<13, SignExt = 1<<14};
ZeroExt = 1<<13, SignExt = 1<<14, NoFPClass = 1<<15 };

ParamAttrs(unsigned bits = None) : bits(bits) {}

uint64_t derefBytes = 0; // Dereferenceable
uint64_t derefOrNullBytes = 0; // DereferenceableOrNull
uint64_t blockSize = 0; // exact block size for e.g. byval args
uint64_t align = 1;
uint16_t nofpclass = 0;

bool has(Attribute a) const { return (bits & a) != 0; }
void set(Attribute a) { bits |= (unsigned)a; }
Expand Down Expand Up @@ -125,7 +126,7 @@ class FnAttrs final {
DereferenceableOrNull = 1 << 10,
NullPointerIsValid = 1 << 11,
AllocSize = 1 << 12, ZeroExt = 1<<13,
SignExt = 1<<14 };
SignExt = 1<<14, NoFPClass = 1<<15, };

FnAttrs(unsigned bits = None) : bits(bits) {}

Expand All @@ -143,6 +144,8 @@ class FnAttrs final {

std::string allocfamily;

uint16_t nofpclass = 0;

void add(AllocKind k) { allockind |= (uint8_t)k; }
bool has(AllocKind k) const { return allockind & (uint8_t)k; }
bool isAlloc() const { return allockind != 0; }
Expand Down Expand Up @@ -209,4 +212,6 @@ struct FpExceptionMode final {
friend std::ostream& operator<<(std::ostream &os, FpExceptionMode ex);
};

smt::expr isfpclass(const smt::expr &v, const Type &ty, uint16_t mask);

}
63 changes: 11 additions & 52 deletions ir/instr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
assert((flags & Exact) == flags);
break;
default:
assert((flags & NoUndef) == flags);
assert(flags == 0);
break;
}
}
Expand All @@ -137,7 +137,7 @@ bool BinOp::propagatesPoison() const {
}

bool BinOp::hasSideEffects() const {
return isDivOrRem() || (flags & NoUndef);
return isDivOrRem();
}

void BinOp::rauw(const Value &what, Value &with) {
Expand Down Expand Up @@ -191,8 +191,6 @@ void BinOp::print(ostream &os) const {
if (flags & Exact)
os << "exact ";
os << *lhs << ", " << rhs->getName();
if (flags & NoUndef)
os << ", !noundef";
}

static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
Expand Down Expand Up @@ -451,33 +449,25 @@ StateValue BinOp::toSMT(State &s) const {
break;
}

bool noundef = flags & NoUndef;
function<pair<StateValue,StateValue>(const expr&, const expr&, const expr&,
const expr&)> zip_op;
if (vertical_zip) {
zip_op = [&](auto &a, auto &ap, auto &b, auto &bp) {
auto [v1, v2] = fn(a, ap, b, bp);
expr non_poison = ap && bp;
if (noundef) {
s.addUB(std::move(non_poison));
non_poison = true;
}
StateValue sv1(std::move(v1), expr(non_poison));
return make_pair(std::move(sv1), StateValue(std::move(v2), std::move(non_poison)));
return make_pair(std::move(sv1),
StateValue(std::move(v2), std::move(non_poison)));
};
} else {
scalar_op = [&](auto &a, auto &ap, auto &b, auto &bp) -> StateValue {
auto [v, np] = fn(a, ap, b, bp);
if (noundef) {
s.addUB(std::move(np));
np = true;
}
return { std::move(v), ap && bp && np };
};
}

auto &a = s.getVal(*lhs, noundef);
auto &b = s.getVal(*rhs, isDivOrRem() || noundef);
auto &a = s[*lhs];
auto &b = s.getVal(*rhs, isDivOrRem());

if (lhs->getType().isVectorType()) {
auto retty = getType().getAsAggregateType();
Expand Down Expand Up @@ -1480,32 +1470,9 @@ StateValue TestOp::toSMT(State &s) const {
switch (op) {
case Is_FPClass:
fn = [&](const expr &v, const Type &ty) -> expr {
uint64_t n;
ENSURE(b.value.isUInt(n) && b.non_poison.isTrue());
auto *fpty = ty.getAsFloatType();
auto a = fpty->getFloat(v);
OrExpr result;
if (n & (1 << 0))
result.add(fpty->isNaN(v, true));
if (n & (1 << 1))
result.add(fpty->isNaN(v, false));
if (n & (1 << 2))
result.add(a.isFPNegative() && a.isInf());
if (n & (1 << 3))
result.add(a.isFPNegative() && a.isFPNormal());
if (n & (1 << 4))
result.add(a.isFPNegative() && a.isFPSubNormal());
if (n & (1 << 5))
result.add(a.isFPNegZero());
if (n & (1 << 6))
result.add(a.isFPZero() && !a.isFPNegative());
if (n & (1 << 7))
result.add(!a.isFPNegative() && a.isFPSubNormal());
if (n & (1 << 8))
result.add(!a.isFPNegative() && a.isFPNormal());
if (n & (1 << 9))
result.add(!a.isFPNegative() && a.isInf());
return result().toBVBool();
uint64_t mask;
ENSURE(b.value.isUInt(mask) && b.non_poison.isTrue());
return isfpclass(v, ty, mask).toBVBool();
};
break;
}
Expand Down Expand Up @@ -1693,7 +1660,7 @@ bool FpConversionOp::propagatesPoison() const {
}

bool FpConversionOp::hasSideEffects() const {
return flags & NoUndef;
return false;
}

void FpConversionOp::rauw(const Value &what, Value &with) {
Expand All @@ -1718,13 +1685,10 @@ void FpConversionOp::print(ostream &os) const {
os << ", rounding=" << rm;
if (!ex.ignore())
os << ", exceptions=" << ex;
if (flags & NoUndef)
os << ", !noundef";
}

StateValue FpConversionOp::toSMT(State &s) const {
bool noundef = flags & NoUndef;
auto &v = s.getVal(*val, noundef);
auto &v = s[*val];
function<StateValue(const expr &, const Type &, FpRoundingMode)> fn;

switch (op) {
Expand Down Expand Up @@ -1810,11 +1774,6 @@ StateValue FpConversionOp::toSMT(State &s) const {
: fn(val, to_type, rm);
np.add(std::move(ret.non_poison));

if (noundef) {
s.addUB(np());
np.reset();
}

return { to_type.isFloatType()
? to_type.getAsFloatType()->fromFloat(s, ret.value)
: std::move(ret.value), np()};
Expand Down
12 changes: 3 additions & 9 deletions ir/instr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,7 @@ class BinOp final : public Instr {
SAdd_Overflow, UAdd_Overflow, SSub_Overflow, USub_Overflow,
SMul_Overflow, UMul_Overflow,
And, Or, Xor, Cttz, Ctlz, UMin, UMax, SMin, SMax, Abs };
enum Flags { None = 0, NSW = 1 << 0, NUW = 1 << 1, Exact = 1 << 2,
NoUndef = 1 << 3 };
enum Flags { None = 0, NSW = 1 << 0, NUW = 1 << 1, Exact = 1 << 2 };

private:
Value *lhs, *rhs;
Expand Down Expand Up @@ -288,21 +287,16 @@ class FpConversionOp final : public Instr {
enum Op { SIntToFP, UIntToFP, FPToSInt, FPToUInt, FPExt, FPTrunc, LRInt,
LRound };

enum Flags { None = 0, NoUndef = 1<<0 };

private:
Value *val;
Op op;
FpRoundingMode rm;
FpExceptionMode ex;
unsigned flags;

public:
FpConversionOp(Type &type, std::string &&name, Value &val, Op op,
FpRoundingMode rm = {}, FpExceptionMode ex = {},
unsigned flags = None)
: Instr(type, std::move(name)), val(&val), op(op), rm(rm), ex(ex),
flags(flags) {}
FpRoundingMode rm = {}, FpExceptionMode ex = {})
: Instr(type, std::move(name)), val(&val), op(op), rm(rm), ex(ex) {}

std::vector<Value*> operands() const override;
bool propagatesPoison() const override;
Expand Down
36 changes: 24 additions & 12 deletions llvm_util/llvm2alive.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,14 @@ string_view s(llvm::StringRef str) {
return ret; \
} while (0)

#define RETURN_IDENTIFIER_FNATTRS(op, attrs) \
do { \
auto ret = op; \
add_identifier(i, *ret.get()); \
if (attrs.has(FnAttrs::NoUndef)) \
BB->addInstr(make_unique<Assume>(*ret, Assume::WellDefined)); \
return ret; \
} while (0)


class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
Expand Down Expand Up @@ -853,11 +861,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}
FnAttrs attrs;
parse_fn_attrs(i, attrs);
unsigned flags = BinOp::None;
if (attrs.has(FnAttrs::NoUndef))
flags |= BinOp::NoUndef;
RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, op,
flags));
RETURN_IDENTIFIER_FNATTRS(
make_unique<BinOp>(*ty, value_name(i), *a, *b, op), attrs);
}
case llvm::Intrinsic::bitreverse:
case llvm::Intrinsic::bswap:
Expand Down Expand Up @@ -1067,13 +1072,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}
FnAttrs attrs;
parse_fn_attrs(i, attrs);
unsigned flags = FpConversionOp::None;
if (attrs.has(FnAttrs::NoUndef))
flags |= FpConversionOp::NoUndef;
RETURN_IDENTIFIER(make_unique<FpConversionOp>(*ty, value_name(i), *val,
op, parse_rounding(i),
parse_exceptions(i),
flags));
RETURN_IDENTIFIER_FNATTRS(
make_unique<FpConversionOp>(*ty, value_name(i), *val, op,
parse_rounding(i), parse_exceptions(i)),
attrs);
}
case llvm::Intrinsic::is_fpclass:
{
Expand Down Expand Up @@ -1353,6 +1355,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
attrs.set(ParamAttrs::NoUndef);
break;

case llvm::Attribute::NoFPClass:
attrs.set(ParamAttrs::NoFPClass);
attrs.nofpclass = (uint16_t)llvmattr.getNoFPClass();
break;

case llvm::Attribute::Returned:
attrs.set(ParamAttrs::Returned);
break;
Expand Down Expand Up @@ -1404,6 +1411,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
attrs.align = max(attrs.align, llvmattr.getAlignment()->value());
break;

case llvm::Attribute::NoFPClass:
attrs.set(FnAttrs::NoFPClass);
attrs.nofpclass = (uint16_t)llvmattr.getNoFPClass();
break;

default: break;
}
}
Expand Down

0 comments on commit 8f12144

Please sign in to comment.