cspec: Use CMake for building the C kernel
The seL4 kernel now supports a CMake based build in addition to the original Make based one. This changes the Makefile that previously included the kernel Makefile to instead have rules for instantiating a sub CMake build As the location of built files have changed the KernelInc_C theory also needs to be updated to point to the new locations for the generated artifacts.
This commit is contained in:
Adrian Danis
parent
100e738f21
commit
ba94117969
|
|
@ -17,6 +17,7 @@
|
|||
/spec/cspec/*/c/plat/
|
||||
/spec/cspec/*/c/sources_list_updated
|
||||
/spec/cspec/*/c/autoconf.h
|
||||
/spec/cspec/*/c/build
|
||||
|
||||
/spec/haskell/doc/**/*.aux
|
||||
/spec/haskell/doc/**/*.bbl
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ ExecSpec ASpec : design-spec
|
|||
|
||||
# Preprocess the kernel's source code and bitfield theory files.
|
||||
c-kernel: c-parser .FORCE
|
||||
cd cspec/$(L4V_ARCH)/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec
|
||||
cd cspec/$(L4V_ARCH)/c && L4V_REPO_PATH=$(L4V_REPO_PATH) L4V_ARCH=$(L4V_ARCH) $(MAKE) cspec
|
||||
.PHONY: c-kernel
|
||||
|
||||
# Run the haskell translator
|
||||
|
|
|
|||
|
|
@ -12,10 +12,10 @@ theory KernelInc_C
|
|||
imports
|
||||
Kernel_C
|
||||
"../Substitute"
|
||||
"c/arch/object/structures_defs"
|
||||
"c/arch/object/structures_proofs"
|
||||
"c/32/mode/api/shared_types_defs"
|
||||
"c/32/mode/api/shared_types_proofs"
|
||||
"c/build/generated/arch/object/structures_defs"
|
||||
"c/build/generated/arch/object/structures_proofs"
|
||||
"c/build/generated/mode/api/shared_types_defs"
|
||||
"c/build/generated/mode/api/shared_types_proofs"
|
||||
begin
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -17,10 +17,6 @@ export PATH
|
|||
TOOLPREFIX ?= arm-none-eabi-
|
||||
SHELL=bash
|
||||
|
||||
ARCH=arm
|
||||
ARMV=armv7-a
|
||||
PLAT=imx6
|
||||
CPU=cortex-a9
|
||||
CONFIG_DOMAIN_SCHEDULE=config_sched.c
|
||||
|
||||
ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
||||
|
|
@ -33,18 +29,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
|||
endif
|
||||
|
||||
# modifies are produced by the parser
|
||||
SKIP_MODIFIES=1
|
||||
SKIP_MODIFIES=ON
|
||||
FASTPATH=yes
|
||||
CSPEC_DIR=..
|
||||
|
||||
build/CMakeCache.txt:
|
||||
mkdir -p build
|
||||
cd build && \
|
||||
cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
|
||||
-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
|
||||
-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
|
||||
-DSKIP_MODIFIES=${SKIP_MODIFIES} \
|
||||
-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
|
||||
-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
|
||||
|
||||
kernel_all_pp: build/CMakeCache.txt
|
||||
cd build && ninja kernel_all_pp_wrapper
|
||||
cp -a build/kernel_all_pp.c kernel_all.c_pp
|
||||
|
||||
.PHONY: kernel_all_pp
|
||||
|
||||
# called by ../../spec/Makefile
|
||||
cspec: kernel_all.c_pp ${UMM_TYPES} theories
|
||||
# theories is defined in seL4 makefile
|
||||
cspec: ${UMM_TYPES} kernel_all_pp
|
||||
cd build && ninja kernel_theories
|
||||
|
||||
.PHONY: cspec
|
||||
|
||||
# Create "umm_types" if necessary.
|
||||
${UMM_TYPES}: kernel_all.c_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
|
||||
|
||||
include ${SOURCE_ROOT}/Makefile
|
||||
${UMM_TYPES}: kernel_all_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@
|
||||
|
||||
|
|
|
|||
|
|
@ -12,10 +12,10 @@ theory KernelInc_C
|
|||
imports
|
||||
Kernel_C
|
||||
"../Substitute"
|
||||
"c/arch/object/structures_defs"
|
||||
"c/arch/object/structures_proofs"
|
||||
"c/32/mode/api/shared_types_defs"
|
||||
"c/32/mode/api/shared_types_proofs"
|
||||
"c/build/generated/arch/object/structures_defs"
|
||||
"c/build/generated/arch/object/structures_proofs"
|
||||
"c/build/generated/mode/api/shared_types_defs"
|
||||
"c/build/generated/mode/api/shared_types_proofs"
|
||||
begin
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -17,10 +17,6 @@ export PATH
|
|||
TOOLPREFIX ?= arm-none-eabi-
|
||||
SHELL=bash
|
||||
|
||||
ARCH=arm
|
||||
ARMV=armv7-a
|
||||
PLAT=tk1
|
||||
CPU=cortex-a15
|
||||
CONFIG_DOMAIN_SCHEDULE=config_sched.c
|
||||
|
||||
ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
||||
|
|
@ -33,18 +29,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
|||
endif
|
||||
|
||||
# modifies are produced by the parser
|
||||
SKIP_MODIFIES=1
|
||||
SKIP_MODIFIES=ON
|
||||
FASTPATH=yes
|
||||
CSPEC_DIR=..
|
||||
|
||||
build/CMakeCache.txt:
|
||||
mkdir -p build
|
||||
cd build && \
|
||||
cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
|
||||
-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
|
||||
-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
|
||||
-DSKIP_MODIFIES=${SKIP_MODIFIES} \
|
||||
-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
|
||||
-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
|
||||
|
||||
kernel_all_pp: build/CMakeCache.txt
|
||||
cd build && ninja kernel_all_pp_wrapper
|
||||
cp -a build/kernel_all_pp.c kernel_all.c_pp
|
||||
|
||||
.PHONY: kernel_all_pp
|
||||
|
||||
# called by ../../spec/Makefile
|
||||
cspec: kernel_all.c_pp ${UMM_TYPES} theories
|
||||
# theories is defined in seL4 makefile
|
||||
cspec: ${UMM_TYPES} kernel_all_pp
|
||||
cd build && ninja kernel_theories
|
||||
|
||||
.PHONY: cspec
|
||||
|
||||
# Create "umm_types" if necessary.
|
||||
${UMM_TYPES}: kernel_all.c_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
|
||||
|
||||
include ${SOURCE_ROOT}/Makefile
|
||||
${UMM_TYPES}: kernel_all_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@
|
||||
|
||||
|
|
|
|||
|
|
@ -12,10 +12,10 @@ theory KernelInc_C
|
|||
imports
|
||||
Kernel_C
|
||||
"../Substitute"
|
||||
"c/arch/object/structures_defs"
|
||||
"c/arch/object/structures_proofs"
|
||||
"c/64/mode/api/shared_types_defs"
|
||||
"c/64/mode/api/shared_types_proofs"
|
||||
"c/build/generated/arch/object/structures_defs"
|
||||
"c/build/generated/arch/object/structures_proofs"
|
||||
"c/build/generated/mode/api/shared_types_defs"
|
||||
"c/build/generated/mode/api/shared_types_proofs"
|
||||
begin
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -16,9 +16,6 @@ PATH:=${PARSERPATH}:${PATH}
|
|||
export PATH
|
||||
SHELL=bash
|
||||
|
||||
ARCH=x86
|
||||
SEL4_ARCH=x86_64
|
||||
PLAT=pc99
|
||||
CONFIG_DOMAIN_SCHEDULE=config_sched.c
|
||||
|
||||
ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
||||
|
|
@ -31,18 +28,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
|
|||
endif
|
||||
|
||||
# modifies are produced by the parser
|
||||
SKIP_MODIFIES=1
|
||||
SKIP_MODIFIES=ON
|
||||
FASTPATH=yes
|
||||
CSPEC_DIR=..
|
||||
|
||||
build/CMakeCache.txt:
|
||||
mkdir -p build
|
||||
cd build && \
|
||||
cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
|
||||
-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
|
||||
-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
|
||||
-DSKIP_MODIFIES=${SKIP_MODIFIES} \
|
||||
-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
|
||||
-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
|
||||
|
||||
kernel_all_pp: build/CMakeCache.txt
|
||||
cd build && ninja kernel_all_pp_wrapper
|
||||
cp -a build/kernel_all_pp.c kernel_all.c_pp
|
||||
|
||||
.PHONY: kernel_all_pp
|
||||
|
||||
# called by ../../spec/Makefile
|
||||
cspec: kernel_all.c_pp ${UMM_TYPES} theories
|
||||
# theories is defined in seL4 makefile
|
||||
cspec: ${UMM_TYPES} kernel_all_pp
|
||||
cd build && ninja kernel_theories
|
||||
|
||||
.PHONY: cspec
|
||||
|
||||
# Create "umm_types" if necessary.
|
||||
${UMM_TYPES}: kernel_all.c_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
|
||||
|
||||
include ${SOURCE_ROOT}/Makefile
|
||||
${UMM_TYPES}: kernel_all_pp
|
||||
python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue