better typing for statements in code_blockt

Author: Daniel Kroening

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();
   // Skip any top-of-block declarations;
   // all other children are labelled subblocks.
-  while(child_iter!=this_block.operands().end() &&
-        to_code(*child_iter).get_statement()==ID_decl)
+  while(child_iter!=this_block.statements().end() &&
+        child_iter->get_statement()==ID_decl)
     ++child_iter;
-  assert(child_iter!=this_block.operands().end());
+  assert(child_iter!=this_block.statements().end());
   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());
+  auto &child_label=to_code_label(*child_iter);
   auto &child_block=to_code_block(child_label.code());
 
   bool single_child(afterstart==findlim);
@@ -866,15 +866,15 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
           << findlim_block_start_address << eom;
 
   // Make a new block containing every child of interest:
-  auto &this_block_children=this_block.operands();
+  auto &this_block_children=this_block.statements();
   assert(tree.branch.size()==this_block_children.size());
   for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
       blockidx!=blocklim;
       ++blockidx)
-    newblock.move(to_code(this_block_children[blockidx]));
+    newblock.move(this_block_children[blockidx]);
 
   // Relabel the inner header:
-  to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
+  to_code_label(newblock.statements()[0]).set_label(new_label_irep);
   // Relabel internal gotos:
   replace_goto_target(newblock, child_label_name, new_label_irep);
 
@@ -1761,15 +1761,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
           if(last_statement.get_statement()==ID_goto)
           {
             // Insert stack twiddling before branch:
-            last_statement.make_block();
-            last_statement.operands().insert(
-              last_statement.operands().begin(),
-              more_code.operands().begin(),
-              more_code.operands().end());
+            auto &block=last_statement.make_block();
+            block.statements().insert(
+              block.statements().begin(),
+              more_code.statements().begin(),
+              more_code.statements().end());
           }
           else
-            forall_operands(o_it, more_code)
-              c.copy_to_operands(*o_it);
+            for(const auto &m_c_s : more_code.statements())
+              to_code_block(c).add(m_c_s);
         }
       }
       a_it2->second.stack=stack;
@@ -1843,7 +1843,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(root_block.statements().back());
       auto &add_to_block=to_code_block(lastlabel.code());
       add_to_block.add(c);
     }
@@ -1907,11 +1907,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
       v.start_pc+v.length,
       std::numeric_limits<unsigned>::max());
     code_declt d(v.symbol_expr);
-    block.operands().insert(block.operands().begin(), d);
+    block.statements().insert(block.statements().begin(), d);
   }
 
-  for(auto &block : root_block.operands())
-    code.move(to_code(block));
+  for(auto &block : root_block.statements())
+    code.move(block);
 
   return code;
 }

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -273,8 +273,9 @@ exprt allocate_dynamic_object_with_decl(
     output_code.add(decl);
   }
 
-  for(const exprt &code : tmp_block.operands())
-    output_code.add(to_code(code));
+  for(const auto &code : tmp_block.statements())
+    output_code.add(code);
+
   return dynamic_object;
 }
 

src/ansi-c/c_typecheck_base.h

@@ -125,7 +125,7 @@ class c_typecheck_baset:
 
   virtual void typecheck_assign(codet &expr);
   virtual void typecheck_asm(codet &code);
-  virtual void typecheck_block(codet &code);
+  virtual void typecheck_block(code_blockt &code);
   virtual void typecheck_break(codet &code);
   virtual void typecheck_continue(codet &code);
   virtual void typecheck_decl(codet &code);

src/ansi-c/c_typecheck_code.cpp

@@ -43,7 +43,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_gcc_switch_case_range)
     typecheck_gcc_switch_case_range(code);
   else if(statement==ID_block)
-    typecheck_block(code);
+    typecheck_block(to_code_block(code));
   else if(statement==ID_decl_block)
   {
   }
@@ -181,23 +181,21 @@ void c_typecheck_baset::typecheck_assign(codet &code)
   implicit_typecast(code.op1(), code.op0().type());
 }
 
-void c_typecheck_baset::typecheck_block(codet &code)
+void c_typecheck_baset::typecheck_block(code_blockt &code)
 {
-  Forall_operands(it, code)
-    typecheck_code(to_code(*it));
+  for(auto &c : code.statements())
+    typecheck_code(c);
 
   // do decl-blocks
 
   code_blockt new_ops;
-  new_ops.operands().reserve(code.operands().size());
+  new_ops.statements().reserve(code.statements().size());
 
-  Forall_operands(it1, code)
+  for(auto &code_op : code.statements())
   {
-    if(it1->is_nil())
+    if(code_op.is_nil())
       continue;
 
-    codet &code_op=to_code(*it1);
-
     if(code_op.get_statement()==ID_label)
     {
       // these may be nested
@@ -217,7 +215,7 @@ void c_typecheck_baset::typecheck_block(codet &code)
       new_ops.move(code_op);
   }
 
-  code.operands().swap(new_ops.operands());
+  code.statements().swap(new_ops.statements());
 }
 
 void c_typecheck_baset::typecheck_break(codet &code)

src/ansi-c/expr2c.cpp

@@ -2840,12 +2840,12 @@ std::string expr2ct::convert_code_block(
   std::string dest=indent_str(indent);
   dest+="{\n";
 
-  forall_operands(it, src)
+  for(const auto &c : src.statements())
   {
-    if(it->get(ID_statement)==ID_label)
-      dest+=convert_code(to_code(*it), indent);
+    if(c.get_statement()==ID_label)
+      dest+=convert_code(c, indent);
     else
-      dest+=convert_code(to_code(*it), indent+2);
+      dest+=convert_code(c, indent+2);
 
     dest+="\n";
   }

src/cpp/cpp_constructor.cpp

@@ -266,7 +266,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
 
     tmp_this=address_of_exprt(object_tc);
 
-    if(block.operands().empty())
+    if(block.statements().empty())
       return to_code(initializer);
     else
     {

src/cpp/cpp_typecheck.h

@@ -420,7 +420,7 @@ class cpp_typecheckt:public c_typecheck_baset
   virtual void typecheck_try_catch(codet &code);
   virtual void typecheck_member_initializer(codet &code);
   virtual void typecheck_decl(codet &code);
-  virtual void typecheck_block(codet &code);
+  virtual void typecheck_block(code_blockt &code);
   virtual void typecheck_ifthenelse(code_ifthenelset &code);
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_switch(code_switcht &code);

src/cpp/cpp_typecheck_code.cpp

@@ -447,7 +447,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
   code.swap(new_code);
 }
 
-void cpp_typecheckt::typecheck_block(codet &code)
+void cpp_typecheckt::typecheck_block(code_blockt &code)
 {
   cpp_save_scopet saved_scope(cpp_scopes);
   cpp_scopes.new_block_scope();

src/cpp/cpp_typecheck_destructor.cpp

@@ -108,7 +108,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
       ptrmember.operands().push_back(exprt("cpp-this"));
 
       code_assignt assign(ptrmember, address);
-      block.operands().push_back(assign);
+      block.add(assign);
       continue;
     }
   }

src/goto-instrument/dump_c.cpp

@@ -624,7 +624,7 @@ void dump_ct::cleanup_decl(
     system_headers);
   p2s();
 
-  POSTCONDITION(b.operands().size()==1);
+  POSTCONDITION(b.statements().size()==1);
   decl.swap(b.op0());
 }
 
@@ -936,10 +936,8 @@ void dump_ct::cleanup_harness(code_blockt &b)
     decls.add(d);
   }
 
-  Forall_operands(it, b)
+  for(auto &code : b.statements())
   {
-    codet &code=to_code(*it);
-
     if(code.get_statement()==ID_function_call)
     {
       exprt &func=to_code_function_call(code).function();

src/goto-instrument/goto_program2code.cpp

@@ -1697,19 +1697,19 @@ static bool has_labels(const codet &code)
 }
 
 static bool move_label_ifthenelse(
-    exprt &expr,
-    exprt &label_dest)
+  exprt &expr,
+  exprt &label_dest)
 {
   if(expr.is_nil() ||
-      to_code(expr).get_statement()!=ID_block)
+     to_code(expr).get_statement()!=ID_block)
     return false;
 
   code_blockt &block=to_code_block(to_code(expr));
-  if(!block.has_operands() ||
-      to_code(block.operands().back()).get_statement()!=ID_label)
+  if(block.statements().empty() ||
+     block.statements().back().get_statement()!=ID_label)
     return false;
 
-  code_labelt &label=to_code_label(to_code(block.operands().back()));
+  code_labelt &label=to_code_label(block.statements().back());
   if(label.get_label().empty() ||
       label.code().get_statement()!=ID_skip)
     return false;

src/goto-programs/goto_convert.cpp

@@ -578,11 +578,8 @@ void goto_convertt::convert_block(
   std::size_t old_stack_size=targets.destructor_stack.size();
 
   // now convert block
-  forall_operands(it, code)
-  {
-    const codet &b_code=to_code(*it);
-    convert(b_code, dest, mode);
-  }
+  for(const auto &s : code.statements())
+    convert(s, dest, mode);
 
   // see if we need to do any destructors -- may have been processed
   // in a prior break/continue/return already, don't create dead code

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())
   {
-    codet &c=to_code(*it);
-
     if(c.get_statement()!=ID_label)
       continue;
 

src/util/format_expr.cpp

@@ -240,7 +240,7 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
     else if(statement == ID_block)
     {
       os << '{';
-      for(const auto &s : to_code_block(code).operands())
+      for(const auto &s : to_code_block(code).statements())
         os << ' ' << format(s);
       return os << " }";
     }

src/util/std_code.cpp

@@ -111,11 +111,11 @@ const codet &codet::last_statement() const
 /// \param extra_block: The input code_blockt
 void code_blockt::append(const code_blockt &extra_block)
 {
-  operands().reserve(operands().size()+extra_block.operands().size());
+  statements().reserve(statements().size()+extra_block.statements().size());
 
-  for(const auto &operand : extra_block.operands())
+  for(const auto &s : extra_block.statements())
   {
-    add(to_code(operand));
+    add(s);
   }
 }
 
@@ -125,8 +125,8 @@ code_blockt create_fatal_assertion(
   code_blockt result;
   result.add(code_assertt(condition));
   result.add(code_assumet(condition));
-  for(auto &op : result.operands())
-    op.add_source_location() = loc;
+  for(auto &s : result.statements())
+    s.add_source_location() = loc;
   result.add_source_location() = loc;
   return result;
 }

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()
+  { return (code_operandst &)get_sub(); }
+
+  const code_operandst &code_operands() const
+  { return (const code_operandst &)get_sub(); }
+
   code_blockt():codet(ID_block)
   {
   }
 
   explicit code_blockt(const std::list<codet> &_list):codet(ID_block)
   {
-    operandst &o=operands();
-    reserve_operands(_list.size());
+    auto &o=code_operands();
+    o.reserve(_list.size());
     for(std::list<codet>::const_iterator
         it=_list.begin();
         it!=_list.end();
         it++)
       o.push_back(*it);
   }
 
+  code_operandst &statements()
+  {
+    return code_operands();
+  }
+
+  const code_operandst &statements() const
+  {
+    return code_operands();
+  }
+
   void move(codet &code)
   {
     exprt::move_to_operands(code);