il: document pointer provenance rules

2f7beb74644448da87f0e894651b62a509db561e294210c9bf0308ebd825a93f 
Phase 4: formalize the closed set of pointer-producing instructions
in the RIL documentation.

- Document the Ptr type distinction in the type system section
- Add 'Pointer Provenance' section listing the exhaustive set of
  instructions that may produce a Ptr-typed register: Reserve,
  Copy(DataSym/FnAddr), Load with Ptr type, BinOp::Add on Ptr,
  Call returning Ptr, block parameters, and WordToPtr
- Document pointer arithmetic constraints
- Annotate Reserve and Copy instructions with provenance semantics
Alexis Sellier committed ago 1 parent e8882a03
lib/std/lang/il.rad +31 -1
12 12 
//! >   -- "Single-Pass Generation of Static Single-Assignment Form for
13 13 
//! >       Structured Languages", by Marc M. Brandis and Hanspeter Mossenbock
14 14 
//!
15 15 
//! # Type System
16 16 
//!
17 - 
//! Primitive types: `W8`, `W16`, `W32` (word sizes).
17 + 
//! Primitive types: `W8`, `W16`, `W32`, `W64` (word sizes) and `Ptr`.
18 18 
//! Signedness is encoded in operations (e.g., `Sdiv` vs `Udiv`), not types.
19 19 
//!
20 + 
//! `Ptr` is the same physical width as `W64` on RV64 but is semantically
21 + 
//! distinct: it marks values with pointer provenance. A verifier treats
22 + 
//! `Ptr` and `W64` as incompatible types.
23 + 
//!
20 24 
//! Types on arithmetic operations indicate logical width but don't
21 25 
//! change code generation. Arithmetic is always machine word sized,
22 26 
//! no 8-bit or 16-bit add instruction.
23 27 
//!
24 28 
//! # Truncation and Narrowing
48 52 
//! Field access is expressed as address arithmetic plus load/store.
49 53 
//!
50 54 
//! Bounds check elimination and nullable pointer optimization happen during
51 55 
//! this lowering phase.
52 56 
//!
57 + 
//! # Pointer Provenance
58 + 
//!
59 + 
//! A `Ptr`-typed register may only be produced by the following closed
60 + 
//! set of operations:
61 + 
//!
62 + 
//! | Instruction            | Provenance                              |
63 + 
//! |------------------------|------------------------------------------|
64 + 
//! | `Reserve`              | Stack allocation (local provenance)      |
65 + 
//! | `Copy(DataSym)`        | Global/static data address               |
66 + 
//! | `Copy(FnAddr)`         | Function address (code section)          |
67 + 
//! | `Load` with `typ: Ptr` | Derived from an existing pointer         |
68 + 
//! | `BinOp::Add` on `Ptr`  | Pointer arithmetic (derived)             |
69 + 
//! | `Call` returning `Ptr`  | Callee-produced pointer                 |
70 + 
//! | Block parameter         | Merges pointer values from predecessors  |
71 + 
//! | `WordToPtr`            | Explicit escape hatch (trusted code)     |
72 + 
//!
73 + 
//! Any other instruction producing a register used as a memory base is
74 + 
//! a verifier error. `PtrToWord` converts a pointer to `W64`; the
75 + 
//! resulting integer cannot be used as a memory base.
76 + 
//!
77 + 
//! Pointer arithmetic (`BinOp::Add` with `typ: Ptr`) requires exactly
78 + 
//! one `Ptr` operand and one integer operand. The result is `Ptr` with
79 + 
//! the same provenance as the pointer operand.
80 + 
//!
53 81 
//! # Control Flow
54 82 
//!
55 83 
//! Uses block parameters instead of phi nodes (like MLIR/SIL). Each block
56 84 
//! can declare parameters, and jumps/branches pass arguments to their targets.
57 85 

    

  
  
  

  
  

  

  
  
    

      196
      224
       
      
    // Memory operations //

    

  
    

      197
      225
       
      
    ///////////////////////

    

  
    

      198
      226
       
      

    

  
    

      199
      227
       
      
    /// Allocate space on the stack: `reserve %dst <size> <alignment>;`

    

  
    

      200
      228
       
      
    /// Size can be a register for dynamic stack allocation (eg. VLAs).

    

  
    

      
      229
      +
      
    /// The result is always `Ptr` (stack provenance).

    

  
    

      201
      230
       
      
    Reserve { dst: Reg, size: Val, alignment: u32 },

    

  
    

      202
      231
       
      
    /// Load a value from memory (zero-extending): `load <type> %dst %src <offset>;`

    

  
    

      203
      232
       
      
    Load { typ: Type, dst: Reg, src: Reg, offset: i32 },

    

  
    

      204
      233
       
      
    /// Signed load from memory (sign-extending): `sload <type> %dst %src <offset>;`

    

  
    

      205
      234
       
      
    Sload { typ: Type, dst: Reg, src: Reg, offset: i32 },

    

  
  
  

  
  

  

  
  
    

      223
      252
       
      
        src: Reg,

    

  
    

      224
      253
       
      
        /// Size to copy in bytes.

    

  
    

      225
      254
       
      
        size: Val

    

  
    

      226
      255
       
      
    },

    

  
    

      227
      256
       
      
    /// Copy a value into a register: `copy %dst <val>;`.

    

  
    

      
      257
      +
      
    /// When the source is `DataSym` or `FnAddr`, the result is `Ptr`.

    

  
    

      228
      258
       
      
    Copy { dst: Reg, val: Val },

    

  
    

      229
      259
       
      

    

  
    

      230
      260
       
      
    /////////////////////

    

  
    

      231
      261
       
      
    // ALU operations  //

    

  
    

      232
      262
       
      
    /////////////////////