Skip to content

Commit a82e456

Browse files
author
Enrico Steffinlongo
authored
Merge pull request #7836 from esteffin/esteffin/shadow-memory-init
Shadow memory initialization functions
2 parents 1ecce42 + 4f5df20 commit a82e456

File tree

4 files changed

+202
-17
lines changed

4 files changed

+202
-17
lines changed

src/goto-symex/shadow_memory.cpp

Lines changed: 148 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,44 +12,80 @@ Author: Peter Schrammel
1212
#include "shadow_memory.h"
1313

1414
#include <util/bitvector_types.h>
15+
#include <util/expr_initializer.h>
16+
#include <util/format_expr.h>
1517
#include <util/format_type.h>
1618
#include <util/fresh_symbol.h>
19+
#include <util/pointer_expr.h>
20+
#include <util/prefix.h>
21+
#include <util/string_constant.h>
1722

1823
#include <langapi/language_util.h>
24+
#include <linking/static_lifetime_init.h>
1925

2026
#include "goto_symex_state.h"
2127
#include "shadow_memory_util.h"
2228

2329
void shadow_memoryt::initialize_shadow_memory(
2430
goto_symex_statet &state,
25-
const exprt &expr,
31+
exprt expr,
2632
const shadow_memory_field_definitionst::field_definitiont &fields)
2733
{
28-
// To be implemented
34+
typet type = ns.follow(expr.type());
35+
clean_pointer_expr(expr, type);
36+
for(const auto &field_pair : fields)
37+
{
38+
const symbol_exprt &shadow = add_field(state, expr, field_pair.first, type);
39+
40+
if(
41+
field_pair.second.id() == ID_typecast &&
42+
to_typecast_expr(field_pair.second).op().is_zero())
43+
{
44+
const auto zero_value =
45+
zero_initializer(type, expr.source_location(), ns);
46+
CHECK_RETURN(zero_value.has_value());
47+
48+
symex_assign(state, shadow, *zero_value);
49+
}
50+
else
51+
{
52+
exprt init_expr = field_pair.second;
53+
if(init_expr.id() == ID_typecast)
54+
init_expr = to_typecast_expr(field_pair.second).op();
55+
const auto init_value =
56+
expr_initializer(type, expr.source_location(), ns, init_expr);
57+
CHECK_RETURN(init_value.has_value());
58+
59+
symex_assign(state, shadow, *init_value);
60+
}
61+
62+
log.debug() << "Shadow memory: initialize field "
63+
<< id2string(shadow.get_identifier()) << " for " << format(expr)
64+
<< " with initial value " << format(field_pair.second)
65+
<< messaget::eom;
66+
}
2967
}
3068

31-
symbol_exprt shadow_memoryt::add_field(
69+
const symbol_exprt &shadow_memoryt::add_field(
3270
goto_symex_statet &state,
3371
const exprt &expr,
3472
const irep_idt &field_name,
3573
const typet &field_type)
3674
{
37-
// To be completed
38-
3975
const auto &function_symbol = ns.lookup(state.source.function_id);
40-
41-
symbolt &new_symbol = get_fresh_aux_symbol(
76+
const symbolt &new_symbol = get_fresh_aux_symbol(
4277
field_type,
4378
id2string(state.source.function_id),
4479
SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
4580
state.source.pc->source_location(),
4681
function_symbol.mode,
4782
state.symbol_table);
4883

49-
// Call some function on ns to silence the compiler in the meanwhile.
50-
ns.get_symbol_table();
84+
auto &addresses = state.shadow_memory.address_fields[field_name];
85+
addresses.push_back(
86+
shadow_memory_statet::shadowed_addresst{expr, new_symbol.symbol_expr()});
5187

52-
return new_symbol.symbol_expr();
88+
return addresses.back().shadow;
5389
}
5490

5591
void shadow_memoryt::symex_set_field(
@@ -67,34 +103,132 @@ void shadow_memoryt::symex_get_field(
67103
// To be implemented
68104
}
69105

106+
// TODO: the following 4 functions (`symex_field_static_init`,
107+
// `symex_field_static_init_string_constant`,
108+
// `symex_field_local_init`,
109+
// `symex_field_dynamic_init`) do filtering on
110+
// the input symbol name and then call `initialize_shadow_memory` accordingly.
111+
// We want to refactor and improve the way the filtering is done, but given
112+
// that we don't have an easy mechanism to validate that we haven't changed the
113+
// behaviour, we want to postpone changing this until the full shadow memory
114+
// functionalities are integrated and we have good regression/unit testing.
115+
70116
void shadow_memoryt::symex_field_static_init(
71117
goto_symex_statet &state,
72118
const ssa_exprt &lhs)
73119
{
74-
// To be implemented
120+
if(lhs.get_original_expr().id() != ID_symbol)
121+
return;
122+
123+
const irep_idt &identifier =
124+
to_symbol_expr(lhs.get_original_expr()).get_identifier();
125+
126+
if(state.source.function_id != INITIALIZE_FUNCTION)
127+
return;
128+
129+
if(
130+
has_prefix(id2string(identifier), CPROVER_PREFIX) &&
131+
!has_prefix(id2string(identifier), CPROVER_PREFIX "errno"))
132+
{
133+
return;
134+
}
135+
136+
const symbolt &symbol = ns.lookup(identifier);
137+
138+
if(
139+
(id2string(symbol.name).find("::return_value") == std::string::npos &&
140+
symbol.is_auxiliary) ||
141+
!symbol.is_static_lifetime)
142+
return;
143+
if(id2string(symbol.name).find("__cs_") != std::string::npos)
144+
return;
145+
146+
const typet &type = symbol.type;
147+
log.debug() << "Shadow memory: global memory " << id2string(identifier)
148+
<< " of type " << from_type(ns, "", type) << messaget::eom;
149+
150+
initialize_shadow_memory(
151+
state, lhs, state.shadow_memory.fields.global_fields);
75152
}
76153

77154
void shadow_memoryt::symex_field_static_init_string_constant(
78155
goto_symex_statet &state,
79156
const ssa_exprt &expr,
80157
const exprt &rhs)
81158
{
82-
// To be implemented
159+
if(
160+
expr.get_original_expr().id() == ID_symbol &&
161+
has_prefix(
162+
id2string(to_symbol_expr(expr.get_original_expr()).get_identifier()),
163+
CPROVER_PREFIX))
164+
{
165+
return;
166+
}
167+
const index_exprt &index_expr =
168+
to_index_expr(to_address_of_expr(rhs).object());
169+
170+
const typet &type = index_expr.array().type();
171+
log.debug() << "Shadow memory: global memory "
172+
<< id2string(to_string_constant(index_expr.array()).get_value())
173+
<< " of type " << from_type(ns, "", type) << messaget::eom;
174+
175+
initialize_shadow_memory(
176+
state, index_expr.array(), state.shadow_memory.fields.global_fields);
83177
}
84178

85179
void shadow_memoryt::symex_field_local_init(
86180
goto_symex_statet &state,
87181
const ssa_exprt &expr)
88182
{
89-
// To be implemented
183+
const symbolt &symbol =
184+
ns.lookup(to_symbol_expr(expr.get_original_expr()).get_identifier());
185+
186+
const std::string symbol_name = id2string(symbol.name);
187+
if(
188+
symbol.is_auxiliary &&
189+
symbol_name.find("::return_value") == std::string::npos)
190+
return;
191+
if(
192+
symbol_name.find("malloc::") != std::string::npos &&
193+
(symbol_name.find("malloc_size") != std::string::npos ||
194+
symbol_name.find("malloc_res") != std::string::npos ||
195+
symbol_name.find("record_malloc") != std::string::npos ||
196+
symbol_name.find("record_may_leak") != std::string::npos))
197+
{
198+
return;
199+
}
200+
if(
201+
symbol_name.find("__builtin_alloca::") != std::string::npos &&
202+
(symbol_name.find("alloca_size") != std::string::npos ||
203+
symbol_name.find("record_malloc") != std::string::npos ||
204+
symbol_name.find("record_alloca") != std::string::npos ||
205+
symbol_name.find("res") != std::string::npos))
206+
{
207+
return;
208+
}
209+
if(symbol_name.find("__cs_") != std::string::npos)
210+
return;
211+
212+
const typet &type = expr.type();
213+
ssa_exprt expr_l1 = remove_level_2(expr);
214+
log.debug() << "Shadow memory: local memory "
215+
<< id2string(expr_l1.get_identifier()) << " of type "
216+
<< from_type(ns, "", type) << messaget::eom;
217+
218+
initialize_shadow_memory(
219+
state, expr_l1, state.shadow_memory.fields.local_fields);
90220
}
91221

92222
void shadow_memoryt::symex_field_dynamic_init(
93223
goto_symex_statet &state,
94224
const exprt &expr,
95225
const side_effect_exprt &code)
96226
{
97-
// To be implemented
227+
log.debug() << "Shadow memory: dynamic memory of type "
228+
<< from_type(ns, "", expr.type()) << messaget::eom;
229+
230+
initialize_shadow_memory(
231+
state, expr, state.shadow_memory.fields.global_fields);
98232
}
99233

100234
shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations(

src/goto-symex/shadow_memory.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Peter Schrammel
1414

1515
#include <util/expr.h>
1616
#include <util/message.h>
17-
#include <util/std_expr.h>
1817

1918
#include "shadow_memory_field_definitions.h"
2019

@@ -30,6 +29,7 @@ class abstract_goto_modelt;
3029
class goto_symex_statet;
3130
class side_effect_exprt;
3231
class ssa_exprt;
32+
class symbol_exprt;
3333

3434
/// \brief The shadow memory instrumentation performed during symbolic execution
3535
class shadow_memoryt
@@ -115,7 +115,7 @@ class shadow_memoryt
115115
/// \param fields The field definition to be used
116116
void initialize_shadow_memory(
117117
goto_symex_statet &state,
118-
const exprt &expr,
118+
exprt expr,
119119
const shadow_memory_field_definitionst::field_definitiont &fields);
120120

121121
/// Registers a shadow memory field for the given original memory
@@ -124,7 +124,7 @@ class shadow_memoryt
124124
/// \param field_name The field name
125125
/// \param field_type The field type
126126
/// \return The resulting shadow memory symbol expression
127-
symbol_exprt add_field(
127+
const symbol_exprt &add_field(
128128
goto_symex_statet &state,
129129
const exprt &expr,
130130
const irep_idt &field_name,

src/goto-symex/shadow_memory_util.cpp

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,10 @@ Author: Peter Schrammel
1111

1212
#include "shadow_memory_util.h"
1313

14+
#include <util/c_types.h>
1415
#include <util/invariant.h>
1516
#include <util/pointer_expr.h>
17+
#include <util/ssa_expr.h>
1618
#include <util/std_expr.h>
1719

1820
irep_idt extract_field_name(const exprt &string_expr)
@@ -30,3 +32,42 @@ irep_idt extract_field_name(const exprt &string_expr)
3032
else
3133
UNREACHABLE;
3234
}
35+
36+
/// If the given type is an array type, then remove the L2 level
37+
/// renaming from its size.
38+
/// \param type Type to be modified
39+
static void remove_array_type_l2(typet &type)
40+
{
41+
if(to_array_type(type).size().id() != ID_symbol)
42+
return;
43+
44+
ssa_exprt &size = to_ssa_expr(to_array_type(type).size());
45+
size.remove_level_2();
46+
}
47+
48+
void clean_pointer_expr(exprt &expr, const typet &type)
49+
{
50+
if(
51+
type.id() == ID_array && expr.id() == ID_symbol &&
52+
to_array_type(type).size().get_bool(ID_C_SSA_symbol))
53+
{
54+
remove_array_type_l2(expr.type());
55+
exprt original_expr = to_ssa_expr(expr).get_original_expr();
56+
remove_array_type_l2(original_expr.type());
57+
to_ssa_expr(expr).set_expression(original_expr);
58+
}
59+
if(expr.id() == ID_string_constant)
60+
{
61+
expr = address_of_exprt(expr);
62+
expr.type() = pointer_type(char_type());
63+
}
64+
else if(expr.id() == ID_dereference)
65+
{
66+
expr = to_dereference_expr(expr).pointer();
67+
}
68+
else
69+
{
70+
expr = address_of_exprt(expr);
71+
}
72+
POSTCONDITION(expr.type().id() == ID_pointer);
73+
}

src/goto-symex/shadow_memory_util.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,21 @@ Author: Peter Schrammel
1515
#include <util/irep.h>
1616

1717
class exprt;
18+
class typet;
1819

1920
/// Extracts the field name identifier from a string expression,
2021
/// e.g. as passed as argument to a __CPROVER_field_decl_local call.
2122
/// \param string_expr The string argument expression
2223
/// \return The identifier denoted by the string argument expression
2324
irep_idt extract_field_name(const exprt &string_expr);
2425

26+
/// Clean the given pointer expression so that it has the right
27+
/// shape for being used for identifying shadow memory.
28+
/// This handles some quirks regarding array sizes containing
29+
/// L2 symbols and string constants not having char-pointer type.
30+
/// \param expr The pointer to the original memory, e.g. as passed to
31+
/// __CPROVER_field_get.
32+
/// \param type The followed type of expr.
33+
void clean_pointer_expr(exprt &expr, const typet &type);
34+
2535
#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H

0 commit comments

Comments
 (0)