| 1088 | } |
| 1089 | |
| 1090 | void Memory::access(const Pointer &ptr, const expr &bytes, uint64_t align, |
| 1091 | bool write, const |
| 1092 | function<void(MemBlock&, const Pointer&, unsigned, bool, |
| 1093 | expr&&)> &fn) { |
| 1094 | assert(!ptr.isLogical().isFalse()); |
| 1095 | auto aliasing = computeAliasing(ptr, bytes, align, write); |
| 1096 | unsigned has_local = aliasing.numMayAlias(true); |
| 1097 | unsigned has_nonlocal = aliasing.numMayAlias(false); |
| 1098 | bool has_both = has_local && has_nonlocal; |
| 1099 | bool is_singleton = has_local + has_nonlocal == 1; |
| 1100 | |
| 1101 | expr addr = ptr.getAddress(); |
| 1102 | expr offset = ptr.getOffset(); |
| 1103 | expr is_local = ptr.isLocal(); |
| 1104 | expr bid = has_both ? ptr.getBid() : ptr.getShortBid(); |
| 1105 | expr one = expr::mkUInt(1, 1); |
| 1106 | |
| 1107 | auto sz_local = aliasing.size(true); |
| 1108 | auto sz_nonlocal = aliasing.size(false); |
| 1109 | |
| 1110 | #define call_fn(block, local, cond_log) \ |
| 1111 | fn(block, Pointer(*this, i, local) + offset, i, local, \ |
| 1112 | is_singleton ? expr(true) : (cond_log)); |
| 1113 | |
| 1114 | for (unsigned i = 0; i < sz_local; ++i) { |
| 1115 | if (!aliasing.mayAlias(true, i)) |
| 1116 | continue; |
| 1117 | |
| 1118 | auto n = expr::mkUInt(i, Pointer::bitsShortBid()); |
| 1119 | call_fn(local_block_val[i], true, |
| 1120 | has_local == 1 ? is_local : (bid == (has_both ? one.concat(n) : n))) |
| 1121 | } |
| 1122 | |
| 1123 | for (unsigned i = 0; i < sz_nonlocal; ++i) { |
| 1124 | if (!aliasing.mayAlias(false, i)) |
| 1125 | continue; |
| 1126 | |
| 1127 | // A nonlocal block for encoding fn calls' side effects cannot be |
| 1128 | // accessed. |
| 1129 | // If aliasing info says it can, either imprecise analysis or incorrect |
| 1130 | // block id encoding is happening. |
| 1131 | assert(!is_fncall_mem(i)); |
| 1132 | |
| 1133 | call_fn(non_local_block_val[i], false, |
| 1134 | has_nonlocal == 1 ? !is_local : bid == i) |
| 1135 | } |
| 1136 | } |
| 1137 | |
| 1138 | static expr raw_load(const expr &block, const expr &offset, |
| 1139 | uint64_t max_idx = UINT64_MAX) { |