FEXIT

assembly

[
  "FEXIT [RegDst0 ~ RegDstn], sp!, uimm"
]

block

[]

catalog_indices

[
  63
]

catalog_records

[
  {
    "asm": "FEXIT [RegDst0 ~ RegDstn], sp!, uimm",
    "constraints": [
      {
        "field": "DstBegin",
        "operator": "one-of",
        "values": [
          2,
          3,
          4,
          5,
          6,
          7,
          8,
          9,
          10,
          11,
          12,
          13,
          14,
          15,
          16,
          17,
          18,
          19,
          20,
          21,
          22,
          23
        ]
      },
      {
        "field": "DstEnd",
        "operator": "one-of",
        "values": [
          2,
          3,
          4,
          5,
          6,
          7,
          8,
          9,
          10,
          11,
          12,
          13,
          14,
          15,
          16,
          17,
          18,
          19,
          20,
          21,
          22,
          23
        ]
      }
    ],
    "encoding": [
      {
        "index": 0,
        "mask": "0x0000707f",
        "match": "0x00001041",
        "width_bits": 32
      }
    ],
    "encoding_kind": "L32",
    "fields": [
      {
        "name": "DstBegin",
        "pieces": [
          {
            "instruction_lsb": 15,
            "value_lsb": 0,
            "width": 5
          }
        ],
        "signedness": "encoding-defined",
        "width": 5
      },
      {
        "name": "DstEnd",
        "pieces": [
          {
            "instruction_lsb": 20,
            "value_lsb": 0,
            "width": 5
          }
        ],
        "signedness": "encoding-defined",
        "width": 5
      },
      {
        "name": "uimm",
        "pieces": [
          {
            "instruction_lsb": 25,
            "value_lsb": 3,
            "width": 7
          },
          {
            "instruction_lsb": 7,
            "value_lsb": 10,
            "width": 5
          }
        ],
        "signedness": "unsigned",
        "width": 15
      }
    ],
    "form_id": "fexit_32_37b663f2a34d",
    "length_bits": 32,
    "mnemonic": "FEXIT",
    "semantic_family": "CMD",
    "semantic_group": "Bundle Split",
    "semantic_handler": "ExecuteFrameExit",
    "semantic_summary": "Destroys a restartable stack frame and restores one inclusive callee-save register-ring range.",
    "status": "accepted"
  }
]

classification

[
  "lifecycle"
]

contract

{
  "block_composition": [
    "none"
  ],
  "canonical_assembly": [
    "FEXIT [RegDst0 ~ RegDstn], sp!, uimm"
  ],
  "defaults": [
    "The inclusive register range is the ring R2..R23. Singleton, full-ring, and wraparound ranges are assigned.",
    "uimm is always present and represents a byte count in multiples of eight; encoded zero is real zero and is illegal because every assigned range contains at least one register."
  ],
  "encoding_class": "standalone-encoded",
  "examples": [
    "FEXIT [RegDst0 ~ RegDstn], sp!, uimm"
  ],
  "exceptions": [
    "Reserved endpoints or an insufficient frame size raise Fault_IllegalInstruction before sp, register, memory, target, progress, or TPC effects.",
    "Each eight-byte stack access is a restart boundary. A recoverable access fault preserves earlier committed events and retries exactly the first uncommitted event from trap-preserved template state."
  ],
  "field_contracts": {},
  "field_zero_meanings": {
    "DstBegin": "Encoded zero is outside the callee-save ring and is reserved.",
    "DstEnd": "Encoded zero is outside the callee-save ring and is reserved.",
    "uimm": "Encoded zero is a real zero-byte frame size and is illegal for every nonempty range."
  },
  "legality": [
    "DstBegin and DstEnd select the inclusive R2..R23 callee-save ring; every endpoint outside 2..23 is reserved before effects.",
    "If the range contains N registers, uimm must be at least 8*N bytes. The encoding supplies only multiples of eight."
  ],
  "memory_effects": [
    "Load one aligned eight-byte value per selected destination from caller_sp-8, caller_sp-16, and subsequent descending slots."
  ],
  "operands": [
    {
      "field": "DstBegin",
      "role": "first register in the inclusive R2..R23 ring range"
    },
    {
      "field": "DstEnd",
      "role": "last register in the inclusive R2..R23 ring range"
    },
    {
      "field": "uimm",
      "role": "frame byte count, encoded in multiples of eight"
    }
  ],
  "ordering": [
    "Add uimm to sp first, then load descending caller-frame slots in inclusive register-ring order.",
    "Each load, destination write, and progress advance commit as one restart event; recovery does not add sp twice or repeat earlier loads."
  ],
  "standalone_opcode": true,
  "state_effects": [
    "The accepted start records instruction PC, endpoints, count, frame size, reconstructed caller sp, and zero progress.",
    "After the final load, decrement nonzero frame depth, publish the last-frame tuple, clear active progress, and retire once."
  ]
}

depends_on

[
  "PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"
]

id

PTO-BLOCK-FEXIT

mnemonic

FEXIT

summary

Destroys a restartable stack frame and restores one inclusive callee-save register-ring range.

surface

block

{
  "classification": [
    "lifecycle"
  ],
  "documentation": "docs/block/lifecycle/FEXIT.md",
  "id": "PTO-BLOCK-FEXIT",
  "instruction_contract": {
    "artifact": "spec/evidence/instruction-contract-closure.json",
    "mnemonic": "FEXIT",
    "ndf_clause": "PTO-INST-BLOCK-FEXIT"
  },
  "mnemonic": "FEXIT",
  "readiness_subjects": [
    "ADR-0032",
    "ADR-0052",
    "ADR-0059",
    "ADR-0084"
  ],
  "semantic_tests": [
    "PTO-AVS-BLOCK-FEXIT-FRAME-001",
    "PTO-AVS-BLOCK-FEXIT-RESTART-001"
  ],
  "source": "asl/block/lifecycle/FEXIT.asl",
  "surface": "block",
  "tests": [
    "PTO-AVS-BLOCK-FEXIT-DECODE-001",
    "PTO-AVS-BLOCK-FEXIT-FRAME-001",
    "PTO-AVS-BLOCK-FEXIT-RESTART-001"
  ]
}