handle_exception_sync.v

Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import RealmSyncHandler.Spec.

Local Open Scope Z_scope.

Section Spec.

  Definition handle_exception_sync_spec (rec: Pointer) (adt: RData) : option (RData * Z) :=
    rely (peq (base rec) buffer_loc);
    when gidx == (buffer (priv adt)) @ (offset rec);
    let gn := (gs (share adt)) @ gidx in
    rely (g_tag (ginfo gn) =? GRANULE_STATE_REC);
    rely (ref_accessible gn CPU_ID);
    let esr := r_esr_el2 (cpu_regs (priv adt)) in
    rely is_int64 esr;
    let ec := Z.land esr ESR_EL2_EC_MASK in
    if ec =? ESR_EL2_EC_WFX then
      let esr := Z.land esr (Z.lor ESR_EL2_EC_MASK ESR_EL2_WFx_TI_BIT) in
      Some (adt {priv: (priv adt) {rec_run: (rec_run (priv adt)) # 1 == esr}}, 0)
    else
      if ec =? ESR_EL2_EC_HVC then
        let info := Z.land esr (Z.lor ESR_EL2_EC_MASK ESR_EL2_xVC_IMM_MASK) in
        let g' := gn {grec: (grec gn) {g_esr: info}} in
        rely regs_is_int64_dec (g_regs (grec gn));
        Some (adt {priv: (priv adt) {rec_run: (rec_run (priv adt))
                                              # 1 == info # 5 == (r_x0 (g_regs (grec gn)))
                                              # 6 == (r_x1 (g_regs (grec gn))) # 7 == (r_x2 (g_regs (grec gn)))
                                              # 8 == (r_x3 (g_regs (grec gn))) # 9 == (r_x4 (g_regs (grec gn)))
                                              # 10 == (r_x5 (g_regs (grec gn))) # 11 == (r_x6 (g_regs (grec gn)))}}
                  {share: (share adt) {gs: (gs (share adt)) # gidx == g'}}, 0)
      else
        if ec =? ESR_EL2_EC_SMC then
          let pc := r_elr_el2 (cpu_regs (priv adt)) in
          rely is_int64 pc; rely is_int64 (pc + 4);
          let adt' := adt {priv: (priv adt) {cpu_regs: (cpu_regs (priv adt)) {r_elr_el2: (pc + 4)}}} in
          when ret, adt == handle_realm_rsi_spec rec adt';
          rely is_int ret;
          Some (adt, ret)
        else
          if ec =? ESR_EL2_EC_SYSREG then
            when adt == handle_sysreg_access_trap_spec rec (VZ64 esr) adt;
            let pc := r_elr_el2 (cpu_regs (priv adt)) in
            rely is_int64 pc; rely is_int64 (pc + 4);
            Some (adt {priv: (priv adt) {cpu_regs: (cpu_regs (priv adt)) {r_elr_el2: (pc + 4)}}}, 1)
          else
            let adt' := adt {priv: (priv adt) {rec_run: (rec_run (priv adt)) # 1 == 0 # 2 == 0 # 3 == 0}} in
            if ec =? ESR_EL2_EC_INST_ABORT then
              let fsc := Z.land esr ESR_EL2_ABORT_FSC_MASK in
              let fsc_type := Z.land fsc NOT_ESR_EL2_ABORT_FSC_LEVEL_MASK in
              let hpfar := r_hpfar_el2 (cpu_regs (priv adt)) in
              rely is_int64 hpfar;
              if fsc_type =? ESR_EL2_ABORT_FSC_PERMISSION_FAULT then
                Some (adt', 0)
              else
                if fsc_type =? ESR_EL2_ABORT_FSC_TRANSLATION_FAULT then
                  let fipa := Z.shiftl (Z.land hpfar HPFAR_EL2_FIPA_MASK) HPFAR_EL2_FIPA_OFFSET in
                  rely is_int64 fipa;
                  let par_base := g_rec_par_base (grec gn) in
                  let par_end := g_rec_par_end (grec gn) in
                  rely is_int64 par_base; rely is_int64 par_end;
                  if (par_base <=? fipa) && (fipa <? par_end) then
                    let esr := Z.land esr (Z.lor ESR_EL2_EC_MASK ESR_EL2_ABORT_FSC_MASK) in
                    Some (adt {priv: (priv adt) {rec_run: (rec_run (priv adt)) # 1 == esr # 3 == hpfar}}, 0)
                  else Some (adt', 0)
                else Some (adt', 0)
            else
              if ec =? ESR_EL2_EC_DATA_ABORT then
                when adt == handle_data_abort_spec rec (VZ64 esr) adt;
                Some (adt, 0)
              else Some (adt', 0).

End Spec.