Skip to content

Commit ced9234

Browse files
committed
irept: use single map for all named sub-nodes
1 parent 5e68531 commit ced9234

File tree

17 files changed

+208
-245
lines changed

17 files changed

+208
-245
lines changed

src/ansi-c/README.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -78,9 +78,9 @@ data structures. In particular, \ref exprt "expressions",
7878
An irep is a tree of ireps. A subtlety is that an irep is actually the
7979
root of _three_ (possibly empty) trees, i.e. it has three disjoint sets
8080
of children: \ref irept::get_sub() returns a list of children, and
81-
\ref irept::get_named_sub() and \ref irept::get_comments() each return an
82-
association from names to children. **Most clients never use these
83-
functions directly**, as subtypes of irept generally provide more
81+
\ref irept::get_named_sub() returns an association from names to children.
82+
**Most clients never use these functions directly**,
83+
as subtypes of irept generally provide more
8484
descriptive functions. For example, the operands of an
8585
\ref exprt "expression" (\ref exprt::op0() "op0", op1 etc) are
8686
really that expression's children; the

src/cpp/cpp_type2name.cpp

Lines changed: 14 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -36,30 +36,29 @@ static void irep2name(const irept &irep, std::string &result)
3636
if(irep.id()!="")
3737
result+=do_prefix(irep.id_string());
3838

39-
if(irep.get_named_sub().empty() &&
40-
irep.get_sub().empty() &&
41-
irep.get_comments().empty())
39+
if(irep.get_named_sub().empty() && irep.get_sub().empty())
4240
return;
4341

4442
result+='(';
4543
bool first=true;
4644

4745
forall_named_irep(it, irep.get_named_sub())
48-
{
49-
if(first)
50-
first=false;
51-
else
52-
result+=',';
46+
if(!irept::is_comment(it->first))
47+
{
48+
if(first)
49+
first = false;
50+
else
51+
result += ',';
5352

54-
result+=do_prefix(name2string(it->first));
53+
result += do_prefix(name2string(it->first));
5554

56-
result+='=';
57-
std::string tmp;
58-
irep2name(it->second, tmp);
59-
result+=tmp;
60-
}
55+
result += '=';
56+
std::string tmp;
57+
irep2name(it->second, tmp);
58+
result += tmp;
59+
}
6160

62-
forall_named_irep(it, irep.get_comments())
61+
forall_named_irep(it, irep.get_named_sub())
6362
if(it->first==ID_C_constant ||
6463
it->first==ID_C_volatile ||
6564
it->first==ID_C_restricted)

src/goto-programs/json_goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ void convert_decl(
155155
if(trace_options.json_full_lhs)
156156
{
157157
// Not language specific, still mangled, fully-qualified name of lhs
158-
json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
158+
json_assignment["rawLhs"] = json_irept().convert_from_irep(simplified);
159159
}
160160
json_assignment["hidden"] = jsont::json_boolean(step.hidden);
161161
json_assignment["internal"] = jsont::json_boolean(step.internal);

src/goto-programs/show_goto_functions_json.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ json_objectt show_goto_functions_jsont::convert(
4040
const goto_functionst &goto_functions)
4141
{
4242
json_arrayt json_functions;
43-
const json_irept no_comments_irep_converter(false);
43+
const json_irept no_comments_irep_converter;
4444

4545
const auto sorted = goto_functions.sorted();
4646

src/goto-programs/show_symbol_table.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ static void show_symbol_table_json_ui(
166166
result_wrapper.push_back_stream_object("symbolTable");
167167

168168
const namespacet ns(symbol_table);
169-
json_irept irep_converter(true);
169+
json_irept irep_converter;
170170

171171
for(const auto &id_and_symbol : symbol_table.symbols)
172172
{
@@ -241,7 +241,7 @@ static void show_symbol_table_brief_json_ui(
241241
result_wrapper.push_back_stream_object("symbolTable");
242242

243243
const namespacet ns(symbol_table);
244-
json_irept irep_converter(true);
244+
json_irept irep_converter;
245245

246246
for(const auto &id_and_symbol : symbol_table.symbols)
247247
{

src/json-symtab-language/json_symbol.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ symbolt symbol_from_json(const jsont &in)
4747
if(!in.is_object())
4848
throw deserialization_exceptiont("symbol_from_json takes an object");
4949
symbolt result;
50-
json_irept json2irep(true);
50+
json_irept json2irep;
5151
for(const auto &kv : in.object)
5252
{
5353
if(kv.first == "type")

src/util/README.md

Lines changed: 17 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,15 @@ CPROVER codebase.
1414

1515
See detailed documentation at \ref irept.
1616

17-
[irept](\ref irept)s are generic tree nodes. You
18-
should think of each node as holding a single string ([data](\ref irept::data),
19-
actually an \ref irep_idt) and lots of child nodes, some of which are numbered
20-
([sub](\ref irept::dt::sub)) and some of which are labelled, and the label
21-
can either start with a “\#([comments](\ref irept::dt::comments)) or without
22-
one ([named_sub](\ref irept::dt::named_sub)). The meaning of the “\#” is that
23-
this child shouldn't be counted when comparing two [irept](\ref irept)s for
24-
equality; this is usually used when making an advisory annotation which does
25-
not alter the semantics of the program.
17+
[irept](\ref irept)s are generic tree nodes. You should think of each node
18+
as holding a single string ([data](\ref irept::data), actually an \ref
19+
irep_idt) and lots of child nodes, some of which are numbered ([sub](\ref
20+
irept::dt::sub)) and some of which are labelled ([named_sub](\ref
21+
irept::dt::named_sub)). The the label can either start with a “\#or
22+
without one. The meaning of the “\#” is that this child shouldn't be
23+
considered when comparing two [irept](\ref irept)s for equality; this is
24+
usually used when making an advisory annotation which does not alter the
25+
semantics of the program.
2626

2727
They are used to represent many kinds of structured objects throughout the
2828
CPROVER codebase, such as expressions, types and code. An \ref exprt represents
@@ -72,9 +72,8 @@ standard data structures as in irept.
7272

7373
\subsection irep_idt_section Strings: dstringt, the string_container and the ID_*
7474

75-
Within cbmc, strings are represented using \ref irep_idt, or \ref irep_namet
76-
for keys to [named_sub](\ref irept::dt::named_sub) or
77-
[comments](\ref irept::dt::comments). By default these are both
75+
Within cbmc, strings are represented using \ref irep_idt or \ref irep_namet
76+
for keys to [named_sub](\ref irept::dt::named_sub). By default these are both
7877
typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`,
7978
in which case they are both typedefed to `std::string`. You can also easily
8079
convert an [irep_idt](\ref irep_idt) or [irep_namet](\ref irep_namet) to a
@@ -91,11 +90,10 @@ in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has ind
9190
You can refer to this \ref irep_idt as `ID_type`. The other kind of line you
9291
see is \c "IREP_ID_TWO(C_source_location, #source_location)", which means the
9392
\ref irep_idt for the string “\#source_location” can be referred to as
94-
`ID_C_source_location`. The “C” is for comment, meaning that it should be
95-
stored in the [comments](\ref irept::dt::comments). Any strings that need
96-
to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def`
97-
are added to the end of the table when they are first encountered, and the
98-
same index is used for all instances.
93+
`ID_C_source_location`. The “C” is for comment, meaning that it starts with
94+
\#”. Any strings that need to be stored as [irep_idt](\ref irep_idt)s
95+
which aren't in `irep_ids.def` are added to the end of the table when they
96+
are first encountered, and the same index is used for all instances.
9997

10098
See documentation at \ref dstringt.
10199

@@ -125,8 +123,8 @@ of size 2 (for the two arguments of minus).
125123

126124
Recall that every \ref irept has one piece of data of its own, i.e. its
127125
[id()](\ref irept::id()), and all other information is in its
128-
[named_sub](\ref irept::dt::named_sub), [comments](\ref irept::dt::comments)
129-
or [sub](\ref irept::dt::sub). For [exprt](\ref exprt)s, the
126+
[named_sub](\ref irept::dt::named_sub) or [sub](\ref irept::dt::sub).
127+
For [exprt](\ref exprt)s, the
130128
[id()](\ref irept::id()) is used to specify why kind of \ref exprt this is,
131129
so a \ref minus_exprt has `ID_minus` as its [id()](\ref irept::id()). This
132130
means that a \ref minus_exprt can be passed wherever an \ref exprt is

0 commit comments

Comments
 (0)