Merge pull request #7567 from esteffin/esteffin/creating-public-archive-with-all-components

Creating library archive with all components

Author: Enrico Steffinlongo

regression/libcprover-cpp/call_bmc.cpp

@@ -4,7 +4,7 @@
 #include <util/exception_utils.h>
 
 #include <libcprover-cpp/api.h>
-#include <libcprover-cpp/options.h>
+#include <libcprover-cpp/api_options.h>
 
 #include "goto_model.h"
 

src/CMakeLists.txt

@@ -1,4 +1,12 @@
-project(CBMC)
+file(STRINGS
+        "${CMAKE_CURRENT_SOURCE_DIR}/config.inc"
+        cbmc_version_string
+        REGEX "CBMC_VERSION.*")
+
+string(REGEX REPLACE "CBMC_VERSION = (.*)" "\\1" CBMC_VERSION "${cbmc_version_string}")
+unset(cbmc_version_string)
+
+project(CBMC VERSION ${CBMC_VERSION})
 
 find_package(BISON REQUIRED)
 find_package(FLEX REQUIRED)
@@ -102,7 +110,6 @@ add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)
-add_subdirectory(libcprover-cpp)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
@@ -119,6 +126,7 @@ add_subdirectory(goto-diff)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-synthesizer)
 add_subdirectory(symtab2gb)
+add_subdirectory(libcprover-cpp)
 
 if(UNIX OR WITH_MEMORY_ANALYZER)
 add_subdirectory(memory-analyzer)

src/libcprover-cpp/CMakeLists.txt

@@ -1,23 +1,92 @@
-file(GLOB_RECURSE sources "*.cpp" "*.h")
+# Scan for all source files in the current or child directories
+file(GLOB_RECURSE sources "*.cpp")
+# Scan for all header files in the current or child directories (necessary to install them later)
+file(GLOB_RECURSE headers "*.h")
 
-# This step builds the API in the form of a statically linked library (libcprover-api-cpp.a)
+# This step builds the API in the form of a statically linked library
 add_library(cprover-api-cpp ${sources})
+
+# Being a library we should include them privately, but for now fair enough
 generic_includes(cprover-api-cpp)
-target_link_libraries(cprover-api-cpp 
-    goto-checker
-    goto-programs
-    util
-    langapi
-    ansi-c
-    json-symtab-language
-    solvers
-    xml
-    cpp
-    cbmc-lib
-    analyses
-    statement-list
-    linking
-    pointer-analysis
-    goto-instrument-lib
-    goto-analyzer-lib
-    goto-cc-lib)
+
+# Add all the current and the installed `include` directories as a PUBLIC header location
+target_include_directories(cprover-api-cpp PUBLIC
+                           "$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>"
+                           "$<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>"
+                           "$<INSTALL_INTERFACE:include>")
+
+# To create a full static API library we need to archive together the content of all the other
+# module libraries we depend on.  To do this we will use the `ar` command to unpack the other module
+# static libraries and append to the current library `.a` file.
+
+# Get the dependency targets of the `solver` target (see `../solver/CMakeLists.txt`), so that they
+# are merged to the final library too.  (such dependencies are not known statically as the selection
+# of the SAT backend is left to the building user.
+get_target_property(LIBRARY_DEPENDENCIES solvers LINK_LIBRARIES)
+
+# Get all the dependency targets we know statically.
+list(APPEND
+        LIBRARY_DEPENDENCIES
+        "goto-programs"
+        "util"
+        "langapi"
+        "ansi-c"
+        "analyses"
+        "goto-instrument-lib"
+        "big-int"
+        "linking"
+        "goto-checker"
+        "solvers"
+        "assembler"
+        "xml"
+        "json"
+        "json-symtab-language"
+        "jsil"
+        "statement-list"
+        "goto-symex"
+        "pointer-analysis"
+        "cbmc-lib")
+
+# Remove possible duplicate library targets
+list(REMOVE_DUPLICATES LIBRARY_DEPENDENCIES)
+
+# Add all the dependency targets as dependencies of `cprover-api-cpp`
+target_link_libraries(cprover-api-cpp
+                      PRIVATE
+                      ${LIBRARY_DEPENDENCIES})
+
+# To be able to invoke `ar` on the dependencies we need the paths of the libraries `.a` files.
+# Ths is done by using the cmake generator `$<TARGET_FILE:dependency>`, that in turn will be
+# substituted with the absolute path of the `dependency` output file (a `.a` file in this case).
+# Here we prepare a space-separated list of cmake generators that will resolved in  absolute paths.
+set(DEPENDENCY_TARGETS "")
+foreach(dep ${LIBRARY_DEPENDENCIES})
+    list(APPEND DEPENDENCY_TARGETS "$<TARGET_FILE:${dep}>")
+endforeach(dep LIBRARY_DEPENDENCIES)
+string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}")
+
+# To aggregate all the dependencies into a final `.a` file we add a custom pass after target
+# `cprover-api-cpp` has been built where the `aggregate_dependencies.sh` script is run with the `ar`
+# command, the destination library and the dependencies paths
+add_custom_command(TARGET cprover-api-cpp POST_BUILD
+                   COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/add_dependencies.sh" "${CMAKE_AR}" "$<TARGET_FILE:cprover-api-cpp>" "${DEPENDENCY_TARGETS}"
+                   WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}")
+
+# Set the properties of `cprover-api-cpp`.  Mainly the output name `libcprover.<version>.a`, its
+# version (CBMC version) and the list of public headers to be installed
+set_target_properties(cprover-api-cpp
+        PROPERTIES
+        OUTPUT_NAME "cprover.${CMAKE_PROJECT_VERSION}" # libcprover.<version>.a
+        SOVERSION "${CMAKE_PROJECT_VERSION}"
+        PUBLIC_HEADER "${headers}"
+        )
+
+# Install the target as usual in `lib` the library and in `include/cprover` the public headers.
+install(TARGETS         cprover-api-cpp
+        ARCHIVE         DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+                        COMPONENT lib
+        LIBRARY         DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+                        COMPONENT lib
+        PUBLIC_HEADER   DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/cprover"
+                        COMPONENT lib
+        )

src/libcprover-cpp/add_dependencies.sh

@@ -0,0 +1,25 @@
+#!/usr/bin/env sh
+
+# This script adds to a static library archive file `lib<name>.a` all the object files of a set of
+# other libraries it depends on.
+# This script takes 3 or more arguments:
+# 1. the archive command
+# 2. the destination library path
+# 3. a list of paths of static libraries to be added to the destination library archive
+
+set -e
+
+AR_COMMAND=$1
+shift
+DESTINATION=$1
+shift
+LIB_LIST=$@
+
+# For each library to add:
+for lib in ${LIB_LIST}; do
+  # Unpack the library
+  ${AR_COMMAND} -x ${lib}
+done
+
+# Append all the unpacked files to the destination library
+${AR_COMMAND} -rcs ${DESTINATION} *.o

src/libcprover-cpp/api.h

@@ -17,7 +17,7 @@ struct api_session_implementationt;
 // a pragma like below to silence the warning (at least as long
 // as the design principle is to be followed.)
 
-#include "options.h" // IWYU pragma: keep
+#include "api_options.h" // IWYU pragma: keep
 
 /// Opaque message type. Properties of messages to be fetched through further
 /// api calls.

src/libcprover-cpp/options.cpp renamed to src/libcprover-cpp/api_options.cpp

@@ -1,6 +1,6 @@
 // Author: Fotis Koutoulakis for Diffblue Ltd.
 
-#include "options.h"
+#include "api_options.h"
 
 #include <util/cmdline.h>
 #include <util/make_unique.h>

src/libcprover-cpp/options.h renamed to src/libcprover-cpp/api_options.h

@@ -111,28 +111,6 @@ fn main() {
         "cargo:rustc-link-search=native={}",
         libraries_path.display()
     );
-    println!("cargo:rustc-link-lib=static=goto-programs");
-    println!("cargo:rustc-link-lib=static=util");
-    println!("cargo:rustc-link-lib=static=langapi");
-    println!("cargo:rustc-link-lib=static=ansi-c");
-    println!("cargo:rustc-link-lib=static=analyses");
-    println!("cargo:rustc-link-lib=static=goto-instrument-lib");
-    println!("cargo:rustc-link-lib=static=big-int");
-    println!("cargo:rustc-link-lib=static=linking");
-    println!("cargo:rustc-link-lib=static=goto-checker");
-    println!("cargo:rustc-link-lib=static=solvers");
-    println!("cargo:rustc-link-lib=static=assembler");
-    println!("cargo:rustc-link-lib=static=xml");
-    println!("cargo:rustc-link-lib=static=json");
-    println!("cargo:rustc-link-lib=static=json-symtab-language");
-    println!("cargo:rustc-link-lib=static=cpp");
-    println!("cargo:rustc-link-lib=static=jsil");
-    println!("cargo:rustc-link-lib=static=statement-list");
-    println!("cargo:rustc-link-lib=static=goto-symex");
-    println!("cargo:rustc-link-lib=static=pointer-analysis");
-    for solver_lib in solver_libs {
-        println!("cargo:rustc-link-lib=static={}", solver_lib);
-    }
-    println!("cargo:rustc-link-lib=static=cbmc-lib");
-    println!("cargo:rustc-link-lib=static=cprover-api-cpp");
+
+    println!("cargo:rustc-link-lib=static=cprover.5.77.0");
 }