Skip to content

Commit 11149ef

Browse files
tautschnigtautschnig
authored
Merge pull request #5932 from tautschnig/memory-analyzer-tests
Fix CMake syntax to enable memory analyzer tests
2 parents 2f7dcb5 + 0e6b393 commit 11149ef

File tree

11 files changed

+102
-28
lines changed

11 files changed

+102
-28
lines changed

‎.github/workflows/pull-request-checks.yaml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ jobs:
132132
DEBIAN_FRONTEND: noninteractive
133133
run: |
134134
sudo apt-get update
135-
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
135+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
136136
- name: Confirm z3 solver is available and log the version installed
137137
run: z3 --version
138138
- name: Prepare ccache
@@ -448,7 +448,7 @@ jobs:
448448
- name: Fetch dependencies
449449
run: |
450450
sudo apt-get update
451-
sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
451+
sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
452452
# remove libgcc-s1, which isn't normally available in Ubuntu 18.04
453453
target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
454454
# libgcc1 uses an epoch, thus the extra 1:
@@ -536,7 +536,7 @@ jobs:
536536
DEBIAN_FRONTEND: noninteractive
537537
run: |
538538
sudo apt-get update
539-
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
539+
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
540540
- name: Confirm z3 solver is available and log the version installed
541541
run: z3 --version
542542
- name: Prepare ccache

‎.github/workflows/release-packages.yaml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ jobs:
1313
with:
1414
submodules: recursive
1515
- name: Fetch dependencies
16-
run: sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
16+
run: sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
1717
- name: Prepare ccache
1818
uses: actions/cache@v2
1919
with:
@@ -70,7 +70,7 @@ jobs:
7070
submodules: recursive
7171
- name: Fetch dependencies
7272
run: |
73-
sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
73+
sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
7474
# remove libgcc-s1, which isn't normally available in Ubuntu 18.04
7575
target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
7676
# libgcc1 uses an epoch, thus the extra 1:

‎CMakeLists.txt‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -182,17 +182,14 @@ function(cprover_default_properties)
182182
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY})
183183
endfunction()
184184

185-
option(WITH_MEMORY_ANALYZER OFF
186-
"build the memory analyzer")
187-
188185
if(CMAKE_SYSTEM_NAME STREQUAL Linux)
189186
set(WITH_MEMORY_ANALYZER_DEFAULT ON)
190187
else()
191188
set(WITH_MEMORY_ANALYZER_DEFAULT OFF)
192189
endif()
193190

194-
option(WITH_MEMORY_ANALYZER ${WITH_MEMORY_ANALYZER_DEFAULT}
195-
"build the memory analyzer")
191+
option(WITH_MEMORY_ANALYZER
192+
"build the memory analyzer" ${WITH_MEMORY_ANALYZER_DEFAULT})
196193

197194
add_subdirectory(src)
198195
add_subdirectory(regression)

‎regression/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,4 +78,5 @@ add_subdirectory(cpp-linter)
7878
if(WITH_MEMORY_ANALYZER)
7979
add_subdirectory(snapshot-harness)
8080
add_subdirectory(memory-analyzer)
81+
add_subdirectory(extract_type_header)
8182
endif()

‎regression/Makefile‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,8 @@ endif
6464

6565
ifeq ($(WITH_MEMORY_ANALYZER),1)
6666
DIRS += snapshot-harness \
67-
memory-analyzer
67+
memory-analyzer \
68+
extract_type_header
6869
endif
6970

7071
# Run all test directories in sequence

‎regression/extract_type_header/CMakeLists.txt‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ../../../scripts/extract_type_header.py ${is_windows}"
9+
)

‎regression/extract_type_header/chain.sh‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,12 @@ name=${name%.c}
1414
args=${*:6:$#-6}
1515

1616
if [[ "${is_windows}" == "true" ]]; then
17-
$goto_cc "${name}.c"
18-
mv "${name}.exe" "${name}.gb"
17+
$goto_cc "${name}.c" "/Fe${name}.gb"
1918
else
2019
$goto_cc -o "${name}.gb" "${name}.c"
2120
fi
2221

23-
export PATH=$PATH:"$(pwd)../../../src/goto-instrument/"
22+
export PATH=$PATH:"$(cd $(dirname $goto_instrument) && pwd)"
2423
$python_script "${name}.gb" "${name}.c" "header.h"
2524
cat "header.h"
2625
rm -f "header.h"

‎src/memory-analyzer/gdb_api.cpp‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -132,13 +132,13 @@ void gdb_apit::create_gdb_process()
132132

133133
// Only reachable, if execvp failed
134134
int errno_value = errno;
135-
dprintf(pipe_output[1], "errno in child: %s\n", strerror(errno_value));
135+
dprintf(pipe_output[1], "Starting gdb failed: %s\n", strerror(errno_value));
136+
dprintf(pipe_output[1], "(gdb) \n");
137+
throw gdb_interaction_exceptiont("could not run gdb");
136138
}
137139
else
138140
{
139141
// parent process
140-
gdb_state = gdb_statet::CREATED;
141-
142142
close(pipe_input[0]);
143143
close(pipe_output[1]);
144144

@@ -149,6 +149,11 @@ void gdb_apit::create_gdb_process()
149149
command_stream = fdopen(pipe_input[1], "w");
150150

151151
std::string line = read_most_recent_line();
152+
if(has_prefix(line, "Starting gdb failed:"))
153+
throw gdb_interaction_exceptiont(line);
154+
155+
gdb_state = gdb_statet::CREATED;
156+
152157
CHECK_RETURN(
153158
has_prefix(line, R"(~"done)") ||
154159
has_prefix(line, R"(~"Reading)"));

‎unit/CMakeLists.txt‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,34 @@ file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
1616
if(NOT WITH_MEMORY_ANALYZER)
1717
file(GLOB_RECURSE memory_analyzer_sources "memory-analyzer/*.cpp")
1818
list(REMOVE_ITEM sources ${memory_analyzer_sources})
19+
else()
20+
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer"
21+
COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer
22+
)
23+
function(make_mm_inc input output)
24+
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/${output}"
25+
COMMAND $<TARGET_FILE:file_converter>
26+
"${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/${input}" >
27+
"${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/${output}"
28+
DEPENDS
29+
"${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/${input}"
30+
"${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer"
31+
$<TARGET_FILE:file_converter>
32+
)
33+
endfunction(make_mm_inc)
34+
35+
make_mm_inc(input.txt input.inc)
36+
make_mm_inc(test.c test.inc)
37+
38+
set(generated_mm_files
39+
"${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/input.inc"
40+
"${CMAKE_CURRENT_BINARY_DIR}/memory-analyzer/test.inc"
41+
)
42+
set_source_files_properties(
43+
"${CMAKE_CURRENT_SOURCE_DIR}/memory-analyzer/gdb_api.cpp"
44+
PROPERTIES
45+
OBJECT_DEPENDS "${generated_mm_files}"
46+
)
1947
endif()
2048

2149
list(REMOVE_ITEM sources
@@ -44,6 +72,7 @@ target_include_directories(unit
4472
${CBMC_BINARY_DIR}
4573
${CBMC_SOURCE_DIR}
4674
${CMAKE_CURRENT_SOURCE_DIR}
75+
${CMAKE_CURRENT_BINARY_DIR}
4776
${CUDD_INCLUDE}
4877
)
4978
target_link_libraries(

‎unit/Makefile‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,16 @@ N_CATCH_TESTS = $(shell \
242242
$$(printf ' -not -name %s ' $(EXCLUDED_TESTS))) | \
243243
grep -E "(SCENARIO|TEST_CASE)" | grep -c -v '\[\.\]')
244244

245-
CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT)
245+
memory-analyzer/input.inc: memory-analyzer/input.txt
246+
../src/ansi-c/file_converter$(EXEEXT) $< > $@
247+
248+
memory-analyzer/test.inc: memory-analyzer/test.c
249+
../src/ansi-c/file_converter$(EXEEXT) $< > $@
250+
251+
memory-analyzer/gdb_api$(OBJEXT): memory-analyzer/input.inc memory-analyzer/test.inc
252+
253+
CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) \
254+
memory-analyzer/input.inc memory-analyzer/test.inc
246255

247256
# only add a dependency for libraries to avoid triggering implicit rules, which
248257
# would cause unnecessary rebuilds

0 commit comments

Comments
 (0)