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 Ident.
Local Open Scope Z_scope.
Definition _Rd : ident := 999%positive.
Definition _addr := 1%positive.
Definition _alloc := 2%positive.
Definition _arg := 3%positive.
Definition _arg1 := 4%positive.
Definition _arg2 := 5%positive.
Definition _arg3 := 6%positive.
Definition _arg4 := 7%positive.
Definition _arg5 := 8%positive.
Definition _base := 9%positive.
Definition _base__1 := 10%positive.
Definition _cb_offset := 11%positive.
Definition _cbndx := 12%positive.
Definition _cnt := 13%positive.
Definition _count := 14%positive.
Definition _ctxtid := 15%positive.
Definition _cur_vcpuid := 16%positive.
Definition _cur_vmid := 17%positive.
Definition _data := 18%positive.
Definition _ec := 19%positive.
Definition _end := 20%positive.
Definition _esr := 21%positive.
Definition _esr_el2 := 22%positive.
Definition _exit_type := 23%positive.
Definition _fault_ipa := 24%positive.
Definition _gfn := 25%positive.
Definition _gpa := 26%positive.
Definition _hsr := 27%positive.
Definition _i := 28%positive.
Definition _index := 29%positive.
Definition _init_smmu_spt := 30%positive.
Definition _iova := 31%positive.
Definition _is_write := 32%positive.
Definition _kvm := 33%positive.
Definition _len := 34%positive.
Definition _level := 35%positive.
Definition _load_addr := 36%positive.
Definition _load_idx := 37%positive.
Definition _load_info_cnt := 38%positive.
Definition _main := 39%positive.
Definition _map := 40%positive.
Definition _mapped := 41%positive.
Definition _n := 42%positive.
Definition _new_ttbr := 43%positive.
Definition _next := 44%positive.
Definition _num := 45%positive.
Definition _num_context_banks := 46%positive.
Definition _offset := 47%positive.
Definition _owner := 48%positive.
Definition _p_index := 49%positive.
Definition _p_index__1 := 50%positive.
Definition _pa := 51%positive.
Definition _paddr := 52%positive.
Definition _page_count := 53%positive.
Definition _perm := 54%positive.
Definition _pfn := 55%positive.
Definition _pgd := 56%positive.
Definition _pgd_idx := 57%positive.
Definition _pgd_pa := 58%positive.
Definition _pgnum := 59%positive.
Definition _pmd := 60%positive.
Definition _pmd_idx := 61%positive.
Definition _pmd_pa := 62%positive.
Definition _power := 63%positive.
Definition _prot := 64%positive.
Definition _pte := 65%positive.
Definition _pte_idx := 66%positive.
Definition _pte_pa := 67%positive.
Definition _pud := 68%positive.
Definition _pud_idx := 69%positive.
Definition _pud_pa := 70%positive.
Definition _r_index := 71%positive.
Definition _reg := 72%positive.
Definition _remap := 73%positive.
Definition _remap_addr := 74%positive.
Definition _res := 75%positive.
Definition _ret := 76%positive.
Definition _ret64 := 77%positive.
Definition _rt := 78%positive.
Definition _size := 79%positive.
Definition _size__1 := 80%positive.
Definition _smmu_enable := 81%positive.
Definition _smmu_index := 82%positive.
Definition _start := 83%positive.
Definition _state := 84%positive.
Definition _t_vmid := 85%positive.
Definition _target := 86%positive.
Definition _target_addr := 87%positive.
Definition _target_vmid := 88%positive.
Definition _total_smmu := 89%positive.
Definition _ttbr := 90%positive.
Definition _ttbr_pa := 91%positive.
Definition _type := 92%positive.
Definition _val := 93%positive.
Definition _valid := 94%positive.
Definition _vcpu := 95%positive.
Definition _vcpu_state := 96%positive.
Definition _vcpuid := 97%positive.
Definition _vm_state := 98%positive.
Definition _vmid := 99%positive.
Definition _vttbr := 100%positive.
Definition _vttbr_pa := 101%positive.
Definition _write_val := 102%positive.
Definition _t'1 := 103%positive.
Definition _t'2 := 104%positive.
Definition _t'3 := 105%positive.
Definition _t'4 := 106%positive.
Definition host_hvc_handler_body :=
(Ssequence
(Scall None
(Evar host_to_core (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Scall None
(Evar host_hvc_dispatcher (Tfunction Tnil tint
cc_default))
nil)
(Scall None
(Evar core_to_host (Tfunction Tnil tvoid
cc_default))
nil))).
Definition f_host_hvc_handler := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := nil;
fn_body := host_hvc_handler_body
|}.
Definition host_npt_handler_body :=
(Ssequence
(Scall None
(Evar host_to_core (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Scall None
(Evar handle_host_stage2_fault (Tfunction Tnil tvoid cc_default)) nil)
(Scall None
(Evar core_to_host (Tfunction Tnil tvoid
cc_default))
nil))).
Definition f_host_npt_handler := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := nil;
fn_body := host_npt_handler_body
|}.
Definition host_vcpu_run_handler_body :=
(Ssequence
(Scall None
(Evar host_to_core (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Scall None
(Evar save_host (Tfunction Tnil tint
cc_default))
nil)
(Ssequence
(Scall None (Evar restore_vm (Tfunction Tnil tvoid cc_default)) nil)
(Scall None
(Evar core_to_vm (Tfunction Tnil tvoid
cc_default))
nil)))).
Definition f_host_vcpu_run_handler := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := nil;
fn_body := host_vcpu_run_handler_body
|}.
Definition vm_exit_handler_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1) (Evar get_cur_vmid (Tfunction Tnil tuint cc_default))
nil)
(Sset _vmid (Etempvar _t'1 tuint)))
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar get_cur_vcpuid (Tfunction Tnil tuint cc_default)) nil)
(Sset _vcpuid (Etempvar _t'2 tuint)))
(Ssequence
(Scall None
(Evar vm_to_core (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Scall None
(Evar exit_populate_fault (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar get_shadow_ctxt (Tfunction
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))
tulong cc_default))
((Etempvar _vmid tuint) :: (Etempvar _vcpuid tuint) ::
(Econst_int (Int.repr 44) tuint) :: nil))
(Sset _ec (Etempvar _t'3 tulong)))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_long (Int64.repr 2) tulong) tint)
(Ssequence
(Ssequence
(Scall (Some _t'4)
(Evar vm_exit_dispatcher (Tfunction Tnil tint
cc_default))
((Etempvar _vmid tuint) :: (Etempvar _vcpuid tuint) :: nil))
(Sset _ret (Etempvar _t'4 tint)))
(Sifthenelse (Ebinop Oeq (Etempvar _ret tuint)
(Econst_int (Int.repr 0) tint) tint)
(Scall None
(Evar core_to_vm (Tfunction Tnil tvoid
cc_default))
nil)
(Ssequence
(Scall None
(Evar save_vm (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall None
(Evar restore_host (Tfunction Tnil tint
cc_default))
nil)
(Scall None
(Evar core_to_host (Tfunction Tnil tvoid
cc_default))
nil)))))
(Sifthenelse (Ebinop Oeq (Etempvar _ec tulong)
(Econst_int (Int.repr 24) tuint) tint)
(Ssequence
(Scall None (Evar save_vm (Tfunction Tnil tvoid cc_default))
nil)
(Ssequence
(Scall None
(Evar restore_host (Tfunction Tnil tint
cc_default))
nil)
(Scall None
(Evar core_to_host (Tfunction Tnil tvoid
cc_default))
nil)))
(Scall None (Evar panic (Tfunction Tnil tvoid cc_default))
nil)))))))).
Definition f_vm_exit_handler := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_ec, tulong) :: (_vmid, tuint) :: (_vcpuid, tuint) ::
(_ret, tuint) :: (_t'4, tint) :: (_t'3, tulong) ::
(_t'2, tuint) :: (_t'1, tuint) :: nil);
fn_body := vm_exit_handler_body
|}.
Definition dev_load_body :=
(Scall None
(Evar dev_load_ref (Tfunction
(Tcons tulong
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))))
tvoid cc_default))
((Etempvar _gfn tulong) :: (Etempvar _reg tuint) ::
(Etempvar _cbndx tuint) :: (Etempvar _index tuint) :: nil)).
Definition f_dev_load := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_gfn, tulong) :: (_reg, tuint) :: (_cbndx, tuint) ::
(_index, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := dev_load_body
|}.
Definition dev_store_body :=
(Scall None
(Evar dev_store_ref (Tfunction
(Tcons tulong
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))))
tvoid cc_default))
((Etempvar _gfn tulong) :: (Etempvar _reg tuint) ::
(Etempvar _cbndx tuint) :: (Etempvar _index tuint) :: nil)).
Definition f_dev_store := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_gfn, tulong) :: (_reg, tuint) :: (_cbndx, tuint) ::
(_index, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := dev_store_body
|}.