introduce code_frontend_declt

kroening · kroening · commit d15f2b2ea831 · 2021-10-19T15:37:50.000+01:00
This introduces code_fontend_declt, which separates code_declt (for use in
goto instructions) and the statement in C programs.

The two differ (the variant for goto programs has no initializer), and
separating them enables changes.
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -316,7 +316,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)
     }
     else
     {
-      code_declt decl(symbol.symbol_expr());
+      code_frontend_declt decl(symbol.symbol_expr());
       decl.add_source_location() = symbol.location;
       decl.symbol().add_source_location() = symbol.location;
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -323,7 +323,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
 
     // replace declarations by symbol expressions
     for(auto &binding : bindings)
-      binding = to_code_decl(to_code(binding)).symbol();
+      binding = to_code_frontend_decl(to_code(binding)).symbol();
 
     if(expr.id() == ID_lambda)
     {
@@ -788,7 +788,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
         throw 0;
       }
 
-      code_declt decl(symbol.symbol_expr());
+      code_frontend_declt decl(symbol.symbol_expr());
       decl.add_source_location() = declaration.source_location();
 
       binding = decl;
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -635,7 +635,7 @@ static void instantiate_atomic_fetch_op(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -697,7 +697,7 @@ static void instantiate_atomic_op_fetch(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -810,7 +810,7 @@ static void instantiate_sync_val_compare_and_swap(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -868,7 +868,7 @@ static void instantiate_sync_lock_test_and_set(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
@@ -990,7 +990,7 @@ static void instantiate_atomic_load_n(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
     symbol_exprt::typeless(ID___atomic_load),
@@ -1105,7 +1105,7 @@ static void instantiate_atomic_exchange_n(
   const symbol_exprt result =
     result_symbol(identifier_with_type, type, source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   block.add(code_expressiont{side_effect_expr_function_callt{
     symbol_exprt::typeless(ID___atomic_exchange),
@@ -1142,7 +1142,7 @@ static void instantiate_atomic_compare_exchange(
     result_symbol(
       identifier_with_type, c_bool_type(), source_location, symbol_table)
       .symbol_expr();
-  block.add(codet{ID_decl_block, {code_declt{result}}});
+  block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -634,7 +634,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       // produce the code that declares and initializes the symbol
       symbol_exprt symbol_expr = new_symbol.symbol_expr();
 
-      code_declt declaration(symbol_expr);
+      code_frontend_declt declaration(symbol_expr);
       declaration.add_source_location() = size_source_location;
 
       code_assignt assignment;
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -2761,9 +2761,8 @@ std::string expr2ct::convert_code_continue(unsigned indent)
   return dest;
 }
 
-std::string expr2ct::convert_code_decl(
-  const codet &src,
-  unsigned indent)
+std::string
+expr2ct::convert_code_frontend_decl(const codet &src, unsigned indent)
 {
   // initializer to go away
   if(src.operands().size()!=1 &&
@@ -3013,7 +3012,7 @@ std::string expr2ct::convert_code(
     return convert_code_continue(indent);
 
   if(statement==ID_decl)
-    return convert_code_decl(src, indent);
+    return convert_code_frontend_decl(src, indent);
 
   if(statement==ID_decl_block)
     return convert_code_decl_block(src, indent);
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -214,7 +214,7 @@ class expr2ct
   std::string convert_code_break(unsigned indent);
   std::string convert_code_switch(const codet &src, unsigned indent);
   std::string convert_code_continue(unsigned indent);
-  std::string convert_code_decl(const codet &src, unsigned indent);
+  std::string convert_code_frontend_decl(const codet &, unsigned indent);
   std::string convert_code_decl_block(const codet &src, unsigned indent);
   std::string convert_code_dead(const codet &src, unsigned indent);
   // NOLINTNEXTLINE(whitespace/line_length)
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
@@ -120,7 +120,7 @@ void cpp_typecheckt::typecheck_try_catch(codet &code)
       {
         // turn references into non-references
         {
-          code_declt &decl = to_code_decl(statements.front());
+          code_frontend_declt &decl = to_code_frontend_decl(statements.front());
           cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
 
           assert(cpp_declaration.declarators().size()==1);
@@ -139,8 +139,8 @@ void cpp_typecheckt::typecheck_try_catch(codet &code)
           catch_block.statements().front().get_statement() == ID_decl_block);
 
         // get the declaration
-        const code_declt &code_decl =
-          to_code_decl(to_code(catch_block.statements().front().op0()));
+        const code_frontend_declt &code_decl = to_code_frontend_decl(
+          to_code(catch_block.statements().front().op0()));
 
         // get the type
         const typet &type = code_decl.symbol().type();
@@ -199,7 +199,7 @@ void cpp_typecheckt::typecheck_switch(codet &code)
     assert(decl.operands().size()==1);
 
     // replace declaration by its symbol
-    value = to_code_decl(to_code(to_unary_expr(decl).op())).symbol();
+    value = to_code_frontend_decl(to_code(to_unary_expr(decl).op())).symbol();
 
     c_typecheck_baset::typecheck_switch(code);
 
@@ -456,7 +456,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
       throw 0;
     }
 
-    code_declt decl_statement(cpp_symbol_expr(symbol));
+    code_frontend_declt decl_statement(cpp_symbol_expr(symbol));
     decl_statement.add_source_location()=symbol.location;
 
     // Do we have an initializer that's not code?
diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp
@@ -58,7 +58,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
     throw 0;
   }
 
-  new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));
+  new_code.add_to_operands(code_frontend_declt(cpp_symbol_expr(symbol)));
 
   // do scoping
   symbolt union_symbol =
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
@@ -679,7 +679,7 @@ optionalt<codet> Parser::rTypedefStatement()
   if(!rTypedef(declaration))
     return {};
 
-  return code_declt(
+  return code_frontend_declt(
     static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
 }
 
@@ -7501,7 +7501,7 @@ optionalt<codet> Parser::rStatement()
         cpp_declarationt declaration;
         if(!rTypedefUsing(declaration))
           return {};
-        code_declt statement(
+        code_frontend_declt statement(
           static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
         statement.add_source_location() = declaration.source_location();
         return std::move(statement);
@@ -7790,7 +7790,7 @@ optionalt<codet> Parser::rTryStatement()
       if(declaration.declarators().front().name().is_nil())
         declaration.declarators().front().name() = cpp_namet("#anon");
 
-      code_declt code_decl(
+      code_frontend_declt code_decl(
         static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
       set_location(code_decl, catch_token);
 
@@ -8237,7 +8237,7 @@ optionalt<codet> Parser::rDeclarationStatement()
       cpp_declarationt declaration;
       if(!rConstDeclaration(declaration))
         return {};
-      return code_declt(
+      return code_frontend_declt(
         static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     }
     else
@@ -8268,7 +8268,7 @@ optionalt<codet> Parser::rIntegralDeclStatement(
   if(lex.LookAhead(0)==';')
   {
     lex.get_token(tk);
-    code_declt statement(
+    code_frontend_declt statement(
       static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     set_location(statement, tk);
     return std::move(statement);
@@ -8281,7 +8281,7 @@ optionalt<codet> Parser::rIntegralDeclStatement(
     if(lex.get_token(tk)!=';')
       return {};
 
-    code_declt statement(
+    code_frontend_declt statement(
       static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
     set_location(statement, tk);
     return std::move(statement);
@@ -8333,7 +8333,7 @@ Parser::rOtherDeclStatement(cpp_storage_spect &storage_spec, typet &cv_q)
   if(lex.get_token(tk)!=';')
     return {};
 
-  code_declt statement(
+  code_frontend_declt statement(
     static_cast<symbol_exprt &>(static_cast<exprt &>(declaration)));
   set_location(statement, tk);
   return std::move(statement);
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
@@ -649,7 +649,7 @@ void dump_ct::convert_compound_enum(
 }
 
 void dump_ct::cleanup_decl(
-  code_declt &decl,
+  code_frontend_declt &decl,
   std::list<irep_idt> &local_static,
   std::list<irep_idt> &local_type_decls)
 {
@@ -908,7 +908,7 @@ void dump_ct::convert_global_variable(
       !converted_global.insert(symbol.name).second)
     return;
 
-  code_declt d(symbol.symbol_expr());
+  code_frontend_declt d(symbol.symbol_expr());
 
   find_symbols_sett syms;
   if(symbol.value.is_not_nil())
@@ -1214,7 +1214,7 @@ void dump_ct::insert_local_static_decls(
       local_static_decls.find(*it);
     PRECONDITION(d_it!=local_static_decls.end());
 
-    code_declt d=d_it->second;
+    code_frontend_declt d = d_it->second;
     std::list<irep_idt> redundant;
     cleanup_decl(d, redundant, type_decls);
 
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
@@ -198,7 +198,7 @@ class dump_ct
       const typet &type)
   {
     symbol_exprt sym(identifier, type);
-    code_declt d(sym);
+    code_frontend_declt d(sym);
 
     std::string d_str=expr_to_string(d);
     assert(!d_str.empty());
@@ -232,7 +232,7 @@ class dump_ct
     const typet &type,
     std::ostream &os);
 
-  typedef std::unordered_map<irep_idt, code_declt> local_static_declst;
+  typedef std::unordered_map<irep_idt, code_frontend_declt> local_static_declst;
 
   void convert_global_variable(
       const symbolt &symbol,
@@ -259,7 +259,7 @@ class dump_ct
   void cleanup_expr(exprt &expr);
   void cleanup_type(typet &type);
   void cleanup_decl(
-    code_declt &decl,
+    code_frontend_declt &decl,
     std::list<irep_idt> &local_static,
     std::list<irep_idt> &local_type_decls);
   void cleanup_harness(code_blockt &b);
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -449,7 +449,7 @@ goto_programt::const_targett goto_program2codet::convert_decl(
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
 {
-  code_declt d = code_declt{target->decl_symbol()};
+  code_frontend_declt d = code_frontend_declt{target->decl_symbol()};
   symbol_exprt &symbol = d.symbol();
 
   goto_programt::const_targett next=target;
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -436,7 +436,7 @@ void goto_convertt::convert(
   if(statement==ID_block)
     convert_block(to_code_block(code), dest, mode);
   else if(statement==ID_decl)
-    convert_decl(to_code_decl(code), dest, mode);
+    convert_frontend_decl(to_code_frontend_decl(code), dest, mode);
   else if(statement==ID_decl_type)
     convert_decl_type(code, dest);
   else if(statement==ID_expression)
@@ -606,8 +606,8 @@ void goto_convertt::convert_expression(
   }
 }
 
-void goto_convertt::convert_decl(
-  const code_declt &code,
+void goto_convertt::convert_frontend_decl(
+  const code_frontend_declt &code,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1845,9 +1845,9 @@ symbolt &goto_convertt::new_tmp_symbol(
     mode,
     symbol_table);
 
-  code_declt decl(new_symbol.symbol_expr());
+  code_frontend_declt decl(new_symbol.symbol_expr());
   decl.add_source_location()=source_location;
-  convert_decl(decl, dest, mode);
+  convert_frontend_decl(decl, dest, mode);
 
   return new_symbol;
 }
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
@@ -222,9 +222,9 @@ class goto_convertt:public messaget
     const code_blockt &code,
     goto_programt &dest,
     const irep_idt &mode);
-  void convert_decl(
-    const code_declt &code,
-    goto_programt &dest,
+  void convert_frontend_decl(
+    const code_frontend_declt &,
+    goto_programt &,
     const irep_idt &mode);
   void convert_decl_type(const codet &code, goto_programt &dest);
   void convert_expression(
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
@@ -381,9 +381,9 @@ void goto_convertt::remove_function_call(
     symbol_table);
 
   {
-    code_declt decl(new_symbol.symbol_expr());
+    code_frontend_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest, mode);
+    convert_frontend_decl(decl, dest, mode);
   }
 
   {
@@ -421,9 +421,9 @@ void goto_convertt::remove_cpp_new(
     ID_cpp,
     symbol_table);
 
-  code_declt decl(new_symbol.symbol_expr());
+  code_frontend_declt decl(new_symbol.symbol_expr());
   decl.add_source_location()=new_symbol.location;
-  convert_decl(decl, dest, ID_cpp);
+  convert_frontend_decl(decl, dest, ID_cpp);
 
   const code_assignt call(new_symbol.symbol_expr(), expr);
 
@@ -467,9 +467,9 @@ void goto_convertt::remove_malloc(
       mode,
       symbol_table);
 
-    code_declt decl(new_symbol.symbol_expr());
+    code_frontend_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest, mode);
+    convert_frontend_decl(decl, dest, mode);
 
     code_assignt call(new_symbol.symbol_expr(), expr);
     call.add_source_location()=expr.source_location();
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
diff --git a/src/util/std_code.h b/src/util/std_code.h
diff --git a/unit/util/format.cpp b/unit/util/format.cpp

Original file line number	Diff line number	Diff line change
`@@ -316,7 +316,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)`
`316`	`316`	`}`
`317`	`317`	`else`
`318`	`318`	`{`
`319`		`- code_declt decl(symbol.symbol_expr());`
	`319`	`+ code_frontend_declt decl(symbol.symbol_expr());`
`320`	`320`	`decl.add_source_location() = symbol.location;`
`321`	`321`	`decl.symbol().add_source_location() = symbol.location;`
`322`	`322`
Original file line number	Diff line number	Diff line change
`@@ -323,7 +323,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)`
`323`	`323`
`324`	`324`	`// replace declarations by symbol expressions`
`325`	`325`	`for(auto &binding : bindings)`
`326`		`- binding = to_code_decl(to_code(binding)).symbol();`
	`326`	`+ binding = to_code_frontend_decl(to_code(binding)).symbol();`
`327`	`327`
`328`	`328`	`if(expr.id() == ID_lambda)`
`329`	`329`	`{`
`@@ -788,7 +788,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)`
`788`	`788`	`throw 0;`
`789`	`789`	`}`
`790`	`790`
`791`		`- code_declt decl(symbol.symbol_expr());`
	`791`	`+ code_frontend_declt decl(symbol.symbol_expr());`
`792`	`792`	`decl.add_source_location() = declaration.source_location();`
`793`	`793`
`794`	`794`	`binding = decl;`
Original file line number	Diff line number	Diff line change
`@@ -58,7 +58,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)`
`58`	`58`	`throw 0;`
`59`	`59`	`}`
`60`	`60`
`61`		`- new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));`
	`61`	`+ new_code.add_to_operands(code_frontend_declt(cpp_symbol_expr(symbol)));`
`62`	`62`
`63`	`63`	`// do scoping`
`64`	`64`	`symbolt union_symbol =`