Merge pull request #3267 from diffblue/type_code_declt

Daniel Kroening · web-flow · commit 9d69f68e6d94 · 2018-11-06T13:04:29.000Z
Type the operand of code_declt
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -683,7 +683,7 @@ void add_pointer_to_array_association(
     loc,
     ID_java,
     symbol_table);
-  exprt return_expr = return_sym.symbol_expr();
+  auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
@@ -715,7 +715,7 @@ void add_array_to_length_association(
     loc,
     ID_java,
     symbol_table);
-  const exprt return_expr = return_sym.symbol_expr();
+  const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
@@ -747,7 +747,7 @@ void add_character_set_constraint(
   PRECONDITION(pointer.type().id() == ID_pointer);
   symbolt &return_sym = get_fresh_aux_symbol(
     java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
-  const exprt return_expr = return_sym.symbol_expr();
+  const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   const constant_exprt char_set_expr(char_set, string_typet());
   code.add(
@@ -790,7 +790,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
     loc,
     ID_java,
     symbol_table);
-  const exprt return_code = return_code_sym.symbol_expr();
+  const auto return_code = return_code_sym.symbol_expr();
   code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
@@ -1232,7 +1232,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   std::string aux_name="tmp_"+id2string(type_name);
   symbolt symbol=get_fresh_aux_symbol(
     value_type, aux_name, aux_name, loc, ID_java, symbol_table);
-  exprt value=symbol.symbol_expr();
+  auto value = symbol.symbol_expr();
 
   // Check that the type of the object is in the symbol table,
   // otherwise there is no safe way of finding its value.
@@ -1340,8 +1340,9 @@ exprt java_string_library_preprocesst::make_argument_for_format(
       std::string tmp_name="tmp_"+id2string(name);
       symbolt field_symbol = get_fresh_aux_symbol(
         type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
-      field_expr=field_symbol.symbol_expr();
-      code.add(code_declt(field_expr), loc);
+      auto field_symbol_expr = field_symbol.symbol_expr();
+      field_expr = field_symbol_expr;
+      code.add(code_declt(field_symbol_expr), loc);
     }
     else
       field_expr =
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
@@ -93,7 +93,7 @@ void constant_propagator_domaint::transform(
   if(from->is_decl())
   {
     const code_declt &code_decl=to_code_decl(from->code);
-    const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol());
+    const symbol_exprt &symbol = code_decl.symbol();
     values.set_to_top(symbol);
   }
   else if(from->is_assign())
diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp
@@ -21,8 +21,7 @@ void localst::build(const goto_functiont &goto_function)
     if(it->is_decl())
     {
       const code_declt &code_decl=to_code_decl(it->code);
-      locals_map[code_decl.get_identifier()]=
-        to_symbol_expr(code_decl.symbol());
+      locals_map[code_decl.get_identifier()] = code_decl.symbol();
     }
 
   for(const auto &param : goto_function.type.parameters())
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
@@ -100,7 +100,7 @@ void cpp_typecheckt::typecheck_try_catch(codet &code)
           to_code_decl(to_code(code.op0().op0()));
 
         // get the type
-        const typet &type=code_decl.op0().type();
+        const typet &type = code_decl.symbol().type();
 
         // annotate exception ID
         op.set(ID_exception_id, cpp_exception_id(type, *this));
diff --git a/src/cpp/cpp_util.cpp b/src/cpp/cpp_util.cpp
@@ -11,12 +11,12 @@
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
-exprt cpp_symbol_expr(const symbolt &symbol)
+symbol_exprt cpp_symbol_expr(const symbolt &symbol)
 {
   symbol_exprt tmp(symbol.name, symbol.type);
 
   if(symbol.is_lvalue)
     tmp.set(ID_C_lvalue, true);
 
-  return std::move(tmp);
+  return tmp;
 }
diff --git a/src/cpp/cpp_util.h b/src/cpp/cpp_util.h
@@ -13,7 +13,7 @@
 #include <util/expr.h>
 #include <util/symbol.h>
 
-exprt cpp_symbol_expr(const symbolt &symbol);
+symbol_exprt cpp_symbol_expr(const symbolt &symbol);
 
 inline void already_typechecked(irept &irep)
 {
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
@@ -80,8 +80,8 @@ void full_slicert::operator()(
       jumps.push_back(e_it->second);
     else if(e_it->first->is_decl())
     {
-      const exprt &s=to_code_decl(e_it->first->code).symbol();
-      decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
+      const auto &s=to_code_decl(e_it->first->code).symbol();
+      decl_dead[s.get_identifier()].push(e_it->second);
     }
     else if(e_it->first->is_dead())
     {
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -546,8 +546,8 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
 
   // Start building the program.  Begin by decl'ing each of the
   // master distinguishers.
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     program.add_instruction(DECL)->code=code_declt(*it);
@@ -888,8 +888,8 @@ void disjunctive_polynomial_accelerationt::build_fixed()
 
   // Create shadow distinguisher variables.  These guys identify the path that
   // is taken through the fixed-path body.
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     exprt &distinguisher=*it;
@@ -1006,8 +1006,8 @@ void disjunctive_polynomial_accelerationt::record_path(
 {
   distinguish_valuest path_val;
 
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     path_val[*it]=program.eval(*it).is_true();
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
@@ -98,7 +98,7 @@ class disjunctive_polynomial_accelerationt
   acceleration_utilst utils;
   exprt loop_counter;
   distinguish_mapt distinguishing_points;
-  std::list<exprt> distinguishers;
+  std::list<symbol_exprt> distinguishers;
   expr_sett modified;
   goto_programt fixed;
   std::list<distinguish_valuest> accelerated_paths;
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
@@ -894,7 +894,9 @@ void dump_ct::convert_global_variable(
   }
 
   if(!func.empty() && !symbol.is_extern)
-    local_static_decls[symbol.name]=d;
+  {
+    local_static_decls.emplace(symbol.name, d);
+  }
   else if(!symbol.value.is_nil())
   {
     os << "// " << symbol.name << '\n';
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
@@ -310,8 +310,8 @@ void full_slicert::operator()(
       jumps.push_back(e_it->second);
     else if(e_it->first->is_decl())
     {
-      const exprt &s=to_code_decl(e_it->first->code).symbol();
-      decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
+      const auto &s = to_code_decl(e_it->first->code).symbol();
+      decl_dead[s.get_identifier()].push(e_it->second);
     }
     else if(e_it->first->is_dead())
     {
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -458,7 +458,7 @@ goto_programt::const_targett goto_program2codet::convert_decl(
     codet &dest)
 {
   code_declt d=to_code_decl(target->code);
-  symbol_exprt &symbol=to_symbol_expr(d.symbol());
+  symbol_exprt &symbol = d.symbol();
 
   goto_programt::const_targett next=target;
   ++next;
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -607,7 +607,7 @@ void goto_convertt::convert_decl(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  const irep_idt &identifier = to_symbol_expr(code.symbol()).get_identifier();
+  const irep_idt &identifier = code.get_identifier();
 
   const symbolt &symbol = ns.lookup(identifier);
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
@@ -29,7 +29,7 @@ void goto_symext::symex_decl(statet &state)
   // we handle the decl with only one operand
   PRECONDITION(code.operands().size() == 1);
 
-  symex_decl(state, to_symbol_expr(to_code_decl(code).symbol()));
+  symex_decl(state, to_code_decl(code).symbol());
 }
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp
@@ -13,11 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_expr.h"
 
-const irep_idt &code_declt::get_identifier() const
-{
-  return to_symbol_expr(symbol()).get_identifier();
-}
-
 const irep_idt &code_deadt::get_identifier() const
 {
   return to_symbol_expr(symbol()).get_identifier();
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-#include "expr.h"
 #include "expr_cast.h"
 #include "invariant.h"
+#include "std_expr.h"
 
 /// Data structure for representing an arbitrary statement in a program. Every
 /// specific type of statement (e.g. block of statements, assignment,
@@ -276,28 +276,25 @@ inline code_assignt &to_code_assign(codet &code)
 class code_declt:public codet
 {
 public:
-  DEPRECATED("use code_declt(symbol) instead")
-  code_declt():codet(ID_decl)
+  explicit code_declt(const symbol_exprt &symbol) : codet(ID_decl)
   {
-    operands().resize(1);
+    add_to_operands(symbol);
   }
 
-  explicit code_declt(const exprt &symbol):codet(ID_decl)
+  symbol_exprt &symbol()
   {
-    add_to_operands(symbol);
+    return static_cast<symbol_exprt &>(op0());
   }
 
-  exprt &symbol()
+  const symbol_exprt &symbol() const
   {
-    return op0();
+    return static_cast<const symbol_exprt &>(op0());
   }
 
-  const exprt &symbol() const
+  const irep_idt &get_identifier() const
   {
-    return op0();
+    return symbol().get_identifier();
   }
-
-  const irep_idt &get_identifier() const;
 };
 
 template<> inline bool can_cast_expr<code_declt>(const exprt &base)

Original file line number	Diff line number	Diff line change
`@@ -93,7 +93,7 @@ void constant_propagator_domaint::transform(`
`93`	`93`	`if(from->is_decl())`
`94`	`94`	`{`
`95`	`95`	`const code_declt &code_decl=to_code_decl(from->code);`
`96`		`- const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol());`
	`96`	`+ const symbol_exprt &symbol = code_decl.symbol();`
`97`	`97`	`values.set_to_top(symbol);`
`98`	`98`	`}`
`99`	`99`	`else if(from->is_assign())`
Original file line number	Diff line number	Diff line change
`@@ -21,8 +21,7 @@ void localst::build(const goto_functiont &goto_function)`
`21`	`21`	`if(it->is_decl())`
`22`	`22`	`{`
`23`	`23`	`const code_declt &code_decl=to_code_decl(it->code);`
`24`		`- locals_map[code_decl.get_identifier()]=`
`25`		`- to_symbol_expr(code_decl.symbol());`
	`24`	`+ locals_map[code_decl.get_identifier()] = code_decl.symbol();`
`26`	`25`	`}`
`27`	`26`
`28`	`27`	`for(const auto &param : goto_function.type.parameters())`
Original file line number	Diff line number	Diff line change
`@@ -11,12 +11,12 @@`
`11`	`11`	`#include <util/std_expr.h>`
`12`	`12`	`#include <util/symbol.h>`
`13`	`13`
`14`		`-exprt cpp_symbol_expr(const symbolt &symbol)`
	`14`	`+symbol_exprt cpp_symbol_expr(const symbolt &symbol)`
`15`	`15`	`{`
`16`	`16`	`symbol_exprt tmp(symbol.name, symbol.type);`
`17`	`17`
`18`	`18`	`if(symbol.is_lvalue)`
`19`	`19`	`tmp.set(ID_C_lvalue, true);`
`20`	`20`
`21`		`- return std::move(tmp);`
	`21`	`+ return tmp;`
`22`	`22`	`}`
Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,7 @@`
`13`	`13`	`#include <util/expr.h>`
`14`	`14`	`#include <util/symbol.h>`
`15`	`15`
`16`		`-exprt cpp_symbol_expr(const symbolt &symbol);`
	`16`	`+symbol_exprt cpp_symbol_expr(const symbolt &symbol);`
`17`	`17`
`18`	`18`	`inline void already_typechecked(irept &irep)`
`19`	`19`	`{`
Original file line number	Diff line number	Diff line change
`@@ -80,8 +80,8 @@ void full_slicert::operator()(`
`80`	`80`	`jumps.push_back(e_it->second);`
`81`	`81`	`else if(e_it->first->is_decl())`
`82`	`82`	`{`
`83`		`- const exprt &s=to_code_decl(e_it->first->code).symbol();`
`84`		`- decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);`
	`83`	`+ const auto &s=to_code_decl(e_it->first->code).symbol();`
	`84`	`+ decl_dead[s.get_identifier()].push(e_it->second);`
`85`	`85`	`}`
`86`	`86`	`else if(e_it->first->is_dead())`
`87`	`87`	`{`
Original file line number	Diff line number	Diff line change
`@@ -894,7 +894,9 @@ void dump_ct::convert_global_variable(`
`894`	`894`	`}`
`895`	`895`
`896`	`896`	`if(!func.empty() && !symbol.is_extern)`
`897`		`- local_static_decls[symbol.name]=d;`
	`897`	`+ {`
	`898`	`+ local_static_decls.emplace(symbol.name, d);`
	`899`	`+ }`
`898`	`900`	`else if(!symbol.value.is_nil())`
`899`	`901`	`{`
`900`	`902`	`os << "// " << symbol.name << '\n';`