diff --git a/regression/snapshot-harness/nondet_initialize_static_arrays/main.c b/regression/snapshot-harness/nondet_initialize_static_arrays/main.c new file mode 100644 index 00000000000..79a8cf545db --- /dev/null +++ b/regression/snapshot-harness/nondet_initialize_static_arrays/main.c @@ -0,0 +1,51 @@ +#include +#include + +typedef struct st1 +{ + struct st2 *to_st2; + int data; +} st1_t; + +typedef struct st2 +{ + struct st1 *to_st1; + int data; +} st2_t; + +typedef struct st3 +{ + st1_t *array[3]; +} st3_t; + +st3_t *p; + +void initialize() +{ + p = malloc(sizeof(st3_t)); +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p != NULL); + for(int index = 0; index < 3; index++) + { + // check that the arrays in structs (and structs in those arrays) were + // initialized up-to the input depth + assert(p->array[index]->to_st2 != NULL); + assert(p->array[index]->to_st2->to_st1 != NULL); + assert(p->array[index]->to_st2->to_st1->to_st2 == NULL); + } + + // non-deterministically initializated objects should not be equal + assert(p->array[0] != p->array[1]); + assert(p->array[1] != p->array[2]); + assert(p->array[0] != p->array[2]); +} diff --git a/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc b/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc new file mode 100644 index 00000000000..5176c9aed07 --- /dev/null +++ b/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/main.c b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/main.c new file mode 100644 index 00000000000..dab0e9c0c73 --- /dev/null +++ b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/main.c @@ -0,0 +1,42 @@ +#include +#include + +typedef struct st1 +{ + struct st2 *to_st2; + int data; +} st1_t; + +typedef struct st2 +{ + struct st1 *to_st1; + int data; +} st2_t; + +st1_t dummy1; +st2_t dummy2; + +st1_t *p; + +void initialize() +{ +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p != NULL); + assert(p->to_st2 != NULL); + assert(p->to_st2->to_st1 != NULL); + assert(p->to_st2->to_st1->to_st2 == NULL); + + assert(p != &dummy1); + assert(p->to_st2 != &dummy2); + assert(p->to_st2->to_st1 != &dummy1); +} diff --git a/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc new file mode 100644 index 00000000000..dca0b623d91 --- /dev/null +++ b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3 +^SIGNAL=0$ +^EXIT=0$ +VERIFICATION SUCCESSFUL +-- +unwinding assertion loop \d+: FAILURE diff --git a/regression/snapshot-harness/pointer-to-array-char/main.c b/regression/snapshot-harness/pointer-to-array-char/main.c new file mode 100644 index 00000000000..3497b5de74c --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-char/main.c @@ -0,0 +1,28 @@ +#include +#include + +char *first; +char *second; +int array_size; + +void initialize() +{ + first = malloc(sizeof(char) * 12); + first = "1234567890a"; + second = first; + array_size = 11; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(first == second); + assert(second[array_size - 1] == 'a'); + return 0; +} diff --git a/regression/snapshot-harness/pointer-to-array-char/test.desc b/regression/snapshot-harness/pointer-to-array-char/test.desc new file mode 100644 index 00000000000..05e08784a54 --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-char/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^SIGNAL=0$ +^EXIT=0$ +VERIFICATION SUCCESSFUL +-- +unwinding assertion loop \d+: FAILURE diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/main.c b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/main.c new file mode 100644 index 00000000000..c765ca154f0 --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/main.c @@ -0,0 +1,41 @@ +#include + +char *first = "12345678901"; +char *second; +int string_size; +const char *prefix; +int prefix_size; + +void initialize() +{ + second = first; + string_size = 11; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(first == second); + if(prefix_size > 0) + assert(second[prefix_size - 1] != 'a'); + + if(string_size < prefix_size) + { + return 0; + } + + for(int ix = 0; ix < prefix_size; ++ix) + { + if(second[ix] != prefix[ix]) + { + return 0; + } + } + return 1; +} diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc new file mode 100644 index 00000000000..be2aa201473 --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5 +^SIGNAL=0$ +^EXIT=0$ +VERIFICATION SUCCESSFUL +-- +unwinding assertion loop \d+: FAILURE diff --git a/regression/snapshot-harness/pointer-to-array-int/main.c b/regression/snapshot-harness/pointer-to-array-int/main.c new file mode 100644 index 00000000000..622f6f61c9a --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-int/main.c @@ -0,0 +1,44 @@ +#include +#include + +int *first; +int *second; +int *third; +int array_size; +const int *prefix; +int prefix_size; + +void initialize() +{ + first = (int *)malloc(sizeof(int) * 5); + first[0] = 0; + first[1] = 1; + first[2] = 2; + first[3] = 3; + first[4] = 4; + second = first; + array_size = 5; + third = &array_size; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(first == second); + // The following assertions will be check in the following PR once + // dynamically allocated snapshots are properly implemented. + /* assert(array_size >= prefix_size); */ + /* assert(prefix_size >= 0); */ + /* assert(second[prefix_size] != 6); */ + /* assert(second[4] == 4); */ + + /* for(int i = 0; i < prefix_size; i++) */ + /* assert(second[i] != prefix[i]); */ + return 0; +} diff --git a/regression/snapshot-harness/pointer-to-array-int/test.desc b/regression/snapshot-harness/pointer-to-array-int/test.desc new file mode 100644 index 00000000000..2d8e1689498 --- /dev/null +++ b/regression/snapshot-harness/pointer-to-array-int/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4 +^SIGNAL=0$ +^EXIT=0$ +VERIFICATION SUCCESSFUL +-- +unwinding assertion loop \d+: FAILURE diff --git a/regression/snapshot-harness/pointer_07/main.c b/regression/snapshot-harness/pointer_07/main.c new file mode 100644 index 00000000000..ef9e181e6d0 --- /dev/null +++ b/regression/snapshot-harness/pointer_07/main.c @@ -0,0 +1,26 @@ +#include +#include + +int *p1; + +void initialize() +{ + p1 = malloc(sizeof(int)); + *p1 = 1; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p1[0] == 1); + assert(*p1 == 1); + p1[0] = 2; + assert(*p1 == 1); + assert(*p1 != 1); +} diff --git a/regression/snapshot-harness/pointer_07/test.desc b/regression/snapshot-harness/pointer_07/test.desc new file mode 100644 index 00000000000..9976dccae64 --- /dev/null +++ b/regression/snapshot-harness/pointer_07/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p1\[0\] == 1: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \*p1 == 1: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p1 == 1: FAILURE +\[main.assertion.4\] line [0-9]+ assertion \*p1 != 1: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/static-array-char/main.c b/regression/snapshot-harness/static-array-char/main.c new file mode 100644 index 00000000000..958baaf60fd --- /dev/null +++ b/regression/snapshot-harness/static-array-char/main.c @@ -0,0 +1,32 @@ +#include + +char tmp[12]; +char *first; +char *second; +int array_size; + +void initialize() +{ + tmp[0] = '1'; + tmp[9] = '0'; + tmp[10] = 'a'; + first = (char *)tmp; + second = first; + array_size = 11; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(first == second); + assert(second[array_size - 1] == 'a'); + assert(first[0] == '1'); + assert(second[9] == '0'); + return 0; +} diff --git a/regression/snapshot-harness/static-array-char/test.desc b/regression/snapshot-harness/static-array-char/test.desc new file mode 100644 index 00000000000..69d4e8c5bfd --- /dev/null +++ b/regression/snapshot-harness/static-array-char/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^SIGNAL=0$ +^EXIT=0$ +VERIFICATION SUCCESSFUL +-- +unwinding assertion loop \d+: FAILURE diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h new file mode 100644 index 00000000000..844309f59b3 --- /dev/null +++ b/src/goto-harness/common_harness_generator_options.h @@ -0,0 +1,46 @@ +/******************************************************************\ + +Module: common_harness_generator_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#ifndef CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H +#define CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H + +#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth" +#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + "max-nondet-tree-depth" +#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size" +#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size" + +// clang-format off +#define COMMON_HARNESS_GENERATOR_OPTIONS \ + "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ +// COMMON_HARNESS_GENERATOR_OPTIONS + +// clang-format on + +// clang-format off +#define COMMON_HARNESS_GENERATOR_HELP \ + "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ + " N minimum level at which a pointer can first be NULL\n" \ + " in a recursively nondet initialized struct\n" \ + "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ + " N limit size of nondet (e.g. input) object tree;\n" \ + " at level N pointers are set to null\n" \ + "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \ + " N minimum size of dynamically created arrays\n" \ + " (default: 1)\n" \ + "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ + " N maximum size of dynamically created arrays\n" \ + " (default: 2)\n" \ + // COMMON_HARNESS_GENERATOR_HELP + +// clang-format on + +#endif // CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index f36766be7e2..65233cca013 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -90,7 +90,14 @@ void function_call_harness_generatort::handle_option( const std::string &option, const std::list &values) { - if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT) + auto &require_exactly_one_value = + harness_options_parser::require_exactly_one_value; + + if(p_impl->recursive_initialization_config.handle_option(option, values)) + { + // the option belongs to recursive initialization + } + else if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT) { p_impl->function = require_exactly_one_value(option, values); } @@ -98,50 +105,6 @@ void function_call_harness_generatort::handle_option( { p_impl->nondet_globals = true; } - else if(option == FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT) - { - auto const value = require_exactly_one_value(option, values); - auto const min_null_tree_depth = string2optional(value, 10); - if(min_null_tree_depth.has_value()) - { - p_impl->recursive_initialization_config.min_null_tree_depth = - min_null_tree_depth.value(); - } - else - { - throw invalid_command_line_argument_exceptiont{ - "failed to convert `" + value + "' to integer", - "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT}; - } - } - else if(option == FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT) - { - auto const value = require_exactly_one_value(option, values); - auto const max_nondet_tree_depth = string2optional(value, 10); - if(max_nondet_tree_depth.has_value()) - { - p_impl->recursive_initialization_config.max_nondet_tree_depth = - max_nondet_tree_depth.value(); - } - else - { - throw invalid_command_line_argument_exceptiont{ - "failed to convert `" + value + "' to integer", - "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT}; - } - } - else if(option == FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT) - { - p_impl->recursive_initialization_config.max_dynamic_array_size = - require_one_size_value( - FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values); - } - else if(option == FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT) - { - p_impl->recursive_initialization_config.min_dynamic_array_size = - require_one_size_value( - FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values); - } else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT) { p_impl->function_parameters_to_treat_as_arrays.insert( @@ -285,25 +248,8 @@ void function_call_harness_generatort::validate_options( { throw invalid_command_line_argument_exceptiont{ "min dynamic array size cannot be greater than max dynamic array size", - "--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT - " --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT}; - } -} - -std::size_t function_call_harness_generatort::require_one_size_value( - const std::string &option, - const std::list &values) -{ - auto const string_value = require_exactly_one_value(option, values); - auto value = string2optional(string_value, 10); - if(value.has_value()) - { - return value.value(); - } - else - { - throw invalid_command_line_argument_exceptiont{ - "failed to parse `" + string_value + "' as integer", "--" + option}; + "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT + " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT}; } } diff --git a/src/goto-harness/function_harness_generator_options.h b/src/goto-harness/function_harness_generator_options.h index 245902efed6..83cf1bcabac 100644 --- a/src/goto-harness/function_harness_generator_options.h +++ b/src/goto-harness/function_harness_generator_options.h @@ -9,13 +9,10 @@ Author: Diffblue Ltd. #ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H #define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H +#include "common_harness_generator_options.h" + #define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function" #define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals" -#define FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth" -#define FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ - "max-nondet-tree-depth" -#define FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size" -#define FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size" #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ "treat-pointer-as-array" #define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ @@ -27,10 +24,6 @@ Author: Diffblue Ltd. #define FUNCTION_HARNESS_GENERATOR_OPTIONS \ "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \ - "(" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ - "(" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \ "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):" \ @@ -42,29 +35,24 @@ Author: Diffblue Ltd. #define FUNCTION_HARNESS_GENERATOR_HELP \ "function harness generator (--harness-type call-function)\n\n" \ "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \ - " the function the harness should call\n" \ + " the function the harness should call\n" \ "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \ - " set global variables to non-deterministic values in harness\n" \ - "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \ - " N minimum level at which a pointer can first be\n" \ - " NULL in a recursively nondet initialized struct\n" \ - "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \ - " N limit size of nondet (e.g. input) object tree;\n" \ - " at level N pointers are set to null\n" \ - "--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \ - " N minimum size of dynamically created arrays (default: 1)\n" \ - "--" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ - " N maximum size of dynamically created arrays (default: 2)\n" \ + " set global variables to non-deterministic values\n" \ + " in harness\n" \ + COMMON_HARNESS_GENERATOR_HELP \ "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ - " parameter treat the function parameter with the name `parameter'\n" \ - " as an array\n" \ + " p treat the function parameter with the name `p' as\n" \ + " an array\n" \ "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ " array_name:size_name\n" \ - " set the parameter to the size\n"\ - " of the array \n" \ - " (implies " \ - "-- " FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \ + " set the parameter to the size" \ + " of\n the array \n" \ + " (implies " \ + "-- " FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \ " )\n" \ + "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \ + " p treat the function parameter with the name `p' as\n" \ + " a string of characters\n" \ // FUNCTION_HARNESS_GENERATOR_HELP // clang-format on diff --git a/src/goto-harness/goto_harness_generator.cpp b/src/goto-harness/goto_harness_generator.cpp index f045d9dd047..45917e4db70 100644 --- a/src/goto-harness/goto_harness_generator.cpp +++ b/src/goto-harness/goto_harness_generator.cpp @@ -13,8 +13,12 @@ Author: Diffblue Ltd. #include #include +#include -std::string goto_harness_generatort::require_exactly_one_value( +// NOLINTNEXTLINE(readability/namespace) +namespace harness_options_parser +{ +std::string require_exactly_one_value( const std::string &option, const std::list &values) { @@ -27,9 +31,28 @@ std::string goto_harness_generatort::require_exactly_one_value( return values.front(); } -void goto_harness_generatort::assert_no_values( +void assert_no_values( const std::string &option, const std::list &values) { PRECONDITION_WITH_DIAGNOSTICS(values.empty(), option); } + +std::size_t require_one_size_value( + const std::string &option, + const std::list &values) +{ + auto const string_value = require_exactly_one_value(option, values); + auto value = string2optional(string_value, 10); + if(value.has_value()) + { + return value.value(); + } + else + { + throw invalid_command_line_argument_exceptiont{ + "failed to parse `" + string_value + "' as integer", "--" + option}; + } +} +// NOLINTNEXTLINE(readability/namespace) +} // namespace harness_options_parser diff --git a/src/goto-harness/goto_harness_generator.h b/src/goto-harness/goto_harness_generator.h index ada7bae4fd3..95bbfc2252e 100644 --- a/src/goto-harness/goto_harness_generator.h +++ b/src/goto-harness/goto_harness_generator.h @@ -16,6 +16,28 @@ Author: Diffblue Ltd. class goto_modelt; +// NOLINTNEXTLINE(readability/namespace) +namespace harness_options_parser +{ +/// Returns the only value of a single element list, +/// throws an exception if not passed a single element list +std::string require_exactly_one_value( + const std::string &option, + const std::list &values); + +/// Asserts that the list of values to an option passed is empty +void assert_no_values( + const std::string &option, + const std::list &values); + +/// Returns the only Nat value of a single element list, +/// throws an exception if not passed a single element list (or not Nat) +std::size_t require_one_size_value( + const std::string &option, + const std::list &values); +// NOLINTNEXTLINE(readability/namespace) +} // namespace harness_options_parser + class goto_harness_generatort { public: @@ -36,17 +58,6 @@ class goto_harness_generatort /// Check if options are in a sane state, throw otherwise virtual void validate_options(const goto_modelt &goto_model) = 0; - - /// Returns the only value of a single element list, - /// throws an exception if not passed a single element list - static std::string require_exactly_one_value( - const std::string &option, - const std::list &values); - - /// Asserts that the list of values to an option passed is empty - static void assert_no_values( - const std::string &option, - const std::list &values); }; #endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h index edcf045bff8..60b1c155283 100644 --- a/src/goto-harness/goto_harness_parse_options.h +++ b/src/goto-harness/goto_harness_parse_options.h @@ -17,11 +17,13 @@ Author: Diffblue Ltd. #include "function_harness_generator_options.h" #include "goto_harness_generator_factory.h" +#include "memory_snapshot_harness_generator_options.h" // clang-format off #define GOTO_HARNESS_OPTIONS \ "(version)" \ GOTO_HARNESS_FACTORY_OPTIONS \ + COMMON_HARNESS_GENERATOR_OPTIONS \ FUNCTION_HARNESS_GENERATOR_OPTIONS \ MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ // end GOTO_HARNESS_OPTIONS diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index 324a3b69bcb..0d59add0caa 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -9,6 +9,7 @@ Author: Daniel Poetzl #include #include "memory_snapshot_harness_generator.h" +#include "memory_snapshot_harness_generator_options.h" #include @@ -26,25 +27,75 @@ Author: Daniel Poetzl #include #include "goto_harness_generator_factory.h" -#include "recursive_initialization.h" void memory_snapshot_harness_generatort::handle_option( const std::string &option, const std::list &values) { - if(option == "memory-snapshot") + auto &require_exactly_one_value = + harness_options_parser::require_exactly_one_value; + if(recursive_initialization_config.handle_option(option, values)) + { + // the option belongs to recursive initialization + } + else if(option == MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT) + { + recursive_initialization_config.pointers_to_treat_as_arrays.insert( + values.begin(), values.end()); + } + else if(option == MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT) + { + for(auto const &array_size_pair : values) + { + try + { + std::string array; + std::string size; + split_string(array_size_pair, ':', array, size); + // --associated-array-size implies --treat-pointer-as-array + // but it is not an error to specify both, so we don't check + // for duplicates here + recursive_initialization_config.pointers_to_treat_as_arrays.insert( + array); + auto const inserted = + recursive_initialization_config + .array_name_to_associated_array_size_variable.emplace(array, size); + if(!inserted.second) + { + throw invalid_command_line_argument_exceptiont{ + "can not have two associated array sizes for one array", + "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT}; + } + } + catch(const deserialization_exceptiont &) + { + throw invalid_command_line_argument_exceptiont{ + "`" + array_size_pair + + "' is in an invalid format for array size pair", + "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT, + "array_name:size_name, where both are the names of global " + "variables"}; + } + } + } + else if(option == MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT) { memory_snapshot_file = require_exactly_one_value(option, values); } - else if(option == "initial-goto-location") + else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT) { initial_goto_location_line = require_exactly_one_value(option, values); } - else if(option == "havoc-variables") + else if(option == MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT) { - variables_to_havoc.insert(values.begin(), values.end()); + std::vector havoc_candidates; + split_string(values.front(), ',', havoc_candidates, true); + for(const auto &candidate : havoc_candidates) + { + variables_to_havoc.insert(candidate); + } } - else if(option == "initial-source-location") + else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT) { initial_source_location_line = require_exactly_one_value(option, values); } @@ -148,15 +199,43 @@ const symbolt &memory_snapshot_harness_generatort::fresh_symbol_copy( return tmp_symbol; } +size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const +{ + if(t.id() != ID_pointer) + return 0; + else + return pointer_depth(t.subtype()) + 1; +} + code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( const symbol_tablet &snapshot, goto_modelt &goto_model) const { recursive_initializationt recursive_initialization{ - recursive_initialization_configt{}, goto_model}; + recursive_initialization_config, goto_model}; + + using snapshot_pairt = std::pair; + std::vector ordered_snapshot_symbols; + for(auto pair : snapshot) + { + const auto name = id2string(pair.first); + if(name.find(CPROVER_PREFIX) != 0) + ordered_snapshot_symbols.push_back(pair); + } + + // sort the snapshot symbols so that the non-pointer symbols are first, then + // pointers, then pointers-to-pointers, etc. so that we don't assign + // uninitialized values + std::stable_sort( + ordered_snapshot_symbols.begin(), + ordered_snapshot_symbols.end(), + [this](const snapshot_pairt &left, const snapshot_pairt &right) { + return pointer_depth(left.second.symbol_expr().type()) < + pointer_depth(right.second.symbol_expr().type()); + }); code_blockt code; - for(const auto &pair : snapshot) + for(const auto &pair : ordered_snapshot_symbols) { const symbolt &snapshot_symbol = pair.second; symbol_tablet &symbol_table = goto_model.symbol_table; diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 1a62d3ec15d..1b6a98a1196 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -13,35 +13,13 @@ Author: Daniel Poetzl #include #include "goto_harness_generator.h" +#include "recursive_initialization.h" #include #include #include -// clang-format off -#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ - "(memory-snapshot):" \ - "(initial-goto-location):" \ - "(initial-source-location):" \ - "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS -// clang-format on - -// clang-format off -#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ - "memory snapshot harness generator (--harness-type\n" \ - " initialise-from-memory-snapshot)\n\n" \ - "--memory-snapshot initialise memory from JSON memory snapshot\n"\ - "--initial-goto-location ]>\n" \ - " use given function and location number as " \ - "entry\n point\n" \ - "--initial-source-location \n" \ - " use given file and line as entry point\n" \ - "--havoc-variables vars initialise variables from vars to\n" \ - " non-deterministic values" \ - // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP -// clang-format on - /// Generates a harness which first assigns global variables with values from /// a given memory snapshot and then calls a specified function. The called /// function is also modified such that it appears to start executing at the @@ -261,6 +239,11 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort goto_modelt &goto_model, const symbolt &function) const; + /// Recursively compute the pointer depth + /// \param t: input type + /// \return pointer depth of type \p t + size_t pointer_depth(const typet &t) const; + /// data to store the command-line options std::string memory_snapshot_file; std::string initial_goto_location_line; @@ -271,6 +254,8 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort entry_locationt entry_location; message_handlert &message_handler; + + recursive_initialization_configt recursive_initialization_config; }; #endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/src/goto-harness/memory_snapshot_harness_generator_options.h new file mode 100644 index 00000000000..14a32946fb7 --- /dev/null +++ b/src/goto-harness/memory_snapshot_harness_generator_options.h @@ -0,0 +1,63 @@ +/******************************************************************\ + +Module: memory_snapshot_harness_generator_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H +#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H + +#include "common_harness_generator_options.h" + +#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "memory-snapshot" +#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "initial-goto-location" +#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "initial-source-location" +#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "havoc-variables" +#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "pointer-as-array" +#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "size-of-array" + +// clang-format off +#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ + "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "):" \ + "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):" \ +// MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS + +// clang-format on + +// clang-format off +#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ + "memory snapshot harness generator (--harness-type\n" \ + " initialise-from-memory-snapshot)\n\n" \ + "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " initialise memory " \ + "from JSON memory snapshot\n" \ + "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " ]>\n" \ + " use given function and location number as " \ + "entry\n point\n" \ + "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT " >\n" \ + " use given file name and line number as " \ + "entry\n point\n" \ + "--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT " vars initialise" \ + " variables from `vars' to\n" \ + " non-deterministic values\n" \ + COMMON_HARNESS_GENERATOR_HELP \ + "--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + " p treat the global pointer with the name `p' as\n" \ + " an array\n" \ + "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT \ + " array_name:size_name\n" \ + " set the parameter to the size" \ + " of\n the array \n" \ + " (implies " \ + "-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \ + " )\n" \ +// MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP + +// clang-format on + +#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 92c0e4d11ea..1ba172a51b0 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -16,9 +16,65 @@ Author: Diffblue Ltd. #include #include #include +#include #include +bool recursive_initialization_configt::handle_option( + const std::string &option, + const std::list &values) +{ + if(option == COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT) + { + auto const value = + harness_options_parser::require_exactly_one_value(option, values); + auto const user_min_null_tree_depth = + string2optional(value, 10); + if(user_min_null_tree_depth.has_value()) + { + min_null_tree_depth = user_min_null_tree_depth.value(); + } + else + { + throw invalid_command_line_argument_exceptiont{ + "failed to convert `" + value + "' to integer", + "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT}; + } + return true; + } + else if(option == COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT) + { + auto const value = + harness_options_parser::require_exactly_one_value(option, values); + auto const user_max_nondet_tree_depth = + string2optional(value, 10); + if(user_max_nondet_tree_depth.has_value()) + { + max_nondet_tree_depth = user_max_nondet_tree_depth.value(); + } + else + { + throw invalid_command_line_argument_exceptiont{ + "failed to convert `" + value + "' to integer", + "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT}; + } + return true; + } + else if(option == COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT) + { + max_dynamic_array_size = harness_options_parser::require_one_size_value( + COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values); + return true; + } + else if(option == COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT) + { + min_dynamic_array_size = harness_options_parser::require_one_size_value( + COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values); + return true; + } + return false; +} + recursive_initializationt::recursive_initializationt( recursive_initialization_configt initialization_config, goto_modelt &goto_model) diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index f17bc9d5218..e6956bc42fe 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -18,6 +18,9 @@ Author: Diffblue Ltd. #include #include +#include "function_harness_generator_options.h" +#include "goto_harness_generator.h" + struct recursive_initialization_configt { std::size_t min_null_tree_depth = 1; @@ -35,6 +38,15 @@ struct recursive_initialization_configt std::set pointers_to_treat_as_cstrings; std::string to_string() const; // for debugging purposes + + /// Parse the options specific for recursive initialisation + /// \param option: the user option name + /// \param values: the (one-or-more) values for this option + /// \return true if the option belonged to recursive initialisation and was + /// successfully parsed here + bool handle_option( + const std::string &option, + const std::list &values); }; /// Class for generating initialisation code diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 7e73e7905f2..0cc6a296265 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -160,10 +160,13 @@ exprt gdb_value_extractort::get_char_pointer_value( values.insert(std::make_pair(memory_location, new_symbol)); + // check that we are returning objects of the right type + CHECK_RETURN(new_symbol.type().subtype() == expr.type().subtype()); return new_symbol; } else { + CHECK_RETURN(it->second.type().subtype() == expr.type().subtype()); return it->second; } } @@ -174,7 +177,6 @@ exprt gdb_value_extractort::get_pointer_to_member_value( const source_locationt &location) { PRECONDITION(expr.type().id() == ID_pointer); - PRECONDITION(!is_c_char_type(expr.type().subtype())); const auto &memory_location = pointer_value.address; std::string memory_location_string = memory_location.string(); PRECONDITION(memory_location_string != "0x0"); @@ -240,9 +242,35 @@ exprt gdb_value_extractort::get_pointer_to_member_value( return *maybe_member_expr; } + const auto it = values.find(memory_location); + // if the structure we are pointing to does not exists we need to build a + // temporary object for it: get the type from symbol table, query gdb for + // value, allocate new object for it and then store into assignments + if(it == values.end()) + { + const auto symbol_expr = struct_symbol->symbol_expr(); + const auto zero = zero_initializer(symbol_expr.type(), location, ns); + CHECK_RETURN(zero.has_value()); + const auto val = get_expr_value(symbol_expr, *zero, location); + + symbol_exprt dummy("tmp", pointer_type(symbol_expr.type())); + code_blockt assignments; + + const symbol_exprt new_symbol = + to_symbol_expr(allocate_objects.allocate_automatic_local_object( + assignments, dummy, symbol_expr.type())); + + add_assignment(new_symbol, val); + values[memory_location] = val; + } + const auto maybe_member_expr = get_subexpression_at_offset( struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns); - CHECK_RETURN(maybe_member_expr.has_value()); + DATA_INVARIANT( + maybe_member_expr.has_value(), "structure doesn't have member"); + + // check that we return the right type + CHECK_RETURN(maybe_member_expr->type() == expr.type().subtype()); return *maybe_member_expr; } @@ -266,18 +294,60 @@ exprt gdb_value_extractort::get_non_char_pointer_value( symbol_exprt dummy("tmp", expr.type()); code_blockt assignments; + const auto zero_expr = zero_initializer(target_type, location, ns); + CHECK_RETURN(zero_expr); + + // Check if pointer was dynamically allocated (via malloc). If so we will + // replace the pointee with a static array filled with values stored at the + // expected positions. Since the allocated size is over-approximation we may + // end up querying pass the allocated bounds and building larger array with + // meaningless values. + size_t allocated_size = + gdb_api.query_malloc_size(c_converter.convert(expr)); + // get the sizeof(target_type) and thus the number of elements + const auto target_size_bits = pointer_offset_bits(target_type, ns); + CHECK_RETURN(target_size_bits.has_value()); + const auto number_of_elements = allocated_size / (*target_size_bits / 8); + if(number_of_elements > 1) + { + array_exprt::operandst elements; + // build the operands by querying for an index expression + for(size_t i = 0; i < number_of_elements; i++) + { + const auto sub_expr_value = get_expr_value( + index_exprt{expr, from_integer(i, index_type())}, + *zero_expr, + location); + elements.push_back(sub_expr_value); + } + CHECK_RETURN(elements.size() == number_of_elements); + + // knowing the number of elements we can build the type + const typet target_array_type = + array_typet{target_type, from_integer(elements.size(), index_type())}; + + array_exprt new_array{elements, to_array_type(target_array_type)}; + + // allocate a new symbol for the temporary static array + symbol_exprt array_dummy("tmp", pointer_type(target_array_type)); + const auto array_symbol = + allocate_objects.allocate_automatic_local_object( + assignments, array_dummy, target_array_type); + + // add assignment of value to newly created symbol + add_assignment(array_symbol, new_array); + values[memory_location] = array_symbol; + return array_symbol; + } + const symbol_exprt new_symbol = to_symbol_expr(allocate_objects.allocate_automatic_local_object( assignments, dummy, target_type)); dereference_exprt dereference_expr(expr); - const auto zero_expr = zero_initializer(target_type, location, ns); - CHECK_RETURN(zero_expr); - const exprt target_expr = get_expr_value(dereference_expr, *zero_expr, location); - // add assignment of value to newly created symbol add_assignment(new_symbol, target_expr); @@ -325,33 +395,58 @@ exprt gdb_value_extractort::get_pointer_value( std::string c_expr = c_converter.convert(expr); const pointer_valuet value = gdb_api.get_memory(c_expr); + if(!value.valid) + return zero_expr; const auto memory_location = value.address; if(!memory_location.is_null()) { - if(is_c_char_type(expr.type().subtype())) + // pointers-to-char can point to members as well, e.g. char[] + if(points_to_member(value)) { - return get_char_pointer_value(expr, memory_location, location); + const auto target_expr = + get_pointer_to_member_value(expr, value, location); + CHECK_RETURN(target_expr.is_not_nil()); + const auto result_expr = address_of_exprt(target_expr); + CHECK_RETURN(result_expr.type() == zero_expr.type()); + return result_expr; } - else + + // non-member: split for char/non-char + const auto target_expr = + is_c_char_type(expr.type().subtype()) + ? get_char_pointer_value(expr, memory_location, location) + : get_non_char_pointer_value(expr, memory_location, location); + + // postpone if we cannot resolve now + if(target_expr.is_nil()) { - const exprt target_expr = - points_to_member(value) - ? get_pointer_to_member_value(expr, value, location) - : get_non_char_pointer_value(expr, memory_location, location); + outstanding_assignments[expr] = memory_location; + return zero_expr; + } - if(target_expr.id() == ID_nil) - { - outstanding_assignments[expr] = memory_location; - } - else - { - const auto result_expr = address_of_exprt(target_expr); - CHECK_RETURN(result_expr.type() == zero_expr.type()); - return result_expr; - } + // the pointee was (probably) dynamically allocated (but the allocation + // would not be visible in the snapshot) so we pretend it is statically + // allocated (we have the value) and return address to the first element + // of the array (instead of the array as char*) + if(target_expr.type().id() == ID_array) + { + const auto result_indexed_expr = get_subexpression_at_offset( + target_expr, 0, zero_expr.type().subtype(), ns); + CHECK_RETURN(result_indexed_expr.has_value()); + const auto result_expr = address_of_exprt{*result_indexed_expr}; + return result_expr; } + + // if the types match return right away + if(target_expr.type() == zero_expr.type()) + return target_expr; + + // otherwise the address of target should type-match + const auto result_expr = address_of_exprt(target_expr); + CHECK_RETURN(result_expr.type() == zero_expr.type()); + return result_expr; } return zero_expr; @@ -395,26 +490,53 @@ exprt gdb_value_extractort::get_expr_value( { INVARIANT(zero_expr.is_constant(), "zero initializer is a constant"); - return from_integer(string2integer(get_gdb_value(expr)), expr.type()); + std::string c_expr = c_converter.convert(expr); + const auto maybe_value = gdb_api.get_value(c_expr); + if(!maybe_value.has_value()) + return zero_expr; + const std::string value = *maybe_value; + + const mp_integer int_rep = string2integer(value); + + return from_integer(int_rep, type); } else if(is_c_char_type(type)) { INVARIANT(zero_expr.is_constant(), "zero initializer is a constant"); - return zero_expr; // currently left at 0 + // check the char-value and return as bitvector-type value + std::string c_expr = c_converter.convert(expr); + const auto maybe_value = gdb_api.get_value(c_expr); + if(!maybe_value.has_value() || maybe_value->empty()) + return zero_expr; + const std::string value = *maybe_value; + + const mp_integer int_rep = value[0]; + return from_integer(int_rep, type); } else if(type.id() == ID_c_bool) { INVARIANT(zero_expr.is_constant(), "zero initializer is a constant"); - return from_c_boolean_value(id2boolean(get_gdb_value(expr)), type); + std::string c_expr = c_converter.convert(expr); + const auto maybe_value = gdb_api.get_value(c_expr); + if(!maybe_value.has_value()) + return zero_expr; + const std::string value = *maybe_value; + + return from_c_boolean_value(id2boolean(value), type); } else if(type.id() == ID_c_enum) { INVARIANT(zero_expr.is_constant(), "zero initializer is a constant"); - return convert_member_name_to_enum_value( - get_gdb_value(expr), to_c_enum_type(type)); + std::string c_expr = c_converter.convert(expr); + const auto maybe_value = gdb_api.get_value(c_expr); + if(!maybe_value.has_value()) + return zero_expr; + const std::string value = *maybe_value; + + return convert_member_name_to_enum_value(value, to_c_enum_type(type)); } else if(type.id() == ID_struct_tag) { @@ -503,5 +625,8 @@ void gdb_value_extractort::process_outstanding_assignments() std::string gdb_value_extractort::get_gdb_value(const exprt &expr) { - return gdb_api.get_value(c_converter.convert(expr)); + std::string c_expr = c_converter.convert(expr); + const auto maybe_value = gdb_api.get_value(c_expr); + CHECK_RETURN(maybe_value.has_value()); + return *maybe_value; } diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index e487933f905..470ae9c020b 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -24,6 +24,7 @@ Author: Malte Mues #include #include +#include #include #include @@ -56,6 +57,47 @@ gdb_apit::~gdb_apit() wait(NULL); } +size_t gdb_apit::query_malloc_size(const std::string &pointer_expr) +{ +#ifdef __linux__ + write_to_gdb("-var-create tmp * malloc_usable_size(" + pointer_expr + ")"); +#elif __APPLE__ + write_to_gdb("-var-create tmp * malloc_size(" + pointer_expr + ")"); +#else + // Under non-linux/OSX system we simple return 1, i.e. as if the \p + // pointer_expr was not dynamically allocated. + return 1; +#endif + + if(!was_command_accepted()) + { + return 1; + } + + write_to_gdb("-var-evaluate-expression tmp"); + gdb_output_recordt record = get_most_recent_record("^done", true); + + write_to_gdb("-var-delete tmp"); + check_command_accepted(); + + const auto it = record.find("value"); + CHECK_RETURN(it != record.end()); + + const std::string value = it->second; + + INVARIANT( + value.back() != '"' || + (value.length() >= 2 && value[value.length() - 2] == '\\'), + "quotes should have been stripped off from value"); + INVARIANT(value.back() != '\n', "value should not end in a newline"); + + const auto result = string2optional_size_t(value); + if(result.has_value()) + return *result; + else + return 1; +} + void gdb_apit::create_gdb_process() { PRECONDITION(gdb_state == gdb_statet::NOT_CREATED); @@ -335,14 +377,23 @@ gdb_apit::pointer_valuet gdb_apit::get_memory(const std::string &expr) { PRECONDITION(gdb_state == gdb_statet::STOPPED); - std::string value = eval_expr(expr); + std::string value; + try + { + value = eval_expr(expr); + } + catch(gdb_interaction_exceptiont &e) + { + return pointer_valuet{}; + } std::regex regex( r_hex_addr + r_opt(' ' + r_id) + r_opt(' ' + r_or(r_char, r_string))); std::smatch result; const bool b = regex_match(value, result, regex); - CHECK_RETURN(b); + if(!b) + return pointer_valuet{}; optionalt opt_string; const std::string string = result[4]; @@ -370,14 +421,22 @@ gdb_apit::pointer_valuet gdb_apit::get_memory(const std::string &expr) opt_string = string.substr(2, len - 4); } - return pointer_valuet(result[1], result[2], result[3], opt_string); + return pointer_valuet(result[1], result[2], result[3], opt_string, true); } -std::string gdb_apit::get_value(const std::string &expr) +optionalt gdb_apit::get_value(const std::string &expr) { PRECONDITION(gdb_state == gdb_statet::STOPPED); - const std::string value = eval_expr(expr); + std::string value; + try + { + value = eval_expr(expr); + } + catch(gdb_interaction_exceptiont &e) + { + return {}; + } // Get char value { @@ -389,7 +448,7 @@ std::string gdb_apit::get_value(const std::string &expr) if(b) { - return result[1]; + return std::string{result[1]}; } } diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 1312bebe6fb..ad86e44ffbf 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -68,13 +68,17 @@ class gdb_apit struct pointer_valuet { - pointer_valuet() = delete; pointer_valuet( - const std::string &address, - const std::string &pointee, - const std::string &character, - const optionalt &string) - : address(address), pointee(pointee), character(character), string(string) + const std::string &address = "", + const std::string &pointee = "", + const std::string &character = "", + const optionalt &string = nullopt, + const bool valid = false) + : address(address), + pointee(pointee), + character(character), + string(string), + valid(valid) { } @@ -88,8 +92,21 @@ class gdb_apit return std::any_of( pointee.begin(), pointee.end(), [](char c) { return c == '+'; }); } + + bool valid; }; + /// Get the allocated size estimate for a pointer by evaluating + /// `malloc_usable_size'. The function returns the number of usable bytes in + /// the block pointed to by the pointer to a block of memory allocated by + /// `malloc' or a related function. The value may be greater than the + /// requested size of the allocation because of alignment and minimum size + /// constraints. + /// \param pointer_expr: expression with a pointer name + /// \return 1 if the pointer was not allocated with malloc otherwise return + /// the result of calling `malloc_usable_size' + size_t query_malloc_size(const std::string &pointer_expr); + /// Create a new gdb process for analysing the binary indicated by the member /// variable `binary` void create_gdb_process(); @@ -104,17 +121,12 @@ class gdb_apit /// \param corefile: core dump void run_gdb_from_core(const std::string &corefile); - /// Get value of the given value expression - /// \param expr: an expression of non-pointer type or pointer to char - /// \return value of the expression; if the expression is of type pointer to - /// char and represents a string, the string value is returned; otherwise - /// the value is returned just as it is printed by gdb - std::string get_value(const std::string &expr); - /// Get the memory address pointed to by the given pointer expression /// \param expr: an expression of pointer type (e.g., `&x` with `x` being of /// type `int` or `p` with `p` being of type `int *`) /// \return memory address in hex format + optionalt get_value(const std::string &expr); + pointer_valuet get_memory(const std::string &expr); /// Return the vector of commands that have been written to gdb so far diff --git a/src/util/c_types_util.h b/src/util/c_types_util.h index 26b46d6282c..37a0e6738b4 100644 --- a/src/util/c_types_util.h +++ b/src/util/c_types_util.h @@ -100,9 +100,9 @@ constant_exprt convert_member_name_to_enum_value( /// Convert id to a Boolean value /// \param bool_value: A string that is compared to "true" ignoring case. /// \return a constant of type Boolean -bool id2boolean(const irep_idt &bool_value) +bool id2boolean(const std::string &bool_value) { - std::string string_value = id2string(bool_value); + std::string string_value = bool_value; std::transform( string_value.begin(), string_value.end(), string_value.begin(), ::tolower); if(string_value == "true") diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index 25022371d2b..f8cfcd38ce7 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -167,9 +167,16 @@ TEST_CASE("gdb api test", "[core][memory-analyzer]") const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); REQUIRE(r); - REQUIRE(gdb_api.get_value("x") == "8"); - REQUIRE(gdb_api.get_value("y") == "2.5"); - REQUIRE(gdb_api.get_value("z") == "c"); + const auto &x_value = gdb_api.get_value("x"); + const auto &y_value = gdb_api.get_value("y"); + const auto &z_value = gdb_api.get_value("z"); + + REQUIRE(x_value.has_value()); + REQUIRE(*x_value == "8"); + REQUIRE(y_value.has_value()); + REQUIRE(*y_value == "2.5"); + REQUIRE(z_value.has_value()); + REQUIRE(*z_value == "c"); } SECTION("query pointers")