| 2136 | } |
| 2137 | |
| 2138 | pair<expr, expr> |
| 2139 | Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind, |
| 2140 | const expr &precond, const expr &nonnull, |
| 2141 | optional<unsigned> bidopt, unsigned *bid_out, bool is_function) { |
| 2142 | assert(!memory_unused()); |
| 2143 | |
| 2144 | // Produce a local block if blockKind is heap or stack. |
| 2145 | bool is_local = blockKind != GLOBAL && blockKind != CONSTGLOBAL; |
| 2146 | bool is_const = blockKind == CONSTGLOBAL; |
| 2147 | |
| 2148 | auto &last_bid = is_local ? next_local_bid |
| 2149 | : (is_const ? next_const_bid : next_global_bid); |
| 2150 | unsigned bid = bidopt.value_or(last_bid); |
| 2151 | assert((is_local && bid < numLocals()) || |
| 2152 | (!is_local && bid < numNonlocals())); |
| 2153 | if (!bidopt) |
| 2154 | ++last_bid; |
| 2155 | assert(bid < last_bid); |
| 2156 | |
| 2157 | if (bid_out) |
| 2158 | *bid_out = bid; |
| 2159 | |
| 2160 | expr size_zext; |
| 2161 | expr nooverflow = true; |
| 2162 | if (size) { |
| 2163 | size_zext = size->zextOrTrunc(bits_size_t); |
| 2164 | // we round up the size statically instead of creating a large expr later |
| 2165 | if (!has_globals_diff_align) |
| 2166 | size_zext = size_zext.round_up(expr::mkUInt(align, bits_size_t)); |
| 2167 | nooverflow = size->bits() <= bits_size_t ? true : |
| 2168 | size->extract(size->bits()-1, bits_size_t) == 0; |
| 2169 | } |
| 2170 | |
| 2171 | expr allocated = precond && nooverflow; |
| 2172 | state->addPre(nonnull.implies(allocated)); |
| 2173 | allocated |= nonnull; |
| 2174 | |
| 2175 | Pointer p(*this, bid, is_local); |
| 2176 | auto short_bid = p.getShortBid(); |
| 2177 | // TODO: If address space is not 0, the address can be 0. |
| 2178 | // TODO: add support for C++ allocs |
| 2179 | unsigned alloc_ty = 0; |
| 2180 | switch (blockKind) { |
| 2181 | case MALLOC: alloc_ty = Pointer::MALLOC; break; |
| 2182 | case CXX_NEW: alloc_ty = Pointer::CXX_NEW; break; |
| 2183 | case STACK: alloc_ty = Pointer::STACK; break; |
| 2184 | case GLOBAL: |
| 2185 | case CONSTGLOBAL: alloc_ty = Pointer::GLOBAL; break; |
| 2186 | } |
| 2187 | |
| 2188 | assert(align != 0); |
| 2189 | auto align_bits = ilog2(align); |
| 2190 | expr align_expr = expr::mkUInt(align_bits, bitsAlignmentInfo()); |
| 2191 | bool is_null = !is_local && has_null_block && bid == 0; |
| 2192 | |
| 2193 | if (is_local) { |
| 2194 | assert(size); |
| 2195 | mkLocalDisjAddrAxioms(allocated, short_bid, size_zext, align_expr, |
no test coverage detected