Fix CMake syntax to enable memory analyzer tests

.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

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

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)

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

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

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 $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ../../../scripts/extract_type_header.py ${is_windows}"
+)

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"

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

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 $<TARGET_FILE:file_converter>
+                "${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"
+              $<TARGET_FILE:file_converter>
+        )
+    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(

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

unit/memory-analyzer/gdb_api.cpp

@@ -18,13 +18,28 @@ Author: Malte Mues <[email protected]>
 #include <iostream>
 
 #include <memory-analyzer/gdb_api.cpp>
+
 #include <util/run.h>
+#include <util/tempfile.h>
 
-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 <memory-analyzer/test.inc>
+      ; // 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<std::string> 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 <memory-analyzer/input.inc>
+      ; // 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<std::string> args;
-  args.push_back("test");
+  args.push_back(test_file.compiled());
 
   {
     gdb_apit gdb_api(args, true);