Library mcertikos.proc.VEPTInitCSource

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.


Notation tcpuid := 5000 % positive.
Notation vmcsStruct := 5100 % positive.
Notation revid := 5200 % positive.
Notation abort_code := 5300 % positive.
Notation impl_specific := 5400 % positive.

Definition t_struct_vmcsStruct :=
   (Tstruct vmcsStruct
            (Fcons revid tuint
                   (Fcons abort_code tuint
                          (Fcons impl_specific (tarray tchar 4088) Fnil))) noattr).

Definition v_vmcs :=
  {|
    gvar_info := (tarray t_struct_vmcsStruct 8);
    gvar_init := Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (1022 × 4) ::
                             Init_int32 Int.zero :: Init_int32 Int.zero ::
                             Init_space (852800) :: nil;
    gvar_readonly := false;
    gvar_volatile := false
  |}.

Definition f_vmcs_get_revid_body :=
(Ssequence
   (Scall (Some tcpuid)
          (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
   (Sreturn (Some (Efield
                     (Ederef
                        (Ebinop Oadd (Evar VMCS_LOC (tarray t_struct_vmcsStruct 8))
                                (Etempvar tcpuid tuint) (tptr t_struct_vmcsStruct))
                        t_struct_vmcsStruct) revid tuint)))).

Definition f_vmcs_get_revid :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := nil;
    fn_vars := nil;
    fn_temps := ((tcpuid, tuint) :: nil);
    fn_body := f_vmcs_get_revid_body
  |}.


Notation tid := 1 % positive.

Definition f_vmcs_set_revid_body :=
(Ssequence
   (Scall (Some tcpuid)
          (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
   (Sassign
      (Efield
         (Ederef
            (Ebinop Oadd (Evar VMCS_LOC (tarray t_struct_vmcsStruct 8))
                    (Etempvar tcpuid tuint) (tptr t_struct_vmcsStruct))
            t_struct_vmcsStruct) revid tuint) (Etempvar tid tuint))).

Definition f_vmcs_set_revid :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((tid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((tcpuid, tuint) :: nil);
    fn_body := f_vmcs_set_revid_body
  |}.


Definition f_vmcs_get_abrtid_body :=
  (Ssequence
     (Scall (Some tcpuid)
            (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
     (Sreturn (Some (Efield
                       (Ederef
                          (Ebinop Oadd (Evar VMCS_LOC (tarray t_struct_vmcsStruct 8))
                                  (Etempvar tcpuid tuint) (tptr t_struct_vmcsStruct))
                          t_struct_vmcsStruct) abort_code tuint)))).

Definition f_vmcs_get_abrtid := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((tcpuid, tuint) :: nil);
  fn_body := f_vmcs_get_abrtid_body
|}.


Notation tcode := 2 % positive.

Definition f_vmcs_set_abrtid_body :=
(Ssequence
   (Scall (Some tcpuid)
          (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
   (Sassign
      (Efield
         (Ederef
            (Ebinop Oadd (Evar VMCS_LOC (tarray t_struct_vmcsStruct 8))
                    (Etempvar tcpuid tuint) (tptr t_struct_vmcsStruct))
            t_struct_vmcsStruct) abort_code tuint) (Etempvar tcode tuint))).

Definition f_vmcs_set_abrtid :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((tcode, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((tcpuid, tuint) :: nil);
    fn_body := f_vmcs_set_abrtid_body
  |}.