SmmuCoreAuxCode

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

Definition handle_smmu_global_access_body :=
  (Ssequence
    (Ssequence
      (Scall (Some _t'1)
        (Evar host_get_mmio_data (Tfunction (Tcons tuint Tnil) tulong
                                    cc_default))
        ((Etempvar _hsr tuint) :: nil))
      (Sset _data (Etempvar _t'1 tulong)))
    (Ssequence
      (Ssequence
        (Sifthenelse (Ebinop Oge (Etempvar _offset tulong)
                       (Econst_int (Int.repr 0) tint) tint)
          (Sset _t'5
            (Ecast
              (Ebinop Ole (Etempvar _offset tulong)
                (Econst_int (Int.repr 4096) tuint) tint) tbool))
          (Sset _t'5 (Econst_int (Int.repr 0) tint)))
        (Sifthenelse (Etempvar _t'5 tint)
          (Sifthenelse (Ebinop Oeq (Etempvar _offset tulong)
                         (Econst_int (Int.repr 0) tuint) tint)
            (Ssequence
              (Sset _smmu_enable
                (Ebinop Oand
                  (Ebinop Oshr (Etempvar _data tulong)
                    (Econst_int (Int.repr 21) tuint) tulong)
                  (Econst_int (Int.repr 1) tuint) tulong))
              (Sifthenelse (Ebinop Oeq (Etempvar _smmu_enable tulong)
                             (Econst_long (Int64.repr 0) tulong) tint)
                (Sset _ret (Econst_int (Int.repr 0) tuint))
                (Sset _ret (Econst_int (Int.repr 1) tuint))))
            (Sifthenelse (Ebinop Oeq (Etempvar _offset tulong)
                           (Econst_int (Int.repr 8) tuint) tint)
              (Sifthenelse (Ebinop Oeq
                             (Ebinop Oand (Etempvar _data tulong)
                               (Econst_int (Int.repr 255) tint) tulong)
                             (Econst_long (Int64.repr 0) tulong) tint)
                (Sset _ret (Econst_int (Int.repr 1) tuint))
                (Sset _ret (Econst_int (Int.repr 0) tuint)))
              (Sset _ret (Econst_int (Int.repr 1) tuint))))
          (Ssequence
            (Sifthenelse (Ebinop Oge (Etempvar _offset tulong)
                           (Econst_int (Int.repr 4096) tuint) tint)
              (Sset _t'4
                (Ecast
                  (Ebinop Olt (Etempvar _offset tulong)
                    (Econst_int (Int.repr 6144) tuint) tint) tbool))
              (Sset _t'4 (Econst_int (Int.repr 0) tint)))
            (Sifthenelse (Etempvar _t'4 tint)
              (Ssequence
                (Sset _n
                  (Ebinop Odiv
                    (Ebinop Osub (Etempvar _offset tulong)
                      (Econst_int (Int.repr 4096) tuint) tulong)
                    (Econst_int (Int.repr 4) tuint) tulong))
                (Ssequence
                  (Ssequence
                    (Scall (Some _t'2)
                      (Evar get_smmu_cfg_vmid (Tfunction
                                                 (Tcons tuint
                                                   (Tcons tuint Tnil)) tuint
                                                 cc_default))
                      ((Etempvar _n tulong) :: (Etempvar _smmu_index tuint) ::
                       nil))
                    (Sset _vmid (Ecast (Etempvar _t'2 tuint) tulong)))
                  (Ssequence
                    (Sset _type
                      (Ebinop Oshr (Etempvar _data tulong)
                        (Econst_int (Int.repr 16) tuint) tulong))
                    (Ssequence
                      (Sset _t_vmid
                        (Ebinop Oand (Etempvar _data tulong)
                          (Econst_int (Int.repr 255) tint) tulong))
                      (Sifthenelse (Ebinop Oeq (Etempvar _vmid tulong)
                                     (Econst_int (Int.repr 0) tuint) tint)
                        (Sset _ret (Econst_int (Int.repr 1) tuint))
                        (Ssequence
                          (Sifthenelse (Ebinop Oeq (Etempvar _type tulong)
                                         (Econst_int (Int.repr 0) tuint) tint)
                            (Sset _t'3
                              (Ecast
                                (Ebinop Oeq (Etempvar _vmid tulong)
                                  (Etempvar _t_vmid tulong) tint) tbool))
                            (Sset _t'3 (Econst_int (Int.repr 0) tint)))
                          (Sifthenelse (Etempvar _t'3 tint)
                            (Sset _ret (Econst_int (Int.repr 1) tuint))
                            (Sset _ret (Econst_int (Int.repr 0) tuint)))))))))
              (Sset _ret (Econst_int (Int.repr 1) tuint))))))
      (Ssequence
        (Scall (Some _t'6)
          (Evar check (Tfunction (Tcons tuint Tnil) tuint cc_default))
          ((Etempvar _ret tuint) :: nil))
        (Sreturn (Some (Etempvar _t'6 tuint)))))).

Definition f_handle_smmu_global_access := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := ((_hsr, tuint) :: (_offset, tulong) :: (_smmu_index, tuint) ::
                nil);
  fn_vars := nil;
  fn_temps := ((_data, tulong) :: (_smmu_enable, tulong) :: (_n, tulong) ::
               (_vmid, tulong) :: (_type, tulong) :: (_t_vmid, tulong) ::
               (_ret, tuint) :: (_t'6, tuint) :: (_t'5, tint) ::
               (_t'4, tint) :: (_t'3, tint) :: (_t'2, tuint) ::
               (_t'1, tulong) :: nil);
  fn_body := handle_smmu_global_access_body
|}.

Definition handle_smmu_cb_access_body :=
  (Ssequence
    (Sset _offset
      (Ebinop Osub (Etempvar _offset tulong)
        (Econst_int (Int.repr 32768) tuint) tulong))
    (Ssequence
      (Sset _cb_offset
        (Ebinop Oand (Etempvar _offset tulong)
          (Econst_int (Int.repr 4095) tuint) tulong))
      (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar _cb_offset tulong)
                       (Econst_int (Int.repr 32) tint) tint)
          (Sset _ret (Econst_int (Int.repr 2) tuint))
          (Sifthenelse (Ebinop Oeq (Etempvar _cb_offset tulong)
                         (Econst_int (Int.repr 52) tint) tint)
            (Sset _ret (Econst_int (Int.repr 0) tuint))
            (Sset _ret (Econst_int (Int.repr 1) tuint))))
        (Ssequence
          (Scall (Some _t'1)
            (Evar check (Tfunction (Tcons tuint Tnil) tuint cc_default))
            ((Etempvar _ret tuint) :: nil))
          (Sreturn (Some (Etempvar _t'1 tuint))))))).

Definition f_handle_smmu_cb_access := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := ((_offset, tulong) :: nil);
  fn_vars := nil;
  fn_temps := ((_cb_offset, tulong) :: (_ret, tuint) :: (_t'1, tuint) :: nil);
  fn_body := handle_smmu_cb_access_body
|}.

Definition __handle_smmu_write_body :=
  (Sifthenelse (Ebinop Oeq (Etempvar _len tuint)
                 (Econst_int (Int.repr 8) tuint) tint)
    (Sifthenelse (Ebinop Oeq (Etempvar _write_val tuint)
                   (Econst_int (Int.repr 0) tuint) tint)
      (Ssequence
        (Ssequence
          (Scall (Some _t'1)
            (Evar host_get_mmio_data (Tfunction (Tcons tuint Tnil) tulong
                                        cc_default))
            ((Etempvar _hsr tuint) :: nil))
          (Sset _data (Etempvar _t'1 tulong)))
        (Scall None
          (Evar writeq_relaxed (Tfunction (Tcons tulong (Tcons tulong Tnil))
                                  tvoid cc_default))
          ((Etempvar _data tulong) :: (Etempvar _fault_ipa tulong) :: nil)))
      (Scall None
        (Evar writeq_relaxed (Tfunction (Tcons tulong (Tcons tulong Tnil))
                                tvoid cc_default))
        ((Etempvar _val tulong) :: (Etempvar _fault_ipa tulong) :: nil)))
    (Sifthenelse (Ebinop Oeq (Etempvar _len tuint)
                   (Econst_int (Int.repr 4) tuint) tint)
      (Scall None
        (Evar writel_relaxed (Tfunction (Tcons tulong (Tcons tulong Tnil))
                                tvoid cc_default))
        ((Etempvar _val tulong) :: (Etempvar _fault_ipa tulong) :: nil))
      (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil))).

Definition f___handle_smmu_write := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_hsr, tuint) :: (_fault_ipa, tulong) :: (_len, tuint) ::
                (_val, tulong) :: (_write_val, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((_data, tulong) :: (_t'1, tulong) :: nil);
  fn_body := __handle_smmu_write_body
|}.

Definition __handle_smmu_read_body :=
  (Ssequence
    (Ssequence
      (Scall (Some _t'1)
        (Evar host_dabt_get_rd (Tfunction (Tcons tuint Tnil) tuint cc_default))
        ((Etempvar _hsr tuint) :: nil))
      (Sset _rt (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)))
      (Sifthenelse (Ebinop Oeq (Etempvar _len tuint)
                     (Econst_int (Int.repr 8) tuint) tint)
        (Ssequence
          (Ssequence
            (Scall (Some _t'3)
              (Evar readq_relaxed (Tfunction (Tcons tulong Tnil) tulong
                                     cc_default))
              ((Etempvar _fault_ipa tulong) :: nil))
            (Sset _data (Etempvar _t'3 tulong)))
          (Scall None
            (Evar set_shadow_ctxt (Tfunction
                                     (Tcons tuint
                                       (Tcons tuint
                                         (Tcons tuint (Tcons tulong Tnil))))
                                     tvoid cc_default))
            ((Econst_int (Int.repr 0) tuint) :: (Etempvar _vcpuid tuint) ::
             (Etempvar _rt tuint) :: (Etempvar _data tulong) :: nil)))
        (Sifthenelse (Ebinop Oeq (Etempvar _len tuint)
                       (Econst_int (Int.repr 4) tuint) tint)
          (Ssequence
            (Ssequence
              (Scall (Some _t'4)
                (Evar readl_relaxed (Tfunction (Tcons tulong Tnil) tulong
                                       cc_default))
                ((Etempvar _fault_ipa tulong) :: nil))
              (Sset _data (Etempvar _t'4 tulong)))
            (Scall None
              (Evar set_shadow_ctxt (Tfunction
                                       (Tcons tuint
                                         (Tcons tuint
                                           (Tcons tuint (Tcons tulong Tnil))))
                                       tvoid cc_default))
              ((Econst_int (Int.repr 0) tuint) :: (Etempvar _vcpuid tuint) ::
               (Etempvar _rt tuint) :: (Etempvar _data tulong) :: nil)))
          (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil))))).

Definition f___handle_smmu_read := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_hsr, tuint) :: (_fault_ipa, tulong) :: (_len, tuint) ::
                nil);
  fn_vars := nil;
  fn_temps := ((_data, tulong) :: (_rt, tuint) :: (_vcpuid, tuint) ::
               (_t'4, tulong) :: (_t'3, tulong) :: (_t'2, tuint) ::
               (_t'1, tuint) :: nil);
  fn_body := __handle_smmu_read_body
|}.