Library mcertikos.trap.TTrapCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Export GlobalOracle.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Export GlobalOracle.
extern unsigned int uctx_arg1(void);
extern unsigned int uctx_arg2(void);
extern unsigned int uctx_arg3(void);
extern unsigned int uctx_arg4(void);
extern unsigned int uctx_arg5(void);
extern void uctx_set_errno(unsigned int);
extern void uctx_set_retval1(unsigned int);
extern unsigned int syncsendto_chan_pre(unsigned int, unsigned int, unsigned int);
unsigned int trap_sendtochan_pre()
{
unsigned int chid;
unsigned int vaddr;
unsigned int scount;
unsigned int val;
chid = uctx_arg2();
vaddr = uctx_arg3();
scount = uctx_arg4();
val = syncsendto_chan_pre(chid, vaddr, scount);
return val;
}
Definition _chid := 100 % positive.
Definition _vaddr := 101 % positive.
Definition _scount := 102 % positive.
Definition _val := 103 % positive.
Definition trap_sendtochan_pre_body :=
(Ssequence
(Scall (Some _chid) (Evar uctx_arg2 (Tfunction Tnil tuint cc_default))
nil)
(Ssequence
(Scall (Some _vaddr)
(Evar uctx_arg3 (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall (Some _scount)
(Evar uctx_arg4 (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall None
(Evar acquire_lock_CHAN (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _val)
(Evar syncsendto_chan_pre (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tuint cc_default))
((Etempvar _chid tuint) :: (Etempvar _vaddr tuint) ::
(Etempvar _scount tuint) :: nil))
(Ssequence
(Scall None
(Evar release_lock (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Econst_int (Int.repr ID_SC) tint) :: nil))
(Sreturn (Some (Etempvar _val tuint))))))))).
Definition f_trap_sendtochan_pre := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_chid, tuint) :: (_vaddr, tuint) :: (_scount, tuint) :: (_val, tuint) :: nil);
fn_body := trap_sendtochan_pre_body
|}.
extern void uctx_set_errno(unsigned int);
extern void uctx_set_retval1(unsigned int);
extern unsigned int syncsendto_chan_post(void);
void trap_sendtochan_post()
{
unsigned int val;
val = syncsendto_chan_post();
uctx_set_retval1(val);
uctx_set_errno(0);
}
Definition trap_sendtochan_post_body :=
(Ssequence
(Scall None
(Evar acquire_lock_CHAN (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _val)
(Evar syncsendto_chan_post (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall None
(Evar release_lock (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Econst_int (Int.repr ID_SC) tint) :: nil))
(Ssequence
(Scall None
(Evar uctx_set_retval1 (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Etempvar _val tuint) :: nil))
(Scall None
(Evar uctx_set_errno (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Econst_int (Int.repr 0) tint) :: nil)))))).
Definition f_trap_sendtochan_post := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_val, tuint) :: nil);
fn_body := trap_sendtochan_post_body
|}.
#define SYS_puts 0
#define SYS_ring0_spawn 1
#define SYS_spawn 2
#define SYS_yield 3
#define SYS_sleep 4
#define SYS_disk_op 5
#define SYS_disk_cap 6
#define SYS_is_chan_ready 7
#define SYS_send 8
#define SYS_recv 9
#define SYS_get_tsc_per_ms 10
#define SYS_hvm_run_vm 11
#define SYS_hvm_get_exitinfo 12
#define SYS_hvm_mmap 13
#define SYS_hvm_set_seg 14
#define SYS_hvm_set_reg 15
#define SYS_hvm_get_reg 16
#define SYS_hvm_get_next_eip 17
#define SYS_hvm_inject_event 18
#define SYS_hvm_check_int_shadow 19
#define SYS_hvm_check_pending_event 20
#define SYS_hvm_intercept_int_window 21
#define SYS_hvm_get_tsc_offset 22
#define SYS_hvm_set_tsc_offset 23
#define SYS_hvm_handle_rdmsr 24
#define SYS_hvm_handle_wrmsr 25
#define SYS_get_quota 26
#define SYS_getc 27
#define SYS_putc 28
#define SYS_hvm_set_seg1 40
#define SYS_hvm_set_seg2 41
#define MAX_SYSCALL_NR 42
#define E_INVAL_CALLNR 3
extern void sys_proc_create(void);
extern void sys_receive_chan(void);
extern void sys_get_quota(void);
extern void uctx_set_errno(unsigned int);
extern unsigned int uctx_arg1(void);
void syscall_dispatch_c()
{
unsigned int arg1;
arg1 = uctx_arg1();
if (arg1 == SYS_spawn)
sys_proc_create();
else if(arg1 == SYS_get_quota)
sys_get_quota();
else if(arg1 == SYS_send)
sys_sendto_chan();
else if(arg1 == SYS_recv)
sys_receive_chan();
else if(arg1 == SYS_yield)
thread_yield();
else if(arg1 == SYS_getc)
sys_getc();
else if(arg1 == SYS_putc)
sys_putc();
else if (arg1 == SYS_hvm_get_tsc_offset)
sys_get_tsc_offset ();
else if (arg1 == SYS_hvm_set_tsc_offset)
sys_set_tsc_offset ();
else if (arg1 == SYS_hvm_get_exitinfo)
sys_get_exitinfo ();
else if (arg1 == SYS_hvm_mmap)
sys_mmap ();
else if (arg1 == SYS_hvm_set_reg)
sys_set_reg ();
else if (arg1 == SYS_hvm_get_reg)
sys_get_reg ();
else if (arg1 == SYS_hvm_set_seg1)
sys_set_seg1 ();
else if (arg1 == SYS_hvm_set_seg2)
sys_set_seg2 ();
else if (arg1 == SYS_hvm_get_next_eip)
sys_get_next_eip ();
else if (arg1 == SYS_hvm_inject_event)
sys_inject_event ();
else if (arg1 == SYS_hvm_check_pending_event)
sys_check_pending_event ();
else if (arg1 == SYS_hvm_check_int_shadow)
sys_check_int_shadow ();
else if (arg1 == SYS_hvm_intercept_int_window)
sys_intercept_int_window ();
else if (arg1 == SYS_hvm_handle_rdmsr)
sys_handle_rdmsr ();
else if (arg1 == SYS_hvm_handle_wrmsr)
sys_handle_wrmsr ();
else
uctx_set_errno(E_INVAL_CALLNR);
}
Definition _arg1 := 1 % positive.
Definition syscall_dispatch_c_body :=
(Ssequence
(Scall (Some _arg1) (Evar uctx_arg1 (Tfunction Tnil tuint cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 2) tint) tint)
(Scall None (Evar sys_proc_create (Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 26) tint) tint)
(Scall None (Evar sys_get_quota (Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 8) tint) tint)
(Scall None (Evar sys_sendto_chan (Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 9) tint) tint)
(Scall None
(Evar sys_receive_chan (Tfunction Tnil tvoid cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 3) tint) tint)
(Scall None
(Evar thread_yield (Tfunction Tnil tvoid cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 27) tint) tint)
(Scall None (Evar sys_getc (Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 28) tint) tint)
(Scall None
(Evar sys_putc (Tfunction Tnil tvoid cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 22) tint) tint)
(Scall None
(Evar sys_get_tsc_offset (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 23) tint) tint)
(Scall None
(Evar sys_set_tsc_offset (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 12) tint) tint)
(Scall None
(Evar sys_get_exitinfo (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 13) tint) tint)
(Scall None
(Evar sys_mmap (Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 15) tint) tint)
(Scall None
(Evar sys_set_reg (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 16) tint)
tint)
(Scall None
(Evar sys_get_reg (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 40) tint)
tint)
(Scall None
(Evar sys_set_seg1 (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 41) tint)
tint)
(Scall None
(Evar sys_set_seg2 (Tfunction Tnil tvoid
cc_default)) nil)
(Sifthenelse (Ebinop Oeq (Etempvar _arg1 tuint)
(Econst_int (Int.repr 17) tint)
tint)
(Scall None
(Evar sys_get_next_eip (Tfunction Tnil
tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 18) tint)
tint)
(Scall None
(Evar sys_inject_event (Tfunction Tnil
tvoid
cc_default))
nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 20) tint)
tint)
(Scall None
(Evar sys_check_pending_event
(Tfunction Tnil tvoid cc_default)) nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 19) tint)
tint)
(Scall None
(Evar sys_check_int_shadow (Tfunction
Tnil
tvoid
cc_default))
nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 21) tint)
tint)
(Scall None
(Evar sys_intercept_int_window
(Tfunction Tnil tvoid cc_default))
nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 24) tint)
tint)
(Scall None
(Evar sys_handle_rdmsr (Tfunction
Tnil
tvoid
cc_default))
nil)
(Sifthenelse (Ebinop Oeq
(Etempvar _arg1 tuint)
(Econst_int (Int.repr 25) tint)
tint)
(Scall None
(Evar sys_handle_wrmsr
(Tfunction Tnil tvoid
cc_default)) nil)
(Scall None
(Evar uctx_set_errno (Tfunction (Tcons tuint Tnil) tvoid
cc_default))
((Econst_int (Int.repr 3) tint) :: nil))))))))))))))))))))))))).
Definition f_syscall_dispatch_c := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_arg1, tuint) :: nil);
fn_body := syscall_dispatch_c_body
|}.