Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

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

Aperta
  • Qualcosa non va?
#1,002 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
35/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Tranquilla
Stack tecnologico
rust
Ambito
compilers

Direzione di ricerca

Inizia individuando ed eseguendo ptr-transmute-nonzero-fail.rs, ptr-transmute-two-locals-fail.rs e interior-mut3.rs per riprodurre il comportamento attuale. Leggi la gestione esistente di PTR_OFFSET da PR #812 e segui gli entry point castKindPointerExposeAddress e castKindPointerWithExposedProvenance. Il lavoro è completato quando i test rinominati passano, gli indirizzi distinti e non nulli e i round trip funzionano e tutti i test prove esistenti rimangono verdi.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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
Lingua principale
Python
Stelle
52
Fork
5
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Non abbiamo ancora controllato i file di configurazione di questo progetto. Parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/mir-semantics

Tutte le issue di runtimeverification/mir-semantics

Issue simili

Altre issue su Python

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.