use code_blockt::statements() where appropriate #2830

kroening · 2018-08-23T19:32:19Z

add/move are type-safe; copy_to_operands and move_to_operands are not.

kroening · 2018-08-24T08:59:38Z

I'll clang-format once reviewed; it's easier to review without.

thk123

This would I suppose be a good time to apply this change in TG as well - how urgently do you want to get this in? It still needs a bump and I'd rather not see the introduction of synonym methods (labelled ❓ )

thk123 · 2018-08-24T09:29:36Z

src/util/std_code.h

@@ -118,12 +118,12 @@ class code_blockt:public codet

  void move(codet &code)
  {
-    move_to_operands(code);
+    exprt::move_to_operands(code);


What's the reason for this change?

thk123 · 2018-08-24T09:50:15Z

src/util/std_code.h

@@ -101,21 +101,39 @@ inline codet &to_code(exprt &expr)
 class code_blockt:public codet
 {
 public:
+  typedef std::vector<codet> code_operandst;
+
+  code_operandst &code_operands()


❓ What's the purpose of having both code_operands() and statements()?

The idea is to eventually have code_operands() in codet, once codet stops inheriting from exprt.

kroening · 2018-08-24T10:39:05Z

No genuine urgency to do this on TG.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 658c93f).
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).

tautschnig · 2018-09-04T13:57:01Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -787,16 +787,16 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
    return this_block;

  // Find the child code_blockt where the queried range begins:
-  auto child_iter=this_block.operands().begin();
+  auto child_iter=this_block.statements().begin();


Throughout this commit: please weave in clang-format style spacing while touching the various lines.

tautschnig · 2018-09-04T13:57:19Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

    ++child_iter;
-  assert(child_iter!=this_block.operands().end());
+  assert(child_iter!=this_block.statements().end());


Should be a DATA_INVARIANT

tautschnig · 2018-09-04T13:58:20Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

  std::advance(child_iter, child_offset);
-  assert(child_iter!=this_block.operands().end());
-  auto &child_label=to_code_label(to_code(*child_iter));
+  assert(child_iter!=this_block.statements().end());


This assert actually never was good enough as far as I can tell: the iterator should have been advanced well beyond the end() iterator.

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

allredj

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

smowton · 2018-10-14T15:47:14Z

src/goto-instrument/goto_program2code.cpp

-static bool move_label_ifthenelse(
-    exprt &expr,
-    exprt &label_dest)
+static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)


Unrelated changes?

That was clang-format.

allredj

Passed Diffblue compatibility checks (cbmc commit: 7813fec).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87882190

martin-cs

goto-instrument changes look fine.

This avoids a runtime check that the operand is codet.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: ec1b59a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88419397
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: 5dceb25).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88420660
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

Passed Diffblue compatibility checks (cbmc commit: 01fd831).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88424313

kroening added the cleanup label Aug 23, 2018

kroening requested review from thk123, tautschnig and peterschrammel August 23, 2018 19:32

kroening requested review from cesaro, chrisr-diffblue, cristina-david, martin-cs, mgudemann, NathanJPhillips, pkesseli and smowton as code owners August 23, 2018 19:32

kroening force-pushed the code_block_move_add branch from 62eafff to 3dd0a63 Compare August 24, 2018 08:59

kroening assigned thk123 and peterschrammel Aug 24, 2018

thk123 reviewed Aug 24, 2018

View reviewed changes

tautschnig assigned kroening and unassigned thk123 and peterschrammel Sep 3, 2018

tautschnig added the Needs rebase label Sep 3, 2018

kroening force-pushed the code_block_move_add branch from 3dd0a63 to 658c93f Compare September 3, 2018 15:21

kroening removed the Needs rebase label Sep 3, 2018

kroening assigned thk123 and unassigned kroening Sep 3, 2018

allredj reviewed Sep 4, 2018

View reviewed changes

tautschnig reviewed Sep 4, 2018

View reviewed changes

kroening force-pushed the code_block_move_add branch from 658c93f to b8d45ef Compare September 30, 2018 11:11

kroening mentioned this pull request Sep 30, 2018

use code_blockt::add and ::move for adding a statement #3067

Merged

7 tasks

tautschnig approved these changes Oct 8, 2018

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated Show resolved Hide resolved

tautschnig assigned kroening and unassigned tautschnig Oct 8, 2018

kroening force-pushed the code_block_move_add branch from 2311e72 to 361bba3 Compare October 11, 2018 10:17

allredj reviewed Oct 11, 2018

View reviewed changes

kroening force-pushed the code_block_move_add branch from 361bba3 to 7813fec Compare October 14, 2018 13:45

kroening assigned smowton and unassigned kroening Oct 14, 2018

smowton approved these changes Oct 14, 2018

View reviewed changes

allredj reviewed Oct 14, 2018

View reviewed changes

tautschnig assigned kroening, martin-cs and chrisr-diffblue and unassigned smowton and thk123 Oct 14, 2018

martin-cs approved these changes Oct 15, 2018

View reviewed changes

tautschnig unassigned peterschrammel, martin-cs and chrisr-diffblue Oct 15, 2018

tautschnig added the Needs rebase label Oct 15, 2018

kroening force-pushed the code_block_move_add branch from 7813fec to ec1b59a Compare October 18, 2018 13:31

kroening removed the Needs rebase label Oct 18, 2018

kroening force-pushed the code_block_move_add branch from ec1b59a to 5dceb25 Compare October 18, 2018 13:33

use code_blockt::statements() where appropriate

01fd831

This avoids a runtime check that the operand is codet.

kroening force-pushed the code_block_move_add branch from 5dceb25 to 01fd831 Compare October 18, 2018 13:34

allredj reviewed Oct 18, 2018

View reviewed changes

kroening merged commit 68a0b70 into develop Oct 20, 2018

kroening deleted the code_block_move_add branch October 20, 2018 09:09

use code_blockt::statements() where appropriate #2830

use code_blockt::statements() where appropriate #2830

Uh oh!

Conversation

kroening commented Aug 23, 2018

Uh oh!

kroening commented Aug 24, 2018

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!

Choose a reason for hiding this comment

Uh oh!

kroening commented Aug 24, 2018

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!

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!

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!

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!