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 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. 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) diff --git a/Kconfig b/Kconfig index ddc45e83d..e933525b0 100644 --- a/Kconfig +++ b/Kconfig @@ -357,6 +357,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/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 diff --git a/config.cmake b/config.cmake index ce15f61c1..916d83c51 100644 --- a/config.cmake +++ b/config.cmake @@ -18,10 +18,10 @@ 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(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(CSPEC_DIR "." CACHE PATH "") +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) @@ -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 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 "") 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 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 "") 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 "" 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/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 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 diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml index 43fce385d..8c9590335 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. @@ -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/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); 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}. 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} 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..f0c333d17 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))) { 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; } 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 ) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index 1e528ae0d..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 @@ -476,7 +483,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 +499,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 ''' @@ -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 \ @@ -584,14 +593,14 @@ 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', + 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) @@ -641,16 +650,16 @@ 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', + 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 + ''') @@ -679,7 +688,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 +696,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'''], @@ -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' : [ @@ -754,23 +763,25 @@ 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 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) @@ -1028,7 +1049,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) @@ -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 @@ -1275,7 +1316,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) @@ -1297,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, @@ -1371,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, @@ -1409,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: @@ -1458,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), @@ -1468,7 +1507,7 @@ class TaggedUnion: (self.name, ref.name, field), \ "args": ', '.join([ "\%s_ptr" % self.name, - "\v"] )}, + "\v%(base)d"] )}, params.sorry)) # Set spec @@ -1590,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 %d" % mask - - field_inits.append("\n " + initialiser) + field_inits.append("\n " + initialiser + ")") if len(field_inits) == 0: value = gen_name(name, True) @@ -1868,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), @@ -2173,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 %d" % 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)}, @@ -2219,7 +2264,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) @@ -2254,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, @@ -2279,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 @@ -2321,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, @@ -2329,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)) @@ -2465,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, @@ -2625,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(): @@ -2682,9 +2731,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) @@ -2695,9 +2746,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(): @@ -2744,14 +2795,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(): @@ -2760,12 +2807,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) @@ -2781,10 +2824,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) 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)