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

@@ -1536,13 +1536,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 +1558,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

@@ -119,7 +119,11 @@ class java_bytecode_convert_methodt:public messaget
     bool is_parameter;
     std::vector<holet> holes;
 
-    variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false)
+    variablet()
+      : symbol_expr("", typet()),
+        start_pc(0),
+        length(0),
+        is_parameter(false)
     {
     }
   };

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1600,7 +1600,7 @@ exprt java_bytecode_parsert::get_relement_value()
   case 'c':
     {
       u2 class_info_index = read_u2();
-      return symbol_exprt(pool_entry(class_info_index).s);
+      return symbol_exprt(pool_entry(class_info_index).s, typet());
     }
 
   case '@':

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1560,14 +1560,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/src/java_bytecode/java_utils.cpp

@@ -285,7 +285,8 @@ exprt make_function_application(
   declare_function(fun_name, type, symbol_table);
 
   // Function application
-  return function_application_exprt(symbol_exprt(fun_name), arguments, type);
+  return function_application_exprt(
+    symbol_exprt(fun_name, typet()), arguments, type);
 }
 
 /// Strip java:: prefix from given identifier

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

@@ -185,7 +185,7 @@ SCENARIO("instantiate_not_contains",
   {
     // Creating "ab".lastIndexOf("b", 0)
     const function_application_exprt func(
-      symbol_exprt(ID_cprover_string_last_index_of_func),
+      symbol_exprt(ID_cprover_string_last_index_of_func, typet()),
       {ab, b, from_integer(2)},
       t.length_type());
 
@@ -215,7 +215,7 @@ SCENARIO("instantiate_not_contains",
         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";
       });
@@ -287,7 +287,7 @@ SCENARIO("instantiate_not_contains",
     // 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");
@@ -337,7 +337,7 @@ SCENARIO("instantiate_not_contains",
     // 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");
@@ -388,7 +388,7 @@ SCENARIO("instantiate_not_contains",
     // 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");
@@ -441,7 +441,7 @@ SCENARIO("instantiate_not_contains",
     // 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");
@@ -492,7 +492,7 @@ SCENARIO("instantiate_not_contains",
     // 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");

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

@@ -65,19 +65,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 
     // fun1 is s3 = s1.concat(s2)
     const function_application_exprt fun1(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string3.op0(), string3.op1(), string1, string2},
       fun_type);
 
     // fun2 is s5 = s3.concat(s4)
     const function_application_exprt fun2(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string5.op0(), string5.op1(), string3, string4},
       fun_type);
 
     // fun3 is s6 = s5.concat(s2)
     const function_application_exprt fun3(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string6.op0(), string6.op1(), string5, string2},
       fun_type);
 

src/analyses/constant_propagator.cpp

@@ -649,7 +649,8 @@ bool constant_propagator_domaint::partial_evaluate(
   // if the current rounding mode is top we can
   // still get a non-top result by trying all rounding
   // modes and checking if the results are all the same
-  if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
+  if(!known_values.is_constant(
+       symbol_exprt(ID_cprover_rounding_mode_str, typet())))
   {
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
   }

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_base.cpp

@@ -697,9 +697,9 @@ void c_typecheck_baset::typecheck_declaration(
         // also cater for renaming/placement in sections
         const auto &renaming_entry = asm_label_map.find(full_spec.alias);
         if(renaming_entry == asm_label_map.end())
-          symbol.value = symbol_exprt(full_spec.alias);
+          symbol.value = symbol_exprt(full_spec.alias, typet());
         else
-          symbol.value = symbol_exprt(renaming_entry->second);
+          symbol.value = symbol_exprt(renaming_entry->second, typet());
         symbol.is_macro=true;
       }
 

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;

src/cpp/cpp_typecheck_compound_type.cpp

@@ -743,8 +743,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
       }
       else
       {
-        symbol_exprt symexpr;
-        symexpr.set_identifier(new_symbol->name);
+        symbol_exprt symexpr(new_symbol->name, typet());
 
         exprt::operandst ops;
         ops.push_back(value);

src/cpp/cpp_typecheck_expr.cpp

@@ -1450,13 +1450,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       code_typet t(
         {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1483,14 +1481,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
         ptr_arg.type().subtype());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1517,15 +1513,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type().subtype()),
          code_typet::parametert(signed_int_type())},
         empty_typet());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1552,15 +1546,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type().subtype()),
          code_typet::parametert(signed_int_type())},
         ptr_arg.type().subtype());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1595,15 +1587,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
 
       const exprt &ptr_arg=fargs.operands.front();
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
         empty_typet());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1644,16 +1634,14 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
 
       const exprt &ptr_arg=fargs.operands.front();
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       const code_typet t(
         {code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(ptr_arg.type()),
          code_typet::parametert(signed_int_type())},
         empty_typet());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1699,9 +1687,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
 
       const exprt &ptr_arg=fargs.operands.front();
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       code_typet::parameterst parameters;
       parameters.push_back(code_typet::parametert(ptr_arg.type()));
       parameters.push_back(code_typet::parametert(ptr_arg.type()));
@@ -1715,7 +1700,8 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       parameters.push_back(code_typet::parametert(signed_int_type()));
       parameters.push_back(code_typet::parametert(signed_int_type()));
       code_typet t(std::move(parameters), c_bool_type());
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1744,13 +1730,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       code_typet t(
         {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }
@@ -1779,13 +1763,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
         throw 0;
       }
 
-      symbol_exprt result;
-      result.add_source_location()=source_location;
-      result.set_identifier(identifier);
       code_typet t(
         {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      result.type()=t;
+      symbol_exprt result(identifier, t);
+      result.add_source_location() = source_location;
       expr.swap(result);
       return;
     }

src/cpp/cpp_typecheck_resolve.cpp

@@ -2133,7 +2133,7 @@ bool cpp_typecheck_resolvet::disambiguate_functions(
       {
         // it's a constructor
         const typet &object_type=parameter.type().subtype();
-        symbol_exprt object(object_type);
+        symbol_exprt object("", object_type);
         object.set(ID_C_lvalue, true);
 
         cpp_typecheck_fargst new_fargs(fargs);