Add cover goals verifier [blocks: 3969] #3968

peterschrammel · 2019-01-27T23:05:38Z

Replaces bmc_covert

~~Based on #3796, only review last 10 commits~~

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.

allredj

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

tautschnig · 2019-01-28T09:44:58Z

src/goto-checker/goto_trace_storage.cpp

@@ -25,6 +25,16 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
  return traces.back();
 }

+const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
+{
+  traces.push_back(trace);


Doesn't this require a std::move to make use of the rvalue reference?

tautschnig · 2019-01-28T09:46:14Z

src/goto-checker/goto_trace_storage.h

@@ -21,6 +21,7 @@ class goto_trace_storaget
  goto_trace_storaget(const goto_trace_storaget &) = delete;

  const goto_tracet &insert(goto_tracet &&);
+  const goto_tracet &insert_all(goto_tracet &&);


Both of these lack documentation, and given they have the same signature it's not clear what the difference might be.

tautschnig · 2019-01-28T09:48:36Z

src/goto-checker/cover_goals_report_util.h

+void output_goals(
+  const propertiest &properties,
+  unsigned iterations,
+  ui_message_handlert &ui_message_handler);


Documentation, please. In particular, it's not clear to me what the iterations parameter is good for (the other two intuitively make sense).

tautschnig · 2019-01-28T09:49:42Z

src/goto-checker/cover_goals_report_util.cpp

+    break;
+  }
+  }
+  output_goals_iterations(properties, iterations, log);


What is the rationale that this part is not XML/JSON formatted?

This is current behaviour. Improvement suggestion noted #4013

tautschnig · 2019-01-28T09:53:33Z

regression/cbmc-cover/assertion1/test.desc

-^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
-^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
+^\[main.coverage.1\] file main.c line 9 function main assertion: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main assertion: SATISFIED$


Any idea which commit exactly fixed this? Might be good to merge this change into that other commit.

Squashed and amended commit message

tautschnig · 2019-01-28T10:03:13Z

src/cbmc/c_test_input_generator.cpp

+      if(step.io_args.size() == 1)
+        out << from_expr(ns, "", step.io_args.front());
+    }
+  }


Nowadays I'd actually use

const auto range = make_range(goto_trace.steps).filter( [](const goto_tracet::stept &step) { return step.is_input(); }).map( [](const goto_tracet::stept &step) { return id2string(step.io_id) + '=' + from_expr(ns, step.function_id, step.io_args.front()); }); join_strings(out, range.begin(), range.end(), ", ");

but maybe that's actually less readable...

Either way, there are two problems here: 1) a weird/incomplete output in case step.io_args.size() != 1 and 2) the use of "" in from_expr, which should use step.function_id instead.

tautschnig · 2019-01-28T10:03:50Z

src/cbmc/c_test_input_generator.cpp

+
+  if(print_trace)
+  {
+    // currently ignored


The comment in the header file suggests otherwise!

tautschnig · 2019-01-28T10:04:55Z

src/cbmc/c_test_input_generator.cpp

+    {
+      json_objectt json_input({{"id", json_stringt(step.io_id)}});
+      if(step.io_args.size() == 1)
+        json_input["value"] = json(step.io_args.front(), ns, ID_unknown);


Use ns.lookup(step.function_id).mode instead of ID_unknown.

This is useful for retrieving all coverage goals covered by a trace.

std::move was missing.

allredj

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

forejtv · 2019-02-01T14:04:27Z

src/goto-checker/goto_trace_storage.cpp

+const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
+{
+  traces.push_back(std::move(trace));
+  for(const auto &property_id : traces.back().get_all_property_ids())


Do you expect insert_all to ever be called on a trace hitting no properties? If not, can you add an invariant that traces.back().get_all_property_ids() is non-empty?

There wouldn't be a trace of no property was hit, but right, this invariant is quite far away from this place. I'll add it.

Coverage traces cover several properties.

The output for --cover is quite different from verification. These functions should be moved into the prospective ccover tool.

Replaces the goal covering and trace generation part of bmc_covert. Does not produce any test output. May be moved into a prospective ccover tool.

Replaces the test input extraction part of bmc_covert, which is entirely independent of producing traces now. To be moved into a prospective ccover tool.

instead of bmc_covert Fixes --cover tests without property descriptions. The unified property handling introduced in a1100e1 used by goto verifier does not allow properties without description.

w.r.t. cover goals verifier

allredj

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

peterschrammel added dependent - do not merge Goto-checker labels Jan 27, 2019

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, NathanJPhillips, pkesseli, smowton, tautschnig and thk123 as code owners January 27, 2019 23:05

peterschrammel force-pushed the cover-verifier branch 2 times, most recently from 28305eb to 997f125 Compare January 28, 2019 00:29

allredj reviewed Jan 28, 2019

View reviewed changes

tautschnig approved these changes Jan 28, 2019

View reviewed changes

tautschnig assigned peterschrammel Jan 28, 2019

peterschrammel changed the title ~~Add cover goals verifier [depends: 3796]~~ Add cover goals verifier [depends: 3796, blocks: 3969] Jan 28, 2019

peterschrammel added the blocker label Jan 28, 2019

peterschrammel mentioned this pull request Jan 31, 2019

Improvement suggestions for CBMC output #4013

Open

peterschrammel force-pushed the cover-verifier branch 3 times, most recently from e26526d to 29e1def Compare January 31, 2019 23:35

tautschnig removed the dependent - do not merge label Feb 1, 2019

tautschnig changed the title ~~Add cover goals verifier [depends: 3796, blocks: 3969]~~ Add cover goals verifier [blocks: 3969] Feb 1, 2019

peterschrammel added 3 commits February 1, 2019 10:21

Inline in class declaration is implicit

52f813e

Get all property IDs from a trace

92cceff

This is useful for retrieving all coverage goals covered by a trace.

Fix and document goto trace storage insert

67b2588

std::move was missing.

peterschrammel force-pushed the cover-verifier branch 3 times, most recently from 138cc67 to 07b1e7b Compare February 1, 2019 11:11

allredj reviewed Feb 1, 2019

View reviewed changes

forejtv reviewed Feb 1, 2019

View reviewed changes

peterschrammel added 7 commits February 1, 2019 14:13

Extend goto trace storage to coverage traces

cb9e287

Coverage traces cover several properties.

Add reporting utils for covering goals

7f14fb3

The output for --cover is quite different from verification. These functions should be moved into the prospective ccover tool.

Add goto verifier for covering goals

c4e93de

Replaces the goal covering and trace generation part of bmc_covert. Does not produce any test output. May be moved into a prospective ccover tool.

Fix unit test dependencies

27e3efd

Add C test input generator

5d5d61b

Replaces the test input extraction part of bmc_covert, which is entirely independent of producing traces now. To be moved into a prospective ccover tool.

Use goto verifier for --cover in CBMC

29509e5

instead of bmc_covert Fixes --cover tests without property descriptions. The unified property handling introduced in a1100e1 used by goto verifier does not allow properties without description.

Update goto-checker docs

969f5d6

w.r.t. cover goals verifier

peterschrammel force-pushed the cover-verifier branch from 07b1e7b to 969f5d6 Compare February 1, 2019 14:13

allredj reviewed Feb 1, 2019

View reviewed changes

peterschrammel merged commit c74d257 into diffblue:develop Feb 1, 2019

peterschrammel deleted the cover-verifier branch February 1, 2019 16:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add cover goals verifier [blocks: 3969] #3968

Add cover goals verifier [blocks: 3969] #3968

Uh oh!

peterschrammel commented Jan 27, 2019 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

peterschrammel Jan 31, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

peterschrammel Jan 31, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

tautschnig Jan 28, 2019

Uh oh!

allredj left a comment

Uh oh!

forejtv Feb 1, 2019

Uh oh!

peterschrammel Feb 1, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Add cover goals verifier [blocks: 3969] #3968

Add cover goals verifier [blocks: 3969] #3968

Uh oh!

Conversation

peterschrammel commented Jan 27, 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!

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!

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!

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!

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!

Uh oh!

peterschrammel commented Jan 27, 2019 •

edited

Loading