Skip to content

Fix cmake build from VS2019 command prompt #5306

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
markrtuttle wants to merge 2 commits into from
Closed

Fix cmake build from VS2019 command prompt #5306

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3d19eb5
Fix cmake build from VS2019 command prompt
Apr 19, 2020
4f76ac7
Fix clang-format error.
Apr 20, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 11 additions & 3 deletions src/ansi-c/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,17 @@ add_executable(converter library/converter.cpp)

file(GLOB ansi_c_library_sources "library/*.c")

add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
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}"
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Apr 21, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

@markrtuttle markrtuttle Apr 21, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

ansi_c_library_sources_paths)
file(TO_NATIVE_PATH "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
cprover_library_path)
file(TO_NATIVE_PATH "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/converter"
converter_path)

add_custom_command(OUTPUT "${cprover_library_path}"
COMMAND cat ${ansi_c_library_sources_paths} | ${converter_path} > ${cprover_library_path}
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Apr 20, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

@markrtuttle markrtuttle Apr 20, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Apr 21, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

@markrtuttle markrtuttle Apr 21, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Apr 21, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

@tautschnig tautschnig Apr 21, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

DEPENDS converter ${ansi_c_library_sources_paths})

add_executable(file_converter file_converter.cpp)

Expand Down
14 changes: 11 additions & 3 deletions src/cpp/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,16 @@
file(GLOB cpp_library_sources "library/*.c")

add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
COMMAND cat ${cpp_library_sources} | $<TARGET_FILE:converter> > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
DEPENDS converter ${cpp_library_sources})
# Convert cmake paths to native paths for Windows builds
file(TO_NATIVE_PATH "${cpp_library_sources}"
cpp_library_sources_paths)
file(TO_NATIVE_PATH "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
cprover_library_path)
file(TO_NATIVE_PATH "${CMAKE_RUNTIME_OUTPUT_DIRECTORY}/converter"
converter_path)

add_custom_command(OUTPUT "${cprover_library_path}"
COMMAND cat ${cpp_library_sources_paths} | "${converter_path}" > "${cprover_library_path}"
DEPENDS converter ${cpp_library_sources_paths})

################################################################################

Expand Down
5 changes: 4 additions & 1 deletion src/util/expr_iterator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,10 @@ class depth_iterator_baset
{ m_stack=std::move(other.m_stack); }
depth_iterator_baset &operator=(const depth_iterator_baset&)=default;
depth_iterator_baset &operator=(depth_iterator_baset &&other)
{ m_stack=std::move(other.m_stack); }
{
m_stack = std::move(other.m_stack);
return *this;
}

const exprt &get_root()
{
Expand Down