Do not define project(CBMC ...) twice to fix CMake failures

tautschnig · tautschnig · commit aeeb39f00d26 · 2024-09-03T12:51:50.000Z
`project(P, ...)` sets the CMake variablee `P_SOURCE_DIR` to whichever directory that CMake file is in. We happen to rely on the value of `CBMC_SOURCE_DIR` in several places. Invoking `project(P, ...)` twice in different directories for the same value of `P` will cause hard-to-reproduce behaviour. Even though this duplication was in place ever since, 7949cac, we apparently got lucky until a few days ago. Now, however, we see sporadic failures on GitHub runners, such as https://github.com/diffblue/cbmc/actions/runs/10677152028/job/29591809621. GitHub's runner image notes do not point out any recent change to CMake, but it might as well be changes to the kernel's scheduler.
diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt
@@ -1,4 +1,4 @@
-set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl")
 
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
diff --git a/jbmc/src/CMakeLists.txt b/jbmc/src/CMakeLists.txt
@@ -7,7 +7,7 @@ macro(generic_includes name)
         ${JBMC_BINARY_DIR}
         ${JBMC_SOURCE_DIR}
         ${CBMC_BINARY_DIR}
-        ${CBMC_SOURCE_DIR}
+        ${CBMC_SOURCE_DIR}/src
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
         ${CUDD_INCLUDE}
diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt
@@ -1,5 +1,5 @@
 file(GLOB_RECURSE sources "*.cpp" "*.h")
-list(APPEND sources  ${CBMC_SOURCE_DIR}/../unit/unit_tests.cpp)
+list(APPEND sources  ${CBMC_SOURCE_DIR}/unit/unit_tests.cpp)
 
 file(GLOB_RECURSE java-testing_utils "java-testing-utils/*.cpp" "java-testing-utils/*.h")
 
@@ -14,8 +14,8 @@ add_executable(java-unit ${sources})
 target_include_directories(java-unit
     PUBLIC
     ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
-    ${CBMC_SOURCE_DIR}/../unit
+    ${CBMC_SOURCE_DIR}/src
+    ${CBMC_SOURCE_DIR}/unit
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
 target_link_libraries(java-unit
diff --git a/jbmc/unit/java-testing-utils/CMakeLists.txt b/jbmc/unit/java-testing-utils/CMakeLists.txt
@@ -7,5 +7,5 @@ target_link_libraries(java-testing-utils
 target_include_directories(java-testing-utils
     PUBLIC
     ${CMAKE_CURRENT_SOURCE_DIR}/..
-    ${CBMC_SOURCE_DIR}/../unit
+    ${CBMC_SOURCE_DIR}/unit
 )
diff --git a/regression/libcprover-cpp/CMakeLists.txt b/regression/libcprover-cpp/CMakeLists.txt
@@ -4,13 +4,13 @@ cprover_default_properties(api-binary-driver)
 target_include_directories(api-binary-driver
     PUBLIC
     ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
+    ${CBMC_SOURCE_DIR}/src
     # TODO: Should be fixed for the proper include form.
     ${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)
 target_link_libraries(api-binary-driver goto-programs util langapi ansi-c cprover-api-cpp)
 
 # Enable test running
-set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl")
 
 macro(add_test_pl_profile name cmdline flag profile)
     add_test(
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -1,5 +1,3 @@
-project(CBMC VERSION ${CBMC_VERSION})
-
 find_package(BISON REQUIRED)
 find_package(FLEX REQUIRED)
 
@@ -66,8 +64,8 @@ endmacro(generic_flex)
 macro(generic_includes name)
     target_include_directories(${name}
         PUBLIC
-        ${CBMC_BINARY_DIR}
-        ${CBMC_SOURCE_DIR}
+        ${CBMC_BINARY_DIR}/src
+        ${CBMC_SOURCE_DIR}/src
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
     )
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
@@ -59,7 +59,7 @@ list(REMOVE_ITEM sources
 
 add_library(solvers ${sources})
 
-include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
+include("${CBMC_SOURCE_DIR}/cmake/DownloadProject.cmake")
 
 foreach(SOLVER ${sat_impl})
     if("${SOLVER}" STREQUAL "minisat2")
@@ -70,8 +70,8 @@ foreach(SOLVER ${sat_impl})
         # to 2 times)
         download_project(PROJ minisat2
             URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
-            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/minisat-2.2.1-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/minisat2_CMakeLists.txt CMakeLists.txt
             URL_MD5 27faa19ee0508660bd6fb7f894646d42
         )
 
@@ -103,8 +103,8 @@ foreach(SOLVER ${sat_impl})
 
         download_project(PROJ glucose
             URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
-            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt
             URL_MD5 7c539c62c248b74210aef7414787323a
         )
 
@@ -122,8 +122,8 @@ foreach(SOLVER ${sat_impl})
 
         download_project(PROJ cadical
             URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch
-            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
             COMMAND ./configure
             URL_MD5 9fc2a66196b86adceb822a583318cc35
         )
@@ -145,7 +145,7 @@ foreach(SOLVER ${sat_impl})
 
         download_project(PROJ cadical
             URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
             COMMAND ./configure
             URL_MD5 9fc2a66196b86adceb822a583318cc35
         )
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
@@ -5,7 +5,7 @@ find_package(Git)
 if(GIT_FOUND)
   file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
     "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+    file(STRINGS \${SRC}/src/config.inc
       config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
     string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
     execute_process(
@@ -20,7 +20,7 @@ if(GIT_FOUND)
 else()
   file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
     "
-    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+    file(STRINGS \${SRC}/src/config.inc
       config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
     string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
     set(GIT_INFO \"n/a\")
@@ -35,7 +35,7 @@ add_custom_target(
   generate_version_cpp
   BYPRODUCTS version.cpp
   COMMAND ${CMAKE_COMMAND}
-    -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
+    -D SRC=${CBMC_SOURCE_DIR}
     -D CUR=${CMAKE_CURRENT_BINARY_DIR}
     -P ${CMAKE_BINARY_DIR}/version.cmake
 )
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
@@ -75,7 +75,7 @@ add_executable(unit ${sources})
 target_include_directories(unit
     PUBLIC
     ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
+    ${CBMC_SOURCE_DIR}/src
     ${CMAKE_CURRENT_SOURCE_DIR}
     ${CMAKE_CURRENT_BINARY_DIR}
     ${CUDD_INCLUDE}
diff --git a/unit/libcprover-cpp/CMakeLists.txt b/unit/libcprover-cpp/CMakeLists.txt
@@ -4,7 +4,7 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_executable(lib-unit ${sources})
 target_include_directories(lib-unit
     PUBLIC
-    ${CBMC_SOURCE_DIR}/libcprover-cpp
+    ${CBMC_SOURCE_DIR}/src/libcprover-cpp
 )
 target_link_libraries(lib-unit
     cprover-api-cpp

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")`
	`1`	`+set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl")`
`2`	`2`
`3`	`3`	`# For the best possible utilisation of multiple cores when`
`4`	`4`	`# running tests in parallel, it is important that these directories are`
Original file line number	Diff line number	Diff line change
`@@ -7,5 +7,5 @@ target_link_libraries(java-testing-utils`
`7`	`7`	`target_include_directories(java-testing-utils`
`8`	`8`	`PUBLIC`
`9`	`9`	`${CMAKE_CURRENT_SOURCE_DIR}/..`
`10`		`- ${CBMC_SOURCE_DIR}/../unit`
	`10`	`+ ${CBMC_SOURCE_DIR}/unit`
`11`	`11`	`)`
Original file line number	Diff line number	Diff line change
`@@ -4,7 +4,7 @@ file(GLOB_RECURSE sources ".cpp" ".h")`
`4`	`4`	`add_executable(lib-unit ${sources})`
`5`	`5`	`target_include_directories(lib-unit`
`6`	`6`	`PUBLIC`
`7`		`- ${CBMC_SOURCE_DIR}/libcprover-cpp`
	`7`	`+ ${CBMC_SOURCE_DIR}/src/libcprover-cpp`
`8`	`8`	`)`
`9`	`9`	`target_link_libraries(lib-unit`
`10`	`10`	`cprover-api-cpp`