start adding support for fn attributes on allocation calls
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -156,8 +156,7 @@ encodePtrAttrs(const State &s, const expr &ptrvalue,
UB.add(p.isDereferenceable(derefBytes, align));
if (derefOrNullBytes)
UB.add(p.isDereferenceable(derefOrNullBytes, align)() || p.isNull());
- } else if (align != 1)
- // align
+ } else if (align > 1)
non_poison &= p.isAligned(align);
}
@@ -179,6 +178,11 @@ ParamAttrs::encode(const State &s, const StateValue &val, const Type &ty) const
}
+bool FnAttrs::isNonNull() const {
+ return has(NonNull) ||
+ (!has(NullPointerIsValid) && derefBytes > 0);
+}
+
bool FnAttrs::poisonImpliesUB() const {
return has(Dereferenceable) || has(NoUndef) || has(NNaN) ||
has(DereferenceableOrNull);

MODIFY
ir/attrs.h
ir/attrs.h
@@ -79,7 +79,9 @@ public:
uint64_t derefBytes = 0; // Dereferenceable
uint64_t derefOrNullBytes = 0; // DereferenceableOrNull
- unsigned align = 1;
+ unsigned align = 0;
+
+ bool isNonNull() const;
// Returns true if returning poison or an aggregate having a poison is UB
bool poisonImpliesUB() const;

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2013,7 +2013,7 @@ FnCall::ByteAccessInfo FnCall::getByteAccessInfo() const {
if (attr.has(decay<decltype(attr)>::type::DereferenceableOrNull)) \
sz = gcd(sz, attr.derefOrNullBytes); \
/* Without align, nothing is guaranteed about the bytesize */ \
- sz = gcd(sz, retattr.align); \
+ sz = gcd(sz, retattr.align ? retattr.align : 1); \
bytesize = bytesize ? gcd(bytesize, sz) : sz; \
} while (0)
@@ -3124,7 +3124,7 @@ bool Malloc::canFree() const {
}
uint64_t Malloc::getAlign() const {
- return align ? align : heap_block_alignment;
+ return attrs.align ? attrs.align : heap_block_alignment;
}
vector<Value*> Malloc::operands() const {
@@ -3145,11 +3145,7 @@ void Malloc::print(ostream &os) const {
os << " = malloc ";
else
os << " = realloc " << *ptr << ", ";
- os << *size;
- if (align)
- os << ", align " << align;
- if (isNonNull)
- os << ", nonnull";
+ os << *size << ',' << attrs;
}
StateValue Malloc::toSMT(State &s) const {
@@ -3163,13 +3159,14 @@ StateValue Malloc::toSMT(State &s) const {
expr nullp = Pointer::mkNullPointer(m)();
expr ret = expr::mkIf(allocated, p_new, nullp);
- if (!ptr) {
- if (isNonNull) {
+ if (attrs.isNonNull()) {
+ // TODO: In C++ we need to throw an exception if the allocation fails.
s.addPre(std::move(allocated));
+ allocated = true;
ret = p_new;
}
- // TODO: In C++ we need to throw an exception if the allocation fails.
- } else {
+
+ if (ptr) {
auto &[p, np_ptr] = s.getAndAddUndefs(*ptr);
s.addUB(np_ptr);
check_can_store(s, p);
@@ -3196,10 +3193,9 @@ expr Malloc::getTypeConstraints(const Function &f) const {
unique_ptr<Instr> Malloc::dup(Function &f, const string &suffix) const {
return ptr
- ? make_unique<Malloc>(getType(), getName() + suffix, *ptr, *size, isNonNull,
- align)
- : make_unique<Malloc>(getType(), getName() + suffix, *size, isNonNull,
- align);
+ ? make_unique<Malloc>(getType(), getName() + suffix, *ptr, *size,
+ FnAttrs(attrs))
+ : make_unique<Malloc>(getType(), getName() + suffix, *size, FnAttrs(attrs));
}
@@ -3225,7 +3221,7 @@ Calloc::ByteAccessInfo Calloc::getByteAccessInfo() const {
}
uint64_t Calloc::getAlign() const {
- return align ? align : heap_block_alignment;
+ return attrs.align ? attrs.align : heap_block_alignment;
}
vector<Value*> Calloc::operands() const {
@@ -3254,6 +3250,11 @@ StateValue Calloc::toSMT(State &s) const {
auto [p, allocated] = m.alloc(size, getAlign(), Memory::MALLOC,
np && nm.mul_no_uoverflow(sz), nonnull);
+ if (attrs.isNonNull()) {
+ s.addPre(std::move(allocated));
+ allocated = true;
+ }
+
m.memset(p, { expr::mkUInt(0, 8), true }, size, getAlign(), {}, false);
return { expr::mkIf(allocated, p, Pointer::mkNullPointer(m)()), true };
@@ -3268,7 +3269,8 @@ expr Calloc::getTypeConstraints(const Function &f) const {
}
unique_ptr<Instr> Calloc::dup(Function &f, const string &suffix) const {
- return make_unique<Calloc>(getType(), getName() + suffix, *num, *size);
+ return make_unique<Calloc>(getType(), getName() + suffix, *num, *size,
+ FnAttrs(attrs));
}

MODIFY
ir/instr.h
ir/instr.h
@@ -654,19 +654,16 @@ public:
class Malloc final : public MemInstr {
Value *ptr = nullptr, *size;
- uint64_t align;
- bool isNonNull = false;
+ FnAttrs attrs;
public:
- Malloc(Type &type, std::string &&name, Value &size, bool isNonNull,
- uint64_t align)
- : MemInstr(type, std::move(name)), size(&size), align(align),
- isNonNull(isNonNull) {}
+ Malloc(Type &type, std::string &&name, Value &size, FnAttrs &&attrs)
+ : MemInstr(type, std::move(name)), size(&size), attrs(std::move(attrs)) {}
Malloc(Type &type, std::string &&name, Value &ptr, Value &size,
- bool isNonNull, uint64_t align)
- : MemInstr(type, std::move(name)), ptr(&ptr), size(&size), align(align),
- isNonNull(isNonNull) {}
+ FnAttrs &&attrs)
+ : MemInstr(type, std::move(name)), ptr(&ptr), size(&size),
+ attrs(std::move(attrs)) {}
Value& getSize() const { return *size; }
uint64_t getAlign() const;
@@ -690,11 +687,12 @@ public:
class Calloc final : public MemInstr {
Value *num, *size;
- uint64_t align;
+ FnAttrs attrs;
public:
Calloc(Type &type, std::string &&name, Value &num, Value &size,
- uint64_t align = 0)
- : MemInstr(type, std::move(name)), num(&num), size(&size), align(align) {}
+ FnAttrs &&attrs)
+ : MemInstr(type, std::move(name)), num(&num), size(&size),
+ attrs(std::move(attrs)) {}
Value& getNum() const { return *num; }
Value& getSize() const { return *size; }

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -327,7 +327,7 @@ expr Pointer::isBlockAligned(uint64_t align, bool exact) const {
}
expr Pointer::isAligned(uint64_t align) {
- if (align == 1)
+ if (align <= 1)
return true;
auto offset = getOffset();

MODIFY
llvm_util/known_fns.cpp
llvm_util/known_fns.cpp
using namespace IR;
using namespace std;
-static unsigned align(llvm::CallInst &i) {
- auto a = i.getRetAlign();
- return a.hasValue() ? a.getValue().value() : 0;
-}
-
namespace llvm_util {
-#define RETURN_EXACT() \
- return { std::move(param_attrs), false }
-#define RETURN_APPROX() \
- return { std::move(param_attrs), true }
+#define RETURN_EXACT() return false
+#define RETURN_APPROX() return true
-static pair<vector<ParamAttrs>, bool>
-implict_attrs_(llvm::LibFunc libfn, FnAttrs &attrs, bool is_void,
+bool implict_attrs_(llvm::LibFunc libfn, FnAttrs &attrs,
+ vector<ParamAttrs> &param_attrs, bool is_void,
unsigned num_args) {
- vector<ParamAttrs> param_attrs;
-
auto set_param = [&](unsigned i, ParamAttrs::Attribute attr) {
if (param_attrs.size() <= i)
param_attrs.resize(i+1);
@@ -390,31 +381,26 @@ implict_attrs_(llvm::LibFunc libfn, FnAttrs &attrs, bool is_void,
}
}
-pair<vector<ParamAttrs>, bool>
-llvm_implict_attrs(llvm::Function &f, const llvm::TargetLibraryInfo &TLI,
- FnAttrs &attrs) {
+bool llvm_implict_attrs(llvm::Function &f, const llvm::TargetLibraryInfo &TLI,
+ FnAttrs &attrs, vector<ParamAttrs> &param_attrs) {
llvm::LibFunc libfn;
if (!TLI.getLibFunc(f, libfn) || !TLI.has(libfn))
- return { {}, false };
- return
- implict_attrs_(libfn, attrs, f.getReturnType()->isVoidTy(), f.arg_size());
+ return false;
+ return implict_attrs_(libfn, attrs, param_attrs,
+ f.getReturnType()->isVoidTy(), f.arg_size());
}
#undef RETURN_EXACT
#undef RETURN_APPROX
-#define RETURN_VAL(op) \
- return { op, std::move(attrs), std::move(param_attrs), false }
-#define RETURN_EXACT() \
- return { nullptr, std::move(attrs), std::move(param_attrs), false }
-#define RETURN_APPROX() \
- return { nullptr, std::move(attrs), std::move(param_attrs), true }
+#define RETURN_VAL(op) return { op, false }
+#define RETURN_EXACT() return { nullptr, false }
+#define RETURN_APPROX() return { nullptr, true }
-tuple<unique_ptr<Instr>, FnAttrs, vector<ParamAttrs>, bool>
+pair<unique_ptr<Instr>, bool>
known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
- BasicBlock &BB, const vector<Value*> &args) {
- FnAttrs attrs;
- vector<ParamAttrs> param_attrs;
+ BasicBlock &BB, const vector<Value*> &args, FnAttrs &&attrs,
+ vector<ParamAttrs> &param_attrs) {
auto ty = llvm_type2alive(i.getType());
if (!ty)
@@ -422,15 +408,12 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
// TODO: add support for checking mismatch of C vs C++ alloc fns
if (llvm::isMallocOrCallocLikeFn(&i, &TLI)) {
- bool isNonNull = i.hasRetAttr(llvm::Attribute::NonNull);
- //TODO: also null for C++'s new throwing operator
-
// aligned malloc
if (auto *algn = llvm::getAllocAlignment(&i, &TLI)) {
if (auto algnint = dyn_cast<llvm::ConstantInt>(algn)) {
+ attrs.align = algnint->getZExtValue();
RETURN_VAL(
- make_unique<Malloc>(*ty, value_name(i), *args[1], isNonNull,
- algnint->getZExtValue()));
+ make_unique<Malloc>(*ty, value_name(i), *args[1], std::move(attrs)));
} else {
// TODO: add support for non-const alignments
RETURN_APPROX();
@@ -440,23 +423,24 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
// calloc
if (auto *init = llvm::getInitialValueOfAllocation(&i, &TLI, i.getType());
init && init->isNullValue())
- RETURN_VAL(
- make_unique<Calloc>(*ty, value_name(i), *args[0], *args[1], align(i)));
+ RETURN_VAL(make_unique<Calloc>(*ty, value_name(i), *args[0], *args[1],
+ std::move(attrs)));
// malloc or new
RETURN_VAL(
- make_unique<Malloc>(*ty, value_name(i), *args[0], isNonNull, align(i)));
+ make_unique<Malloc>(*ty, value_name(i), *args[0], std::move(attrs)));
}
if (llvm::getReallocatedOperand(&i, &TLI)) {
- bool isNonNull = i.hasRetAttr(llvm::Attribute::NonNull);
+ // TODO: allow other args
RETURN_VAL(make_unique<Malloc>(*ty, value_name(i), *args[0], *args[1],
- isNonNull, align(i)));
+ std::move(attrs)));
}
if (llvm::getFreedOperand(&i, &TLI)) {
if (i.hasFnAttr(llvm::Attribute::NoFree)) {
auto zero = make_intconst(0, 1);
RETURN_VAL(make_unique<Assume>(*zero, Assume::AndNonPoison));
}
+ // TODO: allow other args
RETURN_VAL(make_unique<Free>(*args[0]));
}
@@ -564,8 +548,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
// (void)fwrite(const void *ptr, 1, 1, FILE *stream) ->
// (void)fputc(int c, FILE *stream))
if (bytes == 1 && i.use_empty() && TLI.has(llvm::LibFunc_fputc)) {
- auto [param_attrs, _]
- = implict_attrs_(llvm::LibFunc_fputc, attrs, false, 2);
+ (void)implict_attrs_(llvm::LibFunc_fputc, attrs, param_attrs, false, 2);
auto &byteTy = get_int_type(8); // FIXME
auto &i32 = get_int_type(32);
auto call
@@ -588,8 +571,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
break;
}
- auto [params, approx] = llvm_implict_attrs(*decl, TLI, attrs);
- return { nullptr, std::move(attrs), std::move(params), approx };
+ return { nullptr, llvm_implict_attrs(*decl, TLI, attrs, param_attrs) };
}
}

MODIFY
llvm_util/known_fns.h
llvm_util/known_fns.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
-#include "ir/attrs.h"
#include <memory>
-#include <tuple>
#include <vector>
namespace llvm {
@@ -16,21 +14,23 @@ class TargetLibraryInfo;
namespace IR {
class BasicBlock;
+class FnAttrs;
class Instr;
+class ParamAttrs;
class Value;
}
namespace llvm_util {
-// returned bool indicates whether it's a known function call
-std::pair<std::vector<IR::ParamAttrs>, bool>
-llvm_implict_attrs(llvm::Function &f, const llvm::TargetLibraryInfo &TLI,
- IR::FnAttrs &attrs);
+// returns true if it's a known function call
+bool llvm_implict_attrs(llvm::Function &f, const llvm::TargetLibraryInfo &TLI,
+ IR::FnAttrs &attrs,
+ std::vector<IR::ParamAttrs> &param_attrs);
-// returned bool indicates whether it's a known function call
-std::tuple<std::unique_ptr<IR::Instr>, IR::FnAttrs, std::vector<IR::ParamAttrs>,
- bool>
+// returns true if it's a known function call
+std::pair<std::unique_ptr<IR::Instr>, bool>
known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
- IR::BasicBlock &BB, const std::vector<IR::Value*> &args);
+ IR::BasicBlock &BB, const std::vector<IR::Value*> &args,
+ IR::FnAttrs &&attrs, std::vector<IR::ParamAttrs> &param_attr);
}

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -283,14 +283,20 @@ public:
FnAttrs attrs;
vector<ParamAttrs> param_attrs;
+
+ parse_fn_attrs(i, attrs);
+
+ if (auto op = dyn_cast<llvm::FPMathOperator>(&i)) {
+ if (op->hasNoNaNs())
+ attrs.set(FnAttrs::NNaN);
+ }
+
if (!approx) {
- auto [known, attrs0, params0, approx0] = known_call(i, TLI, *BB, args);
+ auto [known, approx0]
+ = known_call(i, TLI, *BB, args, std::move(attrs), param_attrs);
+ approx = approx0;
if (known)
RETURN_IDENTIFIER(std::move(known));
-
- attrs = std::move(attrs0);
- param_attrs = std::move(params0);
- approx = approx0;
}
auto ty = llvm_type2alive(i.getType());
@@ -305,7 +311,8 @@ public:
if (!iasm->canThrow())
attrs.set(FnAttrs::NoThrow);
call = make_unique<InlineAsm>(*ty, value_name(i), iasm->getAsmString(),
- iasm->getConstraintString(), std::move(attrs));
+ iasm->getConstraintString(),
+ std::move(attrs));
} else {
if (!fn) // TODO: support indirect calls
return error(i);
@@ -318,13 +325,6 @@ public:
llvm::AttributeList attrs_fndef = fn ? fn->getAttributes()
: llvm::AttributeList();
- parse_fn_attrs(i, attrs);
-
- if (auto op = dyn_cast<llvm::FPMathOperator>(&i)) {
- if (op->hasNoNaNs())
- attrs.set(FnAttrs::NNaN);
- }
-
if (fn)
call = make_unique<FnCall>(*ty, value_name(i),
'@' + fn->getName().str(), std::move(attrs));
@@ -1469,7 +1469,8 @@ public:
reset_state(Fn);
auto &attrs = Fn.getFnAttrs();
- auto [param_attrs, approx] = llvm_implict_attrs(f, TLI, attrs);
+ vector<ParamAttrs> param_attrs;
+ (void)llvm_implict_attrs(f, TLI, attrs, param_attrs);
llvm::AttributeList attrlist = f.getAttributes();

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -1103,7 +1103,7 @@ static unique_ptr<Instr> parse_malloc(string_view name) {
auto &op = parse_operand(ty);
// Malloc returns a pointer at address space 0
Type &pointer_type = get_pointer_type(0);
- return make_unique<Malloc>(pointer_type, string(name), op, false, 0);
+ return make_unique<Malloc>(pointer_type, string(name), op, FnAttrs::None);
}
static unique_ptr<Instr> parse_extractelement(string_view name) {

start adding support for fn attributes on allocation calls