Skip to content

Commit

Permalink
start adding support for non-const alignments
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Aug 22, 2023
1 parent 4bd483b commit 9b8b86b
Show file tree
Hide file tree
Showing 8 changed files with 47 additions and 19 deletions.
9 changes: 3 additions & 6 deletions ir/attrs.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -353,16 +353,13 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
s.addUB(p.isNull() ||
merge(Pointer(m, ptrvalue)
.isDereferenceable(deref_expr, align, false, true)));
} else if (align > 1)
} else if (align != 1)
non_poison &= Pointer(m, ptrvalue).isAligned(align);

// TODO: handle non-constant allocalign
if (allocalign) {
StateValue align = s[*allocalign];
auto &align = s[*allocalign];
non_poison &= align.non_poison;
uint64_t val;
if (align.value.isUInt(val))
non_poison &= Pointer(m, ptrvalue).isAligned(val);
non_poison &= Pointer(m, ptrvalue).isAligned(align.value);
}
return non_poison;
}
Expand Down
2 changes: 1 addition & 1 deletion ir/attrs.h
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ class FnAttrs final {

uint64_t derefBytes = 0; // Dereferenceable
uint64_t derefOrNullBytes = 0; // DereferenceableOrNull
uint64_t align = 0;
uint64_t align = 1;

unsigned allocsize_0 = 0; // AllocSize
unsigned allocsize_1 = -1u; // AllocSize
Expand Down
18 changes: 7 additions & 11 deletions ir/instr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2096,12 +2096,13 @@ Value* FnCall::getAlignArg() const {
}

uint64_t FnCall::getAlign() const {
uint64_t align = 0;
uint64_t align = 1;
// TODO: add support for non constant alignments
if (auto *arg = getAlignArg())
align = getIntOr(*arg, 0);
align = getIntOr(*arg, 1);

return max(align, attrs.align ? attrs.align : heap_block_alignment);
return max(align,
attrs.has(FnAttrs::Align) ? attrs.align : heap_block_alignment);
}

uint64_t FnCall::getMaxAccessSize() const {
Expand Down Expand Up @@ -3201,14 +3202,9 @@ StateValue Assume::toSMT(State &s) const {
break;
case Align: {
// assume(ptr, align)
const auto &vptr = s.getAndAddPoisonUB(*args[0]);
if (auto align = dynamic_cast<IntConst *>(args[1])) {
Pointer ptr(s.getMemory(), vptr.value);
s.addGuardableUB(ptr.isAligned(*align->getInt()));
} else {
// TODO: add support for non-constant align
s.addUB(expr());
}
const auto &ptr = s.getAndAddPoisonUB(*args[0]).value;
const auto &align = s.getAndAddPoisonUB(*args[1]).value;
s.addGuardableUB(Pointer(s.getMemory(), ptr).isAligned(align));
break;
}
case NonNull: {
Expand Down
18 changes: 17 additions & 1 deletion ir/pointer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -346,8 +346,12 @@ expr Pointer::isBlockAligned(uint64_t align, bool exact) const {
}

expr Pointer::isAligned(uint64_t align) {
if (align <= 1)
if (align == 0)
return isNull();
if (align == 1)
return true;
if (!is_power2(align))
return false;

auto offset = getOffset();
if (isUndef(offset))
Expand Down Expand Up @@ -376,6 +380,18 @@ expr Pointer::isAligned(uint64_t align) {
return getAddress().extract(bits - 1, 0) == 0;
}

expr Pointer::isAligned(const expr &align) {
uint64_t n;
if (align.isUInt(n))
return isAligned(n);

return
expr::mkIf(align == 0,
isNull(),
align.isPowerOf2() &&
getAddress().urem(align.zextOrTrunc(bits_ptr_address)) == 0);
}

static pair<expr, expr> is_dereferenceable(Pointer &p,
const expr &bytes_off,
const expr &bytes,
Expand Down
1 change: 1 addition & 0 deletions ir/pointer.h
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ class Pointer {

// WARNING: these modify the pointer in place
smt::expr isAligned(uint64_t align);
smt::expr isAligned(const smt::expr &align);
std::pair<smt::AndExpr, smt::expr>
isDereferenceable(uint64_t bytes, uint64_t align, bool iswrite = false,
bool ignore_accessability = false);
Expand Down
4 changes: 4 additions & 0 deletions smt/expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -991,6 +991,10 @@ static expr log2_rec(const expr &e, unsigned idx, unsigned bw) {
log2_rec(e, idx - 1, bw));
}

expr expr::isPowerOf2() const {
return *this != 0 && (*this & (*this - expr::mkUInt(1, *this))) == 0;
}

expr expr::log2(unsigned bw_output) const {
C();
return log2_rec(*this, bits() - 1, bw_output);
Expand Down
1 change: 1 addition & 0 deletions smt/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,7 @@ class expr {
expr ashr_exact(const expr &rhs) const;
expr lshr_exact(const expr &rhs) const;

expr isPowerOf2() const;
expr log2(unsigned bw_output) const;
expr bswap() const;
expr bitreverse() const;
Expand Down
13 changes: 13 additions & 0 deletions tests/alive-tv/non-ub-exploitation/poison_ptr_load.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
; TEST-ARGS: -disallow-ub-exploitation
; SKIP-IDENTITY

define i8 @src() {
%y = load i8, ptr poison
ret i8 %y
}

define i8 @tgt() {
unreachable
}

; ERROR: Source has guardable UB

0 comments on commit 9b8b86b

Please sign in to comment.