Incremental unwinding of one specified loop #4361

peterschrammel · 2019-03-10T18:28:32Z

Incremental unwinding and assertion checking of a specified loop.

~~Based on #4054~~

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 · 2019-03-11T06:10:29Z

regression/test.pl

@@ -65,7 +65,7 @@ ($$)

  chomp @data;
  if($exit_signal_checks) {
-    grep { /^\^EXIT=[\(\|\d]*\d+\)?\$$/ } @data or die "$fname: Missing EXIT test\n";
+    grep { /^\^?EXIT=[\(\|\d]*\d+\)?\$$/ } @data or die "$fname: Missing EXIT test\n";


I'm aware this is work-in-progress, but I'd really like to get a better understanding of what's going on here. The EXIT=... output is generated by test.pl itself. If that isn't at the beginning of a line, then something else has gone wrong.

Still experimenting with that. I have some tests that succeed when they are killed by a timeout. In that case the EXIT output can get appended to whatever line is being printed at that moment. Surprisingly, printing \nEXIT... in test.pl doesn't put it on a new line either...

Is that a race condition with some buffers only being flushed? You might try doing

$| = 1; print "\n";

before it's printing EXIT.

Just noting: this change no longer appears in #5217

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d3b9962).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106452418
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

martin-cs

I think I am only listed as a reviewer due to the base patch. If this is not the case and when this is ready; give me a shout and I will review.

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.

allredj

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

chrisr-diffblue · 2019-06-07T10:58:35Z

regression/cbmc-incr-oneloop/alarm1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
--incremental-check main.0 --unwind-max 25 --no-unwinding-assertions
+--incremental-loop main.0 --unwind-max 15


Is --increment-check still needed/tested somewhere?

The tests have been in the codebase without the actual implementation (= this PR). We decided to give the option a different name now.

chrisr-diffblue · 2019-06-07T11:32:04Z

regression/cbmc-incr-oneloop/unwind-forever2/test.desc

+--
+Tests whether goto-symex does not stop early when it cannot figure out the
+loop bound and there is no error in the loop.
+Mac OS exit code is 14


Why are the exit codes different? Is the exit code not under our control in this situation? What process is receiving the SIGALRM - perl, or cbmc? or something else?

perl - the exit codes seem to be different on linux vs mac os.

chrisr-diffblue · 2019-06-07T11:37:24Z

regression/test.pl

-  print $FH "EXIT=$exit_value\n";
-  print $FH "SIGNAL=$signal_num\n";
-  close $FH;
+  system("bash", "-c", "cd '$name' ; echo '\nEXIT=$exit_value\nSIGNAL=$signal_num\n' >> '$output'");


This seems annoyingly messy and fragile - why has this not shown up before now - or is it related to the signal handling for sigalrm?

It's related to sigalrm. That was the only robust way of getting the second output appended to the file without losing the leading newline (see discussion with @tautschnig above).
In the end I'm not sure it's worth the hassle. Probably I should just remove these two tests.

chrisr-diffblue · 2019-06-07T11:41:14Z

src/goto-checker/single_loop_incremental_symex_checker.h

+  symbol_tablet symex_symbol_table;
+  namespacet ns;
+  symex_target_equationt equation;
+  path_fifot path_storage; // should go away


Is this something that should be tracked as a github Issue? If so, a reference to that issue here would nice :-)

tautschnig · 2019-06-11T16:26:59Z

src/goto-symex/goto_symex.h

@@ -197,6 +197,10 @@ class goto_symext
  /// symbolic execution from that state.
  bool should_pause_symex;

+  /// If this flag is set to true then assertions will be temporarily ignored
+  /// by the symbolic executions.


What exactly does "ignored" mean? Any why is this ever the right thing to do?

tautschnig · 2019-06-11T16:29:56Z

src/goto-symex/symex_target_equation.cpp

@@ -468,7 +468,7 @@ void symex_target_equationt::convert_assertions(
    {
      // ignore already converted assertions in the error trace
      if(step.is_assert() && step.converted)
-        step.ignore = true;
+        step.hidden = true;


That makes the comment above seem rather odd?

tautschnig · 2019-06-11T16:30:04Z

src/goto-symex/symex_target_equation.cpp

@@ -495,7 +495,7 @@ void symex_target_equationt::convert_assertions(
  {
    // ignore already converted assertions in the error trace
    if(step.is_assert() && step.converted)
-      step.ignore = true;
+      step.hidden = true;


tautschnig · 2019-06-11T20:25:09Z

src/goto-symex/symex_target_equation.cpp

+  convert_function_calls(decision_procedure);
+  convert_io(decision_procedure);
+  convert_constraints(decision_procedure);
+}


Could this be refactored so that we don't have almost-the-same-code twice?

tautschnig · 2019-06-11T20:27:01Z

src/goto-symex/goto_symex.h

+    bool is_function,
+    statet &state,
+    const exprt &cond,
+    unsigned unwind);


Documentation?

tautschnig · 2019-06-11T20:27:30Z

src/goto-symex/symex_goto.cpp

+      if(check_break(loop_id, false, state, new_guard, unwind))
+      {
+        should_pause_symex = true;
+      }


Why is this only done in the new_guard.is_true() case? What about a non-constant guard for a backwards-goto?

tautschnig · 2019-06-11T20:29:28Z

src/goto-checker/bmc_util.h

@@ -188,7 +188,10 @@ void run_property_decider(
  "(unwind):" \
  "(unwindset):" \
  "(graphml-witness):" \
-  "(unwindset):"


I was confused at first - maybe we should have a separate commit that cleans up this duplicate (unwindset):?

tautschnig · 2019-06-11T20:31:11Z

regression/cbmc-incr-oneloop/Makefile

@@ -1,10 +1,10 @@
 default: tests.log

 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"


Why is there a perl -e wrapper for those tests?

for the timeout

I think a comment would be nice to have.

tautschnig · 2019-06-11T20:33:36Z

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -35,6 +35,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
      options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min")
                                   : 0)
 {
+  ignore_assertions =
+    options.get_bool_option("ignore-properties-before-unwind-min");


When was this option introduced and where is it documented?

tautschnig · 2021-01-25T00:35:12Z

@peterschrammel Is there still anything left to be merged here?

peterschrammel · 2021-01-25T10:58:15Z

No, this has been fully merged by another PR.

peterschrammel added work in progress dependent - do not merge Goto-checker labels Mar 10, 2019

peterschrammel requested review from chrisr-diffblue, kroening, martin-cs, smowton and tautschnig as code owners March 10, 2019 18:28

peterschrammel self-assigned this Mar 10, 2019

peterschrammel force-pushed the incremental-one-loop branch from 66a2e73 to df73a7b Compare March 10, 2019 21:26

tautschnig reviewed Mar 11, 2019

View reviewed changes

peterschrammel force-pushed the incremental-one-loop branch from df73a7b to 55e695c Compare March 11, 2019 11:22

peterschrammel force-pushed the incremental-one-loop branch 2 times, most recently from e85459d to 5fadf38 Compare March 29, 2019 13:21

peterschrammel requested review from allredj, cesaro, cristina-david, danpoe, hannes-steffenhagen-diffblue, pkesseli and romainbrenguier as code owners March 29, 2019 13:21

peterschrammel force-pushed the incremental-one-loop branch 2 times, most recently from ff84207 to 49606e6 Compare March 29, 2019 22:38

peterschrammel changed the title ~~[WIP] Incremental unwinding of one specified loop [depends: 4054]~~ Incremental unwinding of one specified loop [depends: 4054] Mar 29, 2019

peterschrammel removed the work in progress label Mar 29, 2019

peterschrammel force-pushed the incremental-one-loop branch 2 times, most recently from 012f82a to d3b9962 Compare March 30, 2019 22:27

allredj reviewed Mar 31, 2019

View reviewed changes

martin-cs reviewed Apr 1, 2019

View reviewed changes

peterschrammel mentioned this pull request Apr 11, 2019

decision_proceduret interface #4497

Merged

3 tasks

peterschrammel added 14 commits June 7, 2019 10:51

Allow symex to temporarily ignore assertions

1fb7d2d

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

73fb826

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

Use only remaining properties in property decider

41d3864

We can ignore already failed properties.

Add callback to decide on interrupting goto-symex

7fbc6b0

Required for incremental loop unwinding.

Add symex BMC incremental one loop

2a7b16c

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

Add single-loop incremental symex checker

cef212c

Checks the assertions after each iteration of a specified loop.

Add options for incremental one-loop BMC

4e894a4

for incremental unwinding and assertion checking of a specified loop.

Add --incremental-loop to CBMC

d7581bd

for incremental unwinding and assertion checking of a specified loop.

Fix quoting in test command

30ca986

Otherwise single quotes get incorrectly stripped off.

Make sure output buffers are flushed before writing exit code

aa1389b

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

Clean up cbmc-incr-oneloop tests

657a899

Option name has changed.

Set induction tests to FUTURE

cc60ab3

These require more options that have not been implemented yet.

Clang-format cbmc-incr-oneloop tests

f1af977

Ignore properties before unwind min

20613e8

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

peterschrammel force-pushed the incremental-one-loop branch from 3f41327 to 20613e8 Compare June 7, 2019 09:58

peterschrammel assigned tautschnig and chrisr-diffblue and unassigned peterschrammel Jun 7, 2019

allredj reviewed Jun 7, 2019

View reviewed changes

chrisr-diffblue reviewed Jun 7, 2019

View reviewed changes

tautschnig reviewed Jun 11, 2019

View reviewed changes

tautschnig assigned peterschrammel Jun 11, 2019

xbauch mentioned this pull request Jan 27, 2020

Incremental unwinding of one specified loop -- rebase #5217

Merged

7 tasks

tautschnig added the Needs rebase label Jan 25, 2021

tautschnig unassigned tautschnig and chrisr-diffblue Jan 25, 2021

peterschrammel closed this Jan 25, 2021

peterschrammel deleted the incremental-one-loop branch January 25, 2021 10:58

Incremental unwinding of one specified loop #4361

Incremental unwinding of one specified loop #4361

Uh oh!

Conversation

peterschrammel commented Mar 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

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!

peterschrammel Jun 8, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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!

tautschnig commented Jan 25, 2021

Uh oh!

peterschrammel commented Jan 25, 2021

Uh oh!

Uh oh!

peterschrammel commented Mar 10, 2019 •

edited

Loading

peterschrammel Jun 8, 2019 •

edited

Loading