Skip to content

Commit f4fff94

Browse files
authored
Merge pull request #3913 from tautschnig/irept-opt-move
Encapsulate ID_already_typechecked in a proper API
2 parents 409c492 + 09410a6 commit f4fff94

16 files changed

+105
-95
lines changed

src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -643,7 +643,7 @@ void c_typecheck_baset::typecheck_declaration(
643643
typecheck_type(declaration.type());
644644

645645
// mark as 'already typechecked'
646-
make_already_typechecked(declaration.type());
646+
already_typechecked_typet::make_already_typechecked(declaration.type());
647647

648648
irept contract;
649649

src/ansi-c/c_typecheck_base.h

Lines changed: 56 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -225,13 +225,6 @@ class c_typecheck_baset:
225225
const mp_integer &min, const mp_integer &max,
226226
bool is_packed) const;
227227

228-
void make_already_typechecked(typet &dest)
229-
{
230-
typet result(ID_already_typechecked);
231-
result.subtype().swap(dest);
232-
result.swap(dest);
233-
}
234-
235228
// this cleans expressions in array types
236229
std::list<codet> clean_code;
237230

@@ -272,4 +265,60 @@ class c_typecheck_baset:
272265
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
273266
};
274267

268+
class already_typechecked_exprt : public expr_protectedt
269+
{
270+
public:
271+
explicit already_typechecked_exprt(exprt expr)
272+
: expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
273+
{
274+
}
275+
276+
static void make_already_typechecked(exprt &expr)
277+
{
278+
already_typechecked_exprt a{expr};
279+
expr.swap(a);
280+
}
281+
282+
exprt &get_expr()
283+
{
284+
return op0();
285+
}
286+
};
287+
288+
class already_typechecked_typet : public type_with_subtypet
289+
{
290+
public:
291+
explicit already_typechecked_typet(typet type)
292+
: type_with_subtypet(ID_already_typechecked, std::move(type))
293+
{
294+
}
295+
296+
static void make_already_typechecked(typet &type)
297+
{
298+
already_typechecked_typet a{type};
299+
type.swap(a);
300+
}
301+
302+
typet &get_type()
303+
{
304+
return subtype();
305+
}
306+
};
307+
308+
inline already_typechecked_exprt &to_already_typechecked_expr(exprt &expr)
309+
{
310+
PRECONDITION(expr.id() == ID_already_typechecked);
311+
PRECONDITION(expr.operands().size() == 1);
312+
313+
return static_cast<already_typechecked_exprt &>(expr);
314+
}
315+
316+
inline already_typechecked_typet &to_already_typechecked_type(typet &type)
317+
{
318+
PRECONDITION(type.id() == ID_already_typechecked);
319+
PRECONDITION(type.has_subtype());
320+
321+
return static_cast<already_typechecked_typet &>(type);
322+
}
323+
275324
#endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)
3838
{
3939
if(expr.id()==ID_already_typechecked)
4040
{
41-
assert(expr.operands().size()==1);
42-
exprt tmp;
43-
tmp.swap(expr.op0());
44-
expr.swap(tmp);
41+
expr.swap(to_already_typechecked_expr(expr).get_expr());
4542
return;
4643
}
4744

src/ansi-c/c_typecheck_type.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,17 @@ void c_typecheck_baset::typecheck_type(typet &type)
4040

4141
if(type.id()==ID_already_typechecked)
4242
{
43+
already_typechecked_typet &already_typechecked =
44+
to_already_typechecked_type(type);
45+
4346
// need to preserve any qualifiers
4447
c_qualifierst c_qualifiers(type);
45-
c_qualifiers+=c_qualifierst(type.subtype());
48+
c_qualifiers += c_qualifierst(already_typechecked.get_type());
4649
bool packed=type.get_bool(ID_C_packed);
4750
exprt alignment=static_cast<const exprt &>(type.find(ID_C_alignment));
4851
irept _typedef=type.find(ID_C_typedef);
4952

50-
type=type.subtype();
53+
type = already_typechecked.get_type();
5154

5255
c_qualifiers.write(type);
5356
if(packed)
@@ -896,7 +899,7 @@ void c_typecheck_baset::typecheck_compound_body(
896899
{
897900
// do first half of type
898901
typecheck_type(declaration.type());
899-
make_already_typechecked(declaration.type());
902+
already_typechecked_typet::make_already_typechecked(declaration.type());
900903

901904
for(const auto &declarator : declaration.declarators())
902905
{

src/cpp/cpp_constructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ void cpp_typecheckt::new_temporary(
276276
new_object.set(ID_C_lvalue, true);
277277
new_object.type()=tmp_object_expr.type();
278278

279-
already_typechecked(new_object);
279+
already_typechecked_exprt::make_already_typechecked(new_object);
280280

281281
auto new_code = cpp_constructor(source_location, new_object, ops);
282282

src/cpp/cpp_destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,7 +109,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
109109
std::move(member), {}, uninitialized_typet{}, source_location);
110110

111111
typecheck_side_effect_function_call(function_call);
112-
already_typechecked(function_call);
112+
already_typechecked_exprt::make_already_typechecked(function_call);
113113

114114
code_expressiont new_code(function_call);
115115
new_code.add_source_location() = source_location;

src/cpp/cpp_typecheck_code.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -359,7 +359,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
359359
else
360360
{
361361
// it's a data member
362-
already_typechecked(symbol_expr);
362+
already_typechecked_exprt::make_already_typechecked(symbol_expr);
363363

364364
auto call =
365365
cpp_constructor(code.source_location(), symbol_expr, code.operands());
@@ -423,7 +423,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
423423
}
424424

425425
// mark as 'already typechecked'
426-
make_already_typechecked(type);
426+
already_typechecked_typet::make_already_typechecked(type);
427427

428428
codet new_code(ID_decl_block);
429429
new_code.reserve_operands(declaration.declarators().size());
@@ -469,7 +469,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
469469
{
470470
exprt object_expr=cpp_symbol_expr(symbol);
471471

472-
already_typechecked(object_expr);
472+
already_typechecked_exprt::make_already_typechecked(object_expr);
473473

474474
auto constructor_call = cpp_constructor(
475475
symbol.location, object_expr, declarator.init_args().operands());

src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -668,17 +668,16 @@ void cpp_typecheckt::typecheck_compound_declarator(
668668
code_type.return_type().id()!=ID_destructor)
669669
{
670670
expr_call.type()=to_code_type(component.type()).return_type();
671-
exprt already_typechecked(ID_already_typechecked);
672-
already_typechecked.add_to_operands(std::move(expr_call));
673671

674-
func_symb.value = code_returnt(already_typechecked).make_block();
672+
func_symb.value =
673+
code_returnt(already_typechecked_exprt{std::move(expr_call)})
674+
.make_block();
675675
}
676676
else
677677
{
678-
exprt already_typechecked(ID_already_typechecked);
679-
already_typechecked.add_to_operands(std::move(expr_call));
680-
681-
func_symb.value = code_expressiont(already_typechecked).make_block();
678+
func_symb.value =
679+
code_expressiont(already_typechecked_exprt{std::move(expr_call)})
680+
.make_block();
682681
}
683682

684683
// add this new function to the list of components

src/cpp/cpp_typecheck_constructor.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -235,7 +235,7 @@ void cpp_typecheckt::default_cpctor(
235235
address_of_exprt address(var);
236236
assert(address.type() == mem_c.type());
237237

238-
already_typechecked(address);
238+
already_typechecked_exprt::make_already_typechecked(address);
239239

240240
exprt ptrmember(ID_ptrmember);
241241
ptrmember.set(ID_component_name, mem_c.get_name());
@@ -690,7 +690,7 @@ void cpp_typecheckt::full_member_initialization(
690690
address_of_exprt address(var);
691691
assert(address.type() == c.type());
692692

693-
already_typechecked(address);
693+
already_typechecked_exprt::make_already_typechecked(address);
694694

695695
exprt ptrmember(ID_ptrmember);
696696
ptrmember.set(ID_component_name, c.get_name());

src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 9 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -971,11 +971,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
971971

972972
exprt func_symb = cpp_symbol_expr(lookup(component.get_name()));
973973
func_symb.type()=comp_type;
974-
{
975-
exprt tmp(ID_already_typechecked);
976-
tmp.copy_to_operands(func_symb);
977-
func_symb.swap(func_symb);
978-
}
974+
already_typechecked_exprt::make_already_typechecked(func_symb);
979975

980976
// create temporary object
981977
side_effect_expr_function_callt ctor_expr(
@@ -1023,11 +1019,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
10231019

10241020
exprt func_symb = cpp_symbol_expr(lookup(component.get_name()));
10251021
func_symb.type()=comp_type;
1026-
{
1027-
exprt tmp(ID_already_typechecked);
1028-
tmp.copy_to_operands(func_symb);
1029-
func_symb.swap(func_symb);
1030-
}
1022+
already_typechecked_exprt::make_already_typechecked(func_symb);
10311023

10321024
side_effect_expr_function_callt ctor_expr(
10331025
std::move(func_symb),
@@ -1086,9 +1078,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
10861078

10871079
exprt member_func(ID_member);
10881080
member_func.add(ID_component_cpp_name)=cpp_func_name;
1089-
exprt ac(ID_already_typechecked);
1090-
ac.copy_to_operands(expr);
1091-
member_func.copy_to_operands(ac);
1081+
member_func.copy_to_operands(already_typechecked_exprt{expr});
10921082

10931083
side_effect_expr_function_callt func_expr(
10941084
std::move(member_func),
@@ -1326,9 +1316,7 @@ bool cpp_typecheckt::reference_binding(
13261316

13271317
exprt member_func(ID_member);
13281318
member_func.add(ID_component_cpp_name)=cpp_func_name;
1329-
exprt ac(ID_already_typechecked);
1330-
ac.copy_to_operands(expr);
1331-
member_func.copy_to_operands(ac);
1319+
member_func.copy_to_operands(already_typechecked_exprt{expr});
13321320

13331321
side_effect_expr_function_callt func_expr(
13341322
std::move(member_func),
@@ -1932,10 +1920,12 @@ bool cpp_typecheckt::static_typecast(
19321920
{
19331921
if(!cpp_is_pod(type))
19341922
{
1935-
exprt tc(ID_already_typechecked);
1936-
tc.copy_to_operands(new_expr);
19371923
exprt temporary;
1938-
new_temporary(e.source_location(), type, tc, temporary);
1924+
new_temporary(
1925+
e.source_location(),
1926+
type,
1927+
already_typechecked_exprt{new_expr},
1928+
temporary);
19391929
new_expr.swap(temporary);
19401930
}
19411931
else

src/cpp/cpp_typecheck_declaration.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ void cpp_typecheckt::convert_non_template_declaration(
116116

117117
// mark as 'already typechecked'
118118
if(!declaration.declarators().empty())
119-
make_already_typechecked(declaration_type);
119+
already_typechecked_typet::make_already_typechecked(declaration_type);
120120

121121
// Special treatment for anonymous unions
122122
if(declaration.declarators().empty() &&

src/cpp/cpp_typecheck_destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr)
8181
address_of_exprt address(var);
8282
assert(address.type() == c.type());
8383

84-
already_typechecked(address);
84+
already_typechecked_exprt::make_already_typechecked(address);
8585

8686
exprt ptrmember(ID_ptrmember);
8787
ptrmember.set(ID_component_name, c.get_name());

0 commit comments

Comments
 (0)