Replace all uses of deprecated symbol_exprt constructors

This helps type safety has it avoids constructing symbol_exprts that never get a
proper type (or identifier).

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -481,21 +481,17 @@ void java_bytecode_convert_methodt::convert(
     // be rewritten below in the loop that iterates through the method
     // parameters; the only field that seem to be useful to write here is the
     // symbol_expr, others will be rewritten
-    variables[v.index].push_back(variablet());
-    auto &newv=variables[v.index].back();
-    newv.symbol_expr=result;
-    newv.start_pc=v.start_pc;
-    newv.length=v.length;
+    variables[v.index].emplace_back(result, v.start_pc, v.length);
   }
 
   // The variables is a expanding_vectort, and the loop above may have expanded
   // the vector introducing gaps where the entries are empty vectors. We now
   // make sure that the vector of each LV slot contains exactly one variablet,
-  // possibly default-initialized
+  // which we will add below
   std::size_t param_index=0;
   for(const auto &param : parameters)
   {
-    variables[param_index].resize(1);
+    variables[param_index].clear();
     param_index+=java_local_variable_slots(param.type());
   }
   INVARIANT(
@@ -549,10 +545,11 @@ void java_bytecode_convert_methodt::convert(
     symbol_table.add(parameter_symbol);
 
     // Add as a JVM local variable
-    variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
-    variables[param_index][0].is_parameter=true;
-    variables[param_index][0].start_pc=0;
-    variables[param_index][0].length=std::numeric_limits<size_t>::max();
+    variables[param_index].emplace_back(
+      parameter_symbol.symbol_expr(),
+      0,
+      std::numeric_limits<size_t>::max(),
+      true);
     param_index+=java_local_variable_slots(param.type());
   }
 
@@ -921,17 +918,14 @@ static void gather_symbol_live_ranges(
   if(e.id()==ID_symbol)
   {
     const auto &symexpr=to_symbol_expr(e);
-    auto findit = result.insert(
-      {symexpr.get_identifier(), java_bytecode_convert_methodt::variablet()});
-    auto &var=findit.first->second;
-    if(findit.second)
-    {
-      var.symbol_expr=symexpr;
-      var.start_pc=pc;
-      var.length=1;
-    }
-    else
+    auto findit = result.emplace(
+      std::piecewise_construct,
+      std::forward_as_tuple(symexpr.get_identifier()),
+      std::forward_as_tuple(symexpr, pc, 1));
+    if(!findit.second)
     {
+      auto &var = findit.first->second;
+
       if(pc<var.start_pc)
       {
         var.length+=(var.start_pc-pc);
@@ -1536,13 +1530,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="getstatic")
     {
       PRECONDITION(op.empty() && results.size() == 1);
-      symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       const bool is_assertions_disabled_field=
         field_name.find("$assertionsDisabled")!=std::string::npos;
 
-      symbol_expr.set_identifier(
-        get_static_field(arg0.get_string(ID_class), field_name));
+      const symbol_exprt symbol_expr(
+        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
 
       INVARIANT(
         symbol_table.has_symbol(symbol_expr.get_identifier()),
@@ -1559,10 +1552,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="putstatic")
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
-      symbol_expr.set_identifier(
-        get_static_field(arg0.get_string(ID_class), field_name));
+
+      const symbol_exprt symbol_expr(
+        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
 
       INVARIANT(
         symbol_table.has_symbol(symbol_expr.get_identifier()),

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -116,10 +116,40 @@ class java_bytecode_convert_methodt:public messaget
     symbol_exprt symbol_expr;
     size_t start_pc;
     size_t length;
-    bool is_parameter;
+    bool is_parameter = false;
     std::vector<holet> holes;
 
-    variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false)
+    variablet(
+      const symbol_exprt &_symbol_expr,
+      std::size_t _start_pc,
+      std::size_t _length)
+      : symbol_expr(_symbol_expr), start_pc(_start_pc), length(_length)
+    {
+    }
+
+    variablet(
+      const symbol_exprt &_symbol_expr,
+      std::size_t _start_pc,
+      std::size_t _length,
+      bool _is_parameter)
+      : symbol_expr(_symbol_expr),
+        start_pc(_start_pc),
+        length(_length),
+        is_parameter(_is_parameter)
+    {
+    }
+
+    variablet(
+      const symbol_exprt &_symbol_expr,
+      std::size_t _start_pc,
+      std::size_t _length,
+      bool _is_parameter,
+      std::vector<holet> &&_holes)
+      : symbol_expr(_symbol_expr),
+        start_pc(_start_pc),
+        length(_length),
+        is_parameter(_is_parameter),
+        holes(std::move(_holes))
     {
     }
   };

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -773,7 +773,7 @@ void java_bytecode_convert_methodt::setup_local_variables(
   // to calculate which variable to use, one uses the address of the instruction
   // that uses the variable, the size of the instruction and the start_pc /
   // length values in the local variable table
-  for(const auto &v : vars_with_holes)
+  for(auto &v : vars_with_holes)
   {
     if(v.is_parameter)
       continue;
@@ -807,12 +807,8 @@ void java_bytecode_convert_methodt::setup_local_variables(
     // Create a new local variable in the variables[] array, the result of
     // merging multiple local variables with equal name (parameters excluded)
     // into a single local variable with holes
-    variables[v.var.index].push_back(variablet());
-    auto &newv=variables[v.var.index].back();
-    newv.symbol_expr=result;
-    newv.start_pc=v.var.start_pc;
-    newv.length=v.var.length;
-    newv.holes=std::move(v.holes);
+    variables[v.var.index].emplace_back(
+      result, v.var.start_pc, v.var.length, false, std::move(v.holes));
 
     // Register the local variable in the symbol table
     symbolt new_symbol;
@@ -862,9 +858,7 @@ java_bytecode_convert_methodt::find_variable_for_slot(
   // with scope from 0 to SIZE_T_MAX
   // as it is at the end of the vector, it will only be taken into account
   // if no other variable is valid
-  size_t list_length=var_list.size();
-  var_list.resize(list_length+1);
-  var_list[list_length].start_pc=0;
-  var_list[list_length].length=std::numeric_limits<size_t>::max();
-  return var_list[list_length];
+  var_list.emplace_back(
+    symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits<size_t>::max());
+  return var_list.back();
 }

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1559,14 +1559,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
     loc);
 
   // > class1 = Class.forName(string1)
+  java_method_typet fun_type(
+    {java_method_typet::parametert(string_ptr_type)}, class_type);
   code_function_callt fun_call(
     class1,
     symbol_exprt(
-      "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
+      "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;",
+      std::move(fun_type)),
     {string1});
-  const java_method_typet fun_type(
-    {java_method_typet::parametert(string_ptr_type)}, class_type);
-  fun_call.function().type()=fun_type;
   code.add(fun_call, loc);
 
   // > return class1;

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -224,7 +224,7 @@ SCENARIO(
         simplify(sc.premise, empty_ns);
         simplify(sc.s0, empty_ns);
         simplify(sc.s1, empty_ns);
-        witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
+        witnesses.emplace(sc, generator.fresh_symbol("w", t.witness_type()));
         nc_axioms.push_back(sc);
         return accu + to_string(sc) + "\n\n";
       });
@@ -296,7 +296,7 @@ SCENARIO(
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(vacuous) + "\n\n");
@@ -346,7 +346,7 @@ SCENARIO(
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -397,7 +397,7 @@ SCENARIO(
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -450,7 +450,7 @@ SCENARIO(
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -501,7 +501,7 @@ SCENARIO(
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");

src/analyses/locals.cpp

@@ -21,12 +21,13 @@ 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()] = code_decl.symbol();
+      locals_map.emplace(code_decl.get_identifier(), code_decl.symbol());
     }
 
   for(const auto &param : goto_function.type.parameters())
-    locals_map[param.get_identifier()]=
-      symbol_exprt(param.get_identifier(), param.type());
+    locals_map.emplace(
+      param.get_identifier(),
+      symbol_exprt(param.get_identifier(), param.type()));
 }
 
 void localst::output(std::ostream &out) const

src/ansi-c/c_typecheck_type.cpp

@@ -635,9 +635,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       symbol_table.add(new_symbol);
 
       // produce the code that declares and initializes the symbol
-      symbol_exprt symbol_expr;
-      symbol_expr.set_identifier(temp_identifier);
-      symbol_expr.type()=new_symbol.type;
+      symbol_exprt symbol_expr(temp_identifier, new_symbol.type);
 
       code_declt declaration(symbol_expr);
       declaration.add_source_location() = size_source_location;