Squashed commits from Prerequisite PR diffblue#4438 -- Do not review

Author: Petr Bauch

CMakeLists.txt

@@ -148,6 +148,8 @@ set_target_properties(
     json-symtab-language
     langapi
     linking
+    memory-analyzer
+    memory-analyzer-lib
     pointer-analysis
     solvers
     testing-utils

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
+```

regression/CMakeLists.txt

@@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(snapshot-harness)

regression/Makefile

@@ -23,6 +23,7 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       snapshot-harness \
        systemc \
        contracts \
        # Empty last line

regression/memory-analyzer/Makefile

@@ -0,0 +1,21 @@
+default: clean tests.log
+
+clean:
+	find -name '*.exe' -execdir $(RM) '{}' \;
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+test:
+	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+	@../test.pl -p -c ../chain.sh
+
+tests.log: ../test.pl
+	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+	@../test.pl -p -c ../chain.sh
+
+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->initalized = 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 initalized;
+  unsigned char values[70];
+  struct a_sub_typet childs[4];
+} * test_struct;
+
+typedef struct a_sub_typet entryt;

regression/memory-analyzer/arrays/test.desc

@@ -0,0 +1,24 @@
+FUTURE
+arrays.exe
+--breakpoint manipulate_data --symbols test_struct
+analyzing symbol: test_struct
+GENERATED CODE: 
+\{
+  char _test_struct_childs0_options0_text_1\[\]="accept";
+  char _test_struct_childs0_options1_text_2\[\]="unique0";
+  char _test_struct_childs1_options1_text_3\[\]="unique1";
+  char _test_struct_childs2_options1_text_4\[\]="unique2";
+  char _test_struct_childs3_options1_text_5\[\]="unique3";
+  struct a_typet test_struct_0=\{ .config=\{ 10, 11, 12, 13, 14, 15, 16, 17, 18, 19 \}, .initalized=0,
+    .values=\{ 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, 63, 63, 63, 63, 63, 63, 63, 63, 63, 63, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 171, 171, 171, 171, 171, 171, 171, 171, 171, 171 \}, .childs=\{ \{ .id=12, .options=\{ \{ .text=\(char \*\)&_test_struct_childs0_options0_text_1 \},
+    \{ .text=\(char \*\)&_test_struct_childs0_options1_text_2 \} \} \}, 
+    \{ .id=13, .options=\{ \{ .text=\(char \*\)&_test_struct_childs0_options0_text_1 \},
+    \{ .text=\(char \*\)&_test_struct_childs1_options1_text_3 \} \} \}, 
+    \{ .id=14, .options=\{ \{ .text=\(char \*\)&_test_struct_childs0_options0_text_1 \},
+    \{ .text=\(char \*\)&_test_struct_childs2_options1_text_4 \} \} \}, 
+    \{ .id=15, .options=\{ \{ .text=\(char \*\)&_test_struct_childs0_options0_text_1 \},
+    \{ .text=\(char \*\)&_test_struct_childs3_options1_text_5 \} \} \} \} \};
+  test_struct = &test_struct_0;
+\}
+^EXIT=0$
+^SIGNAL=0$

regression/memory-analyzer/arrays_01/main.c

@@ -0,0 +1,14 @@
+void checkpoint()
+{
+}
+
+int array[] = {1, 2, 3};
+
+int main()
+{
+  array[1] = 4;
+
+  checkpoint();
+
+  return 0;
+}

regression/memory-analyzer/arrays_01/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.exe
+--breakpoint checkpoint --symbols array
+array = \{ 1, 4, 3 \};
+^EXIT=0$
+^SIGNAL=0$

regression/memory-analyzer/chain.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+MEMORY_ANALYZER="../../../src/memory-analyzer/memory-analyzer"
+
+set -e
+
+NAME=${*:$#}
+NAME=${NAME%.exe}
+
+../../../src/goto-cc/goto-gcc -g -std=c11 -o $NAME.exe $NAME.c
+$MEMORY_ANALYZER $@

regression/memory-analyzer/cycles/cycles.c

@@ -0,0 +1,61 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// This example deals with cyclic data structures,
+/// see comment in example2.h explaining why this is necessary.
+/// add_element is just declared as a helper method for cycle construction.
+/// process_buffer isn't supposed to do meaningfull stuff.
+/// It is the hook for the gdb breakpoint used in the test.
+/// free_buffer just does clean up, if you run this.
+
+#include "cycles.h"
+void add_element(char *content)
+{
+  cycle_buffer_entry_t *new_entry = malloc(sizeof(cycle_buffer_entry_t));
+  new_entry->data = content;
+  if(buffer.end && buffer.start)
+  {
+    new_entry->next = buffer.start;
+    buffer.end->next = new_entry;
+    buffer.end = new_entry;
+  }
+  else
+  {
+    new_entry->next = new_entry;
+    buffer.end = new_entry;
+    buffer.start = new_entry;
+  }
+}
+
+int process_buffer()
+{
+  return 0;
+}
+
+void free_buffer()
+{
+  cycle_buffer_entry_t *current;
+  cycle_buffer_entry_t *free_next;
+  if(buffer.start)
+  {
+    current = buffer.start->next;
+    while(current != buffer.start)
+    {
+      free_next = current;
+      current = current->next;
+      free(free_next);
+    }
+    free(current);
+  }
+}
+
+int main()
+{
+  add_element("snow");
+  add_element("sun");
+  add_element("rain");
+  add_element("thunder storm");
+
+  process_buffer();
+  free_buffer();
+}

regression/memory-analyzer/cycles/cycles.h

@@ -0,0 +1,27 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// Example2 deals with cycles in datastructures.
+///
+/// While it is common that some datastructures contain cylces,
+/// it is necessary that the memory-analyzer does recognize them.
+/// Otherwise it would follow the datastructures pointer establishing
+/// the cycle for ever and never terminate execution.
+/// The cycle_buffer described below contains a cycle.
+/// As long as this regression test works, cycle introduced by using pointers
+/// are handle the correct way.
+
+#include <stdlib.h>
+typedef struct cycle_buffer_entry
+{
+  char *data;
+  struct cycle_buffer_entry *next;
+} cycle_buffer_entry_t;
+
+struct cycle_buffer
+{
+  cycle_buffer_entry_t *start;
+  struct cycle_buffer_entry *end;
+};
+
+struct cycle_buffer buffer;