Memory analyzer to take memory snapshots [blocks: #2649, #4438] #4261

danpoe · 2019-02-22T18:01:41Z

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).
n/a 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.

xbauch · 2019-02-24T16:38:10Z

src/util/c_types_util.h

+
+/// \file
+/// This file contains functions, that should support test for underlying
+/// c types, in cases where this is required for anlysis purpose.


xbauch · 2019-02-24T16:40:45Z

src/util/c_types_util.h

+  return type.id() == ID_c_bool;
+}
+
+/// This function checks, whether the type is has been some kind of integer


is has been -> has been

xbauch · 2019-02-24T16:43:45Z

src/util/c_types_util.h

+/// \param c_enum the enum type memeber_name is supposed to be part of.
+/// \return value a constant, that could be assigned as value for an expression
+/// with type c_enum.
+constant_exprt convert_memeber_name_to_enum_value(


xbauch · 2019-02-24T16:44:29Z

src/util/c_types_util.h

+/// This function creates a constant representing the
+/// bitvector encoded integer value of a string in the enum.
+/// \param member_name is a string that should be in the enum.
+/// \param c_enum the enum type memeber_name is supposed to be part of.


\p member_name

xbauch · 2019-02-24T16:47:39Z

src/util/c_types_util.h

+  {
+    if(id2string(enum_value.get_identifier()) == member_name)
+    {
+      mp_integer int_value = string2integer(id2string(enum_value.get_value()));


Could this the call the safe version returning optionalt?

This should just be numeric_cast<mp_integer>(enum_value.get_value()) I think

This is just trying to convert constants between different types - I think we might have a function for that already, but I'm not sure

xbauch · 2019-02-24T16:51:30Z

src/util/c_types_util.h

+/// bitvector encoded integer value of a string in the enum.
+/// \param member_name is a string that should be in the enum.
+/// \param c_enum the enum type memeber_name is supposed to be part of.
+/// \return value a constant, that could be assigned as value for an expression


This sounds strange.

xbauch · 2019-03-06T10:28:36Z

src/memory-analyzer/memory_analyzer_parse_options.cpp

+    << " --breakpoint <breakpoint>    analyze from breakpoint\n"
+    << " --symbols <symbol-list>      list of symbols to analyze\n"
+    << " --symtab-snapshot            output snapshot as symbol table\n"
+    << " --output-file <file>         write snapshot to file\n"


Could we add a --json-ui here, since it's somewhat useful for goto-harness?

Currently we have the option --symtab-snapshot which outputs the memory snapshot in json format.

$ ../../../build/bin/memory-analyzer --symtab-snapshot --breakpoint checkpoint --symbols array main_exe Symbols: Symbol......: __CPROVER_size_t Pretty name.: __CPROVER_size_t Module......: main Base name...: __CPROVER_size_t Mode........: C Type........: __CPROVER_size_t Value.......: Flags.......: thread_local file_local type macro Location....: file <built-in-additions> line 1 Symbol......: array Pretty name.: array Module......: main Base name...: array Mode........: C Type........: signed int [3l] Value.......: { 1, 4, 3 } Flags.......: lvalue static_lifetime Location....: file main.c line 5

Am I using it wrong?

Oh, you're right. --json-ui is indeed needed and missing from the help section.

GDB API [blocks: #4261]

allredj

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

tautschnig · 2019-05-15T13:27:15Z

I'll leave merging to @danpoe or @xbauch to do some squashing (or consider it too much overhead and just merge straight away).

This code takes a static symbol, zero initalizes the typet of the symbol and then fills it up with values if possible. Following the declared structure in the typet, the analyzer queries the gdb api for values of the attributes of typet. It the symbol is a primtive type, the analyzer directly queries for the value of the symbol.

These test have been used as driving example for the memory analyzer. They test basic functionality and handling of cycles in structs.

This adds an updated chain.sh file, and disables the existing regression tests. They currently fail due to two issues: goto code to c conversion currently ignores array sizes (i.e., even int arrays of known sizes are output as int[]), and void pointers are not handled (i.e., analyze_symbol() may try to zero initialize an object of type void, yielding an invariant violation).

This update the gdb api to return more information about pointers (via the method get_memory() which returns an object of type pointer_valuet describing the pointer and pointed-to data). Unit tests for the new functionality are included.

…pr.h A previous commit introduced e.g. function is_pointer() to check type.id() == ID_pointer. These have become obsolete as these expressions are now used directly.

This updates the symbol analyzer which is used by the memory analyzer. The class is refactored and updated to use the new gdb api.

We were doing this in multiple places, this should make it a bit easier to keep set properties consistent among different places. Ideally we could eventually move away from mentioning targets from modules here on the top level (and instead have each module call cprover_default_properties) but this isn't done in this commit. Because memory analyzer depends on GDB being present and further uses platform specific functionality at the moment it had some ifdef functionality to disable itself. This made the code a bit more complicated than it needed to be, and also lead to the code effectively building defunct executables. This removes these ifdefs and instead excludes memory-analyzer (and related tests) from the build unless requested (via WITH_MEMORY_ANALYZER environment variable or CMake option depending on whether it is a Make or CMake build respectively). Also force building memory-analyzer on Linux and test it there by default (unless explicitly unset). Behaviour on other platforms should be preserved.

and update the chain script accordingly.

mostly the description and expected output.

mostly white spaces and cprover_default_properties.

Add memory_addresst and documentation.

Better names and small code refactoring.

and add documentation.

Remove ui_message_handler dependence, fix header, etc.

to the new interface.

to CPROVER manual.

allredj

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

danpoe requested review from chrisr-diffblue, forejtv, kroening, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners February 22, 2019 18:01

danpoe added the dependent - do not merge label Feb 22, 2019

danpoe changed the title ~~Memory analyzer to take memory snapshots~~ Memory analyzer to take memory snapshots [depends-on: #3983] Feb 22, 2019

danpoe added the do not review label Feb 22, 2019

xbauch reviewed Feb 24, 2019

View reviewed changes

tautschnig mentioned this pull request Feb 25, 2019

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

Closed

tautschnig assigned danpoe Feb 26, 2019

tautschnig mentioned this pull request Feb 27, 2019

Add array initialisation support in default goto-harness. #4234

Merged

7 tasks

xbauch reviewed Mar 6, 2019

View reviewed changes

xbauch mentioned this pull request Mar 12, 2019

Memory snapshot harness havoc #4351

Merged

7 tasks

chrisr-diffblue self-assigned this Mar 19, 2019

danpoe added a commit that referenced this pull request Mar 19, 2019

Merge pull request #3983 from danpoe/feature/gdb-api

6533631

GDB API [blocks: #4261]

chrisr-diffblue removed dependent - do not merge do not review labels Mar 19, 2019

chrisr-diffblue changed the title ~~Memory analyzer to take memory snapshots [depends-on: #3983]~~ Memory analyzer to take memory snapshots Mar 19, 2019

danpoe force-pushed the feature/memory-analyzer branch 3 times, most recently from 32a410e to 9be9e7f Compare March 20, 2019 11:07

allredj reviewed May 15, 2019

View reviewed changes

tautschnig assigned danpoe and xbauch and unassigned peterschrammel and chrisr-diffblue May 15, 2019

mmuesly and others added 19 commits May 16, 2019 10:58

Add regression tests for the memory analyzer

46ca388

These test have been used as driving example for the memory analyzer. They test basic functionality and handling of cycles in structs.

Add Makefiles enabeling memory-analyzer and tests

767a385

Remove obsolete functions is_pointer(), is_struct(), etc. from std_ex…

c4e560e

…pr.h A previous commit introduced e.g. function is_pointer() to check type.id() == ID_pointer. These have become obsolete as these expressions are now used directly.

Update memory analyzer driver and options parsing

6bdd7bf

Update symbol_analyzert

72809e5

This updates the symbol analyzer which is used by the memory analyzer. The class is refactored and updated to use the new gdb api.

Add additional regression tests for the memory analyzer

c70540c

Add support for running regression tests under CMake

9f88304

and update the chain script accordingly.

Improve the regression tests

98816c2

mostly the description and expected output.

Improve building scripts

ac4cd65

mostly white spaces and cprover_default_properties.

Improve gdb_api

af27d1f

Add memory_addresst and documentation.

Improve type utility functions

2fddd15

Better names and small code refactoring.

Refactor analyze_symbols

554a166

and add documentation.

Improve memory_analyzer parser and main

6565c4b

Remove ui_message_handler dependence, fix header, etc.

Update unit test

9703af1

to the new interface.

Add User level documentation

35abeee

to CPROVER manual.

danpoe force-pushed the feature/memory-analyzer branch from c19aa7b to 35abeee Compare May 16, 2019 11:01

danpoe mentioned this pull request May 16, 2019

Memory analyzer squash danpoe/cbmc#10

Closed

allredj reviewed May 16, 2019

View reviewed changes

tautschnig merged commit 09875c3 into diffblue:develop May 16, 2019

danpoe deleted the feature/memory-analyzer branch June 2, 2020 17:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Memory analyzer to take memory snapshots [blocks: #2649, #4438] #4261

Memory analyzer to take memory snapshots [blocks: #2649, #4438] #4261

Uh oh!

danpoe commented Feb 22, 2019 •

edited

Loading

Uh oh!

xbauch Feb 24, 2019

Uh oh!

xbauch Feb 24, 2019

Uh oh!

xbauch Feb 24, 2019

Uh oh!

xbauch Feb 24, 2019

Uh oh!

xbauch Feb 24, 2019

Uh oh!

hannes-steffenhagen-diffblue Mar 22, 2019

Uh oh!

xbauch Feb 24, 2019

Uh oh!

xbauch Mar 6, 2019

Uh oh!

danpoe Mar 6, 2019 •

edited

Loading

Uh oh!

xbauch Mar 6, 2019

Uh oh!

danpoe Mar 6, 2019

Uh oh!

allredj left a comment

Uh oh!

tautschnig commented May 15, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Memory analyzer to take memory snapshots [blocks: #2649, #4438] #4261

Memory analyzer to take memory snapshots [blocks: #2649, #4438] #4261

Uh oh!

Conversation

danpoe commented Feb 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danpoe Mar 6, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented May 15, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Feb 22, 2019 •

edited

Loading

danpoe Mar 6, 2019 •

edited

Loading