Fix CPP models when using CMake Build #5285

thk123 · 2020-04-01T10:35:01Z

In trying to track down why the defines don't work in the library, I discovered that the cpp models (that includes definitions for new) do not work on CMake builds. I'm working on a fix, but just to confirm my suspicion I've added a test that I believe will pass on non-cmake builds but will fail on cmake builds.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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).
[na] 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.

codecov-io · 2020-04-01T14:23:05Z

Codecov Report

Merging #5285 into develop will increase coverage by 0.43%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5285      +/-   ##
===========================================
+ Coverage    67.51%   67.95%   +0.43%     
===========================================
  Files         1170     1170              
  Lines        96338    96338              
===========================================
+ Hits         65044    65464     +420     
+ Misses       31294    30874     -420

Flag	Coverage Δ
#cproversmt2	`42.40% <100.00%> (ø)`
#regression	`64.46% <100.00%> (+0.43%)`	⬆️
#unit	`31.76% <0.00%> (ø)`

Impacted Files	Coverage Δ
src/ansi-c/cprover_library.cpp	`96.42% <100.00%> (+3.57%)`	⬆️
src/util/config.cpp	`56.66% <0.00%> (+0.17%)`	⬆️
src/cpp/parse.cpp	`68.59% <0.00%> (+0.41%)`	⬆️
src/linking/linking.cpp	`56.93% <0.00%> (+0.63%)`	⬆️
src/ansi-c/c_typecheck_expr.cpp	`74.92% <0.00%> (+0.74%)`	⬆️
src/cbmc/cbmc_parse_options.cpp	`76.76% <0.00%> (+0.93%)`	⬆️
src/goto-programs/string_instrumentation.cpp	`11.41% <0.00%> (+11.41%)`	⬆️
src/cpp/cpp_token_buffer.cpp	`77.55% <0.00%> (+12.24%)`	⬆️
src/goto-programs/pointer_arithmetic.cpp	`50.00% <0.00%> (+50.00%)`	⬆️
... and 2 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 ca8c1a9...29a481a. Read the comment docs.

thk123 · 2020-04-01T17:30:23Z

This PR shouldn't pass:

the cpp new test should fail on all cmake builds
the string abstraction tests should also fail on cmake builds

The reason is the cmake file for the cpp folder does not add the dependency so the cprover_library.inc file is never generated, which means only the C library is imported, but it is imported without the ability to turn string abstraction on. I have a fix for the CMake which I'll apply once this is failing CI.

The CI isn't failing:

the windows cmake build bases regardless of build outcome (and has done since the start)
the linux gcc cmake build has disappeared from the checks

Therefore we have no CI for CMake builds 😭

thk123 · 2020-04-02T13:07:05Z

Rebased on top of #5287 to ensure the cbmc-linux-cmake-gcc job now fails.

thk123 · 2020-04-02T13:38:56Z

Confirmed both the cpp-new test (no model for __new) and the string-abstraction tests are failing as expected on CMake job. And indeed CI fails 🎉

when linking the cprover library. The default mode for this constructor of stringstream is to over-write the string used in construction, which presumably was not the intention here. Note: until now there wasn't anything too interesting in the prologue except for the string-abstraction define, which was ignored. But we might want more defines in the future.

Currently the CPP library is not built in cmake builds

This checks the body of goto functions whose implementation depends on whether the string abstraction macro is defined.

This ensures that the library is actually built (and therefore used) by the C++ frontend (otherwise, the CMake version never genreates cprover_library.inc and the C version of the file is imported twice. Also mirrored the changes made in the ansi-c CMakeLists.txt which detects changes in the source of the library

thk123 · 2020-04-02T14:22:25Z

Now added commit that should fix the tests for the CMake build
@smowton a review of the last commit (that actually fixes the problem) would be useful.

smowton · 2020-04-02T15:15:37Z

Write -> append? Seen it already, LGTM

thk123 · 2020-04-02T15:53:29Z

Ah sorry @smowton, I think you're looking at the wrong commit, I added this commit to fix the cmake file: 9c5a5c4

smowton · 2020-04-02T16:24:23Z

Also looks sane except nitpick above

thk123 · 2020-04-03T09:29:56Z

@smowton in this case though ${cpp_library_sources} is the result of file(GLOB cpp_library_sources "library/*.c") which is a list of files, I think you need to use cat to join them together? That said - this doesn't (and didn't) work on the Windows CMake build - so an alternative to cat will be needed in a subsequent PR.

smowton · 2020-04-03T09:31:35Z

Doh right, sorry

hannes-steffenhagen-diffblue · 2020-04-03T10:07:22Z

src/cpp/CMakeLists.txt

+        ${sources}
+        PROPERTIES
+        OBJECT_DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+)


This should just be add_dependencies(cpp "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc") I think?

Copied from ansi-c, will try updating both.

This doesn't work:

CMake Error at src/cpp/CMakeLists.txt:30 (add_dependencies): The dependency target "/home/tkiley/workspace/cbmc/build/debug/src/cpp/cprover_library.inc" of target "cpp" does not exist.

You're more than welcome to raise a follow up PR making this nicer, but I'd rather just merge this as is, rather than spend more time on it, since it does fix the problem of the C++ library and macros in the C library not working on CMake.

thk123 requested review from chrisr-diffblue, kroening and tautschnig as code owners April 1, 2020 10:35

thk123 force-pushed the cpp-new-cmake branch 2 times, most recently from 4cbefcb to 29a481a Compare April 1, 2020 13:26

thk123 force-pushed the cpp-new-cmake branch from 29a481a to 58734c9 Compare April 1, 2020 16:57

thk123 force-pushed the cpp-new-cmake branch 2 times, most recently from b294b47 to c8cdb19 Compare April 2, 2020 13:06

thk123 requested review from peterschrammel and smowton as code owners April 2, 2020 13:06

thk123 added the dependent - do not merge label Apr 2, 2020

smowton approved these changes Apr 2, 2020

View reviewed changes

petr-bauch and others added 4 commits April 2, 2020 15:21

Add test for the new operator

3abc5db

Currently the CPP library is not built in cmake builds

Add test verifying that the string abstraction is enabled

64f1c3d

This checks the body of goto functions whose implementation depends on whether the string abstraction macro is defined.

thk123 force-pushed the cpp-new-cmake branch from c8cdb19 to 9c5a5c4 Compare April 2, 2020 14:21

thk123 changed the title ~~Cpp new cmake~~ Fix CPP models when using CMake Build Apr 2, 2020

thk123 removed the dependent - do not merge label Apr 2, 2020

thk123 requested a review from hannes-steffenhagen-diffblue April 3, 2020 09:28

hannes-steffenhagen-diffblue reviewed Apr 3, 2020

View reviewed changes

tautschnig approved these changes Apr 4, 2020

View reviewed changes

tautschnig merged commit e4c80a5 into diffblue:develop Apr 4, 2020

thk123 mentioned this pull request Apr 9, 2020

Fix over-writing library prologue #5244

Closed

7 tasks

thk123 deleted the cpp-new-cmake branch April 9, 2020 11:23

Fix CPP models when using CMake Build #5285

Fix CPP models when using CMake Build #5285

Uh oh!

Conversation

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

Uh oh!

Uh oh!

codecov-io commented Apr 1, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

thk123 commented Apr 1, 2020

Uh oh!

thk123 commented Apr 2, 2020

Uh oh!

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

Uh oh!

Uh oh!

thk123 commented Apr 2, 2020

Uh oh!

smowton commented Apr 2, 2020

Uh oh!

thk123 commented Apr 2, 2020

Uh oh!

smowton commented Apr 2, 2020

Uh oh!

thk123 commented Apr 3, 2020

Uh oh!

smowton commented Apr 3, 2020

Uh oh!

hannes-steffenhagen-diffblue Apr 3, 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!

thk123 Apr 3, 2020

Choose a reason for hiding this comment

Uh oh!

thk123 Apr 3, 2020

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

thk123 commented Apr 1, 2020 •

edited

Loading

codecov-io commented Apr 1, 2020 •

edited

Loading

thk123 commented Apr 2, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Apr 3, 2020 •

edited

Loading