Library mcertikos.mm.DAbsHandlerCSource
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Definition _id : ident := 1%positive.
Definition _p : ident := 2%positive.
Definition _i : ident := 3%positive.
Definition _mbi : ident := 4%positive.
Definition _n : ident := 5%positive.
Definition t_i : ident := 6%positive.
Definition _child : ident := 7%positive.
Definition t_u : ident := 8%positive.
Definition t_q : ident := 9%positive.
void container_init(unsigned int mbi_addr)
{
preinit(mbi_addr);
container_LOC[0].quota = (VM_USERHI - VM_USERLO) / PAGESIZE;
container_LOC[0].usage = 0;
container_LOC[0].parent = 0;
container_LOC[0].nchildren = 0;
container_LOC[0].used = 1;
}
Definition container_init_body :=
(Ssequence
(Scall None (Evar boot_loader (Tfunction (Tcons tint Tnil) tvoid cc_default))
((Etempvar _mbi tint) :: nil))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Econst_int (Int.repr 0) tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint)
(Econst_int (Int.repr root_quota) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Econst_int (Int.repr 0) tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Econst_int (Int.repr 0) tint)
(tptr t_struct_AC)) t_struct_AC)
AC_parent tint) (Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Econst_int (Int.repr 0) tint)
(tptr t_struct_AC)) t_struct_AC)
AC_nchildren tint) (Econst_int (Int.repr 0) tint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Econst_int (Int.repr 0) tint)
(tptr t_struct_AC)) t_struct_AC)
AC_used tint) (Econst_int (Int.repr 1) tint))))))).
Definition f_container_init :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_mbi, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_init_body
|}.
unsigned int container_get_parent(unsigned int id)
{
return container_LOC[id].parent;
}
Definition container_get_parent_body :=
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_parent tint))).
Definition f_container_get_parent :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_parent_body
|}.
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_parent tint))).
Definition f_container_get_parent :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_parent_body
|}.
unsigned int container_get_quota(unsigned int id)
{
return container_LOC[id].quota;
}
Definition container_get_quota_body :=
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint))).
Definition f_container_get_quota :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_quota_body
|}.
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint))).
Definition f_container_get_quota :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_quota_body
|}.
unsigned int container_get_usage(unsigned int id)
{
return container_LOC[id].usage;
}
Definition container_get_usage_body :=
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint))).
Definition f_container_get_usage :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_usage_body
|}.
(Sreturn (Some (Efield
(Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint))).
Definition f_container_get_usage :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_usage_body
|}.
unsigned int container_can_consume(unsigned int id, unsigned int n)
{
if (container_LOC[id].usage + n > container_LOC[id].quota) return 0;
return 1;
}
Definition container_can_consume_body :=
(Ssequence
(Sifthenelse (Ebinop Ole (Etempvar _n tint)
(Efield (Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint) tint)
(Sifthenelse (Ebinop Ole
(Efield (Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Ebinop Osub
(Efield (Ederef (Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint)
(Etempvar _n tint) tint) tint)
(Sreturn (Some (Econst_int (Int.repr 1) tint)))
Sskip)
Sskip)
(Sreturn (Some (Econst_int (Int.repr 0) tint)))).
Definition f_container_can_consume :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: (_n, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_can_consume_body
|}.
unsigned int container_split(unsigned int id, unsigned int quota, unsigned int child)
{
container_LOC[child].used = 1;
container_LOC[child].quota = quota;
container_LOC[child].usage = 0;
container_LOC[child].parent = id;
container_LOC[child].nchildren = 0;
container_LOC[id].usage += quota;
container_LOC[id].nchildren++;
return child;
}
Definition container_split_body :=
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _child tint) (tptr t_struct_AC))
t_struct_AC) AC_used tint)
(Econst_int (Int.repr 1) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _child tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint)
(Etempvar _n tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _child tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _child tint) (tptr t_struct_AC))
t_struct_AC) AC_parent tint)
(Etempvar _id tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _child tint)
(tptr t_struct_AC))
t_struct_AC) AC_nchildren tint)
(Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint)
(tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint)
(tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Etempvar _n tint) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint)
(tptr t_struct_AC))
t_struct_AC) AC_nchildren tint)
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint)
(tptr t_struct_AC))
t_struct_AC) AC_nchildren tint)
(Econst_int (Int.repr 1) tint) tint))
(Sreturn (Some (Etempvar _child tint)))))))))).
Definition f_container_split :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: (_n, tint) :: (_child, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_split_body
|}.
unsigned int container_alloc(unsigned int id)
{
unsigned int u, q;
u = container_LOC[id].usage;
q = container_LOC[id].quota;
if (u == q) return 0;
container_LOC[id].usage = u+1;
return 1;
}
Definition container_alloc_body :=
Ssequence
(Sset t_u
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint))
(Ssequence
(Sset t_q
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_quota tint))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar t_u tint) (Etempvar t_q tint) tint)
(Sreturn (Some (Econst_int (Int.repr 0) tint)))
Sskip)
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tint) (tptr t_struct_AC))
t_struct_AC) AC_usage tint)
(Ebinop Oadd (Etempvar t_u tint) (Econst_int (Int.repr 1) tint)
tint))
(Sreturn (Some (Econst_int (Int.repr 1) tint)))))).
Definition f_container_alloc :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := ((t_u, tint) :: (t_q, tint) :: nil);
fn_body := container_alloc_body
|}.