diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md
index 7df1a093943f..49a1f0845ecc 100644
--- a/docs/src/rust-feature-support/intrinsics.md
+++ b/docs/src/rust-feature-support/intrinsics.md
@@ -220,6 +220,7 @@ truncf64 | Yes | |
try | No | [#267](https://github.com/model-checking/kani/issues/267) |
type_id | Yes | |
type_name | Yes | |
+typed_swap | Yes | |
unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
unchecked_add | Yes | |
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 8fce4b309820..8a61d46ed518 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -580,6 +580,7 @@ impl<'tcx> GotocCtx<'tcx> {
"truncf64" => codegen_simple_intrinsic!(Trunc),
"type_id" => codegen_intrinsic_const!(),
"type_name" => codegen_intrinsic_const!(),
+ "typed_swap" => self.codegen_swap(fargs, farg_types, loc),
"unaligned_volatile_load" => {
unstable_codegen!(
self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference())
@@ -1943,6 +1944,47 @@ impl<'tcx> GotocCtx<'tcx> {
let zero = Type::size_t().zero();
cast_ptr.rem(align).eq(zero)
}
+
+ /// Swaps the memory contents pointed to by arguments `x` and `y`, respectively, which is
+ /// required for the `typed_swap` intrinsic.
+ ///
+ /// The standard library API requires that `x` and `y` are readable and writable as their
+ /// (common) type (which auto-generated checks for dereferencing will take care of), and the
+ /// memory regions pointed to must be non-overlapping.
+ pub fn codegen_swap(&mut self, mut fargs: Vec<Expr>, farg_types: &[Ty], loc: Location) -> Stmt {
+ // two parameters, and both must be raw pointers with the same base type
+ assert!(fargs.len() == 2);
+ assert!(farg_types[0].kind().is_raw_ptr());
+ assert!(farg_types[0] == farg_types[1]);
+
+ let x = fargs.remove(0);
+ let y = fargs.remove(0);
+
+ // if(same_object(x, y)) {
+ // assert(x + 1 <= y || y + 1 <= x);
+ // assume(x + 1 <= y || y + 1 <= x);
+ // }
+ let one = Expr::int_constant(1, Type::c_int());
+ let non_overlapping =
+ x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone()));
+ let non_overlapping_check = self.codegen_assert_assume(
+ non_overlapping,
+ PropertyClass::SafetyCheck,
+ "memory regions pointed to by `x` and `y` must not overlap",
+ loc,
+ );
+ let non_overlapping_stmt =
+ Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc);
+
+ // T t = *y; *y = *x; *x = t;
+ let deref_y = y.clone().dereference();
+ let (temp_var, assign_to_t) =
+ self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
+ let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
+ let assign_to_x = x.dereference().assign(temp_var, loc);
+
+ Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+ }
}
fn instance_args(instance: &Instance) -> GenericArgs {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 5867448d9973..74622d41ed50 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
.bytes(),
Type::size_t(),
),
- NullOp::UbCheck(_) => Expr::c_false(),
+ NullOp::UbChecks => Expr::c_false(),
}
}
Rvalue::ShallowInitBox(ref operand, content_ty) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 089d871d22b4..b5ccf1a83716 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -570,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
// Note: This is not valid C but CBMC seems to be ok with it.
ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
ty::Str => Type::unsigned_int(8).flexible_array_of(),
- ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
+ ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
ty::FnDef(def_id, args) => {
let instance =
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
@@ -993,7 +993,7 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::Foreign(_)
| ty::Coroutine(..)
| ty::Int(_)
- | ty::RawPtr(_)
+ | ty::RawPtr(_, _)
| ty::Ref(..)
| ty::Tuple(_)
| ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
@@ -1352,10 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> {
// `F16` and `F128` are not yet handled.
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
Primitive::F16 | Primitive::F128 => unimplemented!(),
- Primitive::Pointer(_) => Ty::new_ptr(
- self.tcx,
- ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },
- ),
+ Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
}
}
@@ -1659,7 +1656,7 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
match mir_type.kind() {
ty::Ref(_, pointee_type, _) => Some(*pointee_type),
- ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type),
+ ty::RawPtr(pointee_type, _) => Some(*pointee_type),
_ => None,
}
}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index a25e502aa574..3a6501d544d8 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -23,7 +23,6 @@ use crate::kani_queries::QueryDb;
use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
use cbmc::utils::aggr_tag;
use cbmc::{InternedString, MachineModel};
-use kani_metadata::HarnessMetadata;
use rustc_data_structures::fx::FxHashMap;
use rustc_middle::span_bug;
use rustc_middle::ty::layout::{
@@ -61,8 +60,6 @@ pub struct GotocCtx<'tcx> {
/// map from symbol identifier to string literal
/// TODO: consider making the map from Expr to String instead
pub str_literals: FxHashMap<InternedString, String>,
- pub proof_harnesses: Vec<HarnessMetadata>,
- pub test_harnesses: Vec<HarnessMetadata>,
/// a global counter for generating unique IDs for checks
pub global_checks_count: u64,
/// A map of unsupported constructs that were found while codegen
@@ -98,8 +95,6 @@ impl<'tcx> GotocCtx<'tcx> {
current_fn: None,
type_map: FxHashMap::default(),
str_literals: FxHashMap::default(),
- proof_harnesses: vec![],
- test_harnesses: vec![],
global_checks_count: 0,
unsupported_constructs: FxHashMap::default(),
concurrent_constructs: FxHashMap::default(),
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index ab694ceec614..17992953d5c7 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -46,7 +46,7 @@ pub mod transform;
/// error was found.
pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
let krate = tcx.crate_name(LOCAL_CRATE);
- for item in tcx.hir_crate_items(()).items() {
+ for item in tcx.hir().items() {
let def_id = item.owner_id.def_id.to_def_id();
KaniAttributes::for_item(tcx, def_id).check_attributes();
if tcx.def_kind(def_id) == DefKind::GlobalAsm {
@@ -127,9 +127,11 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
pub struct SourceLocation {
pub filename: String,
pub start_line: usize,
- pub start_col: usize,
+ #[allow(dead_code)]
+ pub start_col: usize, // set, but not currently used in Goto output
pub end_line: usize,
- pub end_col: usize,
+ #[allow(dead_code)]
+ pub end_col: usize, // set, but not currently used in Goto output
}
impl SourceLocation {
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index eb40f7ec673d..456d5425b245 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -25,7 +25,6 @@ use rustc_middle::ty::{TyCtxt, VtblEntry};
use rustc_smir::rustc_internal;
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
-use stable_mir::mir::pretty::pretty_ty;
use stable_mir::mir::{
visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
TerminatorKind,
@@ -434,7 +433,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
`{}`. The function `{}` \
cannot be stubbed by `{}` due to \
generic bounds not being met. Callee: {}",
- pretty_ty(receiver_ty.kind()),
+ receiver_ty,
trait_,
caller,
self.tcx.def_path_str(stub),
@@ -453,10 +452,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
objects in the modifies clause (including return types) \
implement `{}`.\nThis is a strict condition to use \
function contracts as verified stubs.",
- pretty_ty(receiver_ty.kind()),
- trait_,
- callee,
- trait_,
+ receiver_ty, trait_, callee, trait_,
),
);
} else {
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index 32ffb373d767..d14aca3a7c5b 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -173,7 +173,7 @@ impl MutableBody {
let terminator = Terminator { kind, span };
self.split_bb(source, terminator);
}
- CheckType::Panic(..) | CheckType::NoCore => {
+ CheckType::Panic | CheckType::NoCore => {
tcx.sess
.dcx()
.struct_err("Failed to instrument the code. Cannot find `kani::assert`")
@@ -231,7 +231,7 @@ pub enum CheckType {
/// This is used by default when the `kani` crate is available.
Assert(Instance),
/// When the `kani` crate is not available, we have to model the check as an `if { panic!() }`.
- Panic(Instance),
+ Panic,
/// When building non-core crate, such as `rustc-std-workspace-core`, we cannot
/// instrument code, but we can still compile them.
NoCore,
@@ -246,8 +246,8 @@ impl CheckType {
pub fn new(tcx: TyCtxt) -> CheckType {
if let Some(instance) = find_instance(tcx, "KaniAssert") {
CheckType::Assert(instance)
- } else if let Some(instance) = find_instance(tcx, "panic_str") {
- CheckType::Panic(instance)
+ } else if find_instance(tcx, "panic_str").is_some() {
+ CheckType::Panic
} else {
CheckType::NoCore
}
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index a806331401cd..7d0edf6f50e5 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -11,7 +11,7 @@ use std::time::{Duration, Instant};
use crate::args::{OutputFormat, VerificationArgs};
use crate::cbmc_output_parser::{
- extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput,
+ extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput,
};
use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
use crate::session::KaniSession;
@@ -45,9 +45,6 @@ pub struct VerificationResult {
pub status: VerificationStatus,
/// The compact representation for failed properties
pub failed_properties: FailedProperties,
- /// The parsed output, message by message, of CBMC. However, the `Result` message has been
- /// removed and is available in `results` instead.
- pub messages: Option<Vec<ParserItem>>,
/// The `Result` properties in detail or the exit_status of CBMC.
/// Note: CBMC process exit status is only potentially useful if `status` is `Failure`.
/// Kani will see CBMC report "failure" that's actually success (interpreting "failed"
@@ -254,7 +251,7 @@ impl VerificationResult {
start_time: Instant,
) -> VerificationResult {
let runtime = start_time.elapsed();
- let (items, results) = extract_results(output.processed_items);
+ let (_, results) = extract_results(output.processed_items);
if let Some(results) = results {
let (status, failed_properties) =
@@ -262,7 +259,6 @@ impl VerificationResult {
VerificationResult {
status,
failed_properties,
- messages: Some(items),
results: Ok(results),
runtime,
generated_concrete_test: false,
@@ -272,7 +268,6 @@ impl VerificationResult {
VerificationResult {
status: VerificationStatus::Failure,
failed_properties: FailedProperties::Other,
- messages: Some(items),
results: Err(output.process_status),
runtime,
generated_concrete_test: false,
@@ -284,7 +279,6 @@ impl VerificationResult {
VerificationResult {
status: VerificationStatus::Success,
failed_properties: FailedProperties::None,
- messages: None,
results: Ok(vec![]),
runtime: Duration::from_secs(0),
generated_concrete_test: false,
@@ -295,7 +289,6 @@ impl VerificationResult {
VerificationResult {
status: VerificationStatus::Failure,
failed_properties: FailedProperties::Other,
- messages: None,
// on failure, exit codes in theory might be used,
// but `mock_failure` should never be used in a context where they will,
// so again use something weird:
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 1bb353d7d4c0..127f98beab56 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -287,9 +287,7 @@ fn filepath(file: String) -> String {
#[derive(Clone, Debug, Deserialize)]
#[serde(rename_all = "camelCase")]
pub struct TraceItem {
- pub thread: u32,
pub step_type: String,
- pub hidden: bool,
pub lhs: Option<String>,
pub source_location: Option<SourceLocation>,
pub value: Option<TraceValue>,
@@ -301,7 +299,6 @@ pub struct TraceItem {
/// The fields included right now are relevant to primitive types.
#[derive(Clone, Debug, Deserialize)]
pub struct TraceValue {
- pub name: String,
pub binary: Option<String>,
pub data: Option<TraceData>,
pub width: Option<u32>,
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index 53c3a92dd94c..dbd2fb9e03d2 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/kani-driver/src/concrete_playback/test_generator.rs
@@ -588,9 +588,7 @@ mod tests {
line: None,
},
trace: Some(vec![TraceItem {
- thread: 0,
step_type: "assignment".to_string(),
- hidden: false,
lhs: Some("goto_symex$$return_value".to_string()),
source_location: Some(SourceLocation {
column: None,
@@ -599,7 +597,6 @@ mod tests {
line: None,
}),
value: Some(TraceValue {
- name: "".to_string(),
binary: Some("0000001100000001".to_string()),
data: Some(TraceData::NonBool("385".to_string())),
width: Some(16),
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index d08e3a84f0ad..eee073e29a89 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-03-21"
+channel = "nightly-2024-03-29"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs
new file mode 100644
index 000000000000..4279bb713ece
--- /dev/null
+++ b/tests/kani/Intrinsics/typed_swap.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `typed_swap` yields the expected results.
+// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap.html
+
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
+#[kani::proof]
+fn test_typed_swap_u32() {
+ let mut a: u32 = kani::any();
+ let a_before = a;
+ let mut b: u32 = kani::any();
+ let b_before = b;
+ unsafe {
+ std::intrinsics::typed_swap(&mut a, &mut b);
+ }
+ assert!(b == a_before);
+ assert!(a == b_before);
+}