gh0s7/mckernel
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add ACSL annotation to cpu.c

Browse Source
This commit is contained in:
NAKAMURA Gou
2015-03-25 15:54:08 +09:00
parent 7bba05cfa4
commit 9271d5346d
1 changed files with 125 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

125
arch/x86/kernel/cpu.c
View File

@@ -446,6 +446,10 @@ static void init_smp_processor(void)
static char *trampoline_va, *first_page_va; static char *trampoline_va, *first_page_va;
/*@
@ assigns torampoline_va;
@ assigns first_page_va;
@*/
void ihk_mc_init_ap(void) void ihk_mc_init_ap(void)
{ {
struct ihk_mc_cpu_info *cpu_info = ihk_mc_get_cpu_info(); struct ihk_mc_cpu_info *cpu_info = ihk_mc_get_cpu_info();
@@ -791,31 +795,65 @@ void cpu_halt(void)
asm volatile("hlt"); asm volatile("hlt");
} }
/*@
@ assigns \nothing;
@ ensures \interrupt_disabled == 0;
@*/
void cpu_safe_halt(void) void cpu_safe_halt(void)
{ {
asm volatile("sti; hlt"); asm volatile("sti; hlt");
} }
/*@
@ assigns \nothing;
@ ensures \interrupt_disabled == 0;
@*/
void cpu_enable_interrupt(void) void cpu_enable_interrupt(void)
{ {
asm volatile("sti"); asm volatile("sti");
} }
/*@
@ assigns \nothing;
@ ensures \interrupt_disabled > 0;
@*/
void cpu_disable_interrupt(void) void cpu_disable_interrupt(void)
{ {
asm volatile("cli"); asm volatile("cli");
} }
/*@
@ assigns \nothing;
@ behavior to_enabled:
@ assumes flags & RFLAGS_IF;
@ ensures \interrupt_disabled == 0;
@ behavior to_disabled:
@ assumes !(flags & RFLAGS_IF);
@ ensures \interrupt_disabled > 0;
@*/
void cpu_restore_interrupt(unsigned long flags) void cpu_restore_interrupt(unsigned long flags)
{ {
asm volatile("push %0; popf" : : "g"(flags) : "memory", "cc"); asm volatile("push %0; popf" : : "g"(flags) : "memory", "cc");
} }
/*@
@ assigns \nothing;
@*/
void cpu_pause(void) void cpu_pause(void)
{ {
asm volatile("pause" ::: "memory"); asm volatile("pause" ::: "memory");
} }
/*@
@ assigns \nothing;
@ ensures \interrupt_disabled > 0;
@ behavior from_enabled:
@ assumes \interrupt_disabled == 0;
@ ensures \result & RFLAGS_IF;
@ behavior from_disabled:
@ assumes \interrupt_disabled > 0;
@ ensures !(\result & RFLAGS_IF);
@*/
unsigned long cpu_disable_interrupt_save(void) unsigned long cpu_disable_interrupt_save(void)
{ {
unsigned long flags; unsigned long flags;
@@ -825,6 +863,17 @@ unsigned long cpu_disable_interrupt_save(void)
return flags; return flags;
} }
/*@
@ behavior valid_vector:
@ assumes 32 <= vector <= 255;
@ requires \valid(h);
@ assigns handlers[vector-32];
@ ensures \result == 0;
@ behavior invalid_vector:
@ assumes (vector < 32) || (255 < vector);
@ assigns \nothing;
@ ensures \result == -EINVAL;
@*/
int ihk_mc_register_interrupt_handler(int vector, int ihk_mc_register_interrupt_handler(int vector,
struct ihk_mc_interrupt_handler *h) struct ihk_mc_interrupt_handler *h)
{ {
@@ -846,6 +895,11 @@ int ihk_mc_unregister_interrupt_handler(int vector,
extern unsigned long __page_fault_handler_address; extern unsigned long __page_fault_handler_address;
/*@
@ requires \valid(h);
@ assigns __page_fault_handler_address;
@ ensures __page_fault_handler_address == h;
@*/
void ihk_mc_set_page_fault_handler(void (*h)(void *, uint64_t, void *)) void ihk_mc_set_page_fault_handler(void (*h)(void *, uint64_t, void *))
{ {
__page_fault_handler_address = (unsigned long)h; __page_fault_handler_address = (unsigned long)h;
@@ -855,6 +909,18 @@ extern char trampoline_code_data[], trampoline_code_data_end[];
struct page_table *get_init_page_table(void); struct page_table *get_init_page_table(void);
unsigned long get_transit_page_table(void); unsigned long get_transit_page_table(void);
/* reusable, but not reentrant */
/*@
@ requires \valid_apicid(cpuid); // valid APIC ID or not
@ requires \valid(pc);
@ requires \valid(trampoline_va);
@ requires \valid(trampoline_code_data
@ +(0..(trampoline_code_data_end - trampoline_code_data)));
@ requires \valid_physical(ap_trampoline); // valid physical address or not
@ assigns (char *)trampoline_va+(0..trampoline_code_data_end - trampoline_code_data);
@ assigns cpu_boot_status;
@ ensures cpu_boot_status != 0;
@*/
void ihk_mc_boot_cpu(int cpuid, unsigned long pc) void ihk_mc_boot_cpu(int cpuid, unsigned long pc)
{ {
unsigned long *p; unsigned long *p;
@@ -882,6 +948,11 @@ void ihk_mc_boot_cpu(int cpuid, unsigned long pc)
} }
} }
/*@
@ requires \valid(new_ctx);
@ requires (stack_pointer == NULL) || \valid((unsigned long *)stack_pointer-1);
@ requires \valid(next_function);
@*/
void ihk_mc_init_context(ihk_mc_kernel_context_t *new_ctx, void ihk_mc_init_context(ihk_mc_kernel_context_t *new_ctx,
void *stack_pointer, void (*next_function)(void)) void *stack_pointer, void (*next_function)(void))
{ {
@@ -901,6 +972,15 @@ void ihk_mc_init_context(ihk_mc_kernel_context_t *new_ctx,
extern char enter_user_mode[]; extern char enter_user_mode[];
/*@
@ requires \valid(ctx);
@ requires \valid(puctx);
@ requires \valid((ihk_mc_user_context_t *)stack_pointer-1);
@ requires \valid_user(new_pc); // valid user space address or not
@ requires \valid_user(user_sp-1);
@ assigns *((ihk_mc_user_context_t *)stack_pointer-1);
@ assigns ctx->rsp0;
@*/
void ihk_mc_init_user_process(ihk_mc_kernel_context_t *ctx, void ihk_mc_init_user_process(ihk_mc_kernel_context_t *ctx,
ihk_mc_user_context_t **puctx, ihk_mc_user_context_t **puctx,
void *stack_pointer, unsigned long new_pc, void *stack_pointer, unsigned long new_pc,
@@ -927,6 +1007,18 @@ void ihk_mc_init_user_process(ihk_mc_kernel_context_t *ctx,
ctx->rsp0 = (unsigned long)stack_pointer; ctx->rsp0 = (unsigned long)stack_pointer;
} }
/*@
@ behavior rsp:
@ assumes reg == IHK_UCR_STACK_POINTER;
@ requires \valid(uctx);
@ assigns uctx->gpr.rsp;
@ ensures uctx->gpr.rsp == value;
@ behavior rip:
@ assumes reg == IHK_UCR_PROGRAM_COUNTER;
@ requires \valid(uctx);
@ assigns uctx->gpr.rip;
@ ensures uctx->gpr.rip == value;
@*/
void ihk_mc_modify_user_context(ihk_mc_user_context_t *uctx, void ihk_mc_modify_user_context(ihk_mc_user_context_t *uctx,
enum ihk_mc_user_context_regtype reg, enum ihk_mc_user_context_regtype reg,
unsigned long value) unsigned long value)
@@ -946,11 +1038,19 @@ void ihk_mc_print_user_context(ihk_mc_user_context_t *uctx)
uctx->gpr.rsi, uctx->gpr.rdi, uctx->gpr.rsp); uctx->gpr.rsi, uctx->gpr.rdi, uctx->gpr.rsp);
} }
/*@
@ requires \valid(handler);
@ assigns __x86_syscall_handler;
@ ensures __x86_syscall_handler == handler;
@*/
void ihk_mc_set_syscall_handler(long (*handler)(int, ihk_mc_user_context_t *)) void ihk_mc_set_syscall_handler(long (*handler)(int, ihk_mc_user_context_t *))
{ {
__x86_syscall_handler = handler; __x86_syscall_handler = handler;
} }
/*@
@ assigns \nothing;
@*/
void ihk_mc_delay_us(int us) void ihk_mc_delay_us(int us)
{ {
arch_delay(us); arch_delay(us);
@@ -1012,6 +1112,14 @@ void arch_show_interrupt_context(const void *reg)
kprintf_unlock(irqflags); kprintf_unlock(irqflags);
} }
/*@
@ behavior fs_base:
@ assumes type == IHK_ASR_X86_FS;
@ ensures \result == 0;
@ behavior invaiid_type:
@ assumes type != IHK_ASR_X86_FS;
@ ensures \result == -EINVAL;
@*/
int ihk_mc_arch_set_special_register(enum ihk_asr_type type, int ihk_mc_arch_set_special_register(enum ihk_asr_type type,
unsigned long value) unsigned long value)
{ {
@@ -1025,6 +1133,15 @@ int ihk_mc_arch_set_special_register(enum ihk_asr_type type,
} }
} }
/*@
@ behavior fs_base:
@ assumes type == IHK_ASR_X86_FS;
@ requires \valid(value);
@ ensures \result == 0;
@ behavior invalid_type:
@ assumes type != IHK_ASR_X86_FS;
@ ensures \result == -EINVAL;
@*/
int ihk_mc_arch_get_special_register(enum ihk_asr_type type, int ihk_mc_arch_get_special_register(enum ihk_asr_type type,
unsigned long *value) unsigned long *value)
{ {
@@ -1038,6 +1155,10 @@ int ihk_mc_arch_get_special_register(enum ihk_asr_type type,
} }
} }
/*@
@ requires \valid_apicid(cpu); // valid APIC ID or not
@ ensures \result == 0
@*/
int ihk_mc_interrupt_cpu(int cpu, int vector) int ihk_mc_interrupt_cpu(int cpu, int vector)
{ {
dkprintf("[%d] ihk_mc_interrupt_cpu: %d\n", ihk_mc_get_processor_id(), cpu); dkprintf("[%d] ihk_mc_interrupt_cpu: %d\n", ihk_mc_get_processor_id(), cpu);
@@ -1047,6 +1168,10 @@ int ihk_mc_interrupt_cpu(int cpu, int vector)
return 0; return 0;
} }
/*@
@ requires \valid(proc);
@ ensures proc->fp_regs == NULL;
@*/
void void
release_fp_regs(struct process *proc) release_fp_regs(struct process *proc)
{ {