Feature memory-analyzer [depends-on: #2680, #4261]

CMakeLists.txt

@@ -68,6 +68,8 @@ set_target_properties(
     json
     langapi
     linking
+    memory-analyzer
+    memory-analyzer-lib
     miniBDD
     pointer-analysis
     solvers

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 ../compile_example.sh
+
+tests.log: ../test.pl
+	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+	@../test.pl -p -c ../compile_example.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 @@
+CORE
+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;
+\}
+--
+--

regression/memory-analyzer/compile_example.sh

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

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;

regression/memory-analyzer/cycles/test.desc

@@ -0,0 +1,20 @@
+CORE
+cycles.exe
+--breakpoint process_buffer --symbols buffer
+analyzing symbol: buffer
+GENERATED CODE: 
+\{
+  char _buffer_start_data_1\[\]="snow";
+  char __buffer_start_next_data_3\[\]="sun";
+  char ___buffer_start_next_next_data_5\[\]="rain";
+  char ____buffer_start_next_next_next_data_7\[\]="thunder storm";
+  struct cycle_buffer_entry ___buffer_start_next_next_next_6=\{ .data=\(char \*\)&____buffer_start_next_next_next_data_7, .next=\(\(struct cycle_buffer_entry \*\)NULL\) \};
+  struct cycle_buffer_entry __buffer_start_next_next_4=\{ .data=\(char \*\)&___buffer_start_next_next_data_5, .next=&___buffer_start_next_next_next_6 \};
+  struct cycle_buffer_entry _buffer_start_next_2=\{ .data=\(char \*\)&__buffer_start_next_data_3, .next=&__buffer_start_next_next_4 \};
+  struct cycle_buffer_entry buffer_start_0=\{ .data=\(char \*\)&_buffer_start_data_1, .next=&_buffer_start_next_2 \};
+  buffer.start = &buffer_start_0;
+  buffer.end = &___buffer_start_next_next_next_6;
+  \(\*\(\*\(\*\(\*buffer.start\).next\).next\).next\).next = &buffer_start_0;
+\}
+--
+--

regression/memory-analyzer/primitive_types/primitive_types.c

@@ -0,0 +1,42 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// This is just a basic example.
+/// Pointer references are tested and ensured, that for example f and f_1 are
+/// pointing to the same int value location after running memory-analyzer.
+
+#include "primitive_types.h"
+int my_function(char *s)
+{
+  int a = 10;
+  g->a = a;
+  g->b = s;
+  return 0;
+}
+
+int main(int argc, char **argv)
+{
+  char *test;
+
+  e = 17;
+
+  f = malloc(sizeof(int));
+  f = &e;
+  f_1 = f;
+
+  h = "test";
+
+  g = malloc(sizeof(struct mapping_things));
+  d.a = 4;
+  d.c = -32;
+  test = "test2";
+
+  d.b = test;
+
+  my_function(test);
+
+  free(g);
+  free(f);
+
+  return 0;
+}

regression/memory-analyzer/primitive_types/primitive_types.h

@@ -0,0 +1,28 @@
+//Copyright 2018 Author: Malte Mues <[email protected]>
+
+/// \file
+/// Example1 is just demonstrating, that the tool works in general.
+/// A small struct and a few primitive pointers are declared in the global
+/// namespace. These are assigned with values before calling my_function
+/// and then, it is tested that this global state can be reconstructed before
+/// calling my_function. As long as this example work basic functionallity is
+/// provided.
+
+#include <stdlib.h>
+
+struct mapping_things
+{
+  int a;
+  char *b;
+  int c;
+};
+
+typedef struct mapping_things other_things;
+
+other_things d;
+int e;
+int *f;
+int *f_1;
+struct mapping_things *g;
+char *h;
+int my_function(char *s);

regression/memory-analyzer/primitive_types/test.desc

@@ -0,0 +1,27 @@
+CORE
+primitive_types.exe
+--breakpoint my_function --symbols e,f,f_1,d,g,h
+analyzing symbol: e
+analyzing symbol: f
+analyzing symbol: f_1
+analyzing symbol: d
+analyzing symbol: g
+analyzing symbol: h
+GENERATED CODE: 
+\{
+  e = 17;
+  f = &e;
+  f_1 = &e;
+  char d_b_0\[\]="test2";
+  d.a = 4;
+  d.b = \(char \*\)&d_b_0;
+  d.c = -32;
+  struct mapping_things g_1=\{ .a=0, .b=\(\(char \*\)NULL\), .c=0 \};
+  g = &g_1;
+  char h_2\[\]="test";
+  h = \(char \*\)&h_2;
+}
+^EXIT=0
+^SIGNAL=0
+--
+--