From 9d582abbac6be80d6d70842216c176cdbe5ec262 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Feb 2024 17:50:19 +0000 Subject: [PATCH] Make exprt::with_source_location type safe Do not perform an unchecked cast. Instead, just re-implement the method in *_exprt classes as needed (currently only needed in array_exprt). --- .../dynamic-frames/dfcc_wrapper_program.cpp | 2 +- src/goto-programs/builtin_functions.cpp | 8 ++------ src/goto-programs/rewrite_rw_ok.cpp | 4 ++-- src/util/expr.h | 16 ++++------------ src/util/std_expr.h | 8 ++++++-- 5 files changed, 15 insertions(+), 23 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index fe355938f69..826e5283e11 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/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(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); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 50e49709a93..9277593a30e 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/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(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(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 diff --git a/src/goto-programs/rewrite_rw_ok.cpp b/src/goto-programs/rewrite_rw_ok.cpp index b23c7616402..100042d386e 100644 --- a/src/goto-programs/rewrite_rw_ok.cpp +++ b/src/goto-programs/rewrite_rw_ok.cpp @@ -32,7 +32,7 @@ static std::optional 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(*it); + .with_source_location(*it); it.mutate() = std::move(replacement); unchanged = false; @@ -49,7 +49,7 @@ static std::optional 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(*it); + .with_source_location(*it); it.mutate() = std::move(replacement); unchanged = false; diff --git a/src/util/expr.h b/src/util/expr.h index 6ebe1c4b681..56e8611a7d3 100644 --- a/src/util/expr.h +++ b/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 - T &with_source_location(const exprt &other) & + exprt &with_source_location(const exprt &other) & { - static_assert( - std::is_base_of::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(this); + return *this; } /// Add the source location from \p other, if it has any. - template - T &&with_source_location(const exprt &other) && + exprt &&with_source_location(const exprt &other) && { - static_assert( - std::is_base_of::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(this)); + return std::move(*this); } protected: diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 3445073c17c..90b2877f1f4 100644 --- a/src/util/std_expr.h +++ b/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(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(other); + if(other.source_location().is_not_nil()) + add_source_location() = other.source_location(); + return std::move(*this); } };