Add CMakeLists alongside existing makefiles #1293

reuk · 2017-08-24T10:13:59Z

By adding a CMake build alongside the makefile build, we can continue supporting existing users of CBMC, while also supporting development in a wider range of IDEs, with faster build back-ends and better integration with clang-based static-analysis and code completion tools (clang-tidy and YCM).

As long as both builds are tested in CI, we don't need to worry about the build systems getting out-of-sync. I don't think having two build systems will add maintenance overhead: I've been maintaining this build for the last three months or so, and the only time I've had to update it was when unit tests were added. This is possible because I've set the build to automatically pick-up all the source files in each directory containing a CMakeLists.txt (in fact, some of the source files don't build and should probably be removed).

thk123

I'm not going to pretend to understand CMake to verify that this is correct. This does appear to build on my machine (+ with the travis change I suppose we can have some certainty it builds elsewhere).

I have two questions:

Is there a way to verify that the make files generated by this are equivalent (or perhaps generate them from this, and replace the current Makefiles with the generated ones)
if there are any gotchas or weird non cmake-standard things in here, could they be documented (perhaps there are none).

reuk · 2017-08-24T13:23:55Z

Is there a way to verify that the make files generated by this are equivalent (or perhaps generate them from this, and replace the current Makefiles with the generated ones)

The generated makefiles will not be equivalent. CMake generates machine-dependent makefiles (the point being that it abstracts over different machine configurations itself, and generates tailor-made makefiles). Therefore, it's not viable to replace the makefile build with cmake-generated makefiles.

if there are any gotchas or weird non cmake-standard things in here, could they be documented (perhaps there are none).

There's nothing too weird in here, but if this is adopted I'll add a "getting started with CMake" to the wiki.

tautschnig · 2017-08-24T13:26:37Z

Please add documentation to COMPILING that explains how to use the build system, if there are any changes over the current state.

thk123

I'd like to see a test-gen PR introducing this just to check that there aren't any nasty surprises, otherwise LGTM.

tautschnig · 2017-08-25T08:30:43Z

The CI jobs should do some form of checking beyond "it compiles." This might either be enabling the regression and/or unit tests, or a simple comparison of the binaries (which ought to be identical, after all).

reuk · 2017-08-25T08:31:26Z

I just thought of something that won't work yet: the CBMC executable will be built out-of-source, so the regression tests won't be able to find it. Given that the user might put the build anywhere, it's not practical to hard-code the path. Maybe for now I should just explain that users need to symlink the CBMC executable into src/cbmc, but there's probably a better solution I haven't thought of.

tautschnig · 2017-08-25T08:31:55Z

COMPILING

+---------------------------------
+
+There is an experimental build based on CMake instead of hand-written
+makefiles. You may prefer to use this, as it should work on a wider variety of


Omit "You may prefer to use this" -- this isn't marketing.

tautschnig · 2017-08-25T08:33:45Z

COMPILING

+   have a package for CMake, and Mac users can get it through homebrew.
+   Windows users should download it manually from cmake.org.
+
+1) Navigate to the CBMC directory in a terminal.


Get the instructions in line with the above instructions: precise commands, no fuffing about a "CBMC directory" (no idea what that is).

tautschnig · 2017-08-25T08:34:40Z

COMPILING

+
+1) Navigate to the CBMC directory in a terminal.
+
+2) Create somewhere to store your build:


Be precise in your wording: "Create a directory", not "somewhere"

tautschnig · 2017-08-25T08:41:55Z

COMPILING

+   build back-ends. You can use clang (for example) by adding the argument
+   `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
+   CMake to generate IDE projects by supplying the `-G` flag.
+   Run `cmake -G` for a comprehensive list of supported back-ends.


Thank you for the detailed instructions. Yet: how to set compiler options? For example, how to change optimisation, how to set additional linking flags? The bits currently in config.inc must be clearly documented here.

tautschnig · 2017-08-25T08:44:01Z

src/ansi-c/CMakeLists.txt

+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
+)
+
+generic_includes(ansi-c)


Where is make library_check implemented?

It's not yet. I'll look at that now.

tautschnig · 2017-08-25T08:46:09Z

src/CMakeLists.txt

+)
+add_dependencies(minisat2-condensed minisat2-extern)
+
+#   Override add_executable to automatically sign the target on OSX.


Where are universal binaries and the MacOS version implemented?

That's handled automatically. By default, the build will be for the architecture of the machine running the build. However, you can also supply the flag -DCMAKE_OSX_ARCHITECTURES=i386;x86_64 to build fat binaries.

Will -mmacosx-version-min=10.9 also be supported? Note that this ought to be the default as we have had problems in the past with users being unable to run the tool on those older MacOS versions.

Essentially, whatever is currently configured in common and config.inc ought to be the default for the CMake builds as well.

tautschnig

In a few areas I do not yet understand how CMake mimics all the previous features. See comments above.

tautschnig · 2017-08-25T08:49:28Z

I just thought of something that won't work yet: the CBMC executable will be built out-of-source, so the regression tests won't be able to find it. Given that the user might put the build anywhere, it's not practical to hard-code the path. Maybe for now I should just explain that users need to symlink the CBMC executable into src/cbmc, but there's probably a better solution I haven't thought of.

Shouldn't the regression tests (and unit tests!) also be run from within the "build" (or whatever the user chosen name) folder? That is, all the artifacts generated by running regression tests ought to end up within the "build" folder, not underneath the "regression" folder as is currently the case.

reuk · 2017-08-25T10:16:15Z

Shouldn't the regression tests (and unit tests!) also be run from within the "build" (or whatever the user chosen name) folder? That is, all the artifacts generated by running regression tests ought to end up within the "build" folder, not underneath the "regression" folder as is currently the case.

They should, and this is the case for the unit tests. I'll try to fix this for regression tests too.

reuk · 2017-08-25T14:19:02Z

I've been hacking around with the regression tests. The ones with custom driver scripts are a bit awkward, because the scripts have to be adjusted to drive arbitrary executables instead of hard-coded ones. Other than that, it seems to work (on my machine). If it gets through CI I'll squash the commits appropriately.

Tests can be run with ctest -V from the build directory. That will run everything (units + regressions), but specific tests can be singled out using the -R flag.

peterschrammel

Tested on Ubuntu and Mac. Works fine.

peterschrammel · 2017-09-07T20:34:12Z

src/solvers/CMakeLists.txt

@@ -0,0 +1,85 @@
+#   TODO Specify which solver to use (minisat2 etc.)


Could you try using glucose and document the changes required to get it to run?

I'll do that now.

peterschrammel · 2017-09-07T20:52:59Z

.travis.yml

+          packages:
+            - g++-5
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_FLAGS_RELEASE=-O3' '-DCMAKE_CXX_FLAGS=-Wall -Wpedantic -Werror' '-DCMAKE_CXX_COMPILER=g++-5'


Do we compile with -O3 now?

The default "Release" flags for clang++ and g++ are -O3 -DNDEBUG. We have to keep assertions enabled, which is why I've manually overridden the flags. I can switch to -O2 too if you'd like.

I'd say for a start the Release build ought to be using an as similar set of flags as the current build as possible. Is it possible to make this the default in the CMake configuration rather than requiring overrides on the command line?

reuk · 2017-09-08T10:21:00Z

I've addressed the last few comments.

The glucose build can now be enabled by supplying the flag '-Dsat_impl=glucose' to the initial call to CMake (there's an example in the travis config). The default sat impl remains minisat2. As a byproduct of this, I updated satcheck.h and config.inc a bit, so that glucose can be enabled from the makefiles just by modifying config.inc with the path to glucose. There's no longer a need to update the defines in satcheck.h.

Also, build flags should match the makefile flags more closely by default. This also allows the travis config to be simplified.

reuk · 2017-09-08T10:44:35Z

I've also simplified the CMake files based on #1321.

reuk · 2017-09-08T12:18:06Z

Some of the regression tests fail when glucose is used. Switching this off for now.

tautschnig · 2017-09-10T22:25:28Z

Some of the regression tests fail when glucose is used. Switching this off for now. Can this be captured in an issue, possibly also with a note on what the mismatch is? Thanks!

reuk · 2017-09-11T09:11:50Z

I've added an issue, #1366, describing the problem

reuk · 2017-09-13T08:52:09Z

@peterschrammel are you happy with this now?

peterschrammel

LGTM

peterschrammel · 2017-09-13T14:12:31Z

@reuk, is this mergeable or do you plan further additions for now?

reuk · 2017-09-13T14:13:09Z

Yes, it's mergeable

08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914 e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914 4df244c Merge pull request diffblue#1383 from reuk/reuk/sync-projects f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code 1fae64c Remove stray use of overlay_map 1264b4d Re-enable old function signatures for test-gen compat e54c0e9 Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program 63c9a1e Merge pull request diffblue#1374 from reuk/reuk/maintain-pointer-invariants 00e4555 Fix up CMake build (unrelated) 81f1300 Use PRECONDITION in std_types.h a9806c0 Ensure pointer invariants are maintained a46ad62 Regenerate malformed binary blobs f77822b Merge pull request diffblue#1380 from diffblue/remove-musketeer 22f06fd Correcting windows build 3ede81b Merge pull request diffblue#1293 from reuk/cmake-develop 92a52a5 Corrected doxygen errors c6f1430 Ensure symex and goto-analyzer regenerate functions e37d3d5 Disable failing test in the symex directory 15b89fc Weaked the tests for pointer-function-parameters dee89b0 Fixing the method to work with java_bytecode 1ccd1a2 Add support for using the --function flag to goto-analyze and symex 0732580 Adding missing overrides 71dec3d Use ID_main as the default name for entry function 2aea88d Made generate_start_function abstract f0d6d72 Refactored the regenerate function into goto-programs 71e6800 Added regression test for using --function on a GOTO program 94b7185 Implemented generate_start_function for Java cd416bc Call generate_start_function only when regenerating the start function ee5fb93 Protect against invalid function label 2a3d876 Adding explanatory comment f347a22 Cause a regeneration of the entry method if a --function is provided 69d05a9 Merge pull request diffblue#1382 from pkesseli/bugfix/language-opaque-stubs d45325c Merge pull request diffblue#1378 from thk123/bugfix/fix-symex-appveyor 444f256 Add initial value to languaget::generate_opaque_stubs 91e733d Manually disable some failing tests 41bafc0 Merge pull request diffblue#1375 from pkesseli/bugfix/uncaught-exceptions-invariant a31f1d9 remove musketeer af8d46f Reverting manually commited fixes e73a884 Attempt to fix the symex appveyor build 0496142 Account for replaced functions in exceptions_map 2816b80 revert symex regression until Appvoyer works 6a2fd50 added symex to Appveyor build a2834d0 Map wrappers: forward more of the std::map interface 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2 8cd4490 Merge pull request diffblue#1373 from diffblue/symex-trace-fix 5d2d07b enable symex regression testing 5195d24 avoid confusion between SSA lhs and full lhs during assignment 430218f option is now --trace 746bff5 remove_returns missing in symex 211355d comments on test 3896110 output statements 8fc714d use __CPROVER_assert 728ac5b Merge pull request diffblue#1367 from reuk/reuk/disable-alpine-in-travis 73b4357 Merge pull request diffblue#1339 from diffblue/initialize_goto_model 4febd10 Merge pull request diffblue#1364 from diffblue/phread-create-fix 0cfd7b0 Remove PRE_COMMAND scaffolding 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc 577fa6c Tightened up usage of maps 8782103 Merge pull request diffblue#1365 from smowton/smowton/feature/more_map_forwarding 4dde3c5 Disable glucose in Travis 91684da Clean up CMake files after diffblue#1321 7d4e9b5 Make CMake release flags similar to Makefile build 5ee349f Control SAT library from makefiles ad486f8 Set up glucose externalproject 5afa929 Quote paths in flex/bison commands 9afbced Disable 32-bit builds in Travis d953327 Enable caching for CMake builds (hopefully) 6251055 Fix and refactor library_check target 3c36aa5 Enable CMake in Travis f6e4968 Enable running tests from CMake e609bbb Add CMake howto to COMPILING file 22c2ab9 Add CMakeLists 6facf74 Map wrappers: forward more of the std::map interface b846858 Merge pull request diffblue#1291 from LAJW/optional 3ddd377 clean-out ill-modeled optimization in string comparisons 95c5e63 Disable Alpine in Travis fe60e60 pthread_create arguments null/nonnull fix 7d30cde missing copyright header 8c4ff7b remove spurious references to langapi/language_ui.h e4498ca brief list of symbols, from language_uit fc4d44a use goto_modelt 9469552 use initialize_goto_model in CBMC/goto-analyse/etc 40fe0f8 simplify API of goto_convert 40557df Used range iterators d4e89fd Tidy up symbol_tablet::move c125146 Merge pull request diffblue#1245 from tautschnig/run-diagnostic 435c0bf Merge pull request diffblue#1321 from reuk/reuk/remove-unused-files 08a4077 Make the child process that failed to execvp exit 4928f69 Diagnostic output if run/execve fails 5863a75 Merge pull request diffblue#1333 from tautschnig/remove-c_sizeof 498718f Code readability 2217501 Remove unused files 1c8d81a Merge pull request diffblue#1356 from smowton/smowton/feature/test_pl_add_dry_run 56b5e25 Merge pull request diffblue#1358 from thk123/feature/decrease-message-spam 359a3e3 Modified verbosity for loaded message 296349c Add dry-run mode to test.pl f6d94cf clean out an unused method 3613ebc When possible, update array types before typechecking initializer 3273bf5 Fix type casts from initializer lists to arrays of unspecified size 1fa569f sizeof(*(void*)) is sizeof(char) d79067e Remove long-deprecated c_sizeof in favour of size_of_expr et al. 254f133 Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const 388a25e Make uncaught_exceptions_analysis.output const 211fcc2 Make path_nodet.output const 9be84ea Make automatont.output const 567eaa7 Make basic_blockst.output const ebbbf5f Make goto_modelt.output const ae584df Move optional unit tests into util directory 4dbf939 Manually fix optional 43d0602 Add unit tests for nonstd::optional 8584bb0 Add nonstd/optional.hpp library 281e384 Workaround for travis performing shallow clones with wrong branch git-subtree-dir: cbmc git-subtree-split: 08f269c

reuk force-pushed the cmake-develop branch from e682e5e to 08285f8 Compare August 24, 2017 13:16

thk123 reviewed Aug 24, 2017

View reviewed changes

reuk force-pushed the cmake-develop branch 9 times, most recently from ee8bc72 to 58fc70d Compare August 24, 2017 17:04

thk123 approved these changes Aug 25, 2017

View reviewed changes

tautschnig reviewed Aug 25, 2017

View reviewed changes

reuk force-pushed the cmake-develop branch from 7cb2539 to 734d5dd Compare August 25, 2017 10:13

reuk force-pushed the cmake-develop branch 2 times, most recently from 3c694b5 to 957fc5b Compare August 25, 2017 14:10

reuk force-pushed the cmake-develop branch from 68ac28c to 9993f12 Compare August 25, 2017 16:59

peterschrammel reviewed Sep 7, 2017

View reviewed changes

reuk force-pushed the cmake-develop branch from 67faaf9 to 80321b4 Compare September 8, 2017 10:07

reuk force-pushed the cmake-develop branch from 1306e4a to ed44ec1 Compare September 8, 2017 10:43

reuk mentioned this pull request Sep 11, 2017

Some CORE regression tests do not complete when CBMC is built with Glucose #1366

Closed

reuk added 13 commits September 11, 2017 14:29

Add CMakeLists

22c2ab9

Add CMake howto to COMPILING file

e609bbb

Enable running tests from CMake

f6e4968

Enable CMake in Travis

3c36aa5

Fix and refactor library_check target

6251055

Enable caching for CMake builds (hopefully)

d953327

Disable 32-bit builds in Travis

9afbced

Quote paths in flex/bison commands

5afa929

Set up glucose externalproject

ad486f8

Control SAT library from makefiles

5ee349f

Make CMake release flags similar to Makefile build

7d4e9b5

Clean up CMake files after diffblue#1321

91684da

Disable glucose in Travis

4dde3c5

reuk force-pushed the cmake-develop branch from 8c046fa to 4dde3c5 Compare September 11, 2017 13:29

peterschrammel approved these changes Sep 13, 2017

View reviewed changes

peterschrammel merged commit 3ede81b into diffblue:develop Sep 13, 2017

reuk deleted the cmake-develop branch September 14, 2017 17:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add CMakeLists alongside existing makefiles #1293

Add CMakeLists alongside existing makefiles #1293

reuk commented Aug 24, 2017

thk123 left a comment

reuk commented Aug 24, 2017

tautschnig commented Aug 24, 2017

thk123 left a comment

tautschnig commented Aug 25, 2017

reuk commented Aug 25, 2017

tautschnig Aug 25, 2017

tautschnig Aug 25, 2017

tautschnig Aug 25, 2017

tautschnig Aug 25, 2017

tautschnig Aug 25, 2017

reuk Aug 25, 2017

tautschnig Aug 25, 2017

reuk Aug 25, 2017

tautschnig Aug 25, 2017

tautschnig left a comment •

edited

Loading

tautschnig commented Aug 25, 2017

reuk commented Aug 25, 2017

reuk commented Aug 25, 2017 •

edited

Loading

peterschrammel left a comment

peterschrammel Sep 7, 2017

reuk Sep 8, 2017

peterschrammel Sep 7, 2017

reuk Sep 8, 2017

tautschnig Sep 8, 2017

reuk commented Sep 8, 2017 •

edited

Loading

reuk commented Sep 8, 2017

reuk commented Sep 8, 2017

tautschnig commented Sep 10, 2017 via email

reuk commented Sep 11, 2017 •

edited

Loading

reuk commented Sep 13, 2017

peterschrammel left a comment

peterschrammel commented Sep 13, 2017

reuk commented Sep 13, 2017


		1) Navigate to the CBMC directory in a terminal.

		2) Create somewhere to store your build:

		@@ -0,0 +1,85 @@
		# TODO Specify which solver to use (minisat2 etc.)

Add CMakeLists alongside existing makefiles #1293

Add CMakeLists alongside existing makefiles #1293

Conversation

reuk commented Aug 24, 2017

thk123 left a comment

Choose a reason for hiding this comment

reuk commented Aug 24, 2017

tautschnig commented Aug 24, 2017

thk123 left a comment

Choose a reason for hiding this comment

tautschnig commented Aug 25, 2017

reuk commented Aug 25, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment • edited Loading

Choose a reason for hiding this comment

tautschnig commented Aug 25, 2017

reuk commented Aug 25, 2017

reuk commented Aug 25, 2017 • edited Loading

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk commented Sep 8, 2017 • edited Loading

reuk commented Sep 8, 2017

reuk commented Sep 8, 2017

tautschnig commented Sep 10, 2017 via email

reuk commented Sep 11, 2017 • edited Loading

reuk commented Sep 13, 2017

peterschrammel left a comment

Choose a reason for hiding this comment

peterschrammel commented Sep 13, 2017

reuk commented Sep 13, 2017

tautschnig left a comment •

edited

Loading

reuk commented Aug 25, 2017 •

edited

Loading

reuk commented Sep 8, 2017 •

edited

Loading

reuk commented Sep 11, 2017 •

edited

Loading