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 proc_exit_user := 1060.
Let svm_run_vm := 1070.
Let svm_exit_vm := 1080.
Let trap_get := 1090.
Let trap_set := 1100.
Let la2pa_resv := 1110.
Let uctx_arg1 := 1120.
Let uctx_arg2 := 1130.
Let uctx_arg3 := 1140.
Let uctx_arg4 := 1150.
Let uctx_arg5 := 1160.
Let uctx_arg6 := 1170.
Let uctx_set_errno := 1180.
Let uctx_set_retval1 := 1190.
Let uctx_set_retval2 := 1200.
Let uctx_set_retval3 := 1210.
Let uctx_set_retval4 := 1220.
Let npt_insert := 1230.
Let svm_set_intercept_intwin := 1240.
Let vmcb_set_seg := 1250.
Let vmcb_check_int_shadow := 1260.
Let vmcb_check_pending_event := 1270.
Let svm_get_exit_reason := 1280.
Let svm_get_exit_io_port := 1290.
Let svm_get_exit_io_width := 1300.
Let svm_get_exit_io_rep := 1310.
Let svm_get_exit_io_str := 1320.
Let svm_get_exit_io_write := 1330.
Let svm_get_exit_io_neip := 1340.
Let svm_get_exit_fault_addr := 1350.
Let vmcb_get_next_eip := 1360.
Let svm_sync := 1370.
Let is_chan_ready := 1380.
Let sendto_chan := 1390.
Let receive_chan := 1400.
Let proc_create := 1410.
Let svm_set_reg := 1420.
Let svm_get_reg := 1430.
Let restore_hctx := 1440.
Let svm_state_save := 1450.
Let host_in := 1460.
Let pt_resv := 1470.
Let pt_resv2 := 1480.
Let uctx_get := 1490.
Let vmcb_set_intercept_vint := 1500.
Let vmcb_get_exit_info := 1510.
Let vmcb_inject_virq := 1520.
Let vmcb_clear_virq := 1530.
Let vmcb_inject_event := 1540.
Let xvmst_read := 1550.
Let xvmst_write := 1560.
Let vmcb_set_reg := 1570.
Let vmcb_get_reg := 1580.
Let vmcb_restore := 1590.
Let xvmst_restore := 1600.
Let save_hctx := 1610.
Let vmcb_read_z := 1620.
Let vmcb_read_v := 1630.
Let vmcb_write_v := 1640.
Let XVMST_LOC := 1650.
Let vmcb_write_z := 1660.
Let npt_init := 1670.
Let host_out := 1680.
Let VMCB_Z_LOC := 1690.
Let HCtxt_LOC := 1700.
Let proc_init := 1710.
Let NPT_LOC := 1720.
Let restore_uctx := 1730.
Let save_uctx := 1740.
Let pt_out := 1750.
Let pt_in := 1760.
Let trap_in := 1770.
Let uctx_set := 1780.
Let uctx_set_eip := 1790.
Let elf_load := 1800.
Let thread_spawn := 1810.
Let thread_kill := 1820.
Let trap_out := 1830.
Let UCTX_LOC := 1840.
Let get_chan_info := 1850.
Let set_chan_info := 1860.
Let get_chan_content := 1870.
Let set_chan_content := 1880.
Let get_curid := 1890.
Let thread_wakeup := 1900.
Let init_chan := 1910.
Let sched_init := 1920.
Let CHPOOL_LOC := 1930.
Let offer_shared_mem := 1940.
Let shared_mem_status := 1950.
Let shared_mem_init := 1960.
Let get_shared_mem_status_seen := 1970.
Let shared_mem_to_ready := 1980.
Let shared_mem_to_pending := 1990.
Let shared_mem_to_dead := 2000.
Let clear_shared_mem := 2010.
Let set_shared_mem_seen := 2020.
Let set_shared_mem_loc := 2030.
Let set_shared_mem_state := 2040.
Let get_shared_mem_seen := 2050.
Let get_shared_mem_loc := 2060.
Let get_shared_mem_state := 2070.
Let SHRDMEMPOOL_LOC := 2080.
Let thread_sched := 2090.
Let kctxt_switch := 2100.
Let set_curid := 2110.
Let set_state := 2120.
Let enqueue := 2130.
Let dequeue := 2140.
Let queue_rmv := 2150.
Let kctxt_new := 2160.
Let tdqueue_init := 2170.
Let thread_free := 2180.
Let CURID_LOC := 2190.
Let get_prev := 2200.
Let get_state := 2210.
Let set_prev := 2220.
Let get_next := 2230.
Let set_next := 2240.
Let get_head := 2250.
Let set_head := 2260.
Let get_tail := 2270.
Let set_tail := 2280.
Let tdq_init := 2290.
Let thread_init := 2300.
Let TDQPool_LOC := 2310.
Let tcb_init := 2320.
Let pmap_init := 2330.
Let pt_free := 2340.
Let TCBPool_LOC := 2350.
Let set_RA := 2360.
Let set_SP := 2370.
Let pt_new := 2380.
Let KCtxtPool_LOC := 2390.
Let pfree := 2400.
Let palloc := 2410.
Let set_bit := 2420.
Let is_used := 2430.
Let pt_init := 2440.
Let PTP_LOC := 2450.
Let pt_init_kern := 2460.
Let clear_cr2 := 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 vmx_return_from_guest := 2930.
Let rcr0 := 2940.
Let rcr3 := 2950.
Let rcr4 := 2960.
Let rdmsr := 2970.
Let wrmsr := 2980.
Let vmptrld := 2990.
Let VMCS_LOC := 3000.
Let VMX_LOC := 3010.
Let msr_bitmap_LOC := 3020.
Let io_bitmap_LOC := 3030.
Let tss_LOC := 3040.
Let gdt_LOC := 3050.
Let idt_LOC := 3060.
Let vmx_read := 3070.
Let vmx_write := 3080.
Let vmx_readz := 3090.
Let vmx_writez := 3100.
Let vmx_readz64 := 3110.
Let vmx_writez64 := 3120.
Let set_NPDE := 3130.
Let set_NPTE := 3140.
Let vmcs_get_abrtid := 3150.
Let vmcs_set_abrtid := 3160.
Let vmcs_get_revid := 3170.
Let vmcs_set_revid := 3180.
Let vmcs_readz := 3190.
Let vmcs_writez := 3200.
Let vmcs_readz64 := 3210.
Let vmcs_writez64 := 3220.
Let vmcs_read := 3230.
Let vmcs_write := 3240.
Let vmcs_write_ident := 3250.
Let vmx_get_exit_io_port := 3260.
Let vmx_set_intercept_intwin := 3270.
Let vmx_set_desc := 3280.
Let vmx_inject_event := 3290.
Let vmx_check_pending_event := 3300.
Let vmx_check_int_shadow := 3310.
Let vmx_get_exit_reason := 3320.
Let vmx_set_tsc_offset := 3330.
Let vmx_get_tsc_offset := 3340.
Let vmx_get_exit_fault_addr := 3350.
Let vmcs_set_defaults := 3360.
Let vmx_get_reg := 3370.
Let vmx_set_reg := 3380.
Let vmx_get_next_eip := 3390.
Let vmx_get_io_width := 3400.
Let vmx_get_io_write := 3410.
Let vmx_get_exit_io_rep := 3420.
Let vmx_get_exit_io_str := 3430.
Let vmx_set_mmap := 3440.
Let vmx_set_ctlreg := 3450.
Let vmx_run_vm := 3460.
Let vmx_run_return_from_guest := 3470.
Let vmx_init := 3480.
Let vmx_enter_pre := 3490.
Let vmx_exit_post := 3500.
Let EPT_LOC := 3510.
Let set_EPML4E := 3520.
Let get_EPTE := 3530.
Let set_EPTE := 3540.
Let set_EPDTE := 3550.
Let set_EPDPTE := 3560.
Let ept_invalidate_mappings := 3570.
Let ept_insert := 3580.
Let ept_init := 3590.
Let ept_add_mapping := 3600.
Let ept_get_page_entry := 3610.
Let ept_set_page_entry := 3620.
Let ept_gpa_to_hpa := 3630.
Let ept_set_permission := 3640.
Let ept_mmap := 3650.
Let vmxinfo_get := 3660.
Let vmx_exit := 3670.
Let vmx_enter := 3680.
Let sys_palloc := 3690.
Let sys_pfree := 3700.
Let sys_pt_read := 3710.
Let sys_thread_kill := 3720.
Let sys_thread_wakeup := 3730.
Let sys_get_curid := 3740.
Let sys_get_quota := 3750.
Let sys_uctx_get := 3760.
Let sys_uctx_set := 3770.
Let sys_thread_yield := 3780.
Let sys_thread_sleep := 3790.
Let sys_svm_exit_vm := 3800.
Let sys_proc_create := 3810.
Let sys_npt_insert := 3820.
Let sys_ept_insert := 3830.
Let sys_set_intercept_intwin := 3840.
Let sys_set_seg := 3850.
Let sys_check_int_shadow := 3860.
Let sys_check_pending_event := 3870.
Let sys_get_exit_reason := 3880.
Let sys_get_exit_io_port := 3890.
Let sys_get_exit_io_width := 3900.
Let sys_get_exit_io_rep := 3910.
Let sys_get_exit_io_str := 3920.
Let sys_get_exit_io_write := 3930.
Let sys_get_exit_io_neip := 3940.
Let sys_get_exit_fault_addr := 3950.
Let sys_inject_event := 3960.
Let sys_get_next_eip := 3970.
Let sys_sync := 3980.
Let sys_set_reg := 3990.
Let sys_get_reg := 4000.
Let sys_run_vm := 4010.
Let sys_is_chan_ready := 4020.
Let sys_sendto_chan := 4030.
Let sys_receive_chan := 4040.
Let sys_yield := 4050.
Let sys_send := 4060.
Let sys_recv := 4070.
Let sys_spawn := 4080.
Let sys_sleep := 4090.
Let sys_ready := 4100.
Let pgf_handler := 4110.
Let sys_certikos_init := 4120.
Let ptfault_resv := 4130.
Let syscall_dispatch_C := 4140.
Let syscall_dispatch := 4150.
Let sys_puts := 4160.
Let sys_ring0_spawn := 4170.
Let sys_disk_op := 4180.
Let sys_disk_cap := 4190.
Let sys_get_tsc_per_ms := 4200.
Let sys_get_tsc_offset := 4210.
Let sys_set_tsc_offset := 4220.
Let sys_get_exitinfo := 4230.
Let sys_mmap := 4240.
Let sys_intercept_int_window := 4250.
Let sys_handle_rdmsr := 4260.
Let sys_handle_wrmsr := 4270.
Let yield := 4280.
Let AC_LOC := 4290.
Let container_init := 4300.
Let container_get_parent := 4310.
Let container_get_nchildren := 4320.
Let container_get_quota := 4330.
Let container_get_usage := 4340.
Let container_can_consume := 4350.
Let container_split := 4360.
Let container_revoke := 4370.
Let container_alloc := 4380.
Let container_free := 4390.
Let flatmem_copy := 4400.
Let init_sync_chan := 4410.
Let set_sync_chan_to := 4420.
Let get_sync_chan_to := 4430.
Let set_sync_chan_paddr := 4440.
Let get_sync_chan_paddr := 4450.
Let set_sync_chan_count := 4460.
Let get_sync_chan_count := 4470.
Let is_pid_sending_to := 4480.
Let syncsendto_chan_pre := 4490.
Let syncsendto_chan_post := 4500.
Let syncreceive_chan := 4510.
Let get_kernel_pa := 4520.
Let SYNCCHPOOL_LOC := 4530.
Let sys_ssend_to_chan := 4540.
Let sys_srecv_chan := 4550.
Let ssend_to_chan := 4560.
Let srecv_chan := 4570.
Let thread_sleep2 := 4580.
Let thread_wakeup2 := 4590.
Let trap_sendtochan_pre := 4600.
Let trap_sendtochan_post := 4610.
Let sys_sendtochan_post := 4620.
Let sys_sendtochan_pre := 4630.
Let device_output := 4640.
Let print := 4650.
Let sys_print := 4660.
Let trap_print := 4670.
Let sys_offer_shared_mem := 4680.