Skip to content

Commit 6489696

Browse files
Implement shadow_memoryt::gather_field_declarations
Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model and stores them in a shadow_memory_field_definitionst.
1 parent c8f307e commit 6489696

File tree

2 files changed

+83
-9
lines changed

2 files changed

+83
-9
lines changed

src/goto-symex/shadow_memory.cpp

Lines changed: 76 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,14 @@ Author: Peter Schrammel
1111

1212
#include "shadow_memory.h"
1313

14+
#include <util/bitvector_types.h>
15+
#include <util/format_type.h>
1416
#include <util/fresh_symbol.h>
1517

1618
#include <langapi/language_util.h>
1719

1820
#include "goto_symex_state.h"
21+
#include "shadow_memory_util.h"
1922

2023
void shadow_memoryt::initialize_shadow_memory(
2124
goto_symex_statet &state,
@@ -93,17 +96,84 @@ void shadow_memoryt::symex_field_dynamic_init(
9396
}
9497

9598
shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations(
96-
abstract_goto_modelt &goto_model,
99+
const abstract_goto_modelt &goto_model,
97100
message_handlert &message_handler)
98101
{
99-
// To be implemented
100-
101-
return shadow_memory_field_definitionst();
102+
shadow_memory_field_definitionst field_definitions;
103+
104+
// Gather shadow memory declarations from goto model
105+
for(const auto &goto_function : goto_model.get_goto_functions().function_map)
106+
{
107+
const auto &goto_program = goto_function.second.body;
108+
forall_goto_program_instructions(target, goto_program)
109+
{
110+
if(!target->is_function_call())
111+
continue;
112+
113+
const auto &code_function_call =
114+
to_code_function_call(target->get_code());
115+
const exprt &function = code_function_call.function();
116+
117+
if(function.id() != ID_symbol)
118+
continue;
119+
120+
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
121+
122+
if(
123+
identifier ==
124+
CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_GLOBAL_SCOPE)
125+
{
126+
convert_field_declaration(
127+
code_function_call,
128+
field_definitions.global_fields,
129+
true,
130+
message_handler);
131+
}
132+
else if(
133+
identifier ==
134+
CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_LOCAL_SCOPE)
135+
{
136+
convert_field_declaration(
137+
code_function_call,
138+
field_definitions.local_fields,
139+
false,
140+
message_handler);
141+
}
142+
}
143+
}
144+
return field_definitions;
102145
}
103146

104147
void shadow_memoryt::convert_field_declaration(
105148
const code_function_callt &code_function_call,
106-
shadow_memory_field_definitionst::field_definitiont &fields)
149+
shadow_memory_field_definitionst::field_definitiont &fields,
150+
bool is_global,
151+
message_handlert &message_handler)
107152
{
108-
// To be implemented
153+
INVARIANT(
154+
code_function_call.arguments().size() == 2,
155+
std::string(CPROVER_PREFIX) + SHADOW_MEMORY_FIELD_DECL +
156+
(is_global ? SHADOW_MEMORY_GLOBAL_SCOPE : SHADOW_MEMORY_LOCAL_SCOPE) +
157+
" requires 2 arguments");
158+
irep_idt field_name = extract_field_name(code_function_call.arguments()[0]);
159+
160+
exprt expr = code_function_call.arguments()[1];
161+
162+
messaget log(message_handler);
163+
log.debug() << "Shadow memory: declare " << (is_global ? "global " : "local ")
164+
<< "field " << id2string(field_name) << " of type "
165+
<< format(expr.type()) << messaget::eom;
166+
if(!can_cast_type<bitvector_typet>(expr.type()))
167+
{
168+
throw unsupported_operation_exceptiont(
169+
"A shadow memory field must be of a bitvector type.");
170+
}
171+
if(to_bitvector_type(expr.type()).get_width() > 8)
172+
{
173+
throw unsupported_operation_exceptiont(
174+
"A shadow memory field must not be larger than 8 bits.");
175+
}
176+
177+
// record field type
178+
fields[field_name] = expr;
109179
}

src/goto-symex/shadow_memory.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ class shadow_memoryt
5050
/// \param message_handler For logging
5151
/// \return The field definitions
5252
static shadow_memory_field_definitionst gather_field_declarations(
53-
abstract_goto_modelt &goto_model,
53+
const abstract_goto_modelt &goto_model,
5454
message_handlert &message_handler);
5555

5656
/// Initialize global-scope shadow memory for global/static variables.
@@ -100,9 +100,13 @@ class shadow_memoryt
100100
/// Converts a field declaration
101101
/// \param code_function_call The __CPROVER_field_decl_* call
102102
/// \param fields The field declaration to be extended
103-
void convert_field_declaration(
103+
/// \param is_global True if the declaration is global
104+
/// \param message_handler For logging
105+
static void convert_field_declaration(
104106
const code_function_callt &code_function_call,
105-
shadow_memory_field_definitionst::field_definitiont &fields);
107+
shadow_memory_field_definitionst::field_definitiont &fields,
108+
bool is_global,
109+
message_handlert &message_handler);
106110

107111
/// Allocates and initializes a shadow memory field for the given original
108112
/// memory.

0 commit comments

Comments
 (0)