Deactivate broken tests that depend on assert on MacOS. #5541

NlightNFotis · 2020-11-02T14:10:19Z

The reason we are deactivating the tests is that there
was a change to the assert.h header under MacOS that
makes it now include some other C++ headers which include
type_traits causing template errors that have broken
CI under that platform.

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.
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).
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.

hannes-steffenhagen-diffblue · 2020-11-02T14:25:44Z

regression/ansi-c/CMakeLists.txt

+    )
+elseif("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+    add_test_pl_tests(
+        "$<TARGET_FILE:goto-cc>" -X mac-frontend-broken


These changes need to go in the Makefile too

‘mac-frontend-broken’ is a bad name. What’s broken about the frontend? Which frontend are we even talking about? In fact this is basically a lie, the C++ frontend on mac isn’t more broken than anywhere else.

martin-cs

I'm a bit concerned by this. assert.h is a C header and should not be including C++. The C++ header should be cassert. If assert.h doesn't work on Mac then I doubt the tool will be usable at all on Mac. Are you sure about this? If it is really a problem with assert.h it should break hundreds of regression tests, not just three.

codecov · 2020-11-02T14:49:10Z

Codecov Report

Merging #5541 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5541   +/-   ##
========================================
  Coverage    68.52%   68.52%           
========================================
  Files         1187     1187           
  Lines        98265    98265           
========================================
  Hits         67339    67339           
  Misses       30926    30926

Flag	Coverage Δ
cproversmt2	`42.96% <ø> (ø)`
regression	`65.68% <ø> (ø)`
unit	`32.26% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out 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 a46f12d...7a8c427. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-11-02T14:52:01Z

@martin-cs Basically what’s happening is that assert.h has something along the lines of

#ifdef __cplusplus
#include <type_traits>
#define assert(cond) some fancy thing that probably allows for better error reporting or whatever
#else
#define assert(cond) the normal/straightforward way
#endif

A lot of standard libraries just have their cassert header consist of #include "assert.h"

here’s the full text of my cassert header for instance:

// -*- C++ -*- forwarding header.

// Copyright (C) 1997-2020 Free Software Foundation, Inc.
//
// This file is part of the GNU ISO C++ Library.  This library is free
// software; you can redistribute it and/or modify it under the
// terms of the GNU General Public License as published by the
// Free Software Foundation; either version 3, or (at your option)
// any later version.

// This library is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.

// Under Section 7 of GPL version 3, you are granted additional
// permissions described in the GCC Runtime Library Exception, version
// 3.1, as published by the Free Software Foundation.

// You should have received a copy of the GNU General Public License and
// a copy of the GCC Runtime Library Exception along with this program;
// see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see
// <http://www.gnu.org/licenses/>.

/** @file cassert
 *  This is a Standard C++ Library file.  You should @c \#include this file
 *  in your programs, rather than any of the @a *.h implementation files.
 *
 *  This is the C++ version of the Standard C Library header @c assert.h,
 *  and its contents are (mostly) the same as that header, but are all
 *  contained in the namespace @c std (except for names which are defined
 *  as macros in C).
 */

//
// ISO C++ 14882: 19.2  Assertions
//

// No include guards on this header...

#pragma GCC system_header

#include <bits/c++config.h>
#include <assert.h>

and handle all the language differing logic (if any) there (libstdc++ also has some C++ specific logic in there, but apparently nothing that trips up the C++ frontend – note that on Mac the default is libc++, not libstdc++ though). As long as you don’t try to compile with -x c++ there’s no problem.

martin-cs · 2020-11-02T15:02:53Z

OK... but then why are these tests, in ansi-c being compiled with the C++ flag? I've had a look an these are not C++ tests. Please look into this more deeply and fix a different way. Just disabling tests is not a solution.

martin-cs · 2020-11-02T15:03:55Z

Also, while I am at it, @NlightNFotis the code coverage is broken. I remember commenting on this when you were changing the CI infrastructure and you said it was temporary and would go away. It hasn't. Please can you fix it?

hannes-steffenhagen-diffblue · 2020-11-02T15:09:22Z

OK... but then why are these tests, in ansi-c being compiled with the C++ flag?

The reason seems to be related to something @tautschnig did in 2019, apparently the idea was that these tests should also pass if the C++ frontend is used to compile them. I think perhaps a better way would be to move them over to the C++ frontend tests, please note that this is currently blocking our CI (and thus everything) though. The correct solution here is going to involve disabling these tests on macOS or deleting them (for C++, not for C!) though, as the reason they’re broken is not a regression – it’s just that the C++ frontend is flaky.

martin-cs · 2020-11-02T15:13:14Z

They are not C++ tests! Have a look at them! The correct fix is to work out why they are being compiled as C++ and have them compiled as C instead.

hannes-steffenhagen-diffblue · 2020-11-02T15:14:12Z

They are not C++ tests! Have a look at them! The correct fix is to work out why they are being compiled as C++ and have them compiled as C instead.

They are compiled as C++ because they are tagged as "this should be compiled with C++". Take a look at 723620d

Basically what this commit did was it changed the C tests so they would be tested with both the C and the C++ frontend, the idea being that most C tests should also work for a C++ frontend. Whether or not that’s a good idea is neither here nor there, but that’s what’s causing the issue we have right now.

martin-cs · 2020-11-02T15:28:18Z

This raises more questions than it answers...

Why is it only these three that cause issues? Why not the others?
Why are the rest of the C++ tests passing on Mac?
This should be run as C++ as well as being run as C.

If assert.h on Mac is broken when compiled as C++ then I am fine disabling the testing of the C++ front-end on Mac as a solution.

thomasspriggs · 2020-11-02T16:12:20Z

They are not C++ tests! Have a look at them! The correct fix is to work out why they are being compiled as C++ and have them compiled as C instead.

My understanding is that these tests are run as both C and C++ tests. They are C tests which are also used to check the C++ front-end's compatibility with C code. The problem is that the latest Mac versions of assert.h are detecting that they are being used by a C++ front end and then using C++ features, which we don't support.

martin-cs · 2020-11-02T16:39:18Z

@thomasspriggs Thanks. Do you know why this is not affecting other C++ tests, like the ones in cpp or cbmc-cpp?

hannes-steffenhagen-diffblue · 2020-11-02T16:41:36Z

Why is it only these three that cause issues? Why not the others?

I’ve not looked at all of the other tests for which C++ testing is enabled but none of the ones I looked at that aren’t disabled by this PR include assert.h.

Why are the rest of the C++ tests passing on Mac?

Now that’s an excellent question. For the most part it seems the C++ tests also don’t use assertions, but it’s possible the ansi-c tests (C++ version) are somehow treated slightly differently than the C++ proper tests.

martin-cs · 2020-11-02T17:30:05Z

On Mon, 2020-11-02 at 08:41 -0800, hannes-steffenhagen-diffblue wrote: > Why is it only these three that cause issues? Why not the others? I’ve not looked at _all_ of the other tests for which C++ testing is enabled but none of the ones I looked at that aren’t disabled by this PR include `assert.h`.

Right; that seems like a good answer.

> Why are the rest of the C++ tests passing on Mac? Now that’s an excellent question. For the most part it seems the C++ tests also don’t use assertions, but it’s possible the ansi-c tests (C++ version) are somehow treated slightly differently than the C++ proper tests.

Many don't but enough do to make this concerning. $ find ../regression/ -name '*.cpp' -print | wc -l 405 $ find ../regression/ -name '*.cpp' -exec grep '<assert.h>' {} \; | wc -l 11 $ find ../regression/ -name '*.cpp' -exec grep '<cassert>' {} \; | wc -l 49 I don't get why these don't break as well? ../regression/cbmc-cpp/MethodParam1/main.cpp #include <assert.h> assert(x<4); assert(x<5); ../regression/cbmc-cpp/lvalue1/main.cpp #include <cassert> assert(a == ASD); assert(a == ABC);

NlightNFotis · 2020-11-02T18:55:29Z

One thing to note here is that you are right @martin-cs, more tests are broken than the ones excluded here. I'm in the process of excluding them as well.

NlightNFotis · 2020-11-02T19:10:50Z

Right, so now there should be a lot more tests excluded, which should paint a more accurate picture of what was broken.

There might be one or two missing, but I'm waiting CI to see what's being reported and fix it later.

martin-cs · 2020-11-03T15:55:30Z

Thanks @NlightNFotis this is starting to look like something that will actually fix the problem. One more thing; please could you add a comment, to the Makefiles or to the test cases, explaining what is broken and why.

regression/ansi-c/CMakeLists.txt

thomasspriggs · 2020-11-03T18:49:43Z

regression/ansi-c/Makefile

 endif

 tests.log: ../test.pl
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(exclude_mac_broken_tests)


🚫 Likewise, I thought that the C tests were still fine on mac?

The reason we are deactivating the tests is that there was a change to the `assert.h` header under MacOS that makes it now include some other C++ headers which include `type_traits` causing template errors that have broken CI under that platform.

martin-cs

This seems more consistent and understandable. Thanks for the discussion and extra work on sorting this out, I think it has really improved it.

NlightNFotis self-assigned this Nov 2, 2020

thomasspriggs approved these changes Nov 2, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Nov 2, 2020

View reviewed changes

martin-cs reviewed Nov 2, 2020

View reviewed changes

NlightNFotis force-pushed the fix_mac_ci branch from 2247dcb to caf24ec Compare November 2, 2020 19:09

NlightNFotis force-pushed the fix_mac_ci branch from caf24ec to 711530a Compare November 3, 2020 00:32

NlightNFotis changed the title ~~Deactivate three broken tests on MacOS.~~ Deactivate broken tests that depend on assert on MacOS. Nov 3, 2020

NlightNFotis force-pushed the fix_mac_ci branch from 711530a to 30888f2 Compare November 3, 2020 11:43

thomasspriggs reviewed Nov 3, 2020

View reviewed changes

NlightNFotis force-pushed the fix_mac_ci branch 5 times, most recently from 2e3aa6b to b4b47cd Compare November 5, 2020 19:56

martin-cs mentioned this pull request Nov 6, 2020

Disable C regression tests with C++ front-end when assert.h is used #5545

Closed

3 tasks

tautschnig approved these changes Nov 6, 2020

View reviewed changes

NlightNFotis force-pushed the fix_mac_ci branch from b4b47cd to 7a8c427 Compare November 6, 2020 11:06

martin-cs approved these changes Nov 6, 2020

View reviewed changes

NlightNFotis merged commit fa4569e into diffblue:develop Nov 6, 2020

NlightNFotis deleted the fix_mac_ci branch November 6, 2020 13:08

thomasspriggs mentioned this pull request Nov 9, 2020

Dummy PR to check CI #5540

Closed

Deactivate broken tests that depend on assert on MacOS. #5541

Deactivate broken tests that depend on assert on MacOS. #5541

Uh oh!

Conversation

NlightNFotis commented Nov 2, 2020

Uh oh!

hannes-steffenhagen-diffblue Nov 2, 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!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

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

Uh oh!

Uh oh!

martin-cs commented Nov 2, 2020

Uh oh!

martin-cs commented Nov 2, 2020

Uh oh!

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

Uh oh!

Uh oh!

martin-cs commented Nov 2, 2020

Uh oh!

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

Uh oh!

Uh oh!

martin-cs commented Nov 2, 2020

Uh oh!

thomasspriggs commented Nov 2, 2020

Uh oh!

martin-cs commented Nov 2, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Nov 2, 2020

Uh oh!

martin-cs commented Nov 2, 2020 via email

Uh oh!

NlightNFotis commented Nov 2, 2020

Uh oh!

NlightNFotis commented Nov 2, 2020

Uh oh!

martin-cs commented Nov 3, 2020

Uh oh!

Uh oh!

thomasspriggs Nov 3, 2020

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue Nov 2, 2020 •

edited

Loading

codecov bot commented Nov 2, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Nov 2, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Nov 2, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Nov 2, 2020 •

edited

Loading