Skip to content

Commit 51c956b

Browse files
nmantheynmanthey
committed
List global unused variables
List variables/symbols that are never read in a given goto-program. Adds regression tests.
1 parent 7c273cd commit 51c956b

File tree

11 files changed

+315
-1
lines changed

11 files changed

+315
-1
lines changed

‎regression/goto-instrument-unused/Makefile

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
default: tests.log
2+
3+
test:
4+
@../test.pl -c ../run.sh
5+
6+
tests.log: ../test.pl
7+
@../test.pl -c ../run.sh
8+
9+
clean:
10+
@for dir in *; do \
11+
if [ -d "$$dir" ]; then \
12+
rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
13+
fi; \
14+
done;
15+
16+
show:
17+
@for dir in *; do \
18+
if [ -d "$$dir" ]; then \
19+
vim -o "$$dir/*.c" "$$dir/*.out"; \
20+
fi; \
21+
done;

‎regression/goto-instrument-unused/global-unused/main.c

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
#include <stdio.h>
2+
3+
int a = 2; // unused
4+
char b;
5+
unsigned long int c;
6+
unsigned char d; // write only
7+
int e = 9; // used in return statement
8+
9+
int usedi = 100;
10+
11+
struct
12+
{
13+
int data;
14+
} s_unused, s_writeonly, s_used;
15+
16+
unsigned long int f()
17+
{
18+
usedi = usedi + 1;
19+
unsigned long int *p_f = &c; // uses as read
20+
return *p_f;
21+
}
22+
23+
int *g()
24+
{
25+
usedi = usedi + 2;
26+
return &e; // uses e, but return value of g is used in write only
27+
}
28+
29+
int h()
30+
{
31+
return s_used.data;
32+
}
33+
34+
unsigned long int i()
35+
{
36+
return c = d + e;
37+
}
38+
39+
int main()
40+
{
41+
int p_a = 5; // unused
42+
unsigned long int p_b = f();
43+
int *p_c = g(); // unused
44+
int p_d = 6;
45+
int p_e = 7;
46+
int p_f = 8;
47+
int *p_g = g();
48+
i();
49+
50+
s_used.data = 0;
51+
s_writeonly = s_used;
52+
53+
d = p_b + 9;
54+
printf("%d\n", p_d);
55+
printf("%p\n", &p_e);
56+
printf("%d\n", s_used.data);
57+
printf("%d\n", *p_g);
58+
printf("%d\n", h());
59+
if(p_f)
60+
{
61+
return 0;
62+
}
63+
else
64+
{
65+
return 1;
66+
}
67+
}

‎regression/goto-instrument-unused/global-unused/test.desc

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
CORE
2+
main.c
3+
0
4+
^SIGNAL=0$
5+
main.c:35 variable p_c is never read
6+
main.c:4 variable b is never read
7+
main.c:3 variable a is never read
8+
main.c:11 variable s_writeonly is never read
9+
main.c:33 variable p_a is never read
10+
main.c:11 variable s_unused is never read
11+
--
12+
main.c:9 variable usedi is never read
13+
main.c:34 variable p_b is never read
14+
main.c:11 variable s_used is never read
15+
main.c:39 variable p_g is never read
16+
main.c:15 variable p_f is never read
17+
main.c:6 variable d is never read
18+
main.c:38 variable p_f is never read
19+
main.c:50 variable return_value_h$1 is never read
20+
main.c:36 variable p_d is never read
21+
^warning: ignoring

‎regression/goto-instrument-unused/mmap/main.c

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#include <inttypes.h>
2+
#include <stdio.h>
3+
#include <sys/mman.h>
4+
5+
#include <fcntl.h>
6+
#include <sys/stat.h>
7+
#include <sys/types.h>
8+
9+
void *mapmem(off_t offset, size_t length)
10+
{
11+
int fd;
12+
uint8_t *mem, *tmp;
13+
const int prot = PROT_READ | PROT_WRITE;
14+
const int flags = MAP_SHARED;
15+
16+
mem = NULL;
17+
fd = open("/dev/mem", O_RDWR | O_CLOEXEC);
18+
if(fd == -1)
19+
goto out;
20+
21+
tmp = mmap(NULL, length, prot, flags, fd, offset);
22+
close(fd);
23+
if(tmp == MAP_FAILED)
24+
goto out;
25+
mem = tmp;
26+
out:
27+
return mem;
28+
}
29+
30+
int main()
31+
{
32+
unsigned int target = 0xffffff;
33+
uint8_t *mem;
34+
mem = mapmem(target, 1024L);
35+
printf("got address %p from target %p\n", mem, (unsigned int *)target);
36+
return 0;
37+
}

‎regression/goto-instrument-unused/mmap/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
0
4+
^SIGNAL=0$
5+
--
6+
mmap/main.c:12 variable mem is never read
7+
mmap/main.c:33 variable mem is never read
8+
mmap/main.c:21 variable return_value_mmap$1 is never rea
9+
mmap/main.c:34 variable return_value_mapmem$1 is never read
10+
mmap/main.c:9 variable offset is never read
11+
mmap/main.c:9 variable length is never read
12+
mmap/main.c:32 variable target is never read
13+
mmap/main.c:11 variable fd is never read
14+
mmap/main.c:14 variable flags is never read
15+
mmap/main.c:13 variable prot is never read
16+
mmap/main.c:12 variable tmp is never read

‎regression/goto-instrument-unused/run.sh

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# compile test case
2+
# to be called from sub-directories only, to match path to tools
3+
../../../src/goto-cc/goto-cc main.c -o test &> /dev/null; echo $?
4+
5+
../../../src/goto-instrument/goto-instrument --show-unused test
6+
echo $?

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ SRC = accelerate/accelerate.cpp \
5454
remove_function.cpp \
5555
rw_set.cpp \
5656
show_locations.cpp \
57+
show_unused.cpp \
5758
skip_loops.cpp \
5859
splice_call.cpp \
5960
stack_depth.cpp \

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,7 @@ Author: Daniel Kroening, [email protected]
100100
#include "undefined_functions.h"
101101
#include "remove_function.h"
102102
#include "splice_call.h"
103+
#include "show_unused.h"
103104

104105
/// invoke main modules
105106
int goto_instrument_parse_optionst::doit()
@@ -438,6 +439,13 @@ int goto_instrument_parse_optionst::doit()
438439
return CPROVER_EXIT_SUCCESS;
439440
}
440441

442+
if(cmdline.isset("show-unused"))
443+
{
444+
do_indirect_call_and_rtti_removal();
445+
show_unused(get_ui(), goto_model);
446+
return CPROVER_EXIT_SUCCESS;
447+
}
448+
441449
if(cmdline.isset("show-rw-set"))
442450
{
443451
namespacet ns(goto_model.symbol_table);
@@ -1494,6 +1502,8 @@ void goto_instrument_parse_optionst::help()
14941502
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
14951503
" --print-internal-representation\n" // NOLINTNEXTLINE(*)
14961504
" show verbose internal representation of the program\n"
1505+
" --show-unused list variables that are never read\n"
1506+
" --show-goto-functions show goto program\n"
14971507
" --list-undefined-functions list functions without body\n"
14981508
" --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
14991509
" --show-natural-loops show natural loop heads\n"

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ Author: Daniel Kroening, [email protected]
7474
"(print-internal-representation)" \
7575
"(remove-function-pointers)" \
7676
"(show-claims)(property):" \
77-
"(show-symbol-table)(show-points-to)(show-rw-set)" \
77+
"(show-symbol-table)(show-points-to)(show-rw-set)(show-unused)" \
7878
"(cav11)" \
7979
OPT_TIMESTAMP \
8080
"(show-natural-loops)(accelerate)(havoc-loops)" \

‎src/goto-instrument/show_unused.cpp

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/*******************************************************************\
2+
3+
Module: Show unused variables (including write only)
4+
5+
Author: Norbert Manthey [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <cassert>
10+
#include <iostream>
11+
12+
#include <util/file_util.h>
13+
#include <util/prefix.h>
14+
15+
#include <analyses/dirty.h>
16+
#include <goto-instrument/rw_set.h>
17+
#include <pointer-analysis/value_set_analysis_fi.h>
18+
19+
#include "show_unused.h"
20+
21+
/*******************************************************************\
22+
23+
Function: show_unused
24+
25+
Inputs: symbol table, goto program
26+
27+
Outputs: prints list of variables that are never read
28+
returns false, if no unused variables have been found,
29+
else true
30+
31+
Purpose: help to spot variables that are never used globally in a
32+
program
33+
34+
\*******************************************************************/
35+
36+
bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model)
37+
{
38+
const symbol_tablet &symbol_table = goto_model.symbol_table;
39+
const goto_functionst &goto_functions = goto_model.goto_functions;
40+
const namespacet ns(symbol_table);
41+
rw_set_baset global_reads(ns);
42+
43+
// get all symbols whose address is used
44+
dirtyt dirty_symbols(goto_functions);
45+
46+
// compute for each function the set of read and written symbols
47+
forall_goto_functions(it, goto_functions)
48+
{
49+
if(!it->second.body_available())
50+
continue;
51+
52+
if(!symbol_table.has_symbol(it->first))
53+
{
54+
std::cerr << " warning: did not find symbol for: " << id2string(it->first)
55+
<< std::endl;
56+
continue;
57+
}
58+
const symbolt *symbol = symbol_table.lookup(it->first);
59+
60+
value_set_analysis_fit value_sets(ns);
61+
rw_set_functiont rw_set(value_sets, goto_model, symbol->symbol_expr());
62+
global_reads += rw_set;
63+
}
64+
65+
// check the symbol table against the global_reads set, collect unused symbols
66+
std::vector<std::pair<const irep_idt, symbolt>> actual_unused_symbols;
67+
// forall_symbols(it, symbol_table.symbols)
68+
for(const auto symbol_pair : symbol_table.symbols)
69+
{
70+
// we are not interested in functions that are not read
71+
if(symbol_pair.second.type.id() == ID_code)
72+
continue;
73+
74+
// skip internal, anonymous symbols, and if no location is present
75+
if(has_prefix(id2string(symbol_pair.second.name), "__CPROVER"))
76+
continue;
77+
if(has_prefix(id2string(symbol_pair.second.base_name), "#anon"))
78+
continue;
79+
if(symbol_pair.second.location.as_string().empty())
80+
continue;
81+
82+
if(
83+
!global_reads.has_r_entry(symbol_pair.second.name) &&
84+
dirty_symbols.get_dirty_ids().find(symbol_pair.second.name) ==
85+
dirty_symbols.get_dirty_ids().end())
86+
{
87+
actual_unused_symbols.push_back(symbol_pair);
88+
}
89+
}
90+
91+
// print collected symbols
92+
switch(ui)
93+
{
94+
case ui_message_handlert::uit::PLAIN:
95+
std::cerr << "found " << actual_unused_symbols.size()
96+
<< " symbols to report" << std::endl;
97+
for(auto it = actual_unused_symbols.begin();
98+
it != actual_unused_symbols.end();
99+
++it)
100+
{
101+
const source_locationt &location = it->second.location;
102+
std::cout << concat_dir_file(
103+
id2string(location.get_working_directory()),
104+
id2string(location.get_file()))
105+
<< ":" << id2string(location.get_line()) << " variable "
106+
<< id2string(it->second.base_name) << " is never read"
107+
<< std::endl;
108+
}
109+
break;
110+
default:
111+
assert(false && "chosen UI is not yet implemented");
112+
}
113+
return 0;
114+
}

‎src/goto-instrument/show_unused.h

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/*******************************************************************\
2+
3+
Module: Show unused variables (including write only)
4+
5+
Author: Norbert Manthey [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H
10+
#define CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H
11+
12+
#include <util/ui_message.h>
13+
14+
#include <goto-programs/goto_model.h>
15+
16+
class symbol_tablet;
17+
18+
/** display all variables that are never read in the program */
19+
bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model);
20+
21+
#endif

0 commit comments

Comments
 (0)