blob: 2520a0b46a6d668b6f85d9750d37314e1bf2ae32 [file] [log] [blame]
Adrian Danisec8f7092017-10-16 16:47:58 +11001#
2# Copyright 2018, Data61
3# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4# ABN 41 687 119 230.
5#
6# This software may be distributed and modified according to the terms of
7# the BSD 2-Clause license. Note that NO WARRANTY is provided.
8# See "LICENSE_BSD2.txt" for details.
9#
10# @TAG(DATA61_BSD)
11#
12
13cmake_minimum_required(VERSION 3.7.2)
14
15include(ExternalProject)
16
17include(${KERNEL_HELPERS_PATH})
18
19set(configure_string "")
20
21config_string(CAmkESDefaultStackSize CAMKES_DEFAULT_STACK_SIZE
22 "Stack size to allocate per-component, in bytes. Note that this value
23 should be page-aligned. If not, it will be rounded up."
24 DEFAULT 16384
25 UNQUOTE
26)
27
28config_string(CAmkESDefaultHeapSize CAMKES_DEFAULT_HEAP_SIZE
29 "Heap size to allocate per-component, in bytes."
30 DEFAULT 1048576
31 UNQUOTE
32)
33
34config_choice(CAmkESErrorHandlingMode CAMKES_ERROR_HANDLING_MODE
35 "Select the mode of error handling used in the glue code. It should only
36 be necessary to adjust this setting if you are doing verification.
37 Otherwise, the default error handling mechanism allows for
38 configuration at runtime.
39
40 Standard -> Standard error handling mechanism, that is configurable by the user at
41 runtime. See the documentation for details of the API for this.
42
43 Guards -> Use verification-visible guards at the site of each potential error.
44 Note that this assumes that none of the error conditions are possible.
45 If you are trying to verify code, you will be forced to prove that none
46 of the error conditions can ever actually occur.
47
48 Abort -> Call 'abort' inline when an error occurs. For debugging purposes, this
49 is probably not the behaviour you want as it will give you no
50 information about the error. The standard error handling mechanism has
51 a nicer default for debugging. This mode is primarily useful when you
52 want to verify code whose error handlers are unreachable for
53 non-trivial reasons.
54
55 Discard -> Perform the 'discard' action on any error that occurs. The advantage of
56 this over simply configuring this behaviour via the standard mechanism
57 is that you will not need to reason about any of the complicated error
58 handling structures or control flow. This has no implementation
59 advantages over the standard mechanism."
60 "Standard;CAmkESErrorHandlingConfigurable;CAMKES_ERROR_HANDLER_CONFIGURABLE"
61 "Guards;CAmkESErrorHandlingGuard;CAMKES_ERROR_HANDLER_GUARD"
62 "Abort;CAmkESErrorHandlingAbort;CAMKES_ERROR_HANDLER_ABORT"
63 "Discard;CAmkESErrorHandlingDiscard;CAMKES_ERROR_HANDLER_DISCARD"
64)
65
66config_option(CAmkESConnectorTiming CAMKES_CONNECTOR_TIMING
67 "Enable timing points within connector templates that take cycle counter
68 values as they are passed. This timing data can then be retrieved after
69 execution."
70 DEFAULT OFF
71)
72
73config_option(CAmkESProvideTCBCaps CAMKES_PROVIDE_TCB_CAPS
74 "Hand out TCB caps to components. These caps are used by the component
75 to exit cleanly by suspending. Disabling this option leaves components
76 with an empty slot in place of their TCB cap. This means they will cap
77 fault when attempting to exit. The advantage is that your resulting
78 CapDL specification contains no TCB caps and is thus easier to reason
79 about."
80 DEFAULT ON
81)
82
83config_choice(CAmkESTLSModel CAMKES_TLS_MODEL
84 "The CAmkES glue code uses thread-local variables for marshalling and
85 unmarshalling of RPC parameters. This setting controls how this thread-
86 local storage is implemented.
87
88 standard -> Allocate thread-local variables on the stack or the heap as appropriate.
89 This is the default and will hold the fewest surprises for C
90 programmers.
91
92 per-thread -> Allocate per-thread global variables for use as thread-local storage.
93 The main purpose of this implementation is to avoid taking the address
94 of local variables, an idiom that cannot be handled by the verification
95 C parser."
96 "standard;CAmkESTLSStandard;CAMKES_TLS_STANDARD"
97 "per-thread;CAmkESTLSPerThreadGlobal;CAMKES_TLS_PTG"
98)
99
Adrian Danis4a99eb32018-03-07 15:58:12 +1100100config_string(CAmkESDefaultPriority CAMKES_DEFAULT_PRIORITY
101 "Default priority for component threads if this is not overridden via an
102 attribute. Generally you want to set this as high as possible due to
103 the suboptimal seL4 scheduler."
104 # Default to one less than max prio to avoid interleaving with the CapDL intialiser
105 DEFAULT 254
106 UNQUOTE
107)
108if ((${CAmkESDefaultPriority} LESS 0) OR (${CAmkESDefaultPriority} GREATER 255))
109 message(FATAL_ERROR "CAmkESDefaultPriority must be [0, 255]")
110endif()
111
Adrian Danisec8f7092017-10-16 16:47:58 +1100112add_config_library(camkes_config "${configure_string}")
113
114# These options are not declared with the config_* system because they only need to exist
115# in the build system, and not appear in a configuration library
116set(CAmkESCPP OFF CACHE BOOL
117 "Run CPP on the input specification(s) before parsing them into an AST.
118 This can allow you to write parameterised specs in the case of more
119 complex system"
120)
121
122set(CAmkESImportPath "" CACHE STRING
123 "CAmkES can include components and interfaces stored outside the current application
124 directory. This option is a space delimited list of absolute paths to directories
125 to be searched for components or interfaces included with angle brackets."
126)
127
Adrian Danisec8f7092017-10-16 16:47:58 +1100128set(CAmkESDefaultAffinity 0 CACHE STRING
129 # Default to 0 as this is the index assigned to the BSP (Boot Strap Processor) by seL4
130 "Default affinity for component threads if this is not overridden via an
131 attribute. Think carefully when organizing your applications for
132 multiprocessor operation"
133)
134math(EXPR MaxNumNodesMin1 "${KernelMaxNumNodes} - 1")
135if((${CAmkESDefaultAffinity} < 0) OR (${CAmkESDefaultAffinity} GREATER ${MaxNumNodesMin1}))
136 message(FATAL_ERROR "Invalid CAmkESDefaultAffinity")
137endif()
138
139set(CAmkESAllowForwardReferences OFF CACHE BOOL
140 "By default, you can only refer to objects in your specification which
141 have been defined before the point at which you reference them.
142 Selecting this option allows you to also reference objects that are
143 defined below the point at which the reference occurs. This option is
144 off by default because it leads to a slight performance degradation in
145 parsing specification"
146)
147
148set(CAmkESObjdumpMethod "auto" CACHE STRING
149 "Instead of using the internal ELF parsing functionality, it is
150 possible to call out to your toolchain's objdump to perform
151 required operations. This is more fragile than using internal
152 functionality, but can provide a performance boost in compilation
153 times. If you set this to auto (default), CAmkES will use your
154 toolchain's objdump if it is in your PATH.
155
156 off -> Disable the use of objdump for ELF symbol lookups. Lookups will be
157 done via standard built-in CAmkES mechanisms. This may be slightly
158 slower.
159
160 auto -> Automatically detect whether objdump is available for use for ELF
161 symbol lookups, and use it if so. This will result in the fastest
162 available method for ELF symbol lookup being used automatically and
163 is the recommended default.
164
165 on -> Use objdump for ELF symbol lookups. Lookups will be done by calling
166 out to your toolchain's objdump binary. This is fastest at the
167 expense of some robustness."
168)
169set_property(CACHE CAmkESObjdumpMethod PROPERTY STRINGS "auto;on;off")
170
Adrian Danisec8f7092017-10-16 16:47:58 +1100171set(CAmkESRPCLockElision ON CACHE BOOL
172 "Detect when it is safe to exclude locking operations in the seL4RPC connector and
173 automatically do so. This is an optimisation that can improve the performance of
174 this connector."
175)
176
177set(CAmkESSpecialiseSyscallStubs ON CACHE BOOL
178 "Detect when glue code overhead could be reduced with a custom syscall
179 stub and generate and use this instead of the libsel4 stubs. This does
180 not affect whether a given IPC will hit the fastpath, but it does
181 reduce the userlevel overhead of these system calls. In ideal
182 conditions this will give you RPC as fast as native seL4 IPC. This only
183 has an effect on ARM."
184)
185
186set(CAmkESLargeFramePromotion ON CACHE BOOL
187 "Some hardware platforms support multiple page sizes. In components with
188 large virtual address spaces, it is possible to reduce memory usage
189 (and consequent load time) by backing the component's address space with
190 pages of these larger sizes. When this setting is enabled, small
191 consecutive page mappings will be promoted to fewer consecutive large
192 mappings. Note that larger frame sizes are directly mapped into page
193 directories and can also save the overhead of an accompanying page
194 table."
195)
196
197set(CAmkESDMALargeFramePromotion OFF CACHE BOOL
198 "For components with a configured DMA pool, the frames backing this
199 are not automatically promoted to large frames even if the pool is
200 sufficiently large. Select this option to enable such promotion
201 automatically. This is off by default because it requires support
202 for large alignments in your toolchain's assembler, which is often
203 absent in ARM toolchains."
204)
205
206set(CAmkESPythonOptimisation "none" CACHE STRING
207 "Select the optimisation flag to pass to the Python interpreter. The
208 default is for no optimisation because profiling has suggested this
209 has a detrimental effect for CAmkES. However, you may find
210 different results depending on your wor
211
212 none -> Do not pass any optimisation flags to the Python interpreter.
213
214 -O -> Enable basic optimisations. This disables assertions and is not
215 recommended if you are working on the internals of CAmkES itself.
216
217 -OO -> Enable basic optimisations and also strip docstrings."
218)
219set_property(CACHE CAmkESPythonOptimisation PROPERTY STRINGS "none;-O;-OO")
220
221set(CAmkESPythonInterpreter "cpython" CACHE STRING
222 "Select the Python interpreter used for executing CAmkES. The default
223 CPython interpreter should be acceptable for any normal use, but you
224 may find PyPy provides better build system performance under some
225 circumstances. To use PyPy, obviously you need it installed. The other
226 interpreters are for profiling or dynamic analysis.
227
228 cpython -> Use CPython, the default Python interpreter. This is what will be
229 most familiar to Python users.
230
231 cpython2 -> Force the use of Python 2, instead of the default Python
232 executable.
233
234 cpython3 -> Force the use of Python 3, instead of the default Python
235 executable. Note that Python 3 support is currently experimental
236 and should not be expected to work without tweaks.
237
238 pypy -> Use PyPy, an optimised Python interpreter. PyPy is intended to be
239 faster than CPython with maximum compatibility, but it is not
240 recommended for use with CAmkES because profiling has indicated it
241 is actually *slower* in general for CAmkES' workload.
242
243 figleaf -> Use Figleaf, an interpreter that reports code coverage statistics.
244 This interpreter is primarily useful for profiling or debugging
245 CAmkES itself.
246
247 coverage -> Use Python-coverage, an interpreter that reports code coverage
248 statistics. This interpreter is primarily useful for profiling or
249 debugging CAmkES itself."
250)
251set_property(CACHE CAmkESPythonInterpreter PROPERTY STRINGS "cpython;cpython2;cpython3;pypy;figleaf;coverage")
252
253set(CAmkESFaultHandlers ON CACHE BOOL
254 "When a component references invalid virtual memory or an invalid
255 capability, the access generates a fault. With this option selected
256 a handler is provided that decodes this fault for debugging
257 purposes. You will want to disable this in a production system or in
258 a system where you want to handle your own faults."
259)
260
261set(CAmkESSupportInit ON CACHE BOOL
262 "Support the pre_init, post_init and interface init functions as part of
263 component startup. These functions allow extra functionality, but
264 introduce some endpoint caps for synchronisation. You probably want
265 this option enabled unless you are targetting verification."
266)
267
268# TODO: The following options are not yet supported in cmake build template, as a result
269# these are currently commented out to as not to confuse users. They should be uncommented
270# as support is added
271#set(CAmkESPruneGenerated OFF CACHE BOOL
272# "Prune generated C files
273# When selected, this option minimises the number of C functions in a
274# given generated file. This can be done because the CAmkES generation
275# logic knows which functions are required by the user's components and
276# which are not. This option implies a separate pre-process step on the
277# generated files prior to pruning/compilation, otherwise the generated
278# C files are already minimal. Note, you will need libclang-dev installed
279# to enable this option."
280#)
281
282#set(CAmkESThys OFF CACHE BOOL
283# "Generate correctness proofs
284# Generate AutoCorres-based theories of connector correctness during
285# compilation."
286#)
287
288#set(CAmkESUnifiedThy OFF CACHE BOOL
289# "Generate unified correctness proof
290# Generate an AutoCorred-based theory combining the two glue code halves
291# of a connector, resulting in a final correctness statement."
292# DEPENDS CAmkESPruneGenerated
293#)
294
295#set(CAmkESArchThy OFF CACHE BOOL
296# "Generate architectural specification
297# Generate an Isabelle theory specifying the architecture of the
298# system, using the l4.verified formal model of ADL."
299#)
300
301#set(CAmkESCImpThy OFF CACHE BOOL
302# "Generate dynamic behavioural specification
303# Generate an Isabelle theory specifying the dynamic behaviour of the
304# system. This theory builds on top of the CIMP formalisation."
305#)
306
307#set(CAmkESCapDLThy OFF CACHE BOOL
308# "Generate CapDL Isabelle specification
309# During a CAmkES build, a textual CapDL specification of the system
310# is generated for the purpose of initialisation. Selecting this
311# option causes an Isabelle version of this specification to be
312# generated as well for the purposes of reasoning about the
313# capability distribution of a CAmkES system"
314#)
315
316#set(CAmkESLabelMapping OFF CACHE BOOL
317# "Generate policy label mapping
318# Enable this option to generate a mapping from labels to kernel objects
319# during compilation. A label per-CAmkES entity (component instance or
320# connection) is generated and they are intended to form the input domain
321# of a function mapping these to final policy labels. The final labels
322# are then used to reason about the security properties of a system."
323#)
324
325set(CAmkESVerbose OFF CACHE BOOL
326 "Enable verbose output from CAmkES. This is disabled by default as it
327 can result in a lot of output, but is useful for debugging CAmkES problems"
328)
329
Adrian Danisca89b102018-03-14 16:41:18 +1100330# Save the path to to python-capdl whilst we know it (unless it was already specified)
331if (NOT PYTHON_CAPDL_PATH)
Kent McLeodf5d7fd62018-07-24 13:43:44 +1000332 set(PYTHON_CAPDL_PATH "${CMAKE_SOURCE_DIR}/projects/capdl/python-capdl-tool")
Adrian Danisca89b102018-03-14 16:41:18 +1100333endif()
334if (NOT CAPDL_TOOL_SOURCE_PATH)
Kent McLeodf5d7fd62018-07-24 13:43:44 +1000335 set(CAPDL_TOOL_SOURCE_PATH "${CMAKE_SOURCE_DIR}/projects/capdl/capDL-tool")
Adrian Danisca89b102018-03-14 16:41:18 +1100336endif()
Adrian Danisec8f7092017-10-16 16:47:58 +1100337
338# Save the location of the camkes tool wrapper script
339RequireFile(CAMKES_TOOL camkes.sh PATHS "${CMAKE_CURRENT_LIST_DIR}")
340
341# Use the camkes script to determine the location of other things
342get_filename_component(CAMKES_TOOL_DIR "${CAMKES_TOOL}" DIRECTORY)
343set(CAMKES_TOOL_BUILTIN_DIR "${CAMKES_TOOL_DIR}/include/builtin")
344
Adrian Danisec8f7092017-10-16 16:47:58 +1100345# Require the parse-capDL tool
346ExternalProject_Add(parse_capdl_tool
347 SOURCE_DIR "${CAPDL_TOOL_SOURCE_PATH}"
348 CONFIGURE_COMMAND bash -c "cp -ra ${CAPDL_TOOL_SOURCE_PATH}/* ."
349 BUILD_ALWAYS ON
350 BUILD_COMMAND ${CMAKE_COMMAND} -E env "CONFIG_CAPDL_LOADER_MAX_IRQS=${CapDLLoaderMaxIRQs}" make
351 INSTALL_COMMAND ${CMAKE_COMMAND} -E env "PATH=$ENV{PATH}:${CMAKE_CURRENT_BINARY_DIR}/parse_capdl_tool-prefix/src/parse_capdl_tool-build" make install
352)
353ExternalProject_Get_property(parse_capdl_tool BINARY_DIR)
354set(CAPDL_TOOL_PATH "${BINARY_DIR}")
355
356# Search for a FMT tool for reformatting generated CAmkES C files
357find_program(CLANG_FORMAT_TOOL clang-format)
358if ("${CLANG_FORMAT_TOOL}" STREQUAL "CLANG_FORMAT_TOOL-NOTFOUND")
359 set(CAMKES_C_FMT_INVOCATION "")
360else()
361 set(CAMKES_C_FMT_INVOCATION "${CLANG_FORMAT_TOOL} --style=LLVM")
362endif()
363
364# Find the sponge tool, or emulate it
365find_program(SPONGE_TOOL sponge)
366if ("${SPONGE_TOOL}" STREQUAL "SPONGE_TOOL-NOTFOUND")
Adrian Danis0fdc9d62018-06-22 15:01:49 +1000367 set(CAMKES_SPONGE_INVOCATION "sh ${CMAKE_CURRENT_BINARY_DIR}/sponge_emul.sh")
Adrian Danisec8f7092017-10-16 16:47:58 +1100368 file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/sponge_emul.sh" "python -c 'import sys; data = sys.stdin.read(); f = open(sys.argv[1], \"w\"); f.write(data); f.close()' $@")
369else()
370 set(CAMKES_SPONGE_INVOCATION "${SPONGE_TOOL}")
371endif()
372
373# Find the Isabelle theory pre-process for formatting theory files
Kent McLeodf5d7fd62018-07-24 13:43:44 +1000374find_program(TPP_TOOL tpp PATHS ${CMAKE_CURRENT_LIST_DIR}/tools)
Adrian Danisec8f7092017-10-16 16:47:58 +1100375if ("${TPP_TOOL}" STREQUAL "TPP_TOOL-NOTFOUND")
376 message(FATAL_ERROR "Failed to find tpp tool")
377endif()
378
379# CAmkES defines its own heaps and for this to work muslcsys must not be configured to
380# use a static morecore. We make the morecore dynamic by setting the size to 0
381set(LibSel4MuslcSysMorecoreBytes 0 CACHE STRING "" FORCE)
382
383# Function to help build the CAMKES_TOOL_ENVIRONMENT below
384function(camkes_append_env_if)
385 # Loop through each pair of arguments and build the environment
386 set(local_env "${CAMKES_TOOL_ENVIRONMENT}")
387 math(EXPR limit "${ARGC} - 1")
388 foreach(i RANGE 0 ${limit} 2)
389 math(EXPR ip1 "${i} + 1")
390 set(check "${ARGV${i}}")
391 string(REGEX REPLACE " +" ";" check "${check}")
392 if(${check})
393 # Add the environment
394 list(APPEND local_env "${ARGV${ip1}}=1")
395 endif()
396 endforeach()
397 set(CAMKES_TOOL_ENVIRONMENT "${local_env}" PARENT_SCOPE)
398endfunction(camkes_append_env_if)
399
400function(camkes_append_flags)
401 math(EXPR limit "${ARGC} - 1")
402 set(local_flags "${CAMKES_FLAGS}")
403 foreach(i RANGE 0 ${limit})
404 set(list "${ARGV${i}}")
405 list(GET list 0 check)
406 string(REGEX REPLACE " +" ";" check "${check}")
407 if(${check})
408 list(GET list 1 when_true)
409 list(APPEND local_flags "${when_true}")
410 else()
411 list(LENGTH list len)
412 if (${len} GREATER 2)
413 list(GET list 2 when_false)
414 list(APPEND local_flags "${when_false}")
415 endif()
416 endif()
417 endforeach()
418 set(CAMKES_FLAGS "${local_flags}" PARENT_SCOPE)
419endfunction(camkes_append_flags)
420
421# This is called from the context of a CAmkES application that has decided what the 'root'
422# application is. This function will effectively generate a rule for building the final
423# rootserver image
424function(DeclareCAmkESRootserver adl)
425 cmake_parse_arguments(PARSE_ARGV 1 CAMKES_ROOT
426 "" # Option arguments
427 "" # Single arguments
428 "CPP_FLAGS;CPP_INCLUDES" # Multiple aguments
429 )
430 # Stash this request as a global property. The main CAmkES build file will call
431 # GenerateCAmkESRootserver later once all the build scripts are processed
432 get_property(declared GLOBAL PROPERTY CAMKES_ROOT_DECLARED)
433 if (declared)
434 message(FATAL_ERROR "A CAmkES rootserver was already declared")
435 endif()
436 foreach(include IN LISTS CAMKES_ROOT_CPP_INCLUDES)
Kent McLeod94369c42018-07-24 13:46:25 +1000437 get_absolute_list_source_or_binary(include "${include}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100438 list(APPEND CAMKES_ROOT_CPP_FLAGS "-I${include}")
439 endforeach()
Kent McLeod94369c42018-07-24 13:46:25 +1000440 get_absolute_list_source_or_binary(adl "${adl}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100441 set_property(GLOBAL PROPERTY CAMKES_ROOT_ADL "${adl}")
442 set_property(GLOBAL PROPERTY CAMKES_ROOT_CPP_FLAGS "${CAMKES_ROOT_CPP_FLAGS}")
443 set_property(GLOBAL PROPERTY CAMKES_ROOT_DECLARED TRUE)
444endfunction(DeclareCAmkESRootserver)
445
Adrian Danis84a80212018-03-23 11:35:17 +1100446# This takes a camkes produced dependency file (this means we can assume one dependency
447# per line) and produces a cmake list of dependencies
448function(MakefileDepsToList mdfile output_variable)
449 file(READ "${mdfile}" raw_file)
450 # First remove the target of the dependency list
451 string(REGEX REPLACE "^[^:]*: \\\\\r?\n" "" string_deps "${raw_file}")
452 # Now turn the list of dependencies into a cmake list. We have assumed
453 # that this makefile dep file was generated by camkes and so it has one
454 # item per line
455 string(REGEX REPLACE "\\\\\r?\n" ";" deps "${string_deps}")
456 # Strip the space from each dep
457 foreach(dep IN LISTS deps)
458 # Strip extra spacing
459 string(STRIP "${dep}" dep)
460 list(APPEND final_deps "${dep}")
461 endforeach()
462 # Write the output to the parent
463 set("${output_variable}" "${final_deps}" PARENT_SCOPE)
464endfunction(MakefileDepsToList)
465
Adrian Danisec8f7092017-10-16 16:47:58 +1100466# Called to actually generate the definitions for the CAmkES rootserver. Due to its
467# use of properties for some configuration it needs to be run after all other build
468# scripts, typically by the main CAmkES build file
469function(GenerateCAmkESRootserver)
470 # Retrieve properties from the declare call above
471 get_property(declared GLOBAL PROPERTY CAMKES_ROOT_DECLARED)
472 if (NOT declared)
473 message(FATAL_ERROR "No CAmkES rootserver was declared")
474 endif()
475 get_property(adl GLOBAL PROPERTY CAMKES_ROOT_ADL)
476 get_property(CAMKES_ROOT_CPP_FLAGS GLOBAL PROPERTY CAMKES_ROOT_CPP_FLAGS)
477 set(CAMKES_TOOL_ENVIRONMENT "")
478 set(CAMKES_TOOL_DEPENDENCIES "")
479 # Build the environment expected by camkes, as well as the camkes.sh wrapper script
480 list(APPEND CAMKES_TOOL_ENVIRONMENT "PYTHONPATH=$ENV{PYTHONPATH}:${PYTHON_CAPDL_PATH}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100481 # List of 'if condition' 'definition to add' for building the environment exports
482 camkes_append_env_if(
Adrian Danisec8f7092017-10-16 16:47:58 +1100483 "${CAmkESObjdumpMethod} STREQUAL on" CONFIG_CAMKES_USE_OBJDUMP_ON
484 "${CAmkESObjdumpMethod} STREQUAL auto" CONFIG_CAMKES_USE_OBJDUMP_AUTO
485 "${CAmkESPythonOptimisation} STREQUAL -O" CONFIG_CAMKES_PYTHON_OPTIMISE_BASIC
486 "${CAmkESPythonOptimisation} STREQUAL -OO" CONFIG_CAMKES_PYTHON_OPTIMISE_MORE
487 "${CAmkESPythonInterpreter} STREQUAL cpython" CONFIG_CAMKES_PYTHON_INTERPRETER_CPYTHON
488 "${CAmkESPythonInterpreter} STREQUAL cpython2" CONFIG_CAMKES_PYTHON_INTERPRETER_CPYTHON2
489 "${CAmkESPythonInterpreter} STREQUAL cpython3" CONFIG_CAMKES_PYTHON_INTERPRETER_CPYTHON3
490 "${CAmkESPythonInterpreter} STREQUAL pypy" CONFIG_CAMKES_PYTHON_INTERPRETER_PYPY
491 "${CAmkESPythonInterpreter} STREQUAL figleaf" CONFIG_CAMKES_PYTHON_INTERPRETER_FIGLEAF
492 "${CAmkESPythonInterpreter} STREQUAL coverage" CONFIG_CAMKES_PYTHON_INTERPRETER_COVERAGE
493 )
494 # Use the path as constructed at generation time
495 list(APPEND CAMKES_TOOL_ENVIRONMENT "PATH=$ENV{PATH}")
496 get_filename_component(CAMKES_CDL_TARGET "${adl}" NAME_WE)
497 set(CAMKES_CDL_TARGET "${CMAKE_CURRENT_BINARY_DIR}/${CAMKES_CDL_TARGET}.cdl")
498 # Get an absolute reference to the ADL source
Kent McLeod94369c42018-07-24 13:46:25 +1000499 get_absolute_list_source_or_binary(CAMKES_ADL_SOURCE "${adl}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100500 # Declare a common CAMKES_FLAGS that we will need to give to every invocation of camkes
501 set(CAMKES_FLAGS
502 "--import-path=${CAMKES_TOOL_BUILTIN_DIR}"
503 --platform seL4
504 --architecture ${KernelSel4Arch}
505 --default-priority ${CAmkESDefaultPriority}
506 --default-affinity ${CAmkESDefaultAffinity}
Adrian Danisec8f7092017-10-16 16:47:58 +1100507 )
508 # Build extra flags from the configuration
509 # Each of these arguments is a CONDITION FLAG_IF_CONDITION_TRUE [FLAG_IF_CONDITION_FALSE]
510 camkes_append_flags(
511 "CAmkESVerbose;--debug"
Adrian Danisec8f7092017-10-16 16:47:58 +1100512 "KernelIsMCS;--realtime"
513 "CAmkESRPCLockElision;--frpc-lock-elision;--fno-rpc-lock-elision"
514 "CAmkESSpecialiseSyscallStubs;--fspecialise-syscall-stubs;--fno-specialise-syscall-stubs"
515 "CAmkESProvideTCBCaps;--fprovide-tcb-caps;--fno-provide-tcb-caps"
516 "CAmkESSupportInit;--fsupport-init;--fno-support-init"
517 "CAmkESLargeFramePromotion;--largeframe"
518 "CAmkESDMALargeFramePromotion;--largeframe-dma"
519 "CAmkESAllowForwardReferences;--allow-forward-references"
520 "CAmkESFaultHandlers;--debug-fault-handlers"
521 "CAmkESCPP;--cpp"
522 )
523 foreach(flag IN LISTS CAMKES_ROOT_CPP_FLAGS)
524 if(NOT CAmkESCPP)
525 message(FATAL_ERROR "Given CPP_FLAGS ${CAMKES_ROOT_CPP_FLAGS} but CAmkESCPP is disabled")
526 endif()
527 list(APPEND CAMKES_FLAGS "--cpp-flag=${flag}")
528 endforeach()
529 # Retrieve any extra import paths
530 get_property(imports GLOBAL PROPERTY CAmkESExtraImportPaths)
531 foreach(import IN LISTS imports)
532 list(APPEND CAMKES_FLAGS "--import-path=${import}")
533 endforeach()
534 # Retrieve any templte paths
535 get_property(templates GLOBAL PROPERTY CAmkESTemplatePaths)
536 foreach(template IN LISTS templates)
537 list(APPEND CAMKES_FLAGS --templates "${template}")
538 endforeach()
Adrian Danis0f24c722018-03-23 11:30:23 +1100539 # Need to ensure our camkes_gen folder exists as camkes will not create the directory
540 file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/camkes_gen")
541 set(deps_file "${CMAKE_CURRENT_BINARY_DIR}/camkes_gen/deps")
Adrian Danis2bf14a02018-03-23 11:45:22 +1100542 set(invoc_file "${CMAKE_CURRENT_BINARY_DIR}/camkes_gen/last_invocation")
Adrian Daniscf76ead2018-03-23 10:57:41 +1100543 set(gen_outfile "${CMAKE_CURRENT_BINARY_DIR}/camkes-gen.cmake")
Adrian Danisbd2f3752018-03-23 11:36:52 +1100544 set(camkes_invocation
Adrian Danisec8f7092017-10-16 16:47:58 +1100545 ${CMAKE_COMMAND} -E env ${CAMKES_TOOL_ENVIRONMENT} "${CAMKES_TOOL}"
546 --file "${CAMKES_ADL_SOURCE}"
547 --item camkes-gen.cmake
Adrian Daniscf76ead2018-03-23 10:57:41 +1100548 --outfile "${gen_outfile}"
Adrian Danis0f24c722018-03-23 11:30:23 +1100549 --makefile-dependencies "${deps_file}"
Adrian Danisec8f7092017-10-16 16:47:58 +1100550 ${CAMKES_FLAGS}
Adrian Danisbd2f3752018-03-23 11:36:52 +1100551 )
Adrian Danise2e22902018-03-23 11:41:59 +1100552 # We need to determine if we actually need to regenerate. We start by assuming that we do
553 set(regen TRUE)
Adrian Danis2bf14a02018-03-23 11:45:22 +1100554 if((EXISTS "${invoc_file}") AND (EXISTS "${deps_file}") AND (EXISTS "${gen_outfile}"))
555 file(READ "${invoc_file}" old_contents)
556 if ("${old_contents}" STREQUAL "${camkes_invocation}")
557 MakefileDepsToList("${deps_file}" deps)
558 # At this point assume we do not need to regenerate, unless we found a newer file
559 set(regen FALSE)
560 foreach(dep IN LISTS deps)
561 if("${dep}" IS_NEWER_THAN "${gen_outfile}")
562 set(regen TRUE)
563 break()
564 endif()
565 endforeach()
566 endif()
567 endif()
Adrian Danise2e22902018-03-23 11:41:59 +1100568 if (regen)
Adrian Danis2bf14a02018-03-23 11:45:22 +1100569 message(STATUS "camkes-gen.cmake is out of date. Regenerating...")
Adrian Danise2e22902018-03-23 11:41:59 +1100570 execute_process(
571 # First delete the data structure cache directory as this is a new build
572 COMMAND
573 ${CMAKE_COMMAND} -E remove_directory "${CMAKE_CURRENT_BINARY_DIRECTOR}/camkes_pickle"
574 COMMAND ${camkes_invocation}
575 RESULT_VARIABLE camkes_gen_error
576 OUTPUT_VARIABLE camkes_output
577 ERROR_VARIABLE camkes_output
578 )
Adrian Danis2bf14a02018-03-23 11:45:22 +1100579 file(WRITE "${invoc_file}" "${camkes_invocation}")
Adrian Danise2e22902018-03-23 11:41:59 +1100580 if (camkes_gen_error)
Kent McLeod6eb834f2018-07-13 12:02:07 +1000581 file(REMOVE ${gen_outfile})
Adrian Danise2e22902018-03-23 11:41:59 +1100582 message(FATAL_ERROR "Failed to generate camkes-gen.cmake: ${camkes_output}")
583 endif()
584 # Add dependencies
585 MakefileDepsToList("${deps_file}" deps)
586 set_property(DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" APPEND PROPERTY CMAKE_CONFIGURE_DEPENDS "${deps}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100587 endif()
588 # We set a property to indicate that we have done execute_process (which happens during the
589 # generation phase. This just allows us to do some debugging and detect cases where options
590 # are changed *after* this point that would have affected the execute_process
591 set_property(GLOBAL PROPERTY CAMKES_GEN_DONE TRUE)
Adrian Daniscf76ead2018-03-23 10:57:41 +1100592 include("${gen_outfile}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100593endfunction(GenerateCAmkESRootserver)
594
Adrian Danis3291bed2018-03-08 13:47:17 +1100595# Internal helper function for setting camkes component properties
596function(AppendCAmkESComponentTarget target_name)
Adrian Danisec8f7092017-10-16 16:47:58 +1100597 cmake_parse_arguments(PARSE_ARGV 1 CAMKES_COMPONENT
598 "" # Option arguments
Kent McLeodcede2f12018-07-19 18:39:48 +1000599 "CAKEML_HEAP_SIZE;CAKEML_STACK_SIZE;LINKER_LANGUAGE" # Single arguments
Adrian Danis4b2a8502018-07-02 17:02:27 +1000600 "SOURCES;CAKEML_SOURCES;INCLUDES;C_FLAGS;LD_FLAGS;LIBS" # Multiple aguments
Adrian Danisec8f7092017-10-16 16:47:58 +1100601 )
602 # Declare a target that we will set properties on
Adrian Danis3291bed2018-03-08 13:47:17 +1100603 if (NOT (TARGET "${target_name}"))
604 add_custom_target("${target_name}")
Adrian Danis810df602018-03-08 13:44:21 +1100605 endif()
Adrian Danisec8f7092017-10-16 16:47:58 +1100606 # Get absolute paths for the includes and sources
607 set(includes "")
608 set(sources "")
Adrian Danis4b2a8502018-07-02 17:02:27 +1000609 set(cakeml_sources "")
Adrian Danisec8f7092017-10-16 16:47:58 +1100610 foreach(inc IN LISTS CAMKES_COMPONENT_INCLUDES)
Kent McLeod94369c42018-07-24 13:46:25 +1000611 get_absolute_list_source_or_binary(inc "${inc}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100612 list(APPEND includes "${inc}")
613 endforeach()
614 foreach(file IN LISTS CAMKES_COMPONENT_SOURCES)
Kent McLeod94369c42018-07-24 13:46:25 +1000615 get_absolute_list_source_or_binary(file "${file}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100616 list(APPEND sources "${file}")
617 endforeach()
Adrian Danis4b2a8502018-07-02 17:02:27 +1000618 foreach(file IN LISTS CAMKES_COMPONENT_CAKEML_SOURCES)
Kent McLeod94369c42018-07-24 13:46:25 +1000619 get_absolute_list_source_or_binary(file "${file}")
Adrian Danis4b2a8502018-07-02 17:02:27 +1000620 list(APPEND cakeml_sources "${file}")
621 endforeach()
Adrian Danis3291bed2018-03-08 13:47:17 +1100622 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_INCLUDES "${includes}")
623 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_SOURCES "${sources}")
Adrian Danis4b2a8502018-07-02 17:02:27 +1000624 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_CAKEML_SOURCES "${cakeml_sources}")
Adrian Danis3291bed2018-03-08 13:47:17 +1100625 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_C_FLAGS "${CAMKES_COMPONENT_C_FLAGS}")
626 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_LD_FLAGS "${CAMKES_COMPONENT_LD_FLAGS}")
627 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_LIBS "${CAMKES_COMPONENT_LIBS}")
Adrian Danis4b2a8502018-07-02 17:02:27 +1000628 # Overwrite any previous CakeML heap or stack size
629 if (CAMKES_COMPONENT_CAKEML_HEAP_SIZE)
630 set_property(TARGET "${target_name}" PROPERTY COMPONENT_CAKEML_HEAP_SIZE "${CAMKES_COMPONENT_CAKEML_HEAP_SIZE}")
631 endif()
632 if (CAMKES_COMPONENT_CAKEML_STACK_SIZE)
633 set_property(TARGET "${target_name}" PROPERTY COMPONENT_CAKEML_STACK_SIZE "${CAMKES_COMPONENT_CAKEML_STACK_SIZE}")
634 endif()
Kent McLeodcede2f12018-07-19 18:39:48 +1000635 if (CAMKES_COMPONENT_LINKER_LANGUAGE)
636 set_property(TARGET "${target_name}" APPEND PROPERTY COMPONENT_LINKER_LANGUAGE "${CAMKES_COMPONENT_LINKER_LANGUAGE}")
637 endif()
Adrian Danis3291bed2018-03-08 13:47:17 +1100638endfunction(AppendCAmkESComponentTarget)
639
640# This is called by CAmkES components to declare information needed for the camkes-gen.cmake to
641# actually build them. Can be called multiple times to append additional information.
642function(DeclareCAmkESComponent name)
643 AppendCAmkESComponentTarget(CAmkESComponent_${name} ${ARGN})
Adrian Danisec8f7092017-10-16 16:47:58 +1100644endfunction(DeclareCAmkESComponent)
645
Kent McLeodd786bc22018-05-09 10:09:05 +1000646# Declare built-in components that are constructed from templates and have no source files
647DeclareCAmkESComponent(debug_server)
648DeclareCAmkESComponent(debug_serial)
649
Adrian Danis39b28602018-03-08 14:19:08 +1100650# Extend a particular instantiation of a CAmkES component with additional information. This takes
651# similar arguments to DeclareCAmkESComponent and all of the declared includes, flags etc also
652# apply to the sources from DeclareCAmkESComponent. The includes provided here will be passed
653# prior to the original includes allowing for overriding. This can be called multiple times for the
654# same instance to repeatedly extend it. Similar flags will be placed after.
655function(ExtendCAmkESComponentInstance component_name instance_name)
656 AppendCAmkESComponentTarget(CAmkESComponent_${component_name}_instance_${instance_name} ${ARGN})
657endfunction(ExtendCAmkESComponentInstance)
658
Adrian Danisec8f7092017-10-16 16:47:58 +1100659# Helper function for adding additional import paths. Largely it exists to allow list
660# files to give relative paths and have them automatically expanded to absolute paths
661# We add the import paths to a property, instead of a target, since we need to use
662# it in an `execute_process` above, which cannot take generator expressions
663function(CAmkESAddImportPath)
664 # Ensure we haven't generated the camkes-gen.cmake yet
665 get_property(is_done GLOBAL PROPERTY CAMKES_GEN_DONE)
666 if (is_done)
667 message(FATAL_ERROR "Adding import path after camkes-gen.cmake has been generated")
668 endif()
669 foreach(arg IN LISTS ARGV)
Kent McLeod94369c42018-07-24 13:46:25 +1000670 get_absolute_list_source_or_binary(arg "${arg}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100671 set_property(GLOBAL APPEND PROPERTY CAmkESExtraImportPaths "${arg}")
672 endforeach()
673endfunction(CAmkESAddImportPath)
674function(CAmkESAddTemplatesPath)
675 # Ensure we haven't generated the camkes-gen.cmake yet
676 get_property(is_done GLOBAL PROPERTY CAMKES_GEN_DONE)
677 if (is_done)
678 message(FATAL_ERROR "Adding templates path after camkes-gen.cmake has been generated")
679 endif()
680 foreach(arg IN LISTS ARGV)
Kent McLeod94369c42018-07-24 13:46:25 +1000681 get_absolute_list_source_or_binary(arg "${arg}")
Adrian Danisec8f7092017-10-16 16:47:58 +1100682 set_property(GLOBAL APPEND PROPERTY CAmkESTemplatePaths "${arg}")
683 endforeach()
684endfunction(CAmkESAddTemplatesPath)