From 2e226d8f39977efa98445b816a2c16037195a3b3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 18:13:04 +0100 Subject: [PATCH 1/6] use a separate message for show_goto_functions() for the console Rationale: the messages are output into a string buffer, which does not scale well in case there are many functions. Output can be delayed substantially. --- src/goto-programs/show_goto_functions.cpp | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 4180e38c719..f8855d9bc9d 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -62,14 +62,24 @@ void show_goto_functions( << (fun.second.body_available() ? "" : ", body not available") << " */"; + msg.status() << messaget::eom; } - - msg.status() << messaget::eom; } else { - goto_functions.output(ns, msg.status()); - msg.status() << messaget::eom; + auto &out = msg.status(); + for(const auto &fun : goto_functions.function_map) + { + if(fun.second.body_available()) + { + out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; + + const symbolt &symbol = ns.lookup(fun.first); + out << symbol.display_name() << " /* " << symbol.name << " */\n"; + fun.second.body.output(ns, symbol.name, out); + msg.status() << messaget::eom; + } + } } break; From b8212584f3389955c19813a1bd216de7989df7fa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 18:57:35 +0100 Subject: [PATCH 2/6] use color in show_goto_functions() --- src/goto-programs/show_goto_functions.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index f8855d9bc9d..03b2f14e9b8 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -75,7 +75,8 @@ void show_goto_functions( out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; const symbolt &symbol = ns.lookup(fun.first); - out << symbol.display_name() << " /* " << symbol.name << " */\n"; + out << messaget::bold << symbol.display_name() << messaget::reset + << " /* " << symbol.name << " */\n"; fun.second.body.output(ns, symbol.name, out); msg.status() << messaget::eom; } From 7e7445f0738ad3c1ab7c7e2a76a0d0b1691c7a4c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 20:13:56 +0100 Subject: [PATCH 3/6] consolidate the two variants of show-goto-functions --- src/goto-programs/show_goto_functions.cpp | 33 ++++++++++------------- 1 file changed, 14 insertions(+), 19 deletions(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 03b2f14e9b8..e02298d7fd0 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -52,32 +52,27 @@ void show_goto_functions( break; case ui_message_handlert::uit::PLAIN: - if(list_only) { for(const auto &fun : goto_functions.function_map) { const symbolt &symbol = ns.lookup(fun.first); - msg.status() << '\n' - << symbol.display_name() << " /* " << symbol.name - << (fun.second.body_available() ? "" - : ", body not available") - << " */"; - msg.status() << messaget::eom; - } - } - else - { - auto &out = msg.status(); - for(const auto &fun : goto_functions.function_map) - { - if(fun.second.body_available()) + const bool has_body = fun.second.body_available(); + + if(list_only) + { + msg.status() << '\n' + << symbol.display_name() << " /* " << symbol.name + << (has_body ? "" : ", body not available") << " */"; + msg.status() << messaget::eom; + } + else if(has_body) { - out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; + msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; const symbolt &symbol = ns.lookup(fun.first); - out << messaget::bold << symbol.display_name() << messaget::reset - << " /* " << symbol.name << " */\n"; - fun.second.body.output(ns, symbol.name, out); + msg.status() << messaget::bold << symbol.display_name() + << messaget::reset << " /* " << symbol.name << " */\n"; + fun.second.body.output(ns, symbol.name, msg.status()); msg.status() << messaget::eom; } } From 5841c2a94156b3818aa4915f6814d32ce88c2970 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 20:14:15 +0100 Subject: [PATCH 4/6] remove unused header --- src/goto-programs/show_goto_functions.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index e02298d7fd0..67827237c17 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -11,8 +11,6 @@ Author: Peter Schrammel #include "show_goto_functions.h" -#include - #include #include #include From 2a76328b3f1eea899d29a05cb031b7fe7f305f8d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 20:47:16 +0100 Subject: [PATCH 5/6] remove goto_modelt::output and goto_functionst::output Use show_goto_functions() instead --- src/goto-programs/goto_functions.cpp | 19 ------------------- src/goto-programs/goto_functions.h | 4 ---- src/goto-programs/goto_model.h | 6 ------ 3 files changed, 29 deletions(-) diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index 1b604509632..d9159731289 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -13,25 +13,6 @@ Date: June 2003 #include "goto_functions.h" -void goto_functionst::output( - const namespacet &ns, - std::ostream &out) const -{ - for(const auto &fun : function_map) - { - if(fun.second.body_available()) - { - out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; - - const symbolt &symbol=ns.lookup(fun.first); - out << symbol.display_name() << " /* " << symbol.name << " */\n"; - fun.second.body.output(ns, symbol.name, out); - - out << std::flush; - } - } -} - void goto_functionst::compute_location_numbers() { unused_location_number = 0; diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index a0cd4b14850..e9261c5dea9 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -72,10 +72,6 @@ class goto_functionst function_map.clear(); } - void output( - const namespacet &ns, - std::ostream &out) const; - void compute_location_numbers(); void compute_location_numbers(goto_programt &); void compute_loop_numbers(); diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 80c14205968..aea03ae86da 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -37,12 +37,6 @@ class goto_modelt : public abstract_goto_modelt goto_functions.clear(); } - void output(std::ostream &out) const - { - namespacet ns(symbol_table); - goto_functions.output(ns, out); - } - goto_modelt() { } From 4fcde9af6b06ab5d42733a910e0ef9e62fe64479 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Oct 2018 20:16:32 +0100 Subject: [PATCH 6/6] show_goto_functions: sort alphabetically --- src/goto-programs/goto_functions.cpp | 43 +++++++++++++++++++ src/goto-programs/goto_functions.h | 3 ++ src/goto-programs/show_goto_functions.cpp | 12 +++--- .../show_goto_functions_json.cpp | 9 ++-- src/goto-programs/show_goto_functions_xml.cpp | 9 ++-- 5 files changed, 65 insertions(+), 11 deletions(-) diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index d9159731289..169f57b91d1 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -13,6 +13,8 @@ Date: June 2003 #include "goto_functions.h" +#include + void goto_functionst::compute_location_numbers() { unused_location_number = 0; @@ -54,3 +56,44 @@ void goto_functionst::compute_loop_numbers() func.second.body.compute_loop_numbers(); } } + +/// returns a vector of the iterators in alphabetical order +std::vector +goto_functionst::sorted() const +{ + std::vector result; + + result.reserve(function_map.size()); + + for(auto it = function_map.begin(); it != function_map.end(); it++) + result.push_back(it); + + std::sort( + result.begin(), + result.end(), + [](function_mapt::const_iterator a, function_mapt::const_iterator b) { + return id2string(a->first) < id2string(b->first); + }); + + return result; +} + +/// returns a vector of the iterators in alphabetical order +std::vector goto_functionst::sorted() +{ + std::vector result; + + result.reserve(function_map.size()); + + for(auto it = function_map.begin(); it != function_map.end(); it++) + result.push_back(it); + + std::sort( + result.begin(), + result.end(), + [](function_mapt::iterator a, function_mapt::iterator b) { + return id2string(a->first) < id2string(b->first); + }); + + return result; +} diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index e9261c5dea9..6e49f30af5c 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -114,6 +114,9 @@ class goto_functionst for(const auto &fun : other.function_map) function_map[fun.first].copy_from(fun.second); } + + std::vector sorted() const; + std::vector sorted(); }; #define Forall_goto_functions(it, functions) \ diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 67827237c17..408c448d070 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -51,10 +51,13 @@ void show_goto_functions( case ui_message_handlert::uit::PLAIN: { - for(const auto &fun : goto_functions.function_map) + // sort alphabetically + const auto sorted = goto_functions.sorted(); + + for(const auto &fun : sorted) { - const symbolt &symbol = ns.lookup(fun.first); - const bool has_body = fun.second.body_available(); + const symbolt &symbol = ns.lookup(fun->first); + const bool has_body = fun->second.body_available(); if(list_only) { @@ -67,10 +70,9 @@ void show_goto_functions( { msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; - const symbolt &symbol = ns.lookup(fun.first); msg.status() << messaget::bold << symbol.display_name() << messaget::reset << " /* " << symbol.name << " */\n"; - fun.second.body.output(ns, symbol.name, msg.status()); + fun->second.body.output(ns, symbol.name, msg.status()); msg.status() << messaget::eom; } } diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 49e3b08f26a..3e9fb146516 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -41,10 +41,13 @@ json_objectt show_goto_functions_jsont::convert( { json_arrayt json_functions; const json_irept no_comments_irep_converter(false); - for(const auto &function_entry : goto_functions.function_map) + + const auto sorted = goto_functions.sorted(); + + for(const auto &function_entry : sorted) { - const irep_idt &function_name=function_entry.first; - const goto_functionst::goto_functiont &function=function_entry.second; + const irep_idt &function_name = function_entry->first; + const goto_functionst::goto_functiont &function = function_entry->second; json_objectt &json_function= json_functions.push_back(jsont()).make_object(); diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index db8b17ee666..41fd545a7fe 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -43,10 +43,13 @@ xmlt show_goto_functions_xmlt::convert( const goto_functionst &goto_functions) { xmlt xml_functions=xmlt("functions"); - for(const auto &function_entry : goto_functions.function_map) + + const auto sorted = goto_functions.sorted(); + + for(const auto &function_entry : sorted) { - const irep_idt &function_name=function_entry.first; - const goto_functionst::goto_functiont &function=function_entry.second; + const irep_idt &function_name = function_entry->first; + const goto_functionst::goto_functiont &function = function_entry->second; xmlt &xml_function=xml_functions.new_element("function"); xml_function.set_attribute("name", id2string(function_name));