Skip to content

Commit

Permalink
Maintain source location while replacing symbol expressions
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
tautschnig committed Mar 7, 2024
1 parent 0d29ab6 commit 1a2918e
Show file tree
Hide file tree
Showing 5 changed files with 47 additions and 0 deletions.
11 changes: 11 additions & 0 deletions regression/goto-cc-multi-file/maintain-location/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
int foo()
{
return 0;
}

int main()
{
int result;
result = foo();
return result;
}
6 changes: 6 additions & 0 deletions regression/goto-cc-multi-file/maintain-location/other.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
int foo();

int bar()
{
return foo();
}
9 changes: 9 additions & 0 deletions regression/goto-cc-multi-file/maintain-location/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
main.c
other.c
file main.c line 9 function main
^EXIT=0$
^SIGNAL=0$
--
--
We previously lost the location attached to the call of `foo` in function main.
6 changes: 6 additions & 0 deletions src/linking/linking.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -100,13 +100,19 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const

const exprt &e = it->second;

source_locationt previous_source_location{s.source_location()};
DATA_INVARIANT_WITH_DIAGNOSTICS(
previous_source_location.is_not_nil(),
"front-ends should construct symbol expressions with source locations",
s.pretty());
if(e.type().id() != ID_array && e.type().id() != ID_code)
{
typet type = s.type();
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
}
else
static_cast<exprt &>(s) = e;
s.add_source_location() = std::move(previous_source_location);

return false;
}
Expand Down
15 changes: 15 additions & 0 deletions src/util/replace_symbol.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,12 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
s.type() == it->second.type(),
"types to be replaced should match. s.type:\n" + s.type().pretty() +
"\nit->second.type:\n" + it->second.type().pretty());
source_locationt previous_source_location{s.source_location()};
static_cast<exprt &>(s) = it->second;
// back-end generated or internal symbols (like rounding mode) might not have
// a source location
if(s.source_location().is_nil() && previous_source_location.is_not_nil())
s.add_source_location() = std::move(previous_source_location);

return false;
}
Expand Down Expand Up @@ -334,7 +339,12 @@ bool unchecked_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
if(it == expr_map.end())
return true;

source_locationt previous_source_location{s.source_location()};
static_cast<exprt &>(s) = it->second;
// back-end generated or internal symbols (like rounding mode) might not have
// a source location
if(s.source_location().is_nil() && previous_source_location.is_not_nil())
s.add_source_location() = std::move(previous_source_location);

return false;
}
Expand Down Expand Up @@ -415,7 +425,12 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr(

// Note s_copy is no longer a symbol_exprt due to the replace operation,
// and after this line `s` won't be either
source_locationt previous_source_location{s.source_location()};
s = s_copy;
// back-end generated or internal symbols (like rounding mode) might not have
// a source location
if(s.source_location().is_nil() && previous_source_location.is_not_nil())
s.add_source_location() = std::move(previous_source_location);

return false;
}

0 comments on commit 1a2918e

Please sign in to comment.