Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

feat: add address allocation model for pointer-to-integer semantics

Abierto
  • ¿Algo no está bien?
#1,002 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
35/100
Tipo de issue
Nueva funcionalidad
Claridad
Bastante claro
Estado de actividad
Tranquilo
Stack tecnológico
rust
Área
compilers

Línea de trabajo

Comienza localizando y ejecutando ptr-transmute-nonzero-fail.rs, ptr-transmute-two-locals-fail.rs e interior-mut3.rs para reproducir el comportamiento actual. Lee el manejo existente de PTR_OFFSET de PR #812 y sigue los puntos de entrada castKindPointerExposeAddress y castKindPointerWithExposedProvenance. Se considera terminado cuando las pruebas renombradas pasan, las direcciones distintas de cero y los recorridos de ida y vuelta funcionan, y todas las pruebas prove existentes siguen en verde.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

status:ready

Problem

PR #812 added PtrLocal transmute-to-usize support, making the interior-mut3 test pass. However, the implementation uses the pointer metadata PTR_OFFSET (typically 0) as a stand-in for a real memory address, producing incorrect semantics:

Confirmed fail tests:

  • ptr-transmute-nonzero-fail: a stack pointer transmuted to usize yields 0, but real Rust stack addresses are never null
  • ptr-transmute-two-locals-fail: two different local variable pointers both transmute to 0, making them indistinguishable

Root cause: KMIR uses symbolic references (PtrLocal(offset, place(local(N), ...))) to represent pointers with no numeric address concept. When Rust code converts a pointer to an integer (transmute, ptr as usize), KMIR cannot produce a meaningful value.

Industry Comparison

Miri: Lazy Address Allocation + Provenance Tracking

Miri pointers are abstract (AllocId, offset) pairs. Concrete addresses are only assigned on demand (at ptr-to-int cast time).

Core mechanism:

  • alloc_addresses/mod.rs maintains base_addr: FxHashMap<AllocId, u64>
  • ptr→int: addr_from_alloc_id() lazily assigns a base address, returns base + offset, adds AllocId to the exposed set
  • int→ptr: searches the exposed set for an allocation whose address range contains the target integer, recovering provenance
  • Inserts random gaps between allocations to simulate real allocator behavior

Source: alloc_addresses/mod.rs

Kani: CBMC Object Encoding, No Provenance

Kani compiles Rust to CBMC's GOTO programs, inheriting CBMC's object-based memory model.

Core mechanism:

  • Pointers are bitvectors: top N bits (default 16) = object-id, remaining bits = offset
  • ptr→int and int→ptr are both bitvector reinterpretations (codegen_misc_cast → cast_to)
  • Does not distinguish PointerExposeAddress, Transmute, IntToInt — all go through the same path
  • Does not track provenance — Issue #1274 decided not to handle it

Limitation: Cast integers are not real addresses but CBMC's internal (object-id << N | offset) encoding. Integer arithmetic mixes object-id and offset bits.

Source: rvalue.rs
Docs: Kani Rust Feature Support

Verus: Strict Provenance + Ghost Permission Tokens

Verus follows Rust's Strict Provenance model (RFC 3559), using ghost types for memory permission tracking.

Core mechanism:

  • Pointer = PtrData<T> = (address: usize, provenance: Provenance, metadata)
  • Memory access requires PointsTo<T> ghost permission token
  • ptr→int: cast_ptr_to_usize extracts the address component (no preconditions)
  • int→ptr: requires expose_provenance() to obtain an IsExposed ghost token, then with_exposed_provenance() to reconstruct

Source: raw_ptr.rs
PR: verus#1244 (Ptrs)

Comparison Summary
Dimension Miri Kani Verus KMIR (current)
Pointer repr (AllocId, offset) bitvector (obj_id, offset) (addr, provenance, meta) PtrLocal(offset, place, ...)
ptr→int lazy base + offset bitvector cast extract addr PTR_OFFSET (usually 0)
int→ptr search exposed set bitvector cast needs IsExposed token unsupported
Provenance Stacked/Tree Borrows none ghost token none
Address uniqueness yes (random gaps) yes (unique obj-id) yes (abstract) no (all zero)

Rust-level reference: unsafe-code-guidelines#286

Proposed Approach: Miri-style Lazy Address Allocation

Add address mapping cells to the K configuration:

<addressMap> .Map </addressMap>        // local(N) -> (base_addr, size)
<nextAddress> 4096:Int </nextAddress>  // start from non-zero to avoid NULL
<exposedSet> .Set </exposedSet>        // allocations with exposed provenance

ptr→int rule:

rule <k> #cast(PtrLocal(_, place(LOCAL, _), _, metadata(_, PTR_OFFSET, _)),
               castKindTransmute, _, TY_TARGET)
      => #intAsType(BASE +Int (PTR_OFFSET *Int ELEM_SIZE), ...) ... </k>
     <addressMap> ... LOCAL |-> (BASE, _) ... </addressMap>
  requires #isIntType(lookupTy(TY_TARGET))

// Lazy allocation: if LOCAL doesn't have an address yet
rule <k> #cast(PtrLocal(_, place(LOCAL, _), _, _), castKindTransmute, _, TY_TARGET)
      => #allocAddress(LOCAL, SIZE) ~> #cast(...) ... </k>
     <addressMap> MAP </addressMap>
  requires #isIntType(lookupTy(TY_TARGET))
   andBool notBool LOCAL in_keys(MAP)

Pros:

  • Most complete semantics: different allocations get different addresses, supports roundtrip
  • Lazy — no overhead for programs that never do ptr→int
  • Can support both PointerExposeAddress and with_exposed_provenance

Cons:

  • Requires new configuration cells
  • Concrete vs symbolic address decision needed for symbolic execution
  • Stack frame lifetime management (cleanup on function return)

Related PRs / Issues (can be closed)

  • PR #812 — current PTR_OFFSET workaround, superseded by address model
  • PR #877 — skips alignment checking block; with real addresses, alignment checks execute normally
  • Issue #638 — "Extend pointer emulation to pass alignment check" — exactly what the address model achieves

Acceptance Criteria

  • ptr-transmute-nonzero-fail.rs renamed to ptr-transmute-nonzero.rs (test passes)
  • ptr-transmute-two-locals-fail.rs renamed to ptr-transmute-two-locals.rs (test passes)
  • interior-mut3.rs continues to pass
  • Support castKindPointerExposeAddress (ptr as usize)
  • Support castKindPointerWithExposedProvenance (usize as *const T) via exposed set
  • Different allocations produce different ptr→int results
  • All ptr→int results are non-zero
  • ptr→int→ptr roundtrip recovers the original allocation
  • No regressions: all existing prove tests pass
Lenguaje dominante
Python
Estrellas
52
Forks
5
Sin PR fusionados en 30 d

Preparar el entorno

Aún no hemos revisado los archivos de configuración de este proyecto. Empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de runtimeverification/mir-semantics

Todos los issues de runtimeverification/mir-semantics

Issues similares

Más issues de Python

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.