Skip to content

Commit c6c7a7b

Browse files
nunoplopesnunoplopes
committed
revert the fix #1028; alignment no longer implies dereferenceability
Per the latest LangRef changes
1 parent c8cb8a2 commit c6c7a7b

File tree

9 files changed

+35
-84
lines changed

9 files changed

+35
-84
lines changed

‎ir/instr.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4246,7 +4246,7 @@ DEFINE_AS_RETZEROALIGN(Load, getMaxAllocSize)
42464246
DEFINE_AS_RETZERO(Load, getMaxGEPOffset)
42474247

42484248
uint64_t Load::getMaxAccessSize() const {
4249-
return round_up(Memory::getStoreByteSize(getType()), align);
4249+
return Memory::getStoreByteSize(getType());
42504250
}
42514251

42524252
MemInstr::ByteAccessInfo Load::getByteAccessInfo() const {
@@ -4292,7 +4292,7 @@ DEFINE_AS_RETZEROALIGN(Store, getMaxAllocSize)
42924292
DEFINE_AS_RETZERO(Store, getMaxGEPOffset)
42934293

42944294
uint64_t Store::getMaxAccessSize() const {
4295-
return round_up(Memory::getStoreByteSize(val->getType()), align);
4295+
return Memory::getStoreByteSize(val->getType());
42964296
}
42974297

42984298
MemInstr::ByteAccessInfo Store::getByteAccessInfo() const {

‎ir/memory.cpp‎

Lines changed: 18 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -951,7 +951,7 @@ bool Memory::mayalias(const Pointer &p, bool local, unsigned bid0,
951951
if (state->isUndef(offset0))
952952
return false;
953953

954-
if (p.blockSizeAligned().ult(bytes).isTrue())
954+
if (p.blockSize().ult(bytes).isTrue())
955955
return false;
956956

957957
//expr offset = offset0.sextOrTrunc(bits_size_t);
@@ -1172,10 +1172,9 @@ vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
11721172
}
11731173
} else {
11741174
uint64_t blk_size = UINT64_MAX;
1175-
bool single_load
1176-
= ptr.blockSizeAligned().isUInt(blk_size) && blk_size == bytes;
1177-
auto offset = ptr.getShortOffset();
1178-
expr blk_offset = single_load ? expr::mkUInt(0, offset) : offset;
1175+
bool single_load = ptr.blockSize().isUInt(blk_size) && blk_size == bytes;
1176+
auto offset = ptr.getShortOffset();
1177+
expr blk_offset = single_load ? expr::mkUInt(0, offset) : offset;
11791178

11801179
for (unsigned i = 0; i < loaded_bytes; ++i) {
11811180
unsigned idx = left2right ? i : (loaded_bytes - i - 1);
@@ -1246,8 +1245,7 @@ void Memory::store(const Pointer &ptr,
12461245
auto mem = blk.val;
12471246

12481247
uint64_t blk_size;
1249-
bool full_write
1250-
= ptr.blockSizeAligned().isUInt(blk_size) && blk_size == bytes;
1248+
bool full_write = ptr.blockSize().isUInt(blk_size) && blk_size == bytes;
12511249

12521250
// optimization: if fully rewriting the block, don't bother with the old
12531251
// contents. Pick a value as the default one.
@@ -1313,7 +1311,7 @@ void Memory::storeLambda(const Pointer &ptr, const expr &offset,
13131311
auto orig_val = ::raw_load(blk.val, offset);
13141312

13151313
// optimization: full rewrite
1316-
if (full_write || bytes.eq(ptr.blockSizeAligned())) {
1314+
if (full_write || bytes.eq(ptr.blockSize())) {
13171315
blk.val = val_no_offset
13181316
? mk_block_if(cond, val, std::move(blk.val))
13191317
: expr::mkLambda(offset, "#offset",
@@ -1611,12 +1609,6 @@ void Memory::mkAxioms(const Memory &tgt) const {
16111609
if (!p_align.isConst() || !q_align.isConst())
16121610
state->addAxiom(p_align == q_align);
16131611
}
1614-
for (unsigned bid = num_nonlocals_src; bid < num_nonlocals; ++bid) {
1615-
if (skip_bid(bid))
1616-
continue;
1617-
Pointer q(tgt, bid, false);
1618-
state->addAxiom(q.isHeapAllocated().implies(q.blockAlignment() == align));
1619-
}
16201612

16211613
for (unsigned bid = skip_null(); bid < num_nonlocals_src; ++bid) {
16221614
Pointer p(*this, bid, false);
@@ -1666,17 +1658,13 @@ void Memory::mkAxioms(const Memory &tgt) const {
16661658
expr::mkUInt(0, 1).concat(last.extract(bits_ptr_address-2, 0)))
16671659
: addr != last);
16681660
} else {
1669-
sz = p1.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address);
16701661
state->addAxiom(
16711662
Pointer::hasLocalBit()
16721663
// don't spill to local addr section
16731664
? (addr + sz).sign() == 0
16741665
: addr.add_no_uoverflow(sz));
16751666
}
16761667

1677-
state->addAxiom(p1.blockMaxSize()
1678-
.round_up_bits_no_overflow(p1.blockAlignment()));
1679-
16801668
if (num_nonlocals > max_quadratic_disjoint)
16811669
continue;
16821670

@@ -1686,8 +1674,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
16861674
continue;
16871675
Pointer p2(tgt, bid2, false);
16881676
state->addAxiom(disjoint(addr, sz, align, p2.getAddress(),
1689-
p2.blockMaxSizeAligned()
1690-
.zextOrTrunc(bits_ptr_address),
1677+
p2.blockMaxSize().zextOrTrunc(bits_ptr_address),
16911678
p2.blockAlignment()));
16921679
}
16931680
}
@@ -1706,10 +1693,10 @@ void Memory::mkAxioms(const Memory &tgt) const {
17061693
expr::mkForAll(2, vars, names,
17071694
bid1 == bid2 ||
17081695
disjoint(p1.getAddress(),
1709-
p1.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address),
1696+
p1.blockMaxSize().zextOrTrunc(bits_ptr_address),
17101697
p1.blockAlignment(),
17111698
p2.getAddress(),
1712-
p2.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address),
1699+
p2.blockMaxSize().zextOrTrunc(bits_ptr_address),
17131700
p2.blockAlignment())));
17141701
}
17151702
}
@@ -2150,8 +2137,7 @@ static expr disjoint_local_blocks(const Memory &m, const expr &addr,
21502137
Pointer p2(m, Pointer::mkLongBid(sbid, true), zero);
21512138
disj &= p2.isBlockAlive()
21522139
.implies(disjoint(addr, sz, align, p2.getAddress(),
2153-
p2.blockSizeAligned()
2154-
.zextOrTrunc(bits_ptr_address),
2140+
p2.blockSize().zextOrTrunc(bits_ptr_address),
21552141
p2.blockAlignment()));
21562142
}
21572143
return disj;
@@ -2305,7 +2291,7 @@ void Memory::startLifetime(const StateValue &ptr) {
23052291
!ptr.non_poison ||
23062292
p.isBlockAlive() ||
23072293
disjoint_local_blocks(*this, p.getAddress(),
2308-
p.blockSizeAligned().zextOrTrunc(bits_ptr_address),
2294+
p.blockSize().zextOrTrunc(bits_ptr_address),
23092295
p.blockAlignment(), local_blk_addr));
23102296

23112297
store_bv(p, true, local_block_liveness, non_local_block_liveness, true,
@@ -2481,7 +2467,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
24812467
unsigned bytesz = bits_byte / 8;
24822468
Pointer ptr(*this, p);
24832469
if (deref_check)
2484-
state->addUB(ptr.isDereferenceable(bytesize, align, true, false, false));
2470+
state->addUB(ptr.isDereferenceable(bytesize, align, true, false));
24852471

24862472
auto wval = val;
24872473
for (unsigned i = 1; i < bytesz; ++i) {
@@ -2545,8 +2531,8 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
25452531
unsigned bytesz = bits_byte / 8;
25462532

25472533
Pointer dst(*this, d), src(*this, s);
2548-
state->addUB(dst.isDereferenceable(bytesize, align_dst, true, false, false));
2549-
state->addUB(src.isDereferenceable(bytesize, align_src, false, false, false));
2534+
state->addUB(dst.isDereferenceable(bytesize, align_dst, true, false));
2535+
state->addUB(src.isDereferenceable(bytesize, align_src, false, false));
25502536
if (!is_move)
25512537
src.isDisjointOrEqual(bytesize, dst, bytesize);
25522538

@@ -2623,7 +2609,7 @@ void Memory::copy(const Pointer &src, const Pointer &dst) {
26232609

26242610
void Memory::fillPoison(const expr &bid) {
26252611
Pointer p(*this, bid, expr::mkUInt(0, bits_for_offset));
2626-
expr blksz = p.blockSizeAligned();
2612+
expr blksz = p.blockSize();
26272613
memset(std::move(p).release(), IntType("i8", 8).getDummyValue(false),
26282614
std::move(blksz), bits_byte / 8, {}, false);
26292615
}
@@ -2708,7 +2694,7 @@ expr Memory::blockValRefined(const Pointer &src, const Memory &tgt,
27082694
expr ptr_offset = src.getShortOffset();
27092695
uint64_t bytes;
27102696
if (full_check &&
2711-
src.blockSizeAligned().isUInt(bytes) && (bytes / bytes_per_byte) <= 8) {
2697+
src.blockSize().isUInt(bytes) && (bytes / bytes_per_byte) <= 8) {
27122698
expr val_refines = true;
27132699
for (unsigned off = 0; off < (bytes / bytes_per_byte); ++off) {
27142700
expr off_expr = expr::mkUInt(off, ptr_offset);
@@ -2719,8 +2705,7 @@ expr Memory::blockValRefined(const Pointer &src, const Memory &tgt,
27192705
expr cnstr = refined(ptr_offset);
27202706
if (!full_check)
27212707
return cnstr;
2722-
return
2723-
src.getOffsetSizet().ult(src.blockSizeAlignedOffsetT()).implies(cnstr);
2708+
return src.getOffsetSizet().ult(src.blockSizeOffsetT()).implies(cnstr);
27242709
}
27252710
}
27262711

@@ -2797,8 +2782,7 @@ Memory::refined(const Memory &other, bool fncall,
27972782
!stored_tgt.second && stored_tgt.first.empty()) {
27982783
// block not stored; no need to verify
27992784
}
2800-
else if (p.blockSizeAligned().isUInt(bytes) &&
2801-
(bytes / (bits_byte / 8)) <= 8) {
2785+
else if (p.blockSize().isUInt(bytes) && (bytes / (bits_byte / 8)) <= 8) {
28022786
// this is a small block; just check it thoroughly
28032787
val_refined = blockValRefined(p, other, bid, undef_vars, true);
28042788
}

‎ir/pointer.cpp‎

Lines changed: 12 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -342,22 +342,8 @@ expr Pointer::blockSizeOffsetT() const {
342342
return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
343343
}
344344

345-
expr Pointer::blockSizeAligned() const {
346-
return blockSize().round_up_bits(blockAlignment().zextOrTrunc(bits_size_t));
347-
}
348-
349-
expr Pointer::blockSizeAlignedOffsetT() const {
350-
expr sz = blockSizeAligned();
351-
return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
352-
}
353-
354-
expr Pointer::blockMaxSizeAligned() const {
355-
return
356-
blockMaxSize().round_up_bits(blockAlignment().zextOrTrunc(bits_size_t));
357-
}
358-
359-
expr Pointer::blockMaxSizeAlignedOffsetT() const {
360-
expr sz = blockMaxSizeAligned();
345+
expr Pointer::blockMaxSizeOffsetT() const {
346+
expr sz = blockMaxSize();
361347
return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
362348
}
363349

@@ -428,7 +414,7 @@ expr Pointer::isOfBlock(const Pointer &block, const expr &bytes,
428414
assert(block.getOffset().isZero());
429415
expr addr = is_phy ? getPhysicalAddress() : getAddress();
430416
expr block_addr = block.getLogAddress();
431-
expr block_size = block.blockSizeAlignedOffsetT();
417+
expr block_size = block.blockSizeOffsetT();
432418

433419
if (bytes.eq(block_size))
434420
return addr == block_addr;
@@ -445,7 +431,7 @@ expr Pointer::isInboundsOf(const Pointer &block, const expr &bytes0,
445431
expr bytes = bytes0.zextOrTrunc(bits_ptr_address);
446432
expr addr = is_phy ? getPhysicalAddress() : getAddress();
447433
expr block_addr = block.getLogAddress();
448-
expr block_size = block.blockSizeAligned().zextOrTrunc(bits_ptr_address);
434+
expr block_size = block.blockSize().zextOrTrunc(bits_ptr_address);
449435

450436
if (bytes.eq(block_size))
451437
return addr == block_addr;
@@ -459,8 +445,8 @@ expr Pointer::isInboundsOf(const Pointer &block, const expr &bytes0,
459445

460446
expr Pointer::isInbounds(bool strict, bool max_size) const {
461447
auto offset = getOffsetSizet();
462-
auto size = max_size ? blockMaxSizeAlignedOffsetT()
463-
: blockSizeAlignedOffsetT();
448+
auto size = max_size ? blockMaxSizeOffsetT()
449+
: blockSizeOffsetT();
464450
expr ret = strict ? offset.ult(size) : offset.ule(size);
465451
if (bits_for_offset <= bits_size_t) // implied
466452
ret &= !offset.isNegative();
@@ -548,12 +534,9 @@ expr Pointer::isAligned(const expr &align) {
548534
// When bytes is 0, pointer is always dereferenceable
549535
pair<AndExpr, expr>
550536
Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
551-
bool iswrite, bool ignore_accessability,
552-
bool round_size_to_align) {
537+
bool iswrite, bool ignore_accessability) {
553538
bool is_asm = m.state->isAsmMode();
554539
expr bytes = bytes0.zextOrTrunc(bits_for_offset);
555-
if (round_size_to_align)
556-
bytes = bytes.round_up(expr::mkUInt(align, bytes));
557540

558541
auto block_constraints = [&](const Pointer &p) {
559542
expr ret = p.isBlockAlive();
@@ -588,7 +571,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
588571
};
589572

590573
auto log_ptr = [&](Pointer &p) {
591-
expr block_sz = p.blockSizeAlignedOffsetT();
574+
expr block_sz = p.blockSizeOffsetT();
592575
expr offset = p.getOffset();
593576

594577
expr cond;
@@ -632,7 +615,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
632615

633616
Pointer this_ptr(m, i, local, p.getAttrs());
634617

635-
bool same_size = bytes.eq(this_ptr.blockSizeAlignedOffsetT());
618+
bool same_size = bytes.eq(this_ptr.blockSizeOffsetT());
636619
expr this_addr = this_ptr.getLogAddress();
637620
expr offset = same_size ? expr::mkUInt(0, addr) : addr - this_addr;
638621

@@ -749,10 +732,9 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
749732

750733
pair<AndExpr, expr>
751734
Pointer::isDereferenceable(uint64_t bytes, uint64_t align,
752-
bool iswrite, bool ignore_accessability,
753-
bool round_size_to_align) {
735+
bool iswrite, bool ignore_accessability) {
754736
return isDereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite,
755-
ignore_accessability, round_size_to_align);
737+
ignore_accessability);
756738
}
757739

758740
// This function assumes that both begin + len don't overflow
@@ -971,7 +953,7 @@ expr Pointer::isNull() const {
971953

972954
bool Pointer::isBlkSingleByte() const {
973955
uint64_t blk_size;
974-
return blockSizeAligned().isUInt(blk_size) && blk_size == bits_byte/8;
956+
return blockSize().isUInt(blk_size) && blk_size == bits_byte/8;
975957
}
976958

977959
pair<Pointer, expr> Pointer::findLogicalLocalPointer(const expr &addr) const {

‎ir/pointer.h‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -90,10 +90,7 @@ class Pointer {
9090
smt::expr blockSize() const;
9191
smt::expr blockMaxSize() const;
9292
smt::expr blockSizeOffsetT() const; // to compare with offsets
93-
smt::expr blockSizeAligned() const;
94-
smt::expr blockSizeAlignedOffsetT() const; // to compare with offsets
95-
smt::expr blockMaxSizeAligned() const;
96-
smt::expr blockMaxSizeAlignedOffsetT() const;
93+
smt::expr blockMaxSizeOffsetT() const; // to compare with offsets
9794

9895
smt::expr leftoverSize() const;
9996

@@ -131,12 +128,10 @@ class Pointer {
131128
smt::expr isAligned(const smt::expr &align);
132129
std::pair<smt::AndExpr, smt::expr>
133130
isDereferenceable(uint64_t bytes, uint64_t align, bool iswrite = false,
134-
bool ignore_accessability = false,
135-
bool round_size_to_align = true);
131+
bool ignore_accessability = false);
136132
std::pair<smt::AndExpr, smt::expr>
137133
isDereferenceable(const smt::expr &bytes, uint64_t align, bool iswrite,
138-
bool ignore_accessability = false,
139-
bool round_size_to_align = true);
134+
bool ignore_accessability = false);
140135

141136
void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
142137
const smt::expr &len2) const;

‎tests/alive-tv/attrs/align-callsite-withnoundef.srctgt.ll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
; ERROR: Source is more defined than target
2-
31
define void @src(ptr %p) {
42
call void @g(ptr %p)
53
load i8, ptr %p

‎tests/alive-tv/attrs/align-callsite2-withnoundef.srctgt.ll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
; ERROR: Source is more defined than target
2-
31
define void @src(ptr %p) {
42
call void @g(ptr align(4) %p)
53
load i8, ptr %p

‎tests/alive-tv/attrs/align-callsite3-withnoundef.srctgt.ll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
; ERROR: Source is more defined than target
2-
31
define void @src(ptr %p) {
42
call void @g(ptr align(4) %p)
53
load i8, ptr %p

‎tests/alive-tv/memory/align.src.ll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
; ERROR: Source is more defined than target
2-
31
define i32 @foo1(ptr %a) {
42
%v = load i32, ptr %a, align 4
53
%ptrint = ptrtoint ptr %a to i64

‎tests/alive-tv/memory/nullptr-align.srctgt.ll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
; ERROR: Source is more defined than target
2-
31
define i8 @src() null_pointer_is_valid {
42
%v = load i8, ptr null, align 4
53
ret i8 %v

0 commit comments

Comments
 (0)