Fix in readme and CMake build system #7652
Conversation
jparsert
requested review from
a team,
kroening,
tautschnig,
peterschrammel and
chris-ryder
as code owners
Codecov ReportPatch coverage has no change and project coverage change:
Additional details and impacted files@@ Coverage Diff @@
## develop #7652 +/- ##
===========================================
+ Coverage 78.50% 78.51% +0.01%
===========================================
Files 1670 1674 +4
Lines 191714 191935 +221
===========================================
+ Hits 150498 150704 +206
- Misses 41216 41231 +15 see 50 files with indirect coverage changes Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report in Codecov by Sentry. |
There was a problem hiding this comment.
Some questions.
As an aside, could you please remove the last commit?
The way we work in CBMC is we rebase our branches on top of branch develop, rather than using merge commits (outside of PRs getting merged).
That should be an easy fix - rebase -i HEAD~4 and drop the last commit, then git checkout develop && git pull origin develop followed by a git checkout <yourbranch> && git rebase develop. (EDIT: A faster way might be git pull origin develop --rebase while on top of your branch, but I'm not sure if this equivalent. A slightly more adventurous option if you're up for it).
CMakeLists.txt
Outdated
| @@ -73,7 +73,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR | |||
| set(CMAKE_CXX_FLAGS_RELEASE "-O2") | |||
| set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") | |||
| # Enable lots of warnings | |||
| set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum") | |||
| set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wno-return-type -Wswitch-enum") | |||
There was a problem hiding this comment.
I'm not sure if this change is correct - the commit message indicates that this would trigger on code marked with our internal UNREACHABLE macro (unless I've misunderstood it), but these are supposed to behave in the way they do to indicate a path that the developer intended to be unreachable (and fail loudly if they are not).
There was a problem hiding this comment.
The problem I get when compiling is sometimes there the function ends in a UNREACHABLE macro but not a return statement. Since GCC does not know that this is unreachable, it complains that there is a path in the non-void function that does not end in a return statement. Hence, it throws a compiler warning, an since -Wall is set, this warning is actually an error and compilation fails.
An other way to resolve this is by forcing to also add a return statement even when the unreachable makro is used.
There was a problem hiding this comment.
I removed the last commit. Hope everything works out now.
There was a problem hiding this comment.
The problem you explain with UNREACHABLE and return warnings isn't one I have encountered when building with GCC myself. The control flow is such that encountering an UNREACHABLE will either result in an exception being thrown or the termination of the process. Either way execution does not continue after the UNREACHABLE which means that neither return statements or suppressing the warnings should be required. Can you give us any further information about the platform and build options which are required to reproduce this issue?
There was a problem hiding this comment.
When building CBMC in my IDE (clion) I get the following error:
/usr/bin/c++ -DHAVE_MINISAT2 -DSATCHECK_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/home/cbmc/cmake-build-debug/src -I/home/cbmc/src -I/home/cbmc/cmake-build-debug/src/solvers -I/home/cbmc/src/solvers -I/home/cbmc/cmake-build-debug/minisat2-src -I/home/cbmc/cmake-build-debug/src/util -I/home/cbmc/src/util -I/home/cbmc/cmake-build-debug/src/big-int -I/home/cbmc/src/big-int -I/home/cbmc/cmake-build-debug/src/langapi -I/home/cbmc/src/langapi -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum -g -fdiagnostics-color=always -std=gnu++11 -MD -MT src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o -MF src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o.d -o src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o -c /home/cbmc/src/solvers/flattening/boolbv_get.cpp
/home/cbmc/src/solvers/flattening/boolbv_get.cpp: In member function ‘virtual exprt boolbvt::bv_get_rec(const exprt&, const bvt&, std::size_t) const’:
/home/cbmc/src/solvers/flattening/boolbv_get.cpp:272:1: error: control reaches end of non-void function [-Werror=return-type]
272 | }
| ^
cc1plus: all warnings being treated as errors
EDIT 2:
See below on how to reproduce this issue
There was a problem hiding this comment.
That is helpful. Can you also confirm which OS flavour / version you have observed this issue with?
There was a problem hiding this comment.
Manjaro Linux. Kernel 6.2.9, worth noting that I had that issue some time ago as well but back then I did not end up using cbmc for my project so I never went looking. Also, I just looked and it seems to not be an issue with ninja, as I also get it when using make instead of ninja.
There was a problem hiding this comment.
@jparsert I see on your compiler invocation that it's building with -std=gnu++11.
I'm not sure if this is at fault here - could you try forcing it to build with -std=c++11 and see what happens?
(Sorry, blueskying here - can't be more helpful than that as I don't use GCC or Linux myself).
There was a problem hiding this comment.
That's a good suggestion, but changing it did not solve the error. I get the same error with the following compilation command:
/usr/bin/c++ -DHAVE_MINISAT2 -DSATCHECK_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/home/julian/Documents/cbmc/cmake-build-debug/src -I/home/julian/Documents/cbmc/src -I/home/julian/Documents/cbmc/cmake-build-debug/src/solvers -I/home/julian/Documents/cbmc/src/solvers -I/home/julian/Documents/cbmc/cmake-build-debug/minisat2-src -I/home/julian/Documents/cbmc/cmake-build-debug/src/util -I/home/julian/Documents/cbmc/src/util -I/home/julian/Documents/cbmc/cmake-build-debug/src/big-int -I/home/julian/Documents/cbmc/src/big-int -I/home/julian/Documents/cbmc/cmake-build-debug/src/langapi -I/home/julian/Documents/cbmc/src/langapi -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum -g -fdiagnostics-color=always -std=c++11 -MD -MT src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o -MF src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o.d -o src/solvers/CMakeFiles/solvers.dir/flattening/boolbv_get.cpp.o -c /home/julian/Documents/cbmc/src/solvers/flattening/boolbv_get.cpp
There was a problem hiding this comment.
I managed to reproduce the issue here.
GCC 12 fails to build CBMC when using Debug as CMake build type.
I created an issue about this here.
I suggest to change the build configuration to something different than Debug on CLion while the issue is being addressed.
Also I would suggest removing this change from the current PR and resolve the issue properly (ideally without the need for -Wno-return-type as compile flag).
| @@ -107,7 +107,7 @@ Contributing to the code base | |||
| 6. Create a Pull Request targeting the `develop` branch | |||
|
|
|||
| New contributors can look through the [mini | |||
| projects](https://github.com/diffblue/cbmc/blob/develop/MINI-PROJECTS.md) | |||
| projects](https://github.com/diffblue/cbmc/blob/develop/FEATURE_IDEAS.md) | |||
src/cbmc/CMakeLists.txt
Outdated
| add_custom_command(OUTPUT "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh" | ||
| COMMAND "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/extract_switches.sh" | ||
| add_custom_command(OUTPUT "${CMAKE_CURRENT_SOURCE_DIR}/../../scripts/bash-autocomplete/cbmc.sh" | ||
| COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/../../scripts/bash-autocomplete/extract_switches.sh" |
There was a problem hiding this comment.
I want to defer checking the correctness of that to @esteffin
There was a problem hiding this comment.
This solves the problem, however I would suggest a tidier approach that avoids the ../...
Why not adding a variable CBMC_ROOT_DIR to the CMakeLists.txt with the value of ${CMAKE_CURRENT_SOURCE_DIR}, and then refer to that from src/cbmc/CMakeLists.txt?
This will remove all the ..s and also will be usable from other folders in case it is needed.
There was a problem hiding this comment.
Thanks for the suggestion, I changed it to your suggestion.
|
A quick general comment on this PR is that it would be easier to manage on our side if it was 2 PRs. The clue to this is that you needed the word "and" in the title. The documentation fix is fairly straight forwardly an improvement, which could be merged straight away. But the changes to the build system require slightly more scrutiny, potentially from different reviewers with different expertise. It isn't worth going to the effort of splitting this PR into 2 PRs right now in my opinion. But it would be good to consider next time though. |
There was a problem hiding this comment.
The PR has changes on several unrelated files.
Is this because some other commits have been dragged in when rebasing?
Also there is a huge amount of padding added to src/cbmc/CMakeLists.txt that seems due to some automatic linter, but that obfuscate the commit.
Please drop the commits that touch unrelated files and remove the extra padding added.
After this I will be more than happy to approve as the other changes are good.
My suggestion is to totally drop commits e684a7b04aa22118fea2df3a7d7d721983bcb3aa, 51d143b9880205a857b4646f9cc3333a3aa43fcf and 31bccd218dbc63e28727cb0b21e987a6aaf1bf18. Then to squash 87ce062f83e881c6a1486b5a6b81ad6d33db89b5, 36a581c37aa88422a1cb41ffd9fe191e57c43979, 143f97d0515681efdd4de5bb228e5e6332e22525 (after removing the extra padding).
Alternatively this can be closed here and the changes moved to a PR with a cleaner history.
src/cbmc/CMakeLists.txt
Outdated
| @@ -1,73 +1,73 @@ | |||
| # Library | |||
| file(GLOB_RECURSE sources "*.cpp" "*.h") | |||
| list(REMOVE_ITEM sources | |||
| ${CMAKE_CURRENT_SOURCE_DIR}/cbmc_main.cpp | |||
| ) | |||
| ${CMAKE_CURRENT_SOURCE_DIR}/cbmc_main.cpp | |||
There was a problem hiding this comment.
Why this line has been tabbed so much?
Similar changes are also everywhere in the file
| COMMAND "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/extract_switches.sh" | ||
| DEPENDS $<TARGET_FILE:cbmc> | ||
| ) | ||
| add_custom_command(OUTPUT "${CBMC_ROOT_DIR}/scripts/bash-autocomplete/cbmc.sh" |
There was a problem hiding this comment.
This is actually one of the 4 lines that should have been modified, but still without the extra padding.
src/libcprover-cpp/api.cpp
Outdated
| @@ -133,57 +133,7 @@ void api_sessiont::load_model_from_files( | |||
| files, *implementation->message_handler, *implementation->options)); | |||
| } | |||
|
|
|||
| void api_sessiont::verify_model() const | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
src/libcprover-cpp/api.h
Outdated
| @@ -69,8 +69,9 @@ struct api_sessiont | |||
| /// \param files: A vector<string> containing the filenames to be loaded | |||
| void load_model_from_files(const std::vector<std::string> &files) const; | |||
|
|
|||
| /// Verify previously loaded model. | |||
| void verify_model() const; | |||
| // Run the verification engine against previously loaded model and return | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
src/libcprover-rust/include/c_api.h
Outdated
| @@ -3,6 +3,7 @@ | |||
| #pragma once | |||
|
|
|||
| #include <memory> | |||
| #include <stdexcept> | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
| @@ -2,6 +2,8 @@ | |||
|
|
|||
| #pragma once | |||
|
|
|||
| #include <string> | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
src/libcprover-rust/src/c_api.cc
Outdated
| @@ -59,3 +59,33 @@ std::vector<std::string> const &get_messages() | |||
| { | |||
| return output; | |||
| } | |||
|
|
|||
| verifier_resultt get_verification_result( | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
src/libcprover-rust/src/lib.rs
Outdated
| @@ -5,14 +5,74 @@ | |||
| #[cxx::bridge] | |||
| pub mod cprover_api { | |||
|
|
|||
| // The following two definitions for enums are *shared types* - in | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
| @@ -8,6 +8,7 @@ | |||
| #include <libcprover-cpp/verification_result.h> | |||
|
|
|||
| #include <iostream> | |||
| #include <memory> | |||
There was a problem hiding this comment.
Why has this file being touched by this PR?
It shouldn't be changed.
jparsert
requested review from
qinheping,
feliperodri,
remi-delmas-3000,
romainbrenguier and
jimgrundy
as code owners
…ve path with CMAKE_CURRENT_SOURCE_DIR.
|
Sorry for adding clutter/commits that should not belong. I cleaned it up and it should now only contain my changes (without padding issues) |
|
Is there anything more I have to do to get pull request accepted? |
The approval from @esteffin should be sufficient to get the cmake change merged. He is a member of the @diffblue/diffblue-opensource group which is codeowner for the I think this still needs separate approval for the docs change as neither of your approvals are from documentation code owners. @NlightNFotis can you approve so we have docs code owner approval? FYI - Who exactly needs to approve should be defined based on https://github.com/diffblue/cbmc/blob/develop/CODEOWNERS |
Fixes #7649 for Cmake builds using
add_subdirectoryas well asfetch_content.Now the bash scripts are generated/called relative to the directory where
/src/cbmc/CMakeFiles.txtis located. This means that when the originalCMakeFiles.txtis outside of cbmc's root directory (for example in an external project) then the correct path is used when running the bash scripts.Edit( This has been removed and a separate issue has been created): I also added the "-Wno-return-type" flag as that threw compilation errors in cases where
UNREACHABLEwas used but no return was used in dead code.I also fixed a link in the readme.md that used to point to "MINI-PROJECTS". It now points to "FEATURE_IDEAS.md".