Fix cmake build from VS2019 command prompt #5306

markrtuttle · 2020-04-19T16:05:13Z

I made these changes to get cbmc to build on Windows from the VS2019 command prompt with the cmake, git, and ninja installed there.

My method was

Install Visual Studio Community 2019
- Desktop development with C++
- Individual components -> Code tools -> Git for windows, Git extension for Visual Studio
Open x64 Native Tools Command Prompt for VS 2019
PATH="c:\Program Files\Git\usr\bin";%PATH%
curl -L https://downloads.sourceforge.net/project/winflexbison/win_flex_bison-latest.zip > bison.zip
unzip bison.zip
cmake -S. -Bbuild -GNinja -DWITH_JBMC=NO
cmake --build build

hannes-steffenhagen-diffblue · 2020-04-20T10:26:50Z

src/util/expr_iterator.h

-  { m_stack=std::move(other.m_stack); }
+  {
+    m_stack=std::move(other.m_stack);
+    // VS 2019 cl wants this function definition to return a value


👍 to the change, but I don't think this comment is necessary. Considering this is declared as returning a value it certainly should.

hannes-steffenhagen-diffblue · 2020-04-20T10:28:18Z

src/util/expr_iterator.h

  depth_iterator_baset &operator=(depth_iterator_baset &&other)
-  { m_stack=std::move(other.m_stack); }
+  {
+    m_stack=std::move(other.m_stack);


clang-format

Suggested change

m_stack=std::move(other.m_stack);

m_stack = std::move(other.m_stack);

hannes-steffenhagen-diffblue · 2020-04-20T10:36:19Z

src/ansi-c/CMakeLists.txt

+     converter_path)
+
+add_custom_command(OUTPUT "${cprover_library_path}"
+    COMMAND cat ${ansi_c_library_sources_paths} | ${converter_path} > ${cprover_library_path}


I'm afraid this doesn't quite work on windows (not on our CodeBuild machines here); We'd need Get-Content here or add a cat alias for Get-Content in the codebuild.

Frustratingly this isn't showing up as a failure in codebuild due to an unrelated bug in how that build is set up. I've been thinking of changing the build so it publishes the build log somewhere publicly visible at least, but I've note gotten around to that yet.

I'm not sure what to do here. The add_custom_command is not my contribution. My contribution is invocations of TO_NATIVE_PATH to get the right path separators on windows so the invocation of cat won't fail.

Is the issue that we are using different instances of cat? Maybe you are getting the cat that comes with cygwin that wants linux path separators and I am getting the cat that comes with the git shell that on windows wants windows path separators?

Personally, I think that if we get rid of cygwin completely and just build from the native command shell, that is the right way to go.

On our codebuild jobs we're actually building on powershell, not a cygwin environment. The TO_NATIVE_PATH actually shouldn't make a difference for the most part; All windows builtins I'm aware of understand POSIX path separators.

I think the natural thing to do is to build cbmc with the natural build environment on windows. I have been trying to get cbmc to build within the visual studio command prompt that is just cmd with all the paths set correctly to run visual studio. Visual studio comes with cmake and ninja. Visual studio can be installed with git and the git shell that gives you access to all the linux utilities you might need. I gave my procedure in the top comment of this pull request.

We can simulate this inside an ordinary cmd shell, just run the script vcvars64.bat to set up the environment variables as the visual studio command shell does.

Let's stop doing all this crazy stuff to cbmc to build, and just get it to build the right way in the native build environment.

This is exactly what we're already doing. https://github.com/diffblue/cbmc/blob/develop/buildspec-windows-cmake.yml

This is exactly what we're already doing. https://github.com/diffblue/cbmc/blob/develop/buildspec-windows-cmake.yml

Though, as far as I'm aware, this doesn't actually work? I believe this PR is a way towards making this work? Of course, we should discuss each individual change to see whether it's the right/best way to make things work.

hannes-steffenhagen-diffblue · 2020-04-21T09:16:39Z

src/ansi-c/CMakeLists.txt

-    COMMAND cat ${ansi_c_library_sources} | $<TARGET_FILE:converter> > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
-    DEPENDS converter ${ansi_c_library_sources})
+# Convert cmake paths to native paths for Windows builds
+file(TO_NATIVE_PATH "${ansi_c_library_sources}"


I don't think this really quite does what you want here; ansi_c_library_sources is a list not a single path. Also, without a second argument to store the result in this is just a no-op. The main problem with cat on windows isn't that it doesn't understand forward slashes as path separators, it's that it doesn't exist. On cygwin it'd work fine, but on powershell we'd need Get-Content and I'm not even sure what the right way to do this on cmd would be.

TBH I think the correct solution here would to be just scrap the cmake bits of this entirely and just change our file converter to read from files passed in as arguments rather than from STDIN, then we don't have to worry about cross platform quirkiness. I'll have a look at that today, then maybe this patch won't be necessary at all?

I may be abusing the semantics of TO_NATIVE_PATH, but the effect of this invocation is to replace the path separators. The second argument is in the second line below your comment.

I like the idea of scrapping cat. The cbmc project has been getting it from various ports of linux utilities. The cbmc build has traditionally been getting it from cygwin. I am trying to avoid cygwin, and I'm using the version that comes with the git shell that is part of the visual studio installation git installation. The problem is that different ports do different things with path separators.

Whatever you come up with, I'm going to apply the patch to the 5.12 distribution to build it. I'm trying to build distributions patches of 5.12 for the major repositories (homebrew, debian, windows). I'm trying to set up github actions to automate this for head versions.

tautschnig · 2020-04-21T14:17:23Z

@thk123 we had a conversation about this a few days ago - would you mind weighing in?

tautschnig · 2020-04-21T16:58:48Z

@markrtuttle @hannes-steffenhagen-diffblue How about the following approach:

The expr_iterator.h change should be a PR of its own, it seems non-controversial.
The converters learn to open a list of files rather than relying on cat/redirects? I'll put together a patch.

markrtuttle · 2020-04-21T17:50:48Z

Done. I'm closing this in favor of #5312 and #5313.

thk123 · 2020-04-22T13:38:28Z

FWIW I agree with @tautschnig here - don't rely on UNIX commands like cat in the build if it can be avoided so prefer #5314 to #5313

Fix cmake build from VS2019 command prompt

3d19eb5

markrtuttle requested review from chrisr-diffblue, kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners April 19, 2020 16:05

hannes-steffenhagen-diffblue reviewed Apr 20, 2020

View reviewed changes

Fix clang-format error.

4f76ac7

markrtuttle requested a review from hannes-steffenhagen-diffblue April 20, 2020 20:59

hannes-steffenhagen-diffblue reviewed Apr 21, 2020

View reviewed changes

markrtuttle requested a review from hannes-steffenhagen-diffblue April 21, 2020 12:23

markrtuttle closed this Apr 21, 2020

This was referenced Apr 22, 2020

Use native path separators to make cmake build under vs2019 work. #5313

Closed

Build system: make C string converters read files #5314

Merged

	m_stack=std::move(other.m_stack);
	m_stack = std::move(other.m_stack);

Fix cmake build from VS2019 command prompt #5306

Fix cmake build from VS2019 command prompt #5306

Uh oh!

Conversation

markrtuttle commented Apr 19, 2020

Uh oh!

hannes-steffenhagen-diffblue Apr 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Apr 21, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

markrtuttle Apr 21, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Apr 21, 2020

Uh oh!

tautschnig commented Apr 21, 2020

Uh oh!

markrtuttle commented Apr 21, 2020

Uh oh!

thk123 commented Apr 22, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

hannes-steffenhagen-diffblue Apr 20, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Apr 21, 2020 •

edited

Loading

markrtuttle Apr 21, 2020 •

edited

Loading