From dad59cae178a0caaf1e63206c262b7860f2ddaca Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 18 Nov 2016 14:16:58 +0100 Subject: [PATCH 1/3] rw_set: handle return and other When calculating the set of touched symbols, also consider the symbols that are passed to return statements. Furthermore, continue with reading symbols that are in code labelled with "other". Added a check to test whether return statements have at most one argument. --- src/goto-instrument/rw_set.cpp | 8 ++++++++ src/util/std_code.h | 6 ++++++ 2 files changed, 14 insertions(+) diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index d6a2380dd78..abc7267564c 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -51,6 +51,10 @@ void _rw_set_loct::compute() assert(target->code.operands().size()==2); assign(target->code.op0(), target->code.op1()); } + else if(target->is_return()) + { + read(to_code_return(target->code)); + } else if(target->is_goto() || target->is_assume() || target->is_assert()) @@ -74,6 +78,10 @@ void _rw_set_loct::compute() if(code_function_call.lhs().is_not_nil()) write(code_function_call.lhs()); } + else if(target->is_other()) + { + read(target->code); + } } void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs) diff --git a/src/util/std_code.h b/src/util/std_code.h index 422a492896e..e094544d32d 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -933,12 +933,18 @@ template<> inline bool can_cast_expr(const exprt &base) inline const code_returnt &to_code_return(const codet &code) { assert(code.get_statement()==ID_return); + assert( + code.operands().size() <= 1 && + "there should be at most one operand in an return statement"); return static_cast(code); } inline code_returnt &to_code_return(codet &code) { assert(code.get_statement()==ID_return); + assert( + code.operands().size() <= 1 && + "there should be at most one operand in an return statement"); return static_cast(code); } From 7c273cd55cc9dd2e52d8e423c79f71403d7bf24a Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 18 Nov 2016 14:18:26 +0100 Subject: [PATCH 2/3] objects read: also treat ADDRESS_OF as read Previously, all objects that are passed via address are not considered as being read. This commit adds this case to the analysis. --- src/goto-programs/goto_program.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index a69432ce316..41e17ff23f6 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -340,6 +340,9 @@ void objects_read( else if(src.id()==ID_address_of) { // don't traverse! + assert(src.operands().size() == 1); + dest.push_back(src); + objects_read(src.op0(), dest); } else if(src.id()==ID_dereference) { From 51c956bbc3c73e61376747e3d2d4e857b2d9a52d Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 6 Jul 2018 10:07:38 +0200 Subject: [PATCH 3/3] List global unused variables List variables/symbols that are never read in a given goto-program. Adds regression tests. --- regression/goto-instrument-unused/Makefile | 21 ++++ .../global-unused/main.c | 67 ++++++++++ .../global-unused/test.desc | 21 ++++ regression/goto-instrument-unused/mmap/main.c | 37 ++++++ .../goto-instrument-unused/mmap/test.desc | 16 +++ regression/goto-instrument-unused/run.sh | 6 + src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 10 ++ .../goto_instrument_parse_options.h | 2 +- src/goto-instrument/show_unused.cpp | 114 ++++++++++++++++++ src/goto-instrument/show_unused.h | 21 ++++ 11 files changed, 315 insertions(+), 1 deletion(-) create mode 100644 regression/goto-instrument-unused/Makefile create mode 100644 regression/goto-instrument-unused/global-unused/main.c create mode 100644 regression/goto-instrument-unused/global-unused/test.desc create mode 100644 regression/goto-instrument-unused/mmap/main.c create mode 100644 regression/goto-instrument-unused/mmap/test.desc create mode 100755 regression/goto-instrument-unused/run.sh create mode 100644 src/goto-instrument/show_unused.cpp create mode 100644 src/goto-instrument/show_unused.h diff --git a/regression/goto-instrument-unused/Makefile b/regression/goto-instrument-unused/Makefile new file mode 100644 index 00000000000..2379cc78ca3 --- /dev/null +++ b/regression/goto-instrument-unused/Makefile @@ -0,0 +1,21 @@ +default: tests.log + +test: + @../test.pl -c ../run.sh + +tests.log: ../test.pl + @../test.pl -c ../run.sh + +clean: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \ + fi; \ + done; + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; diff --git a/regression/goto-instrument-unused/global-unused/main.c b/regression/goto-instrument-unused/global-unused/main.c new file mode 100644 index 00000000000..6368de7f138 --- /dev/null +++ b/regression/goto-instrument-unused/global-unused/main.c @@ -0,0 +1,67 @@ +#include + +int a = 2; // unused +char b; +unsigned long int c; +unsigned char d; // write only +int e = 9; // used in return statement + +int usedi = 100; + +struct +{ + int data; +} s_unused, s_writeonly, s_used; + +unsigned long int f() +{ + usedi = usedi + 1; + unsigned long int *p_f = &c; // uses as read + return *p_f; +} + +int *g() +{ + usedi = usedi + 2; + return &e; // uses e, but return value of g is used in write only +} + +int h() +{ + return s_used.data; +} + +unsigned long int i() +{ + return c = d + e; +} + +int main() +{ + int p_a = 5; // unused + unsigned long int p_b = f(); + int *p_c = g(); // unused + int p_d = 6; + int p_e = 7; + int p_f = 8; + int *p_g = g(); + i(); + + s_used.data = 0; + s_writeonly = s_used; + + d = p_b + 9; + printf("%d\n", p_d); + printf("%p\n", &p_e); + printf("%d\n", s_used.data); + printf("%d\n", *p_g); + printf("%d\n", h()); + if(p_f) + { + return 0; + } + else + { + return 1; + } +} diff --git a/regression/goto-instrument-unused/global-unused/test.desc b/regression/goto-instrument-unused/global-unused/test.desc new file mode 100644 index 00000000000..7c855f02ed3 --- /dev/null +++ b/regression/goto-instrument-unused/global-unused/test.desc @@ -0,0 +1,21 @@ +CORE +main.c +0 +^SIGNAL=0$ +main.c:35 variable p_c is never read +main.c:4 variable b is never read +main.c:3 variable a is never read +main.c:11 variable s_writeonly is never read +main.c:33 variable p_a is never read +main.c:11 variable s_unused is never read +-- +main.c:9 variable usedi is never read +main.c:34 variable p_b is never read +main.c:11 variable s_used is never read +main.c:39 variable p_g is never read +main.c:15 variable p_f is never read +main.c:6 variable d is never read +main.c:38 variable p_f is never read +main.c:50 variable return_value_h$1 is never read +main.c:36 variable p_d is never read +^warning: ignoring diff --git a/regression/goto-instrument-unused/mmap/main.c b/regression/goto-instrument-unused/mmap/main.c new file mode 100644 index 00000000000..23dd143835b --- /dev/null +++ b/regression/goto-instrument-unused/mmap/main.c @@ -0,0 +1,37 @@ +#include +#include +#include + +#include +#include +#include + +void *mapmem(off_t offset, size_t length) +{ + int fd; + uint8_t *mem, *tmp; + const int prot = PROT_READ | PROT_WRITE; + const int flags = MAP_SHARED; + + mem = NULL; + fd = open("/dev/mem", O_RDWR | O_CLOEXEC); + if(fd == -1) + goto out; + + tmp = mmap(NULL, length, prot, flags, fd, offset); + close(fd); + if(tmp == MAP_FAILED) + goto out; + mem = tmp; +out: + return mem; +} + +int main() +{ + unsigned int target = 0xffffff; + uint8_t *mem; + mem = mapmem(target, 1024L); + printf("got address %p from target %p\n", mem, (unsigned int *)target); + return 0; +} diff --git a/regression/goto-instrument-unused/mmap/test.desc b/regression/goto-instrument-unused/mmap/test.desc new file mode 100644 index 00000000000..4303addfab6 --- /dev/null +++ b/regression/goto-instrument-unused/mmap/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +0 +^SIGNAL=0$ +-- +mmap/main.c:12 variable mem is never read +mmap/main.c:33 variable mem is never read +mmap/main.c:21 variable return_value_mmap$1 is never rea +mmap/main.c:34 variable return_value_mapmem$1 is never read +mmap/main.c:9 variable offset is never read +mmap/main.c:9 variable length is never read +mmap/main.c:32 variable target is never read +mmap/main.c:11 variable fd is never read +mmap/main.c:14 variable flags is never read +mmap/main.c:13 variable prot is never read +mmap/main.c:12 variable tmp is never read diff --git a/regression/goto-instrument-unused/run.sh b/regression/goto-instrument-unused/run.sh new file mode 100755 index 00000000000..3740cfa8986 --- /dev/null +++ b/regression/goto-instrument-unused/run.sh @@ -0,0 +1,6 @@ +# compile test case +# to be called from sub-directories only, to match path to tools +../../../src/goto-cc/goto-cc main.c -o test &> /dev/null; echo $? + +../../../src/goto-instrument/goto-instrument --show-unused test +echo $? diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index eb67f14f140..207357ee39e 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -54,6 +54,7 @@ SRC = accelerate/accelerate.cpp \ remove_function.cpp \ rw_set.cpp \ show_locations.cpp \ + show_unused.cpp \ skip_loops.cpp \ splice_call.cpp \ stack_depth.cpp \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index fd9a511eeb4..d8fb0a940af 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -100,6 +100,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "undefined_functions.h" #include "remove_function.h" #include "splice_call.h" +#include "show_unused.h" /// invoke main modules int goto_instrument_parse_optionst::doit() @@ -438,6 +439,13 @@ int goto_instrument_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } + if(cmdline.isset("show-unused")) + { + do_indirect_call_and_rtti_removal(); + show_unused(get_ui(), goto_model); + return CPROVER_EXIT_SUCCESS; + } + if(cmdline.isset("show-rw-set")) { namespacet ns(goto_model.symbol_table); @@ -1494,6 +1502,8 @@ void goto_instrument_parse_optionst::help() " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) " --print-internal-representation\n" // NOLINTNEXTLINE(*) " show verbose internal representation of the program\n" + " --show-unused list variables that are never read\n" + " --show-goto-functions show goto program\n" " --list-undefined-functions list functions without body\n" " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*) " --show-natural-loops show natural loop heads\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index dd6950932e4..d1f2d72d847 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -74,7 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com "(print-internal-representation)" \ "(remove-function-pointers)" \ "(show-claims)(property):" \ - "(show-symbol-table)(show-points-to)(show-rw-set)" \ + "(show-symbol-table)(show-points-to)(show-rw-set)(show-unused)" \ "(cav11)" \ OPT_TIMESTAMP \ "(show-natural-loops)(accelerate)(havoc-loops)" \ diff --git a/src/goto-instrument/show_unused.cpp b/src/goto-instrument/show_unused.cpp new file mode 100644 index 00000000000..86f73aa1dda --- /dev/null +++ b/src/goto-instrument/show_unused.cpp @@ -0,0 +1,114 @@ +/*******************************************************************\ + +Module: Show unused variables (including write only) + +Author: Norbert Manthey nmanthey@iamazon.com + +\*******************************************************************/ + +#include +#include + +#include +#include + +#include +#include +#include + +#include "show_unused.h" + +/*******************************************************************\ + +Function: show_unused + + Inputs: symbol table, goto program + + Outputs: prints list of variables that are never read + returns false, if no unused variables have been found, + else true + + Purpose: help to spot variables that are never used globally in a + program + +\*******************************************************************/ + +bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model) +{ + const symbol_tablet &symbol_table = goto_model.symbol_table; + const goto_functionst &goto_functions = goto_model.goto_functions; + const namespacet ns(symbol_table); + rw_set_baset global_reads(ns); + + // get all symbols whose address is used + dirtyt dirty_symbols(goto_functions); + + // compute for each function the set of read and written symbols + forall_goto_functions(it, goto_functions) + { + if(!it->second.body_available()) + continue; + + if(!symbol_table.has_symbol(it->first)) + { + std::cerr << " warning: did not find symbol for: " << id2string(it->first) + << std::endl; + continue; + } + const symbolt *symbol = symbol_table.lookup(it->first); + + value_set_analysis_fit value_sets(ns); + rw_set_functiont rw_set(value_sets, goto_model, symbol->symbol_expr()); + global_reads += rw_set; + } + + // check the symbol table against the global_reads set, collect unused symbols + std::vector> actual_unused_symbols; + // forall_symbols(it, symbol_table.symbols) + for(const auto symbol_pair : symbol_table.symbols) + { + // we are not interested in functions that are not read + if(symbol_pair.second.type.id() == ID_code) + continue; + + // skip internal, anonymous symbols, and if no location is present + if(has_prefix(id2string(symbol_pair.second.name), "__CPROVER")) + continue; + if(has_prefix(id2string(symbol_pair.second.base_name), "#anon")) + continue; + if(symbol_pair.second.location.as_string().empty()) + continue; + + if( + !global_reads.has_r_entry(symbol_pair.second.name) && + dirty_symbols.get_dirty_ids().find(symbol_pair.second.name) == + dirty_symbols.get_dirty_ids().end()) + { + actual_unused_symbols.push_back(symbol_pair); + } + } + + // print collected symbols + switch(ui) + { + case ui_message_handlert::uit::PLAIN: + std::cerr << "found " << actual_unused_symbols.size() + << " symbols to report" << std::endl; + for(auto it = actual_unused_symbols.begin(); + it != actual_unused_symbols.end(); + ++it) + { + const source_locationt &location = it->second.location; + std::cout << concat_dir_file( + id2string(location.get_working_directory()), + id2string(location.get_file())) + << ":" << id2string(location.get_line()) << " variable " + << id2string(it->second.base_name) << " is never read" + << std::endl; + } + break; + default: + assert(false && "chosen UI is not yet implemented"); + } + return 0; +} diff --git a/src/goto-instrument/show_unused.h b/src/goto-instrument/show_unused.h new file mode 100644 index 00000000000..82fc290dc11 --- /dev/null +++ b/src/goto-instrument/show_unused.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: Show unused variables (including write only) + +Author: Norbert Manthey nmanthey@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H +#define CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H + +#include + +#include + +class symbol_tablet; + +/** display all variables that are never read in the program */ +bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model); + +#endif