C++ front end fixes [blocks: #2554] #1260

tautschnig · 2017-08-21T15:36:43Z

This is a series of fixes mainly compiled by @peterschrammel plus some additional work of mine.

This includes the following commits to be reviewed:

tautschnig · 2017-08-21T16:42:47Z

I will need to make the linter happy and figure out how to support the Visual Studio-provided syntax.

andreast271 · 2017-09-29T17:01:03Z

I am currently looking at the failing checks. I fixed the linter complaints outside of regression, but there will be new ones, because assert() must be replaced by INVARIANT or one of its derivatives.
There are also 9 failing regression tests, all in the cpp directory, and all with the same error message. I plan to look at that next week, using branch peterschrammel:systemc as baseline, since at least one of the test is not failing on peterschrammel:systemc.

andreast271 · 2017-09-29T17:03:42Z

I have a fix for the compilation errors with that happen with -DDEBUG.

martin-cs · 2017-10-02T08:18:29Z

@andreast271 ( and @tautschnig and @peterschrammel ) thank you for looking at this; this is incredibly valuable work.

andreast271 · 2017-10-03T08:00:15Z

src/cpp/parse.cpp

+      merge_types(attr, t);
+      break;
+    }
+


This creates a merged type with op0 = function_type, op1 = noreturn.
Is that intended? Typecheck code assumes that following subtypes uses the back of the list for merged types. Here this would be the noreturn node, which seems odd.
Adding the noreturn attribute in this way will currently cause an assertion failure in cpp_declaratort::merge_type for regression test cases that #include assert.h.
Even after a fix in cpp_declaratort::merge_type the type would then fail to typecheck in cpp_convert_plain_type(typet &type)
I'm happy to work on fix after getting an explanation of the intended use of merged_type in C++ frontend.

I believe I had tried to mimic what the C front-end does. The obvious fix would be to swap the parameters here, but I'm not sure this will result in the attribute being picked up at all?

Where should the attribute end up after type checking? At some point function_type is converted to code_type. At that stage the type qualifiers need to be put somewhere in the code_type node. I didn't see anything in the C++ front end that does that, so right now cpp_convert_plain_type fails because it cannot deal with a qualifier of a function type. I could fix it if I understood how the result of type checking the function should look like.

The merge_types function in the C and C++ front end use a different convention for the order of arguments: in the C front end, it is merge_types(dest, src), while in C++ it is merge_types(src, dest). A possible fix would then be to change the merge_types function in C++ so that it adds the new type at the front of the subtypes (or rather anywhere but at the end). Thoughts?

Changing the merge_types functions seems to work. Regression passes and I also have a fix for the -DDEBUG compilation failures and some of the linter issues. What is the process for gettings these fixes into the PR?

Could you check whether you are able to push to my branch? If you aren't, you can certainly create a pull request in my fork (against that branch), and as soon as I merge it the changes will show up here.

andreast271

Even with these changes C++ is not fully supported yet (not even C++-98). However, the known problematic areas are clearly documented in the code.

peterschrammel · 2017-10-27T16:18:38Z

This would need rebasing...

tautschnig · 2017-10-27T16:44:40Z

Rebase done.

andreast271 · 2017-10-30T08:09:02Z

The linter failures are all from cpp files in the regression. I discussed this with @thk123 a while ago. He agreed that the linter shouldn't run on regression test sources, and also clarified that linter failures do not prevent a merge. IMO the correct fix is to change the linter so that it skips the regression directory, but that should be a separate PR.

andreast271 · 2017-10-30T08:54:41Z

Prefix: I have given up on supporting VS headers in cbmc. I compile cbmc on Windows with VisualStudio (not just the compiler, but the IDE), but even then I run under cygwin using --gcc --cpp98, so that preprocessing is done by gcc using -std=c++98. Everything else fails as soon as I include a system header file.

There are 5 test failures in the cpp group on windows reported by the appveyor build:

Function_Overloading2. This is a KNOWNBUG in develop, so it never ran on windows, so it's not a regression. Solution: remove test from appveyor build
Function_Overloading3. This is a new test, so it never ran on windows, so it's not a regression. Solution: remove test from appveyor build.
to 5. Resolver10, Resolver11, Template_Parameters1: These tests were changed to #include <cassert> in main.cpp. This causes failures on windows - see Prefix above re. VS headers. Solution: since the test sources don't actually contain any assertions, revert the changes.

@tautschnig : I can create a PR to tautschnig/c++-front-end-fixes with the suggested solutions if you agree with them.

smowton

A few style comments. I won't approve since I don't know nearly enough about the C++ front-end.

smowton · 2017-10-30T09:48:03Z

src/cpp/cpp_typecheck_declaration.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]

 \********************************************************************/

+


smowton · 2017-10-30T10:10:04Z

src/cpp/cpp_typecheck_method_bodies.cpp

+
+  // We have to prevent the same method to be added multiple times
+  //   otherwise we get duplicated symbol prefixes
+  if(methods_seen.find(_method_symbol->name) != methods_seen.end())


Use insert and check its return value rather than find-then-insert double-lookup

smowton · 2017-10-30T10:12:14Z

src/cpp/cpp_typecheck_resolve.cpp

-        it1!=identifiers.end();
+    for(resolve_identifierst::const_iterator
+        it1=old_identifiers.begin();
+        it1!=old_identifiers.end();
        it1++)


Might as well switch to pre-increment while we're changing things here

smowton · 2017-10-30T14:41:10Z

src/cpp/cpp_typecheck_resolve.cpp

        it1++)
    {
+#if 0


ifdef DEBUG?

smowton · 2017-10-30T14:46:29Z

src/cpp/parse.cpp

+    // since several analysis functions traverse via the end for
+    // merged_types
+    typet::subtypest &sub=dest.subtypes();
+    sub.emplace(sub.begin(), src);


Might as well use insert, since emplace is just calling a copy-constructor itself here plus doing some mildly-costly (in my experience) gymnastics to avoid copying the argument in the meantime

smowton · 2017-10-30T14:48:28Z

src/goto-programs/goto_convert_functions.cpp

@@ -1,4 +1,4 @@
-/**** ***************************************************************\
+/********************************************************************\


Accidental change?

No: 03c9894 ("Fix broken comment frame", 2017-07-31)

thk123

Got to commit: "C++ front-end: parse GCC attributes"

Since the changes come from a range of people, I have tagged the comments with who the commit was introduced by. I don't know if it is easier for you to apply them all @tautschnig or for the relevant people to apply the changes (in particular the comments).

I also should flag up I've not made an attempt to deeply understand the C++ parsing so cannot verify that the code is reasonable or that the tests are sufficient.

thk123 · 2017-10-31T13:06:50Z

regression/cpp/Apple_extensions1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG


If there isn't already, could you raise an issue and add it as a comment at the bottom of test.desc ( @tautschnig )

thk123 · 2017-10-31T13:07:41Z

regression/cpp/Template_Specialisation2/main.ii

@@ -15,3 +15,6 @@ struct __member_pointer_traits_imp<_Rp (_Class::*)() const>
 {
 };

+int main(int argc, char* argv[])


Should this become main.cpp as with the other file ( @tautschnig )

I don't know -- there isn't really enough information in the initial commit message for that file (e155e42), so I'd suggest to leave it as is. It should not have any impact. Should.

thk123 · 2017-10-31T13:08:57Z

src/cpp/cpp_constructor.cpp

@@ -47,12 +47,16 @@ codet cpp_typecheckt::cpp_constructor(
    // The purpose of the tag #array_ini is to rule out ill-formed
    // programs.

+    // TODO: in a program it is not allowed, but the implementation of the


I don't think this comment is very clear ( @peterschrammel )

De/activating this code has no effect on cpp and systemc regression tests. We should remove this change from this PR.

I have removed the commit "Deactivate internal array initializer".

thk123 · 2017-10-31T13:09:31Z

src/cpp/cpp_declarator_converter.cpp

@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]

 #include "cpp_declarator_converter.h"

+//#define DEBUG


Nit: don't check this line in ( @peterschrammel )

thk123 · 2017-10-31T13:10:09Z

src/cpp/cpp_declarator_converter.cpp

@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]

 #include "cpp_declarator_converter.h"

+//#define DEBUG
+
+#ifdef DEBUG


Possibly this is just ending up in the wrong commit - but we don't seem to use iostream in this cpp. ( @peterschrammel )

thk123 · 2017-10-31T13:20:44Z

src/cpp/cpp_typecheck_method_bodies.cpp

@@ -9,19 +9,30 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// C++ Language Type Checking

+//#define DEBUG


Nit: don't check this in ( @peterschrammel )

thk123 · 2017-10-31T13:25:20Z

src/cpp/cpp_typecheck_resolve.cpp

@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]

 #include "cpp_typecheck_resolve.h"

+//#define DEBUG


Nit: don't check in ( @peterschrammel )

thk123 · 2017-10-31T13:26:58Z

src/cpp/cpp_typecheck.cpp

+{
+  if(expr.id()==ID_cpp_name)
+    return true;
+  forall_operands(it, expr)


Nit: can you use a range based for loop here? Also since for loop extends over multiple lines please wrap in braces

Done in PR #6

thk123 · 2017-10-31T13:27:40Z

src/cpp/cpp_typecheck_resolve.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]

 #include "cpp_typecheck_resolve.h"

-//#define DEBUG
+// #define DEBUG


Nit: remove this line ( @peterschrammel )

thk123 · 2017-10-31T13:28:42Z

src/cpp/cpp_typecheck_resolve.cpp

-          identifiers.begin();
-          it2!=identifiers.end();
-          ) // no it2++
+      for(resolve_identifierst::const_iterator it2=it1+1;


Nit: giving these iterators meaningful names might make this code a bit easier to follow

thk123 · 2017-10-31T13:32:11Z

Did review commit by commit, so might still be worth checking the comments that are now out-dated, but they may be fixed in later commits

tautschnig · 2017-12-04T09:35:24Z

@andreast271 I've addressed the remaining concerns voiced by @thk123. I believe this would not warrant a final (?) review by @peterschrammel and should then be merged. There is of course a lot of work left to be done in this front-end...

thk123

Mostly minor suggestions (and I should stress I am not familiar with this code), but looks good. Main thing I'd like to see if the tests for the attribute support if they don't already exist.

thk123 · 2017-12-04T11:19:13Z

regression/cpp/gcc_vector1/main.cpp

+
+#else
+
+void setzero()


How come we're only testing on GNUC?

I have no idea whether Visual Studio supports (the same) vector types?

MSVC doesn't support the vector_size attribute. It does have 128-bit data types. However, these are defined in header files, and the cbmc C++ front end cannot parse MSVC C++ header files.

Is the syntax to use them the same as with GCC/Clang? Would you actually be able to contribute a KNOWNBUG regression test that uses them?

The existing testcase uses the typedef for __m128 from the xmmintrin.h header files that ships with gcc. I can do the same for MSVC and add that to the existing test case in a separate PR (after this one is merged). There is an interesting problem, though: CBMC with PARSER.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO accepts the syntax of the test case, but the MSVC compiler does not: it complains that error C4576: a parenthesized type followed by an initializer list is a non-standard explicit type conversion syntax
Should cbmc in this case follow MSVC and report a parser error?

It would be desirable if the CBMC front-end mimicked exactly what MSVC does, but that's surely not of the highest priority.

thk123 · 2017-12-04T11:19:59Z

src/cpp/parse.cpp

@@ -4401,6 +4401,16 @@ bool Parser::rClassSpec(typet &spec)
  {
    if(!optAlignas(spec))
      return false;
+
+    if(lex.LookAhead(0)==TOK_GCC_ATTRIBUTE)


I don't know what this means exactly, but it would probably make sense to have some tests off GCC attributes after struct/class declarations.

I'll try to dig up with those tests were: we do have them already, otherwise the change wouldn't have happened :-) - but then it might be rather implicit in that it's drawn in from system headers.

thk123 · 2017-12-04T11:24:49Z

regression/cbmc/cpp1/test.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring


Link to the issue would be great

thk123 · 2017-12-04T11:25:20Z

regression/cbmc/cpp2/test.desc

+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^equality without matching types


Nit: Link to the issue

thk123 · 2017-12-04T11:28:02Z

src/cpp/cpp_convert_type.cpp

@@ -130,6 +130,10 @@ void cpp_convert_typet::read_rec(const typet &type)
    constexpr_cnt++;
  else if(type.id()==ID_extern)
    extern_cnt++;
+  else if(type.id()==ID_noreturn)
+  {
+    noreturn_cnt++;


Nit: prefer prefix increment for consistency

++noreturn_cnt;

But ... that wouldn't be consistent here?

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 6447274).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/109163273
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 349875a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/109328420
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 9b416ca).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/109357730
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

tautschnig · 2019-05-15T14:46:07Z

@kroening This is finally ready for review - it used to be a monster, but is now down to 2 commits with just +90/−26 modified lines.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ddef9eb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111944054

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1690609).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112249534

This mirrors what the C front-end already does, but requires changes to constant propagation in the C++ front-end: we previously used macros, which serve a very different purpose otherwise. Fixes: diffblue#1490

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a1c7330).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112357550

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: feb3c1d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112359540
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

We should perform as much sanity checking in regression tests as possible. This required cleaning up unused parameter identifiers and disabling sanity checking of names as is already done for Java, because we similarly have name mangling in C++.

While we already configured this in goto-cc, running CBMC with --winx64 or --win32 previously failed to set this.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 86d4c0d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112363584

tautschnig added the bugfix label Aug 21, 2017

tautschnig requested a review from peterschrammel August 21, 2017 15:36

tautschnig self-assigned this Aug 21, 2017

tautschnig changed the base branch from master to develop August 22, 2017 12:12

andreast271 reviewed Oct 3, 2017

View reviewed changes

andreast271 approved these changes Oct 13, 2017

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from 6458759 to 7d8b507 Compare October 27, 2017 16:44

tautschnig requested review from kroening and smowton as code owners October 27, 2017 16:44

tautschnig force-pushed the c++-front-end-fixes branch from 7d8b507 to 36246e1 Compare October 27, 2017 17:02

smowton reviewed Oct 30, 2017

View reviewed changes

thk123 reviewed Oct 31, 2017

View reviewed changes

tautschnig requested a review from forejtv as a code owner November 2, 2017 19:27

tautschnig force-pushed the c++-front-end-fixes branch from 32d1703 to 23a40ff Compare November 2, 2017 19:30

tautschnig mentioned this pull request Nov 3, 2017

Run cbmc c++ regression as part of default regression test #1481

Merged

tautschnig force-pushed the c++-front-end-fixes branch from 669de88 to 8524b10 Compare December 4, 2017 09:33

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Dec 4, 2017

thk123 reviewed Dec 4, 2017

View reviewed changes

tautschnig requested review from martin-cs and owen-mc-diffblue as code owners April 22, 2019 16:16

allredj reviewed Apr 22, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from 6447274 to 349875a Compare April 22, 2019 19:50

allredj reviewed Apr 23, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from 349875a to 9b416ca Compare April 23, 2019 21:27

allredj reviewed Apr 23, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from 9b416ca to ddef9eb Compare May 15, 2019 14:41

tautschnig changed the title ~~C++ front end fixes [depends-on: #4560, blocks: #2554]~~ C++ front end fixes [blocks: #2554] May 15, 2019

tautschnig removed the dependent - do not merge label May 15, 2019

tautschnig assigned kroening and unassigned tautschnig May 15, 2019

allredj reviewed May 15, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from ddef9eb to 1690609 Compare May 17, 2019 14:27

allredj reviewed May 17, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch from 1690609 to 5a735d6 Compare May 17, 2019 19:47

C++ front-end: Remove internal symbols before linking

9f79244

This mirrors what the C front-end already does, but requires changes to constant propagation in the C++ front-end: we previously used macros, which serve a very different purpose otherwise. Fixes: diffblue#1490

tautschnig force-pushed the c++-front-end-fixes branch from 5a735d6 to a1c7330 Compare May 19, 2019 13:46

allredj reviewed May 19, 2019

View reviewed changes

tautschnig force-pushed the c++-front-end-fixes branch 2 times, most recently from feb3c1d to 196ef9a Compare May 19, 2019 15:29

allredj reviewed May 19, 2019

View reviewed changes

tautschnig added 2 commits May 19, 2019 16:58

Default C++ language standard on Windows is C++14

86d4c0d

While we already configured this in goto-cc, running CBMC with --winx64 or --win32 previously failed to set this.

tautschnig force-pushed the c++-front-end-fixes branch from 196ef9a to 86d4c0d Compare May 19, 2019 17:01

allredj reviewed May 19, 2019

View reviewed changes

kroening approved these changes May 21, 2019

View reviewed changes

kroening merged commit c564b75 into diffblue:develop May 21, 2019

tautschnig deleted the c++-front-end-fixes branch May 22, 2019 07:09

		@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]

		\********************************************************************/

		@@ -1,4 +1,4 @@
		/** *************************************************************\
		/********************************************************************\

		@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]

		#include "cpp_declarator_converter.h"

		//#define DEBUG

		@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]

		#include "cpp_typecheck_resolve.h"

		//#define DEBUG

		@@ -1,4 +1,4 @@
		CORE
		KNOWNBUG

C++ front end fixes [blocks: #2554] #1260

C++ front end fixes [blocks: #2554] #1260

Conversation

tautschnig commented Aug 21, 2017 • edited Loading

tautschnig commented Aug 21, 2017

andreast271 commented Sep 29, 2017 • edited Loading

andreast271 commented Sep 29, 2017

martin-cs commented Oct 2, 2017

andreast271 Oct 3, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

andreast271 Oct 3, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Oct 3, 2017 • edited Loading

Choose a reason for hiding this comment

andreast271 left a comment

Choose a reason for hiding this comment

peterschrammel commented Oct 27, 2017

tautschnig commented Oct 27, 2017

andreast271 commented Oct 30, 2017

andreast271 commented Oct 30, 2017 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Oct 31, 2017

tautschnig commented Dec 4, 2017

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented May 15, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Aug 21, 2017 •

edited

Loading

andreast271 commented Sep 29, 2017 •

edited

Loading

andreast271 Oct 3, 2017 •

edited

Loading

andreast271 Oct 3, 2017 •

edited

Loading

tautschnig Oct 3, 2017 •

edited

Loading

andreast271 commented Oct 30, 2017 •

edited

Loading