memory: fix block_refined for the case bits_byte > 8
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -681,12 +681,13 @@ expr Pointer::block_refined(const Pointer &other) const {
expr blk_size = block_size();
expr val_refines(true);
uint64_t bytes;
+ auto bytes_per_byte = bits_byte / 8;
- if (blk_size.isUInt(bytes) && bytes <= 8) {
+ if (blk_size.isUInt(bytes) && (bytes / bytes_per_byte) <= 8) {
expr bid = get_bid();
expr ptr_offset = get_offset();
- for (unsigned off = 0; off < bytes; ++off) {
+ for (unsigned off = 0; off < bytes; off += bytes_per_byte) {
expr off_expr = expr::mkUInt(off, bits_for_offset);
Pointer p(m, bid, off_expr);
Pointer q(other.m, p());
@@ -1149,6 +1150,8 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
expr size_zext = size.zextOrTrunc(bits_size_t);
expr nooverflow = size_zext.extract(bits_size_t - 1, bits_size_t - 1) == 0;
+ assert(bits_byte == 8 || is_local ||
+ size_zext.urem(expr::mkUInt(bits_byte/8, bits_size_t)).isZero());
expr allocated = precond && nooverflow;
state->addPre(nonnull.implies(allocated));

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -631,7 +631,7 @@ static void calculateAndInitConstants(Transform &t) {
does_int_mem_access = false;
// Mininum access size (in bytes)
- uint64_t min_access_size = 16;
+ uint64_t min_access_size = 8;
bool does_mem_access = false;
bool has_load = false;
@@ -689,6 +689,7 @@ static void calculateAndInitConstants(Transform &t) {
};
// The number of bits needed to encode pointer attributes
// nonnull and byval isn't encoded in ptr attribute bits
+ bool has_byval = has_attr(Input::ByVal);
has_nocapture = has_attr(Input::NoCapture);
has_readonly = has_attr(Input::ReadOnly);
bits_for_ptrattrs = has_nocapture + has_readonly;
@@ -711,7 +712,9 @@ static void calculateAndInitConstants(Transform &t) {
// size of byte
min_access_size = min(min_global_size, min_access_size);
- bits_byte = 8 * ((does_mem_access || has_fncall)
+ if (has_byval)
+ min_access_size = 1;
+ bits_byte = 8 * ((does_mem_access || num_globals != 0)
? (unsigned)min_access_size : 1);
little_endian = t.src.isLittleEndian();

memory: fix block_refined for the case bits_byte > 8