Skip to content

Commit 412ea82

Browse files
committed
Fix dump-c output involving typedef names
Follow-up to 99067de, which made expr2c prefer typedef names over original type expressions. Thanks Andreas Stahlbauer for providing the regression tests and help in debugging. Fixes: #882
1 parent 076c37e commit 412ea82

File tree

6 files changed

+242
-1
lines changed

6 files changed

+242
-1
lines changed
+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
typedef long int off_t;
2+
typedef signed char smallint;
3+
4+
typedef struct chain_s {
5+
struct node_s *first;
6+
struct node_s *last;
7+
const char *programname;
8+
} chain;
9+
10+
typedef struct node_s {
11+
struct node_s *n;
12+
} node;
13+
14+
typedef struct dumper_t_x {
15+
node n;
16+
off_t dump_skip;
17+
signed int dump_length;
18+
smallint dump_vflag;
19+
} dumper_t;
20+
21+
typedef struct FS_x {
22+
struct FS *nextfs;
23+
signed int bcnt;
24+
} FS;
25+
26+
dumper_t * alloc_dumper(void) {
27+
return (void*) 0;
28+
}
29+
30+
typedef unsigned int uint32_t;
31+
32+
const uint32_t xx[2];
33+
34+
typedef struct node_s2 {
35+
uint32_t info;
36+
} node2;
37+
38+
typedef struct {
39+
int x;
40+
} anon_name;
41+
42+
int main() {
43+
node n;
44+
chain c;
45+
dumper_t a;
46+
dumper_t b[3];
47+
node2* sn;
48+
anon_name d;
49+
alloc_dumper();
50+
return 0;
51+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
This test should be run via chain.sh, which will try to recompile the dumped C
10+
code. Missing/incomplete typedef output would cause a failure.

src/goto-instrument/dump_c.cpp

+164-1
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,8 @@ void dump_ct::operator()(std::ostream &os)
6262
std::stringstream func_body_stream;
6363
local_static_declst local_static_decls;
6464

65+
gather_global_typedefs();
66+
6567
// add copies of struct types when ID_C_transparent_union is only
6668
// annotated to parameter
6769
symbol_tablet symbols_transparent;
@@ -113,6 +115,9 @@ void dump_ct::operator()(std::ostream &os)
113115
symbolt &symbol=it->second;
114116
bool tag_added=false;
115117

118+
// TODO we could get rid of some of the ID_anonymous by looking up
119+
// the origin symbol types in typedef_types and adjusting any other
120+
// uses of ID_tag
116121
if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
117122
symbol.type.get(ID_tag).empty())
118123
{
@@ -285,6 +290,8 @@ void dump_ct::operator()(std::ostream &os)
285290
os << std::endl;
286291
}
287292

293+
dump_typedefs(os);
294+
288295
if(!func_decl_stream.str().empty())
289296
os << func_decl_stream.str() << std::endl;
290297
if(!compound_body_stream.str().empty())
@@ -521,7 +528,21 @@ void dump_ct::convert_compound(
521528
struct_body << ";" << std::endl;
522529
}
523530

524-
os << type_to_string(unresolved);
531+
typet unresolved_clean=unresolved;
532+
typedef_typest::const_iterator td_entry=
533+
typedef_types.find(unresolved);
534+
irep_idt typedef_str;
535+
if(td_entry!=typedef_types.end())
536+
{
537+
unresolved_clean.remove(ID_C_typedef);
538+
typedef_str=td_entry->second;
539+
std::pair<std::string, bool> &td_map_entry=typedef_map[typedef_str];
540+
if(!td_map_entry.second)
541+
td_map_entry.first="";
542+
os << "typedef ";
543+
}
544+
545+
os << type_to_string(unresolved_clean);
525546
if(!base_decls.str().empty())
526547
{
527548
assert(language->id()=="cpp");
@@ -548,6 +569,8 @@ void dump_ct::convert_compound(
548569
os << " __attribute__ ((__transparent_union__))";
549570
if(type.get_bool(ID_C_packed))
550571
os << " __attribute__ ((__packed__))";
572+
if(!typedef_str.empty())
573+
os << " " << typedef_str;
551574
os << ";";
552575
os << std::endl;
553576
os << std::endl;
@@ -901,6 +924,10 @@ void dump_ct::cleanup_decl(
901924

902925
tmp.add_instruction(END_FUNCTION);
903926

927+
std::unordered_set<irep_idt, irep_id_hash> typedef_names;
928+
for(const auto &td : typedef_map)
929+
typedef_names.insert(td.first);
930+
904931
code_blockt b;
905932
goto_program2codet p2s(
906933
irep_idt(),
@@ -909,6 +936,7 @@ void dump_ct::cleanup_decl(
909936
b,
910937
local_static,
911938
local_type_decls,
939+
typedef_names,
912940
system_headers);
913941
p2s();
914942

@@ -918,6 +946,132 @@ void dump_ct::cleanup_decl(
918946

919947
/*******************************************************************\
920948
949+
Function: dump_ct::collect_typedefs
950+
951+
Inputs:
952+
type Type to inspect for ID_C_typedef entry
953+
early Set to true to enforce that typedef is dumped before any
954+
function declarations or struct definitions
955+
956+
Outputs:
957+
958+
Purpose: Find any typedef names contained in the input type and store
959+
their declaration strings in typedef_map for eventual output.
960+
961+
\*******************************************************************/
962+
963+
void dump_ct::collect_typedefs(const typet &type, bool early)
964+
{
965+
if(type.id()==ID_code)
966+
{
967+
const code_typet &code_type=to_code_type(type);
968+
969+
collect_typedefs(code_type.return_type(), early);
970+
for(const auto &param : code_type.parameters())
971+
collect_typedefs(param.type(), early);
972+
}
973+
else if(type.id()==ID_pointer || type.id()==ID_array)
974+
{
975+
collect_typedefs(type.subtype(), early);
976+
}
977+
else if(type.id()==ID_symbol)
978+
{
979+
const symbolt &symbol=
980+
ns.lookup(to_symbol_type(type).get_identifier());
981+
collect_typedefs(symbol.type, early);
982+
}
983+
984+
const irep_idt &typedef_str=type.get(ID_C_typedef);
985+
986+
if(!typedef_str.empty())
987+
{
988+
std::pair<typedef_mapt::iterator, bool> entry=
989+
typedef_map.insert({typedef_str, {"", early}});
990+
991+
if(entry.second)
992+
{
993+
if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
994+
{
995+
system_headers.insert("stdarg.h");
996+
}
997+
else
998+
{
999+
typet t=type;
1000+
t.remove(ID_C_typedef);
1001+
1002+
std::ostringstream oss;
1003+
oss << "typedef " << type_to_string(t) << " "
1004+
<< typedef_str << ';';
1005+
1006+
entry.first->second.first=oss.str();
1007+
}
1008+
}
1009+
else if(early)
1010+
{
1011+
entry.first->second.second=true;
1012+
}
1013+
}
1014+
}
1015+
1016+
/*******************************************************************\
1017+
1018+
Function: dump_ct::gather_global_typedefs
1019+
1020+
Inputs:
1021+
1022+
Outputs:
1023+
1024+
Purpose: find all global typdefs in the symbol table and store them
1025+
in typedef_types
1026+
1027+
\*******************************************************************/
1028+
1029+
void dump_ct::gather_global_typedefs()
1030+
{
1031+
forall_symbols(it, copied_symbol_table.symbols)
1032+
{
1033+
const symbolt &symbol=it->second;
1034+
1035+
if(symbol.is_macro && symbol.is_type && !ignore(symbol) &&
1036+
symbol.location.get_function().empty())
1037+
{
1038+
assert(!symbol.type.get(ID_C_typedef).empty());
1039+
typedef_types[symbol.type]=symbol.type.get(ID_C_typedef);
1040+
collect_typedefs(symbol.type, false);
1041+
}
1042+
}
1043+
}
1044+
1045+
/*******************************************************************\
1046+
1047+
Function: dump_ct::dump_typedefs
1048+
1049+
Inputs:
1050+
1051+
Outputs: os output stream
1052+
1053+
Purpose: print all typedefs that are not covered via
1054+
typedef struct xyz { ... } name;
1055+
1056+
\*******************************************************************/
1057+
1058+
void dump_ct::dump_typedefs(std::ostream &os) const
1059+
{
1060+
bool need_newline=false;
1061+
1062+
for(const auto &td : typedef_map)
1063+
if(!td.second.first.empty())
1064+
{
1065+
need_newline=true;
1066+
os << td.second.first << std::endl;
1067+
}
1068+
1069+
if(need_newline)
1070+
os << std::endl;
1071+
}
1072+
1073+
/*******************************************************************\
1074+
9211075
Function: dump_ct::convert_global_variables
9221076
9231077
Inputs:
@@ -1024,13 +1178,18 @@ void dump_ct::convert_function_declaration(
10241178
code_blockt b;
10251179
std::list<irep_idt> type_decls, local_static;
10261180

1181+
std::unordered_set<irep_idt, irep_id_hash> typedef_names;
1182+
for(const auto &td : typedef_map)
1183+
typedef_names.insert(td.first);
1184+
10271185
goto_program2codet p2s(
10281186
symbol.name,
10291187
func_entry->second.body,
10301188
copied_symbol_table,
10311189
b,
10321190
local_static,
10331191
type_decls,
1192+
typedef_names,
10341193
system_headers);
10351194
p2s();
10361195

@@ -1065,6 +1224,10 @@ void dump_ct::convert_function_declaration(
10651224
if(symbol.name!=goto_functionst::entry_point() &&
10661225
symbol.name!=ID_main)
10671226
{
1227+
// make sure typedef names are available before outputting this
1228+
// declaration
1229+
collect_typedefs(symbol.type, true);
1230+
10681231
os_decl << "// " << symbol.name << std::endl;
10691232
os_decl << "// " << symbol.location << std::endl;
10701233
os_decl << make_decl(symbol.name, symbol.type) << ";" << std::endl;

src/goto-instrument/dump_c_class.h

+9
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,11 @@ class dump_ct
5959
declared_enum_constants_mapt;
6060
declared_enum_constants_mapt declared_enum_constants;
6161

62+
typedef std::map<irep_idt, std::pair<std::string, bool>> typedef_mapt;
63+
typedef_mapt typedef_map;
64+
typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
65+
typedef_typest typedef_types;
66+
6267
void init_system_library_map();
6368

6469
std::string type_to_string(const typet &type);
@@ -85,6 +90,10 @@ class dump_ct
8590
return d_str.substr(0, d_str.size()-1);
8691
}
8792

93+
void collect_typedefs(const typet &type, bool early);
94+
void gather_global_typedefs();
95+
void dump_typedefs(std::ostream &os) const;
96+
8897
void convert_compound_declaration(
8998
const symbolt &symbol,
9099
std::ostream &os_body);

src/goto-instrument/goto_program2code.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -1818,6 +1818,11 @@ void goto_program2codet::cleanup_code(
18181818

18191819
add_local_types(code.op0().type());
18201820

1821+
const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
1822+
if(!typedef_str.empty() &&
1823+
typedef_names.find(typedef_str)==typedef_names.end())
1824+
code.op0().type().remove(ID_C_typedef);
1825+
18211826
return;
18221827
}
18231828
else if(code.get_statement()==ID_function_call)

src/goto-instrument/goto_program2code.h

+3
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ class goto_program2codet
4949
code_blockt &_dest,
5050
id_listt &_local_static,
5151
id_listt &_type_names,
52+
const id_sett &_typedef_names,
5253
std::set<std::string> &_system_headers):
5354
func_name(identifier),
5455
goto_program(_goto_program),
@@ -57,6 +58,7 @@ class goto_program2codet
5758
toplevel_block(_dest),
5859
local_static(_local_static),
5960
type_names(_type_names),
61+
typedef_names(_typedef_names),
6062
system_headers(_system_headers)
6163
{
6264
assert(local_static.empty());
@@ -78,6 +80,7 @@ class goto_program2codet
7880
code_blockt &toplevel_block;
7981
id_listt &local_static;
8082
id_listt &type_names;
83+
const id_sett &typedef_names;
8184
std::set<std::string> &system_headers;
8285
std::unordered_set<exprt, irep_hash> va_list_expr;
8386

0 commit comments

Comments
 (0)