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

danpoe · 2018-10-08T14:31:50Z

This PR introduces a framework for well-formedness checking of goto models. It also introduces two new macros DATA_CHECK() and DATA_CHECK_WITH_DIAGNOSTICS() for use in the various validation methods (like validate(), validate_full() on expressions). Based on the value of a variable vm (the validation mode, which is an enum with values INVARIANT or EXCEPTION), when a well-formedness check fails either a DATA_INVARIANT() fails or an incorrect_goto_program_exceptiont is thrown.

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: bcca1a6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87221686
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).

danpoe · 2018-10-08T16:27:14Z

src/util/validate_expressions.cpp

+  C<expr_type>()(expr, std::forward<Args>(args)...)
+
+template <template <typename> class C, typename... Args>
+void call_on_expr(const exprt &expr, Args &&... args)


This function simulates virtual call resolution on exprt via a case distinction on id(). The structs call_checkt, call_validatet, and call_validate_fullt in validate.h specify the method to be called (check(), validate(), and validate_full() resp.) and take as a template parameter the expression type to cast to.

danpoe · 2018-10-08T16:32:52Z

src/util/validate_expressions.cpp

+  else
+  {
+    CALL_ON_EXPR(exprt);
+  }


Cases for more expressions will be added here in the future.

In the end the last case should fail an invariant in order to actually detect when something is missing. For now it would be good if it could output a warning or so.

I've added a macro REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS that can be set when compiling. If enabled the ids for currently unimplemented expression checks are reported to stderr.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 37a4de4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87236032
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-09T10:05:11Z

src/goto-programs/goto_functions.h

+  /// reported via DATA_INVARIANT violations or exceptions.
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    for(const auto &entry : function_map)


I have this loop on the goto_model level: one less file to modify. But this works just as good.

…e#3123 The condition to be checked is the same. Interface function name was changed to follow the above PR. Also the check is now optional via command line.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 42bf8fe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87472451
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).

peterschrammel · 2018-10-10T11:40:02Z

src/util/validate.h

+template <typename T>
+struct call_checkt
+{
+  static_assert(std::is_base_of<irept, T>::value, "");


missing message (several occurrences)

Hm, the message wouldn't really add anything here. With C++17 the message will become optional then we could remove it.

peterschrammel · 2018-10-10T11:44:00Z

src/util/validate_expressions.cpp

+  else
+  {
+    CALL_ON_EXPR(exprt);
+  }


In the end the last case should fail an invariant in order to actually detect when something is missing. For now it would be good if it could output a warning or so.

peterschrammel · 2018-10-10T11:44:46Z

src/util/validate_types.cpp

+  }
+  else
+  {
+    CALL_ON_TYPE(typet);


see comment for exprt

Added a macro REPORT_UNIMPLEMENTED_TYPE_CHECKS

peterschrammel · 2018-10-10T11:50:36Z

src/util/validate_code.cpp

+  }
+  else
+  {
+    CALL_ON_CODE(codet);


see comment for exprt

added a macro REPORT_UNIMPLEMENTED_CODE_CHECKS

peterschrammel · 2018-10-10T11:51:22Z

src/util/validate_code.cpp

+}
+
+/// Check that the given code statement is well-formed, assuming that all its
+/// enclosed statements, subexpressions, etc. have all ready been checked for


peterschrammel · 2018-10-10T12:00:00Z

src/util/std_code.h

+  ///
+  /// The validation mode indicates whether well-formedness check failures are
+  /// reported via DATA_INVARIANT violations or exceptions.
+  void check(const validation_modet vm = validation_modet::INVARIANT) const


see comment for exprt

see reply for exprt :)

src/util/symbol_table.h

peterschrammel · 2018-10-10T12:01:44Z

src/cbmc/cbmc_parse_options.cpp

@@ -972,6 +978,7 @@ void cbmc_parse_optionst::help()
    " --xml-ui                     use XML-formatted output\n"
    " --xml-interface              bi-directional XML interface\n"
    " --json-ui                    use JSON-formatted output\n"
+    " --validate-goto-model        enables additional well-formedness checks on the goto program\n" // NOLINT(*)


break long help text and align below enables

You mean so the output of --help will be at most 80 characters wide, or that the code should be at most 80 characters wide, or both?

cbmc/src/goto-instrument/reachability_slicer.h

Lines 44 to 47 in 7905492

" --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \

" that visits all given functions. The list of\n" \

" functions has to be given as a comma separated\n" \

" list f.\n" \

Thanks @xbauch. So that seems to suggest 80 characters in the output but not necessarily in the code. I'm gonna change it to that.

peterschrammel · 2018-10-10T12:02:38Z

src/cbmc/cbmc_parse_options.cpp

@@ -526,6 +526,12 @@ int cbmc_parse_optionst::doit()
  if(set_properties())
    return CPROVER_EXIT_SET_PROPERTIES_FAILED;

+  if(cmdline.isset("validate-goto-model"))


Would we like to have this in the other driver programs too?

I would have thought goto-instrument was the place for it.

Yes, I think we should have the option in all of the tools to validate the goto model.

@martin-cs I think also in e.g. cbmc it would make sense to validate the goto program as a safety net sort of thing. Once right after goto_convert and perhaps once more before goto_symex to check that all the transformation passes like remove_function_pointers, etc. did not produce an ill-formed goto model.

@danpoe : I'm very much in favour of validating the program between all transformation passes; that sounds great. To the point I might suggest making that the last step of each transformation. I think this will need to be able to check for various "normal forms" as well, i.e. returns and function pointers removed, etc. ( @tautschnig may have opinions on this subject ). As I first envisaged this, that should be enough to prove that all of the DATA_INVARIANTs hold.

i also like the "with exceptions when we load it and with invariants after" approach. My only question is about the specific, user accessible command-line flag to just check the validity of the goto-program and nothing else. That seems like something we definitely want but that it should probably be in goto-instrument as a "checking and modifying the goto-program" bit of functionality, rather than in every tool.

Ah yes, that makes sense. @sonodtt is currently working on some additional checks of the goto program that will allow to pass flags that indicate whether function pointers and returns are expected to have been removed.

Cool.

@sonodtt : having looked at this in the past ( #751 is the first bit I have written down ), may I suggest that you make the flags independent for each feature. For example, one of the last few differences between the static_analyst and ait frameworks is that the later requires the abscence of function pointers (naturally or removed) and return removal. function pointer removal is an (at the moment undocumented) precondition of return removal and so on. It would be amazing if we could actually map out and enforce these requirements on "normal forms".

martin-cs

This seems like a useful and a worthwhile thing to do. I'm not sure I quite 'get' the architecture of this but I think I could be persuaded. I slightly worry that this might lead to duplication of checks but that is better than not having any at all!

src/cbmc/cbmc_parse_options.cpp

src/util/std_types.h

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 41cb816).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87476584
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).

allredj

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

Using DATA_CHECK instead of calling error handling directly.

chrisr-diffblue · 2018-10-10T15:24:32Z

src/util/validate.h

+
+/// This macro takes a condition which denotes a well-formedness criterion on
+/// goto programs, expressions, instructions, etc. Based on the value of the
+/// variable vm (the validation mode), it either uses DATA_INVARIANT() to check


I may have missed a global declaration of vm somewhere, but from what I've seen it looks like vm is just 'whatever variable of that name is in scope at the moment?` - Could you either make that explicit in the docs and/or actually add a global declaration for it somewhere? I'm otherwise wondering what the compile error messages might look like if someone tries to use these macros outside of a validate() function, or if the try to declare a variable of a different type but the same name... :-)

Ok, I've added some doc and added a static assertion to check that vm has the expected type.

src/util/validate.h

allredj

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

…flags) There are two flags: --validate-goto-binary reads in a goto binary and checks that it is well formed and then exits; --validate-goto-model enables additional well-formedness checks at various points during the execution of goto-instrument in addition to the normal analyses that it runs.

allredj

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

kroening · 2018-11-09T15:04:26Z

src/util/std_code.h

+    DATA_CHECK(
+      base_type_eq(code.op0().type(), code.op1().type(), ns),
+      "lhs and rhs of assignment must have same type");
+  }


It is no longer necessary to use base_type_eq to compare types -- you can simply use == !

That's not quite the case just yet, is it? Otherwise we should have a major campaign removing all cases of base_type_eq.

Yes, we should have that campaign, together with getting rid of most instances of ns.follow().

kroening · 2018-11-09T15:08:33Z

src/util/std_expr.h

+    DATA_CHECK(
+      base_type_eq(expr.op0().type(), expr.op1().type(), ns),
+      "lhs and rhs of binary relation expression should have same type");
+  }


kroening · 2018-11-09T15:11:01Z

If you use == instead of base_type_eq, then the namespace that gets passed around becomes unused. If that bugs you, you could use it to check whether the tag types are in the symbol table, and whether symbol_exprt identifiers are in the symbol table.

danpoe · 2018-11-09T15:21:56Z

Checking that all symbols/tags in the goto program exist in the symbol table and are consistent with the corresponding entries is the topic of @xbauch's PR #3118.

kroening · 2018-11-09T15:53:23Z

Ok, if that is meant to remain separate, then you could get rid of the namespacet parameters.

Follows the diffblue#3123 skeleton with additional checks in SSA_stept.

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

danpoe requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners October 8, 2018 14:31

danpoe added the work in progress label Oct 8, 2018

allredj reviewed Oct 8, 2018

View reviewed changes

danpoe force-pushed the feature/well-formedness-checking branch 2 times, most recently from a293f3e to 37a4de4 Compare October 8, 2018 16:18

danpoe commented Oct 8, 2018

View reviewed changes

danpoe removed the work in progress label Oct 8, 2018

allredj reviewed Oct 8, 2018

View reviewed changes

xbauch approved these changes Oct 9, 2018

View reviewed changes

xbauch mentioned this pull request Oct 9, 2018

Consistency between goto programs and symbol table #3118

Merged

7 tasks

danpoe force-pushed the feature/well-formedness-checking branch 2 times, most recently from 42bf8fe to 41cb816 Compare October 10, 2018 11:09

allredj reviewed Oct 10, 2018

View reviewed changes

peterschrammel reviewed Oct 10, 2018

View reviewed changes

danpoe force-pushed the feature/well-formedness-checking branch from 41cb816 to 0316f5f Compare October 10, 2018 12:11

martin-cs reviewed Oct 10, 2018

View reviewed changes

src/cbmc/cbmc_parse_options.cpp Outdated Show resolved Hide resolved

src/util/std_types.h Outdated Show resolved Hide resolved

allredj reviewed Oct 10, 2018

View reviewed changes

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

Reworked based on PR diffblue#3123

43052d5

Using DATA_CHECK instead of calling error handling directly.

chrisr-diffblue reviewed Oct 10, 2018

View reviewed changes

src/util/validate.h Show resolved Hide resolved

danpoe force-pushed the feature/well-formedness-checking branch from 0316f5f to 69c46d5 Compare October 10, 2018 16:04

allredj reviewed Oct 10, 2018

View reviewed changes

danpoe force-pushed the feature/well-formedness-checking branch from 69c46d5 to 5befa49 Compare October 10, 2018 18:05

danpoe added 13 commits November 9, 2018 12:14

Add functions to validate statements

c73ff05

Add validation methods to exprt

c0ebb38

Add and use validation methods in equal_exprt

552298f

Add validation methods to typet

8743abd

Add and use validation methods in unsignedbv_typet

5f1f35e

Add validation methods to codet

6539283

Add and use validation methods in code_assignt

90e2b53

Add validate() methods to (components of) goto models

0ec8986

Add macros for common command line interface for goto model validation

d11cece

Validate goto models in cbmc (if enabled via command line flag)

1d8fc32

Add check for well-formedness of assign instructions

f61e4e9

Validate goto models in goto-analyzer (if enabled via command line flag)

cc955f1

danpoe force-pushed the feature/well-formedness-checking branch from af3aa4f to d638ea7 Compare November 9, 2018 12:18

tautschnig unassigned danpoe Nov 9, 2018

allredj reviewed Nov 9, 2018

View reviewed changes

kroening reviewed Nov 9, 2018

View reviewed changes

kroening approved these changes Nov 9, 2018

View reviewed changes

kroening assigned danpoe and unassigned kroening Nov 9, 2018

tautschnig merged commit f08e23b into diffblue:develop Nov 9, 2018

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Nov 14, 2018

Initial attempt at introducing well-formedness checking for SSA

ea8c694

Follows the diffblue#3123 skeleton with additional checks in SSA_stept.

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Nov 16, 2018

Well-formedness checking for SSA

6bc7648

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Nov 16, 2018

Well-formedness checking for SSA

242655b

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Nov 30, 2018

Well-formedness checking for SSA

eb0b86b

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

danpoe deleted the feature/well-formedness-checking branch June 2, 2020 17:13

	" --fp-reachability-slice f remove instructions that cannot appear on a trace\n" \
	" that visits all given functions. The list of\n" \
	" functions has to be given as a comma separated\n" \
	" list f.\n" \

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

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

Conversation

danpoe commented Oct 8, 2018 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe Oct 8, 2018 • edited Loading

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

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

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

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

martin-cs 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

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

kroening commented Nov 9, 2018

danpoe commented Nov 9, 2018

kroening commented Nov 9, 2018

danpoe commented Oct 8, 2018 •

edited

Loading

danpoe Oct 8, 2018 •

edited

Loading