Library mcertikos.mm.MContainerIntroCSource
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 _mbi_addr : ident := 1%positive.
Definition container_init_body :=
(Ssequence
(Scall None
(Evar ticket_lock_init (Tfunction (Tcons tuint Tnil) tvoid cc_default))
((Etempvar _mbi_addr tuint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil))) tvoid
cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 720896) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_usage (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 720896) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 1) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 2) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 3) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 4) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 5) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 6) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 7) tint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 8) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 1) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 2) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 3) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint Tnil))) tvoid
cc_default))
((Econst_int (Int.repr 4) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint Tnil))) tvoid
cc_default))
((Econst_int (Int.repr 5) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 6) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 7) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 8) tint) ::
(Ebinop Odiv (Econst_int (Int.repr 720896) tint)
(Econst_int (Int.repr 8) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil)))))))))))))))))))).
Definition f_container_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_mbi_addr, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := container_init_body
|}.
Definition _cur_usage : ident := 2%positive.
Definition _cur_quota : ident := 3%positive.
Definition _n : ident := 4%positive.
Definition _id : ident := 5%positive.
Definition _child : ident := 6%positive.
Definition _quota : ident := 7%positive.
Definition _nc : ident := 8%positive.
Definition container_split_body :=
(Ssequence
(Scall (Some _nc)
(Evar container_get_nchildren (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Etempvar _id tuint) :: nil))
(Ssequence
(Scall (Some _cur_usage)
(Evar container_get_usage (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Etempvar _id tuint) :: nil))
(Ssequence
(Sset _child
(Ebinop Oadd
(Ebinop Oadd
(Ebinop Omul (Etempvar _id tuint) (Econst_int (Int.repr 8) tint)
tuint) (Econst_int (Int.repr 1) tint) tuint)
(Etempvar _nc tuint) tuint))
(Ssequence
(Scall None
(Evar container_set_usage (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Etempvar _id tuint) ::
(Ebinop Oadd (Etempvar _cur_usage tuint) (Etempvar _quota tuint)
tuint) :: nil))
(Ssequence
(Scall None
(Evar container_set_nchildren (Tfunction
(Tcons tuint
(Tcons tuint Tnil)) tvoid
cc_default))
((Etempvar _id tuint) :: (Etempvar _child tuint) :: nil))
(Ssequence
(Scall None
(Evar container_node_init (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
((Etempvar _child tuint) :: (Etempvar _quota tuint) ::
(Etempvar _id tuint) :: nil))
(Sreturn (Some (Etempvar _child tuint))))))))).
Definition f_container_split := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_id, tuint) :: (_quota, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_child, tuint) :: (_cur_usage, tuint) :: (_nc, tuint) :: nil);
fn_body := container_split_body
|}.