Skip to content
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

Add missing source locations #7856

Merged
merged 7 commits into from
Mar 8, 2024
Merged

Add missing source locations #7856

merged 7 commits into from
Mar 8, 2024

Conversation

tautschnig
Copy link
Collaborator

Linking (and also other workflows) use expression replacement. Doing so
must not destroy the source location annotated to an expression. This
left us with instructions without location.

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

@tautschnig tautschnig added bugfix aws Bugs or features of importance to AWS CBMC users labels Aug 18, 2023
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 861a411 to 9df6b29 Compare August 18, 2023 13:58
@codecov
Copy link

codecov bot commented Aug 18, 2023 •
edited
Loading

Codecov Report

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

Project coverage is 79.67%. Comparing base (6f628d8) to head (5d8abbe).

Files Patch % Lines
src/ansi-c/c_typecheck_expr.cpp 91.66% 1 Missing ⚠️
src/util/replace_symbol.cpp 88.88% 1 Missing ⚠️
Additional details and impacted files 
@@           Coverage Diff            @@
##           develop    #7856   +/-   ##
========================================
  Coverage    79.66%   79.67%           
========================================
  Files         1682     1682           
  Lines       195431   195489   +58     
========================================
+ Hits        155694   155748   +54     
- Misses       39737    39741    +4

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

@peterschrammel peterschrammel removed their assignment Sep 19, 2023
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 9df6b29 to b8de17a Compare November 24, 2023 10:33
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 0392ca4 to 697598d Compare December 15, 2023 21:15
@kroening
Copy link
Member

I'd be curious why the various program elements end up not having a source location to begin with.

@kroening
Copy link
Member

It may be preferable to fix that when they are generated, as opposed to fixing it up later.

@tautschnig
Copy link
Collaborator Author

It may be preferable to fix that when they are generated, as opposed to fixing it up later.

Is this specifically about the commit "switch-case conversion: ensure case selection has source location" - I think all other commits do as you say, or am I missing something?

@tautschnig tautschnig self-assigned this Feb 7, 2024
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 697598d to d9c01d5 Compare February 9, 2024 13:54
@tautschnig tautschnig requested a review from martin-cs as a code owner February 9, 2024 13:54
@tautschnig
Copy link
Collaborator Author

It may be preferable to fix that when they are generated, as opposed to fixing it up later.

Thank you for insisting that this be done. I believe I have now fixed the root causes as far as feasible. (There are still places outside the language front-ends that generate symbol expressions without a source location, but we might not even have a reasonable source location to pick in those cases.)

@tautschnig tautschnig assigned tautschnig and unassigned tautschnig Feb 9, 2024
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from d9c01d5 to a959d8d Compare February 9, 2024 14:14
@tautschnig tautschnig assigned tautschnig and unassigned tautschnig Feb 9, 2024
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from a959d8d to a220db8 Compare February 12, 2024 15:49
@tautschnig tautschnig requested a review from TGWDB as a code owner February 12, 2024 15:49
@tautschnig tautschnig removed their assignment Feb 12, 2024
@tautschnig tautschnig changed the title Maintain source location while replacing symbol expressions Add missing source locations Feb 21, 2024
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from a220db8 to 861fabd Compare February 21, 2024 17:17
@tautschnig tautschnig mentioned this pull request Feb 21, 2024
Merged
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 861fabd to 1f28ad1 Compare February 21, 2024 21:52
@tautschnig
Add exprt::with_source_location with source_locationt parameter
5f90785 
We already supported the fluent-style with_source_location for copying
from another expression (since 917f9a0). Now also support passing a
source location directly.
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 1f28ad1 to 661e6e7 Compare March 6, 2024 21:28
@tautschnig tautschnig assigned tautschnig and unassigned kroening Mar 6, 2024
@tautschnig
Reduce the number of symbol_exprt without a source location
5951105 
Create or maintain source location information in symbol expressions.
@tautschnig
Actually run goto-cc-multi-file regression suite
0d29ab6 
We had this folder in place for a while, but it was neither included
in the Makefile nor the CMake-based regression test execution.
@tautschnig
Maintain source location while replacing symbol expressions
1a2918e 
Linking (and also other workflows) use expression replacement. Doing so
must not destroy the source location annotated to an expression. This
left us with instructions without location.
@tautschnig
All if-then-else goto conversion instructions have a location
25f4436 
We must not produce goto-program instructions without location, even
when they are considered dummy instructions: those instructions may
subsequently be used to produce a source location, which was thus
missing when converting nested if-then-else statements.
@tautschnig
switch-case conversion: ensure case selection has source location
f3da348 
The expression operand was at times lacking a source location when it
had been subject to expression simplification. Fixes the root cause in
the C front-end, and makes sure the invariant is maintained during goto
conversion.
@tautschnig
Function pointer removal: ensure presence of source location
5d8abbe 
Return type fix-up tried to use the source location from the
function-call code, which had just been constructed and necessarily
lacked a source location. Instead, explicitly pass a source location.
@tautschnig tautschnig force-pushed the bugfixes/linking-location branch from 661e6e7 to 5d8abbe Compare March 7, 2024 12:27
@tautschnig tautschnig merged commit 9411c77 into diffblue:develop Mar 8, 2024
39 checks passed
@tautschnig tautschnig deleted the bugfixes/linking-location branch March 8, 2024 22:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@remi-delmas-3000 remi-delmas-3000 remi-delmas-3000 left review comments

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

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

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

Assignees

@tautschnig tautschnig

Labels
aws Bugs or features of importance to AWS CBMC users bugfix
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @kroening @remi-delmas-3000 @peterschrammel