Merge pull request #4578 from xbauch/feature/dynamic-memory-snapshot

Dynamic memory snapshot

Author: petr-bauch

regression/memory-analyzer/pointer_03/test.desc

@@ -2,6 +2,6 @@ CORE
 main.gb
 --breakpoint checkpoint --symbols x,p
 x = 3;
-p = &x;
+p = \(void \*\)\&x;
 ^EXIT=0$
 ^SIGNAL=0$

regression/memory-analyzer/pointer_to_struct_01/test.desc

@@ -1,8 +1,7 @@
 CORE
 main.gb
 --breakpoint checkpoint --symbols p
-struct S tmp;
-tmp = \{ \.next=\(\(struct S \*\)0\) \};
-p = \&tmp;
+st = \{ .next=\&st \};
+p = \&st;
 ^EXIT=0$
 ^SIGNAL=0$

regression/memory-analyzer/structs_02/test.desc

@@ -1,8 +1,7 @@
 CORE
 main.gb
 --breakpoint checkpoint --symbols st
-signed int tmp;
-tmp = 3;
-st = \{ .c1=1, .c2=&tmp \};
+i = 3;
+st = \{ .c1=1, .c2=\&i \};
 ^EXIT=0$
 ^SIGNAL=0$

regression/snapshot-harness/arrays_02/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int array[] = {1, 2, 3};
+int *p;
+int *q;
+
+void initialize()
+{
+  p = &(array[1]);
+  q = array + 1;
+  array[0] = 4;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p == q);
+  assert(*p == *q);
+  *p = 4;
+  q = q - 1;
+  assert(*q == *p);
+}

regression/snapshot-harness/arrays_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion \*p == \*q: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion \*q == \*p: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/snapshot-harness/dynamic-array-int/main.c

@@ -0,0 +1,47 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *array;
+int *iterator1;
+int *iterator2;
+int *iterator3;
+
+void initialize()
+{
+  array = (int *)malloc(sizeof(int) * 10);
+  array[0] = 1;
+  array[1] = 2;
+  array[2] = 3;
+  array[3] = 4;
+  array[4] = 5;
+  array[5] = 6;
+  array[6] = 7;
+  array[7] = 8;
+  array[8] = 9;
+  array[9] = 10;
+  iterator1 = (int *)array;
+  iterator2 = &array[1];
+  iterator3 = array + 1;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == iterator3);
+  assert(iterator2 == &array[1]);
+  assert(*iterator3 == array[1]);
+  assert(*iterator3 == 2);
+  iterator3 = &array[9];
+  iterator3++;
+  assert(*iterator3 == 0);
+
+  return 0;
+}

regression/snapshot-harness/dynamic-array-int/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == iterator3: SUCCESS
+\[main.assertion.4\] line [0-9]+ assertion iterator2 == \&array\[1\]: SUCCESS
+\[main.assertion.5\] line [0-9]+ assertion \*iterator3 == array\[1\]: SUCCESS
+\[main.assertion.6\] line [0-9]+ assertion \*iterator3 == 2: SUCCESS
+\[main.pointer_dereference.27\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator3: FAILURE
+\[main.assertion.7\] line [0-9]+ assertion \*iterator3 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-int/main.c

@@ -31,14 +31,10 @@ int main()
   checkpoint();
 
   assert(first == second);
-  // The following assertions will be check in the following PR once
-  // dynamically allocated snapshots are properly implemented.
-  /* assert(array_size >= prefix_size); */
-  /* assert(prefix_size >= 0); */
-  /* assert(second[prefix_size] != 6); */
-  /* assert(second[4] == 4); */
+  assert(array_size >= prefix_size);
+  assert(prefix_size >= 0);
+  assert(second[prefix_size] != 6);
+  assert(second[4] == 4);
 
-  /* for(int i = 0; i < prefix_size; i++) */
-  /*   assert(second[i] != prefix[i]); */
   return 0;
 }

regression/snapshot-harness/static-array-float/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+float array[10];
+float *iterator1;
+float *iterator2;
+
+void initialize()
+{
+  array[0] = 1.11;
+  array[8] = 9.999;
+  array[9] = 10.0;
+  iterator1 = (float *)array;
+  iterator2 = &array[9];
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 >= 1.10 && *iterator1 <= 1.12);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == &array[9]);
+  iterator2++;
+  assert(*iterator2 == 0.0);
+
+  return 0;
+}

regression/snapshot-harness/static-array-float/test.desc

@@ -0,0 +1,15 @@
+FUTURE
+main.c
+array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 \>= 1.10 \&\& \*iterator1 \<= 1.12: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == \&array\[9\]: SUCCESS
+\[main.pointer_dereference.13\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator2: FAILURE
+\[main.assertion.4\] line [0-9]+ assertion \*iterator2 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE
+--
+memory analyzer does not yet allow extract floating point values

regression/snapshot-harness/static-array-int/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+int array[10];
+int *iterator1;
+int *iterator2;
+
+void initialize()
+{
+  array[0] = 1;
+  array[8] = 9;
+  array[9] = 10;
+  iterator1 = (int *)array;
+  iterator2 = &array[9];
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*iterator1 == 1);
+  assert(iterator1 != iterator2);
+  assert(iterator2 == &array[9]);
+  iterator2++;
+  assert(*iterator2 == 0);
+
+  return 0;
+}

regression/snapshot-harness/static-array-int/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion iterator1 != iterator2: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion iterator2 == \&array\[9\]: SUCCESS
+\[main.pointer_dereference.13\] line [0-9]+ dereference failure: pointer outside object bounds in \*iterator2: FAILURE
+\[main.assertion.4\] line [0-9]+ assertion \*iterator2 == 0: FAILURE
+VERIFICATION FAILED
+--
+unwinding assertion loop \d+: FAILURE

src/goto-cc/Makefile

@@ -40,15 +40,16 @@ INCLUDES= -I ..
 
 LIBS =
 
-CLEANFILES = goto-cc$(EXEEXT) goto-cl$(EXEEXT)
+CLEANFILES = goto-cc$(EXEEXT) goto-gcc$(EXEEXT) goto-cl$(EXEEXT)
 
 include ../config.inc
 include ../common
 
 ifeq ($(BUILD_ENV_),MSVC)
 all: goto-cl$(EXEEXT)
+else
+all: goto-gcc$(EXEEXT)
 endif
-all: goto-cc$(EXEEXT)
 
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
@@ -57,6 +58,9 @@ endif
 
 ###############################################################################
 
+goto-gcc$(EXEEXT): goto-cc$(EXEEXT)
+	ln -sf goto-cc$(EXEEXT) goto-gcc$(EXEEXT)
+
 goto-cc$(EXEEXT): $(OBJ)
 	$(LINKBIN)
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -207,6 +207,18 @@ size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
     return pointer_depth(t.subtype()) + 1;
 }
 
+bool memory_snapshot_harness_generatort::refers_to(
+  const exprt &expr,
+  const irep_idt &name) const
+{
+  if(expr.id() == ID_symbol)
+    return to_symbol_expr(expr).get_identifier() == name;
+  return std::any_of(
+    expr.operands().begin(),
+    expr.operands().end(),
+    [this, name](const exprt &subexpr) { return refers_to(subexpr, name); });
+}
+
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   const symbol_tablet &snapshot,
   goto_modelt &goto_model) const
@@ -230,8 +242,11 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
     ordered_snapshot_symbols.begin(),
     ordered_snapshot_symbols.end(),
     [this](const snapshot_pairt &left, const snapshot_pairt &right) {
-      return pointer_depth(left.second.symbol_expr().type()) <
-             pointer_depth(right.second.symbol_expr().type());
+      if(refers_to(right.second.value, left.first))
+        return true;
+      else
+        return pointer_depth(left.second.symbol_expr().type()) <
+               pointer_depth(right.second.symbol_expr().type());
     });
 
   code_blockt code;

src/goto-harness/memory_snapshot_harness_generator.h

@@ -244,6 +244,12 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   /// \return pointer depth of type \p t
   size_t pointer_depth(const typet &t) const;
 
+  /// Recursively test pointer reference
+  /// \param expr: expression to be tested
+  /// \param name: name to be located
+  /// \return true if \p expr refers to an object named \p name
+  bool refers_to(const exprt &expr, const irep_idt &name) const;
+
   /// data to store the command-line options
   std::string memory_snapshot_file;
   std::string initial_goto_location_line;