Squashed commits from Prerequisite PR #4261 -- Do not review

Author: petr-bauch

.travis.yml

@@ -200,7 +200,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 +228,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 +264,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)
@@ -284,7 +284,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
@@ -330,16 +330,16 @@ install:
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
   - make -C src/cpp library_check
-  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
+  - env WITH_MEMORY_ANALYZER=1 make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
-  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
-  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
-  - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
-  - make -C unit test
+  - env UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression/cbmc test-paths-lifo
+  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 WITH_MEMORY_ANALYZER=1 make -C regression/cbmc test-cprover-smt2
+  - env WITH_MEMORY_ANALYZER=1 make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
+  - env WITH_MEMORY_ANALYZER=1 make -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C jbmc/unit test

CMakeLists.txt

@@ -104,16 +104,28 @@ 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")
+
 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
@@ -144,13 +156,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/memory-analyzer.md

@@ -0,0 +1,78 @@
+[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. 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 -std=c11 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).
+
+The user can choose to either run GDB from a core-file `--core-file cf` or to a
+break-point `--breakpoint bp` (and only one of those). 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 -std=c11 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:
+
+```
+{
+  array = { 1, 4, 3 };
+}
+```
+
+Finally, to obtain an output in JSON format, e.g. for further analyses by
+`goto-harness` pass the additional option `--json-ui` together with requesting
+the output to be a symbol table by `--symtab-snapshot`.
+
+```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

@@ -51,3 +51,7 @@ add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
+
+if(WITH_MEMORY_ANALYZER)
+add_subdirectory(memory-analyzer)
+endif()

regression/Makefile

@@ -25,13 +25,16 @@ DIRS = cbmc \
        goto-cc-goto-analyzer \
        systemc \
        contracts \
+       memory-analyzer
        # Empty last line
 
 # Run all test directories in sequence
 .PHONY: test
 test:
 	@for dir in $(DIRS); do \
+	  if [ "$$dir" != memory-analyzer -o "$WITH_MEMORY_ANALYZER" = 1 ]; then \
 		$(MAKE) "$$dir" || exit 1; \
+	  fi \
 	done;
 
 # Pattern to execute a single test suite directory

regression/memory-analyzer/CMakeLists.txt

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

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;
+}

regression/memory-analyzer/arrays/arrays.h

@@ -0,0 +1,32 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// Example3 test explicitly the array support.
+/// It ensures, that arrays are handled right.
+/// The different typedefs have been used, to make sure the memory-analyzer
+/// is aware of the different appeareances in the gdb responses.
+
+#include <stdbool.h>
+
+struct a_sub_sub_typet
+{
+  char *text;
+};
+
+typedef struct a_sub_sub_typet messaget;
+
+struct a_sub_typet
+{
+  int id;
+  messaget options[2];
+};
+
+struct a_typet
+{
+  int config[10];
+  bool initialized;
+  unsigned char values[70];
+  struct a_sub_typet childs[4];
+} * test_struct;
+
+typedef struct a_sub_typet entryt;