Merge pull request #4261 from danpoe/feature/memory-analyzer

Memory analyzer to take memory snapshots [blocks: #2649, #4438]

Author: tautschnig

.travis.yml

@@ -108,6 +108,7 @@ jobs:
       env:
         - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
+        - WITH_MEMORY_ANALYZER=1
 
     # OS X using clang++
     - stage: Test different OS/CXX/Flags
@@ -118,7 +119,9 @@ jobs:
       before_install:
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel gdb
         - export PATH=$PATH:/usr/local/opt/ccache/libexec
-      env: COMPILER="ccache clang++"
+      env:
+        - COMPILER="ccache clang++"
+        - WITH_MEMORY_ANALYZER=0
 
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
@@ -144,6 +147,7 @@ jobs:
       env:
         - COMPILER="ccache /usr/bin/g++-5"
         - EXTRA_CXXFLAGS="-DDEBUG"
+        - WITH_MEMORY_ANALYZER=1
       script: echo "Not running any tests for a debug build."
 
     # Ubuntu Linux with glibc using clang++-7, debug mode, disable USE_DSTRING
@@ -175,6 +179,7 @@ jobs:
         - COMPILER="ccache /usr/bin/clang++-7"
         - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DDEBUG -DUSE_STD_STRING"
         - CCACHE_CPP2=yes
+        - WITH_MEMORY_ANALYZER=1
       script: echo "Not running any tests for a debug build."
 
     # cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST
@@ -200,7 +205,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; bin/unit "[core][irept]")
@@ -228,7 +233,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -264,7 +269,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -321,6 +326,7 @@ jobs:
       env:
         - NAME="COVERITY_SCAN"
         - COMPILER="ccache g++"
+        - WITH_MEMORY_ANALYZER=1
       script: echo "This is coverity build. No need for tests."
 
 install:

CMakeLists.txt

@@ -104,16 +104,37 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     endif()
 endif()
 
+function(cprover_default_properties)
+    set(CBMC_CXX_STANDARD 11)
+    set(CBMC_CXX_STANDARD_REQUIRED true)
+    set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
+            "Developer ID Application: Daniel Kroening")
+
+    set_target_properties(
+      ${ARGN}
+     PROPERTIES
+     CXX_STANDARD ${CBMC_CXX_STANDARD}
+     CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
+     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")
+
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)
 
-set(CBMC_CXX_STANDARD 11)
-set(CBMC_CXX_STANDARD_REQUIRED true)
-set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
-    "Developer ID Application: Daniel Kroening")
-
-set_target_properties(
+cprover_default_properties(
     analyses
     ansi-c
     assembler
@@ -145,13 +166,7 @@ set_target_properties(
     testing-utils
     unit
     util
-    xml
-
-    PROPERTIES
-    CXX_STANDARD ${CBMC_CXX_STANDARD}
-    CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
-    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}
-)
+    xml)
 
 option(WITH_JBMC "Build the JBMC Java front-end" ON)
 if(WITH_JBMC)

doc/cprover-manual/index.md

@@ -8,7 +8,9 @@
 
 [A Short Tutorial](cbmc/tutorial/),
 [Loop Unwinding](cbmc/unwinding/),
-[Assertion Checking](cbmc/assertions/)
+[Assertion Checking](cbmc/assertions/),
+[Memory Analyzer](cbmc/memory-analyzer/),
+[Program Harness](cbmc/goto-harness/)
 
 ## 4. [Test Suite Generation](test-suite/)
 

doc/cprover-manual/memory-analyzer.md

@@ -0,0 +1,89 @@
+[CPROVER Manual TOC](../../)
+
+## Memory Analyzer
+
+The memory analyzer is a front-end for running and querying GDB in order to
+obtain a state of the input program. The GDB is not needed to be executed
+directly but is rather used as a back-end for the memory analysis. A common
+application would be to obtain a snapshot of a program under analysis at a
+particular state of execution. Such a snapshot could be useful on its own: to
+query about values of particular variables. Furthermore, since that snapshot is
+a state of a valid concrete execution, it can also be used for subsequent
+analyses.
+
+## Usage
+
+We assume that the user wants to inspect a binary executable compiled with
+debugging symbols and a symbol table information understandable by CBMC, e.g.
+(having `goto-gcc` on the `PATH`):
+
+```sh
+$ goto-gcc -g input_program.c -o input_program_exe
+```
+
+Calling `goto-gcc` instead of simply compiling with `gcc` produces an ELF binary
+with a goto section that contains the goto model (goto program + symbol table)
+[goto-cc-variants](../goto-cc/variants/).
+
+The memory analyzer supports two workflows to initiate the GDB with user code:
+either to run the code from a core-file or up to a break-point. If the user
+already has a core-file, they can specify it with the option `--core-file cf`.
+If the user knows the point of their program from where they want to run the
+analysis, they can specify it with the option `--breakpoint bp`. Only one of
+core-file/break-point option can be used.
+
+The tool also expects a comma-separated list of symbols to be analysed
+`--symbols s1, s2, ..`. Given its dependence on GDB, `memory-analyzer` is a
+Unix-only tool. The tool calls `gdb` to obtain the snapshot which is why the
+`-g` option is necessary for the program symbols to be visible.
+
+Take for example the following program:
+
+```C
+// main.c
+void checkpoint() {}
+
+int array[] = {1, 2, 3};
+
+int main()
+{
+  array[1] = 4;
+
+  checkpoint();
+
+  return 0;
+}
+```
+
+Say we are interested in the evaluation of `array` at the call-site of
+`checkpoint`. We compile the program with
+
+```sh
+$ goto-gcc -g main.c -o main_exe
+```
+
+And then we call `memory-analyzer` with:
+
+```sh
+$ memory-analyzer --breakpoint checkpoint --symbols array main_exe
+```
+
+to obtain as output the human readable list of values for each requested symbol:
+
+```
+{
+  array = { 1, 4, 3 };
+}
+```
+
+The above option is useful for the user and their preliminary analysis but does
+not contain enough information for further computer-based analyses. To that end,
+memory analyzer has an option to request the result to be a snapshot of the
+whole symbol table `--symtab-snapshot`. Finally, to obtain an output in JSON
+format, e.g. for further analyses by `goto-harness` pass the additional option
+`--json-ui`.
+
+```sh
+$ memory-analyzer --symtab-snapshot --json-ui \
+--breakpoint checkpoint --symbols array main_exe > snapshot.json
+```

jbmc/CMakeLists.txt

@@ -8,7 +8,7 @@ add_custom_target(java-models-library ALL
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library
 )
 
-set_target_properties(
+cprover_default_properties(
     java_bytecode
     java-models-library
     jbmc
@@ -20,9 +20,4 @@ set_target_properties(
     java-testing-utils
     java-unit
     miniz
-
-    PROPERTIES
-    CXX_STANDARD ${CBMC_CXX_STANDARD}
-    CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
-    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}
 )

regression/CMakeLists.txt

@@ -53,3 +53,7 @@ add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
+
+if(WITH_MEMORY_ANALYZER)
+add_subdirectory(memory-analyzer)
+endif()

regression/Makefile

@@ -30,6 +30,23 @@ DIRS = cbmc \
        symtab2gb \
        # Empty last line
 
+ifeq ($(OS),Windows_NT)
+    detected_OS := Windows
+else
+    detected_OS := $(shell sh -c 'uname 2>/dev/null || echo Unknown')
+endif
+
+ifeq ($(detected_OS),Linux)
+  ifneq ($(WITH_MEMORY_ANALYZER),0)
+    # only set if it wasn't explicitly unset
+    WITH_MEMORY_ANALYZER=1
+  endif
+endif
+
+ifeq ($(WITH_MEMORY_ANALYZER),1)
+  DIRS += memory-analyzer
+endif
+
 # Run all test directories in sequence
 .PHONY: test
 test:

regression/memory-analyzer/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+  "../chain.sh \
+   $<TARGET_FILE:memory-analyzer> $<TARGET_FILE_DIR:goto-cc>/goto-gcc")

regression/memory-analyzer/Makefile

@@ -0,0 +1,22 @@
+default: clean tests.log
+
+GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc
+MEMORY_ANALYZER_EXE=../../../src/memory-analyzer/memory-analyzer
+
+clean:
+	find -name '*.exe' -execdir $(RM) '{}' \;
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+test:
+	@../test.pl -e -p -c "../chain.sh $(MEMORY_ANALYZER_EXE) $(GOTO_GCC_EXE)"
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c "../chain.sh $(MEMORY_ANALYZER_EXE) $(GOTO_GCC_EXE)"
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/memory-analyzer/arrays/arrays.c

@@ -0,0 +1,82 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// This file test array support in the memory-analyzer.
+/// A more detailed description of the test idea is in example3.h.
+/// setup() prepares the data structure.
+/// manipulate_data() is the hook used for the test,
+/// where gdb reaches the breakpoint.
+/// main() is just the required boilerplate around this methods,
+/// to make the compiled result executable.
+
+#include "arrays.h"
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+void setup()
+{
+  test_struct = malloc(sizeof(struct a_typet));
+  for(int i = 0; i < 10; i++)
+  {
+    test_struct->config[i] = i + 10;
+  }
+  for(int i = 0; i < 10; i++)
+  {
+    test_struct->values[i] = 0xf3;
+  }
+  for(int i = 10; i < 20; i++)
+  {
+    test_struct->values[i] = 0x3f;
+  }
+  for(int i = 20; i < 30; i++)
+  {
+    test_struct->values[i] = 0x01;
+  }
+  for(int i = 30; i < 40; i++)
+  {
+    test_struct->values[i] = 0x01;
+  }
+  for(int i = 40; i < 50; i++)
+  {
+    test_struct->values[i] = 0xff;
+  }
+  for(int i = 50; i < 60; i++)
+  {
+    test_struct->values[i] = 0x00;
+  }
+  for(int i = 60; i < 70; i++)
+  {
+    test_struct->values[i] = 0xab;
+  }
+  messaget option1 = {.text = "accept"};
+  for(int i = 0; i < 4; i++)
+  {
+    char *value = malloc(sizeof(char *));
+    sprintf(value, "unique%i", i);
+    entryt your_options = {
+      .id = 1, .options[0] = option1, .options[1].text = value};
+    your_options.id = i + 12;
+    test_struct->childs[i].id = your_options.id;
+    test_struct->childs[i].options[0] = your_options.options[0];
+    test_struct->childs[i].options[1].text = your_options.options[1].text;
+  }
+  test_struct->initialized = true;
+}
+
+int manipulate_data()
+{
+  for(int i = 0; i < 4; i++)
+  {
+    free(test_struct->childs[i].options[1].text);
+    test_struct->childs[i].options[1].text = "decline";
+  }
+}
+
+int main()
+{
+  setup();
+  manipulate_data();
+  return 0;
+}