Library mcertikos.driver.Symbols
Require Import String.
Require Import compcert.lib.Coqlib.
Require Import compcert.common.AST.
Require Import compcertx.backend.I64helpers.
Require Import liblayers.compcertx.ErrorMonad.
Require Import mcertikos.layerlib.GlobIdent.
Fixpoint reserved_symbols_aux (accu: list (ident × string)) (l: list string): res (list (ident × string)) :=
match l with
| nil ⇒ ret accu
| (s :: l´) ⇒
i <- reserved_id s;
reserved_symbols_aux ((i, s) :: accu) l´
end.
Definition reserved_symbols_strong :
{l | reserved_symbols_aux nil reserved_strings = ret l}.
Proof.
vm_compute. eauto.
Defined.
Definition reserved_symbols :=
let (l, _) := reserved_symbols_strong in l.
Open Scope string_scope.
Definition symbols: list (ident × string) :=
(AC_LOC, "AC_LOC") ::
(ATC_LOC, "ATC_LOC") ::
(AT_LOC, "AT_LOC") ::
(CAS_log, "CAS_log") ::
(CAS_ticket, "CAS_ticket") ::
(CHPOOL_LOC, "CHPOOL_LOC") ::
(CURID_LOC, "CURID_LOC") ::
(ELF_ENTRY_LOC, "ELF_ENTRY_LOC") ::
(ELF_LOC, "ELF_LOC") ::
(EPT_LOC, "EPT_LOC") ::
(FlatMem_LOC, "FlatMem_LOC") ::
(HCtxt_LOC, "HCtxt_LOC") ::
(IDPMap_LOC, "IDPMap_LOC") ::
(KCtxtPool_LOC, "KCtxtPool_LOC") ::
(MCS_LOCK_LOC, "MCS_LOCK_LOC") ::
(NPS_LOC, "NPS_LOC") ::
(NPT_LOC, "NPT_LOC") ::
(PAGE_BUFFER_LOC, "PAGE_BUFFER_LOC") ::
(PTP_LOC, "PTP_LOC") ::
(PTPool_LOC, "PTPool_LOC") ::
(QUEUE_OWNER_POOL_LOC, "QUEUE_OWNER_POOL_LOC") ::
(QUEUE_SIZE_POOL_LOC, "QUEUE_SIZE_POOL_LOC") ::
(SHRDMEMPOOL_LOC, "SHRDMEMPOOL_LOC") ::
(SLEEPER_LOC, "SLEEPER_LOC") ::
(STACK_LOC, "STACK_LOC") ::
(START_USER_FUN_LOC, "proc_start_user") ::
(START_USER_FUN_LOC2, "proc_start_user2") ::
(SYNCCHPOOL_LOC, "SYNCCHPOOL_LOC") ::
(TCBPool_LOC, "TCBPool_LOC") ::
(TDQPool_LOC, "TDQPool_LOC") ::
(TICKET_LOCK_LOC, "TICKET_LOCK_LOC") ::
(UCTX_LOC, "UCTX_LOC") ::
(VMCB_Z_LOC, "VMCB_Z_LOC") ::
(VMCS_LOC, "VMCS_LOC") ::
(VMX_LOC, "VMX_LOC") ::
(XVMST_LOC, "XVMST_LOC") ::
(acquire_lock, "acquire_lock") ::
(acquire_lock_AT, "acquire_lock_AT") ::
(acquire_lock_CHAN, "acquire_lock_CHAN") ::
(acquire_lock_PB, "acquire_lock_PB") ::
(acquire_lock_TCB, "acquire_lock_TCB") ::
(acquire_lock_TDQ, "acquire_lock_TDQ") ::
(acquire_shared, "acquire_shared") ::
(at_get, "at_get") ::
(at_get_c, "at_get_c") ::
(at_set, "at_set") ::
(at_set_c, "at_set_c") ::
(atomic_FAI, "atomic_FAI") ::
(atomic_mcs_CAS, "atomic_mcs_CAS") ::
(atomic_mcs_SWAP, "atomic_mcs_SWAP") ::
(atomic_mcs_log, "atomic_mcs_log") ::
(boot_loader, "boot_loader") ::
(clear_PDE, "clear_PDE") ::
(clear_qowner, "clear_qowner") ::
(clear_shared_mem, "clear_shared_mem") ::
(cli, "cli") ::
(cons_buf_LOC, "cons_buf_LOC") ::
(cons_buf_init, "cons_buf_init") ::
(cons_buf_init_concrete, "cons_buf_init_concrete") ::
(cons_buf_read, "cons_buf_read") ::
(cons_buf_wpos, "cons_buf_wpos") ::
(cons_buf_write, "cons_buf_write") ::
(cons_buf_write_concrete, "cons_buf_write_concrete") ::
(cons_init, "cons_init") ::
(cons_intr, "cons_intr") ::
(container_alloc, "container_alloc") ::
(container_can_consume, "container_can_consume") ::
(container_free, "container_free") ::
(container_get_nchildren, "container_get_nchildren") ::
(container_get_parent, "container_get_parent") ::
(container_get_quota, "container_get_quota") ::
(container_get_usage, "container_get_usage") ::
(container_init, "container_init") ::
(container_node_init, "container_node_init") ::
(container_revoke, "container_revoke") ::
(container_set_nchildren, "container_set_nchildren") ::
(container_set_parent, "container_set_parent") ::
(container_set_quota, "container_set_quota") ::
(container_set_usage, "container_set_usage") ::
(container_split, "container_split") ::
(curr_intr_num_LOC, "curr_intr_num_LOC") ::
(dequeue, "dequeue") ::
(dequeue_atomic, "dequeue_atomic") ::
(dequeue_local, "dequeue_local") ::
(dequeue_try, "dequeue_try") ::
(elf_load, "elf_load") ::
(enqueue, "enqueue") ::
(enqueue_atomic, "enqueue_atomic") ::
(enqueue_local, "enqueue_local") ::
(enqueue_try, "enqueue_try") ::
(ept_add_mapping, "ept_add_mapping") ::
(ept_get_page_entry, "ept_get_page_entry") ::
(ept_gpa_to_hpa, "ept_gpa_to_hpa") ::
(ept_init, "ept_init") ::
(ept_insert, "ept_insert") ::
(ept_invalidate_mappings, "ept_invalidate_mappings") ::
(ept_mmap, "ept_mmap") ::
(ept_set_page_entry, "ept_set_page_entry") ::
(ept_set_permission, "ept_set_permission") ::
(fifobbq_get_front, "fifobbq_get_front") ::
(fifobbq_get_head, "fifobbq_get_head") ::
(fifobbq_get_max, "fifobbq_get_max") ::
(fifobbq_get_next, "fifobbq_get_next") ::
(fifobbq_get_tail, "fifobbq_get_tail") ::
(fifobbq_init, "fifobbq_init") ::
(fifobbq_pool_init, "fifobbq_pool_init") ::
(fifobbq_post_insert, "fifobbq_post_insert") ::
(fifobbq_post_remove, "fifobbq_post_remove") ::
(fifobbq_pre_insert, "fifobbq_pre_insert") ::
(fifobbq_pre_remove, "fifobbq_pre_remove") ::
(fifobbq_set_front, "fifobbq_set_front") ::
(fifobbq_set_head, "fifobbq_set_head") ::
(fifobbq_set_max, "fifobbq_set_max") ::
(fifobbq_set_next, "fifobbq_set_next") ::
(fifobbq_set_tail, "fifobbq_set_tail") ::
(flatmem_copy, "flatmem_copy") ::
(fload, "fload") ::
(fstore, "fstore") ::
(gdt_LOC, "gdt_LOC") ::
(get_CPU_ID, "get_CPU_ID") ::
(get_EPTE, "get_EPTE") ::
(get_PDE, "get_PDE") ::
(get_PTE, "get_PTE") ::
(get_chan_content, "get_chan_content") ::
(get_chan_info, "get_chan_info") ::
(get_curid, "get_curid") ::
(get_curr_intr_num, "get_curr_intr_num") ::
(get_head, "get_head") ::
(get_kernel_pa, "get_kernel_pa") ::
(get_mml, "get_mml") ::
(get_mms, "get_mms") ::
(get_next, "get_next") ::
(get_now, "get_now") ::
(get_nps, "get_nps") ::
(get_prev, "get_prev") ::
(get_qowner, "get_qowner") ::
(get_qsize, "get_qsize") ::
(get_serial_exists, "get_serial_exists") ::
(get_shared_mem_loc, "get_shared_mem_loc") ::
(get_shared_mem_seen, "get_shared_mem_seen") ::
(get_shared_mem_state, "get_shared_mem_state") ::
(get_shared_mem_status_seen, "get_shared_mem_status_seen") ::
(get_size, "get_size") ::
(get_state, "get_state") ::
(get_sync_chan_busy, "get_sync_chan_busy") ::
(get_sync_chan_count, "get_sync_chan_count") ::
(get_sync_chan_paddr, "get_sync_chan_paddr") ::
(get_sync_chan_to, "get_sync_chan_to") ::
(get_tail, "get_tail") ::
(host_in, "host_in") ::
(host_out, "host_out") ::
(hw_intr, "hw_intr") ::
(ic_intr, "ic_intr") ::
(idpde_init, "idpde_init") ::
(idq_get_next, "idq_get_next") ::
(idq_get_prev, "idq_get_prev") ::
(idq_init, "idq_init") ::
(idq_peek, "idq_peek") ::
(idq_pool_init, "idq_pool_init") ::
(idq_pull, "idq_pull") ::
(idq_push, "idq_push") ::
(idq_set_next, "idq_set_next") ::
(idq_set_prev, "idq_set_prev") ::
(idt_LOC, "idt_LOC") ::
(incr_now, "incr_now") ::
(incr_ticket, "incr_ticket") ::
(init_chan, "init_chan") ::
(init_qowner, "init_qowner") ::
(init_sync_chan, "init_sync_chan") ::
(init_ticket, "init_ticket") ::
(interrupt_handler, "interrupt_handler") ::
(intr_default_handler, "intr_default_handler") ::
(io_bitmap_LOC, "io_bitmap_LOC") ::
(ioapic_enable, "ioapic_enable") ::
(ioapic_init, "ioapic_init") ::
(ioapic_mask, "ioapic_mask") ::
(ioapic_read, "ioapic_read") ::
(ioapic_unmask, "ioapic_unmask") ::
(ioapic_write, "ioapic_write") ::
(ipc_receive_body, "ipc_receive_body") ::
(ipc_send_body, "ipc_send_body") ::
(iret, "iret") ::
(is_chan_ready, "is_chan_ready") ::
(is_norm, "is_norm") ::
(is_pid_sending_to, "is_pid_sending_to") ::
(is_usable, "is_usable") ::
(is_used, "is_used") ::
(kbd_buf_LOC, "kbd_buf_LOC") ::
(kbd_buf_init, "kbd_buf_init") ::
(kbd_buf_init_concrete, "kbd_buf_init_concrete") ::
(kbd_buf_read, "kbd_buf_read") ::
(kbd_buf_write, "kbd_buf_write") ::
(kbd_buf_write_concrete, "kbd_buf_write_concrete") ::
(kbd_intr_disable, "kbd_intr_disable") ::
(kbd_intr_disable_handler, "kbd_intr_disable_handler") ::
(kbd_intr_enable, "kbd_intr_enable") ::
(kbd_states_LOC, "kbd_states_LOC") ::
(kctxt_new, "kctxt_new") ::
(kctxt_switch, "kctxt_switch") ::
(keyboard_getc, "keyboard_getc") ::
(keyboard_hw_intr, "keyboard_hw_intr") ::
(keyboard_in, "keyboard_in") ::
(keyboard_init, "keyboard_init") ::
(keyboard_intr, "keyboard_intr") ::
(keyboard_irq_check, "keyboard_irq_check") ::
(keyboard_map, "keyboard_map") ::
(keyboard_proc_data, "keyboard_proc_data") ::
(keyboard_scan, "keyboard_scan") ::
(keyboard_scan_code_normal_LOC, "keyboard_scan_code_normal_LOC") ::
(keyboard_scan_code_shift_LOC, "keyboard_scan_code_shift_LOC") ::
(keyboard_shift_check, "keyboard_shift_check") ::
(keyboard_shift_reset, "keyboard_shift_reset") ::
(keyboard_shift_toggle, "keyboard_shift_toggle") ::
(keyboard_switch_key_map, "keyboard_switch_key_map") ::
(la2pa_resv, "la2pa_resv") ::
(lapic_eoi, "lapic_eoi") ::
(lapic_init, "lapic_init") ::
(lapic_read, "lapic_read") ::
(lapic_write, "lapic_write") ::
(local_irq_restore, "local_irq_restore") ::
(local_irq_save, "local_irq_save") ::
(log_get, "log_get") ::
(log_hold, "log_hold") ::
(log_incr, "log_incr") ::
(log_init, "log_init") ::
(mcs_CAS_TAIL, "mcs_CAS_TAIL") ::
(mcs_GET_BUSY, "mcs_GET_BUSY") ::
(mcs_GET_BUSY_log, "mcs_GET_BUSY_log") ::
(mcs_GET_NEXT, "mcs_GET_NEXT") ::
(mcs_GET_NEXT_log, "mcs_GET_NEXT_log") ::
(mcs_SET_BUSY, "mcs_SET_BUSY") ::
(mcs_SET_BUSY_log, "mcs_SET_BUSY_log") ::
(mcs_SET_NEXT, "mcs_SET_NEXT") ::
(mcs_SET_NEXT_log, "mcs_SET_NEXT_log") ::
(mcs_SWAP_TAIL, "mcs_SWAP_TAIL") ::
(mcs_cas_tail, "mcs_cas_tail") ::
(mcs_get_busy, "mcs_get_busy") ::
(mcs_get_next, "mcs_get_next") ::
(mcs_init_node, "mcs_init_node") ::
(mcs_init_node_log, "mcs_init_node_log") ::
(mcs_lock_get_index, "mcs_lock_get_index") ::
(mcs_lock_init, "mcs_lock_init") ::
(mcs_log, "mcs_log") ::
(mcs_pass_lock, "mcs_pass_lock") ::
(mcs_set_busy, "mcs_set_busy") ::
(mcs_set_next, "mcs_set_next") ::
(mcs_swap_tail, "mcs_swap_tail") ::
(mcs_wait_lock, "mcs_wait_lock") ::
(mem_init, "mem_init") ::
(msr_bitmap_LOC, "msr_bitmap_LOC") ::
(npt_init, "npt_init") ::
(npt_insert, "npt_insert") ::
(offer_shared_mem, "offer_shared_mem") ::
(page_copy, "page_copy") ::
(page_copy_back, "page_copy_back") ::
(palloc, "palloc") ::
(palloc_aux, "palloc_aux") ::
(pass_lock, "pass_lock") ::
(pass_queue, "pass_queue") ::
(pcpumsg_recv, "pcpumsg_recv") ::
(pcpumsg_send, "pcpumsg_send") ::
(pcpumsg_try_recv, "pcpumsg_try_recv") ::
(pfree, "pfree") ::
(pgf_handler, "pgf_handler") ::
(pmap_init, "pmap_init") ::
(pre_acquire_lock, "pre_acquire_lock") ::
(proc_create, "proc_create") ::
(proc_create_postinit, "proc_create_postinit") ::
(proc_exit_user, "proc_exit_user") ::
(proc_exit_user2, "proc_exit_user2") ::
(proc_init, "proc_init") ::
(proc_start_user, "proc_start_user") ::
(proc_start_user2, "proc_start_user2") ::
(pt_alloc_pde, "pt_alloc_pde") ::
(pt_free, "pt_free") ::
(pt_free_pde, "pt_free_pde") ::
(pt_in, "pt_in") ::
(pt_init, "pt_init") ::
(pt_init_comm, "pt_init_comm") ::
(pt_init_kern, "pt_init_kern") ::
(pt_insert, "pt_insert") ::
(pt_insert_aux, "pt_insert_aux") ::
(pt_insert_pde, "pt_insert_pde") ::
(pt_new, "pt_new") ::
(pt_out, "pt_out") ::
(pt_read, "pt_read") ::
(pt_read_pde, "pt_read_pde") ::
(pt_resv, "pt_resv") ::
(pt_resv2, "pt_resv2") ::
(pt_rmv, "pt_rmv") ::
(pt_rmv_aux, "pt_rmv_aux") ::
(pt_rmv_pde, "pt_rmv_pde") ::
(ptfault_resv, "ptfault_resv") ::
(queue_rmv, "queue_rmv") ::
(queue_rmv_atomic, "queue_rmv_atomic") ::
(queue_rmv_local, "queue_rmv_local") ::
(queue_rmv_try, "queue_rmv_try") ::
(rcr0, "rcr0") ::
(rcr3, "rcr3") ::
(rcr4, "rcr4") ::
(rdmsr, "rdmsr") ::
(read_now, "read_now") ::
(receive_chan, "receive_chan") ::
(release_lock, "release_lock") ::
(release_lock_AT, "release_lock_AT") ::
(release_lock_CHAN, "release_lock_CHAN") ::
(release_lock_PB, "release_lock_PB") ::
(release_lock_TCB, "release_lock_TCB") ::
(release_lock_TDQ, "release_lock_TDQ") ::
(release_shared, "release_shared") ::
(restore_context, "restore_context") ::
(restore_hctx, "restore_hctx") ::
(restore_uctx, "restore_uctx") ::
(rmv_PDE, "rmv_PDE") ::
(rmv_PTE, "rmv_PTE") ::
(save_context, "save_context") ::
(save_hctx, "save_hctx") ::
(save_uctx, "save_uctx") ::
(sched_init, "sched_init") ::
(sendto_chan, "sendto_chan") ::
(serial_exists_LOC, "serial_exists_LOC") ::
(serial_getc, "serial_getc") ::
(serial_hw_intr, "serial_hw_intr") ::
(serial_in, "serial_in") ::
(serial_init, "serial_init") ::
(serial_intr_disable, "serial_intr_disable") ::
(serial_intr_disable_handler, "serial_intr_disable_handler") ::
(serial_intr_enable, "serial_intr_enable") ::
(serial_intr_enable_handler, "serial_intr_enable_handler") ::
(serial_intr_handler_asm, "serial_intr_handler_asm") ::
(serial_intr_handler_ext, "serial_intr_handler_ext") ::
(serial_intr_handler_sw, "serial_intr_handler_sw") ::
(serial_irq_check, "serial_irq_check") ::
(serial_irq_current, "serial_irq_current") ::
(serial_out, "serial_out") ::
(serial_putc, "serial_putc") ::
(set_EPDPTE, "set_EPDPTE") ::
(set_EPDTE, "set_EPDTE") ::
(set_EPML4E, "set_EPML4E") ::
(set_EPTE, "set_EPTE") ::
(set_IDPTE, "set_IDPTE") ::
(set_NPDE, "set_NPDE") ::
(set_NPTE, "set_NPTE") ::
(set_PDE, "set_PDE") ::
(set_PDEU, "set_PDEU") ::
(set_PTE, "set_PTE") ::
(set_RA, "set_RA") ::
(set_SP, "set_SP") ::
(set_bit, "set_bit") ::
(set_chan_content, "set_chan_content") ::
(set_chan_info, "set_chan_info") ::
(set_cr3, "set_cr3") ::
(set_curid, "set_curid") ::
(set_curid_init, "set_curid_init") ::
(set_head, "set_head") ::
(set_lock_status, "set_lock_status") ::
(set_next, "set_next") ::
(set_norm, "set_norm") ::
(set_nps, "set_nps") ::
(set_pg, "set_pg") ::
(set_prev, "set_prev") ::
(set_pt, "set_pt") ::
(set_qowner, "set_qowner") ::
(set_qsize, "set_qsize") ::
(set_serial_exists, "set_serial_exists") ::
(set_shared_mem_loc, "set_shared_mem_loc") ::
(set_shared_mem_seen, "set_shared_mem_seen") ::
(set_shared_mem_state, "set_shared_mem_state") ::
(set_state, "set_state") ::
(set_sync_chan_busy, "set_sync_chan_busy") ::
(set_sync_chan_count, "set_sync_chan_count") ::
(set_sync_chan_paddr, "set_sync_chan_paddr") ::
(set_sync_chan_to, "set_sync_chan_to") ::
(set_tail, "set_tail") ::
(set_tf, "set_tf") ::
(shared_mem_init, "shared_mem_init") ::
(shared_mem_status, "shared_mem_status") ::
(shared_mem_to_dead, "shared_mem_to_dead") ::
(shared_mem_to_pending, "shared_mem_to_pending") ::
(shared_mem_to_ready, "shared_mem_to_ready") ::
(sleeper_dec, "sleeper_dec") ::
(sleeper_get, "sleeper_get") ::
(sleeper_inc, "sleeper_inc") ::
(sleeper_set, "sleeper_set") ::
(sleeper_zzz, "sleeper_zzz") ::
(srecv_chan, "srecv_chan") ::
(ssend_to_chan, "ssend_to_chan") ::
(sti, "sti") ::
(svm_exit_vm, "svm_exit_vm") ::
(svm_get_exit_fault_addr, "svm_get_exit_fault_addr") ::
(svm_get_exit_io_neip, "svm_get_exit_io_neip") ::
(svm_get_exit_io_port, "svm_get_exit_io_port") ::
(svm_get_exit_io_rep, "svm_get_exit_io_rep") ::
(svm_get_exit_io_str, "svm_get_exit_io_str") ::
(svm_get_exit_io_width, "svm_get_exit_io_width") ::
(svm_get_exit_io_write, "svm_get_exit_io_write") ::
(svm_get_exit_reason, "svm_get_exit_reason") ::
(svm_get_reg, "svm_get_reg") ::
(svm_run_vm, "svm_run_vm") ::
(svm_set_intercept_intwin, "svm_set_intercept_intwin") ::
(svm_set_reg, "svm_set_reg") ::
(svm_state_save, "svm_state_save") ::
(svm_sync, "svm_sync") ::
(syncreceive_chan, "syncreceive_chan") ::
(syncsendto_chan, "syncsendto_chan") ::
(syncsendto_chan_post, "syncsendto_chan_post") ::
(syncsendto_chan_pre, "syncsendto_chan_pre") ::
(sys_certikos_init, "sys_certikos_init") ::
(sys_check_int_shadow, "sys_check_int_shadow") ::
(sys_check_pending_event, "sys_check_pending_event") ::
(sys_disk_cap, "sys_disk_cap") ::
(sys_disk_op, "sys_disk_op") ::
(sys_ept_insert, "sys_ept_insert") ::
(sys_get_curid, "sys_get_curid") ::
(sys_get_exit_fault_addr, "sys_get_exit_fault_addr") ::
(sys_get_exit_io_neip, "sys_get_exit_io_neip") ::
(sys_get_exit_io_port, "sys_get_exit_io_port") ::
(sys_get_exit_io_rep, "sys_get_exit_io_rep") ::
(sys_get_exit_io_str, "sys_get_exit_io_str") ::
(sys_get_exit_io_width, "sys_get_exit_io_width") ::
(sys_get_exit_io_write, "sys_get_exit_io_write") ::
(sys_get_exit_reason, "sys_get_exit_reason") ::
(sys_get_exitinfo, "sys_get_exitinfo") ::
(sys_get_next_eip, "sys_get_next_eip") ::
(sys_get_quota, "sys_get_quota") ::
(sys_get_reg, "sys_get_reg") ::
(sys_get_tsc_offset, "sys_get_tsc_offset") ::
(sys_get_tsc_per_ms, "sys_get_tsc_per_ms") ::
(sys_getc, "sys_getc") ::
(sys_handle_rdmsr, "sys_handle_rdmsr") ::
(sys_handle_wrmsr, "sys_handle_wrmsr") ::
(sys_inject_event, "sys_inject_event") ::
(sys_intercept_int_window, "sys_intercept_int_window") ::
(sys_is_chan_ready, "sys_is_chan_ready") ::
(sys_mmap, "sys_mmap") ::
(sys_npt_insert, "sys_npt_insert") ::
(sys_palloc, "sys_palloc") ::
(sys_pfree, "sys_pfree") ::
(sys_proc_create, "sys_proc_create") ::
(sys_pt_read, "sys_pt_read") ::
(sys_putc, "sys_putc") ::
(sys_puts, "sys_puts") ::
(sys_ready, "sys_ready") ::
(sys_receive_chan, "sys_receive_chan") ::
(sys_recv, "sys_recv") ::
(sys_ring0_spawn, "sys_ring0_spawn") ::
(sys_run_vm, "sys_run_vm") ::
(sys_send, "sys_send") ::
(sys_sendto_chan, "sys_sendto_chan") ::
(sys_sendtochan_post, "sys_sendtochan_post") ::
(sys_sendtochan_pre, "sys_sendtochan_pre") ::
(sys_set_intercept_intwin, "sys_set_intercept_intwin") ::
(sys_set_reg, "sys_set_reg") ::
(sys_set_seg, "sys_set_seg") ::
(sys_set_seg1, "sys_set_seg1") ::
(sys_set_seg2, "sys_set_seg2") ::
(sys_set_tsc_offset, "sys_set_tsc_offset") ::
(sys_sleep, "sys_sleep") ::
(sys_spawn, "sys_spawn") ::
(sys_srecv_chan, "sys_srecv_chan") ::
(sys_ssend_to_chan, "sys_ssend_to_chan") ::
(sys_svm_exit_vm, "sys_svm_exit_vm") ::
(sys_sync, "sys_sync") ::
(sys_thread_kill, "sys_thread_kill") ::
(sys_thread_sleep, "sys_thread_sleep") ::
(sys_thread_wakeup, "sys_thread_wakeup") ::
(sys_thread_yield, "sys_thread_yield") ::
(sys_tryreceive_chan, "sys_tryreceive_chan") ::
(sys_tryrecv, "sys_tryrecv") ::
(sys_trysend, "sys_trysend") ::
(sys_trysendto_chan, "sys_trysendto_chan") ::
(sys_uctx_get, "sys_uctx_get") ::
(sys_uctx_set, "sys_uctx_set") ::
(sys_yield, "sys_yield") ::
(syscall_dispatch, "syscall_dispatch") ::
(syscall_dispatch_C, "syscall_dispatch_C") ::
(tcb_get_CPU_ID, "tcb_get_CPU_ID") ::
(tcb_init, "tcb_init") ::
(tcb_set_CPU_ID, "tcb_set_CPU_ID") ::
(tdq_init, "tdq_init") ::
(tdqueue_init, "tdqueue_init") ::
(test_lock, "test_lock") ::
(thread_free, "thread_free") ::
(thread_init, "thread_init") ::
(thread_kill, "thread_kill") ::
(thread_poll_pending, "thread_poll_pending") ::
(thread_sched, "thread_sched") ::
(thread_sleep, "thread_sleep") ::
(thread_sleep2, "thread_sleep2") ::
(thread_sleep_lock, "thread_sleep_lock") ::
(thread_spawn, "thread_spawn") ::
(thread_wakeup, "thread_wakeup") ::
(thread_wakeup2, "thread_wakeup2") ::
(thread_wakeup_lock, "thread_wakeup_lock") ::
(thread_yield, "thread_yield") ::
(ticket_lock_init, "ticket_lock_init") ::
(trap_get, "trap_get") ::
(trap_in, "trap_in") ::
(trap_out, "trap_out") ::
(trap_sendtochan_post, "trap_sendtochan_post") ::
(trap_sendtochan_pre, "trap_sendtochan_pre") ::
(trap_set, "trap_set") ::
(try_lock, "try_lock") ::
(try_lock_AT, "try_lock_AT") ::
(try_lock_CHAN, "try_lock_CHAN") ::
(try_lock_PB, "try_lock_PB") ::
(try_lock_TCB, "try_lock_TCB") ::
(try_lock_TDQ, "try_lock_TDQ") ::
(tryreceive_chan, "tryreceive_chan") ::
(trysendto_chan, "trysendto_chan") ::
(tss_LOC, "tss_LOC") ::
(uctx_arg1, "uctx_arg1") ::
(uctx_arg2, "uctx_arg2") ::
(uctx_arg3, "uctx_arg3") ::
(uctx_arg4, "uctx_arg4") ::
(uctx_arg5, "uctx_arg5") ::
(uctx_arg6, "uctx_arg6") ::
(uctx_get, "uctx_get") ::
(uctx_set, "uctx_set") ::
(uctx_set_eip, "uctx_set_eip") ::
(uctx_set_errno, "uctx_set_errno") ::
(uctx_set_retval1, "uctx_set_retval1") ::
(uctx_set_retval2, "uctx_set_retval2") ::
(uctx_set_retval3, "uctx_set_retval3") ::
(uctx_set_retval4, "uctx_set_retval4") ::
(vmcb_check_int_shadow, "vmcb_check_int_shadow") ::
(vmcb_check_pending_event, "vmcb_check_pending_event") ::
(vmcb_clear_virq, "vmcb_clear_virq") ::
(vmcb_get_exit_info, "vmcb_get_exit_info") ::
(vmcb_get_next_eip, "vmcb_get_next_eip") ::
(vmcb_get_reg, "vmcb_get_reg") ::
(vmcb_inject_event, "vmcb_inject_event") ::
(vmcb_inject_virq, "vmcb_inject_virq") ::
(vmcb_read_v, "vmcb_read_v") ::
(vmcb_read_z, "vmcb_read_z") ::
(vmcb_restore, "vmcb_restore") ::
(vmcb_set_intercept_vint, "vmcb_set_intercept_vint") ::
(vmcb_set_reg, "vmcb_set_reg") ::
(vmcb_set_seg, "vmcb_set_seg") ::
(vmcb_write_v, "vmcb_write_v") ::
(vmcb_write_z, "vmcb_write_z") ::
(vmcs_get_abrtid, "vmcs_get_abrtid") ::
(vmcs_get_revid, "vmcs_get_revid") ::
(vmcs_read, "vmcs_read") ::
(vmcs_readz, "vmcs_readz") ::
(vmcs_readz64, "vmcs_readz64") ::
(vmcs_set_abrtid, "vmcs_set_abrtid") ::
(vmcs_set_defaults, "vmcs_set_defaults") ::
(vmcs_set_revid, "vmcs_set_revid") ::
(vmcs_write, "vmcs_write") ::
(vmcs_write_ident, "vmcs_write_ident") ::
(vmcs_writez, "vmcs_writez") ::
(vmcs_writez64, "vmcs_writez64") ::
(vmptrld, "vmptrld") ::
(vmx_check_int_shadow, "vmx_check_int_shadow") ::
(vmx_check_pending_event, "vmx_check_pending_event") ::
(vmx_enable, "vmx_enable") ::
(vmx_enter, "vmx_enter") ::
(vmx_enter_bottom_half, "vmx_enter_bottom_half") ::
(vmx_enter_pre, "vmx_enter_pre") ::
(vmx_exit, "vmx_exit") ::
(vmx_exit_bottom_half, "vmx_exit_bottom_half") ::
(vmx_exit_post, "vmx_exit_post") ::
(vmx_get_exit_fault_addr, "vmx_get_exit_fault_addr") ::
(vmx_get_exit_io_port, "vmx_get_exit_io_port") ::
(vmx_get_exit_io_rep, "vmx_get_exit_io_rep") ::
(vmx_get_exit_io_str, "vmx_get_exit_io_str") ::
(vmx_get_exit_qualification, "vmx_get_exit_qualification") ::
(vmx_get_exit_reason, "vmx_get_exit_reason") ::
(vmx_get_io_width, "vmx_get_io_width") ::
(vmx_get_io_write, "vmx_get_io_write") ::
(vmx_get_next_eip, "vmx_get_next_eip") ::
(vmx_get_reg, "vmx_get_reg") ::
(vmx_get_tsc_offset, "vmx_get_tsc_offset") ::
(vmx_init, "vmx_init") ::
(vmx_inject_event, "vmx_inject_event") ::
(vmx_read, "vmx_read") ::
(vmx_readz, "vmx_readz") ::
(vmx_readz64, "vmx_readz64") ::
(vmx_return_from_guest, "vmx_return_from_guest") ::
(vmx_run_return_from_guest, "vmx_run_return_from_guest") ::
(vmx_run_vm, "vmx_run_vm") ::
(vmx_set_ctlreg, "vmx_set_ctlreg") ::
(vmx_set_desc, "vmx_set_desc") ::
(vmx_set_desc1, "vmx_set_desc1") ::
(vmx_set_desc2, "vmx_set_desc2") ::
(vmx_set_intercept_intwin, "vmx_set_intercept_intwin") ::
(vmx_set_mmap, "vmx_set_mmap") ::
(vmx_set_reg, "vmx_set_reg") ::
(vmx_set_tsc_offset, "vmx_set_tsc_offset") ::
(vmx_write, "vmx_write") ::
(vmx_writez, "vmx_writez") ::
(vmx_writez64, "vmx_writez64") ::
(vmxinfo_get, "vmxinfo_get") ::
(vmxon, "vmxon") ::
(wait_lock, "wait_lock") ::
(wait_queue, "wait_queue") ::
(wrmsr, "wrmsr") ::
(xvmst_read, "xvmst_read") ::
(xvmst_restore, "xvmst_restore") ::
(xvmst_write, "xvmst_write") ::
reserved_symbols.
Require Import compcert.lib.Coqlib.
Require Import compcert.common.AST.
Require Import compcertx.backend.I64helpers.
Require Import liblayers.compcertx.ErrorMonad.
Require Import mcertikos.layerlib.GlobIdent.
Fixpoint reserved_symbols_aux (accu: list (ident × string)) (l: list string): res (list (ident × string)) :=
match l with
| nil ⇒ ret accu
| (s :: l´) ⇒
i <- reserved_id s;
reserved_symbols_aux ((i, s) :: accu) l´
end.
Definition reserved_symbols_strong :
{l | reserved_symbols_aux nil reserved_strings = ret l}.
Proof.
vm_compute. eauto.
Defined.
Definition reserved_symbols :=
let (l, _) := reserved_symbols_strong in l.
Open Scope string_scope.
Definition symbols: list (ident × string) :=
(AC_LOC, "AC_LOC") ::
(ATC_LOC, "ATC_LOC") ::
(AT_LOC, "AT_LOC") ::
(CAS_log, "CAS_log") ::
(CAS_ticket, "CAS_ticket") ::
(CHPOOL_LOC, "CHPOOL_LOC") ::
(CURID_LOC, "CURID_LOC") ::
(ELF_ENTRY_LOC, "ELF_ENTRY_LOC") ::
(ELF_LOC, "ELF_LOC") ::
(EPT_LOC, "EPT_LOC") ::
(FlatMem_LOC, "FlatMem_LOC") ::
(HCtxt_LOC, "HCtxt_LOC") ::
(IDPMap_LOC, "IDPMap_LOC") ::
(KCtxtPool_LOC, "KCtxtPool_LOC") ::
(MCS_LOCK_LOC, "MCS_LOCK_LOC") ::
(NPS_LOC, "NPS_LOC") ::
(NPT_LOC, "NPT_LOC") ::
(PAGE_BUFFER_LOC, "PAGE_BUFFER_LOC") ::
(PTP_LOC, "PTP_LOC") ::
(PTPool_LOC, "PTPool_LOC") ::
(QUEUE_OWNER_POOL_LOC, "QUEUE_OWNER_POOL_LOC") ::
(QUEUE_SIZE_POOL_LOC, "QUEUE_SIZE_POOL_LOC") ::
(SHRDMEMPOOL_LOC, "SHRDMEMPOOL_LOC") ::
(SLEEPER_LOC, "SLEEPER_LOC") ::
(STACK_LOC, "STACK_LOC") ::
(START_USER_FUN_LOC, "proc_start_user") ::
(START_USER_FUN_LOC2, "proc_start_user2") ::
(SYNCCHPOOL_LOC, "SYNCCHPOOL_LOC") ::
(TCBPool_LOC, "TCBPool_LOC") ::
(TDQPool_LOC, "TDQPool_LOC") ::
(TICKET_LOCK_LOC, "TICKET_LOCK_LOC") ::
(UCTX_LOC, "UCTX_LOC") ::
(VMCB_Z_LOC, "VMCB_Z_LOC") ::
(VMCS_LOC, "VMCS_LOC") ::
(VMX_LOC, "VMX_LOC") ::
(XVMST_LOC, "XVMST_LOC") ::
(acquire_lock, "acquire_lock") ::
(acquire_lock_AT, "acquire_lock_AT") ::
(acquire_lock_CHAN, "acquire_lock_CHAN") ::
(acquire_lock_PB, "acquire_lock_PB") ::
(acquire_lock_TCB, "acquire_lock_TCB") ::
(acquire_lock_TDQ, "acquire_lock_TDQ") ::
(acquire_shared, "acquire_shared") ::
(at_get, "at_get") ::
(at_get_c, "at_get_c") ::
(at_set, "at_set") ::
(at_set_c, "at_set_c") ::
(atomic_FAI, "atomic_FAI") ::
(atomic_mcs_CAS, "atomic_mcs_CAS") ::
(atomic_mcs_SWAP, "atomic_mcs_SWAP") ::
(atomic_mcs_log, "atomic_mcs_log") ::
(boot_loader, "boot_loader") ::
(clear_PDE, "clear_PDE") ::
(clear_qowner, "clear_qowner") ::
(clear_shared_mem, "clear_shared_mem") ::
(cli, "cli") ::
(cons_buf_LOC, "cons_buf_LOC") ::
(cons_buf_init, "cons_buf_init") ::
(cons_buf_init_concrete, "cons_buf_init_concrete") ::
(cons_buf_read, "cons_buf_read") ::
(cons_buf_wpos, "cons_buf_wpos") ::
(cons_buf_write, "cons_buf_write") ::
(cons_buf_write_concrete, "cons_buf_write_concrete") ::
(cons_init, "cons_init") ::
(cons_intr, "cons_intr") ::
(container_alloc, "container_alloc") ::
(container_can_consume, "container_can_consume") ::
(container_free, "container_free") ::
(container_get_nchildren, "container_get_nchildren") ::
(container_get_parent, "container_get_parent") ::
(container_get_quota, "container_get_quota") ::
(container_get_usage, "container_get_usage") ::
(container_init, "container_init") ::
(container_node_init, "container_node_init") ::
(container_revoke, "container_revoke") ::
(container_set_nchildren, "container_set_nchildren") ::
(container_set_parent, "container_set_parent") ::
(container_set_quota, "container_set_quota") ::
(container_set_usage, "container_set_usage") ::
(container_split, "container_split") ::
(curr_intr_num_LOC, "curr_intr_num_LOC") ::
(dequeue, "dequeue") ::
(dequeue_atomic, "dequeue_atomic") ::
(dequeue_local, "dequeue_local") ::
(dequeue_try, "dequeue_try") ::
(elf_load, "elf_load") ::
(enqueue, "enqueue") ::
(enqueue_atomic, "enqueue_atomic") ::
(enqueue_local, "enqueue_local") ::
(enqueue_try, "enqueue_try") ::
(ept_add_mapping, "ept_add_mapping") ::
(ept_get_page_entry, "ept_get_page_entry") ::
(ept_gpa_to_hpa, "ept_gpa_to_hpa") ::
(ept_init, "ept_init") ::
(ept_insert, "ept_insert") ::
(ept_invalidate_mappings, "ept_invalidate_mappings") ::
(ept_mmap, "ept_mmap") ::
(ept_set_page_entry, "ept_set_page_entry") ::
(ept_set_permission, "ept_set_permission") ::
(fifobbq_get_front, "fifobbq_get_front") ::
(fifobbq_get_head, "fifobbq_get_head") ::
(fifobbq_get_max, "fifobbq_get_max") ::
(fifobbq_get_next, "fifobbq_get_next") ::
(fifobbq_get_tail, "fifobbq_get_tail") ::
(fifobbq_init, "fifobbq_init") ::
(fifobbq_pool_init, "fifobbq_pool_init") ::
(fifobbq_post_insert, "fifobbq_post_insert") ::
(fifobbq_post_remove, "fifobbq_post_remove") ::
(fifobbq_pre_insert, "fifobbq_pre_insert") ::
(fifobbq_pre_remove, "fifobbq_pre_remove") ::
(fifobbq_set_front, "fifobbq_set_front") ::
(fifobbq_set_head, "fifobbq_set_head") ::
(fifobbq_set_max, "fifobbq_set_max") ::
(fifobbq_set_next, "fifobbq_set_next") ::
(fifobbq_set_tail, "fifobbq_set_tail") ::
(flatmem_copy, "flatmem_copy") ::
(fload, "fload") ::
(fstore, "fstore") ::
(gdt_LOC, "gdt_LOC") ::
(get_CPU_ID, "get_CPU_ID") ::
(get_EPTE, "get_EPTE") ::
(get_PDE, "get_PDE") ::
(get_PTE, "get_PTE") ::
(get_chan_content, "get_chan_content") ::
(get_chan_info, "get_chan_info") ::
(get_curid, "get_curid") ::
(get_curr_intr_num, "get_curr_intr_num") ::
(get_head, "get_head") ::
(get_kernel_pa, "get_kernel_pa") ::
(get_mml, "get_mml") ::
(get_mms, "get_mms") ::
(get_next, "get_next") ::
(get_now, "get_now") ::
(get_nps, "get_nps") ::
(get_prev, "get_prev") ::
(get_qowner, "get_qowner") ::
(get_qsize, "get_qsize") ::
(get_serial_exists, "get_serial_exists") ::
(get_shared_mem_loc, "get_shared_mem_loc") ::
(get_shared_mem_seen, "get_shared_mem_seen") ::
(get_shared_mem_state, "get_shared_mem_state") ::
(get_shared_mem_status_seen, "get_shared_mem_status_seen") ::
(get_size, "get_size") ::
(get_state, "get_state") ::
(get_sync_chan_busy, "get_sync_chan_busy") ::
(get_sync_chan_count, "get_sync_chan_count") ::
(get_sync_chan_paddr, "get_sync_chan_paddr") ::
(get_sync_chan_to, "get_sync_chan_to") ::
(get_tail, "get_tail") ::
(host_in, "host_in") ::
(host_out, "host_out") ::
(hw_intr, "hw_intr") ::
(ic_intr, "ic_intr") ::
(idpde_init, "idpde_init") ::
(idq_get_next, "idq_get_next") ::
(idq_get_prev, "idq_get_prev") ::
(idq_init, "idq_init") ::
(idq_peek, "idq_peek") ::
(idq_pool_init, "idq_pool_init") ::
(idq_pull, "idq_pull") ::
(idq_push, "idq_push") ::
(idq_set_next, "idq_set_next") ::
(idq_set_prev, "idq_set_prev") ::
(idt_LOC, "idt_LOC") ::
(incr_now, "incr_now") ::
(incr_ticket, "incr_ticket") ::
(init_chan, "init_chan") ::
(init_qowner, "init_qowner") ::
(init_sync_chan, "init_sync_chan") ::
(init_ticket, "init_ticket") ::
(interrupt_handler, "interrupt_handler") ::
(intr_default_handler, "intr_default_handler") ::
(io_bitmap_LOC, "io_bitmap_LOC") ::
(ioapic_enable, "ioapic_enable") ::
(ioapic_init, "ioapic_init") ::
(ioapic_mask, "ioapic_mask") ::
(ioapic_read, "ioapic_read") ::
(ioapic_unmask, "ioapic_unmask") ::
(ioapic_write, "ioapic_write") ::
(ipc_receive_body, "ipc_receive_body") ::
(ipc_send_body, "ipc_send_body") ::
(iret, "iret") ::
(is_chan_ready, "is_chan_ready") ::
(is_norm, "is_norm") ::
(is_pid_sending_to, "is_pid_sending_to") ::
(is_usable, "is_usable") ::
(is_used, "is_used") ::
(kbd_buf_LOC, "kbd_buf_LOC") ::
(kbd_buf_init, "kbd_buf_init") ::
(kbd_buf_init_concrete, "kbd_buf_init_concrete") ::
(kbd_buf_read, "kbd_buf_read") ::
(kbd_buf_write, "kbd_buf_write") ::
(kbd_buf_write_concrete, "kbd_buf_write_concrete") ::
(kbd_intr_disable, "kbd_intr_disable") ::
(kbd_intr_disable_handler, "kbd_intr_disable_handler") ::
(kbd_intr_enable, "kbd_intr_enable") ::
(kbd_states_LOC, "kbd_states_LOC") ::
(kctxt_new, "kctxt_new") ::
(kctxt_switch, "kctxt_switch") ::
(keyboard_getc, "keyboard_getc") ::
(keyboard_hw_intr, "keyboard_hw_intr") ::
(keyboard_in, "keyboard_in") ::
(keyboard_init, "keyboard_init") ::
(keyboard_intr, "keyboard_intr") ::
(keyboard_irq_check, "keyboard_irq_check") ::
(keyboard_map, "keyboard_map") ::
(keyboard_proc_data, "keyboard_proc_data") ::
(keyboard_scan, "keyboard_scan") ::
(keyboard_scan_code_normal_LOC, "keyboard_scan_code_normal_LOC") ::
(keyboard_scan_code_shift_LOC, "keyboard_scan_code_shift_LOC") ::
(keyboard_shift_check, "keyboard_shift_check") ::
(keyboard_shift_reset, "keyboard_shift_reset") ::
(keyboard_shift_toggle, "keyboard_shift_toggle") ::
(keyboard_switch_key_map, "keyboard_switch_key_map") ::
(la2pa_resv, "la2pa_resv") ::
(lapic_eoi, "lapic_eoi") ::
(lapic_init, "lapic_init") ::
(lapic_read, "lapic_read") ::
(lapic_write, "lapic_write") ::
(local_irq_restore, "local_irq_restore") ::
(local_irq_save, "local_irq_save") ::
(log_get, "log_get") ::
(log_hold, "log_hold") ::
(log_incr, "log_incr") ::
(log_init, "log_init") ::
(mcs_CAS_TAIL, "mcs_CAS_TAIL") ::
(mcs_GET_BUSY, "mcs_GET_BUSY") ::
(mcs_GET_BUSY_log, "mcs_GET_BUSY_log") ::
(mcs_GET_NEXT, "mcs_GET_NEXT") ::
(mcs_GET_NEXT_log, "mcs_GET_NEXT_log") ::
(mcs_SET_BUSY, "mcs_SET_BUSY") ::
(mcs_SET_BUSY_log, "mcs_SET_BUSY_log") ::
(mcs_SET_NEXT, "mcs_SET_NEXT") ::
(mcs_SET_NEXT_log, "mcs_SET_NEXT_log") ::
(mcs_SWAP_TAIL, "mcs_SWAP_TAIL") ::
(mcs_cas_tail, "mcs_cas_tail") ::
(mcs_get_busy, "mcs_get_busy") ::
(mcs_get_next, "mcs_get_next") ::
(mcs_init_node, "mcs_init_node") ::
(mcs_init_node_log, "mcs_init_node_log") ::
(mcs_lock_get_index, "mcs_lock_get_index") ::
(mcs_lock_init, "mcs_lock_init") ::
(mcs_log, "mcs_log") ::
(mcs_pass_lock, "mcs_pass_lock") ::
(mcs_set_busy, "mcs_set_busy") ::
(mcs_set_next, "mcs_set_next") ::
(mcs_swap_tail, "mcs_swap_tail") ::
(mcs_wait_lock, "mcs_wait_lock") ::
(mem_init, "mem_init") ::
(msr_bitmap_LOC, "msr_bitmap_LOC") ::
(npt_init, "npt_init") ::
(npt_insert, "npt_insert") ::
(offer_shared_mem, "offer_shared_mem") ::
(page_copy, "page_copy") ::
(page_copy_back, "page_copy_back") ::
(palloc, "palloc") ::
(palloc_aux, "palloc_aux") ::
(pass_lock, "pass_lock") ::
(pass_queue, "pass_queue") ::
(pcpumsg_recv, "pcpumsg_recv") ::
(pcpumsg_send, "pcpumsg_send") ::
(pcpumsg_try_recv, "pcpumsg_try_recv") ::
(pfree, "pfree") ::
(pgf_handler, "pgf_handler") ::
(pmap_init, "pmap_init") ::
(pre_acquire_lock, "pre_acquire_lock") ::
(proc_create, "proc_create") ::
(proc_create_postinit, "proc_create_postinit") ::
(proc_exit_user, "proc_exit_user") ::
(proc_exit_user2, "proc_exit_user2") ::
(proc_init, "proc_init") ::
(proc_start_user, "proc_start_user") ::
(proc_start_user2, "proc_start_user2") ::
(pt_alloc_pde, "pt_alloc_pde") ::
(pt_free, "pt_free") ::
(pt_free_pde, "pt_free_pde") ::
(pt_in, "pt_in") ::
(pt_init, "pt_init") ::
(pt_init_comm, "pt_init_comm") ::
(pt_init_kern, "pt_init_kern") ::
(pt_insert, "pt_insert") ::
(pt_insert_aux, "pt_insert_aux") ::
(pt_insert_pde, "pt_insert_pde") ::
(pt_new, "pt_new") ::
(pt_out, "pt_out") ::
(pt_read, "pt_read") ::
(pt_read_pde, "pt_read_pde") ::
(pt_resv, "pt_resv") ::
(pt_resv2, "pt_resv2") ::
(pt_rmv, "pt_rmv") ::
(pt_rmv_aux, "pt_rmv_aux") ::
(pt_rmv_pde, "pt_rmv_pde") ::
(ptfault_resv, "ptfault_resv") ::
(queue_rmv, "queue_rmv") ::
(queue_rmv_atomic, "queue_rmv_atomic") ::
(queue_rmv_local, "queue_rmv_local") ::
(queue_rmv_try, "queue_rmv_try") ::
(rcr0, "rcr0") ::
(rcr3, "rcr3") ::
(rcr4, "rcr4") ::
(rdmsr, "rdmsr") ::
(read_now, "read_now") ::
(receive_chan, "receive_chan") ::
(release_lock, "release_lock") ::
(release_lock_AT, "release_lock_AT") ::
(release_lock_CHAN, "release_lock_CHAN") ::
(release_lock_PB, "release_lock_PB") ::
(release_lock_TCB, "release_lock_TCB") ::
(release_lock_TDQ, "release_lock_TDQ") ::
(release_shared, "release_shared") ::
(restore_context, "restore_context") ::
(restore_hctx, "restore_hctx") ::
(restore_uctx, "restore_uctx") ::
(rmv_PDE, "rmv_PDE") ::
(rmv_PTE, "rmv_PTE") ::
(save_context, "save_context") ::
(save_hctx, "save_hctx") ::
(save_uctx, "save_uctx") ::
(sched_init, "sched_init") ::
(sendto_chan, "sendto_chan") ::
(serial_exists_LOC, "serial_exists_LOC") ::
(serial_getc, "serial_getc") ::
(serial_hw_intr, "serial_hw_intr") ::
(serial_in, "serial_in") ::
(serial_init, "serial_init") ::
(serial_intr_disable, "serial_intr_disable") ::
(serial_intr_disable_handler, "serial_intr_disable_handler") ::
(serial_intr_enable, "serial_intr_enable") ::
(serial_intr_enable_handler, "serial_intr_enable_handler") ::
(serial_intr_handler_asm, "serial_intr_handler_asm") ::
(serial_intr_handler_ext, "serial_intr_handler_ext") ::
(serial_intr_handler_sw, "serial_intr_handler_sw") ::
(serial_irq_check, "serial_irq_check") ::
(serial_irq_current, "serial_irq_current") ::
(serial_out, "serial_out") ::
(serial_putc, "serial_putc") ::
(set_EPDPTE, "set_EPDPTE") ::
(set_EPDTE, "set_EPDTE") ::
(set_EPML4E, "set_EPML4E") ::
(set_EPTE, "set_EPTE") ::
(set_IDPTE, "set_IDPTE") ::
(set_NPDE, "set_NPDE") ::
(set_NPTE, "set_NPTE") ::
(set_PDE, "set_PDE") ::
(set_PDEU, "set_PDEU") ::
(set_PTE, "set_PTE") ::
(set_RA, "set_RA") ::
(set_SP, "set_SP") ::
(set_bit, "set_bit") ::
(set_chan_content, "set_chan_content") ::
(set_chan_info, "set_chan_info") ::
(set_cr3, "set_cr3") ::
(set_curid, "set_curid") ::
(set_curid_init, "set_curid_init") ::
(set_head, "set_head") ::
(set_lock_status, "set_lock_status") ::
(set_next, "set_next") ::
(set_norm, "set_norm") ::
(set_nps, "set_nps") ::
(set_pg, "set_pg") ::
(set_prev, "set_prev") ::
(set_pt, "set_pt") ::
(set_qowner, "set_qowner") ::
(set_qsize, "set_qsize") ::
(set_serial_exists, "set_serial_exists") ::
(set_shared_mem_loc, "set_shared_mem_loc") ::
(set_shared_mem_seen, "set_shared_mem_seen") ::
(set_shared_mem_state, "set_shared_mem_state") ::
(set_state, "set_state") ::
(set_sync_chan_busy, "set_sync_chan_busy") ::
(set_sync_chan_count, "set_sync_chan_count") ::
(set_sync_chan_paddr, "set_sync_chan_paddr") ::
(set_sync_chan_to, "set_sync_chan_to") ::
(set_tail, "set_tail") ::
(set_tf, "set_tf") ::
(shared_mem_init, "shared_mem_init") ::
(shared_mem_status, "shared_mem_status") ::
(shared_mem_to_dead, "shared_mem_to_dead") ::
(shared_mem_to_pending, "shared_mem_to_pending") ::
(shared_mem_to_ready, "shared_mem_to_ready") ::
(sleeper_dec, "sleeper_dec") ::
(sleeper_get, "sleeper_get") ::
(sleeper_inc, "sleeper_inc") ::
(sleeper_set, "sleeper_set") ::
(sleeper_zzz, "sleeper_zzz") ::
(srecv_chan, "srecv_chan") ::
(ssend_to_chan, "ssend_to_chan") ::
(sti, "sti") ::
(svm_exit_vm, "svm_exit_vm") ::
(svm_get_exit_fault_addr, "svm_get_exit_fault_addr") ::
(svm_get_exit_io_neip, "svm_get_exit_io_neip") ::
(svm_get_exit_io_port, "svm_get_exit_io_port") ::
(svm_get_exit_io_rep, "svm_get_exit_io_rep") ::
(svm_get_exit_io_str, "svm_get_exit_io_str") ::
(svm_get_exit_io_width, "svm_get_exit_io_width") ::
(svm_get_exit_io_write, "svm_get_exit_io_write") ::
(svm_get_exit_reason, "svm_get_exit_reason") ::
(svm_get_reg, "svm_get_reg") ::
(svm_run_vm, "svm_run_vm") ::
(svm_set_intercept_intwin, "svm_set_intercept_intwin") ::
(svm_set_reg, "svm_set_reg") ::
(svm_state_save, "svm_state_save") ::
(svm_sync, "svm_sync") ::
(syncreceive_chan, "syncreceive_chan") ::
(syncsendto_chan, "syncsendto_chan") ::
(syncsendto_chan_post, "syncsendto_chan_post") ::
(syncsendto_chan_pre, "syncsendto_chan_pre") ::
(sys_certikos_init, "sys_certikos_init") ::
(sys_check_int_shadow, "sys_check_int_shadow") ::
(sys_check_pending_event, "sys_check_pending_event") ::
(sys_disk_cap, "sys_disk_cap") ::
(sys_disk_op, "sys_disk_op") ::
(sys_ept_insert, "sys_ept_insert") ::
(sys_get_curid, "sys_get_curid") ::
(sys_get_exit_fault_addr, "sys_get_exit_fault_addr") ::
(sys_get_exit_io_neip, "sys_get_exit_io_neip") ::
(sys_get_exit_io_port, "sys_get_exit_io_port") ::
(sys_get_exit_io_rep, "sys_get_exit_io_rep") ::
(sys_get_exit_io_str, "sys_get_exit_io_str") ::
(sys_get_exit_io_width, "sys_get_exit_io_width") ::
(sys_get_exit_io_write, "sys_get_exit_io_write") ::
(sys_get_exit_reason, "sys_get_exit_reason") ::
(sys_get_exitinfo, "sys_get_exitinfo") ::
(sys_get_next_eip, "sys_get_next_eip") ::
(sys_get_quota, "sys_get_quota") ::
(sys_get_reg, "sys_get_reg") ::
(sys_get_tsc_offset, "sys_get_tsc_offset") ::
(sys_get_tsc_per_ms, "sys_get_tsc_per_ms") ::
(sys_getc, "sys_getc") ::
(sys_handle_rdmsr, "sys_handle_rdmsr") ::
(sys_handle_wrmsr, "sys_handle_wrmsr") ::
(sys_inject_event, "sys_inject_event") ::
(sys_intercept_int_window, "sys_intercept_int_window") ::
(sys_is_chan_ready, "sys_is_chan_ready") ::
(sys_mmap, "sys_mmap") ::
(sys_npt_insert, "sys_npt_insert") ::
(sys_palloc, "sys_palloc") ::
(sys_pfree, "sys_pfree") ::
(sys_proc_create, "sys_proc_create") ::
(sys_pt_read, "sys_pt_read") ::
(sys_putc, "sys_putc") ::
(sys_puts, "sys_puts") ::
(sys_ready, "sys_ready") ::
(sys_receive_chan, "sys_receive_chan") ::
(sys_recv, "sys_recv") ::
(sys_ring0_spawn, "sys_ring0_spawn") ::
(sys_run_vm, "sys_run_vm") ::
(sys_send, "sys_send") ::
(sys_sendto_chan, "sys_sendto_chan") ::
(sys_sendtochan_post, "sys_sendtochan_post") ::
(sys_sendtochan_pre, "sys_sendtochan_pre") ::
(sys_set_intercept_intwin, "sys_set_intercept_intwin") ::
(sys_set_reg, "sys_set_reg") ::
(sys_set_seg, "sys_set_seg") ::
(sys_set_seg1, "sys_set_seg1") ::
(sys_set_seg2, "sys_set_seg2") ::
(sys_set_tsc_offset, "sys_set_tsc_offset") ::
(sys_sleep, "sys_sleep") ::
(sys_spawn, "sys_spawn") ::
(sys_srecv_chan, "sys_srecv_chan") ::
(sys_ssend_to_chan, "sys_ssend_to_chan") ::
(sys_svm_exit_vm, "sys_svm_exit_vm") ::
(sys_sync, "sys_sync") ::
(sys_thread_kill, "sys_thread_kill") ::
(sys_thread_sleep, "sys_thread_sleep") ::
(sys_thread_wakeup, "sys_thread_wakeup") ::
(sys_thread_yield, "sys_thread_yield") ::
(sys_tryreceive_chan, "sys_tryreceive_chan") ::
(sys_tryrecv, "sys_tryrecv") ::
(sys_trysend, "sys_trysend") ::
(sys_trysendto_chan, "sys_trysendto_chan") ::
(sys_uctx_get, "sys_uctx_get") ::
(sys_uctx_set, "sys_uctx_set") ::
(sys_yield, "sys_yield") ::
(syscall_dispatch, "syscall_dispatch") ::
(syscall_dispatch_C, "syscall_dispatch_C") ::
(tcb_get_CPU_ID, "tcb_get_CPU_ID") ::
(tcb_init, "tcb_init") ::
(tcb_set_CPU_ID, "tcb_set_CPU_ID") ::
(tdq_init, "tdq_init") ::
(tdqueue_init, "tdqueue_init") ::
(test_lock, "test_lock") ::
(thread_free, "thread_free") ::
(thread_init, "thread_init") ::
(thread_kill, "thread_kill") ::
(thread_poll_pending, "thread_poll_pending") ::
(thread_sched, "thread_sched") ::
(thread_sleep, "thread_sleep") ::
(thread_sleep2, "thread_sleep2") ::
(thread_sleep_lock, "thread_sleep_lock") ::
(thread_spawn, "thread_spawn") ::
(thread_wakeup, "thread_wakeup") ::
(thread_wakeup2, "thread_wakeup2") ::
(thread_wakeup_lock, "thread_wakeup_lock") ::
(thread_yield, "thread_yield") ::
(ticket_lock_init, "ticket_lock_init") ::
(trap_get, "trap_get") ::
(trap_in, "trap_in") ::
(trap_out, "trap_out") ::
(trap_sendtochan_post, "trap_sendtochan_post") ::
(trap_sendtochan_pre, "trap_sendtochan_pre") ::
(trap_set, "trap_set") ::
(try_lock, "try_lock") ::
(try_lock_AT, "try_lock_AT") ::
(try_lock_CHAN, "try_lock_CHAN") ::
(try_lock_PB, "try_lock_PB") ::
(try_lock_TCB, "try_lock_TCB") ::
(try_lock_TDQ, "try_lock_TDQ") ::
(tryreceive_chan, "tryreceive_chan") ::
(trysendto_chan, "trysendto_chan") ::
(tss_LOC, "tss_LOC") ::
(uctx_arg1, "uctx_arg1") ::
(uctx_arg2, "uctx_arg2") ::
(uctx_arg3, "uctx_arg3") ::
(uctx_arg4, "uctx_arg4") ::
(uctx_arg5, "uctx_arg5") ::
(uctx_arg6, "uctx_arg6") ::
(uctx_get, "uctx_get") ::
(uctx_set, "uctx_set") ::
(uctx_set_eip, "uctx_set_eip") ::
(uctx_set_errno, "uctx_set_errno") ::
(uctx_set_retval1, "uctx_set_retval1") ::
(uctx_set_retval2, "uctx_set_retval2") ::
(uctx_set_retval3, "uctx_set_retval3") ::
(uctx_set_retval4, "uctx_set_retval4") ::
(vmcb_check_int_shadow, "vmcb_check_int_shadow") ::
(vmcb_check_pending_event, "vmcb_check_pending_event") ::
(vmcb_clear_virq, "vmcb_clear_virq") ::
(vmcb_get_exit_info, "vmcb_get_exit_info") ::
(vmcb_get_next_eip, "vmcb_get_next_eip") ::
(vmcb_get_reg, "vmcb_get_reg") ::
(vmcb_inject_event, "vmcb_inject_event") ::
(vmcb_inject_virq, "vmcb_inject_virq") ::
(vmcb_read_v, "vmcb_read_v") ::
(vmcb_read_z, "vmcb_read_z") ::
(vmcb_restore, "vmcb_restore") ::
(vmcb_set_intercept_vint, "vmcb_set_intercept_vint") ::
(vmcb_set_reg, "vmcb_set_reg") ::
(vmcb_set_seg, "vmcb_set_seg") ::
(vmcb_write_v, "vmcb_write_v") ::
(vmcb_write_z, "vmcb_write_z") ::
(vmcs_get_abrtid, "vmcs_get_abrtid") ::
(vmcs_get_revid, "vmcs_get_revid") ::
(vmcs_read, "vmcs_read") ::
(vmcs_readz, "vmcs_readz") ::
(vmcs_readz64, "vmcs_readz64") ::
(vmcs_set_abrtid, "vmcs_set_abrtid") ::
(vmcs_set_defaults, "vmcs_set_defaults") ::
(vmcs_set_revid, "vmcs_set_revid") ::
(vmcs_write, "vmcs_write") ::
(vmcs_write_ident, "vmcs_write_ident") ::
(vmcs_writez, "vmcs_writez") ::
(vmcs_writez64, "vmcs_writez64") ::
(vmptrld, "vmptrld") ::
(vmx_check_int_shadow, "vmx_check_int_shadow") ::
(vmx_check_pending_event, "vmx_check_pending_event") ::
(vmx_enable, "vmx_enable") ::
(vmx_enter, "vmx_enter") ::
(vmx_enter_bottom_half, "vmx_enter_bottom_half") ::
(vmx_enter_pre, "vmx_enter_pre") ::
(vmx_exit, "vmx_exit") ::
(vmx_exit_bottom_half, "vmx_exit_bottom_half") ::
(vmx_exit_post, "vmx_exit_post") ::
(vmx_get_exit_fault_addr, "vmx_get_exit_fault_addr") ::
(vmx_get_exit_io_port, "vmx_get_exit_io_port") ::
(vmx_get_exit_io_rep, "vmx_get_exit_io_rep") ::
(vmx_get_exit_io_str, "vmx_get_exit_io_str") ::
(vmx_get_exit_qualification, "vmx_get_exit_qualification") ::
(vmx_get_exit_reason, "vmx_get_exit_reason") ::
(vmx_get_io_width, "vmx_get_io_width") ::
(vmx_get_io_write, "vmx_get_io_write") ::
(vmx_get_next_eip, "vmx_get_next_eip") ::
(vmx_get_reg, "vmx_get_reg") ::
(vmx_get_tsc_offset, "vmx_get_tsc_offset") ::
(vmx_init, "vmx_init") ::
(vmx_inject_event, "vmx_inject_event") ::
(vmx_read, "vmx_read") ::
(vmx_readz, "vmx_readz") ::
(vmx_readz64, "vmx_readz64") ::
(vmx_return_from_guest, "vmx_return_from_guest") ::
(vmx_run_return_from_guest, "vmx_run_return_from_guest") ::
(vmx_run_vm, "vmx_run_vm") ::
(vmx_set_ctlreg, "vmx_set_ctlreg") ::
(vmx_set_desc, "vmx_set_desc") ::
(vmx_set_desc1, "vmx_set_desc1") ::
(vmx_set_desc2, "vmx_set_desc2") ::
(vmx_set_intercept_intwin, "vmx_set_intercept_intwin") ::
(vmx_set_mmap, "vmx_set_mmap") ::
(vmx_set_reg, "vmx_set_reg") ::
(vmx_set_tsc_offset, "vmx_set_tsc_offset") ::
(vmx_write, "vmx_write") ::
(vmx_writez, "vmx_writez") ::
(vmx_writez64, "vmx_writez64") ::
(vmxinfo_get, "vmxinfo_get") ::
(vmxon, "vmxon") ::
(wait_lock, "wait_lock") ::
(wait_queue, "wait_queue") ::
(wrmsr, "wrmsr") ::
(xvmst_read, "xvmst_read") ::
(xvmst_restore, "xvmst_restore") ::
(xvmst_write, "xvmst_write") ::
reserved_symbols.