Ignore messages for assert, panic, and unreachable macros

[zhassan-aws]

Description of changes:

We've had a myriad of issues related to the processing of messages for the assert, panic, and unreachable macros using the format_args macro. The purpose of using format_args in an unreachable (if false) block was to make sure the args are checked for errors/warnings. However, the usage of format_args caused Kani to fail to compile crates that use assert and panic in const contexts (e.g. https://github.com/time-rs/time/blob/4c13327d5fed8571316b181e828067fc54038e05/time/src/lib.rs#L362). Fixing this would require using a macro that has the following properties:

1. It processes the format args and checks for errors
2. It can be used in a const context
3. It is not overridden by Kani

We're unaware of a macro that satisfies those 3 properties. The format_args macro seems to be on its way to be usable in const contexts as the error message indicates:

error: `std::fmt::Arguments::<'a>::new_v1` is not yet stable as a const fn
   --> /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/time-0.3.17/src/lib.rs:356:5
    |
356 |     panic!("{}", message)
    |     ^^^^^^^^^^^^^^^^^^^^^
    |
    = help: add `#![feature(const_fmt_arguments_new)]` to the crate attributes to enable
    = note: this error originates in the macro `format_args` which comes from the expansion of the macro `panic` (in Nightly builds, run with -Z macro-backtrace for more info)

so in the meantime, we've decided to drop the processing of arguments. This may cause Kani to not produce compile-time errors in some cases.

Resolved issues:

Resolves #1586

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

This PR will reintroduce two issues that were previously addressed by processing the messages using the format_args macro:

1. Kani's assert macro implementation bypasses some compile-time checks #803
2. Spurious unused variable warnings for variables used in asserts #1556

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.

[celinval]

Didn't we talk about updating the documentation? We should also mention that we don't invoke the fmt() function of the arguments, since they could introduce some bad behavior or side effect.

[celinval]

Can you turn this into fixme test instead?

[zhassan-aws]

We currently don't have a way to add fixme tests that are passing, but should actually fail (see discussion on #1666). That's why I deleted it. I'm not happy about that though, so I'm open to ideas on how we can keep the test in our regressions in a meaningful way.

[celinval]

Honestly, I just rename the test, add a comment and change the expected file to the current output. It won't be part of a fixme suite, but I think it's better than deleting it.

[zhassan-aws]

Didn't we talk about updating the documentation?

Added.

We should also mention that we don't invoke the fmt() function of the arguments, since they could introduce some bad behavior or side effect.

Can you clarify what you mean?

[celinval]

I think we should also call out that we may miss invalid behavior present in the formatting code and that the analysis result can be affected if the format code has any side effect.

[zhassan-aws]

I found a way to make #1918 work fully, so might abandon this PR!

[zhassan-aws]

Closing in favor of #1918.