Well formedness checking goto #3188

xbauch · 2018-10-16T14:17:16Z

Fills the skeleton of #3123 with additional checks of goto instructions. Each commit contains a unit test for its instruction.

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

xbauch · 2018-10-16T14:30:24Z

Only the last 4 commits are relevant. Feel free to have a look/review/comments but form my still be adopted to potential changes to #3123.

martin-cs

Generally : yes, a big step in the right direction. Comments are details although some of them are part of bigger discussions and maybe should be split out into separate issues (which was part of the point of this line of work).

src/goto-programs/goto_function.h

src/goto-programs/goto_program.cpp

martin-cs · 2018-10-16T15:19:32Z

src/util/std_code.h

+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(
+      operands().size() == 3, "function calls must have three operands");


A little more documentation? What are these three?

src/goto-programs/goto_program.cpp

martin-cs · 2018-10-17T14:13:34Z

Looks much better.

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

allredj

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

hannes-steffenhagen-diffblue · 2018-11-30T17:05:02Z

src/goto-programs/goto_program.cpp

+      source_location);
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      !ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
+      "declaring unknown symbol: " +


These texts seem to sometimes follow the style of "this property should hold" and other times "this property was violated". I think we should choose the same one every time (and probably prefer the former).

hannes-steffenhagen-diffblue · 2018-11-30T17:06:06Z

src/goto-programs/goto_program.cpp

+    DATA_CHECK_WITH_DIAGNOSTICS(
+      !ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
+      "removing unknown symbol: " +
+        id2string(to_code_dead(code).get_identifier()) + " from scope",


This part should go into the diagnostics bits instead of being part of the description (same applies to several other places).

hannes-steffenhagen-diffblue · 2018-11-30T17:07:39Z

unit/goto-programs/goto_program_declaration.cpp

+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(


We add a unit test for the decl checks here, but not for the dead checks which were also added in the same commit

hannes-steffenhagen-diffblue · 2018-11-30T17:09:04Z

src/util/std_expr.cpp

+  if(e.type().id() != ID_bool)
+    return false;
+  if(e.id() == ID_typecast)
+    return e.type().id() == ID_bool;


This is always true because of the previous if

hannes-steffenhagen-diffblue · 2018-11-30T17:10:12Z

src/util/std_expr.cpp

+  if(e.id() == ID_exists || e.id() == ID_forall)
+    return true;
+
+  //weird


These are for floating point numbers I think

hannes-steffenhagen-diffblue · 2018-11-30T17:12:09Z

src/util/std_expr.cpp

@@ -211,3 +211,47 @@ const exprt &object_descriptor_exprt::root_object() const

  return *p;
 }
+
+bool evaluates_to_boolean(const exprt &e)


This function is defined here, but not actually used anywhere?

Yes, Michael wanted it in util but Martin did not want it to be used (in this PR).

So maybe it should also be removed from this PR and be added to whichever PR actually does make use of it?

hannes-steffenhagen-diffblue · 2018-11-30T17:14:29Z

src/util/std_code.h

@@ -1080,6 +1080,47 @@ class code_function_callt:public codet
  {
    return op2().operands();
  }
+
+  static void check(const codet& code,


What's the difference between check, validate and validate_full?

It's explained here: https://github.com/diffblue/cbmc/blob/develop/src/util/validate_expressions.cpp

xbauch · 2018-12-03T16:29:55Z

Addressed comments by @hannes-steffenhagen-diffblue, rebased. Will squash the excessive commits once approved.

tautschnig

Just two comments about procedures.

tautschnig · 2018-12-03T17:08:59Z

src/util/std_expr.cpp

@@ -211,3 +211,47 @@ const exprt &object_descriptor_exprt::root_object() const

  return *p;
 }
+
+bool evaluates_to_boolean(const exprt &e)


So maybe it should also be removed from this PR and be added to whichever PR actually does make use of it?

tautschnig · 2018-12-03T17:10:04Z

unit/Makefile

+       goto-programs/goto_program_dead.cpp \
+       goto-programs/goto_program_declaration.cpp \
+       goto-programs/goto_program_function_call.cpp \
+       goto-programs/goto_program_goto_target.cpp \


Lexicographic ordering, please. (goto_program*<goto_trace_output)

@tautschnig I fixed the ordering. As to the above evaluates_to_boolean function: that PR hasn't been made yet. I removed it from here, and will put it to a PR once we actually make it.

allredj

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

Check that declared/removed symbol is known and the statement is valid.

Check that the guard evaluates to a Boolean value.

Check that returned types are matching.

Check that targets are well-formed and consistent.

allredj

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

xbauch requested review from cesaro, chrisr-diffblue, cristina-david, forejtv, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners October 16, 2018 14:17

xbauch added the do not merge label Oct 16, 2018

martin-cs reviewed Oct 16, 2018

View reviewed changes

sonodtt mentioned this pull request Oct 17, 2018

Goto programs validation #3191

Merged

6 tasks

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]

tautschnig assigned xbauch Nov 10, 2018

xbauch force-pushed the well-formedness-checking-goto branch from 7c2e774 to 37e570b Compare November 13, 2018 08:33

xbauch removed the do not merge label Nov 13, 2018

xbauch force-pushed the well-formedness-checking-goto branch from 66ed960 to 9447d2b Compare November 20, 2018 08:16

xbauch assigned tautschnig and unassigned xbauch Nov 20, 2018

allredj reviewed Nov 20, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Nov 30, 2018

View reviewed changes

xbauch force-pushed the well-formedness-checking-goto branch from 9447d2b to 6db85da Compare December 3, 2018 16:28

tautschnig approved these changes Dec 3, 2018

View reviewed changes

tautschnig assigned xbauch and unassigned tautschnig Dec 3, 2018

allredj reviewed Dec 3, 2018

View reviewed changes

Petr Bauch added 4 commits December 4, 2018 08:24

Well-formedness check for decl and dead instructions

5aa708a

Check that declared/removed symbol is known and the statement is valid.

Well-formedness check for assume and assert instructions

909f897

Check that the guard evaluates to a Boolean value.

Well-formedness check for function calls and returns

c742e85

Check that returned types are matching.

Well-formedness check for goto instructions

2c9a5c3

Check that targets are well-formed and consistent.

xbauch force-pushed the well-formedness-checking-goto branch from 6db85da to 2c9a5c3 Compare December 4, 2018 08:28

xbauch merged commit 6a0cafa into diffblue:develop Dec 4, 2018

allredj reviewed Dec 4, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Well formedness checking goto #3188

Well formedness checking goto #3188

xbauch commented Oct 16, 2018

xbauch commented Oct 16, 2018

martin-cs left a comment

martin-cs Oct 16, 2018

xbauch Oct 17, 2018

martin-cs commented Oct 17, 2018

allredj left a comment

hannes-steffenhagen-diffblue Nov 30, 2018

hannes-steffenhagen-diffblue Nov 30, 2018

hannes-steffenhagen-diffblue Nov 30, 2018

hannes-steffenhagen-diffblue Nov 30, 2018

hannes-steffenhagen-diffblue Nov 30, 2018

hannes-steffenhagen-diffblue Nov 30, 2018

xbauch Dec 3, 2018

tautschnig Dec 3, 2018

hannes-steffenhagen-diffblue Nov 30, 2018 •

edited

Loading

xbauch Dec 3, 2018

xbauch commented Dec 3, 2018

tautschnig left a comment

tautschnig Dec 3, 2018

tautschnig Dec 3, 2018

xbauch Dec 4, 2018

allredj left a comment

allredj left a comment

Well formedness checking goto #3188

Well formedness checking goto #3188

Conversation

xbauch commented Oct 16, 2018

xbauch commented Oct 16, 2018

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Oct 17, 2018

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

hannes-steffenhagen-diffblue Nov 30, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch commented Dec 3, 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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Nov 30, 2018 •

edited

Loading