Fix dump-c output involving typedef names #858

tautschnig · 2017-04-22T15:41:50Z

Follow-up to 99067de, which made expr2c prefer typedef names over
original type expressions.

thk123

Apologies if some of the questions are not meaningful - I've not looked at this code much.

thk123 · 2017-05-02T13:50:09Z

src/goto-instrument/dump_c.cpp

@@ -915,6 +945,66 @@ void dump_ct::cleanup_decl(

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

+Function: dump_ct::collect_typedefs
+
+Inputs:


Missing documentation for this method.

Comment addressed.

thk123 · 2017-05-02T14:00:21Z

src/goto-instrument/dump_c.cpp

@@ -1062,6 +1160,8 @@ void dump_ct::convert_function_declaration(
  if(symbol.name!=goto_functionst::entry_point() &&
     symbol.name!=ID_main)
  {
+    collect_typedefs(symbol.type);


How come we don't collect typedef's for the main function?

thk123 · 2017-05-02T14:03:15Z

src/goto-instrument/dump_c.cpp

@@ -935,6 +1025,9 @@ void dump_ct::convert_global_variable(
      !converted_global.insert(symbol.name).second)
    return;

+  if(func.empty() || symbol.is_extern)


I don't really understand this condition. For example, is this function supposed to just convert global symbols and therefore we must first check either the containing function func is empty OR the symbol is external. Is there a reason why this condition does not include the possibility of symbol.value.is_not_nil().

thk123 · 2017-05-02T14:06:43Z

src/goto-instrument/dump_c.cpp

+    {
+      system_headers.insert("stdarg.h");
+    }
+    else if(entry.second)


This might be more clearly expressed as:

// If not already in the map if(entry.second) { if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list") { system_headers.insert("stdarg.h"); } else { typet t=type; t.remove(ID_C_typedef); std::ostringstream oss; oss << "typedef " << type_to_string(t) << " " << typedef_str << ';'; entry.first->second=oss.str(); } }

To make it clearer that in either case the entry must be new to the map

thk123 · 2017-05-02T14:07:51Z

regression/goto-instrument/typedef1/test.desc

+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$


It isn't clear to me what this test actually checks - could you perhaps add some matching lines

I've added comments in the test to clarify!

thk123 · 2017-05-02T14:11:38Z

src/goto-instrument/dump_c.cpp

@@ -285,6 +285,13 @@ void dump_ct::operator()(std::ostream &os)
    os << std::endl;
  }

+  // global typedefs
+  for(const auto &td : typedef_map)


This function (operator()) is already unmanageably large - could this perhaps be pulled out into a dump_typedef_map(os) const method?

thk123 · 2017-05-03T08:27:50Z

I don't really understand this condition. For example, is this function supposed to just convert global symbols and therefore we must first check either the containing function func is empty OR the symbol is external. Is there a reason why this condition does not include the possibility of symbol.value.is_not_nil().

Is this addressed by moving the code to here: https://github.com/diffblue/cbmc/pull/858/files#diff-61b958cb13458a39e3868eea217a8bfcR65?

thk123 · 2017-05-03T08:17:57Z

src/goto-instrument/dump_c.cpp

@@ -62,6 +62,19 @@ void dump_ct::operator()(std::ostream &os)
  std::stringstream func_body_stream;
  local_static_declst local_static_decls;

+  forall_symbols(it, copied_symbol_table.symbols)


Can this be for(const auto &symbol_entry : copied_symbol_table.symbols)?

thk123 · 2017-05-03T08:21:19Z

src/goto-instrument/dump_c.cpp

@@ -1062,6 +1178,8 @@ void dump_ct::convert_function_declaration(
  if(symbol.name!=goto_functionst::entry_point() &&
     symbol.name!=ID_main)
  {
+    collect_typedefs(symbol.type, true);


This comment still seems relevant: How come we don't collect typedef's for the main function?

tautschnig · 2017-05-03T10:45:20Z

@thk123 Thank you very much for all your comments! Several of them have indeed been addressed by more comments ;-)

thk123 · 2017-05-04T09:10:14Z

@tautschnig I think both of the last two review comments are still applicable, let me know if you disagree. 1, 2

tautschnig · 2017-05-04T09:16:33Z

Would you mind copy-pasting your comment "1" as that link appears to be no longer valid? Also I think "2" is addressed by an additional comment that I've inserted above that line. But I may well be wrong!

thk123

Sorry about that! I've just reapplied the comments in the correct positions

thk123 · 2017-05-04T09:30:33Z

src/goto-instrument/dump_c.cpp

+
+void dump_ct::gather_global_typedefs()
+{
+  forall_symbols(it, copied_symbol_table.symbols)


Can this be for(const auto &symbol_entry : copied_symbol_table.symbols)

thk123 · 2017-05-04T09:32:40Z

src/goto-instrument/dump_c.cpp

@@ -1062,6 +1224,10 @@ void dump_ct::convert_function_declaration(
  if(symbol.name!=goto_functionst::entry_point() &&
     symbol.name!=ID_main)
  {
+    // make sure typedef names are available before outputting this
+    // declaration
+    collect_typedefs(symbol.type, true);


How come we don't collect typedef's for the main function?

Also I think "2" is addressed by an additional comment that I've inserted above that line

Well maybe, for me I read it as a justification to call colllect_typedefs, rather than to exclude collecting typedefs when looking at main. It also seems inconsistent, if user runs with --function foo we will collect typedefs from foo but not from main.

If you think this is correct, could you add a typedef within the main function?

Ah, thank you, I'll address this!

tautschnig · 2017-05-08T16:38:40Z

@thk123 I think I've finally addressed your comments, which were spot on!

thk123

Thanks - glad they were useful!

peterschrammel · 2017-05-12T23:03:11Z

src/goto-instrument/dump_c.cpp

@@ -857,6 +883,14 @@ bool dump_ct::ignore(const symbolt &symbol)
    system_headers.insert(it->second);
    return true;
  }
+  else if(!system_library_map.empty() &&


no else after return needed

peterschrammel · 2017-05-12T23:09:57Z

src/goto-instrument/dump_c.cpp

@@ -857,6 +883,14 @@ bool dump_ct::ignore(const symbolt &symbol)
    system_headers.insert(it->second);
    return true;
  }
+  else if(!system_library_map.empty() &&
+          has_prefix(file_str, "/usr/include/") &&


I suggest to declare a constant string, since it should be used consistently in both occurrences.

kroening · 2017-05-25T14:15:39Z

The test needs some #ifdef to make it not fail for the Windows world.

tautschnig · 2017-05-25T14:25:51Z

Test amended as the __attribute__ was completely irrelevant to the purpose of the test.

tautschnig · 2017-06-01T06:49:31Z

This should be ready to go as it has been tested on a few thousand Debian packages.

peterschrammel · 2017-06-25T20:53:55Z

@tautschnig, please rebase

tautschnig · 2017-06-28T14:28:03Z

@peterschrammel Rebase done, assert -> invariant fixes added (2f7e317).

remove_internal_symbols must get to see typedef names so as not to remove type symbols that constitute typedef names. Follow-up to 99067de

Follow-up to 99067de, which made expr2c prefer typedef names over original type expressions. Thanks Andreas Stahlbauer for providing the regression tests and help in debugging. Fixes: diffblue#882 Fixes: diffblue#964 Fixes: diffblue#972

Fixes: diffblue#973

Fixes: diffblue#934

These refer to invalid symbols.

GCC does not accept an "f" suffix on integer constants.

Cleanup of list of known functions; added several C-library internal struct types to avoid their output when the header will be declaring them.

The user-friendly default now is to produce #include statements for C library functions; this can be disabled using --no-system-headers.

peterschrammel added the bugfix label Apr 24, 2017

tautschnig force-pushed the dump-c-typedef branch 2 times, most recently from c6584f3 to cd720f1 Compare April 26, 2017 19:16

peterschrammel requested a review from thk123 April 28, 2017 18:23

thk123 suggested changes May 2, 2017

View reviewed changes

tautschnig force-pushed the dump-c-typedef branch from cd720f1 to 67c533a Compare May 3, 2017 07:18

thk123 suggested changes May 3, 2017

View reviewed changes

tautschnig force-pushed the dump-c-typedef branch 2 times, most recently from e173913 to 412ea82 Compare May 3, 2017 10:44

thk123 suggested changes May 4, 2017

View reviewed changes

tautschnig mentioned this pull request May 4, 2017

Handling of system headers. tautschnig/cbmc#1

Closed

tautschnig force-pushed the dump-c-typedef branch from 412ea82 to 2f09d57 Compare May 8, 2017 16:37

thk123 approved these changes May 9, 2017

View reviewed changes

peterschrammel reviewed May 12, 2017

View reviewed changes

tautschnig force-pushed the dump-c-typedef branch from 1a3cfb2 to 2aa435b Compare May 22, 2017 15:36

tautschnig mentioned this pull request May 22, 2017

Handling of system headers. Several adjustments tautschnig/cbmc#3

Merged

tautschnig assigned peterschrammel May 23, 2017

tautschnig force-pushed the dump-c-typedef branch 2 times, most recently from 00536bc to 66d2def Compare May 25, 2017 07:04

tautschnig mentioned this pull request May 25, 2017

goto-instrument: anonymous structs in typedefs #964

Closed

tautschnig force-pushed the dump-c-typedef branch from 66d2def to 47be491 Compare May 25, 2017 11:22

tautschnig force-pushed the dump-c-typedef branch from 47be491 to d1eb096 Compare May 25, 2017 14:25

tautschnig force-pushed the dump-c-typedef branch from d1eb096 to 6c3b9d2 Compare May 26, 2017 11:36

tautschnig force-pushed the dump-c-typedef branch from 18d860b to f763593 Compare June 8, 2017 06:31

peterschrammel assigned tautschnig and unassigned peterschrammel Jun 25, 2017

tautschnig force-pushed the dump-c-typedef branch from f763593 to d340b92 Compare June 28, 2017 13:55

tautschnig assigned kroening and unassigned tautschnig Jul 3, 2017

tautschnig and others added 15 commits July 3, 2017 14:26

dump-c: Try to guess further system headers

5938ecb

Typedef names are symbols

c54ddb8

remove_internal_symbols must get to see typedef names so as not to remove type symbols that constitute typedef names. Follow-up to 99067de

Fix dump-c output involving typedef names

dc5ae8c

Follow-up to 99067de, which made expr2c prefer typedef names over original type expressions. Thanks Andreas Stahlbauer for providing the regression tests and help in debugging. Fixes: diffblue#882 Fixes: diffblue#964 Fixes: diffblue#972

No special handling of $link. This might appear due to unknown reasons.

f56a398

Do not dump certain types if they are defined in system headers

2aa140c

Do not dump anonymous types from system headers

b0e0c0a

Fixes: diffblue#973

Dump the global declarations after the included system headers

ac270c5

Locate var args use even when va_arg_next is not used

fe04e59

Fixes: diffblue#934

Output _Noreturn qualifier at appropriate place

0428f6a

Do not dump internal $object declarations

3a57645

These refer to invalid symbols.

Output float literals in a GCC-compatible fashion

f6509c3

GCC does not accept an "f" suffix on integer constants.

bswap is not a library function; use __builtin_bswap[bit-suffix] instead

ad55c4f

Improve --use-system-headers output for GCC compatibility

a9dca20

Cleanup of list of known functions; added several C-library internal struct types to avoid their output when the header will be declaring them.

dump-c: respect local translation bounds in resolving switch/case

38b4c48

Use invariant annotations instead of asserts

e2cfed3

tautschnig force-pushed the dump-c-typedef branch from 2f7e317 to 18460bf Compare July 3, 2017 13:31

dump-c: Replace --use-system-headers by --no-system-headers

34a476f

The user-friendly default now is to produce #include statements for C library functions; this can be disabled using --no-system-headers.

tautschnig force-pushed the dump-c-typedef branch from 18460bf to 34a476f Compare July 3, 2017 14:24

kroening merged commit c7ce527 into diffblue:master Jul 3, 2017

tautschnig deleted the dump-c-typedef branch July 3, 2017 16:56

tautschnig mentioned this pull request Jul 4, 2017

Make output of --dump-c --use-system-headers compilable #249

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix dump-c output involving typedef names #858

Fix dump-c output involving typedef names #858

tautschnig commented Apr 22, 2017

thk123 left a comment

thk123 May 2, 2017

tautschnig May 3, 2017

thk123 May 2, 2017

thk123 May 2, 2017

thk123 May 2, 2017 •

edited

Loading

thk123 May 2, 2017

tautschnig May 3, 2017

thk123 May 2, 2017

thk123 commented May 3, 2017 •

edited

Loading

thk123 May 3, 2017

thk123 May 3, 2017

tautschnig commented May 3, 2017

thk123 commented May 4, 2017

tautschnig commented May 4, 2017

thk123 left a comment

thk123 May 4, 2017 •

edited

Loading

thk123 May 4, 2017

thk123 May 4, 2017

tautschnig May 4, 2017

tautschnig commented May 8, 2017

thk123 left a comment

peterschrammel May 12, 2017

peterschrammel May 12, 2017

kroening commented May 25, 2017

tautschnig commented May 25, 2017

tautschnig commented Jun 1, 2017

peterschrammel commented Jun 25, 2017

tautschnig commented Jun 28, 2017

Fix dump-c output involving typedef names #858

Fix dump-c output involving typedef names #858

Conversation

tautschnig commented Apr 22, 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

thk123 May 2, 2017 • edited Loading

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 May 3, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented May 3, 2017

thk123 commented May 4, 2017

tautschnig commented May 4, 2017

thk123 left a comment

Choose a reason for hiding this comment

thk123 May 4, 2017 • edited Loading

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

tautschnig commented May 8, 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

kroening commented May 25, 2017

tautschnig commented May 25, 2017

tautschnig commented Jun 1, 2017

peterschrammel commented Jun 25, 2017

tautschnig commented Jun 28, 2017

thk123 May 2, 2017 •

edited

Loading

thk123 commented May 3, 2017 •

edited

Loading

thk123 May 4, 2017 •

edited

Loading