diff --git a/CHANGELOG b/CHANGELOG index 0f15c3d5081..14fd89ae52c 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,12 @@ +5.8 +=== + +* GOTO-INSTRUMENT: New option --list-calls-args +* GOTO-INSTRUMENT: New option --print-path-lenghts +* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions +* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false + + 5.7 === diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index bceddfadc54..04836903ea9 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -265,6 +265,54 @@ int goto_analyzer_parse_optionst::doit() return 0; } + if(cmdline.isset("unreachable-functions")) + { + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + unreachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + unreachable_functions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_functions(goto_model, true, ofs); + } + + return 0; + } + + if(cmdline.isset("reachable-functions")) + { + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + reachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + reachable_functions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + reachable_functions(goto_model, true, ofs); + } + + return 0; + } + if(cmdline.isset("show-local-may-alias")) { namespacet ns(goto_model.symbol_table); @@ -489,6 +537,10 @@ void goto_analyzer_parse_optionst::help() // 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" " --intervals interval analysis\n" " --non-null non-null analysis\n" "\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 7b319c8b99b..416a6df1888 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -36,7 +36,8 @@ class optionst; "(taint):(show-taint)" \ "(show-local-may-alias)" \ "(json):(xml):" \ - "(unreachable-instructions)" \ + "(unreachable-instructions)(unreachable-functions)" \ + "(reachable-functions)" \ "(intervals)(show-intervals)" \ "(non-null)(show-non-null)" diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 06edd28bca6..73514f5b5d5 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -198,7 +198,12 @@ void unreachable_instructions( const goto_programt &goto_program=f_it->second.body; dead_mapt dead_map; - if(called.find(f_it->first)!=called.end()) + const symbolt &decl=ns.lookup(f_it->first); + + // f_it->first may be a link-time renamed version, use the + // base_name instead; do not list inlined functions + if(called.find(decl.base_name)!=called.end() || + f_it->second.is_inlined()) unreachable_instructions(goto_program, dead_map); else all_unreachable(goto_program, dead_map); @@ -215,3 +220,150 @@ void unreachable_instructions( if(json && !json_result.array.empty()) os << json_result << std::endl; } + +/*******************************************************************\ + +Function: json_output_function + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void json_output_function( + const irep_idt &function, + const source_locationt &first_location, + const source_locationt &last_location, + json_arrayt &dest) +{ + json_objectt &entry=dest.push_back().make_object(); + + entry["function"]=json_stringt(id2string(function)); + entry["file name"]= + json_stringt(concat_dir_file( + id2string(first_location.get_working_directory()), + id2string(first_location.get_file()))); + entry["first line"]= + json_numbert(id2string(first_location.get_line())); + entry["last line"]= + json_numbert(id2string(last_location.get_line())); +} + +/*******************************************************************\ + +Function: list_functions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void list_functions( + const goto_modelt &goto_model, + const bool json, + std::ostream &os, + bool unreachable) +{ + json_arrayt json_result; + + std::set called; + compute_called_functions(goto_model, called); + + const namespacet ns(goto_model.symbol_table); + + forall_goto_functions(f_it, goto_model.goto_functions) + { + const symbolt &decl=ns.lookup(f_it->first); + + // f_it->first may be a link-time renamed version, use the + // base_name instead; do not list inlined functions + if(unreachable == + (called.find(decl.base_name)!=called.end() || + f_it->second.is_inlined())) + continue; + + source_locationt first_location=decl.location; + + source_locationt last_location; + if(f_it->second.body_available()) + { + const goto_programt &goto_program=f_it->second.body; + + goto_programt::const_targett end_function= + goto_program.instructions.end(); + --end_function; + assert(end_function->is_end_function()); + last_location=end_function->source_location; + } + else + // completely ignore functions without a body, both for + // reachable and unreachable functions; we could also restrict + // this to macros/asm renaming + continue; + + if(!json) + { + os << concat_dir_file( + id2string(first_location.get_working_directory()), + id2string(first_location.get_file())) << " " + << decl.base_name << " " + << first_location.get_line() << " " + << last_location.get_line() << "\n"; + } + else + json_output_function( + decl.base_name, + first_location, + last_location, + json_result); + } + + if(json && !json_result.array.empty()) + os << json_result << std::endl; +} + +/*******************************************************************\ + +Function: unreachable_functions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void unreachable_functions( + const goto_modelt &goto_model, + const bool json, + std::ostream &os) +{ + list_functions(goto_model, json, os, true); +} + +/*******************************************************************\ + +Function: reachable_functions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void reachable_functions( + const goto_modelt &goto_model, + const bool json, + std::ostream &os) +{ + list_functions(goto_model, json, os, false); +} diff --git a/src/goto-analyzer/unreachable_instructions.h b/src/goto-analyzer/unreachable_instructions.h index 137e6a62040..a408e004bd8 100644 --- a/src/goto-analyzer/unreachable_instructions.h +++ b/src/goto-analyzer/unreachable_instructions.h @@ -20,4 +20,14 @@ void unreachable_instructions( const bool json, std::ostream &os); +void unreachable_functions( + const goto_modelt &, + const bool json, + std::ostream &os); + +void reachable_functions( + const goto_modelt &, + const bool json, + std::ostream &os); + #endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 4cbd6121b24..3fbaac8620b 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -23,7 +23,8 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \ wmm/event_graph.cpp wmm/pair_collection.cpp \ goto_instrument_main.cpp horn_encoding.cpp \ thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \ - code_contracts.cpp cover.cpp model_argc_argv.cpp + code_contracts.cpp cover.cpp model_argc_argv.cpp \ + undefined_functions.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 65fa225c7ed..875d89051a6 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -13,6 +13,7 @@ Date: April 2013 #include #include +#include #include "call_sequences.h" @@ -358,3 +359,83 @@ void check_call_sequence(const goto_functionst &goto_functions) check_call_sequencet(goto_functions, sequence)(); } + +/*******************************************************************\ + +Function: list_calls_and_arguments + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void list_calls_and_arguments( + const namespacet &ns, + const irep_idt &function, + const goto_programt &goto_program) +{ + forall_goto_program_instructions(i_it, goto_program) + { + if(!i_it->is_function_call()) + continue; + + const code_function_callt call=to_code_function_call(i_it->code); + + const exprt &f=call.function(); + + if(f.id()!=ID_symbol) + continue; + + const irep_idt &identifier=to_symbol_expr(f).get_identifier(); + if(identifier=="__CPROVER_initialize") + continue; + + std::string name=from_expr(ns, identifier, f); + std::string::size_type java_type_suffix=name.find(":("); + if(java_type_suffix!=std::string::npos) + name.erase(java_type_suffix); + + std::cout << "found call to " << name; + + if(!call.arguments().empty()) + { + std::cout << " with arguments "; + for(exprt::operandst::const_iterator + it=call.arguments().begin(); + it!=call.arguments().end(); + ++it) + { + if(it!=call.arguments().begin()) + std::cout << ", "; + std::cout << from_expr(ns, identifier, simplify_expr(*it, ns)); + } + } + + std::cout << '\n'; + } +} + +/*******************************************************************\ + +Function: show_call_sequences + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void list_calls_and_arguments( + const namespacet &ns, + const goto_functionst &goto_functions) +{ + // do per function + + forall_goto_functions(f_it, goto_functions) + list_calls_and_arguments(ns, f_it->first, f_it->second.body); +} diff --git a/src/goto-instrument/call_sequences.h b/src/goto-instrument/call_sequences.h index 5036d5bc845..ecfc5921ef8 100644 --- a/src/goto-instrument/call_sequences.h +++ b/src/goto-instrument/call_sequences.h @@ -16,4 +16,8 @@ Date: September 2011 void show_call_sequences(const goto_functionst &goto_functions); void check_call_sequence(const goto_functionst &goto_functions); +void list_calls_and_arguments( + const namespacet &ns, + const goto_functionst &goto_functions); + #endif // CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 96b21195a82..a54bc11f2ad 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -14,6 +14,8 @@ Date: December 2012 #include #include +#include + #include "count_eloc.h" typedef std::unordered_set linest; @@ -104,3 +106,83 @@ void list_eloc(const goto_functionst &goto_functions) std::cout << file << ':' << line << '\n'; } } + +/*******************************************************************\ + +Function: print_path_lengths + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void print_path_lengths(const goto_functionst &goto_functions) +{ + const irep_idt &entry_point=goto_functions.entry_point(); + goto_functionst::function_mapt::const_iterator start= + goto_functions.function_map.find(entry_point); + + if(start==goto_functions.function_map.end() || + !start->second.body_available()) + { + std::cout << "No entry point found, path length undefined\n"; + return; + } + + struct visited_cfg_nodet + { + bool visited; + + visited_cfg_nodet():visited(false) + { + } + }; + + typedef cfg_baset cfgt; + cfgt cfg; + cfg(goto_functions); + + const goto_programt &start_program=start->second.body; + + const cfgt::entryt &start_node= + cfg.entry_map[start_program.instructions.begin()]; + const cfgt::entryt &last_node= + cfg.entry_map[--start_program.instructions.end()]; + + cfgt::patht shortest_path; + cfg.shortest_path(start_node, last_node, shortest_path); + std::cout << "Shortest control-flow path: " << shortest_path.size() + << " instructions\n"; + + std::size_t n_loops=0, loop_ins=0; + forall_goto_functions(gf_it, goto_functions) + forall_goto_program_instructions(i_it, gf_it->second.body) + // loops or recursion + if(i_it->is_backwards_goto() || + i_it==gf_it->second.body.instructions.begin()) + { + const cfgt::entryt &node=cfg.entry_map[i_it]; + cfgt::patht loop; + cfg.shortest_loop(node, loop); + + if(!loop.empty()) + { + ++n_loops; + loop_ins+=loop.size()-1; + } + } + + if(n_loops>0) + std::cout << "Loop information: " << n_loops << " loops, " + << loop_ins << " instructions in shortest paths of loop bodies\n"; + + std::size_t n_reachable=0; + cfg.visit_reachable(start_node); + for(std::size_t i=0; ifirst).is_macro && - !it->second.body_available()) - std::cout << it->first << std::endl; + list_undefined_functions(goto_functions, ns, std::cout); return 0; } @@ -752,6 +766,13 @@ int goto_instrument_parse_optionst::doit() remove_unused_functions(goto_functions, get_message_handler()); } + if(cmdline.isset("undefined-function-is-assume-false")) + { + do_indirect_call_and_rtti_removal(); + + undefined_function_abort_path(goto_functions); + } + // write new binary? if(cmdline.args.size()==2) { @@ -1508,6 +1529,8 @@ void goto_instrument_parse_optionst::help() " --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" + // NOLINTNEXTLINE(whitespace/line_length) + " --list-calls-args list all function calls with their arguments\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" @@ -1530,6 +1553,8 @@ void goto_instrument_parse_optionst::help() " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*) " --check-invariant function instruments invariant checking function\n" " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) + " --undefined-function-is-assume-false\n" + " convert each call to an undefined function to assume(false)\n" "\n" "Loop transformations:\n" " --k-induction check loops with k-induction\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 180eeb7a2f5..fff8910971b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -69,7 +69,8 @@ Author: Daniel Kroening, kroening@kroening.com "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ - "(show-threaded)" + "(show-threaded)(list-calls-args)(print-path-lengths)" \ + "(undefined-function-is-assume-false)" class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-instrument/undefined_functions.cpp new file mode 100644 index 00000000000..53fff3ff84b --- /dev/null +++ b/src/goto-instrument/undefined_functions.cpp @@ -0,0 +1,81 @@ +/*******************************************************************\ + +Module: Handling of functions without body + +Author: Michael Tautschnig + +Date: July 2016 + +\*******************************************************************/ + +#include + +#include + +#include "undefined_functions.h" + +/*******************************************************************\ + +Function: list_undefined_functions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void list_undefined_functions( + const goto_functionst &goto_functions, + const namespacet &ns, + std::ostream &os) +{ + forall_goto_functions(it, goto_functions) + if(!ns.lookup(it->first).is_macro && + !it->second.body_available()) + os << it->first << std::endl; +} + +/*******************************************************************\ + +Function: undefined_function_abort_path + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void undefined_function_abort_path(goto_functionst &goto_functions) +{ + Forall_goto_functions(it, goto_functions) + Forall_goto_program_instructions(iit, it->second.body) + { + goto_programt::instructiont &ins=*iit; + + if(!ins.is_function_call()) + continue; + + const code_function_callt &call=to_code_function_call(ins.code); + + if(call.function().id()!=ID_symbol) + continue; + + const irep_idt &function= + to_symbol_expr(call.function()).get_identifier(); + + goto_functionst::function_mapt::const_iterator entry= + goto_functions.function_map.find(function); + assert(entry!=goto_functions.function_map.end()); + + if(entry->second.body_available()) + continue; + + ins.make_assumption(false_exprt()); + ins.source_location.set_comment( + "`"+id2string(function)+"' is undefined"); + } +} diff --git a/src/goto-instrument/undefined_functions.h b/src/goto-instrument/undefined_functions.h new file mode 100644 index 00000000000..7b700c839a0 --- /dev/null +++ b/src/goto-instrument/undefined_functions.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Handling of functions without body + +Author: Michael Tautschnig + +Date: July 2016 + +\*******************************************************************/ + +#ifndef CPROVER_UNDEFINED_FUNCTIONS_H +#define CPROVER_UNDEFINED_FUNCTIONS_H + +#include + +class goto_functionst; + +void list_undefined_functions( + const goto_functionst &goto_functions, + const namespacet &ns, + std::ostream &os); + +void undefined_function_abort_path(goto_functionst &goto_functions); + +#endif