Naming collisions prevent linking against libcprover.5.78.0.a

[NlightNFotis]

In #7567 we have implemented a build system enhancement wherein we are packaging CBMC and the assorted tools as a static library, as part of our preparation for building using the external APIs.

In #7493 we also allowed building CBMC by default with support for both minisat2 and cadical as sat solvers.

The interaction between these two PRs is causing an issue with our static library (which is effectively an archive of object .o files): if any of the projects being integrated have naming collisions, only one of the two colliding files is going to be included in the final static archive.

This is unfortunate, as CBMC contains (as an example) a file called message.cpp under src/util/message.cpp, which collides with a similarly named file (message.cpp) in cadical under cadical/src/message.cpp.

As a result, we are getting issues when trying to link (this is from the compilation of the Rust API):

  = note: Undefined symbols for architecture arm64:
            "CaDiCaL::fatal_message_end()", referenced from:
                CaDiCaL::Checker::add_derived_clause(std::__1::vector<int, std::__1::allocator<int> > const&) in libcprover.5.78.0.a(checker.cpp.o)
                CaDiCaL::Checker::delete_clause(std::__1::vector<int, std::__1::allocator<int> > const&) in libcprover.5.78.0.a(checker.cpp.o)
                CaDiCaL::External::check_satisfiable() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_solution_on_learned_clause() in libcprover.5.78.0.a(solution.cpp.o)
                CaDiCaL::External::check_solution_on_shrunken_clause(CaDiCaL::Clause*) in libcprover.5.78.0.a(solution.cpp.o)
            "CaDiCaL::fatal_message_start()", referenced from:
                CaDiCaL::Checker::add_derived_clause(std::__1::vector<int, std::__1::allocator<int> > const&) in libcprover.5.78.0.a(checker.cpp.o)
                CaDiCaL::Checker::delete_clause(std::__1::vector<int, std::__1::allocator<int> > const&) in libcprover.5.78.0.a(checker.cpp.o)
                CaDiCaL::require_solver_pointer_to_be_non_zero(void const*, char const*, char const*) (.cold.1) in libcprover.5.78.0.a(contract.cpp.o)
                CaDiCaL::External::check_satisfiable() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_solution_on_learned_clause() in libcprover.5.78.0.a(solution.cpp.o)
                CaDiCaL::External::check_solution_on_shrunken_clause(CaDiCaL::Clause*) in libcprover.5.78.0.a(solution.cpp.o)
                CaDiCaL::Solver::~Solver() in libcprover.5.78.0.a(solver.cpp.o)
                ...
            "CaDiCaL::fatal(char const*, ...)", referenced from:
                CaDiCaL::External::internalize(int) in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_satisfiable() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_assumptions_satisfied() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_assumptions_failing() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_no_solution_after_learning_empty_clause() in libcprover.5.78.0.a(solution.cpp.o)
                CaDiCaL::External::check_solution_on_learned_unit_clause(int) in libcprover.5.78.0.a(solution.cpp.o)
                CaDiCaL::Solver::Solver() in libcprover.5.78.0.a(solver.cpp.o)
                ...
            "CaDiCaL::Options::set(char const*, int)", referenced from:
                CaDiCaL::Solver::set(char const*, int) in libcprover.5.78.0.a(solver.cpp.o)
            "CaDiCaL::Options::Options(CaDiCaL::Internal*)", referenced from:
                CaDiCaL::Internal::Internal() in libcprover.5.78.0.a(internal.cpp.o)
            "CaDiCaL::version()", referenced from:
                CaDiCaL::Solver::version() in libcprover.5.78.0.a(solver.cpp.o)
            "CaDiCaL::Internal::print_prefix()", referenced from:
                CaDiCaL::Internal::report(char, int) in libcprover.5.78.0.a(report.cpp.o)
            "CaDiCaL::Internal::cover()", referenced from:
                CaDiCaL::Internal::elim(bool) in libcprover.5.78.0.a(elim.cpp.o)
            "CaDiCaL::Internal::phase(char const*, long long, char const*, ...)", referenced from:
                CaDiCaL::Internal::rescale_variable_scores() in libcprover.5.78.0.a(analyze.cpp.o)
                CaDiCaL::Internal::block_schedule(CaDiCaL::Blocker&) in libcprover.5.78.0.a(block.cpp.o)
                CaDiCaL::Internal::block() in libcprover.5.78.0.a(block.cpp.o)
                CaDiCaL::Internal::delete_garbage_clauses() in libcprover.5.78.0.a(collect.cpp.o)
                CaDiCaL::Internal::copy_non_garbage_clauses() in libcprover.5.78.0.a(collect.cpp.o)
                CaDiCaL::Internal::compact() in libcprover.5.78.0.a(compact.cpp.o)
                CaDiCaL::Internal::condition_round(long) in libcprover.5.78.0.a(condition.cpp.o)
                ...
            "CaDiCaL::Internal::message(char const*, ...)", referenced from:
                CaDiCaL::Internal::add_new_original_clause() in libcprover.5.78.0.a(clause.cpp.o)
                CaDiCaL::Internal::report(char, int) in libcprover.5.78.0.a(report.cpp.o)
            "CaDiCaL::Internal::verbose(int, char const*, ...)", referenced from:
                CaDiCaL::Internal::failing() in libcprover.5.78.0.a(assume.cpp.o)
                CaDiCaL::Internal::add_new_original_clause() in libcprover.5.78.0.a(clause.cpp.o)
                CaDiCaL::External::check_satisfiable() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_assumptions_satisfied() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::External::check_assumptions_failing() in libcprover.5.78.0.a(external.cpp.o)
                CaDiCaL::Internal::instantiate(CaDiCaL::Instantiator&) in libcprover.5.78.0.a(instantiate.cpp.o)
                CaDiCaL::Internal::trivially_false_satisfiable() in libcprover.5.78.0.a(lucky.cpp.o)
                ...
            "CaDiCaL::Internal::vmessage(char const*, char*&)", referenced from:
                CaDiCaL::Solver::message(char const*, ...) in libcprover.5.78.0.a(solver.cpp.o)
          ld: symbol(s) not found for architecture arm64
          clang: error: linker command failed with exit code 1 (use -v to see invocation)
          

error: could not compile `cprover-api-rust` due to previous error
error: Recipe `test-rust-api` failed on line 28 with exit code 101

In the linking error, you can see some of the files that were included from Cadical (clause.cpp, external.cpp, etc) fail to link because of the reference to a function (CaDiCaL::fatal_message_end()) defined in message.cpp that wasn't included.

[peterschrammel]

Namespaces?

[NlightNFotis]

@peterschrammel Are you referring to the C++ language feature?

If yes, C++ Namespaces are not going to help with this particular issue, as this is a linking issue, and the linker (more precisely, the archiver - the static library packager) is operating on a more crude basis, taking filenames into account.

The exact problem here is that two files of the same name are included in an order that causes one to be shadowed by the other on a file-system basis - at least as far as I understand it.

[peterschrammel]

I see. There are clashing compilation units.

[tautschnig]

Two options:

1. GNU ar knows 'P', which will preserve full path names. But that might not be portable.
2. Rename files to encode directory names in the base name (something like cadical-src-message.o).