Function type consistency between goto programs and symbol table #3127

xbauch · 2018-10-09T08:45:02Z

A simple iteration over goto-functions to check that it's base type is the same
as the one stored in the symbol table.

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
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).
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.

A simple iteration over goto-functions to check that it's base type is the same as the one stored in the symbol table.

smowton · 2018-10-09T08:47:19Z

src/goto-programs/goto_model.h

+      if(!base_type_eq(
+           it->second.type, symbol_table.lookup_ref(it->first).type, ns))
+      {
+        msg.error() << "error" << messaget::eom;


Say what's wrong!

Yes, a better error message here would be good.

smowton · 2018-10-09T08:47:51Z

src/cbmc/cbmc_parse_options.cpp

@@ -515,6 +515,10 @@ int cbmc_parse_optionst::doit()
  if(get_goto_program_ret!=-1)
    return get_goto_program_ret;

+  INVARIANT(
+    !goto_model.check_internal_invariants(*this),


check_consistency?

I find these a little bit confusing in design, both here and in #3118. Do you think it would be better if check_internal_invariants returned true by default, as the all is good case, and false otherwise? This invariant would also look cleaner as well, as it would just read as the internal invariants of the goto model should always hold, which this is what the invariant will check by essence of it returning true and not if this doesn't return false, then the internal invariants hold. Like, it's the double negative both in the condition here, and the return values of check_internal_invariants that's slightly confusing, as it's inverse logic to what's expected. But that's just me, certainly not required.

@smowton Within this PR, yes. But we are preparing a larger collection of checks and not all of them target consistency.

@NlightNFotis it was my understanding that we prefer returning true when things fail. It can of course be negated.

@NlightNFotis My understanding is that linux programs return 0 to indicate no error and a non-zero integer to represent some kind of error. C programs copy this and return 0 to indicate no error. We follow this by returning false to indicate no error and true to indicate error. I find it confusing too.

Yeah most functions return true on error and false on success. Let's stick with this convention for consistency for now.

NlightNFotis

A couple of comments.

NlightNFotis · 2018-10-09T09:44:01Z

src/goto-programs/goto_model.h

+      if(!base_type_eq(
+           it->second.type, symbol_table.lookup_ref(it->first).type, ns))
+      {
+        msg.error() << "error" << messaget::eom;


Yes, a better error message here would be good.

NlightNFotis · 2018-10-09T09:47:27Z

src/cbmc/cbmc_parse_options.cpp

@@ -515,6 +515,10 @@ int cbmc_parse_optionst::doit()
  if(get_goto_program_ret!=-1)
    return get_goto_program_ret;

+  INVARIANT(
+    !goto_model.check_internal_invariants(*this),


I find these a little bit confusing in design, both here and in #3118. Do you think it would be better if check_internal_invariants returned true by default, as the all is good case, and false otherwise? This invariant would also look cleaner as well, as it would just read as the internal invariants of the goto model should always hold, which this is what the invariant will check by essence of it returning true and not if this doesn't return false, then the internal invariants hold. Like, it's the double negative both in the condition here, and the return values of check_internal_invariants that's slightly confusing, as it's inverse logic to what's expected. But that's just me, certainly not required.

allredj

Passed Diffblue compatibility checks (cbmc commit: 8558e89).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87310747

Now reports the id of violating function and the two inconsistent types.

allredj

Passed Diffblue compatibility checks (cbmc commit: 150cf46).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87323737

danpoe · 2018-10-09T15:21:28Z

src/cbmc/cbmc_parse_options.cpp

@@ -515,6 +515,10 @@ int cbmc_parse_optionst::doit()
  if(get_goto_program_ret!=-1)
    return get_goto_program_ret;

+  INVARIANT(
+    !goto_model.check_internal_invariants(*this),


Yeah most functions return true on error and false on success. Let's stick with this convention for consistency for now.

danpoe · 2018-10-09T15:23:44Z

src/goto-programs/goto_model.h

+    namespacet ns(symbol_table);
+    forall_goto_functions(it, goto_functions)
+    {
+      if(!base_type_eq(


Could use the DATA_CHECK macros.

Using DATA_CHECK instead of calling error handling directly.

allredj

Passed Diffblue compatibility checks (cbmc commit: 43052d5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87497802

Builds a goto model with one function and checks that: 1) with the right type in the table the validation succeeds, 2) with the wrong type the validation fails.

allredj

Passed Diffblue compatibility checks (cbmc commit: 00357ff).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87657183

hannes-steffenhagen-diffblue · 2018-10-12T09:30:26Z

src/util/validate.h

+/// goto programs, expressions, instructions, etc. Based on the value of the
+/// variable vm (the validation mode), it either uses DATA_INVARIANT() to check
+/// those conditions, or throws an exception when a condition does not hold.
+#define DATA_CHECK(condition, message)                                         \


I'm unclear why we want this. Either something is an invariant or it isn't, I don't see the value in having a single construct for both cases.

xbauch · 2018-11-12T14:05:33Z

Moved to #3118.

Function type consistency between goto programs and symbol table

8558e89

A simple iteration over goto-functions to check that it's base type is the same as the one stored in the symbol table.

xbauch requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners October 9, 2018 08:45

smowton reviewed Oct 9, 2018

View reviewed changes

NlightNFotis reviewed Oct 9, 2018

View reviewed changes

allredj reviewed Oct 9, 2018

View reviewed changes

Better error message

150cf46

Now reports the id of violating function and the two inconsistent types.

allredj reviewed Oct 9, 2018

View reviewed changes

danpoe reviewed Oct 9, 2018

View reviewed changes

danpoe and others added 2 commits October 10, 2018 13:59

Add macros for goto model validation

7dd2aa5

Reworked based on PR diffblue#3123

43052d5

Using DATA_CHECK instead of calling error handling directly.

allredj reviewed Oct 10, 2018

View reviewed changes

xbauch force-pushed the program_table_type_consistency branch from 408c810 to 7ceafcc Compare October 11, 2018 14:07

xbauch requested a review from chrisr-diffblue as a code owner October 11, 2018 14:07

Added unit test for wrong type in table

00357ff

Builds a goto model with one function and checks that: 1) with the right type in the table the validation succeeds, 2) with the wrong type the validation fails.

xbauch force-pushed the program_table_type_consistency branch from 7ceafcc to 00357ff Compare October 11, 2018 14:10

allredj reviewed Oct 11, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Oct 12, 2018

View reviewed changes

danpoe mentioned this pull request Oct 12, 2018

Well-formedness checking of goto models #3152

Closed

tautschnig added the Needs rebase label Nov 10, 2018

tautschnig assigned xbauch Nov 10, 2018

xbauch closed this Nov 12, 2018

Function type consistency between goto programs and symbol table #3127

Function type consistency between goto programs and symbol table #3127

Uh oh!

Conversation

xbauch commented Oct 9, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch Oct 9, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj 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!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Nov 12, 2018

Uh oh!

Uh oh!

xbauch Oct 9, 2018 •

edited

Loading