Add stub for new goto-harness tool [depends-on: #3920] #3875

hannes-steffenhagen-diffblue · 2019-01-21T17:14:15Z

This adds a new executable called goto-harness. Right now it doesn't actually do anything, but ultimately its purpose will be to generate "harness" functions for goto-programs - i.e. given some specification, it'll generate a function suitable as a cbmc entry point function that implements that specification.

Planned for now are two types of harnesses:

One that takes the name of a function with parameters and then generates a function that sets up these parameters and calls the function with them. This is similar to what cbmc does already, however will allow more flexibility in choosing how exactly these parameters will be initialised which was deemed out of scope for cbmc.

The other will be able to take a snapshot of a concrete execution of a program, and then start an analysis from that point.

This PR should serve as a common start point for both of these pieces of work. It's marked as Work In Progress for now as we've not settled on a sensible command line interface; The problem being that different harness generators have mostly completely different sets of options, with only a handful of common options.

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.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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

Please copy some of the description into the commit message.
It would likely be good to include a regression test directory (without any actual tests just yet, just the makefiles) in the initial commit as well.

With those we'd in fact have a very nice commit to serve as template for further tools to be created.

tautschnig · 2019-01-21T22:40:08Z

src/Makefile

@@ -27,6 +28,7 @@ all: cbmc.dir \
     goto-cc.dir \
     goto-diff.dir \
     goto-instrument.dir \
+		 goto-harness.dir \


Wrong indent or tabs vs spaces issue.

tautschnig · 2019-01-21T22:42:29Z

src/goto-harness/goto_harness_parse_options.cpp

+            << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2019") << '\n'
+            << align_center_with_border("Diffblue Ltd.") << '\n'
+            << align_center_with_border("[email protected]")


We should likely have this align_center_with_border code for everyone...

sonodtt

Looks good! Once again, many thanks for the introduction you give. Awesome.

Very interesting the codesign section of the makefile :)

allredj

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

hannes-steffenhagen-diffblue · 2019-01-25T17:53:11Z

test-gain failures are non-transient (i.e. not going to magically disappear with a force push) but unrelated to this PR

This adds a new executable called goto-harness. Right now it doesn't actually do anything, but ultimately its purpose will be to generate "harness" functions for goto-programs - i.e. given some specification, it'll generate a function suitable as a cbmc entry point function that implements that specification. Planned for now are two types of harnesses: One that takes the name of a function with parameters and then generates a function that sets up these parameters and calls the function with them. This is similar to what cbmc does already, however will allow more flexibility in choosing how exactly these parameters will be initialised which was deemed out of scope for cbmc. The other will be able to take a snapshot of a concrete execution of a program, and then start an analysis from that point.

tautschnig

Repeating my earlier wishlist request: please also add a regression test folder and quite possibly a first regression test, simply running --version (and testing the exit code). That will make this commit a very nice template for future tools.

allredj

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

hannes-steffenhagen-diffblue · 2019-01-25T18:36:36Z

@tautschnig Ah sorry, forgot about that! Yeah that makes sense, I've added this now! (I also checked that the regression test is indeed executed - do you know if there is a good way to ensure this mechanically? The only method I know is deliberately failing a test; Accidentally adding adding tests without making sure they are actually being run has been a problem in the past)

EDIT I forgot to do the makefile version of the regression, adding that now

allredj

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

This merely shows that the goto-harness executable was built (and indeed executable)

allredj

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

allredj

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

allredj

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

hannes-steffenhagen-diffblue added the work in progress label Jan 21, 2019

hannes-steffenhagen-diffblue assigned danpoe and hannes-steffenhagen-diffblue Jan 21, 2019

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners January 21, 2019 17:14

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from 194b8a1 to ad1597d Compare January 21, 2019 17:23

tautschnig reviewed Jan 21, 2019

View reviewed changes

sonodtt approved these changes Jan 22, 2019

View reviewed changes

hannes-steffenhagen-diffblue changed the title ~~Add stub for new goto-harness tool~~ Add stub for new goto-harness tool [depends-on: #3920] Jan 24, 2019

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from ad1597d to f93807a Compare January 24, 2019 17:03

allredj reviewed Jan 25, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from ff0da3a to a07b2cb Compare January 25, 2019 17:39

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from a07b2cb to 9459b30 Compare January 25, 2019 17:55

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from 9459b30 to 30cb51c Compare January 25, 2019 17:56

tautschnig approved these changes Jan 25, 2019

View reviewed changes

allredj reviewed Jan 25, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from 96d7af4 to 4064bc7 Compare January 25, 2019 18:36

allredj reviewed Jan 25, 2019

View reviewed changes

Add goto-harness regression test

7a8d3a8

This merely shows that the goto-harness executable was built (and indeed executable)

hannes-steffenhagen-diffblue force-pushed the feature-goto_harness_stub branch from 4064bc7 to 7a8d3a8 Compare January 25, 2019 18:55

allredj reviewed Jan 25, 2019

View reviewed changes

hannes-steffenhagen-diffblue removed the work in progress label Jan 26, 2019

hannes-steffenhagen-diffblue merged commit d3d19f9 into diffblue:develop Jan 26, 2019

martin-cs mentioned this pull request Jan 28, 2019

Add an output stream to goto-harness for parse_options_baset #3984

Merged

7 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add stub for new goto-harness tool [depends-on: #3920] #3875

Add stub for new goto-harness tool [depends-on: #3920] #3875

Uh oh!

hannes-steffenhagen-diffblue commented Jan 21, 2019 •

edited

Loading

Uh oh!

tautschnig left a comment

Uh oh!

tautschnig Jan 21, 2019

Uh oh!

tautschnig Jan 21, 2019

Uh oh!

hannes-steffenhagen-diffblue Jan 24, 2019

Uh oh!

sonodtt left a comment

Uh oh!

allredj left a comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 25, 2019

Uh oh!

tautschnig left a comment

Uh oh!

allredj left a comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 25, 2019 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Add stub for new goto-harness tool [depends-on: #3920] #3875

Add stub for new goto-harness tool [depends-on: #3920] #3875

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented Jan 21, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 21, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 21, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

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

hannes-steffenhagen-diffblue commented Jan 25, 2019

Uh oh!

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

hannes-steffenhagen-diffblue commented Jan 25, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

Uh oh!

hannes-steffenhagen-diffblue commented Jan 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue commented Jan 25, 2019 •

edited

Loading