Library mcertikos.virt.intel.VEPTInitCSource

***********************************************************************
*                                                                     *
*            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.


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

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

Definition v_vmcs := {|
                      gvar_info := t_struct_vmcsStruct;
                      gvar_init := Init_int32 Int.zero :: Init_int32 Int.zero ::
                                   Init_space ((C_VMCS_HOST_RIP + 2) × 4) :: nil;
                      gvar_readonly := false;
                      gvar_volatile := false
                    |}.

Definition vmcs_get_revid_body := (Sreturn (Some (Efield (Evar VMCS_LOC t_struct_vmcsStruct) revid tint))).

Definition f_vmcs_get_revid := {|
                                fn_return := tint;
                                fn_callconv := cc_default;
                                fn_params := nil;
                                fn_vars := nil;
                                fn_temps := nil;
                                fn_body := vmcs_get_revid_body
                              |}.


Notation tid := 1 % positive.

Definition vmcs_set_revid_body :=
  (Sassign
     (Efield (Evar VMCS_LOC t_struct_vmcsStruct) revid tint)
     (Etempvar tid tint)
  ).

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


Definition vmcs_get_abrtid_body := (Sreturn (Some (Efield (Evar VMCS_LOC t_struct_vmcsStruct) abort_code tint))).

Definition f_vmcs_get_abrtid := {|
                                 fn_return := tint;
                                 fn_callconv := cc_default;
                                 fn_params := nil;
                                 fn_vars := nil;
                                 fn_temps := nil;
                                 fn_body := vmcs_get_abrtid_body
                               |}.


Notation tcode := 2 % positive.

Definition vmcs_set_abrtid_body := (Sassign (Efield (Evar VMCS_LOC t_struct_vmcsStruct) abort_code tint)
                                            (Etempvar tcode tint)).

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