Method mkSubByteZExtStoreCond

ir/memory.cpp:1434–1457

}

expr Memory::mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const {
  bool mk_axiom = &val == &val2;

  // optimization: the initial block is assumed to follow the ABI already.
  if (!mk_axiom && isInitialMemBlock(val.p, true))
    return true;

  bool always_1_byte = bits_byte >= (1u << num_sub_byte_bits);
  auto stored_bits   = val.numStoredBits();
  auto num_bytes
    = always_1_byte ? expr::mkUInt(0, size_byte_number())
                    : stored_bits.udiv(expr::mkUInt(bits_byte, stored_bits))
                        .zextOrTrunc(size_byte_number());
  auto leftover_bits
    = (always_1_byte ? stored_bits
                      : stored_bits.urem(expr::mkUInt(bits_byte, stored_bits))
      ).zextOrTrunc(bits_byte);

  return val.isPtr() ||
         (mk_axiom ? expr(false) : !val.boolNonptrNonpoison()) ||
         stored_bits == 0 ||
         val.byteNumber() != num_bytes ||
         val2.nonptrValue().lshr(leftover_bits) == 0;
}

void Memory::mkNonlocalValAxioms(const expr &block) const {
  expr offset = expr::mkQVar(0, Pointer::bitsShortOffset());