Skip to content

Commit

Permalink
fix #1021: implement support range attribute in fn args & ret val
Browse files Browse the repository at this point in the history
  • Loading branch information
@nunoplopes
nunoplopes committed Apr 8, 2024
1 parent 9b7d1ab commit f19cf14
Show file tree
Hide file tree
Showing 10 changed files with 94 additions and 62 deletions.
1 change: 1 addition & 0 deletions BugList.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ Please contact us or submit a PR if something is missing or inaccurate.
83. Vectorization of loop reduction introduces an aligned store incorrectly (https://llvm.org/PR65212)
84. InstCombine: incorrect sink of FP math through select changes NaN payload (https://llvm.org/PR74297)
85. InstCombine: fold of shuffle into fadd changes NaN payload (https://llvm.org/PR74326)
86. Attributor & Function-attrs mark function as noundef incorrectly due to return value not in range (https://llvm.org/PR88026)


### Bugs found in Z3
Expand Down
4 changes: 3 additions & 1 deletion ir/attrs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,9 @@ class ParamAttrs final {
NoAlias = 1<<9, DereferenceableOrNull = 1<<10,
AllocPtr = 1<<11, AllocAlign = 1<<12,
ZeroExt = 1<<13, SignExt = 1<<14, InReg = 1<<15,
NoFPClass = 1<<16, IsArg = 1<<17 };
NoFPClass = 1<<16,
IsArg = 1<<31 // used internally to make values as arguments
};

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

Expand Down
1 change: 1 addition & 0 deletions ir/function.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,7 @@ class Function final {
const BasicBlock& getFirstBB() const { return *BB_order[0]; }
BasicBlock& getFirstBB() { return *BB_order[0]; }
const BasicBlock& getSinkBB() const { return sink_bb; }
BasicBlock& getBB(unsigned idx) { return *BB_order.at(idx); }
BasicBlock& getBB(std::string_view name, bool push_front = false);
const BasicBlock& getBB(std::string_view name) const;
const BasicBlock& bbOf(const Instr &i) const;
Expand Down
10 changes: 7 additions & 3 deletions ir/value.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -187,9 +187,13 @@ static string attr_str(const ParamAttrs &attr) {
return std::move(ss).str();
}

Input::Input(Type &type, string &&name, ParamAttrs &&attributes)
: Value(type, attr_str(attributes) + name), smt_name(std::move(name)),
attrs(std::move(attributes)) {}
Input::Input(Type &type, string &&name)
: Value(type, std::string(name)), smt_name(std::move(name)) {}

void Input::setAttributes(ParamAttrs &&new_attrs) {
attrs = std::move(new_attrs);
setName(attr_str(attrs) + getName());
}

void Input::copySMTName(const Input &other) {
smt_name = other.smt_name;
Expand Down
3 changes: 2 additions & 1 deletion ir/value.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,8 @@ class Input final : public Value {
std::string getSMTName(unsigned child) const;
StateValue mkInput(State &s, const Type &ty, unsigned child) const;
public:
Input(Type &type, std::string &&name, ParamAttrs &&attrs = ParamAttrs::None);
Input(Type &type, std::string &&name);
void setAttributes(ParamAttrs &&new_attrs);
void copySMTName(const Input &other);
void print(std::ostream &os) const override;
bool hasAttribute(ParamAttrs::Attribute a) const { return attrs.has(a); }
Expand Down
57 changes: 38 additions & 19 deletions llvm_util/llvm2alive.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -379,7 +379,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
assert(fn->getFunctionType() ==
llvm::FunctionType::get(llvm::Type::getVoidTy(ctx),
{ llvm::Type::getInt1Ty(ctx) }, false));
return make_unique<Assume>(*args[0], Assume::AndNonPoison);
return make_unique<Assume>(*args.at(0), Assume::AndNonPoison);
}

Function::FnDecl decl;
Expand All @@ -395,8 +395,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
return error(i);

unsigned attr_argidx = llvm::AttributeList::FirstArgIndex + idx;
auto &arg = args.at(idx);
ParamAttrs pattr;
handleParamAttrs(attrs_fndef.getAttributes(attr_argidx), pattr, true);
handleParamAttrs(attrs_fndef.getAttributes(attr_argidx), pattr,
*arg, arg, true);
decl.inputs.emplace_back(ty, std::move(pattr));
}
alive_fn->addFnDecl(std::move(decl));
Expand Down Expand Up @@ -444,16 +446,16 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
unique_ptr<Instr> ret_val;

for (uint64_t argidx = 0, nargs = i.arg_size(); argidx < nargs; ++argidx) {
auto *arg = args[argidx];
auto &arg = args.at(argidx);
ParamAttrs pattr = argidx < param_attrs.size() ? param_attrs[argidx]
: ParamAttrs();

unsigned attr_argidx = llvm::AttributeList::FirstArgIndex + argidx;
approx |= !handleParamAttrs(attrs_callsite.getAttributes(attr_argidx),
pattr, true);
pattr, *arg, arg, true);
if (fn && argidx < fn->arg_size())
approx |= !handleParamAttrs(attrs_fndef.getAttributes(attr_argidx),
pattr, true);
pattr, *arg, arg, true);

if (i.paramHasAttr(argidx, llvm::Attribute::NoUndef)) {
if (i.getArgOperand(argidx)->getType()->isAggregateType())
Expand Down Expand Up @@ -711,6 +713,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
if (!ty || !val)
return error(i);

auto *Fn = i.getFunction();
if (Fn->hasRetAttribute(llvm::Attribute::Range))
val = handleRangeAttr(Fn->getRetAttribute(llvm::Attribute::Range), *val);

return make_unique<Return>(*ty, *val);
}

Expand Down Expand Up @@ -1336,24 +1342,29 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
return true;
}

Value* handleRangeAttr(const llvm::Attribute &attr, Value &val) {
auto CR = attr.getValueAsConstantRange();
vector<Value *> bounds{ make_intconst(CR.getLower()),
make_intconst(CR.getUpper()) };
auto assume
= make_unique<AssumeVal>(val.getType(), "%#range_" + val.getName(), val,
std::move(bounds), AssumeVal::Range);
auto ret = assume.get();
BB->addInstr(std::move(assume));
return ret;
}

// If is_callsite is true, encode attributes at call sites' params
// Otherwise, encode attributes at function definition's arguments
// TODO: Once attributes at a call site are fully supported, we should
// remove is_callsite flag
bool handleParamAttrs(const llvm::AttributeSet &aset, ParamAttrs &attrs,
bool is_callsite) {
Value &val, Value* &newval, bool is_callsite) {
bool precise = true;
for (const llvm::Attribute &llvmattr : aset) {
// To call getKindAsEnum, llvmattr should be enum or int attribute
// llvm/include/llvm/IR/Attributes.td has attribute types
if (!llvmattr.isEnumAttribute() && // e.g. nonnull
!llvmattr.isIntAttribute() && // e.g. dereferenceable
!llvmattr.isTypeAttribute()) // e.g. byval
continue;

switch (llvmattr.getKindAsEnum()) {
case llvm::Attribute::InReg:
attrs.set(ParamAttrs::InReg);
attrs.set(ParamAttrs::InReg);
break;

case llvm::Attribute::SExt:
Expand Down Expand Up @@ -1418,6 +1429,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
attrs.set(ParamAttrs::NoUndef);
break;

case llvm::Attribute::Range:
newval = handleRangeAttr(llvmattr, val);
break;

case llvm::Attribute::NoFPClass:
attrs.set(ParamAttrs::NoFPClass);
attrs.nofpclass = (uint16_t)llvmattr.getNoFPClass();
Expand Down Expand Up @@ -1641,6 +1656,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
reset_state(Fn);

alive_fn = &Fn;
BB = &Fn.getBB("#init", true);

auto &attrs = Fn.getFnAttrs();
vector<ParamAttrs> param_attrs;
Expand All @@ -1653,15 +1669,18 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {

auto ty = llvm_type2alive(arg.getType());
ParamAttrs attrs;
if (!ty || !handleParamAttrs(argattr, attrs, false))
auto val = make_unique<Input>(*ty, value_name(arg));
Value *newval = val.get();

if (!ty || !handleParamAttrs(argattr, attrs, *val, newval, false))
return {};
auto val = make_unique<Input>(*ty, value_name(arg), std::move(attrs));
add_identifier(arg, *val.get());
val->setAttributes(std::move(attrs));
add_identifier(arg, *newval);

if (arg.hasReturnedAttr()) {
// Cache this to avoid linear lookup at return
assert(Fn.getReturnedInput() == nullptr);
Fn.setReturnedInput(val.get());
Fn.setReturnedInput(newval);
}
Fn.addInput(std::move(val));
}
Expand Down Expand Up @@ -1770,7 +1789,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
};

// If there is a global variable with initializer, put them at init block.
auto &entry_name = Fn.getFirstBB().getName();
auto &entry_name = Fn.getBB(1).getName();
BB = &Fn.getBB("#init", true);
insert_constexpr_before = nullptr;

Expand Down
22 changes: 14 additions & 8 deletions llvm_util/utils.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,19 @@ Value* make_intconst(uint64_t val, int bits) {
return ret;
}

IR::Value* make_intconst(const llvm::APInt &val) {
unique_ptr<IntConst> c;
auto bw = val.getBitWidth();
auto &ty = get_int_type(bw);
if (bw <= 64)
c = make_unique<IntConst>(ty, val.getZExtValue());
else
c = make_unique<IntConst>(ty, toString(val, 10, false));
auto ret = c.get();
current_fn->addConstant(std::move(c));
return ret;
}

#define RETURN_CACHE(val) \
do { \
auto val_cpy = val; \
Expand All @@ -267,14 +280,7 @@ Value* get_operand(llvm::Value *v,
return nullptr;

if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
unique_ptr<IntConst> c;
if (cnst->getBitWidth() <= 64)
c = make_unique<IntConst>(*ty, cnst->getZExtValue());
else
c = make_unique<IntConst>(*ty, toString(cnst->getValue(), 10, false));
auto ret = c.get();
current_fn->addConstant(std::move(c));
RETURN_CACHE(ret);
RETURN_CACHE(make_intconst(cnst->getValue()));
}

if (auto cnst = dyn_cast<llvm::ConstantFP>(v)) {
Expand Down
2 changes: 2 additions & 0 deletions llvm_util/utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
#include <string>

namespace llvm {
class APInt;
class BasicBlock;
class ConstantExpr;
class DataLayout;
Expand Down Expand Up @@ -40,6 +41,7 @@ IR::Type& get_int_type(unsigned bits);
IR::Type* llvm_type2alive(const llvm::Type *ty);

IR::Value* make_intconst(uint64_t val, int bits);
IR::Value* make_intconst(const llvm::APInt &val);
IR::Value* get_operand(llvm::Value *v,
std::function<IR::Value*(llvm::ConstantExpr *)> constexpr_conv,
std::function<IR::Value*(IR::AggregateValue *)> copy_inserter);
Expand Down
11 changes: 3 additions & 8 deletions tools/alive-exec.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,17 +89,12 @@ optional<StateValue> exec(llvm::Function &F,
sym_exec_init(state);

const BasicBlock *curr_bb = &Func->getFirstBB();
state.startBB(*curr_bb);

// initialize global variables
// #init block has been executed already by sym_exec_init
if (curr_bb->getName() == "#init") {
for (auto &i : curr_bb->instrs()) {
state.exec(i);
}
curr_bb = Func->getBBs()[1];
state.startBB(*curr_bb);
curr_bb = &Func->getBB(1);
}
state.finishInitializer();
state.startBB(*curr_bb);

auto It = curr_bb->instrs().begin();
Solver solver(true);
Expand Down
45 changes: 23 additions & 22 deletions util/symexec.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,20 @@ using namespace IR;
using namespace std;
using util::config::dbg;

static void sym_exec_instr(State &s, const Instr &i) {
auto &val = s.exec(i);

if (util::config::symexec_print_each_value) {
auto &name = i.getName();
dbg() << name;
if (name[0] == '%')
dbg() << " = " << val.val << " /";
dbg() << " UB=" << val.domain << '\n';
if (!val.return_domain.isTrue())
dbg() << " RET=" << val.return_domain << '\n';
}
}

namespace util {

void sym_exec_init(State &s) {
Expand All @@ -36,6 +50,13 @@ void sym_exec_init(State &s) {
}
}

if (f.getFirstBB().getName() == "#init") {
for (auto &i : f.getFirstBB().instrs()) {
sym_exec_instr(s, i);
}
}
s.finishInitializer();

s.saveReturnedInput();
s.exec(Value::voidVal);
}
Expand All @@ -45,33 +66,13 @@ void sym_exec(State &s) {

Function &f = const_cast<Function&>(s.getFn());

bool first = true;
if (f.getFirstBB().getName() != "#init") {
s.finishInitializer();
first = false;
}

for (auto &bb : f.getBBs()) {
if (!s.startBB(*bb))
if (!s.startBB(*bb) || bb->getName() == "#init")
continue;

for (auto &i : bb->instrs()) {
if (first && dynamic_cast<const JumpInstr *>(&i))
s.finishInitializer();
auto &val = s.exec(i);
auto &name = i.getName();

if (config::symexec_print_each_value) {
dbg() << name;
if (name[0] == '%')
dbg() << " = " << val.val << " /";
dbg() << " UB=" << val.domain << '\n';
if (!val.return_domain.isTrue())
dbg() << " RET=" << val.return_domain << '\n';
}
sym_exec_instr(s, i);
}

first = false;
}

if (config::symexec_print_each_value) {
Expand Down

0 comments on commit f19cf14

Please sign in to comment.