Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

Add a new workflow that automatically adds the label "Z-BenchCI" to PRs that touch compiler, toolchain, dependencies and driver files that invoke our dependencies.

I also removed the label from the toolchain update job since this workflow will add the label once the PR is created.

Deprecate kani::slice::any_slice in Kani 0.38.0 (and the related AnySlice struct), and remove it in a later version.

Motivation: The Kani library's `slice::any_slice` API is doing more harm than benefit: it is meant to provide a convenient way for users to generate non-deterministic slices, but its current implementation aims to avoid any unsoundness by making sure that for the non-deterministic slice returned by the API, accessing memory beyond the slice length is flagged as an out-of-bounds access (see #1009 for details). However, in practical scenarios, using it ends up causing memory to blowup for CBMC. Given that users may not care about this type of unsoundness, which is only possible through using a pointer dereference inside an unsafe block (see discussion in #2634). Thus, we should leave it to the user to decide the suitable method for generating slices that fits their verification needs. For example, they can use Kani's alternative API, `any_slice_of_array` that extracts a slice of a non-deterministic start and end from a given array.

### Description of changes: 

Expands the contract features introduced in #2655 by completing the
checking with stubbing/replacement capabilities.

### Resolved issues:

Resolves #2621 

### Related RFC: [0009 Function
Contracts](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)

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

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

… also include ZSTs (#2794)

This change considers another case for the code generation of scalar data.
In particular, when the expected type is an ADT, we previously
considered two cases: either there is no field or there is one. But in
cases where the ADT includes a ZST, the ADT will contain multiple
fields: one associated to the scalar data, and other fields associated
to the ZSTs. In those cases, we ended up crashing as in #2680:

```rust
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_161424092592971241517604180463813633314")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_161424092592971241517604180463813633314")
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
```

With the changes in this PR, that's no longer the case.

Resolves #2364 
Resolves #2680

Change the template to be more concise to address the team's concern that the template was too verbose.

The new template is also cleaner since we are now using the PR description as the base for the commit message.
---------
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Upgrade CBMC version to latest (5.93.0).

Resolves #2650

Updated via `cargo update`. No further (manual) updates were suggested
by `cargo outdated --workspace`.

> Please ensure your PR description includes the following:
> 1. A description of how your changes improve Kani.
> 2. Some context on the problem you are solving.
> 3. A list of issues that are resolved by this PR.
> 4. If you had to perform any manual test, please describe them.
>
> **Make sure you remove this list from the final PR description.**

By using the `tar` file as a lock mechanism, we can detect incomplete
setups i.e when both `kani's` working directory and the tar file present
before setup, we can simply use the local bundle to start setup again.

Resolves #1545 

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

Concrete playback seeks to generate unit tests in the original source
file. An intermediate temporary file is used to reduce the risk of
corrupting original source files. Once the temporary file has been
completely written to, it is to be atomically moved to replace the
source file. This can only be done on the same file system.

We now create the temporary file in the same source directory as the
original source file to ensure we are on the same file system. The
implementation uses NamedTempFile from the tempfile crate, which renders
our own tempfile implementation redundant.

Tested on Ubuntu 20.04 with /tmp on a different partition (where our
regression tests would previously fail).

Resolves: #2705

Versions of clippy that come with newer toolchains report a large number
of needless_borrows_for_generic_args. We can address these now so that
we don't have to make these changes as part of a toolchain update.

Source changes required by the following upstream commits:

* rust-lang/rust@5a0a1ff0cd move ConstValue into mir
* rust-lang/rust@ea22adbabd adjust constValue::Slice to work for
arbitrary slice types
* rust-lang/rust@c94410c145 rename mir::Constant -> mir::ConstOperand,
mir::ConstKind -> mir::Const

Fixes: #2784

Next Kani release. Also includes fixes to changelog formatting.