GDB API [blocks: #4261] #3983

danpoe · 2019-01-28T19:11:17Z

This adds an API to run a program with gdb up to some breakpoint and then query the values of expressions. It is a partial rewrite of @mmuesly's gdb API (part of #2649). It now uses the gdb machine interface instead of the gdb user interface.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

martin-cs · 2019-01-28T21:20:48Z

+1 looking back at the original patch set, connecting using the remote protocol was one of the things I requested. Glad to hear this is moving again.

smowton

This sort of interactive child process management is prone to deadlock whenever gdb might start writing output (for example, an error message) before you're done writing input, and the pipe buffers are small enough that its write op blocks. Therefore usually you should use poll or similar to check for this circumstance and buffer any output it starts producing before your input command is complete.

smowton · 2019-01-29T09:24:11Z

src/memory-analyzer/gdb_api.cpp

+
+    dprintf(pipe_output[1], "binary name: %s\n", binary);
+
+    char *arg[] = {const_cast<char *>("gdb"),


? Surely this is a char *const [] as required by execvp and these const casts should go away?

smowton · 2019-01-29T09:37:58Z

unit/memory-analyzer/gdb_api.cpp

+
+#include <testing-utils/use_catch.h>
+
+#ifdef __linux__


Anything Unix-y I'd have thought? Are you doing anything tricky enough that Cygwin wouldn't support it?

Yes, changed to allow various Unices.

smowton · 2019-01-29T09:39:44Z

src/memory-analyzer/gdb_api.cpp

+
+/// Termiante the gdb process and close open streams (for reading from and
+/// writing to gdb)
+void gdb_apit::terminate_gdb_process()


Do this in a destructor to raise the chances of cleaning up your child on exception?

danpoe · 2019-01-29T10:52:45Z

@smowton I'm not sure if that's an issue here. So we only write a command to gdb when we have read the (gdb) prompt. Then we write one command (terminated by a newline). Then gdb only does something and writes output when it has read a complete command. Before writing another command we again wait for the prompt (gdb).

tautschnig · 2019-02-01T12:31:14Z

unit/memory-analyzer/gdb_api.cpp

@@ -0,0 +1,153 @@
+/*******************************************************************\
+
+Module: GDB Machine Interface API unit tests


Is it really worth having a unit test here? It might be better to just run this in regression/ as an integration test? There isn't a whole lot to the API, and the unit test is fairly close to being a shell script written in C++?

The back and forth interaction with gdb is actually quite complicated. I feel like there definitely need to be unit tests to check that the API does this correctly.

Ok, fine with me. I was just wondering whether doing this as a unit test just made things more complicated than necessary.

tautschnig · 2019-02-01T12:37:48Z

src/memory-analyzer/gdb_api.cpp

+/// \file
+/// Low-level interface to gdb
+
+#ifdef __linux__


Which part of this code is really Linux-specific? If any at all? Even when we might never be able to run a gdb binary on Visual Studio, it's good to know that at least the code compiles and can be re-used/adapted.

Yes, changed to allow various Unices. We need the fork() call from unistd.h.

tautschnig · 2019-02-01T12:38:22Z

src/memory-analyzer/gdb_api.cpp

+/// variable `binary`
+void gdb_apit::create_gdb_process()
+{
+  PRECONDITION(gdb_state == gdb_statet::NOT_CREATED); std::cout << "GDB Here 0" << std::endl;


I guess this needs some cleanup :-) You might as well use a debug() mstreamt, possibly with a separate debug logger so that you can use, e.g., a stream-based message handler that puts all the debug output on stderr?

Ah yes I just added this as I'm debugging some CI issues. This will be removed later.

…t review

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.

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.

This switches gdb_apit to use streams to communicate with the gdb subprocess instead of using pipes/file descriptors directly.

This changes gdb_apit to use the gdb machine interface (mi) instead of the gdb command line user interface to communicate with gdb.

We require the Unix fork() system call (in unistd.h)

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.

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).

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: fa2ed7b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104995261

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: d803bde).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104996155

danpoe requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners January 28, 2019 19:11

smowton reviewed Jan 29, 2019

View reviewed changes

danpoe force-pushed the feature/gdb-api branch from 78add3d to 464f292 Compare January 29, 2019 13:35

danpoe requested review from forejtv and thk123 as code owners January 29, 2019 13:35

danpoe force-pushed the feature/gdb-api branch 7 times, most recently from 23642a0 to d5b99d2 Compare February 1, 2019 11:28

tautschnig reviewed Feb 1, 2019

View reviewed changes

tautschnig assigned danpoe Feb 1, 2019

danpoe added the do not merge label Feb 1, 2019

danpoe force-pushed the feature/gdb-api branch 9 times, most recently from 11cfbd2 to 8088eb0 Compare February 1, 2019 16:57

tautschnig unassigned tautschnig, kroening, peterschrammel and forejtv Mar 2, 2019

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 4, 2019

Squashed commits from prerequisite PR diffblue#3983 (GDB API) - Do no…

e34d041

…t review

xbauch pushed a commit to xbauch/cbmc that referenced this pull request Mar 4, 2019

Squashed commits from prerequisite PR diffblue#3983 (GDB API) - Do no…

2ad4194

…t review

chrisr-diffblue self-assigned this Mar 19, 2019

danpoe force-pushed the feature/gdb-api branch from a7f71ca to 5d14896 Compare March 19, 2019 13:41

mmuesly and others added 10 commits March 19, 2019 13:42

Remove unnecessary forward declarations of cprover types

81fcf26

Use streams to communicate with gdb subprocess

b73bb29

This switches gdb_apit to use streams to communicate with the gdb subprocess instead of using pipes/file descriptors directly.

Adapt gdb interaction exception to cprover style

d44dfb9

Add #endif comments to gdb api header file

a49c421

Update banners for gdb api files

0b9480b

Switch gdb_apit to using the gdb machine interface

fa3c78f

This changes gdb_apit to use the gdb machine interface (mi) instead of the gdb command line user interface to communicate with gdb.

Remove unused gdb_inaccessible_memory_exceptiont

58f6d11

Add empty lines in gdb_api.cpp to improve readability

5c518e7

danpoe force-pushed the feature/gdb-api branch from 5d14896 to fa2ed7b Compare March 19, 2019 15:52

danpoe and others added 7 commits March 19, 2019 15:52

Install gdb package in CI to make gdb_apit unit tests work

b72245b

Add file module_dependencies.txt to memory-analyzer

0e1a5ca

Replace #ifdef __linux__ by guards allowing more Unices

7e6bd17

We require the Unix fork() system call (in unistd.h)

Enable and update gdb api unit tests

aece5a5

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.

Add new unit tests for the gdb api

fcbe7b9

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).

Install gdb on macos builds

fa2ed7b

Fix based on comments

d803bde

danpoe merged commit 6533631 into diffblue:develop Mar 19, 2019

allredj reviewed Mar 19, 2019

View reviewed changes

danpoe deleted the feature/gdb-api branch June 2, 2020 17:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

GDB API [blocks: #4261] #3983

GDB API [blocks: #4261] #3983

danpoe commented Jan 28, 2019 •

edited

Loading

martin-cs commented Jan 28, 2019

smowton left a comment

smowton Jan 29, 2019

tautschnig Mar 2, 2019

xbauch Mar 13, 2019

smowton Jan 29, 2019

danpoe Feb 14, 2019

smowton Jan 29, 2019

xbauch Mar 13, 2019

danpoe commented Jan 29, 2019

tautschnig Feb 1, 2019

danpoe Feb 1, 2019 •

edited

Loading

tautschnig Feb 1, 2019

tautschnig Feb 1, 2019

danpoe Feb 14, 2019

tautschnig Feb 1, 2019

danpoe Feb 1, 2019

allredj left a comment

allredj left a comment


		dprintf(pipe_output[1], "binary name: %s\n", binary);

		char arg[] = {const_cast<char >("gdb"),

		@@ -0,0 +1,153 @@
		/*******************************************************************\

		Module: GDB Machine Interface API unit tests

GDB API [blocks: #4261] #3983

GDB API [blocks: #4261] #3983

Conversation

danpoe commented Jan 28, 2019 • edited Loading

martin-cs commented Jan 28, 2019

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe commented Jan 29, 2019

Choose a reason for hiding this comment

danpoe Feb 1, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Jan 28, 2019 •

edited

Loading

danpoe Feb 1, 2019 •

edited

Loading