allow introduction of readnone with dereferenceable attr
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -193,15 +193,16 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
if (derefBytes || derefOrNullBytes || deref_expr.isValid()) {
// dereferenceable, byval (ParamAttrs), dereferenceable_or_null
if (derefBytes)
- s.addUB(Pointer(m, ptrvalue).isDereferenceable(derefBytes, align));
- if (derefOrNullBytes)
s.addUB(
- Pointer(m, ptrvalue).isDereferenceable(derefOrNullBytes, align)() ||
- p.isNull());
+ Pointer(m, ptrvalue).isDereferenceable(derefBytes, align, false, true));
+ if (derefOrNullBytes)
+ s.addUB(p.isNull() ||
+ Pointer(m, ptrvalue).isDereferenceable(derefOrNullBytes, align,
+ false, true)());
if (deref_expr.isValid())
- s.addUB(
- Pointer(m, ptrvalue).isDereferenceable(deref_expr, align, false)() ||
- p.isNull());
+ s.addUB(p.isNull() ||
+ Pointer(m, ptrvalue).isDereferenceable(deref_expr, align, false,
+ true)());
} else if (align > 1)
non_poison &= Pointer(m, ptrvalue).isAligned(align);

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -359,7 +359,8 @@ expr Pointer::isAligned(uint64_t align) {
static pair<expr, expr> is_dereferenceable(Pointer &p,
const expr &bytes_off,
const expr &bytes,
- uint64_t align, bool iswrite) {
+ uint64_t align, bool iswrite,
+ bool ignore_accessability) {
expr block_sz = p.blockSizeOffsetT();
expr offset = p.getOffset();
@@ -371,10 +372,12 @@ static pair<expr, expr> is_dereferenceable(Pointer &p,
cond &= p.isBlockAlive();
+ if (!ignore_accessability) {
if (iswrite)
cond &= p.isWritable() && !p.isNoWrite();
else
cond &= !p.isNoRead();
+ }
// try some constant folding; these are implied by the conditions above
if (bytes.ugt(p.blockSize()).isTrue() ||
@@ -387,7 +390,7 @@ static pair<expr, expr> is_dereferenceable(Pointer &p,
// When bytes is 0, pointer is always derefenceable
AndExpr Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
- bool iswrite) {
+ bool iswrite, bool ignore_accessability) {
expr bytes_off = bytes0.zextOrTrunc(bits_for_offset);
expr bytes = bytes0.zextOrTrunc(bits_size_t);
DisjointExpr<expr> UB(expr(false)), is_aligned(expr(false)), all_ptrs;
@@ -395,7 +398,7 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
Pointer ptr(m, ptr_expr);
auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align,
- iswrite);
+ iswrite, ignore_accessability);
// record pointer if not definitely unfeasible
if (!ub.isFalse() && !aligned.isFalse() && !ptr.blockSize().isZero())
@@ -425,8 +428,9 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
}
AndExpr Pointer::isDereferenceable(uint64_t bytes, uint64_t align,
- bool iswrite) {
- return isDereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite);
+ bool iswrite, bool ignore_accessability) {
+ return isDereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite,
+ ignore_accessability);
}
// This function assumes that both begin + len don't overflow

MODIFY
ir/pointer.h
ir/pointer.h
@@ -89,9 +89,11 @@ public:
// WARNING: these modify the pointer in place
smt::expr isAligned(uint64_t align);
smt::AndExpr isDereferenceable(uint64_t bytes, uint64_t align,
- bool iswrite = false);
+ bool iswrite = false,
+ bool ignore_accessability = false);
smt::AndExpr isDereferenceable(const smt::expr &bytes, uint64_t align,
- bool iswrite);
+ bool iswrite,
+ bool ignore_accessability = false);
void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;

ADD
tests/alive-tv/attrs/intro-readnone.srctgt.ll
+define void @src(ptr dereferenceable(1) %p) {
+ ret void
+}
+
+define void @tgt(ptr readnone dereferenceable(1) %p) {
+ ret void
+}

allow introduction of readnone with dereferenceable attr