Skip to content

Commit f10e61c

Browse files
remi-delmas-3000Remi Delmas
andauthored
Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 (rust-lang#3199)
- Linter fixes in documentation, - Added the `lld` package for ubuntu builds, - Propagated a `TyCtx` API change. 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: Remi Delmas <delmasrd@amazon.com>
1 parent f6ab6bf commit f10e61c

File tree

21 files changed

+59
-31
lines changed

21 files changed

+59
-31
lines changed

cprover_bindings/src/goto_program/expr.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1055,6 +1055,7 @@ impl Expr {
10551055
/// <https://github.com/rust-lang/rfcs/blob/master/text/1199-simd-infrastructure.md#comparisons>).
10561056
/// The signedness doesn't matter, as the result for each element is
10571057
/// either "all ones" (true) or "all zeros" (false).
1058+
///
10581059
/// For example, one can use `simd_eq` on two `f64x4` vectors and assign the
10591060
/// result to a `u64x4` vector. But it's not possible to assign it to: (1) a
10601061
/// `u64x2` because they don't have the same length; or (2) another `f64x4`
@@ -1665,7 +1666,7 @@ impl Expr {
16651666
continue;
16661667
}
16671668
let name = field.name();
1668-
exprs.insert(name, self.clone().member(&name.to_string(), symbol_table));
1669+
exprs.insert(name, self.clone().member(name.to_string(), symbol_table));
16691670
}
16701671
}
16711672
}

cprover_bindings/src/irep/goto_binary_serde.rs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,9 @@ pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
7878
/// [NumberedIrep] from its unique number.
7979
///
8080
/// In practice:
81-
/// - the forward directon from [IrepKey] to unique numbers is
82-
/// implemented using a `HashMap<IrepKey,usize>`
83-
/// - the inverse direction from unique numbers to [NumberedIrep] is implemented
84-
/// using a `Vec<NumberedIrep>` called the `index` that stores [NumberedIrep]
85-
/// under their unique number.
81+
/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
82+
/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
83+
/// called the `index` that stores [NumberedIrep] under their unique number.
8684
///
8785
/// Earlier we said that an [NumberedIrep] is conceptually a pair formed of
8886
/// an [IrepKey] and its unique number. It is represented using only

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
204204
let body = self.transformer.body(self.tcx, instance);
205205
self.set_current_fn(instance, &body);
206206
debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
207-
self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {
207+
self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
208208
Symbol::function(
209209
fname,
210210
ctx.fn_typ(instance, &body),

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -871,6 +871,7 @@ impl<'tcx> GotocCtx<'tcx> {
871871
/// its primary argument and returns a tuple that contains:
872872
/// * the previous value
873873
/// * a boolean value indicating whether the operation was successful or not
874+
///
874875
/// In a sequential context, the update is always sucessful so we assume the
875876
/// second value to be true.
876877
/// -------------------------
@@ -955,9 +956,10 @@ impl<'tcx> GotocCtx<'tcx> {
955956
/// * Both `src`/`dst` must be valid for reads/writes of `count *
956957
/// size_of::<T>()` bytes (done by calls to `memmove`)
957958
/// * (Exclusive to nonoverlapping copy) The region of memory beginning
958-
/// at `src` with a size of `count * size_of::<T>()` bytes must *not*
959-
/// overlap with the region of memory beginning at `dst` with the same
960-
/// size.
959+
/// at `src` with a size of `count * size_of::<T>()` bytes must *not*
960+
/// overlap with the region of memory beginning at `dst` with the same
961+
/// size.
962+
///
961963
/// In addition, we check that computing `count` in bytes (i.e., the third
962964
/// argument of the copy built-in call) would not overflow.
963965
pub fn codegen_copy(
@@ -1834,7 +1836,7 @@ impl<'tcx> GotocCtx<'tcx> {
18341836
///
18351837
/// TODO: Add a check for the condition:
18361838
/// * `src` must point to a properly initialized value of type `T`
1837-
/// See <https://github.com/model-checking/kani/issues/920> for more details
1839+
/// See <https://github.com/model-checking/kani/issues/920> for more details
18381840
fn codegen_volatile_load(
18391841
&mut self,
18401842
mut fargs: Vec<Expr>,
@@ -1894,6 +1896,7 @@ impl<'tcx> GotocCtx<'tcx> {
18941896
/// Undefined behavior if any of these conditions are violated:
18951897
/// * `dst` must be valid for writes (done by memset writable check)
18961898
/// * `dst` must be properly aligned (done by `align_check` below)
1899+
///
18971900
/// In addition, we check that computing `bytes` (i.e., the third argument
18981901
/// for the `memset` call) would not overflow
18991902
fn codegen_write_bytes(

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -393,7 +393,7 @@ impl<'tcx> GotocCtx<'tcx> {
393393

394394
/// Generate a goto expression for a pointer to a static or thread-local variable.
395395
fn codegen_instance_pointer(&mut self, instance: Instance, is_thread_local: bool) -> Expr {
396-
let sym = self.ensure(&instance.mangled_name(), |ctx, name| {
396+
let sym = self.ensure(instance.mangled_name(), |ctx, name| {
397397
// Rust has a notion of "extern static" variables. These are in an "extern" block,
398398
// and so aren't initialized in the current codegen unit. For example (from std):
399399
// extern "C" {

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -333,8 +333,9 @@ impl<'tcx> GotocCtx<'tcx> {
333333
/// assert!(v.0 == [1, 2]); // refers to the entire array
334334
/// }
335335
/// ```
336-
/// * Note that projection inside SIMD structs may eventually become illegal.
337-
/// See <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609> thread.
336+
///
337+
/// Note that projection inside SIMD structs may eventually become illegal.
338+
/// See thread <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609>.
338339
///
339340
/// Since the goto representation for both is the same, we use the expected type to decide
340341
/// what to return.

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ impl TypeExt for Type {
7373
&& components.iter().any(|x| x.name() == "vtable" && x.typ().is_pointer())
7474
}
7575
Type::StructTag(tag) => {
76-
st.lookup(&tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
76+
st.lookup(tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
7777
}
7878
_ => false,
7979
}
@@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> {
11401140
/// Mapping enums to CBMC types is rather complicated. There are a few cases to consider:
11411141
/// 1. When there is only 0 or 1 variant, this is straightforward as the code shows
11421142
/// 2. When there are more variants, rust might decides to apply the typical encoding which
1143-
/// regard enums as tagged union, or an optimized form, called niche encoding.
1143+
/// regard enums as tagged union, or an optimized form, called niche encoding.
11441144
///
11451145
/// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs.
11461146
/// e.g.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
//! This file is for defining the data-structure itself.
1212
//! 1. Defines `GotocCtx<'tcx>`
1313
//! 2. Provides constructors, getters and setters for the context.
14+
//!
1415
//! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
1516
//! this structure as input.
1617
use super::current_fn::CurrentFnCtx;

kani-compiler/src/kani_compiler.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -110,9 +110,10 @@ struct CrateInfo {
110110
/// compilation. The crate metadata is stored here (even if no codegen was actually performed).
111111
/// - [CompilationStage::CompilationSkipped] no compilation was actually performed.
112112
/// No work needs to be done.
113-
/// - Note: In a scenario where the compilation fails, the compiler will exit immediately,
114-
/// independent on the stage. Any artifact produced shouldn't be used.
115-
/// I.e.:
113+
///
114+
/// Note: In a scenario where the compilation fails, the compiler will exit immediately,
115+
/// independent on the stage. Any artifact produced shouldn't be used. I.e.:
116+
///
116117
/// ```dot
117118
/// graph CompilationStage {
118119
/// Init -> {CodegenNoStubs, CompilationSkipped}

kani-compiler/src/kani_middle/reachability.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,7 +303,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
303303
/// 1. Every function / method / closures that may be directly invoked.
304304
/// 2. Every function / method / closures that may have their address taken.
305305
/// 3. Every method that compose the impl of a trait for a given type when there's a conversion
306-
/// from the type to the trait.
306+
/// from the type to the trait.
307307
/// - I.e.: If we visit the following code:
308308
/// ```
309309
/// let var = MyType::new();
@@ -313,7 +313,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
313313
/// 4. Every Static variable that is referenced in the function or constant used in the function.
314314
/// 5. Drop glue.
315315
/// 6. Static Initialization
316-
/// This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
316+
///
317+
/// Remark: This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
317318
impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
318319
/// Collect the following:
319320
/// - Trait implementations when casting from concrete to dyn Trait.

0 commit comments

Comments
 (0)