Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Load reduction #39

Closed
wants to merge 25 commits into from
Closed
Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
8398771
Update cargo dependencies (#3776)
tautschnig Dec 13, 2024
c1c5b46
Automatic toolchain upgrade to nightly-2024-12-14 (#3780)
github-actions[bot] Dec 14, 2024
86f5366
Automatic cargo update to 2024-12-16 (#3782)
github-actions[bot] Dec 16, 2024
68f1adb
Bump Kani version to 0.57.0 (#3777)
tautschnig Dec 16, 2024
d253bda
Bump tests/perf/s2n-quic from `e4a2365` to `0b3f892` (#3785)
dependabot[bot] Dec 16, 2024
e6f6d7d
Upgrade toolchain to 2024-12-15 (#3784)
carolynzech Dec 16, 2024
9fd39c0
Fix toolchain version in 0.57.0 CHANGELOG (#3786)
tautschnig Dec 16, 2024
3f5f8e8
Package Docker release step: ensure compiler is installed (#3789)
tautschnig Dec 17, 2024
b7ae080
Improve `--jobs` UI (#3790)
carolynzech Dec 18, 2024
7a08474
Update kissat to v4.0.1 (#3791)
remi-delmas-3000 Dec 20, 2024
4251ae8
Automatic cargo update to 2024-12-23 (#3792)
github-actions[bot] Dec 23, 2024
f212ce5
Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` (#3793)
dependabot[bot] Dec 23, 2024
33b74e0
Upgrade toolchain to nightly-2024-12-18 (#3794)
zhassan-aws Dec 26, 2024
a3f28bb
replace ClosureType with ContractMode (to be consistent with kani-com…
carolynzech Dec 28, 2024
b18d35a
move split_for_remembers to shared.rs; remove unused variants
carolynzech Dec 28, 2024
11f3e04
add ContractMode for assertions to library/kani_macros
carolynzech Dec 29, 2024
1f135c9
add option to use Assert ContractMode
carolynzech Dec 29, 2024
7913e3c
Automatic cargo update to 2024-12-30 (#3800)
github-actions[bot] Dec 30, 2024
d4a8fc0
tests
carolynzech Dec 30, 2024
979ecb0
documentation
carolynzech Dec 30, 2024
ba4a108
tweak comment
carolynzech Dec 30, 2024
e8c9311
doc nits
carolynzech Dec 30, 2024
f4f5816
Merge branch 'main' of github.com:model-checking/kani into contracts-…
carolynzech Dec 31, 2024
c4e2090
try splitting & simplifying tests to reduce runner load
carolynzech Dec 31, 2024
15ee0a6
format
carolynzech Dec 31, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 27 additions & 27 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -225,9 +225,9 @@ dependencies = [

[[package]]
name = "cc"
version = "1.2.5"
version = "1.2.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c31a0499c1dc64f458ad13872de75c0eb7e3fdb0e67964610c914b034fc5956e"
checksum = "8d6dbb628b8f8555f86d0323c2eb39e3ec81901f4b83e091db8a6a76d316a333"
dependencies = [
"shlex",
]
Expand Down Expand Up @@ -307,7 +307,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -627,9 +627,9 @@ checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"

[[package]]
name = "glob"
version = "0.3.1"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
checksum = "a8d1add55171497b4705a648c6b583acafb01d58050a51727785f0b2c8e0a2b2"

[[package]]
name = "graph-cycles"
Expand Down Expand Up @@ -785,7 +785,7 @@ dependencies = [
"shell-words",
"strum",
"strum_macros",
"syn 2.0.91",
"syn 2.0.93",
"tracing",
"tracing-subscriber",
"tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
Expand Down Expand Up @@ -860,7 +860,7 @@ dependencies = [
"proc-macro-error2",
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -924,7 +924,7 @@ version = "0.1.0"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -1252,7 +1252,7 @@ dependencies = [
"proc-macro-error-attr2",
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand All @@ -1275,9 +1275,9 @@ dependencies = [

[[package]]
name = "quote"
version = "1.0.37"
version = "1.0.38"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc"
dependencies = [
"proc-macro2",
]
Expand Down Expand Up @@ -1425,9 +1425,9 @@ dependencies = [

[[package]]
name = "rustversion"
version = "1.0.18"
version = "1.0.19"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248"
checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4"

[[package]]
name = "ryu"
Expand Down Expand Up @@ -1473,9 +1473,9 @@ dependencies = [

[[package]]
name = "serde"
version = "1.0.216"
version = "1.0.217"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e"
checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70"
dependencies = [
"serde_derive",
]
Expand All @@ -1491,13 +1491,13 @@ dependencies = [

[[package]]
name = "serde_derive"
version = "1.0.216"
version = "1.0.217"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e"
checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -1648,7 +1648,7 @@ dependencies = [
"proc-macro2",
"quote",
"rustversion",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand All @@ -1664,9 +1664,9 @@ dependencies = [

[[package]]
name = "syn"
version = "2.0.91"
version = "2.0.93"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d53cbcb5a243bd33b7858b1d7f4aca2153490815872d86d955d6ea29f743c035"
checksum = "9c786062daee0d6db1132800e623df74274a0a87322d8e183338e01b3d98d058"
dependencies = [
"proc-macro2",
"quote",
Expand Down Expand Up @@ -1724,7 +1724,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand All @@ -1735,7 +1735,7 @@ checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -1858,7 +1858,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]

[[package]]
Expand Down Expand Up @@ -1940,9 +1940,9 @@ dependencies = [

[[package]]
name = "tree-sitter"
version = "0.24.5"
version = "0.24.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8ac95b18f0f727aaaa012bd5179a1916706ee3ed071920fdbda738750b0c0bf5"
checksum = "5f2434c86ba59ed15af56039cc5bf1acf8ba76ce301e32ef08827388ef285ec5"
dependencies = [
"cc",
"regex",
Expand Down Expand Up @@ -2216,5 +2216,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.91",
"syn 2.0.93",
]
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::Location;
use lazy_static::lazy_static;
use rustc_ast::Attribute;
use rustc_hir::Attribute;
use rustc_smir::rustc_internal;
use rustc_span::Span;
use stable_mir::ty::Span as SpanStable;
Expand Down
45 changes: 12 additions & 33 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,9 @@ use std::collections::{BTreeMap, HashSet};

use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
use quote::ToTokens;
use rustc_ast::{
AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr,
};
use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr};
use rustc_errors::ErrorGuaranteed;
use rustc_hir::{def::DefKind, def_id::DefId};
use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId};
use rustc_middle::ty::{Instance, TyCtxt, TyKind};
use rustc_session::Session;
use rustc_smir::rustc_internal;
Expand Down Expand Up @@ -684,31 +682,12 @@ fn expect_key_string_value(
attr: &Attribute,
) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
let span = attr.span;
let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else {
let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else {
return Err(sess
.dcx()
.span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
};
let maybe_str = match value {
AttrArgsEq::Ast(expr) => {
if let ExprKind::Lit(tok) = expr.kind {
match LitKind::from_token_lit(tok) {
Ok(l) => l.str(),
Err(err) => {
return Err(sess.dcx().span_err(
span,
format!("Invalid string literal on right hand side of `=` {err:?}"),
));
}
}
} else {
return Err(sess
.dcx()
.span_err(span, "Expected literal string as right hand side of `=`"));
}
}
AttrArgsEq::Hir(lit) => lit.kind.str(),
};
let maybe_str = expr.kind.str();
if let Some(str) = maybe_str {
Ok(str)
} else {
Expand Down Expand Up @@ -852,7 +831,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
attributes
.iter()
.filter_map(|attr| {
let paths = parse_paths(attr).unwrap_or_else(|_| {
let paths = parse_paths(tcx, attr).unwrap_or_else(|_| {
tcx.dcx().span_err(
attr.span,
format!(
Expand Down Expand Up @@ -963,8 +942,8 @@ fn parse_integer(attr: &Attribute) -> Option<u128> {
/// Extracts a vector with the path arguments of an attribute.
///
/// Emits an error if it couldn't convert any of the arguments and return an empty vector.
fn parse_paths(attr: &Attribute) -> Result<Vec<TypePath>, syn::Error> {
let syn_attr = syn_attr(attr);
fn parse_paths(tcx: TyCtxt, attr: &Attribute) -> Result<Vec<TypePath>, syn::Error> {
let syn_attr = syn_attr(tcx, attr);
let parser = Punctuated::<TypePath, syn::Token![,]>::parse_terminated;
let paths = syn_attr.parse_args_with(parser)?;
Ok(paths.into_iter().collect())
Expand Down Expand Up @@ -1001,11 +980,11 @@ fn parse_str_value(attr: &Attribute) -> Option<String> {
fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
match &attr.kind {
AttrKind::Normal(normal) => {
let segments = &normal.item.path.segments;
if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
let segments = &normal.path.segments;
if (!segments.is_empty()) && segments[0].as_str() == "kanitool" {
let ident_str = segments[1..]
.iter()
.map(|segment| segment.ident.as_str())
.map(|segment| segment.as_str())
.intersperse("::")
.collect::<String>();
KaniAttributeKind::try_from(ident_str.as_str())
Expand All @@ -1025,8 +1004,8 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
/// Parse an attribute using `syn`.
///
/// This provides a user-friendly interface to manipulate than the internal compiler AST.
fn syn_attr(attr: &Attribute) -> syn::Attribute {
let attr_str = rustc_ast_pretty::pprust::attribute_to_string(attr);
fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute {
let attr_str = rustc_hir_pretty::attribute_to_string(&tcx, attr);
let parser = syn::Attribute::parse_outer;
parser.parse_str(&attr_str).unwrap().pop().unwrap()
}
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ extern crate rustc_data_structures;
extern crate rustc_driver;
extern crate rustc_errors;
extern crate rustc_hir;
extern crate rustc_hir_pretty;
extern crate rustc_index;
extern crate rustc_interface;
extern crate rustc_metadata;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-12-15"
channel = "nightly-2024-12-18"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
22 changes: 11 additions & 11 deletions tests/expected/uninit/delayed-ub/expected
Original file line number Diff line number Diff line change
@@ -1,44 +1,44 @@
delayed_ub_trigger_copy.assertion.1\
delayed_ub_trigger_copy.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\

delayed_ub_slices.assertion.4\
delayed_ub_slices.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"

delayed_ub_structs.assertion.2\
delayed_ub_structs.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`"

delayed_ub_double_copy.assertion.1\
delayed_ub_double_copy.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\

delayed_ub_copy.assertion.1\
delayed_ub_copy.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub_closure_capture_laundered.assertion.2\
delayed_ub_closure_capture_laundered.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub_closure_laundered.assertion.2\
delayed_ub_closure_laundered.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub_laundered.assertion.2\
delayed_ub_laundered.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub_static.assertion.4\
delayed_ub_static.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub_transmute.assertion.2\
delayed_ub_transmute.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

delayed_ub.assertion.2\
delayed_ub.assertion.\
- Status: FAILURE\
- Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"

Expand Down