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) 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" 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)")); 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);