When bytes is 0, pointer is always dereferenceable
| 522 | |
| 523 | // When bytes is 0, pointer is always dereferenceable |
| 524 | pair<AndExpr, expr> |
| 525 | Pointer::isDereferenceable(const expr &bytes0, uint64_t align, |
| 526 | bool iswrite, bool ignore_accessability, |
| 527 | bool round_size_to_align) { |
| 528 | bool is_asm = m.state->isAsmMode(); |
| 529 | expr bytes = bytes0.zextOrTrunc(bits_for_offset); |
| 530 | if (round_size_to_align) |
| 531 | bytes = bytes.round_up(expr::mkUInt(align, bytes)); |
| 532 | |
| 533 | auto block_constraints = [&](const Pointer &p) { |
| 534 | expr ret = p.isBlockAlive(); |
| 535 | if (iswrite) |
| 536 | ret &= p.isWritable() && !p.isNoWrite(); |
| 537 | else if (!ignore_accessability) |
| 538 | ret &= !p.isNoRead(); |
| 539 | |
| 540 | // If we are loading from an argument and it has the 'initializes' |
| 541 | // attribute, make sure we have already stored to it before. |
| 542 | if (!ignore_accessability && !iswrite && has_initializes_attr) { |
| 543 | auto &s = m.getState(); |
| 544 | for (auto &input0 : s.getFn().getInputs()) { |
| 545 | auto &input = static_cast<const Input&>(input0); |
| 546 | auto &inits = input.getAttributes().initializes; |
| 547 | if (inits.empty()) |
| 548 | continue; |
| 549 | |
| 550 | Pointer arg(m, s[input].value); |
| 551 | expr offsets = true; |
| 552 | for (auto [l, h] : inits) { |
| 553 | offsets &= (p.getOffset().uge((arg + l).getOffset()) && |
| 554 | p.getOffset().ult((arg + h).getOffset()) |
| 555 | ).implies(m.hasStored(p, bytes)); |
| 556 | } |
| 557 | // TODO: isBasedOnArg is not sufficient; we have to store the arg number |
| 558 | // in the pointer as we can have 2 args with same initializes attr |
| 559 | ret&= (p.isBasedOnArg() && p.getBid() == arg.getBid()).implies(offsets); |
| 560 | } |
| 561 | } |
| 562 | return ret; |
| 563 | }; |
| 564 | |
| 565 | auto log_ptr = [&](Pointer &p) { |
| 566 | expr block_sz = p.blockSizeAlignedOffsetT(); |
| 567 | expr offset = p.getOffset(); |
| 568 | |
| 569 | expr cond; |
| 570 | if (m.state->isUndef(offset) || |
| 571 | m.state->isUndef(p.getBid()) || |
| 572 | bytes.ugt(block_sz).isTrue() || |
| 573 | p.getOffsetSizet().uge(block_sz).isTrue()) { |
| 574 | cond = false; |
| 575 | } else { |
| 576 | // optimized conditions that are equivalent to the condition below |
| 577 | if (block_sz.isConst() && bytes.isConst()) { |
| 578 | cond = offset.ule(block_sz - bytes); |
| 579 | } else if (bits_for_offset > bits_size_t && bytes.isOne()) { |
| 580 | cond = offset.ult(block_sz); |
| 581 | } else { |
no test coverage detected