Library mcertikos.proc.VEPTOpCSource

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


Definition tgpa : ident := 34%positive.
Definition tentry : ident := 35%positive.
Definition tresult : ident := 36%positive.

Definition ept_gpa_to_hpa_body : statement :=
(Ssequence
  (Scall (Some tentry)
    (Evar ept_get_page_entry (Tfunction (Tcons tuint Tnil) tuint
                                  cc_default))
    ((Etempvar tgpa tuint) :: nil))
  (Ssequence
    (Sifthenelse (Ebinop Oeq
                   (Ebinop Oand (Etempvar tentry tuint)
                     (Econst_int (Int.repr 7) tint) tuint)
                   (Econst_int (Int.repr 0) tint) tint)
      (Sset tresult (Econst_int (Int.repr 0) tint))
      (Sset tresult
        (Ebinop Oor
          (Ebinop Oand (Etempvar tentry tuint)
            (Econst_int (Int.repr 4294963200) tuint) tuint)
          (Ebinop Oand (Etempvar tgpa tuint)
            (Econst_int (Int.repr 4095) tint) tuint) tuint)))
    (Sreturn (Some (Etempvar tresult tuint))))).

Definition f_ept_gpa_to_hpa := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := ((tgpa, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((tentry, tuint) :: (tresult, tuint) :: nil);
  fn_body := ept_gpa_to_hpa_body
|}.


Definition thpa : ident := 37%positive.
Definition tmemtype : ident := 38%positive.
Definition tpg_entry : ident := 39%positive.

Definition ept_mmap_body : statement :=
(Ssequence
  (Scall (Some tpg_entry)
    (Evar ept_get_page_entry (Tfunction (Tcons tuint Tnil) tuint
                                cc_default))
    ((Etempvar tgpa tuint) :: nil))
  (Ssequence
    (Sifthenelse (Ebinop Oeq
                   (Ebinop Oand (Etempvar tpg_entry tuint)
                     (Econst_int (Int.repr 7) tint) tuint)
                   (Econst_int (Int.repr 0) tint) tint)
        (Scall (Some tresult)
          (Evar ept_add_mapping (Tfunction
                                   (Tcons tuint
                                     (Tcons tuint (Tcons tuint Tnil))) tuint
                                   cc_default))
          ((Etempvar tgpa tuint) :: (Etempvar thpa tuint) ::
           (Etempvar tmemtype tuint) :: nil))
      (Sset tresult (Econst_int (Int.repr 1) tint)))
    (Sreturn (Some (Etempvar tresult tuint))))).

Definition f_ept_mmap := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := ((tgpa, tuint) :: (thpa, tuint) :: (tmemtype, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((tpg_entry, tuint) :: (tresult, tuint) :: nil);
  fn_body := ept_mmap_body
|}.


Definition tperm : ident := 40%positive.

Definition ept_set_permission_body : statement :=
(Ssequence
  (Scall (Some tentry)
      (Evar ept_get_page_entry (Tfunction (Tcons tuint Tnil) tuint
                                  cc_default))
      ((Etempvar tgpa tuint) :: nil))
    (Scall None
      (Evar ept_set_page_entry (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                  tvoid cc_default))
      ((Etempvar tgpa tuint) ::
       (Ebinop Oor
         (Ebinop Oand (Etempvar tentry tuint)
           (Econst_int (Int.repr 4294967288) tuint) tuint)
         (Ebinop Oand (Etempvar tperm tuint) (Econst_int (Int.repr 7) tint)
           tuint) tuint) :: nil))).

Definition f_ept_set_permission := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((tgpa, tuint) :: (tperm, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((tentry, tuint) :: nil);
  fn_body := ept_set_permission_body
|}.