Skip to content

CMake error when building cbmc with -Dsat_impl=ipasir-cadical #7641

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
jiegec opened this issue Apr 2, 2023 · 3 comments
Closed

CMake error when building cbmc with -Dsat_impl=ipasir-cadical #7641

jiegec opened this issue Apr 2, 2023 · 3 comments
Labels
pending merge

Comments

@jiegec
Copy link

jiegec commented Apr 2, 2023

CBMC version: develop branch commit f8380e5
Operating system: Debian Linux bookworm
Exact command line resulting in the issue:

mkdir build
cd build
cmake .. -Dsat_impl=ipasir-cadical -DWITH_JBMC=OFF

What behaviour did you expect: It can build
What happened instead: It fails with:

-- Building CBMC version 5.80.0
-- The C compiler identification is GNU 12.2.0
-- The CXX compiler identification is GNU 12.2.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found BISON: /usr/bin/bison (found version "3.8.2")
-- Found FLEX: /usr/bin/flex (found version "2.6.4")
-- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE)
-- Building with IPASIR solver linking against: CaDiCaL
-- Downloading/updating cadical
CMake Deprecation Warning at CMakeLists.txt:4 (cmake_minimum_required):
  Compatibility with CMake < 2.8.12 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.


CMake Warning (dev) at /usr/share/cmake-3.25/Modules/ExternalProject.cmake:3075 (message):
  The DOWNLOAD_EXTRACT_TIMESTAMP option was not given and policy CMP0135 is
  not set.  The policy's OLD behavior will be used.  When using a URL
  download, the timestamps of extracted files should preferably be that of
  the time of extraction, otherwise code that depends on the extracted
  contents might not be rebuilt if the URL changes.  The OLD behavior
  preserves the timestamps from the archive instead, but this is usually not
  what you want.  Update your project to the NEW behavior or specify the
  DOWNLOAD_EXTRACT_TIMESTAMP option with a value of true to avoid this
  robustness issue.
Call Stack (most recent call first):
  /usr/share/cmake-3.25/Modules/ExternalProject.cmake:4185 (_ep_add_download_command)
  CMakeLists.txt:9 (ExternalProject_Add)
This warning is for project developers.  Use -Wno-dev to suppress it.

-- Configuring done
-- Generating done
-- Build files have been written to: /home/jiegec/nixpkgs-dev/cbmc/build/cadical-download
[ 11%] Creating directories for 'cadical-download'
[ 22%] Performing download step (download, verify and extract) for 'cadical-download'
-- Downloading...
   dst='/home/jiegec/nixpkgs-dev/cbmc/build/cadical-download/cadical-download-prefix/src/rel-1.4.1.tar.gz'
   timeout='none'
   inactivity timeout='none'
-- Using src='https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz'
-- verifying file...
       file='/home/jiegec/nixpkgs-dev/cbmc/build/cadical-download/cadical-download-prefix/src/rel-1.4.1.tar.gz'
-- Downloading... done
-- extracting...
     src='/home/jiegec/nixpkgs-dev/cbmc/build/cadical-download/cadical-download-prefix/src/rel-1.4.1.tar.gz'
     dst='/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src'
-- extracting... [tar xfz]
-- extracting... [analysis]
-- extracting... [rename]
-- extracting... [clean up]
-- extracting... done
[ 33%] No update step for 'cadical-download'
[ 44%] Performing patch step for 'cadical-download'
configure: making default 'build' directory
configure: building in default '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/build'
configure: root directory '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src'
configure: source directory '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/src'
configure: compiler supports all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with '/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/build/makefile'
configure: linking '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
[ 55%] No configure step for 'cadical-download'
[ 66%] No build step for 'cadical-download'
[ 77%] No install step for 'cadical-download'
[ 88%] No test step for 'cadical-download'
[100%] Completed 'cadical-download'
[100%] Built target cadical-download
-- Building CaDiCaL
make -C "/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/build"
make[1]: Entering directory '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/build'
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/analyze.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/arena.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/assume.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/averages.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/backtrack.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/backward.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/bins.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/block.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/ccadical.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/checker.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/clause.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/collect.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/compact.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/condition.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/config.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/contract.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/cover.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/decide.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/decompose.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/deduplicate.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/elim.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/ema.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/extend.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/external.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/file.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/flags.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/format.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/gates.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/instantiate.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/internal.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/ipasir.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/limit.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/logging.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/lookahead.cpp
In file included from ../src/lookahead.cpp:1:
In constructor ‘CaDiCaL::CubesWithStatus::CubesWithStatus(CaDiCaL::CubesWithStatus&&)’,
    inlined from ‘CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)’ at ../src/lookahead.cpp:394:12:
../src/internal.hpp:100:8: warning: ‘cubes.CaDiCaL::CubesWithStatus::status’ may be used uninitialized [-Wmaybe-uninitialized]
  100 | struct CubesWithStatus {
      |        ^~~~~~~~~~~~~~~
../src/lookahead.cpp: In member function ‘CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)’:
../src/lookahead.cpp:392:21: note: ‘cubes’ declared here
  392 |     CubesWithStatus cubes;
      |                     ^~~~~
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/lucky.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/message.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/minimize.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/occs.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/options.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/parse.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/phases.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/probe.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/profile.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/proof.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/propagate.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/queue.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/random.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/reap.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/reduce.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/rephase.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/report.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/resources.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/restart.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/restore.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/score.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/shrink.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/signal.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/solution.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/solver.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/stats.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/subsume.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/terminal.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/ternary.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/tracer.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/transred.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/util.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
make-build-header.sh: warning: could not determine 'COMPILER' ('CXX')
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/version.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/vivify.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/walk.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/cadical.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -o cadical cadical.o -L. -lcadical
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -c ../src/mobical.cpp
/usr/bin/c++ -std=c++14 -W -O -DNDEBUG -O3 -ggdb3 -I../build -o mobical mobical.o -L. -lcadical
make[1]: Leaving directory '/home/jiegec/nixpkgs-dev/cbmc/build/cadical-src/build'
-- Found Git: /home/jiegec/.nix-profile/bin/git (found version "2.39.2")
-- Adding tests in directory: cbmc
-- Adding tests in directory: cbmc-library
-- Adding tests in directory: cprover
-- Adding tests in directory: crangler
-- Adding tests in directory: goto-analyzer
-- Adding tests in directory: goto-instrument
-- Adding tests in directory: cpp
-- Adding tests in directory: cbmc-concurrency
-- Adding tests in directory: cbmc-cover
-- Adding tests in directory: cbmc-incr-oneloop
-- Adding tests in directory: cbmc-incr
-- Adding tests in directory: cbmc-shadow-memory
-- Adding tests in directory: cbmc-output-file
-- Adding tests in directory: cbmc-with-incr
-- Adding tests in directory: array-refinement-with-incr
-- Adding tests in directory: goto-instrument-chc
-- Adding tests in directory: goto-instrument-json
-- Adding tests in directory: goto-instrument-wmm-core
-- Adding tests in directory: goto-instrument-typedef
-- Adding tests in directory: smt2_solver
-- Adding tests in directory: smt2_strings
-- Adding tests in directory: strings
-- Adding tests in directory: invariants
-- Adding tests in directory: goto-diff
-- Adding tests in directory: test-script
-- Adding tests in directory: goto-analyzer-taint
-- Adding tests in directory: goto-gcc
-- Adding tests in directory: goto-cc-cbmc
-- Adding tests in directory: goto-cc-cbmc-shared-options
-- Adding tests in directory: cbmc-cpp
-- Adding tests in directory: goto-cc-goto-analyzer
-- Adding tests in directory: goto-analyzer-simplify
-- Adding tests in directory: statement-list
-- Adding tests in directory: systemc
-- Adding tests in directory: contracts
-- Adding tests in directory: contracts-dfcc
-- Adding tests in directory: goto-synthesizer
-- Adding tests in directory: acceleration
-- Adding tests in directory: k-induction
-- Adding tests in directory: goto-harness
-- Adding tests in directory: goto-harness-multi-file-project
-- Adding tests in directory: goto-cc-file-local
-- Adding tests in directory: goto-cc-regression-gh-issue-5380
-- Adding tests in directory: linking-goto-binaries
-- Adding tests in directory: symtab2gb
-- Adding tests in directory: symtab2gb-cbmc
-- Adding tests in directory: solver-hardness
-- Adding tests in directory: goto-ld
-- Found PythonInterp: /usr/bin/python3 (found suitable version "3.11.2", minimum required is "3.5")
CMake Warning at regression/validate-trace-xml-schema/CMakeLists.txt:5 (message):
  xmllint not found, skipping trace schema tests


Z3_EXISTS-NOTFOUND
-- Adding tests in directory: cbmc-primitives
-- Adding tests in directory: goto-interpreter
-- Adding tests in directory: cbmc-sequentialization
-- Adding tests in directory: cpp-linter
-- Adding tests in directory: catch-framework
-- Adding tests in directory: model_loading
-- Adding tests in directory: snapshot-harness
-- Adding tests in directory: memory-analyzer
-- Adding tests in directory: extract_type_header
-- Configuring done
CMake Error at src/libcprover-cpp/CMakeLists.txt:71 (add_custom_command):
  Error evaluating generator expression:

    $<TARGET_FILE:cadical_ipasir>

  No target "cadical_ipasir"


CMake Error at src/libcprover-cpp/CMakeLists.txt:71 (add_custom_command):
  Error evaluating generator expression:

    $<TARGET_FILE:cadical_ipasir>

  No target "cadical_ipasir"


CMake Error at src/libcprover-cpp/CMakeLists.txt:71 (add_custom_command):
  Error evaluating generator expression:

    $<TARGET_FILE:cadical_ipasir>

  No target "cadical_ipasir"


-- Generating done
CMake Generate step failed.  Build files cannot be regenerated correctly.
@jiegec
Copy link
Author

jiegec commented Apr 2, 2023 •
edited
Loading

Offending commit: 2cee3b1 @esteffin #7567

@esteffin
Copy link
Contributor

esteffin commented Apr 4, 2023 •
edited
Loading

The offending commit is part of a PR that merges all CBMC sub-component static libraries (.a files) into a large one with all symbols defined.
This step takes all dependency locations by using $<TARGET_FILE> and apparently CMake does not allow to access the generator property $<TARGET_FILE> of target imported from out of the scope.

This means that at the moment all solvers that are added as imported targets will fail to build the C++ library or the modules depending on it (like regressions).

To solve this issue it should be possible to either:

  • Provide a different mechanism to resolve the sub-component dependency locations that works with imported libraries from another scope, OR
  • Change the way the cadical-ipasir imported target is created in src/solvers/CMakeLists.txt.

@tautschnig
Copy link
Collaborator

To solve this issue it should be possible to either:

* Provide a different mechanism to resolve the sub-component dependency locations that works with imported libraries from another scope, OR

[...]

#7644 happens to do this, and alas also fixes this problem (just tested).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@tautschnig @esteffin @jiegec