is_invalid_pointer is now defined as a bi-implication #6366

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

kroening wants to merge 1 commit into develop from invalid_pointers

Member

kroening commented Sep 25, 2021

The previous encoding of is_invalid_pointer is an implication,
which means that constraints that a pointer is not an invalid
pointer have no meaning.

This commit changes the encoding to be a bi-implication, using
the numerical range of the valid pointers.

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.
n/a 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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

kroening force-pushed the invalid_pointers branch 2 times, most recently from a6542e7 to afd2d09 Compare

September 25, 2021 16:59

codecov bot commented Sep 25, 2021 •

edited

Loading

Codecov Report

Merging #6366 (c9a22ab) into develop (af94148) will increase coverage by 0.00%.
The diff coverage is 89.28%.

@@           Coverage Diff            @@
##           develop    #6366   +/-   ##
========================================
  Coverage    75.97%   75.97%           
========================================
  Files         1523     1523           
  Lines       164191   164196    +5     
========================================
+ Hits        124748   124754    +6     
+ Misses       39443    39442    -1

Impacted Files	Coverage Δ
src/goto-instrument/dot.cpp	`0.00% <0.00%> (ø)`
src/goto-programs/goto_program.h	`90.49% <ø> (+0.21%)`	⬆️
src/solvers/flattening/pointer_logic.cpp	`89.61% <ø> (-0.14%)`	⬇️
src/solvers/flattening/pointer_logic.h	`80.00% <ø> (-5.72%)`	⬇️
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/goto-symex/symex_main.cpp	`86.00% <60.00%> (+0.03%)`	⬆️
src/goto-analyzer/taint_analysis.cpp	`78.21% <75.00%> (-0.22%)`	⬇️
src/goto-instrument/goto_program2code.cpp	`69.33% <87.50%> (+0.12%)`	⬆️
src/goto-programs/remove_virtual_functions.cpp	`92.85% <100.00%> (+0.04%)`	⬆️
src/goto-programs/restrict_function_pointers.cpp	`82.20% <100.00%> (ø)`
... and 3 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 038a53b...c9a22ab. Read the comment docs.

kroening force-pushed the invalid_pointers branch 6 times, most recently from ff64c00 to ea71734 Compare

September 26, 2021 07:23

kroening marked this pull request as ready for review

September 26, 2021 08:03

kroening requested review from allredj, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners

September 26, 2021 08:03

feliperodri added the aws label

Collaborator

feliperodri commented Sep 26, 2021

@SaswatPadhi @jimgrundy @remi-delmas-3000

jimgrundy added the aws-high label

TGWDB approved these changes

View reviewed changes

tautschnig previously approved these changes

View reviewed changes

Collaborator

tautschnig left a comment

Is there any data on how much slower things get in practice?

regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc

               main.c
               --pointer-check
               ^EXIT=0$
               ^SIGNAL=0$
               ^VERIFICATION SUCCESSFUL$
               --
-              ^warning: ignoring

Collaborator

tautschnig Oct 7, 2021

Why is this pattern being removed?

regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc

               main.c
               --pointer-check --no-simplify --no-propagation
               ^EXIT=0$
               ^SIGNAL=0$
               ^VERIFICATION SUCCESSFUL$
               --
-              ^warning: ignoring

Collaborator

tautschnig Oct 7, 2021

Why is this pattern being removed?

regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc

               main.c
               --pointer-check
               ^EXIT=0$
               ^SIGNAL=0$
               ^VERIFICATION SUCCESSFUL$
               --
-              ^warning: ignoring

Collaborator

tautschnig Oct 7, 2021

Why is this pattern being removed?

regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc

               main.c
               --pointer-check --no-simplify --no-propagation
               ^EXIT=0$
               ^SIGNAL=0$
               ^VERIFICATION SUCCESSFUL$
               --
-              ^warning: ignoring

Collaborator

tautschnig Oct 7, 2021

Why is this pattern being removed?

regression/cbmc-primitives/r_w_ok_bug/test.desc

               ^SIGNAL=0$
               --
-              ^warning: ignoring

Collaborator

tautschnig Oct 7, 2021

Why is this pattern being removed?

tautschnig assigned kroening

SaswatPadhi mentioned this pull request

enable nondeterministic pointers #6326

Merged

4 tasks


          is_invalid_pointer is now defined as a bi-implication

c9a22ab

The previous encoding of is_invalid_pointer is an implication,
which means that constraints that a pointer is not an invalid
pointer have no meaning.

This commit changes the encoding to be a bi-implication, using
the numerical range of the valid pointers.

kroening force-pushed the invalid_pointers branch from ea71734 to c9a22ab Compare

October 19, 2021 14:58

feliperodri added the do not merge label

Collaborator

tautschnig commented Apr 14, 2022

Returning to this after some time. A bunch of thoughts:

[SV-COMP'18 11/19] invalid_object(pointer) is true for all non-existent objects #2000 previously proposed a similar solution, but was rejected in out-of-band communication with @kroening for it would be incompatible with incrementally adding objects. Doesn't this problem exist here as well?
An aspect that [SV-COMP'18 11/19] invalid_object(pointer) is true for all non-existent objects #2000 tried to tackle in addition to what is covered here are objects that symex created, yet the path condition of which isn't true. [SV-COMP'18 11/19] invalid_object(pointer) is true for all non-existent objects #2000 specifically did this for dynamic objects, but the same would actually apply to stack-allocated data. I would therefore like to ask: should "is invalid object" also be true for objects the life span of which hasn't yet begun?
As a possible alternative to address concern 1) above: make "is invalid object" evaluate to false for any known object, but don't specify a value for all other cases. This permits adding constraints in subsequent solver calls.

Collaborator

jimgrundy commented Apr 16, 2022

@tautschnig suggests above

As a possible alternative to address concern 1) above: make "is invalid object" evaluate to false for any known object, but don't specify a value for all other cases. This permits adding constraints in subsequent solver calls.

Does that take us back to being an implication rather than an equivalence, and were we trying to get away from that?

Also, if this is an equivalence, can we please invert the sense and change the name to "is_valid_pointer". It's confusing to have to say that a pointer is valid by saying that it is not invalid.

Collaborator

tautschnig commented Apr 17, 2022

@tautschnig suggests above

As a possible alternative to address concern 1) above: make "is invalid object" evaluate to false for any known object, but don't specify a value for all other cases. This permits adding constraints in subsequent solver calls.

Does that take us back to being an implication rather than an equivalence, and were we trying to get away from that?

It should be noted that the existing implementation (prior to the changes proposed in this PR) was a bi-implication on the object that is singled out as the "invalid" object. Therefore, "is invalid object" (at present) has to be read as "is the invalid object," and not "is not a valid object." It may well be that we should ...

Also, if this is an equivalence, can we please invert the sense and change the name to "is_valid_pointer". It's confusing to have to say that a pointer is valid by saying that it is not invalid.

... keep the current is_invalid_object as-is and instead make the implementation proposed in this PR back a new primitive "is_valid_object" (we shouldn't use "is_valid_pointer," because then we'd also have to check pointer offsets).

Collaborator

jimgrundy commented Apr 17, 2022

... keep the current is_invalid_object as-is and instead make the implementation proposed in this PR back a new primitive "is_valid_object" (we shouldn't use "is_valid_pointer," because then we'd also have to check pointer offsets).

Agree about calling the proposed thing "is_valid_object" (not "is_valid_pointer") for sure.

What would keeping the current "is_invalid_object" do? Would it still track a single distinguished invalid object? Or would it be the negation of "is_valid_object". Is the motivation to keep it to avoid breaking existing code or is there another reason to have "is_invalid_object" kept around?

Member Author

kroening commented Apr 18, 2022

I think we need a proper 'object factory' facility!

feliperodri assigned tautschnig

feliperodri added aws-medium and removed aws-high labels

tautschnig dismissed their stale review

October 19, 2022 11:26

Revoking my approval as the solution likely is not the right one to address the user request.

Collaborator

tautschnig commented Oct 19, 2022

Some notes as @kroening and myself discussed this out of band: the proposed approach may have a substantial performance penalty. This may be fixed by making improvements to post-processing, but even then is_invalid_pointer will not necessarily be what a user even wants: 1) use within assumptions requires a proper object factory as noted above, assumptions over !is_invalid_pointer are not the right approach; 2) is_invalid_pointer does not match the informal understanding of an "invalid" pointer, but really just says that the pointed-to object is CBMC's internal "invalid object."

tautschnig removed their assignment

jimgrundy removed the aws-medium label

Collaborator

jimgrundy commented Oct 21, 2022

This one doesn't seem like the way to go. Should we close it to declutter?

Collaborator

feliperodri commented Nov 7, 2022

This one doesn't seem like the way to go. Should we close it to declutter?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

TGWDB TGWDB approved these changes

tautschnig tautschnig left review comments

allredj Awaiting requested review from allredj

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

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

romainbrenguier Awaiting requested review from romainbrenguier

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

Labels

aws do not merge