memory: add support for readonly arguemnts
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -20,6 +20,7 @@ bool has_ptr2int;
bool has_malloc;
bool has_free;
bool has_nocapture;
+bool has_readonly;
bool has_dead_allocas;
bool does_int_mem_access;
bool does_ptr_mem_access;

MODIFY
ir/globals.h
ir/globals.h
@@ -44,6 +44,7 @@ extern bool has_free;
/// Whether any function argument (not function call arg) has the attribute
extern bool has_nocapture;
+extern bool has_readonly;
/// Whether there are allocas that are initially dead (need start_lifetime)
extern bool has_dead_allocas;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -272,6 +272,19 @@ static unsigned bits_shortbid() {
return bits_for_bid - ptr_has_local_bit();
}
+static expr attr_to_bitvec(unsigned attributes) {
+ if (!bits_for_ptrattrs)
+ return expr();
+ auto e = expr::mkUInt(0, bits_for_ptrattrs);
+ auto idx = 0;
+ auto to_bit = [&](bool b, Input::Attribute a) -> expr {
+ return expr::mkUInt(b ? (((attributes & a) ? 1 : 0) << idx++) : 0,
+ bits_for_ptrattrs);
+ };
+ e = e | to_bit(has_nocapture, Input::NoCapture);
+ e = e | to_bit(has_readonly, Input::ReadOnly);
+ return e;
+}
namespace IR {
@@ -494,7 +507,7 @@ static pair<expr, expr> is_dereferenceable(const Pointer &p, const expr &bytes,
cond &= p.is_block_alive();
if (iswrite)
- cond &= p.is_writable();
+ cond &= p.is_writable() && !p.is_readonly();
// try some constant folding; these are implied by the conditions above
if (bytes.ugt(block_sz).isTrue() ||
@@ -711,6 +724,12 @@ expr Pointer::is_nocapture() const {
return p.extract(0, 0) == 1;
}
+expr Pointer::is_readonly() const {
+ if (!has_readonly)
+ return false;
+ return p.extract(has_nocapture, has_nocapture) == 1;
+}
+
Pointer Pointer::mkNullPointer(const Memory &m) {
assert(num_nonlocals > 0);
// A null pointer points to block 0 without any attribute.
@@ -950,10 +969,7 @@ void Memory::markByVal(unsigned bid) {
}
expr Memory::mkInput(const char *name, unsigned attributes) const {
- bool is_nocapture = (attributes & Input::NoCapture) != 0;
- Pointer p(*this, name, false, false,
- bits_for_ptrattrs ? expr::mkUInt(is_nocapture, bits_for_ptrattrs) :
- expr());
+ Pointer p(*this, name, false, false, attr_to_bitvec(attributes));
if (attributes & Input::NonNull)
state->addAxiom(p.isNonZero());
state->addAxiom(p.get_short_bid().ule(num_nonlocals - 1));
@@ -976,10 +992,8 @@ pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
one << var.zextOrTrunc(bits_for_offset));
offset = undef.extract(bits_undef - 1, log_offset) | shl;
}
- bool is_nocapture = (attributes & Input::NoCapture) != 0;
Pointer p(*this, expr::mkUInt(0, bits_for_bid), offset,
- bits_for_ptrattrs ? expr::mkUInt(is_nocapture, bits_for_ptrattrs) :
- expr());
+ attr_to_bitvec(attributes));
return { p.release(), move(undef) };
}

MODIFY
ir/memory.h
ir/memory.h
@@ -76,7 +76,7 @@ public:
class Pointer {
const Memory &m;
- // [bid, offset, is-nocapture]
+ // [bid, offset, is-readonly, is-nocapture]
// The top bit of bid is 1 if the block is local, 0 otherwise.
// A local memory block is a memory block that is
// allocated by an instruction during the current function call. This does
@@ -84,8 +84,9 @@ class Pointer {
// block can also be a local memory block.
// Otherwise, a pointer is pointing to a non-local block, which can be either
// of global variable, heap, or a stackframe that is not this function call.
- // The lowest bit represents whether the pointer value came from nocapture
- // argument. If block is local, is-nocapture cannot be 1.
+ // The lowest bits represent whether the pointer value came from a nocapture/
+ // readonly argument. If block is local, is-readonly or is-nocapture cannot
+ // be 1.
// TODO: missing support for address space
smt::expr p;
@@ -161,6 +162,7 @@ public:
smt::expr get_alloc_type() const;
smt::expr is_heap_allocated() const;
smt::expr is_nocapture() const;
+ smt::expr is_readonly() const;
smt::expr refined(const Pointer &other) const;
smt::expr fninput_refined(const Pointer &other) const;

MODIFY
ir/value.cpp
ir/value.cpp
@@ -164,6 +164,8 @@ static string attr_str(unsigned attributes) {
ret += "byval ";
if (attributes & Input::NoCapture)
ret += "nocapture ";
+ if (attributes & Input::ReadOnly)
+ ret += "readonly ";
return ret;
}

MODIFY
ir/value.h
ir/value.h
@@ -109,7 +109,8 @@ public:
class Input final : public Value {
public:
- enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1, NoCapture = 1<<2 };
+ enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1, NoCapture = 1<<2,
+ ReadOnly = 1 << 3 };
private:
std::string smt_name;
unsigned attributes;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -750,6 +750,10 @@ public:
attrs |= Input::NoCapture;
continue;
+ case llvm::Attribute::ReadOnly:
+ attrs |= Input::ReadOnly;
+ continue;
+
default:
*out << "ERROR: Unsupported attribute: " << attr.getAsString() << '\n';
return {};

ADD
tests/alive-tv/attrs/readonly.src.ll
+define void @f(i8* readonly %x) {
+ store i8 0, i8* %x
+ ret void
+}

ADD
tests/alive-tv/attrs/readonly.tgt.ll
+define void @f(i8* readonly %x) {
+ unreachable
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -585,7 +585,8 @@ static void calculateAndInitConstants(Transform &t) {
// The number of bits needed to encode pointer attributes
// nonnull and byval isn't encoded in ptr attribute bits
has_nocapture = has_attr(Input::NoCapture);
- bits_for_ptrattrs = has_nocapture;
+ has_readonly = has_attr(Input::ReadOnly);
+ bits_for_ptrattrs = has_nocapture + has_readonly;
// ceil(log2(maxblks)) + 1 for local bit
bits_for_bid = max(1u, ilog2_ceil(max(num_locals, num_nonlocals)))

memory: add support for readonly arguemnts (#257)