Fix C frontend array type sync in goto program#8799
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Fix C frontend array type sync in goto program#8799tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
When arrays are declared without a length at file scope (e.g., int A[];), C standard 6.9.2 paragraph 5 makes them arrays of size 1 as tentative definitions. The static_lifetime_init function updates the symbol table accordingly, but the function body expressions (symbol values) still reference the old incomplete array type with nil size. When goto_convert later builds the goto program from these expressions, the stale types propagate into the goto program. Add a targeted pass in static_lifetime_init that, after processing all symbols, walks function bodies in the symbol table and updates symbol_exprt nodes whose type is an incomplete array (nil size) to use the completed array type. This ensures goto_convert produces goto programs with consistent types, eliminating the need for the previous workaround in field_sensitivity.cpp that looked up the symbol table at symex time. Fixes: diffblue#5022 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-5022-array-length
branch
from
673ef5f to
2b52ffe
Compare
There was a problem hiding this comment.
Pull request overview
This PR fixes a type inconsistency between the symbol table and function bodies in the generated goto program when C tentative array definitions (e.g., int A[];) are later completed with a concrete size per C standard 6.9.2.
Changes:
- Propagates completed array types from the symbol table into function body expressions before goto conversion.
- Removes a now-redundant field-sensitivity fallback that attempted to recover missing array sizes from the symbol table during symex.
- Adds a regression test covering tentative array definition completion and use across functions.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| src/linking/static_lifetime_init.cpp | Updates symbol expressions inside function bodies to use completed array types from the symbol table. |
| src/goto-symex/field_sensitivity.cpp | Removes a symbol-table lookup fallback for incomplete array sizes when computing field-sensitivity. |
| regression/cbmc/Tentative_definition_array1/test.desc | Adds expected-output specification for the new regression test. |
| regression/cbmc/Tentative_definition_array1/main.c | New C test reproducing tentative array completion behavior and validating consistent typing in goto program. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+168
to
+170
| for(const std::string &id : symbols) | ||
| { | ||
| symbolt &symbol = symbol_table.get_writeable_ref(id); |
Comment on lines
+174
to
+191
| symbol.value.visit_pre( | ||
| [&symbol_table](exprt &expr) | ||
| { | ||
| if(expr.id() != ID_symbol) | ||
| return; | ||
| if(expr.type().id() != ID_array) | ||
| return; | ||
| if(!to_array_type(expr.type()).size().is_nil()) | ||
| return; | ||
| const auto *sym = | ||
| symbol_table.lookup(to_symbol_expr(expr).get_identifier()); | ||
| if( | ||
| sym != nullptr && sym->type.id() == ID_array && | ||
| !to_array_type(sym->type).size().is_nil()) | ||
| { | ||
| expr.type() = sym->type; | ||
| } | ||
| }); |
| @@ -215,15 +215,6 @@ exprt field_sensitivityt::apply( | |||
| bool was_l2 = !tmp.get_level_2().empty(); | |||
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8799 +/- ##
===========================================
- Coverage 80.41% 80.41% -0.01%
===========================================
Files 1703 1703
Lines 188398 188408 +10
Branches 73 73
===========================================
+ Hits 151498 151503 +5
- 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.
Update goto program expressions to use updated array type from symbol table when arrays declared without length are later defined per C standard 6.9.2
Co-authored-by: Kiro autonomous agent
Fixes: #5022