MmioPTAllocCode

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 _arg := 2%positive.
Definition _base := 3%positive.
Definition _cb_offset := 4%positive.
Definition _cbndx := 5%positive.
Definition _cnt := 6%positive.
Definition _count := 7%positive.
Definition _cur_vcpuid := 8%positive.
Definition _cur_vmid := 9%positive.
Definition _data := 10%positive.
Definition _end := 11%positive.
Definition _esr := 12%positive.
Definition _fault_ipa := 13%positive.
Definition _gfn := 14%positive.
Definition _gpa := 15%positive.
Definition _hsr := 16%positive.
Definition _i := 17%positive.
Definition _index := 18%positive.
Definition _iova := 19%positive.
Definition _is_write := 20%positive.
Definition _kvm := 21%positive.
Definition _len := 22%positive.
Definition _level := 23%positive.
Definition _load_addr := 24%positive.
Definition _load_idx := 25%positive.
Definition _load_info_cnt := 26%positive.
Definition _main := 27%positive.
Definition _map := 28%positive.
Definition _mapped := 29%positive.
Definition _n := 30%positive.
Definition _next := 31%positive.
Definition _num := 32%positive.
Definition _num_context_banks := 33%positive.
Definition _offset := 34%positive.
Definition _owner := 35%positive.
Definition _pa := 36%positive.
Definition _paddr := 37%positive.
Definition _page_count := 38%positive.
Definition _pass_lock := 39%positive.
Definition _perm := 40%positive.
Definition _pfn := 41%positive.
Definition _pgnum := 42%positive.
Definition _power := 43%positive.
Definition _prot := 44%positive.
Definition _pte := 45%positive.
Definition _pte_pa := 46%positive.
Definition _remap := 47%positive.
Definition _remap_addr := 48%positive.
Definition _res := 49%positive.
Definition _ret := 50%positive.
Definition _rt := 51%positive.
Definition _size := 52%positive.
Definition _smmu_enable := 53%positive.
Definition _smmu_index := 54%positive.
Definition _start := 55%positive.
Definition _state := 56%positive.
Definition _t_vmid := 57%positive.
Definition _target := 58%positive.
Definition _target_addr := 59%positive.
Definition _target_vmid := 60%positive.
Definition _total_smmu := 61%positive.
Definition _type := 62%positive.
Definition _val := 63%positive.
Definition _valid := 64%positive.
Definition _vcpu := 65%positive.
Definition _vcpu_state := 66%positive.
Definition _vcpuid := 67%positive.
Definition _vm_state := 68%positive.
Definition _vmid := 69%positive.
Definition _wait_lock := 70%positive.
Definition _write_val := 71%positive.
Definition _t'1 := 72%positive.
Definition _t'2 := 73%positive.

Definition alloc_smmu_pgd_page_body :=
  (Ssequence
    (Ssequence
      (Scall (Some _t'1)
        (Evar get_smmu_pgd_next (Tfunction Tnil tulong cc_default)) nil)
      (Sset _next (Etempvar _t'1 tulong)))
    (Ssequence
      (Sset _end (Econst_long (Int64.repr 2162688) tulong))
      (Ssequence
        (Sifthenelse (Ebinop Ole
                       (Ebinop Oadd (Etempvar _next tulong)
                         (Econst_long (Int64.repr 4096) tulong) tulong)
                       (Etempvar _end tulong) tint)
          (Scall None
            (Evar set_smmu_pgd_next (Tfunction (Tcons tulong Tnil) tvoid
                                       cc_default))
            ((Ebinop Oadd (Etempvar _next tulong)
               (Econst_long (Int64.repr 4096) tulong) tulong) :: nil))
          (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil))
        (Ssequence
          (Scall (Some _t'2)
            (Evar check64 (Tfunction (Tcons tulong Tnil) tulong cc_default))
            ((Etempvar _next tulong) :: nil))
          (Sreturn (Some (Etempvar _t'2 tulong))))))).

Definition f_alloc_smmu_pgd_page := {|
  fn_return := tulong;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_next, tulong) :: (_end, tulong) :: (_t'2, tulong) ::
               (_t'1, tulong) :: nil);
  fn_body := alloc_smmu_pgd_page_body
|}.

Definition alloc_smmu_pmd_page_body :=
  (Ssequence
    (Ssequence
      (Scall (Some _t'1)
        (Evar get_smmu_pmd_next (Tfunction Tnil tulong cc_default)) nil)
      (Sset _next (Etempvar _t'1 tulong)))
    (Ssequence
      (Sset _end (Econst_long (Int64.repr 3211264) tulong))
      (Ssequence
        (Sifthenelse (Ebinop Ole
                       (Ebinop Oadd (Etempvar _next tulong)
                         (Econst_long (Int64.repr 4096) tulong) tulong)
                       (Etempvar _end tulong) tint)
          (Scall None
            (Evar set_smmu_pmd_next (Tfunction (Tcons tulong Tnil) tvoid
                                       cc_default))
            ((Ebinop Oadd (Etempvar _next tulong)
               (Econst_long (Int64.repr 4096) tulong) tulong) :: nil))
          (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil))
        (Ssequence
          (Scall (Some _t'2)
            (Evar check64 (Tfunction (Tcons tulong Tnil) tulong cc_default))
            ((Etempvar _next tulong) :: nil))
          (Sreturn (Some (Etempvar _t'2 tulong))))))).

Definition f_alloc_smmu_pmd_page := {|
  fn_return := tulong;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_next, tulong) :: (_end, tulong) :: (_t'2, tulong) ::
               (_t'1, tulong) :: nil);
  fn_body := alloc_smmu_pmd_page_body
|}.