Skip to content

Commit 242a89d

Browse files
tautschnigtautschnig
committed
Move casting_replace_symbolt to files of their own
Increase readability of linking code by moving aside code that is not specific to just linking.
1 parent 4337587 commit 242a89d

File tree

5 files changed

+135
-102
lines changed

5 files changed

+135
-102
lines changed

‎src/linking/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
SRC = linking.cpp \
1+
SRC = casting_replace_symbol.cpp \
2+
linking.cpp \
23
remove_internal_symbols.cpp \
34
static_lifetime_init.cpp \
45
# Empty last line

‎src/linking/casting_replace_symbol.cpp

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
/*******************************************************************\
2+
3+
Module: ANSI-C Linking
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// ANSI-C Linking
11+
12+
#include "casting_replace_symbol.h"
13+
14+
bool casting_replace_symbolt::replace(exprt &dest) const
15+
{
16+
bool result = true; // unchanged
17+
18+
// first look at type
19+
20+
const exprt &const_dest(dest);
21+
if(have_to_replace(const_dest.type()))
22+
if(!replace_symbolt::replace(dest.type()))
23+
result = false;
24+
25+
// now do expression itself
26+
27+
if(!have_to_replace(dest))
28+
return result;
29+
30+
if(dest.id() == ID_side_effect)
31+
{
32+
if(auto call = expr_try_dynamic_cast<side_effect_expr_function_callt>(dest))
33+
{
34+
if(!have_to_replace(call->function()))
35+
return replace_symbolt::replace(dest);
36+
37+
exprt before = dest;
38+
code_typet type = to_code_type(call->function().type());
39+
40+
result &= replace_symbolt::replace(call->function());
41+
42+
// maybe add type casts here?
43+
for(auto &arg : call->arguments())
44+
result &= replace_symbolt::replace(arg);
45+
46+
if(
47+
type.return_type() !=
48+
to_code_type(call->function().type()).return_type())
49+
{
50+
call->type() = to_code_type(call->function().type()).return_type();
51+
dest = typecast_exprt(*call, type.return_type());
52+
result = true;
53+
}
54+
55+
return result;
56+
}
57+
}
58+
else if(dest.id() == ID_address_of)
59+
{
60+
pointer_typet ptr_type = to_pointer_type(dest.type());
61+
62+
result &= replace_symbolt::replace(dest);
63+
64+
address_of_exprt address_of = to_address_of_expr(dest);
65+
if(address_of.object().type() != ptr_type.base_type())
66+
{
67+
to_pointer_type(address_of.type()).base_type() =
68+
address_of.object().type();
69+
dest = typecast_exprt{address_of, std::move(ptr_type)};
70+
result = true;
71+
}
72+
73+
return result;
74+
}
75+
76+
return replace_symbolt::replace(dest);
77+
}
78+
79+
bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
80+
{
81+
expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
82+
83+
if(it == expr_map.end())
84+
return true;
85+
86+
const exprt &e = it->second;
87+
88+
source_locationt previous_source_location{s.source_location()};
89+
DATA_INVARIANT_WITH_DIAGNOSTICS(
90+
previous_source_location.is_not_nil(),
91+
"front-ends should construct symbol expressions with source locations",
92+
s.pretty());
93+
if(e.type().id() != ID_array && e.type().id() != ID_code)
94+
{
95+
typet type = s.type();
96+
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
97+
}
98+
else
99+
static_cast<exprt &>(s) = e;
100+
s.add_source_location() = std::move(previous_source_location);
101+
102+
return false;
103+
}

‎src/linking/casting_replace_symbol.h

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: ANSI-C Linking
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// ANSI-C Linking
11+
12+
#ifndef CPROVER_LINKING_CASTING_REPLACE_SYMBOL_H
13+
#define CPROVER_LINKING_CASTING_REPLACE_SYMBOL_H
14+
15+
#include <util/replace_symbol.h>
16+
17+
/// A variant of \ref replace_symbolt that does not require types to match, but
18+
/// instead inserts type casts as needed when replacing one symbol by another.
19+
class casting_replace_symbolt : public replace_symbolt
20+
{
21+
public:
22+
bool replace(exprt &dest) const override;
23+
24+
private:
25+
bool replace_symbol_expr(symbol_exprt &dest) const override;
26+
};
27+
28+
#endif // CPROVER_LINKING_CASTING_REPLACE_SYMBOL_H

‎src/linking/linking.cpp

Lines changed: 0 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -26,97 +26,6 @@ Author: Daniel Kroening, [email protected]
2626

2727
#include <deque>
2828

29-
bool casting_replace_symbolt::replace(exprt &dest) const
30-
{
31-
bool result = true; // unchanged
32-
33-
// first look at type
34-
35-
const exprt &const_dest(dest);
36-
if(have_to_replace(const_dest.type()))
37-
if(!replace_symbolt::replace(dest.type()))
38-
result = false;
39-
40-
// now do expression itself
41-
42-
if(!have_to_replace(dest))
43-
return result;
44-
45-
if(dest.id() == ID_side_effect)
46-
{
47-
if(auto call = expr_try_dynamic_cast<side_effect_expr_function_callt>(dest))
48-
{
49-
if(!have_to_replace(call->function()))
50-
return replace_symbolt::replace(dest);
51-
52-
exprt before = dest;
53-
code_typet type = to_code_type(call->function().type());
54-
55-
result &= replace_symbolt::replace(call->function());
56-
57-
// maybe add type casts here?
58-
for(auto &arg : call->arguments())
59-
result &= replace_symbolt::replace(arg);
60-
61-
if(
62-
type.return_type() !=
63-
to_code_type(call->function().type()).return_type())
64-
{
65-
call->type() = to_code_type(call->function().type()).return_type();
66-
dest = typecast_exprt(*call, type.return_type());
67-
result = true;
68-
}
69-
70-
return result;
71-
}
72-
}
73-
else if(dest.id() == ID_address_of)
74-
{
75-
pointer_typet ptr_type = to_pointer_type(dest.type());
76-
77-
result &= replace_symbolt::replace(dest);
78-
79-
address_of_exprt address_of = to_address_of_expr(dest);
80-
if(address_of.object().type() != ptr_type.base_type())
81-
{
82-
to_pointer_type(address_of.type()).base_type() =
83-
address_of.object().type();
84-
dest = typecast_exprt{address_of, std::move(ptr_type)};
85-
result = true;
86-
}
87-
88-
return result;
89-
}
90-
91-
return replace_symbolt::replace(dest);
92-
}
93-
94-
bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
95-
{
96-
expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
97-
98-
if(it == expr_map.end())
99-
return true;
100-
101-
const exprt &e = it->second;
102-
103-
source_locationt previous_source_location{s.source_location()};
104-
DATA_INVARIANT_WITH_DIAGNOSTICS(
105-
previous_source_location.is_not_nil(),
106-
"front-ends should construct symbol expressions with source locations",
107-
s.pretty());
108-
if(e.type().id() != ID_array && e.type().id() != ID_code)
109-
{
110-
typet type = s.type();
111-
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
112-
}
113-
else
114-
static_cast<exprt &>(s) = e;
115-
s.add_source_location() = std::move(previous_source_location);
116-
117-
return false;
118-
}
119-
12029
static const typet &follow_tags_symbols(
12130
const namespacet &ns,
12231
const typet &type)

‎src/linking/linking_class.h

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,23 +14,15 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/namespace.h>
1616
#include <util/rename_symbol.h>
17-
#include <util/replace_symbol.h>
1817
#include <util/std_expr.h>
1918
#include <util/symbol.h>
2019

20+
#include "casting_replace_symbol.h"
21+
2122
#include <unordered_set>
2223

2324
class message_handlert;
2425

25-
class casting_replace_symbolt : public replace_symbolt
26-
{
27-
public:
28-
bool replace(exprt &dest) const override;
29-
30-
private:
31-
bool replace_symbol_expr(symbol_exprt &dest) const override;
32-
};
33-
3426
class linkingt
3527
{
3628
public:

0 commit comments

Comments
 (0)