Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing. #3767

chrisr-diffblue · 2019-01-11T17:33:35Z

This PR supersedes #3661 by taking the first commit in that PR (which makes regression tests run with --validate-goto-program) and then the subsequent commits in this PR fix up a few places that causes regression tests to fail. The final commit in this PR adds a few special cases to the symbol.is_well_formed() check that was previously added in #3193.

I have a few concerns about these additional 'special cases' - so I'd welcome feedback on those - they feel a bit like a breaking of abstraction.

@kroening Feel free to either cherry-pick commits from this PR into #3661, or close that and focus on this PR instead. As mentioned by @tautschnig - this PR also supersedes/compliments #2734 as well.

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.

allredj

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

allredj

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

tautschnig · 2019-01-15T16:27:55Z

Just noting that this will help us close out #2734, where I complained about the missing test.

chrisr-diffblue · 2019-01-15T16:30:07Z

Good spot!

allredj

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

tautschnig · 2019-01-28T12:54:13Z

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>

+#include <goto-programs/remove_returns.h>


I'd prefer #include "remove_returns.h" and placing that at the bottom of the list of includes, for consistency with how that's done in other files.

And a nit-pick: s/differnet/different/ in the commit message.

tautschnig · 2019-01-28T12:56:15Z

src/goto-programs/goto_program.cpp

+              // type of the function and use that full type to check
+              // consistency with the goto program
+              auto full_table_symbol_type = to_code_type(table_symbol->type);
+              full_table_symbol_type.return_type() = return_value_symbol->type;


This can be simplified by using original_return_type (from remove_returns.{h,cpp}).

Thanks - I did actually look for a utility function to use here, but somehow managed to miss that. I much appreciate the pointer.

tautschnig · 2019-01-28T12:58:54Z

Some smaller suggestions for improvement above, but otherwise I'd suggest to merge this as soon as possible.

The symbol naming check added in df616e4 attempts to assert that the 'base_name' of a symbol is a suffix of that symbol's 'name'. In general, this should be the case, but there are certain classes of symbols where this does not currently hold. This commit adds special cases to handle: * Type symbols that are typedefs or tags * Symbols that have been renamed by the linker With these special cases handled, it is possible to run the CORE regression tests with --validate-goto-model enabled.

…ified types Return removal sets the return type of a function symbol table entry to 'void', but some callsites still expect the original type (e.g. if a function is passed as a parameter to a different function)

…types

…types When a function declaration and its definition appear in different translation units they may have different return types. This commit relaxes the checks in goto_programt::instructiont::validate() in these circumstances.

This will prevent the introduction of changes that violate the checks in the goto-validation procedure.

chrisr-diffblue · 2019-01-28T15:20:14Z

I'll wait for CI to pass, then merge if nobody else wants to block it.

smowton · 2019-01-28T16:18:08Z

The function-type mismatch due to declaration vs. definition inconsistency smells a bit off. Is there future work to figure out why that results in a symbol-table vs. goto-program type clash?

chrisr-diffblue · 2019-01-28T16:20:38Z

@smowton I don't have a fixed plan to dig into that deeper, but yes, I'd like to at some point - though its the kind of code that, say, GCC will compile relatively happily... regression/cbmc/Linking7/return_type*.c is an example of such a program.

tautschnig · 2019-01-28T16:26:10Z

@smowton @chrisr-diffblue The goto-program linker permits various type inconsistencies to compile (poor) real-world C code. Some of it is fixed up by casts done in symbolic execution, other bits are fixed via object_type_updates in link_goto_model.cpp. There is a risk that some inconsistencies prevail, and we might have to become more stringent about the check that is being relaxed here. But as long as a type cast can fix it we're probably ok...

chrisr-diffblue · 2019-01-28T16:46:29Z

OK, CI has passed, so I'm going to hit merge. If anyone feels strongly that I shouldn't have relaxed the check declaration vs. definition check, I can sort that out in a different PR.

allredj

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

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.

As a follow up to #3767 and to keep naming consistency between C and Java.

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.

chrisr-diffblue added do not merge In progress do not review labels Jan 11, 2019

chrisr-diffblue self-assigned this Jan 11, 2019

chrisr-diffblue requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners January 11, 2019 17:33

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch 2 times, most recently from a8f7384 to d877f19 Compare January 11, 2019 21:30

allredj reviewed Jan 12, 2019

View reviewed changes

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch from 25b5339 to eec235f Compare January 14, 2019 16:41

chrisr-diffblue requested review from cesaro, cristina-david, forejtv, martin-cs, NathanJPhillips and thk123 as code owners January 14, 2019 16:41

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch 5 times, most recently from 8bf6b77 to 94da2fc Compare January 15, 2019 15:00

allredj reviewed Jan 15, 2019

View reviewed changes

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch from 94da2fc to 95bfb7d Compare January 15, 2019 16:24

allredj reviewed Jan 15, 2019

View reviewed changes

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch from 95bfb7d to 4c699cf Compare January 15, 2019 17:11

tautschnig approved these changes Jan 28, 2019

View reviewed changes

tautschnig mentioned this pull request Jan 28, 2019

set mode of gcc_builtin_va_arg symbol; partially addresses issue #2663 #2734

Closed

chrisr-diffblue and others added 11 commits January 28, 2019 15:07

Fix base_name of return' symbol to match its name

cb9fc73

Fix base_name of argc' symbol to match its name

f13dbea

Ensure the gcc_builtin_va_arg symbol has a mode

2130073

Make #anon symbols have consistent naming between base_name and name

03518c9

Ensure the '$exception_flag' symbol has a valid mode

e5bae7e

Correct validation check for return statements from void functions

33be524

Make goto_programt::instructiont::validate() accept incomplete array …

1447ad6

…types

enable --validate-goto-model for all cbmc regressions

933c2ef

This will prevent the introduction of changes that violate the checks in the goto-validation procedure.

chrisr-diffblue force-pushed the validate_goto_programs_symbol_check_fixup branch from a6b3123 to 933c2ef Compare January 28, 2019 15:18

chrisr-diffblue merged commit 1ab9364 into diffblue:develop Jan 28, 2019

allredj reviewed Jan 28, 2019

View reviewed changes

allredj pushed a commit to allredj/cbmc that referenced this pull request Jan 29, 2019

Rename return symbol to return'

50cd278

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.

allredj mentioned this pull request Jan 29, 2019

Rename return symbol to return' #3985

Merged

7 tasks

allredj pushed a commit that referenced this pull request Jan 29, 2019

Rename return symbol to return'

51240cd

As a follow up to #3767 and to keep naming consistency between C and Java.

allredj pushed a commit to allredj/cbmc that referenced this pull request Jan 29, 2019

Rename return symbol to return'

ac0075f

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.

allredj pushed a commit to allredj/cbmc that referenced this pull request Jan 29, 2019

Rename return symbol to return'

0f4ec5c

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.

tautschnig mentioned this pull request Jan 30, 2019

enable --validate-goto-model for all cbmc regressions #3661

Closed

3 tasks

sonodtt mentioned this pull request Feb 6, 2019

Goto programs validation #3191

Merged

6 tasks

tautschnig mentioned this pull request Jan 15, 2021

Use validation options in regression tests #3525

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing. #3767

Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing. #3767

chrisr-diffblue commented Jan 11, 2019 •

edited

Loading

allredj left a comment

allredj left a comment

tautschnig commented Jan 15, 2019

chrisr-diffblue commented Jan 15, 2019

allredj left a comment

tautschnig Jan 28, 2019

chrisr-diffblue Jan 28, 2019

tautschnig Jan 28, 2019

chrisr-diffblue Jan 28, 2019

tautschnig commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

smowton commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

tautschnig commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

allredj left a comment

Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing. #3767

Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing. #3767

Conversation

chrisr-diffblue commented Jan 11, 2019 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig commented Jan 15, 2019

chrisr-diffblue commented Jan 15, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig Jan 28, 2019

Choose a reason for hiding this comment

chrisr-diffblue Jan 28, 2019

Choose a reason for hiding this comment

tautschnig Jan 28, 2019

Choose a reason for hiding this comment

chrisr-diffblue Jan 28, 2019

Choose a reason for hiding this comment

tautschnig commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

smowton commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

tautschnig commented Jan 28, 2019

chrisr-diffblue commented Jan 28, 2019

allredj left a comment

Choose a reason for hiding this comment

chrisr-diffblue commented Jan 11, 2019 •

edited

Loading