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_lock := 1040.
Let thread_sleep := 1050.
Let START_USER_FUN_LOC := 1060.
Let proc_start_user := 1070.
Let proc_exit_user := 1080.
Let START_USER_FUN_LOC2 := 1090.
Let proc_start_user2 := 1100.
Let proc_exit_user2 := 1110.
Let svm_run_vm := 1120.
Let svm_exit_vm := 1130.
Let trap_get := 1140.
Let trap_set := 1150.
Let la2pa_resv := 1160.
Let uctx_arg1 := 1170.
Let uctx_arg2 := 1180.
Let uctx_arg3 := 1190.
Let uctx_arg4 := 1200.
Let uctx_arg5 := 1210.
Let uctx_arg6 := 1220.
Let uctx_set_errno := 1230.
Let uctx_set_retval1 := 1240.
Let uctx_set_retval2 := 1250.
Let uctx_set_retval3 := 1260.
Let uctx_set_retval4 := 1270.
Let npt_insert := 1280.
Let svm_set_intercept_intwin := 1290.
Let vmcb_set_seg := 1300.
Let vmcb_check_int_shadow := 1310.
Let vmcb_check_pending_event := 1320.
Let svm_get_exit_reason := 1330.
Let svm_get_exit_io_port := 1340.
Let svm_get_exit_io_width := 1350.
Let svm_get_exit_io_rep := 1360.
Let svm_get_exit_io_str := 1370.
Let svm_get_exit_io_write := 1380.
Let svm_get_exit_io_neip := 1390.
Let svm_get_exit_fault_addr := 1400.
Let vmcb_get_next_eip := 1410.
Let svm_sync := 1420.
Let is_chan_ready := 1430.
Let sendto_chan := 1440.
Let receive_chan := 1450.
Let proc_create := 1460.
Let proc_create_postinit := 1470.
Let svm_set_reg := 1480.
Let svm_get_reg := 1490.
Let restore_hctx := 1500.
Let svm_state_save := 1510.
Let host_in := 1520.
Let pt_resv := 1530.
Let pt_resv2 := 1540.
Let uctx_get := 1550.
Let vmcb_set_intercept_vint := 1560.
Let vmcb_get_exit_info := 1570.
Let vmcb_inject_virq := 1580.
Let vmcb_clear_virq := 1590.
Let vmcb_inject_event := 1600.
Let xvmst_read := 1610.
Let xvmst_write := 1620.
Let vmcb_set_reg := 1630.
Let vmcb_get_reg := 1640.
Let vmcb_restore := 1650.
Let xvmst_restore := 1660.
Let save_hctx := 1670.
Let vmcb_read_z := 1680.
Let vmcb_read_v := 1690.
Let vmcb_write_v := 1700.
Let XVMST_LOC := 1710.
Let vmcb_write_z := 1720.
Let npt_init := 1730.
Let host_out := 1740.
Let VMCB_Z_LOC := 1750.
Let HCtxt_LOC := 1760.
Let proc_init := 1770.
Let NPT_LOC := 1780.
Let restore_uctx := 1790.
Let save_uctx := 1800.
Let pt_out := 1810.
Let pt_in := 1820.
Let trap_in := 1830.
Let uctx_set := 1840.
Let uctx_set_eip := 1850.
Let elf_load := 1860.
Let thread_spawn := 1870.
Let thread_kill := 1880.
Let trap_out := 1890.
Let UCTX_LOC := 1900.
Let get_chan_info := 1910.
Let set_chan_info := 1920.
Let get_chan_content := 1930.
Let set_chan_content := 1940.
Let get_curid := 1950.
Let thread_wakeup := 1960.
Let thread_wakeup_lock := 1970.
Let init_chan := 1980.
Let sched_init := 1990.
Let CHPOOL_LOC := 2000.
Let offer_shared_mem := 2010.
Let shared_mem_status := 2020.
Let shared_mem_init := 2030.
Let get_shared_mem_status_seen := 2040.
Let shared_mem_to_ready := 2050.
Let shared_mem_to_pending := 2060.
Let shared_mem_to_dead := 2070.
Let clear_shared_mem := 2080.
Let set_shared_mem_seen := 2090.
Let set_shared_mem_loc := 2100.
Let set_shared_mem_state := 2110.
Let get_shared_mem_seen := 2120.
Let get_shared_mem_loc := 2130.
Let get_shared_mem_state := 2140.
Let SHRDMEMPOOL_LOC := 2150.
Let thread_sched := 2160.
Let kctxt_switch := 2170.
Let set_curid := 2180.
Let set_curid_init := 2190.
Let set_state := 2200.
Let enqueue := 2210.
Let dequeue := 2220.
Let queue_rmv := 2230.
Let kctxt_new := 2240.
Let tdqueue_init := 2250.
Let thread_free := 2260.
Let CURID_LOC := 2270.
Let get_prev := 2280.
Let get_state := 2290.
Let set_prev := 2300.
Let get_next := 2310.
Let set_next := 2320.
Let get_head := 2330.
Let set_head := 2340.
Let get_tail := 2350.
Let set_tail := 2360.
Let tdq_init := 2370.
Let thread_init := 2380.
Let TDQPool_LOC := 2390.
Let tcb_init := 2400.
Let pmap_init := 2410.
Let pt_free := 2420.
Let TCBPool_LOC := 2430.
Let set_RA := 2440.
Let set_SP := 2450.
Let pt_new := 2460.
Let KCtxtPool_LOC := 2470.
Let pfree := 2480.
Let palloc := 2490.
Let palloc_aux := 2500.
Let set_bit := 2510.
Let is_used := 2520.
Let pt_init := 2530.
Let PTP_LOC := 2540.
Let pt_init_kern := 2550.
Let set_cr3 := 2560.
Let set_pg := 2570.
Let pt_init_comm := 2580.
Let pt_insert := 2590.
Let pt_rmv := 2600.
Let pt_alloc_pde := 2610.
Let pt_free_pde := 2620.
Let idpde_init := 2630.
Let pt_read := 2640.
Let pt_read_pde := 2650.
Let pt_rmv_aux := 2660.
Let pt_rmv_pde := 2670.
Let pt_insert_aux := 2680.
Let pt_insert_pde := 2690.
Let set_IDPTE := 2700.
Let rmv_PDE := 2710.
Let set_PDE := 2720.
Let set_PDEU := 2730.
Let get_PDE := 2740.
Let clear_PDE := 2750.
Let mem_init := 2760.
Let get_PTE := 2770.
Let set_PTE := 2780.
Let rmv_PTE := 2790.
Let set_pt := 2800.
Let PTPool_LOC := 2810.
Let IDPMap_LOC := 2820.
Let at_get_c := 2830.
Let at_set_c := 2840.
Let at_get := 2850.
Let at_set := 2860.
Let is_norm := 2870.
Let get_nps := 2880.
Let get_size := 2890.
Let get_mms := 2900.
Let get_mml := 2910.
Let is_usable := 2920.
Let set_norm := 2930.
Let set_nps := 2940.
Let boot_loader := 2950.
Let NPS_LOC := 2960.
Let AT_LOC := 2970.
Let ATC_LOC := 2980.
Let fload := 2990.
Let fstore := 3000.
Let FlatMem_LOC := 3010.
Let vmx_return_from_guest := 3020.
Let rcr0 := 3030.
Let rcr3 := 3040.
Let rcr4 := 3050.
Let rdmsr := 3060.
Let wrmsr := 3070.
Let vmptrld := 3080.
Let VMCS_LOC := 3090.
Let VMX_LOC := 3100.
Let msr_bitmap_LOC := 3110.
Let io_bitmap_LOC := 3120.
Let tss_LOC := 3130.
Let gdt_LOC := 3140.
Let idt_LOC := 3150.
Let vmx_read := 3160.
Let vmx_write := 3170.
Let vmx_readz := 3180.
Let vmx_writez := 3190.
Let vmx_readz64 := 3200.
Let vmx_writez64 := 3210.
Let set_NPDE := 3220.
Let set_NPTE := 3230.
Let vmcs_get_abrtid := 3240.
Let vmcs_set_abrtid := 3250.
Let vmcs_get_revid := 3260.
Let vmcs_set_revid := 3270.
Let vmcs_readz := 3280.
Let vmcs_writez := 3290.
Let vmcs_readz64 := 3300.
Let vmcs_writez64 := 3310.
Let vmcs_read := 3320.
Let vmcs_write := 3330.
Let vmcs_write_ident := 3340.
Let vmx_get_exit_qualification := 3350.
Let vmx_get_exit_io_port := 3360.
Let vmx_set_intercept_intwin := 3370.
Let vmx_set_desc := 3380.
Let vmx_set_desc1 := 3390.
Let vmx_set_desc2 := 3400.
Let vmx_inject_event := 3410.
Let vmx_check_pending_event := 3420.
Let vmx_check_int_shadow := 3430.
Let vmx_get_exit_reason := 3440.
Let vmx_set_tsc_offset := 3450.
Let vmx_get_tsc_offset := 3460.
Let vmx_get_exit_fault_addr := 3470.
Let vmcs_set_defaults := 3480.
Let vmx_get_reg := 3490.
Let vmx_set_reg := 3500.
Let vmx_get_next_eip := 3510.
Let vmx_get_io_width := 3520.
Let vmx_get_io_write := 3530.
Let vmx_get_exit_io_rep := 3540.
Let vmx_get_exit_io_str := 3550.
Let vmx_set_mmap := 3560.
Let vmx_set_ctlreg := 3570.
Let vmx_run_vm := 3580.
Let vmx_run_return_from_guest := 3590.
Let vmx_init := 3600.
Let vmx_enter_pre := 3610.
Let vmx_exit_post := 3620.
Let EPT_LOC := 3630.
Let set_EPML4E := 3640.
Let get_EPTE := 3650.
Let set_EPTE := 3660.
Let set_EPDTE := 3670.
Let set_EPDPTE := 3680.
Let ept_invalidate_mappings := 3690.
Let ept_insert := 3700.
Let ept_init := 3710.
Let ept_add_mapping := 3720.
Let ept_get_page_entry := 3730.
Let ept_set_page_entry := 3740.
Let ept_gpa_to_hpa := 3750.
Let ept_set_permission := 3760.
Let ept_mmap := 3770.
Let vmxinfo_get := 3780.
Let vmx_exit := 3790.
Let vmx_enter := 3800.
Let vmx_enter_bottom_half := 3810.
Let vmx_exit_bottom_half := 3820.
Let vmxon := 3830.
Let vmx_enable := 3840.
Let sys_palloc := 3850.
Let sys_pfree := 3860.
Let sys_pt_read := 3870.
Let sys_thread_kill := 3880.
Let sys_thread_wakeup := 3890.
Let sys_get_curid := 3900.
Let sys_get_quota := 3910.
Let sys_uctx_get := 3920.
Let sys_uctx_set := 3930.
Let sys_thread_yield := 3940.
Let sys_thread_sleep := 3950.
Let sys_svm_exit_vm := 3960.
Let sys_proc_create := 3970.
Let sys_npt_insert := 3980.
Let sys_ept_insert := 3990.
Let sys_set_intercept_intwin := 4000.
Let sys_set_seg := 4010.
Let sys_set_seg1 := 4020.
Let sys_set_seg2 := 4030.
Let sys_check_int_shadow := 4040.
Let sys_check_pending_event := 4050.
Let sys_get_exit_reason := 4060.
Let sys_get_exit_io_port := 4070.
Let sys_get_exit_io_width := 4080.
Let sys_get_exit_io_rep := 4090.
Let sys_get_exit_io_str := 4100.
Let sys_get_exit_io_write := 4110.
Let sys_get_exit_io_neip := 4120.
Let sys_get_exit_fault_addr := 4130.
Let sys_inject_event := 4140.
Let sys_get_next_eip := 4150.
Let sys_sync := 4160.
Let sys_set_reg := 4170.
Let sys_get_reg := 4180.
Let sys_run_vm := 4190.
Let sys_is_chan_ready := 4200.
Let sys_sendto_chan := 4210.
Let sys_receive_chan := 4220.
Let sys_yield := 4230.
Let sys_send := 4240.
Let sys_recv := 4250.
Let sys_trysendto_chan := 4260.
Let sys_tryreceive_chan := 4270.
Let sys_trysend := 4280.
Let sys_tryrecv := 4290.
Let sys_spawn := 4300.
Let sys_sleep := 4310.
Let sys_ready := 4320.
Let pgf_handler := 4330.
Let sys_certikos_init := 4340.
Let ptfault_resv := 4350.
Let syscall_dispatch_C := 4360.
Let syscall_dispatch := 4370.
Let sys_puts := 4380.
Let sys_ring0_spawn := 4390.
Let sys_disk_op := 4400.
Let sys_disk_cap := 4410.
Let sys_get_tsc_per_ms := 4420.
Let sys_get_tsc_offset := 4430.
Let sys_set_tsc_offset := 4440.
Let sys_get_exitinfo := 4450.
Let sys_mmap := 4460.
Let sys_intercept_int_window := 4470.
Let sys_handle_rdmsr := 4480.
Let sys_handle_wrmsr := 4490.
Let AC_LOC := 4500.
Let container_init := 4510.
Let container_get_parent := 4520.
Let container_get_nchildren := 4530.
Let container_get_quota := 4540.
Let container_get_usage := 4550.
Let container_can_consume := 4560.
Let container_split := 4570.
Let container_revoke := 4580.
Let container_alloc := 4590.
Let container_free := 4600.
Let container_set_parent := 4610.
Let container_set_nchildren := 4620.
Let container_set_quota := 4630.
Let container_set_usage := 4640.
Let container_node_init := 4650.
Let flatmem_copy := 4660.
Let init_sync_chan := 4670.
Let set_sync_chan_to := 4680.
Let get_sync_chan_to := 4690.
Let set_sync_chan_paddr := 4700.
Let get_sync_chan_paddr := 4710.
Let set_sync_chan_count := 4720.
Let get_sync_chan_count := 4730.
Let is_pid_sending_to := 4740.
Let set_sync_chan_busy := 4750.
Let get_sync_chan_busy := 4760.
Let syncsendto_chan := 4770.
Let syncsendto_chan_pre := 4780.
Let syncsendto_chan_post := 4790.
Let syncreceive_chan := 4800.
Let trysendto_chan := 4810.
Let tryreceive_chan := 4820.
Let get_kernel_pa := 4830.
Let SYNCCHPOOL_LOC := 4840.
Let sys_ssend_to_chan := 4850.
Let sys_srecv_chan := 4860.
Let ssend_to_chan := 4870.
Let srecv_chan := 4880.
Let thread_sleep2 := 4890.
Let thread_wakeup2 := 4900.
Let trap_sendtochan_pre := 4910.
Let trap_sendtochan_post := 4920.
Let sys_sendtochan_post := 4930.
Let sys_sendtochan_pre := 4940.
Let get_CPU_ID := 4950.
Let release_lock := 4960.
Let acquire_lock := 4970.
Let acquire_lock_AT := 4980.
Let acquire_lock_PB := 4990.
Let acquire_lock_TCB := 5000.
Let acquire_lock_TDQ := 5010.
Let acquire_lock_CHAN := 5020.
Let release_lock_AT := 5030.
Let release_lock_PB := 5040.
Let release_lock_TCB := 5050.
Let release_lock_TDQ := 5060.
Let release_lock_CHAN := 5070.
Let try_lock := 5080.
Let try_lock_AT := 5090.
Let try_lock_PB := 5100.
Let try_lock_TCB := 5110.
Let try_lock_TDQ := 5120.
Let try_lock_CHAN := 5130.
Let acquire_shared := 5140.
Let release_shared := 5150.
Let get_now := 5160.
Let incr_now := 5170.
Let incr_ticket := 5180.
Let init_ticket := 5190.
Let log_get := 5200.
Let log_hold := 5210.
Let log_incr := 5220.
Let atomic_FAI := 5230.
Let log_init := 5240.
Let pre_acquire_lock := 5250.
Let set_lock_status := 5260.
Let TICKET_LOCK_LOC := 5270.
Let ticket_lock_init := 5280.
Let wait_lock := 5290.
Let pass_lock := 5300.
Let test_lock := 5310.
Let CAS_ticket := 5320.
Let CAS_log := 5330.
Let read_now := 5340.
Let MCS_LOCK_LOC := 5350.
Let atomic_mcs_log := 5360.
Let atomic_mcs_SWAP := 5370.
Let atomic_mcs_CAS := 5380.
Let mcs_init_node_log := 5390.
Let mcs_GET_NEXT_log := 5400.
Let mcs_SET_NEXT_log := 5410.
Let mcs_GET_BUSY_log := 5420.
Let mcs_SET_BUSY_log := 5430.
Let mcs_log := 5440.
Let mcs_init_node := 5450.
Let mcs_SWAP_TAIL := 5460.
Let mcs_CAS_TAIL := 5470.
Let mcs_GET_NEXT := 5480.
Let mcs_SET_NEXT := 5490.
Let mcs_GET_BUSY := 5500.
Let mcs_SET_BUSY := 5510.
Let mcs_swap_tail := 5520.
Let mcs_cas_tail := 5530.
Let mcs_get_next := 5540.
Let mcs_set_next := 5550.
Let mcs_get_busy := 5560.
Let mcs_set_busy := 5570.
Let mcs_lock_get_index := 5580.
Let mcs_lock_init := 5590.
Let mcs_wait_lock := 5600.
Let mcs_pass_lock := 5610.
Let get_qsize := 5620.
Let set_qsize := 5630.
Let get_qowner := 5640.
Let init_qowner := 5650.
Let clear_qowner := 5660.
Let set_qowner := 5670.
Let QUEUE_SIZE_POOL_LOC := 5680.
Let QUEUE_OWNER_POOL_LOC := 5690.
Let wait_queue := 5700.
Let pass_queue := 5710.
Let serial_in := 5720.
Let serial_out := 5730.
Let serial_hw_intr := 5740.
Let serial_irq_check := 5750.
Let serial_irq_current := 5760.
Let keyboard_in := 5770.
Let keyboard_hw_intr := 5780.
Let keyboard_irq_check := 5790.
Let ioapic_read := 5800.
Let ioapic_write := 5810.
Let lapic_read := 5820.
Let lapic_write := 5830.
Let hw_intr := 5840.
Let ic_intr := 5850.
Let cons_buf_LOC := 5860.
Let cons_buf_init_concrete := 5870.
Let cons_buf_write_concrete := 5880.
Let cons_buf_init := 5890.
Let cons_buf_write := 5900.
Let cons_buf_read := 5910.
Let cons_buf_wpos := 5920.
Let cons_intr := 5930.
Let cons_init := 5940.
Let serial_init := 5950.
Let serial_putc := 5960.
Let serial_getc := 5970.
Let get_serial_exists := 5980.
Let set_serial_exists := 5990.
Let kbd_buf_LOC := 6000.
Let kbd_states_LOC := 6010.
Let kbd_buf_init_concrete := 6020.
Let kbd_buf_write_concrete := 6030.
Let kbd_buf_init := 6040.
Let kbd_buf_write := 6050.
Let kbd_buf_read := 6060.
Let keyboard_init := 6070.
Let keyboard_scan := 6080.
Let keyboard_scan_code_normal_LOC := 6090.
Let keyboard_scan_code_shift_LOC := 6100.
Let keyboard_shift_toggle := 6110.
Let keyboard_shift_reset := 6120.
Let keyboard_shift_check := 6130.
Let keyboard_switch_key_map := 6140.
Let keyboard_map := 6150.
Let keyboard_proc_data := 6160.
Let keyboard_getc := 6170.
Let keyboard_intr := 6180.
Let kbd_intr_disable := 6190.
Let serial_exists_LOC := 6200.
Let ioapic_init := 6210.
Let ioapic_enable := 6220.
Let ioapic_mask := 6230.
Let ioapic_unmask := 6240.
Let lapic_init := 6250.
Let lapic_eoi := 6260.
Let interrupt_handler := 6270.
Let cli := 6280.
Let sti := 6290.
Let local_irq_save := 6300.
Let local_irq_restore := 6310.
Let save_context := 6320.
Let restore_context := 6330.
Let set_tf := 6340.
Let serial_intr_enable := 6350.
Let serial_intr_disable := 6360.
Let serial_intr_enable_handler := 6370.
Let serial_intr_disable_handler := 6380.
Let serial_intr_handler_asm := 6390.
Let serial_intr_handler_sw := 6400.
Let serial_intr_handler_ext := 6410.
Let kbd_intr_enable := 6420.
Let kbd_intr_disable_handler := 6430.
Let iret := 6440.
Let curr_intr_num_LOC := 6450.
Let get_curr_intr_num := 6460.
Let intr_default_handler := 6470.
Let sys_getc := 6480.
Let sys_putc := 6490.
Let tcb_get_CPU_ID := 6500.
Let tcb_set_CPU_ID := 6510.
Let pcpumsg_send := 6520.
Let pcpumsg_recv := 6530.
Let pcpumsg_try_recv := 6540.
Let enqueue_local := 6550.
Let dequeue_local := 6560.
Let queue_rmv_local := 6570.
Let enqueue_atomic := 6580.
Let dequeue_atomic := 6590.
Let queue_rmv_atomic := 6600.
Let enqueue_try := 6610.
Let dequeue_try := 6620.
Let queue_rmv_try := 6630.
Let thread_poll_pending := 6640.
Let sleeper_inc := 6650.
Let sleeper_dec := 6660.
Let sleeper_zzz := 6670.
Let SLEEPER_LOC := 6680.
Let sleeper_get := 6690.
Let sleeper_set := 6700.
Let fifobbq_init := 6710.
Let fifobbq_pre_insert := 6720.
Let fifobbq_post_insert := 6730.
Let fifobbq_pre_remove := 6740.
Let fifobbq_post_remove := 6750.
Let fifobbq_pool_init := 6760.
Let fifobbq_get_max := 6770.
Let fifobbq_get_front := 6780.
Let fifobbq_get_next := 6790.
Let fifobbq_get_head := 6800.
Let fifobbq_get_tail := 6810.
Let fifobbq_set_max := 6820.
Let fifobbq_set_front := 6830.
Let fifobbq_set_next := 6840.
Let fifobbq_set_head := 6850.
Let fifobbq_set_tail := 6860.
Let idq_init := 6870.
Let idq_pool_init := 6880.
Let idq_get_next := 6890.
Let idq_set_next := 6900.
Let idq_get_prev := 6910.
Let idq_set_prev := 6920.
Let idq_push := 6930.
Let idq_peek := 6940.
Let idq_pull := 6950.
Let ipc_send_body := 6960.
Let ipc_receive_body := 6970.
Let page_copy := 6980.
Let page_copy_back := 6990.
Let PAGE_BUFFER_LOC := 7000.