Skip to content

Commit 7e5922a

Browse files
danpoedanpoe
committed
remove functions without a body
1 parent bc2c0cd commit 7e5922a

File tree

17 files changed

+315
-68
lines changed

17 files changed

+315
-68
lines changed

‎regression/goto-instrument/inline_09/test.desc

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--inline
3+
--inline --remove-calls-no-body
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
@@ -9,4 +9,5 @@ main.c
99
^\s*a;$
1010
no body.*[`]f
1111
--
12+
f\(\)
1213
^warning: ignoring

‎regression/goto-instrument/inline_16/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func1();
2+
3+
int main()
4+
{
5+
int ret;
6+
7+
func1();
8+
ret = func2();
9+
}

‎regression/goto-instrument/inline_16/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--inline
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func1\(\)
8+
ret.*=.*func2\(\)
9+
no body for function.*func1
10+
no body for function.*func2
11+
--
12+
^warning: ignoring

‎regression/goto-instrument/inline_17/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func1()
2+
{
3+
func2();
4+
}
5+
6+
int main()
7+
{
8+
func1();
9+
}

‎regression/goto-instrument/inline_17/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--function-inline func1
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func1\(\)
8+
func2\(\)
9+
--
10+
^warning: ignoring

‎regression/goto-instrument/remove-calls-no-body1/main.c

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
void func1();
2+
3+
void func3()
4+
{
5+
}
6+
7+
void func4()
8+
{
9+
func1();
10+
func2();
11+
}
12+
13+
void main()
14+
{
15+
func1();
16+
func2();
17+
func3();
18+
func4();
19+
}

‎regression/goto-instrument/remove-calls-no-body1/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--remove-calls-no-body
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func3\(\)
8+
func4\(\)
9+
--
10+
func1\(\)
11+
func2\(\)
12+
^warning: ignoring

‎regression/goto-instrument/remove-calls-no-body2/main.c

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
int func1(int arg1, int arg2);
2+
3+
void func3()
4+
{
5+
}
6+
7+
void func4()
8+
{
9+
func1(567, 285);
10+
func2();
11+
}
12+
13+
void main()
14+
{
15+
int ret1;
16+
17+
ret1 = func1(567, 285);
18+
func2();
19+
func3();
20+
func4();
21+
}

‎regression/goto-instrument/remove-calls-no-body2/test.desc

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--remove-calls-no-body
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
func3\(\)
8+
func4\(\)
9+
567;
10+
285;
11+
ret1.*=.*NONDET
12+
--
13+
func1\(.*\)
14+
func2\(.*\)
15+
^warning: ignoring

‎src/goto-instrument/goto_instrument_parse_options.cpp

+21-4
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
2323

2424
#include <goto-programs/class_hierarchy.h>
2525
#include <goto-programs/goto_convert_functions.h>
26+
#include <goto-programs/remove_calls_no_body.h>
2627
#include <goto-programs/remove_function_pointers.h>
2728
#include <goto-programs/remove_virtual_functions.h>
2829
#include <goto-programs/remove_exceptions.h>
@@ -729,6 +730,10 @@ int goto_instrument_parse_optionst::doit()
729730
status() << "Performing full inlining" << eom;
730731
goto_inline(goto_model, get_message_handler());
731732

733+
status() << "Removing calls to functions without a body" << eom;
734+
remove_calls_no_bodyt remove_calls_no_body;
735+
remove_calls_no_body(goto_model.goto_functions);
736+
732737
status() << "Accelerating" << eom;
733738
accelerate_functions(
734739
goto_model, get_message_handler(), cmdline.isset("z3"));
@@ -992,7 +997,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
992997
// now do full inlining, if requested
993998
if(cmdline.isset("inline"))
994999
{
995-
do_indirect_call_and_rtti_removal(/*force=*/true);
1000+
do_indirect_call_and_rtti_removal(true);
9961001

9971002
if(cmdline.isset("show-custom-bitvector-analysis") ||
9981003
cmdline.isset("custom-bitvector-analysis"))
@@ -1113,10 +1118,21 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11131118
do_indirect_call_and_rtti_removal();
11141119

11151120
status() << "Partial inlining" << eom;
1116-
goto_partial_inline(goto_functions, ns, ui_message_handler, 0, true);
1121+
goto_partial_inline(goto_model, ui_message_handler, 0, true);
1122+
1123+
goto_model.goto_functions.update();
1124+
goto_model.goto_functions.compute_loop_numbers();
1125+
}
11171126

1118-
goto_functions.update();
1119-
goto_functions.compute_loop_numbers();
1127+
if(cmdline.isset("remove-calls-no-body"))
1128+
{
1129+
status() << "Removing calls to functions without a body" << eom;
1130+
1131+
remove_calls_no_bodyt remove_calls_no_body;
1132+
remove_calls_no_body(goto_model.goto_functions);
1133+
1134+
goto_model.goto_functions.update();
1135+
goto_model.goto_functions.compute_loop_numbers();
11201136
}
11211137

11221138
if(cmdline.isset("constant-propagator"))
@@ -1545,6 +1561,7 @@ void goto_instrument_parse_optionst::help()
15451561
" --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
15461562
" --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
15471563
" --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1564+
HELP_REMOVE_CALLS_NO_BODY
15481565
HELP_REMOVE_CONST_FUNCTION_POINTERS
15491566
" --add-library add models of C library functions\n"
15501567
" --model-argc-argv <n> model up to <n> command line arguments\n"

‎src/goto-instrument/goto_instrument_parse_options.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
#include <goto-programs/goto_functions.h>
2020
#include <goto-programs/show_goto_functions.h>
2121
#include <goto-programs/show_properties.h>
22+
#include <goto-programs/remove_calls_no_body.h>
2223
#include <goto-programs/remove_const_function_pointers.h>
2324

2425
#include <analyses/goto_check.h>
@@ -84,7 +85,8 @@ Author: Daniel Kroening, [email protected]
8485
"(show-threaded)(list-calls-args)(print-path-lengths)" \
8586
"(undefined-function-is-assume-false)" \
8687
"(remove-function-body):"\
87-
"(splice-call):"
88+
"(splice-call):" \
89+
OPT_REMOVE_CALLS_NO_BODY
8890
// clang-format on
8991

9092
class goto_instrument_parse_optionst:

‎src/goto-programs/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ SRC = basic_blocks.cpp \
4040
read_goto_binary.cpp \
4141
rebuild_goto_start_function.cpp \
4242
remove_asm.cpp \
43+
remove_calls_no_body.cpp \
4344
remove_complex.cpp \
4445
remove_const_function_pointers.cpp \
4546
remove_exceptions.cpp \

‎src/goto-programs/goto_inline.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ void goto_inline(
7979

8080
Forall_goto_program_instructions(i_it, goto_program)
8181
{
82-
if(!goto_inlinet::is_call(i_it))
82+
if(!i_it->is_function_call())
8383
continue;
8484

8585
call_list.push_back(goto_inlinet::callt(i_it, false));

‎src/goto-programs/goto_inline_class.cpp

+7-54
Original file line numberDiff line numberDiff line change
@@ -380,59 +380,6 @@ void goto_inlinet::insert_function_body(
380380
dest.destructive_insert(target, tmp);
381381
}
382382

383-
void goto_inlinet::insert_function_nobody(
384-
goto_programt &dest,
385-
const exprt &lhs,
386-
goto_programt::targett target,
387-
const symbol_exprt &function,
388-
const exprt::operandst &arguments)
389-
{
390-
PRECONDITION(target->is_function_call());
391-
PRECONDITION(!dest.empty());
392-
393-
const irep_idt identifier=function.get_identifier();
394-
395-
if(no_body_set.insert(identifier).second) // newly inserted
396-
{
397-
warning().source_location=function.find_source_location();
398-
warning() << "no body for function `" << identifier << "'" << eom;
399-
}
400-
401-
goto_programt tmp;
402-
403-
// evaluate function arguments -- they might have
404-
// pointer dereferencing or the like
405-
forall_expr(it, arguments)
406-
{
407-
goto_programt::targett t=tmp.add_instruction();
408-
t->make_other(code_expressiont(*it));
409-
t->source_location=target->source_location;
410-
t->function=target->function;
411-
}
412-
413-
// return value
414-
if(lhs.is_not_nil())
415-
{
416-
side_effect_expr_nondett rhs(lhs.type());
417-
rhs.add_source_location()=target->source_location;
418-
419-
code_assignt code(lhs, rhs);
420-
code.add_source_location()=target->source_location;
421-
422-
goto_programt::targett t=tmp.add_instruction(ASSIGN);
423-
t->source_location=target->source_location;
424-
t->function=target->function;
425-
t->code.swap(code);
426-
}
427-
428-
// kill call
429-
target->type=LOCATION;
430-
target->code.clear();
431-
target++;
432-
433-
dest.destructive_insert(target, tmp);
434-
}
435-
436383
void goto_inlinet::expand_function_call(
437384
goto_programt &dest,
438385
const inline_mapt &inline_map,
@@ -551,7 +498,13 @@ void goto_inlinet::expand_function_call(
551498
}
552499
else // no body available
553500
{
554-
insert_function_nobody(dest, lhs, target, function, arguments);
501+
const irep_idt identifier = function.get_identifier();
502+
503+
if(no_body_set.insert(identifier).second) // newly inserted
504+
{
505+
warning().source_location = function.find_source_location();
506+
warning() << "no body for function `" << identifier << "'" << eom;
507+
}
555508
}
556509
}
557510

‎src/goto-programs/goto_inline_class.h

+1-7
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
910
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
1011
#define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
1112

@@ -171,13 +172,6 @@ class goto_inlinet:public messaget
171172
const symbol_exprt &function,
172173
const exprt::operandst &arguments);
173174

174-
void insert_function_nobody(
175-
goto_programt &dest,
176-
const exprt &lhs,
177-
goto_programt::targett target,
178-
const symbol_exprt &function,
179-
const exprt::operandst &arguments);
180-
181175
void replace_return(
182176
goto_programt &body,
183177
const exprt &lhs);

0 commit comments

Comments
 (0)