1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7typedef long word_t; 8typedef struct { int fld1, fld2; } tcb_t; 9 10/** 11 DONT_TRANSLATE 12 */ 13__attribute__((noreturn)) 14static inline void 15fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread) 16{ 17 register word_t r0 asm ("r0") = badge; 18 register word_t r1 asm ("r1") = msgInfo; 19 asm volatile ( 20 "add sp, %[cur_thread], %[offset]\n\t" /* Point to LR_svc */ 21 "ldmdb sp, {r2-lr}^\n\t" 22 "rfeia sp\n\t" 23 : 24 : [offset] "i" (PT_LR_svc), 25 [cur_thread] "r" (cur_thread), 26 "r"(r0), "r"(r1) 27 : "memory" ); 28} 29