added code_blockt::statements(), which is a vector of codet #3080

kroening · 2018-10-02T10:14:11Z

The key benefit is that clients no longer need to do conversion of the
operands to codet.

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.

smowton · 2018-10-02T10:16:44Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

-  while(child_iter!=this_block.operands().end() &&
-        to_code(*child_iter).get_statement()==ID_decl)
+  while(child_iter != this_block.statements().end() &&
+        to_code(*child_iter).get_statement() == ID_decl)


to_code not longer needed

smowton · 2018-10-02T10:17:18Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

  assert(tree.branch.size()==this_block_children.size());
  for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
      blockidx!=blocklim;
      ++blockidx)
    newblock.move_to_operands(this_block_children[blockidx]);

  // Relabel the inner header:
-  to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
+  to_code_label(to_code(newblock.statements()[0])).set_label(new_label_irep);


smowton · 2018-10-02T10:17:41Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1845,7 +1845,7 @@ codet java_bytecode_convert_methodt::convert_instructions(

    if(c.get_statement()!=ID_skip)
    {
-      auto &lastlabel=to_code_label(to_code(root_block.operands().back()));
+      auto &lastlabel = to_code_label(to_code(root_block.statements().back()));


allredj

Passed Diffblue compatibility checks (cbmc commit: 4a6119a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86588721

tautschnig

Overall ok with me, some more suggestions below.

tautschnig · 2018-10-02T12:28:07Z

src/goto-instrument/goto_program2code.cpp

-      to_code(block.operands().back()).get_statement()!=ID_label)
+  if(
+    !block.has_operands() ||
+    block.statements().back().get_statement() != ID_label)
    return false;


Nit pick: please add braces for readability

tautschnig · 2018-10-02T12:28:46Z

src/cpp/cpp_constructor.cpp

      return to_code(initializer);
    else
    {
-      block.move_to_operands(initializer);
+      block.add(to_code(initializer));


I think it would be worth moving this use of to_code further up.

tautschnig · 2018-10-02T12:29:35Z

src/util/std_code.h

+
+  code_operandst &statements()
+  {
+    return (code_operandst &)get_sub();


Use static_cast

That doesn't work, the C++ type system isn't that elaborate.

The key benefit is that clients no longer need to do conversion of the operands to codet.

allredj

Passed Diffblue compatibility checks (cbmc commit: 7d8b70c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86610791

peterschrammel · 2018-10-06T21:43:23Z

src/util/std_code.h

  explicit code_blockt(const std::list<codet> &_list):codet(ID_block)
  {
-    operandst &o=operands();
+    auto &o = statements();


ois probably not the best variable name anymore here.

peterschrammel · 2018-10-06T21:44:19Z

src/jsil/jsil_parse_tree.cpp

@@ -22,10 +22,8 @@ static bool insert_at_label(
  const irep_idt &label,
  code_blockt &dest)
 {
-  Forall_operands(it, dest)
+  for(auto &c : dest.statements())


What does c stand for?

kroening added the cleanup label Oct 2, 2018

kroening assigned smowton and tautschnig Oct 2, 2018

kroening requested review from smowton and tautschnig October 2, 2018 10:14

kroening requested review from cesaro, chrisr-diffblue, cristina-david, martin-cs, NathanJPhillips, peterschrammel, pkesseli and thk123 as code owners October 2, 2018 10:14

kroening changed the title ~~added code_blockt::statenents(), which is a vector of codet~~ added code_blockt::statements(), which is a vector of codet Oct 2, 2018

kroening force-pushed the code_blockt_operands branch from 380ad23 to bc925a1 Compare October 2, 2018 10:14

smowton reviewed Oct 2, 2018

View reviewed changes

kroening force-pushed the code_blockt_operands branch from bc925a1 to 4a6119a Compare October 2, 2018 10:20

allredj reviewed Oct 2, 2018

View reviewed changes

tautschnig approved these changes Oct 2, 2018

View reviewed changes

tautschnig assigned kroening and peterschrammel and unassigned smowton and tautschnig Oct 2, 2018

kroening removed their assignment Oct 2, 2018

added code_blockt::statements(), which is a vector of codet

7d8b70c

The key benefit is that clients no longer need to do conversion of the operands to codet.

kroening force-pushed the code_blockt_operands branch from 4a6119a to 7d8b70c Compare October 2, 2018 13:25

kroening assigned smowton Oct 2, 2018

smowton approved these changes Oct 2, 2018

View reviewed changes

allredj reviewed Oct 2, 2018

View reviewed changes

kroening unassigned smowton Oct 2, 2018

kroening assigned chrisr-diffblue Oct 6, 2018

peterschrammel approved these changes Oct 6, 2018

View reviewed changes

peterschrammel removed their assignment Oct 6, 2018

tautschnig assigned kroening and unassigned chrisr-diffblue Oct 7, 2018

kroening merged commit 2dc9574 into develop Oct 7, 2018

kroening deleted the code_blockt_operands branch October 7, 2018 16:11

added code_blockt::statements(), which is a vector of codet #3080

added code_blockt::statements(), which is a vector of codet #3080

Uh oh!

Conversation

kroening commented Oct 2, 2018

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!

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

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!

Uh oh!