From 1a2918eb6e6e28297f06413a13ec116693cdd6ec Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 18 Aug 2023 12:56:10 +0000
Subject: [PATCH] Maintain source location while replacing symbol expressions

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.
---
 .../goto-cc-multi-file/maintain-location/main.c   | 11 +++++++++++
 .../goto-cc-multi-file/maintain-location/other.c  |  6 ++++++
 .../maintain-location/test.desc                   |  9 +++++++++
 src/linking/linking.cpp                           |  6 ++++++
 src/util/replace_symbol.cpp                       | 15 +++++++++++++++
 5 files changed, 47 insertions(+)
 create mode 100644 regression/goto-cc-multi-file/maintain-location/main.c
 create mode 100644 regression/goto-cc-multi-file/maintain-location/other.c
 create mode 100644 regression/goto-cc-multi-file/maintain-location/test.desc

diff --git a/regression/goto-cc-multi-file/maintain-location/main.c b/regression/goto-cc-multi-file/maintain-location/main.c
new file mode 100644
index 00000000000..a55afb81e20
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/main.c
@@ -0,0 +1,11 @@
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  int result;
+  result = foo();
+  return result;
+}
diff --git a/regression/goto-cc-multi-file/maintain-location/other.c b/regression/goto-cc-multi-file/maintain-location/other.c
new file mode 100644
index 00000000000..6a794a79c27
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/other.c
@@ -0,0 +1,6 @@
+int foo();
+
+int bar()
+{
+  return foo();
+}
diff --git a/regression/goto-cc-multi-file/maintain-location/test.desc b/regression/goto-cc-multi-file/maintain-location/test.desc
new file mode 100644
index 00000000000..4cdabb403ff
--- /dev/null
+++ b/regression/goto-cc-multi-file/maintain-location/test.desc
@@ -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.
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 5ed4d1dfb03..b4ba95fab2f 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -100,6 +100,11 @@ 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();
@@ -107,6 +112,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
   }
   else
     static_cast<exprt &>(s) = e;
+  s.add_source_location() = std::move(previous_source_location);
 
   return false;
 }
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index ce30b84b239..7487f69c3bb 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -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;
 }
@@ -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;
 }
@@ -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;
 }