Merge pull request #8216 from tautschnig/cleanup/expr-with-source-location

Make exprt::with_source_location type safe

Author: kroening

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -607,7 +607,7 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
   {
     exprt ensures = to_lambda_expr(e)
                       .application(contract_lambda_parameters)
-                      .with_source_location<exprt>(e);
+                      .with_source_location(e);
 
     if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
       add_quantified_variable(goto_model.symbol_table, ensures, language_mode);

src/goto-programs/builtin_functions.cpp

@@ -840,9 +840,7 @@ void goto_convertt::do_function_call_symbol(
 
     // use symbol->symbol_expr() to ensure we use the type from the symbol table
     code_function_callt function_call(
-      lhs,
-      symbol->symbol_expr().with_source_location<symbol_exprt>(function),
-      arguments);
+      lhs, symbol->symbol_expr().with_source_location(function), arguments);
     function_call.add_source_location() = function.source_location();
 
     // remove void-typed assignments, which may have been created when the
@@ -1487,9 +1485,7 @@ void goto_convertt::do_function_call_symbol(
     // insert function call
     // use symbol->symbol_expr() to ensure we use the type from the symbol table
     code_function_callt function_call(
-      lhs,
-      symbol->symbol_expr().with_source_location<symbol_exprt>(function),
-      arguments);
+      lhs, symbol->symbol_expr().with_source_location(function), arguments);
     function_call.add_source_location()=function.source_location();
 
     // remove void-typed assignments, which may have been created when the

src/goto-programs/rewrite_rw_ok.cpp

@@ -32,7 +32,7 @@ static std::optional<exprt> rewrite_rw_ok(exprt expr, const namespacet &ns)
           r_or_w_ok->size(),
           ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
           ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
-          .with_source_location<exprt>(*it);
+          .with_source_location(*it);
 
       it.mutate() = std::move(replacement);
       unchanged = false;
@@ -49,7 +49,7 @@ static std::optional<exprt> rewrite_rw_ok(exprt expr, const namespacet &ns)
           pointer_in_range->upper_bound(),
           ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
           ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
-          .with_source_location<exprt>(*it);
+          .with_source_location(*it);
 
       it.mutate() = std::move(replacement);
       unchanged = false;

src/util/expr.h

@@ -98,27 +98,19 @@ class exprt:public irept
   { return (const operandst &)get_sub(); }
 
   /// Add the source location from \p other, if it has any.
-  template <typename T>
-  T &with_source_location(const exprt &other) &
+  exprt &with_source_location(const exprt &other) &
   {
-    static_assert(
-      std::is_base_of<exprt, T>::value,
-      "The template argument T must be derived from exprt.");
     if(other.source_location().is_not_nil())
       add_source_location() = other.source_location();
-    return *static_cast<T *>(this);
+    return *this;
   }
 
   /// Add the source location from \p other, if it has any.
-  template <typename T>
-  T &&with_source_location(const exprt &other) &&
+  exprt &&with_source_location(const exprt &other) &&
   {
-    static_assert(
-      std::is_base_of<exprt, T>::value,
-      "The template argument T must be derived from exprt.");
     if(other.source_location().is_not_nil())
       add_source_location() = other.source_location();
-    return std::move(*static_cast<T *>(this));
+    return std::move(*this);
   }
 
 protected:

src/util/std_expr.h

@@ -1600,12 +1600,16 @@ class array_exprt : public multi_ary_exprt
 
   array_exprt &with_source_location(const exprt &other) &
   {
-    return exprt::with_source_location<array_exprt>(other);
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return *this;
   }
 
   array_exprt &&with_source_location(const exprt &other) &&
   {
-    return std::move(*this).exprt::with_source_location<array_exprt>(other);
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return std::move(*this);
   }
 };