Every size the containers compute is a product of a capacity the program chose and an element size the checker did, and a product that wraps leaves a block that fits beside a capacity that does not. The next write goes past the end of an allocation a sanitizer was told to expect, which is the one corruption nothing in the suite could have found. The Vec's growth, the Pool's two blocks and their sum, the map's five runs and the budget check now go through checked arithmetic. A size with no representation reports along the path an out-of-memory already takes, with the largest number the condition's field can hold, since the true one has none. The test pins the case the guard exists for: an element of 2^33 + 1 bytes at a capacity of 2^31 wraps to 2 GiB, which a heap allocator answers.
31 lines
1.5 KiB
Plaintext
31 lines
1.5 KiB
Plaintext
;;;; A capacity whose byte count has no representation — the overflow half of
|
|
;;;; spec-memory.md's "Allocation failure".
|
|
;;;;
|
|
;;;; (reserve v n) forwards n to the growth path unfiltered and the bytes asked
|
|
;;;; for are the capacity times the element size, so a large element and a
|
|
;;;; large count multiply past what a signed 64-bit count of bytes can hold.
|
|
;;;; The element here is 2^33 + 1 bytes and the capacity the doubling settles
|
|
;;;; on is 2^31, whose product is 2^64 + 2^31: the wrap leaves 2 GiB, which a
|
|
;;;; heap allocator answers. The block then fits and the recorded capacity does
|
|
;;;; not, and the first push past 2 GiB writes outside it with nothing said —
|
|
;;;; no trap, no diagnostic, and a sanitizer sees a write inside a block it was
|
|
;;;; told to expect. That is why the guard is on the arithmetic and not on the
|
|
;;;; allocator's answer.
|
|
;;;;
|
|
;;;; A size that cannot be represented is a request no allocator can satisfy,
|
|
;;;; so it reports as StorageExhausted along the path an out-of-memory takes,
|
|
;;;; and with nothing handling it the program stops here rather than carrying
|
|
;;;; on — the same rule exhausted-unhandled.flan pins for a ceiling that was
|
|
;;;; genuinely reached.
|
|
(defstruct Big
|
|
[f0 [1073741824 u8] f1 [1073741824 u8] f2 [1073741824 u8]
|
|
f3 [1073741824 u8] f4 [1073741824 u8] f5 [1073741824 u8]
|
|
f6 [1073741824 u8] f7 [1073741824 u8] tail [1 u8]])
|
|
|
|
(defn main [] i32
|
|
(let [v (vec-new Big)]
|
|
(println "before")
|
|
(reserve v 1073741825)
|
|
(println "unreachable"))
|
|
0)
|