Compile cbmc with NDEBUG using gcc tool chain on linux.

[andreast271]

This will catch compilation and regression test failures caused
by -DNDEBUG.
The chance of an escape is sufficiently low, since compilation and
regression without -DNDEBUG are tested with clang.

Requesting a review from @thk123

[thk123]

My feeling is this should be a separate build since in general I don't think we've replaced all asserts with invariant (@peterschrammel may have an opinion on this).

[andreast271]

I didn't think a separate build was needed, since all assertions are checked in the clang build. Thus an escape would be an assertion that only fails with gcc, but not with clang. That scenario seemed sufficiently unlikely to me.

[peterschrammel]

The problem is that this build is run in the first stage, which should provide quick diagnostic information. A segfault there wouldn't provide useful information. Once all asserts have been replaced this problem would disappear, of course.

I am not quite sure what is the motivation for this change? Have you observed different behaviour w/wo NDEBUG?

[andreast271]

The motivation for the change is to ensure that compiling with -DNDEBUG does not get broken again. So there should be a build in the CI that checks this. That build could either be a new one, or the modification of an existing one. The PR does the latter, @thk123 suggested the former.

[martin-cs]

@andreast271 The issue isn't so much checking as it's things with side effects in asserts and / or INVARIANT et al. I'm not sure I'm so confident that you won't find difference between compilers; but maybe I'm just old an cynical.

I'm generally +1 super enthusiastic about -DNDEBUG not breaking things and testing it. Whether adding to an existing build or a new one; I'm not sure I care that much.

Can I request that we also have -DCPROVER_INVARIANT_DO_NOT_CHECK to prevent the "next generation" version of this problem as well.

[andreast271]

Building with -DCPROVER_INVARIANT_DO_NOT_CHECK is already broken. I have seen 6 different errors:

./std_types.h:143:3: error: must specify at least one argument for '...' parameter of variadic macro [-Werror,-Wgnu-zero-variadic-macro-arguments]

goto_symex_state.cpp:532:40: error: 'nullptr_exceptiont' does not refer to a
      value
  INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");

expr_util.cpp:37:16: error: unused variable 'type' [-Werror,-Wunused-variable]
  const typet &type=expr.type();

c_types.cpp:72:1: error: control may reach end of non-void function
      [-Werror,-Wreturn-type]

flattening/flatten_byte_operators.cpp:202:11: error: variable 'little_endian' is
      used uninitialized whenever 'if' condition is false
      [-Werror,-Wsometimes-uninitialized]
  else if(src.id()==ID_byte_extract_big_endian)
}

refinement/string_refinement.cpp:2076:13: error: unused function
      'is_valid_string_constraint' [-Werror,-Wunused-function]

I will suggest fixes for the first two errors in the next commit, and I'd like to hear suggestions about the other issues. Meanwhile in the travis build I will add -DCPROVER_INVARIANT_DO_NOT_CHECK and disable the specific warnings that cause compilation failures. The warnings can be re-enabled once the macros are fixed.

[tautschnig]

Suggestions for issues 3-6:
3. const typet &type=expr.type(); -> just use expr.type() in those PRECONDITION checks.
4. and 5.: Make the last else if an else and move the condition tested into the INVARIANT.
6. Surround the declaration and definition of is_valid_string_constraint by #ifndef NDEBUG.

[martin-cs]

I'm not quite sure what the changes to sharing tree have to do with this PR but ... sure?

[andreast271]

Unit tests did not compile with -DNDEBUG for the same reason as regular code. After fixing the files, the linter script complained about the missing copyright statement, so I fixed that as well.

[tautschnig]

Could that be placed in a separate commit? Not a big deal, but it seems like a change that should never get reverted even when others would.

[andreast271]

@tautschnig : you mean the changes to src/util/sharing_node.h and unit/sharing_node.cpp should be a separate commit, not just the copyright statement in unit/sharing_node.cpp. Correct?

[martin-cs]

@andreast271 The issue isn't so much checking as it's things with side effects in asserts and / or INVARIANT et al. I'm not sure I'm so confident that you won't find difference between compilers; but maybe I'm just old an cynical.

I'm generally +1 super enthusiastic about -DNDEBUG not breaking things and testing it. Whether adding to an existing build or a new one; I'm not sure I care that much.

Can I request that we also have -DCPROVER_INVARIANT_DO_NOT_CHECK to prevent the "next generation" version of this problem as well.

[andreast271]

Having the ellipsis in the macro definition results in a warning, and without defining INVARIANT_STRUCTURED compilation will always fail. How did this ever work?

[tautschnig]

Which warning would that be? It would be surprising that you are the first one to observe it?!

[andreast271]

I was surprised as well. See the discussion of the first commit.

[martin-cs]

I suspect it didn't. The structured invariant stuff was added after the initial invariant support and it may have simply not been tested. I don't recall reviewing it.

[tautschnig]

Could that be placed in a separate commit? Not a big deal, but it seems like a change that should never get reverted even when others would.

[tautschnig]

Have all the concerns about Travis being too slow been remedied in some way?

[andreast271]

@thk123 should answer this. I don't mind if the build with -NDEBUG -DCPROVER_INVARIANT_DO_NOT_CHECK is done by adding a new build or modifying an existing one. It is very clear, however, that such a build is needed.

[andreast271]

I've split the PR into two as suggested by @tautschnig. The other PR is #1536 and enables compilation with clang++ -DNDEBUG.
This PR creates a new travis build with clang++ -DNDEBUG -DCPROVER_INVARIANT_DO_NOT_CHECK, and contains a quick fix to invariant.h to enable that build. It also disables some warnings that would cause a build failure. Fixing all these warnings by changing the source code is out of scope for this PR, but I would welcome ideas on how to change the INVARIANT macro such that the warnings are not triggered.

[andreast271]

On reflection the current version of the PR is pointless: the new build disables warnings, and the goal of the PR is to make sure that no-debug builds succeed without warnings. I still don't see how to achieve that for CPROVER_INVARIANT_DO_NOT_CHECK with reasonable effort. One option is to add a build with NDEBUG for now, and raise the problem of compilation with CPROVER_INVARIANT_DO_NOT_CHECK as an issue.

[andreast271]

I removed the extra build that compiled with NDEBUG without running regression, and added NDEBUG to an existing linux/clang build.
Motivation: The CI builds should aim to cover pairwise combinations of OS / compiler / build system / flags. For example, the cmake builds could do double-duty by checking some of the clang/flags combinations instead of using the standard gcc build.

[tautschnig]

@martin-cs Are you happy with this one?

[martin-cs]

Sorry for being out-of-the-loop on this one. My understanding of the current state of this patch is that it:

1. Adds NDEBUG but not CPROVER_INVARIANT_DO_NOT_CHECK to the Ubuntu / clang build.

2. Fixes the issue of INVARIANT_STRUCTURED not compiling with CPROVER_INVARIANT_DO_NOT_CHECK .

I believe both of these to be correctly implemented and useful. I'm not sure I fully understand why CPROVER_INVARIANT_DO_NOT_CHECK is omitted but I'm happy that, if there are build problems with that, they are raised as another PR.

[martin-cs]

Let's go for it!

[martin-cs]

"Structured Invariant" might be a tad better but ... only if you are editing anyway.

[martin-cs]

I suspect it didn't. The structured invariant stuff was added after the initial invariant support and it may have simply not been tested. I don't recall reviewing it.

[martin-cs]

Ping @kroening and @forejtv please can we have this merged?