Library mcertikos.clib.CDataTypes
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Events.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
Require Import Cop.
Require Import ZArith.Zwf.
Require Export GlobIdent.
Require Export Constant.
Require Import AuxStateDataType.
Require Import GlobalOracle.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Events.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
Require Import Cop.
Require Import ZArith.Zwf.
Require Export GlobIdent.
Require Export Constant.
Require Import AuxStateDataType.
Require Import GlobalOracle.
Notation tchar := (Tint I8 Unsigned noattr).
Notation tuchar := tchar.
Notation tint := (Tint I32 Unsigned noattr).
Notation tbool := (Tint IBool Unsigned noattr).
Notation tuint := tint.
Notation tulong := (Tlong Unsigned noattr).
Notation tptr := (fun ty ⇒ Tpointer ty noattr).
Notation tarray := (fun ty size ⇒ Tarray ty size noattr).
Notation tvoid := (Tvoid).
Definition exec_stmt `{compiler_config_ops: CompilerConfigOps} `{writable_block_ops: WritableBlockOps} ge :=
ClightBigstep.exec_stmt ge (fun _ ⇒ function_entry2).
Lemma tcharsize: sizeof tchar = 1.
Proof. trivial. Qed.
Lemma tintsize: sizeof tint = 4.
Proof. trivial. Qed.
Lemma tptrsize: ∀ ty, sizeof (tptr ty) = 4.
Proof. intros. trivial. Qed.
Definition v_serial_exists := {|
gvar_info := tuint;
gvar_init := (Init_int32 (Int.repr 0) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition v_curr_intr_num := {|
gvar_info := tuint;
gvar_init := (Init_int32 (Int.repr 0) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
gvar_info := tuint;
gvar_init := (Init_int32 (Int.repr 0) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition v_curr_intr_num := {|
gvar_info := tuint;
gvar_init := (Init_int32 (Int.repr 0) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation PDXPERM := 7.
Notation S := Datatypes.S.
Notation STACK_TOP:= (Int.repr (kern_high × PgSize)).
Lemma adr_high_val: adr_high = 4026531840.
Proof. reflexivity. Qed.
Lemma adr_low_val: adr_low = 1073741824.
Proof. reflexivity. Qed.
Lemma adr_max_val: adr_max = 4294967296.
Proof. reflexivity. Qed.
Lemma one_k_val: one_k = 1024.
Proof. compute. trivial. Qed.
Lemma one_k_minus1: PDX Int.max_unsigned = one_k - 1.
Proof. compute; trivial. Qed.
Lemma one_k_plus1: PDX Int.max_unsigned + 2 = one_k + 1.
Proof. compute; trivial. Qed.
Lemma one_k_minus1´: PTX Int.max_unsigned = one_k - 1.
Proof. compute. trivial. Qed.
Lemma valid_addr: 0 < kern_low < kern_high ∧ kern_low < maxpage.
Proof. omega. Qed.
Lemma valid_n_proc: num_proc > 0.
Proof. omega. Qed.
Lemma valid_pgs: PgSize > 260.
Proof. omega. Qed.
Lemma div_pgs: (4 | PgSize).
Proof.
unfold Z.divide.
∃ 1024.
compute.
trivial.
Qed.
Lemma HPS: PgSize > 0.
Proof. omega. Qed.
Lemma Hmax: maxpage × 8 + 4 < Int.max_unsigned.
Proof.
vm_compute; reflexivity.
Qed.
Lemma HPS4: PgSize ≥ 4.
Proof. omega. Qed.
Lemma Hnpc: num_proc > 0.
Proof. omega. Qed.
Lemma Hlow: (PgSize × one_k | kern_low × PgSize).
Proof.
unfold Z.divide.
∃ (kern_low / one_k).
compute.
trivial.
Qed.
Lemma Hhigh: (PgSize × one_k | kern_high × PgSize).
Proof.
unfold Z.divide.
∃ (kern_high / one_k).
compute.
trivial.
Qed.
Lemma Hnchan: num_chan > 0.
Proof. omega. Qed.
Local Open Scope positive.
Definition flatmem_loc_type : globvar type :=
{|
gvar_info := (tarray tchar adr_max);
gvar_init := ((Init_space adr_max)::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation AC := 500.
Notation AC_quota := 510.
Notation AC_usage := 520.
Notation AC_parent := 530.
Notation AC_nchildren := 540.
Notation AC_used := 550.
Notation t_struct_AC :=
(Tstruct AC
(Fcons AC_quota tint
(Fcons AC_usage tint
(Fcons AC_parent tint
(Fcons AC_nchildren tint (Fcons AC_used tint Fnil))))) noattr).
Fact sizeof_AC : sizeof t_struct_AC = 20%Z.
Proof. auto. Qed.
Definition container_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_AC num_proc);
gvar_init := (Init_space (num_proc × 20) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition nps_loc_type : globvar type :=
{|
gvar_info := tint;
gvar_init := (Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation A := 1000. Notation A_isnorm_ident := 1100. Notation A_allocated_ident := 1200. Notation t_struct_A := (Tstruct A (Fcons A_isnorm_ident tint (Fcons A_allocated_ident tint Fnil)) noattr).
Definition at_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_A maxpage);
gvar_init := ((Init_space (maxpage*8))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition atc_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_A maxpage);
gvar_init := ((Init_space (maxpage*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition ptp_loc_type : globvar type :=
{|
gvar_info := (tarray tint num_proc);
gvar_init := ((Init_space (num_proc*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition ptpool_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray (tptr tchar) 1024%Z) num_proc%Z);
gvar_init := ((Init_space (num_proc×PgSize))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition idpmap_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray tint 1024%Z) 1024%Z);
gvar_init := ((Init_space (1024%Z×PgSize))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation KCtxtStruct := 1600.
Notation ESP := 1700.
Notation EDI := 1800.
Notation ESI := 1900.
Notation EBX := 2000.
Notation EBP := 2100.
Notation RA := 2200.
Notation t_struct_KCtxt := (Tstruct KCtxtStruct
(Fcons ESP (tptr tvoid)
(Fcons EDI (tptr tvoid)
(Fcons ESI (tptr tvoid)
(Fcons EBX (tptr tvoid)
(Fcons EBP (tptr tvoid)
(Fcons RA (tptr tvoid) Fnil)))))) noattr).
Definition kctxtpool_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_KCtxt num_proc);
gvar_init := ((Init_space (num_proc*24))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation struct_TCB := 7000.
Notation TCB_pool := 7100.
Notation struct_TCB_node := 7200.
Notation state := 7300.
Notation cpu_id := 7400.
Notation prev := 7500.
Notation next := 7600.
Notation TDQ_pool := 7700.
Notation struct_TDQ_node := 7800.
Notation head := 7900.
Notation tail := 8000.
Definition t_struct_TCB :=
(Tstruct struct_TCB
(Fcons TCB_pool
(tarray (Tstruct struct_TCB_node
(Fcons state tuint
(Fcons cpu_id tuint
(Fcons prev tuint (Fcons next tuint Fnil)))) noattr) num_proc)
(Fcons TDQ_pool
(tarray (Tstruct struct_TDQ_node
(Fcons head tuint (Fcons tail tuint Fnil)) noattr) num_chan)
Fnil)) noattr).
Definition t_struct_TCB_node :=
(Tstruct struct_TCB_node
(Fcons state tuint
(Fcons cpu_id tuint (Fcons prev tuint (Fcons next tuint Fnil))))
noattr).
Definition t_struct_TDQ_node :=
(Tstruct struct_TDQ_node (Fcons head tuint (Fcons tail tuint Fnil))
noattr).
Definition tcbpool_loc_type :=
{|
gvar_info := t_struct_TCB;
gvar_init := Init_space (num_proc × 16 + num_chan × 8) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
Definition curid_loc_type : globvar type :=
{|
gvar_info := tarray tuint TOTAL_CPU;
gvar_init := Init_space (TOTAL_CPU × 4) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
Lemma t_struct_TCB_node_size: sizeof t_struct_TCB_node = 16%Z.
Proof. reflexivity. Qed.
Lemma t_struct_TDQ_node_size: sizeof t_struct_TDQ_node = 8%Z.
Proof. reflexivity. Qed.
Notation ChanStruct := 3100.
Notation isbusy := 3200.
Notation content := 3300.
Notation t_struct_Chan := (Tstruct ChanStruct
(Fcons isbusy tint (Fcons content tint Fnil)) noattr).
Definition chpool_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_Chan num_proc);
gvar_init := ((Init_space (num_chan*8))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition uctx_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray tint UCTXT_SIZE) num_proc);
gvar_init := ((Init_space (num_proc×UCTXT_SIZE*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation cons_buf := 4100.
Notation buffer := 4200.
Notation rpos := 4300.
Notation wpos := 4400.
Notation t_struct_cons_buf :=
(Tstruct cons_buf
(Fcons buffer (tarray tuint CONSOLE_BUFFER_SIZE)
(Fcons rpos tuint
(Fcons wpos tuint Fnil)))
noattr).
Definition cons_buf_loc_type := {|
gvar_info := t_struct_cons_buf;
gvar_init := (Init_space (CONSOLE_BUFFER_SIZE*4) :: Init_int32 Int.zero :: Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation kbd_buf := 5100.
Notation kbd_buffer := 5200.
Notation kbd_rpos := 5300.
Notation kbd_wpos := 5400.
Notation t_struct_kbd_buf :=
(Tstruct kbd_buf
(Fcons kbd_buffer (tarray tuint KEYBOARD_SW_BUF_SIZE)
(Fcons kbd_rpos tuint
(Fcons kbd_wpos tuint Fnil)))
noattr).
Definition kbd_buf_loc_type := {|
gvar_info := t_struct_kbd_buf;
gvar_init := (Init_space (KEYBOARD_SW_BUF_SIZE*4) :: Init_int32 Int.zero :: Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition sleeper_loc_type : globvar type :=
{|
gvar_info := (tarray tuint num_proc);
gvar_init := (Init_space (TOTAL_CPU × 4) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation _node_pool := 6100.
Notation _tail := 6200.
Notation _next := 6300.
Notation _busy := 6400.
Notation _lock_padding := 6500.
Notation _node_padding := 6600.
Notation mcs_lock := 6700.
Notation mcs_node := 6800.
Notation t_struct_mcs_lock :=
(Tstruct mcs_lock
(Fcons _tail tuint
(Fcons _lock_padding (tarray tuint 15%Z)
(Fcons _node_pool
(tarray (Tstruct mcs_node
(Fcons _next tuint
(Fcons _busy tuint
(Fcons _node_padding (tarray tuint 14%Z) Fnil)))
noattr) TOTAL_CPU) Fnil))) noattr).
Notation t_struct_mcs_node :=
(Tstruct mcs_node
(Fcons _next tuint
(Fcons _busy tuint (Fcons _node_padding (tarray tuint 14%Z) Fnil)))
noattr).
Definition mcslock_loc_type :=
{|
gvar_info := (tarray t_struct_mcs_lock lock_range);
gvar_init := (Init_space (((TOTAL_CPU × (2 + 14) + (15 + 1)) × 4) × lock_range) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition flatmem_loc_type : globvar type :=
{|
gvar_info := (tarray tchar adr_max);
gvar_init := ((Init_space adr_max)::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation AC := 500.
Notation AC_quota := 510.
Notation AC_usage := 520.
Notation AC_parent := 530.
Notation AC_nchildren := 540.
Notation AC_used := 550.
Notation t_struct_AC :=
(Tstruct AC
(Fcons AC_quota tint
(Fcons AC_usage tint
(Fcons AC_parent tint
(Fcons AC_nchildren tint (Fcons AC_used tint Fnil))))) noattr).
Fact sizeof_AC : sizeof t_struct_AC = 20%Z.
Proof. auto. Qed.
Definition container_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_AC num_proc);
gvar_init := (Init_space (num_proc × 20) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition nps_loc_type : globvar type :=
{|
gvar_info := tint;
gvar_init := (Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation A := 1000. Notation A_isnorm_ident := 1100. Notation A_allocated_ident := 1200. Notation t_struct_A := (Tstruct A (Fcons A_isnorm_ident tint (Fcons A_allocated_ident tint Fnil)) noattr).
Definition at_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_A maxpage);
gvar_init := ((Init_space (maxpage*8))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition atc_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_A maxpage);
gvar_init := ((Init_space (maxpage*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition ptp_loc_type : globvar type :=
{|
gvar_info := (tarray tint num_proc);
gvar_init := ((Init_space (num_proc*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition ptpool_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray (tptr tchar) 1024%Z) num_proc%Z);
gvar_init := ((Init_space (num_proc×PgSize))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition idpmap_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray tint 1024%Z) 1024%Z);
gvar_init := ((Init_space (1024%Z×PgSize))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation KCtxtStruct := 1600.
Notation ESP := 1700.
Notation EDI := 1800.
Notation ESI := 1900.
Notation EBX := 2000.
Notation EBP := 2100.
Notation RA := 2200.
Notation t_struct_KCtxt := (Tstruct KCtxtStruct
(Fcons ESP (tptr tvoid)
(Fcons EDI (tptr tvoid)
(Fcons ESI (tptr tvoid)
(Fcons EBX (tptr tvoid)
(Fcons EBP (tptr tvoid)
(Fcons RA (tptr tvoid) Fnil)))))) noattr).
Definition kctxtpool_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_KCtxt num_proc);
gvar_init := ((Init_space (num_proc*24))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation struct_TCB := 7000.
Notation TCB_pool := 7100.
Notation struct_TCB_node := 7200.
Notation state := 7300.
Notation cpu_id := 7400.
Notation prev := 7500.
Notation next := 7600.
Notation TDQ_pool := 7700.
Notation struct_TDQ_node := 7800.
Notation head := 7900.
Notation tail := 8000.
Definition t_struct_TCB :=
(Tstruct struct_TCB
(Fcons TCB_pool
(tarray (Tstruct struct_TCB_node
(Fcons state tuint
(Fcons cpu_id tuint
(Fcons prev tuint (Fcons next tuint Fnil)))) noattr) num_proc)
(Fcons TDQ_pool
(tarray (Tstruct struct_TDQ_node
(Fcons head tuint (Fcons tail tuint Fnil)) noattr) num_chan)
Fnil)) noattr).
Definition t_struct_TCB_node :=
(Tstruct struct_TCB_node
(Fcons state tuint
(Fcons cpu_id tuint (Fcons prev tuint (Fcons next tuint Fnil))))
noattr).
Definition t_struct_TDQ_node :=
(Tstruct struct_TDQ_node (Fcons head tuint (Fcons tail tuint Fnil))
noattr).
Definition tcbpool_loc_type :=
{|
gvar_info := t_struct_TCB;
gvar_init := Init_space (num_proc × 16 + num_chan × 8) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
Definition curid_loc_type : globvar type :=
{|
gvar_info := tarray tuint TOTAL_CPU;
gvar_init := Init_space (TOTAL_CPU × 4) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
Lemma t_struct_TCB_node_size: sizeof t_struct_TCB_node = 16%Z.
Proof. reflexivity. Qed.
Lemma t_struct_TDQ_node_size: sizeof t_struct_TDQ_node = 8%Z.
Proof. reflexivity. Qed.
Notation ChanStruct := 3100.
Notation isbusy := 3200.
Notation content := 3300.
Notation t_struct_Chan := (Tstruct ChanStruct
(Fcons isbusy tint (Fcons content tint Fnil)) noattr).
Definition chpool_loc_type : globvar type :=
{|
gvar_info := (tarray t_struct_Chan num_proc);
gvar_init := ((Init_space (num_chan*8))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition uctx_loc_type : globvar type :=
{|
gvar_info := (tarray (tarray tint UCTXT_SIZE) num_proc);
gvar_init := ((Init_space (num_proc×UCTXT_SIZE*4))::nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation cons_buf := 4100.
Notation buffer := 4200.
Notation rpos := 4300.
Notation wpos := 4400.
Notation t_struct_cons_buf :=
(Tstruct cons_buf
(Fcons buffer (tarray tuint CONSOLE_BUFFER_SIZE)
(Fcons rpos tuint
(Fcons wpos tuint Fnil)))
noattr).
Definition cons_buf_loc_type := {|
gvar_info := t_struct_cons_buf;
gvar_init := (Init_space (CONSOLE_BUFFER_SIZE*4) :: Init_int32 Int.zero :: Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation kbd_buf := 5100.
Notation kbd_buffer := 5200.
Notation kbd_rpos := 5300.
Notation kbd_wpos := 5400.
Notation t_struct_kbd_buf :=
(Tstruct kbd_buf
(Fcons kbd_buffer (tarray tuint KEYBOARD_SW_BUF_SIZE)
(Fcons kbd_rpos tuint
(Fcons kbd_wpos tuint Fnil)))
noattr).
Definition kbd_buf_loc_type := {|
gvar_info := t_struct_kbd_buf;
gvar_init := (Init_space (KEYBOARD_SW_BUF_SIZE*4) :: Init_int32 Int.zero :: Init_int32 Int.zero :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition sleeper_loc_type : globvar type :=
{|
gvar_info := (tarray tuint num_proc);
gvar_init := (Init_space (TOTAL_CPU × 4) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Notation _node_pool := 6100.
Notation _tail := 6200.
Notation _next := 6300.
Notation _busy := 6400.
Notation _lock_padding := 6500.
Notation _node_padding := 6600.
Notation mcs_lock := 6700.
Notation mcs_node := 6800.
Notation t_struct_mcs_lock :=
(Tstruct mcs_lock
(Fcons _tail tuint
(Fcons _lock_padding (tarray tuint 15%Z)
(Fcons _node_pool
(tarray (Tstruct mcs_node
(Fcons _next tuint
(Fcons _busy tuint
(Fcons _node_padding (tarray tuint 14%Z) Fnil)))
noattr) TOTAL_CPU) Fnil))) noattr).
Notation t_struct_mcs_node :=
(Tstruct mcs_node
(Fcons _next tuint
(Fcons _busy tuint (Fcons _node_padding (tarray tuint 14%Z) Fnil)))
noattr).
Definition mcslock_loc_type :=
{|
gvar_info := (tarray t_struct_mcs_lock lock_range);
gvar_init := (Init_space (((TOTAL_CPU × (2 + 14) + (15 + 1)) × 4) × lock_range) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Open Local Scope Z.
Lemma t_struct_mcs_node_size : sizeof t_struct_mcs_node = 64. Proof. reflexivity. Qed.
Lemma t_struct_mcs_lock_size : sizeof t_struct_mcs_lock = 576. Proof. reflexivity. Qed.
Lemma t_struct_KCtxt_size: sizeof t_struct_KCtxt = 24.
Proof. reflexivity. Qed.
Lemma ptr_size: ∀ t, sizeof (tptr t) = 4.
Proof. intro. reflexivity. Qed.
Lemma tvoid_size: sizeof tvoid = 1.
Proof. reflexivity. Qed.
Lemma t_struct_Chan_size: sizeof t_struct_Chan = 8.
Proof. reflexivity. Qed.