# # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) # # SPDX-License-Identifier: BSD-2-Clause # cmake_minimum_required(VERSION 3.8.2) include_guard(GLOBAL) find_program(HOLMAKE_BIN NAMES "Holmake") find_program(CAKEML_BIN NAMES "cake") find_file( BUILD_SCRIPT_IN buildScript.sml.in PATHS ${CMAKE_CURRENT_LIST_DIR} CMAKE_FIND_ROOT_PATH_BOTH ) find_file(HOLMAKEFILE_IN Holmakefile.in PATHS ${CMAKE_CURRENT_LIST_DIR} CMAKE_FIND_ROOT_PATH_BOTH) # Turns a selection of CakeML HOL scripts (Script.sml files) into a library that can # be linked against. Note that the library *only* contains the output of the CakeML # compiler, and it may have hanging symbols to ffi functions that need to be fullfilled # The position argument library_name is the name of the library that will be created and # is directly passed to addlibrary in the end # Other arguments are # SOURCES - One or more Script.sml files to use when performing compilation. These will # all get copied into a flat directory structure for the actual build # TRANSLATION_THEORY - This is the name of the theory that does the final `append_prog` # command. As a result you almost certainly pass a TRANSLATION_THEORYScript.sml file # as one of the SOURCES # CAKEML_ENTRY - Defines the 'entry' function in your CakeML program that should get called # by the CakeML runtime on startup # RUNTIME_ENTRY - Symbol exported from the library that you can call to enter the CakeML # runtime. Note that CakeML does not return and so this function is divergent # STACK_SIZE - Size of the stack for the CakeML runtime in MB - default is 1000 # HEAP_SIZE - Size of the heap for the CakeML runtime in MB - defaultis 1000 # DEPENDS - List of any additional targets to depend upon # INCLUDES - List of any additional INCLUDES to add to the INCLUDES list in the Holmakefile function(DeclareCakeMLLib library_name) cmake_parse_arguments( PARSE_ARGV 1 PARSE_CML_LIB "" "TRANSLATION_THEORY;RUNTIME_ENTRY;CAKEML_ENTRY;STACK_SIZE;HEAP_SIZE" "SOURCES;DEPENDS;INCLUDES" ) if(NOT "${PARSE_CML_LIB_UNPARSED_ARGUMENTS}" STREQUAL "") message( FATAL_ERROR "Unknown arguments to DeclareCakeMLLib ${PARSE_CML_LIB_UNPARSED_ARGUMENTS}" ) endif() # require TRANSLATION_THEORY if("${PARSE_CML_LIB_TRANSLATION_THEORY}" STREQUAL "") message(FATAL_ERROR "Must provide TRANSLATION_THEORY to DeclareCakeMLLib") endif() # require CAKEML_ENTRY if("${PARSE_CML_LIB_CAKEML_ENTRY}" STREQUAL "") message(FATAL_ERROR "Must provide CAKEML_ENTRY to DeclareCakeMLLib") endif() # default RUNTIME_ENTRY to main if("${PARSE_CML_LIB_RUNTIME_ENTRY}" STREQUAL "") set(PARSE_CML_LIB_RUNTIME_ENTRY "main") endif() # default stack and heap size if("${PARSE_CML_LIB_STACK_SIZE}" STREQUAL "") set(PARSE_CML_LIB_STACK_SIZE "1000") endif() if("${PARSE_CML_LIB_HEAP_SIZE}" STREQUAL "") set(PARSE_CML_LIB_HEAP_SIZE "1000") endif() # Work out what --target we need to pass to cake if(KernelSel4ArchX86_64) set(CAKE_TARGET "x64") elseif(KernelArchArmV6) message(FATAL_ERROR "ArmV6 not supported for CakeML builds.") elseif(KernelArchArmV7a OR KernelArchArmV7ve) set(CAKE_TARGET "arm7") elseif(KernelArchArmV8a) set(CAKE_TARGET "arm8") else() # We don't generate an error right here incase configuration is still going on # Setting the target to "unknown" will happily cause 'cake' to fail if it gets to that point set(CAKE_TARGET "unknown") endif() # Check we have all the right tools setup if(${HOLMAKE_BIN} STREQUAL "HOLMAKE_BIN-NOTFOUND") message(FATAL_ERROR "Holmake not found. Expected to be on the system PATH") endif() set(CAKEMLDIR "$ENV{CAKEMLDIR}" CACHE STRING "Path to the CakeML compiler") if(("${CAKEMLDIR}" STREQUAL "") AND NOT ("$ENV{CAKEMLDIR}" STREQUAL "")) message( FATAL_ERROR "CAKEMLDIR is set in the environment, but our CAKEMLDIR is not. Please run ccmake and update CAKEMLDIR" ) endif() if(NOT EXISTS "${CAKEMLDIR}") message(FATAL_ERROR "CAKEMLDIR \"${CAKEMLDIR}\" is not a valid directory") endif() if(${CAKEML_BIN} STREQUAL "CAKEML_BIN-NOTFOUND") message(FATAL_ERROR "Failed to find cake binary. Consider cmake -DCAKEML_BIN=/path/to/cake") endif() # Generate a directory at the top level of the binary directory for placing our CakeML related # files. Placing all the CakeML related sources together simplifies development of of CakeML # projects set(CML_DIR "${CMAKE_BINARY_DIR}/cakeml_${library_name}") set(SEXP_FILE "${CML_DIR}/cake.sexp") set(ASM_FILE "${CML_DIR}/cake.S") set(BUILD_SCRIPT "${CML_DIR}/buildScript.sml") set(HOLMAKEFILE "${CML_DIR}/Holmakefile") # Ensure this desired directory exists file(MAKE_DIRECTORY "${CML_DIR}") # Generate rule for symlinking our sources set(stampfile "${CMAKE_CURRENT_BINARY_DIR}/${library_name}cakeml_symlink.stamp") add_custom_command( OUTPUT "${stampfile}" # First remove any existing symlinks to prevent any confusion if dependencies are changed # between builds. COMMAND bash -c "find '${CML_DIR}' -name '*.sml' -type l | xargs rm -f" # Symlink any of our files. We have to escape into some inline shell expressions here since # we want to support our sources containing generator expressions, and we do not know the value # of these until build time COMMAND ln -s ${PARSE_CML_LIB_SOURCES} "${CML_DIR}" COMMAND touch "${stampfile}" # We do not depend upon the sources here as there is no need to recreate the symlinks if the # sources change. This requires that the later build rules do depend upon the original sources COMMAND_EXPAND_LISTS VERBATIM ) add_custom_target( ${library_name}cakeml_symlink_theory_files DEPENDS ${library_name}cakeml_copy.stamp ) # Write out a build script. configure_file(${BUILD_SCRIPT_IN} ${BUILD_SCRIPT} @ONLY) # Write out a Holmakefile string( REPLACE ";" " " CAKEML_INCLUDES_SPACE_SEP "${PARSE_CML_LIB_INCLUDES}" ) configure_file(${HOLMAKEFILE_IN} ${HOLMAKEFILE} @ONLY) # Extra options for Holmake, provide them to init-build.sh with -DHOL_EXTRA_OPTS="--arg1;--arg2" set( HOL_EXTRA_OPTS "$ENV{HOL_EXTRA_OPTS}" CACHE STRING "Extra arguments to provide to Holmake when building CakeML code" ) add_custom_command( OUTPUT "${ASM_FILE}" BYPRODUCTS "${SEXP_FILE}" COMMAND env CAKEML_DIR=${CAKEMLDIR} ${HOLMAKE_BIN} --quiet ${HOL_EXTRA_OPTS} COMMAND sh -c "${CAKEML_BIN} --sexp=true --exclude_prelude=true --heap_size=${PARSE_CML_LIB_HEAP_SIZE} --stack_size=${PARSE_CML_LIB_STACK_SIZE} --target=${CAKE_TARGET} < ${SEXP_FILE} > ${ASM_FILE}" # the 'cake' program is garbage and does not return an exit code upon failure and instead # just outputs nothing over stdout. We therefore test for an empty file and then both delete # the file to trigger rebuilds in future and generate an explicit error code COMMAND sh -c "if ! [ -s ${ASM_FILE} ]; then rm ${ASM_FILE}; fi" COMMAND test -s "${ASM_FILE}" # 'cake' currently just outputs a global 'main' symbol as its entry point and this is not # configurable. We don't expect many other plain strings to be in the assembly file so we # do a somewhat risky 'sed' to change the name of the main function COMMAND sed -i "s/cdecl(main)/cdecl(${PARSE_CML_LIB_RUNTIME_ENTRY})/g" "${ASM_FILE}" DEPENDS ${PARSE_CML_LIB_SOURCES} "${stampfile}" "${BUILD_SCRIPT}" "${HOLMAKEFILE}" ${PARSE_CML_LIB_DEPENDS} WORKING_DIRECTORY "${CML_DIR}" VERBATIM ${USES_TERMINAL_DEBUG} ) add_custom_target(${library_name}cakeml_asm_theory_target DEPENDS "${ASM_FILE}") add_library(${library_name} STATIC EXCLUDE_FROM_ALL "${ASM_FILE}") # Holmake doesn't support concurrent builds and so we need to serialise any Cakeml # libraries that we build. We do this by adding a dependency on the previously defined # library for each library we define. get_property(cmake_serialise GLOBAL PROPERTY CAKEML_PREVIOUS_LIBRARY) if(NOT "${cmake_serialise}" STREQUAL "") add_dependencies(${library_name} ${cmake_serialise}) endif() set_property(GLOBAL PROPERTY CAKEML_PREVIOUS_LIBRARY ${library_name}) add_dependencies(${library_name} ${library_name}cakeml_asm_theory_target) endfunction(DeclareCakeMLLib)