Dynamic memory snapshot #4578

xbauch · 2019-04-27T07:21:37Z

Enable tracking information about dynamically allocated memory from memory-analyzer across to goto-harness via memory snapshots. The knowledge about what addresses have been allocated dynamically (and the scope of these allocation in byte size) is collected by breaking the execution at malloc call-sites and inspecting the registers of these function calls.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

hannes-steffenhagen-diffblue

Looks ok to me (with the disclaimer that I don't really understand this)

hannes-steffenhagen-diffblue · 2019-04-29T14:25:04Z

src/memory-analyzer/analyze_symbol.cpp

+bool gdb_value_extractort::memory_scopet::contains(
+  const memory_addresst &point) const
+{
+  size_t begin_int = std::strtoul(begin.address_string.c_str(), NULL, 0);


This is a unchecked conversion effectively (size_t is not necessarily the same size as unsigned long, even though it's often the case). I'd recommend using safe_string2size_t from string2int.h (same with all the other string to int conversions here).

I wasn't sure if the safe-conversion would work on hex-numbers.

They should, they use stoll which basically works the same way as the str* functions except it's easier to detect failures.

Done and refactored so that the conversion is computed once in case of distance. See: 3812c28.

hannes-steffenhagen-diffblue · 2019-04-29T14:26:21Z

src/memory-analyzer/analyze_symbol.h

@@ -91,6 +91,70 @@ class gdb_value_extractort
  ///   value of `symbol`.
  std::map<memory_addresst, exprt> values;

+  struct memory_scopet
+  {
+    memory_addresst begin;


Why not private, if these are not arbitrary (as the deleted default constructor implies)?

Done, also added getters when necessary.

hannes-steffenhagen-diffblue · 2019-04-29T14:31:25Z

src/memory-analyzer/analyze_symbol.h

+  optionalt<mp_integer> get_malloc_size(irep_idt name);
+
+  /// Build the pointee string for address \p point assuming it points to a
+  ///   dynamic allocation of `n' elements each of size \p member_size. E.g.:


what's n here?

T* point = (T*) malloc(sizeof(T) * n); .. that n.

hannes-steffenhagen-diffblue · 2019-04-29T14:33:34Z

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -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))


Can you explain what this is for?

For example, say int* p = malloc(8); int *q = p+1; is the source code for which we want to take the memory snapshot. Then the snapshot will contain: int tmp[2]; int* p = tmp[0]; int* q = tmp[1]; And both p and q refer_to tmp. I sort the symbols based on this notion of reference so that when building the harness entry function, tmp is assigned before the two pointers.

hannes-steffenhagen-diffblue · 2019-04-29T14:49:17Z

src/memory-analyzer/gdb_api.h

-    const std::string pointee;
-    const std::string character;
-    const optionalt<std::string> string;
+    memory_addresst address;


These fields are all related, so I don't think they should be both be constant and public at the same time.

Well they are not const in the final version.

hannes-steffenhagen-diffblue · 2019-04-29T14:59:18Z

src/memory-analyzer/analyze_symbol.cpp

 {
  if(pointer_value.pointee.find("+") != std::string::npos)
    return true;

+  if(pointer_value.pointee.empty())


why is this only done if the pointee is empty? What does that mean?

Well pointer_value is the result of the gdb query get_memory. When the pointee is empty it means that gdb did not know what structure the pointer points to. This can happen if the pointer points to inside a dynamically allocated memory.

tautschnig · 2019-05-05T15:05:48Z

src/memory-analyzer/analyze_symbol.cpp

+bool gdb_value_extractort::memory_scopet::contains(
+  const memory_addresst &point) const
+{
+  size_t begin_int = std::strtoul(begin.address_string.c_str(), NULL, 0);


tautschnig · 2019-05-05T15:06:13Z

src/memory-analyzer/analyze_symbol.h

+    memory_scopet() = delete;
+    memory_scopet(
+      const memory_addresst &begin,
+      mp_integer byte_size,


const mp_integer &byte_size

tautschnig · 2019-05-05T15:06:28Z

src/memory-analyzer/analyze_symbol.h

+    memory_scopet(
+      const memory_addresst &begin,
+      mp_integer byte_size,
+      irep_idt name)


const irep_idt &name

tautschnig · 2019-05-05T15:07:05Z

src/memory-analyzer/analyze_symbol.cpp

+  CHECK_RETURN(contains(point));
+  size_t begin_int = std::strtoul(begin.address_string.c_str(), NULL, 0);
+  size_t point_int = std::strtoul(point.address_string.c_str(), NULL, 0);
+  return (point_int - begin_int) / member_size;


Shouldn't you first do CHECK_RETURN(point_int >= begin_int);?

That was implied by contains. But I refactored this section a bit to avoid duplicate computation of the address-to-string conversion. See: 3812c28.

tautschnig · 2019-05-05T15:08:31Z

src/memory-analyzer/analyze_symbol.h

+    mp_integer byte_size;
+    irep_idt name;
+
+    memory_scopet() = delete;


I'm not sure that's necessary if you explicitly define some other constructor?

You are right. Removed.

tautschnig · 2019-05-05T15:19:35Z

src/memory-analyzer/analyze_symbol.cpp

  }

  const auto it = values.find(memory_location);
  // if the structure we are pointing to does not exists we need to build a
  // temporary object for it: get the type from symbol table, query gdb for
  // value, allocate new object for it and then store into assignments
  if(it == values.end())
+  if(struct_symbol->symbol_expr().type().id() == ID_pointer)


This looks very weird?!

What about struct_symbol->type.id() ? Changed.

tautschnig · 2019-05-05T15:19:49Z

src/memory-analyzer/analyze_symbol.cpp

@@ -303,6 +303,7 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
  }

  if(!found)
+  if(struct_symbol->symbol_expr().type().id() == ID_array)


Looks weird!?

tautschnig · 2019-05-05T15:20:45Z

src/memory-analyzer/analyze_symbol.cpp

@@ -291,6 +291,8 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
  bool found = false;
  CHECK_RETURN(maybe_struct_size.has_value());
  for(const auto &value_pair : values)
+
+  if(memory_map.count(struct_name) == 0)


This looks weird.

Wrapped in a helper function has_known_memory_location.

tautschnig · 2019-05-05T15:23:39Z

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

@@ -0,0 +1,13 @@
+FUTURE


Please explain (after another -- at the end of the file) what isn't supported here so far.

tautschnig · 2019-05-05T15:25:24Z

regression/memory-analyzer/pointer_to_struct_01/test.desc

-tmp = \{ \.next=\(\(struct S \*\)0\) \};
-p = \&tmp;
+st = \{ .next=\&st \};
+p = \&st;


Could you please squash this into the commit that made this possible?

It was this one: 33d0a79. I will squash them together.

tautschnig · 2019-05-29T17:38:26Z

@xbauch My apologies for taking this long! You might want to squash some commits and then just merge. Thank you for all the work!!!

tautschnig · 2019-05-30T07:47:46Z

@xbauch Please rebase now that #4729 is in to make CI happy.

In memory-snapshot-harness: so that pointer to objects are initialised after those objects.

no functional change

So that we can assume the implicit assignment operator.

One for value, one for register-value.

by breaking the execution at malloc entry and extracting the byte size and memory address from registers.

by returning the exact value rather than an estimate collected during preceding execution.

memory_scopet keeps the starting point and allocated size for a malloc(ed) site. We also include helper methods to query about dynamic allocation.

To account for the possibility of the pointee to be dynamically allocated.

Via dynamically_allocated and memory_map.

into a member method.

Unnecessary now that we enforce analysing those objects.

1: If pointee is known, return it's value instead. 2: malloc-size is precise and type-size has a wrapper 3: do not cast values from dynamically allocated pointers: we would loose the information about them being arrays.

1: Use memory map to get pointer-values (but double-check if gdb previously claimed that their pointees are themselves) 2: add more checks before casting.

instead of a vector to prevent duplications.

1: Casts are a part of the output 2: We can use some of the assertions previously left out (now that we get the dynamic allocation right).

Floating point numbers cannot be extracted for now.

rather than as a part of regression testing and only under non-MSVC environment.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ba8beb5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113721650

xbauch added the dependent - do not merge label Apr 27, 2019

xbauch marked this pull request as ready for review April 29, 2019 14:15

xbauch requested review from chrisr-diffblue, danpoe, forejtv, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners April 29, 2019 14:15

hannes-steffenhagen-diffblue approved these changes Apr 29, 2019

View reviewed changes

tautschnig reviewed May 5, 2019

View reviewed changes

tautschnig assigned xbauch May 5, 2019

xbauch force-pushed the feature/dynamic-memory-snapshot branch from d803707 to 3812c28 Compare May 8, 2019 09:22

xbauch mentioned this pull request May 17, 2019

User controlled havoc(ing) for memory-snapshot harness #4482

Merged

7 tasks

xbauch added Needs rebase and removed dependent - do not merge labels May 20, 2019

xbauch changed the title ~~Dynamic memory snapshot [depends-on: #4482]~~ Dynamic memory snapshot May 20, 2019

xbauch force-pushed the feature/dynamic-memory-snapshot branch from 3812c28 to 71ee2f1 Compare May 20, 2019 13:35

xbauch removed the Needs rebase label May 20, 2019

xbauch force-pushed the feature/dynamic-memory-snapshot branch 7 times, most recently from 785cf3a to 410fd84 Compare May 21, 2019 18:41

tautschnig assigned xbauch and unassigned tautschnig May 29, 2019

xbauch force-pushed the feature/dynamic-memory-snapshot branch 3 times, most recently from 89f8805 to 5453ba7 Compare May 30, 2019 05:45

xbauch pushed a commit to xbauch/cbmc that referenced this pull request May 30, 2019

Squashed commit from prerequisite PR diffblue#4578 -- Do not review here

70c3554

xbauch mentioned this pull request May 30, 2019

Extract function pointers using memory analyzer #4730

Merged

7 tasks

petr-bauch added 17 commits May 30, 2019 09:03

Fix the ordering in which symbols are initialised

221a7ae

In memory-snapshot-harness: so that pointer to objects are initialised after those objects.

Add documentation to gdb api

c1a65c4

no functional change

Un-constify pointer_valuet data

b4ebeff

So that we can assume the implicit assignment operator.

Helpers to extract values from gdb record

4807320

One for value, one for register-value.

Collecting the malloc information directly

e1b446b

by breaking the execution at malloc entry and extracting the byte size and memory address from registers.

Reimplement query-malloc-size

43cb772

by returning the exact value rather than an estimate collected during preceding execution.

Introduce facilities for tracking dynamically allocated memory

22368b0

memory_scopet keeps the starting point and allocated size for a malloc(ed) site. We also include helper methods to query about dynamic allocation.

Re-implement points_to_member query

dff2162

To account for the possibility of the pointee to be dynamically allocated.

Initialise the databases for dynamic allocation and known symbols

a20ee20

Via dynamically_allocated and memory_map.

Wrap extracting the type size

3113c15

into a member method.

Remove building dummies for pointee objects

3950c99

Unnecessary now that we enforce analysing those objects.

Refactor get-pointer-to-member-value

46ac404

1: If pointee is known, return it's value instead. 2: malloc-size is precise and type-size has a wrapper 3: do not cast values from dynamically allocated pointers: we would loose the information about them being arrays.

Refactor get-pointer-value

23f02fb

1: Use memory map to get pointer-values (but double-check if gdb previously claimed that their pointees are themselves) 2: add more checks before casting.

Make the assignments into a map

5712386

instead of a vector to prevent duplications.

Update older tests

8ef9155

1: Casts are a part of the output 2: We can use some of the assertions previously left out (now that we get the dynamic allocation right).

More tests for static and dynamic arrays

e01e0df

Floating point numbers cannot be extracted for now.

Build goto-gcc during compilation

ba8beb5

rather than as a part of regression testing and only under non-MSVC environment.

xbauch force-pushed the feature/dynamic-memory-snapshot branch from 2ab16c4 to ba8beb5 Compare May 30, 2019 08:04

xbauch merged commit 97f1619 into diffblue:develop May 30, 2019

allredj reviewed May 30, 2019

View reviewed changes

xbauch deleted the feature/dynamic-memory-snapshot branch June 10, 2019 12:30

Dynamic memory snapshot #4578

Dynamic memory snapshot #4578

Conversation

xbauch commented Apr 27, 2019 • edited Loading

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented May 29, 2019

tautschnig commented May 30, 2019

allredj left a comment

Choose a reason for hiding this comment

xbauch commented Apr 27, 2019 •

edited

Loading