add_subdirectory(headers)

file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr)
file(TOUCH ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/libc.h
           ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/libm.h)
file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/headers)
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/headers/libc_hdr.h
           "#include \"${CMAKE_CURRENT_BINARY_DIR}/headers/libc_hdr.h\"")

add_executable(c2goto c2goto.cpp cprover_blank_library.cpp cprover_libc_sources.cpp)
target_include_directories(c2goto
    PRIVATE ${Boost_INCLUDE_DIRS}
    PRIVATE ${CMAKE_BINARY_DIR}/src
    PRIVATE ${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr
    )
target_link_libraries(c2goto
  clangcfrontend langapi c2gotoheaders
  filesystem ${Boost_LIBRARIES} ${OS_INCLUDE_LIBS})
set_target_properties(c2goto PROPERTIES
  PRIVATE_HEADER "${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/libc.h;${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/libm.h;${CMAKE_CURRENT_BINARY_DIR}/c2goto-hdr/headers/libc_hdr.h")


if(DEFINED C2GOTO_SYSROOT)
  set(multiarch_flags --sysroot "${C2GOTO_SYSROOT}")
endif()

function(foreach_in_cross_product_rec fn acc_i acc_v)
  list(LENGTH ARGN n)
  if(n EQUAL 0)
    # quotes around ${acc_v} are necessary since CMake does not handle empty
    # 'list' elements, sigh...
    cmake_language(CALL ${fn} "${acc_i}" "${acc_v}")
  else()
    list(GET ARGN 0 x)
    if(n GREATER 1)
      list(SUBLIST ARGN 1 -1 xs)
    else()
      list(SUBLIST ARGN 0 0 xs)
    endif()
    set(n 0)
    foreach(item IN LISTS ${x})
      set(ai ${acc_i})
      list(APPEND ai "${n}")
      set(av "${acc_v}")
      list(APPEND av "${item}")
      math(EXPR n "${n}+1")
      foreach_in_cross_product_rec(${fn} "${ai}" "${av}" ${xs})
    endforeach()
  endif()
endfunction()

function(foreach_in_cross_product fn)
  foreach_in_cross_product_rec(${fn} "" "" ${ARGN})
endfunction()

if(ESBMC_BUNDLE_LIBC)

  set(archs --64)
  if(ENABLE_BUNDLE_LIBC_32BIT)
    set(archs --32 --64)
  endif()
  set(floats "--fixedbv -D__ESBMC_FIXEDBV" --floatbv)
  # for some reason CMake does not differentiate between [""], "" and [] so we
  # have to 'represent' the empty string by a non-empty string in order to get
  # the non-cheri combinations, sigh...
  set(cherimodes " ")
  if(ESBMC_CHERI_CLANG)
    if(ESBMC_CHERI_HYBRID_SYSROOT)
      list(APPEND cherimodes "--cheri hybrid --sysroot ${ESBMC_CHERI_HYBRID_SYSROOT}")
    endif()
    if(ESBMC_CHERI_PURECAP_SYSROOT)
      list(APPEND cherimodes "--cheri purecap --sysroot ${ESBMC_CHERI_PURECAP_SYSROOT}")
    endif()
  endif()

  function(clib_join_argv idcs tuple)
    #message(STATUS "test: idcs: ${idcs}, tuple: ${tuple}")
    list(JOIN idcs "_" idcs)
    list(PREPEND tuple clib_${idcs}.c)
    list(JOIN tuple " " clib_config_${idcs})
    list(APPEND clib_configs clib_config_${idcs})
    message(STATUS "test: ${clib_config_${idcs}}")
  endfunction()

  foreach_in_cross_product(clib_join_argv cherimodes floats archs)

  set(clib64_config clib64.c --64 --fixedbv -D__ESBMC_FIXEDBV)
  set(clib64f_config clib64_fp.c --64 --floatbv)
  set(inputs clib64_config clib64f_config)
  if(ENABLE_BUNDLE_LIBC_32BIT)
    set(clib32_config clib32.c --32 --fixedbv -D__ESBMC_FIXEDBV)
    set(clib32f_config clib32_fp.c --32 --floatbv)
    set(inputs clib32_config
      clib64_config
      clib32f_config
      clib64f_config)
  endif()

  if(ESBMC_CHERI_HYBRID_SYSROOT)
    set(clib32_cherih_config clib32_cherih.c --32 --fixedbv -D__ESBMC_FIXEDBV --cheri hybrid --sysroot "${ESBMC_CHERI_HYBRID_SYSROOT}")
    set(clib64_cherih_config clib64_cherih.c --64 --fixedbv -D__ESBMC_FIXEDBV --cheri hybrid --sysroot "${ESBMC_CHERI_HYBRID_SYSROOT}")
    set(clib32f_cherih_config clib32_fp_cherih.c --32 --floatbv --cheri hybrid --sysroot "${ESBMC_CHERI_HYBRID_SYSROOT}")
    set(clib64f_cherih_config clib64_fp_cherih.c --64 --floatbv --cheri hybrid --sysroot "${ESBMC_CHERI_HYBRID_SYSROOT}")
    list(APPEND inputs
              #clib32_cherih_config
              clib64_cherih_config
              #clib32f_cherih_config
              clib64f_cherih_config)
  endif()

  if(ESBMC_CHERI_PURECAP_SYSROOT)
    set(clib32_cherip_config clib32_cherip.c --32 --fixedbv -D__ESBMC_FIXEDBV --cheri purecap --sysroot "${ESBMC_CHERI_PURECAP_SYSROOT}")
    set(clib64_cherip_config clib64_cherip.c --64 --fixedbv -D__ESBMC_FIXEDBV --cheri purecap --sysroot "${ESBMC_CHERI_PURECAP_SYSROOT}")
    set(clib32f_cherip_config clib32_fp_cherip.c --32 --floatbv --cheri purecap --sysroot "${ESBMC_CHERI_PURECAP_SYSROOT}")
    set(clib64f_cherip_config clib64_fp_cherip.c --64 --floatbv --cheri purecap --sysroot "${ESBMC_CHERI_PURECAP_SYSROOT}")
    list(APPEND inputs
              #clib32_cherip_config
              clib64_cherip_config
              #clib32f_cherip_config
              clib64f_cherip_config)
  endif()
endif()

function(mangle_clib output)
  set(result "")
  # Extract a list of C's operational models
  file(GLOB c2goto_library_files CONFIGURE_DEPENDS
    "${CMAKE_CURRENT_SOURCE_DIR}/library/*.c")
  # Extract a list of C's math operational models
  file(GLOB c2goto_libm_files CONFIGURE_DEPENDS
    "${CMAKE_CURRENT_SOURCE_DIR}/library/libm/*.c"
    "${CMAKE_CURRENT_SOURCE_DIR}/library/libm/musl/*.c")
  file(GLOB_RECURSE c2goto_header_files CONFIGURE_DEPENDS
    "${CMAKE_CURRENT_SOURCE_DIR}/headers/*.h")

  # Extract C models for Python
  if(ENABLE_PYTHON_FRONTEND)
    file(GLOB_RECURSE c2goto_python_files CONFIGURE_DEPENDS
      "${CMAKE_CURRENT_SOURCE_DIR}/library/python/*.c")
  else()
    set(c2goto_python_files "")
  endif()

  # Extract C models for Solidity
  if(ENABLE_SOLIDITY_FRONTEND)
    file(GLOB_RECURSE c2goto_solidity_files CONFIGURE_DEPENDS
      "${CMAKE_CURRENT_SOURCE_DIR}/library/solidity/*.c")
  else()
    set(c2goto_solidity_files "")
  endif()

  # For each config, generate clib*.c and clib*.goto file in the current binary directory
  foreach(in_f ${ARGN})
    set(in_f "${${in_f}}")
    list(GET in_f 0 out_name)
    list(SUBLIST in_f 1 -1 in_flags)
    file(RELATIVE_PATH out_file ${CMAKE_CURRENT_SOURCE_DIR}
                                ${CMAKE_CURRENT_SOURCE_DIR}/${out_name})
    string(REGEX REPLACE \\.c$ .goto out_goto "${out_name}")
    set(out_goto "${CMAKE_CURRENT_BINARY_DIR}/${out_goto}")
    set(out_file "${CMAKE_CURRENT_BINARY_DIR}/${out_file}")

    set(inputs_c ${c2goto_library_files})

    if(ENABLE_LIBM)
      list(APPEND inputs_c ${c2goto_libm_files})
    endif()

    if(ENABLE_PYTHON_FRONTEND)
      list(APPEND inputs_c ${c2goto_python_files})
    endif()

    # Solidity models are built as a separate goto binary (sol64.goto),
    # NOT mixed into clib64, for faster runtime loading.

    if(ESBMC_CHERI_CLANG)
      list(APPEND in_flags -I "${cheri_compressed_cap_SOURCE_DIR}")
    endif()

    set(run_c2goto c2goto ${multiarch_flags} ${OS_C2GOTO_FLAGS}
                   ${inputs_c} ${in_flags} --output ${out_goto})

    # Convert a list of C operational models (e.g. *.c) into a single goto binary file (e.g. clib32.goto) at CMake build time
    add_custom_command(OUTPUT ${out_goto}
      COMMAND ${run_c2goto}
      DEPENDS c2goto ${c2goto_library_files} ${c2goto_libm_files} ${c2goto_header_files} ${c2goto_python_files}
      WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
      COMMENT "Generating libc model ${out_goto}"
      VERBATIM
      )

    # Convert the content of goto binary file (e.g. clib32.goto) into a C source file (e.g. clib32.c) containing the content of the binary
    add_custom_command(OUTPUT ${out_file}
      COMMAND ${Python_EXECUTABLE} ${CMAKE_SOURCE_DIR}/scripts/flail.py -o ${out_file} ${out_goto}
      DEPENDS ${out_goto} ${CMAKE_SOURCE_DIR}/scripts/flail.py
      WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
      COMMENT "Converting libc model ${out_goto} to data"
      VERBATIM
      )

    list(APPEND result ${out_file})
  endforeach()

  # `mangle` function defined in src/scripts/cmake/Utils.cmake
  mangle(${CMAKE_CURRENT_BINARY_DIR}/libc.c  # an aggregate of C operational models
         ${CMAKE_CURRENT_SOURCE_DIR}/library # the directory containing all C operational models
         WILDCARD *.c
         SINGLE
         PREFIX esbmc_libc_
         MACRO ESBMC_FLAIL
         ACC_HEADERS_INTO ${CMAKE_CURRENT_BINARY_DIR}/libc.h)
  mangle(${CMAKE_CURRENT_BINARY_DIR}/libm.c       # an aggregate of C math operational models
         ${CMAKE_CURRENT_SOURCE_DIR}/library/libm # the directory C math operational models
         WILDCARD *.c
         SINGLE
         PREFIX esbmc_libm_
         MACRO ESBMC_FLAIL
         ACC_HEADERS_INTO ${CMAKE_CURRENT_BINARY_DIR}/libm.h)

  if(ENABLE_PYTHON_FRONTEND)
    mangle(${CMAKE_CURRENT_BINARY_DIR}/libpython.c
           ${CMAKE_CURRENT_SOURCE_DIR}/library/python
           WILDCARD *.c
           SINGLE
           PREFIX esbmc_python_
           MACRO ESBMC_FLAIL
           ACC_HEADERS_INTO ${CMAKE_CURRENT_BINARY_DIR}/libpython.h)

    list(APPEND result
      ${CMAKE_CURRENT_BINARY_DIR}/libpython.c
      ${CMAKE_CURRENT_BINARY_DIR}/libpython.h)
  endif()

  if(ENABLE_SOLIDITY_FRONTEND)
    mangle(${CMAKE_CURRENT_BINARY_DIR}/libsolidity.c
           ${CMAKE_CURRENT_SOURCE_DIR}/library/solidity
           WILDCARD *.c
           SINGLE
           PREFIX esbmc_solidity_
           MACRO ESBMC_FLAIL
           ACC_HEADERS_INTO ${CMAKE_CURRENT_BINARY_DIR}/libsolidity.h)

    # Build a separate goto binary for Solidity operational models (sol64.goto)
    # This is loaded at runtime instead of the full clib64.goto for performance.
    set(sol64_goto "${CMAKE_CURRENT_BINARY_DIR}/sol64.goto")
    set(sol64_c "${CMAKE_CURRENT_BINARY_DIR}/sol64.c")
    if(APPLE)
      # Apple Clang does not support _BitInt > 128, so c2goto cannot compile
      # solidity_types.h on macOS. Emit an empty stub so the link succeeds;
      # runtime verification of Solidity contracts is unavailable on macOS.
      file(WRITE ${sol64_c}
        "/* Auto-generated stub: sol64 unavailable on macOS (_BitInt>128). */\n"
        "#include <stdint.h>\n"
        "const uint8_t sol64_buf[1] = {0};\n"
        "const unsigned int sol64_buf_size = 0;\n")
    else()
      # Amalgamate all solidity .c files into one TU. Passing the originals
      # separately makes c2goto invoke clang::ASTImporter to merge them, which
      # on LLVM 16 (Windows) cannot import _BitInt(N)-using decls and emits
      # "UnsupportedConstruct" until the whole step aborts. A single TU avoids
      # the importer entirely.
      set(sol64_unified_c "${CMAKE_CURRENT_BINARY_DIR}/sol64_unified.c")
      set(sol64_unified_body
        "/* Auto-generated by CMake: amalgamation of solidity *.c models. */\n")
      foreach(_f ${c2goto_solidity_files})
        string(APPEND sol64_unified_body "#include \"${_f}\"\n")
      endforeach()
      file(WRITE ${sol64_unified_c} "${sol64_unified_body}")

      add_custom_command(OUTPUT ${sol64_goto}
        COMMAND c2goto ${multiarch_flags} ${OS_C2GOTO_FLAGS}
                ${sol64_unified_c} --64 --fixedbv -D__ESBMC_FIXEDBV
                --output ${sol64_goto}
        DEPENDS c2goto ${c2goto_solidity_files} ${c2goto_header_files}
                ${sol64_unified_c}
        WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
        COMMENT "Generating Solidity model ${sol64_goto}"
        VERBATIM
      )
      add_custom_command(OUTPUT ${sol64_c}
        COMMAND ${Python_EXECUTABLE} ${CMAKE_SOURCE_DIR}/scripts/flail.py
                -o ${sol64_c} ${sol64_goto}
        DEPENDS ${sol64_goto} ${CMAKE_SOURCE_DIR}/scripts/flail.py
        WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
        COMMENT "Converting Solidity model ${sol64_goto} to data"
        VERBATIM
      )
    endif()

    list(APPEND result
      ${CMAKE_CURRENT_BINARY_DIR}/libsolidity.c
      ${CMAKE_CURRENT_BINARY_DIR}/libsolidity.h
      ${sol64_c})
  endif()


  list(APPEND result ${CMAKE_CURRENT_BINARY_DIR}/libc.c
                     ${CMAKE_CURRENT_BINARY_DIR}/libm.c)
  set(${output} "${result}" PARENT_SCOPE)
endfunction()

message(STATUS "Multiarch flags for c2goto: ${multiarch_flags}. You may want to override C2GOTO_SYSROOT")
mangle_clib(mangled_files ${inputs})

# Auto-generate the Python operational-model allowlist from the model sources so
# new models register automatically (scripts/gen_python_c_models.py). The header
# is consumed by cprover_library.cpp under #ifdef ENABLE_PYTHON_FRONTEND.
if(ENABLE_PYTHON_FRONTEND)
  find_package(Python REQUIRED COMPONENTS Interpreter)
  file(GLOB_RECURSE python_model_sources CONFIGURE_DEPENDS
    "${CMAKE_CURRENT_SOURCE_DIR}/library/python/*.c")
  set(python_c_models_header ${CMAKE_CURRENT_BINARY_DIR}/python_c_models_generated.h)
  add_custom_command(OUTPUT ${python_c_models_header}
    COMMAND ${Python_EXECUTABLE} ${CMAKE_SOURCE_DIR}/scripts/gen_python_c_models.py
            -o ${python_c_models_header} ${python_model_sources}
    DEPENDS ${CMAKE_SOURCE_DIR}/scripts/gen_python_c_models.py ${python_model_sources}
    COMMENT "Generating Python C-model allowlist ${python_c_models_header}"
    VERBATIM)
  add_custom_target(gen_python_c_models DEPENDS ${python_c_models_header})
endif()

add_library(clibs ${mangled_files} cprover_library.cpp cprover_libc_sources.cpp)
target_include_directories(clibs
    PRIVATE ${Boost_INCLUDE_DIRS}
    PRIVATE ${CMAKE_BINARY_DIR}/src
    PRIVATE ${CMAKE_CURRENT_BINARY_DIR}
)
target_link_libraries(clibs c2gotoheaders fmt::fmt filesystem)
if(ENABLE_PYTHON_FRONTEND)
  add_dependencies(clibs gen_python_c_models)
endif()

set(private_headers
  "${CMAKE_CURRENT_BINARY_DIR}/libc.h"
  "${CMAKE_CURRENT_BINARY_DIR}/libm.h"
)

if(ENABLE_PYTHON_FRONTEND)
  list(APPEND private_headers "${CMAKE_CURRENT_BINARY_DIR}/libpython.h")
endif()

if(ENABLE_SOLIDITY_FRONTEND)
  list(APPEND private_headers "${CMAKE_CURRENT_BINARY_DIR}/libsolidity.h")
endif()

set_target_properties(clibs PROPERTIES PRIVATE_HEADER "${private_headers}")


