Add checks for symbol well-formedness. by NlightNFotis · Pull Request #3193 · diffblue/cbmc

NlightNFotis · 2018-10-17T16:25:48Z

Add a well-formedness check method to the symbol class, and add it as an extra criterion to the
soundness of a symbol table that every symbol is well-formed.

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.
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).
n/a 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.

src/util/symbol.cpp

src/util/symbol_table.cpp

chrisr-diffblue · 2018-10-17T16:32:25Z

unit/util/symbol.cpp

+      }
+    }
+  }
+}


Missing newline

chrisr-diffblue · 2018-10-17T16:32:35Z

src/util/symbol.cpp

+  }
+
+  return true;
+}


Missing newline

martin-cs

[ Approval for the last commit only. ]
Seems reasonable.

danpoe

LGTM

Skeleton for well-formedness checking of goto models [blocks: #3118, #3147, #3188, #3191, #3187, #3193]

NlightNFotis · 2018-11-19T11:13:47Z

There was a problem with the introduction of this set of changes that made the unit tests in unit/util/symbol_table.cpp to fail. The change introduced is that this introduces the well-formedness checks for the individual symbols, which are getting invoked by symbol_tablet::validate(). Because the symbol constructed by hand in unit/util/symbol_table.cpp doesn't pass the well-formedness criteria, the test failed because it tested validate(), which called symbol.is_well_formed() on the symbol.

hannes-steffenhagen-diffblue

LGTM

allredj

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

smowton · 2018-12-14T10:27:16Z

unit/util/symbol.cpp

+
+    WHEN("The symbol doesn't have base name as a suffix to name")
+    {
+      symbol.name = "TEST";


That will fail due to a non-empty mode, which isn't what you intend to test.

Yes, you were right. I fixed this now.

smowton · 2018-12-14T10:28:28Z

unit/util/symbol_table.cpp


    symbolt symbol;
-    irep_idt symbol_name = "Test";
+    irep_idt symbol_name = "Test_TestBase";


Given this test doesn't check symbol.is_well_formed(), it's a little surprising to see this check happening at the same time.

This is because this was a test for something related added by @chrisr-diffblue but went in first, so my change had now broken this test, so I had to edit this test to conform to what the validity checks expected, and make it pass again.

NlightNFotis · 2018-12-14T10:41:34Z

@smowton Addressed your latest comments. Can you re-review now please?

smowton

CI looks actually broken, but the code LGTM

Add a method that checks a symbol for structural validity according to some predetermined rule, and add it as an extra rule for symbol-table validity that each symbol is well-formed.

allredj

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

NlightNFotis self-assigned this Oct 17, 2018

NlightNFotis requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue and kroening October 17, 2018 16:25

NlightNFotis requested review from martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners October 17, 2018 16:25

chrisr-diffblue reviewed Oct 17, 2018

View reviewed changes

NlightNFotis force-pushed the symbol-well-formedness branch from 30e7adc to 6754dbe Compare October 19, 2018 10:21

martin-cs approved these changes Oct 19, 2018

View reviewed changes

danpoe approved these changes Oct 19, 2018

View reviewed changes

tautschnig added a commit that referenced this pull request Nov 9, 2018

Merge pull request #3123 from danpoe/feature/well-formedness-checking

f08e23b

Skeleton for well-formedness checking of goto models [blocks: #3118, #3147, #3188, #3191, #3187, #3193]

NlightNFotis force-pushed the symbol-well-formedness branch 3 times, most recently from 86b6c4d to be2492a Compare November 12, 2018 14:45

NlightNFotis force-pushed the symbol-well-formedness branch from be2492a to cf34d42 Compare November 19, 2018 11:14

NlightNFotis assigned tautschnig, kroening and peterschrammel Nov 19, 2018

hannes-steffenhagen-diffblue approved these changes Nov 19, 2018

View reviewed changes

allredj reviewed Nov 19, 2018

View reviewed changes

smowton reviewed Dec 14, 2018

View reviewed changes

johnnonweiler unassigned tautschnig, kroening and peterschrammel Dec 14, 2018

NlightNFotis force-pushed the symbol-well-formedness branch from cf34d42 to 7dc7d36 Compare December 14, 2018 10:39

smowton approved these changes Dec 14, 2018

View reviewed changes

NlightNFotis force-pushed the symbol-well-formedness branch 2 times, most recently from 91919ae to 5c1319d Compare December 17, 2018 16:11

Add well-formedness checks for symbols.

df616e4

Add a method that checks a symbol for structural validity according to some predetermined rule, and add it as an extra rule for symbol-table validity that each symbol is well-formed.

NlightNFotis force-pushed the symbol-well-formedness branch from 5c1319d to df616e4 Compare December 18, 2018 15:45

NlightNFotis merged commit 94ebd97 into diffblue:develop Dec 18, 2018

allredj reviewed Dec 18, 2018

View reviewed changes

NlightNFotis deleted the symbol-well-formedness branch December 19, 2018 10:58

chrisr-diffblue mentioned this pull request Jan 3, 2019

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

Closed

3 tasks

chrisr-diffblue mentioned this pull request Jan 15, 2019

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

Merged

7 tasks

+                    }
+                  }
+                }
+              }

                
                    No newline at end of file

Conversation

NlightNFotis commented Oct 17, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisr-diffblue Oct 17, 2018

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Oct 17, 2018

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Nov 19, 2018

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Dec 14, 2018

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Dec 14, 2018

Choose a reason for hiding this comment

Uh oh!

smowton Dec 14, 2018

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Dec 14, 2018 • 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!

NlightNFotis commented Dec 14, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants

NlightNFotis commented Oct 17, 2018 •

edited

Loading

NlightNFotis Dec 14, 2018 •

edited

Loading