#include <config.h>
#include <util.h>
#include <api/types.h>
#include <arch/types.h>
#include <arch/model/statedata.h>
#include <arch/object/structures.h>
UP_STATE_DEFINE(interrupt_t, x86KScurInterrupt VISIBLE);
UP_STATE_DEFINE(interrupt_t, x86KSPendingInterrupt);
UP_STATE_DEFINE(tss_io_t, x86KStss VISIBLE);
UP_STATE_DEFINE(gdt_entry_t, x86KSgdt[GDT_ENTRIES]);
asid_pool_t* x86KSASIDTable[BIT(asidHighBits)];
UP_STATE_DEFINE(word_t, x86KSCurrentFSBase);
UP_STATE_DEFINE(word_t, x86KSCurrentGSBase);
UP_STATE_DEFINE(word_t, x86KSGPExceptReturnTo);
SMP_STATE_DEFINE(cpu_id_mapping_t, cpu_mapping);
UP_STATE_DEFINE(idt_entry_t, x86KSidt[IDT_ENTRIES]);
uint32_t x86KScacheLineSizeBits;
user_fpu_state_t x86KSnullFpuState ALIGN(MIN_FPU_ALIGNMENT);
uint32_t x86KSnumDrhu;
vtd_rte_t* x86KSvtdRootTable;
uint32_t x86KSnumIOPTLevels;
uint32_t x86KSnumIODomainIDBits;
uint32_t x86KSFirstValidIODomain;
#ifdef CONFIG_VTX
UP_STATE_DEFINE(vcpu_t *, x86KSCurrentVCPU);
#endif
#ifdef CONFIG_PRINTING
uint16_t x86KSconsolePort;
#endif
#ifdef CONFIG_DEBUG_BUILD
uint16_t x86KSdebugPort;
#endif
x86_irq_state_t x86KSIRQState[maxIRQ + 1];