set_next and get_next truncate pointers unsafely on some x86 and ARM configurations

[eric-wieser]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

lean_object has a clever optimization to mutate into a linked list for handling deletions without stack growth:

lean4/src/include/lean/lean.h

Lines 119 to 121 in e60078d

	For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
	stored in compact regions, we use the page information to retrieve its size so that we can reuse
	`m_cs_sz` to store the deletion list inline. Using the page information is not an option with

which effectively assumes that a 64-bit pointer can be truncated to 48-bits, and that zero-extending will round-trip, This is implemented here:

lean4/src/runtime/object.cpp

Lines 278 to 301 in e60078d

	static inline lean_object * get_next(lean_object * o) {
	if (sizeof(void*) == 8) {
	size_t header = ((size_t*)o)[0];
	LEAN_BYTE(header, 7) = 0;
	LEAN_BYTE(header, 6) = 0;
	return (lean_object*)(header);
	} else {
	// 32-bit version
	return ((lean_object**)o)[0];
	}
	}
	static inline void set_next(lean_object * o, lean_object * n) {
	if (sizeof(void*) == 8) {
	size_t new_header = (size_t)n;
	LEAN_BYTE(new_header, 7) = o->m_tag;
	LEAN_BYTE(new_header, 6) = o->m_other;
	((size_t*)o)[0] = new_header;
	lean_assert(get_next(o) == n);
	} else {
	// 32-bit version
	((lean_object**)o)[0] = n;
	}
	}

Unfortunately, like many clever optimizations, eventually compilers and hardware adjust such that its assumptions no longer hold.

In particular, the following configurations lead to segfaults due to the top bits of the address space being zeroed out:

• Arm's memory tagging hardware extension (MTE), which uses the top bits to implement address sanitization.
• Arm's large virtual addressing, which extends the virtual address space from 48 bits to 52 bits (i.e. with CONFIG_ARM64_FORCE_52BIT=y)
• Intel's 5-level paging, which extends the virtual address space from 48 bits to 57 bits

Context

Detected in some address-sanitization runs of AlphaProof infrastructure.

Steps to Reproduce

1. Build with some of the suggested flags above

Expected behavior: Lean's tests pass

Actual behavior: Segfault due to invalid addresses, or the lean_assert(get_next(o) == n); firing.

Versions

4.27.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.