| 406 | } |
| 407 | |
| 408 | expr Byte::refined(const Byte &other) const { |
| 409 | bool asm_mode = other.m.isAsmMode(); |
| 410 | expr is_ptr = isPtr(); |
| 411 | expr is_ptr2 = other.isPtr(); |
| 412 | |
| 413 | // allow int -> ptr type punning in asm mode |
| 414 | // this is only need to support removal of 'store int undef' |
| 415 | expr v1 = nonptrValue(); |
| 416 | expr v2 = asm_mode ? other.forceCastToInt() : other.nonptrValue(); |
| 417 | expr np1 = nonptrNonpoison(); |
| 418 | expr np2 = asm_mode ? other.nonPoison() : other.nonptrNonpoison(); |
| 419 | |
| 420 | // int byte |
| 421 | expr int_cnstr = (asm_mode || !num_sub_byte_bits) ? expr(true) |
| 422 | : (np1 == 0 || |
| 423 | (numStoredBits() == other.numStoredBits() && |
| 424 | byteNumber() == other.byteNumber())); |
| 425 | |
| 426 | if (does_int_mem_access) { |
| 427 | if (bits_poison_per_byte == bits_byte) { |
| 428 | int_cnstr &= (np2 & np1) == np1 && (v1 & np1) == (v2 & np1); |
| 429 | } |
| 430 | else if (bits_poison_per_byte > 1) { |
| 431 | assert((bits_byte % bits_poison_per_byte) == 0); |
| 432 | unsigned bits_val = bits_byte / bits_poison_per_byte; |
| 433 | for (unsigned i = 0; i < bits_poison_per_byte; ++i) { |
| 434 | expr ev1 = v1.extract((i+1) * bits_val - 1, i * bits_val); |
| 435 | expr ev2 = v2.extract((i+1) * bits_val - 1, i * bits_val); |
| 436 | expr enp1 = np1.extract(i, i); |
| 437 | expr enp2 = np2.extract(i, i); |
| 438 | int_cnstr |
| 439 | &= enp1 == 0 || ((enp1.eq(enp2) ? true : enp2 == 1) && ev1 == ev2); |
| 440 | } |
| 441 | } else { |
| 442 | assert(!np1.isValid() || np1.bits() == 1); |
| 443 | int_cnstr &= np1 == 0 || ((np1.eq(np2) ? true : np2 == 1) && v1 == v2); |
| 444 | } |
| 445 | } |
| 446 | |
| 447 | expr ptr_cnstr; |
| 448 | |
| 449 | // fast path: if we didn't do any ptr store, then all ptrs in memory were |
| 450 | // already there and don't need checking |
| 451 | if (!does_ptr_store || is_ptr.isFalse() || (!asm_mode && is_ptr2.isFalse())) { |
| 452 | ptr_cnstr = *this == other; |
| 453 | } else { |
| 454 | // allow ptr -> int type punning in asm mode |
| 455 | expr extra = false; |
| 456 | if (asm_mode) { |
| 457 | extra = !is_ptr2 && |
| 458 | other.boolNonptrNonpoison() && |
| 459 | castPtrToInt() == other.nonptrValue(); |
| 460 | } |
| 461 | ptr_cnstr = ptrNonpoison().implies( |
| 462 | (other.ptrNonpoison() && |
| 463 | ptrByteoffset() == other.ptrByteoffset() && |
| 464 | ptr().refined(other.ptr())) || |
| 465 | extra); |
no test coverage detected