dbe3e41a88
For performing verification on libsel4 the syscall invocations need to not be inlined. This provides a (somewhat hacky) way of doing that.
65 lines
2 KiB
Text
65 lines
2 KiB
Text
#
|
|
# Copyright 2014, NICTA
|
|
#
|
|
# This software may be distributed and modified according to the terms of
|
|
# the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
|
# See "LICENSE_BSD2.txt" for details.
|
|
#
|
|
# @TAG(NICTA_BSD)
|
|
#
|
|
|
|
menu "libsel4"
|
|
config LIB_SEL4
|
|
bool "libsel4"
|
|
default y
|
|
select HAVE_LIB_SEL4
|
|
help
|
|
seL4 API library
|
|
|
|
config LIB_SEL4_INLINE_INVOCATIONS
|
|
bool "Inline generated syscall invocations"
|
|
depends on LIB_SEL4
|
|
default y
|
|
help
|
|
When set to true will mark generated functions as 'inline', allowing
|
|
them to be inlined by the callee user code. This may be undesirable
|
|
for verification, so setting to 'n' will forcively prevent the function
|
|
from being inlined
|
|
|
|
config LIB_SEL4_HAVE_REGISTER_STUBS
|
|
bool "Support syscall stubs without IPC buffer"
|
|
depends on LIB_SEL4 && !USER_OPTIMISATION_O0 && ARCH_ARM
|
|
default y
|
|
help
|
|
Generate the 'WithMRs' variants of the syscall stubs. These stubs
|
|
avoid the use of the IPC buffer where possible and attempt to
|
|
place syscall arguments directly into and out of cpu registers.
|
|
GCC's register allocation is a hint only and cannot be relied upon,
|
|
as a result these stubs are known to be broken, and are disabled,
|
|
at -O0
|
|
|
|
if LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM)
|
|
config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
|
|
bool "use only IPC buffer for syscalls"
|
|
depends on LIB_SEL4
|
|
default n
|
|
help
|
|
When generating syscall wrappers, only use the IPC buffer for
|
|
marshalling and unmarshalling arguments. Without this option set,
|
|
arguments will be passed in registers where possible for better
|
|
performance.
|
|
endif
|
|
|
|
if !(LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM))
|
|
menu "libsel4 hidden"
|
|
visible if false
|
|
config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
|
|
bool "Use only IPC buffer for syscalls"
|
|
depends on LIB_SEL4
|
|
default y
|
|
endmenu
|
|
endif
|
|
|
|
config HAVE_LIB_SEL4
|
|
bool
|
|
endmenu
|