1# 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.8.2) 14 15include(debug) 16 17# /*? macros.generated_file_notice() ?*/ 18 19# Define names for tools we will use 20set(OBJCOPY ${CROSS_COMPILER_PREFIX}objcopy) 21 22# Declare our 'core' CAmkES libraries. These are the libraries that are considered minimal for the 23# glue code that is linked to camkes applications to run 24set(CAMKES_CORE_LIBS "sel4;sel4runtime;muslc;sel4camkes;sel4sync;utils;sel4vka;sel4utils;sel4bench;sel4platsupport;platsupport;sel4vspace;sel4muslcsys;sel4camkes_Config;sel4runtime_Config;sel4_autoconf") 25 26# The main function generated by CAmkES does not conform to the standard main 27# signatures, so disable warnings for this. 28set(CAMKES_C_FLAGS "-Wno-main") 29 30/*- set instances = composition.instances -*/ 31/*- set connections = composition.connections -*/ 32 33/*# The terms 'group' and 'address space' are currently synonymous. We can 34 *# derive the groups by collecting all the instances' address spaces. 35 #*/ 36/*- set groups = set(map(lambda('x: x.address_space'), filter(lambda('x: not x.type.hardware'), instances))) -*/ 37 38# We build up a list of all the generated items that we want to construct a single 39# camkes invocation 40set(item_list "") 41set(outfile_list "") 42set(template_list "") 43set(reflow_commands "") 44set(deps_list "") 45set(camkes_ver_opts "") 46 47macro(ParentListAppend list) 48 set(local_list_value "${${list}}") 49 list(APPEND local_list_value ${ARGN}) 50 set(${list} "${local_list_value}" PARENT_SCOPE) 51endmacro(ParentListAppend list) 52 53# Helper function for declaring a generated file 54function(CAmkESGen output item template) 55 cmake_parse_arguments(PARSE_ARGV 3 CAMKES_GEN "SOURCE;C_STYLE;THY_STYLE" "SOURCES_VAR;VER_BASE_NAME" "DEPENDS") 56 if (NOT "${CAMKES_GEN_UNPARSED_ARGUMENTS}" STREQUAL "") 57 message(FATAL_ERROR "Unknown arguments to CAmkESGen: ${CAMKES_GEN_UNPARSED_ARGUMENTS}") 58 endif() 59 # generate command 60 get_filename_component(out_dir "${output}" DIRECTORY) 61 # Reflow generated files if requested 62 if (CAMKES_GEN_C_STYLE AND (NOT ("${CAMKES_C_FMT_INVOCATION}" STREQUAL ""))) 63 ParentListAppend(reflow_commands COMMAND sh -c 64 "${CAMKES_C_FMT_INVOCATION} ${output} | ${CAMKES_SPONGE_INVOCATION} ${output}") 65 elseif(CAMKES_GEN_THY_STYLE) 66 ParentListAppend(reflow_commands COMMAND sh -c 67 "${TPP_TOOL} ${output} | ${CAMKES_SPONGE_INVOCATION} ${output}") 68 endif() 69 # Append the item and outfile 70 ParentListAppend(item_list "${item}") 71 ParentListAppend(outfile_list "${output}") 72 ParentListAppend(template_list "${template}") 73 ParentListAppend(deps_list "${CAMKES_GEN_DEPENDS}") 74 # Pass along base name for verification templates 75 if (NOT "${CAMKES_GEN_VER_BASE_NAME}" STREQUAL "") 76 ParentListAppend(camkes_ver_opts "--verification-base-name=${CAMKES_GEN_VER_BASE_NAME}") 77 endif() 78 # Add to the sources list if it's a source file 79 if (CAMKES_GEN_SOURCE) 80 if (CAMKES_GEN_SOURCES_VAR) 81 ParentListAppend("${CAMKES_GEN_SOURCES_VAR}" "${output}") 82 else () 83 ParentListAppend(gen_sources "${output}") 84 endif() 85 endif() 86 # Always add to the list of generated files 87 ParentListAppend(gen_files "${output}") 88endfunction(CAmkESGen) 89 90# Generate all the files declared previously. object_state_op is either 91# load- or save-object-state, depending on whether the object state has 92# already been built. 93function(CAmkESOutputGenCommand object_state_op object_state_file) 94 if ("${item_list}" STREQUAL "") 95 return() 96 endif() 97 list(LENGTH outfile_list outfile_list_count) 98 # Calculate the string length of ${CMAKE_BINARY_DIR} + 1 to do a hacky relative 99 # path calculation when editing our generated depfile. This is because, we need 100 # to calculate the depfile path depending on the top level build directory, but 101 # the tool generating the depfile only knows the current subdirectory and doesn't 102 # get told the top level one. 103 string(LENGTH ${CMAKE_BINARY_DIR} strlen) 104 math(EXPR strlen "${strlen} + 1") 105 set(depfile ${CMAKE_CURRENT_BINARY_DIR}/${object_state_op}moredeps) 106 string(COMPARE EQUAL ${object_state_op} "load-object-state" load_object_state) 107 set(object_file_depends) 108 set(object_file_output) 109 if(load_object_state) 110 set(object_file_depends ${object_state_file}) 111 else() 112 set(object_file_output ${object_state_file}) 113 endif() 114 add_custom_command( 115 OUTPUT ${outfile_list} ${object_file_output} 116 COMMAND 117 ${CAMKES_TOOL} 118 "--item;$<JOIN:${item_list},;--item;>" 119 "--outfile;$<JOIN:${outfile_list},;--outfile;>" 120 "--template;$<JOIN:${template_list},;--template;>" 121 "--load-ast=${CMAKE_CURRENT_BINARY_DIR}/ast.pickle" 122 "--${object_state_op}=${object_state_file}" 123 "--object-sizes=$<TARGET_PROPERTY:object_sizes,FILE_PATH>" 124 --makefile-dependencies "${depfile}" 125 ${camkes_ver_opts} 126 ${CAMKES_FLAGS} ${CAMKES_RENDER_FLAGS} 127 # For some reason, ninja only accepts relative targets. 128 # We truncate the first `strlen` chars which takes off the CMAKE_BINARY_DIR from the depfile. 129 COMMAND sh -c "dd if=${depfile} of=${depfile}.truncated bs=${strlen} skip=1 2> /dev/null && mv ${depfile}.truncated ${depfile}" 130 ${reflow_commands} 131 DEPENDS 132 ${CMAKE_CURRENT_BINARY_DIR}/ast.pickle 133 # This pulls in miscellaneous dependencies 134 # which is used by the camkes tool 135 ${CAMKES_TOOL_DEPENDENCIES} 136 # Any additional dependencies from the files 137 ${deps_list} 138 ${object_file_depends} 139 object_sizes 140 VERBATIM 141 DEPFILE "${depfile}" 142 ${USES_TERMINAL_DEBUG} 143 COMMAND_EXPAND_LISTS 144 COMMENT "Performing CAmkES generation for ${outfile_list_count} files" 145 ) 146 set(reflow_commands "" PARENT_SCOPE) 147 set(item_list "" PARENT_SCOPE) 148 set(deps_list "" PARENT_SCOPE) 149 set(outfile_list "" PARENT_SCOPE) 150 set(template_list "" PARENT_SCOPE) 151 set(camkes_ver_opts "" PARENT_SCOPE) 152endfunction(CAmkESOutputGenCommand) 153 154 155# Helper for constructing a generator expression that evalutes to the provided value if it exists, 156# or to a default value. 157# if maybe_value is the empty string 158# evaluate to the contents of default 159# else 160# evaluate to the contents of maybe_value 161# Both 'default' and 'maybe_value' can themselves be generator expressions, allow for chaining usages of 162# this together to build nested ORs. 163function(GeneratorValueOrDefault output default maybe_value) 164 set(new_output "$<IF:$<STREQUAL:${maybe_value},>,${default},${maybe_value}>") 165 set(${output} "${new_output}" PARENT_SCOPE) 166endfunction(GeneratorValueOrDefault) 167 168CAmkESGen("${CMAKE_CURRENT_BINARY_DIR}/graph.dot" assembly/ graph.dot) 169 170RequireFile(CONFIGURE_FILE_SCRIPT configure_file.cmake PATHS ${CMAKE_MODULE_PATH}) 171 172# A target for each binary that we need to build 173/*- for i in instances if not i.type.hardware -*/ 174 # Variable for collecting generated files 175 set(gen_files "") 176 set(gen_sources "") 177 set(cakeml_sources "") 178 # If no instance target exists declare it to simplify the logic of the generator expressions 179 set (instance_target "CAmkESComponent_/*? i.type.name ?*/_instance_/*? i.name ?*/") 180 if (NOT (TARGET ${instance_target})) 181 add_custom_target(${instance_target}) 182 endif() 183 if (NOT (TARGET CAmkESComponent_/*? i.type.name ?*/)) 184 add_custom_target(CAmkESComponent_/*? i.type.name ?*/) 185 endif() 186 # Retrieve the static sources for the component 187 set(static_sources "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_SOURCES>") 188 list(APPEND static_sources "$<TARGET_PROPERTY:${instance_target},COMPONENT_SOURCES>") 189 set(extra_c_flags "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_C_FLAGS>") 190 list(APPEND extra_c_flags "$<TARGET_PROPERTY:${instance_target},COMPONENT_C_FLAGS>") 191 set(extra_ld_flags "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_LD_FLAGS>") 192 list(APPEND extra_ld_flags "$<TARGET_PROPERTY:${instance_target},COMPONENT_LD_FLAGS>") 193 set(extra_libs "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_LIBS>") 194 list(APPEND extra_libs "$<TARGET_PROPERTY:${instance_target},COMPONENT_LIBS>") 195 # Retrieve the static headers for the component. Ensure instance headers are placed first 196 set(includes "$<TARGET_PROPERTY:${instance_target},COMPONENT_INCLUDES>") 197 list(APPEND includes "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_INCLUDES>") 198 set(generated_dir "${CMAKE_CURRENT_BINARY_DIR}//*? i.name ?*/") 199 # Generated different entry points for the instance 200 CAmkESGen("${generated_dir}/camkes.c" component//*? i.name ?*/ component.common.c SOURCE C_STYLE) 201 # Generate camkes header 202 203 unset(CMAKE_INTERFACE_INCLUDES) 204 CAmkESGen("${generated_dir}/include/camkes.h.in" component//*? i.name ?*/ component.template.h) 205 206 /*- if configuration[i.name].get('environment', 'c').lower() == 'c' -*/ 207 CAmkESGen("${generated_dir}/camkes.environment.c" component//*? i.name ?*/ component.environment.c SOURCE C_STYLE) 208 /*- elif configuration[i.name].get('environment').lower() == 'cakeml' -*/ 209 set(cakeml_sources "$<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_CAKEML_SOURCES>") 210 CAmkESGen("${generated_dir}/camkesStartScript.sml" component//*? i.name ?*/ component.environment.start.cakeml SOURCE SOURCES_VAR cakeml_sources) 211 CAmkESGen("${generated_dir}/camkesConstants.sml" component//*? i.name ?*/ camkesConstants.sml SOURCE SOURCES_VAR cakeml_sources) 212 CAmkESGen("${generated_dir}/camkesEndScript.sml" component//*? i.name ?*/ component.environment.end.cakeml SOURCE SOURCES_VAR cakeml_sources) 213 /*- else -*/ 214 /*? raise(TemplateError('Unknown environment')) ?*/ 215 /*- endif -*/ 216 217 # Generate our linker script 218 set(linker_file "${generated_dir}/linker.lds") 219 CAmkESGen("${linker_file}" component//*? i.name ?*/ linker.lds) 220 221 # Generate connectors for this instance 222 /*- for c in connections -*/ 223 /*- for id, e in enumerate(c.from_ends) -*/ 224 set(unique_name /*? e.interface.name ?*/_/*? c.type.name ?*/_/*? id ?*/) 225 /*- if e.instance.name == i.name -*/ 226 set(connector_target CAmkESConnector_/*? c.type.name ?*/) 227 get_property(c_from_template TARGET ${connector_target} PROPERTY CONNECTOR_FROM) 228 CAmkESGen("${generated_dir}/${unique_name}.c" connector//*? c.name ?*//from//*? id ?*/ ${c_from_template} SOURCE C_STYLE) 229 get_property(c_from_template_header TARGET ${connector_target} PROPERTY CONNECTOR_FROM_HEADER) 230 if (NOT "${c_from_template_header}" STREQUAL "") 231 CAmkESGen("${generated_dir}/include/${unique_name}.h" connector//*? c.name ?*//from//*? id ?*/ ${c_from_template_header} C_STYLE) 232 set(CMAKE_INTERFACE_INCLUDES "${CMAKE_INTERFACE_INCLUDES}#include <${unique_name}.h>\n") 233 endif() 234 get_property(c_from_libs TARGET ${connector_target} PROPERTY CONNECTOR_FROM_LIBS) 235 list(APPEND extra_libs ${c_from_libs}) 236 237 /*- endif -*/ 238 /*- endfor -*/ 239 /*- for id, e in enumerate(c.to_ends) -*/ 240 set(unique_name /*? e.interface.name ?*/_/*? c.type.name ?*/_/*? id ?*/) 241 /*- if e.instance.name == i.name -*/ 242 set(connector_target CAmkESConnector_/*? c.type.name ?*/) 243 244 /*- if configuration[i.name].get('environment', 'c').lower() == 'cakeml' -*/ 245 get_property(cake_to_template TARGET ${connector_target} PROPERTY CONNECTOR_CAKEML_TO) 246 if (NOT "${cake_to_template}" STREQUAL "") 247 CAmkESGen("${generated_dir}/connectorScript.sml" connector//*? c.name ?*//to//*? id ?*/ ${cake_to_template} SOURCE SOURCES_VAR cakeml_sources) 248 else() 249 get_property(c_to_template TARGET ${connector_target} PROPERTY CONNECTOR_TO) 250 CAmkESGen("${generated_dir}/${unique_name}.c" connector//*? c.name ?*//to//*? id ?*/ ${c_to_template} SOURCE C_STYLE) 251 endif() 252 /*- else -*/ 253 get_property(c_to_template TARGET ${connector_target} PROPERTY CONNECTOR_TO) 254 CAmkESGen("${generated_dir}/${unique_name}.c" connector//*? c.name ?*//to//*? id ?*/ ${c_to_template} SOURCE C_STYLE) 255 get_property(c_to_template_header TARGET ${connector_target} PROPERTY CONNECTOR_TO_HEADER) 256 if (NOT "${c_to_template_header}" STREQUAL "") 257 CAmkESGen("${generated_dir}/include/${unique_name}.h" connector//*? c.name ?*//to//*? id ?*/ ${c_to_template_header} C_STYLE) 258 set(CMAKE_INTERFACE_INCLUDES "${CMAKE_INTERFACE_INCLUDES}#include <${unique_name}.h>\n") 259 endif() 260 261 /*- endif -*/ 262 get_property(c_to_libs TARGET ${connector_target} PROPERTY CONNECTOR_TO_LIBS) 263 list(APPEND extra_libs ${c_to_libs}) 264 /*- endif -*/ 265 /*- endfor -*/ 266 /*- endfor -*/ 267 get_target_property(template_sources CAmkESComponent_/*? i.type.name ?*/ COMPONENT_TEMPLATE_SOURCES) 268 if (NOT "${template_sources}" STREQUAL "template_sources-NOTFOUND") 269 foreach(template_file IN LISTS template_sources) 270 get_filename_component(filename ${template_file} NAME) 271 CAmkESGen("${generated_dir}/${filename}" component//*? i.name ?*/ ${template_file} SOURCE C_STYLE) 272 endforeach() 273 endif() 274 get_target_property(template_headers CAmkESComponent_/*? i.type.name ?*/ COMPONENT_TEMPLATE_HEADERS) 275 if (NOT "${template_headers}" STREQUAL "template_headers-NOTFOUND") 276 foreach(template_file IN LISTS template_headers) 277 get_filename_component(filename ${template_file} NAME) 278 CAmkESGen("${generated_dir}/include/${filename}" component//*? i.name ?*/ ${template_file} C_STYLE) 279 set(CMAKE_INTERFACE_INCLUDES "${CMAKE_INTERFACE_INCLUDES}#include <${filename}>\n") 280 endforeach() 281 endif() 282 /*- if configuration[i.name].get('single_threaded') -*/ 283 CAmkESGen("${generated_dir}/seL4SingleThreadedComponent.template.c" component//*? i.name ?*/ seL4SingleThreadedComponent.template.c SOURCE C_STYLE) 284 CAmkESGen("${generated_dir}/include/seL4SingleThreadedComponent.template.h" component//*? i.name ?*/ seL4SingleThreadedComponent.template.h SOURCE C_STYLE) 285 set(CMAKE_INTERFACE_INCLUDES "${CMAKE_INTERFACE_INCLUDES}#include <seL4SingleThreadedComponent.template.h>\n") 286 /*- endif -*/ 287 288 /*- if configuration[i.name].get('debug') -*/ 289 CAmkESGen("${generated_dir}/camkes.debug.c" component//*? i.name ?*/ component.debug.c SOURCE C_STYLE) 290 /*- endif -*/ 291 /*- if configuration[i.name].get('simple') -*/ 292 CAmkESGen("${generated_dir}/camkes.simple.c" component//*? i.name ?*/ component.simple.c SOURCE C_STYLE) 293 /*- endif -*/ 294 /*- if configuration[i.name].get('rump_config') -*/ 295 CAmkESGen("${generated_dir}/camkes.rumprun.c" component//*? i.name ?*/ component.rumprun.c SOURCE C_STYLE) 296 /*- endif -*/ 297 298 # Add interface header files to camkes.h 299 file(WRITE "${generated_dir}/include/camkes.h.cmd" "${CMAKE_COMMAND} -DCONFIGURE_INPUT_FILE=\"${generated_dir}/include/camkes.h.in\" \ 300 -DCONFIGURE_OUTPUT_FILE=\"${generated_dir}/include/camkes.h\" -DCMAKE_INTERFACE_INCLUDES=\"${CMAKE_INTERFACE_INCLUDES}\" -P ${CONFIGURE_FILE_SCRIPT}") 301 add_custom_command(OUTPUT ${generated_dir}/include/camkes.h 302 COMMAND sh "${generated_dir}/include/camkes.h.cmd" 303 DEPENDS "${generated_dir}/include/camkes.h.in" "${generated_dir}/include/camkes.h.cmd" 304 ) 305 set_property(SOURCE /*? i.name ?*//camkes.c PROPERTY OBJECT_DEPENDS ${generated_dir}/include/camkes.h) 306 307 # Create a target for all our generated files 308 set(gen_target /*? i.name ?*/_generated) 309 add_custom_target(${gen_target} DEPENDS ${gen_files}) 310 # Build the actual binary 311 set(target /*? i.name ?*/.instance.bin) 312 add_executable(${target} EXCLUDE_FROM_ALL 313 ${static_sources} 314 ${gen_sources} 315 316 ) 317 # If COMPONENT_LINKER_LANGUAGE is set on the component target, set the LINKER_LANGUAGE of the executable 318 get_property(link_language TARGET CAmkESComponent_/*? i.type.name ?*/ PROPERTY COMPONENT_LINKER_LANGUAGE) 319 if (NOT "${link_language}" STREQUAL "") 320 set_property(TARGET ${target} PROPERTY LINKER_LANGUAGE ${link_language}) 321 endif() 322 # Build any CakeML library 323 if (NOT ("${cakeml_sources}" STREQUAL "")) 324 # Pull heap/stack size from component expression OR instances expression OR default to an arbitrary 50 325 # The order here is important as we want the instance property to be able to override the component property 326 GeneratorValueOrDefault(heap 50 $<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_CAKEML_HEAP_SIZE>) 327 GeneratorValueOrDefault(heap "${heap}" $<TARGET_PROPERTY:${instance_target},COMPONENT_CAKEML_HEAP_SIZE>) 328 GeneratorValueOrDefault(stack 50 $<TARGET_PROPERTY:CAmkESComponent_/*? i.type.name ?*/,COMPONENT_CAKEML_STACK_SIZE>) 329 GeneratorValueOrDefault(stack "${stack}" $<TARGET_PROPERTY:${instance_target},COMPONENT_CAKEML_STACK_SIZE>) 330 # Additional directories for the HOL build to depend on 331 get_property(cakeml_includes TARGET CAmkESComponent_/*? i.type.name ?*/ PROPERTY COMPONENT_CAKEML_INCLUDES) 332 get_property(cakeml_depends TARGET CAmkESComponent_/*? i.type.name ?*/ PROPERTY COMPONENT_CAKEML_DEPENDS) 333 DeclareCakeMLLib(/*? i.name ?*/_camkescakeml_contents 334 SOURCES "${cakeml_sources}" 335 TRANSLATION_THEORY "camkesEnd" 336 HEAP_SIZE "${heap}" 337 STACK_SIZE "${stack}" 338 RUNTIME_ENTRY "component_control_main" 339 CAKEML_ENTRY "camkes_entry" 340 INCLUDES ${cakeml_includes} 341 DEPENDS "${gen_target}" "${cakeml_depends}" 342 ) 343 target_link_libraries(${target} camkescakeml /*? i.name ?*/_camkescakeml_contents) 344 endif() 345 target_include_directories(${target} PRIVATE ${includes} "${generated_dir}/include") 346 # Depend upon core camkes libraries 347 target_link_libraries(${target} ${CAMKES_CORE_LIBS}) 348 # Depend upon additional libraries 349 target_link_libraries(${target} ${extra_libs}) 350 # Depend upon target that creates the generated source files 351 add_dependencies(${target} ${gen_target} CAmkESComponent_/*? i.type.name ?*/) 352 # Set our CAmkES specific additional link flags 353 set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS 354 " -static -nostdlib -u _camkes_start -e _camkes_start ") 355 # Add extra flags specified by the user 356 target_compile_options(${target} PRIVATE ${extra_c_flags} ${CAMKES_C_FLAGS}) 357 set_property(TARGET ${TARGET} APPEND_STRING PROPERTY LINK_FLAGS ${extra_ld_flags}) 358 # Only incrementally link if this instance is going on to become part of a 359 # group. 360 # TODO: we care about being grouped elsewhere as well. generalize this 361 /*- set grouped = [False] -*/ 362 /*- for inst in instances if not i.type.hardware -*/ 363 /*- if id(i) != id(inst) and inst.address_space == i.address_space -*/ 364 /*- do grouped.__setitem__(0, True) -*/ 365 /*- endif -*/ 366 /*- endfor -*/ 367 /*- if grouped[0] -*/ 368 set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " -Wl,--relocatable ") 369 /*- endif -*/ 370 set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " -Wl,--script=${linker_file} ") 371/*- endfor -*/ 372 373# We need to apply objcopy to each component instance's ELF before we link them 374# into a flattened binary in order to avoid symbol collision. Note that when we 375# mangle symbols, we use the prefix 'camkes ' to avoid colliding with any 376# user-provided symbols. 377/*- set instancelist = set() -*/ 378/*- for i in instances if not i.type.hardware -*/ 379 set(input_target /*? i.name ?*/.instance.bin) 380 set(output ${CMAKE_CURRENT_BINARY_DIR}//*? i.name ?*/.instance-copy.bin) 381 set(output_target /*? i.name ?*/_instance_copy_target) 382 set(input $<TARGET_FILE:${input_target}>) 383 add_custom_command( 384 OUTPUT "${output}" 385 COMMAND 386 # Brace yourself. This is going to be a bumpy ride. 387 ${OBJCOPY} 388 /*# Use a dummy impossible symbol of the empty string here, because 389 *# marking one symbol as 'keep global' causes all others to be demoted 390 *# to local. This allows us to avoid symbol collisions from 391 *# user-provided symbols. 392 #*/ 393 --keep-global-symbol "" 394 395 /*# Rename the entry point to avoid symbol conflicts when we are 396 *# colocated with other components. Note that we will still use this as 397 *# the entry point. 398 #*/ 399 --redefine-sym "_camkes_start=/*? "camkes %s _camkes_start" % i.name ?*/" 400 401 /*- for c in connections -*/ 402 /*- if c.type.name == 'seL4DirectCall' -*/ 403 /*# For all 'from' connection ends (calls to unresolved symbols), 404 *# rename the symbols so they will correctly link to the 405 *# implementations provided by the 'to' side. 406 #*/ 407 /*- for e in c.from_ends -*/ 408 /*- if id(e.instance) == id(i) -*/ 409 /*- for m in e.interface.type.methods -*/ 410 --redefine-sym "/*? e.interface.name ?*/_/*? m.name ?*/=camkes connection /*? e.parent.name ?*/_/*? m.name ?*/" 411 /*- endfor -*/ 412 /*- endif -*/ 413 /*- endfor -*/ 414 /*# For all 'to' connection ends (implementations of procedures), 415 *# rename the symbols so they will be found during the next 416 *# linking stage. Note we need to mark them as 'keep global' or 417 *# they will not be visible during the next link. 418 #*/ 419 /*- for e in c.to_ends -*/ 420 /*- if id(e.instance) == id(i) -*/ 421 /*- if '%s_%s' % (i.name, e.interface.name) in instancelist -*/ 422 /*- continue -*/ 423 /*- endif -*/ 424 /*- do instancelist.add('%s_%s' % (i.name, e.interface.name)) -*/ 425 /*- for m in e.interface.type.methods -*/ 426 --redefine-sym "/*? e.interface.name ?*/_/*? m.name ?*/=camkes connection /*? e.parent.name ?*/_/*? m.name ?*/" 427 --keep-global-symbol "camkes connection /*? e.parent.name ?*/_/*? m.name ?*/" 428 /*- endfor -*/ 429 /*- endif -*/ 430 /*- endfor -*/ 431 /*- endif -*/ 432 /*- endfor -*/ 433 "${input}" "${output}" 434 COMMAND 435 # Some toolchains insert exception handling infrastructure whether we ask 436 # for it or not. The preceding `objcopy` step breaks references in 437 # implicit `.eh_frame`s and friends, which then goes on to cause a linker 438 # warning. Rather than attempt some complicated gymnastics to repair these 439 # references, we just strip the exception handling pieces. To further 440 # complicate the process, some architectures require an `.eh_frame` and 441 # attempting to remove it causes errors. To handle this we just blindly 442 # try to remove it and mask errors. We can't do this unconditionally in 443 # the preceding `objcopy` because it fails when our toolchain has *not* 444 # inserted exception handling pieces or when we're targeting an 445 # architecture that requires `.eh_frame`. 446 bash -c "${OBJCOPY} --remove-section .eh_frame --remove-section .eh_frame_hdr \ 447 --remove-section .rel.eh_frame --remove-section .rela.eh_frame ${output} \ 448 >/dev/null 2>/dev/null" 449 VERBATIM 450 DEPENDS ${input_target} 451 ) 452 add_custom_target(/*? i.name ?*/_instance_copy_target DEPENDS "${output}") 453 # TODO target for dependencies 454/*- endfor -*/ 455 456# Define the linker we used for instances groups. This is just C linking but without crt objects 457# or any other libraries, we just want the flags to generate the correct binary type 458set(CMAKE_INSTANCE_GROUP_LINK_EXECUTABLE "<CMAKE_C_COMPILER> <FLAGS> <CMAKE_C_LINK_FLAGS> <LINK_FLAGS> <OBJECTS> -o <TARGET>" CACHE INTERNAL "" FORCE) 459# Finally link together the instances in the different groups */ 460/*- for g in groups -*/ 461 /*- set elf_name = "%s_group_bin" % g -*/ 462 list(APPEND key_names /*? g ?*/) 463 # Find all the instances that are part of this group */ 464 set(instances "") 465 set(instance_targets "") 466 /*- for i in instances if not i.type.hardware -*/ 467 /*- set other_elf_name = "%s_group_bin" % i.address_space -*/ 468 /*- if elf_name == other_elf_name -*/ 469 list(APPEND instances "/*? i.name ?*/.instance-copy.bin") 470 list(APPEND instance_targets "/*? i.name ?*/_instance_copy_target") 471 # Define the copies as objects in case we need to link them into a group and 472 # we would like cmake to not attempt to compile them 473 set_property(SOURCE "/*? i.name ?*/.instance-copy.bin" PROPERTY EXTERNAL_OBJECT TRUE) 474 /*- endif -*/ 475 /*- endfor -*/ 476 set(target ${CMAKE_CURRENT_BINARY_DIR}//*? elf_name ?*/) 477 list(LENGTH instances instances_len) 478 if (${instances_len} GREATER 1) 479 add_executable(/*? elf_name ?*/ EXCLUDE_FROM_ALL ${instances}) 480 add_dependencies(/*? elf_name ?*/ ${instance_targets}) 481 # Use a custom linker definition that will not include crt objects 482 set_property(TARGET /*? elf_name ?*/ PROPERTY LINKER_LANGUAGE INSTANCE_GROUP) 483 # Note that we deliberately give groups a 484 # broken entry point so that, if they are incorrectly loaded without correct 485 # initial instruction pointers, threads will immediately fault 486 set_property(TARGET /*? elf_name ?*/ APPEND PROPERTY LINK_FLAGS " -static -nostdlib --entry=0x0 -Wl,--build-id=none -T${TLS_LINKER_LDS}") 487 else() 488 add_custom_command( 489 OUTPUT ${target} 490 COMMAND 491 cp "${instances}" "${target}" 492 DEPENDS 493 ${instances} 494 ${instance_targets} 495 ) 496 endif() 497 add_custom_target(/*? elf_name ?*/_group_target DEPENDS "${target}") 498/*- endfor -*/ 499 500# Generate our targets up to this point 501CAmkESOutputGenCommand(save-object-state ${CMAKE_CURRENT_BINARY_DIR}/object.pickle) 502 503# CapDL generation. Aside from depending upon the CAmkES specifications themselves, it 504# depends upon the copied instance binaries and (optionally) the bootinfo untyped list. 505 506# First, find all instance binaries 507set(capdl_elf_depends "") 508set(capdl_elf_targets "") 509/*- for g in groups -*/ 510 /*- set elf_name = "%s_group_bin" % g -*/ 511 list(APPEND capdl_elfs "${CMAKE_CURRENT_BINARY_DIR}//*? elf_name ?*/") 512 list(APPEND capdl_elf_targets "/*? elf_name ?*/_group_target") 513/*- endfor -*/ 514 515# Generate boot untyped info for capDL allocator (if applicable) 516if(CAmkESCapDLStaticAlloc) 517 add_custom_command( 518 OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/untyped.yaml 519 COMMAND 520 ${CAPDL_UNTYPED_GEN} 521 "--input=${platform_yaml}" 522 "--output=${CMAKE_CURRENT_BINARY_DIR}/untyped.yaml" 523 "--linker=${CMAKE_CURRENT_BINARY_DIR}/linker.lds" 524 --architecture ${KernelSel4Arch} 525 "--object-sizes=$<TARGET_PROPERTY:object_sizes,FILE_PATH>" 526 --dtb-size ${KernelDTBSize} 527 --kernel-elf "$<TARGET_FILE:kernel.elf>" 528 "$<$<BOOL:${capdl_elfs}>:--elffile$<SEMICOLON>>$<JOIN:${capdl_elfs},$<SEMICOLON>--elffile$<SEMICOLON>>" 529 DEPENDS 530 # This pulls in miscellaneous dependencies 531 # which is used by the camkes tool 532 ${CAPDL_UNTYPED_GEN_DEPENDENCIES} 533 object_sizes 534 ${platform_yaml} 535 ${capdl_elfs} 536 VERBATIM 537 ${USES_TERMINAL_DEBUG} 538 COMMAND_EXPAND_LISTS 539 COMMENT "Generating untyped list" 540 ) 541 add_custom_target(untyped_capdl_target DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/untyped.yaml") 542 set(CAPDL_UNTYPED_YAML_FILE "${CMAKE_CURRENT_BINARY_DIR}/untyped.yaml") 543else() 544 add_custom_target(untyped_capdl_target) 545 set(CAPDL_UNTYPED_YAML_FILE "") 546endif() 547 548# Now, define the capDL spec generation from CAmkES 549if(CAmkESCapDLStaticAlloc) 550 set(CAPDL_LINKER_ALLOC_OPT "--static-alloc") 551 set(CAPDL_LINKER_UNTYPED_OPT "--untyped=${CAPDL_UNTYPED_YAML_FILE}") 552else() 553 set(CAPDL_LINKER_ALLOC_OPT "--dynamic-alloc") 554 set(CAPDL_LINKER_UNTYPED_OPT "") 555endif() 556add_custom_command( 557 OUTPUT ${CAMKES_CDL_TARGET} ${CMAKE_CURRENT_BINARY_DIR}/object-final.pickle 558 COMMAND 559 ${CAPDL_LINKER} 560 "--object-sizes=$<TARGET_PROPERTY:object_sizes,FILE_PATH>" 561 --architecture ${KernelSel4Arch} 562 gen_cdl 563 "--manifest-in=${CMAKE_CURRENT_BINARY_DIR}/object.pickle" 564 "--save-object-state=${CMAKE_CURRENT_BINARY_DIR}/object-final.pickle" 565 ${CAPDL_LINKER_ALLOC_OPT} 566 ${CAPDL_LINKER_UNTYPED_OPT} 567 "$<$<BOOL:${capdl_elfs}>:--elffile$<SEMICOLON>>$<JOIN:${capdl_elfs},$<SEMICOLON>--elffile$<SEMICOLON>>" 568 "$<$<BOOL:${key_names}>:--key$<SEMICOLON>>$<JOIN:${key_names},$<SEMICOLON>--key$<SEMICOLON>>" 569 --outfile ${CAMKES_CDL_TARGET} 570 DEPENDS 571 ${CMAKE_CURRENT_BINARY_DIR}/ast.pickle 572 # This pulls in miscellaneous dependencies 573 # which is used by the camkes tool 574 ${CAPDL_LINKER_DEPENDENCIES} 575 # Any additional dependencies from the files 576 ${CMAKE_CURRENT_BINARY_DIR}/object.pickle 577 object_sizes 578 untyped_capdl_target 579 ${CAPDL_UNTYPED_YAML_FILE} 580 ${capdl_elfs} 581 ${capdl_elf_targets} 582 VERBATIM 583 ${USES_TERMINAL_DEBUG} 584 COMMAND_EXPAND_LISTS 585 COMMENT "Generating final \"${CAMKES_CDL_TARGET}\" file" 586) 587add_custom_target(camkes_capdl_target DEPENDS "${CAMKES_CDL_TARGET}" "${CMAKE_CURRENT_BINARY_DIR}/object-final.pickle") 588add_dependencies(camkes_capdl_target object_sizes ${capdl_elf_targets}) 589 590# Invoke the parse-capDL tool to turn the CDL spec into a C spec 591CapDLToolCFileGen(capdl_c_spec_target capdl_spec.c ${CAmkESCapDLStaticAlloc} "$<TARGET_PROPERTY:object_sizes,FILE_PATH>" "${CAMKES_CDL_TARGET}" "${CAPDL_TOOL_BINARY}" 592 DEPENDS camkes_capdl_target install_capdl_tool "${CAPDL_TOOL_BINARY}") 593 594# Ask the CapDL tool to generate an image with our given copied/mangled instances 595BuildCapDLApplication( 596 C_SPEC "capdl_spec.c" 597 /*- for g in groups -*/ 598 ELF "${CMAKE_CURRENT_BINARY_DIR}//*? "%s_group_bin" % g ?*/" 599 /*- endfor -*/ 600 DEPENDS 601 # Dependency on the C_SPEC and ELFs are added automatically, we just have to add the target 602 # dependencies 603 capdl_c_spec_target 604 ${capdl_elf_targets} 605 OUTPUT "capdl-loader" 606) 607include(rootserver) 608DeclareRootserver("capdl-loader") 609 610# Generate Isabelle theory scripts if needed 611if (CAmkESCapDLVerification) 612 # Base name for Isabelle theories. We derive this from the top-level ADL name, 613 # but mangled to ensure that it is a valid identifier. 614 get_filename_component(VER_BASE_NAME "${adl}" NAME_WE) 615 string(MAKE_C_IDENTIFIER "${VER_BASE_NAME}" VER_BASE_NAME) 616 617 # Generated theory names. These must be consistent with the templates. 618 set(CAMKES_CDL_THY "${CMAKE_CURRENT_BINARY_DIR}/cdl-refine/${VER_BASE_NAME}_CDL.thy") 619 set(CAMKES_ADL_THY "${CMAKE_CURRENT_BINARY_DIR}/cdl-refine/${VER_BASE_NAME}_Arch_Spec.thy") 620 set(CAMKES_CDL_REFINE_THY "${CMAKE_CURRENT_BINARY_DIR}/cdl-refine/${VER_BASE_NAME}_CDL_Refine.thy") 621 set(CAMKES_VER_ROOT "${CMAKE_CURRENT_BINARY_DIR}/cdl-refine/ROOT") 622 623 # ROOT file 624 CAmkESGen("${CAMKES_VER_ROOT}" assembly/ "root.thy" THY_STYLE VER_BASE_NAME ${VER_BASE_NAME}) 625 add_custom_target(isabelle_root DEPENDS "${CAMKES_VER_ROOT}") 626 627 # Generate these theory files as part of overall build 628 # FIXME: hack? 629 add_dependencies("capdl-loader" isabelle_root) 630 631 # Isabelle capDL spec 632 add_custom_command( 633 OUTPUT "${CAMKES_CDL_THY}" 634 COMMAND 635 ${CAPDL_TOOL_BINARY} 636 --isabelle "${CAMKES_CDL_THY}" 637 --object-sizes "$<TARGET_PROPERTY:object_sizes,FILE_PATH>" 638 "${CAMKES_CDL_TARGET}" 639 DEPENDS 640 "${CAMKES_CDL_TARGET}" 641 camkes_capdl_target 642 "${CAPDL_TOOL_BINARY}" 643 install_capdl_tool 644 "$<TARGET_PROPERTY:object_sizes,FILE_PATH>" 645 ) 646 add_custom_target(camkes_cdl_thy DEPENDS "${CAMKES_CDL_THY}") 647 add_dependencies(isabelle_root camkes_cdl_thy) 648 649 # ADL spec 650 CAmkESGen("${CAMKES_ADL_THY}" assembly/ "arch-definitions.thy" THY_STYLE VER_BASE_NAME ${VER_BASE_NAME}) 651 add_custom_target(camkes_adl_thy DEPENDS "${CAMKES_ADL_THY}") 652 add_dependencies(isabelle_root camkes_adl_thy) 653 654 # CDL refinement proof 655 CAmkESGen("${CAMKES_CDL_REFINE_THY}" assembly/ "cdl-refine.thy" THY_STYLE VER_BASE_NAME ${VER_BASE_NAME} 656 DEPENDS camkes_capdl_target) 657 add_custom_target(camkes_cdl_refine_thy DEPENDS "${CAMKES_CDL_REFINE_THY}") 658 add_dependencies(isabelle_root camkes_cdl_refine_thy) 659 660 CAmkESOutputGenCommand(load-object-state ${CMAKE_CURRENT_BINARY_DIR}/object-final.pickle) 661endif() 662 663# Ensure we generated all the files we intended to, this is just sanity checking 664if (NOT ("${item_list}" STREQUAL "")) 665 message(FATAL_ERROR "Items added through CAmkESGen not generated") 666endif() 667