fix assertion in gep for large objects
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1921,7 +1921,6 @@ StateValue GEP::toSMT(State &s) const {
for (auto &[sz, idx] : offsets) {
auto &[v, np] = idx;
- assert(ilog2_ceil(sz) <= bits_for_offset);
auto multiplier = expr::mkUInt(sz, bits_for_offset);
auto val = v.sextOrTrunc(bits_for_offset);
auto inc = multiplier * val;
@@ -1932,6 +1931,12 @@ StateValue GEP::toSMT(State &s) const {
non_poison &= ptr.add_no_overflow(inc);
}
+#ifndef NDEBUG
+ int64_t n;
+ if (inc.isInt(n))
+ assert(ilog2_ceil(abs(n), true) <= bits_for_offset);
+#endif
+
ptr += inc;
non_poison &= np;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -978,7 +978,7 @@ expr Memory::mkInput(const char *name, unsigned attributes) const {
pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
bool nonnull = attributes & Input::NonNull;
- unsigned log_offset = ilog2_ceil(bits_for_offset);
+ unsigned log_offset = ilog2_ceil(bits_for_offset, false);
unsigned bits_undef = bits_for_offset + nonnull * log_offset;
expr undef = expr::mkFreshVar("undef", expr::mkUInt(0, bits_undef));
expr offset = undef;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -617,15 +617,14 @@ static void calculateAndInitConstants(Transform &t) {
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)))
+ bits_for_bid = max(1u, ilog2_ceil(max(num_locals, num_nonlocals), false))
+ (num_locals && num_nonlocals);
// reserve a multiple of 4 for the number of offset bits to make SMT &
// counterexamples more readable
- // Allow an extra bit for the sign, and another for power-of-2 cases
- // e.g. gep(p, 8) -> log(8)=3, but +8 = 01000 (5 bits)
- auto max_geps = ilog2_ceil(max(max_gep_src, max_gep_tgt)) + 2;
- bits_for_offset = min(round_up(max(max_geps, 1u), 4), (uint64_t)bits_size_t);
+ // Allow an extra bit for the sign
+ auto max_geps = ilog2_ceil(max(max_gep_src, max_gep_tgt), true) + 1;
+ bits_for_offset = min(round_up(max_geps, 4), (uint64_t)bits_size_t);
// size of byte
bits_byte = 8 * (does_mem_access ? (unsigned)min_access_size : 1);

MODIFY
util/compiler.cpp
util/compiler.cpp
@@ -18,9 +18,9 @@ unsigned ilog2(uint64_t n) {
#endif
}
-unsigned ilog2_ceil(uint64_t n) {
+unsigned ilog2_ceil(uint64_t n, bool up_power2) {
auto log = ilog2(n);
- return is_power2(n) ? log : log + 1;
+ return !up_power2 && is_power2(n) ? log : log + 1;
}
bool is_power2(uint64_t n, uint64_t *log) {

MODIFY
util/compiler.h
util/compiler.h
@@ -43,7 +43,9 @@ struct const_strip_unique_ptr {
};
unsigned ilog2(uint64_t n);
-unsigned ilog2_ceil(uint64_t n);
+// if up_power2 is true, then we do +1 for powers of 2
+// e.g. ilog2_ceil(8, false) = 3 ; ilog2_ceil(8, true) = 4
+unsigned ilog2_ceil(uint64_t n, bool up_power2);
bool is_power2(uint64_t n, uint64_t *log = nullptr);
unsigned num_sign_bits(uint64_t n);
unsigned num_leading_zeros(uint64_t n);

fix assertion in gep for large objects