Merge branch zcu102-7.0.0 into master
This commit is contained in:
Adrian Danis
commit
383a6d959f
32 changed files with 673 additions and 243 deletions
|
|
@ -10,3 +10,4 @@ manual/figs/*
|
|||
.git/*
|
||||
*parsetab.py
|
||||
manual/*
|
||||
CHANGES
|
||||
|
|
|
|||
33
CHANGES
Normal file
33
CHANGES
Normal file
|
|
@ -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.
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
6
Kconfig
6
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
|
||||
|
|
|
|||
2
VERSION
2
VERSION
|
|
@ -1 +1 @@
|
|||
7.0.0
|
||||
7.0.0-dev
|
||||
13
config.cmake
13
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
|
||||
|
|
|
|||
29
configs/ARM_HYP_verified.cmake
Normal file
29
configs/ARM_HYP_verified.cmake
Normal file
|
|
@ -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 "")
|
||||
26
configs/X64_verified.cmake
Normal file
26
configs/X64_verified.cmake
Normal file
|
|
@ -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 "")
|
||||
|
|
@ -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 ""
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -148,7 +148,7 @@ enum vm_rights {
|
|||
VMReadOnly = 2,
|
||||
VMReadWrite = 3
|
||||
};
|
||||
typedef uint32_t vm_rights_t;
|
||||
typedef word_t vm_rights_t;
|
||||
|
||||
#include <mode/object/structures.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
|
||||
|
||||
|
|
|
|||
|
|
@ -239,7 +239,7 @@
|
|||
</interface>
|
||||
|
||||
<interface name="seL4_X86_ASIDPool" manual_name="ASID Pool">
|
||||
<method id="X86ASIDPoolAssign" name="Assign" manual_label='asid_pool_assign'>
|
||||
<method id="X86ASIDPoolAssign" name="Assign" manual_label='asidpool_assign'>
|
||||
<brief>
|
||||
Assign an ASID pool.
|
||||
</brief>
|
||||
|
|
@ -368,61 +368,206 @@
|
|||
</method>
|
||||
</interface>
|
||||
<interface name="seL4_TCB" manual_name="TCB">
|
||||
<method id="TCBSetEPTRoot" name="SetEPTRoot" condition="defined(CONFIG_VTX)" manual_name="Set EPT Root">
|
||||
<param dir="in" name="vcpu" type="seL4_CPtr"/>
|
||||
<method id="TCBSetEPTRoot" name="SetEPTRoot" condition="defined(CONFIG_VTX)" manual_name="Set EPT Root" manual_label="set_eptroot">
|
||||
<brief>
|
||||
Set the EPT root of a thread
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label='sec:virt'/>.
|
||||
</description>
|
||||
<param dir="in" name="eptpml4" type="seL4_CPtr"
|
||||
description='CPTR to an EPT PML4 object to act as the guest mode vspace root'/>
|
||||
</method>
|
||||
</interface>
|
||||
<interface name="seL4_X86_VCPU" manual_name="VCPU">
|
||||
<interface name="seL4_X86_VCPU" manual_name="VCPU" cap_description='VCPU object to operate on'>
|
||||
<method id="X86VCPUSetTCB" name="SetTCB" condition="defined(CONFIG_VTX)" manual_name="Set TCB">
|
||||
<param dir="in" name="tcb" type="seL4_CNode" />
|
||||
<brief>
|
||||
Bind TCB to VCPU
|
||||
</brief>
|
||||
<description>
|
||||
Configures the one-to-one binding of a VCPU and TCB, overwriting any previous binding
|
||||
in both. See <autoref label='sec:virt'/>.
|
||||
</description>
|
||||
<param dir="in" name="tcb" type="seL4_CNode" description='CPTR of the TCB to bind to'/>
|
||||
</method>
|
||||
<method id="X86VCPUReadVMCS" name="ReadVMCS" condition="defined(CONFIG_VTX)" manual_name="Read VMCS">
|
||||
<param dir="in" name="field" type="seL4_Word"/>
|
||||
<param dir="out" name="value" type="seL4_Word"/>
|
||||
<method id="X86VCPUReadVMCS" name="ReadVMCS" condition="defined(CONFIG_VTX)" manual_name="Read VMCS" manual_label="vcpu_readvmcs">
|
||||
<brief>
|
||||
Read VMCS field from the hardware
|
||||
</brief>
|
||||
<description>
|
||||
Thin wrapper around the <texttt text='vmread'/> 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.
|
||||
</description>
|
||||
<return>
|
||||
A <texttt text='seL4_X86_VCPU_ReadVMCS_t'/> struct that contains a
|
||||
<texttt text='seL4_Word value'/>, which holds the return result of the <texttt text='vmread'/> instruction,
|
||||
and <texttt text='int error'/>. See <autoref label='sec:errors'/> for a description
|
||||
of the message register and tag contents upon error.
|
||||
</return>
|
||||
<param dir="in" name="field" type="seL4_Word"
|
||||
description='Field to give to \texttt{vmread} instruction'/>
|
||||
<param dir="out" name="value" type="seL4_Word"
|
||||
description='Value returned by `vmread` instruction'/>
|
||||
</method>
|
||||
<method id="X86VCPUWriteVMCS" name="WriteVMCS" condition="defined(CONFIG_VTX)" manual_name="Write VMCS">
|
||||
<param dir="in" name="field" type="seL4_Word"/>
|
||||
<param dir="in" name="value" type="seL4_Word"/>
|
||||
<param dir="out" name="written" type="seL4_Word"/>
|
||||
<method id="X86VCPUWriteVMCS" name="WriteVMCS" condition="defined(CONFIG_VTX)" manual_name="Write VMCS" manual_label="vcpu_writevmcs">
|
||||
<brief>
|
||||
Write VMCS field to the hardware
|
||||
</brief>
|
||||
<description>
|
||||
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 <autoref label='sec:virt'/>).
|
||||
|
||||
The final value written to the hardware is returned and can be compared
|
||||
to the input parameter to determine what bits the kernel changed.
|
||||
</description>
|
||||
<return>
|
||||
A <texttt text='seL4_X86_VCPU_WriteVMCS_t'/> struct that contains a
|
||||
<texttt text='seL4_Word writen'/>, which holds the final value written with the <texttt text='vmwrite'/> instruction,
|
||||
and <texttt text='int error'/>. See <autoref label='sec:errors'/> for a description
|
||||
of the message register and tag contents upon error.
|
||||
</return>
|
||||
<param dir="in" name="field" type="seL4_Word"
|
||||
description='Field to give to `vmwrite` instruction'/>
|
||||
<param dir="in" name="value" type="seL4_Word"
|
||||
description='Value to write using `vmwrite` instruction'/>
|
||||
<param dir="out" name="written" type="seL4_Word"
|
||||
description='Final value written using `vmwrite` after kernel validation'/>
|
||||
</method>
|
||||
<method id="X86VCPUEnableIOPort" name="EnableIOPort" condition="defined(CONFIG_VTX)"
|
||||
manual_name="Enable IO Port">
|
||||
<param dir="in" name="ioPort" type="seL4_CNode"/>
|
||||
<param dir="in" name="low" type="seL4_Word"/>
|
||||
<param dir="in" name="high" type="seL4_Word"/>
|
||||
manual_name="Enable IO Port" manual_label="vcpu_enableioport">
|
||||
<brief>
|
||||
Enable I/O port range in guest execution
|
||||
</brief>
|
||||
<description>
|
||||
Enables a range of I/O ports for direct access by the execution mode in
|
||||
the <texttt text='VCPU'/>. 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 <texttt text='VCPU'/>, see <autoref label='sec:virt'/> for details.
|
||||
</description>
|
||||
<param dir="in" name="ioPort" type="seL4_CPtr"
|
||||
description='I/O port capability whose authority is being delegating'/>
|
||||
<param dir="in" name="low" type="seL4_Word"
|
||||
description='Start of the I/O port range to enable'/>
|
||||
<param dir="in" name="high" type="seL4_Word"
|
||||
description='Last I/O port in the range to enable'/>
|
||||
</method>
|
||||
<method id="X86VCPUDisableIOPort" name="DisableIOPort" condition="defined(CONFIG_VTX)"
|
||||
manual_name="Disable IO Port">
|
||||
<param dir="in" name="low" type="seL4_Word"/>
|
||||
<param dir="in" name="high" type="seL4_Word"/>
|
||||
<brief>
|
||||
Disable I/O port range in privileged execution
|
||||
</brief>
|
||||
<description>
|
||||
Disable a range of I/O ports for direct access by the execution mode in
|
||||
the <texttt text='VCPU'/>.
|
||||
</description>
|
||||
<param dir="in" name="low" type="seL4_Word"
|
||||
description='Start of the I/O port range to disable'/>
|
||||
<param dir="in" name="high" type="seL4_Word"
|
||||
description='Last I/O port in the range to disable'/>
|
||||
</method>
|
||||
<method id="X86VCPUWriteRegisters" name="WriteRegisters" condition="defined(CONFIG_VTX)"
|
||||
manual_name="Write Registers">
|
||||
<param dir="in" name="regs" type="seL4_VCPUContext"/>
|
||||
<brief>
|
||||
Set guest mode registers to the fields of a given <texttt text="seL4_VCPUContext"/>
|
||||
</brief>
|
||||
<description>
|
||||
Sets the guest mode registers, which is any registers not already part of the VMCS.
|
||||
</description>
|
||||
<param dir="in" name="regs" type="seL4_VCPUContext"
|
||||
description='Data structure containing the new register values.'/>
|
||||
</method>
|
||||
</interface>
|
||||
<interface name="seL4_X86_EPTPDPT" manual_name="Extended Page Table Page Directory Page Table">
|
||||
<interface name="seL4_X86_EPTPDPT" manual_name="Extended Page Table Page Directory Page Table"
|
||||
cap_description="Capability to the EPT PDPT being operated on.">
|
||||
<method id="X86EPTPDPTMap" name="Map" condition="defined(CONFIG_VTX)">
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
|
||||
<brief>
|
||||
Map an EPT page directory page table.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"
|
||||
description='Capability to the EPT root which will contain the mapping'/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"
|
||||
description='Guest physical address to map the page into.'/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes">
|
||||
<description>
|
||||
VM attributes for the mapping. Possible values for this type are
|
||||
given in <autoref label='ch:vspace'/>
|
||||
</description>
|
||||
</param>
|
||||
</method>
|
||||
<method id="X86EPTPDPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
|
||||
<brief>
|
||||
Unmap an EPT page directory page table.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
</method>
|
||||
<method id="X86EPTPDPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)"/>
|
||||
</interface>
|
||||
<interface name="seL4_X86_EPTPD" manual_name="Extended Page Table Page Directory">
|
||||
<interface name="seL4_X86_EPTPD" manual_name="Extended Page Table Page Directory"
|
||||
cap_description="Capability to the EPT PD being operated on.">
|
||||
<method id="X86EPTPDMap" name="Map" condition="defined(CONFIG_VTX)">
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
|
||||
<brief>
|
||||
Map an EPT page directory.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"
|
||||
description='Capability to the EPT root which will contain the mapping'/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"
|
||||
description='Guest physical address to map the page into.'/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes">
|
||||
<description>
|
||||
VM attributes for the mapping. Possible values for this type are
|
||||
given in <autoref label='ch:vspace'/>
|
||||
</description>
|
||||
</param>
|
||||
</method>
|
||||
<method id="X86EPTPDUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
|
||||
<brief>
|
||||
Unmap an EPT page directory.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
</method>
|
||||
<method id="X86EPTPDUnmap" name="Unmap" condition="defined(CONFIG_VTX)"/>
|
||||
</interface>
|
||||
<interface name="seL4_X86_EPTPT" manual_name="Extended Page Table Page Table">
|
||||
<interface name="seL4_X86_EPTPT" manual_name="Extended Page Table Page Table"
|
||||
cap_description="Capability to the EPT PT being operated on.">
|
||||
<method id="X86EPTPTMap" name="Map" condition="defined(CONFIG_VTX)">
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
|
||||
<brief>
|
||||
Map an EPT page table.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
<param dir="in" name="pml4" type="seL4_X86_EPTPML4"
|
||||
description='Capability to the EPT root which will contain the mapping'/>
|
||||
<param dir="in" name="gpa" type="seL4_Word"
|
||||
description='Guest physical address to map the page into.'/>
|
||||
<param dir="in" name="attr" type="seL4_X86_VMAttributes">
|
||||
<description>
|
||||
VM attributes for the mapping. Possible values for this type are
|
||||
given in <autoref label='ch:vspace'/>
|
||||
</description>
|
||||
</param>
|
||||
</method>
|
||||
<method id="X86EPTPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
|
||||
<brief>
|
||||
Unmap an EPT page table.
|
||||
</brief>
|
||||
<description>
|
||||
See <autoref label="ch:vspace"/>
|
||||
</description>
|
||||
</method>
|
||||
<method id="X86EPTPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)"/>
|
||||
</interface>
|
||||
</api>
|
||||
|
|
|
|||
|
|
@ -474,6 +474,67 @@ seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr);
|
|||
#endif
|
||||
/** @} */
|
||||
|
||||
#ifdef CONFIG_ARCH_X86
|
||||
/**
|
||||
* @defgroup X86SystemCalls X86 System Calls
|
||||
* @{
|
||||
*/
|
||||
|
||||
#ifdef CONFIG_VTX
|
||||
/**
|
||||
* @xmlonly <manual name="VMEnter" label="sel4_vmenter"/> @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 <autoref label="sec:virt"/>.
|
||||
* @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 <autoref label="sec:messageinfo"/>)
|
||||
* @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 */
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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}.
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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 */
|
||||
|
|
|
|||
|
|
@ -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 */
|
||||
|
|
|
|||
|
|
@ -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 */
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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))) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 \<noteq> %(classmask)d)
|
||||
''' AND 0x%(classmask)x \<noteq> 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 \<noteq> %(classmask)d)
|
||||
'''if ((x << %(tag_shift)d) AND 0x%(classmask)x \<noteq> 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:
|
||||
"\<lbrakk> w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \<rbrakk>
|
||||
|
|
@ -584,14 +593,14 @@ def ptr_get_template(ptrname):
|
|||
return ptr_basic_template('get_%(field)s', ptrname, '\<acute>%(ret_name)s :== ', '',
|
||||
'''\<lbrace>\<acute>%(ret_name)s = ''' \
|
||||
'''%(name)s_CL.%(field)s_CL ''' \
|
||||
'''(%(name)s_lift (%(access_path)s))\<rbrace>''') # AND %(mask)s
|
||||
'''(%(name)s_lift (%(access_path)s))\<rbrace>''')
|
||||
|
||||
def ptr_set_template(name, ptrname):
|
||||
return ptr_basic_template(name, ptrname, '', ', \<acute>v',
|
||||
return ptr_basic_template(name, ptrname, '', ', \<acute>v%(base)d',
|
||||
'''{t. \<exists>%(name)s.
|
||||
%(name)s_lift %(name)s =
|
||||
%(name)s_lift (%(access_path)s) \<lparr> %(name)s_CL.%(field)s_CL ''' \
|
||||
''':= \<^bsup>s\<^esup>v AND %(mask)s \<rparr> \<and>
|
||||
''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr> \<and>
|
||||
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
||||
(''' + ptrname + ''')
|
||||
%(update_path)s)
|
||||
|
|
@ -641,16 +650,16 @@ def ptr_union_get_template(ptrname):
|
|||
'\<and> %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s',
|
||||
'''\<lbrace>\<acute>%(ret_name)s = ''' \
|
||||
'''%(name)s_%(block)s_CL.%(field)s_CL ''' \
|
||||
'''(%(name)s_%(block)s_lift %(access_path)s)\<rbrace>''') # AND %(mask)s --- given by _lift?
|
||||
'''(%(name)s_%(block)s_lift %(access_path)s)\<rbrace>''')
|
||||
|
||||
def ptr_union_set_template(ptrname):
|
||||
return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \<acute>v',
|
||||
return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \<acute>v%(base)d',
|
||||
'\<and> %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s',
|
||||
'''{t. \<exists>%(name)s. ''' \
|
||||
'''%(name)s_%(block)s_lift %(name)s =
|
||||
%(name)s_%(block)s_lift %(access_path)s ''' \
|
||||
'''\<lparr> %(name)s_%(block)s_CL.%(field)s_CL ''' \
|
||||
''':= \<^bsup>s\<^esup>v AND %(mask)s \<rparr> \<and>
|
||||
''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr> \<and>
|
||||
%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \<and>
|
||||
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) \<Longrightarrow>
|
||||
ptr_aligned ((Ptr &(p\<rightarrow>[''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 \<Longrightarrow>
|
||||
ptr_safe (Ptr &(p\<rightarrow>[''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(\<acute>%(name)s)
|
||||
\<lbrace>\<acute>%(ret_name)s = ''' \
|
||||
'''%(name)s_CL.%(field)s_CL ''' \
|
||||
'''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\<rbrace>"''', # AND %(mask)s
|
||||
'''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\<rbrace>"''',
|
||||
''' 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:
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s}
|
||||
\<acute>ret__struct_%(name)s_C :== ''' \
|
||||
'''PROC %(name)s_set_%(field)s(\<acute>%(name)s, \<acute>v)
|
||||
'''PROC %(name)s_set_%(field)s(\<acute>%(name)s, \<acute>v%(base)d)
|
||||
\<lbrace>%(name)s_lift \<acute>ret__struct_%(name)s_C = ''' \
|
||||
'''%(name)s_lift \<^bsup>s\<^esup>%(name)s \<lparr> ''' \
|
||||
'''%(name)s_CL.%(field)s_CL ''' \
|
||||
''':= \<^bsup>s\<^esup>v AND %(mask) s \<rparr>\<rbrace>"''',
|
||||
''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr>\<rbrace>"''',
|
||||
''' 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:
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s}
|
||||
\<acute>ret__unsigned :== ''' \
|
||||
\<acute>%(ret_name)s :== ''' \
|
||||
'''PROC %(name)s_get_%(tagname)s(\<acute>%(name)s)
|
||||
\<lbrace>\<acute>ret__unsigned = ''' \
|
||||
\<lbrace>\<acute>%(ret_name)s = ''' \
|
||||
'''%(name)s_get_tag \<^bsup>s\<^esup>%(name)s\<rbrace>"''',
|
||||
''' apply(rule allI, rule conseqPre, vcg)
|
||||
apply(clarsimp)
|
||||
|
|
@ -1028,7 +1049,7 @@ done'''],
|
|||
\<lbrace>\<acute>%(ret_name)s = ''' \
|
||||
'''%(name)s_%(block)s_CL.%(field)s_CL ''' \
|
||||
'''(%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s)''' \
|
||||
'''\<rbrace>"''', # AND %(mask)s
|
||||
'''\<rbrace>"''',
|
||||
''' 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'''],
|
|||
'''\<lbrace>s. %(name)s_get_tag \<acute>%(name)s = ''' \
|
||||
'''scast %(name)s_%(block)s\<rbrace>
|
||||
\<acute>ret__struct_%(name)s_C :== ''' \
|
||||
'''PROC %(name)s_%(block)s_set_%(field)s(\<acute>%(name)s, \<acute>v)
|
||||
'''PROC %(name)s_%(block)s_set_%(field)s(\<acute>%(name)s, \<acute>v%(base)d)
|
||||
\<lbrace>%(name)s_%(block)s_lift \<acute>ret__struct_%(name)s_C = ''' \
|
||||
'''%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s \<lparr> ''' \
|
||||
'''%(name)s_%(block)s_CL.%(field)s_CL ''' \
|
||||
''':= \<^bsup>s\<^esup>v AND %(mask)s\<rparr> \<and>
|
||||
''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s)\<rparr> \<and>
|
||||
%(name)s_get_tag \<acute>ret__struct_%(name)s_C = ''' \
|
||||
'''scast %(name)s_%(block)s\<rbrace>"''',
|
||||
''' 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
|
|||
['\\<lambda>_. ' + 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([
|
||||
"\<acute>ret__struct_%s_C" % self.name,
|
||||
"\<acute>%s" % self.name,
|
||||
"\<acute>v"] )},
|
||||
"\<acute>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([
|
||||
"\<acute>%s_ptr" % self.name,
|
||||
"\<acute>v"] )},
|
||||
"\<acute>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([
|
||||
"\<acute>ret__struct_%s_C" % self.name,
|
||||
"\<acute>%s" % self.name,
|
||||
"\<acute>v"] )},
|
||||
"\<acute>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([
|
||||
"\<acute>%s_ptr" % self.name,
|
||||
"\<acute>v"] )},
|
||||
"\<acute>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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue