From 1e71fd7fbc4d225c99e80ffe02fb8a050c8a280d Mon Sep 17 00:00:00 2001 From: Malte Mues Date: Thu, 12 Jul 2018 10:22:16 -0400 Subject: [PATCH 01/17] Add an api to analyze a core dump with gdb Applying CBMC on large code bases requires sometimes to model a test environment. Running a program until a certain point and let it crash, allows to analyze the memory state at this point in time. In continuation, the memory state might be reconstructed as base for the test environment model. By using gdb to analyze the core dump, I don't have to take care of reading and interpreting the core dump myself. --- src/memory-analyzer/gdb_api.cpp | 266 +++++++++++++++++++++++++++++++ src/memory-analyzer/gdb_api.h | 76 +++++++++ unit/memory-analyzer/gdb_api.cpp | 235 +++++++++++++++++++++++++++ 3 files changed, 577 insertions(+) create mode 100644 src/memory-analyzer/gdb_api.cpp create mode 100644 src/memory-analyzer/gdb_api.h create mode 100644 unit/memory-analyzer/gdb_api.cpp diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp new file mode 100644 index 00000000000..a363c004a2f --- /dev/null +++ b/src/memory-analyzer/gdb_api.cpp @@ -0,0 +1,266 @@ +// Copyright 2018 Author: Malte Mues +#ifdef __linux__ +#include +#include +#include +#include +#include + +#include "gdb_api.h" +#include + +gdb_apit::gdb_apit(const char *arg) + : binary_name(arg), buffer_position(0), last_read_size(0) +{ + memset(buffer, 0, MAX_READ_SIZE_GDB_BUFFER); +} + +int gdb_apit::create_gdb_process() +{ + if(pipe(pipe_input) == -1) + { + throw gdb_interaction_exceptiont("could not create pipe for stdin!"); + } + if(pipe(pipe_output) == -1) + { + throw gdb_interaction_exceptiont("could not create pipe for stdout!"); + } + + gdb_process = fork(); + if(gdb_process == -1) + { + throw gdb_interaction_exceptiont("could not create gdb process."); + } + if(gdb_process == 0) + { + // child process + close(pipe_input[1]); + close(pipe_output[0]); + dup2(pipe_input[0], STDIN_FILENO); + dup2(pipe_output[1], STDOUT_FILENO); + dup2(pipe_output[1], STDERR_FILENO); + dprintf(pipe_output[1], "binary name: %s\n", binary_name); + char *arg[] = { + const_cast("gdb"), const_cast(binary_name), NULL}; + + dprintf(pipe_output[1], "Loading gdb...\n"); + execvp("gdb", arg); + + // Only reachable, if execvp failed + int errno_value = errno; + dprintf(pipe_output[1], "errno in child: %s\n", strerror(errno_value)); + } + else + { + // parent process + close(pipe_input[0]); + close(pipe_output[1]); + write_to_gdb("set max-value-size unlimited\n"); + } + return 0; +} + +void gdb_apit::terminate_gdb_process() +{ + close(pipe_input[0]); + close(pipe_input[1]); +} + +void gdb_apit::write_to_gdb(const std::string &command) +{ + if( + write(pipe_input[1], command.c_str(), command.length()) != + (ssize_t)command.length()) + { + throw gdb_interaction_exceptiont("Could not write a command to gdb"); + } +} + +std::string gdb_apit::read_next_line() +{ + char token; + std::string line; + do + { + while(buffer_position >= last_read_size) + { + read_next_buffer_chunc(); + } + token = buffer[buffer_position]; + line += token; + ++buffer_position; + } while(token != '\n'); + return line; +} + +void gdb_apit::read_next_buffer_chunc() +{ + memset(buffer, 0, last_read_size); + const auto read_size = + read(pipe_output[0], &buffer, MAX_READ_SIZE_GDB_BUFFER); + if(read_size < 0) + { + throw gdb_interaction_exceptiont("Error reading from gdb_process"); + } + last_read_size = read_size; + buffer_position = 0; +} + +void gdb_apit::run_gdb_from_core(const std::string &corefile) +{ + const std::string command = "core " + corefile + "\n"; + write_to_gdb(command); + std::string line; + while(!isdigit(line[0])) + { + line = read_next_line(); + if(check_for_gdb_core_error(line)) + { + terminate_gdb_process(); + throw gdb_interaction_exceptiont( + "This core file doesn't work with the binary."); + } + } +} + +bool gdb_apit::check_for_gdb_core_error(const std::string &line) +{ + const std::regex core_init_error_r("exec file is newer than core"); + return regex_search(line, core_init_error_r); +} + +void gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) +{ + std::string command = "break " + breakpoint + "\n"; + write_to_gdb(command); + command = "run\n"; + write_to_gdb(command); + std::string line; + while(!isdigit(line[0])) + { + line = read_next_line(); + if(check_for_gdb_breakpoint_error(line)) + { + terminate_gdb_process(); + throw gdb_interaction_exceptiont("This is not a valid breakpoint\n"); + } + } +} + +bool gdb_apit::check_for_gdb_breakpoint_error(const std::string &line) +{ + const std::regex breakpoint_init_error_r("Make breakpoint pending on future"); + return regex_search(line, breakpoint_init_error_r); +} + +std::string gdb_apit::create_command(const std::string &variable) +{ + return "p " + variable + "\n"; +} + +std::string gdb_apit::get_memory(const std::string &variable) +{ + write_to_gdb(create_command(variable)); + const std::string &response = read_next_line(); + return extract_memory(response); +} + +// All lines in the output start with something like +// '$XX = ' where XX is a digit. => shared_prefix. +const char shared_prefix[] = R"(\$[0-9]+\s=\s)"; + +// Matching a hex encoded address. +const char memory_address[] = R"(0x[[:xdigit:]]+)"; + +std::string gdb_apit::extract_memory(const std::string &line) +{ + // The next patterns matches the type information, + // which be "(classifier struct name (*)[XX])" + // for pointer to struct arrayes. classsifier and struct is optional => {1,3} + // If it isn't an array, than the ending is " *)" + // => or expression in pointer_star_or_array_suffix. + const std::string struct_name = R"((?:\S+\s){1,3})"; + const std::string pointer_star_or_arary_suffix = + R"((?:\*|(?:\*)?\(\*\)\[[0-9]+\])?)"; + const std::string pointer_type_info = + R"(\()" + struct_name + pointer_star_or_arary_suffix + R"(\))"; + + // The pointer type info is followed by the memory value and eventually + // extended by the name of the pointer content, if gdb has an explicit symbol. + // See unit test cases for more examples of expected input. + const std::regex pointer_pattern( + std::string(shared_prefix) + pointer_type_info + R"(\s()" + memory_address + + R"()(\s\S+)?)"); + const std::regex null_pointer_pattern( + std::string(shared_prefix) + R"((0x0))"); + // Char pointer output the memory adress followed by the string in there. + const std::regex char_pointer_pattern( + std::string(shared_prefix) + R"(()" + memory_address + + R"()\s"[\S[:s:]]*")"); + + std::smatch result; + if(regex_search(line, result, char_pointer_pattern)) + { + return result[1]; + } + if(regex_search(line, result, pointer_pattern)) + { + return result[1]; + } + if(regex_search(line, result, null_pointer_pattern)) + { + return result[1]; + } + throw gdb_interaction_exceptiont("Cannot resolve memory_address: " + line); +} + +std::string gdb_apit::get_value(const std::string &variable) +{ + write_to_gdb(create_command(variable)); + const std::string &response = read_next_line(); + return extract_value(response); +} + +std::string gdb_apit::extract_value(const std::string &line) +{ + // This pattern matches primitive int values and bools. + const std::regex value_pattern( + std::string(shared_prefix) + R"(((?:-)?\d+|true|false))"); + // This pattern matches the char pointer content. + // It is printed behind the address. + const std::regex char_value_pattern( + std::string(shared_prefix) + memory_address + "\\s\"([\\S ]*)\""); + // An enum entry just prints the name of the value on the commandline. + const std::regex enum_value_pattern( + std::string(shared_prefix) + R"(([\S]+)(?:\n|$))"); + // A void pointer outputs it type first, followed by the memory address it + // is pointing to. This pattern should extract the address. + const std::regex void_pointer_pattern( + std::string(shared_prefix) + R"((?:[\S\s]+)\s()" + memory_address + ")"); + + std::smatch result; + if(regex_search(line, result, char_value_pattern)) + { + return result[1]; + } + if(regex_search(line, result, value_pattern)) + { + return result[1]; + } + if(regex_search(line, result, enum_value_pattern)) + { + return result[1]; + } + if(regex_search(line, result, void_pointer_pattern)) + { + return result[1]; + } + std::regex memmory_access_error("Cannot access memory"); + if(regex_search(line, memmory_access_error)) + { + throw gdb_inaccessible_memoryt("ERROR: " + line); + } + throw gdb_interaction_exceptiont("Cannot extract value from this: " + line); +} + +#endif diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h new file mode 100644 index 00000000000..b9e3d915b9c --- /dev/null +++ b/src/memory-analyzer/gdb_api.h @@ -0,0 +1,76 @@ +// Copyright 2018 Author: Malte Mues +#ifdef __linux__ +#ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H +#define CPROVER_MEMORY_ANALYZER_GDB_API_H +#include + +#include + +class namespacet; +class symbolt; +class irept; + +class gdb_apit +{ +public: + explicit gdb_apit(const char *binary); + + int create_gdb_process(); + void terminate_gdb_process(); + + void run_gdb_to_breakpoint(const std::string &breakpoint); + void run_gdb_from_core(const std::string &corefile); + + std::string get_value(const std::string &variable); + std::string get_memory(const std::string &variable); + +private: + static const int MAX_READ_SIZE_GDB_BUFFER = 600; + + const char *binary_name; + char buffer[MAX_READ_SIZE_GDB_BUFFER]; + int buffer_position; + pid_t gdb_process; + int last_read_size; + int pipe_input[2]; + int pipe_output[2]; + + static std::string create_command(const std::string &variable); + void write_to_gdb(const std::string &command); + + std::string read_next_line(); + void read_next_buffer_chunc(); + + static bool check_for_gdb_breakpoint_error(const std::string &line); + static bool check_for_gdb_core_error(const std::string &line); + + static std::string extract_value(const std::string &line); + static std::string extract_memory(const std::string &line); +}; + +class gdb_interaction_exceptiont : public std::exception +{ +public: + explicit gdb_interaction_exceptiont(std::string reason) : std::exception() + { + error = reason; + } + const char *what() const throw() + { + return error.c_str(); + } + +private: + std::string error; +}; + +class gdb_inaccessible_memoryt : public gdb_interaction_exceptiont +{ +public: + explicit gdb_inaccessible_memoryt(std::string reason) + : gdb_interaction_exceptiont(reason) + { + } +}; +#endif +#endif diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp new file mode 100644 index 00000000000..80547419040 --- /dev/null +++ b/unit/memory-analyzer/gdb_api.cpp @@ -0,0 +1,235 @@ +// Copyright 2018 Malte Mues +#include + +#ifdef __linux__ +// \file Test that the regex expression used work as expected. +#define private public +#include +#include + +SCENARIO( + "gdb_apit uses regex as expected for memory", + "[core][memory-analyzer]") +{ + gdb_apit gdb_api(""); + GIVEN("The result of a struct pointer") + { + const std::string line = "$2 = (struct cycle_buffer *) 0x601050 "; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x601050"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x601050"); + } + } + + GIVEN("The result of a typedef pointer") + { + const std::string line = "$4 = (cycle_buffer_entry_t *) 0x602010"; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x602010"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x602010"); + } + } + + GIVEN("The result of a char pointer") + { + const std::string line = "$5 = 0x400734 \"snow\""; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x400734"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x400734"); + } + } + + GIVEN("The result of a null pointer") + { + const std::string line = "$2 = 0x0"; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x0"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x0"); + } + } + + GIVEN("The result of a char pointer at very low address") + { + const std::string line = "$34 = 0x007456 \"snow\""; + THEN("the result matches the memory address and not nullpointer") + { + REQUIRE(gdb_api.extract_memory(line) == "0x007456"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x007456"); + } + } + + GIVEN("The result of a char pointer with some more whitespaces") + { + const std::string line = "$12 = 0x400752 \"thunder storm\"\n"; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x400752"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x400752"); + } + } + + GIVEN("The result of an array pointer") + { + const std::string line = "$5 = (struct a_sub_type_t (*)[4]) 0x602080"; + THEN("the result matches the memory address in the output") + { + REQUIRE(gdb_api.extract_memory(line) == "0x602080"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x602080"); + } + } + + GIVEN("A constant struct pointer pointing to 0x0") + { + const std::string line = "$3 = (const struct name *) 0x0"; + THEN("the returned memory address should be 0x0") + { + REQUIRE(gdb_api.extract_memory(line) == "0x0"); + } + } + + GIVEN("An enum address") + { + const std::string line = "$2 = (char *(*)[5]) 0x7e5500 "; + THEN("the returned address is the address of the enum") + { + REQUIRE(gdb_api.extract_memory(line) == "0x7e5500"); + } + } + + GIVEN("The result of an int pointer") + { + const std::string line = "$1 = (int *) 0x601088 \n"; + THEN("the result is the value of memory address of the int pointer") + { + REQUIRE(gdb_api.extract_memory(line) == "0x601088"); + } + THEN("adding '(gdb) ' to the line doesn't have an influence") + { + REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x601088"); + } + } + + GIVEN("Non matching result") + { + const std::string line = "Something that must not match 0x605940"; + THEN("an exception is thrown") + { + REQUIRE_THROWS_AS( + gdb_api.extract_memory(line), gdb_interaction_exceptiont); + } + } +} + +SCENARIO( + "gdb_apit uses regex as expected for value extraction", + "[core][memory-analyzer]") +{ + gdb_apit gdb_api(""); + GIVEN("An integer value") + { + const std::string line = "$90 = 100"; + THEN("the result schould be '100'") + { + REQUIRE(gdb_api.extract_value(line) == "100"); + } + } + + GIVEN("A string value") + { + const std::string line = "$5 = 0x602010 \"snow\""; + THEN("the result should be 'snow'") + { + REQUIRE(gdb_api.extract_value(line) == "snow"); + } + } + + GIVEN("A string with withe spaces") + { + const std::string line = "$1323 = 0x1243253 \"thunder storm\"\n"; + THEN("the result should be 'thunder storm'") + { + REQUIRE(gdb_api.extract_value(line) == "thunder storm"); + } + } + + GIVEN("A byte value") + { + const std::string line = "$2 = 243 '\363'"; + THEN("the result should be 243") + { + REQUIRE(gdb_api.extract_value(line) == "243"); + } + } + + GIVEN("A negative int value") + { + const std::string line = "$8 = -32"; + THEN("the result should be -32") + { + REQUIRE(gdb_api.extract_value(line) == "-32"); + } + } + + GIVEN("An enum value") + { + const std::string line = "$1 = INFO"; + THEN("the result should be INFO") + { + REQUIRE(gdb_api.extract_value(line) == "INFO"); + } + } + + GIVEN("A void pointer value") + { + const std::string line = "$6 = (const void *) 0x71"; + THEN("the requried result should be 0x71") + { + REQUIRE(gdb_api.extract_value(line) == "0x71"); + } + } + + GIVEN("A gdb response that contains 'cannot access memory'") + { + const std::string line = "Cannot access memory at address 0x71"; + THEN("a gdb_inaccesible_memoryt excepition must be raised") + { + REQUIRE_THROWS_AS(gdb_api.extract_value(line), gdb_inaccessible_memoryt); + } + } + + GIVEN("A value that must not match") + { + const std::string line = "$90 = must not match 20"; + THEN("an exception is raised") + { + REQUIRE_THROWS_AS( + gdb_api.extract_value(line), gdb_interaction_exceptiont); + } + } +} +#endif From d28c85c94ef5c46a632e9789ce0fdb22e27c92fd Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 23 Jan 2019 12:33:44 +0000 Subject: [PATCH 02/17] Add method to parse gdb output records When using the gdb machine interface (option --interpreter=mi), gdb outputs results (such as that of printing a value) as records which are comma-separated lists of key=value pairs. This adds a method parse_gdb_output_record() to parse such records into a std::map. --- src/memory-analyzer/gdb_api.cpp | 68 ++++++++++++++++++++++++++++++++- src/memory-analyzer/gdb_api.h | 3 ++ 2 files changed, 69 insertions(+), 2 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index a363c004a2f..42eef52a192 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -9,8 +9,9 @@ #include "gdb_api.h" #include -gdb_apit::gdb_apit(const char *arg) - : binary_name(arg), buffer_position(0), last_read_size(0) +#include + +gdb_apit::gdb_apit(const char *arg) : binary_name(arg) { memset(buffer, 0, MAX_READ_SIZE_GDB_BUFFER); } @@ -263,4 +264,67 @@ std::string gdb_apit::extract_value(const std::string &line) throw gdb_interaction_exceptiont("Cannot extract value from this: " + line); } +gdb_apit::gdb_output_recordt +gdb_apit::parse_gdb_output_record(const std::string &s) +{ + PRECONDITION(s.back() != '\n'); + + gdb_output_recordt result; + + unsigned depth = 0; + std::string::size_type start = 0; + + const std::string::size_type n = s.length(); + + for(std::string::size_type i = 0; i < n; i++) + { + const char c = s[i]; + + if(c == '{' || c == '[') + { + depth++; + } + else if(c == '}' || c == ']') + { + depth--; + } + + if(depth == 0 && (c == ',' || i == n - 1)) + { + const std::string item = + i == n - 1 ? s.substr(start) : s.substr(start, i - start); + + // Split on first `=` + std::string::size_type j = item.find('='); + CHECK_RETURN(j != std::string::npos); + CHECK_RETURN(j > 0); + CHECK_RETURN(j < s.length()); + + const std::string key = strip_string(item.substr(0, j)); + std::string value = strip_string(item.substr(j + 1)); + + const char first = value.front(); + const char last = value.back(); + + INVARIANT(first == '"' || first == '{' || first == '[', ""); + INVARIANT(first != '"' || last == '"', ""); + INVARIANT(first != '{' || last == '}', ""); + INVARIANT(first != '[' || last == ']', ""); + + // Remove enclosing `"` for primitive values + if(first == '"') + { + value = value.substr(1, value.length() - 2); + } + + auto r = result.insert(std::make_pair(key, value)); + CHECK_RETURN(r.second); + + start = i + 1; + } + } + + return result; +} + #endif diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index b9e3d915b9c..f5ddf5a2e18 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -46,6 +46,9 @@ class gdb_apit static std::string extract_value(const std::string &line); static std::string extract_memory(const std::string &line); + + typedef std::map gdb_output_recordt; + static gdb_output_recordt parse_gdb_output_record(const std::string &s); }; class gdb_interaction_exceptiont : public std::exception From 81fcf262097e19a2f1b692be3ae9050396189829 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 23 Jan 2019 14:11:32 +0000 Subject: [PATCH 03/17] Remove unnecessary forward declarations of cprover types --- src/memory-analyzer/gdb_api.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index f5ddf5a2e18..171e9b01c07 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -6,10 +6,6 @@ #include -class namespacet; -class symbolt; -class irept; - class gdb_apit { public: From b73bb29b7ae1db3257555c195e96b058b8cc479f Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 14:40:35 +0000 Subject: [PATCH 04/17] Use streams to communicate with gdb subprocess This switches gdb_apit to use streams to communicate with the gdb subprocess instead of using pipes/file descriptors directly. --- src/memory-analyzer/gdb_api.cpp | 63 +++++++++++++++++++-------------- src/memory-analyzer/gdb_api.h | 13 +++---- 2 files changed, 40 insertions(+), 36 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index 42eef52a192..edc7898bdc7 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -13,11 +13,15 @@ gdb_apit::gdb_apit(const char *arg) : binary_name(arg) { - memset(buffer, 0, MAX_READ_SIZE_GDB_BUFFER); } int gdb_apit::create_gdb_process() { + pid_t gdb_process; + + int pipe_input[2]; + int pipe_output[2]; + if(pipe(pipe_input) == -1) { throw gdb_interaction_exceptiont("could not create pipe for stdin!"); @@ -56,6 +60,13 @@ int gdb_apit::create_gdb_process() // parent process close(pipe_input[0]); close(pipe_output[1]); + + // get stream for reading the gdb output + input_stream = fdopen(pipe_output[0], "r"); + + // get stream for writing to gdb + output_stream = fdopen(pipe_input[1], "w"); + write_to_gdb("set max-value-size unlimited\n"); } return 0; @@ -63,15 +74,13 @@ int gdb_apit::create_gdb_process() void gdb_apit::terminate_gdb_process() { - close(pipe_input[0]); - close(pipe_input[1]); + fclose(input_stream); + fclose(output_stream); } void gdb_apit::write_to_gdb(const std::string &command) { - if( - write(pipe_input[1], command.c_str(), command.length()) != - (ssize_t)command.length()) + if(fputs(command.c_str(), output_stream) == EOF) { throw gdb_interaction_exceptiont("Could not write a command to gdb"); } @@ -79,32 +88,32 @@ void gdb_apit::write_to_gdb(const std::string &command) std::string gdb_apit::read_next_line() { - char token; - std::string line; + std::string result; + do { - while(buffer_position >= last_read_size) + const size_t buf_size = 1024; + char buf[buf_size]; + + const char *c = fgets(buf, buf_size, input_stream); + + if(c == NULL) { - read_next_buffer_chunc(); + if(ferror(input_stream)) + { + throw gdb_interaction_exceptiont("error reading from gdb"); + } + + INVARIANT(feof(input_stream), ""); + INVARIANT(result.back() != '\n', ""); + + return result; } - token = buffer[buffer_position]; - line += token; - ++buffer_position; - } while(token != '\n'); - return line; -} -void gdb_apit::read_next_buffer_chunc() -{ - memset(buffer, 0, last_read_size); - const auto read_size = - read(pipe_output[0], &buffer, MAX_READ_SIZE_GDB_BUFFER); - if(read_size < 0) - { - throw gdb_interaction_exceptiont("Error reading from gdb_process"); - } - last_read_size = read_size; - buffer_position = 0; + result += std::string(buf); + } while(result.back() != '\n'); + + return result; } void gdb_apit::run_gdb_from_core(const std::string &corefile) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 171e9b01c07..8b88955100b 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -6,6 +6,8 @@ #include +#include + class gdb_apit { public: @@ -21,21 +23,14 @@ class gdb_apit std::string get_memory(const std::string &variable); private: - static const int MAX_READ_SIZE_GDB_BUFFER = 600; - const char *binary_name; - char buffer[MAX_READ_SIZE_GDB_BUFFER]; - int buffer_position; - pid_t gdb_process; - int last_read_size; - int pipe_input[2]; - int pipe_output[2]; + FILE *input_stream; + FILE *output_stream; static std::string create_command(const std::string &variable); void write_to_gdb(const std::string &command); std::string read_next_line(); - void read_next_buffer_chunc(); static bool check_for_gdb_breakpoint_error(const std::string &line); static bool check_for_gdb_core_error(const std::string &line); From d44dfb99c93510f869cac5905f26cf08e9a9470a Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 14:49:38 +0000 Subject: [PATCH 05/17] Adapt gdb interaction exception to cprover style --- src/memory-analyzer/gdb_api.cpp | 2 +- src/memory-analyzer/gdb_api.h | 25 ++++++++++++++++--------- unit/memory-analyzer/gdb_api.cpp | 3 ++- 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index edc7898bdc7..d12c4edeb28 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -268,7 +268,7 @@ std::string gdb_apit::extract_value(const std::string &line) std::regex memmory_access_error("Cannot access memory"); if(regex_search(line, memmory_access_error)) { - throw gdb_inaccessible_memoryt("ERROR: " + line); + throw gdb_inaccessible_memory_exceptiont("ERROR: " + line); } throw gdb_interaction_exceptiont("Cannot extract value from this: " + line); } diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 8b88955100b..b4e18edde6a 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -42,29 +42,36 @@ class gdb_apit static gdb_output_recordt parse_gdb_output_record(const std::string &s); }; -class gdb_interaction_exceptiont : public std::exception +class gdb_interaction_exceptiont : public cprover_exception_baset { public: - explicit gdb_interaction_exceptiont(std::string reason) : std::exception() + explicit gdb_interaction_exceptiont(std::string reason) : reason(reason) { - error = reason; } - const char *what() const throw() + std::string what() const override { - return error.c_str(); + return reason; } private: - std::string error; + std::string reason; }; -class gdb_inaccessible_memoryt : public gdb_interaction_exceptiont +class gdb_inaccessible_memory_exceptiont : public cprover_exception_baset { public: - explicit gdb_inaccessible_memoryt(std::string reason) - : gdb_interaction_exceptiont(reason) + explicit gdb_inaccessible_memory_exceptiont(std::string reason) + : reason(reason) { } + + std::string what() const override + { + return reason; + } + +private: + std::string reason; }; #endif #endif diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index 80547419040..d0e17b4f87b 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -218,7 +218,8 @@ SCENARIO( const std::string line = "Cannot access memory at address 0x71"; THEN("a gdb_inaccesible_memoryt excepition must be raised") { - REQUIRE_THROWS_AS(gdb_api.extract_value(line), gdb_inaccessible_memoryt); + REQUIRE_THROWS_AS( + gdb_api.extract_value(line), gdb_inaccessible_memory_exceptiont); } } From a49c4214c492dd4b810bac4658938a8cea4b1371 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 14:54:23 +0000 Subject: [PATCH 06/17] Add #endif comments to gdb api header file --- src/memory-analyzer/gdb_api.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index b4e18edde6a..6ac80ec267f 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -73,5 +73,5 @@ class gdb_inaccessible_memory_exceptiont : public cprover_exception_baset private: std::string reason; }; -#endif -#endif +#endif // CPROVER_MEMORY_ANALYZER_GDB_API_H +#endif // __linux__ From 0b9480bb4053968adf62a49953760033efe9a602 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 18:09:25 +0000 Subject: [PATCH 07/17] Update banners for gdb api files --- src/memory-analyzer/gdb_api.cpp | 10 +++++++++- src/memory-analyzer/gdb_api.h | 10 +++++++++- unit/memory-analyzer/gdb_api.cpp | 12 ++++++++++-- 3 files changed, 28 insertions(+), 4 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index d12c4edeb28..b85ac2b9816 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -1,4 +1,12 @@ -// Copyright 2018 Author: Malte Mues +/*******************************************************************\ + +Module: GDB Machine Interface API + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + #ifdef __linux__ #include #include diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 6ac80ec267f..55740320cfc 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -1,4 +1,12 @@ -// Copyright 2018 Author: Malte Mues +/*******************************************************************\ + +Module: GDB Machine Interface API + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + #ifdef __linux__ #ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H #define CPROVER_MEMORY_ANALYZER_GDB_API_H diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index d0e17b4f87b..67e808ac889 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -1,5 +1,13 @@ -// Copyright 2018 Malte Mues -#include +/*******************************************************************\ + +Module: GDB Machine Interface API unit tests + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + +#include #ifdef __linux__ // \file Test that the regex expression used work as expected. From fa3c78f9fbfb9946a747abe4620295682352eb3d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 27 Jan 2019 19:19:50 +0000 Subject: [PATCH 08/17] Switch gdb_apit to using the gdb machine interface This changes gdb_apit to use the gdb machine interface (mi) instead of the gdb command line user interface to communicate with gdb. --- src/memory-analyzer/gdb_api.cpp | 379 +++++++++++++++++++++----------- src/memory-analyzer/gdb_api.h | 54 +++-- 2 files changed, 294 insertions(+), 139 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index b85ac2b9816..f344ed55110 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -7,6 +7,9 @@ Author: Malte Mues \*******************************************************************/ +/// \file +/// Low-level interface to gdb + #ifdef __linux__ #include #include @@ -19,12 +22,23 @@ Author: Malte Mues #include -gdb_apit::gdb_apit(const char *arg) : binary_name(arg) +/// Create a gdb_apit object +/// +/// \param binary the binary to run with gdb +/// \param log boolean indicating whether gdb input and output should be logged +gdb_apit::gdb_apit(const char *binary, const bool log) + : binary(binary), log(log), gdb_state(gdb_statet::NOT_CREATED) { } -int gdb_apit::create_gdb_process() +/// Create a new gdb process for analysing the binary indicated by the member +/// variable `binary` +void gdb_apit::create_gdb_process() { + PRECONDITION(gdb_state == gdb_statet::NOT_CREATED); + + command_log.clear(); + pid_t gdb_process; int pipe_input[2]; @@ -32,17 +46,17 @@ int gdb_apit::create_gdb_process() if(pipe(pipe_input) == -1) { - throw gdb_interaction_exceptiont("could not create pipe for stdin!"); + throw gdb_interaction_exceptiont("could not create pipe for stdin"); } if(pipe(pipe_output) == -1) { - throw gdb_interaction_exceptiont("could not create pipe for stdout!"); + throw gdb_interaction_exceptiont("could not create pipe for stdout"); } gdb_process = fork(); if(gdb_process == -1) { - throw gdb_interaction_exceptiont("could not create gdb process."); + throw gdb_interaction_exceptiont("could not create gdb process"); } if(gdb_process == 0) { @@ -52,9 +66,11 @@ int gdb_apit::create_gdb_process() dup2(pipe_input[0], STDIN_FILENO); dup2(pipe_output[1], STDOUT_FILENO); dup2(pipe_output[1], STDERR_FILENO); - dprintf(pipe_output[1], "binary name: %s\n", binary_name); - char *arg[] = { - const_cast("gdb"), const_cast(binary_name), NULL}; + dprintf(pipe_output[1], "binary name: %s\n", binary); + char *arg[] = {const_cast("gdb"), + const_cast("--interpreter=mi"), + const_cast(binary), + NULL}; dprintf(pipe_output[1], "Loading gdb...\n"); execvp("gdb", arg); @@ -66,6 +82,8 @@ int gdb_apit::create_gdb_process() else { // parent process + gdb_state = gdb_statet::CREATED; + close(pipe_input[0]); close(pipe_output[1]); @@ -75,23 +93,66 @@ int gdb_apit::create_gdb_process() // get stream for writing to gdb output_stream = fdopen(pipe_input[1], "w"); - write_to_gdb("set max-value-size unlimited\n"); + CHECK_RETURN(most_recent_line_has_tag(R"(~"done)")); + + if(log) + { + // logs output to `gdb.txt` in the current directory, input is not logged + // hence we log it to `command_log` + write_to_gdb("-gdb-set logging on"); + CHECK_RETURN(most_recent_line_has_tag("^done")); + } + + write_to_gdb("-gdb-set max-value-size unlimited"); + CHECK_RETURN(most_recent_line_has_tag("^done")); } - return 0; } +/// Terminate the gdb process and close open streams (for reading from and +/// writing to gdb) void gdb_apit::terminate_gdb_process() { - fclose(input_stream); + PRECONDITION( + gdb_state == gdb_statet::CREATED || gdb_state == gdb_statet::STOPPED); + + write_to_gdb("-gdb-exit"); + // we cannot use most_recent_line_has_tag() here as it checks the last line + // before the next `(gdb) \n` prompt in the output; however when gdb exits no + // next prompt is printed + CHECK_RETURN(has_tag("^exit", read_next_line())); + + gdb_state = gdb_statet::NOT_CREATED; + fclose(output_stream); + fclose(input_stream); } void gdb_apit::write_to_gdb(const std::string &command) { - if(fputs(command.c_str(), output_stream) == EOF) + PRECONDITION(!command.empty()); + PRECONDITION(command.back() != '\n'); + + std::string line(command); + line += '\n'; + + if(log) + { + command_log.push_back(command); + } + + if(fputs(line.c_str(), output_stream) == EOF) { - throw gdb_interaction_exceptiont("Could not write a command to gdb"); + throw gdb_interaction_exceptiont("could not write a command to gdb"); } + + fflush(output_stream); +} + +/// Return the vector of commands that have been written to gdb so far +const std::vector &gdb_apit::get_command_log() +{ + PRECONDITION(log); + return command_log; } std::string gdb_apit::read_next_line() @@ -101,7 +162,7 @@ std::string gdb_apit::read_next_line() do { const size_t buf_size = 1024; - char buf[buf_size]; + char buf[buf_size]; // NOLINT(runtime/arrays) const char *c = fgets(buf, buf_size, input_stream); @@ -112,173 +173,241 @@ std::string gdb_apit::read_next_line() throw gdb_interaction_exceptiont("error reading from gdb"); } - INVARIANT(feof(input_stream), ""); - INVARIANT(result.back() != '\n', ""); + INVARIANT( + feof(input_stream), + "EOF must have been reached when the error indicator on the stream " + "is not set and fgets returned NULL"); + INVARIANT( + result.empty() || result.back() != '\n', + "when EOF is reached then either no characters were read or the string" + " read does not end in a newline"); return result; } - result += std::string(buf); + std::string chunk(buf); + INVARIANT(!chunk.empty(), "chunk cannot be empty when EOF was not reached"); + + result += chunk; } while(result.back() != '\n'); return result; } -void gdb_apit::run_gdb_from_core(const std::string &corefile) +std::string gdb_apit::read_most_recent_line() { - const std::string command = "core " + corefile + "\n"; - write_to_gdb(command); std::string line; - while(!isdigit(line[0])) + std::string output; + + do { + output = line; line = read_next_line(); - if(check_for_gdb_core_error(line)) - { - terminate_gdb_process(); - throw gdb_interaction_exceptiont( - "This core file doesn't work with the binary."); - } - } -} + } while(line != "(gdb) \n"); -bool gdb_apit::check_for_gdb_core_error(const std::string &line) -{ - const std::regex core_init_error_r("exec file is newer than core"); - return regex_search(line, core_init_error_r); + return output; } -void gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) +gdb_apit::gdb_output_recordt +gdb_apit::get_most_recent_record(const std::string &tag, const bool must_exist) { - std::string command = "break " + breakpoint + "\n"; - write_to_gdb(command); - command = "run\n"; - write_to_gdb(command); - std::string line; - while(!isdigit(line[0])) + std::string line = read_most_recent_line(); + const bool b = has_tag(tag, line); + + if(must_exist) { - line = read_next_line(); - if(check_for_gdb_breakpoint_error(line)) - { - terminate_gdb_process(); - throw gdb_interaction_exceptiont("This is not a valid breakpoint\n"); - } + CHECK_RETURN(b); } + else if(!b) + { + throw gdb_interaction_exceptiont("record does not exist"); + } + + std::string record = strip_string(line.substr(line.find(',') + 1)); + + return parse_gdb_output_record(record); } -bool gdb_apit::check_for_gdb_breakpoint_error(const std::string &line) +bool gdb_apit::has_tag(const std::string &tag, const std::string &line) { - const std::regex breakpoint_init_error_r("Make breakpoint pending on future"); - return regex_search(line, breakpoint_init_error_r); + return line.compare(0, tag.length(), tag) == 0; } -std::string gdb_apit::create_command(const std::string &variable) +bool gdb_apit::most_recent_line_has_tag(const std::string &tag) { - return "p " + variable + "\n"; + const std::string line = read_most_recent_line(); + return has_tag(tag, line); } -std::string gdb_apit::get_memory(const std::string &variable) +/// Run gdb with the given core file +/// +/// \param corefile core dump +void gdb_apit::run_gdb_from_core(const std::string &corefile) { - write_to_gdb(create_command(variable)); - const std::string &response = read_next_line(); - return extract_memory(response); -} + PRECONDITION(gdb_state == gdb_statet::CREATED); -// All lines in the output start with something like -// '$XX = ' where XX is a digit. => shared_prefix. -const char shared_prefix[] = R"(\$[0-9]+\s=\s)"; + // there does not seem to be a gdb mi command to run from a core file + const std::string command = "core " + corefile; -// Matching a hex encoded address. -const char memory_address[] = R"(0x[[:xdigit:]]+)"; + write_to_gdb(command); + CHECK_RETURN(most_recent_line_has_tag("^done")); + + gdb_state = gdb_statet::STOPPED; +} -std::string gdb_apit::extract_memory(const std::string &line) +/// Run gdb to the given breakpoint +/// +/// \param breakpoint the breakpoint to set (can be e.g. a line number or a +/// function name) +bool gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) { - // The next patterns matches the type information, - // which be "(classifier struct name (*)[XX])" - // for pointer to struct arrayes. classsifier and struct is optional => {1,3} - // If it isn't an array, than the ending is " *)" - // => or expression in pointer_star_or_array_suffix. - const std::string struct_name = R"((?:\S+\s){1,3})"; - const std::string pointer_star_or_arary_suffix = - R"((?:\*|(?:\*)?\(\*\)\[[0-9]+\])?)"; - const std::string pointer_type_info = - R"(\()" + struct_name + pointer_star_or_arary_suffix + R"(\))"; - - // The pointer type info is followed by the memory value and eventually - // extended by the name of the pointer content, if gdb has an explicit symbol. - // See unit test cases for more examples of expected input. - const std::regex pointer_pattern( - std::string(shared_prefix) + pointer_type_info + R"(\s()" + memory_address + - R"()(\s\S+)?)"); - const std::regex null_pointer_pattern( - std::string(shared_prefix) + R"((0x0))"); - // Char pointer output the memory adress followed by the string in there. - const std::regex char_pointer_pattern( - std::string(shared_prefix) + R"(()" + memory_address + - R"()\s"[\S[:s:]]*")"); + PRECONDITION(gdb_state == gdb_statet::CREATED); - std::smatch result; - if(regex_search(line, result, char_pointer_pattern)) + std::string command("-break-insert"); + command += " " + breakpoint; + + write_to_gdb(command); + if(!most_recent_line_has_tag("^done")) { - return result[1]; + throw gdb_interaction_exceptiont("could not set breakpoint"); } - if(regex_search(line, result, pointer_pattern)) + + write_to_gdb("-exec-run"); + + if(!most_recent_line_has_tag("*running")) { - return result[1]; + throw gdb_interaction_exceptiont("could not run program"); } - if(regex_search(line, result, null_pointer_pattern)) + + gdb_output_recordt record = get_most_recent_record("*stopped"); + const auto it = record.find("reason"); + CHECK_RETURN(it != record.end()); + + const std::string &reason = it->second; + + if(reason == "breakpoint-hit") { - return result[1]; + gdb_state = gdb_statet::STOPPED; + return true; + } + else if(reason == "exited-normally") + { + return false; } - throw gdb_interaction_exceptiont("Cannot resolve memory_address: " + line); + else + { + throw gdb_interaction_exceptiont( + "gdb stopped for unhandled reason `" + reason + "`"); + } + + // not reached + return true; } -std::string gdb_apit::get_value(const std::string &variable) +std::string gdb_apit::eval_expr(const std::string &expr) { - write_to_gdb(create_command(variable)); - const std::string &response = read_next_line(); - return extract_value(response); + write_to_gdb("-var-create tmp * " + expr); + + if(!most_recent_line_has_tag("^done")) + { + throw gdb_interaction_exceptiont( + "could not create variable for " + "expression `" + + expr + "`"); + } + + write_to_gdb("-var-evaluate-expression tmp"); + gdb_output_recordt record = get_most_recent_record("^done", true); + + write_to_gdb("-var-delete tmp"); + CHECK_RETURN(most_recent_line_has_tag("^done")); + + 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"); + + return value; } -std::string gdb_apit::extract_value(const std::string &line) +/// 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 +std::string gdb_apit::get_memory(const std::string &expr) { - // This pattern matches primitive int values and bools. - const std::regex value_pattern( - std::string(shared_prefix) + R"(((?:-)?\d+|true|false))"); - // This pattern matches the char pointer content. - // It is printed behind the address. - const std::regex char_value_pattern( - std::string(shared_prefix) + memory_address + "\\s\"([\\S ]*)\""); - // An enum entry just prints the name of the value on the commandline. - const std::regex enum_value_pattern( - std::string(shared_prefix) + R"(([\S]+)(?:\n|$))"); - // A void pointer outputs it type first, followed by the memory address it - // is pointing to. This pattern should extract the address. - const std::regex void_pointer_pattern( - std::string(shared_prefix) + R"((?:[\S\s]+)\s()" + memory_address + ")"); + PRECONDITION(gdb_state == gdb_statet::STOPPED); + + std::string mem; + + // regex matching a hex memory address followed by an optional identifier in + // angle brackets (e.g., `0x601060 `) + std::regex regex(R"(^(0x[1-9a-f][0-9a-f]*)( <.*>)?)"); + + const std::string value = eval_expr(expr); std::smatch result; - if(regex_search(line, result, char_value_pattern)) - { - return result[1]; - } - if(regex_search(line, result, value_pattern)) + if(regex_match(value, result, regex)) { + // return hex address only return result[1]; } - if(regex_search(line, result, enum_value_pattern)) + else { - return result[1]; + throw gdb_interaction_exceptiont( + "value `" + value + + "` is not a memory address or has unrecognised format"); } - if(regex_search(line, result, void_pointer_pattern)) + + // not reached + return ""; +} + +/// 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 gdb_apit::get_value(const std::string &expr) +{ + PRECONDITION(gdb_state == gdb_statet::STOPPED); + + const std::string value = eval_expr(expr); + { - return result[1]; + // get string from char pointer + const std::regex regex(R"(0x[1-9a-f][0-9a-f]* \\"(.*)\\")"); + + std::smatch result; + if(regex_match(value, result, regex)) + { + return result[1]; + } } - std::regex memmory_access_error("Cannot access memory"); - if(regex_search(line, memmory_access_error)) + + // this case will go away eventually, once client code has been refactored to + // use get_memory() instead { - throw gdb_inaccessible_memory_exceptiont("ERROR: " + line); + // get void pointer address + const std::regex regex(R"(0x[1-9a-f][0-9a-f]*)"); + + std::smatch result; + if(regex_match(value, result, regex)) + { + return result[1]; + } } - throw gdb_interaction_exceptiont("Cannot extract value from this: " + line); + + // return raw value + return value; } gdb_apit::gdb_output_recordt diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 55740320cfc..ac8372ecd26 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -7,6 +7,14 @@ Author: Malte Mues \*******************************************************************/ +/// \file +/// Low-level interface to gdb +/// +/// This provides an API to run a program under gdb up to some +/// breakpoint, and then query the values of expressions. It uses the +/// gdb machine interface (see section "The GDB/MI Interface" in the +/// gdb manual to communicate with gdb. + #ifdef __linux__ #ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H #define CPROVER_MEMORY_ANALYZER_GDB_API_H @@ -19,35 +27,53 @@ Author: Malte Mues class gdb_apit { public: - explicit gdb_apit(const char *binary); + explicit gdb_apit(const char *binary, const bool log = false); - int create_gdb_process(); + void create_gdb_process(); void terminate_gdb_process(); - void run_gdb_to_breakpoint(const std::string &breakpoint); + bool run_gdb_to_breakpoint(const std::string &breakpoint); void run_gdb_from_core(const std::string &corefile); - std::string get_value(const std::string &variable); - std::string get_memory(const std::string &variable); + std::string get_value(const std::string &expr); + std::string get_memory(const std::string &expr); + + const std::vector &get_command_log(); + +protected: + const char *binary; -private: - const char *binary_name; FILE *input_stream; FILE *output_stream; - static std::string create_command(const std::string &variable); + const bool log; + std::vector command_log; + + enum class gdb_statet + { + NOT_CREATED, + CREATED, + STOPPED + }; + + gdb_statet gdb_state; + + typedef std::map gdb_output_recordt; + static gdb_output_recordt parse_gdb_output_record(const std::string &s); + void write_to_gdb(const std::string &command); std::string read_next_line(); + std::string read_most_recent_line(); - static bool check_for_gdb_breakpoint_error(const std::string &line); - static bool check_for_gdb_core_error(const std::string &line); + std::string eval_expr(const std::string &expr); - static std::string extract_value(const std::string &line); - static std::string extract_memory(const std::string &line); + gdb_output_recordt + get_most_recent_record(const std::string &tag, const bool must_exist = false); - typedef std::map gdb_output_recordt; - static gdb_output_recordt parse_gdb_output_record(const std::string &s); + static bool has_tag(const std::string &tag, const std::string &line); + + bool most_recent_line_has_tag(const std::string &tag); }; class gdb_interaction_exceptiont : public cprover_exception_baset From 58f6d116d98c02a118f5481ae22bed00ee805b04 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 28 Jan 2019 16:07:21 +0000 Subject: [PATCH 09/17] Remove unused gdb_inaccessible_memory_exceptiont --- src/memory-analyzer/gdb_api.h | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index ac8372ecd26..f45ba0d63ff 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -91,21 +91,5 @@ class gdb_interaction_exceptiont : public cprover_exception_baset std::string reason; }; -class gdb_inaccessible_memory_exceptiont : public cprover_exception_baset -{ -public: - explicit gdb_inaccessible_memory_exceptiont(std::string reason) - : reason(reason) - { - } - - std::string what() const override - { - return reason; - } - -private: - std::string reason; -}; #endif // CPROVER_MEMORY_ANALYZER_GDB_API_H #endif // __linux__ From 5c518e70ac8d85be77bfb6b1d29a038b6c2927a8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 28 Jan 2019 19:04:37 +0000 Subject: [PATCH 10/17] Add empty lines in gdb_api.cpp to improve readability --- src/memory-analyzer/gdb_api.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index f344ed55110..450af45f42d 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -18,6 +18,7 @@ Author: Malte Mues #include #include "gdb_api.h" + #include #include @@ -48,25 +49,31 @@ void gdb_apit::create_gdb_process() { throw gdb_interaction_exceptiont("could not create pipe for stdin"); } + if(pipe(pipe_output) == -1) { throw gdb_interaction_exceptiont("could not create pipe for stdout"); } gdb_process = fork(); + if(gdb_process == -1) { throw gdb_interaction_exceptiont("could not create gdb process"); } + if(gdb_process == 0) { // child process close(pipe_input[1]); close(pipe_output[0]); + dup2(pipe_input[0], STDIN_FILENO); dup2(pipe_output[1], STDOUT_FILENO); dup2(pipe_output[1], STDERR_FILENO); + dprintf(pipe_output[1], "binary name: %s\n", binary); + char *arg[] = {const_cast("gdb"), const_cast("--interpreter=mi"), const_cast(binary), From b72245b45df97ee143fdebebda759ac4b10a7712 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 29 Jan 2019 13:35:44 +0000 Subject: [PATCH 11/17] Install gdb package in CI to make gdb_apit unit tests work --- .travis.yml | 6 ++++++ buildspec.yml | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index ffbfb288b96..cae92bf0bfa 100644 --- a/.travis.yml +++ b/.travis.yml @@ -99,6 +99,7 @@ jobs: - libubsan0 - parallel - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -134,6 +135,7 @@ jobs: - g++-5 - libubsan0 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -162,6 +164,7 @@ jobs: - libstdc++-5-dev - libubsan0 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -189,6 +192,7 @@ jobs: packages: - g++-7 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-7 bin/gcc @@ -216,6 +220,7 @@ jobs: packages: - g++-7 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-7 bin/gcc @@ -249,6 +254,7 @@ jobs: - libubsan0 - parallel - jq + - gdb before_install: - mkdir bin # Use gcc/g++ 5 for tests, as Clang doesn't work yet diff --git a/buildspec.yml b/buildspec.yml index 975e3eea7a7..6394753b0e7 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -8,7 +8,7 @@ phases: - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F - add-apt-repository ppa:openjdk-r/ppa -y - apt-get update -y - - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq + - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb - apt-get install -y openjdk-8-jdk - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1 From 0e1a5ca35da8f342fa2335f783624f751d336bd6 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 29 Jan 2019 15:33:53 +0000 Subject: [PATCH 12/17] Add file module_dependencies.txt to memory-analyzer --- src/memory-analyzer/module_dependencies.txt | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 src/memory-analyzer/module_dependencies.txt diff --git a/src/memory-analyzer/module_dependencies.txt b/src/memory-analyzer/module_dependencies.txt new file mode 100644 index 00000000000..a7a95a1321a --- /dev/null +++ b/src/memory-analyzer/module_dependencies.txt @@ -0,0 +1,2 @@ +goto-programs +util From 7e6bd17018a82ce8fb8d5a891775088a3722a800 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 4 Feb 2019 17:03:54 +0000 Subject: [PATCH 13/17] Replace #ifdef __linux__ by guards allowing more Unices We require the Unix fork() system call (in unistd.h) --- src/memory-analyzer/gdb_api.cpp | 10 +++++++++- src/memory-analyzer/gdb_api.h | 12 ++++++++++-- unit/memory-analyzer/gdb_api.cpp | 20 +++++++++++++++++--- 3 files changed, 36 insertions(+), 6 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index 450af45f42d..deb497989c3 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -10,7 +10,15 @@ Author: Malte Mues /// \file /// Low-level interface to gdb -#ifdef __linux__ +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +// clang-format on + #include #include #include diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index f45ba0d63ff..ab9be8b8d4e 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -15,7 +15,15 @@ Author: Malte Mues /// gdb machine interface (see section "The GDB/MI Interface" in the /// gdb manual to communicate with gdb. -#ifdef __linux__ +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +// clang-format on + #ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H #define CPROVER_MEMORY_ANALYZER_GDB_API_H #include @@ -92,4 +100,4 @@ class gdb_interaction_exceptiont : public cprover_exception_baset }; #endif // CPROVER_MEMORY_ANALYZER_GDB_API_H -#endif // __linux__ +#endif diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index 67e808ac889..bbf56498e6e 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -9,9 +9,23 @@ Author: Malte Mues #include -#ifdef __linux__ -// \file Test that the regex expression used work as expected. -#define private public +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +// clang-format on + +#include +#include +#include +#include + +#include +#include + #include #include From aece5a5644c9c8e82b5574947e71aecb02abadfa Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 15:28:16 +0000 Subject: [PATCH 14/17] Enable and update gdb api unit tests This enables the gdb api unit tests (in memory-analyzer/gdb_api.cpp) and adapts them to include use_catch.h instead of catch.hpp. --- unit/Makefile | 1 + unit/memory-analyzer/module_dependencies.txt | 2 ++ unit/module_dependencies.txt | 1 + 3 files changed, 4 insertions(+) create mode 100644 unit/memory-analyzer/module_dependencies.txt diff --git a/unit/Makefile b/unit/Makefile index 8b3f5343b1d..c93aa6fc932 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -32,6 +32,7 @@ SRC += analyses/ai/ai.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ json_symbol_table.cpp \ + memory-analyzer/gdb_api.cpp \ path_strategies.cpp \ pointer-analysis/value_set.cpp \ solvers/bdd/miniBDD/miniBDD.cpp \ diff --git a/unit/memory-analyzer/module_dependencies.txt b/unit/memory-analyzer/module_dependencies.txt new file mode 100644 index 00000000000..aa1bc7f84f8 --- /dev/null +++ b/unit/memory-analyzer/module_dependencies.txt @@ -0,0 +1,2 @@ +memory-analyzer +testing-utils diff --git a/unit/module_dependencies.txt b/unit/module_dependencies.txt index 65410cabc47..ffb35402365 100644 --- a/unit/module_dependencies.txt +++ b/unit/module_dependencies.txt @@ -7,6 +7,7 @@ goto-programs goto-symex json langapi # should go away +memory-analyzer solvers/flattening solvers/floatbv solvers/miniBDD From fcbe7b933b064da9734e2fa8401e9bf4881221fb Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 24 Jan 2019 17:49:47 +0000 Subject: [PATCH 15/17] Add new unit tests for the gdb api This adds new unit tests for gdb_apit. The tests compile a test file test.c and then run gdb on it (via gdb_apit). --- unit/memory-analyzer/gdb_api.cpp | 310 +++++++++++++------------------ unit/memory-analyzer/input.txt | 3 + unit/memory-analyzer/test.c | 27 +++ 3 files changed, 160 insertions(+), 180 deletions(-) create mode 100644 unit/memory-analyzer/input.txt create mode 100644 unit/memory-analyzer/test.c diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index bbf56498e6e..6889eb84cf5 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -16,8 +16,12 @@ Author: Malte Mues defined(__unix__) || \ defined(__CYGWIN__) || \ defined(__MACH__) +#define RUN_GDB_API_TESTS +#endif // clang-format on +#ifdef RUN_GDB_API_TESTS + #include #include #include @@ -27,232 +31,178 @@ Author: Malte Mues #include #include -#include -SCENARIO( - "gdb_apit uses regex as expected for memory", - "[core][memory-analyzer]") +void compile_test_file() { - gdb_apit gdb_api(""); - GIVEN("The result of a struct pointer") - { - const std::string line = "$2 = (struct cycle_buffer *) 0x601050 "; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x601050"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x601050"); - } - } + std::string test_file("memory-analyzer/test.c"); - GIVEN("The result of a typedef pointer") - { - const std::string line = "$4 = (cycle_buffer_entry_t *) 0x602010"; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x602010"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x602010"); - } - } + std::string cmd("gcc -g -o test "); + cmd += test_file; - GIVEN("The result of a char pointer") - { - const std::string line = "$5 = 0x400734 \"snow\""; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x400734"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x400734"); - } - } + const int r = system(cmd.c_str()); + REQUIRE(!r); +} - GIVEN("The result of a null pointer") +class gdb_api_testt : public gdb_apit +{ + explicit gdb_api_testt(const char *binary) : gdb_apit(binary) { - const std::string line = "$2 = 0x0"; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x0"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x0"); - } } - GIVEN("The result of a char pointer at very low address") - { - const std::string line = "$34 = 0x007456 \"snow\""; - THEN("the result matches the memory address and not nullpointer") - { - REQUIRE(gdb_api.extract_memory(line) == "0x007456"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x007456"); - } - } + friend void gdb_api_internals_test(); +}; - GIVEN("The result of a char pointer with some more whitespaces") - { - const std::string line = "$12 = 0x400752 \"thunder storm\"\n"; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x400752"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x400752"); - } - } +void gdb_api_internals_test() +{ + compile_test_file(); - GIVEN("The result of an array pointer") + SECTION("parse gdb output record") { - const std::string line = "$5 = (struct a_sub_type_t (*)[4]) 0x602080"; - THEN("the result matches the memory address in the output") - { - REQUIRE(gdb_api.extract_memory(line) == "0x602080"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x602080"); - } - } + gdb_api_testt gdb_api("test"); - GIVEN("A constant struct pointer pointing to 0x0") - { - const std::string line = "$3 = (const struct name *) 0x0"; - THEN("the returned memory address should be 0x0") - { - REQUIRE(gdb_api.extract_memory(line) == "0x0"); - } - } + gdb_api_testt::gdb_output_recordt gor; - GIVEN("An enum address") - { - const std::string line = "$2 = (char *(*)[5]) 0x7e5500 "; - THEN("the returned address is the address of the enum") - { - REQUIRE(gdb_api.extract_memory(line) == "0x7e5500"); - } + gor = gdb_api.parse_gdb_output_record( + "a = \"1\", b = \"2\", c = {1, 2}, d = [3, 4], e=\"0x0\""); + + REQUIRE(gor["a"] == "1"); + REQUIRE(gor["b"] == "2"); + REQUIRE(gor["c"] == "{1, 2}"); + REQUIRE(gor["d"] == "[3, 4]"); + REQUIRE(gor["e"] == "0x0"); } - GIVEN("The result of an int pointer") + SECTION("read a line from an input stream") { - const std::string line = "$1 = (int *) 0x601088 \n"; - THEN("the result is the value of memory address of the int pointer") - { - REQUIRE(gdb_api.extract_memory(line) == "0x601088"); - } - THEN("adding '(gdb) ' to the line doesn't have an influence") - { - REQUIRE(gdb_api.extract_memory("(gdb) " + line) == "0x601088"); - } + gdb_api_testt gdb_api("test"); + + FILE *f = fopen("memory-analyzer/input.txt", "r"); + gdb_api.input_stream = f; + + std::string line; + + line = gdb_api.read_next_line(); + REQUIRE(line == "abc\n"); + + line = gdb_api.read_next_line(); + REQUIRE(line == std::string(1120, 'a') + "\n"); + + line = gdb_api.read_next_line(); + REQUIRE(line == "xyz"); } - GIVEN("Non matching result") + SECTION("start and exit gdb") { - const std::string line = "Something that must not match 0x605940"; - THEN("an exception is thrown") - { - REQUIRE_THROWS_AS( - gdb_api.extract_memory(line), gdb_interaction_exceptiont); - } + gdb_api_testt gdb_api("test"); + + gdb_api.create_gdb_process(); + + // check input and output streams + REQUIRE(!ferror(gdb_api.input_stream)); + REQUIRE(!ferror(gdb_api.output_stream)); + + gdb_api.terminate_gdb_process(); } } -SCENARIO( - "gdb_apit uses regex as expected for value extraction", - "[core][memory-analyzer]") +#endif + +TEST_CASE("gdb api internals test", "[core][memory-analyzer]") { - gdb_apit gdb_api(""); - GIVEN("An integer value") - { - const std::string line = "$90 = 100"; - THEN("the result schould be '100'") - { - REQUIRE(gdb_api.extract_value(line) == "100"); - } - } +#ifdef RUN_GDB_API_TESTS + gdb_api_internals_test(); +#endif +} - GIVEN("A string value") - { - const std::string line = "$5 = 0x602010 \"snow\""; - THEN("the result should be 'snow'") - { - REQUIRE(gdb_api.extract_value(line) == "snow"); - } - } +TEST_CASE("gdb api test", "[core][memory-analyzer]") +{ +#ifdef RUN_GDB_API_TESTS + compile_test_file(); - GIVEN("A string with withe spaces") { - const std::string line = "$1323 = 0x1243253 \"thunder storm\"\n"; - THEN("the result should be 'thunder storm'") + gdb_apit gdb_api("test", true); + gdb_api.create_gdb_process(); + + try { - REQUIRE(gdb_api.extract_value(line) == "thunder storm"); - } - } + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); - GIVEN("A byte value") - { - const std::string line = "$2 = 243 '\363'"; - THEN("the result should be 243") + gdb_api.terminate_gdb_process(); + } + catch(const gdb_interaction_exceptiont &e) { - REQUIRE(gdb_api.extract_value(line) == "243"); + std::cerr << "warning: cannot fully unit test GDB API as program cannot " + << "be run with gdb\n"; + std::cerr << "warning: this may be due to not having the required " + << "permissions (e.g., to invoke ptrace() or to disable ASLR)" + << "\n"; + std::cerr << "gdb_interaction_exceptiont:" << '\n'; + std::cerr << e.what() << '\n'; + + std::ifstream file("gdb.txt"); + CHECK_RETURN(file.is_open()); + std::string line; + + std::cerr << "=== gdb log begin ===\n"; + + while(getline(file, line)) + { + std::cerr << line << '\n'; + } + + file.close(); + + std::cerr << "=== gdb log end ===\n"; + + gdb_api.terminate_gdb_process(); + + return; } } - GIVEN("A negative int value") + gdb_apit gdb_api("test"); + gdb_api.create_gdb_process(); + + SECTION("breakpoint is hit") { - const std::string line = "$8 = -32"; - THEN("the result should be -32") - { - REQUIRE(gdb_api.extract_value(line) == "-32"); - } + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); } - GIVEN("An enum value") + SECTION("breakpoint is not hit") { - const std::string line = "$1 = INFO"; - THEN("the result should be INFO") - { - REQUIRE(gdb_api.extract_value(line) == "INFO"); - } + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint2"); + REQUIRE(!r); } - GIVEN("A void pointer value") + SECTION("breakpoint does not exist") { - const std::string line = "$6 = (const void *) 0x71"; - THEN("the requried result should be 0x71") - { - REQUIRE(gdb_api.extract_value(line) == "0x71"); - } + REQUIRE_THROWS_AS( + gdb_api.run_gdb_to_breakpoint("checkpoint3"), gdb_interaction_exceptiont); } - GIVEN("A gdb response that contains 'cannot access memory'") + SECTION("query memory") { - const std::string line = "Cannot access memory at address 0x71"; - THEN("a gdb_inaccesible_memoryt excepition must be raised") + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); + + REQUIRE(gdb_api.get_value("x") == "8"); + REQUIRE(gdb_api.get_value("s") == "abc"); + + const std::regex regex(R"(0x[1-9a-f][0-9a-f]*)"); + { - REQUIRE_THROWS_AS( - gdb_api.extract_value(line), gdb_inaccessible_memory_exceptiont); + std::string address = gdb_api.get_memory("p"); + REQUIRE(std::regex_match(address, regex)); } - } - GIVEN("A value that must not match") - { - const std::string line = "$90 = must not match 20"; - THEN("an exception is raised") { - REQUIRE_THROWS_AS( - gdb_api.extract_value(line), gdb_interaction_exceptiont); + std::string address = gdb_api.get_memory("vp"); + REQUIRE(std::regex_match(address, regex)); } } -} + + gdb_api.terminate_gdb_process(); #endif +} diff --git a/unit/memory-analyzer/input.txt b/unit/memory-analyzer/input.txt new file mode 100644 index 00000000000..5d3bfc24a58 --- /dev/null +++ b/unit/memory-analyzer/input.txt @@ -0,0 +1,3 @@ +abc +aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa +xyz \ No newline at end of file diff --git a/unit/memory-analyzer/test.c b/unit/memory-analyzer/test.c new file mode 100644 index 00000000000..8c23338cddb --- /dev/null +++ b/unit/memory-analyzer/test.c @@ -0,0 +1,27 @@ +int x; +char *s = "abc"; +int *p; +void *vp; + +void checkpoint() +{ +} +void checkpoint2() +{ +} + +void func() +{ + checkpoint2(); +} + +int main() +{ + x = 8; + p = &x; + vp = (void *)&x; + + checkpoint(); + + return 0; +} From fa2ed7b3a8d5325a6194666a30dcd8ea8a8ba5c2 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 11 Feb 2019 17:11:46 +0000 Subject: [PATCH 16/17] Install gdb on macos builds --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index cae92bf0bfa..2957786e6cd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -116,7 +116,7 @@ jobs: compiler: clang cache: ccache before_install: - - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel + - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel gdb - export PATH=$PATH:/usr/local/opt/ccache/libexec env: COMPILER="ccache clang++" @@ -276,7 +276,7 @@ jobs: compiler: clang cache: ccache before_install: - - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache + - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache gdb - export PATH=$PATH:/usr/local/opt/ccache/libexec env: - BUILD_SYSTEM=cmake From d803bde3c950425c1e322526f7c00e235a19da55 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Wed, 13 Mar 2019 11:01:48 +0000 Subject: [PATCH 17/17] Fix based on comments --- src/memory-analyzer/gdb_api.cpp | 122 +++++++++++--------- src/memory-analyzer/gdb_api.h | 18 +-- src/memory-analyzer/module_dependencies.txt | 1 + unit/memory-analyzer/gdb_api.cpp | 21 +--- 4 files changed, 84 insertions(+), 78 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index deb497989c3..4a1e452f2df 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -29,8 +29,11 @@ Author: Malte Mues #include +#include #include +#include + /// Create a gdb_apit object /// /// \param binary the binary to run with gdb @@ -40,6 +43,31 @@ gdb_apit::gdb_apit(const char *binary, const bool log) { } +/// Terminate the gdb process and close open streams (for reading from and +/// writing to gdb) +gdb_apit::~gdb_apit() +{ + PRECONDITION( + gdb_state == gdb_statet::CREATED || gdb_state == gdb_statet::STOPPED || + gdb_state == gdb_statet::NOT_CREATED); + + if(gdb_state == gdb_statet::NOT_CREATED) + return; + + write_to_gdb("-gdb-exit"); + // we cannot use most_recent_line_has_tag() here as it checks the last line + // before the next `(gdb) \n` prompt in the output; however when gdb exits no + // next prompt is printed + CHECK_RETURN(has_prefix(read_next_line(), "^exit")); + + gdb_state = gdb_statet::NOT_CREATED; + + fclose(command_stream); + fclose(response_stream); + + wait(NULL); +} + /// Create a new gdb process for analysing the binary indicated by the member /// variable `binary` void gdb_apit::create_gdb_process() @@ -82,10 +110,10 @@ void gdb_apit::create_gdb_process() dprintf(pipe_output[1], "binary name: %s\n", binary); - char *arg[] = {const_cast("gdb"), - const_cast("--interpreter=mi"), - const_cast(binary), - NULL}; + char *const arg[] = {const_cast("gdb"), + const_cast("--interpreter=mi"), + const_cast(binary), + NULL}; dprintf(pipe_output[1], "Loading gdb...\n"); execvp("gdb", arg); @@ -103,68 +131,50 @@ void gdb_apit::create_gdb_process() close(pipe_output[1]); // get stream for reading the gdb output - input_stream = fdopen(pipe_output[0], "r"); + response_stream = fdopen(pipe_output[0], "r"); // get stream for writing to gdb - output_stream = fdopen(pipe_input[1], "w"); + command_stream = fdopen(pipe_input[1], "w"); - CHECK_RETURN(most_recent_line_has_tag(R"(~"done)")); + bool has_done_tag = most_recent_line_has_tag(R"(~"done)"); + CHECK_RETURN(has_done_tag); if(log) { // logs output to `gdb.txt` in the current directory, input is not logged // hence we log it to `command_log` write_to_gdb("-gdb-set logging on"); - CHECK_RETURN(most_recent_line_has_tag("^done")); + check_command_accepted(); } write_to_gdb("-gdb-set max-value-size unlimited"); - CHECK_RETURN(most_recent_line_has_tag("^done")); + check_command_accepted(); } } -/// Terminate the gdb process and close open streams (for reading from and -/// writing to gdb) -void gdb_apit::terminate_gdb_process() -{ - PRECONDITION( - gdb_state == gdb_statet::CREATED || gdb_state == gdb_statet::STOPPED); - - write_to_gdb("-gdb-exit"); - // we cannot use most_recent_line_has_tag() here as it checks the last line - // before the next `(gdb) \n` prompt in the output; however when gdb exits no - // next prompt is printed - CHECK_RETURN(has_tag("^exit", read_next_line())); - - gdb_state = gdb_statet::NOT_CREATED; - - fclose(output_stream); - fclose(input_stream); -} - void gdb_apit::write_to_gdb(const std::string &command) { PRECONDITION(!command.empty()); - PRECONDITION(command.back() != '\n'); + PRECONDITION(command.find('\n') == std::string::npos); std::string line(command); line += '\n'; if(log) { - command_log.push_back(command); + command_log.push_front(command); } - if(fputs(line.c_str(), output_stream) == EOF) + if(fputs(line.c_str(), command_stream) == EOF) { throw gdb_interaction_exceptiont("could not write a command to gdb"); } - fflush(output_stream); + fflush(command_stream); } /// Return the vector of commands that have been written to gdb so far -const std::vector &gdb_apit::get_command_log() +const gdb_apit::commandst &gdb_apit::get_command_log() { PRECONDITION(log); return command_log; @@ -179,17 +189,17 @@ std::string gdb_apit::read_next_line() const size_t buf_size = 1024; char buf[buf_size]; // NOLINT(runtime/arrays) - const char *c = fgets(buf, buf_size, input_stream); + const char *c = fgets(buf, buf_size, response_stream); if(c == NULL) { - if(ferror(input_stream)) + if(ferror(response_stream)) { throw gdb_interaction_exceptiont("error reading from gdb"); } INVARIANT( - feof(input_stream), + feof(response_stream), "EOF must have been reached when the error indicator on the stream " "is not set and fgets returned NULL"); INVARIANT( @@ -227,7 +237,7 @@ gdb_apit::gdb_output_recordt gdb_apit::get_most_recent_record(const std::string &tag, const bool must_exist) { std::string line = read_most_recent_line(); - const bool b = has_tag(tag, line); + const bool b = has_prefix(line, tag); if(must_exist) { @@ -243,15 +253,10 @@ gdb_apit::get_most_recent_record(const std::string &tag, const bool must_exist) return parse_gdb_output_record(record); } -bool gdb_apit::has_tag(const std::string &tag, const std::string &line) -{ - return line.compare(0, tag.length(), tag) == 0; -} - bool gdb_apit::most_recent_line_has_tag(const std::string &tag) { const std::string line = read_most_recent_line(); - return has_tag(tag, line); + return has_prefix(line, tag); } /// Run gdb with the given core file @@ -265,7 +270,7 @@ void gdb_apit::run_gdb_from_core(const std::string &corefile) const std::string command = "core " + corefile; write_to_gdb(command); - CHECK_RETURN(most_recent_line_has_tag("^done")); + check_command_accepted(); gdb_state = gdb_statet::STOPPED; } @@ -282,7 +287,7 @@ bool gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) command += " " + breakpoint; write_to_gdb(command); - if(!most_recent_line_has_tag("^done")) + if(!was_command_accepted()) { throw gdb_interaction_exceptiont("could not set breakpoint"); } @@ -315,27 +320,24 @@ bool gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) "gdb stopped for unhandled reason `" + reason + "`"); } - // not reached - return true; + UNREACHABLE; } std::string gdb_apit::eval_expr(const std::string &expr) { write_to_gdb("-var-create tmp * " + expr); - if(!most_recent_line_has_tag("^done")) + if(!was_command_accepted()) { throw gdb_interaction_exceptiont( - "could not create variable for " - "expression `" + - expr + "`"); + "could not create variable for expression `" + expr + "`"); } write_to_gdb("-var-evaluate-expression tmp"); gdb_output_recordt record = get_most_recent_record("^done", true); write_to_gdb("-var-delete tmp"); - CHECK_RETURN(most_recent_line_has_tag("^done")); + check_command_accepted(); const auto it = record.find("value"); CHECK_RETURN(it != record.end()); @@ -381,8 +383,7 @@ std::string gdb_apit::get_memory(const std::string &expr) "` is not a memory address or has unrecognised format"); } - // not reached - return ""; + UNREACHABLE; } /// Get value of the given value expression @@ -432,7 +433,7 @@ gdb_apit::parse_gdb_output_record(const std::string &s) gdb_output_recordt result; - unsigned depth = 0; + std::size_t depth = 0; std::string::size_type start = 0; const std::string::size_type n = s.length(); @@ -488,4 +489,15 @@ gdb_apit::parse_gdb_output_record(const std::string &s) return result; } +bool gdb_apit::was_command_accepted() +{ + return most_recent_line_has_tag("^done"); +} + +void gdb_apit::check_command_accepted() +{ + bool was_accepted = was_command_accepted(); + CHECK_RETURN(was_accepted); +} + #endif diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index ab9be8b8d4e..92c73df2234 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -29,13 +29,17 @@ Author: Malte Mues #include #include +#include #include class gdb_apit { public: + using commandst = std::forward_list; + explicit gdb_apit(const char *binary, const bool log = false); + ~gdb_apit(); void create_gdb_process(); void terminate_gdb_process(); @@ -46,22 +50,22 @@ class gdb_apit std::string get_value(const std::string &expr); std::string get_memory(const std::string &expr); - const std::vector &get_command_log(); + const commandst &get_command_log(); protected: const char *binary; - FILE *input_stream; - FILE *output_stream; + FILE *response_stream; + FILE *command_stream; const bool log; - std::vector command_log; + commandst command_log; enum class gdb_statet { NOT_CREATED, CREATED, - STOPPED + STOPPED // valid state, reached e.g. after breakpoint was hit }; gdb_statet gdb_state; @@ -79,9 +83,9 @@ class gdb_apit gdb_output_recordt get_most_recent_record(const std::string &tag, const bool must_exist = false); - static bool has_tag(const std::string &tag, const std::string &line); - bool most_recent_line_has_tag(const std::string &tag); + bool was_command_accepted(); + void check_command_accepted(); }; class gdb_interaction_exceptiont : public cprover_exception_baset diff --git a/src/memory-analyzer/module_dependencies.txt b/src/memory-analyzer/module_dependencies.txt index a7a95a1321a..5e3f81fdcc7 100644 --- a/src/memory-analyzer/module_dependencies.txt +++ b/src/memory-analyzer/module_dependencies.txt @@ -1,2 +1,3 @@ goto-programs util +sys diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index 6889eb84cf5..fb4ef130549 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -60,9 +60,7 @@ void gdb_api_internals_test() { gdb_api_testt gdb_api("test"); - gdb_api_testt::gdb_output_recordt gor; - - gor = gdb_api.parse_gdb_output_record( + gdb_api_testt::gdb_output_recordt gor = gdb_api.parse_gdb_output_record( "a = \"1\", b = \"2\", c = {1, 2}, d = [3, 4], e=\"0x0\""); REQUIRE(gor["a"] == "1"); @@ -77,11 +75,9 @@ void gdb_api_internals_test() gdb_api_testt gdb_api("test"); FILE *f = fopen("memory-analyzer/input.txt", "r"); - gdb_api.input_stream = f; - - std::string line; + gdb_api.response_stream = f; - line = gdb_api.read_next_line(); + std::string line = gdb_api.read_next_line(); REQUIRE(line == "abc\n"); line = gdb_api.read_next_line(); @@ -98,10 +94,8 @@ void gdb_api_internals_test() gdb_api.create_gdb_process(); // check input and output streams - REQUIRE(!ferror(gdb_api.input_stream)); - REQUIRE(!ferror(gdb_api.output_stream)); - - gdb_api.terminate_gdb_process(); + REQUIRE(!ferror(gdb_api.response_stream)); + REQUIRE(!ferror(gdb_api.command_stream)); } } @@ -127,8 +121,6 @@ TEST_CASE("gdb api test", "[core][memory-analyzer]") { const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); REQUIRE(r); - - gdb_api.terminate_gdb_process(); } catch(const gdb_interaction_exceptiont &e) { @@ -155,8 +147,6 @@ TEST_CASE("gdb api test", "[core][memory-analyzer]") std::cerr << "=== gdb log end ===\n"; - gdb_api.terminate_gdb_process(); - return; } } @@ -203,6 +193,5 @@ TEST_CASE("gdb api test", "[core][memory-analyzer]") } } - gdb_api.terminate_gdb_process(); #endif }