Library mcertikos.mm.DAbsHandlerCSource
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 GlobalOracle.
Definition _id : ident := 1%positive.
Definition _usage_val : ident := 12%positive.
Definition _cur_num : ident := 13%positive.
Definition _next_child : ident := 14%positive.
Definition _q_val : ident := 15%positive.
Definition _p_val : ident := 16%positive.
Definition container_set_usage_body :=
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC)) t_struct_AC)
AC_usage tuint) (Etempvar _usage_val tuint)).
Definition f_container_set_usage := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_id, tuint) :: (_usage_val, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_set_usage_body
|}.
Definition container_set_nchildren_body :=
(Ssequence
(Sset _cur_num
(Efield
(Ederef
(Ebinop Oadd (Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_nchildren tuint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_nchildren tuint)
(Ebinop Oadd (Etempvar _cur_num tuint) (Econst_int (Int.repr 1) tint)
tuint))).
Definition f_container_set_nchildren := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_id, tuint) :: (_next_child, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_cur_num, tuint) :: nil);
fn_body := container_set_nchildren_body
|}.
Definition container_set_values_body :=
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd (Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_quota tuint) (Etempvar _q_val tuint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_usage tuint) (Econst_int (Int.repr 0) tint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_parent tuint) (Etempvar _p_val tuint))
(Ssequence
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_nchildren tuint)
(Econst_int (Int.repr 0) tint))
(Sassign
(Efield
(Ederef
(Ebinop Oadd
(Evar AC_LOC (gvar_info container_loc_type))
(Etempvar _id tuint) (tptr t_struct_AC))
t_struct_AC) AC_used tuint)
(Econst_int (Int.repr 1) tint)))))).
Definition f_container_set_values := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_id, tuint) :: (_q_val, tuint) :: (_p_val, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_set_values_body
|}.
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
|}.
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_get_nchildren(unsigned int id)
{
return container_LOC[id].nchildren;
}
Definition container_get_nchildren_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_nchildren tint))).
Definition f_container_get_nchildren :=
{|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_id, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_get_nchildren_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 _n : ident := 20%positive.
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
|}.
Definition t_u : ident := 25%positive.
Definition t_q : ident := 26%positive.
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
|}.