Hi Mike, Those coprocessor registers are not currently saved or restored in the VCPU. If they were you could use the ARMVCPUReadReg and ARMVCPUWriteReg invocations to control the value of those registers for the guest. There is an active task internally to add those coprocessor registers to the VCPU which would allow you to use those invocations, but at this stage it isn't supported sorry.
If you wanted, you could look at adding a special case to the above invocations in the kernel (looking in /kernel/src/arch/arm/object/vcpu.c and kernel/include/arch/arm/arch/object/vcpu.h) where you would have to add the assembly to read and write to the registers yourself. Kind regards, Kent McLeod ________________________________________ From: Mike Clark <undefinedsp...@gmail.com> Sent: Thursday, June 22, 2017 12:04 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation Kent, Thanks, that was very helpful. I've now gotten to the point where I can trap on access to a specific coprocessor register (c2 of cp15) by using HSTR. I wrote a handler function that parses the ISS to get everything I need. I'm not sure if I am headed down the right path from there, however. I'm assuming that somehow I can set the virtual c2 of cp15 to effectively emulate the instruction using the data pulled from the ISS. I have access to the vm and the fault. Are there some data structures in one of those that store the current value of the coprocessor registers? Once I do that, it looks like I can call ignore_fault, which advances the PC and restarts the VM. Is that the right path to head down? On Fri, Jun 16, 2017 at 12:24 AM, <kent.mcl...@data61.csiro.au> wrote: > Hi Mike, > > If you look at handle_page_fault(), the VMM can do limited instruction > emulation if the relevant info is in the ISS segment of the HSR. Any other > emulation isn't supported. handle_page_fault() handles cases of restarting a > faulting instruction, emulating an instruction, or in the > https://github.com/smaccm/darpa-bsp project, when using the vm-tk1_defconfig > configuration forwards reads and writes to uart hardware to a separate CAmkES > component. If you are wanting to trap access to certain mmio registers, then > looking at how that project handles access to the UART and CLKCAR devices (on > TK1) could be a place to start. > > Traps caused by HSTR should end up being sent to the VMM by seL4 as a > seL4_Fault_VCPUFault (You can look in kernel/src/arch/arm/32/hyp_traps.S > under "Traps taken to HYP mode" to see where the trap enters the kernel). > > Kind regards, > Kent McLeod. > ________________________________________ > From: Devel <devel-bounces@sel4.systems> on behalf of Mike Clark > <undefinedsp...@gmail.com> > Sent: Friday, June 16, 2017 5:18 AM > To: Lyons, Anna (Data61, Kensington NSW) > Cc: devel@sel4.systems > Subject: Re: [seL4] vmm documentation > > Here is another question, again on ARM. Let's say I want to configure > the VCPU to trap on certain instructions or register accesses. It is > my understanding I can do this by setting either HCR or HSTR to trap > the way I want it to. > > I've played with setting HCR how I want it, and it looks like I can > handle the trap in the vm_event function of vm.c, under the > seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the > trap. I need to emulate the trapped instruction, right? Is there a > particularly good place to do that or is it already implemented? > > If I switch to using HSTR to trap, where should that be handled? Also > in the seL4_Fault_VCPUFault case? > > On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark <undefinedsp...@gmail.com> wrote: >> Thanks Anna. That is great. Is there a quick and easy way to get up >> and running with hypercalls on ARM? >> >> On Mon, Jun 12, 2017 at 8:17 PM, <anna.ly...@data61.csiro.au> wrote: >>> Hi Mike, >>> >>> We have some pages on the developer wiki. For x86 there is a pretty >>> comprehensive tutorial on adding a hypercall and more: >>> >>> https://wiki.sel4.systems/CAmkESVM >>> >>> We're starting to develop docs on the ARM vm here: >>> https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty >>> bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, >>> as they are structured differently. >>> >>> Anna. >>> >>> >>> ________________________________________ >>> From: Devel <devel-bounces@sel4.systems> on behalf of Mike Clark >>> <undefinedsp...@gmail.com> >>> Sent: Friday, 9 June 2017 10:56 PM >>> To: Danis, Adrian (Data61, Kensington NSW) >>> Cc: devel@sel4.systems >>> Subject: Re: [seL4] vmm documentation >>> >>> Okay, so I'll start with something more concrete that should help me >>> understand a few things. Let's say I wanted to implement a hypercall >>> and for the purposes of this discussion, let's assume ARM. >>> >>> A user process on the Linux VM can issue a hypercall with the HVC >>> instruction, right? Where would I need to add code to the VMM to >>> handle this hypercall? >>> >>> Also, it is my understanding that certain instructions will cause a >>> trap into the VMM. Where is that handled? >>> >>> Thanks! >>> >>> On Thu, Jun 8, 2017 at 8:10 PM, <adrian.da...@data61.csiro.au> wrote: >>>> Hi Mike, >>>> >>>> Unfortunately we haven't yet written any documentation on the VMM internals >>>> or how it works. You are actually the first person to express interest in >>>> this. Will try to make it a higher priority to write at least a brief >>>> overview of the structure. For now my advice is to be familiar with CAmkES, >>>> have a built version of the VMM so that you can code search for generated >>>> code and then start exploring from either >>>> https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L525 >>>> or >>>> https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main.c#L472 >>>> depending on whether you are asking about the arm or x86 VMM. >>>> >>>> Adrian >>>> >>>> >>>> On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote: >>>> >>>> Is there any documentation on how the VMM works? If I wanted to start >>>> hacking on the VMM and extend its capability, where should I start >>>> looking to learn how it works, etc? >>>> >>>> That might be a pretty broad topic, because there are lots of ways the >>>> VMM can be extended, I'm sure. Broad is fine, until I get things more >>>> figured out. >>>> >>>> _______________________________________________ >>>> Devel mailing list >>>> Devel@sel4.systems >>>> https://sel4.systems/lists/listinfo/devel >>>> >>>> >>> >>> _______________________________________________ >>> Devel mailing list >>> Devel@sel4.systems >>> https://sel4.systems/lists/listinfo/devel > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
