Permit re-setting --object-bits #7858

tautschnig · 2023-08-18T17:21:44Z

Support choosing the number of object bits to be used by CBMC at runtime even with pre-compiled goto binaries.

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.
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.

codecov · 2023-08-21T15:12:38Z

Codecov Report

Attention: Patch coverage is 98.57143% with 1 lines in your changes are missing coverage. Please review.

Project coverage is 78.34%. Comparing base (1ed7b2f) to head (97e2439).

Files	Patch %	Lines
src/goto-instrument/nondet_static.cpp	91.66%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7858      +/-   ##
===========================================
- Coverage    78.38%   78.34%   -0.05%     
===========================================
  Files         1720     1720              
  Lines       187982   188100     +118     
  Branches     18474    18508      +34     
===========================================
+ Hits        147346   147358      +12     
- Misses       40636    40742     +106

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

kroening · 2023-08-28T12:14:05Z

The title of the PR is a bit misleading -- this moves the setting of object bits from goto-cc (or the front-end) to the solver.

This is the right thing to do (the only better thing is to get rid of object bits altogether).

This is a change of user-visible behaviour, and needs to be advertised appropriately.

tautschnig · 2023-08-29T18:23:10Z

The title of the PR is a bit misleading -- this moves the setting of object bits from goto-cc (or the front-end) to the solver.

I'm all up for changing the title -- I just thought a key problem that, with the previous implementation, GOTO binaries had their object bits firmly set. Now, one can use different values with cbmc --object-bits ... on a single GOTO binary.

This is the right thing to do (the only better thing is to get rid of object bits altogether).

This is a change of user-visible behaviour, and needs to be advertised appropriately.

Yes, this is user-visible -- but we hadn't really documented that undesirable need of setting --object-bits via goto-ccit seems?! Any suggestions on how to best document this change?

kroening · 2023-08-29T18:53:41Z

The title of the PR is a bit misleading -- this moves the setting of object bits from goto-cc (or the front-end) to the solver.

I'm all up for changing the title -- I just thought a key problem that, with the previous implementation, GOTO binaries had their object bits firmly set. Now, one can use different values with cbmc --object-bits ... on a single GOTO binary.

After the change, is it still possible to set object-bits via goto-cc? If not, then it's moving!

Yes, this is user-visible -- but we hadn't really documented that undesirable need of setting --object-bits via goto-ccit seems?! Any suggestions on how to best document this change?

It may be helpful for users to keep a note in the man page for a while, saying that the option is now given to cdmc. Given that the option was always considered surprising, I'd be ok to make the change without a major version increase.

martin-cs

The small amount that touched things I am "owner" for seems to be correctly implemented. As I understand it this should be a back-end option so yes, setting it in cbmc not goto-cc makes sense.

tautschnig · 2023-11-16T09:41:52Z

Yes, this is user-visible -- but we hadn't really documented that undesirable need of setting --object-bits via goto-ccit seems?! Any suggestions on how to best document this change?

It may be helpful for users to keep a note in the man page for a while, saying that the option is now given to cdmc. Given that the option was always considered surprising, I'd be ok to make the change without a major version increase.

I have now added a section "BACKWARD COMPATIBILITY" to the man page.

thomasspriggs · 2023-12-13T19:08:25Z

@tautschnig The regression tests for this PR should pass, once it is based on top of - #8104

tautschnig · 2023-12-13T23:51:51Z

@tautschnig The regression tests for this PR should pass, once it is based on top of - #8104

Rebased, thank you very much for the very quick fix!!

tautschnig · 2023-12-14T15:11:58Z

CSmith test failure is down to a fix in our CSmith script being required since #8093 has been merged.

tautschnig · 2023-12-14T15:26:41Z

CSmith test failure is down to a fix in our CSmith script being required since #8093 has been merged.

Fixed in #8105.

peterschrammel · 2023-12-15T13:26:21Z

doc/man/goto-cc.1

-Configure the number of bits used for object numbering in CBMC's pointer encoding.
+.SH BACKWARD COMPATIBILITY
+.B goto\-cc
+will warn and ignore the use of \fB\-\-object\-bits\fR, which previous versions


❓ Where is this warning produced in this PR? Or does that already exist?

goto-cc warns about all options that it doesn't explicitly know about, so by virtue of removing it from gcc_cmdline.cpp we get this.

This is to make sure that that re-creating initialisation functions restores non-deterministic values.

Support choosing the number of object bits to be used by CBMC at runtime even with pre-compiled goto binaries. Update the goto-cc section in the CPROVER manual to remove any documentation of object-bits (it remains documented in the "Memory and pointers in CBMC" section). Fixes: diffblue#5443

The object:offset encoding is an implementation detail that should be private to the back-end. Expression simplification must not rely on such details. Partly reverts 4d35274.

This test appears to take several hours when running on Windows in GitHub's CI.

tautschnig added the work in progress label Aug 18, 2023

tautschnig self-assigned this Aug 18, 2023

tautschnig mentioned this pull request Aug 18, 2023

Synchronise goto-cc command-line options to re-enable Windows regression tests #5572

Closed

3 tasks

tautschnig force-pushed the features/objects-bits-set-up branch from 951b6ce to 2a9ccc9 Compare August 21, 2023 14:17

tautschnig changed the title ~~Permit re-setting --object-bits and malloc failure mode~~ Permit re-setting --object-bits Aug 21, 2023

tautschnig removed the work in progress label Aug 21, 2023

tautschnig force-pushed the features/objects-bits-set-up branch from 2a9ccc9 to cf98d57 Compare August 21, 2023 14:21

tautschnig marked this pull request as ready for review August 21, 2023 14:52

tautschnig requested review from qinheping, feliperodri, remi-delmas-3000, martin-cs, peterschrammel, kroening, NlightNFotis, thomasspriggs, jimgrundy and TGWDB as code owners August 21, 2023 14:52

tautschnig assigned kroening and unassigned tautschnig Aug 21, 2023

tautschnig force-pushed the features/objects-bits-set-up branch from cf98d57 to dbe9264 Compare August 29, 2023 18:03

tautschnig self-assigned this Aug 29, 2023

martin-cs approved these changes Sep 29, 2023

View reviewed changes

tautschnig force-pushed the features/objects-bits-set-up branch from dbe9264 to 549b3e4 Compare November 16, 2023 09:41

tautschnig added the Version 6 Pull requests and issues requiring a major version bump label Nov 16, 2023

tautschnig unassigned tautschnig and kroening Dec 13, 2023

thomasspriggs mentioned this pull request Dec 13, 2023

Keep symbols as nondet rather than using their symbol table values in SMT decision procedure. #8104

Merged

7 tasks

tautschnig force-pushed the features/objects-bits-set-up branch from 045c685 to 98d3df5 Compare December 13, 2023 23:51

tautschnig assigned tautschnig and unassigned thomasspriggs Dec 13, 2023

tautschnig assigned kroening and unassigned tautschnig Dec 14, 2023

tautschnig force-pushed the features/objects-bits-set-up branch from 98d3df5 to a588dd4 Compare December 14, 2023 16:29

thomasspriggs mentioned this pull request Dec 15, 2023

[CI] Bring back core release processes #8108

Merged

peterschrammel approved these changes Dec 15, 2023

View reviewed changes

tautschnig assigned tautschnig and feliperodri and unassigned tautschnig Dec 15, 2023

feliperodri approved these changes Dec 18, 2023

View reviewed changes

tautschnig unassigned feliperodri Jan 22, 2024

tautschnig force-pushed the features/objects-bits-set-up branch 2 times, most recently from f0a795c to 8b953f4 Compare February 14, 2024 11:41

tautschnig added 4 commits April 23, 2024 09:01

Nondet-static: also update symbol table

944c151

This is to make sure that that re-creating initialisation functions restores non-deterministic values.

Do not use back-end pointer encoding details in the simplifier

fb578a6

The object:offset encoding is an implementation detail that should be private to the back-end. Expression simplification must not rely on such details. Partly reverts 4d35274.

Mark pointer-in-range-requires test as expensive

97e2439

This test appears to take several hours when running on Windows in GitHub's CI.

tautschnig force-pushed the features/objects-bits-set-up branch from 8b953f4 to 97e2439 Compare April 23, 2024 09:03

kroening approved these changes May 1, 2024

View reviewed changes

kroening merged commit 905033e into diffblue:develop May 1, 2024
38 of 40 checks passed

tautschnig deleted the features/objects-bits-set-up branch May 2, 2024 08:25

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Permit re-setting --object-bits #7858

Permit re-setting --object-bits #7858

tautschnig commented Aug 18, 2023 •

edited

Loading

codecov bot commented Aug 21, 2023 •

edited

Loading

kroening commented Aug 28, 2023

tautschnig commented Aug 29, 2023

kroening commented Aug 29, 2023

martin-cs left a comment

tautschnig commented Nov 16, 2023

thomasspriggs commented Dec 13, 2023

tautschnig commented Dec 13, 2023

tautschnig commented Dec 14, 2023

tautschnig commented Dec 14, 2023

peterschrammel Dec 15, 2023

tautschnig Dec 15, 2023

Permit re-setting --object-bits #7858

Permit re-setting --object-bits #7858

Conversation

tautschnig commented Aug 18, 2023 • edited Loading

codecov bot commented Aug 21, 2023 • edited Loading

Codecov Report

kroening commented Aug 28, 2023

tautschnig commented Aug 29, 2023

kroening commented Aug 29, 2023

martin-cs left a comment

Choose a reason for hiding this comment

tautschnig commented Nov 16, 2023

thomasspriggs commented Dec 13, 2023

tautschnig commented Dec 13, 2023

tautschnig commented Dec 14, 2023

tautschnig commented Dec 14, 2023

peterschrammel Dec 15, 2023

Choose a reason for hiding this comment

tautschnig Dec 15, 2023

Choose a reason for hiding this comment

tautschnig commented Aug 18, 2023 •

edited

Loading

codecov bot commented Aug 21, 2023 •

edited

Loading