Consistency between goto programs and symbol table #3118

xbauch · 2018-10-08T10:28:47Z

Introduce a chain of methods that (at the lowest level) iterate over all symbols
in a goto program and for each one check that it is present in the symbol table
as well. On the lower levels, the methods collect inconsistency messages and
print them to error output. On the top level, e.g. cbmc-parser, they return a
Boolean value to be caught by an invariant check.

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.

tautschnig · 2018-10-08T10:43:00Z

I'm not sure I'm convinced this is a design that is easy to extend - it seems each additional check will required about the same amount of changes? See #918 for an attempt of mine that should make it fairly easy to add new checks?

NlightNFotis

Some changes to be done, otherwise looks good to me.

NlightNFotis · 2018-10-08T10:40:41Z

src/goto-programs/goto_model.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #include "abstract_goto_model.h"
 #include "goto_functions.h"

+#include <iostream>


#include <iostream> in a header is a very bad idea. Please remove this and move the implementation of check_id_consistency_symbol_table to a .cpp file.

Ok, removed iostream and reworked to use messaget instance.

NlightNFotis · 2018-10-08T10:42:29Z

src/goto-programs/goto_model.h

+    }
+    if(!message_collector.empty())
+    {
+      std::cerr << "Error messages collected while checking the goto "


Also, can you see if you have a reference to a message handler like error() or info(), instead of writing to std::cerr? If it's possible please do that instead.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 0f2ee10).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87188872
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

xbauch · 2018-10-08T14:26:01Z

The second commit rewrites the functionality following #918 style to simplify adding further checks.

NlightNFotis

LGTM just one comment

NlightNFotis · 2018-10-08T14:26:45Z

src/goto-programs/goto_program.cpp

+
+  switch(type)
+  {
+  case GOTO:


I think this whole construct can be simplified, unless there's a reason not to? just keep the case ASSERT and case FUNCTION_CALL that require special handling, and just remove the other ones and add one default?

There's method in this madness. When we add further checks we simply put them under the right case, without having to add more cases. (At least I think so: this part I've also copied from #918.)

Another thing to keep in mind is the semantics of what you've written. The behaviour is the same for all of case GOTO, case ASSUME and case ASSERT for example, where for each one of them guard.visit(symbol_finder); will run because of fall through of the switch cases. Is that intended, or only case ASSERT should demonstrate that? If yes that's okay. If no, then what I suggested is a better/cleaner idea, and semantically correct while reducing the possibility of having cases being unintendedly massed together.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 30cc479).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87218803
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

This first commit is just PR diffblue#3118 to reuse the common structure of checking this kind of consistency.

sonodtt · 2018-10-09T12:03:43Z

src/cbmc/cbmc_parse_options.cpp

+  INVARIANT(
+    !goto_model.check_internal_invariants(*this),
+    "goto program internal invariants failed");
+


Not entirely sure what the best approach is, but this might be relevant going forward as we extend this.
I'm considering calling my goto_program checks from the try block of cbmc_parse_optionst::get_goto_program so that any exceptions of type 'incorrect_goto_program_exceptiont' are caught there.
If called directly from the doit() method exceptions are then caught in parse_options_baset::main()
which has only the base exception type or the invalid_user_input_exceptiont type.
(I think)

Well in #3123 @danpoe makes it switchable to throw exception of check invariant. Also, the whole well-formedness is optional (user-wise). So, yes, I expect the point of entry to be modified at some point.

This first commit is just PR diffblue#3118 to reuse the common structure of checking this kind of consistency.

sonodtt

Comment was addressed.

Comment was addressed

danpoe · 2018-10-09T15:10:39Z

src/goto-programs/goto_program.cpp

+  bool found_violation = false;
+  std::vector<std::string> id_collector;
+  auto symbol_finder = [&](const exprt &e) {
+    if(e.id() == ID_symbol)


I think we should also check the types with IDs ID_symbol_type, ID_struct_tag, ID_c_enum_tag, and ID_union_tag here (see std_types.h). Those types also hold an identifier which indexes into the symbol table.

Ok, I've added those checks and reworked the code to use DATA_CHECK.

danpoe · 2018-10-09T15:15:16Z

src/goto-programs/goto_program.cpp

+    {
+      auto symbol_expr = to_symbol_expr(e);
+      if(!table.has_symbol(symbol_expr.get_identifier()))
+        id_collector.push_back(id2string(symbol_expr.get_identifier()));


We could probably also use the DATA_CHECK() macros here as in #3128. I was thinking if we want a third method where we keep going and report all errors we could add a third validation mode, say validation_modet::KEEP_GOING which does not throw an exception or yield a DATA_INVARIANT violation but instead prints the error messages to the error() stream. But that's future work I'd say.

allredj

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

allredj

Passed Diffblue compatibility checks (cbmc commit: 8cb487f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87618130

tautschnig · 2018-11-14T13:29:58Z

src/goto-programs/goto_function.h

@@ -117,7 +117,59 @@ class goto_functiont
  /// reported via DATA_INVARIANT violations or exceptions.
  void validate(const namespacet &ns, const validation_modet vm) const
  {
-    body.validate(ns, vm);
+    auto type_symbol_finder =


These seem very useful utilities - can we move them to/reconcile them with util/find_symbols.{h,cpp}?

tautschnig · 2018-11-14T13:32:09Z

src/util/expr.cpp

@@ -327,6 +327,24 @@ void exprt::visit(const_expr_visitort &visitor) const
  }
 }

+void exprt::visit(const std::function<void(const exprt &)> &f) const


Ok, but we should really have this in a separate commit, it would in fact warrant both documentation and a unit test.

unit/Makefile

xbauch · 2018-11-19T16:23:50Z

I've added a few fixes to appease the CI, then squashed. The above comments should all be addressed.

allredj

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

xbauch · 2018-12-04T11:13:51Z

@tautschnig I've rebased to include #3480 changes.

tautschnig · 2018-12-04T11:43:48Z

@xbauch I'll take a look, but it seems CI is failing.

xbauch · 2018-12-04T12:18:05Z

@tautschnig Yes, my older tests were not smart enough for the new validation checks. Should be fine now.

tautschnig

Various smaller comments, but the part I'm most concerned about are the two new find_* functions that don't actually seem to be "finding" much, but just doing the checking. I think these are two distinct activities.

tautschnig · 2018-12-04T11:46:38Z

src/util/expr.cpp

+{
+  std::stack<const exprt *> stack;
+  stack.push(this);
+  while(!stack.empty())


Why is this not using the depth_iteratort? And I don't think it actually implements the visitor pattern in any way? Maybe we should at least not call this method visit?

I haven't noticed we have iterators (probably confused by the existing visit methods that do not use them). In which case I can as well call std::for_each directly.

And thus we don't need the unit test at all.

Yay for less code!

tautschnig · 2018-12-04T11:47:09Z

src/util/expr.h

@@ -305,6 +305,12 @@ class exprt:public irept
  void visit(class expr_visitort &visitor);
  void visit(class const_expr_visitort &visitor) const;

+  /// Recursively traverse the expression tree (via operands) and call \p f on
+  /// every subexpressions, including `this`. The input function has
+  /// side-effects and does not modify the expression.


"has no side-effects" - or "may have side-effects"? At least I don't understand why we would have to prescribe that this function has side effects (though arguably it might not make sense to do this if it does not have any effect).

Changed to "may have side effects"

tautschnig · 2018-12-04T11:49:58Z

src/util/find_symbols.h


 class exprt;
 class symbol_exprt;
 class typet;
+class symbolt;
+class source_locationt;


Nit pick: lexicographic ordering.

tautschnig · 2018-12-04T11:50:28Z

src/goto-programs/goto_function.h

@@ -118,6 +119,13 @@ class goto_functiont
  void validate(const namespacet &ns, const validation_modet vm) const
  {
    body.validate(ns, vm);
+    source_locationt nil_location;
+    nil_location.make_nil();


Is this important?

tautschnig · 2018-12-04T12:21:14Z

src/goto-programs/goto_function.h

+    forall_subtypes(it, type)
+    {
+      find_typetag_in_namespace(*it, nil_location, ns, vm);
+    }


Hmm, I don't get the impression that this is doing much of a "find." Couldn't you actually use one of the find_* functions to find the identifiers, and then check all of those that you have found?

@tautschnig Ok, but this last bit required a bit more code change so I pushed it as a new commit and will squash once approved.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: bbeb694).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93516892
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig

Looks good to me, especially the increased code reuse and less code being added.

allredj

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

Iterate over all symbols in a goto program and for each one check that it is present in the symbol table as well. Includes a unit test for the check.

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

Look up the symbol id in symbol table and call base_type_eq on every symbol expression in guard and code whenever relevant. Includes a unit test. Also fixes unit tests that these new checks brake.

allredj

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

xbauch requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners October 8, 2018 10:28

NlightNFotis suggested changes Oct 8, 2018

View reviewed changes

allredj reviewed Oct 8, 2018

View reviewed changes

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

xbauch force-pushed the program_table_identifier_consistency branch from 3dfac03 to 30cc479 Compare October 8, 2018 14:15

NlightNFotis approved these changes Oct 8, 2018

View reviewed changes

allredj reviewed Oct 8, 2018

View reviewed changes

NlightNFotis mentioned this pull request Oct 9, 2018

Function type consistency between goto programs and symbol table #3127

Closed

7 tasks

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Oct 9, 2018

Type consistency between goto programs and symbol table

13f0398

This first commit is just PR diffblue#3118 to reuse the common structure of checking this kind of consistency.

xbauch mentioned this pull request Oct 9, 2018

Program table symbol type consistency #3128

Closed

7 tasks

sonodtt previously requested changes Oct 9, 2018

View reviewed changes

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Oct 9, 2018

Type consistency between goto programs and symbol table

efb95a6

This first commit is just PR diffblue#3118 to reuse the common structure of checking this kind of consistency.

sonodtt reviewed Oct 9, 2018

View reviewed changes

danpoe reviewed Oct 9, 2018

View reviewed changes

xbauch force-pushed the program_table_identifier_consistency branch 4 times, most recently from 0da7ada to c668985 Compare October 10, 2018 15:25

allredj reviewed Oct 10, 2018

View reviewed changes

allredj reviewed Oct 11, 2018

View reviewed changes

danpoe mentioned this pull request Oct 12, 2018

Well-formedness checking of goto models #3152

Closed

xbauch mentioned this pull request Oct 16, 2018

Well formedness checking goto #3188

Merged

6 tasks

danpoe mentioned this pull request Nov 9, 2018

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

Merged

6 tasks

tautschnig added the Needs rebase label Nov 10, 2018

xbauch force-pushed the program_table_identifier_consistency branch from 8cb487f to af862d2 Compare November 12, 2018 10:54

xbauch changed the title ~~Symbol consistency between goto programs and symbol table~~ Consistency between goto programs and symbol table Nov 12, 2018

xbauch removed the Needs rebase label Nov 12, 2018

tautschnig reviewed Nov 14, 2018

View reviewed changes

xbauch force-pushed the program_table_identifier_consistency branch 3 times, most recently from 6c6e5ca to 0f33641 Compare November 19, 2018 15:09

xbauch assigned tautschnig and unassigned xbauch Nov 19, 2018

allredj reviewed Nov 19, 2018

View reviewed changes

xbauch force-pushed the program_table_identifier_consistency branch 2 times, most recently from 8a09089 to aaf342a Compare December 4, 2018 11:05

xbauch force-pushed the program_table_identifier_consistency branch from aaf342a to bbeb694 Compare December 4, 2018 12:16

tautschnig reviewed Dec 4, 2018

View reviewed changes

tautschnig assigned xbauch and unassigned tautschnig Dec 4, 2018

allredj reviewed Dec 4, 2018

View reviewed changes

tautschnig approved these changes Dec 5, 2018

View reviewed changes

allredj reviewed Dec 5, 2018

View reviewed changes

Petr Bauch added 3 commits December 5, 2018 10:43

Symbol consistency between goto programs and symbol table

bc281cc

Iterate over all symbols in a goto program and for each one check that it is present in the symbol table as well. Includes a unit test for the check.

Function type consistency between goto programs and symbol table

a0289a7

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

Program table symbol type consistency

60a833e

Look up the symbol id in symbol table and call base_type_eq on every symbol expression in guard and code whenever relevant. Includes a unit test. Also fixes unit tests that these new checks brake.

xbauch force-pushed the program_table_identifier_consistency branch from 559e78f to 60a833e Compare December 5, 2018 10:52

allredj reviewed Dec 5, 2018

View reviewed changes

tautschnig merged commit 55029d6 into diffblue:develop Dec 5, 2018

Consistency between goto programs and symbol table #3118

Consistency between goto programs and symbol table #3118

Conversation

xbauch commented Oct 8, 2018

tautschnig commented Oct 8, 2018

NlightNFotis 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

allredj left a comment

Choose a reason for hiding this comment

xbauch commented Oct 8, 2018

NlightNFotis 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

allredj 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

sonodtt 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

allredj left a comment

Choose a reason for hiding this comment

allredj 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

xbauch commented Nov 19, 2018

allredj left a comment

Choose a reason for hiding this comment

xbauch commented Dec 4, 2018

tautschnig commented Dec 4, 2018

xbauch commented Dec 4, 2018

tautschnig 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

allredj left a comment

Choose a reason for hiding this comment

tautschnig 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