text: /*
   * Copyright 2017, Data61
   * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
   * ABN 41 687 119 230.
   *
   * This software may be distributed and modified according to the terms of
   * the GNU General Public License version 2. Note that NO WARRANTY is provided.
   * See "LICENSE_GPLv2.txt" for details.
   *
   * @TAG(DATA61_GPL)
   */
  
  #include <config.h>
  #include <types.h>
  #include <api/faults.h>
  #include <api/syscall.h>
  #include <kernel/thread.h>
  #include <arch/kernel/thread.h>
  #include <machine/debug.h>
  
  /* consistency with libsel4 */
  compile_assert(InvalidRoot, lookup_fault_invalid_root + 1 == seL4_InvalidRoot)
  compile_assert(MissingCapability, lookup_fault_missing_capability + 1 == seL4_MissingCapability)
  compile_assert(DepthMismatch, lookup_fault_depth_mismatch + 1 == seL4_DepthMismatch)
  compile_assert(GuardMismatch, lookup_fault_guard_mismatch + 1 == seL4_GuardMismatch)
  compile_assert(seL4_UnknownSyscall_Syscall, (word_t) n_syscallMessage == seL4_UnknownSyscall_Syscall)
  compile_assert(seL4_UserException_Number, (word_t) n_exceptionMessage == seL4_UserException_Number)
  compile_assert(seL4_UserException_Code, (word_t) n_exceptionMessage + 1 == seL4_UserException_Code)
  
  static inline unsigned int
  setMRs_lookup_failure(tcb_t *receiver, word_t* receiveIPCBuffer,
                        lookup_fault_t luf, unsigned int offset)
  {
      word_t lufType = lookup_fault_get_lufType(luf);
      word_t i;
  
      i = setMR(receiver, receiveIPCBuffer, offset, lufType + 1);
  
      /* check constants match libsel4 */
      if (offset == seL4_CapFault_LookupFailureType) {
          assert(offset + 1 == seL4_CapFault_BitsLeft);
          assert(offset + 2 == seL4_CapFault_DepthMismatch_BitsFound);
          assert(offset + 2 == seL4_CapFault_GuardMismatch_GuardFound);
          assert(offset + 3 == seL4_CapFault_GuardMismatch_BitsFound);
      } else {
          assert(offset == 1);
      }
  
      switch (lufType) {
      case lookup_fault_invalid_root:
          return i;
  
      case lookup_fault_missing_capability:
          return setMR(receiver, receiveIPCBuffer, offset + 1,
                       lookup_fault_missing_capability_get_bitsLeft(luf));
  
      case lookup_fault_depth_mismatch:
          setMR(receiver, receiveIPCBuffer, offset + 1,
                lookup_fault_depth_mismatch_get_bitsLeft(luf));
          return setMR(receiver, receiveIPCBuffer, offset + 2,
                       lookup_fault_depth_mismatch_get_bitsFound(luf));
  
      case lookup_fault_guard_mismatch:
          setMR(receiver, receiveIPCBuffer, offset + 1,
                lookup_fault_guard_mismatch_get_bitsLeft(luf));
          setMR(receiver, receiveIPCBuffer, offset + 2,
                lookup_fault_guard_mismatch_get_guardFound(luf));
          return setMR(receiver, receiveIPCBuffer, offset + 3,
                       lookup_fault_guard_mismatch_get_bitsFound(luf));
  
      default:
          fail("Invalid lookup failure");
      }
  }
  
  static inline void
  copyMRsFaultReply(tcb_t *sender, tcb_t *receiver, MessageID_t id, word_t length)
  {
      word_t i;
      bool_t archInfo;
  
      archInfo = Arch_getSanitiseRegisterInfo(receiver);
  
      for (i = 0; i < MIN(length, n_msgRegisters); i++) {
          register_t r = fault_messages[id][i];
          word_t v = getRegister(sender, msgRegisters[i]);
          setRegister(receiver, r, sanitiseRegister(r, v, archInfo));
      }
  
      if (i < length) {
          word_t *sendBuf = lookupIPCBuffer(false, sender);
          if (sendBuf) {
              for (; i < length; i++) {
                  register_t r = fault_messages[id][i];
                  word_t v = sendBuf[i + 1];
                  setRegister(receiver, r, sanitiseRegister(r, v, archInfo));
              }
          }
      }
  }
  
  static inline void
  copyMRsFault(tcb_t *sender, tcb_t *receiver, MessageID_t id,
               word_t length, word_t *receiveIPCBuffer)
  {
      word_t i;
      for (i = 0; i < MIN(length, n_msgRegisters); i++) {
          setRegister(receiver, msgRegisters[i], getRegister(sender, fault_messages[id][i]));
      }
  
      if (receiveIPCBuffer) {
          for (; i < length; i++) {
              receiveIPCBuffer[i + 1] = getRegister(sender, fault_messages[id][i]);
          }
      }
  }
  
  bool_t
  handleFaultReply(tcb_t *receiver, tcb_t *sender)
  {
      /* These lookups are moved inward from doReplyTransfer */
      seL4_MessageInfo_t tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
      word_t label = seL4_MessageInfo_get_label(tag);
      word_t length = seL4_MessageInfo_get_length(tag);
      seL4_Fault_t fault = receiver->tcbFault;
  
      switch (seL4_Fault_get_seL4_FaultType(fault)) {
      case seL4_Fault_CapFault:
          return true;
  
      case seL4_Fault_UnknownSyscall:
          copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage));
          return (label == 0);
  
      case seL4_Fault_UserException:
          copyMRsFaultReply(sender, receiver, MessageID_Exception, MIN(length, n_exceptionMessage));
          return (label == 0);
  
  #ifdef CONFIG_HARDWARE_DEBUG_API
      case seL4_Fault_DebugException: {
          word_t n_instrs;
  
          if (seL4_Fault_DebugException_get_exceptionReason(fault) != seL4_SingleStep) {
              /* Only single-step replies are required to set message registers.
               */
              return (label == 0);
          }
  
          if (length < DEBUG_REPLY_N_EXPECTED_REGISTERS) {
              /* A single-step reply doesn't mean much if it isn't composed of the bp
               * number and number of instructions to skip. But even if both aren't
               * set, we can still allow the thread to continue because replying
               * should uniformly resume thread execution, based on the general seL4
               * API model.
               *
               * If it was single-step, but no reply registers were set, just
               * default to skipping 1 and continuing.
               *
               * On x86, bp_num actually doesn't matter for single-stepping
               * because single-stepping doesn't use a hardware register -- it
               * uses EFLAGS.TF.
               */
              n_instrs = 1;
          } else {
              /* If the reply had all expected registers set, proceed as normal */
              n_instrs = getRegister(sender, msgRegisters[0]);
          }
  
          syscall_error_t res;
  
          res = Arch_decodeConfigureSingleStepping(receiver, 0, n_instrs, true);
          if (res.type != seL4_NoError) {
              return false;
          };
  
          configureSingleStepping(receiver, 0, n_instrs, true);
  
          /* Replying will always resume the thread: the only variant behaviour
           * is whether or not the thread will be resumed with stepping still
           * enabled.
           */
          return (label == 0);
      }
  #endif
  
      default:
          return Arch_handleFaultReply(receiver, sender, seL4_Fault_get_seL4_FaultType(fault));
      }
  }
  
  word_t
  setMRs_fault(tcb_t *sender, tcb_t* receiver, word_t *receiveIPCBuffer)
  {
      switch (seL4_Fault_get_seL4_FaultType(sender->tcbFault)) {
      case seL4_Fault_CapFault:
          setMR(receiver, receiveIPCBuffer, seL4_CapFault_IP, getRestartPC(sender));
          setMR(receiver, receiveIPCBuffer, seL4_CapFault_Addr,
                seL4_Fault_CapFault_get_address(sender->tcbFault));
          setMR(receiver, receiveIPCBuffer, seL4_CapFault_InRecvPhase,
                seL4_Fault_CapFault_get_inReceivePhase(sender->tcbFault));
          return setMRs_lookup_failure(receiver, receiveIPCBuffer,
                                       sender->tcbLookupFailure, seL4_CapFault_LookupFailureType);
  
      case seL4_Fault_UnknownSyscall: {
          copyMRsFault(sender, receiver, MessageID_Syscall, n_syscallMessage,
                       receiveIPCBuffer);
  
          return setMR(receiver, receiveIPCBuffer, n_syscallMessage,
                       seL4_Fault_UnknownSyscall_get_syscallNumber(sender->tcbFault));
      }
  
      case seL4_Fault_UserException: {
          copyMRsFault(sender, receiver, MessageID_Exception,
                       n_exceptionMessage, receiveIPCBuffer);
          setMR(receiver, receiveIPCBuffer, n_exceptionMessage,
                seL4_Fault_UserException_get_number(sender->tcbFault));
          return setMR(receiver, receiveIPCBuffer, n_exceptionMessage + 1u,
                       seL4_Fault_UserException_get_code(sender->tcbFault));
      }
  
  #ifdef CONFIG_HARDWARE_DEBUG_API
      case seL4_Fault_DebugException: {
          word_t reason = seL4_Fault_DebugException_get_exceptionReason(sender->tcbFault);
  
          setMR(receiver, receiveIPCBuffer,
                seL4_DebugException_FaultIP, getRestartPC(sender));
          unsigned int ret = setMR(receiver, receiveIPCBuffer,
                                   seL4_DebugException_ExceptionReason, reason);
  
          if (reason != seL4_SingleStep && reason != seL4_SoftwareBreakRequest) {
              ret = setMR(receiver, receiveIPCBuffer,
                          seL4_DebugException_TriggerAddress,
                          seL4_Fault_DebugException_get_breakpointAddress(sender->tcbFault));
  
              /* Breakpoint messages also set a "breakpoint number" register. */
              ret = setMR(receiver, receiveIPCBuffer,
                          seL4_DebugException_BreakpointNumber,
                          seL4_Fault_DebugException_get_breakpointNumber(sender->tcbFault));
          }
          return ret;
      }
  #endif /* CONFIG_HARDWARE_DEBUG_API */
  
      default:
          return Arch_setMRs_fault(sender, receiver, receiveIPCBuffer,
                                   seL4_Fault_get_seL4_FaultType(sender->tcbFault));
      }
  }
  