diff --git a/regression/cbmc-shadow-memory/declarations1/bad1.c b/regression/cbmc-shadow-memory/declarations1/bad1.c new file mode 100644 index 00000000000..0c378872701 --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/bad1.c @@ -0,0 +1,4 @@ +void bad_declaration1() +{ + __CPROVER_field_decl_local("field1", (int)0); +} diff --git a/regression/cbmc-shadow-memory/declarations1/bad2.c b/regression/cbmc-shadow-memory/declarations1/bad2.c new file mode 100644 index 00000000000..44a5ae88c2c --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/bad2.c @@ -0,0 +1,8 @@ +void bad_declaration2() +{ + struct STRUCT + { + char x; + } s; + __CPROVER_field_decl_global("field2", s); +} diff --git a/regression/cbmc-shadow-memory/declarations1/good.c b/regression/cbmc-shadow-memory/declarations1/good.c new file mode 100644 index 00000000000..54a9962f912 --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/good.c @@ -0,0 +1,5 @@ +void good_declarations() +{ + __CPROVER_field_decl_local("field1", (_Bool)0); + __CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])0); +} diff --git a/regression/cbmc-shadow-memory/declarations1/test_bad1.desc b/regression/cbmc-shadow-memory/declarations1/test_bad1.desc new file mode 100644 index 00000000000..8b7e975de28 --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/test_bad1.desc @@ -0,0 +1,9 @@ +CORE +bad1.c +--function bad_declaration1 --verbosity 10 +^EXIT=6$ +^SIGNAL=0$ +^A shadow memory field must not be larger than 8 bits. +-- +-- +Test that a shadow memory declaration of a too large type is rejected. diff --git a/regression/cbmc-shadow-memory/declarations1/test_bad2.desc b/regression/cbmc-shadow-memory/declarations1/test_bad2.desc new file mode 100644 index 00000000000..c818280e3d3 --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/test_bad2.desc @@ -0,0 +1,9 @@ +CORE +bad2.c +--function bad_declaration2 --verbosity 10 +^EXIT=6$ +^SIGNAL=0$ +^A shadow memory field must be of a bitvector type. +-- +-- +Test that a shadow memory declaration of a non-bitvector type is rejected. diff --git a/regression/cbmc-shadow-memory/declarations1/test_good.desc b/regression/cbmc-shadow-memory/declarations1/test_good.desc new file mode 100644 index 00000000000..80e5c804d58 --- /dev/null +++ b/regression/cbmc-shadow-memory/declarations1/test_good.desc @@ -0,0 +1,12 @@ +CORE +good.c +--function good_declarations --verbosity 10 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +^Shadow memory: declare local field field1 of type c_bool\[8\] +^Shadow memory: declare global field field2 of type unsignedbv\[6\] +-- +^A shadow memory field must +-- +Test that shadow memory declarations are correctly gathered. diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 6ed31edb772..c1d8e5b04ce 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -15,6 +15,7 @@ SRC = auto_objects.cpp \ precondition.cpp \ renaming_level.cpp \ shadow_memory.cpp \ + shadow_memory_util.cpp \ show_program.cpp \ show_vcc.cpp \ slice.cpp \ diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index ef39c5d749a..25f1dc55b44 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -11,11 +11,14 @@ Author: Peter Schrammel #include "shadow_memory.h" +#include +#include #include #include #include "goto_symex_state.h" +#include "shadow_memory_util.h" void shadow_memoryt::initialize_shadow_memory( goto_symex_statet &state, @@ -95,17 +98,83 @@ void shadow_memoryt::symex_field_dynamic_init( } shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations( - abstract_goto_modelt &goto_model, + const abstract_goto_modelt &goto_model, message_handlert &message_handler) { - // To be implemented - - return shadow_memory_field_definitionst(); + shadow_memory_field_definitionst field_definitions; + + // Gather shadow memory declarations from goto model + for(const auto &goto_function : goto_model.get_goto_functions().function_map) + { + const auto &goto_program = goto_function.second.body; + forall_goto_program_instructions(target, goto_program) + { + if(!target->is_function_call()) + continue; + + const auto &code_function_call = to_code_function_call(target->code()); + const exprt &function = code_function_call.function(); + + if(function.id() != ID_symbol) + continue; + + const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + + if( + identifier == + CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_GLOBAL_SCOPE) + { + convert_field_declaration( + code_function_call, + field_definitions.global_fields, + true, + message_handler); + } + else if( + identifier == + CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_LOCAL_SCOPE) + { + convert_field_declaration( + code_function_call, + field_definitions.local_fields, + false, + message_handler); + } + } + } + return field_definitions; } void shadow_memoryt::convert_field_declaration( const code_function_callt &code_function_call, - shadow_memory_field_definitionst::field_definitiont &fields) + shadow_memory_field_definitionst::field_definitiont &fields, + bool is_global, + message_handlert &message_handler) { - // To be implemented + INVARIANT( + code_function_call.arguments().size() == 2, + std::string(CPROVER_PREFIX) + SHADOW_MEMORY_FIELD_DECL + + (is_global ? SHADOW_MEMORY_GLOBAL_SCOPE : SHADOW_MEMORY_LOCAL_SCOPE) + + " requires 2 arguments"); + irep_idt field_name = extract_field_name(code_function_call.arguments()[0]); + + exprt expr = code_function_call.arguments()[1]; + + messaget log(message_handler); + log.debug() << "Shadow memory: declare " << (is_global ? "global " : "local ") + << "field " << id2string(field_name) << " of type " + << format(expr.type()) << messaget::eom; + if(!can_cast_type(expr.type())) + { + throw unsupported_operation_exceptiont( + "A shadow memory field must be of a bitvector type."); + } + if(to_bitvector_type(expr.type()).get_width() > 8) + { + throw unsupported_operation_exceptiont( + "A shadow memory field must not be larger than 8 bits."); + } + + // record the field's initial value (and type) + fields[field_name] = expr; } diff --git a/src/goto-symex/shadow_memory.h b/src/goto-symex/shadow_memory.h index 6f42d9f6a25..f1bdef302ef 100644 --- a/src/goto-symex/shadow_memory.h +++ b/src/goto-symex/shadow_memory.h @@ -50,7 +50,7 @@ class shadow_memoryt /// \param message_handler For logging /// \return The field definitions static shadow_memory_field_definitionst gather_field_declarations( - abstract_goto_modelt &goto_model, + const abstract_goto_modelt &goto_model, message_handlert &message_handler); /// Initialize global-scope shadow memory for global/static variables. @@ -100,9 +100,13 @@ class shadow_memoryt /// Converts a field declaration /// \param code_function_call The __CPROVER_field_decl_* call /// \param fields The field declaration to be extended - void convert_field_declaration( + /// \param is_global True if the declaration is global + /// \param message_handler For logging + static void convert_field_declaration( const code_function_callt &code_function_call, - shadow_memory_field_definitionst::field_definitiont &fields); + shadow_memory_field_definitionst::field_definitiont &fields, + bool is_global, + message_handlert &message_handler); /// Allocates and initializes a shadow memory field for the given original /// memory. diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp new file mode 100644 index 00000000000..89d8bfeefaf --- /dev/null +++ b/src/goto-symex/shadow_memory_util.cpp @@ -0,0 +1,32 @@ +/*******************************************************************\ + +Module: Symex Shadow Memory Instrumentation + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Symex Shadow Memory Instrumentation Utilities + +#include "shadow_memory_util.h" + +#include +#include +#include + +irep_idt extract_field_name(const exprt &string_expr) +{ + if(string_expr.id() == ID_typecast) + return extract_field_name(to_typecast_expr(string_expr).op()); + else if(string_expr.id() == ID_address_of) + return extract_field_name(to_address_of_expr(string_expr).object()); + else if(string_expr.id() == ID_index) + return extract_field_name(to_index_expr(string_expr).array()); + else if(string_expr.id() == ID_string_constant) + { + return string_expr.get(ID_value); + } + else + UNREACHABLE; +} diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h new file mode 100644 index 00000000000..1b62bf5f5a6 --- /dev/null +++ b/src/goto-symex/shadow_memory_util.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Symex Shadow Memory Instrumentation + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Symex Shadow Memory Instrumentation Utilities + +#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H +#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H + +#include + +class exprt; + +/// Extracts the field name identifier from a string expression, +/// e.g. as passed as argument to a __CPROVER_field_decl_local call. +/// \param string_expr The string argument expression +/// \return The identifier denoted by the string argument expression +irep_idt extract_field_name(const exprt &string_expr); + +#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H