replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Convert --unreachable-instructions, --unreachable-functions and --reachable-functions 

from specific to general tasks.

If the options are given on their own then the specific version is used.  If a domain
is given as well then that is run and used to determine what is (un)reachable.
This commit is contained in:
martin 2017-12-02 00:12:42 +00:00
parent e936c500d0
commit 1275983b1c
13 changed files with 424 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
regression/goto-analyzer/reachable-functions-basic-json/test.desc Normal file
View File

@ -0,0 +1,9 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--reachable-functions --json -
"function": "main",$
"function": "dead_inside",$
"function": "obviously_dead",$
"function": "not_obviously_dead",$
--
^warning: ignoring

9
regression/goto-analyzer/reachable-functions-basic-text/test.desc Normal file
View File

@ -0,0 +1,9 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--reachable-functions
unreachable.c main 35 42$
unreachable.c dead_inside 8 14$
unreachable.c obviously_dead 16 23$
unreachable.c not_obviously_dead 25 31$
--
^warning: ignoring

11
regression/goto-analyzer/reachable-functions-domain-text/test.desc Normal file
View File

@ -0,0 +1,11 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--reachable-functions --constants
^EXIT=0$
^SIGNAL=0$
unreachable.c main 35 42$
unreachable.c dead_inside 8 14$
unreachable.c obviously_dead 16 23$
unreachable.c not_obviously_dead 25 31$
--
^warning: ignoring

9
regression/goto-analyzer/unreachable-functions-basic-json/test.desc Normal file
View File

@ -0,0 +1,9 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--unreachable-functions --json -
"file name": ".*unreachable.c",
"first line": 3,
"function": "not_called",
"last line": 6
--
^warning: ignoring

6
regression/goto-analyzer/unreachable-functions-basic-text/test.desc Normal file
View File

@ -0,0 +1,6 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--unreachable-functions
unreachable.c not_called 3 6$
--
^warning: ignoring

8
regression/goto-analyzer/unreachable-functions-domain-text/test.desc Normal file
View File

@ -0,0 +1,8 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--unreachable-functions --constants
^EXIT=0$
^SIGNAL=0$
unreachable.c not_called 3 6$
--
^warning: ignoring

21
regression/goto-analyzer/unreachable-instructions-basic-json/test.desc Normal file
View File

@ -0,0 +1,21 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--unreachable-instructions --json -
"function": "not_called",
"unreachableInstructions":
"sourceLocation":
"function": "not_called",
"line": "5",
"statement": "not_called#return_value = x \+ x;"
"sourceLocation":
"function": "not_called",
"line": "5",
"statement": "GOTO 1"
"function": "dead_inside",
"unreachableInstructions":
"sourceLocation":
"function": "dead_inside",
"line": "12",
"statement": "y = y \+ 1;"
--
^warning: ignoring

15
regression/goto-analyzer/unreachable-instructions-basic-text/test.desc Normal file
View File

@ -0,0 +1,15 @@
CORE
unreachable.c
--unreachable-instructions
^EXIT=0$
^SIGNAL=0$
not_called
// 28 file unreachable.c line 5 function not_called$
not_called#return_value = x \+ x;$
// 29 file unreachable.c line 5 function not_called$
GOTO 1$
dead_inside
// 34 file unreachable.c line 12 function dead_inside$
y = y \+ 1;$
--
^warning: ignoring

42
regression/goto-analyzer/unreachable-instructions-basic-text/unreachable.c Normal file
View File

@ -0,0 +1,42 @@
#include <assert.h>
int not_called(int x)
{
return x + x;
}
int dead_inside(int x)
{
int y = x + x;
goto end;
++y;
end : return y;
}
int obviously_dead(int x)
{
if (0)
{
x++;
}
return x;
}
int not_obviously_dead(int x)
{
if (dead_inside(x) != x + x) {
x++;
}
return obviously_dead(x);
}
int nondet_int(void);
int main(int argc, char **argv)
{
int x = 23;
assert(x == not_obviously_dead(x));
return;
}

18
regression/goto-analyzer/unreachable-instructions-domain-text/test.desc Normal file
View File

@ -0,0 +1,18 @@
CORE
../unreachable-instructions-basic-text/unreachable.c
--unreachable-instructions --constants
^EXIT=0$
^SIGNAL=0$
not_called
// 28 file unreachable.c line 5 function not_called$
not_called#return_value = x \+ x;$
// 29 file unreachable.c line 5 function not_called$
GOTO 1$
dead_inside
// 34 file unreachable.c line 12 function dead_inside$
y = y \+ 1;$
obviously_dead
// 40 file unreachable-instructions-basic-text/unreachable.c line 20 function obviously_dead
x = x \+ 1;
--
^warning: ignoring

74
src/goto-analyzer/goto_analyzer_parse_options.cpp
View File

@ -146,20 +146,26 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
options.set_option("taint", true);
options.set_option("specific-analysis", true);
}
// For backwards compatibility,
// these are first recognised as specific analyses
bool reachability_task = false;
if(cmdline.isset("unreachable-instructions"))
{
options.set_option("unreachable-instructions", true);
options.set_option("specific-analysis", true);
reachability_task = true;
}
if(cmdline.isset("unreachable-functions"))
{
options.set_option("unreachable-functions", true);
options.set_option("specific-analysis", true);
reachability_task = true;
}
if(cmdline.isset("reachable-functions"))
{
options.set_option("reachable-functions", true);
options.set_option("specific-analysis", true);
reachability_task = true;
}
if(cmdline.isset("show-local-may-alias"))
{
@ -244,7 +250,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
options.set_option("general-analysis", true);
}
if (options.get_bool_option("general-analysis"))
if(options.get_bool_option("general-analysis") || reachability_task)
{
// Abstract interpreter choice
if(cmdline.isset("location-sensitive"))
@ -280,12 +286,24 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
options.set_option("domain set", true);
}
if(!options.get_bool_option("domain set"))
// Reachability questions, when given with a domain swap from specific
// to general tasks so that they can use the domain & parameterisations.
if(reachability_task)
{
// Deafult to constants as it is light-weight but useful
status() << "Domain defaults to --constants" << eom;
options.set_option("constants", true);
if(options.get_bool_option("domain set"))
{
options.set_option("specific-analysis", false);
options.set_option("general-analysis", true);
}
}
else
{
if(!options.get_bool_option("domain set"))
{
// Default to constants as it is light-weight but useful
status() << "Domain not specified, defaulting to --constants" << eom;
options.set_option("constants", true);
}
}
}
}
@ -468,7 +486,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
}
}
if(options.get_bool_option("unreachable-instructions"))
// If no domain is given, this lightweight version of the analysis is used.
if(options.get_bool_option("unreachable-instructions") &&
options.get_bool_option("specific-analysis"))
{
const std::string json_file=cmdline.get_value("json");
@ -492,7 +512,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
return 0;
}
if(options.get_bool_option("unreachable-functions"))
if(options.get_bool_option("unreachable-functions") &&
options.get_bool_option("specific-analysis"))
{
const std::string json_file=cmdline.get_value("json");
@ -516,7 +537,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
return 0;
}
if(options.get_bool_option("reachable-functions"))
if(options.get_bool_option("reachable-functions") &&
options.get_bool_option("specific-analysis"))
{
const std::string json_file=cmdline.get_value("json");
@ -629,6 +651,30 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
get_message_handler(),
out);
}
else if(options.get_bool_option("unreachable-instructions"))
{
result = static_unreachable_instructions(goto_model,
*analyzer,
options,
get_message_handler(),
out);
}
else if(options.get_bool_option("unreachable-functions"))
{
result = static_unreachable_functions(goto_model,
*analyzer,
options,
get_message_handler(),
out);
}
else if(options.get_bool_option("reachable-functions"))
{
result = static_reachable_functions(goto_model,
*analyzer,
options,
get_message_handler(),
out);
}
else
{
error() << "Unhandled task" << eom;
@ -774,6 +820,11 @@ void goto_analyzer_parse_optionst::help()
" --verify use the abstract domains to check assertions\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --simplify file_name use the abstract domains to simplify the program\n"
" --unreachable-instructions list dead code\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --unreachable-functions list functions unreachable from the entry point\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --reachable-functions list functions reachable from the entry point\n"
"\n"
"Abstract interpreter options:\n"
// NOLINTNEXTLINE(whitespace/line_length)
@ -796,11 +847,6 @@ void goto_analyzer_parse_optionst::help()
"Specific analyses:\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --taint file_name perform taint analysis using rules in given file\n"
" --unreachable-instructions list dead code\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --unreachable-functions list functions unreachable from the entry point\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --reachable-functions list functions reachable from the entry point\n"
"\n"
"C/C++ frontend options:\n"
" -I path set include path (C/C++)\n"

198
src/goto-analyzer/unreachable_instructions.cpp
View File

@ -18,6 +18,7 @@ Date: April 2016
#include <util/json.h>
#include <util/json_expr.h>
#include <util/file_util.h>
#include <util/xml.h>
#include <analyses/cfg_dominators.h>
@ -54,6 +55,16 @@ static void all_unreachable(
dest.insert(std::make_pair(it->location_number, it));
}
static void build_dead_map_from_ai(
const goto_programt &goto_program,
const ai_baset &ai,
dead_mapt &dest)
{
forall_goto_program_instructions(it, goto_program)
if(ai.abstract_state_before(it).is_bottom())
dest.insert(std::make_pair(it->location_number, it));
}
static void output_dead_plain(
const namespacet &ns,
const goto_programt &goto_program,
@ -74,6 +85,34 @@ static void output_dead_plain(
goto_program.output_instruction(ns, "", os, *it->second);
}
static void add_to_xml(
const namespacet &ns,
const goto_programt &goto_program,
const dead_mapt &dead_map,
xmlt &dest)
{
assert(!goto_program.instructions.empty());
goto_programt::const_targett end_function=
goto_program.instructions.end();
--end_function;
assert(end_function->is_end_function());
xmlt &x = dest.new_element("function");
x.set_attribute("name", id2string(end_function->function));
for(dead_mapt::const_iterator it=dead_map.begin();
it!=dead_map.end();
++it)
{
xmlt &inst = x.new_element("instruction");
inst.set_attribute("location_number",
std::to_string(it->second->location_number));
inst.set_attribute("source_location",
it->second->source_location.as_string());
}
return;
}
static void add_to_json(
const namespacet &ns,
const goto_programt &goto_program,
@ -164,6 +203,56 @@ void unreachable_instructions(
os << json_result << '\n';
}
bool static_unreachable_instructions(
const goto_modelt &goto_model,
const ai_baset &ai,
const optionst &options,
message_handlert &message_handler,
std::ostream &out)
{
json_arrayt json_result;
xmlt xml_result("unreachable-instructions");
const namespacet ns(goto_model.symbol_table);
forall_goto_functions(f_it, goto_model.goto_functions)
{
if(!f_it->second.body_available())
continue;
const goto_programt &goto_program=f_it->second.body;
dead_mapt dead_map;
build_dead_map_from_ai(goto_program, ai, dead_map);
if(!dead_map.empty())
{
if(options.get_bool_option("json"))
{
add_to_json(ns, f_it->second.body, dead_map, json_result);
}
else if(options.get_bool_option("xml"))
{
add_to_xml(ns, f_it->second.body, dead_map, xml_result);
}
else
{
INVARIANT(options.get_bool_option("text"),
"Other output formats handled");
output_dead_plain(ns, f_it->second.body, dead_map, out);
}
}
}
if(options.get_bool_option("json") && !json_result.array.empty())
out << json_result << '\n';
else if(options.get_bool_option("xml"))
out << xml_result << '\n';
return false;
}
static void json_output_function(
const irep_idt &function,
const source_locationt &first_location,
@ -183,16 +272,34 @@ static void json_output_function(
json_numbert(id2string(last_location.get_line()));
}
static void xml_output_function(
const irep_idt &function,
const source_locationt &first_location,
const source_locationt &last_location,
xmlt &dest)
{
xmlt &x=dest.new_element("function");
x.set_attribute("name", id2string(function));
x.set_attribute("file name",
concat_dir_file(
id2string(first_location.get_working_directory()),
id2string(first_location.get_file())));
x.set_attribute("first line", id2string(first_location.get_line()));
x.set_attribute("last line", id2string(last_location.get_line()));
}
static void list_functions(
const goto_modelt &goto_model,
const bool json,
const std::set<irep_idt> called,
const optionst &options,
std::ostream &os,
bool unreachable)
{
json_arrayt json_result;
std::set<irep_idt> called=
compute_called_functions(goto_model);
xmlt xml_result(unreachable ?
"unreachable-functions" :
"reachable-functions");
const namespacet ns(goto_model.symbol_table);
@ -226,7 +333,7 @@ static void list_functions(
// this to macros/asm renaming
continue;
if(!json)
if(options.get_bool_option("text"))
{
os << concat_dir_file(
id2string(first_location.get_working_directory()),
@ -235,6 +342,14 @@ static void list_functions(
<< first_location.get_line() << " "
<< last_location.get_line() << "\n";
}
else if(options.get_bool_option("xml"))
{
xml_output_function(
decl.base_name,
first_location,
last_location,
xml_result);
}
else
json_output_function(
decl.base_name,
@ -243,8 +358,10 @@ static void list_functions(
json_result);
}
if(json && !json_result.array.empty())
if(options.get_bool_option("json") && !json_result.array.empty())
os << json_result << '\n';
else if(options.get_bool_option("xml"))
os << xml_result << '\n';
}
void unreachable_functions(
@ -252,7 +369,15 @@ void unreachable_functions(
const bool json,
std::ostream &os)
{
list_functions(goto_model, json, os, true);
optionst options;
if(json)
options.set_option("json", true);
else
options.set_option("text", true);
std::set<irep_idt> called = compute_called_functions(goto_model);
list_functions(goto_model, called, options, os, true);
}
void reachable_functions(
@ -260,5 +385,62 @@ void reachable_functions(
const bool json,
std::ostream &os)
{
list_functions(goto_model, json, os, false);
optionst options;
if(json)
options.set_option("json", true);
else
options.set_option("text", true);
std::set<irep_idt> called = compute_called_functions(goto_model);
list_functions(goto_model, called, options, os, false);
}
std::set<irep_idt> compute_called_functions_from_ai(
const goto_modelt &goto_model,
const ai_baset &ai)
{
std::set<irep_idt> called;
forall_goto_functions(f_it, goto_model.goto_functions)
{
if(!f_it->second.body_available())
continue;
const goto_programt &p = f_it->second.body;
if(!ai.abstract_state_before(p.instructions.begin()).is_bottom())
called.insert(f_it->first);
}
return called;
}
bool static_unreachable_functions(
const goto_modelt &goto_model,
const ai_baset &ai,
const optionst &options,
message_handlert &message_handler,
std::ostream &out)
{
std::set<irep_idt> called = compute_called_functions_from_ai(goto_model, ai);
list_functions(goto_model, called, options, out, true);
return false;
}
bool static_reachable_functions(
const goto_modelt &goto_model,
const ai_baset &ai,
const optionst &options,
message_handlert &message_handler,
std::ostream &out)
{
std::set<irep_idt> called = compute_called_functions_from_ai(goto_model, ai);
list_functions(goto_model, called, options, out, false);
return false;
}

26
src/goto-analyzer/unreachable_instructions.h
View File

@ -16,6 +16,11 @@ Date: April 2016
#include <ostream>
#include <analyses/ai.h>
#include <util/options.h>
#include <util/message.h>
class goto_modelt;
void unreachable_instructions(
@ -33,4 +38,25 @@ void reachable_functions(
const bool json,
std::ostream &os);
bool static_unreachable_instructions(
const goto_modelt &,
const ai_baset &,
const optionst &,
message_handlert &,
std::ostream &);
bool static_unreachable_functions(
const goto_modelt &,
const ai_baset &,
const optionst &,
message_handlert &,
std::ostream &);
bool static_reachable_functions(
const goto_modelt &,
const ai_baset &,
const optionst &,
message_handlert &,
std::ostream &);
#endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H