• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
          • Structures
            • Rflagsbits
            • Cr4bits
            • Xcr0bits
            • Cr0bits
            • Prefixes
            • Ia32_eferbits
            • Evex-byte1
            • Cr3bits
            • Evex-byte3
            • Vex3-byte2
            • Vex3-byte1
            • Vex2-byte1
            • Evex-prefixes
            • Evex-byte2
            • Vex-prefixes
            • Sib
            • Modr/m-structures
            • Vex-prefixes-layout-structures
            • Sib-structures
            • Legacy-prefixes-layout-structure
            • Evex-prefixes-layout-structures
            • Cr8bits
            • Opcode-maps-structures
            • Segmentation-bitstructs
              • System-segment-descriptorbits
              • Data-segment-descriptorbits
              • Code-segment-descriptorbits
              • Interrupt/trap-gate-descriptorbits
              • Call-gate-descriptorbits
              • Data-segment-descriptor-attributesbits
              • Code-segment-descriptor-attributesbits
              • System-segment-descriptor-attributesbits
              • Interrupt/trap-gate-descriptor-attributesbits
              • Call-gate-descriptor-attributesbits
              • Segment-selectorbits
              • Hidden-segment-registerbits
              • Gdtr/idtrbits
              • Interrupt/trap-gate-descriptor-attributesbits-equiv-under-mask
              • System-segment-descriptorbits-debug
              • System-segment-descriptor-attributesbits-equiv-under-mask
              • Interrupt/trap-gate-descriptorbits-equiv-under-mask
              • Data-segment-descriptor-attributesbits-equiv-under-mask
              • Code-segment-descriptor-attributesbits-equiv-under-mask
              • Call-gate-descriptor-attributesbits-equiv-under-mask
              • System-segment-descriptorbits-equiv-under-mask
              • Interrupt/trap-gate-descriptorbits-debug
              • Hidden-segment-registerbits-equiv-under-mask
              • Data-segment-descriptorbits-equiv-under-mask
              • Data-segment-descriptorbits-debug
              • Data-segment-descriptor-attributesbits-debug
              • Code-segment-descriptorbits-equiv-under-mask
              • Code-segment-descriptorbits-debug
              • Code-segment-descriptor-attributesbits-debug
              • Call-gate-descriptorbits-equiv-under-mask
              • System-segment-descriptor-attributesbits-debug
              • Segment-selectorbits-equiv-under-mask
              • Interrupt/trap-gate-descriptor-attributesbits-debug
              • Call-gate-descriptorbits-debug
              • Gdtr/idtrbits-equiv-under-mask
              • Call-gate-descriptor-attributesbits-debug
              • Segment-selectorbits-debug
              • Hidden-segment-registerbits-debug
              • Gdtr/idtrbits-debug
            • 8bits
            • 2bits
            • 4bits
            • 16bits
            • Paging-bitstructs
            • 3bits
            • 11bits
            • 40bits
            • 5bits
            • 32bits
            • 19bits
            • 10bits
            • 7bits
            • 64bits
            • 54bits
            • 45bits
            • 36bits
            • 31bits
            • 24bits
            • 22bits
            • 17bits
            • 13bits
            • 12bits
            • 6bits
            • Vex->x
            • Vex->b
            • Vex-prefixes-map-p
            • Vex-prefixes-byte0-p
            • Vex->w
            • Vex->vvvv
            • Vex->r
            • Fp-bitstructs
            • Cr4bits-debug
            • Vex->pp
            • Vex->l
            • Rflagsbits-debug
            • Evex->v-prime
            • Evex->z
            • Evex->w
            • Evex->vvvv
            • Evex->vl/rc
            • Evex->pp
            • Evex->aaa
            • Xcr0bits-debug
            • Vex3-byte1-equiv-under-mask
            • Vex3-byte2-equiv-under-mask
            • Vex2-byte1-equiv-under-mask
            • Vex-prefixes-equiv-under-mask
            • Rflagsbits-equiv-under-mask
            • Ia32_eferbits-equiv-under-mask
            • Evex-prefixes-equiv-under-mask
            • Evex-byte3-equiv-under-mask
            • Evex-byte2-equiv-under-mask
            • Evex-byte1-equiv-under-mask
            • Cr0bits-debug
            • Xcr0bits-equiv-under-mask
            • Sib-equiv-under-mask
            • Prefixes-equiv-under-mask
            • Cr8bits-equiv-under-mask
            • Cr4bits-equiv-under-mask
            • Cr3bits-equiv-under-mask
            • Cr0bits-equiv-under-mask
            • Vex3-byte1-debug
            • Prefixes-debug
            • Ia32_eferbits-debug
            • Evex-byte1-debug
            • Vex3-byte2-debug
            • Vex2-byte1-debug
            • Vex-prefixes-debug
            • Evex-prefixes-debug
            • Evex-byte3-debug
            • Evex-byte2-debug
            • Cr3bits-debug
            • Sib-debug
            • Cr8bits-debug
          • Utilities
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Structures

Segmentation-bitstructs

Bitstructs related to segmentation, protection, etc.

Subtopics

System-segment-descriptorbits
AMD manual, Jun'23, Vol. 2, Figure 4-22.
Data-segment-descriptorbits
AMD manual, Jun'23, Vol. 2, Figures 4-21 and 4-15.
Code-segment-descriptorbits
AMD manual, Jun'23, Vol. 2, Figures 4-20 and 4-14.
Interrupt/trap-gate-descriptorbits
AMD manual, Jun'23, Vol. 2, Figures 4-24 and 4-18.
Call-gate-descriptorbits
AMD manual, Jun'23, Vol. 2, Figure 4-23.
Data-segment-descriptor-attributesbits
Subset of data-segment-descriptorBits.
Code-segment-descriptor-attributesbits
Subset of code-segment-descriptorBits.
System-segment-descriptor-attributesbits
Subset of system-segment-descriptorBits.
Interrupt/trap-gate-descriptor-attributesbits
Subset of interrupt/trap-gate-descriptorBits above.
Call-gate-descriptor-attributesbits
Subset of call-gate-descriptorBits.
Segment-selectorbits
Intel manual, Mar'23, Vol. 3A, Figure 3-6.
Hidden-segment-registerbits
Intel manual, Dec'23, Vol. 3A, Figure 3-7.
Gdtr/idtrbits
AMD manual, Jun'23, Vol. 2, Figure 4-8.
Interrupt/trap-gate-descriptor-attributesbits-equiv-under-mask
System-segment-descriptorbits-debug
System-segment-descriptor-attributesbits-equiv-under-mask
Interrupt/trap-gate-descriptorbits-equiv-under-mask
Data-segment-descriptor-attributesbits-equiv-under-mask
Code-segment-descriptor-attributesbits-equiv-under-mask
Call-gate-descriptor-attributesbits-equiv-under-mask
System-segment-descriptorbits-equiv-under-mask
Interrupt/trap-gate-descriptorbits-debug
Hidden-segment-registerbits-equiv-under-mask
Data-segment-descriptorbits-equiv-under-mask
Data-segment-descriptorbits-debug
Data-segment-descriptor-attributesbits-debug
Code-segment-descriptorbits-equiv-under-mask
Code-segment-descriptorbits-debug
Code-segment-descriptor-attributesbits-debug
Call-gate-descriptorbits-equiv-under-mask
System-segment-descriptor-attributesbits-debug
Segment-selectorbits-equiv-under-mask
Interrupt/trap-gate-descriptor-attributesbits-debug
Call-gate-descriptorbits-debug
Gdtr/idtrbits-equiv-under-mask
Call-gate-descriptor-attributesbits-debug
Segment-selectorbits-debug
Hidden-segment-registerbits-debug
Gdtr/idtrbits-debug