Hi  Yanyan, 
 According to your advice，I modified the avail_p_regs[] in hardware.h file as tk1. 1 MiB starting from 0x37f00000 is reserved for monitor mode. 

{ /* .start = */ 0x10000000, /* .end = */ 0x37f00000}

And then
#define MON_PA_START     (0x10000000 + 0x27f00000)
#define MON_PA_SIZE      (1 << 20)
#define MON_PA_END       (MON_PA_START + MON_PA_SIZE)
#define MON_PA_STACK     (MON_PA_END - 0x10)
#define MON_VECTOR_START (MON_PA_START)

set sp:
asm volatile ("cps %0\n\t"
                      "isb\n"
                      "mov sp, %1\n\t"         
                     ::"I"(MONITOR_MODE),"r"(MON_PA_STACK));

copy monitor mode vector and write into MVBAR:
uint32_t size = arm_monitor_vector_end - arm_monitor_vector;
printf("Copy monitor mode vector from %x to %x size %x \n", (arm_monitor_vector), MON_VECTOR_START, size);
    memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size);
        asm volatile ("dmb\n isb\n");
        asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START));

I used the arm_monitor_vector provided by the source code in monitor.S and just didn't perform the operation 'blx r0'.  I think the it can jump to smc_handler and return successfully.

#define VECTOR_BASE     0x37f00000
#define STACK_TOP       (VECTOR_BASE + (1 << 20) - 0x10)

arm_monitor_vector:
    ldr pc, [pc, #28]
    ldr pc, [pc, #24]
    ldr pc, [pc, #16]
    ldr pc, [pc, #16]
    ldr pc, [pc, #12]
    ldr pc, [pc, #8]
    ldr pc, [pc, #4]
    ldr pc, [pc, #0]

smc_handler_addr:
.word   VECTOR_BASE + (smc_handler - arm_monitor_vector)//0x1000002c
smc_halt_addr:
.word   VECTOR_BASE + (smc_halt - arm_monitor_vector)
smc_stack:
.word   STACK_TOP

smc_handler:
    /* always have a valid stack */
    ldr sp, [pc, #-12]
    push {lr}
    //blx r0
    isb
    mrc p15, 0, r5, c1, c1, 0
    /* set the NS bit */
    orr r5, r5, #1
    mcr p15, 0, r5, c1, c1, 0
    pop {lr}
    isb
    movs pc, lr
 
However, the problem still exists. And I have another question that why set the sp in monitor mode to sp in SVC mode. 
asm volatile ("mov r8, sp\n\t"   
                      "cps %0\n\t"    
                      "isb\n"         
                      "mov sp, r8\n\t"
                     ::"I"(MONITOR_MODE));


Thank you,
Dongxu Ji

<Yanyan.Shen@data61.csiro.au> 于2018年8月28日周二 下午10:10写道：

Hi Dongxu,


As you can see, the arm_monitor_vector uses PC-relative addressing so that the code can be moved around in memory.  I think ldr pc, =smc_handler breaks this. Also, please set the NS bit in SCR to 1 before returning.


To reserve a memory region for the monitor-mode code and data, I suggest you modify the avail_p_regs[] in kernel/include/plat/imx6/plat/machine/hardware.h file. See the kernel/include/plat/tk1/plat/machine/hardware.h as an example.​



Regards,

Yanyan


From: Dongxu Ji <jidongxu1993@gmail.com>
Sent: Wednesday, August 29, 2018 12:02 AM
To: devel@sel4.systems; Shen, Yanyan (Data61, Kensington NSW)
Subject: Fwd: [seL4] SMC in seL4
 
Hi  Yanyan,
1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do anything). The arm_monitor_vector and the smc_handler():

arm_monitor_vector:
    ldr pc, [pc, #28]
    ldr pc, [pc, #24]
    ldr pc, =smc_handler
    ldr pc, [pc, #16]
    ldr pc, [pc, #12]
    ldr pc, [pc, #8]
    ldr pc, [pc, #4]
    ldr pc, [pc, #0]

smc_handler:
    movs pc, lr

2. I didn't do any extra work other than the boot log:

..........
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10                             
  paddr=[20000000..203fbfff]                                                    
ELF-loading image 'kernel'                                                      
  paddr=[10000000..10026fff]                                                    
  vaddr=[e0000000..e0026fff]                                                    
  virt_entry=e0000000                                                           
ELF-loading image 'sel4test-driver'                                             
  paddr=[10027000..10500fff]                                                    
  vaddr=[8000..4e1fff]                                                          
  virt_entry=25a6c                                                              
Enabling MMU and paging                                                         
Jumping to kernel-image entry point...

3. The initialization operations in platform_init.c:
set sp:
#define MONITOR_MODE        (0x16)
#define MON_VECTOR_START    (0x11000000)
#define VECTOR_BASE     0x11000000
#define STACK_TOP       (VECTOR_BASE + (1 << 12) - 0x10)

asm volatile ( "mrs r1, cpsr\n\t"
                      "cps %0\n\t"
                      "isb\n"
                      "mov sp, %1\n\t"
                      "msr cpsr, r1\n\t"                 
                     ::"I"(MONITOR_MODE),"r"(STACK_TOP));

copy monitor mode vector to MON_VECTOR_START  and write into MVBAR: 
uint32_t size = arm_monitor_vector_end - arm_monitor_vector;
    printf("Copy monitor mode vector from %x to %x size %x\n", (arm_monitor_vector), MON_VECTOR_START, size);
    memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size);
        asm volatile ("dmb\n isb\n");
        asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START));

I enter into SVC mode by software interrupt and call the function smc():
                  asm (".arch_extension sec\n");
     asm volatile ("stmfd    sp!, {r3-r11, lr}\n\t"
                   "dsb\n"
                   "smc #0\n"
                   "ldmfd    sp!, {r3-r11, pc}");

and then the problem arises.

Thank you,
Dongxu Ji


<Yanyan.Shen@data61.csiro.au> 于2018年8月28日周二 下午8:30写道：

Hi,

The smc_handle() in monitor.S, it does nothing but "movs pc, lr".
Does it set the NS bit to 1 in SCR?

Also, what did you do to ensure that 0x11000000 is not used by the kernel?

Could you share the code (if possible) so that I could better understand the problem. 

Regards,
Yanyan


From: Devel <devel-bounces@sel4.systems> on behalf of 冀东旭 <jidongxu1993@gmail.com>
Sent: Tuesday, August 28, 2018 1:02 PM
To: devel@sel4.systems
Subject: [seL4] SMC in seL4
 
Hello,
I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone.  I initialize the monitor mode by setting the sp to  STACK_TOP and copying arm_monitor_vector to MON_VECTOR_START according to the functions "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c".
#define VECTOR_BASE     0x11000000(addr is not used by the seL4 kernel)
#define STACK_TOP       (VECTOR_BASE + (1 << 12) - 0x10)
#define MON_VECTOR_START    0x11000000(The VECTOR_BASE is the same as MON_VECTOR_START)
The smc_handle() in monitor.S, it does nothing but "movs pc, lr".  After calling smc in SVC mode, it hangs without any log.  If I comment the "smc #0", it can return the caller successfully in usr mode.
    stmfd    sp!, {r3-r11, lr}
    dsb
    smc #0
    ldmfd    sp!, {r3-r11, pc}
Is the sp in monitor mode appropriate? Or I need to do something else in initialization operations?  What's wrong with it?  Do you have any ideas?
Thank you!
Dongxu Ji