Add Mopsa-like Warning Selectivity Reporting #1838
Conversation
|
There should be a reference added to Raphael Monat's paper proposing this approach. |
|
I think it's this one: https://inria.hal.science/hal-04652657v2 Should I add it to the code or just to the PR? |
|
Yes! Please add it to the code as well! |
michael-schwarz
changed the title
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| let safe ?(message = "") category = | ||
| match !Node0.current_node with | ||
| | Some (Statement _) -> | ||
| Check.check Kind.Safe category "%s" message | ||
| | _ -> () |
There was a problem hiding this comment.
Why does safe have this conditional, but not warn or error?
There was a problem hiding this comment.
Because warn and error always have a message attached, while most of the time safe doesn't
There was a problem hiding this comment.
Sure, but this isn't conditional on whether there is a message (or really, if it's the empty string), but rather Node0.current_node. These two things aren't related:
- If there's a
current_nodebut the message is empty, then the safe check with empty message is still recorded. - If there's no
current_nodebut there is a safe check (regardless of message), it is just forgotten.
I suspect the current_node check is a roundabout way to prevent safe checks from something that shouldn't output safe checks, but I don't know what that would be.
There was a problem hiding this comment.
The match is here because the safe messages can be sometimes in places where Node0 is None. In this cases we can't have a location and the safe is hence invalid. The check isn't in the warn and error checks because this None case never happen.
There was a problem hiding this comment.
Do you have examples of this were removing the extra condition would be a problem?
because inside Check.check there's a condition on AnalysisState.should_warn anyway, which is the same thing that control's Goblint's existing message output. It could be that there are places where should_warn is currently incorrectly (un)set and should be fixed, instead of covering up the issue here.
The condition on current_node also makes checks kind of asymmetric: warnings/errors from such places would still be added.
Discovered in #1838 (comment). Should be redundant due to #1764.
There was a problem hiding this comment.
Pull request overview
This PR adds Mopsa-like warning selectivity reporting to Goblint, based on a research paper by Raphaël Monat et al. The feature tracks all checks performed during analysis and categorizes them as Error (will definitely fail), Warning (might fail), or Safe (cannot fail). This provides more detailed information about the analyzer's findings beyond traditional warning messages.
Key changes:
- Introduces a new
Checksmodule to track and export check results - Adds "dashboard" output format that includes files, timing, and check results as JSON
- Integrates check tracking throughout the codebase for integer overflow, array bounds, division by zero, assertions, memory access, double free, and string literal writes
Reviewed changes
Copilot reviewed 13 out of 13 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| src/common/util/checks.ml | New module implementing check tracking with Kind (Error/Warning/Safe) and Category enums, hash-based storage, and JSON export |
| src/util/timing/goblint_timing_intf.ml | Adds root_with_current function to get timing tree with in-progress resources |
| src/framework/analysisResultOutput.ml | Adds "dashboard" output format that exports files, timing, and checks as JSON |
| src/config/options.schema.json | Updates schema to include "dashboard" as a valid result format option |
| src/cdomain/value/cdomains/intDomain0.ml | Adds Checks.warn calls for integer overflow/underflow alongside existing warnings |
| src/cdomain/value/cdomains/int/intDomTuple.ml | Adds Checks.safe calls when overflow checks pass, with no_safe parameter to control reporting |
| src/cdomain/value/cdomains/arrayDomain.ml | Integrates check tracking for array bounds, negative array size, null byte checks, and buffer overflow detection |
| src/cdomain/value/cdomains/addressDomain.ml | Adds checks for writing to string literals |
| src/analyses/useAfterFree.ml | Adds check tracking for double free and use-after-free detection |
| src/analyses/memOutOfBounds.ml | Integrates check tracking throughout memory bounds analysis for various pointer and array access scenarios |
| src/analyses/baseInvariant.ml | Adds check tracking for division by zero in invariant analysis |
| src/analyses/base.ml | Integrates checks for division/modulo by zero, null pointer dereference, and invalid memory deallocation |
| src/analyses/assert.ml | Adds check tracking for assertion success, failure, and unknown outcomes |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| | `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction | ||
| | `String "Double free" -> Ok DoubleFree | ||
| | `String "Negative array size" -> Ok NegativeArraySize | ||
| | category -> Error ("Checks.Category.of_yojson: Invalid category :" ^ Yojson.Safe.to_string category) |
There was a problem hiding this comment.
Missing space after colon in error message. Should be "Invalid category: " (with space after colon).
| | category -> Error ("Checks.Category.of_yojson: Invalid category :" ^ Yojson.Safe.to_string category) | |
| | category -> Error ("Checks.Category.of_yojson: Invalid category: " ^ Yojson.Safe.to_string category) |
| | `String "Invalid pointer comparison" -> Ok InvalidPointerComparison | ||
| | `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction | ||
| | `String "Double free" -> Ok DoubleFree | ||
| | `String "Negative array size" -> Ok NegativeArraySize |
There was a problem hiding this comment.
The of_yojson function for Category is missing the case for "Stub condition" that is defined in the to_yojson function. This will cause deserialization to fail for StubCondition checks.
| | `String "Negative array size" -> Ok NegativeArraySize | |
| | `String "Negative array size" -> Ok NegativeArraySize | |
| | `String "Stub condition" -> Ok StubCondition |
| if refine then raise Analyses.Deadcode else man.local | ||
| | `Lifted true -> | ||
| warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); | ||
| Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"%s\" will succeed"); |
There was a problem hiding this comment.
The ~message parameter contains a literal "%s" format specifier that won't be expanded. The message should be constructed using string concatenation like the other calls: ~message:("Assertion \"" ^ expr ^ "\" will succeed") to properly include the assertion expression.
| Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"%s\" will succeed"); | |
| Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"" ^ expr ^ "\" will succeed"); |
| let warn_past_end ?loc ?tags fmt = | ||
| Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore; | ||
| M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt |
There was a problem hiding this comment.
The construct Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore is incorrect. The Checks.error function returns a format continuation that expects additional arguments matching the format string fmt. Piping a format continuation to ignore discards it before it can consume its arguments. This should be restructured - either by making warn_past_end take a pre-formatted string and calling it with Printf.sprintf, or by properly handling the format continuation.
| let warn_past_end ?loc ?tags fmt = | |
| Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore; | |
| M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt | |
| let warn_past_end ?loc ?tags msg = | |
| Checks.error Checks.Category.InvalidMemoryAccess "%s" msg; | |
| M.error ~category:ArrayOobMessage.past_end ?loc ?tags "%s" msg |
| | `String "error" -> Ok Error | ||
| | `String "warning" -> Ok Warning | ||
| | `String "safe" -> Ok Safe | ||
| | kind -> Error ("Checks.Kind.of_yojson: Invalid kind :" ^ Yojson.Safe.to_string kind) |
There was a problem hiding this comment.
Missing space after colon in error message. Should be "Invalid kind: " (with space after colon).
| | kind -> Error ("Checks.Kind.of_yojson: Invalid kind :" ^ Yojson.Safe.to_string kind) | |
| | kind -> Error ("Checks.Kind.of_yojson: Invalid kind: " ^ Yojson.Safe.to_string kind) |
3 participants
The PR adds a new kind of output inspired by this paper from R. Monat & al: https://inria.hal.science/hal-04652657v2. This output contains all the checks performed by the analyzer and their result of three types:
This output only takes into account the following checks: