Merge pull request #3873 from tautschnig/symbol_exprt-typeless

symbol_exprt::typeless [blocks: #3766]

Author: tautschnig

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::typeless(pool_entry(class_info_index).s);
     }
 
   case '@':

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::typeless(full_spec.alias);
         else
-          symbol.value = symbol_exprt(renaming_entry->second);
+          symbol.value = symbol_exprt::typeless(renaming_entry->second);
         symbol.is_macro=true;
       }
 

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 = symbol_exprt::typeless(new_symbol->name);
 
         exprt::operandst ops;
         ops.push_back(value);

src/goto-symex/build_goto_trace.cpp

@@ -224,9 +224,11 @@ void build_goto_trace(
 
       if(it->is_shared_read() || it->is_shared_write())
       {
-        // these are just used to get the time stamp
-        exprt clock_value=prop_conv.get(
-          symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));
+        // these are just used to get the time stamp -- the clock type is
+        // computed to be of the minimal necessary size, but we don't need to
+        // know it to get the value so just use typeless
+        exprt clock_value = prop_conv.get(
+          symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it)));
 
         const auto cv = numeric_cast<mp_integer>(clock_value);
         if(cv.has_value())

src/jsil/jsil_convert.cpp

@@ -91,7 +91,7 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
 
       code_try_catcht t_c(std::move(t));
       // Adding empty symbol to catch decl
-      code_declt d(symbol_exprt("decl_symbol"));
+      code_declt d(symbol_exprt::typeless("decl_symbol"));
       t_c.add_catch(d, g);
       t_c.add_source_location()=code.source_location();
 

src/jsil/jsil_parse_tree.cpp

@@ -66,11 +66,13 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
       static_cast<const codet&>(find(ID_value))));
 
   irept returns(find(ID_return));
-  code_returnt r(symbol_exprt(returns.get(ID_value)));
+  code_returnt r(symbol_exprt::typeless(returns.get(ID_value)));
 
   irept throws(find(ID_throw));
   side_effect_expr_throwt t(
-    symbol_exprt(throws.get(ID_value)), nil_typet(), s.source_location());
+    symbol_exprt::typeless(throws.get(ID_value)),
+    nil_typet(),
+    s.source_location());
   code_expressiont ct(t);
 
   if(insert_at_label(r, returns.get(ID_label), code))

src/jsil/parser.y

@@ -148,7 +148,7 @@ procedure_decl: TOK_PROCEDURE proc_ident '(' parameters_opt ')'
 proc_ident: TOK_IDENTIFIER
           | TOK_EVAL
           {
-            symbol_exprt e("eval");
+            symbol_exprt e = symbol_exprt::typeless("eval");
             newstack($$).swap(e);
           }
           | TOK_BUILTIN_IDENTIFIER
@@ -164,7 +164,8 @@ proc_ident: TOK_IDENTIFIER
 proc_ident_expr: proc_ident
                | TOK_STRING
                {
-                 symbol_exprt s(to_string_constant(stack($$)).get_value());
+                 symbol_exprt s = symbol_exprt::typeless(
+                   to_string_constant(stack($$)).get_value());
                  stack($$).swap(s);
                }
                ;

src/linking/linking.cpp

@@ -227,7 +227,7 @@ void linkingt::detailed_conflict_report_rec(
             {
               std::string msg_bak;
               msg_bak.swap(msg);
-              symbol_exprt c(ID_C_this);
+              symbol_exprt c = symbol_exprt::typeless(ID_C_this);
               detailed_conflict_report_rec(
                 old_symbol,
                 new_symbol,

src/linking/linking_class.h

@@ -143,7 +143,7 @@ class linkingt:public typecheckt
     const typet &type1,
     const typet &type2)
   {
-    symbol_exprt conflict_path(ID_C_this);
+    symbol_exprt conflict_path = symbol_exprt::typeless(ID_C_this);
     detailed_conflict_report_rec(
       old_symbol,
       new_symbol,

src/util/std_expr.h

@@ -179,6 +179,15 @@ class symbol_exprt : public nullary_exprt
     set_identifier(identifier);
   }
 
+  /// Generate a symbol_exprt without a proper type. Use if, and only if, the
+  /// type either cannot be determined just yet (such as during type checking)
+  /// or when the type truly is immaterial. The latter case may better be dealt
+  /// with by using just an irep_idt, and not a symbol_exprt.
+  static symbol_exprt typeless(const irep_idt &id)
+  {
+    return symbol_exprt(id, typet());
+  }
+
   void set_identifier(const irep_idt &identifier)
   {
     set(ID_identifier, identifier);