use a separate message for show_goto_functions() for the console #3165

kroening · 2018-10-14T17:15:19Z

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.

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

Code duplication isn't great, and with the further changes in this PR we actually have two bits of code that generate almost, but not exactly the same output anymore.

tautschnig · 2018-10-14T18:43:19Z

src/goto-programs/show_goto_functions.cpp

    }
    else
    {
-      goto_functions.output(ns, msg.status());
-      msg.status() << messaget::eom;
+      auto &out = msg.status();


I think this just makes the code harder to read, but if it is used then it should be used consistently below.

tautschnig · 2018-10-14T18:44:26Z

src/goto-programs/show_goto_functions.cpp

+      {
+        if(fun.second.body_available())
+        {
+          out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";


I don't think it's a good idea to have code duplication - couldn't this also be fixed within goto_functionst::output? Else, that method should be removed.

It can't be fixed without changing the signature -- contemplating to remove.

Removing might be the best solution. Code that is almost duplicated is the prone to cause trouble.

tautschnig · 2018-10-14T19:40:17Z

As side note: it might be time to factor out a number of commits into PRs of their own. Both discussion and CI failure will likely just hold up a number of commits that are 1) very useful for follow-up work and 2) are easy to merge.

kroening · 2018-10-14T19:43:58Z

#3166 !

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 73558e5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87894799
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

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.

tautschnig

Some more debate plus the note that an overly long line breaks CI.

tautschnig · 2018-10-15T17:08:48Z

src/goto-programs/show_goto_functions.cpp

        {
-          out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
+          msg.status() << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";

          const symbolt &symbol = ns.lookup(fun.first);


Shouldn't this line be removed as it is now redundant?

You mean because of the colouring?

No, because of the refactoring in "consolidate the two variants of show-goto-functions".

sorry, the line was unclear -- yes, redundant, yes, removed

tautschnig · 2018-10-15T17:10:09Z

src/goto-programs/show_goto_functions.cpp

@@ -51,9 +53,19 @@ void show_goto_functions(

  case ui_message_handlert::uit::PLAIN:
    {
+      // sort alphabetically


Why is this only done in the PLAIN output? It might make the most sense for that case, but then at least the commit message should be clear about that.

Ok, will sort all

tautschnig · 2018-10-15T17:12:12Z

src/goto-programs/show_goto_functions.cpp

      {
-        const symbolt &symbol = ns.lookup(fun.first);
+        const symbolt &symbol = ns.lookup(f_id);
+        const auto &fun = *goto_functions.function_map.find(f_id);


We've had all sorts of debates about performance and sorting: in keeping with this, shouldn't this lookup be avoided by using a vector that includes n iterator, and using a custom comparison operator?

Now in a separate function where this can be tweaked further if need be.

tautschnig · 2018-10-16T13:10:08Z

src/goto-programs/show_goto_functions_json.cpp

+
+  const auto sorted = goto_functions.sorted();
+
+  for(const auto function_entry : sorted)


Minor note: here (and also in the XML case) this should likely be a const auto &. It's just an iterator so not terribly expensive to copy, but it's being done in the PLAIN case and would thus at bare minimum ensure consistency.

I'd be tempted to remove the & in the PLAIN case. References to iterators are unusual; copying them is very common.

I have no strong opinion either way, just consistency is what I'd call for.

Use show_goto_functions() instead

allredj

Passed Diffblue compatibility checks (cbmc commit: 4fcde9a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88158804

kroening added the enhancement label Oct 14, 2018

kroening assigned tautschnig and peterschrammel Oct 14, 2018

kroening requested review from tautschnig and peterschrammel October 14, 2018 17:15

kroening requested review from pkesseli and smowton as code owners October 14, 2018 17:15

kroening force-pushed the goto_functions_message branch from 699008b to d9ccb11 Compare October 14, 2018 18:37

tautschnig requested changes Oct 14, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Oct 14, 2018

kroening force-pushed the goto_functions_message branch from 955959c to 73558e5 Compare October 14, 2018 20:35

allredj reviewed Oct 14, 2018

View reviewed changes

use a separate message for show_goto_functions() for the console

2e226d8

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.

kroening force-pushed the goto_functions_message branch from 73558e5 to ae313b1 Compare October 15, 2018 14:30

use color in show_goto_functions()

b821258

kroening force-pushed the goto_functions_message branch from ae313b1 to e6c46fa Compare October 15, 2018 14:37

kroening assigned tautschnig and unassigned kroening Oct 15, 2018

tautschnig reviewed Oct 15, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Oct 16, 2018

kroening force-pushed the goto_functions_message branch from e6c46fa to 71eb7b2 Compare October 16, 2018 12:58

kroening assigned tautschnig and unassigned kroening Oct 16, 2018

tautschnig approved these changes Oct 16, 2018

View reviewed changes

tautschnig reviewed Oct 16, 2018

View reviewed changes

tautschnig removed their assignment Oct 16, 2018

tautschnig assigned kroening and unassigned peterschrammel Oct 16, 2018

Daniel Kroening added 2 commits October 16, 2018 16:21

consolidate the two variants of show-goto-functions

7e7445f

remove unused header

5841c2a

kroening force-pushed the goto_functions_message branch 4 times, most recently from 21d5d8d to a484b8b Compare October 16, 2018 16:30

Daniel Kroening added 2 commits October 16, 2018 18:25

remove goto_modelt::output and goto_functionst::output

2a76328

Use show_goto_functions() instead

show_goto_functions: sort alphabetically

4fcde9a

kroening force-pushed the goto_functions_message branch from a484b8b to 4fcde9a Compare October 16, 2018 17:26

allredj reviewed Oct 16, 2018

View reviewed changes

kroening merged commit 8321a10 into develop Oct 17, 2018

kroening deleted the goto_functions_message branch October 17, 2018 09:53


		const auto sorted = goto_functions.sorted();

		for(const auto function_entry : sorted)

use a separate message for show_goto_functions() for the console #3165

use a separate message for show_goto_functions() for the console #3165

Uh oh!

Conversation

kroening commented Oct 14, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Oct 14, 2018

Uh oh!

kroening commented Oct 14, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kroening commented Oct 14, 2018 •

edited

Loading