Skip to content

Commit 78be04f

Browse files
author
Enrico Steffinlongo
committed
Implementat shadow memory symex_get_field
Add implementation to shadow_memoryt::symex_get_field also adding its subfunctions.
1 parent 8bbfed7 commit 78be04f

File tree

1 file changed

+140
-1
lines changed

1 file changed

+140
-1
lines changed

src/goto-symex/shadow_memory.cpp

Lines changed: 140 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,12 +95,151 @@ void shadow_memoryt::symex_set_field(
9595
// To be implemented
9696
}
9797

98+
// Function synopsis
99+
// value_set = get_value_set(expr)
100+
// foreach object in value_set:
101+
// if(object invalid) continue;
102+
// get_field(&exact_match)
103+
// if(exact_match)
104+
// return;
105+
// return;
98106
void shadow_memoryt::symex_get_field(
99107
goto_symex_statet &state,
100108
const exprt &lhs,
101109
const exprt::operandst &arguments)
102110
{
103-
// To be implemented
111+
INVARIANT(
112+
arguments.size() == 2, CPROVER_PREFIX "get_field requires 2 arguments");
113+
irep_idt field_name = extract_field_name(arguments[1]);
114+
115+
exprt expr = arguments[0];
116+
typet expr_type = expr.type();
117+
DATA_INVARIANT(
118+
expr_type.id() == ID_pointer,
119+
"shadow memory requires a pointer expression");
120+
log_get_field(ns, log, field_name, expr);
121+
122+
INVARIANT(
123+
state.shadow_memory.address_fields.count(field_name) == 1,
124+
id2string(field_name) + " should exist");
125+
const auto &addresses = state.shadow_memory.address_fields.at(field_name);
126+
127+
// Return null (invalid object) instead of auto-object or invalid-object.
128+
// This will "polish" expr from invalid and auto-obj
129+
replace_invalid_object_by_null(expr);
130+
131+
std::vector<exprt> value_set = state.value_set.get_value_set(expr, ns);
132+
log_value_set(ns, log, value_set);
133+
134+
std::vector<std::pair<exprt, exprt>> rhs_conds_values;
135+
const null_pointer_exprt null_pointer(to_pointer_type(expr.type()));
136+
// Used to give a default value for invalid pointers and other usages
137+
const exprt &field_init_expr = get_field_init_expr(field_name, state);
138+
139+
if(contains_null_or_invalid(value_set, null_pointer))
140+
{
141+
log_value_set_match(ns, log, null_pointer, expr);
142+
// If we have an invalid pointer, then return the default value of the
143+
// shadow memory as dereferencing it would fail
144+
rhs_conds_values.emplace_back(
145+
true_exprt(),
146+
typecast_exprt::conditional_cast(field_init_expr, lhs.type()));
147+
}
148+
149+
for(const auto &matched_object : value_set)
150+
{
151+
// Ignore "unknown"
152+
if(matched_object.id() != ID_object_descriptor)
153+
{
154+
log.warning() << "Shadow memory: value set contains unknown for "
155+
<< format(expr) << messaget::eom;
156+
continue;
157+
}
158+
// Ignore "integer_address"
159+
if(
160+
to_object_descriptor_expr(matched_object).root_object().id() ==
161+
ID_integer_address)
162+
{
163+
log.warning() << "Shadow memory: value set contains integer_address for "
164+
<< format(expr) << messaget::eom;
165+
continue;
166+
}
167+
// Ignore "ID_C_is_failed_symbol" (another incarnation of invalid pointer)
168+
// TODO: check if this is obsolete (or removed by
169+
// replace_invalid_object_by_null) or add default value
170+
if(matched_object.type().get_bool(ID_C_is_failed_symbol))
171+
{
172+
log.warning() << "Shadow memory: value set contains failed symbol for "
173+
<< format(expr) << messaget::eom;
174+
continue;
175+
}
176+
177+
bool exact_match = false;
178+
179+
// List of condition ==> value (read condition implies values)
180+
auto per_matched_object_conds_values = get_shadow_dereference_candidates(
181+
ns,
182+
log,
183+
matched_object,
184+
addresses,
185+
field_init_expr.type(),
186+
expr,
187+
lhs.type(),
188+
exact_match);
189+
190+
// If we have an exact match we discard all the previous conditions and
191+
// create an assignment. Then we'll break
192+
if(exact_match)
193+
{
194+
rhs_conds_values.clear();
195+
}
196+
// Process this match (exact will contain only one set of conditions).
197+
rhs_conds_values.insert(
198+
rhs_conds_values.end(),
199+
per_matched_object_conds_values.begin(),
200+
per_matched_object_conds_values.end());
201+
if(exact_match)
202+
{
203+
break;
204+
}
205+
}
206+
207+
// If we have at least a condition ==> value
208+
if(!rhs_conds_values.empty())
209+
{
210+
// Build the rhs expression from the shadow memory (big switch for all
211+
// condition ==> value)
212+
exprt rhs = typecast_exprt::conditional_cast(
213+
build_if_else_expr(rhs_conds_values), lhs.type());
214+
const size_t mux_size = rhs_conds_values.size() - 1;
215+
// Don't debug if the switch is too big
216+
if(mux_size >= 10)
217+
{
218+
log.warning() << "Shadow memory: mux size get_field: " << mux_size
219+
<< messaget::eom;
220+
}
221+
else
222+
{
223+
log.debug() << "Shadow memory: mux size get_field: " << mux_size
224+
<< messaget::eom;
225+
}
226+
#ifdef DEBUG_SM
227+
log.debug() << "Shadow memory: RHS: " << format(rhs) << messaget::eom;
228+
#endif
229+
// TODO: create the assignment of __CPROVER_shadow_memory_get_field
230+
symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
231+
}
232+
else
233+
{
234+
// We don't have any condition ==> value for the pointer, so we fall-back to
235+
// the initialization value of the shadow-memory.
236+
log.warning() << "Shadow memory: cannot get_field for " << format(expr)
237+
<< messaget::eom;
238+
symex_assign(
239+
state,
240+
lhs,
241+
typecast_exprt::conditional_cast(field_init_expr, lhs.type()));
242+
}
104243
}
105244

106245
// TODO: the following 4 functions (`symex_field_static_init`,

0 commit comments

Comments
 (0)