Library mcertikos.proc.PThreadCSource
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 Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
#define num_chan 64 struct ChanStruct { unsigned int isbusy; unsigned int content; }; extern struct ChanStruct CHPOOL_LOC[num_chan]; unsigned int get_chan_info(unsigned int chan_index) { return CHPOOL_LOC[chan_index].isbusy; }
Local Open Scope positive_scope.
Let tchan_index: ident := 1.
Local Open Scope Z_scope.
Definition get_chan_info_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) isbusy tint))).
Definition f_get_chan_info := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: nil);
fn_temps := nil;
fn_body := get_chan_info_body
|}.
Let tchan_index: ident := 1.
Local Open Scope Z_scope.
Definition get_chan_info_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) isbusy tint))).
Definition f_get_chan_info := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: nil);
fn_temps := nil;
fn_body := get_chan_info_body
|}.
#define num_chan 64 struct ChanStruct { unsigned int isbusy; unsigned int content; }; extern struct ChanStruct CHPOOL_LOC[num_chan]; void set_chan_info(unsigned int chan_index, unsigned int info) { CHPOOL_LOC[chan_index].isbusy = info; }
Local Open Scope positive_scope.
Let tinfo: ident := 2.
Local Open Scope Z_scope.
Definition set_chan_info_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) isbusy tint) (Etempvar tinfo tint)).
Definition f_set_chan_info := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: (tinfo, tint) :: nil);
fn_temps := nil;
fn_body := set_chan_info_body
|}.
Let tinfo: ident := 2.
Local Open Scope Z_scope.
Definition set_chan_info_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) isbusy tint) (Etempvar tinfo tint)).
Definition f_set_chan_info := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: (tinfo, tint) :: nil);
fn_temps := nil;
fn_body := set_chan_info_body
|}.
#define num_chan 64 struct ChanStruct { unsigned int isbusy; unsigned int content; }; extern struct ChanStruct CHPOOL_LOC[num_chan]; unsigned int get_chan_content(unsigned int chan_index) { return CHPOOL_LOC[chan_index].content; }
Definition get_chan_content_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) content tint))).
Definition f_get_chan_content := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: nil);
fn_temps := nil;
fn_body := get_chan_content_body
|}.
#define num_chan 64 struct ChanStruct { unsigned int isbusy; unsigned int content; }; extern struct ChanStruct CHPOOL_LOC[num_chan]; void set_chan_content(unsigned int chan_index, unsigned int content) { CHPOOL_LOC[chan_index].content = content; }
Local Open Scope positive_scope.
Let tcontent: ident := 3.
Local Open Scope Z_scope.
Definition set_chan_content_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) content tint) (Etempvar tcontent tint)).
Definition f_set_chan_content := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: (tcontent, tint) :: nil);
fn_temps := nil;
fn_body := set_chan_content_body
|}.
Let tcontent: ident := 3.
Local Open Scope Z_scope.
Definition set_chan_content_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) content tint) (Etempvar tcontent tint)).
Definition f_set_chan_content := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: (tcontent, tint) :: nil);
fn_temps := nil;
fn_body := set_chan_content_body
|}.
#define num_chan 64 struct ChanStruct { unsigned int isbusy; unsigned int content; }; extern struct ChanStruct CHPOOL_LOC[num_chan]; void init_chan(unsigned int chan_index, unsigned int info, unsigned int content) { CHPOOL_LOC[chan_index].isbusy = info; CHPOOL_LOC[chan_index].content = content; }
Definition init_chan_body : statement :=
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) isbusy tint) (Etempvar tinfo tint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar CHPOOL_LOC (tarray t_struct_Chan num_chan))
(Etempvar tchan_index tint) (tptr t_struct_Chan))
t_struct_Chan) content tint) (Etempvar tcontent tint))).
Definition f_init_chan := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tchan_index, tint) :: (tinfo, tint) :: (tcontent, tint) :: nil);
fn_temps := nil;
fn_body := init_chan_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; void init_sync_chan(unsigned int cid) { SYNCCHPOOL_LOC[cid].to = num_proc; SYNCCHPOOL_LOC[cid].vaddr = 0; SYNCCHPOOL_LOC[cid].count = 0; }
Let tchanid := 4%positive.
Definition init_sync_chan_body : statement :=
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) to tint) (Econst_int (Int.repr num_chan) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) paddr tint) (Econst_int (Int.repr 0) tint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) count tint) (Econst_int (Int.repr 0) tint)))).
Definition f_init_sync_chan := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := init_sync_chan_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; void set_sync_chan_to(unsigned int tchanid, unsigned int toval) { SYNCCHPOOL_LOC[tchanid].to = toval; }
Let toval := 5%positive.
Definition set_sync_chan_to_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) to tint) (Etempvar toval tint)).
Definition f_set_sync_chan_to := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: (toval, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_sync_chan_to_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; unsigned int get_sync_chan_to(unsigned int tchanid) { return SYNCCHPOOL_LOC[tchanid].to; }
Definition get_sync_chan_to_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) to tint))).
Definition f_get_sync_chan_to := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := get_sync_chan_to_body
|}.
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) to tint))).
Definition f_get_sync_chan_to := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := get_sync_chan_to_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int paddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; void set_sync_chan_paddr(unsigned int tchanid, unsigned int paddrval) { SYNCCHPOOL_LOC[tchanid].paddr = paddrval; }
Let paddrval := 6%positive.
Definition set_sync_chan_paddr_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) paddr tint) (Etempvar paddrval tint)).
Definition f_set_sync_chan_paddr := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: (paddrval, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_sync_chan_paddr_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int paddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; unsigned int get_sync_chan_paddr(unsigned int tchanid) { return SYNCCHPOOL_LOC[tchanid].paddr; }
Definition get_sync_chan_paddr_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) paddr tint))).
Definition f_get_sync_chan_paddr := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := get_sync_chan_paddr_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; unsigned int is_pid_sending_to(unsigned int tchanid, unsigned int to) { return SYNCCHPOOL_LOC[tchanid].to == to; }
Definition is_pid_sending_to_body : statement :=
(Sreturn (Some (Ebinop Oeq
(Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) to tint) (Etempvar to tint)
tint))).
Definition f_is_pid_sending_to := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: (to, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := is_pid_sending_to_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; unsigned int get_sync_chan_count(unsigned int tchanid) { return SYNCCHPOOL_LOC[tchanid].count; }
Definition get_sync_chan_count_body :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd
(Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) count tint))).
Definition f_get_sync_chan_count := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := get_sync_chan_count_body
|}.
#define num_proc 64 struct SyncIPCChan { unsigned int to; unsigned int vaddr; // Sender's virtual address of the send buffer unsigned int count; }; extern struct SyncIPCChan SYNCCHPOOL_LOC[num_proc]; void set_sync_chan_count(unsigned int tchanid, unsigned int countval) { SYNCCHPOOL_LOC[tchanid].count = countval; }
Let countval := 7%positive.
Definition set_sync_chan_count_body : statement :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar SYNCCHPOOL_LOC (tarray t_struct_SyncIPCChan num_chan))
(Etempvar tchanid tint) (tptr t_struct_SyncIPCChan))
t_struct_SyncIPCChan) count tint) (Etempvar countval tint)).
Definition f_set_sync_chan_count := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tchanid, tint) :: (countval, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_sync_chan_count_body
|}.
#define PAGESIZE 4096 extern unsigned int pt_read(unsigned int pid, unsigned int vaddr); unsigned int get_kernel_pa(unsigned int pid, unsigned int va) { unsigned int kpa = pt_read(pid, va); kpa = kpa / PAGESIZE * PAGESIZE + va % PAGESIZE; return kpa; }
Local Open Scope positive_scope.
Definition _pid : ident := 8.
Definition _kpa : ident := 30.
Definition _va : ident := 31.
Definition get_kernel_pa_body : statement :=
(Ssequence
(Scall (Some _kpa)
(Evar pt_read (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint
cc_default))
((Etempvar _pid tuint) :: (Etempvar _va tuint) :: nil))
(Ssequence
(Sset _kpa
(Ebinop Oadd
(Ebinop Omul
(Ebinop Odiv (Etempvar _kpa tuint)
(Econst_int (Int.repr 4096) tint) tuint)
(Econst_int (Int.repr 4096) tint) tuint)
(Ebinop Omod (Etempvar _va tuint) (Econst_int (Int.repr 4096) tint)
tuint) tuint))
(Sreturn (Some (Etempvar _kpa tuint)))))
.
Definition f_get_kernel_pa := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_pid, tint) :: (_va, tint) :: nil);
fn_vars := nil;
fn_temps := ((_kpa, tint) :: nil);
fn_body := get_kernel_pa_body
|}.