From 3ed7a1412d84c5940a5a56b8aa7052366549cf24 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 10 Jan 2017 18:20:40 +0000 Subject: [PATCH] Merge pull request #44 from NathanJPhillips/cleanup/issue-317 Cleanup logging --- src/analyses/pointsto_summary_domain.cpp | 74 +-- src/analyses/pointsto_summary_domain.h | 14 +- src/goto-analyzer/pointsto_temp_analyser.cpp | 291 ++++++----- src/goto-analyzer/pointsto_temp_analyser.h | 6 +- src/goto-analyzer/taint_fast_analyser.cpp | 72 +-- src/goto-analyzer/taint_fast_analyser.h | 14 +- src/goto-analyzer/taint_planner.cpp | 32 +- src/goto-analyzer/taint_planner.h | 16 +- src/goto-analyzer/taint_summary.cpp | 484 +++++++++---------- src/goto-analyzer/taint_summary.h | 10 +- src/goto-analyzer/taint_trace_recogniser.cpp | 418 ++++++++-------- src/goto-analyzer/taint_trace_recogniser.h | 8 +- src/summaries/summary.h | 4 +- src/summaries/summary_dump.cpp | 65 +-- src/summaries/summary_dump.h | 38 +- 15 files changed, 699 insertions(+), 847 deletions(-) diff --git a/src/analyses/pointsto_summary_domain.cpp b/src/analyses/pointsto_summary_domain.cpp index 02b053e0a1ff..6c8b93a1bcef 100644 --- a/src/analyses/pointsto_summary_domain.cpp +++ b/src/analyses/pointsto_summary_domain.cpp @@ -505,23 +505,25 @@ pointsto_expressiont pointsto_evaluate_expression( } pointsto_expressiont pointsto_evaluate_access_path( - const pointsto_rulest& domain_value, - const access_path_to_memoryt& access_path, - const bool as_lvalue, - const irep_idt& fn_name, - const unsigned int location_id, - const namespacet& ns - ) -{ + const pointsto_rulest& domain_value, + const access_path_to_memoryt& access_path, + const bool as_lvalue, + const irep_idt& fn_name, + const unsigned int location_id, + const namespacet& ns, + message_handlert& message_handler) +{ + messaget msg(message_handler); if (is_typecast(access_path)) - return pointsto_evaluate_access_path( - domain_value, - get_typecast_target(access_path,ns), - as_lvalue, - fn_name, - location_id, - ns - ); + return + pointsto_evaluate_access_path( + domain_value, + get_typecast_target(access_path,ns), + as_lvalue, + fn_name, + location_id, + ns, + message_handler); if (is_identifier(access_path)) { @@ -534,13 +536,13 @@ pointsto_expressiont pointsto_evaluate_access_path( } if (is_dereference(access_path)) return pointsto_evaluate_access_path( - domain_value, - get_dereferenced_operand(access_path), - false, - fn_name, - location_id, - ns - ); + domain_value, + get_dereferenced_operand(access_path), + false, + fn_name, + location_id, + ns, + message_handler); if (is_side_effect_malloc(access_path)) { return pointsto_set_of_concrete_targetst( @@ -553,14 +555,14 @@ pointsto_expressiont pointsto_evaluate_access_path( { const irep_idt& member_name = get_member_name(access_path); const pointsto_expressiont accessor = - pointsto_evaluate_access_path( - domain_value, - get_member_accessor(access_path), - false, - fn_name, - location_id, - ns - ); + pointsto_evaluate_access_path( + domain_value, + get_member_accessor(access_path), + false, + fn_name, + location_id, + ns, + message_handler); if (pointsto_is_empty_set_of_targets(accessor)) return accessor; const pointsto_address_shiftt shift( @@ -577,11 +579,11 @@ pointsto_expressiont pointsto_evaluate_access_path( ); } - std::cout << "\n\n**** UNSUPPORTED YET ***********************************\n"; - dump_access_path_in_html(access_path,ns,std::cout); - std::cout << "\n"; - dump_irept(access_path,std::cout); - std::cout.flush(); + msg.warning() << "\n\n**** UNSUPPORTED YET ***********************************\n"; + dump_access_path_in_html(access_path, ns, msg.debug()); + msg.debug() << "\n"; + dump_irept(access_path, msg.debug()); + msg.debug() << messaget::eom; return pointsto_expression_empty_set_of_targets(); } diff --git a/src/analyses/pointsto_summary_domain.h b/src/analyses/pointsto_summary_domain.h index cd853dfb3e83..0e43a0d476ab 100644 --- a/src/analyses/pointsto_summary_domain.h +++ b/src/analyses/pointsto_summary_domain.h @@ -275,13 +275,13 @@ pointsto_expressiont pointsto_evaluate_expression( ); pointsto_expressiont pointsto_evaluate_access_path( - const pointsto_rulest& domain_value, - const access_path_to_memoryt& access_path, - const bool as_lvalue, - const irep_idt& fn_name, - const unsigned int location_id, - const namespacet& ns - ); + const pointsto_rulest& domain_value, + const access_path_to_memoryt& access_path, + const bool as_lvalue, + const irep_idt& fn_name, + const unsigned int location_id, + const namespacet& ns, + message_handlert& message_handler); pointsto_expressiont pointsto_temp_prune_pure_locals( diff --git a/src/goto-analyzer/pointsto_temp_analyser.cpp b/src/goto-analyzer/pointsto_temp_analyser.cpp index 8eee237c2ea7..0cc495cdbfc5 100644 --- a/src/goto-analyzer/pointsto_temp_analyser.cpp +++ b/src/goto-analyzer/pointsto_temp_analyser.cpp @@ -28,15 +28,15 @@ std::string pointsto_temp_summaryt::description() const noexcept static void initialise_domain( - irep_idt const& function_id, - goto_functionst::goto_functiont const& function, - goto_functionst::function_mapt const& functions_map, - namespacet const& ns, - database_of_summariest const& database, - pointsto_temp_domaint& domain, - std::ostream* const log - ) + irep_idt const& function_id, + goto_functionst::goto_functiont const& function, + goto_functionst::function_mapt const& functions_map, + namespacet const& ns, + database_of_summariest const& database, + pointsto_temp_domaint& domain, + message_handlert& message_handler) { + messaget msg(message_handler); pointsto_rulest entry_map; for (std::size_t i = 0UL; i != function.type.parameters().size(); ++i) { @@ -62,20 +62,18 @@ static void initialise_domain( ++it) domain.insert({it,pointsto_rulest{}}); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Initialising the domain

\n" - "

Domain value at the entry location:

\n" - ; + msg.debug() << "* Initialising the domain\n" + "Domain value at the entry location:\n"; pointsto_dump_rules_in_html( - domain.at(function.body.instructions.cbegin()), - *log - ); - *log << "

Domain value at all other locations:

\n"; + domain.at(function.body.instructions.cbegin()), + msg.debug()); + msg.debug() << "\nDomain value at all other locations:\n"; pointsto_dump_rules_in_html( - domain.at(std::prev(function.body.instructions.cend())), - *log - ); + domain.at(std::prev(function.body.instructions.cend())), + msg.debug()); + msg.debug() << messaget::eom; } } @@ -147,18 +145,18 @@ static pointsto_rulest pointsto_temp_join( static pointsto_rulest pointsto_temp_assign( - const pointsto_rulest& a, - const access_path_to_memoryt& lhs, - const access_path_to_memoryt& rhs, - const irep_idt& fn_name, - const unsigned int location_id, - const namespacet& ns - ) + const pointsto_rulest& a, + const access_path_to_memoryt& lhs, + const access_path_to_memoryt& rhs, + const irep_idt& fn_name, + const unsigned int location_id, + const namespacet& ns, + message_handlert& message_handler) { pointsto_expressiont const left = - pointsto_evaluate_access_path(a,lhs,true,fn_name,location_id,ns); + pointsto_evaluate_access_path(a, lhs, true, fn_name, location_id, ns, message_handler); pointsto_expressiont const right = - pointsto_evaluate_access_path(a,rhs,false,fn_name,location_id,ns); + pointsto_evaluate_access_path(a, rhs, false, fn_name, location_id, ns, message_handler); pointsto_rulest result; for (const auto& elem : a) result = @@ -178,15 +176,15 @@ static pointsto_rulest pointsto_temp_assign( static pointsto_rulest pointsto_temp_transform( - const pointsto_rulest& a, - goto_programt::instructiont const& I, - const irep_idt& caller_ident, - const goto_functionst::function_mapt& functions_map, - const database_of_summariest& database, - const namespacet& ns, - std::ostream* const log - ) + const pointsto_rulest& a, + goto_programt::instructiont const& I, + const irep_idt& caller_ident, + const goto_functionst::function_mapt& functions_map, + const database_of_summariest& database, + const namespacet& ns, + message_handlert& message_handler) { + messaget msg(message_handler); pointsto_rulest result = a; switch(I.type) { @@ -195,77 +193,76 @@ static pointsto_rulest pointsto_temp_transform( code_assignt const& asgn = to_code_assign(I.code); if (is_pointer(asgn.lhs(),ns)) { - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

\nRecognised ASSIGN instruction to a pointer '"; - dump_access_path_in_html(asgn.lhs(),ns,*log); - *log << "'.

\n"; + msg.debug() << "Recognised ASSIGN instruction to a pointer '"; + dump_access_path_in_html(asgn.lhs(), ns, msg.debug()); + msg.debug() << "'." << messaget::eom; } result = pointsto_temp_assign( - a, - asgn.lhs(), - asgn.rhs(), - caller_ident, - I.location_number, - ns - ); + a, + asgn.lhs(), + asgn.rhs(), + caller_ident, + I.location_number, + ns, + message_handler); } else { - if (log != nullptr) - *log << "

\nRecognised ASSIGN instruction NOT writing to a pointer." - " So, we use identity as a transformation function.

\n"; + msg.debug() << "Recognised ASSIGN instruction NOT writing to a pointer." + " So, we use identity as a transformation function." + << messaget::eom; } } break; case FUNCTION_CALL: - if (log != nullptr) - *log << "

!!! WARNING !!! : Unsupported instruction FUNCTION_CALL " - "reached. So, we use identity as a transformation function.

\n" - ; + msg.warning() << "!!! WARNING !!! : Unsupported instruction FUNCTION_CALL " + "reached. So, we use identity as a transformation function." + << messaget::eom; break; case DEAD: - if (log != nullptr) - *log << "

!!! WARNING !!! : Unsupported instruction DEAD reached. " - "So, we use identity as a transformation function.

\n"; + msg.warning() << "!!! WARNING !!! : Unsupported instruction DEAD reached. " + "So, we use identity as a transformation function." + << messaget::eom; break; case NO_INSTRUCTION_TYPE: - if (log != nullptr) - *log << "

Recognised NO_INSTRUCTION_TYPE instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised NO_INSTRUCTION_TYPE instruction. " + "The transformation function is identity." + << messaget::eom; break; case SKIP: - if (log != nullptr) - *log << "

Recognised SKIP instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised SKIP instruction. " + "The transformation function is identity." + << messaget::eom; break; case END_FUNCTION: - if (log != nullptr) - *log << "

Recognised END_FUNCTION instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised END_FUNCTION instruction. " + "The transformation function is identity." + << messaget::eom; break; case GOTO: - if (log != nullptr) - *log << "

Recognised GOTO instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised GOTO instruction. " + "The transformation function is identity." + << messaget::eom; break; case RETURN: - case OTHER: case DECL: case ASSUME: case ASSERT: case LOCATION: - case THROW: - case CATCH: case ATOMIC_BEGIN: case ATOMIC_END: + // These operations have no effect, neither propogating or removing taint + break; + case OTHER: + case THROW: + case CATCH: case START_THREAD: case END_THREAD: - if (log != nullptr) - *log << "

!!! WARNING !!! : Unsupported instruction reached. " - "So, we use identity as a transformation function.

\n"; - break; + msg.warning() << "!!! WARNING !!! : Unsupported instruction reached. " + "So, we use identity as a transformation function." << messaget::eom; break; default: throw std::runtime_error("ERROR: In 'pointsto_temp_transform' - " @@ -277,28 +274,25 @@ static pointsto_rulest pointsto_temp_transform( static void pointsto_temp_build_summary_from_computed_domain( - pointsto_temp_domain_ptrt const domain, - pointsto_rulest& output, - goto_functionst::function_mapt::const_iterator const fn_iter, - namespacet const& ns, - std::ostream* const log - ) + pointsto_temp_domain_ptrt const domain, + pointsto_rulest& output, + goto_functionst::function_mapt::const_iterator const fn_iter, + namespacet const& ns, + message_handlert& message_handler) { + messaget msg(message_handler); const pointsto_rulest& end_svalue = domain->at(std::prev(fn_iter->second.body.instructions.cend())); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Building points-to summary from the computed domain

\n" - << "

It is computed from the symbolic value " - "at location " + msg.debug() << "* Building points-to summary from the computed domain\n" + << "It is computed from the symbolic value at location " << std::prev(fn_iter->second.body.instructions.cend())->location_number - << ":

\n" - ; - pointsto_dump_rules_in_html(end_svalue,*log); + << ":\n"; + pointsto_dump_rules_in_html(end_svalue, msg.debug()); if (!end_svalue.empty()) - *log << "

Processing individual rules:

\n"; - *log << "\n"; + msg.debug() << messaget::eom; } void pointsto_temp_summarise_all_functions( - goto_modelt const& program, - database_of_summariest& summaries_to_compute, - call_grapht const& call_graph, - std::ostream* const log - ) + goto_modelt const& program, + database_of_summariest& summaries_to_compute, + call_grapht const& call_graph, + message_handlert& message_handler) { std::vector inverted_topological_order; { @@ -367,24 +359,22 @@ void pointsto_temp_summarise_all_functions( fn_name, program, summaries_to_compute, - log - ), + message_handler), }); } } pointsto_temp_summary_ptrt pointsto_temp_summarise_function( - irep_idt const& function_id, - goto_modelt const& instrumented_program, - database_of_summariest const& database, - std::ostream* const log - ) + irep_idt const& function_id, + goto_modelt const& instrumented_program, + database_of_summariest const& database, + message_handlert& message_handler) { - if (log != nullptr) - *log << "

Called sumfn::taint::taint_summarise_function( " - << to_html_text(as_string(function_id)) << " )

\n" - ; + messaget msg(message_handler); + msg.debug() << "** Called pointsto_temp_summarise_function( " + << to_html_text(as_string(function_id)) << " )" + << messaget::eom; goto_functionst::function_mapt const& functions = instrumented_program.goto_functions.function_map; @@ -403,8 +393,7 @@ pointsto_temp_summary_ptrt pointsto_temp_summarise_function( ns, database, *domain, - log - ); + message_handler); pointsto_rulest const input = domain->at(fn_iter->second.body.instructions.cbegin()); @@ -417,8 +406,8 @@ int iii = 0; ++iii; if (iii > 50) { - std::cout << "ERROR: The analysis was early terminated (after 50 steps). " - "The fixed point was not reached yet.\n"; + msg.error() << "ERROR: The analysis was early terminated (after 50 steps). " + "The fixed point was not reached yet." << messaget::eom; break; } @@ -439,22 +428,22 @@ int iii = 0; pointsto_rulest& dst_value = domain->at(dst_instr_it); pointsto_rulest const old_dst_value = dst_value; - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Processing transition: " - << src_instr_it->location_number << " ---[ " - ; + msg.debug() + << "* Processing transition: " + << src_instr_it->location_number << " [ "; dump_instruction_code_in_html( - *src_instr_it, - instrumented_program, - *log - ); - *log << " ]---> " << dst_instr_it->location_number << "

\n" - ; - *log << "

Source value:

\n"; - pointsto_dump_rules_in_html(src_value,*log); - *log << "

Old destination value:

\n"; - pointsto_dump_rules_in_html(old_dst_value,*log); + *src_instr_it, + instrumented_program, + msg.debug()); + msg.debug() + << " ] " << dst_instr_it->location_number << messaget::endl; + msg.debug() << "Source value:" << messaget::endl; + pointsto_dump_rules_in_html(src_value, msg.debug()); + msg.debug() << "\nOld destination value:\n"; + pointsto_dump_rules_in_html(old_dst_value, msg.debug()); + msg.debug() << messaget::eom; } pointsto_rulest const transformed = @@ -465,16 +454,16 @@ int iii = 0; functions, database, ns, - log - ); + message_handler); dst_value = pointsto_temp_join(transformed,old_dst_value); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Transformed value:

\n"; - pointsto_dump_rules_in_html(transformed,*log); - *log << "

Resulting destination value:

\n"; - pointsto_dump_rules_in_html(dst_value,*log); + msg.debug() << "Transformed value:\n"; + pointsto_dump_rules_in_html(transformed, msg.debug()); + msg.debug() << "\nResulting destination value:\n"; + pointsto_dump_rules_in_html(dst_value, msg.debug()); + msg.debug() << messaget::eom; } if ( !(pointsto_temp_equal(dst_value,old_dst_value) || @@ -482,10 +471,9 @@ int iii = 0; { work_set.insert(dst_instr_it); - if (log != nullptr) - *log << "

Inserting instruction at location " - << dst_instr_it->location_number << " into 'work_set'.

\n" - ; + msg.debug() << "Inserting instruction at location " + << dst_instr_it->location_number << " into 'work_set'." + << messaget::eom; } } } @@ -496,7 +484,6 @@ int iii = 0; output, fn_iter, ns, - log - ); + message_handler); return std::make_shared(input,output,domain); } diff --git a/src/goto-analyzer/pointsto_temp_analyser.h b/src/goto-analyzer/pointsto_temp_analyser.h index 694921684b09..90557a82c79c 100644 --- a/src/goto-analyzer/pointsto_temp_analyser.h +++ b/src/goto-analyzer/pointsto_temp_analyser.h @@ -54,16 +54,14 @@ void pointsto_temp_summarise_all_functions( goto_modelt const& program, database_of_summariest& summaries_to_compute, call_grapht const& call_graph, - std::ostream* const log = nullptr - ); + message_handlert& message_handler); pointsto_temp_summary_ptrt pointsto_temp_summarise_function( irep_idt const& function_id, goto_modelt const& program, database_of_summariest const& database, - std::ostream* const log = nullptr - ); + message_handlert& message_handler); #endif diff --git a/src/goto-analyzer/taint_fast_analyser.cpp b/src/goto-analyzer/taint_fast_analyser.cpp index 0c9b1a9a75e2..f749d8864c0d 100644 --- a/src/goto-analyzer/taint_fast_analyser.cpp +++ b/src/goto-analyzer/taint_fast_analyser.cpp @@ -13,9 +13,10 @@ static bool find_shortest_path( call_grapht const& inverted_call_graph, std::string const& source_function_name, std::string const& target_function_name, - std::vector< std::pair >& path - ) + std::vector< std::pair >& path, + message_handlert& message_handler) { + messaget msg(message_handler); std::size_t const start_len = path.size(); std::unordered_set visited; std::unordered_map > predecessors; @@ -62,7 +63,8 @@ static bool find_shortest_path( for (auto it = range.first; it != range.second; ++it) { std::string const other_fn_name = as_string(it->second); - std::cout << "other_fn_name [false]: " << other_fn_name << "\n"; + msg.debug() << "other_fn_name [false]: " << other_fn_name + << messaget::eom; if (visited.count(other_fn_name) == 0ULL) { predecessors[other_fn_name] = { fn_name, false }; @@ -96,40 +98,40 @@ static void taint_fast_analyser( std::string const& source_function_name, goto_programt::const_targett const source_instruction, std::string const& sink_function_name, - goto_programt::const_targett const sink_instruction - ) + goto_programt::const_targett const sink_instruction, + message_handlert& message_handler) { std::vector< std::pair > path; if (!find_shortest_path( - call_graph, - inverted_call_graph, - root_function_name, - source_function_name, - path - )) + call_graph, + inverted_call_graph, + root_function_name, + source_function_name, + path, + message_handler)) return; if (!path.empty()) path.pop_back(); if (!find_shortest_path( - call_graph, - inverted_call_graph, - source_function_name, - sink_function_name, - path - )) + call_graph, + inverted_call_graph, + source_function_name, + sink_function_name, + path, + message_handler)) return; refine_path_to_error_traces(goto_model,path,output_traces); } void taint_fast_analyser( - std::vector& output_traces, - goto_modelt const& goto_model, - call_grapht const& call_graph, - std::string const& root_function_name, - taint_sources_mapt const& taint_sources, - taint_sinks_mapt const& taint_sinks - ) + std::vector& output_traces, + goto_modelt const& goto_model, + call_grapht const& call_graph, + std::string const& root_function_name, + taint_sources_mapt const& taint_sources, + taint_sinks_mapt const& taint_sinks, + message_handlert& message_handler) { call_grapht inverted_call_graph; compute_inverted_call_graph(call_graph,inverted_call_graph); @@ -145,17 +147,17 @@ void taint_fast_analyser( for (auto const src_fn_locs : src_it->second) for (auto const src_loc : src_fn_locs.second) taint_fast_analyser( - output_traces, - goto_model, - call_graph, - inverted_call_graph, - root_function_name, - tid_locs.first, - src_fn_locs.first, - src_loc, - fn_locs.first, - loc - ); + output_traces, + goto_model, + call_graph, + inverted_call_graph, + root_function_name, + tid_locs.first, + src_fn_locs.first, + src_loc, + fn_locs.first, + loc, + message_handler); } taint_statisticst::instance().end_error_traces_recognition(); diff --git a/src/goto-analyzer/taint_fast_analyser.h b/src/goto-analyzer/taint_fast_analyser.h index f8947af09fac..8e87d1b50ce4 100644 --- a/src/goto-analyzer/taint_fast_analyser.h +++ b/src/goto-analyzer/taint_fast_analyser.h @@ -10,13 +10,13 @@ void taint_fast_analyser( - std::vector& output_traces, - goto_modelt const& goto_model, - call_grapht const& call_graph, - std::string const& root_function_name, - taint_sources_mapt const& taint_sources, - taint_sinks_mapt const& taint_sinks - ); + std::vector& output_traces, + goto_modelt const& goto_model, + call_grapht const& call_graph, + std::string const& root_function_name, + taint_sources_mapt const& taint_sources, + taint_sinks_mapt const& taint_sinks, + message_handlert& message_handler); #endif diff --git a/src/goto-analyzer/taint_planner.cpp b/src/goto-analyzer/taint_planner.cpp index ca1c941cdcf9..e2c48c682da3 100644 --- a/src/goto-analyzer/taint_planner.cpp +++ b/src/goto-analyzer/taint_planner.cpp @@ -465,9 +465,7 @@ std::string taint_plannert::get_unique_entry_point(jsont const& plan) std::string taint_plannert::solve_top_precision_level( goto_modelt& program, - call_grapht const& call_graph, - std::ostream* const log - ) + call_grapht const& call_graph) { const taint_precision_level_data_ptrt data = get_top_precision_level(); if (data->get_is_computed()) @@ -477,26 +475,20 @@ std::string taint_plannert::solve_top_precision_level( data->get_plan_for_summaries(), data->get_summary_database(), program, - call_graph, - log - ); + call_graph); if (!error_message.empty()) return error_message; error_message = run_taint_analysis( data->get_plan_for_analysis(), data->get_summary_database(), - program, - log - ); + program); if (!error_message.empty()) return error_message; error_message = build_next_precision_level( program, - call_graph, - log - ); + call_graph); if (!error_message.empty()) return error_message; @@ -509,9 +501,7 @@ std::string taint_plannert::compute_summaries( const taint_plan_for_summaries_ptrt plan_for_summaries, const database_of_summaries_ptrt summary_database, goto_modelt const& program, - call_grapht const& call_graph, - std::ostream* const log - ) + call_grapht const& call_graph) { std::vector inverted_topological_order; { @@ -549,9 +539,7 @@ std::string taint_plannert::compute_summaries( {}, taint_object_numbering, object_numbers_by_field, - get_message_handler(), - log - ), + get_message_handler()), }); } } @@ -561,9 +549,7 @@ std::string taint_plannert::compute_summaries( std::string taint_plannert::run_taint_analysis( const taint_plan_for_analysis_ptrt plan_for_analysis, const database_of_summaries_ptrt summary_database, - goto_modelt& program, - std::ostream* const log - ) + goto_modelt& program) { // Plan ignored here, as it is currently used to set the entry point // in goto_analyzer_parse_options.cpp. @@ -574,9 +560,7 @@ std::string taint_plannert::run_taint_analysis( std::string taint_plannert::build_next_precision_level( goto_modelt const& program, - call_grapht const& call_graph, - std::ostream* const log - ) + call_grapht const& call_graph) { // TODO: here goes a code preparing new plans for both analyses // (taint summary and taint analysis). diff --git a/src/goto-analyzer/taint_planner.h b/src/goto-analyzer/taint_planner.h index 3e6bfe945b2c..36e5233e5b1f 100644 --- a/src/goto-analyzer/taint_planner.h +++ b/src/goto-analyzer/taint_planner.h @@ -177,9 +177,7 @@ class taint_plannert : public messaget std::string solve_top_precision_level( goto_modelt& program, - call_grapht const& call_graph, - std::ostream* const log = nullptr - ); + call_grapht const& call_graph); static std::string get_unique_entry_point(jsont const& plan); @@ -189,22 +187,16 @@ class taint_plannert : public messaget const taint_plan_for_summaries_ptrt plan_for_summaries, const database_of_summaries_ptrt summary_database, goto_modelt const& program, - call_grapht const& call_graph, - std::ostream* const log - ); + call_grapht const& call_graph); std::string run_taint_analysis( const taint_plan_for_analysis_ptrt plan_for_analysis, const database_of_summaries_ptrt summary_database, - goto_modelt& program, - std::ostream* const log - ); + goto_modelt& program); std::string build_next_precision_level( goto_modelt const& program, - call_grapht const& call_graph, - std::ostream* const log - ); + call_grapht const& call_graph); precision_levelst computed_levels; taint_symbolst taint_symbols; diff --git a/src/goto-analyzer/taint_summary.cpp b/src/goto-analyzer/taint_summary.cpp index fb9b09979056..9f6c1e85136a 100644 --- a/src/goto-analyzer/taint_summary.cpp +++ b/src/goto-analyzer/taint_summary.cpp @@ -72,12 +72,13 @@ static void initialise_domain( taint_numbered_domaint& domain, written_expressionst& written, local_value_set_analysist* lvsa, - std::ostream* const log, + message_handlert& message_handler, object_numberingt& taint_object_numbering, object_numbers_by_fieldnamet& object_numbers_by_field, const std::map& inst_predecessors ) { + messaget msg(message_handler); // TODO: Improve this to only count as inputs those values which may be read // without a preceding write within the same function. taint_numbered_lvalues_sett environment; @@ -104,7 +105,7 @@ static void initialise_domain( } else if (it->type == ASSERT) { - collect_lvsa_access_paths(it->guard,ns,environment,*lvsa,it,taint_object_numbering); + collect_lvsa_access_paths(it->guard,ns,environment,*lvsa,it,taint_object_numbering); } else if (it->type == FUNCTION_CALL) { @@ -135,20 +136,20 @@ static void initialise_domain( collect_lvsa_access_paths(fn_call.arguments()[paramidx],ns,environment, *lvsa,it,taint_object_numbering); else { - //collect_access_paths(fn_call.arguments()[paramidx],ns,environment); - } + //collect_access_paths(fn_call.arguments()[paramidx],ns,environment); + } } else if (!is_parameter(lvalue_svalue.first,ns) && !is_return_value_auxiliary(lvalue_svalue.first,ns)) - { - environment.insert(taint_object_numbering.number(lvalue_svalue.first)); - } - if(lvalue_svalue.first.id()==ID_external_value_set) - { - const auto& evse=to_external_value_set(lvalue_svalue.first); - if(evse.access_path_size()==1) - object_numbers_by_field.insert({evse.access_path_back().label(),{}}); - } + { + environment.insert(taint_object_numbering.number(lvalue_svalue.first)); + } + if(lvalue_svalue.first.id()==ID_external_value_set) + { + const auto& evse=to_external_value_set(lvalue_svalue.first); + if(evse.access_path_size()==1) + object_numbers_by_field.insert({evse.access_path_back().label(),{}}); + } } for(auto const& lvalue_svalue : summary->output()) written.insert(taint_object_numbering.number(lvalue_svalue.first)); @@ -210,34 +211,30 @@ static void initialise_domain( { auto findit=object_numbers_by_field.find(fieldname); if(findit!=object_numbers_by_field.end()) - findit->second.insert(lvaluenum); + findit->second.insert(lvaluenum); } } - - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Initialising the domain

\n" - "

Domain value at the entry location:

\n" - ; + msg.debug() << "* Initialising the domain\n" + "Domain value at the entry location:\n"; taint_dump_numbered_lvalues_to_svalues_as_html( - domain.at(function.body.instructions.cbegin()), - ns, - taint_object_numbering, - {}/*TODO*/, - *log - ); + domain.at(function.body.instructions.cbegin()), + ns, + taint_object_numbering, + taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, + msg.debug()); - *log << "

Domain value at all other locations:

\n"; + msg.debug() << "\nDomain value at all other locations:\n"; taint_dump_numbered_lvalues_to_svalues_as_html( - domain.at(std::prev(function.body.instructions.cend())), - ns, - taint_object_numbering, - {}/*TODO*/, - *log - ); + domain.at(std::prev(function.body.instructions.cend())), + ns, + taint_object_numbering, + taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, + msg.debug()); + msg.debug() << messaget::eom; } - } @@ -365,14 +362,13 @@ static void build_symbols_substitution( namespacet const& ns, local_value_set_analysist* lvsa, instruction_iteratort const& Iit, - std::ostream* const log, + message_handlert& message_handler, object_numberingt& taint_object_numbering, const object_numbers_by_fieldnamet& object_numbers_by_field ) { - if (log != nullptr) - *log << "

Building 'symbols substitution map':

\n" - "
    \n"; + messaget msg(message_handler); + msg.debug() << "Building 'symbols substitution map':" << messaget::eom; auto parameter_indices=get_parameter_indices(fn_type); @@ -391,7 +387,7 @@ static void build_symbols_substitution( { std::size_t param_idx; { -//std::string const caller = as_string(caller_ident); + //std::string const caller = as_string(caller_ident); std::string const param_name = name_of_symbol_access_path(lvalue_svalue.first); auto const it = parameter_indices.find(param_name); @@ -405,16 +401,16 @@ static void build_symbols_substitution( if(lvsa) { collect_lvsa_access_paths( - fn_call.arguments().at(param_idx), - ns, - argument_lvalues, - *lvsa, - Iit, - taint_object_numbering); + fn_call.arguments().at(param_idx), + ns, + argument_lvalues, + *lvsa, + Iit, + taint_object_numbering); } else { - /* + /* collect_access_paths( fn_call.arguments().at(param_idx), ns, @@ -445,9 +441,6 @@ static void build_symbols_substitution( }); } - - if (log != nullptr) - *log << "
\n"; } @@ -473,11 +466,12 @@ static void build_substituted_summary( code_function_callt const& fn_call, code_typet const& fn_type, namespacet const& ns, - std::ostream* const log, + message_handlert& message_handler, object_numberingt& taint_object_numbering, const object_numbers_by_fieldnamet& object_numbers_by_fieldname ) { + messaget msg(message_handler); for (auto const& lvalue_svalue : original_summary) { const auto& lvalue=lvalue_svalue.first; @@ -510,12 +504,12 @@ static void build_substituted_summary( } } - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

Substituted summary:

\n"; - taint_dump_numbered_lvalues_to_svalues_as_html(substituted_summary,ns, - taint_object_numbering, - {}/*TODO*/,*log); + msg.debug() << "Substituted summary:\n"; + taint_dump_numbered_lvalues_to_svalues_as_html(substituted_summary, ns, + taint_object_numbering, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << messaget::eom; } } @@ -538,17 +532,15 @@ static void build_summary_from_computed_domain( taint_map_from_lvalues_to_svaluest& output, goto_functionst::function_mapt::const_iterator const fn_iter, namespacet const& ns, - std::ostream* const log, + message_handlert& message_handler, const object_numberingt& taint_object_numbering ) { - if (log != nullptr) - *log << "

Building summary from the computed domain

\n" - << "

It is computed from the symbolic value " - "at location " - << std::prev(fn_iter->second.body.instructions.cend())->location_number - << ":

\n
    \n" - ; + messaget msg(message_handler); + msg.debug() << "* Building summary from the computed domain\n" + << "It is computed from the symbolic value at location " + << std::prev(fn_iter->second.body.instructions.cend())->location_number + << ":\n"; auto const& end_svalue = domain.at(std::prev(fn_iter->second.body.instructions.cend())); @@ -559,28 +551,27 @@ static void build_summary_from_computed_domain( { output.insert(std::make_pair(lval,it->second)); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "
  • "; - taint_dump_lvalue_in_html(lval,ns,*log); - *log << " → "; - taint_dump_svalue_in_html(it->second,{}/*TODO*/,*log); - *log << "
    • \n"; + msg.debug() << "o "; + taint_dump_lvalue_in_html(lval, ns, msg.debug()); + msg.debug() << " → "; + taint_dump_svalue_in_html(it->second, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << "\n"; } } else - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "
  • !! EXCLUDING !! : "; - taint_dump_lvalue_in_html(lval,ns,*log); - *log << " → "; - taint_dump_svalue_in_html(it->second,{}/*TODO*/,*log); - *log << "
    • \n"; + msg.debug() << "o !! EXCLUDING !! : "; + taint_dump_lvalue_in_html(lval, ns, msg.debug()); + msg.debug() << " → "; + taint_dump_svalue_in_html(it->second, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << "\n"; } } - if (log != nullptr) - *log << "
\n"; + msg.debug() << messaget::eom; } @@ -910,7 +901,7 @@ static void collect_lvsa_access_paths( { if(target.id()==ID_unknown) { - //std::cerr << "Warning: ignoring unknown value-set entry for now.\n"; + //msg.warning() << "Warning: ignoring unknown value-set entry for now.\n"; continue; } @@ -977,10 +968,10 @@ static void handle_assignment( instruction_iteratort const& Iit, local_value_set_analysist* lvsa, namespacet const& ns, - std::ostream* const log, + message_handlert& message_handler, object_numberingt& taint_object_numbering) { - + messaget msg(message_handler); const auto& lhs_type=ns.follow(asgn.lhs().type()); if(lhs_type.id()==ID_struct) { @@ -990,17 +981,18 @@ static void handle_assignment( { code_assignt member_assign(member_exprt(asgn.lhs(),c.get_name(),c.type()), member_exprt(asgn.rhs(),c.get_name(),c.type())); - handle_assignment(member_assign,a,result,Iit,lvsa,ns,log,taint_object_numbering); + handle_assignment(member_assign, a, result, Iit, lvsa, ns, message_handler, + taint_object_numbering); } return; } - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

\nRecognised ASSIGN instruction. Left-hand-side " - "l-value is { "; - taint_dump_lvalue_in_html(normalise(asgn.lhs(),ns),ns,*log); - *log << " }. Right-hand-side l-values are { "; + msg.debug() << "Recognised ASSIGN instruction. Left-hand-side " + "l-value is { "; + taint_dump_lvalue_in_html(normalise(asgn.lhs(), ns), ns, msg.debug()); + msg.debug() << " }. Right-hand-side l-values are { "; } taint_svaluet rvalue = taint_make_bottom(); @@ -1018,16 +1010,15 @@ static void handle_assignment( if (it != a.cend()) rvalue.add_all(it->second); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - taint_dump_lvalue_in_html(taint_object_numbering[lvalue],ns,*log); - *log << ", "; + taint_dump_lvalue_in_html(taint_object_numbering[lvalue], ns, msg.debug()); + msg.debug() << ", "; } } } - if (log != nullptr) - *log << "}.

\n"; + msg.debug() << "}." << messaget::eom; if(!lvsa) { @@ -1058,10 +1049,10 @@ taint_numbered_lvalue_svalue_mapt transform( object_numberingt& taint_object_numbering, const object_numbers_by_fieldnamet& object_numbers_by_field, taint_specification_symbol_names_to_svalue_symbols_mapt const& - taint_spec_names, - std::ostream* const log - ) + taint_spec_names, + message_handlert& message_handler) { + messaget msg(message_handler); goto_programt::instructiont const& I=*Iit; taint_numbered_lvalue_svalue_mapt result; // Take a cheap read-only view of the incoming domain: @@ -1096,7 +1087,7 @@ taint_numbered_lvalue_svalue_mapt transform( return result; } } - handle_assignment(asgn,a,result,Iit,lvsa,ns,log,taint_object_numbering); + handle_assignment(asgn, a, result, Iit, lvsa, ns, message_handler, taint_object_numbering); } break; case FUNCTION_CALL: @@ -1104,8 +1095,7 @@ taint_numbered_lvalue_svalue_mapt transform( code_function_callt const& fn_call = to_code_function_call(I.code); if (fn_call.function().id() == ID_symbol) { - if (log != nullptr) - *log << "

Recognised FUNCTION_CALL instruction.

\n"; + msg.debug() << "Recognised FUNCTION_CALL instruction." << messaget::eom; std::string const callee_ident = as_string(to_symbol_expr(fn_call.function()).get_identifier()); @@ -1134,7 +1124,7 @@ taint_numbered_lvalue_svalue_mapt transform( ns, lvsa, Iit, - log, + message_handler, taint_object_numbering, object_numbers_by_field ); @@ -1147,7 +1137,7 @@ taint_numbered_lvalue_svalue_mapt transform( fn_call, fn_type, ns, - log, + message_handler, taint_object_numbering, object_numbers_by_field ); @@ -1155,17 +1145,17 @@ taint_numbered_lvalue_svalue_mapt transform( result = assign(result,substituted_summary); } else - if (log != nullptr) - *log << "

!!! WARNING !!! : No summary was found for the called " - "function " << as_string(callee_ident) << "So, we use " - "identity as a transformation function.

\n"; + msg.warning() + << "!!! WARNING !!! : No summary was found for the called function " + << as_string(callee_ident) + << "So, we use identity as a transformation function." << messaget::eom; } else - if (log != nullptr) - *log << "

!!! WARNING !!! : Recognised FUNCTION_CALL instruction " - "using non-identifier call expression. Such call is not " - "supported. So, we use identity as a transformation " - "function.

\n"; + msg.warning() + << "!!! WARNING !!! : Recognised FUNCTION_CALL instruction " + "using non-identifier call expression. Such call is not " + "supported. So, we use identity as a transformation " + "function." << messaget::eom; } break; case OTHER: @@ -1246,20 +1236,20 @@ taint_numbered_lvalue_svalue_mapt transform( code_assignt fake_assignment; fake_assignment.lhs()=dereference_exprt(I.code.op0(),I.code.op0().type().subtype()); fake_assignment.rhs()=constant_exprt("0",I.code.op0().type().subtype()); - handle_assignment(fake_assignment,a,result,Iit,lvsa,ns,log,taint_object_numbering); + handle_assignment(fake_assignment, a, result, Iit, lvsa, ns, message_handler, + taint_object_numbering); } else - if (log != nullptr) - *log << "

!!! WARNING !!! : Recognised OTHER instruction type, which " - "is neither 'set_may' nor 'clear_may' function call. The " - "transformation function is thus identity.

\n"; + msg.warning() + << "!!! WARNING !!! : Recognised OTHER instruction type, which " + "is neither 'set_may' nor 'clear_may' function call. The " + "transformation function is thus identity." << messaget::eom; break; case DEAD: { code_deadt const& dead = to_code_dead(I.code); - if (log != nullptr) - *log << "

\nRecognised DEAD instruction. Removing these l-values { "; + msg.debug() << "Recognised DEAD instruction. Removing these l-values { "; taint_lvalues_sett lvalues; collect_access_paths(dead.symbol(),ns,lvalues); @@ -1267,52 +1257,47 @@ taint_numbered_lvalue_svalue_mapt transform( { erase_dead_lvalue(lvalue,ns,result,taint_object_numbering); - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { - taint_dump_lvalue_in_html(lvalue,ns,*log); - *log << ", "; + taint_dump_lvalue_in_html(lvalue,ns,msg.debug()); + msg.debug() << ", "; } } - if (log != nullptr) - *log << "}.

\n"; + msg.debug() << "}." << messaget::eom; } break; case NO_INSTRUCTION_TYPE: - if (log != nullptr) - *log << "

Recognised NO_INSTRUCTION_TYPE instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised NO_INSTRUCTION_TYPE instruction. " + "The transformation function is identity." << messaget::eom; break; case SKIP: - if (log != nullptr) - *log << "

Recognised SKIP instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised SKIP instruction. " + "The transformation function is identity." << messaget::eom; break; case END_FUNCTION: - if (log != nullptr) - *log << "

Recognised END_FUNCTION instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised END_FUNCTION instruction. " + "The transformation function is identity." << messaget::eom; break; case GOTO: - if (log != nullptr) - *log << "

Recognised GOTO instruction. " - "The transformation function is identity.

\n"; + msg.debug() << "Recognised GOTO instruction. " + "The transformation function is identity." << messaget::eom; break; case RETURN: case DECL: case ASSUME: case ASSERT: case LOCATION: - case THROW: - case CATCH: case ATOMIC_BEGIN: case ATOMIC_END: + // These operations have no effect, neither propogating or removing taint + break; + case THROW: + case CATCH: case START_THREAD: case END_THREAD: - if (log != nullptr) - *log << "

!!! WARNING !!! : Unsupported instruction reached. " - "So, we use identity as a transformation function.

\n"; - break; + msg.warning() << "!!! WARNING !!! : Unsupported instruction reached. " + "So, we use identity as a transformation function." << messaget::eom; break; default: throw std::runtime_error("ERROR: In 'sumfn::taint::transform' - " @@ -1426,28 +1411,25 @@ static void populate_formals_to_actuals( } } -void taint_summarise_all_functions( - goto_modelt const& instrumented_program, - database_of_summariest& summaries_to_compute, - call_grapht const& call_graph, - local_value_set_analysist::dbt* lvsa_database, - taint_specification_symbol_names_to_svalue_symbols_mapt const& - taint_spec_names, - taint_object_numbering_per_functiont& taint_object_numbering, - object_numbers_by_field_per_functiont& object_numbers_by_field, - formals_to_actuals_mapt& formals_to_actuals, - message_handlert& msg, - double timeout, - std::ostream* const log - ) +void taint_summarise_all_functions( + goto_modelt const& instrumented_program, + database_of_summariest& summaries_to_compute, + call_grapht const& call_graph, + local_value_set_analysist::dbt* lvsa_database, + taint_specification_symbol_names_to_svalue_symbols_mapt const& + taint_spec_names, + taint_object_numbering_per_functiont& taint_object_numbering, + object_numbers_by_field_per_functiont& object_numbers_by_field, + formals_to_actuals_mapt& formals_to_actuals, + message_handlert& message_handler, + double timeout) { + messaget msg(message_handler); std::vector inverted_topological_order; get_inverted_topological_order(call_graph, instrumented_program.goto_functions, inverted_topological_order); - messaget msgout; - msgout.set_message_handler(msg); size_t processed = 0UL; size_t modelled = 0UL; size_t skipped = 0UL; @@ -1459,7 +1441,7 @@ void taint_summarise_all_functions( auto duration = std::chrono::duration(end_time-start_time).count(); if (duration >= timeout) { - msgout.progress() + msg.progress() << "[" << std::fixed << std::setprecision(1) << std::setw(5) << (inverted_topological_order.size() == 0UL ? 100.0 : @@ -1480,7 +1462,7 @@ void taint_summarise_all_functions( auto const fn_it = functions_map.find(fn_name); if (taint_summary_libmodelst::instance().has_model_of_function(fn_name)) { - msgout.progress() + msg.progress() << "[" << std::fixed << std::setprecision(1) << std::setw(5) << (inverted_topological_order.size() == 0UL ? 100.0 : @@ -1498,7 +1480,7 @@ void taint_summarise_all_functions( else if (fn_it != functions_map.cend() && fn_it->second.body_available() && fn_name != "_start") { - msgout.progress() + msg.progress() << "[" << std::fixed << std::setprecision(1) << std::setw(5) << (inverted_topological_order.size() == 0UL ? 100.0 : @@ -1511,24 +1493,22 @@ void taint_summarise_all_functions( summaries_to_compute.insert({ as_string(fn_name), taint_summarise_function( - fn_name, - instrumented_program, - summaries_to_compute, - lvsa_database, - taint_spec_names, - taint_object_numbering[as_string(fn_name)], - object_numbers_by_field[as_string(fn_name)], - formals_to_actuals, - msg, - log - ), + fn_name, + instrumented_program, + summaries_to_compute, + lvsa_database, + taint_spec_names, + taint_object_numbering[as_string(fn_name)], + object_numbers_by_field[as_string(fn_name)], + formals_to_actuals, + message_handler), }); ++processed; } else { - msgout.progress() + msg.progress() << "[" << std::fixed << std::setprecision(1) << std::setw(5) << (inverted_topological_order.size() == 0UL ? 100.0 : @@ -1543,7 +1523,7 @@ void taint_summarise_all_functions( ++skipped; } } - msgout.progress() + msg.progress() << "[100.0%] Taint analysis has finished successfully (" << processed << " processed, " << modelled << " modelled, " @@ -1552,25 +1532,22 @@ void taint_summarise_all_functions( } taint_summary_ptrt taint_summarise_function( - irep_idt const& function_id, - goto_modelt const& instrumented_program, - database_of_summariest const& database, - local_value_set_analysist::dbt* lvsa_database, - taint_specification_symbol_names_to_svalue_symbols_mapt const& - taint_spec_names, - object_numberingt& taint_object_numbering, - object_numbers_by_fieldnamet& object_numbers_by_field, - formals_to_actuals_mapt& formals_to_actuals, - message_handlert& msg, - std::ostream* const log - ) + irep_idt const& function_id, + goto_modelt const& instrumented_program, + database_of_summariest const& database, + local_value_set_analysist::dbt* lvsa_database, + taint_specification_symbol_names_to_svalue_symbols_mapt const& + taint_spec_names, + object_numberingt& taint_object_numbering, + object_numbers_by_fieldnamet& object_numbers_by_field, + formals_to_actuals_mapt& formals_to_actuals, + message_handlert& message_handler) { + messaget msg(message_handler); + msg.debug() << "** Called taint_summarise_function( " + << to_html_text(as_string(function_id)) << " )" + << messaget::eom; - if (log != nullptr) - *log << "

Called sumfn::taint::taint_summarise_function( " - << to_html_text(as_string(function_id)) << " )

\n" - ; - goto_functionst::function_mapt const& functions = instrumented_program.goto_functions.function_map; auto const fn_iter = functions.find(function_id); @@ -1585,13 +1562,16 @@ taint_summary_ptrt taint_summarise_function( ); local_value_set_analysist::dbt emptydb(""); - auto& use_database=lvsa_database ? *lvsa_database : emptydb; - local_value_set_analysist lvsainst(ns,fn_iter->second.type,id2string(function_id), - use_database,LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET); - local_value_set_analysist* lvsa=lvsa_database ? &lvsainst : nullptr; - if(lvsa) + local_value_set_analysist::dbt& use_database = + lvsa_database != nullptr ? *lvsa_database : emptydb; + local_value_set_analysist lvsainst(ns,fn_iter->second.type, + id2string(function_id), use_database, + LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET); + local_value_set_analysist* lvsa = nullptr; + if (lvsa_database != nullptr) { - lvsainst.set_message_handler(msg); + lvsa = &lvsainst; + lvsainst.set_message_handler(message_handler); lvsainst(fn_iter->second.body); // Retain this summary for use analysing callers. @@ -1629,19 +1609,18 @@ taint_summary_ptrt taint_summarise_function( } initialise_domain( - function_id, - fn_iter->second, - functions, - ns, - database, - domain, - written_lvalues, - lvsa, - log, - taint_object_numbering, - object_numbers_by_field, - inst_predecessors - ); + function_id, + fn_iter->second, + functions, + ns, + database, + domain, + written_lvalues, + lvsa, + message_handler, + taint_object_numbering, + object_numbers_by_field, + inst_predecessors); auto input = domain.at(fn_iter->second.body.instructions.cbegin()); @@ -1659,24 +1638,24 @@ taint_summary_ptrt taint_summarise_function( auto const transformed = transform( - src_value, - src_instr_it, - function_id, - functions, - database, - lvsa, - ns, - taint_object_numbering, - object_numbers_by_field, - taint_spec_names, - log - ); + src_value, + src_instr_it, + function_id, + functions, + database, + lvsa, + ns, + taint_object_numbering, + object_numbers_by_field, + taint_spec_names, + message_handler); goto_programt::const_targetst successors; fn_iter->second.body.get_successors(src_instr_it, successors); for(auto succ_it = successors.begin(); succ_it != successors.end(); ++succ_it) + { if (*succ_it != fn_iter->second.body.instructions.cend()) { instruction_iteratort const dst_instr_it = *succ_it; @@ -1685,25 +1664,24 @@ taint_summary_ptrt taint_summarise_function( auto const old_dst_value = dst_value; - if (log != nullptr) - { - *log << "

Processing transition: " - << src_instr_it->location_number << " ---[ " - ; + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { + msg.debug() << "* Processing transition: " + << src_instr_it->location_number << " [ "; dump_instruction_code_in_html( *src_instr_it, instrumented_program, - *log - ); - *log << " ]---> " << dst_instr_it->location_number << "

\n" - ; - *log << "

Source value:

\n"; + msg.debug()); + msg.debug() << " ] " << dst_instr_it->location_number + << messaget::endl; + msg.debug() << "Source value:\n"; taint_dump_numbered_lvalues_to_svalues_as_html( - src_value,ns,taint_object_numbering,{}/*TODO*/,*log); - *log << "

Old destination value:

\n"; - taint_dump_numbered_lvalues_to_svalues_as_html( - old_dst_value,ns,taint_object_numbering,{}/*TODO*/,*log); - } + src_value, ns, taint_object_numbering, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << "\nOld destination value:\n"; + taint_dump_numbered_lvalues_to_svalues_as_html( + old_dst_value, ns, taint_object_numbering, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << messaget::eom; + } // First instruction is a loop head in this case, // since callers are also predecessors. @@ -1722,41 +1700,41 @@ taint_summary_ptrt taint_summarise_function( dst_value=join(transformed,old_dst_value); } - if (log != nullptr) - { - *log << "

Transformed value:

\n"; + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { + msg.debug() << "Transformed value:\n"; taint_dump_numbered_lvalues_to_svalues_as_html( - transformed,ns,taint_object_numbering,{}/*TODO*/,*log); - *log << "

Resulting destination value:

\n"; + transformed, ns, taint_object_numbering, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << "\nResulting destination value:\n"; taint_dump_numbered_lvalues_to_svalues_as_html( - dst_value,ns,taint_object_numbering,{}/*TODO*/,*log); - } + dst_value, ns, taint_object_numbering, taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, msg.debug()); + msg.debug() << messaget::eom; + } if (dst_has_unique_predecessor || !taint_map_subset(dst_value,old_dst_value)) { work_set.insert(dst_instr_it); - if (log != nullptr) - *log << "

Inserting instruction at location " - << dst_instr_it->location_number << " into 'work_set'.

\n" - ; + msg.debug() << "Inserting instruction at location " + << dst_instr_it->location_number << " into 'work_set'." + << messaget::eom; } } + } } taint_map_from_lvalues_to_svaluest& output=result.output(); build_summary_from_computed_domain( - domain, - written_lvalues, - output, - fn_iter, - ns, - log, - taint_object_numbering - ); + domain, + written_lvalues, + output, + fn_iter, + ns, + message_handler, + taint_object_numbering); taint_statisticst::instance().end_taint_analysis_of_function( - input,output,domain + input,output,domain ); auto& expr_input=result.input(); @@ -1764,7 +1742,7 @@ taint_summary_ptrt taint_summarise_function( expr_input.insert({taint_object_numbering[p.first],p.second}); result.domain_numbering()=taint_object_numbering; - + return resultp; } diff --git a/src/goto-analyzer/taint_summary.h b/src/goto-analyzer/taint_summary.h index 328f25d63154..c4ec56b570a2 100644 --- a/src/goto-analyzer/taint_summary.h +++ b/src/goto-analyzer/taint_summary.h @@ -382,10 +382,8 @@ void taint_summarise_all_functions( taint_object_numbering_per_functiont& taint_object_numbering, object_numbers_by_field_per_functiont& object_numbers_by_field, formals_to_actuals_mapt&, - message_handlert& msg, - double timeout = 60.0, - std::ostream* const log = nullptr - ); + message_handlert& message_handler, + double timeout = 60.0); /*******************************************************************\ @@ -410,9 +408,7 @@ taint_summary_ptrt taint_summarise_function( object_numberingt& taint_object_numbering, object_numbers_by_fieldnamet& object_numbers_by_field, formals_to_actuals_mapt&, - message_handlert& msg, - std::ostream* const log = nullptr - ); + message_handlert& message_handler); typedef std::set taint_numbered_lvalues_sett; diff --git a/src/goto-analyzer/taint_trace_recogniser.cpp b/src/goto-analyzer/taint_trace_recogniser.cpp index 31285b4ffc3b..f9acd8d18d2f 100644 --- a/src/goto-analyzer/taint_trace_recogniser.cpp +++ b/src/goto-analyzer/taint_trace_recogniser.cpp @@ -18,7 +18,7 @@ data stored in the databese of taint summaries. #include #include #include -#include +#include #include #include #include @@ -28,60 +28,52 @@ data stored in the databese of taint summaries. static const namespacet* global_ns; -static void dump_trace(taint_tracet const& trace, - std::string const& purpose, - namespacet const& ns, - std::stringstream* const log - ) +static void dump_trace(taint_tracet const& trace, std::string const& purpose, + namespacet const& ns, std::ostream& ostr) { - assert(log != nullptr); - *log << "

" << purpose << ":

\n" - "" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - ; - for (taint_trace_elementt const& element : trace) + ostr << + "

" << purpose << ":

\n" + "
FunctionLocationVariablesSymbolsMessageLineFileComment
" + " \n" + " \n" + " \n" + " \n" + " \n" + " \n" + " \n" + " \n" + " \n" + " \n"; + for (taint_trace_elementt const& element : trace) { - *log << " \n" - " \n" - " \n" - ; - *log << " \n" + << " \n" + << " \n"; + ostr << " \n" - " \n" + " \n" - " \n" - " \n" - " \n" - " \n" - " \n"; + ostr); + ostr + << " \n" + << " \n" + << " \n" + << " \n" + << " \n" + << " \n" + << "
FunctionLocationVariablesSymbolsMessageLineFileComment
" - << to_html_text(element.get_name_of_function()) << "" - << element.get_instruction_iterator()->location_number - << "\n"; + ostr + << "
" + << to_html_text(element.get_name_of_function()) << "" + << element.get_instruction_iterator()->location_number << "\n"; taint_dump_lvalues_to_svalues_in_html( element.get_map_from_lvalues_to_svalues(), ns, - {}/*TODO*/, - *log - ); - *log << " \n"; + taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, + ostr); + ostr << + " \n"; taint_dump_svalue_in_html( {element.get_symbols(),false,false}, {}, // TODO: here should be propagated and used instance of: // taint_svalue_symbols_to_specification_symbols_mapt - *log - ); - *log << " " << to_html_text(element.get_message()) - << "" << element.get_line() - << "" << to_html_text(element.get_file()) - << "" << to_html_text(element.get_code_annotation()) - << "
" << to_html_text(element.get_message()) << "" << element.get_line() << "" << to_html_text(element.get_file()) << "" << to_html_text(element.get_code_annotation()) << "
\n"; } } @@ -343,9 +335,7 @@ static void taint_collect_successors_inside_function( taint_svaluet::taint_symbolt const& taint_name, std::string const& sink_function_name, goto_programt::const_targett const sink_instruction, - std::vector& successors, - std::stringstream* const log - ) + std::vector& successors) { goto_functionst::goto_functiont const& fn = goto_model.goto_functions.function_map.at( @@ -536,22 +526,20 @@ static void populate_local_distances_to_taint_sink( void taint_recognise_error_traces( - std::vector& output_traces, - goto_modelt const& goto_model, - call_grapht const& call_graph, - database_of_summariest const& summaries, - taint_sources_mapt const& taint_sources, - taint_sinks_mapt const& taint_sinks, - taint_object_numbering_per_functiont& taint_object_numbering, - object_numbers_by_field_per_functiont& object_numbers_by_field, - const formals_to_actuals_mapt& formals_to_actuals, - bool stop_after_one_trace, - message_handlert& msghandler, - std::stringstream* const log - ) + std::vector& output_traces, + goto_modelt const& goto_model, + call_grapht const& call_graph, + database_of_summariest const& summaries, + taint_sources_mapt const& taint_sources, + taint_sinks_mapt const& taint_sinks, + taint_object_numbering_per_functiont& taint_object_numbering, + object_numbers_by_field_per_functiont& object_numbers_by_field, + const formals_to_actuals_mapt& formals_to_actuals, + bool stop_after_one_trace, + message_handlert& message_handler) { - if (log != nullptr) - *log << "

Building taint error traces

\n"; + messaget msg(message_handler); + msg.debug() << "** Building taint error traces" << messaget::eom; taint_statisticst::instance().begin_error_traces_recognition(); @@ -564,22 +552,20 @@ void taint_recognise_error_traces( for (auto const src_fn_locs : src_it->second) for (auto const src_loc : src_fn_locs.second) taint_recognise_error_traces( - output_traces, - goto_model, - call_graph, - summaries, - tid_locs.first, - src_fn_locs.first, - src_loc, - fn_locs.first, - loc, - taint_object_numbering, - object_numbers_by_field, - formals_to_actuals, - stop_after_one_trace, - msghandler, - log - ); + output_traces, + goto_model, + call_graph, + summaries, + tid_locs.first, + src_fn_locs.first, + src_loc, + fn_locs.first, + loc, + taint_object_numbering, + object_numbers_by_field, + formals_to_actuals, + stop_after_one_trace, + message_handler); } taint_statisticst::instance().end_error_traces_recognition(); @@ -587,45 +573,30 @@ void taint_recognise_error_traces( void taint_recognise_error_traces( - std::vector& output_traces, - goto_modelt const& goto_model, - call_grapht const& call_graph, - database_of_summariest const& summaries, - taint_svaluet::taint_symbolt const& taint_name, - std::string const& source_function_name, - goto_programt::const_targett const source_instruction, - std::string const& sink_function_name, - goto_programt::const_targett const sink_instruction, - taint_object_numbering_per_functiont& taint_object_numbering, - object_numbers_by_field_per_functiont& object_numbers_by_field, - const formals_to_actuals_mapt& formals_to_actuals, - bool stop_after_one_trace, - message_handlert& msghandler, - std::stringstream* const log - ) + std::vector& output_traces, + goto_modelt const& goto_model, + call_grapht const& call_graph, + database_of_summariest const& summaries, + taint_svaluet::taint_symbolt const& taint_name, + std::string const& source_function_name, + goto_programt::const_targett const source_instruction, + std::string const& sink_function_name, + goto_programt::const_targett const sink_instruction, + taint_object_numbering_per_functiont& taint_object_numbering, + object_numbers_by_field_per_functiont& object_numbers_by_field, + const formals_to_actuals_mapt& formals_to_actuals, + bool stop_after_one_trace, + message_handlert& message_handler) { - messaget msg(msghandler); - if (log != nullptr) - *log << "

Building an error trace from source to sink

\n" - "

We will recognise all tained paths from this pair of source " - "and sink:

\n" - "\n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - " \n" - "
Source functionSource locationTaint symbolSink functionSink location
" << to_html_text(source_function_name) << "" << source_instruction->location_number << "" << to_html_text(i2string(taint_name)) << "" << to_html_text(sink_function_name) << "" << sink_instruction->location_number << "
\n" - ; + messaget msg(message_handler); + msg.debug() << "* Building an error trace from source to sink\n" + "We will recognise all tained paths from this pair of source " + "and sink:\n" + " Source function: " << to_html_text(source_function_name) << "\n" + " Source location: " << source_instruction->location_number << "\n" + " Taint symbol: " << to_html_text(i2string(taint_name)) << "\n" + " Sink function: " << to_html_text(sink_function_name) << "\n" + " Sink location: " << sink_instruction->location_number << messaget::eom; call_grapht inverted_call_graph; compute_inverted_call_graph(call_graph,inverted_call_graph); @@ -675,10 +646,8 @@ void taint_recognise_error_traces( } if (may_path_exist == false) { - if (log != nullptr) - *log << "

The sink function is call-graph unreachable from the " - "source function. So, terminating immediatelly.

\n" - ; + msg.debug() << "The sink function is call-graph unreachable from the " + "source function. So, terminating immediatelly." << messaget::eom; return; } } @@ -724,7 +693,7 @@ void taint_recognise_error_traces( taint_trace_elementt const& elem = trace.back(); const auto& local_numbering=taint_object_numbering.at(elem.get_name_of_function()); - if(msghandler.get_verbosity()>=message_clientt::M_DEBUG) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) msg.debug() << trace.get_trace().size() << " " << elem.get_name_of_function() << " " << from_expr(ns,"",elem.get_instruction_iterator()->code) << messaget::eom; if (elem.get_name_of_function() == sink_function_name && @@ -781,9 +750,9 @@ void taint_recognise_error_traces( output_traces.push_back(trace.get_trace()); msg.debug() << "BACKTRACK: successful trace (looking for alternatives)" << messaget::eom; - if (log != nullptr) + if (message_handler.get_verbosity()>=messaget::M_DEBUG) { - *log << "

There is added the following trace into the output:

\n" + msg.debug() << "There is added the following trace into the output:\n" "" " \n" " \n" @@ -798,29 +767,28 @@ void taint_recognise_error_traces( ; for (taint_trace_elementt const& element : output_traces.back()) { - *log << " \n" + msg.debug() << " \n" " \n" " \n" ; - *log << " \n" + taint_svalue_symbols_to_specification_symbols_mapt() /*TODO*/, + msg.debug()); + msg.debug() << " \n" " \n" + msg.debug() << " \n" " \n" " \n" " \n"; } - *log << "
Function
" << to_html_text(element.get_name_of_function()) << "" << element.get_instruction_iterator()->location_number << "\n"; + msg.debug() << " \n"; taint_dump_lvalues_to_svalues_in_html( element.get_map_from_lvalues_to_svalues(), ns, - {}/*TODO*/, - *log - ); - *log << " \n"; taint_dump_svalue_in_html( {element.get_symbols(),false,false}, {}, // TODO: here should be propagated and used instance of: // taint_svalue_symbols_to_specification_symbols_mapt - *log + msg.debug() ); - *log << " " << to_html_text(element.get_message()) << "" << element.get_line() @@ -831,7 +799,7 @@ void taint_recognise_error_traces( << "
"; + msg.debug() << "" << messaget::eom; } if(stop_after_one_trace) @@ -841,17 +809,17 @@ void taint_recognise_error_traces( } else { - if (log != nullptr) + if (message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: sink without appropriate taint" << messaget::eom; bt_trace.backtrack(); - if (log != nullptr) - *log << "

No trace is generates as the taint symbol '" - << taint_name << "' did not reach the sink.

\n"; + msg.debug() << "No trace is generates as the taint symbol '" + << taint_name << "' did not reach the sink." << messaget::eom; } } else if (elem.get_instruction_iterator()->type == FUNCTION_CALL) @@ -909,7 +877,7 @@ void taint_recognise_error_traces( for(const auto number : actuals_list[param_indices[paramsym]]) { - if(msghandler.get_verbosity()>=message_clientt::M_DEBUG) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) msg.debug() << "Actual parameter for " << from_expr(ns,"",callee_lvalue_svalue.first) << ": " << from_expr(ns,"",local_numbering[number]) << messaget::eom; @@ -1005,16 +973,15 @@ void taint_recognise_error_traces( taint_name, sink_function_name, sink_instruction, - successors, - log - ); + successors); if (successors.empty()) { - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: uninteresting call, no successors" << messaget::eom; bt_trace.backtrack(); } @@ -1083,22 +1050,21 @@ void taint_recognise_error_traces( std::vector successors; taint_collect_successors_inside_function( goto_model, - trace, - elem, - summaries, - taint_name, - sink_function_name, - sink_instruction, - successors, - log - ); + trace, + elem, + summaries, + taint_name, + sink_function_name, + sink_instruction, + successors); if (successors.empty()) { - if (log != nullptr) - dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { + dump_trace(trace.get_trace(), "Skipping the following explored path", + ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: interesting call, no successors" << messaget::eom; bt_trace.backtrack(); } @@ -1115,23 +1081,22 @@ void taint_recognise_error_traces( // TODO: Now we step over the call site without entering callees! std::vector successors; taint_collect_successors_inside_function( - goto_model, - trace, - elem, - summaries, - taint_name, - sink_function_name, - sink_instruction, - successors, - log - ); + goto_model, + trace, + elem, + summaries, + taint_name, + sink_function_name, + sink_instruction, + successors); if (successors.empty()) { - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: call without summary, no successors" << messaget::eom; bt_trace.backtrack(); } @@ -1151,23 +1116,22 @@ void taint_recognise_error_traces( std::vector successors; taint_collect_successors_inside_function( - goto_model, - trace, - trace.at(call_index), - summaries, - taint_name, - sink_function_name, - sink_instruction, - successors, - log - ); + goto_model, + trace, + trace.at(call_index), + summaries, + taint_name, + sink_function_name, + sink_instruction, + successors); if (successors.empty()) { - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: function end (have stack) with no successors" << messaget::eom; bt_trace.backtrack(); } @@ -1274,36 +1238,33 @@ void taint_recognise_error_traces( std::vector successors; taint_collect_successors_inside_function( - goto_model, - trace, - taint_trace_elementt( - func_loc.first, - func_loc.second, - explicit_domain, - taint_svaluet::expressiont( - stack_symbols.cbegin(), - stack_symbols.cend() - ), - "" - ), - summaries, - taint_name, - sink_function_name, - sink_instruction, - successors, - log - ); + goto_model, + trace, + taint_trace_elementt( + func_loc.first, + func_loc.second, + explicit_domain, + taint_svaluet::expressiont( + stack_symbols.cbegin(), + stack_symbols.cend()), + ""), + summaries, + taint_name, + sink_function_name, + sink_instruction, + successors); for (taint_trace_elementt const& succ_elem : successors) { bt_trace.add_pending_backtrack(succ_elem,false); } } - if ((!bt_trace.can_backtrack()) && log != nullptr) + if ((!bt_trace.can_backtrack()) && message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } if(!bt_trace.can_backtrack()) msg.debug() << "BACKTRACK: function end, no callers" << messaget::eom; @@ -1314,23 +1275,22 @@ void taint_recognise_error_traces( { std::vector successors; taint_collect_successors_inside_function( - goto_model, - trace, - elem, - summaries, - taint_name, - sink_function_name, - sink_instruction, - successors, - log - ); + goto_model, + trace, + elem, + summaries, + taint_name, + sink_function_name, + sink_instruction, + successors); if (successors.empty()) { - if (log != nullptr) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) + { dump_trace(trace.get_trace(), - "Skipping the following explored path", - ns, - log); + "Skipping the following explored path", ns, msg.debug()); + msg.debug() << messaget::eom; + } msg.debug() << "BACKTRACK: Normal inst no successors" << messaget::eom; bt_trace.backtrack(); } @@ -1371,7 +1331,7 @@ void taint_recognise_error_traces( compare_local_costs comp(insit.first->second); std::sort(successors.begin(),successors.end(),comp); - if(msghandler.get_verbosity()>=message_clientt::M_DEBUG) + if(message_handler.get_verbosity()>=messaget::M_DEBUG) { msg.debug() << "Conditional branch costs:" << messaget::eom; for(const auto& succ : successors) diff --git a/src/goto-analyzer/taint_trace_recogniser.h b/src/goto-analyzer/taint_trace_recogniser.h index 40a404f603f9..4c3ffa14c3e1 100644 --- a/src/goto-analyzer/taint_trace_recogniser.h +++ b/src/goto-analyzer/taint_trace_recogniser.h @@ -101,9 +101,7 @@ void taint_recognise_error_traces( object_numbers_by_field_per_functiont& object_numbers_by_field, const formals_to_actuals_mapt&, bool stop_after_one_trace, - message_handlert&, - std::stringstream* const log - ); + message_handlert& message_handler); void taint_recognise_error_traces( @@ -120,9 +118,7 @@ void taint_recognise_error_traces( object_numbers_by_field_per_functiont& object_numbers_by_field, const formals_to_actuals_mapt&, bool stop_after_one_trace, - message_handlert&, - std::stringstream* const log - ); + message_handlert& message_handler); #endif diff --git a/src/summaries/summary.h b/src/summaries/summary.h index 83fbf9825f40..732584dac469 100644 --- a/src/summaries/summary.h +++ b/src/summaries/summary.h @@ -175,7 +175,7 @@ class summary_json_databaset : public database_of_summariest, public messaget { } { std::ifstream index_stream(index_filename); - if(parse_json(index_stream,index_filename,get_message_handler(),index)) + if(parse_json(index_stream, index_filename, get_message_handler(), index)) throw "Failed to parse summaries index"; assert(index.is_object()); for(const auto& entry : index.object) @@ -218,7 +218,7 @@ class summary_json_databaset : public database_of_summariest, public messaget { jsont entry_json; { std::ifstream entry_stream(filename); - if(parse_json(entry_stream,filename,get_message_handler(),entry_json)) + if(parse_json(entry_stream, filename, get_message_handler(), entry_json)) throw "Failed to parse entry json"; } if(!entry_json.is_object()) diff --git a/src/summaries/summary_dump.cpp b/src/summaries/summary_dump.cpp index f25eaff280f2..cd069a60036a 100644 --- a/src/summaries/summary_dump.cpp +++ b/src/summaries/summary_dump.cpp @@ -415,28 +415,6 @@ std::string dump_goto_program_in_html( } -static std::string dump_log_in_html( - std::ostream const& source, - std::string const& dump_root_directory - ) -{ - fileutl_create_directory(dump_root_directory); - - std::string const log_filename = - msgstream() << dump_root_directory << "/index.html"; - std::fstream ostr(log_filename, std::ios_base::out); - if (!ostr.is_open()) - return msgstream() << "ERROR: sumfn::dump_log_in_html() : " - "Cannot open the log file '" << log_filename << "'." - ; - dump_html_prefix(ostr,"Log"); - ostr << "

Log from the summary computation

\n"; - ostr << source.rdbuf(); - dump_html_suffix(ostr); - return ""; // no error. -} - - static void replace( std::string& str, std::string const& what, @@ -503,14 +481,12 @@ static bool skip_fn_summary(std::string const& fname) std::string dump_in_html( - database_of_summariest const& computed_summaries, - callback_dump_derived_summary_in_htmlt const& summary_dump_callback, - goto_modelt const& program, - call_grapht const& call_graph, - std::string const& dump_root_directory, - bool const do_dump_program, - std::ostream* const log - ) + database_of_summariest const& computed_summaries, + callback_dump_derived_summary_in_htmlt const& summary_dump_callback, + goto_modelt const& program, + call_grapht const& call_graph, + std::string const& dump_root_directory, + bool const do_dump_program) { fileutl_create_directory(dump_root_directory); @@ -528,28 +504,16 @@ std::string dump_in_html( return err_message; } - for (auto it = computed_summaries.cbegin(); - it != computed_summaries.cend(); - ++it) + for(const auto& summary : computed_summaries) { - if (skip_fn_summary(it->first)) + if (skip_fn_summary(summary.first)) continue; - err_message = dump_in_html( - *it, + err_message = + dump_in_html( + summary, summary_dump_callback, program, - msgstream() << dump_root_directory << "/" << to_file_name(it->first) - ); - if (!err_message.empty()) - return err_message; - } - - if (log != nullptr) - { - err_message = dump_log_in_html( - *log, - msgstream() << dump_root_directory << "/log" - ); + msgstream() << dump_root_directory << "/" << to_file_name(summary.first)); if (!err_message.empty()) return err_message; } @@ -590,11 +554,6 @@ std::string dump_in_html( "here

\n" ; - if (log != nullptr) - ostr << "

Log from summary computation is available " - "here

\n" - ; - dump_html_suffix(ostr); return ""; // no error. diff --git a/src/summaries/summary_dump.h b/src/summaries/summary_dump.h index a61665ecf1da..dd0950f83a47 100644 --- a/src/summaries/summary_dump.h +++ b/src/summaries/summary_dump.h @@ -28,7 +28,7 @@ It provides dump of computed summaries in human readable form. Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -48,14 +48,14 @@ void dump_irept( typedef std::function - callback_dump_derived_summary_in_htmlt; + callback_dump_derived_summary_in_htmlt; /*******************************************************************\ Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -63,22 +63,20 @@ typedef std::function - callback_summary_to_jsont; + callback_summary_to_jsont; /*******************************************************************\ Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -135,7 +133,7 @@ std::string to_html_text(std::string result); Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -154,7 +152,7 @@ void dump_access_path_in_html( Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -172,7 +170,7 @@ void dump_html_prefix( Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose @@ -187,7 +185,7 @@ void dump_html_suffix(std::ostream& ostr); Function: - Inputs: See purpose + Inputs: See purpose Outputs: See purpose