From f19cf14127311d761664f8ee1ddb6c625ec943d1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 8 Apr 2024 21:26:42 +0100 Subject: [PATCH] fix #1021: implement support range attribute in fn args & ret val --- BugList.md | 1 + ir/attrs.h | 4 ++- ir/function.h | 1 + ir/value.cpp | 10 ++++--- ir/value.h | 3 ++- llvm_util/llvm2alive.cpp | 57 ++++++++++++++++++++++++++-------------- llvm_util/utils.cpp | 22 ++++++++++------ llvm_util/utils.h | 2 ++ tools/alive-exec.cpp | 11 +++----- util/symexec.cpp | 45 +++++++++++++++---------------- 10 files changed, 94 insertions(+), 62 deletions(-) diff --git a/BugList.md b/BugList.md index 4ef004aa6..dfc16b908 100644 --- a/BugList.md +++ b/BugList.md @@ -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 diff --git a/ir/attrs.h b/ir/attrs.h index e8f8201cb..a56258e55 100644 --- a/ir/attrs.h +++ b/ir/attrs.h @@ -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) {} diff --git a/ir/function.h b/ir/function.h index 24a09f0fb..bbf3471b7 100644 --- a/ir/function.h +++ b/ir/function.h @@ -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; diff --git a/ir/value.cpp b/ir/value.cpp index 1d382558c..fde24e95a 100644 --- a/ir/value.cpp +++ b/ir/value.cpp @@ -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; diff --git a/ir/value.h b/ir/value.h index f1a475cc9..68b3981e4 100644 --- a/ir/value.h +++ b/ir/value.h @@ -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); } diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index be95511f5..5c74799c9 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -379,7 +379,7 @@ class llvm2alive_ : public llvm::InstVisitor> { assert(fn->getFunctionType() == llvm::FunctionType::get(llvm::Type::getVoidTy(ctx), { llvm::Type::getInt1Ty(ctx) }, false)); - return make_unique(*args[0], Assume::AndNonPoison); + return make_unique(*args.at(0), Assume::AndNonPoison); } Function::FnDecl decl; @@ -395,8 +395,10 @@ class llvm2alive_ : public llvm::InstVisitor> { 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)); @@ -444,16 +446,16 @@ class llvm2alive_ : public llvm::InstVisitor> { unique_ptr 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()) @@ -711,6 +713,10 @@ class llvm2alive_ : public llvm::InstVisitor> { 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(*ty, *val); } @@ -1336,24 +1342,29 @@ class llvm2alive_ : public llvm::InstVisitor> { return true; } + Value* handleRangeAttr(const llvm::Attribute &attr, Value &val) { + auto CR = attr.getValueAsConstantRange(); + vector bounds{ make_intconst(CR.getLower()), + make_intconst(CR.getUpper()) }; + auto assume + = make_unique(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: @@ -1418,6 +1429,10 @@ class llvm2alive_ : public llvm::InstVisitor> { 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(); @@ -1641,6 +1656,7 @@ class llvm2alive_ : public llvm::InstVisitor> { reset_state(Fn); alive_fn = &Fn; + BB = &Fn.getBB("#init", true); auto &attrs = Fn.getFnAttrs(); vector param_attrs; @@ -1653,15 +1669,18 @@ class llvm2alive_ : public llvm::InstVisitor> { auto ty = llvm_type2alive(arg.getType()); ParamAttrs attrs; - if (!ty || !handleParamAttrs(argattr, attrs, false)) + auto val = make_unique(*ty, value_name(arg)); + Value *newval = val.get(); + + if (!ty || !handleParamAttrs(argattr, attrs, *val, newval, false)) return {}; - auto val = make_unique(*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)); } @@ -1770,7 +1789,7 @@ class llvm2alive_ : public llvm::InstVisitor> { }; // 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; diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp index 79b091f7d..02ea1a5ec 100644 --- a/llvm_util/utils.cpp +++ b/llvm_util/utils.cpp @@ -247,6 +247,19 @@ Value* make_intconst(uint64_t val, int bits) { return ret; } +IR::Value* make_intconst(const llvm::APInt &val) { + unique_ptr c; + auto bw = val.getBitWidth(); + auto &ty = get_int_type(bw); + if (bw <= 64) + c = make_unique(ty, val.getZExtValue()); + else + c = make_unique(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; \ @@ -267,14 +280,7 @@ Value* get_operand(llvm::Value *v, return nullptr; if (auto cnst = dyn_cast(v)) { - unique_ptr c; - if (cnst->getBitWidth() <= 64) - c = make_unique(*ty, cnst->getZExtValue()); - else - c = make_unique(*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(v)) { diff --git a/llvm_util/utils.h b/llvm_util/utils.h index 2275a25c3..e223d0bd4 100644 --- a/llvm_util/utils.h +++ b/llvm_util/utils.h @@ -9,6 +9,7 @@ #include namespace llvm { +class APInt; class BasicBlock; class ConstantExpr; class DataLayout; @@ -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 constexpr_conv, std::function copy_inserter); diff --git a/tools/alive-exec.cpp b/tools/alive-exec.cpp index 34255aa4a..8a3a0d3ca 100644 --- a/tools/alive-exec.cpp +++ b/tools/alive-exec.cpp @@ -89,17 +89,12 @@ optional 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); diff --git a/util/symexec.cpp b/util/symexec.cpp index 389b26223..e1c06790a 100644 --- a/util/symexec.cpp +++ b/util/symexec.cpp @@ -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) { @@ -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); } @@ -45,33 +66,13 @@ void sym_exec(State &s) { Function &f = const_cast(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(&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) {