Fix pointer_offset expressions in dump-c generated code#8880
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Fix pointer_offset expressions in dump-c generated code#8880tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
When goto-instrument --dump-c converts a goto program back to C, pointer
comparisons like &arr[i][j] == &arr[x][y] get simplified by the
expression simplifier into pointer_offset arithmetic. The
pointer_offset_exprt is then rendered as __CPROVER_POINTER_OFFSET by
expr2c, which is not valid C and cannot be compiled by GCC.
The fix adds handling for pointer_offset expressions in dump_ct's
cleanup_expr. It converts pointer_offset(p) to the equivalent C
expression ((char*)(p) - (char*)&root_object), where root_object is
found by unwrapping address_of, index, member, and typecast operations
from the pointer operand.
Minimal reproducer:
int l[10][10]; int g;
int main(void) { if(&l[g+2][g] == &l[3][3]) return 1; return 0; }
This was found via CSmith test seed 1750841832.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Fixes goto-instrument --dump-c emitting non-compilable __CPROVER_POINTER_OFFSET(...) by rewriting pointer_offset expressions into plain C pointer-difference arithmetic during expression cleanup.
Changes:
- Add
ID_pointer_offsethandling indump_ct::cleanup_exprto rewritepointer_offset(p)into a C expression based onchar *pointer subtraction. - Add a regression test ensuring
--dump-coutput does not contain__CPROVER_POINTER_OFFSET. - Add necessary include for
pointer_offset_exprthelpers.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/goto-instrument/dump_c.cpp | Rewrites pointer_offset expressions to avoid emitting __CPROVER_POINTER_OFFSET in dump-c output. |
| regression/goto-instrument/dump-c-pointer-offset/test.desc | Regression harness: asserts dump-c succeeds and forbids __CPROVER_POINTER_OFFSET in output. |
| regression/goto-instrument/dump-c-pointer-offset/main.c | Minimal reproducer that triggers simplification to pointer_offset during dump-c. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+1606
to
+1631
|
|
||
| // Find the root object by unwrapping address_of, index, member, | ||
| // and typecast operations | ||
| const exprt *obj = &ptr; | ||
| if(obj->id() == ID_address_of) | ||
| obj = &to_address_of_expr(*obj).object(); | ||
| const exprt *root = obj; | ||
| while(root->id() == ID_index || root->id() == ID_typecast || | ||
| root->id() == ID_member) | ||
| { | ||
| if(root->id() == ID_index) | ||
| root = &to_index_expr(*root).array(); | ||
| else if(root->id() == ID_member) | ||
| root = &to_member_expr(*root).compound(); | ||
| else | ||
| root = &to_typecast_expr(*root).op(); | ||
| } | ||
|
|
||
| const typet char_ptr = pointer_type(char_type()); | ||
| const typet result_type = expr.type(); | ||
|
|
||
| exprt cast_ptr = typecast_exprt(ptr, char_ptr); | ||
| exprt cast_base = typecast_exprt(address_of_exprt(*root), char_ptr); | ||
| exprt diff = minus_exprt(cast_ptr, cast_base); | ||
| expr = typecast_exprt(diff, result_type); | ||
| cleanup_expr(expr); |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8880 +/- ##
===========================================
- Coverage 80.41% 80.41% -0.01%
===========================================
Files 1703 1703
Lines 188398 188417 +19
Branches 73 73
===========================================
+ Hits 151498 151512 +14
- Misses 36900 36905 +5 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
When goto-instrument --dump-c converts a goto program back to C, pointer comparisons like &arr[i][j] == &arr[x][y] get simplified by the expression simplifier into pointer_offset arithmetic. The pointer_offset_exprt is then rendered as __CPROVER_POINTER_OFFSET by expr2c, which is not valid C and cannot be compiled by GCC.
The fix adds handling for pointer_offset expressions in dump_ct's cleanup_expr. It converts pointer_offset(p) to the equivalent C expression ((char*)(p) - (char*)&root_object), where root_object is found by unwrapping address_of, index, member, and typecast operations from the pointer operand.
Minimal reproducer:
int l[10][10]; int g;
int main(void) { if(&l[g+2][g] == &l[3][3]) return 1; return 0; }
This was found via CSmith test seed 1750841832.