Skip to content

Commit 5742434

Browse files
tautschnigtautschnig
committed
Reduce the number of symbol_exprt without a source location
Create or maintain source location information in symbol expressions.
1 parent bba0da4 commit 5742434

File tree

6 files changed

+51
-26
lines changed

6 files changed

+51
-26
lines changed

‎src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

Lines changed: 36 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -673,7 +673,8 @@ static void instantiate_atomic_fetch_op(
673673
block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)});
674674

675675
block.add(code_expressiont{side_effect_expr_function_callt{
676-
symbol_exprt::typeless("__atomic_thread_fence"),
676+
symbol_exprt::typeless("__atomic_thread_fence")
677+
.with_source_location<symbol_exprt>(source_location),
677678
{parameter_exprs[2]},
678679
typet{},
679680
source_location}});
@@ -736,7 +737,8 @@ static void instantiate_atomic_op_fetch(
736737

737738
// this instruction implies an mfence, i.e., WRfence
738739
block.add(code_expressiont{side_effect_expr_function_callt{
739-
symbol_exprt::typeless("__atomic_thread_fence"),
740+
symbol_exprt::typeless("__atomic_thread_fence")
741+
.with_source_location<symbol_exprt>(source_location),
740742
{parameter_exprs[2]},
741743
typet{},
742744
source_location}});
@@ -767,11 +769,12 @@ static void instantiate_sync_fetch(
767769
parameter_exprs[1],
768770
from_integer(std::memory_order_seq_cst, signed_int_type())};
769771

770-
block.add(code_returnt{
771-
side_effect_expr_function_callt{symbol_exprt::typeless(atomic_name),
772-
std::move(arguments),
773-
typet{},
774-
source_location}});
772+
block.add(code_returnt{side_effect_expr_function_callt{
773+
symbol_exprt::typeless(atomic_name)
774+
.with_source_location<symbol_exprt>(source_location),
775+
std::move(arguments),
776+
typet{},
777+
source_location}});
775778
}
776779

777780
static void instantiate_sync_bool_compare_and_swap(
@@ -790,7 +793,8 @@ static void instantiate_sync_bool_compare_and_swap(
790793
// _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
791794

792795
block.add(code_returnt{side_effect_expr_function_callt{
793-
symbol_exprt::typeless(ID___atomic_compare_exchange),
796+
symbol_exprt::typeless(ID___atomic_compare_exchange)
797+
.with_source_location<symbol_exprt>(source_location),
794798
{parameter_exprs[0],
795799
address_of_exprt{parameter_exprs[1]},
796800
address_of_exprt{parameter_exprs[2]},
@@ -968,7 +972,8 @@ static void instantiate_atomic_load(
968972
dereference_exprt{parameter_exprs[0]}});
969973

970974
block.add(code_expressiont{side_effect_expr_function_callt{
971-
symbol_exprt::typeless("__atomic_thread_fence"),
975+
symbol_exprt::typeless("__atomic_thread_fence")
976+
.with_source_location<symbol_exprt>(source_location),
972977
{parameter_exprs[2]},
973978
typet{},
974979
source_location}});
@@ -999,7 +1004,8 @@ static void instantiate_atomic_load_n(
9991004
block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
10001005

10011006
block.add(code_expressiont{side_effect_expr_function_callt{
1002-
symbol_exprt::typeless(ID___atomic_load),
1007+
symbol_exprt::typeless(ID___atomic_load)
1008+
.with_source_location<symbol_exprt>(source_location),
10031009
{parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
10041010
typet{},
10051011
source_location}});
@@ -1028,7 +1034,8 @@ static void instantiate_atomic_store(
10281034
dereference_exprt{parameter_exprs[1]}});
10291035

10301036
block.add(code_expressiont{side_effect_expr_function_callt{
1031-
symbol_exprt::typeless("__atomic_thread_fence"),
1037+
symbol_exprt::typeless("__atomic_thread_fence")
1038+
.with_source_location<symbol_exprt>(source_location),
10321039
{parameter_exprs[2]},
10331040
typet{},
10341041
source_location}});
@@ -1051,13 +1058,14 @@ static void instantiate_atomic_store_n(
10511058
// This built-in function implements an atomic store operation. It writes
10521059
// val into *ptr.
10531060

1054-
block.add(code_expressiont{
1055-
side_effect_expr_function_callt{symbol_exprt::typeless(ID___atomic_store),
1056-
{parameter_exprs[0],
1057-
address_of_exprt{parameter_exprs[1]},
1058-
parameter_exprs[2]},
1059-
typet{},
1060-
source_location}});
1061+
block.add(code_expressiont{side_effect_expr_function_callt{
1062+
symbol_exprt::typeless(ID___atomic_store)
1063+
.with_source_location<symbol_exprt>(source_location),
1064+
{parameter_exprs[0],
1065+
address_of_exprt{parameter_exprs[1]},
1066+
parameter_exprs[2]},
1067+
typet{},
1068+
source_location}});
10611069
}
10621070

10631071
static void instantiate_atomic_exchange(
@@ -1083,7 +1091,8 @@ static void instantiate_atomic_exchange(
10831091
dereference_exprt{parameter_exprs[1]}});
10841092

10851093
block.add(code_expressiont{side_effect_expr_function_callt{
1086-
symbol_exprt::typeless("__atomic_thread_fence"),
1094+
symbol_exprt::typeless("__atomic_thread_fence")
1095+
.with_source_location<symbol_exprt>(source_location),
10871096
{parameter_exprs[3]},
10881097
typet{},
10891098
source_location}});
@@ -1114,7 +1123,8 @@ static void instantiate_atomic_exchange_n(
11141123
block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
11151124

11161125
block.add(code_expressiont{side_effect_expr_function_callt{
1117-
symbol_exprt::typeless(ID___atomic_exchange),
1126+
symbol_exprt::typeless(ID___atomic_exchange)
1127+
.with_source_location<symbol_exprt>(source_location),
11181128
{parameter_exprs[0],
11191129
address_of_exprt{parameter_exprs[1]},
11201130
address_of_exprt{result},
@@ -1171,7 +1181,8 @@ static void instantiate_atomic_compare_exchange(
11711181
dereference_exprt{parameter_exprs[2]}};
11721182
assign.add_source_location() = source_location;
11731183
code_expressiont success_fence{side_effect_expr_function_callt{
1174-
symbol_exprt::typeless("__atomic_thread_fence"),
1184+
symbol_exprt::typeless("__atomic_thread_fence")
1185+
.with_source_location<symbol_exprt>(source_location),
11751186
{parameter_exprs[4]},
11761187
typet{},
11771188
source_location}};
@@ -1181,7 +1192,8 @@ static void instantiate_atomic_compare_exchange(
11811192
deref_ptr};
11821193
assign_not_equal.add_source_location() = source_location;
11831194
code_expressiont failure_fence{side_effect_expr_function_callt{
1184-
symbol_exprt::typeless("__atomic_thread_fence"),
1195+
symbol_exprt::typeless("__atomic_thread_fence")
1196+
.with_source_location<symbol_exprt>(source_location),
11851197
{parameter_exprs[5]},
11861198
typet{},
11871199
source_location}};
@@ -1212,7 +1224,8 @@ static void instantiate_atomic_compare_exchange_n(
12121224
// desired, bool weak, int success_memorder, int failure_memorder)
12131225

12141226
block.add(code_returnt{side_effect_expr_function_callt{
1215-
symbol_exprt::typeless(ID___atomic_compare_exchange),
1227+
symbol_exprt::typeless(ID___atomic_compare_exchange)
1228+
.with_source_location<symbol_exprt>(source_location),
12161229
{parameter_exprs[0],
12171230
parameter_exprs[1],
12181231
address_of_exprt{parameter_exprs[2]},

‎src/assembler/remove_asm.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,8 @@ void remove_asmt::gcc_asm_function_call(
134134
empty_typet()};
135135

136136
symbol_exprt fkt(function_identifier, fkt_type);
137+
if(code.source_location().is_not_nil())
138+
fkt.add_source_location() = code.source_location();
137139

138140
code_function_callt function_call(std::move(fkt), std::move(arguments));
139141

@@ -190,6 +192,8 @@ void remove_asmt::msc_asm_function_call(
190192
empty_typet()};
191193

192194
symbol_exprt fkt(function_identifier, fkt_type);
195+
if(code.source_location().is_not_nil())
196+
fkt.add_source_location() = code.source_location();
193197

194198
code_function_callt function_call(std::move(fkt), std::move(arguments));
195199

‎src/pointer-analysis/value_set_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -236,7 +236,7 @@ exprt value_set_dereferencet::handle_dereference_base_case(
236236
pointer.type(),
237237
"derefd_pointer",
238238
"derefd_pointer",
239-
source_locationt(),
239+
pointer.find_source_location(),
240240
language_mode,
241241
new_symbol_table);
242242

‎src/util/ssa_expr.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,9 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
4141
{
4242
set(ID_C_SSA_symbol, true);
4343
add(ID_expression, expr);
44+
const source_locationt &location = expr.source_location();
45+
if(location.is_not_nil())
46+
add_source_location() = location;
4447
std::ostringstream os;
4548
initialize_ssa_identifier(os, expr);
4649
const std::string id = os.str();

‎src/util/symbol.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ void symbolt::swap(symbolt &b)
120120
/// type of the symbol object.
121121
symbol_exprt symbolt::symbol_expr() const
122122
{
123-
return symbol_exprt(name, type);
123+
return symbol_exprt(name, type).with_source_location<symbol_exprt>(location);
124124
}
125125

126126
/// Check that the instance object is well formed.

‎unit/path_strategies.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -337,8 +337,13 @@ void symex_eventt::validate_resume(
337337
REQUIRE(!events.empty());
338338

339339
int dst = 0;
340-
if(!state.saved_target->source_location().get_line().empty())
340+
if(
341+
state.saved_target->source_location().get_file() !=
342+
"<built-in-additions>" &&
343+
!state.saved_target->source_location().get_line().empty())
344+
{
341345
dst = std::stoi(state.saved_target->source_location().get_line().c_str());
346+
}
342347

343348
if(state.has_saved_next_instruction)
344349
{

0 commit comments

Comments
 (0)