goblint / GobPie

Goblint IDE integration via MagpieBridge
MIT License
5 stars 3 forks source link

Mode to show only one warning per message group #44

Closed karoliineh closed 1 year ago

karoliineh commented 1 year ago

@vesalvojdani requested an option for GobPie to only show one warning per message group, especially with the race-warnings, as the current view is very cluttered. The current (cluttered) view, although, should still be available - therefore only a viewing option rather than an actual design desicion.

There are several possible ways how to implement the selection of the warning-to-be-shown:

  1. Select the most meaningful one (ideal, but difficult: how do we know, which one is the most meaningful?)
  2. Select the one occurring the first in the code (needs some warnings sorting)
  3. Randomly select one from the group (the simplest one to implement for sure)
sim642 commented 1 year ago

Blindly only showing one submessage isn't always correct. For example, deadlock warnings output the entire cycle as submessages, but any single one on its own isn't really meaningful.

vesalvojdani commented 1 year ago

What do you mean by one sub-message here? I don't know how the groups are shown for deadlocks, but the way I imagine things, there would not be less information shown. At least for races, we have for each race group, all sub-messages also as independent race warnings, so we get one warning per access essentially. I would just keep one group with all the sub-messages only as "related" locations, but not as independent top-level warning. This should also be okay for deadlocks. There would just not be error markers in the code at every access. I think that's the original reason we wanted all accesses to be top-level warnings.

sim642 commented 1 year ago

If there's a deadlock warning like

[Warning][Deadlock] Locking order cycle:
  lock before: mutex2 with mhp:{tid=[main], {t2@tests/regression/15-deadlock/01-basic_deadlock.c:32:5-32:40}} (tests/regression/15-deadlock/01-basic_deadlock.c:19:3-19:30)
  lock after: mutex1 with [mhp:{tid=[main], {t2@tests/regression/15-deadlock/01-basic_deadlock.c:32:5-32:40}}, lock:{mutex2}] (tests/regression/15-deadlock/01-basic_deadlock.c:20:3-20:30)
  lock before: mutex1 with mhp:{tid=[main], {t1@tests/regression/15-deadlock/01-basic_deadlock.c:31:5-31:40}} (tests/regression/15-deadlock/01-basic_deadlock.c:10:3-10:30)
  lock after: mutex2 with [mhp:{tid=[main], {t1@tests/regression/15-deadlock/01-basic_deadlock.c:31:5-31:40}}, lock:{mutex1}] (tests/regression/15-deadlock/01-basic_deadlock.c:11:3-11:30)

Then only showing a warning

[Warning][Deadlock] Locking order cycle: lock before: mutex2

is confusing because that's neither of the two locations where the code actually deadlocks (those are the lock afters). This group submessage already is contextual information for the actual deadlock locations.

vesalvojdani commented 1 year ago

Okay, but we would still show all the related information. This is strictly about the GobPie translation of a single goblint warning group into multiple warning groups with each of the sub-messages being a separate warning group. I might not have a clean build of goblint/gobpie that I tried this on, but I get 16 warnings for regtest 15/01 in GobPie. So Goblint produces four warnings with four sub-messages each, and GobPie explodes this to 4*4 with lots of duplication. And it's not like the related segment is in any way clustered in VSCode, so it's a jumbled mess to navigate these things.

The only reason to do this explosion is to have markers at all access location, but the amount of clutter for me completely outweighs this benefit. I'd rather have a one-to-one correspondence with Goblint's output than making sure we get markers everywhere.

sim642 commented 1 year ago

My point is just that GobPie cannot make a sensible choice for which one to keep, but Goblint itself could because it knows the semantics of all these things. There was an idea to sort and prioritize accesses in Goblint anyway, so one might as well supply that information from Goblint and not require GobPie to make any decisions.

vesalvojdani commented 1 year ago

Ideally, goblint should supply location information for the entire message group, but until it does so for races, I would prefer an interim solution where these warnings are not exploded. The grouped display in GobPie is extra ugly because the location's message is concatenated with the group warning into a multiline message and then the rest are sub-messages. It would be easier to read if GobPie stayed completely true to the Goblint output.

One consistent approach would be for grouped warnings to be without location unless Goblint supplies one. But wherever it puts the marker for the group it would be more readable if all accesses were sub-messages rather than having one of them concatenated with the group message. I actually don't see a huge problem placing the message at a random location, as long as the complete information is available in the sub-messages.

Anyway, I'd like the GobPie's "problem" panel to look as similar to Goblint's output as possible.