Incremental unwinding of one specified loop -- rebase #5217

xbauch · 2020-01-27T16:52:25Z

Incremental unwinding and assertion checking of a specified loop.

This is a rebase of #4361.

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.

codecov-io · 2020-01-27T18:09:38Z

Codecov Report

Merging #5217 into develop will increase coverage by 0.07%.
The diff coverage is 92.71%.

@@             Coverage Diff             @@
##           develop    #5217      +/-   ##
===========================================
+ Coverage    67.43%   67.51%   +0.07%     
===========================================
  Files         1157     1161       +4     
  Lines        95351    95495     +144     
===========================================
+ Hits         64303    64476     +173     
+ Misses       31048    31019      -29

Flag	Coverage Δ
#cproversmt2	`42.59% <8.6%> (-0.09%)`	⬇️
#regression	`64.04% <92.71%> (+0.08%)`	⬆️
#unit	`31.9% <6.62%> (-0.06%)`	⬇️

Impacted Files	Coverage Δ
src/goto-symex/goto_symex.h	`91.66% <ø> (ø)`	⬆️
src/goto-symex/symex_target_equation.h	`92.3% <ø> (ø)`	⬆️
src/goto-symex/symex_main.cpp	`87.74% <100%> (ø)`	⬆️
src/goto-symex/symex_goto.cpp	`96.6% <100%> (+0.05%)`	⬆️
...to-checker/single_loop_incremental_symex_checker.h	`100% <100%> (ø)`
src/goto-checker/symex_bmc_incremental_one_loop.h	`100% <100%> (ø)`
src/goto-checker/goto_symex_property_decider.cpp	`100% <100%> (+3.22%)`	⬆️
src/goto-symex/symex_target_equation.cpp	`95.69% <85.71%> (+0.52%)`	⬆️
src/cbmc/cbmc_parse_options.cpp	`75.65% <89.47%> (+0.58%)`	⬆️
...-checker/single_loop_incremental_symex_checker.cpp	`92.1% <92.1%> (ø)`
... and 12 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 5b4bcc6...eebfcd9. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-01-28T10:41:14Z

@tautschnig Were your comments from #4361 addressed?

thk123

Comments from @tautschnig on original PR that are still outstanding

src/goto-symex/symex_target_equation.cpp

src/goto-symex/goto_symex.h

regression/cbmc-incr-oneloop/Makefile

thk123 · 2020-01-29T10:19:25Z

src/goto-checker/symex_bmc_incremental_one_loop.cpp

+                                   : 0)
+{
+  ignore_assertions =
+    options.get_bool_option("ignore-properties-before-unwind-min");


Perhaps a question for @peterschrammel

When was this option introduced and where is it documented?

#4361 (comment)

It has been introduced as part of this PR. Maybe it hasn't been documented as part of thIs PR, though.

Hmm, seems to be documented here @tautschnig : https://github.com/diffblue/cbmc/pull/5217/files#diff-e58a25459f0e8ca5a6c351b1d9d75167R225

Suggested change

options.get_bool_option("ignore-properties-before-unwind-min");

incr_min_unwind >= 2 && options.get_bool_option("ignore-properties-before-unwind-min");

@peterschrammel or at least this way it was in 5.4.

Any observable effect of adding this?

Well since the test(s) in question do not set the unwind-min I assume it is 1 by default. So the ignoring would not even occur. So yes, the test passes, but rather trivially.

On the other hand, the test is still wrong if you set the unwind-min (to 10 for example) even with the suggested change.

thk123 · 2020-01-29T10:32:12Z

Niavely looking at coverage we should add the following tests:

a pretty shortest trace (e.g. with --beautify turned on for one of the tests)
building a non-shortest trace for a property
building a full trace

(dunno how you exercise those last two options)

Also, we should add a trivial test for checking exit with non-zero exit code if ran with --paths as well as --incremental-loop just to stop any boneheaded mistakes in future

Also, less nit picky, but it seems like symex_bmc_incremental_one_loopt is not tested with any loop_unwind_handlers. This seems like it should be added

Cannot be used with incremental loop unwinding.

not 'ignore' (which is used for slicing).

Allows ignoring assertions until a certain condition is satisfied (e.g. a certain unwinding is reached). Used for implementation of ignore-assertions-before-unwind-min.

This enables the caller to handle assertion conversion differently, e.g. for incremental loop unwinding.

We can ignore already failed properties.

Required for incremental loop unwinding.

Implement callback that decides on when to interrupt goto-symex during incremental unwinding.

Checks the assertions after each iteration of a specified loop.

for incremental unwinding and assertion checking of a specified loop.

Otherwise single quotes get incorrectly stripped off.

This seems to work when calling bash again. Otherwise, we can get something like: This is half a liEXIT=123

Option name has changed.

These require more options that have not been implemented yet.

Allows to check assertions only between unwind-min and unwind-max iterations of a specified loop.

thk123

AFAICT all of @tautschnig comments from #4361 have been addressed.

thk123 · 2020-01-29T16:36:20Z

src/goto-symex/goto_symex.h

+  /// \param unwind: current unwinding counter
+  /// \return true if the symbolic execution is to be interrupted for checking
+  virtual bool check_break(
+    const irep_idt &id,


⛏️ is this the loop id? given how frequent ids are used in this code base, I'd probably call it loop_id

xbauch · 2020-01-29T16:40:28Z

a pretty shortest trace (e.g. with --beautify turned on for one of the tests)

It seems that the refinement solver does not support beatification

xbauch · 2020-01-29T17:02:57Z

a pretty shortest trace (e.g. with --beautify turned on for one of the tests)

building a non-shortest trace for a property

building a full trace

I have a suspicion that some of the build_*trace functions are only there to override the default and cannot really be called in any of our factory-produced verifiers. I'll keep digging.

`check_break` is now documented in `goto_symex.h` as well (I removed the parameters that were not used anywhere).

xbauch · 2020-01-31T16:36:40Z

@peterschrammel In an attempt to improve coverage, the last commit adds a test for trace production. I've also suggested commenting out the implementation of the "beautified" trace and the "full" trace since I don't think they can be exercised by any of the current verifier combinations. Is it change acceptable?

peterschrammel · 2020-01-31T16:38:53Z

src/goto-checker/single_loop_incremental_symex_checker.cpp

-    goto_trace);
-
-  return goto_trace;
+  UNREACHABLE;


🚫 Write a test for it if you want to cover it.

1: working test for the standard trace. 2: failing test for the beautified shortest trace.

thk123 · 2020-02-04T17:16:38Z

regression/cbmc-incr-oneloop/ignore-before-unwind/main.c

@@ -0,0 +1,14 @@
+int main()


⛏️ typo in commit message KNOWBUG -> KNOWNBUG

thk123 · 2020-02-04T17:20:00Z

regression/cbmc-incr-oneloop/alarm2/fancy_trace_test.desc

+--
+^warning: ignoring
+--
+This will fail the invariant on `build_goto_trace.cpp:320` asserting certain


Could you raise a bug on cbmc and put the issue number here.

thk123 · 2020-02-04T17:20:24Z

regression/cbmc-incr-oneloop/alarm2/trace_test.desc

+^VERIFICATION FAILED$
+^State \d+ file main.c function havocIO line 501 thread \d+$
+--
+^warning: ignoring


A description of why you added this test (e.g. tests the trace production for ??)

thk123 · 2020-02-04T18:02:02Z

Maybe you already knew this, but the key flag is --ignore-properties-before-unwind-min, disabling that causes it to find the failure

peterschrammel · 2020-02-05T13:31:31Z

regression/cbmc-incr-oneloop/ignore-before-unwind/main.c

+
+  while(1)
+  {
+    __CPROVER_assume(property == 1);


What is the purpose of the unused assumption variable?

Hard to say, but if you comment it out, it suddenly starts to work.

I mean the assumption variable, not the assumption statement.

Sorry, yes, that one is irrelevant.

Basically, if unwind-min is zero (by default) the first loop iterations should not be ignored (even if requested). Tests show the problem.

xbauch · 2020-02-05T14:45:05Z

@peterschrammel I've added the check for when to start ignoring properties (eebfcd9) and cleaned up the test.

martin-cs

If this branch has the history I think it does it might be a candidate for the longest running branch as it predates even VSD!

thk123 · 2020-02-07T11:25:33Z

Just noting the travis job has passed, but for some reason the icon has not refreshed on here

peterschrammel · 2020-02-07T15:52:16Z

regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc

+^Unwinding loop main\.3 iteration 3
+--
+^warning: ignoring
+^Unwinding loop main\.0 iteration 6


Missing new line at end of file

Fixed (I had to rerun the CI anyway).

to a test description file.

xbauch added do not merge do not review labels Jan 27, 2020

xbauch requested review from chrisr-diffblue, kroening, peterschrammel, romainbrenguier, smowton and tautschnig as code owners January 27, 2020 16:52

peterschrammel approved these changes Jan 27, 2020

View reviewed changes

xbauch changed the title ~~[CI-TEST] Incremental one loop rebase~~ Incremental unwinding of one specified loop -- rebase Jan 27, 2020

xbauch removed do not merge do not review labels Jan 27, 2020

thk123 assigned tautschnig Jan 29, 2020

thk123 mentioned this pull request Jan 29, 2020

Incremental unwinding of one specified loop #4361

Closed

7 tasks

thk123 reviewed Jan 29, 2020

View reviewed changes

peterschrammel added 12 commits January 29, 2020 14:37

Allow disabling optimized assertion conversion

c6ee001

Cannot be used with incremental loop unwinding.

Hidden field is used for hiding in trace

d303856

not 'ignore' (which is used for slicing).

Allow symex to temporarily ignore assertions

2b69678

Allows ignoring assertions until a certain condition is satisfied (e.g. a certain unwinding is reached). Used for implementation of ignore-assertions-before-unwind-min.

Allow symex_target_equationt to separately convert assertions

b2925a9

This enables the caller to handle assertion conversion differently, e.g. for incremental loop unwinding.

Use only remaining properties in property decider

96bf769

We can ignore already failed properties.

Add callback to decide on interrupting goto-symex

73941a5

Required for incremental loop unwinding.

Add symex BMC incremental one loop

3ef378d

Implement callback that decides on when to interrupt goto-symex during incremental unwinding.

Add single-loop incremental symex checker

1f5c582

Checks the assertions after each iteration of a specified loop.

Add options for incremental one-loop BMC

fb3674b

for incremental unwinding and assertion checking of a specified loop.

Add --incremental-loop to CBMC

6fe6359

for incremental unwinding and assertion checking of a specified loop.

Fix quoting in test command

85b0e82

Otherwise single quotes get incorrectly stripped off.

Make sure output buffers are flushed before writing exit code

666606c

This seems to work when calling bash again. Otherwise, we can get something like: This is half a liEXIT=123

peterschrammel added 4 commits January 29, 2020 14:37

Clean up cbmc-incr-oneloop tests

772084f

Option name has changed.

Set induction tests to FUTURE

732814c

These require more options that have not been implemented yet.

Clang-format cbmc-incr-oneloop tests

dfbc0d4

Ignore properties before unwind min

8fb9cd3

Allows to check assertions only between unwind-min and unwind-max iterations of a specified loop.

xbauch force-pushed the incremental-one-loop-rebase branch 2 times, most recently from 46dad61 to 3bcb5ff Compare January 29, 2020 16:36

thk123 approved these changes Jan 29, 2020

View reviewed changes

xbauch force-pushed the incremental-one-loop-rebase branch from 3bcb5ff to efd8ffe Compare January 30, 2020 16:21

Add documentation and refactor incremental one loop changes

07e3177

`check_break` is now documented in `goto_symex.h` as well (I removed the parameters that were not used anywhere).

xbauch force-pushed the incremental-one-loop-rebase branch from efd8ffe to 6db9447 Compare January 30, 2020 17:01

peterschrammel requested changes Jan 31, 2020

View reviewed changes

xbauch force-pushed the incremental-one-loop-rebase branch from 6db9447 to d91d9d9 Compare February 4, 2020 10:47

Add tests for traces in one-loop checker

39c5ac8

1: working test for the standard trace. 2: failing test for the beautified shortest trace.

xbauch force-pushed the incremental-one-loop-rebase branch from d91d9d9 to 39c5ac8 Compare February 4, 2020 10:49

xbauch requested a review from peterschrammel February 4, 2020 10:49

thk123 reviewed Feb 4, 2020

View reviewed changes

peterschrammel reviewed Feb 5, 2020

View reviewed changes

xbauch force-pushed the incremental-one-loop-rebase branch from 3e2ad1c to dff27a3 Compare February 5, 2020 14:40

Fix ignoring properties before unwind min (off-by-one)

eebfcd9

Basically, if unwind-min is zero (by default) the first loop iterations should not be ignored (even if requested). Tests show the problem.

xbauch force-pushed the incremental-one-loop-rebase branch from dff27a3 to eebfcd9 Compare February 5, 2020 14:42

martin-cs approved these changes Feb 6, 2020

View reviewed changes

peterschrammel approved these changes Feb 7, 2020

View reviewed changes

Add missing newline symbol

ca7dc8c

to a test description file.

xbauch merged commit d51243d into diffblue:develop Feb 11, 2020

	options.get_bool_option("ignore-properties-before-unwind-min");
	incr_min_unwind >= 2 && options.get_bool_option("ignore-properties-before-unwind-min");

Incremental unwinding of one specified loop -- rebase #5217

Incremental unwinding of one specified loop -- rebase #5217

Uh oh!

Conversation

xbauch commented Jan 27, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov-io commented Jan 27, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

hannes-steffenhagen-diffblue commented Jan 28, 2020

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

thk123 commented Jan 29, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

xbauch commented Jan 29, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

xbauch commented Jan 29, 2020

Uh oh!

xbauch commented Jan 31, 2020

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!

thk123 commented Feb 4, 2020

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!

xbauch commented Feb 5, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented Feb 7, 2020

Uh oh!

Choose a reason for hiding this comment

xbauch commented Jan 27, 2020 •

edited

Loading

codecov-io commented Jan 27, 2020 •

edited

Loading

thk123 commented Jan 29, 2020 •

edited

Loading

xbauch commented Jan 29, 2020 •

edited

Loading