SmmuCoreCode

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

Definition handle_smmu_write_body :=
  (Ssequence
    (Sset _offset
      (Ebinop Oand (Etempvar _fault_ipa tulong)
        (Econst_int (Int.repr 65535) tuint) tulong))
    (Ssequence
      (Sset _write_val (Econst_int (Int.repr 0) tuint))
      (Sifthenelse (Ebinop Olt (Etempvar _offset tulong)
                     (Econst_int (Int.repr 32768) tuint) tint)
        (Ssequence
          (Ssequence
            (Scall (Some _t'1)
              (Evar handle_smmu_global_access (Tfunction
                                                 (Tcons tuint
                                                   (Tcons tulong
                                                     (Tcons tuint Tnil))) tuint
                                                 cc_default))
              ((Etempvar _hsr tuint) :: (Etempvar _offset tulong) ::
               (Etempvar _index tuint) :: nil))
            (Sset _ret (Etempvar _t'1 tuint)))
          (Sifthenelse (Ebinop Oeq (Etempvar _ret tuint)
                         (Econst_int (Int.repr 0) tuint) tint)
            (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil)
            (Scall None
              (Evar __handle_smmu_write (Tfunction
                                           (Tcons tuint
                                             (Tcons tulong
                                               (Tcons tuint
                                                 (Tcons tulong
                                                   (Tcons tuint Tnil))))) tvoid
                                           cc_default))
              ((Etempvar _hsr tuint) :: (Etempvar _fault_ipa tulong) ::
               (Etempvar _len tuint) :: (Econst_long (Int64.repr 0) tulong) ::
               (Etempvar _write_val tuint) :: nil))))
        (Ssequence
          (Ssequence
            (Scall (Some _t'2)
              (Evar handle_smmu_cb_access (Tfunction (Tcons tulong Tnil) tuint
                                             cc_default))
              ((Etempvar _offset tulong) :: nil))
            (Sset _ret (Etempvar _t'2 tuint)))
          (Sifthenelse (Ebinop Oeq (Etempvar _ret tuint)
                         (Econst_int (Int.repr 0) tuint) tint)
            (Scall None (Evar panic (Tfunction Tnil tvoid cc_default)) nil)
            (Sifthenelse (Ebinop Oeq (Etempvar _ret tuint)
                           (Econst_int (Int.repr 2) tuint) tint)
              (Ssequence
                (Ssequence
                  (Scall (Some _t'3)
                    (Evar smmu_get_cbndx (Tfunction (Tcons tulong Tnil) tuint
                                            cc_default))
                    ((Etempvar _offset tulong) :: nil))
                  (Sset _cbndx (Etempvar _t'3 tuint)))
                (Ssequence
                  (Ssequence
                    (Scall (Some _t'4)
                      (Evar get_smmu_cfg_hw_ttbr (Tfunction
                                                    (Tcons tuint
                                                      (Tcons tuint Tnil))
                                                    tulong cc_default))
                      ((Etempvar _cbndx tuint) :: (Etempvar _index tuint) ::
                       nil))
                    (Sset _val (Etempvar _t'4 tulong)))
                  (Ssequence
                    (Sset _write_val (Econst_int (Int.repr 1) tuint))
                    (Scall None
                      (Evar __handle_smmu_write (Tfunction
                                                   (Tcons tuint
                                                     (Tcons tulong
                                                       (Tcons tuint
                                                         (Tcons tulong
                                                           (Tcons tuint Tnil)))))
                                                   tvoid cc_default))
                      ((Etempvar _hsr tuint) :: (Etempvar _fault_ipa tulong) ::
                       (Etempvar _len tuint) :: (Etempvar _val tulong) ::
                       (Etempvar _write_val tuint) :: nil)))))
              (Scall None
                (Evar __handle_smmu_write (Tfunction
                                             (Tcons tuint
                                               (Tcons tulong
                                                 (Tcons tuint
                                                   (Tcons tulong
                                                     (Tcons tuint Tnil)))))
                                             tvoid cc_default))
                ((Etempvar _hsr tuint) :: (Etempvar _fault_ipa tulong) ::
                 (Etempvar _len tuint) ::
                 (Econst_long (Int64.repr 0) tulong) ::
                 (Etempvar _write_val tuint) :: nil)))))))).

Definition f_handle_smmu_write := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_hsr, tuint) :: (_fault_ipa, tulong) :: (_len, tuint) ::
                (_index, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((_offset, tulong) :: (_val, tulong) :: (_ret, tuint) ::
               (_write_val, tuint) :: (_cbndx, tuint) :: (_t'4, tulong) ::
               (_t'3, tuint) :: (_t'2, tuint) :: (_t'1, tuint) :: nil);
  fn_body := handle_smmu_write_body
|}.

Definition handle_smmu_read_body :=
  (Ssequence
    (Sset _offset
      (Ebinop Oand (Etempvar _fault_ipa tulong)
        (Econst_int (Int.repr 65535) tuint) tulong))
    (Sifthenelse (Ebinop Olt (Etempvar _offset tulong)
                   (Econst_int (Int.repr 32768) tuint) tint)
      (Scall None
        (Evar __handle_smmu_read (Tfunction
                                    (Tcons tuint
                                      (Tcons tulong (Tcons tuint Tnil))) tvoid
                                    cc_default))
        ((Etempvar _hsr tuint) :: (Etempvar _fault_ipa tulong) ::
         (Etempvar _len tuint) :: nil))
      (Scall None
        (Evar __handle_smmu_read (Tfunction
                                    (Tcons tuint
                                      (Tcons tulong (Tcons tuint Tnil))) tvoid
                                    cc_default))
        ((Etempvar _hsr tuint) :: (Etempvar _fault_ipa tulong) ::
         (Etempvar _len tuint) :: 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 := ((_offset, tulong) :: nil);
  fn_body := handle_smmu_read_body
|}.