Rework system outputting warnings #255

Wherekonshade · 2021-06-17T11:28:25Z

This pull request closes #201
We introduced a must or may tag and the following categories:

    - Behavior
        * Undefined
	* ArrayOutOfBounds
		     * PastEnd
		     * BeforeStart
		     * Unknown
	* NullPointerDereference
	* UseAfterFree
	
    - Implementation
    - Machine

    -Integer
        * Overflow
        * Div_by_zero

    -Cast
        * Type_mismatch (bug)

    -Race

~~We introduced the warning as mywarn, which can be renamed to the normal warn once all warnings have been replaced.~~

The user can enable/disable the following flags(enabled by default) to filter warnings:

dbg.warn.may
dbg.warn.must
dbg.warn.behavior
dbg.warn.integer
dbg.warn.cast
dbg.warn.race
dbg.warn.array

The structure inside messages.ml is the following:
module LogEvent with two fields:
• certainty: May | Must (optional, if it's None, then it's always printed -> this is used for debugging)
• event_type: Behavior | Integer | ... (these can bear additional information but it needs to be determined what information is useful for which warning type)
also has methods .may and .must to shorten the creation of may/must warnings (then it only takes the event_type as an argument)

Calling the warnings should be rather intuitive but here are some examples:
M.warn @@ M.Warning.Unknown "Extra info can be passed here";
M.warn_each ~must:true @@ warn_type M.ArrayOOB.PastEnd;

Path sensitivity was not taken into account as it was ruled out of scope.

But there are still some things open to discussion in our opinion:
~~1. The flags would also make sense in Std in our opinion~~ We will introduce a new category as suggested by @sim642
2. What other categories should be introduced ?
3. Should the user be able to enable/disable subcategories ? Right now he can enable/disable the behavior category but not the subcategory of NullPointerDereference for example

for now with just the unknown type and still the mywarn name

sim642

In #201 (comment) it was said:

Reports and warnings should be merged with this new approach.

Yet Messages.report is still a thing.

src/cdomains/valueDomain.ml

sim642 · 2021-06-28T08:01:43Z

src/util/defaults.ml

+      ; reg Debugging "dbg.warn.behavior"        "true"  "undefined behavior warnings"
+      ; reg Debugging "dbg.warn.integer"        "true"  "integer (Overflow, Div_by_zero) warnings"
+      ; reg Debugging "dbg.warn.cast"        "true"  "Cast (Type_mismatch(bug) warnings"
+      ; reg Debugging "dbg.warn.race"        "true"  "Race warnings"
+      ; reg Debugging "dbg.warn.array"        "true"  "Array (Out_of_bounds of int*int) warnings"
+      ; reg Debugging "dbg.warn.unknown"        "true"  "Unknown (of string) warnings"
+      ; reg Debugging "dbg.warn.debug"        "true"  "Debug (of string) warnings"
+      ; reg Debugging "dbg.warn.may"        "true"  "Enable or disable may warnings"
+      ; reg Debugging "dbg.warn.must"        "true"  "Enable or disable must warnings"


It probably makes sense to have a separate category for warnings instead of shoving them all under debugging.

It is now a separate category, but unfortunately just warn is already used in Std so I named the option warn_filter.

warn should not be needed as often, so it could be renamed to warn_at or sth similar which is more descriptive anyway.

alright, I renamed warn to warn_at and put all the options for our warnings into just warn instead of the warn_filter

Seems to me like the options could even be warn.at and warn.filter also in the warning options category.

Maybe warn.on.x since warn.filter.x can be confused as filter out x or only show x.

sim642 · 2021-06-28T08:06:05Z

src/util/messages.ml

+    | Must -> "[MUST]"
+end
+
+module LogEvent =


Why is this called LogEvent?

We would be happy to change it, if you have a different suggestion ? :)

Why are any of those called Event? IMO sth like Warn.Integer.Overflow would be more readable than M.EventType (M.EventType.Integer M.IntegerEvent.Overflow).
Of course if you want to filter Integer as a group, it can't be flat but you need some run-time representation. Could define some shortcuts or even generate them.

Also see #201 (comment)
I would also nest those modules to reflect the hierarchy of the types. But then you have problems with the different paths w/o shortcuts.

Maybe this should be called Warning?

Warning or Warn sound good 👍
I originally named it LogEvent since I associate warn, debug etc with logging.

okay I changed LogEvent to Warning, EventType to WarnType and the others to the version without Event too - such as IntegerEvent to Integer. Is it okay like this?

I felt like the combination of WarnType and Warning was a little confusing after all and changed it to Warning and WarningWithCertainty. The warn and warn_each functions now accept Warning and an optional bool parameter must. Then the WarningWithCertainty is constructed from that internally. So the users should never have to type this long module name and only use the Warning module.

sim642 · 2021-06-28T08:14:57Z

src/analyses/base.ml

      let warn_and_top_on_zero x =
        if GU.opt_predicate (BI.equal BI.zero) (ID.to_int x) then
-          (M.warn "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
+          (M.warn (M.LogEvent.may (M.EventType.Unknown ("Must Undefined Behavior: Second argument of div or mod is 0, continuing with top")));


What's the point of defining Certainty.Must and BehaviorEvent if they're not properly used? Same goes for many other EventTypes.

We have currently only changed our newly added warnings to their proper types. These changes with the unknowns are for backwards compatibility to make it compile as we were not sure what exact types should be which of these lines. This line you commented on is especially tricky since the text says Undefined behavior but I think in the categories it should be Integer.DivByZero ?

it should be Integer.DivByZero

Which is undefined behavior (same goes for Integer.Overflow).
Those Event modules need some cleanup/reordering.
If each of those modules just consists of a type t and show for it, you could also just put all types in one module and name the types accordingly.

sim642 · 2021-06-28T08:18:44Z

src/util/messages.ml

+module IntegerEvent =
+struct
+  type t = Overflow | DivByZero
+end
+
+module CastEvent =
+struct
+  type t = TypeMismatch
+end
+
+module ArrayEvent =
+struct
+  type t = OutOfBounds of int*int
+end


It's quite clear that these aren't properly used if they don't have show implemented and everything is still fine.

yes, these are just prepared here to be extended as we weren't exactly sure where to use them or what information would be relevant to pass into them. Plus for example, we now have Array out of bounds under Undefined behavior and I actually don't know which one should it be - whether array out of bounds should be in this Array event or whether it should belong under the undefined behavior which it also is.

I would put it in undefined behavior. Most of our warnings prob. are about UB. Which ones aren't besides asserts?
If we had some warnings in Array and UB.Array, it'd be cumbersome to filter for both.
If we have such cases, we could let UB.Array imply Array for filtering.

sim642 · 2021-06-28T08:21:21Z

src/util/messages.ml

+end
+
+module Certainty = struct
+  type t = May | Must


I don't know where, but somewhere we must it very clear that this Must doesn't truly mean "must" as commonly understood in program analysis. Not only does this have to be clear to every Goblint developer in the code, but somehow also to any user just running Goblint and reading the output.

Maybe it just needs a new name like MustIfReach.

We discussed putting this disclaimer into the readme or the docs but a new name as suggested sounds like the best solution to us. We'll do that, thank you

Wouldn't MustIfReach imply that whenever a line is reached then this event occurs? Whereas in the following example the line with the array access is reached multiple times but only once it's a Must out of bounds access.

void f(int n) { int arr[5]; arr[n] = 1; // this line is reached 3 times and in one case it's in bounds, in one certainly out of bounds and in the last one it could be anything } int main() { f(3); // -> this results in an in bounds access f(10); // -> this results in a Must Warning in the function f int top; f(top); // -> this results in a May Warning in the function f }

What I'd like to see here ideally would be something like

arr[n] = 1; is out of bounds following the function call f(10);

Yes, there's dbg.warn_with_context which is off by default and currently only supplied the context for asserts.
If you turn it on and add ~ctx, the warning should include the context of f(10).
Ideally, the result viewer would then take care to indicate such things.

vogler · 2021-06-29T13:24:43Z

src/analyses/region.ml

      let to_exp (v,f) = (v,Lval.Fields.to_offs' f) in
      List.map to_exp (Reg.related_globals ev (part,reg))
-    | `Top -> Messages.warn "Region state is broken :("; []
+    | `Top -> Messages.warn (Messages.LogEvent.may (Messages.EventType.Unknown ("Region state is broken :("))); []


This seems too verbose. Not specific to this, but in general.
Now with the non-polymorphic variants, there's no way around the path, but maybe change all those calls to
Messages.(warn (LogEvent.may (EventType.Unknown ("Region state is broken :("))))?

I think in most modules Messages was imported as just M. Would maybe some similar shortcuts help with the verbosity too? Or bring some more of the types a bit higher like M.warn_may and M.warn_must or may_unknown, must_integer and may_integer ?

Yes. You can also just define aliases instead of pulling them out. Or as I wrote above, just put all types in one module. If there's only going to be the type and show for it, modules for each just makes it unnecessarily verbose (I assume they're not going to be put in some functor).

I think in most modules Messages was imported as just M.

I meant the repeated M.x M.y M.z instead of M.(x y z).

Another way to make it less verbose would be to have the certainty as an optional argument for warn and warn_each as it is already done with ?ctx:
M.(warn Integer "...")
M.(warn ~must:true Integer "...")
I assume we produce more may than must.

The optional must parameter is now there. I also added some nesting and helper methods to build the types from the bottom so now it should be possible to do:

M.warn (M.Warning.Integer.overflow ()); M.warn (M.Warning.Behavior.Undefined.nullpointer_dereference ()); M.warn ~must:true (M.Warning.Behavior.Undefined.ArrayOutOfBounds.before_start ());

also the variants are now not hidden inside modules so the top level variants can be used directly as:

M.warn (M.Unknown "my message");

@vandah Previously, there was the Certainty.t option, which would allow for None in case of "Debug" warnings. How is this handled now?

This remained there. The debug function still works the same.

Before, I just called warn from the debug function. Now there's a function warn_internal which does what warn did previously and is called from both warn and debug. This warn_internal takes the type WarningWithCertainty.t which still has the Certainty.t option inside.

LogEvent -> Warning EventType -> Warn IntegerEvent -> Integer> ...

src/util/messages.ml

also renames Warning -> WarningWithCertainty and WarnType -> Warning

also remove the array type because arrayoob is under UB

src/util/messages.ml

jerhard · 2021-07-07T09:30:17Z

src/util/messages.ml

+  let to_string e =
+    match e with
+    | May -> "may"
+    | Must -> "must"
+
+  let should_warn e =
+    get_bool ("warn." ^ (to_string e))


Same applies here.

src/util/messages.ml

also uses concatenation instead of redundant sprintf

and replace unused parameters with `_`

also adds optional location to warn_each

this eliminates the need to specify the regexes separately in update_suite.rb later it would probably be nice if the categories were parsed and checked there also changes formatting of the warning tags

also adds optional msg argument and removes string params from unknown and debug

vesalvojdani · 2021-07-09T12:30:02Z

I added to our GobCon agenda that we should discuss the follow-up work to this pull request next meeting. There is still a lot of open questions about the warning system, so it would probably be best to merge this pull request, and then proceed with somewhat smaller pull requests and discussions on all the remaining questions.

vandah and others added 15 commits June 15, 2021 20:22

types + functions for new warning system

97f8006

pray for us

da2714d

fix warning type

9bf11a2

Merge branch 'master' into warnings_rework

0a85be6

Added flags for all warning categories

6be69b6

Renamed flags for more clarity

fb9bb6c

basic filtering of warnings

cb20141

scope warning types under dbg.warn.*

ab1983f

fix typos, add required warn types as options

48b2765

Added flag for filtering of must and may

1d496cc

All warning flags are now enabled by default

cf24baf

add filtering for may/must

1c346d0

new warning system for VD

5151067

Merge branch 'goblint:master' into warnings_rework

8aefa56

use new warning system throughout goblint

fe5f164

for now with just the unknown type and still the mywarn name

michael-schwarz added practical-course Practical Course at TUM student-job labels Jun 17, 2021

replace mywarn with warn and fix build with that

4214c5e

michael-schwarz requested review from MartinWehking, felihong, hydrogenoxide and nicokn June 17, 2021 11:52

sim642 reviewed Jun 28, 2021

View reviewed changes

sim642 mentioned this pull request Jun 28, 2021

Detect Array out of bounds #257

Merged

Wherekonshade and others added 2 commits June 28, 2021 12:17

Cleanup

3511979

Merge branch 'master' into warnings_rework

292fc08

vogler reviewed Jun 29, 2021

View reviewed changes

vandah added 3 commits June 30, 2021 22:15

make warnings a separate section of cli options

4993cbc

dbg.warn -> warn_filter

f8a1b06

change type names for warnings

fa058e0

LogEvent -> Warning EventType -> Warn IntegerEvent -> Integer> ...

warn -> warn_at, warn_filter -> warn

9e71887

jerhard reviewed Jul 1, 2021

View reviewed changes

src/util/messages.ml Outdated Show resolved Hide resolved

jerhard reviewed Jul 2, 2021

View reviewed changes

src/util/messages.ml Outdated Show resolved Hide resolved

vandah added 5 commits July 6, 2021 16:37

remove commented out code from messages.ml

049337b

make certainty an optional parameter

19c29cc

also renames Warning -> WarningWithCertainty and WarnType -> Warning

really nested warning types

ac256d7

add create functions to submodules

7f4088a

also remove the array type because arrayoob is under UB

complete the removal of the Array type of warning

4403b56

jerhard reviewed Jul 7, 2021

View reviewed changes

src/util/messages.ml Outdated Show resolved Hide resolved

Merge branch 'master' into warnings_rework

0617b88

jerhard reviewed Jul 7, 2021

View reviewed changes

vandah added 12 commits July 7, 2021 11:47

use parameters of Integer and Cast

2b23f15

also uses concatenation instead of redundant sprintf

remove testing warning

c8b7097

move to_string inside should_warn

c4eb3ad

and replace unused parameters with `_`

M.report -> M.warn_each

3132fc8

also adds optional location to warn_each

add [Warning] tag to all warnings

4bc586f

this eliminates the need to specify the regexes separately in update_suite.rb later it would probably be nice if the categories were parsed and checked there also changes formatting of the warning tags

remove [Warning] tag from Debug

a58eac7

parse warning types from spec analysis

b57e08f

make warning an optional argument

6cc42d2

also adds optional msg argument and removes string params from unknown and debug

try to fix warn calls also in comments

92b8d73

revert irrelevant change in regtests

830bb9c

remove category string from spec warns

73cec78

warnings documentation

843ed01

sim642 mentioned this pull request Jul 23, 2021

Rework system outputting warnings #201

Closed

sim642 self-assigned this Aug 23, 2021

sim642 merged commit 6e33162 into goblint:master Aug 24, 2021

sim642 mentioned this pull request Aug 31, 2021

Refactor and generalize warning system to message system #338

Merged

4 tasks

sim642 mentioned this pull request Oct 11, 2021

SARIF output format #376

Merged

Rework system outputting warnings #255

Rework system outputting warnings #255

Uh oh!

Conversation

Wherekonshade commented Jun 17, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

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!

vogler Jul 1, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Wherekonshade commented Jun 17, 2021 •

edited

Loading

vogler Jul 1, 2021 •

edited

Loading