Skip to content

Commit 4db96d4

Browse files
mmueslydanpoe
authored andcommitted
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.
1 parent 5745139 commit 4db96d4

File tree

3 files changed

+577
-0
lines changed

3 files changed

+577
-0
lines changed

src/memory-analyzer/gdb_api.cpp

Lines changed: 266 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,266 @@
1+
// Copyright 2018 Author: Malte Mues <[email protected]>
2+
#ifdef __linux__
3+
#include <cctype>
4+
#include <cerrno>
5+
#include <cstdio>
6+
#include <cstring>
7+
#include <regex>
8+
9+
#include "gdb_api.h"
10+
#include <goto-programs/goto_model.h>
11+
12+
gdb_apit::gdb_apit(const char *arg)
13+
: binary_name(arg), buffer_position(0), last_read_size(0)
14+
{
15+
memset(buffer, 0, MAX_READ_SIZE_GDB_BUFFER);
16+
}
17+
18+
int gdb_apit::create_gdb_process()
19+
{
20+
if(pipe(pipe_input) == -1)
21+
{
22+
throw gdb_interaction_exceptiont("could not create pipe for stdin!");
23+
}
24+
if(pipe(pipe_output) == -1)
25+
{
26+
throw gdb_interaction_exceptiont("could not create pipe for stdout!");
27+
}
28+
29+
gdb_process = fork();
30+
if(gdb_process == -1)
31+
{
32+
throw gdb_interaction_exceptiont("could not create gdb process.");
33+
}
34+
if(gdb_process == 0)
35+
{
36+
// child process
37+
close(pipe_input[1]);
38+
close(pipe_output[0]);
39+
dup2(pipe_input[0], STDIN_FILENO);
40+
dup2(pipe_output[1], STDOUT_FILENO);
41+
dup2(pipe_output[1], STDERR_FILENO);
42+
dprintf(pipe_output[1], "binary name: %s\n", binary_name);
43+
char *arg[] = {
44+
const_cast<char *>("gdb"), const_cast<char *>(binary_name), NULL};
45+
46+
dprintf(pipe_output[1], "Loading gdb...\n");
47+
execvp("gdb", arg);
48+
49+
// Only reachable, if execvp failed
50+
int errno_value = errno;
51+
dprintf(pipe_output[1], "errno in child: %s\n", strerror(errno_value));
52+
}
53+
else
54+
{
55+
// parent process
56+
close(pipe_input[0]);
57+
close(pipe_output[1]);
58+
write_to_gdb("set max-value-size unlimited\n");
59+
}
60+
return 0;
61+
}
62+
63+
void gdb_apit::terminate_gdb_process()
64+
{
65+
close(pipe_input[0]);
66+
close(pipe_input[1]);
67+
}
68+
69+
void gdb_apit::write_to_gdb(const std::string &command)
70+
{
71+
if(
72+
write(pipe_input[1], command.c_str(), command.length()) !=
73+
(ssize_t)command.length())
74+
{
75+
throw gdb_interaction_exceptiont("Could not write a command to gdb");
76+
}
77+
}
78+
79+
std::string gdb_apit::read_next_line()
80+
{
81+
char token;
82+
std::string line;
83+
do
84+
{
85+
while(buffer_position >= last_read_size)
86+
{
87+
read_next_buffer_chunc();
88+
}
89+
token = buffer[buffer_position];
90+
line += token;
91+
++buffer_position;
92+
} while(token != '\n');
93+
return line;
94+
}
95+
96+
void gdb_apit::read_next_buffer_chunc()
97+
{
98+
memset(buffer, 0, last_read_size);
99+
const auto read_size =
100+
read(pipe_output[0], &buffer, MAX_READ_SIZE_GDB_BUFFER);
101+
if(read_size < 0)
102+
{
103+
throw gdb_interaction_exceptiont("Error reading from gdb_process");
104+
}
105+
last_read_size = read_size;
106+
buffer_position = 0;
107+
}
108+
109+
void gdb_apit::run_gdb_from_core(const std::string &corefile)
110+
{
111+
const std::string command = "core " + corefile + "\n";
112+
write_to_gdb(command);
113+
std::string line;
114+
while(!isdigit(line[0]))
115+
{
116+
line = read_next_line();
117+
if(check_for_gdb_core_error(line))
118+
{
119+
terminate_gdb_process();
120+
throw gdb_interaction_exceptiont(
121+
"This core file doesn't work with the binary.");
122+
}
123+
}
124+
}
125+
126+
bool gdb_apit::check_for_gdb_core_error(const std::string &line)
127+
{
128+
const std::regex core_init_error_r("exec file is newer than core");
129+
return regex_search(line, core_init_error_r);
130+
}
131+
132+
void gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint)
133+
{
134+
std::string command = "break " + breakpoint + "\n";
135+
write_to_gdb(command);
136+
command = "run\n";
137+
write_to_gdb(command);
138+
std::string line;
139+
while(!isdigit(line[0]))
140+
{
141+
line = read_next_line();
142+
if(check_for_gdb_breakpoint_error(line))
143+
{
144+
terminate_gdb_process();
145+
throw gdb_interaction_exceptiont("This is not a valid breakpoint\n");
146+
}
147+
}
148+
}
149+
150+
bool gdb_apit::check_for_gdb_breakpoint_error(const std::string &line)
151+
{
152+
const std::regex breakpoint_init_error_r("Make breakpoint pending on future");
153+
return regex_search(line, breakpoint_init_error_r);
154+
}
155+
156+
std::string gdb_apit::create_command(const std::string &variable)
157+
{
158+
return "p " + variable + "\n";
159+
}
160+
161+
std::string gdb_apit::get_memory(const std::string &variable)
162+
{
163+
write_to_gdb(create_command(variable));
164+
const std::string &response = read_next_line();
165+
return extract_memory(response);
166+
}
167+
168+
// All lines in the output start with something like
169+
// '$XX = ' where XX is a digit. => shared_prefix.
170+
const char shared_prefix[] = R"(\$[0-9]+\s=\s)";
171+
172+
// Matching a hex encoded address.
173+
const char memory_address[] = R"(0x[[:xdigit:]]+)";
174+
175+
std::string gdb_apit::extract_memory(const std::string &line)
176+
{
177+
// The next patterns matches the type information,
178+
// which be "(classifier struct name (*)[XX])"
179+
// for pointer to struct arrayes. classsifier and struct is optional => {1,3}
180+
// If it isn't an array, than the ending is " *)"
181+
// => or expression in pointer_star_or_array_suffix.
182+
const std::string struct_name = R"((?:\S+\s){1,3})";
183+
const std::string pointer_star_or_arary_suffix =
184+
R"((?:\*|(?:\*)?\(\*\)\[[0-9]+\])?)";
185+
const std::string pointer_type_info =
186+
R"(\()" + struct_name + pointer_star_or_arary_suffix + R"(\))";
187+
188+
// The pointer type info is followed by the memory value and eventually
189+
// extended by the name of the pointer content, if gdb has an explicit symbol.
190+
// See unit test cases for more examples of expected input.
191+
const std::regex pointer_pattern(
192+
std::string(shared_prefix) + pointer_type_info + R"(\s()" + memory_address +
193+
R"()(\s\S+)?)");
194+
const std::regex null_pointer_pattern(
195+
std::string(shared_prefix) + R"((0x0))");
196+
// Char pointer output the memory adress followed by the string in there.
197+
const std::regex char_pointer_pattern(
198+
std::string(shared_prefix) + R"(()" + memory_address +
199+
R"()\s"[\S[:s:]]*")");
200+
201+
std::smatch result;
202+
if(regex_search(line, result, char_pointer_pattern))
203+
{
204+
return result[1];
205+
}
206+
if(regex_search(line, result, pointer_pattern))
207+
{
208+
return result[1];
209+
}
210+
if(regex_search(line, result, null_pointer_pattern))
211+
{
212+
return result[1];
213+
}
214+
throw gdb_interaction_exceptiont("Cannot resolve memory_address: " + line);
215+
}
216+
217+
std::string gdb_apit::get_value(const std::string &variable)
218+
{
219+
write_to_gdb(create_command(variable));
220+
const std::string &response = read_next_line();
221+
return extract_value(response);
222+
}
223+
224+
std::string gdb_apit::extract_value(const std::string &line)
225+
{
226+
// This pattern matches primitive int values and bools.
227+
const std::regex value_pattern(
228+
std::string(shared_prefix) + R"(((?:-)?\d+|true|false))");
229+
// This pattern matches the char pointer content.
230+
// It is printed behind the address.
231+
const std::regex char_value_pattern(
232+
std::string(shared_prefix) + memory_address + "\\s\"([\\S ]*)\"");
233+
// An enum entry just prints the name of the value on the commandline.
234+
const std::regex enum_value_pattern(
235+
std::string(shared_prefix) + R"(([\S]+)(?:\n|$))");
236+
// A void pointer outputs it type first, followed by the memory address it
237+
// is pointing to. This pattern should extract the address.
238+
const std::regex void_pointer_pattern(
239+
std::string(shared_prefix) + R"((?:[\S\s]+)\s()" + memory_address + ")");
240+
241+
std::smatch result;
242+
if(regex_search(line, result, char_value_pattern))
243+
{
244+
return result[1];
245+
}
246+
if(regex_search(line, result, value_pattern))
247+
{
248+
return result[1];
249+
}
250+
if(regex_search(line, result, enum_value_pattern))
251+
{
252+
return result[1];
253+
}
254+
if(regex_search(line, result, void_pointer_pattern))
255+
{
256+
return result[1];
257+
}
258+
std::regex memmory_access_error("Cannot access memory");
259+
if(regex_search(line, memmory_access_error))
260+
{
261+
throw gdb_inaccessible_memoryt("ERROR: " + line);
262+
}
263+
throw gdb_interaction_exceptiont("Cannot extract value from this: " + line);
264+
}
265+
266+
#endif

src/memory-analyzer/gdb_api.h

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
// Copyright 2018 Author: Malte Mues
2+
#ifdef __linux__
3+
#ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H
4+
#define CPROVER_MEMORY_ANALYZER_GDB_API_H
5+
#include <unistd.h>
6+
7+
#include <exception>
8+
9+
class namespacet;
10+
class symbolt;
11+
class irept;
12+
13+
class gdb_apit
14+
{
15+
public:
16+
explicit gdb_apit(const char *binary);
17+
18+
int create_gdb_process();
19+
void terminate_gdb_process();
20+
21+
void run_gdb_to_breakpoint(const std::string &breakpoint);
22+
void run_gdb_from_core(const std::string &corefile);
23+
24+
std::string get_value(const std::string &variable);
25+
std::string get_memory(const std::string &variable);
26+
27+
private:
28+
static const int MAX_READ_SIZE_GDB_BUFFER = 600;
29+
30+
const char *binary_name;
31+
char buffer[MAX_READ_SIZE_GDB_BUFFER];
32+
int buffer_position;
33+
pid_t gdb_process;
34+
int last_read_size;
35+
int pipe_input[2];
36+
int pipe_output[2];
37+
38+
static std::string create_command(const std::string &variable);
39+
void write_to_gdb(const std::string &command);
40+
41+
std::string read_next_line();
42+
void read_next_buffer_chunc();
43+
44+
static bool check_for_gdb_breakpoint_error(const std::string &line);
45+
static bool check_for_gdb_core_error(const std::string &line);
46+
47+
static std::string extract_value(const std::string &line);
48+
static std::string extract_memory(const std::string &line);
49+
};
50+
51+
class gdb_interaction_exceptiont : public std::exception
52+
{
53+
public:
54+
explicit gdb_interaction_exceptiont(std::string reason) : std::exception()
55+
{
56+
error = reason;
57+
}
58+
const char *what() const throw()
59+
{
60+
return error.c_str();
61+
}
62+
63+
private:
64+
std::string error;
65+
};
66+
67+
class gdb_inaccessible_memoryt : public gdb_interaction_exceptiont
68+
{
69+
public:
70+
explicit gdb_inaccessible_memoryt(std::string reason)
71+
: gdb_interaction_exceptiont(reason)
72+
{
73+
}
74+
};
75+
#endif
76+
#endif

0 commit comments

Comments
 (0)