Skip to content

Commit

Permalink
Merge branch 'AliveToolkit:master' into mutate
Browse files Browse the repository at this point in the history
  • Loading branch information
Hatsunespica authored Jun 10, 2024
2 parents bfc0a5d + f8d394d commit ccad38a
Show file tree
Hide file tree
Showing 13 changed files with 231 additions and 34 deletions.
57 changes: 39 additions & 18 deletions ir/instr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1584,7 +1584,7 @@ StateValue ConversionOp::toSMT(State &s) const {
unsigned trunc_bits = to_type.bits();
expr val_truncated = val.trunc(trunc_bits);
if (flags & NUW)
non_poison.add(val_truncated.zext(orig_bits - trunc_bits) == val);
non_poison.add(val.extract(orig_bits-1, trunc_bits) == 0);
if (flags & NSW)
non_poison.add(val_truncated.sext(orig_bits - trunc_bits) == val);
return {std::move(val_truncated), non_poison()};
Expand Down Expand Up @@ -3155,13 +3155,8 @@ check_ret_attributes(State &s, StateValue &&sv, const StateValue &returned_arg,
}

StateValue Return::toSMT(State &s) const {
StateValue retval;

auto &attrs = s.getFn().getFnAttrs();
if (attrs.poisonImpliesUB())
retval = s.getAndAddPoisonUB(*val, true);
else
retval = s[*val];
StateValue retval = s.getMaybeUB(*val, attrs.poisonImpliesUB());

s.addGuardableUB(s.getMemory().checkNocapture());

Expand Down Expand Up @@ -3311,9 +3306,9 @@ unique_ptr<Instr> Assume::dup(Function &f, const string &suffix) const {


AssumeVal::AssumeVal(Type &type, string &&name, Value &val,
vector<Value *> &&args0, Kind kind)
vector<Value *> &&args0, Kind kind, bool is_welldefined)
: Instr(type, std::move(name)), val(&val), args(std::move(args0)),
kind(kind) {
kind(kind), is_welldefined(is_welldefined) {
switch (kind) {
case Align:
assert(args.size() == 1);
Expand Down Expand Up @@ -3360,6 +3355,9 @@ void AssumeVal::print(ostream &os) const {
for (auto &arg: args) {
os << ", " << *arg;
}

if (is_welldefined)
os << ", welldefined";
}

StateValue AssumeVal::toSMT(State &s) const {
Expand Down Expand Up @@ -3401,7 +3399,7 @@ StateValue AssumeVal::toSMT(State &s) const {
break;
}

auto &v = s[*val];
auto &v = s.getMaybeUB(*val, is_welldefined);
if (auto agg = getType().getAsAggregateType()) {
vector<StateValue> vals;
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
Expand All @@ -3416,6 +3414,11 @@ StateValue AssumeVal::toSMT(State &s) const {
if (config::disallow_ub_exploitation)
s.addGuardableUB(expr(np));

if (is_welldefined) {
s.addUB(std::move(np));
np = true;
}

return { expr(v.value), v.non_poison && np };
}

Expand All @@ -3441,7 +3444,7 @@ expr AssumeVal::getTypeConstraints(const Function &f) const {

unique_ptr<Instr> AssumeVal::dup(Function &f, const string &suffix) const {
return make_unique<AssumeVal>(getType(), getName() + suffix, *val,
vector<Value*>(args), kind);
vector<Value*>(args), kind, is_welldefined);
}


Expand Down Expand Up @@ -3693,6 +3696,10 @@ void GEP::print(ostream &os) const {
os << getName() << " = gep ";
if (inbounds)
os << "inbounds ";
else if (nusw)
os << "nusw ";
if (nuw)
os << "nuw ";
os << *ptr;

for (auto &[sz, idx] : idxs) {
Expand All @@ -3711,19 +3718,32 @@ StateValue GEP::toSMT(State &s) const {
if (inbounds)
inbounds_np.add(ptr.inbounds());

expr offset_sum = expr::mkUInt(0, bits_for_offset);
for (auto &[sz, idx] : offsets) {
auto &[v, np] = idx;
auto multiplier = expr::mkUInt(sz, bits_for_offset);
auto val = v.sextOrTrunc(bits_for_offset);
auto inc = multiplier * val;

if (inbounds) {
if (sz != 0) {
idx_all_zeros.add(v == 0);
non_poison.add(val.sextOrTrunc(v.bits()) == v);
}
if (inbounds && sz != 0)
idx_all_zeros.add(v == 0);

if (nusw) {
non_poison.add(val.sextOrTrunc(v.bits()) == v);
non_poison.add(multiplier.mul_no_soverflow(val));
non_poison.add(ptr.addNoOverflow(inc));
non_poison.add(ptr.addNoUSOverflow(inc, inbounds));
if (!inbounds) {
// For non-inbounds gep, we have to explicitly check that adding the
// offsets without the base address also doesn't wrap.
non_poison.add(offset_sum.add_no_soverflow(inc));
offset_sum = offset_sum + inc;
}
}

if (nuw) {
non_poison.add(val.zextOrTrunc(v.bits()) == v);
non_poison.add(multiplier.mul_no_uoverflow(val));
non_poison.add(ptr.addNoUOverflow(inc, inbounds));
}

#ifndef NDEBUG
Expand Down Expand Up @@ -3793,7 +3813,8 @@ expr GEP::getTypeConstraints(const Function &f) const {
}

unique_ptr<Instr> GEP::dup(Function &f, const string &suffix) const {
auto dup = make_unique<GEP>(getType(), getName() + suffix, *ptr, inbounds);
auto dup = make_unique<GEP>(getType(), getName() + suffix, *ptr, inbounds,
nusw, nuw);
for (auto &[sz, idx] : idxs) {
dup->addIdx(sz, *idx);
}
Expand Down
16 changes: 13 additions & 3 deletions ir/instr.h
Original file line number Diff line number Diff line change
Expand Up @@ -631,10 +631,12 @@ class AssumeVal final : public Instr {
Value *val;
std::vector<Value*> args;
Kind kind;
bool is_welldefined;

public:
AssumeVal(Type &type, std::string &&name, Value &val,
std::vector<Value *> &&args, Kind kind);
std::vector<Value *> &&args, Kind kind,
bool is_welldefined = false);

std::vector<Value*> operands() const override;
bool propagatesPoison() const override;
Expand Down Expand Up @@ -768,14 +770,22 @@ class GEP final : public MemInstr {
Value *ptr;
std::vector<std::pair<uint64_t, Value*>> idxs;
bool inbounds;
bool nusw;
bool nuw;
public:
GEP(Type &type, std::string &&name, Value &ptr, bool inbounds)
: MemInstr(type, std::move(name)), ptr(&ptr), inbounds(inbounds) {}
GEP(Type &type, std::string &&name, Value &ptr, bool inbounds, bool nusw,
bool nuw)
: MemInstr(type, std::move(name)), ptr(&ptr), inbounds(inbounds),
nusw(nusw), nuw(nuw) {
nusw |= inbounds;
}

void addIdx(uint64_t obj_size, Value &idx);
Value& getPtr() const { return *ptr; }
auto& getIdxs() const { return idxs; }
bool isInBounds() const { return inbounds; }
bool hasNoUnsignedSignedWrap() const { return nusw; }
bool hasNoUnsignedWrap() const { return nuw; }

std::pair<uint64_t, uint64_t> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
Expand Down
12 changes: 10 additions & 2 deletions ir/pointer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -292,8 +292,16 @@ Pointer Pointer::maskOffset(const expr &mask) const {
getAttrs() };
}

expr Pointer::addNoOverflow(const expr &offset) const {
return getOffset().add_no_soverflow(offset);
expr Pointer::addNoUSOverflow(const expr &offset, bool offset_only) const {
if (offset_only)
return getOffset().add_no_soverflow(offset);
return getAddress().add_no_usoverflow(offset.sextOrTrunc(bits_ptr_address));
}

expr Pointer::addNoUOverflow(const expr &offset, bool offset_only) const {
if (offset_only)
return getOffset().add_no_uoverflow(offset);
return getAddress().add_no_uoverflow(offset.sextOrTrunc(bits_ptr_address));
}

expr Pointer::operator==(const Pointer &rhs) const {
Expand Down
3 changes: 2 additions & 1 deletion ir/pointer.h
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,8 @@ class Pointer {

Pointer maskOffset(const smt::expr &mask) const;

smt::expr addNoOverflow(const smt::expr &offset) const;
smt::expr addNoUSOverflow(const smt::expr &offset, bool offset_only) const;
smt::expr addNoUOverflow(const smt::expr &offset, bool offset_only) const;

smt::expr operator==(const Pointer &rhs) const;
smt::expr operator!=(const Pointer &rhs) const;
Expand Down
3 changes: 3 additions & 0 deletions ir/state.h
Original file line number Diff line number Diff line change
Expand Up @@ -210,6 +210,9 @@ class State {
// If undef_ub is true, UB is also added when val was undef
const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false,
bool ptr_compare = false);
const StateValue& getMaybeUB(const Value &val, bool is_UB) {
return is_UB ? getAndAddPoisonUB(val, true) : eval(val, false);
}
const StateValue& getVal(const Value &val, bool is_poison_ub);
const smt::expr& getWellDefinedPtr(const Value &val);

Expand Down
2 changes: 1 addition & 1 deletion llvm_util/cmd_args_def.h
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ config::src_unroll_cnt = opt_src_unrolling_factor;
config::tgt_unroll_cnt = opt_tgt_unrolling_factor;
#else
config::src_unroll_cnt = opt_unrolling_factor;
config::src_unroll_cnt = opt_unrolling_factor;
config::tgt_unroll_cnt = opt_unrolling_factor;
#endif
config::disable_undef_input = opt_disable_undef;
config::disable_poison_input = opt_disable_poison;
Expand Down
20 changes: 13 additions & 7 deletions llvm_util/llvm2alive.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -610,7 +610,9 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
if (!ty || !ptr)
return error(i);

auto gep = make_unique<GEP>(*ty, value_name(i), *ptr, i.isInBounds());
auto gep =
make_unique<GEP>(*ty, value_name(i), *ptr, i.isInBounds(),
i.hasNoUnsignedSignedWrap(), i.hasNoUnsignedWrap());
auto gep_struct_ofs = [&i, this](llvm::StructType *sty, llvm::Value *ofs) {
llvm::Value *vals[] = { llvm::ConstantInt::getFalse(i.getContext()), ofs };
return this->DL().getIndexedOffsetInType(sty, { vals, 2 });
Expand Down Expand Up @@ -854,7 +856,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
auto gep = make_unique<GEP>(
aptr->getType(),
"#align_adjustedptr" + to_string(alignopbundle_idx++),
*aptr, false);
*aptr, false, false, false);
gep->addIdx(-1ull, *get_operand(bundle.Inputs[2].get()));

aptr = gep.get();
Expand Down Expand Up @@ -1349,17 +1351,20 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}

unique_ptr<Instr>
handleRangeAttrNoInsert(const llvm::Attribute &attr, Value &val) {
handleRangeAttrNoInsert(const llvm::Attribute &attr, Value &val,
bool is_welldefined = false) {
auto CR = attr.getValueAsConstantRange();
vector<Value*> bounds{ make_intconst(CR.getLower()),
make_intconst(CR.getUpper()) };
return
make_unique<AssumeVal>(val.getType(), "%#range_" + val.getName(), val,
std::move(bounds), AssumeVal::Range);
std::move(bounds), AssumeVal::Range,
is_welldefined);
}

Value* handleRangeAttr(const llvm::Attribute &attr, Value &val) {
auto assume = handleRangeAttrNoInsert(attr, val);
Value* handleRangeAttr(const llvm::Attribute &attr, Value &val,
bool is_welldefined = false) {
auto assume = handleRangeAttrNoInsert(attr, val, is_welldefined);
auto ret = assume.get();
BB->addInstr(std::move(assume));
return ret;
Expand Down Expand Up @@ -1441,7 +1446,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
break;

case llvm::Attribute::Range:
newval = handleRangeAttr(llvmattr, val);
newval = handleRangeAttr(llvmattr, val,
aset.hasAttribute(llvm::Attribute::NoUndef));
break;

case llvm::Attribute::NoFPClass:
Expand Down
2 changes: 1 addition & 1 deletion scripts/opt-alive.sh.in
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ set -e
# attributor, function-attrs: inter procedural pass that deduces and/or propagates attributes
# metarenamer: anonymizes function names
# sample-profile: inlines functions
SKIP_TV_PASSES="argpromotion deadargelim globalopt hotcoldsplit inline ipconstprop ipsccp mergefunc partial-inliner function-specialization =tbaa loop-extract extract-blocks safe-stack place-safepoints attributor function-attrs metarenamer sample-profile lowertypetests extract-blocks openmp-opt-cgscc prune-eh tailcallelim iroutliner ctx-instr-lower globals-aa debug-pass-manager"
SKIP_TV_PASSES="argpromotion deadargelim globalopt hotcoldsplit inline ipconstprop ipsccp mergefunc partial-inliner function-specialization =tbaa loop-extract extract-blocks safe-stack place-safepoints attributor function-attrs metarenamer sample-profile lowertypetests extract-blocks openmp-opt-cgscc prune-eh tailcallelim iroutliner ctx-instr-lower expand-variadics globals-aa debug-pass-manager"

# see opt.cpp: shouldForceLegacyPM()
FORCE_OLD_NPM="codegenprepare interleaved-load-combine unreachableblockelim atomic-expand expandvp interleaved-access global-merge expand-reductions indirectbr-expand pre-isel-intrinsic-lowering loop-reduce expand-large-div-rem expand-large-fp-convert structurizecfg fix-irreducible expand-memcmp amdgpu-aa-wrapper aarch64-lit"
Expand Down
7 changes: 7 additions & 0 deletions smt/expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -854,6 +854,13 @@ expr expr::add_no_uoverflow(const expr &rhs) const {
return (zext(1) + rhs.zext(1)).sign() == 0;
}

expr expr::add_no_usoverflow(const expr &rhs) const {
if (min_leading_zeros() >= 1 && rhs.min_leading_zeros() >= 1)
return true;

return (zext(1) + rhs.sext(1)).sign() == 0;
}

expr expr::sub_no_soverflow(const expr &rhs) const {
if (min_leading_zeros() >= 1 && rhs.min_leading_zeros() >= 1)
return true;
Expand Down
1 change: 1 addition & 0 deletions smt/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,7 @@ class expr {

expr add_no_soverflow(const expr &rhs) const;
expr add_no_uoverflow(const expr &rhs) const;
expr add_no_usoverflow(const expr &rhs) const;
expr sub_no_soverflow(const expr &rhs) const;
expr sub_no_uoverflow(const expr &rhs) const;
expr mul_no_soverflow(const expr &rhs) const;
Expand Down
12 changes: 12 additions & 0 deletions tests/alive-tv/attrs/noundef_range.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
define i1 @src(i1 %1, i8 noundef range(i8 -32, -16) %2) {
%5 = trunc nuw nsw i8 %2 to i4
%6 = select i1 %1, i4 3, i4 %5
%7 = trunc i4 %6 to i1
ret i1 %7
}

define i1 @tgt(i1 %1, i8 noundef range(i8 -32, -16) %2) {
%5 = trunc i8 %2 to i1
%6 = or i1 %1, %5
ret i1 %6
}
Loading

0 comments on commit ccad38a

Please sign in to comment.