Skip to content

Commit b441862

Browse files
author
Norbert Manthey
committed
List global unused variables
List variables/symbols that are never read in a given goto-program. Adds regression tests.
1 parent 3a3a605 commit b441862

File tree

11 files changed

+310
-2
lines changed

11 files changed

+310
-2
lines changed

‎regression/goto-instrument-unused/Makefile

+21
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

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
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 {int data;} s_unused, s_writeonly, s_used;
12+
13+
unsigned long int f () {
14+
usedi=usedi + 1;
15+
unsigned long int* p_f=&c; // uses as read
16+
return *p_f;
17+
}
18+
19+
int* g () {
20+
usedi=usedi + 2;
21+
return &e; // uses e, but return value of g is used in write only
22+
}
23+
24+
int h () {
25+
return s_used.data;
26+
}
27+
28+
unsigned long int i () {
29+
return c=d + e;
30+
}
31+
32+
int main() {
33+
int p_a=5; // unused
34+
unsigned long int p_b=f();
35+
int* p_c=g(); // unused
36+
int p_d=6;
37+
int p_e=7;
38+
int p_f=8;
39+
int *p_g=g();
40+
i();
41+
42+
s_used.data=0;
43+
s_writeonly=s_used;
44+
45+
d=p_b+9;
46+
printf("%d\n", p_d);
47+
printf("%p\n", &p_e);
48+
printf("%d\n", s_used.data);
49+
printf("%d\n", *p_g);
50+
printf("%d\n", h());
51+
if(p_f) {
52+
return 0;
53+
} else {
54+
return 1;
55+
}
56+
}

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

+21
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

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#include <stdio.h>
2+
#include <inttypes.h>
3+
#include <sys/mman.h>
4+
5+
#include <sys/types.h>
6+
#include <sys/stat.h>
7+
#include <fcntl.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+
31+
int main() {
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

+16
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

+6
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

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \
2323
wmm/event_graph.cpp wmm/pair_collection.cpp \
2424
goto_instrument_main.cpp horn_encoding.cpp \
2525
thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \
26-
code_contracts.cpp cover.cpp
26+
code_contracts.cpp cover.cpp show_unused.cpp
2727

2828
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2929
../cpp/cpp$(LIBEXT) \

‎src/goto-instrument/goto_instrument_parse_options.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ Author: Daniel Kroening, [email protected]
8585
#include "skip_loops.h"
8686
#include "code_contracts.h"
8787
#include "unwind.h"
88+
#include "show_unused.h"
8889

8990
/*******************************************************************\
9091
@@ -427,6 +428,13 @@ int goto_instrument_parse_optionst::doit()
427428
return 0;
428429
}
429430

431+
if(cmdline.isset("show-unused"))
432+
{
433+
do_function_pointer_removal();
434+
show_unused(get_ui(), symbol_table, goto_functions);
435+
return 0;
436+
}
437+
430438
if(cmdline.isset("show-rw-set"))
431439
{
432440
namespacet ns(symbol_table);
@@ -1440,6 +1448,7 @@ void goto_instrument_parse_optionst::help()
14401448
" --show-properties show the properties\n"
14411449
" --show-symbol-table show symbol table\n"
14421450
" --list-symbols list symbols with type information\n"
1451+
" --show-unused list variables that are never read\n"
14431452
" --show-goto-functions show goto program\n"
14441453
" --list-undefined-functions list functions without body\n"
14451454
" --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)

‎src/goto-instrument/goto_instrument_parse_options.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ Author: Daniel Kroening, [email protected]
5454
"(inline)(partial-inline)(function-inline):(log):" \
5555
"(remove-function-pointers)" \
5656
"(show-claims)(show-properties)(property):" \
57-
"(show-symbol-table)(show-points-to)(show-rw-set)" \
57+
"(show-symbol-table)(show-points-to)(show-rw-set)(show-unused)" \
5858
"(cav11)" \
5959
"(show-natural-loops)(accelerate)(havoc-loops)" \
6060
"(error-label):(string-abstraction)" \

‎src/goto-instrument/show_unused.cpp

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

‎src/goto-instrument/show_unused.h

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
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_functions.h>
15+
16+
class symbol_tablet;
17+
18+
/** display all variables that are never read in the program */
19+
bool show_unused(
20+
ui_message_handlert::uit ui,
21+
const symbol_tablet &symbol_table,
22+
const goto_functionst &goto_functions);
23+
24+
#endif

0 commit comments

Comments
 (0)