Native CMake support in VisualStudio #5162

LAJW · 2019-10-13T00:27:04Z

These changes let you compile and run this project using VisualStudio's native CMake support.

To achieve this, I dropped the dependency on Cygwin, and only require git bash (which you're bound to have if you're using git) and the chocolatey winflexbison3 package (chocolatey is already used/preinstalled on CI).

Tested on VS2019 community edition, developer experience is much better than manually generating projects with CMake - it uses Ninja by default, which uses multi core compilation, unlike manually generated CMake projects.

Setup on VS with this PR boils down to two steps:

choco install winflexbison3
File -> Open -> CMake -> CBMC
Each commit message has a non-empty body, explaining why the change was made.
[n/a] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[n/a] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
[n/a] Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton · 2019-10-14T08:46:13Z

Oh actually, question: since at the moment we require VS 2015+, does this degrade the experience on VS2015 or 2017?

LAJW · 2019-10-14T10:04:36Z

@smowton, nope, you still can configure cmake the old way (and with less dependencies). This is just adding cmake native as an option (which is available even in 2017). The only downside is you need to have git.

chrisr-diffblue

The CMake changes look OK to me - might also be worth @hannes-steffenhagen-diffblue taking a look at those too. One thing I am a bit concerned about is that, if I'm reading this PR correctly, you've switched the CI builds from Makefile based builds to CMake based builds, yes? We have end users that depend on Windows Makefile based builds, so I would like to see those builds still exercised in CI somewhere so that they don't bit rot... Unless @peterschrammel is happy for CI to change if he thinks the users I have in mind might be willing to change their build system?

LAJW · 2019-10-14T10:34:10Z

@chrisr-diffblue Fair enough, I'm not particularly attached to CI changes. I just wanted to try to see them work on CI. Removed.

chrisr-diffblue

Thanks @LAJW - the other option would be to liaise with Peter S about potentially adding a second Windows CI build, so that both the CMake and Make based builds get exercised in CI.

chrisr-diffblue · 2019-10-14T10:40:36Z

Oh, and one other thought (sorry! :-) ) - I believe the Windows Makefile builds use CLCACHE - do the CMake based builds do the same?

LAJW · 2019-10-14T10:49:30Z

@chrisr-diffblue That was the intent in the CI changes. We're gonna have to make it work for test-gen too, so it'll come around. Outside of that you can use whichever generator you want.

Suppresses a "missing project" warning. Each CBMC project should have a project tag.

This way you don't have to use Cygwin on Windows to configure cbmc with CMake and allows you to use Windows's native CMake support (assuming git is installed).

It's probably safe to assume (since the project relies on submodules) that the user has git installed, so this will stop configuration rather than display a warning and then stop with a confusing error.

codecov-io · 2019-10-15T17:27:50Z

Codecov Report

Merging #5162 into develop will decrease coverage by 0.06%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #5162      +/-   ##
===========================================
- Coverage    67.25%   67.19%   -0.07%     
===========================================
  Files         1155     1149       -6     
  Lines        94461    94247     -214     
===========================================
- Hits         63534    63328     -206     
+ Misses       30927    30919       -8

Flag	Coverage Δ
#cproversmt2	`42.72% <ø> (+0.07%)`	⬆️
#regression	`63.71% <ø> (-0.03%)`	⬇️
#unit	`31.92% <ø> (-0.05%)`	⬇️

Impacted Files	Coverage Δ
src/analyses/loop_analysis.h	`96% <0%> (-4%)`	⬇️
src/util/expr.cpp	`63.86% <0%> (-1.18%)`	⬇️
src/solvers/strings/string_refinement.cpp	`87.84% <0%> (-0.69%)`	⬇️
src/goto-symex/symex_main.cpp	`87.19% <0%> (-0.55%)`	⬇️
jbmc/src/jbmc/jbmc_parse_options.cpp	`71.56% <0%> (-0.42%)`	⬇️
src/goto-symex/symex_function_call.cpp	`86.71% <0%> (-0.28%)`	⬇️
src/solvers/smt2/smt2_parser.cpp	`66.92% <0%> (-0.06%)`	⬇️
src/util/object_factory_parameters.h	`100% <0%> (ø)`	⬆️
src/solvers/smt2/smt2_parser.h	`100% <0%> (ø)`	⬆️
src/goto-symex/path_storage.h	`100% <0%> (ø)`	⬆️
... and 20 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1cb10ad...069c761. Read the comment docs.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: ecce25f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132017019
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

LAJW · 2019-10-16T10:29:58Z

Edit: fixup - I misunderstood how/where ansi_c_library_sources file was created

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 676cb0b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132178299
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 7707605).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132184613

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 85d15a5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132325446

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 069c761).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132328171

LAJW · 2019-10-17T15:22:52Z

@peterschrammel windows/cmake codebuild added (with ninja and clcache)!

peterschrammel · 2019-10-17T15:34:47Z

@kroening, @tautschnig, this is ready to go.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1cf0056).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132386896
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 519a802).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/132408233

LAJW added the RFC Request for comment label Oct 13, 2019

LAJW requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners October 13, 2019 00:27

LAJW changed the title ~~Native CMake support in VisualStudio~~ [RFC] Native CMake support in VisualStudio Oct 13, 2019

LAJW requested a review from jeannielynnmoulton October 13, 2019 00:33

smowton approved these changes Oct 14, 2019

View reviewed changes

chrisr-diffblue suggested changes Oct 14, 2019

View reviewed changes

chrisr-diffblue approved these changes Oct 14, 2019

View reviewed changes

LAJW removed the RFC Request for comment label Oct 14, 2019

LAJW changed the title ~~[RFC] Native CMake support in VisualStudio~~ Native CMake support in VisualStudio Oct 14, 2019

Lukasz A.J. Wrona added 3 commits October 14, 2019 15:10

Add project(CBMC) to CMakeLists

7949cac

Suppresses a "missing project" warning. Each CBMC project should have a project tag.

Use git bash when configuring CMake

f0887bc

This way you don't have to use Cygwin on Windows to configure cbmc with CMake and allows you to use Windows's native CMake support (assuming git is installed).

Display an error in case Git wasn't found

ecce25f

It's probably safe to assume (since the project relies on submodules) that the user has git installed, so this will stop configuration rather than display a warning and then stop with a confusing error.

allredj reviewed Oct 15, 2019

View reviewed changes

Generate ansi_c_library_sources file in a cross platform way

7707605

allredj reviewed Oct 16, 2019

View reviewed changes

LAJW requested a review from thk123 as a code owner October 16, 2019 21:12

allredj reviewed Oct 17, 2019

View reviewed changes

Lukasz A.J. Wrona added 2 commits October 17, 2019 16:20

Add ansi-c/converter_input.txt to .gitignore

9cf5be3

Add Visual Studio/CMake Codebuild config

519a802

peterschrammel approved these changes Oct 17, 2019

View reviewed changes

peterschrammel assigned tautschnig and kroening Oct 17, 2019

allredj reviewed Oct 17, 2019

View reviewed changes

tautschnig approved these changes Oct 18, 2019

View reviewed changes

tautschnig merged commit ec65596 into diffblue:develop Oct 18, 2019

tautschnig mentioned this pull request Oct 18, 2019

[WIP] Use Visual Studio and CMake in Windows CI builds #4300

Closed

4 tasks

LAJW deleted the lajw/visual-studio-native branch October 19, 2019 21:44

Native CMake support in VisualStudio #5162

Native CMake support in VisualStudio #5162

Uh oh!

Conversation

LAJW commented Oct 13, 2019

Uh oh!

smowton commented Oct 14, 2019

Uh oh!

LAJW commented Oct 14, 2019

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW commented Oct 14, 2019

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue commented Oct 14, 2019

Uh oh!

LAJW commented Oct 14, 2019

Uh oh!

codecov-io commented Oct 15, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW commented Oct 16, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW commented Oct 17, 2019

Uh oh!

peterschrammel commented Oct 17, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Oct 15, 2019 •

edited

Loading

LAJW commented Oct 16, 2019 •

edited

Loading