Fix based on comments
This commit is contained in:
Petr Bauch
Daniel Poetzl
parent
fa2ed7b3a8
commit
d803bde3c9
|
|
@ -29,8 +29,11 @@ Author: Malte Mues <mail.mues@gmail.com>
|
|||
|
||||
#include <goto-programs/goto_model.h>
|
||||
|
||||
#include <util/prefix.h>
|
||||
#include <util/string_utils.h>
|
||||
|
||||
#include <sys/wait.h>
|
||||
|
||||
/// 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<char *>("gdb"),
|
||||
const_cast<char *>("--interpreter=mi"),
|
||||
const_cast<char *>(binary),
|
||||
NULL};
|
||||
char *const arg[] = {const_cast<char *>("gdb"),
|
||||
const_cast<char *>("--interpreter=mi"),
|
||||
const_cast<char *>(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<std::string> &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
|
||||
|
|
|
|||
|
|
@ -29,13 +29,17 @@ Author: Malte Mues <mail.mues@gmail.com>
|
|||
#include <unistd.h>
|
||||
|
||||
#include <exception>
|
||||
#include <forward_list>
|
||||
|
||||
#include <util/exception_utils.h>
|
||||
|
||||
class gdb_apit
|
||||
{
|
||||
public:
|
||||
using commandst = std::forward_list<std::string>;
|
||||
|
||||
explicit gdb_apit(const char *binary, const bool log = false);
|
||||
~gdb_apit();
|
||||
|
||||
void create_gdb_process();
|
||||
void terminate_gdb_process();
|
||||
|
|
@ -46,22 +50,22 @@ public:
|
|||
std::string get_value(const std::string &expr);
|
||||
std::string get_memory(const std::string &expr);
|
||||
|
||||
const std::vector<std::string> &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<std::string> 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 @@ protected:
|
|||
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
|
||||
|
|
|
|||
|
|
@ -1,2 +1,3 @@
|
|||
goto-programs
|
||||
util
|
||||
sys
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
gdb_api.response_stream = f;
|
||||
|
||||
std::string line;
|
||||
|
||||
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
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue