Skip to content

New pointer encoding #6832

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.

Sign up for GitHub

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

Jump to bottom
Open
wants to merge 4 commits into
base: develop
Choose a base branch
from
Open

New pointer encoding #6832

wants to merge 4 commits into from

Conversation

kroening
Copy link
Member

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
src/solvers/smt2/smt2_conv.cpp Outdated
@@ -3151,7 +3151,7 @@ void smt2_convt::convert_mod(const mod_exprt &expr)

void smt2_convt::convert_is_dynamic_object(const unary_exprt &expr)
{
std::vector<std::size_t> dynamic_objects;
std::vector<mp_integer> dynamic_objects;
Copy link
Collaborator

Choose a reason for hiding this comment

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

I believe this change should be part of the earlier commit.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
src/solvers/flattening/bv_pointers.h Outdated
// NOLINTNEXTLINE(readability/identifiers)
typedef boolbvt SUB;

NODISCARD
bvt encode(std::size_t object, const pointer_typet &) const;
bvt encode(const mp_integer &object, const pointer_typet &) const;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should be part of the earlier commit.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
src/solvers/flattening/bv_pointers.cpp
}

bvt bv_pointerst::add_addr(const exprt &expr)
{
std::size_t a=pointer_logic.add_object(expr);
const auto a = pointer_logic.add_object(expr);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Needs to be part of the earlier commit.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
src/solvers/flattening/bv_pointers.cpp
const std::size_t object_bits = get_object_width(type);
const std::size_t max_objects=std::size_t(1)<<object_bits;
const mp_integer object_bits = type.get_width();
const mp_integer max_objects = mp_integer(1) << object_bits;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Not strictly required, but probably better to make this part of the earlier commit.

@kroening
Copy link
Member Author

Pulling out the mp_integer cleanup into #6833.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
CORE thorough-paths broken-smt-backend
KNOWNBUG thorough-paths broken-smt-backend
Copy link
Collaborator

Choose a reason for hiding this comment

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

I believe the "address_space_size_limit*" tests should simply be removed as part this PR.

Copy link
Member Author

Choose a reason for hiding this comment

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

Of course.

tautschnig
tautschnig reviewed Apr 27, 2022
View reviewed changes
regression/cbmc-library/fprintf-01/test.desc Outdated
@@ -1,4 +1,4 @@
CORE
KNOWNBUG
Copy link
Collaborator

Choose a reason for hiding this comment

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

Any idea why this test is newly broken? I can see the reason for the ones doing integer addresses, but this one seems more surprising.

Copy link
Member Author

Choose a reason for hiding this comment

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

No, that one is puzzling me.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Is it a problem that stdout and stderr are non-deterministic pointers?

Copy link
Member Author

@kroening kroening Apr 28, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

Probably. Broadly, I see three kinds of failing tests:

  • The desired effect of removing the limits on objects and offsets. Test should change or be removed.
  • Nondeterminism that now gets resolved in a different way. I.e., the test should be fixed. This one might be in this category.
  • The lack of support for the "integer pointers". Need to think about this one.

@kroening kroening force-pushed the pointer-encoding branch 3 times, most recently from 650d895 to 76cffd1 Compare April 28, 2022 16:47
@kroening kroening marked this pull request as ready for review April 28, 2022 18:01
@tautschnig
Copy link
Collaborator

Is it worth factoring out the first commit into a PR of its own while this one remains work in progress?

kroening added 4 commits April 28, 2022 22:59
@kroening
bv_utilst::sign_extension, zero_extension and zeros can be static
ed2a9fa 
These methods do not use any state of bv_utilst and can therefore be static.
@kroening
new pointer encoding
1ba8148 
This changes the encoding of pointers in the flattening solver as follows:

* Pointers with constant zero offset are encoded by numbering the object (0
  is the NULL object).

* Pointers that might have an offset are numbered, and encoded/decoded as
  needed.  The numbering points into a table, which records an n-bit object
  and n-bit offset for an n-bit pointer.

The key benefit of the encoding above are that a) offset arithmetic no
longer overflows before the given width of the pointer is reached, b) the
full width of the pointer (usually 32 or 64 bits) can be used to encode the
object number, thereby eliminating the requirement to configure the number
of 'object bits'.
@kroening
pointer encoding: tests changed
b08c997
@kroening
re-encode integers converted to pointers
6f42b0e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig left review comments

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
enhancement new feature
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@kroening @tautschnig