From 825dd3be28357e1e9c1ac580fb527e9ae0934ef7 Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Tue, 5 Sep 2017 11:58:10 +1000 Subject: [PATCH 01/29] update VERSION file to 7.0.0-dev --- VERSION | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VERSION b/VERSION index 412252180..cb65b5c78 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -7.0.0 \ No newline at end of file +7.0.0-dev \ No newline at end of file From 750d040a41ef705585f7fa0024df102da5b29cfb Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Tue, 5 Sep 2017 13:49:54 +1000 Subject: [PATCH 02/29] Add CHANGES file The purpose of this file is to track changes as they are made to the kernel in order make writing release notes easier and tracking source or binary level API breakages. --- CHANGES | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 CHANGES diff --git a/CHANGES b/CHANGES new file mode 100644 index 000000000..22d5edbf1 --- /dev/null +++ b/CHANGES @@ -0,0 +1,33 @@ +Revision history for seL4 + +For more information see the release notes at https://wiki.sel4.systems/ReleaseNotes + +--- +7.0.0-dev + += Changes = + += Upgrade notes = + +--- +7.0.0 2017-09-05 + += Changes = + * Support for building standalone ia32 kernel added + * ia32: Set sensible defaults for FS and GS selectors + * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0 + * More seL4 manual documentation added for aarch64 object invocations + * Default NUM_DOMAINS set to 16 for x86-64 standalone builds + * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change ''' + * Add a CMake based build system + * x86: Increase TCB size for debug builds + * libsel4: x86: Remove nested struct declarations ''' This is a source code level breaking change ''' + * Bugfix: x86: Unmap pages when delete non final frame caps + += Upgrade notes = + * This release is not source compatible with previous releases. + * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types will need to be updated to reflect this change. + * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if VESA BIOS Extensions (VBE) information is being used. + += Known issues = + * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform, which is a non verified configuration of the kernel. We are working on fixing this problem, and will likely do a point release once it is fixed. From ad03c3348cdf60bb0376d94815e16abc807ba704 Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Wed, 6 Sep 2017 14:34:50 +1000 Subject: [PATCH 03/29] Add CHANGES to license ignore --- .licenseignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.licenseignore b/.licenseignore index c8f29ddcf..bd27d2c39 100644 --- a/.licenseignore +++ b/.licenseignore @@ -10,3 +10,4 @@ manual/figs/* .git/* *parsetab.py manual/* +CHANGES From cfb30f34b9aee8d2e5ebb5b7a5f5101f96075cff Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 6 Sep 2017 15:48:35 +1000 Subject: [PATCH 04/29] libsel4: Remove unused argument in seL4_VMEnter syscall This VCPU argument does not make sense given semantics of the VMEnter syscall, and as a result the argument is ignored by the kernel. --- libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h | 4 ++-- libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h index 6484737c5..8d9f99bf7 100644 --- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h +++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h @@ -505,14 +505,14 @@ seL4_Yield(void) #ifdef CONFIG_VTX LIBSEL4_INLINE_FUNC seL4_Word -seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender) +seL4_VMEnter(seL4_Word *sender) { seL4_Word fault; seL4_Word badge; seL4_Word mr0 = seL4_GetMR(0); seL4_Word mr1 = seL4_GetMR(1); - x86_sys_send_recv(seL4_SysVMEnter, vcpu, &badge, 0, &fault, &mr0, &mr1); + x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1); seL4_SetMR(0, mr0); seL4_SetMR(1, mr1); diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h index 58dca067a..32022a7d4 100644 --- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h +++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h @@ -304,7 +304,7 @@ seL4_Yield(void) #ifdef CONFIG_VTX static inline seL4_Word -seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender) +seL4_VMEnter(seL4_Word *sender) { seL4_Word fault; seL4_Word badge; @@ -313,7 +313,7 @@ seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender) seL4_Word mr2 = seL4_GetMR(2); seL4_Word mr3 = seL4_GetMR(3); - x64_sys_send_recv(seL4_SysVMEnter, vcpu, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3); + x64_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3); seL4_SetMR(0, mr0); seL4_SetMR(1, mr1); From 71cde34b4548b7176ea4e7caca63fbd62da1d936 Mon Sep 17 00:00:00 2001 From: Anna Lyons Date: Fri, 8 Sep 2017 11:06:55 +1000 Subject: [PATCH 05/29] Add config option for CONFIG_RESET_CHUNK_BITS The config variable is used in the kernel but no setting was provided prio to this commit. --- Kconfig | 6 ++++++ config.cmake | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/Kconfig b/Kconfig index f35e40054..49da8c730 100644 --- a/Kconfig +++ b/Kconfig @@ -348,6 +348,12 @@ menu "seL4 System Parameters" the kernel checks for pending interrupts (and preempts the currently running syscall if interrupts are pending). + config RESET_CHUNK_BITS + int "Max chunks to reset when clearing memory" + default 8 + help + Maximum size in bits of chunks of memory to zero before checking a preemption point. + config MAX_NUM_BOOTINFO_UNTYPED_CAPS int "Max number of bootinfo untyped caps" default 167 diff --git a/config.cmake b/config.cmake index ce15f61c1..d0cecade1 100644 --- a/config.cmake +++ b/config.cmake @@ -83,6 +83,11 @@ config_string(KernelMaxNumWorkUnitsPerPreemption MAX_NUM_WORK_UNITS_PER_PREEMPTI DEFAULT 100 UNQUOTE ) +config_string(KernelResetChunkBits RESET_CHUNK_BITS + "Maximum size in bits of chunks of memory to zero before checking a preemption point." + DEFAULT 8 + UNQUOTE +) config_string(KernelMaxNumBootinfoUntypedCaps MAX_NUM_BOOTINFO_UNTYPED_CAPS "Max number of bootinfo untyped caps" DEFAULT 230 From 128829a919c4d0924f46133443efe7ad9d3e10a5 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Tue, 12 Sep 2017 15:44:17 +1000 Subject: [PATCH 06/29] x86: Rationalize names of paging structures Changes the name of paging structure entries to more clearly indicate the kind of object they map to. Generally this is changing a `pde_small` to `pde_pt` to indicate that this mapping refers to a page table, removing an inconsistency where `pde_large` indicated that the mapping was for a large page. For the same reason the `ept_pde_4k` type is changed to `ept_pde_pt` type to reflect what is present in the actual entry. `pde_large` is left as 'large' and not explicitly given a size as code common between ia32 and x86-64 manipulates these entities and 'large' is already a used abstraction over the two potential page sizes so there is need to introduce a formal abstraction layer and make the names in the structures more specific. --- .../x86/arch/32/mode/object/structures.bf | 8 +++--- .../x86/arch/64/mode/object/structures.bf | 8 +++--- src/arch/x86/32/kernel/vspace.c | 8 +++--- src/arch/x86/32/kernel/vspace_32paging.c | 4 +-- src/arch/x86/64/kernel/vspace.c | 14 +++++----- src/arch/x86/kernel/ept.c | 26 +++++++++---------- src/arch/x86/kernel/vspace.c | 22 ++++++++-------- src/arch/x86/machine/capdl.c | 4 +-- 8 files changed, 47 insertions(+), 47 deletions(-) diff --git a/include/arch/x86/arch/32/mode/object/structures.bf b/include/arch/x86/arch/32/mode/object/structures.bf index ea220e3f8..67c8eb26f 100644 --- a/include/arch/x86/arch/32/mode/object/structures.bf +++ b/include/arch/x86/arch/32/mode/object/structures.bf @@ -407,7 +407,7 @@ block tss { -- PDs and PTs -block pde_small { +block pde_pt { field_high pt_base_address 20 field avl 3 padding 1 @@ -438,7 +438,7 @@ block pde_large { } tagged_union pde page_size { - tag pde_small 0 + tag pde_pt 0 tag pde_large 1 } @@ -491,7 +491,7 @@ block ept_pde_2m { field read 1 } -block ept_pde_4k { +block ept_pde_pt { padding 32 field_high pt_base_address 20 field avl_cte_depth 3 @@ -504,7 +504,7 @@ block ept_pde_4k { } tagged_union ept_pde page_size { - tag ept_pde_4k 0 + tag ept_pde_pt 0 tag ept_pde_2m 1 } diff --git a/include/arch/x86/arch/64/mode/object/structures.bf b/include/arch/x86/arch/64/mode/object/structures.bf index 1e47b08a7..9621b16a0 100644 --- a/include/arch/x86/arch/64/mode/object/structures.bf +++ b/include/arch/x86/arch/64/mode/object/structures.bf @@ -532,7 +532,7 @@ block pde_large { field present 1 } -block pde_small { +block pde_pt { field xd 1 padding 11 padding 1 @@ -549,7 +549,7 @@ block pde_small { } tagged_union pde page_size { - tag pde_small 0 + tag pde_pt 0 tag pde_large 1 } @@ -605,7 +605,7 @@ block ept_pde_2m { field read 1 } -block ept_pde_4k { +block ept_pde_pt { padding 13 field_high pt_base_address 39 field avl_cte_depth 3 @@ -618,7 +618,7 @@ block ept_pde_4k { } tagged_union ept_pde page_size { - tag ept_pde_4k 0 + tag ept_pde_pt 0 tag ept_pde_2m 1 } diff --git a/src/arch/x86/32/kernel/vspace.c b/src/arch/x86/32/kernel/vspace.c index b690e13b6..38b7232b3 100644 --- a/src/arch/x86/32/kernel/vspace.c +++ b/src/arch/x86/32/kernel/vspace.c @@ -252,7 +252,7 @@ map_kernel_window( #ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER /* Map global page table for the log buffer */ - pde = pde_pde_small_new( + pde = pde_pde_pt_new( pptr_to_paddr(ia32KSGlobalLogPT), /* pt_base_address */ 0, /* avl */ 0, /* accessed */ @@ -278,7 +278,7 @@ map_kernel_window( #endif /* ENABLE_SMP_SUPPORT */ /* map page table of last 4M of virtual address space to page directory */ - pde = pde_pde_small_new( + pde = pde_pde_pt_new( pptr_to_paddr(ia32KSGlobalPT), /* pt_base_address */ 0, /* avl */ 0, /* accessed */ @@ -545,7 +545,7 @@ pde_t CONST makeUserPDELargePage(paddr_t paddr, vm_attributes_t vm_attr, vm_righ pde_t CONST makeUserPDEPageTable(paddr_t paddr, vm_attributes_t vm_attr) { - return pde_pde_small_new( + return pde_pde_pt_new( paddr, /* pt_base_address */ 0, /* avl */ 0, /* accessed */ @@ -576,7 +576,7 @@ pde_t CONST makeUserPDELargePageInvalid(void) pde_t CONST makeUserPDEPageTableInvalid(void) { - return pde_pde_small_new( + return pde_pde_pt_new( 0, /* pt_base_address */ 0, /* avl */ 0, /* accessed */ diff --git a/src/arch/x86/32/kernel/vspace_32paging.c b/src/arch/x86/32/kernel/vspace_32paging.c index 3de4d2314..24e7b08dd 100644 --- a/src/arch/x86/32/kernel/vspace_32paging.c +++ b/src/arch/x86/32/kernel/vspace_32paging.c @@ -113,7 +113,7 @@ map_it_pt_cap(cap_t vspace_cap, cap_t pt_cap) vptr_t vptr = cap_page_table_cap_get_capPTMappedAddress(pt_cap); assert(cap_page_table_cap_get_capPTIsMapped(pt_cap)); - *(pd + (vptr >> seL4_LargePageBits)) = pde_pde_small_new( + *(pd + (vptr >> seL4_LargePageBits)) = pde_pde_pt_new( pptr_to_paddr(pt), /* pt_base_address */ 0, /* avl */ 0, /* accessed */ @@ -143,7 +143,7 @@ map_it_frame_cap(cap_t pd_cap, cap_t frame_cap) assert(cap_frame_cap_get_capFMappedASID(frame_cap) != 0); pd += (vptr >> seL4_LargePageBits); - pt = paddr_to_pptr(pde_pde_small_ptr_get_pt_base_address(pd)); + pt = paddr_to_pptr(pde_pde_pt_ptr_get_pt_base_address(pd)); *(pt + ((vptr & MASK(seL4_LargePageBits)) >> seL4_PageBits)) = pte_new( pptr_to_paddr(frame), /* page_base_address */ 0, /* avl */ diff --git a/src/arch/x86/64/kernel/vspace.c b/src/arch/x86/64/kernel/vspace.c index d3b7fa2dc..618084395 100644 --- a/src/arch/x86/64/kernel/vspace.c +++ b/src/arch/x86/64/kernel/vspace.c @@ -127,7 +127,7 @@ map_kernel_window( 1 /* present */ ); /* put the PT into the PD */ - x64KSGlobalPD[0] = pde_pde_small_new( + x64KSGlobalPD[0] = pde_pde_pt_new( 0, /* xd */ kpptr_to_paddr(x64KSGlobalPT), 0, /* accessed */ @@ -226,7 +226,7 @@ map_kernel_window( ); /* put the PT into the PD */ - x64KSGlobalPDs[BIT(PDPT_INDEX_BITS) - 1][0] = pde_pde_small_new( + x64KSGlobalPDs[BIT(PDPT_INDEX_BITS) - 1][0] = pde_pde_pt_new( 0, /* xd */ kpptr_to_paddr(x64KSGlobalPT), 0, /* accessed */ @@ -501,8 +501,8 @@ map_it_frame_cap(cap_t pd_cap, cap_t frame_cap) assert(pdpte_pdpte_pd_ptr_get_present(pdpt)); pd = paddr_to_pptr(pdpte_pdpte_pd_ptr_get_pd_base_address(pdpt)); pd += GET_PD_INDEX(vptr); - assert(pde_pde_small_ptr_get_present(pd)); - pt = paddr_to_pptr(pde_pde_small_ptr_get_pt_base_address(pd)); + assert(pde_pde_pt_ptr_get_present(pd)); + pt = paddr_to_pptr(pde_pde_pt_ptr_get_pt_base_address(pd)); *(pt + GET_PT_INDEX(vptr)) = pte_new( 0, /* xd */ pptr_to_paddr(pptr), /* page_base_address */ @@ -578,7 +578,7 @@ map_it_pt_cap(cap_t vspace_cap, cap_t pt_cap) pdpt += GET_PDPT_INDEX(vptr); assert(pdpte_pdpte_pd_ptr_get_present(pdpt)); pd = paddr_to_pptr(pdpte_pdpte_pd_ptr_get_pd_base_address(pdpt)); - *(pd + GET_PD_INDEX(vptr)) = pde_pde_small_new( + *(pd + GET_PD_INDEX(vptr)) = pde_pde_pt_new( 0, /* xd */ pptr_to_paddr(pt), /* pt_base_address */ 0, /* accessed */ @@ -871,7 +871,7 @@ pde_t CONST makeUserPDEPageTable(paddr_t paddr, vm_attributes_t vm_attr) { - return pde_pde_small_new( + return pde_pde_pt_new( 0, /* xd */ paddr, /* pt_base_address */ 0, /* accessed */ @@ -904,7 +904,7 @@ makeUserPDELargePageInvalid(void) pde_t CONST makeUserPDEPageTableInvalid(void) { - return pde_pde_small_new( + return pde_pde_pt_new( 0, /* xd */ 0, /* pt_base_addr */ 0, /* accessed */ diff --git a/src/arch/x86/kernel/ept.c b/src/arch/x86/kernel/ept.c index a6a40c850..74f7da576 100644 --- a/src/arch/x86/kernel/ept.c +++ b/src/arch/x86/kernel/ept.c @@ -173,8 +173,8 @@ lookupEPTPTSlot(ept_pml4e_t* pml4, vptr_t vptr) return ret; } - if ((ept_pde_ptr_get_page_size(lu_ret.pdSlot) != ept_pde_ept_pde_4k) || - !ept_pde_ept_pde_4k_ptr_get_read(lu_ret.pdSlot)) { + if ((ept_pde_ptr_get_page_size(lu_ret.pdSlot) != ept_pde_ept_pde_pt) || + !ept_pde_ept_pde_pt_ptr_get_read(lu_ret.pdSlot)) { current_lookup_fault = lookup_fault_missing_capability_new(22); ret.ptSlot = NULL; @@ -182,7 +182,7 @@ lookupEPTPTSlot(ept_pml4e_t* pml4, vptr_t vptr) return ret; } - ept_pte_t *pt = paddr_to_pptr(ept_pde_ept_pde_4k_ptr_get_pt_base_address(lu_ret.pdSlot)); + ept_pte_t *pt = paddr_to_pptr(ept_pde_ept_pde_pt_ptr_get_pt_base_address(lu_ret.pdSlot)); uint32_t index = GET_EPT_PT_INDEX(vptr); ret.ptSlot = pt + index; @@ -620,8 +620,8 @@ EPTPageTableMapped(asid_t asid, vptr_t vaddr, ept_pte_t *pt) return ret; } - if (ept_pde_ptr_get_page_size(find_ret.pdSlot) == ept_pde_ept_pde_4k - && ptrFromPAddr(ept_pde_ept_pde_4k_ptr_get_pt_base_address(find_ret.pdSlot)) == pt) { + if (ept_pde_ptr_get_page_size(find_ret.pdSlot) == ept_pde_ept_pde_pt + && ptrFromPAddr(ept_pde_ept_pde_pt_ptr_get_pt_base_address(find_ret.pdSlot)) == pt) { ret.pml4 = asid_ret.ept; ret.pdSlot = find_ret.pdSlot; ret.status = EXCEPTION_NONE; @@ -642,7 +642,7 @@ unmapEPTPageTable(asid_t asid, vptr_t vaddr, ept_pte_t *pt) lu_ret = EPTPageTableMapped(asid, vaddr, pt); if (lu_ret.status == EXCEPTION_NONE) { - *lu_ret.pdSlot = ept_pde_ept_pde_4k_new( + *lu_ret.pdSlot = ept_pde_ept_pde_pt_new( 0, /* pt_base_address */ 0, /* avl_cte_depth */ 0, /* execute */ @@ -767,8 +767,8 @@ decodeX86EPTPTInvocation( return EXCEPTION_SYSCALL_ERROR; } - if (((ept_pde_ptr_get_page_size(lu_ret.pdSlot) == ept_pde_ept_pde_4k) && - ept_pde_ept_pde_4k_ptr_get_read(lu_ret.pdSlot)) || + if (((ept_pde_ptr_get_page_size(lu_ret.pdSlot) == ept_pde_ept_pde_pt) && + ept_pde_ept_pde_pt_ptr_get_read(lu_ret.pdSlot)) || ((ept_pde_ptr_get_page_size(lu_ret.pdSlot) == ept_pde_ept_pde_2m) && ept_pde_ept_pde_2m_ptr_get_read(lu_ret.pdSlot))) { userError("X86EPTPTMap: Page table already mapped here"); @@ -777,7 +777,7 @@ decodeX86EPTPTInvocation( } paddr = pptr_to_paddr((void*)(cap_ept_pt_cap_get_capPTBasePtr(cap))); - pde = ept_pde_ept_pde_4k_new( + pde = ept_pde_ept_pde_pt_new( paddr,/* pt_base_address */ 0, /* avl_cte_depth */ 1, /* execute */ @@ -944,15 +944,15 @@ decodeX86EPTPageMap( } - if ((ept_pde_ptr_get_page_size(lu_ret.pdSlot) == ept_pde_ept_pde_4k) && - ept_pde_ept_pde_4k_ptr_get_read(lu_ret.pdSlot)) { + if ((ept_pde_ptr_get_page_size(lu_ret.pdSlot) == ept_pde_ept_pde_pt) && + ept_pde_ept_pde_pt_ptr_get_read(lu_ret.pdSlot)) { userError("X86EPTPageMap: Page table already present."); current_syscall_error.type = seL4_DeleteFirst; return EXCEPTION_SYSCALL_ERROR; } if (LARGE_PAGE_BITS != EPT_PD_INDEX_OFFSET && - (ept_pde_ptr_get_page_size(lu_ret.pdSlot + 1) == ept_pde_ept_pde_4k) && - ept_pde_ept_pde_4k_ptr_get_read(lu_ret.pdSlot + 1)) { + (ept_pde_ptr_get_page_size(lu_ret.pdSlot + 1) == ept_pde_ept_pde_pt) && + ept_pde_ept_pde_pt_ptr_get_read(lu_ret.pdSlot + 1)) { userError("X86EPTPageMap: Page table already present."); current_syscall_error.type = seL4_DeleteFirst; return EXCEPTION_SYSCALL_ERROR; diff --git a/src/arch/x86/kernel/vspace.c b/src/arch/x86/kernel/vspace.c index 289d875bb..a3f7669b5 100644 --- a/src/arch/x86/kernel/vspace.c +++ b/src/arch/x86/kernel/vspace.c @@ -626,8 +626,8 @@ lookupPTSlot_ret_t lookupPTSlot(vspace_root_t *vspace, vptr_t vptr) ret.status = pdSlot.status; return ret; } - if ((pde_ptr_get_page_size(pdSlot.pdSlot) != pde_pde_small) || - !pde_pde_small_ptr_get_present(pdSlot.pdSlot)) { + if ((pde_ptr_get_page_size(pdSlot.pdSlot) != pde_pde_pt) || + !pde_pde_pt_ptr_get_present(pdSlot.pdSlot)) { current_lookup_fault = lookup_fault_missing_capability_new(PAGE_BITS + PT_INDEX_BITS); ret.ptSlot = NULL; ret.status = EXCEPTION_LOOKUP_FAULT; @@ -637,7 +637,7 @@ lookupPTSlot_ret_t lookupPTSlot(vspace_root_t *vspace, vptr_t vptr) pte_t* ptSlot; word_t ptIndex; - pt = paddr_to_pptr(pde_pde_small_ptr_get_pt_base_address(pdSlot.pdSlot)); + pt = paddr_to_pptr(pde_pde_pt_ptr_get_pt_base_address(pdSlot.pdSlot)); ptIndex = (vptr >> PAGE_BITS) & MASK(PT_INDEX_BITS); ptSlot = pt + ptIndex; @@ -776,9 +776,9 @@ void unmapPageTable(asid_t asid, vptr_t vaddr, pte_t* pt) } /* check if the PD actually refers to the PT */ - if (! (pde_ptr_get_page_size(lu_ret.pdSlot) == pde_pde_small && - pde_pde_small_ptr_get_present(lu_ret.pdSlot) && - (pde_pde_small_ptr_get_pt_base_address(lu_ret.pdSlot) == pptr_to_paddr(pt)))) { + if (! (pde_ptr_get_page_size(lu_ret.pdSlot) == pde_pde_pt && + pde_pde_pt_ptr_get_present(lu_ret.pdSlot) && + (pde_pde_pt_ptr_get_pt_base_address(lu_ret.pdSlot) == pptr_to_paddr(pt)))) { return; } @@ -985,8 +985,8 @@ exception_t decodeX86FrameInvocation( pdeSlot = lu_ret.pdSlot; /* check for existing page table */ - if ((pde_ptr_get_page_size(pdeSlot) == pde_pde_small) && - (pde_pde_small_ptr_get_present(pdeSlot))) { + if ((pde_ptr_get_page_size(pdeSlot) == pde_pde_pt) && + (pde_pde_pt_ptr_get_present(pdeSlot))) { current_syscall_error.type = seL4_DeleteFirst; return EXCEPTION_SYSCALL_ERROR; @@ -1123,8 +1123,8 @@ exception_t decodeX86FrameInvocation( } pdeSlot = lu_ret.pdSlot; - if ((pde_ptr_get_page_size(pdeSlot) == pde_pde_small) && - (pde_pde_small_ptr_get_present(pdeSlot))) { + if ((pde_ptr_get_page_size(pdeSlot) == pde_pde_pt) && + (pde_pde_pt_ptr_get_present(pdeSlot))) { current_syscall_error.type = seL4_DeleteFirst; return EXCEPTION_SYSCALL_ERROR; @@ -1321,7 +1321,7 @@ decodeX86PageTableInvocation( return EXCEPTION_SYSCALL_ERROR; } - if (((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_small) && pde_pde_small_ptr_get_present(pdSlot.pdSlot)) || + if (((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_pt) && pde_pde_pt_ptr_get_present(pdSlot.pdSlot)) || ((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_large) && pde_pde_large_ptr_get_present(pdSlot.pdSlot))) { current_syscall_error.type = seL4_DeleteFirst; diff --git a/src/arch/x86/machine/capdl.c b/src/arch/x86/machine/capdl.c index 534635d3f..534d64086 100644 --- a/src/arch/x86/machine/capdl.c +++ b/src/arch/x86/machine/capdl.c @@ -127,8 +127,8 @@ static void sendPD(unsigned long address) for (i = 0; i < PD_READ_SIZE; i++) { pde_t pde = start[i]; exists = 1; - if (pde_get_page_size(pde) == pde_pde_small && (pde_pde_small_get_pt_base_address(pde) == 0 || - !pde_pde_small_get_present(pde) || !pde_pde_small_get_super_user(pde))) { + if (pde_get_page_size(pde) == pde_pde_pt && (pde_pde_pt_get_pt_base_address(pde) == 0 || + !pde_pde_pt_get_present(pde) || !pde_pde_pt_get_super_user(pde))) { exists = 0; } else if (pde_get_page_size(pde) == pde_pde_large && (pde_pde_large_get_page_base_address(pde) == 0 || !pde_pde_large_get_present(pde) || !pde_pde_large_get_super_user(pde))) { From 8bd43ab7c1a0b8803e63f411ed7b0806b9a95e49 Mon Sep 17 00:00:00 2001 From: Bamboo Date: Tue, 12 Sep 2017 06:15:34 +0000 Subject: [PATCH 07/29] [STYLE_FIX] --- src/arch/x86/machine/capdl.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/arch/x86/machine/capdl.c b/src/arch/x86/machine/capdl.c index 534d64086..f0c333d17 100644 --- a/src/arch/x86/machine/capdl.c +++ b/src/arch/x86/machine/capdl.c @@ -128,7 +128,7 @@ static void sendPD(unsigned long address) pde_t pde = start[i]; exists = 1; if (pde_get_page_size(pde) == pde_pde_pt && (pde_pde_pt_get_pt_base_address(pde) == 0 || - !pde_pde_pt_get_present(pde) || !pde_pde_pt_get_super_user(pde))) { + !pde_pde_pt_get_present(pde) || !pde_pde_pt_get_super_user(pde))) { exists = 0; } else if (pde_get_page_size(pde) == pde_pde_large && (pde_pde_large_get_page_base_address(pde) == 0 || !pde_pde_large_get_present(pde) || !pde_pde_large_get_super_user(pde))) { From d6ebe94d99491cee4e5dcff29754f7c57478ca19 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Wed, 13 Sep 2017 11:55:45 +1000 Subject: [PATCH 08/29] Remove CONFIG_IOMMU for x86_64 This brings x86_64 in line with what is being verified. --- configs/pc99/autoconf.h | 1 - 1 file changed, 1 deletion(-) diff --git a/configs/pc99/autoconf.h b/configs/pc99/autoconf.h index 12f31c248..148c28b2e 100644 --- a/configs/pc99/autoconf.h +++ b/configs/pc99/autoconf.h @@ -150,7 +150,6 @@ #define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1 #define CONFIG_LIB_SEL4_MUSLC_SYS 1 #define CONFIG_HAVE_LIB_SEL4_TEST 1 -#define CONFIG_IOMMU 1 #define CONFIG_LIB_MUSL_C 1 #define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 #define CONFIG_USER_CFLAGS "" From 0df69aa1d1349d5b4df68e29db563848e41a8d08 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 13 Sep 2017 14:54:36 +1000 Subject: [PATCH 09/29] Use prefix consistent with proof tools for verified configurations This matches the name with the L4V_ARCH variable in the verification tools and will allow, as additional configurations are added, selecting the correct configuration directly based on the configured L4V_ARCH from those tools. --- configs/{arm_verified.cmake => ARM_verified.cmake} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename configs/{arm_verified.cmake => ARM_verified.cmake} (100%) diff --git a/configs/arm_verified.cmake b/configs/ARM_verified.cmake similarity index 100% rename from configs/arm_verified.cmake rename to configs/ARM_verified.cmake From 4cf498093d47e83750f82ec4e6464094676d9a51 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 13 Sep 2017 14:57:32 +1000 Subject: [PATCH 10/29] Add verified configuration for arm with hypervisor extensions --- configs/ARM_HYP_verified.cmake | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 configs/ARM_HYP_verified.cmake diff --git a/configs/ARM_HYP_verified.cmake b/configs/ARM_HYP_verified.cmake new file mode 100644 index 000000000..b8ba711b7 --- /dev/null +++ b/configs/ARM_HYP_verified.cmake @@ -0,0 +1,29 @@ +# +# 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) +# + +set(KernelARMPlatform "jetson" CACHE STRING "") +set(KernelArch "arm" CACHE STRING "") +set(KernelArmSel4Arch "arm_hyp" CACHE STRING "") +set(KernelArmHypervisorSupport ON CACHE BOOL "") +set(KernelVerificationBuild ON CACHE BOOL "") +set(KernelIPCBufferLocation "threadID_register" CACHE STRING "") +set(KernelMaxNumNodes "1" CACHE STRING "") +set(KernelOptimisation "-O2" CACHE STRING "") +set(KernelRetypeFanOutLimit "256" CACHE STRING "") +set(KernelBenchmarks "none" CACHE STRING "") +set(KernelDangerousCodeInjection OFF CACHE BOOL "") +set(KernelFastpath ON CACHE BOOL "") +set(KernelPrinting OFF CACHE BOOL "") +set(KernelNumDomains 16 CACHE STRING "") +set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") +set(KernelRootCNodeSizeBits 19 CACHE STRING "") +set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "") From 96bff79f1c33bedb603b90b907a57962b683641a Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 13 Sep 2017 17:38:50 +1000 Subject: [PATCH 11/29] Add verified configuration for x64 --- configs/X64_verified.cmake | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 configs/X64_verified.cmake diff --git a/configs/X64_verified.cmake b/configs/X64_verified.cmake new file mode 100644 index 000000000..04ea21b4e --- /dev/null +++ b/configs/X64_verified.cmake @@ -0,0 +1,26 @@ +# +# 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) +# + +set(KernelArch "x86" CACHE STRING "") +set(KernelX86Sel4Arch "x86_64" CACHE STRING "") +set(KernelVerificationBuild ON CACHE BOOL "") +set(KernelMaxNumNodes "1" CACHE STRING "") +set(KernelOptimisation "-O2" CACHE STRING "") +set(KernelRetypeFanOutLimit "256" CACHE STRING "") +set(KernelBenchmarks "none" CACHE STRING "") +set(KernelDangerousCodeInjection OFF CACHE BOOL "") +set(KernelFastpath ON CACHE BOOL "") +set(KernelPrinting OFF CACHE BOOL "") +set(KernelNumDomains 16 CACHE STRING "") +set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") +set(KernelRootCNodeSizeBits 19 CACHE STRING "") +set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "") From 09ba9fc887491770af303909d4a08ac7718cf86e Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Thu, 14 Sep 2017 14:47:59 +1000 Subject: [PATCH 12/29] pc99: Prevent zero sized array when IOMMU disabled An array is declared of size CONFIG_MAX_RMRR_ENTRIES, and if this is zero (such as when the IOMMU is disabled), then it becomes a zero sized array, which is a GNU C extension. --- src/plat/pc99/config.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plat/pc99/config.cmake b/src/plat/pc99/config.cmake index 253a2f25b..6a4ce4138 100644 --- a/src/plat/pc99/config.cmake +++ b/src/plat/pc99/config.cmake @@ -22,7 +22,7 @@ config_string(KernelMaxRMRREntries MAX_RMRR_ENTRIES "Setsthe maximum number of Reserved Memory Region Reporting structures we support \ recording from the ACPI tables" DEFAULT 32 - DEPENDS "KernelIOMMU" DEFAULT_DISABLED 0 + DEPENDS "KernelIOMMU" DEFAULT_DISABLED 1 UNQUOTE ) From 76dd101fe1dcb1e882dbdf6834d3b04c1b294b4b Mon Sep 17 00:00:00 2001 From: Kent McLeod Date: Mon, 18 Sep 2017 11:28:33 +1000 Subject: [PATCH 13/29] manual: fix python script to be python3 compatible --- manual/tools/parse_doxygen_xml.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/manual/tools/parse_doxygen_xml.py b/manual/tools/parse_doxygen_xml.py index beb79074d..a7d0b171c 100755 --- a/manual/tools/parse_doxygen_xml.py +++ b/manual/tools/parse_doxygen_xml.py @@ -20,6 +20,8 @@ import sys import os import re from bs4 import BeautifulSoup +import six + # Dict mapping characters to their escape sequence in latex LATEX_ESCAPE_PATTERNS = { "_": "\\_", @@ -53,7 +55,7 @@ def get_text(soup, escape=True): if isinstance(soup, str): string = soup - elif isinstance(soup, unicode): + elif isinstance(soup, six.string_types): string = str(soup) elif soup.string: string = str(soup.string) @@ -154,11 +156,11 @@ def parse_detailed_desc(parent, ref_dict): names = parent.find_all('declname') # the first type is the return type - ret_type = types_iter.next() + ret_type = six.next(types_iter) # the rest are parameters for n in names: - param_type = types_iter.next().text + param_type = six.next(types_iter).text if param_type == "void": continue params[str(n.text)] = {"type": param_type} From d3c9f36d946ce1f4bb3e4ebdc217e8b1a8122e50 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Thu, 7 Sep 2017 11:34:05 +1000 Subject: [PATCH 14/29] manual: Correct asidpool assign label Fixes an inconsistency between manual_label for the x86 AsidPool_Assign invocation and its reference in the manual. This makes the x86 align with the ARM name. --- libsel4/arch_include/x86/interfaces/sel4arch.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml index 43fce385d..94fd65afb 100644 --- a/libsel4/arch_include/x86/interfaces/sel4arch.xml +++ b/libsel4/arch_include/x86/interfaces/sel4arch.xml @@ -239,7 +239,7 @@ - + Assign an ASID pool. From a1a6390d650632d06b403bf267dc4d2aca59d7a1 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Thu, 7 Sep 2017 16:13:28 +1000 Subject: [PATCH 15/29] manual: Correct VCPU_SetEPTRoot invocation parameter name Changes the parameter name to match the actual object that should be passed, as required by the kernel code. --- libsel4/arch_include/x86/interfaces/sel4arch.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml index 94fd65afb..237b4d2fa 100644 --- a/libsel4/arch_include/x86/interfaces/sel4arch.xml +++ b/libsel4/arch_include/x86/interfaces/sel4arch.xml @@ -369,7 +369,7 @@ - + From 09443ed0c1c6c18b4a47fa04b19d001b24922db2 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Fri, 8 Sep 2017 11:35:50 +1000 Subject: [PATCH 16/29] manual: Correct parameter type of VCPU_EnableIOPort invocation Type was previously `seL4_CNode`, which is incorrect as the invocation is taking a cptr to an I/O port, not a cnode, this change reflects that. --- libsel4/arch_include/x86/interfaces/sel4arch.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml index 237b4d2fa..5ec8025bb 100644 --- a/libsel4/arch_include/x86/interfaces/sel4arch.xml +++ b/libsel4/arch_include/x86/interfaces/sel4arch.xml @@ -387,7 +387,7 @@ - + From 567127defeedfedd3275a49469765a4baafd0ce2 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 6 Sep 2017 17:24:12 +1000 Subject: [PATCH 17/29] manual: Expand parts of the x86 virtualisation documentation This provides documentation for kernel design of the x86 virtualisation, the additional syscall and object invocations. The ARM design is not fully expanded. --- .../arch_include/x86/interfaces/sel4arch.xml | 211 +++++++++++++++--- libsel4/include/sel4/syscalls.h | 61 +++++ manual/Makefile | 1 + manual/parts/api.tex | 4 + manual/parts/threads.tex | 65 ++++++ 5 files changed, 309 insertions(+), 33 deletions(-) diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml index 5ec8025bb..8c9590335 100644 --- a/libsel4/arch_include/x86/interfaces/sel4arch.xml +++ b/libsel4/arch_include/x86/interfaces/sel4arch.xml @@ -368,61 +368,206 @@ - - + + + Set the EPT root of a thread + + + See . + + - + - + + Bind TCB to VCPU + + + Configures the one-to-one binding of a VCPU and TCB, overwriting any previous binding + in both. See . + + - - - + + + Read VMCS field from the hardware + + + Thin wrapper around the instruction that is performed on the + VMCS region that is part of the VCPU object. After validating that a legal + field is requested the value of `vmread` is returned directly in the result. + + + A struct that contains a + , which holds the return result of the instruction, + and . See for a description + of the message register and tag contents upon error. + + + - - - - + + + Write VMCS field to the hardware + + + Thin wrapper around the `vmwrite` instruction that is performed on the + VMCS region that is part of the VCPU object. As well as validating that + a legal field is requested, the value may be modified to ensure any + bits that are fixed in the hardware are correct, and that any features + required for kernel correctness are not disabled (see ). + + The final value written to the hardware is returned and can be compared + to the input parameter to determine what bits the kernel changed. + + + A struct that contains a + , which holds the final value written with the instruction, + and . See for a description + of the message register and tag contents upon error. + + + + - - - + manual_name="Enable IO Port" manual_label="vcpu_enableioport"> + + Enable I/O port range in guest execution + + + Enables a range of I/O ports for direct access by the execution mode in + the . The requested port range must be a sub range + of the provided I/O port capability. + + This also establishes a link between the provided I/O port capability and + the , see for details. + + + + - - + + Disable I/O port range in privileged execution + + + Disable a range of I/O ports for direct access by the execution mode in + the . + + + - + + Set guest mode registers to the fields of a given + + + Sets the guest mode registers, which is any registers not already part of the VMCS. + + - + - - - + + Map an EPT page directory page table. + + + See + + + + + + VM attributes for the mapping. Possible values for this type are + given in + + + + + + Unmap an EPT page directory page table. + + + See + - - + - - - + + Map an EPT page directory. + + + See + + + + + + VM attributes for the mapping. Possible values for this type are + given in + + + + + + Unmap an EPT page directory. + + + See + - - + - - - + + Map an EPT page table. + + + See + + + + + + VM attributes for the mapping. Possible values for this type are + given in + + + + + + Unmap an EPT page table. + + + See + - diff --git a/libsel4/include/sel4/syscalls.h b/libsel4/include/sel4/syscalls.h index 6605c4387..44f63d730 100644 --- a/libsel4/include/sel4/syscalls.h +++ b/libsel4/include/sel4/syscalls.h @@ -474,6 +474,67 @@ seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr); #endif /** @} */ +#ifdef CONFIG_ARCH_X86 +/** + * @defgroup X86SystemCalls X86 System Calls + * @{ + */ + +#ifdef CONFIG_VTX +/** + * @xmlonly @endxmlonly + * @brief Change current thread to execute from its bound VCPU + * + * Changes the execution mode of the current thread from normal TCB execution, to + * guest execution using its bound VCPU. + * @xmlonly + * For details on VCPUs and execution modes see . + * @endxmlonly + * + * Invoking `seL4_VMEnter` is similar to replying to a fault in that updates to the registers + * can be given in the message, but unlike a fault no message info + * @xmlonly + * (see ) + * @endxmlonly + * is sent as the registers are not optional and the number that must be sent is fixed. + * The mapping of hardware register to message register is + * - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode + * - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls + * - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls + * + * On return these same three message registers will be filled with the values at the point + * that the privlidged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT` + * then the following additional message registers will be filled out + * - `SEL4_VMENTER_FAULT_REASON_MR` + * - `SEL4_VMENTER_FAULT_QUALIFICATION_MR` + * - `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR` + * - `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR` + * - `SEL4_VMENTER_FAULT_RFLAGS_MR` + * - `SEL4_VMENTER_FAULT_GUEST_INT_MR` + * - `SEL4_VMENTER_FAULT_CR3_MR` + * - `SEL4_VMENTER_FAULT_EAX` + * - `SEL4_VMENTER_FAULT_EBX` + * - `SEL4_VMENTER_FAULT_ECX` + * - `SEL4_VMENTER_FAULT_EDX` + * - `SEL4_VMENTER_FAULT_ESI` + * - `SEL4_VMENTER_FAULT_EDI` + * - `SEL4_VMENTER_FAULT_EBP` + * + * @param[out] sender The address to write sender information to. + * If the syscall returns due to receiving a notification + * on the bound notification then the sender information + * is the badge of the notification capability that was invoked. + * This parameter is ignored if `NULL`. + * @return `SEL4_VMENTER_RESULT_NOTIF` if a notification was received or `SEL4_VMENTER_RESULT_FAULT` + * if the guest mode execution faulted for any reason + */ +LIBSEL4_INLINE_FUNC seL4_Word +seL4_VMEnter(seL4_Word *sender); +#endif + +/** @} */ +#endif + /** @} */ #endif /* __LIBSEL4_SYSCALLS_H */ diff --git a/manual/Makefile b/manual/Makefile index 05b3b4e1e..907761266 100644 --- a/manual/Makefile +++ b/manual/Makefile @@ -129,6 +129,7 @@ ${GeneratedLatexDir}/%.tex: ${DoxygenXml}/group__%.xml generated-latex: ${GeneratedLatexDir}/GeneralSystemCalls.tex \ ${GeneratedLatexDir}/DebuggingSystemCalls.tex \ ${GeneratedLatexDir}/BenchmarkingSystemCalls.tex \ + ${GeneratedLatexDir}/X86SystemCalls.tex \ ${GeneratedLatexDir}/ObjectApi.tex \ ${GeneratedLatexDir}/ObjectApiX86.tex \ ${GeneratedLatexDir}/ObjectApiArm.tex \ diff --git a/manual/parts/api.tex b/manual/parts/api.tex index c4353c081..07074e57c 100644 --- a/manual/parts/api.tex +++ b/manual/parts/api.tex @@ -256,6 +256,10 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request. \inputgeneratedapidoc{BenchmarkingSystemCalls} \clearpage +\subsection{X86 System Calls} +\inputgeneratedapidoc{X86SystemCalls} +\clearpage + \section{Architecture-Independent Object Methods} \label{sec:kobj_api} \inputgeneratedapidoc{ObjectApi} diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index d99f6ae71..2512069b3 100644 --- a/manual/parts/threads.tex +++ b/manual/parts/threads.tex @@ -487,4 +487,69 @@ The caller must possess a \obj{Domain} cap and the thread's \obj{TCB} cap. The initial thread starts with a \obj{Domain} cap (see \autoref{sec:messageinfo}). +\section{Virtualisation} +\label{sec:virt} +Hardware execution virtualisation is supported on specific arm and x86 platforms. The interface is exposed through a series +of kernel objects, invocations and syscalls that allow the user to take advantage of hardware +virtualisation features. + +Hardware virtualisation allows for a thread to perform instructions and operations as if it were +running at a higher privilege level. As higher privilege levels typically have access to +additional machine registers and other pieces of state a \obj{VCPU} object is introduced to act +as storage for this state. For simplicity we refer to this virtualised higher privileged level as +'guest mode'. \obj{VCPU}s are bound in a one-to-one relationship with a \obj{TCB} in order +to provide a thread with this ability to run in higher privilege mode. See the section on +ARM or x86 for more precise details. + +\obj{VCPU} objects also have additional, architecture specific, invocations for manipulating +the additional state or other virtualisation controls provided by the hardware. Binding of +a \obj{VCPU} to a \obj{TCB} is done by an invocation on the \obj{VCPU} only, and not the \obj{TCB}. + +The provided objects and invocations are, generally speaking, the thinnest possible shim over +the underlying hardware primitives and operations. As a result an in depth familiarity with +the underlying architecture specific harwdare mechanisms is required to use these objects, and +such familiarity is therefore assumed in description. + +\subsection{ARM} + +When a \obj{TCB} has a bound \obj{VCPU} it is allowed to have the mode portion of the +\texttt{cpsr} register set to values other than \texttt{user}. Specifically it may have any value other than +\texttt{hypervisor}. + +TODO: this section needs more detail + +\subsection{x86} + +A \obj{TCB} with a bound \obj{VCPU} has two execution modes; one is the original thread just as +if there was no bound \obj{VCPU}, and the other is the guest mode execution using the +\obj{VCPU}. Switching from regular execution mode into the guest execution mode is +done by using the \apifunc{seL4\_VMEnter}{sel4_vmenter} syscall. Executing this syscall causes the thread, whenever +it is scheduled thereafter, to execute using the higher privlidged mode controlled by the \obj{VCPU}. +Should the guest execution mode generate any kind of fault, or if a message arrives +on the \obj{TCB}s bound notification, the \obj{TCB} will be switched back to regular mode +and the \apifunc{seL4\_VMEnter}{sel4_vmenter} syscall will return with a message indicating the reason for return. + +\obj{VCPU} state and execution is controlled through the \apifunc{seL4\_VCPU\_ReadVMCS}{x86_vcpu_readvmcs} +and \apifunc{seL4\_VCPU\_WriteVMCS}{x86_vcpu_writevmcs} invocations. +These are very thin wrappers around the hardware \texttt{vmread} and \texttt{vmwrite} instructions and the kernel +merely does enough validation on the parameters to ensure the \obj{VCPU} is not configured +to run in such a way as to violate any kernel properties. For example, it is not possible to +disable the use of External Interrupt Exiting, as this would prevent the kernel from receiving +timer interrupts and allow the thread to monopolise CPU time. + +Memory access of the guest execution mode is controlled by requiring the use of Extended +Page Tables (EPT). A series of EPT related paging structure objects (\obj{EPTPML4}, \obj{EPTPDPT}, \obj{EPTPD}, \obj{EPTPT}) +exist and are manipulated in exactly the same manner as the objects for the regular virtual +address space. Once constructed a \obj{TCB} can be given an \obj{EPTPML4} as an EPT root with \apifunc{seL4\_TCB\_SetEPTRoot}{x86_set_eptroot}, +which serves as the vspace root when executing in guest mode, with the vspace root set +with \apifunc{seL4\_TCB\_SetSPace}{tcb_setspace} or \apifunc{seL4\_TCB\_Configure}{tcb_configure} +continuing to provide translation when the TCB is executing in its normal mode. + +Direct access to I/O ports can be given to the privlidged execution mode through the +\apifunc{seL4\_X86\_VCPU\_EnableIOPort}{x86_vcpu_enableioport} invocation and allows the provided I/O port capability to be +linked to the VCPU, and a subset of its I/O port range to be made accessible to the \obj{VCPU}. +Linking means that an I/O port capability can only be used in a single \apifunc{seL4\_X86\_VCPU\_EnableIOPort}{x86_vcpu_enableioport} +invocation and a second invocation will undo the previous one. The link also means that +if the I/O port capability is deleted for any reason the access will be correspondingly removed +from the \obj{VCPU}. From eac4f6bfa2c22360da5900a91e7a3730dcd1263e Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 20 Sep 2017 14:22:13 +1000 Subject: [PATCH 18/29] proof: Defer theory dependencies to isabelle Instead of explicitly depending on Kernel_C.thy prior to generating proofs, this removes the dependency check and leaves isabelle to check the dependency upon import. --- tools/helpers.cmake | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/helpers.cmake b/tools/helpers.cmake index c8990189d..3a249f4ac 100644 --- a/tools/helpers.cmake +++ b/tools/helpers.cmake @@ -133,7 +133,6 @@ function(GenThyBFTarget args target_name target_file pbf_path pbf_target prunes foreach(prune IN LISTS prunes) list(APPEND args "--prune" "${prune}") endforeach() - list(APPEND deps "${CSPEC_DIR}/Kernel_C.thy" ${prunes}) GenBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}") endfunction(GenThyBFTarget) From 1138d6ab34f174a943aa155073122fe473338c5f Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 20 Sep 2017 14:25:49 +1000 Subject: [PATCH 19/29] proof: Do not check for KernelState_C.thy in CSPEC_DIR path --- config.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/config.cmake b/config.cmake index d0cecade1..6347358ad 100644 --- a/config.cmake +++ b/config.cmake @@ -18,7 +18,7 @@ set(configure_string "") config_set(KernelIsMaster KERNEL_MASTER ON) # Proof based configuration variables -find_path(CSPEC_DIR KernelState_C.thy CMAKE_FIND_ROOT_PATH_BOTH) +set(CSPEC_DIR "." CACHE PATH "") set(SKIP_MODIFIES ON CACHE INTERNAL "") set(TOPLEVELTYPES "cte_C;tcb_C;endpoint_C;notification_C;asid_pool_C;pte_C;pde_C;user_data_C;user_data_device_C" CACHE INTERNAL "") set(SORRY_BITFIELD_PROOFS OFF CACHE INTERNAL "") From 064428781823132c5b03f93dc7bba3e61d0914c0 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 20 Sep 2017 14:26:09 +1000 Subject: [PATCH 20/29] proof: Do not override proof variables Using the `INTERNAL` attribute implied `FORCE` overriding any value the user may have set for these. This was not the intention, and they should merely set a `CACHE` value if one does not already exist. --- config.cmake | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/config.cmake b/config.cmake index 6347358ad..916d83c51 100644 --- a/config.cmake +++ b/config.cmake @@ -19,9 +19,9 @@ config_set(KernelIsMaster KERNEL_MASTER ON) # Proof based configuration variables set(CSPEC_DIR "." CACHE PATH "") -set(SKIP_MODIFIES ON CACHE INTERNAL "") -set(TOPLEVELTYPES "cte_C;tcb_C;endpoint_C;notification_C;asid_pool_C;pte_C;pde_C;user_data_C;user_data_device_C" CACHE INTERNAL "") -set(SORRY_BITFIELD_PROOFS OFF CACHE INTERNAL "") +set(SKIP_MODIFIES ON CACHE BOOL "") +set(TOPLEVELTYPES "cte_C;tcb_C;endpoint_C;notification_C;asid_pool_C;pte_C;pde_C;user_data_C;user_data_device_C" CACHE STRING "") +set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "") find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH) set(force FORCE) if(KernelVerificationBuild) From c57ea388747e6e66be6277b231772446ab4ea7d2 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 May 2017 11:13:40 +1000 Subject: [PATCH 21/29] tools bitfield_gen: use generic base instead of word32 in proofs --- tools/bitfield_gen.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index 1e528ae0d..d7693fe92 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -679,7 +679,7 @@ done'''], '''lemma %(name)s_ptr_words_aligned: "c_guard (p::%(name)s_C ptr) \ ptr_aligned ((Ptr &(p\[''words_C'']))::''' \ - '''((word32[%(words)d]) ptr))"''', + '''((word%(base)d[%(words)d]) ptr))"''', ''' apply(fastforce intro:c_guard_ptr_aligned_fl simp:typ_uinfo_t_def) done'''], @@ -687,7 +687,7 @@ done'''], '''lemma %(name)s_ptr_words_ptr_safe: "ptr_safe (p::%(name)s_C ptr) d \ ptr_safe (Ptr &(p\[''words_C''])::''' \ - '''((word32[%(words)d]) ptr)) d"''', + '''((word%(base)d[%(words)d]) ptr)) d"''', ''' apply(fastforce intro:ptr_safe_mono simp:typ_uinfo_t_def) done'''], @@ -1275,7 +1275,8 @@ class TaggedUnion: # Generate struct field pointer proofs substs = {"name": self.name, - "words": self.multiple} + "words": self.multiple, + "base": self.base} print(make_proof('words_NULL_proof', substs, params.sorry), file=output) @@ -2219,7 +2220,8 @@ class Block: # Generate struct field pointer proofs substs = {"name": self.name, - "words": self.multiple} + "words": self.multiple, + "base": self.base} print(make_proof('words_NULL_proof', substs, params.sorry), file=output) From 0a99d7d4d87da3cd3ae3f004ad5cfd2c82abcb62 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 May 2017 11:24:41 +1000 Subject: [PATCH 22/29] tools bitfield_gen: remove obsolete mask comments (These masks existed in earlier versions of the bitfield proofs, removed because the statements were stronger without them.) --- tools/bitfield_gen.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index d7693fe92..f6c4eed43 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -584,7 +584,7 @@ def ptr_get_template(ptrname): return ptr_basic_template('get_%(field)s', ptrname, '\%(ret_name)s :== ', '', '''\\%(ret_name)s = ''' \ '''%(name)s_CL.%(field)s_CL ''' \ - '''(%(name)s_lift (%(access_path)s))\''') # AND %(mask)s + '''(%(name)s_lift (%(access_path)s))\''') def ptr_set_template(name, ptrname): return ptr_basic_template(name, ptrname, '', ', \v', @@ -641,7 +641,7 @@ def ptr_union_get_template(ptrname): '\ %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s', '''\\%(ret_name)s = ''' \ '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ - '''(%(name)s_%(block)s_lift %(access_path)s)\''') # AND %(mask)s --- given by _lift? + '''(%(name)s_%(block)s_lift %(access_path)s)\''') def ptr_union_set_template(ptrname): return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \v', @@ -754,7 +754,7 @@ done'''], '''PROC %(name)s_get_%(field)s(\%(name)s) \\%(ret_name)s = ''' \ '''%(name)s_CL.%(field)s_CL ''' \ - '''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\"''', # AND %(mask)s + '''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\"''', ''' apply(rule allI, rule conseqPre, vcg) apply(clarsimp) apply(simp add:%(name)s_lift_def @@ -1028,7 +1028,7 @@ done'''], \\%(ret_name)s = ''' \ '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ '''(%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s)''' \ - '''\"''', # AND %(mask)s + '''\"''', ''' apply(rule allI, rule conseqPre, vcg) apply(clarsimp simp:guard_simps) apply(simp add:%(name)s_%(block)s_lift_def) From 38ba9e405b5f95695e46a993b2d5012ad973140f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 May 2017 11:44:03 +1000 Subject: [PATCH 23/29] tools bitfield_gen: simplify theory imports; conform to style --- tools/bitfield_gen.py | 36 ++++++++++++++---------------------- 1 file changed, 14 insertions(+), 22 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index f6c4eed43..87b1820dd 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -2684,9 +2684,11 @@ if __name__ == '__main__': if options.hol_defs: # Fetch kernel if options.multifile_base is None: - print("theory %s_defs imports \"%s/KernelState_C\" begin" % ( - module_name, os.path.relpath(options.cspec_dir, + print("theory %s_defs" % module_name, file=out_file) + print("imports \"%s/KernelState_C\"" % ( + os.path.relpath(options.cspec_dir, os.path.dirname(out_file.filename))), file=out_file) + print("begin", file=out_file) print(file=out_file) print(defs_global_lemmas, file=out_file) @@ -2697,9 +2699,9 @@ if __name__ == '__main__': print("end", file=out_file) else: - print("theory %s_defs imports" % module_name, - file=out_file) - print("\"%s/KernelState_C\"" % ( + print("theory %s_defs" % module_name, file=out_file) + print("imports", file=out_file) + print(" \"%s/KernelState_C\"" % ( os.path.relpath(options.cspec_dir, os.path.dirname(out_file.filename))), file=out_file) for e in blocks.values() + unions.values(): @@ -2746,14 +2748,10 @@ if __name__ == '__main__': type_map[tp] = (toptp, path) if options.multifile_base is None: - print(\ - "theory %s_proofs imports %s_defs \"%s/KernelState_C\" begin" % ( - module_name, module_name, - os.path.relpath(options.cspec_dir, - os.path.dirname(out_file.filename))), - file=out_file) + print("theory %s_proofs" % module_name, file=out_file) + print("imports %s_defs" % module_name, file=out_file) + print("begin", file=out_file) print(file=out_file) - print(file=out_file) for e in blocks.values() + unions.values(): @@ -2762,12 +2760,8 @@ if __name__ == '__main__': print("end", file=out_file) else: # top types are broken here. - print("theory %s_proofs imports" % module_name, file=out_file) - print(" \"%s/KernelState_C\"" % ( - os.path.relpath(options.cspec_dir, - os.path.dirname(out_file.filename))), - file=out_file) - + print("theory %s_proofs" % module_name, file=out_file) + print("imports", file=out_file) for e in blocks.values() + unions.values(): print(" %s_%s_proofs" % (module_name, e.name), file=out_file) @@ -2783,10 +2777,8 @@ if __name__ == '__main__': e.name + "_proofs" + ".thy") print(("theory %s imports " - + "%s_%s_defs \"%s/KernelState_C\" begin") % ( - submodule_name, base_filename, e.name, - os.path.relpath(options.cspec_dir, - os.path.dirname(out_file.filename))), + + "%s_%s_defs begin") % ( + submodule_name, base_filename, e.name), file=out_file) print(file=out_file) From 3b330f9a6a3d98378a6bbb1faa6922a1d2226b6b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 18 May 2017 12:11:59 +1000 Subject: [PATCH 24/29] tools bitfield_gen: use hex literals in proofs and specs --- tools/bitfield_gen.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index 87b1820dd..f9ab0a487 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -476,7 +476,7 @@ where union_get_tag_def_entry_template = \ '''if ((index (%(name)s_C.words_C %(name)s) %(tag_index)d)''' \ -''' AND %(classmask)d \ %(classmask)d) +''' AND 0x%(classmask)x \ 0x%(classmask)x) then ((index (%(name)s_C.words_C %(name)s) %(tag_index)d)'''\ ''' >> %(tag_shift)d) AND mask %(tag_size)d else ''' @@ -492,7 +492,7 @@ union_get_tag_eq_x_def_header_template = \ "(%(name)s_get_tag c = x) = ((''' union_get_tag_eq_x_def_entry_template = \ -'''if ((x << %(tag_shift)d) AND %(classmask)d \ %(classmask)d) +'''if ((x << %(tag_shift)d) AND 0x%(classmask)x \ 0x%(classmask)x) then ((index (%(name)s_C.words_C c) %(tag_index)d)''' \ ''' >> %(tag_shift)d) AND mask %(tag_size)d else ''' @@ -1610,7 +1610,7 @@ class TaggedUnion: else: mask = (1 << size) - 1 - initialiser += " AND %d" % mask + initialiser += " AND 0x%x" % mask field_inits.append("\n " + initialiser) @@ -2195,7 +2195,7 @@ class Block: else: mask = (1 << size) - 1 - initialiser += " AND %d" % mask + initialiser += " AND 0x%x" % mask field_inits.append(initialiser) From 960881d07eaaaf75c713b9eb79cff47e4190b006 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 19 May 2017 09:20:24 +1000 Subject: [PATCH 25/29] tools bitfield_gen: proof updates for new base + sign-extension mechanism --- tools/bitfield_gen.py | 251 +++++++++++++++++++++++++----------------- 1 file changed, 149 insertions(+), 102 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index f9ab0a487..e135b3960 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -36,10 +36,17 @@ import umm # Whether debugging is enabled (turn on with command line option --debug). DEBUG = False -# parametrisation for the win -return_name = 'ret__unsigned' +# name of locale the bitfield proofs should be in loc_name = 'kernel_all_substitute' +# Isabelle word size suffixes for return value names +ret_name_suffix_map = {8 : '', 16 : '', 32 : '', 64 : '_longlong'} + +def return_name(base): + # name of return value for standard word sizes + return 'ret__unsigned' + ret_name_suffix_map[base] + + # Headers to include depending on which environment we are generating code for. INCLUDES = { 'sel4':['assert.h', 'config.h', 'stdint.h', 'util.h'], @@ -272,21 +279,21 @@ ptr_reader_template = \ writer_template = \ """%(inline)s %(block)s_t CONST -%(block)s_set_%(field)s(%(block)s_t %(block)s, %(type)s v) { +%(block)s_set_%(field)s(%(block)s_t %(block)s, %(type)s v%(base)d) { /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(block)s.words[%(index)d] &= ~0x%(mask)x%(suf)s; - %(block)s.words[%(index)d] |= (v %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; + %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; return %(block)s; }""" ptr_writer_template = \ """%(inline)s void -%(block)s_ptr_set_%(field)s(%(block)s_t *%(block)s_ptr, %(type)s v) { +%(block)s_ptr_set_%(field)s(%(block)s_t *%(block)s_ptr, %(type)s v%(base)d) { /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(block)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s; - %(block)s_ptr->words[%(index)d] |= (v %(w_shift_op)s """ \ + %(block)s_ptr->words[%(index)d] |= (v%(base)d %(w_shift_op)s """ \ """%(shift)d) & 0x%(mask)x; }""" @@ -344,31 +351,31 @@ ptr_union_reader_template = \ union_writer_template = \ """%(inline)s %(union)s_t CONST -%(union)s_%(block)s_set_%(field)s(%(union)s_t %(union)s, %(type)s v) { +%(union)s_%(block)s_set_%(field)s(%(union)s_t %(union)s, %(type)s v%(base)d) { %(assert)s(((%(union)s.words[%(tagindex)d] >> %(tagshift)d) & 0x%(tagmask)x) == %(union)s_%(block)s); /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(union)s.words[%(index)d] &= ~0x%(mask)x%(suf)s; - %(union)s.words[%(index)d] |= (v %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; + %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; return %(union)s; }""" ptr_union_writer_template = \ """%(inline)s void %(union)s_%(block)s_ptr_set_%(field)s(%(union)s_t *%(union)s_ptr, - %(type)s v) { + %(type)s v%(base)d) { %(assert)s(((%(union)s_ptr->words[%(tagindex)d] >> """ \ """%(tagshift)d) & 0x%(tagmask)x) == %(union)s_%(block)s); /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(union)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s; %(union)s_ptr->words[%(index)d] |= """ \ - """(v %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; + """(v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s; }""" tag_reader_header_template = \ @@ -424,23 +431,23 @@ ptr_tag_reader_footer_template = \ tag_writer_template = \ """%(inline)s %(union)s_t CONST -%(union)s_set_%(tagname)s(%(union)s_t %(union)s, %(type)s v) { +%(union)s_set_%(tagname)s(%(union)s_t %(union)s, %(type)s v%(base)d) { /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(union)s.words[%(index)d] &= ~0x%(mask)x%(suf)s; - %(union)s.words[%(index)d] |= (v << %(shift)d) & 0x%(mask)x%(suf)s; + %(union)s.words[%(index)d] |= (v%(base)d << %(shift)d) & 0x%(mask)x%(suf)s; return %(union)s; }""" ptr_tag_writer_template = \ """%(inline)s void -%(union)s_ptr_set_%(tagname)s(%(union)s_t *%(union)s_ptr, %(type)s v) { +%(union)s_ptr_set_%(tagname)s(%(union)s_t *%(union)s_ptr, %(type)s v%(base)d) { /* fail if user has passed bits that we will override */ - %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v) == ((%(sign_extend)d && (v & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); + %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0)); %(union)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s; - %(union)s_ptr->words[%(index)d] |= (v << %(shift)d) & 0x%(mask)x%(suf)s; + %(union)s_ptr->words[%(index)d] |= (v%(base)d << %(shift)d) & 0x%(mask)x%(suf)s; }""" # HOL definition templates @@ -544,6 +551,7 @@ where # HOL proof templates +#FIXME: avoid [simp] struct_lemmas_template = \ ''' lemmas %(name)s_ptr_guards[simp] = @@ -551,6 +559,7 @@ lemmas %(name)s_ptr_guards[simp] = %(name)s_ptr_words_aligned %(name)s_ptr_words_ptr_safe''' +# FIXME: move to global theory defs_global_lemmas = ''' lemma word_sub_mask: "\ w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \ @@ -587,11 +596,11 @@ def ptr_get_template(ptrname): '''(%(name)s_lift (%(access_path)s))\''') def ptr_set_template(name, ptrname): - return ptr_basic_template(name, ptrname, '', ', \v', + return ptr_basic_template(name, ptrname, '', ', \v%(base)d', '''{t. \%(name)s. %(name)s_lift %(name)s = %(name)s_lift (%(access_path)s) \ %(name)s_CL.%(field)s_CL ''' \ - ''':= \<^bsup>s\<^esup>v AND %(mask)s \ \ + ''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \ \ t_hrs_' (globals t) = hrs_mem_update (heap_update (''' + ptrname + ''') %(update_path)s) @@ -644,13 +653,13 @@ def ptr_union_get_template(ptrname): '''(%(name)s_%(block)s_lift %(access_path)s)\''') def ptr_union_set_template(ptrname): - return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \v', + return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \v%(base)d', '\ %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s', '''{t. \%(name)s. ''' \ '''%(name)s_%(block)s_lift %(name)s = %(name)s_%(block)s_lift %(access_path)s ''' \ '''\ %(name)s_%(block)s_CL.%(field)s_CL ''' \ - ''':= \<^bsup>s\<^esup>v AND %(mask)s \ \ + ''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \ \ %(name)s_get_tag %(name)s = scast %(name)s_%(block)s \ t_hrs_' (globals t) = hrs_mem_update (heap_update (''' + ptrname + ''') @@ -731,11 +740,11 @@ done'''], apply(simp add:shift_over_ao_dists mask_def ucast_id) apply(unfold %(name)s_lift_def) apply(simp add:shift_over_ao_dists) - apply(((simp add:word_ao_dist), - (simp add:word_bw_assocs), - (simp add:multi_shift_simps), + apply(((simp add:word_ao_dist)?, + (simp add:word_bw_assocs)?, + (simp add:multi_shift_simps)?, (simp add:mask_def word_size))?) - apply(simp add:word_bw_assocs) + apply(simp add:word_bw_assocs)? done'''], 'ptr_new_spec_direct' : [ @@ -760,17 +769,19 @@ done'''], apply(simp add:%(name)s_lift_def mask_shift_simps guard_simps) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? + apply(simp add:max_word_def word_and_max_word)? done'''], 'set_spec' : [ '''lemma (in ''' + loc_name + ''') %(name)s_set_%(field)s_spec: "\s. \ \ {s} \ret__struct_%(name)s_C :== ''' \ - '''PROC %(name)s_set_%(field)s(\%(name)s, \v) + '''PROC %(name)s_set_%(field)s(\%(name)s, \v%(base)d) \%(name)s_lift \ret__struct_%(name)s_C = ''' \ '''%(name)s_lift \<^bsup>s\<^esup>%(name)s \ ''' \ '''%(name)s_CL.%(field)s_CL ''' \ - ''':= \<^bsup>s\<^esup>v AND %(mask) s \\"''', + ''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \\"''', ''' apply(rule allI, rule conseqPre, vcg) apply(clarsimp simp:guard_simps ucast_id %(name)s_lift_def @@ -778,6 +789,8 @@ done'''], multi_shift_simps word_size word_ao_dist word_bw_assocs NOT_eq) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? + apply(simp add:max_word_def word_and_max_word)? done'''], # where the top level type is the bitfield type --- these are split because they have different proofs @@ -788,8 +801,10 @@ done'''], apply(clarsimp simp:h_t_valid_clift_Some_iff) apply(simp add:guard_simps %(name)s_lift_def + mask_def typ_heap_simps ucast_def) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? apply(simp add:max_word_def word_and_max_word)? done'''], @@ -802,6 +817,8 @@ done'''], apply(frule clift_subtype, simp, simp, simp) apply(simp add:h_val_field_clift' typ_heap_simps) apply(simp add:thread_state_lift_def) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? + apply(simp add:max_word_def word_and_max_word)? apply(simp add:mask_shift_simps)? done'''], @@ -817,7 +834,9 @@ done'''], %(name)s_lift_def typ_heap_simps) - apply(simp add:mask_shift_simps) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? + apply(simp add:max_word_def word_and_max_word)? + apply(simp add:mask_shift_simps)? done'''], 'ptr_set_spec_path' : [ @@ -861,16 +880,18 @@ done'''], apply(simp add:o_def %(name)s_lift_def) (* Solve bitwise arithmetic *) - apply(simp add:mask_shift_simps) + apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs shift_over_ao_dists)? + apply(simp add:max_word_def word_and_max_word)? + apply(simp add:mask_shift_simps)? done'''], 'get_tag_spec' : [ '''lemma (in ''' + loc_name + ''') %(name)s_get_%(tagname)s_spec: "\s. \ \ {s} - \ret__unsigned :== ''' \ + \%(ret_name)s :== ''' \ '''PROC %(name)s_get_%(tagname)s(\%(name)s) - \\ret__unsigned = ''' \ + \\%(ret_name)s = ''' \ '''%(name)s_get_tag \<^bsup>s\<^esup>%(name)s\"''', ''' apply(rule allI, rule conseqPre, vcg) apply(clarsimp) @@ -1051,7 +1072,9 @@ done'''], word_ao_dist word_and_max_word max_word_def - ucast_def) + ucast_def + sign_extend_def' + nth_is_and_neq_0) done'''], 'union_set_spec' : [ @@ -1061,11 +1084,11 @@ done'''], '''\s. %(name)s_get_tag \%(name)s = ''' \ '''scast %(name)s_%(block)s\ \ret__struct_%(name)s_C :== ''' \ - '''PROC %(name)s_%(block)s_set_%(field)s(\%(name)s, \v) + '''PROC %(name)s_%(block)s_set_%(field)s(\%(name)s, \v%(base)d) \%(name)s_%(block)s_lift \ret__struct_%(name)s_C = ''' \ '''%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s \ ''' \ '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ - ''':= \<^bsup>s\<^esup>v AND %(mask)s\ \ + ''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s)\ \ %(name)s_get_tag \ret__struct_%(name)s_C = ''' \ '''scast %(name)s_%(block)s\"''', ''' apply(rule allI, rule conseqPre, vcg) @@ -1078,15 +1101,17 @@ done'''], %(name)s_get_tag_eq_x %(tag_mask_helpers)s %(name)s_%(block)s_update_def - %(name)s_tag_defs) + %(name)s_tag_defs + sign_extend_def' + nth_is_and_neq_0) done'''], 'ptr_union_get_spec_direct' : [ ptr_union_get_template(direct_ptr_name), ''' unfolding ptrval_def apply(rule allI, rule conseqPre, vcg) - apply(clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff - guard_simps mask_shift_simps + apply(clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff guard_simps + mask_shift_simps sign_extend_def' nth_is_and_neq_0 %(name)s_lift_%(block)s %(name)s_%(block)s_lift_def) done '''], @@ -1103,7 +1128,7 @@ done apply(simp add: guard_simps mask_shift_simps) apply(simp add:%(name)s_%(block)s_lift_def) apply(subst %(name)s_lift_%(block)s) - apply simp+ + apply(simp add: mask_def)+ done (* ptr_union_get_spec_path *)'''], @@ -1184,6 +1209,22 @@ def emit_named_ptr_proof(fn_name, params, name, type_map, toptps, prf_prefix, su ['\\_. ' + name] + path) + '(the (ptrval s))' + ')' emit_named(fn_name, params, make_proof(prf_prefix + '_path', substs, params.sorry)) +def field_mask_proof(high, base_bits, base, size): + if high: + if base_bits == base: + # equivalent to below, but nicer in proofs + return "NOT (mask %d)" % (base - size) + else: + return "(mask %d << %d)" % (size, base_bits - size) + else: + return "mask %d" % size + +def sign_extend_proof(high, base_bits, base_sign_extend): + if high and base_sign_extend: + return "sign_extend %d " % (base_bits - 1) + else: + return "" + class TaggedUnion: def __init__(self, name, tagname, classes, tags): self.name = name @@ -1298,7 +1339,7 @@ class TaggedUnion: # Generate get_tag specs substs = {"name": self.name, "tagname": self.tagname, - "ret_name": return_name} + "ret_name": return_name(self.base)} if not params.skip_modifies: emit_named("%(name)s_get_%(tagname)s" % substs, params, @@ -1372,14 +1413,11 @@ class TaggedUnion: if field == self.tagname: continue - if high: - mask = "NOT (mask %d)" % (self.base - size) - else: - mask = "(mask %d)" % size - + mask = field_mask_proof(high, self.base_bits, self.base, size) + sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) field_eq_list.append( - "%s_%s_CL.%s_CL = \<^bsup>s\<^esup>%s AND %s" % \ - (self.name, ref.name, field, field, mask)) + "%s_%s_CL.%s_CL = %s(\<^bsup>s\<^esup>%s AND %s)" % \ + (self.name, ref.name, field, sign_extend, field, mask)) field_eqs = ',\n '.join(field_eq_list) emit_named("%s_%s_new" % (self.name, ref.name), params, @@ -1410,17 +1448,17 @@ class TaggedUnion: if field == self.tagname: continue - if high: - mask = "NOT (mask %d)" % (ref.base - size) - else: - mask = "(mask %d)" % size + mask = field_mask_proof(high, self.base_bits, self.base, size) + sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) - substs = {"name": self.name, \ - "block": ref.name, \ - "field": field, \ - "mask": mask, \ + substs = {"name": self.name, + "block": ref.name, + "field": field, + "mask": mask, + "sign_extend": sign_extend, "tag_mask_helpers" : tag_mask_helpers, - "ret_name": return_name} + "ret_name": return_name(self.base), + "base" : self.base} # Get modifies spec if not params.skip_modifies: @@ -1459,7 +1497,7 @@ class TaggedUnion: "args": ', '.join([ "\ret__struct_%s_C" % self.name, "\%s" % self.name, - "\v"] )}, + "\v%(base)d"] )}, params.sorry)) emit_named("%s_%s_ptr_set_%s" % (self.name, ref.name, field), @@ -1469,7 +1507,7 @@ class TaggedUnion: (self.name, ref.name, field), \ "args": ', '.join([ "\%s_ptr" % self.name, - "\v"] )}, + "\v%(base)d"] )}, params.sorry)) # Set spec @@ -1591,28 +1629,30 @@ class TaggedUnion: if field == self.tagname: continue index = offset // self.base + sign_extend = "" if high: shift_op = "<<" - shift = self.base - size - (offset % self.base) + shift = self.base_bits - size - (offset % self.base) + if shift < 0: + shift = -shift + shift_op = ">>" + if self.base_sign_extend: + sign_extend = "sign_extend %d " % (self.base_bits - 1) else: shift_op = ">>" shift = offset % self.base initialiser = \ - "%s_CL.%s_CL = ((index (%s_C.words_C %s) %d) %s %d)" % \ - (gen_name(name), field, self.name, self.name, \ + "%s_CL.%s_CL = %s(((index (%s_C.words_C %s) %d) %s %d)" % \ + (gen_name(name), field, sign_extend, self.name, self.name, \ index, shift_op, shift) if size < self.base: - if high: - mask = ((1 << size) - 1) << (self.base - size) - else: - mask = (1 << size) - 1 + mask = field_mask_proof(high, self.base_bits, self.base, size) + initialiser += " AND " + mask - initialiser += " AND 0x%x" % mask - - field_inits.append("\n " + initialiser) + field_inits.append("\n " + initialiser + ")") if len(field_inits) == 0: value = gen_name(name, True) @@ -1869,7 +1909,8 @@ class TaggedUnion: "suf": self.constant_suffix, "high_bits": high_bits, "sign_extend": self.base_sign_extend and high, - "extend_bit": self.base_bits - 1} + "extend_bit": self.base_bits - 1, + "base": self.base} # Reader emit_named("%s_%s_get_%s" % (self.name, ref.name, field), @@ -2174,31 +2215,34 @@ class Block: for name in self.visible_order: offset, size, high = self.field_map[name] - + index = offset // self.base - + sign_extend = "" + if high: shift_op = "<<" - shift = self.base - size - (offset % self.base) + shift = self.base_bits - size - (offset % self.base) + if shift < 0: + shift = -shift + shift_op = ">>" + if self.base_sign_extend: + sign_extend = "sign_extend %d " % (self.base_bits - 1) else: shift_op = ">>" shift = offset % self.base - + initialiser = \ - "%s_CL.%s_CL = ((index (%s_C.words_C %s) %d) %s %d)" % \ - (self.name, name, self.name, self.name, \ + "%s_CL.%s_CL = %s(((index (%s_C.words_C %s) %d) %s %d)" % \ + (self.name, name, sign_extend, self.name, self.name, \ index, shift_op, shift) - + if size < self.base: - if high: - mask = ((1 << size) - 1) << (self.base_bits - size) - else: - mask = (1 << size) - 1 - - initialiser += " AND 0x%x" % mask - - field_inits.append(initialiser) - + mask = field_mask_proof(high, self.base_bits, self.base, size) + + initialiser += " AND " + mask + + field_inits.append(initialiser + ")") + print(lift_def_template % \ {"name": self.name, \ "fields": ',\n '.join(field_inits)}, @@ -2256,13 +2300,11 @@ class Block: field_eq_list = [] for (field, offset, size, high) in self.fields: - if high: - mask = "NOT (mask %d)" % (self.base - size) - else: - mask = "(mask %d)" % size + mask = field_mask_proof(high, self.base_bits, self.base, size) + sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) - field_eq_list.append("%s_CL.%s_CL = \<^bsup>s\<^esup>%s AND %s" % \ - (self.name, field, field, mask)) + field_eq_list.append("%s_CL.%s_CL = %s(\<^bsup>s\<^esup>%s AND %s)" % \ + (self.name, field, sign_extend, field, mask)) field_eqs = ',\n '.join(field_eq_list) emit_named("%s_new" % self.name, params, @@ -2281,15 +2323,15 @@ class Block: # Generate get/set specs for (field, offset, size, high) in self.fields: - if high: - mask = "NOT (mask %d)" % (self.base - size) - else: - mask = "(mask %d)" % size + mask = field_mask_proof(high, self.base_bits, self.base, size) + sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) substs = {"name": self.name, \ "field": field, \ "mask": mask, - "ret_name": return_name} + "sign_extend": sign_extend, + "ret_name": return_name(self.base), + "base": self.base} if not params.skip_modifies: # Get modifies spec @@ -2323,7 +2365,7 @@ class Block: "args": ', '.join([ "\ret__struct_%s_C" % self.name, "\%s" % self.name, - "\v"] )}, + "\v%(base)d"] )}, params.sorry)) emit_named("%s_ptr_set_%s" % (self.name, field), params, @@ -2331,7 +2373,7 @@ class Block: {"fun_name": "%s_ptr_set_%s" % (self.name, field), \ "args": ', '.join([ "\%s_ptr" % self.name, - "\v"] )}, + "\v%(base)d"] )}, params.sorry)) @@ -2467,7 +2509,8 @@ class Block: "suf": self.constant_suffix, \ "high_bits": high_bits, \ "sign_extend": self.base_sign_extend and high, - "extend_bit": self.base_bits - 1} + "extend_bit": self.base_bits - 1, + "base": self.base} # Reader emit_named("%s_get_%s" % (self.name, field), params, @@ -2627,7 +2670,11 @@ if __name__ == '__main__': unions = {} _, block_map, union_map = yacc.parse(input=in_file.read(), lexer=lexer) base_list = [8, 16, 32, 64] - suffix_map = {8 : 'ul', 16 : 'ul', 32 : 'ul', 64 : 'ull'} + # assumes that unsigned int = 32 bit on 32-bit and 64-bit platforms, + # and that unsigned long long = 64 bit on 64-bit platforms. + # Should still work fine if ull = 128 bit, but will not work + # if unsigned int is less than 32 bit. + suffix_map = {8 : 'u', 16 : 'u', 32 : 'u', 64 : 'ull'} for base_info, block_list in block_map.items(): base, base_bits, base_sign_extend = base_info for name, b in block_list.items(): From d26c2951c1ffdb6bd1532c35d1b90190950a7eb1 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Thu, 21 Sep 2017 12:05:22 +1000 Subject: [PATCH 26/29] x86: Remove needless restriction on TLS_BASE values Restricting the value of TLS_BASE does not make sense as ultimately the user is prevented from accessing the kernel region by virtue of protection levels and paging structures. Whether the access is constructed by the user using a pointer (which in ia32 means an implicit usage of `ds` selector) or through an explicit `fs` or `gs` selector does not matter. --- src/arch/x86/machine/registerset.c | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/arch/x86/machine/registerset.c b/src/arch/x86/machine/registerset.c index 82d897869..f6293a8e4 100644 --- a/src/arch/x86/machine/registerset.c +++ b/src/arch/x86/machine/registerset.c @@ -44,11 +44,5 @@ word_t sanitiseRegister(register_t reg, word_t v, bool_t archInfo) /* remove any other bits that shouldn't be set */ v &= FLAGS_MASK; } - if (reg == TLS_BASE) { - /* forbid users from setting a TLS_BASE that is in the kernel window */ - if (v > PPTR_USER_TOP) { - v = PPTR_USER_TOP; - } - } return v; } From 95b505bee240796212da6e924f5723b29669330e Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Tue, 26 Sep 2017 16:55:16 +1000 Subject: [PATCH 27/29] pc99: Make irq_t a uint8_t type instead of an enum type This renames the previous irq_t enum into a platform_irq_t enum and provides irq_t as a 'well defined' uint8_t typedef. Having irq_t be an integer type, and not an enum, is necessary for consistency with verification. As part of explicitly defining irq_t as an unsigned integer type the definition of irqInvalid is changed to prevent sign extension leading to unexpected invalid comparisons. --- include/plat/pc99/plat/machine.h | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/include/plat/pc99/plat/machine.h b/include/plat/pc99/plat/machine.h index f55f976d6..ff00f6f92 100644 --- a/include/plat/pc99/plat/machine.h +++ b/include/plat/pc99/plat/machine.h @@ -47,8 +47,7 @@ typedef enum _interrupt_t { int_max = 255 } interrupt_t; -typedef enum _irq_t { - irqInvalid = -1, +typedef enum _platform_irq_t { irq_isa_min = int_irq_isa_min - IRQ_INT_OFFSET, irq_isa_max = int_irq_isa_max - IRQ_INT_OFFSET, irq_user_min = int_irq_user_min - IRQ_INT_OFFSET, @@ -61,8 +60,14 @@ typedef enum _irq_t { irq_remote_call_ipi = int_remote_call_ipi - IRQ_INT_OFFSET, irq_reschedule_ipi = int_reschedule_ipi - IRQ_INT_OFFSET, #endif - maxIRQ = int_irq_max - IRQ_INT_OFFSET -} irq_t; + maxIRQ = int_irq_max - IRQ_INT_OFFSET, + /* This is explicitly 255, instead of -1 like on some other platforms, to ensure + * that comparisons between an irq_t (a uint8_t) and irqInvalid (some kind of signed int) + * are well defined and behave as expected */ + irqInvalid = 255, +} platform_irq_t; + +typedef uint8_t irq_t; #define IRQ_CNODE_BITS 13 From 368d5ae65ea50060995bf4707f84e263a5d963b2 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Fri, 29 Sep 2017 10:45:59 +1000 Subject: [PATCH 28/29] x86: Use word_t for vm_rights_t instead of uint32_t This prevents implicit casting and simplifies verification --- include/arch/x86/arch/object/structures.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/arch/x86/arch/object/structures.h b/include/arch/x86/arch/object/structures.h index 68c733de1..fa32fe8ee 100644 --- a/include/arch/x86/arch/object/structures.h +++ b/include/arch/x86/arch/object/structures.h @@ -148,7 +148,7 @@ enum vm_rights { VMReadOnly = 2, VMReadWrite = 3 }; -typedef uint32_t vm_rights_t; +typedef word_t vm_rights_t; #include From a1e6354aa6d94d54dc36d8885634c6b707933f09 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Fri, 29 Sep 2017 15:38:15 +1000 Subject: [PATCH 29/29] Supper compiler versions that disagree on mcpu and march Differing versions of gcc disagree on which combinations of mcpu and march are valid, particularly around the armv7ve architecture. The solution here is to only set march if it would not cause a conflict --- CMakeLists.txt | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0edc2306d..b92147b1c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,6 +11,7 @@ # cmake_minimum_required(VERSION 3.7.2) +include(CheckCSourceCompiles) project(seL4 C ASM) # First find our helpers @@ -59,8 +60,21 @@ if(KernelArchX86) endif() endif() if(KernelArchARM) - set(c_common_flags "${c_common_flags} -mcpu=${KernelArmCPU} -march=${KernelArmArmV}${KernelArmMachFeatureModifiers}") - set(asm_common_flags "${asm_common_flags} -Wa,-mcpu=${KernelArmCPU} -Wa,-march=${KernelArmArmV}${KernelArmMachFeatureModifiers}") + set(c_common_flags "${c_common_flags} -mcpu=${KernelArmCPU}") + set(asm_common_flags "${asm_common_flags} -Wa,-mcpu=${KernelArmCPU}") + # See if the current compiler understands the chosen -mcpu and -march flags when used together. + # them not being supported unfortunately does not indicate an error as older versions of gcc + # *require* mcpu and march flags that are considered invalid on newer versions of gcc. Overall + # newer versions of gcc recommend just setting 'mcpu' and letting the internals determine the + # approproate march and mtune settings, as such we have already set the desired mcpu and + # we will just add the march for safety for the older compilers if it does not cause conflicts + set(CMAKE_REQUIRED_FLAGS "${c_common_flags} -march=${KernelArmArmV}${KernelArmMachFeatureModifiers}") + set(CMAKE_REQUIRED_DEFINITIONS "") + check_c_source_compiles("void main(void){}" ARM_MCPU_MARCH_VALID FAIL_REGEX "warning|error") + if (ARM_MCPU_MARCH_VALID) + set(c_common_flags "${c_common_flags} -march=${KernelArmArmV}${KernelArmMachFeatureModifiers}") + set(asm_common_flags "${asm_common_flags} -Wa,-march=${KernelArmArmV}${KernelArmMachFeatureModifiers}") + endif() endif() set(common_flags "${common_flags} ${build_arch}") if(Kernel64)