Join and format warnings about concurrent constructs #2135

celinval · 2023-01-18T22:55:44Z

Description of changes:

We were emitting warnings using the warn macro at every occurrence of a concurrent constructs, which wasn't very user friendly. Instead, we now aggregate them and only print one warning at the end, similar to how we handle unsupported constructs.

Resolved issues:

Resolves #1460 ??

Related RFC:

N/A

Call-outs:

With this PR, I propose that we close #1460 in favor of reducing the verbosity of those messages by aggregating them as we did for unsupported constructs. @fzaiser @adpaco-aws, would that be OK?

The output now looks like this for the test kani/Intrinsics/Atomic/Stable/Store/main.rs:

$ kani main.rs --only-codegen
warning: Found the following unsupported constructs:
             - caller_location (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: Kani does not support concurrency for now. The following constructs will be treated as sequential operations:
             - atomic_store_relaxed (1)
             - atomic_load_seqcst (1)
             - atomic_store_seqcst (1)
             - atomic_store_release (1)
             - atomic_load_acquire (1)
             - atomic_load_relaxed (1)

warning: 2 warnings emitted

Testing:

How is this change tested?
Is this a refactor change?

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

We were emitting warnings using the `warn` macro at every occurrence of a concurrent constructs, which wasn't very user friendly. Instead, we now aggregate them and only print one warning at the end, similar to how we handle unsupported constructs.

zhassan-aws

Thanks! A couple of minor comments.

Also, we're currently storing the location of each occurrence, but not using it. Would it make sense to include all the locations in the warning under some flag (e.g. --verbose) in case the user wants to find out where they're used?

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

celinval · 2023-01-19T00:29:27Z

Thanks! A couple of minor comments.

Also, we're currently storing the location of each occurrence, but not using it. Would it make sense to include all the locations in the warning under some flag (e.g. --verbose) in case the user wants to find out where they're used?

I thought about expanding the location with --verbose, but I was looking at the logs, they tend to just print the same std file (atomic.rs), so I don't think they were adding much value. I think only thread_local would add something more meaningful. We could include the name of the calling function for the intrinsics case.

That said, I rather not do this as part of this change. I understand that the new format loses that information, so let me know if you think it is a blocker. I could also skip saving the location for now (and even drop the counter in the message).

I do like the suggestion to print more information when requested (especially for unsupported constructs), which I think is even more important since it can result on a harness failure.

celinval · 2023-01-19T05:18:41Z

Should I lower it to an info instead of warning?? @zhassan-aws

zhassan-aws · 2023-01-19T05:44:49Z

Are you asking because we would already emit a warning if the program had other concurrency constructs (e.g. threads)? If so, I still suggest we keep it a warning to make it a bit more obvious to the user how Kani is handling them.

zhassan-aws · 2023-01-19T05:46:18Z

That said, I rather not do this as part of this change. I understand that the new format loses that information, so let me know if you think it is a blocker. I could also skip saving the location for now (and even drop the counter in the message).

No, it's fine to do this in a separate PR.

adpaco-aws

Thanks @celinval for doing this!

I'm in favor of merging it as is, just have a couple of comments to keep in mind.

adpaco-aws · 2023-01-19T14:51:29Z

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

+    /// Kani does not currently support concurrency and the compiler assumes that when generating
+    /// code for some specialized concurrent constructs that this is the case. We store all types of
+    /// operations that had this special handling and print a warning at the end of the compilation.
+    pub fn store_concurrent_construct(&mut self, operation_name: &str, loc: Location) {


As mentioned, printing the location isn't useful at the moment. A better thing to do would be storing locations from function calls up to here, then print whichever is closest to the user's code. But we don't have anything like that at the moment, right?

adpaco-aws · 2023-01-19T14:56:13Z

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

+
+    if !ctx.concurrent_constructs.is_empty() {
+        let mut msg = String::from(
+            "Kani currently does not support concurrency. The following constructs will be treated \


This messaging could also be improved. In particular, I think we should avoid using "Kani" in our messages, and say something like "Concurrency is not supported at the moment". But I'm afraid this will break some stuff, so let's not do it here.

I think we should avoid using "Kani" in our messages

Why is that?

You're running Kani, so it's odd printing messages that mention Kani in any way when you're already in that context. If I'm not mistaken, the Rust compiler won't use its own name in messages unless it's talking about specific editions (e.g., "this construct isn't supported in Rust 2018"). Otherwise, I feel like it becomes repetitive for users to see messages like "Kani does this" or "Kani does that" (there may be exceptions, of course).

tedinski

lgtm, though my thoughts are:

CBMC supports concurrency... For some of these I wonder how hard it's really be to make (at least some of) them work as intended. We could reduce the warning count to the ones we really don't handle right.
It actually still looks like a lot of operations. Wonder if we should bother with any further condensation (e.g. "atomic load/store" as one?) But... this isn't important. Big enough improvement for one PR.

celinval requested a review from a team as a code owner January 18, 2023 22:55

zhassan-aws approved these changes Jan 19, 2023

View reviewed changes

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs Outdated Show resolved Hide resolved

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs Outdated Show resolved Hide resolved

Apply suggestions from code review

48de29a

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Merge branch 'main' into issue-1460-verbose-async

89ee590

adpaco-aws approved these changes Jan 19, 2023

View reviewed changes

tedinski approved these changes Jan 19, 2023

View reviewed changes

celinval merged commit 5de2eb4 into model-checking:main Jan 19, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Join and format warnings about concurrent constructs #2135

Join and format warnings about concurrent constructs #2135

celinval commented Jan 18, 2023

zhassan-aws left a comment

celinval commented Jan 19, 2023 •

edited

Loading

celinval commented Jan 19, 2023

zhassan-aws commented Jan 19, 2023

zhassan-aws commented Jan 19, 2023

adpaco-aws left a comment

adpaco-aws Jan 19, 2023 •

edited

Loading

adpaco-aws Jan 19, 2023

tedinski Jan 19, 2023

adpaco-aws Jan 19, 2023 •

edited

Loading

tedinski left a comment

Join and format warnings about concurrent constructs #2135

Join and format warnings about concurrent constructs #2135

Conversation

celinval commented Jan 18, 2023

Description of changes:

Resolved issues:

Related RFC:

Call-outs:

Testing:

Checklist

zhassan-aws left a comment

Choose a reason for hiding this comment

celinval commented Jan 19, 2023 • edited Loading

celinval commented Jan 19, 2023

zhassan-aws commented Jan 19, 2023

zhassan-aws commented Jan 19, 2023

adpaco-aws left a comment

Choose a reason for hiding this comment

adpaco-aws Jan 19, 2023 • edited Loading

Choose a reason for hiding this comment

adpaco-aws Jan 19, 2023

Choose a reason for hiding this comment

tedinski Jan 19, 2023

Choose a reason for hiding this comment

adpaco-aws Jan 19, 2023 • edited Loading

Choose a reason for hiding this comment

tedinski left a comment

Choose a reason for hiding this comment

celinval commented Jan 19, 2023 •

edited

Loading

adpaco-aws Jan 19, 2023 •

edited

Loading

adpaco-aws Jan 19, 2023 •

edited

Loading