Skip to content

Dynamic memory snapshot #4578

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 17 commits into from
May 30, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/memory-analyzer/pointer_03/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ CORE
main.gb
--breakpoint checkpoint --symbols x,p
x = 3;
p = &x;
p = \(void \*\)\&x;
^EXIT=0$
^SIGNAL=0$
5 changes: 2 additions & 3 deletions regression/memory-analyzer/pointer_to_struct_01/test.desc
Original file line number Diff line number Diff line change
@@ -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;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

^EXIT=0$
^SIGNAL=0$
5 changes: 2 additions & 3 deletions regression/memory-analyzer/structs_02/test.desc
Original file line number Diff line number Diff line change
@@ -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$
28 changes: 28 additions & 0 deletions regression/snapshot-harness/arrays_02/main.c
Original file line number Diff line number Diff line change
@@ -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);
}
11 changes: 11 additions & 0 deletions regression/snapshot-harness/arrays_02/test.desc
Original file line number Diff line number Diff line change
@@ -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
47 changes: 47 additions & 0 deletions regression/snapshot-harness/dynamic-array-int/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
16 changes: 16 additions & 0 deletions regression/snapshot-harness/dynamic-array-int/test.desc
Original file line number Diff line number Diff line change
@@ -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
12 changes: 4 additions & 8 deletions regression/snapshot-harness/pointer-to-array-int/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
32 changes: 32 additions & 0 deletions regression/snapshot-harness/static-array-float/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
15 changes: 15 additions & 0 deletions regression/snapshot-harness/static-array-float/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
FUTURE
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added.

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
32 changes: 32 additions & 0 deletions regression/snapshot-harness/static-array-int/main.c
Original file line number Diff line number Diff line change
@@ -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;
}
13 changes: 13 additions & 0 deletions regression/snapshot-harness/static-array-int/test.desc
Original file line number Diff line number Diff line change
@@ -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
8 changes: 6 additions & 2 deletions src/goto-cc/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you please change the lines above so that this is within an else/endif instead of being done for MSVC as well? Furthermore, please add goto-gcc$(EXEEXT) to CLEANFILES above.

endif
all: goto-cc$(EXEEXT)

ifneq ($(wildcard ../jsil/Makefile),)
OBJ += ../jsil/jsil$(LIBEXT)
Expand All @@ -57,6 +58,9 @@ endif

###############################################################################

goto-gcc$(EXEEXT): goto-cc$(EXEEXT)
ln -sf goto-cc$(EXEEXT) goto-gcc$(EXEEXT)

goto-cc$(EXEEXT): $(OBJ)
$(LINKBIN)

Expand Down
19 changes: 17 additions & 2 deletions src/goto-harness/memory_snapshot_harness_generator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you explain what this is for?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

return true;
else
return pointer_depth(left.second.symbol_expr().type()) <
pointer_depth(right.second.symbol_expr().type());
});

code_blockt code;
Expand Down
6 changes: 6 additions & 0 deletions src/goto-harness/memory_snapshot_harness_generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading