Library mcertikos.layerlib.GlobIdent

Require Import Coqlib.

Open Local Scope positive.

Let ELF_LOC := 1000.
Let ELF_ENTRY_LOC := 1010.
Let STACK_LOC := 1020.
Let thread_yield := 1030.
Let thread_sleep := 1040.
Let proc_start_user := 1050.
Let START_USER_FUN_LOC := 1060.
Let proc_exit_user := 1070.
Let svm_run_vm := 1080.
Let svm_exit_vm := 1090.
Let trap_get := 1100.
Let trap_set := 1110.
Let la2pa_resv := 1120.
Let uctx_arg1 := 1130.
Let uctx_arg2 := 1140.
Let uctx_arg3 := 1150.
Let uctx_arg4 := 1160.
Let uctx_arg5 := 1170.
Let uctx_arg6 := 1180.
Let uctx_set_errno := 1190.
Let uctx_set_retval1 := 1200.
Let uctx_set_retval2 := 1210.
Let uctx_set_retval3 := 1220.
Let uctx_set_retval4 := 1230.
Let npt_insert := 1240.
Let svm_set_intercept_intwin := 1250.
Let vmcb_set_seg := 1260.
Let vmcb_check_int_shadow := 1270.
Let vmcb_check_pending_event := 1280.
Let svm_get_exit_reason := 1290.
Let svm_get_exit_io_port := 1300.
Let svm_get_exit_io_width := 1310.
Let svm_get_exit_io_rep := 1320.
Let svm_get_exit_io_str := 1330.
Let svm_get_exit_io_write := 1340.
Let svm_get_exit_io_neip := 1350.
Let svm_get_exit_fault_addr := 1360.
Let vmcb_get_next_eip := 1370.
Let svm_sync := 1380.
Let is_chan_ready := 1390.
Let sendto_chan := 1400.
Let receive_chan := 1410.
Let proc_create := 1420.
Let svm_set_reg := 1430.
Let svm_get_reg := 1440.
Let restore_hctx := 1450.
Let svm_state_save := 1460.
Let host_in := 1470.
Let pt_resv := 1480.
Let pt_resv2 := 1490.
Let uctx_get := 1500.
Let vmcb_set_intercept_vint := 1510.
Let vmcb_get_exit_info := 1520.
Let vmcb_inject_virq := 1530.
Let vmcb_clear_virq := 1540.
Let vmcb_inject_event := 1550.
Let xvmst_read := 1560.
Let xvmst_write := 1570.
Let vmcb_set_reg := 1580.
Let vmcb_get_reg := 1590.
Let vmcb_restore := 1600.
Let xvmst_restore := 1610.
Let save_hctx := 1620.
Let vmcb_read_z := 1630.
Let vmcb_read_v := 1640.
Let vmcb_write_v := 1650.
Let XVMST_LOC := 1660.
Let vmcb_write_z := 1670.
Let npt_init := 1680.
Let host_out := 1690.
Let VMCB_Z_LOC := 1700.
Let HCtxt_LOC := 1710.
Let proc_init := 1720.
Let NPT_LOC := 1730.
Let restore_uctx := 1740.
Let save_uctx := 1750.
Let pt_out := 1760.
Let pt_in := 1770.
Let trap_in := 1780.
Let uctx_set := 1790.
Let uctx_set_eip := 1800.
Let elf_load := 1810.
Let thread_spawn := 1820.
Let thread_kill := 1830.
Let trap_out := 1840.
Let UCTX_LOC := 1850.
Let get_chan_info := 1860.
Let set_chan_info := 1870.
Let get_chan_content := 1880.
Let set_chan_content := 1890.
Let get_curid := 1900.
Let thread_wakeup := 1910.
Let init_chan := 1920.
Let sched_init := 1930.
Let CHPOOL_LOC := 1940.
Let offer_shared_mem := 1950.
Let shared_mem_status := 1960.
Let shared_mem_init := 1970.
Let get_shared_mem_status_seen := 1980.
Let shared_mem_to_ready := 1990.
Let shared_mem_to_pending := 2000.
Let shared_mem_to_dead := 2010.
Let clear_shared_mem := 2020.
Let set_shared_mem_seen := 2030.
Let set_shared_mem_loc := 2040.
Let set_shared_mem_state := 2050.
Let get_shared_mem_seen := 2060.
Let get_shared_mem_loc := 2070.
Let get_shared_mem_state := 2080.
Let SHRDMEMPOOL_LOC := 2090.
Let thread_sched := 2100.
Let kctxt_switch := 2110.
Let set_curid := 2120.
Let set_state := 2130.
Let enqueue := 2140.
Let dequeue := 2150.
Let queue_rmv := 2160.
Let kctxt_new := 2170.
Let tdqueue_init := 2180.
Let thread_free := 2190.
Let CURID_LOC := 2200.
Let get_prev := 2210.
Let get_state := 2220.
Let set_prev := 2230.
Let get_next := 2240.
Let set_next := 2250.
Let get_head := 2260.
Let set_head := 2270.
Let get_tail := 2280.
Let set_tail := 2290.
Let tdq_init := 2300.
Let thread_init := 2310.
Let TDQPool_LOC := 2320.
Let tcb_init := 2330.
Let pmap_init := 2340.
Let pt_free := 2350.
Let TCBPool_LOC := 2360.
Let set_RA := 2370.
Let set_SP := 2380.
Let pt_new := 2390.
Let KCtxtPool_LOC := 2400.
Let pfree := 2410.
Let palloc := 2420.
Let set_bit := 2430.
Let is_used := 2440.
Let pt_init := 2450.
Let PTP_LOC := 2460.
Let pt_init_kern := 2470.
Let set_cr3 := 2480.
Let set_pg := 2490.
Let pt_init_comm := 2500.
Let pt_insert := 2510.
Let pt_rmv := 2520.
Let pt_alloc_pde := 2530.
Let pt_free_pde := 2540.
Let idpde_init := 2550.
Let pt_read := 2560.
Let pt_read_pde := 2570.
Let pt_rmv_aux := 2580.
Let pt_rmv_pde := 2590.
Let pt_insert_aux := 2600.
Let pt_insert_pde := 2610.
Let set_IDPTE := 2620.
Let rmv_PDE := 2630.
Let set_PDE := 2640.
Let set_PDEU := 2650.
Let get_PDE := 2660.
Let clear_PDE := 2670.
Let mem_init := 2680.
Let get_PTE := 2690.
Let set_PTE := 2700.
Let rmv_PTE := 2710.
Let set_pt := 2720.
Let PTPool_LOC := 2730.
Let IDPMap_LOC := 2740.
Let at_get_c := 2750.
Let at_set_c := 2760.
Let at_get := 2770.
Let at_set := 2780.
Let is_norm := 2790.
Let get_nps := 2800.
Let get_size := 2810.
Let get_mms := 2820.
Let get_mml := 2830.
Let is_usable := 2840.
Let set_norm := 2850.
Let set_nps := 2860.
Let boot_loader := 2870.
Let NPS_LOC := 2880.
Let AT_LOC := 2890.
Let fload := 2900.
Let fstore := 2910.
Let FlatMem_LOC := 2920.
Let serial_in := 2930.
Let serial_out := 2940.
Let serial_hw_intr := 2950.
Let serial_irq_check := 2960.
Let serial_irq_current := 2970.
Let keyboard_in := 2980.
Let keyboard_hw_intr := 2990.
Let keyboard_irq_check := 3000.
Let ioapic_read := 3010.
Let ioapic_write := 3020.
Let lapic_read := 3030.
Let lapic_write := 3040.
Let hw_intr := 3050.
Let ic_intr := 3060.
Let cons_buf_LOC := 3070.
Let cons_buf_init_concrete := 3080.
Let cons_buf_write_concrete := 3090.
Let cons_buf_init := 3100.
Let cons_buf_write := 3110.
Let cons_buf_read := 3120.
Let cons_buf_wpos := 3130.
Let cons_intr := 3140.
Let cons_init := 3150.
Let serial_init := 3160.
Let serial_putc := 3170.
Let serial_getc := 3180.
Let get_serial_exists := 3190.
Let set_serial_exists := 3200.
Let kbd_buf_LOC := 3210.
Let kbd_states_LOC := 3220.
Let kbd_buf_init_concrete := 3230.
Let kbd_buf_write_concrete := 3240.
Let kbd_buf_init := 3250.
Let kbd_buf_write := 3260.
Let kbd_buf_read := 3270.
Let keyboard_init := 3280.
Let keyboard_scan := 3290.
Let keyboard_scan_code_normal_LOC := 3300.
Let keyboard_scan_code_shift_LOC := 3310.
Let keyboard_shift_toggle := 3320.
Let keyboard_shift_reset := 3330.
Let keyboard_shift_check := 3340.
Let keyboard_switch_key_map := 3350.
Let keyboard_map := 3360.
Let keyboard_proc_data := 3370.
Let keyboard_getc := 3380.
Let keyboard_intr := 3390.
Let kbd_intr_disable := 3400.
Let serial_exists_LOC := 3410.
Let ioapic_init := 3420.
Let ioapic_enable := 3430.
Let ioapic_mask := 3440.
Let ioapic_unmask := 3450.
Let lapic_init := 3460.
Let lapic_eoi := 3470.
Let interrupt_handler := 3480.
Let cli := 3490.
Let sti := 3500.
Let local_irq_save := 3510.
Let local_irq_restore := 3520.
Let save_context := 3530.
Let restore_context := 3540.
Let set_tf := 3550.
Let serial_intr_enable := 3560.
Let serial_intr_disable := 3570.
Let serial_intr_enable_handler := 3580.
Let serial_intr_disable_handler := 3590.
Let serial_intr_handler_asm := 3600.
Let serial_intr_handler_sw := 3610.
Let serial_intr_handler_ext := 3620.
Let kbd_intr_enable := 3630.
Let kbd_intr_disable_handler := 3640.
Let iret := 3650.
Let curr_intr_num_LOC := 3660.
Let get_curr_intr_num := 3670.
Let intr_default_handler := 3680.
Let vmx_return_from_guest := 3690.
Let rcr0 := 3700.
Let rcr3 := 3710.
Let rcr4 := 3720.
Let lcr4 := 3730.
Let rdmsr := 3740.
Let wrmsr := 3750.
Let vmptrld := 3760.
Let VMCS_LOC := 3770.
Let VMX_LOC := 3780.
Let msr_bitmap_LOC := 3790.
Let io_bitmap_LOC := 3800.
Let tss_LOC := 3810.
Let gdt_LOC := 3820.
Let idt_LOC := 3830.
Let vmx_read := 3840.
Let vmx_write := 3850.
Let vmx_readz := 3860.
Let vmx_writez := 3870.
Let vmx_readz64 := 3880.
Let vmx_writez64 := 3890.
Let set_NPDE := 3900.
Let set_NPTE := 3910.
Let vmcs_get_abrtid := 3920.
Let vmcs_set_abrtid := 3930.
Let vmcs_get_revid := 3940.
Let vmcs_set_revid := 3950.
Let vmcs_readz := 3960.
Let vmcs_writez := 3970.
Let vmcs_readz64 := 3980.
Let vmcs_writez64 := 3990.
Let vmcs_read := 4000.
Let vmcs_write := 4010.
Let vmcs_write_ident := 4020.
Let vmx_get_exit_io_port := 4030.
Let vmx_set_intercept_intwin := 4040.
Let vmx_set_desc := 4050.
Let vmx_inject_event := 4060.
Let vmx_check_pending_event := 4070.
Let vmx_check_int_shadow := 4080.
Let vmx_get_exit_reason := 4090.
Let vmx_set_tsc_offset := 4100.
Let vmx_get_tsc_offset := 4110.
Let vmx_get_exit_fault_addr := 4120.
Let vmcs_set_defaults := 4130.
Let vmx_get_reg := 4140.
Let vmx_set_reg := 4150.
Let vmx_get_next_eip := 4160.
Let vmx_get_io_width := 4170.
Let vmx_get_io_write := 4180.
Let vmx_get_exit_io_rep := 4190.
Let vmx_get_exit_io_str := 4200.
Let vmx_set_mmap := 4210.
Let vmx_set_ctlreg := 4220.
Let vmx_run_vm := 4230.
Let vmx_run_return_from_guest := 4240.
Let vmx_init := 4250.
Let vmx_enter_pre := 4260.
Let vmx_exit_post := 4270.
Let EPT_LOC := 4280.
Let set_EPML4E := 4290.
Let get_EPTE := 4300.
Let set_EPTE := 4310.
Let set_EPDTE := 4320.
Let set_EPDPTE := 4330.
Let ept_invalidate_mappings := 4340.
Let ept_insert := 4350.
Let ept_init := 4360.
Let ept_add_mapping := 4370.
Let ept_get_page_entry := 4380.
Let ept_set_page_entry := 4390.
Let ept_gpa_to_hpa := 4400.
Let ept_set_permission := 4410.
Let ept_mmap := 4420.
Let vmxinfo_get := 4430.
Let vmx_exit := 4440.
Let vmx_enter := 4450.
Let sys_palloc := 4460.
Let sys_pfree := 4470.
Let sys_pt_read := 4480.
Let sys_thread_kill := 4490.
Let sys_thread_wakeup := 4500.
Let sys_get_curid := 4510.
Let sys_get_quota := 4520.
Let sys_uctx_get := 4530.
Let sys_uctx_set := 4540.
Let sys_thread_yield := 4550.
Let sys_thread_sleep := 4560.
Let sys_svm_exit_vm := 4570.
Let sys_proc_create := 4580.
Let sys_npt_insert := 4590.
Let sys_ept_insert := 4600.
Let sys_set_intercept_intwin := 4610.
Let sys_set_seg := 4620.
Let sys_check_int_shadow := 4630.
Let sys_check_pending_event := 4640.
Let sys_get_exit_reason := 4650.
Let sys_get_exit_io_port := 4660.
Let sys_get_exit_io_width := 4670.
Let sys_get_exit_io_rep := 4680.
Let sys_get_exit_io_str := 4690.
Let sys_get_exit_io_write := 4700.
Let sys_get_exit_io_neip := 4710.
Let sys_get_exit_fault_addr := 4720.
Let sys_inject_event := 4730.
Let sys_get_next_eip := 4740.
Let sys_sync := 4750.
Let sys_set_reg := 4760.
Let sys_get_reg := 4770.
Let sys_run_vm := 4780.
Let sys_is_chan_ready := 4790.
Let sys_sendto_chan := 4800.
Let sys_receive_chan := 4810.
Let sys_yield := 4820.
Let sys_send := 4830.
Let sys_recv := 4840.
Let sys_spawn := 4850.
Let sys_sleep := 4860.
Let sys_ready := 4870.
Let pgf_handler := 4880.
Let sys_certikos_init := 4890.
Let ptfault_resv := 4900.
Let syscall_dispatch_C := 4910.
Let syscall_dispatch := 4920.
Let sys_puts := 4930.
Let sys_ring0_spawn := 4940.
Let sys_disk_op := 4950.
Let sys_disk_cap := 4960.
Let sys_get_tsc_per_ms := 4970.
Let sys_get_tsc_offset := 4980.
Let sys_set_tsc_offset := 4990.
Let sys_get_exitinfo := 5000.
Let sys_mmap := 5010.
Let sys_intercept_int_window := 5020.
Let sys_handle_rdmsr := 5030.
Let sys_handle_wrmsr := 5040.
Let sys_getc := 5050.
Let sys_putc := 5060.
Let sys_getkey := 5070.
Let AC_LOC := 5080.
Let container_init := 5090.
Let container_get_parent := 5100.
Let container_get_quota := 5110.
Let container_get_usage := 5120.
Let container_can_consume := 5130.
Let container_split := 5140.
Let container_revoke := 5150.
Let container_alloc := 5160.
Let container_free := 5170.
Let flatmem_copy := 5180.
Let init_sync_chan := 5190.
Let set_sync_chan_to := 5200.
Let get_sync_chan_to := 5210.
Let set_sync_chan_paddr := 5220.
Let get_sync_chan_paddr := 5230.
Let set_sync_chan_count := 5240.
Let get_sync_chan_count := 5250.
Let is_pid_sending_to := 5260.
Let syncsendto_chan_pre := 5270.
Let syncsendto_chan_post := 5280.
Let syncreceive_chan := 5290.
Let get_kernel_pa := 5300.
Let SYNCCHPOOL_LOC := 5310.
Let sys_ssend_to_chan := 5320.
Let sys_srecv_chan := 5330.
Let ssend_to_chan := 5340.
Let srecv_chan := 5350.
Let thread_sleep2 := 5360.
Let thread_wakeup2 := 5370.
Let trap_sendtochan_pre := 5380.
Let trap_sendtochan_post := 5390.
Let sys_sendtochan_post := 5400.
Let sys_sendtochan_pre := 5410.
Let vmx_enter_bottom_half := 5420.
Let vmx_exit_bottom_half := 5430.
Let vmxon := 5440.
Let vmx_enable := 5450.