| 443 | } |
| 444 | |
| 445 | expr Pointer::inbounds(bool simplify_ptr) { |
| 446 | if (!simplify_ptr) |
| 447 | return isInbounds(false); |
| 448 | |
| 449 | DisjointExpr<expr> ret(expr(false)), all_ptrs; |
| 450 | for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) { |
| 451 | expr inb = Pointer(m, ptr_expr).isInbounds(false); |
| 452 | if (!inb.isFalse()) |
| 453 | all_ptrs.add(ptr_expr, domain); |
| 454 | ret.add(std::move(inb), domain); |
| 455 | } |
| 456 | |
| 457 | // trim set of valid ptrs |
| 458 | auto ptrs = std::move(all_ptrs)(); |
| 459 | p = ptrs ? *std::move(ptrs) : expr::mkUInt(0, totalBits()); |
| 460 | |
| 461 | return *std::move(ret)(); |
| 462 | } |
| 463 | |
| 464 | expr Pointer::blockAlignment() const { |
| 465 | return getValue("blk_align", m.local_blk_align, m.non_local_blk_align, |