Skip to content

Commit 9ca2e66

Browse files
tautschnigtautschnig
committed
Code contracts: cleanup get_fresh_aux_symbol wrappers
1. Consistently either use the wrappers or get_fresh_aux_symbol directly. 2. Remove wrappers that did not yield significant simplification. 3. Make remaining wrappers do all work that was previously done by each caller.
1 parent ce4c504 commit 9ca2e66

15 files changed

+281
-423
lines changed

‎src/goto-instrument/contracts/contracts.cpp‎

Lines changed: 43 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -139,12 +139,13 @@ void code_contractst::check_apply_loop_contracts(
139139
// Create a temporary to track if we entered the loop,
140140
// i.e., the loop guard was satisfied.
141141
const auto entered_loop =
142-
new_tmp_symbol(
142+
get_fresh_aux_symbol(
143143
bool_typet(),
144+
id2string(loop_head_location.get_function()),
145+
std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
144146
loop_head_location,
145147
mode,
146-
symbol_table,
147-
std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number))
148+
symbol_table)
148149
.symbol_expr();
149150
pre_loop_head_instrs.add(
150151
goto_programt::make_decl(entered_loop, loop_head_location));
@@ -154,8 +155,13 @@ void code_contractst::check_apply_loop_contracts(
154155
// Create a snapshot of the invariant so that we can check the base case,
155156
// if the loop is not vacuous and must be abstracted with contracts.
156157
const auto initial_invariant_val =
157-
new_tmp_symbol(
158-
bool_typet(), loop_head_location, mode, symbol_table, INIT_INVARIANT)
158+
get_fresh_aux_symbol(
159+
bool_typet(),
160+
id2string(loop_head_location.get_function()),
161+
INIT_INVARIANT,
162+
loop_head_location,
163+
mode,
164+
symbol_table)
159165
.symbol_expr();
160166
pre_loop_head_instrs.add(
161167
goto_programt::make_decl(initial_invariant_val, loop_head_location));
@@ -173,10 +179,14 @@ void code_contractst::check_apply_loop_contracts(
173179

174180
// Create a temporary variable to track base case vs inductive case
175181
// instrumentation of the loop.
176-
const auto in_base_case =
177-
new_tmp_symbol(
178-
bool_typet(), loop_head_location, mode, symbol_table, "__in_base_case")
179-
.symbol_expr();
182+
const auto in_base_case = get_fresh_aux_symbol(
183+
bool_typet(),
184+
id2string(loop_head_location.get_function()),
185+
"__in_base_case",
186+
loop_head_location,
187+
mode,
188+
symbol_table)
189+
.symbol_expr();
180190
pre_loop_head_instrs.add(
181191
goto_programt::make_decl(in_base_case, loop_head_location));
182192
pre_loop_head_instrs.add(
@@ -298,12 +308,13 @@ void code_contractst::check_apply_loop_contracts(
298308
// havoc (assigns_set);
299309
// ASSIGN in_loop_havoc_block = false;
300310
const auto in_loop_havoc_block =
301-
new_tmp_symbol(
311+
get_fresh_aux_symbol(
302312
bool_typet(),
313+
id2string(loop_head_location.get_function()),
314+
std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number),
303315
loop_head_location,
304316
mode,
305-
symbol_table,
306-
std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number))
317+
symbol_table)
307318
.symbol_expr();
308319
pre_loop_head_instrs.add(
309320
goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
@@ -335,14 +346,26 @@ void code_contractst::check_apply_loop_contracts(
335346
for(const auto &clause : decreases_clause.operands())
336347
{
337348
const auto old_decreases_var =
338-
new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table)
349+
get_fresh_aux_symbol(
350+
clause.type(),
351+
id2string(loop_head_location.get_function()),
352+
"tmp_cc",
353+
loop_head_location,
354+
mode,
355+
symbol_table)
339356
.symbol_expr();
340357
pre_loop_head_instrs.add(
341358
goto_programt::make_decl(old_decreases_var, loop_head_location));
342359
old_decreases_vars.push_back(old_decreases_var);
343360

344361
const auto new_decreases_var =
345-
new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table)
362+
get_fresh_aux_symbol(
363+
clause.type(),
364+
id2string(loop_head_location.get_function()),
365+
"tmp_cc",
366+
loop_head_location,
367+
mode,
368+
symbol_table)
346369
.symbol_expr();
347370
pre_loop_head_instrs.add(
348371
goto_programt::make_decl(new_decreases_var, loop_head_location));
@@ -1251,8 +1274,10 @@ void code_contractst::add_contract_check(
12511274
optionalt<code_returnt> return_stmt;
12521275
if(code_type.return_type() != empty_typet())
12531276
{
1254-
symbol_exprt r = new_tmp_symbol(
1277+
symbol_exprt r = get_fresh_aux_symbol(
12551278
code_type.return_type(),
1279+
id2string(source_location.get_function()),
1280+
"tmp_cc",
12561281
source_location,
12571282
function_symbol.mode,
12581283
symbol_table)
@@ -1275,8 +1300,10 @@ void code_contractst::add_contract_check(
12751300
{
12761301
PRECONDITION(!parameter.empty());
12771302
const symbolt &parameter_symbol = ns.lookup(parameter);
1278-
symbol_exprt p = new_tmp_symbol(
1303+
symbol_exprt p = get_fresh_aux_symbol(
12791304
parameter_symbol.type,
1305+
id2string(source_location.get_function()),
1306+
"tmp_cc",
12801307
source_location,
12811308
parameter_symbol.mode,
12821309
symbol_table)

‎src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp‎

Lines changed: 12 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -471,30 +471,22 @@ static dfcc_loop_infot gen_dfcc_loop_info(
471471

472472
auto &loop = loop_nesting_graph[loop_id];
473473
const auto cbmc_loop_number = loop.latch->loop_number;
474-
const auto &language_mode =
475-
dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
476474

477475
// Generate "write set" variable
478-
const auto &write_set_var =
479-
get_fresh_aux_symbol(
480-
library.dfcc_type[dfcc_typet::WRITE_SET],
481-
id2string(function_id),
482-
"__write_set_loop_" + std::to_string(cbmc_loop_number),
483-
loop.head->source_location(),
484-
language_mode,
485-
symbol_table)
486-
.symbol_expr();
476+
const auto write_set_var = dfcc_utilst::create_symbol(
477+
symbol_table,
478+
library.dfcc_type[dfcc_typet::WRITE_SET],
479+
function_id,
480+
"__write_set_loop_" + std::to_string(cbmc_loop_number),
481+
loop.head->source_location());
487482

488483
// Generate "address of write set" variable
489-
const auto &addr_of_write_set_var =
490-
get_fresh_aux_symbol(
491-
library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
492-
id2string(function_id),
493-
"__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
494-
loop.head->source_location(),
495-
language_mode,
496-
symbol_table)
497-
.symbol_expr();
484+
const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
485+
symbol_table,
486+
library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
487+
function_id,
488+
"__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
489+
loop.head->source_location());
498490

499491
return {
500492
loop_id,

‎src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp‎

Lines changed: 30 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -256,16 +256,12 @@ void dfcc_instrumentt::instrument_harness_function(
256256
// create a local write set symbol
257257
const auto &function_symbol =
258258
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
259-
const auto &write_set = dfcc_utilst::create_symbol(
260-
goto_model.symbol_table,
261-
library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
262-
function_id,
263-
"__write_set_to_check",
264-
function_symbol.location,
265-
function_symbol.mode,
266-
function_symbol.module,
267-
false)
268-
.symbol_expr();
259+
const auto write_set = dfcc_utilst::create_symbol(
260+
goto_model.symbol_table,
261+
library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
262+
function_id,
263+
"__write_set_to_check",
264+
function_symbol.location);
269265

270266
std::set<symbol_exprt> local_statics = get_local_statics(function_id);
271267

@@ -663,7 +659,7 @@ void dfcc_instrumentt::instrument_lhs(
663659
goto_programt &goto_program,
664660
dfcc_cfg_infot &cfg_info)
665661
{
666-
const auto &mode =
662+
const irep_idt &mode =
667663
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
668664

669665
goto_programt payload;
@@ -691,18 +687,12 @@ void dfcc_instrumentt::instrument_lhs(
691687
// ASSIGN lhs := rhs;
692688
// ```
693689

694-
auto &check_sym = dfcc_utilst::create_symbol(
690+
const auto check_var = dfcc_utilst::create_symbol(
695691
goto_model.symbol_table,
696692
bool_typet(),
697-
id2string(function_id),
693+
function_id,
698694
"__check_lhs_assignment",
699-
lhs_source_location,
700-
mode,
701-
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
702-
.module,
703-
false);
704-
705-
const auto &check_var = check_sym.symbol_expr();
695+
lhs_source_location);
706696

707697
payload.add(goto_programt::make_decl(check_var, lhs_source_location));
708698

@@ -950,22 +940,17 @@ void dfcc_instrumentt::instrument_deallocate_call(
950940
// ----
951941
// CALL __CPROVER_deallocate(ptr);
952942
// ```
953-
const auto &mode =
954-
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
955943
goto_programt payload;
956944

957945
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
958946
dfcc_utilst::make_null_check_expr(write_set), target_location));
959947

960-
auto &check_sym = get_fresh_aux_symbol(
948+
const auto check_var = dfcc_utilst::create_symbol(
949+
goto_model.symbol_table,
961950
bool_typet(),
962-
id2string(function_id),
951+
function_id,
963952
"__check_deallocate",
964-
target_location,
965-
mode,
966-
goto_model.symbol_table);
967-
968-
const auto &check_var = check_sym.symbol_expr();
953+
target_location);
969954

970955
payload.add(goto_programt::make_decl(check_var, target_location));
971956

@@ -977,6 +962,8 @@ void dfcc_instrumentt::instrument_deallocate_call(
977962
target_location));
978963

979964
// add property class on assertion source_location
965+
const irep_idt &mode =
966+
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
980967
source_locationt check_location(target_location);
981968
check_location.set_property_class("frees");
982969
std::string comment =
@@ -1040,6 +1027,8 @@ void dfcc_instrumentt::instrument_other(
10401027
const auto &target_location = target->source_location();
10411028
auto &statement = target->get_other().get_statement();
10421029
auto &write_set = cfg_info.get_write_set(target);
1030+
const irep_idt &mode =
1031+
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
10431032

10441033
if(statement == ID_array_set || statement == ID_array_copy)
10451034
{
@@ -1054,23 +1043,17 @@ void dfcc_instrumentt::instrument_other(
10541043
// ----
10551044
// OTHER {statement = array_set, args = {dest, value}};
10561045
// ```
1057-
const auto &mode =
1058-
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
1059-
.mode;
10601046
goto_programt payload;
10611047

10621048
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
10631049
dfcc_utilst::make_null_check_expr(write_set), target_location));
10641050

1065-
auto &check_sym = get_fresh_aux_symbol(
1051+
const auto check_var = dfcc_utilst::create_symbol(
1052+
goto_model.symbol_table,
10661053
bool_typet(),
1067-
id2string(function_id),
1054+
function_id,
10681055
is_array_set ? "__check_array_set" : "__check_array_copy",
1069-
target_location,
1070-
mode,
1071-
goto_model.symbol_table);
1072-
1073-
const auto &check_var = check_sym.symbol_expr();
1056+
target_location);
10741057

10751058
payload.add(goto_programt::make_decl(check_var, target_location));
10761059

@@ -1115,23 +1098,17 @@ void dfcc_instrumentt::instrument_other(
11151098
// ----
11161099
// OTHER {statement = array_replace, args = {dest, src}};
11171100
// ```
1118-
const auto &mode =
1119-
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
1120-
.mode;
11211101
goto_programt payload;
11221102

11231103
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
11241104
dfcc_utilst::make_null_check_expr(write_set), target_location));
11251105

1126-
auto &check_sym = get_fresh_aux_symbol(
1106+
const auto check_var = dfcc_utilst::create_symbol(
1107+
goto_model.symbol_table,
11271108
bool_typet(),
1128-
id2string(function_id),
1109+
function_id,
11291110
"__check_array_replace",
1130-
target_location,
1131-
mode,
1132-
goto_model.symbol_table);
1133-
1134-
const auto &check_var = check_sym.symbol_expr();
1111+
target_location);
11351112

11361113
payload.add(goto_programt::make_decl(check_var, target_location));
11371114

@@ -1170,23 +1147,17 @@ void dfcc_instrumentt::instrument_other(
11701147
// ASSERT(check_havoc_object);
11711148
// DEAD check_havoc_object;
11721149
// ```
1173-
const auto &mode =
1174-
dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
1175-
.mode;
11761150
goto_programt payload;
11771151

11781152
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
11791153
dfcc_utilst::make_null_check_expr(write_set), target_location));
11801154

1181-
auto &check_sym = get_fresh_aux_symbol(
1155+
const auto check_var = dfcc_utilst::create_symbol(
1156+
goto_model.symbol_table,
11821157
bool_typet(),
1183-
id2string(function_id),
1158+
function_id,
11841159
"__check_havoc_object",
1185-
target_location,
1186-
mode,
1187-
goto_model.symbol_table);
1188-
1189-
const auto &check_var = check_sym.symbol_expr();
1160+
target_location);
11901161

11911162
payload.add(goto_programt::make_decl(check_var, target_location));
11921163

0 commit comments

Comments
 (0)