Skip to content

Commit f6054b5

Browse files
authored
Merge pull request #6743 from tautschnig/cleanup/alloca-processing
Lift alloca's deallocation behaviour out of goto_check_ct
2 parents 724467c + da65bce commit f6054b5

File tree

4 files changed

+42
-24
lines changed

4 files changed

+42
-24
lines changed

regression/cbmc-library/CMakeLists.txt

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,7 @@ add_test_pl_tests(
33
"$<TARGET_FILE:cbmc>"
44
)
55
else()
6-
add_test_pl_tests(
7-
"$<TARGET_FILE:cbmc>"
6+
add_test_pl_profile(
87
"cbmc-library"
98
"$<TARGET_FILE:cbmc>"
109
"-C;-X;unix"

regression/cbmc-library/alloca-01/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,5 @@ int main()
99
int *p = alloca(sizeof(int));
1010
*p = 42;
1111
free(p);
12+
(void)alloca(sizeof(int)); // useless, but result still needs to be released
1213
}

src/ansi-c/goto_check_c.cpp

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -2188,28 +2188,6 @@ void goto_check_ct::goto_check(
21882188
std::move(lhs), std::move(rhs), i.source_location()));
21892189
t->code_nonconst().add_source_location() = i.source_location();
21902190
}
2191-
2192-
if(
2193-
variable.type().id() == ID_pointer &&
2194-
function_identifier != "alloca" &&
2195-
(ns.lookup(variable.get_identifier()).base_name ==
2196-
"return_value___builtin_alloca" ||
2197-
ns.lookup(variable.get_identifier()).base_name ==
2198-
"return_value_alloca"))
2199-
{
2200-
// mark pointer to alloca result as dead
2201-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2202-
exprt alloca_result =
2203-
typecast_exprt::conditional_cast(variable, lhs.type());
2204-
if_exprt rhs(
2205-
side_effect_expr_nondett(bool_typet(), i.source_location()),
2206-
std::move(alloca_result),
2207-
lhs);
2208-
goto_programt::targett t =
2209-
new_code.add(goto_programt::make_assignment(
2210-
std::move(lhs), std::move(rhs), i.source_location()));
2211-
t->code_nonconst().add_source_location() = i.source_location();
2212-
}
22132191
}
22142192
}
22152193
else if(i.is_end_function())

src/goto-programs/builtin_functions.cpp

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1389,6 +1389,46 @@ void goto_convertt::do_function_call_symbol(
13891389

13901390
copy(function_call, FUNCTION_CALL, dest);
13911391
}
1392+
else if(
1393+
(identifier == "alloca" || identifier == "__builtin_alloca") &&
1394+
function.source_location().get_function() != "alloca")
1395+
{
1396+
const source_locationt &source_location = function.source_location();
1397+
exprt new_lhs = lhs;
1398+
1399+
if(lhs.is_nil())
1400+
{
1401+
new_lhs = new_tmp_symbol(
1402+
to_code_type(function.type()).return_type(),
1403+
"alloca",
1404+
dest,
1405+
source_location,
1406+
mode)
1407+
.symbol_expr();
1408+
}
1409+
1410+
code_function_callt function_call(new_lhs, function, arguments);
1411+
function_call.add_source_location() = source_location;
1412+
copy(function_call, FUNCTION_CALL, dest);
1413+
1414+
// create a backup copy to ensure that no assignments to the pointer affect
1415+
// the destructor code that will execute eventually
1416+
if(!lhs.is_nil())
1417+
make_temp_symbol(new_lhs, "alloca", dest, mode);
1418+
1419+
// mark pointer to alloca result as dead
1420+
symbol_exprt dead_object_sym =
1421+
ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1422+
exprt alloca_result =
1423+
typecast_exprt::conditional_cast(new_lhs, dead_object_sym.type());
1424+
if_exprt rhs{
1425+
side_effect_expr_nondett{bool_typet(), source_location},
1426+
std::move(alloca_result),
1427+
dead_object_sym};
1428+
code_assignt assign{
1429+
std::move(dead_object_sym), std::move(rhs), source_location};
1430+
targets.destructor_stack.add(assign);
1431+
}
13921432
else
13931433
{
13941434
do_function_call_symbol(*symbol);

0 commit comments

Comments
 (0)