From d83aee3cc31ebccd05214d0efb22a9d1cfcdbb36 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Mar 2021 09:00:16 +0000 Subject: [PATCH 1/4] memory analyzer: fail when gdb cannot be started When gdb wasn't available, the forked child would not terminate and the parent would wait forever. --- src/memory-analyzer/gdb_api.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index c30fb257666..8b280532ee3 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -132,13 +132,13 @@ void gdb_apit::create_gdb_process() // Only reachable, if execvp failed int errno_value = errno; - dprintf(pipe_output[1], "errno in child: %s\n", strerror(errno_value)); + dprintf(pipe_output[1], "Starting gdb failed: %s\n", strerror(errno_value)); + dprintf(pipe_output[1], "(gdb) \n"); + throw gdb_interaction_exceptiont("could not run gdb"); } else { // parent process - gdb_state = gdb_statet::CREATED; - close(pipe_input[0]); close(pipe_output[1]); @@ -149,6 +149,11 @@ void gdb_apit::create_gdb_process() command_stream = fdopen(pipe_input[1], "w"); std::string line = read_most_recent_line(); + if(has_prefix(line, "Starting gdb failed:")) + throw gdb_interaction_exceptiont(line); + + gdb_state = gdb_statet::CREATED; + CHECK_RETURN( has_prefix(line, R"(~"done)") || has_prefix(line, R"(~"Reading)")); From fde85b8f6a22b8014b5d51d0fcb555177d9d3bb9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Mar 2021 09:01:05 +0000 Subject: [PATCH 2/4] Memory analyzer unit tests: embed source files Make the unit tests less fragile by not relying on a particular directory that they are being run from. Test files had to be loaded from a specific location; instead, place them in the source code and generate temporary files at runtime. --- unit/CMakeLists.txt | 29 +++++++++++++++++++++ unit/Makefile | 11 +++++++- unit/memory-analyzer/gdb_api.cpp | 44 ++++++++++++++++++++++++-------- 3 files changed, 73 insertions(+), 11 deletions(-) diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index bcc7f37fc08..81a5b57e24b 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -16,6 +16,34 @@ file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h") if(NOT WITH_MEMORY_ANALYZER) file(GLOB_RECURSE memory_analyzer_sources "memory-analyzer/*.cpp") list(REMOVE_ITEM sources ${memory_analyzer_sources}) +else() + add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer" + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer + ) + function(make_mm_inc input output) + add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/${output}" + COMMAND $ + "${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/${input}" > + "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/${output}" + DEPENDS + "${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/${input}" + "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer" + $ + ) + endfunction(make_mm_inc) + + make_mm_inc(input.txt input.inc) + make_mm_inc(test.c test.inc) + + set(generated_mm_files + "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/input.inc" + "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/test.inc" + ) + set_source_files_properties( + "${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/gdb_api.cpp" + PROPERTIES + OBJECT_DEPENDS "${generated_mm_files}" + ) endif() list(REMOVE_ITEM sources @@ -44,6 +72,7 @@ target_include_directories(unit ${CBMC_BINARY_DIR} ${CBMC_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} + ${CMAKE_CURRENT_BINARY_DIR} ${CUDD_INCLUDE} ) target_link_libraries( diff --git a/unit/Makefile b/unit/Makefile index 1ffbe8c1a6e..43b4ec56ea8 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -242,7 +242,16 @@ N_CATCH_TESTS = $(shell \ $$(printf ' -not -name %s ' $(EXCLUDED_TESTS))) | \ grep -E "(SCENARIO|TEST_CASE)" | grep -c -v '\[\.\]') -CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) +memory-analyzer/input.inc: memory-analyzer/input.txt + ../src/ansi-c/file_converter$(EXEEXT) $< > $@ + +memory-analyzer/test.inc: memory-analyzer/test.c + ../src/ansi-c/file_converter$(EXEEXT) $< > $@ + +memory-analyzer/gdb_api$(OBJEXT): memory-analyzer/input.inc memory-analyzer/test.inc + +CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) \ + memory-analyzer/input.inc memory-analyzer/test.inc # only add a dependency for libraries to avoid triggering implicit rules, which # would cause unnecessary rebuilds diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp index 9c40d5e89cc..758e21b6f94 100644 --- a/unit/memory-analyzer/gdb_api.cpp +++ b/unit/memory-analyzer/gdb_api.cpp @@ -18,13 +18,28 @@ Author: Malte Mues #include #include + #include +#include -void compile_test_file() +struct compile_test_filet { - REQUIRE( - run("gcc", {"gcc", "-g", "-o", "test", "memory-analyzer/test.c"}) == 0); -} + compile_test_filet() : compiled("test", "") + { + temporary_filet tmp("test", ".c"); + std::ofstream of(tmp().c_str()); + REQUIRE(of.is_open()); + + of << +#include + ; // NOLINT(whitespace/semicolon) + of.close(); + + REQUIRE(run("gcc", {"gcc", "-g", "-o", compiled(), tmp()}) == 0); + } + + temporary_filet compiled; +}; void check_for_gdb() { @@ -46,10 +61,10 @@ class gdb_api_testt : public gdb_apit void gdb_api_internals_test() { check_for_gdb(); - compile_test_file(); + compile_test_filet test_file; std::vector args; - args.push_back("test"); + args.push_back(test_file.compiled()); SECTION("parse gdb output record") { @@ -67,9 +82,18 @@ void gdb_api_internals_test() SECTION("read a line from an input stream") { + temporary_filet tmp("input", ".txt"); + std::ofstream of(tmp().c_str()); + REQUIRE(of.is_open()); + + of << +#include + ; // NOLINT(whitespace/semicolon) + of.close(); + gdb_api_testt gdb_api(args); - FILE *f = fopen("memory-analyzer/input.txt", "r"); + FILE *f = fopen(tmp().c_str(), "r"); gdb_api.response_stream = f; std::string line = gdb_api.read_next_line(); @@ -79,7 +103,7 @@ void gdb_api_internals_test() REQUIRE(line == std::string(1120, 'a') + "\n"); line = gdb_api.read_next_line(); - REQUIRE(line == "xyz"); + REQUIRE(line == "xyz\n"); } SECTION("start and exit gdb") @@ -102,10 +126,10 @@ TEST_CASE("gdb api internals test", "[core][memory-analyzer]") TEST_CASE("gdb api test", "[core][memory-analyzer]") { check_for_gdb(); - compile_test_file(); + compile_test_filet test_file; std::vector args; - args.push_back("test"); + args.push_back(test_file.compiled()); { gdb_apit gdb_api(args, true); From d2aeeba55ac5e578de0c6e51b0d1bd553778cff3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Mar 2021 18:07:34 +0000 Subject: [PATCH 3/4] Fix CMake syntax to enable memory analyzer tests "option" requires the help text as second, not as third argument. This resulted in memory analyzer tests being disabled no matter what the OS being built on. --- .github/workflows/pull-request-checks.yaml | 6 +++--- .github/workflows/release-packages.yaml | 4 ++-- CMakeLists.txt | 7 ++----- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index e2b15483d74..79df8ed41e1 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -132,7 +132,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 + sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Prepare ccache @@ -448,7 +448,7 @@ jobs: - name: Fetch dependencies run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 + sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 # remove libgcc-s1, which isn't normally available in Ubuntu 18.04 target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1) # libgcc1 uses an epoch, thus the extra 1: @@ -536,7 +536,7 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ gcc binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3 + sudo apt-get install --no-install-recommends -y g++ gcc gdb binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Prepare ccache diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index e1540c45fde..494ef5009ad 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -13,7 +13,7 @@ jobs: with: submodules: recursive - name: Fetch dependencies - run: sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache + run: sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache - name: Prepare ccache uses: actions/cache@v2 with: @@ -70,7 +70,7 @@ jobs: submodules: recursive - name: Fetch dependencies run: | - sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache + sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache # remove libgcc-s1, which isn't normally available in Ubuntu 18.04 target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1) # libgcc1 uses an epoch, thus the extra 1: diff --git a/CMakeLists.txt b/CMakeLists.txt index d7d637483c6..bc86e39eea8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -182,17 +182,14 @@ function(cprover_default_properties) XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}) endfunction() -option(WITH_MEMORY_ANALYZER OFF - "build the memory analyzer") - if(CMAKE_SYSTEM_NAME STREQUAL Linux) set(WITH_MEMORY_ANALYZER_DEFAULT ON) else() set(WITH_MEMORY_ANALYZER_DEFAULT OFF) endif() -option(WITH_MEMORY_ANALYZER ${WITH_MEMORY_ANALYZER_DEFAULT} - "build the memory analyzer") +option(WITH_MEMORY_ANALYZER + "build the memory analyzer" ${WITH_MEMORY_ANALYZER_DEFAULT}) add_subdirectory(src) add_subdirectory(regression) From 0e6b393f1b56e36a50b4d7b24e41f4a9efd70e7a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Mar 2021 18:35:32 +0000 Subject: [PATCH 4/4] Enable extract_type_header regression tests This test isn't strictly dependent on memory-analyzer being available, but is only of interest if that is the case. --- regression/CMakeLists.txt | 1 + regression/Makefile | 3 ++- regression/extract_type_header/CMakeLists.txt | 9 +++++++++ regression/extract_type_header/chain.sh | 5 ++--- 4 files changed, 14 insertions(+), 4 deletions(-) create mode 100644 regression/extract_type_header/CMakeLists.txt diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 895e0bea401..42c772ac445 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -78,4 +78,5 @@ add_subdirectory(cpp-linter) if(WITH_MEMORY_ANALYZER) add_subdirectory(snapshot-harness) add_subdirectory(memory-analyzer) + add_subdirectory(extract_type_header) endif() diff --git a/regression/Makefile b/regression/Makefile index 166e8f8932c..b3447272f75 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -64,7 +64,8 @@ endif ifeq ($(WITH_MEMORY_ANALYZER),1) DIRS += snapshot-harness \ - memory-analyzer + memory-analyzer \ + extract_type_header endif # Run all test directories in sequence diff --git a/regression/extract_type_header/CMakeLists.txt b/regression/extract_type_header/CMakeLists.txt new file mode 100644 index 00000000000..f64e0802d37 --- /dev/null +++ b/regression/extract_type_header/CMakeLists.txt @@ -0,0 +1,9 @@ +if(WIN32) + set(is_windows true) +else() + set(is_windows false) +endif() + +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ../../../scripts/extract_type_header.py ${is_windows}" +) diff --git a/regression/extract_type_header/chain.sh b/regression/extract_type_header/chain.sh index 3674a002813..1440f3937e0 100755 --- a/regression/extract_type_header/chain.sh +++ b/regression/extract_type_header/chain.sh @@ -14,13 +14,12 @@ name=${name%.c} args=${*:6:$#-6} if [[ "${is_windows}" == "true" ]]; then - $goto_cc "${name}.c" - mv "${name}.exe" "${name}.gb" + $goto_cc "${name}.c" "/Fe${name}.gb" else $goto_cc -o "${name}.gb" "${name}.c" fi -export PATH=$PATH:"$(pwd)../../../src/goto-instrument/" +export PATH=$PATH:"$(cd $(dirname $goto_instrument) && pwd)" $python_script "${name}.gb" "${name}.c" "header.h" cat "header.h" rm -f "header.h"