The same container with its memory extent exactly its file extent. The
4 MiB extent above dates from when the file itself had to cover the
image; the file now does, and nothing is read from memory beyond it (an
embedded artifact's payloads are read with pread). The AArch64 host uses
this one: a loader that maps no zero-filled tail is also one qemu-user
accepts without the segment being writable, so the executable its tests
run is the executable itself. x86-64 keeps the 4 MiB extent, which is
what its published executables carry.
225def fixedZeroELFHeaderExactFor =
226 (lambda unrestricted machine : Byte .
227 (lambda unrestricted machineCode : Bytes .
228 (let unrestricted fileExtent =
229 (elfModelWord64Bytes
230 (modelWord64FromNaturalTruncated
231 (naturalAdd (byte-to-nat (byte 120)) (naturalAdd (bytes-length machineCode) (bytes-length (elfPagePadding machineCode))))))
232 in
233 (bytes-append
234 (elfHeaderPrefixFor machine)
235 (bytes-append fileExtent (bytes-append fileExtent elfHeaderAlign))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.